Commits

Author Commit Message Labels Comments Date
Arlen Cox
New Makefile that works on Mavericks with OCaml 4.01 and is more standard anyway
Arlen Cox
Fixing missing routines. Some parsing routines appear to have been removed from Z3 and they were still in the OCaml bindings.
Arlen Cox
Merge branch 'master' of https://git01.codeplex.com/z3 Conflicts: Makefile.in configure.in
Leonardo de Moura
Display version number using new format Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
New API for adding 'tracked assertions'. Added wrappers for creating existential and universal quantifiers in the C++ API fronted. Added new examples for the C++ API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Nikolaj Bjorner
add missing check for difference logic fragment for clause heads Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Arlen Cox
Fixing documentation
Arlen Cox
ocamlfind library support is now complete! hooray!
Arlen Cox
Modified build files to allow compilation on Mac OS X 10.8 out of the box. It makes use of clang++ by default (since C++11 support is required) and only uses OpenMP if it is available. Since clang does not support OpenMP, this is disabled on Mac OS X.
Leonardo de Moura
cleaned exampled Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
new example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
fixed bug detected in regression tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
Fixed bug reported by Heizmann at codeplex Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
fixed bugs found in regression tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
fixed problem with Python 2.5 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Nikolaj Bjorner
fix model completion bug in PDR, addhoc handling of reals for arithmetic realizers Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Leonardo de Moura
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
Leonardo de Moura
resurrected test/quant_elim.cpp Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Nikolaj Bjorner
set model completion to force value computation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
update slicing to fix unbound variables. test datatype realizer Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
Nikolaj Bjorner
fix if-lifting, added light-weight FM to qe_lite Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Leonardo de Moura
minor fix for ramdisk build Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
fixed some warnings reported by clang++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
Merge branch 'solver_na2as' into unstable
Leonardo de Moura
cleanning solver initialization, and fixing named assertion support Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
removed dead files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
added support for named assertions
Leonardo de Moura
new qe example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
fixed bug in solver_na2as Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
  1. Prev
  2. Next