mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-25 20:46:01 +00:00
Code Activity
16766 commits 63 branches 52 tags 178 MiB
Commit graph

132 commits

Author SHA1 Message Date
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
Jakob Rath
afc711d6ec move into separate component 2022-03-10 16:10:56 +01:00
Jakob Rath
6aee62ef2f Univariate solver interface 2022-03-10 11:01:57 +01:00
Nikolaj Bjorner
1faccffd0d add smul over and underflow predicate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-20 11:39:45 +02: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
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
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
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
d7548f6867 Now we can have a working binary add_eq/add_diseq 2022-01-26 11:50:49 +01:00
Jakob Rath
645f190e35 Add wrapper for external dependencies to prevent accidental conversions 2022-01-26 11:44:01 +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
Jakob Rath
c4c9c84aeb Treat eval'd literals as propagations (not as decisions) 2022-01-21 15:56:16 +01:00
Jakob Rath
0a48846add Add separate state for deciding on lemmas 2022-01-21 11:55:03 +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
fa75a9109e Test forbidden intervals, disequal case 2022-01-19 19:06:35 +01:00
Jakob Rath
ebc4df1ece remove branch_bool 2022-01-17 15:57:05 +01:00
Jakob Rath
e0e03b3fc5 Wrap polysat tests in class 2022-01-12 13:42:04 +01: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
02369647a0 add functionality for bit-wise and 2021-12-15 14:07:53 -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
6eb6eb39a4 more of shr 2021-12-14 19:23:31 -08:00
Nikolaj Bjorner
934564882c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-14 12:34:34 -08:00
Nikolaj Bjorner
33d433d742 split out restart 2021-12-12 17:27:30 -08:00
Nikolaj Bjorner
30a2c32c3b add placeholder for simplification 2021-12-12 14:52:09 -08:00
Nikolaj Bjorner
bf258ee29d add bit shorthand 2021-12-09 15:25:44 -08:00
Nikolaj Bjorner
a4fc63c542 initial overflow test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 14:39:00 -08:00
Nikolaj Bjorner
bd08d766d2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 09:44:45 -08:00
Nikolaj Bjorner
f3ac879fa4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 08:25:52 -08:00
Nikolaj Bjorner
90bd5f186b tune based on test_l5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-26 20:14:00 +01:00
Nikolaj Bjorner
caef8d026f add unsat core, activity, quick pass for viable 2021-11-24 13:23:28 +01:00
Nikolaj Bjorner
8db711bc3c retire deprecated functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-22 18:14:15 +01:00
Nikolaj Bjorner
8ec5ccbb9a roll in new-viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-22 06:17:20 +01:00
Nikolaj Bjorner
d86570ce75 prepare for new viable 2021-11-21 06:18:35 +01:00
Nikolaj Bjorner
1dcb7e6f6a remove justified vars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 15:43:39 -08:00
Nikolaj Bjorner
69a17d0c60 test and fix viable2 2021-11-14 20:55:12 -08:00
Nikolaj Bjorner
4261345503 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-13 17:43:07 -08:00
Nikolaj Bjorner
c9f5ce43b2 viable 2 with dlist 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-10 14:43:10 -08:00
Nikolaj Bjorner
0bec8520e1 adding new viable using forbidden intervals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-10 08:23:45 -08:00
Nikolaj Bjorner
931e1624b2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-10 02:58:35 -08:00
Nikolaj Bjorner
57c40e480b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-08 05:08:57 -08:00
Nikolaj Bjorner
813674087e wip 2021-10-04 14:43:33 -07:00
Nikolaj Bjorner
a574eebd05 fixes, tests 2021-09-25 08:38:48 -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
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