gmalecha / coq-smt-check Goto Github PK

Hi @gmalecha ,
When I try to modify the coq-smt-check to add some new types, it is hard to debug without seeing the input of Z3. The best I can do is to write it into str_formatter, like this:

Format.fprintf Format.str_formatter "Z3 input\n" ;
RealInstance.write_instance Format.str_formatter inst;
debug (fun _ -> Pp.(str (Format.flush_str_formatter ())));

It can solve my problem to a certain degree, but it 's a temporary solution.
Is there a better way to deal with this?

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?

Are you going to update it for Coq8.6?

Since you can export real number expressions from Coq, maybe it is possible to call Polya, too? @avigad or @rlewis1988 will know more about this.