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

18146 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath
01af25ca02 Remove backjump state from conflict 2022-11-14 14:33:19 +01:00
Jakob Rath
406696f0a3 Remove unused code 2022-11-11 10:25:49 +01:00
Jakob Rath
fc773ef19e Remove old file 2022-11-10 14:42:55 +01:00
Jakob Rath
d3f70c0fb8 Rename: explain -> superposition 2022-11-10 14:42:13 +01:00
Nikolaj Bjorner
27f8b8d13a inline definition in header file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-09 09:55:05 -08:00
Nikolaj Bjorner
a98502b62f weaken assertion, remove dependency on hash_compare in unittest for hashtables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-09 09:28:49 -08:00
Jakob Rath
4b146a61ff minor 2022-11-09 17:00:27 +01:00
Jakob Rath
abc4cc5295 Simplify boolean propagation level 2022-11-09 16:59:51 +01:00
Jakob Rath
27d65df70b Use correct level for pvar propagations (v := val) 2022-11-09 16:58:34 +01:00
Jakob Rath
c08866dcec Disable simplify_clause::try_recognize_bailout for now 2022-11-09 14:30:33 +01:00
Jakob Rath
596a53c14b Fix axioms 2022-11-09 12:03:27 +01:00
Jakob Rath
89a2700e5f Print table of unit test results 2022-11-08 17:17:02 +01:00
Jakob Rath
05ddac5ddc Allow disabling log messages 2022-11-08 17:15:56 +01:00
Jakob Rath
1d805807e9 Allow setting a default debug action 
Helps avoiding user interaction when running a batch of unit tests.
 2022-11-08 17:13:36 +01:00
Jakob Rath
eaf38abf17 Normalize to 0 < 0 instead of 1 <= 0 2022-11-07 15:32:34 +01:00
Jakob Rath
e7c77a22ab Dedup quot_rem and lshr too 2022-11-07 15:25:05 +01:00
Jakob Rath
2953b1c093 Dedup op constraints 2022-11-07 15:02:48 +01:00
Jakob Rath
89acd96a89 All constraints have bvars now 2022-11-07 14:14:36 +01:00
Jakob Rath
586ffdf402 Remove unnecessary argument 2022-11-07 14:04:28 +01:00
Jakob Rath
a1736473a4 Move bit-wise expressions to constraint_manager 2022-11-07 14:00:02 +01:00
Jakob Rath
7662427d92 Split constraint_manager into separate file 2022-11-07 13:33:48 +01:00
Jakob Rath
e33f728128 hm 2022-10-31 15:54:56 +01:00
Jakob Rath
29695391de First pass at free variable elimination 2022-10-31 15:22:03 +01:00
Jakob Rath
4cdd3bf77d Add overload for conflict::add_lemma 2022-10-31 15:19:36 +01:00
Jakob Rath
6a03df9017 Track set of variables that occur in conflict constraints 2022-10-31 15:18:48 +01:00
Jakob Rath
eba59356f3 Disable problematic resolve_with_assignment 2022-10-31 15:17:32 +01:00
Nikolaj Bjorner
eca72ffda1 debug simplify_clause 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-14 12:12:21 +02:00
Nikolaj Bjorner
e711808d3e throttle on degree bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-13 20:04:21 +02:00
Nikolaj Bjorner
7036dd826f update defaults to make it easier to test polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-13 19:46:45 +02:00
Nikolaj Bjorner
2d8b7b5ac6 deal with compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-13 17:55:47 +02:00
Jakob Rath
66469bb678 Don't leave propagation loop too early (cause of unsoundness in bench0) 2022-10-12 13:20:34 +02:00
Jakob Rath
4406652c7b Narrow conflicting constraint after backjumping 2022-10-07 18:01:54 +02:00
Jakob Rath
54ed6d4413 Don't cut off output arbitrarily 2022-10-07 17:49:03 +02:00
Jakob Rath
714c71ab88 Try to fix lemma_invariant 2022-10-07 17:48:22 +02:00
Jakob Rath
05f1b4dd1a Update note on subsumption (for later) 2022-10-07 16:32:56 +02:00
Jakob Rath
b2d926362c Move some functions; delete old comments 2022-10-07 16:32:29 +02:00
Jakob Rath
e7c9a99d08 Add note as comment 2022-10-07 16:29:14 +02:00
Jakob Rath
23a747235d Some assertions are now too strict 
If possible, we should set the new constraint to l_true;
and revert most of this change later.
Or we adjust the conflict invariant:
- l_true constraints is the default case as before,
- l_undef constraints are new and justified by some side lemma, but
  should be treated by the conflict resolution methods like l_true
  constraints,
- l_false constraints are disallowed in the conflict (as before).
 2022-10-07 16:24:14 +02:00
Jakob Rath
74b53c3323 Fix checking of lemma invariant 2022-10-07 16:20:44 +02:00
Jakob Rath
8333664433 Simplify handling of side lemmas in conflict 2022-10-07 16:19:41 +02:00
Jakob Rath
8b4a36e3bd Simplify clause_builder 2022-10-07 15:22:49 +02:00
Jakob Rath
e18bc46de1 Move on_scope_exit to util.h 2022-10-07 14:23:26 +02:00
Jakob Rath
dcd6c01a90 revive polynomial superposition (wip) 2022-10-07 10:34:07 +02:00
Jakob Rath
155b746e03 side lemmas 2022-10-07 10:18:29 +02:00
Jakob Rath
bef1be8cb5 should not happen anymore 2022-10-07 10:11:00 +02:00
Jakob Rath
af368b39c9 less output 2022-10-07 10:10:44 +02:00
Jakob Rath
f184545aca Debug dlist insertion 
Found because of assertion failure in
test_polysat::test_fixed_point_arith_div_mul_inverse()
 2022-10-05 17:24:28 +02:00
Jakob Rath
e58815884f Remove debugging leftover 2022-10-04 17:10:10 +02:00
Jakob Rath
dc9373dcbd Change old solver::propagate method 2022-10-04 17:09:09 +02:00
Jakob Rath
a0fe568561 Another possible case for subsumption 2022-10-04 14:13:51 +02:00