mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
16194 commits 24 branches 48 tags 158 MiB
Commit graph

1595 commits

Author SHA1 Message Date
Nikolaj Bjorner
fd8b2ba596 clear regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-29 15:56:01 -07:00
Nikolaj Bjorner
e1224e116f na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 16:45:03 -07:00
Nikolaj Bjorner
f3328c743e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 16:43:55 -07:00
Nikolaj Bjorner
e1edadabec na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-27 17:06:59 -07:00
Nikolaj Bjorner
95e2d174c7 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-25 17:26:18 -07:00
Nikolaj Bjorner
a574eebd05 fixes, tests 2021-09-25 08:38:48 -07:00
Nikolaj Bjorner
e6c413b249 add variable minimization 2021-09-22 14:27:05 -07:00
Nikolaj Bjorner
c82bbaad7d update todos, working on assignment minimization 2021-09-22 13:29:36 -07:00
Nikolaj Bjorner
3447d80310 fix todo on enforcing premises 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 12:26:45 -07:00
Nikolaj Bjorner
e5df395380 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 08:44:37 -07:00
Nikolaj Bjorner
0013ae5089 elim pointer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 08:15:32 -07:00
Nikolaj Bjorner
2d78bc9282 simplify Boolean resolve 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 05:37:46 -07:00
Nikolaj Bjorner
ad267ce294 add notes and unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 05:16:10 -07:00
Nikolaj Bjorner
dc55fbf30d add notes and unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 05:04:07 -07:00
Nikolaj Bjorner
6478e789e9 optimizations, fixes, TODO items 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 14:50:18 -07:00
Nikolaj Bjorner
444084f396 add notes and tangent lemma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 11:30:50 -07:00
Nikolaj Bjorner
0426b23d0c fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 09:44:37 -07:00
Nikolaj Bjorner
23963f274d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 04:58:00 -07:00
Nikolaj Bjorner
959f150e4a Merge branch 'master' of http://github.com/z3prover/z3 into polysat 2021-09-20 17:39:04 -07:00
Nikolaj Bjorner
d4abf16551 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-20 17:38:42 -07:00
Nikolaj Bjorner
ce12c51083 remove last references to unit clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-20 17:36:07 -07:00
Nikolaj Bjorner
cd76fd9edd fixes and expose new bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-20 17:30:41 -07:00
Nikolaj Bjorner
32c3a3e3cc remove cond-log use 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-20 16:11:05 -07:00
Nikolaj Bjorner
8ee54c665a removing unit clauses and dependency manager, use minisat approach by tracking assumption literals directly also in clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-20 15:10:03 -07:00
Nikolaj Bjorner
bb5ff8db24 rename conflict_core to conflict: 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-20 14:05:55 -07:00
Nikolaj Bjorner
1e3ff3179e handle empty clauses created as lemmas as unsat state. 
add unit tests
 2021-09-19 15:43:47 -04:00
Nikolaj Bjorner
c69c316b27 enable reduce_by, more tests 2021-09-19 13:41:39 -04:00
Nikolaj Bjorner
58c66ffee8 remove propagate_bool_at, it is technically not propagating but assigning 2021-09-19 08:47:14 -04:00
Nikolaj Bjorner
16d48c17dd streamline propagation 2021-09-19 08:30:51 -04:00
Nikolaj Bjorner
663b61b612 add propagation after lemma addition 2021-09-19 08:09:53 -04:00
Nikolaj Bjorner
dac2f1c026 cleaning 2021-09-19 07:52:57 -04:00
Nikolaj Bjorner
02a38009b9 remove disjunctive lemma feature 2021-09-19 07:33:20 -04:00
Nikolaj Bjorner
fa3886136b adding Boolean propagation, watch; and factoring 2021-09-18 22:18:15 -04:00
Nikolaj Bjorner
f01da40e49 adding watches on Booleans 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-16 22:01:34 +01:00
Nikolaj Bjorner
c25fd71bf4 fixes 2021-09-16 10:10:50 +01:00
Nikolaj Bjorner
689c5b4e12 generalize level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-15 16:46:30 +01:00
Nikolaj Bjorner
7e7f88ae3d fix backtracking from fi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-15 09:28:59 +01:00
Nikolaj Bjorner
3c8c8f5d40 update var dependency tracking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-15 09:10:36 +01:00
Jakob Rath
34631d972d fix compiler warning 2021-09-14 15:10:17 +02:00
Jakob Rath
b90b888d0f add nicer way of adding inequalities with constants 2021-09-14 15:03:45 +02:00
Jakob Rath
c4e098b5d4 add hack for testing conflict resolution (but commented out) 2021-09-14 14:49:56 +02:00
Jakob Rath
a8e68ebf86 verify_sat should perform a semantic check 2021-09-14 14:49:20 +02:00
Jakob Rath
66a41383e8 remove remove_var 2021-09-14 14:45:03 +02:00
Jakob Rath
8103627e47 fix test_l4 2021-09-14 14:45:03 +02:00
Nikolaj Bjorner
f9b1b4e65d add mode to display to get constraints without wild-card notation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-14 14:13:31 +02:00
Jakob Rath
15ebbbda2c fix assertion 2021-09-14 14:04:35 +02:00
Jakob Rath
f04345724c Ensure core is conflicting also after set(v) 2021-09-14 11:24:09 +02:00
Jakob Rath
d9eca1f40f reset/set on successful superposition 2021-09-14 11:08:57 +02:00
Jakob Rath
640acd2ebc notes for later 2021-09-14 11:01:35 +02:00
Jakob Rath
d935714874 Track FI lemma in core; remove bailout_lemma 2021-09-14 11:01:06 +02:00