search

gmalecha / coq-smt-check

Invoke SMT solvers from Coq to check obligations
MIT License
10 stars 3 forks source link

Support custom types #2

Open wangjwchn opened 7 years ago

wangjwchn commented 7 years ago

Hi @gmalecha , Suppose I have a user-defined integer library as shown bellow(ignored the semantics).

Require Import ZArith.
Parameter int64: Type.
Parameter repr: Z -> int64.
Parameter and: int64 -> int64 -> int64.
Parameter or: int64 -> int64 -> int64.
...

I want to map this library to Bitvectors in Z3. How can I make the coq-smt-check support this library? I tried, but it looks complicated. The main problem is, the int64 is constructed by Z (repr: Z -> int64), and I want to map int64 to BitVec 64 directly. For example, I want to map Int64.repr 5 into #x5. I can get something like (+ 1 (* (+ 1 1) (+ 1 1))) by using coq-smt-check or coq-plugin-utils. If we deal with Int or Real in Z3, it is ok to pass this syntax to Z3, like coq-smt-check did. But Z3 doesn't allow such syntax when build a BitVec. How can I get the result5 in hexadecimal format so that I can add the prefix #x, then pass it to Z3?

gmalecha commented 7 years ago

I don't have a way right now to set up custom types. Perhaps we could do it by having a way to map Coq constr into strings on the SMT side of things. You'd need to do something like:

SMT Add Symbol and "and".
SMT Add Symbol or "or".

I'm not sure that I know a generic way to get the hex formatting though. You could always special-case it.