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

18122 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
b581cbf062 add lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-17 18:25:21 -08:00
Jakob Rath
bf92fa4882 clause_iterator 2022-12-16 15:21:32 +01:00
Jakob Rath
342774eff8 test_ineq_non_axiom4 is slow but doesn't block anymore 2022-12-16 15:02:04 +01:00
Jakob Rath
75a64975b5 test 2022-12-16 15:00:50 +01:00
Jakob Rath
3e6e1e1a8a test 2022-12-16 14:37:31 +01:00
Jakob Rath
ca373836af Merge remote-tracking branch 'origin/polysat' into polysat 2022-12-16 14:26:38 +01:00
Jakob Rath
3b3636b30e Remove conflict::set 2022-12-16 14:25:41 +01:00
Jakob Rath
06e6f27614 refactor 2022-12-16 14:22:50 +01:00
Jakob Rath
9f05f645c1 update types and docs 2022-12-16 13:16:55 +01:00
Jakob Rath
c54c564019 convert to loop 2022-12-16 13:11:20 +01:00
Jakob Rath
e23774a746 reorder definitions 2022-12-16 13:06:16 +01:00
Jakob Rath
afde0e993c Add bitblasting fallback to viable::query 
(integration between conflict/viable is still messy)
 2022-12-16 13:02:54 +01:00
Jakob Rath
44cb528300 Extract usolver 2022-12-16 10:46:57 +01:00
Jakob Rath
5d7833e65e Warn on unused result (mainly for substitution::add) 2022-12-16 10:28:57 +01:00
Clemens Eisenhofer
d5bc4b84a7 Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat 2022-12-16 10:14:10 +01:00
Clemens Eisenhofer
71211f3134 Some bugfixes and unit-tests for variable elimination 2022-12-16 10:12:34 +01:00
Jakob Rath
8a5f1af3d1 univariate::find_max 2022-12-15 15:59:15 +01:00
Jakob Rath
31e0add966 univariate::find_min 2022-12-15 15:51:29 +01:00
Jakob Rath
37536425f4 Encode 2^k*x as (bvshl x k) in the fallback solver 2022-12-15 14:03:42 +01:00
Jakob Rath
06a999e219 skip diseq when not using polysat 2022-12-15 13:46:10 +01:00
Jakob Rath
a6504785b5 print bitblasted constraints 2022-12-15 13:43:23 +01:00
Jakob Rath
5de0007157 very basic refinement loop breaking 2022-12-15 13:39:48 +01:00
Jakob Rath
3d06a90e7f track refinement source 2022-12-15 13:08:13 +01:00
Jakob Rath
e978e4fc8e Strengthen umul_ovfl lemma 2022-12-14 11:07:16 +01:00
Clemens Eisenhofer
dc95179ae5 Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat 2022-12-14 10:39:15 +01:00
Jakob Rath
1bc4313333 Fix unsoundness in previous commit 2022-12-13 15:27:07 +01:00
Jakob Rath
7e7cea54f4 Intervals from equality constraints: remove superfluous side constraints 2022-12-13 15:02:45 +01:00
Jakob Rath
434e794790 test 2022-12-13 12:00:38 +01:00
Jakob Rath
519ebd8a8b log and note 2022-12-13 11:49:54 +01:00
Jakob Rath
a3c7a869cd bool_watch_invariant 2022-12-13 11:47:21 +01:00
Jakob Rath
6f1e4283bb Merge forbidden intervals for positive and negative equations 2022-12-13 11:42:52 +01:00
Nikolaj Bjorner
6c7f556496 activate non-overflow bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-12 20:11:01 -08:00
Nikolaj Bjorner
a5f12e9d57 add parity constraint for disequality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-12 19:40:19 -08:00
Jakob Rath
479e0e58ea Better intervals for equations 2022-12-12 18:18:24 +01:00
Jakob Rath
4a2379c23d Add unit test for refinement loop in bench6 2022-12-12 17:48:23 +01:00
Jakob Rath
eda6534453 more readable intervals 2022-12-12 16:41:18 +01:00
Jakob Rath
9f1f949d9d tests 2022-12-12 14:51:18 +01:00
Jakob Rath
917e1b6a4c When adding clauses, prioritize bool-propagation over evaluation 
See test_band1 and clause:  v2 == v0 & v1  -->  v2 <= 0
 2022-12-12 14:48:13 +01:00
Jakob Rath
587e77648a Keep value_propagate for now 2022-12-12 13:57:30 +01:00
Jakob Rath
759d8f2a94 Fix watching of boolean literals 2022-12-12 13:50:15 +01:00
Jakob Rath
1eb8eb560b test_ineq2 2022-12-12 13:37:28 +01:00
Jakob Rath
b1271ac7fb Check for missed boolean propagations 2022-12-12 11:52:45 +01:00
Jakob Rath
9feefa4c0a Remove clause methods that should not be used 2022-12-12 11:47:27 +01:00
Nikolaj Bjorner
5a27ae6b53 disable tangent lemma, which appears to be counter-productive 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-11 12:56:21 -08:00
Nikolaj Bjorner
d092523733 bugfixes to try_factor_equality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-10 10:51:21 -08:00
Nikolaj Bjorner
c27bd0d650 added try_factor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-09 14:58:37 -08:00
Nikolaj Bjorner
6e886114f9 add parity4 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-09 09:56:47 -08:00
Nikolaj Bjorner
707577644f assignment -> assignment_t for build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-09 09:33:24 -08:00
Nikolaj Bjorner
57f2d72fe2 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-09 09:26:40 -08:00
Jakob Rath
8d13446537 Solve boolean skeleton first 2022-12-09 17:22:51 +01:00