fixed some bugs, add more types.

gmalecha / coq-smt-check

Invoke SMT solvers from Coq to check obligations

MIT License

10 stars 3 forks source link

fixed some bugs, add more types. #5

Closed wangjwchn closed 7 years ago

wangjwchn commented 7 years ago

This PR made the following modifications:

Fix the bug that the checker will crash when there is a ' in the variable name.
Display the input of Z3 for debugging
Add more types:
- nat
- Z
- bool
- int64 Simples can be found in the file test-suite/Test.v. (Some operations of them have not been translated yet, the work is in progress now)

gmalecha commented 7 years ago

I noticed that a lot of what you did was build ocaml representations of the terms. Do you think we could do something like:

| Fn of string * expr list

And then support a way to map Gallina functions to strings? That would allow us to avoid the coupling between this code and libraries and make it possible for other people to extend the system without writing Ocaml code.

wangjwchn commented 7 years ago

I think I may need to clear up the commit then submit the PR.