mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-02 11:46:55 +00:00
Code Activity
17973 commits 44 branches 58 tags 185 MiB
Commit graph

313 commits

Author SHA1 Message Date
Jakob Rath
9fa5096776 conflict logging 2022-04-12 16:06:20 +02:00
Jakob Rath
00fa4b3320 Better search stack printing 2022-04-12 14:13:20 +02:00
Nikolaj Bjorner
afa7162ab1 add parameter class for polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-12 10:35:23 +02:00
Jakob Rath
d98a93bcc8 Remove bdecide 2022-04-11 15:55:41 +02:00
Jakob Rath
63031548cb Store only literals in the conflict state 2022-04-11 15:00:06 +02:00
Nikolaj Bjorner
fde78f99c3 fix propagation when variables are assigned 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-07 13:27:36 +02:00
Nikolaj Bjorner
a623865a82 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-06 05:44:31 +02:00
Jakob Rath
613b0db4cc fix refcount issue 2022-03-19 04:19:16 +01:00
Jakob Rath
d41d3fa6ea fix some bugs 2022-03-18 16:05:51 +01:00
Jakob Rath
fd353bff17 unsat core 2022-03-18 15:49:44 +01:00
Jakob Rath
509a007ed7 Integrate univariate solver in polysat 2022-03-18 15:43:06 +01:00
Jakob Rath
c648b57493 forbidden intervals only used by viable 2022-03-10 16:12:13 +01:00
Nikolaj Bjorner
8c9835bca6 smul no overflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 18:55:07 +02:00
Nikolaj Bjorner
4c4f916917 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-02 08:24:58 -08:00
Nikolaj Bjorner
c48f14e537 updated conflict state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-01 11:47:33 -08:00
Jakob Rath
5ee02ec5df Merge remote-tracking branch 'origin/polysat' into polysat 2022-01-31 15:36:22 +01:00
Nikolaj Bjorner
b488a1fadd WIP revamp conflict state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-29 16:17:58 -08:00
Nikolaj Bjorner
60248d0981 resolution is still wrong 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-29 09:32:14 -08:00
Jakob Rath
67647433ba log justifications during conflict resolution 2022-01-28 15:52:52 +01:00
Nikolaj Bjorner
0677eb1c05 fixing up missing dependencies during resolution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 16:58:16 -08:00
Nikolaj Bjorner
1264fe462d merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 14:33:38 -08:00
Nikolaj Bjorner
ff4b471f93 resurrect Booelan decisions to deal with quot-rem and similar axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 14:26:41 -08:00
Jakob Rath
4236830a8e Also check clauses when returning SAT 2022-01-27 12:23:57 +01:00
Nikolaj Bjorner
be790b8892 add back minimize vars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 18:01:26 -08:00
Nikolaj Bjorner
6df23fbce3 add note about a bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 16:58:00 -08:00
Nikolaj Bjorner
d1fcc41c7f merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 21:53:10 +01:00
Nikolaj Bjorner
ff93c03972 integrate polysat into bv solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 20:20:45 +01:00
Jakob Rath
645f190e35 Add wrapper for external dependencies to prevent accidental conversions 2022-01-26 11:44:01 +01:00
Nikolaj Bjorner
cd11b70864 add value-propagate flag to patch regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-23 12:09:49 +01:00
Nikolaj Bjorner
cbbf1381f7 update to use incremental substitution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-23 03:00:25 +01:00
Nikolaj Bjorner
417a5320c7 forbidden intervals for strict inequalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-22 11:14:53 +01:00
Nikolaj Bjorner
3c940b5125 use nyi to catch uncovered cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-21 17:49:43 +01:00
Jakob Rath
c4c9c84aeb Treat eval'd literals as propagations (not as decisions) 2022-01-21 15:56:16 +01:00
Nikolaj Bjorner
8765dc16a5 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-21 13:11:53 +01:00
Jakob Rath
0a48846add Add separate state for deciding on lemmas 2022-01-21 11:55:03 +01:00
Jakob Rath
daf23cfe02 wlist_invariant 2022-01-20 17:47:26 +01:00
Jakob Rath
543ad2f205 skip unassigned variables when computing level 2022-01-20 17:46:23 +01:00
Jakob Rath
c7a09051fa Assert constraints only once 2022-01-20 17:44:29 +01:00
Jakob Rath
b968898b7e use member variable rather that static 2022-01-20 17:09:36 +01:00
Jakob Rath
64152c338d Don't nest propgate() calls 2022-01-20 17:06:30 +01:00
Jakob Rath
175b348948 Update quot_rem axioms 2022-01-18 10:43:12 +01:00
Jakob Rath
e005838129 clause_builder should not fail on always-true literals 
Otherwise, e.g. when adding axioms, the caller would have to check each literal before adding it.
 2022-01-18 10:32:33 +01:00
Jakob Rath
ebc4df1ece remove branch_bool 2022-01-17 15:57:05 +01:00
Jakob Rath
3895d8d6bb quot_rem needs additional constraint: quot <= a 2022-01-12 13:44:30 +01:00
Nikolaj Bjorner
eb9bfbb3d8 add resolved attribute 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-20 17:39:12 -08:00
Nikolaj Bjorner
adb3d68743 fixes to literal propagation exposed by bitwise and unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-19 15:21:12 -08:00
Nikolaj Bjorner
c1d5111159 add first test for band 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-18 12:28:59 -08:00
Nikolaj Bjorner
a6684824c1 elaborate on narrow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-15 10:13:33 -08:00
Nikolaj Bjorner
a2aa1170f9 rename to op-constraint to give space for other operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-15 09:20:11 -08:00
Nikolaj Bjorner
79bc33b88e na 2021-12-14 19:42:19 -08:00