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

15614 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
b9f6fc5130 debug buidl 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-30 13:55:57 -07:00
Nikolaj Bjorner
5549301335 remove unreachable code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-30 09:13:13 -07:00
Nikolaj Bjorner
b019477378 add cofactoring functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-30 09:11:42 -07:00
Nikolaj Bjorner
1defbc8aa4 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-06-30 01:05:42 -04:00
Nikolaj Bjorner
a374e739f1 prepare for tuned viable sets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-30 01:05:34 -04:00
Jakob Rath
3436b52c4a
Polysat: refactor constraints (#5372) 
* Refactor: remove sign and dep from constraint

* fix some bugs

* improve log messages

* Add missing premises to lemma

* Rename getter in an attempt to fix linux build
 2021-06-25 11:04:25 -07:00
Nikolaj Bjorner
a0b0c1f428 with a fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-23 17:50:33 -07:00
Nikolaj Bjorner
4f0ec82957 functionally complete viable, needs to be debugged 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-23 17:44:52 -07:00
Nikolaj Bjorner
db242c28c6 make it C++17 friendly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-23 15:20:59 -07:00
Jakob Rath
20a5baeb70
Polysat: expand conflict explanation rules (#5366) 
* update example to match slides

* Add normalized view of inequalities

* workaround

* Add a conflict explanation rule

* unit clauses should be asserted at the base level

* Add src constraint to interval

* support non-strict case in first rule

* print conflict constraints only once

* update second rule

* update third rule as well
 2021-06-23 10:12:39 -07:00
Nikolaj Bjorner
dec37aee34 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-22 21:01:17 -07:00
Nikolaj Bjorner
01c81405af remove var-constraint alltogether 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-22 20:58:32 -07:00
Nikolaj Bjorner
b9719768a0 more viable scaffolding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-22 20:55:56 -07:00
Nikolaj Bjorner
8f0c408c0a prepare for new viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-22 20:44:21 -07:00
Jakob Rath
d7b8ea2f7f
Polysat: minor fixes (#5364) 
* update include paths

* bdd fixes

* update/fix some tests

* work around assertion failure when constraint from clause becomes unit

* Remove old code

* use clause_builder

* Verify model when returning SAT

* log

* fix
 2021-06-22 09:27:18 -07:00
Nikolaj Bjorner
52eb473c63 prepare viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-21 21:55:20 -07:00
Nikolaj Bjorner
17294f63b2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-21 21:22:30 -07:00
Nikolaj Bjorner
f18dccebc2 move tbv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-21 21:12:46 -07:00
Nikolaj Bjorner
ce5c8b3066 rename to some saner name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-21 16:19:37 -07:00
Nikolaj Bjorner
63f3c841d8 remove var_constraint to get rid of bdd dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-21 16:14:30 -07:00
Nikolaj Bjorner
9173306adc na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-21 16:00:13 -07:00
Nikolaj Bjorner
6f93ed8dc2 moving out viable functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-21 15:50:04 -07:00
Nikolaj Bjorner
19099244c4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-20 12:38:20 -07:00
Nikolaj Bjorner
4fad0385de tune multiplication slightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-20 11:07:06 -07:00
Nikolaj Bjorner
2522c8b53d display statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-20 10:29:27 -07:00
Nikolaj Bjorner
d78313e001 more pp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-20 10:13:59 -07:00
Nikolaj Bjorner
4066087138 pretty printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-20 09:49:31 -07:00
Nikolaj Bjorner
4bcfcecbbb fix initialization/finalization order for bdd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-19 23:11:06 -07:00
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
4405fa1156 add handling of misc operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-18 14:30:56 -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
d72724f7fd merge master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-18 10:04:38 -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
Nikolaj Bjorner
2138ef2ad0 build 2021-06-17 11:26:12 -07:00
Nikolaj Bjorner
93a4939d49 #5336 2021-06-17 11:15:37 -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
Nikolaj Bjorner
2174bccdba #5336 2021-06-17 00:45:52 -05:00
Nikolaj Bjorner
d016cb1da5 #5336 2021-06-16 23:57:44 -05:00
Nikolaj Bjorner
9038dfd30d #5336 2021-06-16 23:27:26 -05:00
Nikolaj Bjorner
d73ceaddc7 #5336 2021-06-16 23:19:16 -05:00
Nikolaj Bjorner
0b3a8522ac #5336 2021-06-16 21:57:46 -05:00
Nikolaj Bjorner
1dedfe3164 #5336 2021-06-16 21:24:50 -05:00
Nikolaj Bjorner
df9084ba23 #5336 2021-06-16 19:12:50 -05:00
Nikolaj Bjorner
3311bd074f #5336 2021-06-16 18:42:44 -05:00
Nikolaj Bjorner
6b5680f13e #5336 2021-06-16 18:42:19 -05:00
Nikolaj Bjorner
38fc97d18c #5336 2021-06-16 17:47:49 -05:00
Nikolaj Bjorner
29a2838bc9 #5338 #5349 2021-06-16 16:01:42 -05:00