mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-15 04:00:19 +00:00
Code Activity
18867 commits 35 branches 52 tags 174 MiB
Commit graph

1097 commits

Author SHA1 Message Date
Clemens Eisenhofer
578f2ec4e8 Assertions 2023-02-18 14:26:45 +01:00
Clemens Eisenhofer
e8b4875a17 Multiply by inverse to detect more parity constraints 2023-02-18 14:15:51 +01:00
Clemens Eisenhofer
ae70a8e9f0 Blast only one bit per conflict 2023-02-17 17:26:19 +01:00
Clemens Eisenhofer
a6fbd71c6b Bugfixes 2023-02-17 17:06:28 +01:00
Clemens Eisenhofer
d976251390 Removed debug output 2023-02-17 15:42:14 +01:00
Clemens Eisenhofer
3f8edb9aac Contract bit information to large unit-intervals 2023-02-17 15:32:43 +01:00
Clemens Eisenhofer
0dae2d40b5 Prefer larger masks for justifications 2023-02-16 07:31:13 +01:00
Clemens Eisenhofer
5fbfa0be8f Moved quick-check out of the refinement loop 2023-02-16 07:21:17 +01:00
Clemens Eisenhofer
5ddc727f91 Do a quick check for feasibility w.r.t. bits before using forbidden intervals 2023-02-15 20:06:13 +01:00
Jakob Rath
5a45f81d44 lit_pp 2023-02-14 09:36:56 +01:00
Jakob Rath
b0e7852c9c Upgrade bool_watch_invariant 2023-02-14 09:35:56 +01:00
Nikolaj Bjorner
e07c77e072 remove redundant pre-condition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-13 11:54:50 -08:00
Nikolaj Bjorner
4f9b277c32 more code review 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-13 11:48:19 -08:00
Nikolaj Bjorner
49b733c562 more code review 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-13 11:47:46 -08:00
Nikolaj Bjorner
bcbb39f8e5 adding cr comments in variable-elimination 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-13 10:26:51 -08:00
Nikolaj Bjorner
2f86d9de75 bypass assertion violation for parity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-09 16:33:30 -08:00
Clemens Eisenhofer
6b48b25beb Draft: Made division/remainder to op_constraints (not yet used - old code still called) 2023-02-09 23:36:15 +01:00
Jakob Rath
4813fcfe0d re-propagate needs to be checked for all literals 2023-02-09 19:06:16 +01:00
Nikolaj Bjorner
e31eb9a6b1 add monotonicity lemma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-09 09:31:43 -08:00
Jakob Rath
c60a2b10a5 inequality::rewrite_equiv 2023-02-09 16:33:59 +01:00
Jakob Rath
06cc15d1cc refinement loop output 2023-02-09 16:28:52 +01:00
Jakob Rath
a0f5386bdd Use parity helper functions 2023-02-08 15:11:39 +01:00
Jakob Rath
bf03886a87 elem 2023-02-07 09:57:32 +01:00
Jakob Rath
984e98c88f Avoid duplicates 2023-02-06 17:52:52 +01:00
Jakob Rath
a37536e0ae clarify unsat_core 2023-02-06 17:52:52 +01:00
Jakob Rath
c79a16db2a Fix dependency tracking for input boolean conflicts 2023-02-06 16:28:41 +01:00
Jakob Rath
d7797a53df temporary fix 2023-02-06 11:34:28 +01:00
Nikolaj Bjorner
b45f42133d updates to try_div_monotonicity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-04 15:55:14 -08:00
Jakob Rath
539a4e4eae less eval 2023-02-03 17:43:07 +01:00
Jakob Rath
1a733a3a50 compute polysat unsat core 2023-02-03 17:37:09 +01:00
Jakob Rath
579275a17d cleanup 2023-02-03 16:33:02 +01:00
Jakob Rath
4b1ec583ec Remove outdated assertion 2023-02-03 16:07:58 +01:00
Jakob Rath
63416dbcd7 fix 2023-02-03 15:59:26 +01:00
Jakob Rath
6365e322f3 Try to propagate boolean decisions after backjumping 2023-02-03 15:56:19 +01:00
Jakob Rath
5678c1c592 We need more clause names 2023-02-03 15:54:56 +01:00
Jakob Rath
bdf20f513b debug 2023-02-03 11:18:11 +01:00
Clemens Eisenhofer
ae41f82939 Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat 2023-02-03 07:15:58 +01:00
Clemens Eisenhofer
c042505c34 Another monotonicity lemma 2023-02-03 07:15:10 +01:00
Jakob Rath
2dc93116e5 cleanup pdecide 2023-02-02 13:28:28 +01:00
Jakob Rath
5589d3389d Drop assign_verify 2023-02-02 13:22:10 +01:00
Jakob Rath
40519c70aa fix includes 2023-02-01 17:00:26 +01:00
Jakob Rath
53bbb49031 Restore mod_interval for fixplex 2023-02-01 16:34:25 +01:00
Clemens Eisenhofer
4648c35a35 Missing file 2023-02-01 15:10:47 +01:00
Jakob Rath
fe164c843d Fix/simplify constraint_manager::watch 2023-02-01 15:02:56 +01:00
Jakob Rath
0d56edb65c Fix missing boolean propagation after boolean conflict 
Usually in SAT solving, the conflict clause has at least two false literals at the max level (otherwise, the last literal would have been propagated at an earlier level).
But here we are adding clauses on demand; so after backtracking we may have the case that the conflict clause has exactly one undefined literal that must be propagated explicitly.
 2023-02-01 15:02:56 +01:00
Clemens Eisenhofer
783bd60598 Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat 2023-02-01 11:28:15 +01:00
Clemens Eisenhofer
8db575ea3b Division monotonicity 2023-02-01 11:27:46 +01:00
Jakob Rath
975fb25221 Fix to bench15 bug was unsound 2023-02-01 11:17:29 +01:00
Jakob Rath
f0625b604a Promote assertions to release mode 2023-02-01 11:12:13 +01:00
Jakob Rath
576e0b70b2 stub for conflict::find_deps 2023-02-01 10:53:49 +01:00