3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Commit graph

388 commits

Author SHA1 Message Date
Leonardo de Moura 99b7f7509d bump version number in unstable branch
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-11 10:50:24 -08:00
Leonardo de Moura a6db55d21f Display version number using new format
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-10 19:03:16 -08:00
Leonardo de Moura caced62f40 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>
2012-11-10 15:54:31 -08:00
Nikolaj Bjorner 108bbb0597 add missing check for difference logic fragment for clause heads
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-10 11:50:17 +01:00
Leonardo de Moura a5ceff98ea cleaned exampled
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-08 07:11:22 -08:00
Leonardo de Moura 1cf8d61def new example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-08 07:00:27 -08:00
Leonardo de Moura 73a13f209b fixed bug detected in regression tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-07 10:46:00 -08:00
Leonardo de Moura c5b91aef68 Fixed bug reported by Heizmann at codeplex
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-07 07:52:07 -08:00
Leonardo de Moura 8d6a091083 fixed bugs found in regression tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-07 07:36:40 -08:00
Leonardo de Moura c3a0a29c4f fixed problem with Python 2.5
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-07 05:55:41 -08:00
Nikolaj Bjorner cec851440e fix model completion bug in PDR, addhoc handling of reals for arithmetic realizers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-06 15:38:07 +02:00
Leonardo de Moura 2c66afadd6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-04 12:49:58 -08:00
Leonardo de Moura 10b95de82e resurrected test/quant_elim.cpp
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-04 12:49:33 -08:00
Nikolaj Bjorner 5ef505c357 set model completion to force value computation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-04 14:22:56 +02:00
Nikolaj Bjorner 37a13b1d09 update slicing to fix unbound variables. test datatype realizer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-04 14:15:24 +02:00
Nikolaj Bjorner bfbdad3ce6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-04 08:40:23 +02:00
Nikolaj Bjorner 927dc2e490 fix if-lifting, added light-weight FM to qe_lite
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-04 08:40:16 +02:00
Leonardo de Moura 6580a83594 minor fix for ramdisk build
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-02 21:16:52 -07:00
Leonardo de Moura c1587dc37d fixed some warnings reported by clang++
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-02 17:28:27 -07:00
Leonardo de Moura ed52dce9b0 Merge branch 'solver_na2as' into unstable 2012-11-02 16:35:23 -07:00
Leonardo de Moura b70687acc9 cleanning solver initialization, and fixing named assertion support
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-02 16:35:08 -07:00
Leonardo de Moura 181bdb6815 removed dead files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-02 14:18:12 -07:00
Leonardo de Moura e2f6a65aa2 added support for named assertions 2012-11-02 14:00:43 -07:00
Leonardo de Moura e08c569d8d new qe example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-02 12:04:02 -07:00
Leonardo de Moura e1eb3ee8ee fixed bug in solver_na2as
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-02 11:36:59 -07:00
Leonardo de Moura 33c165490c fixed solver_na2as
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-02 09:43:07 -07:00
Leonardo de Moura d545f187f8 working on named assertions support
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-02 08:28:34 -07:00
Leonardo de Moura 230382d4c9 default_solver --> smt_solver
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 21:52:27 -07:00
Leonardo de Moura cadd35bf7a checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 21:44:35 -07:00
Leonardo de Moura adb6d05805 fixed typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 14:43:02 -07:00
Leonardo de Moura 398f1b1de1 moving assertion_stack to mcsat branch
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 13:29:09 -07:00
Leonardo de Moura c096fb534b checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 13:28:10 -07:00
Nikolaj Bjorner 4f2b7049ab Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-01 13:06:16 -07:00
Nikolaj Bjorner 1c17e40fe5 optmizing DL
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-01 13:06:10 -07:00
Leonardo de Moura ef0ee9a0c4 code reorg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 12:47:24 -07:00
Leonardo de Moura 26ffee95fc resurrecting assertion stack
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 12:37:24 -07:00
Leonardo de Moura c9722a1313 removing dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 12:21:14 -07:00
Leonardo de Moura f1c9c9b7cd resurrecting assertion_stack
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 12:15:45 -07:00
Leonardo de Moura 4c98b567e1 old_params ==> front_end_params. Isolated abstract solver interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 11:28:14 -07:00
Leonardo de Moura 62cc752fb6 Fixed bug reported by Arie Gurfinkel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 10:28:26 -07:00
Leonardo de Moura 7cdf5e493b moved smt tactic to smt folder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 08:48:54 -07:00
Leonardo de Moura 81df5ca96f Moved dead code to dead branch
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-01 08:40:20 -07:00
Nikolaj Bjorner 8f7494cb04 disable buggy code in slicer: it removes conjuncts for non-sliced variables. It should use the same criteria as the slice recognizer. reported by Arie Gurfinkel
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-10-31 20:29:28 -07:00
Leonardo de Moura e2f3f9abd7 removed dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-31 14:58:21 -07:00
Leonardo de Moura 9072d80995 fixed typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-31 14:36:18 -07:00
Leonardo de Moura 6d8b8a762c Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-10-31 14:22:00 -07:00
Leonardo de Moura 1ebfcfc2cb removing fat
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-31 14:21:22 -07:00
Nikolaj Bjorner 0b8e77aa57 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-10-31 13:35:45 -07:00
Nikolaj Bjorner 9748b6ed11 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-10-31 13:25:42 -07:00
Leonardo de Moura a274cac2a0 bindings --> api; and moved nlsat/sat/subpaving tactics 2012-10-31 13:25:36 -07:00