mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
19959 commits 49 branches 53 tags 182 MiB
Commit graph

19959 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath
5f2fd039ba Perform clause simplification earlier 2022-12-22 13:07:38 +01:00
Jakob Rath
44f0f88172 test 2022-12-21 16:23:05 +01:00
Jakob Rath
d51031f19b debug 2022-12-21 16:05:27 +01:00
Clemens Eisenhofer
c8b9127028 Added justifications for intermediate values [e.g., 2 * x in the pdd (2 * x) + y] 
This might allow propagation in both directions
 2022-12-21 13:52:27 +01:00
Jakob Rath
ec158845fc Add test for sat branch 2022-12-21 12:24:49 +01:00
Jakob Rath
109ab0be40 Detect more equations in refine_equal_lin 2022-12-21 12:21:22 +01:00
Jakob Rath
8da9850d45 Add rational::pseudo_inverse 2022-12-21 12:13:05 +01:00
Jakob Rath
4a1781d747 more viable refinement tests 2022-12-21 11:18:27 +01:00
Nikolaj Bjorner
0a75585073 revamp parity propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-20 17:45:33 -08:00
Nikolaj Bjorner
ca855fbad3 redoing parity lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-20 15:46:25 -08:00
Nikolaj Bjorner
a8d401864b review 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-20 12:46:15 -08:00
Jakob Rath
5c54ea87f1 Add unit test based on bench27 2022-12-20 09:40:15 +01:00
Jakob Rath
e5b142b265 Rotate first entry for refinement 2022-12-20 09:32:27 +01:00
Nikolaj Bjorner
fe8034731d fix #6501 2022-12-19 21:02:55 -08:00
Nikolaj Bjorner
f961300036 Merge branch 'master' of https://github.com/z3prover/z3 2022-12-19 12:40:51 -08:00
Nikolaj Bjorner
603597a22e deal with cancellation in qe for #6500 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-19 12:40:39 -08:00
Jakob Rath
86a36a524a Fix unsoundness in viable fallback 
(the src constraint of forbidden intervals is not necessarily univariate)
 2022-12-19 15:37:49 +01:00
Jakob Rath
868a3710e0 fix segfault 2022-12-19 14:25:58 +01:00
Jakob Rath
59592754d8 minor univariate tweak 2022-12-19 14:07:57 +01:00
Jakob Rath
ac0e9ebe5f Don't lose variables when aborting decisions 2022-12-19 14:02:47 +01:00
Jakob Rath
69b41a7e70 Check invariant on pvars 2022-12-19 13:55:50 +01:00
Clemens Eisenhofer
ec06027515 First step towards explaining single bits 2022-12-19 12:27:37 +01:00
Jakob Rath
208f166934 Merge remote-tracking branch 'origin/polysat' into polysat 2022-12-19 09:11:18 +01:00
Nikolaj Bjorner
30bbb5399f add stub 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-18 22:02:42 -08:00
Nikolaj Bjorner
1c884c8d72 allow multiple lemmas during processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-18 19:03:28 -08:00
Nikolaj Bjorner
1940f53b31 fix memory smash in cache push 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-18 12:33:58 -08:00
Nikolaj Bjorner
8c775f55a1 adding stub for non-overflow lemma (disabled as not seen to be of use) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-18 12:26:30 -08:00
Nikolaj Bjorner
899b1f8f7e fiddle with univariate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-17 20:02:46 -08:00
Nikolaj Bjorner
4e8bd4425f add find_two 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-17 19:41:09 -08:00
Nikolaj Bjorner
3c035daaa6 fix missing parity propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-17 19:08:40 -08:00
Nikolaj Bjorner
b581cbf062 add lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-17 18:25:21 -08:00
Jakob Rath
bf92fa4882 clause_iterator 2022-12-16 15:21:32 +01:00
Jakob Rath
342774eff8 test_ineq_non_axiom4 is slow but doesn't block anymore 2022-12-16 15:02:04 +01:00
Jakob Rath
75a64975b5 test 2022-12-16 15:00:50 +01:00
Jakob Rath
3e6e1e1a8a test 2022-12-16 14:37:31 +01:00
Jakob Rath
ca373836af Merge remote-tracking branch 'origin/polysat' into polysat 2022-12-16 14:26:38 +01:00
Jakob Rath
3b3636b30e Remove conflict::set 2022-12-16 14:25:41 +01:00
Jakob Rath
06e6f27614 refactor 2022-12-16 14:22:50 +01:00
Jakob Rath
9f05f645c1 update types and docs 2022-12-16 13:16:55 +01:00
Jakob Rath
c54c564019 convert to loop 2022-12-16 13:11:20 +01:00
Jakob Rath
e23774a746 reorder definitions 2022-12-16 13:06:16 +01:00
Jakob Rath
afde0e993c Add bitblasting fallback to viable::query 
(integration between conflict/viable is still messy)
 2022-12-16 13:02:54 +01:00
Jakob Rath
44cb528300 Extract usolver 2022-12-16 10:46:57 +01:00
Jakob Rath
5d7833e65e Warn on unused result (mainly for substitution::add) 2022-12-16 10:28:57 +01:00
Clemens Eisenhofer
d5bc4b84a7 Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat 2022-12-16 10:14:10 +01:00
Clemens Eisenhofer
71211f3134 Some bugfixes and unit-tests for variable elimination 2022-12-16 10:12:34 +01:00
Nikolaj Bjorner
e423fabf6a tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-15 20:35:36 -08:00
Nikolaj Bjorner
0768a2ead1 updated doc 2022-12-15 19:23:32 -08:00
Nikolaj Bjorner
ecf25a4fe2 outline scheme 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-15 14:57:52 -08:00
Nikolaj Bjorner
13920c4772 more doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-15 11:42:02 -08:00