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

697 commits

Author SHA1 Message Date
Nikolaj Bjorner
6f689c3c1f updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-22 12:21:20 +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
Nikolaj Bjorner
f2dd95eaa9 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2022-01-21 15:57:35 +01:00
Nikolaj Bjorner
49d9e3440c use band, add bvneg compile step 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-21 15:57:27 +01:00
Jakob Rath
c4c9c84aeb Treat eval'd literals as propagations (not as decisions) 2022-01-21 15:56:16 +01:00
Jakob Rath
c9b9b5f531 remove obsolete test case 2022-01-19 19:10:10 +01:00
Jakob Rath
fa75a9109e Test forbidden intervals, disequal case 2022-01-19 19:06:35 +01:00
Jakob Rath
3895d8d6bb quot_rem needs additional constraint: quot <= a 2022-01-12 13:44:30 +01:00
Jakob Rath
e0e03b3fc5 Wrap polysat tests in class 2022-01-12 13:42:04 +01:00
Nikolaj Bjorner
2afc58cc08 fix missing dependency, expose inefficiency 2021-12-19 12:32:20 -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
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
bc1e44ab71 fill in some use cases 2021-12-14 19:51:30 -08:00
Nikolaj Bjorner
06f7ba2e78 add stubs for shr 2021-12-14 14:35:08 -08:00
Nikolaj Bjorner
30a2c32c3b add placeholder for simplification 2021-12-12 14:52:09 -08:00
Nikolaj Bjorner
7bf76dd1f6 finally! 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-12 10:26:54 -08:00
Nikolaj Bjorner
f1d46b58a4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-11 17:38:09 -08:00
Nikolaj Bjorner
59acd77981 n 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-11 13:01:08 -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
dcdbbfb925 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 09:50:53 -08:00
Nikolaj Bjorner
8d3c3ede39 save 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-08 12:40:44 -08:00
Lev Nachmanson
7758b519bc
Handle correctly cancelled run (#5695) 
* remove the bound on total iterations in simplex

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove unncesseray checks in  get_freedom_interval_for_column()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix the build of test-z3

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Revert "remove unncesseray checks in  get_freedom_interval_for_column()"

This reverts commit 6770ed85e3.

* optimize get_freedom_interval_for_column() for feasible case

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add function lar_solver::status_feasible

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* rename status_is_feasible() to is_feasible()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix the linux build

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-12-05 18:38:37 -08:00
Nikolaj Bjorner
fc6e127cca don't add viable premises on decisions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-25 20:19:58 +01:00
Nikolaj Bjorner
adf41c5d02 another bug fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-24 13:37:15 +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
de424713e4 if you are really reading this commit message, you must be a programmer who has no life. 2021-11-18 10:10:50 -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
c1d58088be na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-10 01:42:04 -08:00
Nikolaj Bjorner
d0c8240560 refactor forbidden intervals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-09 10:34:11 -08:00
Nikolaj Bjorner
7b845c7138 build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-02 19:26:48 -07:00
Nikolaj Bjorner
3f3bd5948f fixes/debugging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-02 14:48:19 -07:00
Nikolaj Bjorner
813674087e wip 2021-10-04 14:43:33 -07:00
Nikolaj Bjorner
f3328c743e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 16:43:55 -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
dc55fbf30d add notes and unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 05:04:07 -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
cd76fd9edd fixes and expose new bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-20 17:30:41 -07:00
Nikolaj Bjorner
fd799089b7 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-20 11:19:26 -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
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
689c5b4e12 generalize level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-15 16:46:30 +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
4b3af1d0a4 Add notes from discussion 2021-09-14 15:45:17 +02:00