mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
16500 commits 49 branches 53 tags 182 MiB
Commit graph

1729 commits

Author SHA1 Message Date
Nikolaj Bjorner
947ea66cad simplify output to use signed constants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-18 17:39:13 -07:00
Nikolaj Bjorner
a049235caa simplify output to use signed constants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-18 17:26:11 -07:00
Nikolaj Bjorner
f263045f96 modify mk_mul 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-18 17:18:16 -07:00
Nikolaj Bjorner
3da37f4fb5 add unit test driver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-18 10:58:42 -07:00
Nikolaj Bjorner
57df45dc16 Merge branch 'master' of https://github.com/z3prover/z3 into polysat 2021-06-18 10:02:33 -07:00
Jakob Rath
c4963f4381
Polysat: add two more prototype rules (#5355) 
* Add try_div to PDDs

* x>y is false when x==y

* First version of the other two prototype rules

* More band-aid fixes...
 2021-06-18 08:48:50 -07:00
Jakob Rath
3e1cfcd538
Polysat: conflict explanation prototype (#5353) 
* display constraint's extra info in one place

* Add stub for conflict explainer

* Add helper functions to check whether constraint is active at base level

* Add helper class tmp_assign

* Add clause_builder; it skips unnecessary literals during clause creation

* some fixes

* Use clause_builder for forbidden intervals

* remove old comments

* fixes/comments in solver

* print redundant clauses

* First pass at conflict_explainer

* remove unused model class

* Choose value for k

* also print min/max k
 2021-06-17 10:35:32 -05:00
Jakob Rath
1fe7dc40fe
Polysat: add simpler monotonicity unit test + minor changes (#5348) 
* Add simpler versions of monotonicity puzzle

* band-aid fix to conflicts during revert_decision

* minor changes
 2021-06-15 12:18:37 -05:00
Nikolaj Bjorner
c1ab7987f6 #5324 2021-06-07 11:41:35 -07:00
Lev Nachmanson
3a5b88e52b set status to CANCELLED on the total_iterations threshold bailout 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-06-07 07:34:16 -07:00
Nikolaj Bjorner
9afc59d5b4 #5324 2021-06-06 15:39:23 -07:00
Nikolaj Bjorner
7cd901019f #5324 2021-06-05 17:14:51 -07:00
Nikolaj Bjorner
5da4b29136 turn on parity test 2021-06-04 10:18:24 -07:00
Nikolaj Bjorner
0182187296 fix regression in arithmetic resource bound 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-03 11:41:42 -07:00
Nikolaj Bjorner
8a02167e30 get-universe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 21:08:08 -07:00
Nikolaj Bjorner
3e773fba5e get-universe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 21:07:48 -07:00
Nikolaj Bjorner
6a5cdd48e7 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 20:43:45 -07:00
Nikolaj Bjorner
ab3b387076 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 20:37:43 -07:00
Nikolaj Bjorner
45adfc6a66 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 20:31:05 -07:00
Nikolaj Bjorner
0e6d530518 std::cout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 18:49:37 -07:00
Nikolaj Bjorner
2156c74d51 #4702 
initial gcd test implementation for accumulated parity constraints
 2021-06-01 15:26:36 -07:00
Nikolaj Bjorner
5127014f18 track cuts 2021-06-01 15:26:36 -07:00
Jakob Rath
8757f04d20
Polysat: disjunctive lemmas (#5311) 
* Add macro to disable linear solver for development

* Move new_* and add_* to header

* Add ref_vector_core::push_back(ref<T>&&)

* Attempt to simplify lifetime handling

* Make operator bool() explicit

* clause improvements

* display boolean assignment

* clause::resolve

* bug fixes

* more fixes

* final case of backtrack
 2021-05-28 13:53:08 -07:00
Nikolaj Bjorner
5fd3ef6580 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-23 16:50:47 -07:00
Nuno Lopes
f1e0d5dc8a remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
Nikolaj Bjorner
befc47902e track 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 17:57:23 -07:00
Nikolaj Bjorner
79e38c6477 notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 17:47:48 -07:00
Nikolaj Bjorner
52ad5aaa58 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 14:39:31 -07:00
Nikolaj Bjorner
147b3600d9 keep 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 14:36:49 -07:00
Nikolaj Bjorner
b22928bfc9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 14:16:50 -07:00
Nikolaj Bjorner
5ad486901e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-21 18:03:05 -07:00
Nikolaj Bjorner
8ba0fb5b58 rounding mode sort removed for incompatibility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-21 16:18:43 -07:00
Nikolaj Bjorner
00deb12238 signed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-21 15:51:27 -07:00
Jakob Rath
28996429df
Polysat disjunctive lemmas (WIP) (#5275) 
* Extend search state by boolean literals

* Only resolve against positive equality

* mk_dep_ref

* Make clause non-owning

* scoped_clause

* Use scoped_clause

* minor

* scoped_ptr move assignment

* WIP: internal handling of disjunctive constraints

* leaf_value

* disjunctive constraints continued

* Fix bool_lit

* Actually add constraints to storage

* Some fixes

* more fixes

* constraint should have a bool_lit instead of a bool_var

* propagate(bool_lit)

* updates

* interface changes

* small fixes

* Make sat::dimacs_lit's constructor explicit

(otherwise, calling operator<< with sat::literal is ambiguous)

* Use sat::literal

* Print test name at the beginning

* Convention: constraint corresponds to the positive boolean literal

* Make constraint ownership more explicit

* clause stores literals
 2021-05-21 13:50:25 -07:00
Nikolaj Bjorner
26893005c7 Merge branch 'master' of https://github.com/z3prover/z3 into polysat 2021-05-20 15:28:32 -07:00
Nikolaj Bjorner
7a1a2b2525 make unit types generic 2021-05-20 15:28:26 -07:00
Nikolaj Bjorner
ec034679ce #5215 
memory leaks
 2021-05-19 12:42:38 -07:00
Nikolaj Bjorner
973a32a015 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-16 13:50:41 -07:00
Nikolaj Bjorner
eaca24ac01 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-15 17:00:49 -07:00
Nikolaj Bjorner
88bbe9d54e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-15 10:12:11 -07:00
Nikolaj Bjorner
683ce27c8f linear solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-14 17:10:01 -07:00
Nikolaj Bjorner
17fcf79c04 interleave linear solver calls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-14 11:31:35 -07:00
Nikolaj Bjorner
118dc0f3b4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-14 10:25:42 -07:00
Nikolaj Bjorner
587750b9a3 outline layer between polysat solver and fixplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-13 18:04:44 -07:00
Nikolaj Bjorner
334bde7623 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-05-13 17:24:00 -07:00
Nikolaj Bjorner
49a903c875 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-13 17:23:55 -07:00
Nikolaj Bjorner
d833483ca0 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-13 17:18:09 -07:00
Nikolaj Bjorner
cf8b3a0788 add copy constructor to handle reference count miss-match 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-12 17:56:09 -07:00
Nikolaj Bjorner
0d776ecf88 eliminate basic variables from new rows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-12 15:58:35 -07:00
Nikolaj Bjorner
62b7719d5a separate into self-contained mod interval 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-11 11:22:55 -07:00