mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-15 17:06:39 +00:00
Code Activity
11152 commits 43 branches 51 tags 169 MiB
Commit graph

129 commits

Author SHA1 Message Date
Nikolaj Bjorner
41ca956012 expose import model converter over Python, document it, add partial order axioms for lex, disable linear order axioms, prepare ground for re-adding clauses from reconstruction stack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-18 13:45:13 -07:00
Nikolaj Bjorner
333b32b0d2 disable adding redundant ite clauses as lemma. Add as non-redundant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-21 16:32:45 +02:00
Nikolaj Bjorner
cbe52e298b remove tracing, fix doctext 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-21 15:08:26 +02:00
Nikolaj Bjorner
e0d8cefde4 remove cooperate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 20:15:46 -07:00
Nikolaj Bjorner
dc0e9c1919 completing user print experience with seq/re #2200 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 11:46:36 -07:00
Nikolaj Bjorner
a74ac93bcc fix #2196 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-22 13:34:31 -07:00
Nikolaj Bjorner
057151c7a8 fix #2188 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-18 07:56:25 -07:00
Nikolaj Bjorner
4c799c144a fix gc to not remove ternary clauses that are on assignment trail. This addresses issue with drat proofs that don't pass drat-trim due to deletion during gc, but use in conflicts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-22 11:14:20 +01:00
Nikolaj Bjorner
3548057bd1 fix detection of arithmetic operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-20 14:00:05 +01:00
Nikolaj Bjorner
22783a4bcb import more from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 13:09:28 -08:00
Nikolaj Bjorner
d04e72819a abstract solver API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-06 19:42:01 +01:00
Nikolaj Bjorner
d3d392da41 adding maxlex, delay mk_true() calls in goal2sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 21:36:40 -08:00
Nikolaj Bjorner
b11ec3bfbf merge sat_tactic from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:17:42 -08:00
Nikolaj Bjorner
b8d18c6c6d speed-up handling of cnf input to inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-11 20:52:19 -08:00
Bruce Mitchener
3149d7f7a4 Fix typos. 2018-11-30 22:19:30 +07:00
Nikolaj Bjorner
074ed0d874 fix warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-24 17:39:19 -08:00
Nikolaj Bjorner
ec36a9c495 fix user push/pop with ba constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-22 12:40:23 -08:00
Nikolaj Bjorner
cf4bf7b591 more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-02 18:44:53 -05:00
Nikolaj Bjorner
e9d615e309 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 15:16:22 -07:00
Bruce Mitchener
373b691709 Use 'override' where possible. 2018-10-02 10:26:38 +07:00
Bruce Mitchener
cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Nikolaj Bjorner
c8730daea7 fix memory leak, add strengthening 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-03 16:56:07 -07:00
Nikolaj Bjorner
96d3b98a44 fix #1783, wronge clausification of negated pb inequalities. Signs were ignored 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-11 13:33:09 -07:00
Nikolaj Bjorner
84c7df75d6 record statistics setting in config_params so that fp engine can access them, fix serialization bug when check-assumptions returns unsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-06 16:21:27 -07:00
Nuno Lopes
cef17c22a1 remove some allocs from exceptions 2018-07-02 17:08:02 +01:00
Nikolaj Bjorner
335d672bf1 fix #1675, regression in core processing in maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-19 23:23:19 -07:00
Nikolaj Bjorner
ff0f257102 remove iff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Nikolaj Bjorner
e4d24fd2c3 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 09:39:19 -07:00
Nikolaj Bjorner
859c68c2ac merge with opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-30 08:27:54 -07:00
Nikolaj Bjorner
a37303a045 move parallel-tactic to solver level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-16 08:21:21 -07:00
Nikolaj Bjorner
c513f3ca09 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:57:01 -07:00
Nikolaj Bjorner
f04e805fa4 add hiding to auxiliary declarations created in mc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-06 18:02:37 -08:00
Nikolaj Bjorner
718e5a9b6c add unit extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-06 01:08:17 -08:00
Nikolaj Bjorner
4c1379e8c9 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-19 21:49:03 -08:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Nikolaj Bjorner
8fb7fb9f98 add missing caching of PB/cardinality constraints, increase limit for compiling cardinalities to circuits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-11 19:27:00 -08:00
Bruce Mitchener
7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Nikolaj Bjorner
5e482def18 fix local search encoding bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-08 07:27:32 -08:00
Nikolaj Bjorner
61f99b242e xor to xr to avoid clang issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 15:25:02 -08:00
Nikolaj Bjorner
20fe08d80c fix more bugs with compilation of pb equalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-04 09:51:45 -08:00
Nikolaj Bjorner
354c16454a fix bug in translation of pbeq into sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-03 22:19:25 -08:00
Nikolaj Bjorner
3b1810d893 fix hidden tautology bug on non-learned clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-21 23:18:41 -08:00
Nikolaj Bjorner
7fc1b75cb8 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2018-01-19 21:36:24 -08:00
Nikolaj Bjorner
e4f29a7b8a debugging mc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-19 21:09:52 -08:00
Nikolaj Bjorner
67de30ca4a Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2018-01-19 13:57:25 -08:00
Nikolaj Bjorner
d6c49adddb local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-19 13:57:21 -08:00
Nikolaj Bjorner
c7ee532173 fix static 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-18 10:44:40 -08:00
Nikolaj Bjorner
7b8101c502 fix bugs related to model-converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-17 12:25:24 -08:00
Nikolaj Bjorner
3047d930e1 fix xor processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-13 19:53:50 -08:00
Nikolaj Bjorner
d79c33fb21 fix model bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-13 16:12:38 -08:00