mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
3760 commits 23 branches 48 tags 157 MiB
Commit graph

548 commits

Author SHA1 Message Date
Nikolaj Bjorner
d815cf9b7b fix bug in optimization where a variable is updated twice 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-07 16:01:48 -07:00
Nikolaj Bjorner
e81dc5a0a0 fixes issue #143 and memory leak on theory plugin setup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-26 09:03:56 +02:00
Nikolaj Bjorner
108d76270e set undo trail after set-watches to avoid crash during exception handling (the relevancy trail is scoped so ends up traversing the trail if allocating the watch throws an exception). Fixes crash.smt in issue #56 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 19:18:03 +02:00
Nikolaj Bjorner
d9522cfd07 fix mixed integer/real bugs for maximization exposed by non-termination in slow.smt. partially fixes issue #56 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 12:05:19 +02:00
Nikolaj Bjorner
d32e4a9476 exposing facility to extract dependent clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-22 23:36:52 +02:00
Nikolaj Bjorner
b08ccc7816 added missing Copyright forms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:54:02 -07:00
Nikolaj Bjorner
9734407cde disable throttle on unbounded objectives in shared theories. It may violate an interface equality, to fix issue #120 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 11:14:59 -07:00
Nikolaj Bjorner
2d409c6042 revert bug introduced to avoid stack overflow in arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-29 14:32:24 -07:00
Nikolaj Bjorner
f8e2fa0337 fixes issue #93 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-29 11:11:13 -07:00
Nikolaj Bjorner
5acefceada Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-29 08:58:31 -07:00
Christoph M. Wintersteiger
f2f6fc1994 Added QF_BVFP logic alias for QF_FPBV 2015-05-29 13:58:23 +01:00
Nikolaj Bjorner
ed7e0e11a8 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-28 20:55:13 -07:00
Nikolaj Bjorner
534271db08 adding parameters to gomory cut axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 14:48:51 -07:00
Nikolaj Bjorner
e483efd3f4 fixes to Euclidean solver, fixes #100 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 09:21:20 -07:00
Nikolaj Bjorner
cb00555635 local changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 09:18:52 -07:00
Christoph M. Wintersteiger
9912b2cd67 Re-enabled the smt.arith.greatest_error_pivot parameter. 2015-05-23 18:01:00 +01:00
Nuno Lopes
c577ab361b fix assorted undefined behaviors caught by clang 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-23 11:45:12 +01:00
Ken McMillan
4546c3e7bb merge 2015-05-22 11:01:55 -07:00
Ken McMillan
13a3bdd7a3 fix proof for extended GCD rule 2015-05-22 10:28:19 -07:00
Nikolaj Bjorner
c969d78042 throw exception instead of debug mode assertion in ast_manager on malformed input 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-21 15:07:01 -07:00
Nikolaj Bjorner
9d0e3abd24 use static features to set hidden configuration parameters on small integers and int vs. real 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-20 10:41:41 -07:00
Nikolaj Bjorner
92cfc242d2 cast variables to avoid compiler warning on signed/unsigned comparison 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-19 08:15:59 -07:00
Nikolaj Bjorner
203c5015c8 fix debian amd64 warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-18 15:17:21 -07:00
Nikolaj Bjorner
e8811748d3 fix regressions in nl/smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-16 19:08:37 +01:00
Nikolaj Bjorner
64bd62b17e fix gcc compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-16 11:56:04 +01:00
Nikolaj Bjorner
839e3fbb7c add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-09 19:40:34 -07:00
Nikolaj Bjorner
a0f0b53686 fixes to #52, #53 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-28 14:48:59 -07:00
Nikolaj Bjorner
ffc3a36dcb checked ite-expressions as shared for bounds detection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-23 19:59:33 +02:00
Nikolaj Bjorner
3ba2e712b2 merge with unstable branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-12 15:54:52 -07:00
Nikolaj Bjorner
26c53d055a Merge branch 'opt' of https://github.com/Z3Prover/z3 into opt 2015-04-02 15:22:41 -07:00
Nikolaj Bjorner
dca0fb77c2 use same defaults as unstable branch for difference logic configuration 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-02 15:22:32 -07:00
Nikolaj Bjorner
d01c3491a6 simplify with caching, but without expanding number of asserted formulas. Bug reported by Heizmann, codeplex issue 197 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-02 10:28:30 -07:00
Nikolaj Bjorner
6b995c4077 disable wrong fix for simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-02 02:56:40 -07:00
Nikolaj Bjorner
52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
Nikolaj Bjorner
10cdbb881f enable canceling simplex on interrupt, investigating PDR inconsistency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-25 12:13:57 -07:00
Christoph M. Wintersteiger
b76d588c28 Renamed the soft_timeout option to just timeout. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-21 16:10:30 +00:00
Nikolaj Bjorner
4145b92136 use of regions for AUX lemmas from pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-11 11:52:07 -07:00
Nikolaj Bjorner
f47cc70236 use of regions for AUX lemmas from pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-11 11:48:52 -07:00
Nikolaj Bjorner
51267f3aba take into account that bound from optimization may create atom that clashes with inequality bound from term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-11 00:26:49 -07:00
nikolajbjorner
fe6af38d97 debugging assertion violation 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
 2015-03-10 20:57:01 -07:00
Christoph M. Wintersteiger
55ca6ce44b Resurrected the dack* options. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 19:15:22 +00:00
Nuno Lopes
71d31c1267 minor optimization to reset() methods in smt::ketnel and smt::quantifier_manager 
Signed-off-by: Nuno Lopes <a-nlopes@MSRC-4051274.europe.corp.microsoft.com>
 2015-02-27 11:48:14 +00:00
Christoph M. Wintersteiger
a51aed0133 Fixed bug in constant propagation 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-24 21:26:25 +00:00
Nuno Lopes
5676fbbc9e compiler love: make a few symbols static and avoid unneeded relocations 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-22 11:13:51 +00:00
Nikolaj Bjorner
49483fdc28 take conflicts during restart into account. reported by Arie Gurfinkel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-02-21 02:08:00 -08:00
Nikolaj Bjorner
911ffc370a separate MaxSMT functionality to enable using this independently (and incrementally) of overall context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-02-16 09:11:28 +01:00
Nuno Lopes
d3fb5f2a4c fix misc compiler warnings 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-15 11:53:24 +00:00
Christoph M. Wintersteiger
3a8a62fc4c Added array index/element sort detection to static_features 2015-02-09 13:41:45 +00:00
Christoph M. Wintersteiger
d7a37f246c More bugfixes for smt setup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-08 16:59:46 +00:00
Christoph M. Wintersteiger
4792c5fb7c Fixed bugs in static features and smt setup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-08 16:53:08 +00:00