mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
7046 commits 46 branches 52 tags 178 MiB
Commit graph

1498 commits

Author SHA1 Message Date
Murphy Berzish
5fe129b571 use mk_ismt2_pp() instead of mk_bounded_pp() 2015-09-28 02:09:35 -04:00
Murphy Berzish
87b5765e3d clean up traces and make them much easier to read 2015-09-28 02:04:35 -04:00
Murphy Berzish
7da3854a8b really lousy model-building, WIP 2015-09-28 01:56:13 -04:00
Murphy Berzish
02cb329ca5 defer equalities uncovered during init_search 2015-09-27 23:24:41 -04:00
Murphy Berzish
86e6087718 starting solve_concat_eq_str(); currently there is an unsoundness bug 2015-09-27 21:30:45 -04:00
Murphy Berzish
6481fe941a instantiate string-eq length-eq axiom 2015-09-27 17:48:53 -04:00
Murphy Berzish
114b51dec8 only handle equalities in assignments during init_search_eh 2015-09-27 17:26:52 -04:00
Murphy Berzish
91e9cf272a assert string axiom 2 2015-09-27 00:12:04 -04:00
Murphy Berzish
4085db9990 recursive descent through all assertions to discover all String terms 
set up axioms on these terms to be asserted during propagation
 2015-09-26 23:35:23 -04:00
Murphy Berzish
f6affe64d0 deferred addition of basic string axioms 
no longer crashes the solver and got our first correct UNSAT!
 2015-09-26 21:02:56 -04:00
Murphy Berzish
4d5a0ea53f WIP add axioms 2015-09-26 18:51:02 -04:00
Christoph M. Wintersteiger
076e680433 Improved UF suppport in fpa2bv_converter. 2015-09-25 17:28:31 +01:00
Christoph M. Wintersteiger
05d9e188f8 Reactivated smt.max_conflicts option. 
Partially fixes #216.
 2015-09-17 14:08:04 +01:00
Christoph M. Wintersteiger
f3441c6a9b tabs and indentation 2015-09-17 13:25:22 +01:00
Nuno Lopes
45cfb80d14 tentatively fix another issue with char signedness as reported in issue #210 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-09-10 09:01:44 +01:00
Nikolaj Bjorner
d7da64f946 fix crash with incorrect bound computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-08 16:27:57 -07:00
Nikolaj Bjorner
73a8f9960f fix regressions exposed in Internal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-07 20:17:46 -07:00
Murphy Berzish
799fd07c85 optimization: return integer consts for strlen() over constant strings 2015-09-07 19:51:52 -04:00
Murphy Berzish
9b04f1570f instantiate length axiom for concatenation 2015-09-07 19:40:25 -04:00
Murphy Berzish
dc86385e7f add Length function to theory of strings 2015-09-07 16:13:48 -04:00
Murphy Berzish
8137e022e3 load str decl plugin; recognize String sorted constants 2015-09-06 20:53:08 -04:00
Nikolaj Bjorner
963981b3a6 fix memory alias bug and non-termination bug exposed by issue #184 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-31 14:45:10 -07:00
Nikolaj Bjorner
0ed38ed59b add option for using corr set and use partial cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-30 14:48:24 -07:00
Nikolaj Bjorner
7f219e84de check cancellation flag in min/max. Fixes issue #206 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-29 15:51:58 -07:00
Christoph M. Wintersteiger
f4c8463619 Bugfix for FP theory 
Fixes #207
 2015-08-28 15:41:03 +01:00
Christoph M. Wintersteiger
81eecafa66 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-27 18:17:38 +01:00
Christoph M. Wintersteiger
081ba9093a Bugfix for FP theory; handling of UFs and interpreted functions from other theories. 2015-08-27 18:17:26 +01:00
Nikolaj Bjorner
d00d6a3506 enable Boolean propagation in AUFBV to fix inefficiency (bit-blasting destroys simplifications that are possible by simple Boolean propagation). Fixes issue #194 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-25 13:21:33 -07:00
Nikolaj Bjorner
68b441770e Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-25 11:09:35 -07:00
Nikolaj Bjorner
7639eff29b retain default configuration between calls to SMT tactic so that values are not overwritten between calls to smt-setup. Fixes bug #196 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-25 11:09:10 -07:00
Nikolaj Bjorner
ee5f1ad6b6 fix issue #203: domain range was one too large 
Signed-off-by: unknown <nbjorner@nikolaj-z.redmond.corp.microsoft.com>
 2015-08-24 15:55:40 -07:00
Christoph M. Wintersteiger
8c11299be6 Bugfix for theory_fpa, when datatypes contain floats. 
Fixes #201.
 2015-08-24 15:09:02 +01:00
Nikolaj Bjorner
655b44c07b make :weight understand both decimal and integral values, remove dweight, remove deprecated commands for optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-15 00:48:22 +02:00
Nikolaj Bjorner
cd838e5cf4 fix bug reported in issue #193: MBQI needs to avoid instantiating data-types that contain model values in nested positions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-13 14:29:48 +02:00
Nikolaj Bjorner
702af71a2d Check more frequently for cancelation flags to address grep0095.stp.smt2 in issue #178. Z3 spends time in pre-processing simplification, which indicates there is some opportunity to tune this portion of the code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-11 23:14:34 +02:00
Nikolaj Bjorner
424f34d3d9 enable smt tactic to be used even if cores are enabled, as long as no cores are tracked, fixes issue #189 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-11 11:16:41 +02:00
Nikolaj Bjorner
e532657d77 .. adding core validation debug option to ease diagnose issue #158 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-10 11:01:46 +02:00
Nikolaj Bjorner
db24cb8087 add core validation option to directly validate cores using the context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-10 10:56:07 +02:00
Nikolaj Bjorner
6780784bcf filter instantiations for model values to fix issue #183 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-06 14:43:08 +02:00
Nikolaj Bjorner
f96c0b6963 fixes #186, remove ite-lifting from opt_context to detect weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-06 11:52:59 +02:00
Christoph M. Wintersteiger
0cd406ca0b Fixed initialization order and unused variable warnings. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-07-30 09:09:13 +01:00
Christoph M. Wintersteiger
7c282d3719 bugfix for smt::model_finder::set_cancel 
follow-up to fixed #178
 2015-07-29 17:18:15 +01:00
Christoph M. Wintersteiger
b9e273800c Made quantifier-related parts of smt::model_finder and smt::model_checker interruptable. 
Fixes #178
 2015-07-29 16:55:45 +01:00
Nikolaj Bjorner
d7b3aaffbd Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-07-14 13:18:16 -07:00
Nikolaj Bjorner
96c8b1e7ff fixup model construction on undef results for arithmetic. Fixes issue #161 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-13 12:44:07 -07:00
Nikolaj Bjorner
6fbc8fa06c break stack abuse in relevancy propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-12 14:52:43 -07:00
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
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