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
Nikolaj Bjorner
7afcaa5364
update doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-12 18:56:21 -08:00
Nikolaj Bjorner
e648e68d36
add doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-12 17:29:58 -08:00
Duncan Ogilvie
e82c8e78ae
Fix a compilation error with clang-cl (VS2022) ( #6489 )
2022-12-12 22:12:31 +00:00
Nikolaj Bjorner
aded8e5bf4
fix #6488
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-12 11:40:59 -08:00
Nikolaj Bjorner
4598af70c8
fix #6488
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-12 11:04:46 -08:00
Nikolaj Bjorner
a3e6885680
fix #6488
2022-12-12 09:50:44 -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
039de6a2c8
build issues
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-11 15:05:13 -08:00
Nuno Lopes
cb8603177e
fix build
2022-12-11 22:17:11 +00:00
Nuno Lopes
d308b8f555
simplify code + remove unused file
2022-12-11 22:11:19 +00:00
Nikolaj Bjorner
6b60a3dbed
fix syntax
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-11 14:06:08 -08:00
Nikolaj Bjorner
2520dcb04b
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-11 14:03:22 -08:00
Nuno Lopes
2d43ccc4c6
Revert "fix crashes in elim-uncnstr2"
...
This reverts commit a302c2f15e
2022-12-11 21:37:25 +00: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
6a1b3f7344
move debug output to before state update
2022-12-11 12:51:46 -08:00
Nikolaj Bjorner
f7269bb60a
update doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-11 10:16:17 -08:00
Nikolaj Bjorner
a9f52b0069
doc fixes
2022-12-11 10:04:01 -08:00
Nikolaj Bjorner
527fb18366
add doc for card2bv
2022-12-11 09:51:49 -08:00
Nuno Lopes
a302c2f15e
fix crashes in elim-uncnstr2
...
This would crash before:
(declare-fun x () (_ BitVec 4))
(assert (not (bvule x #x1)))
(apply elim-uncnstr2)
That's because the index_set iterator was querying qtail to compute the end of the iteration
But the problem is that elim-uncnstr2 may add new fmls to the goal, as in this case.
The bvule is replaced with an 'or', but since it's negated, it turns into 2 goals
Solve the issue by freezing the qtail for the iteration loop.
This is the right behavior for elim-uncnstr2, as it can't rewrite exprs that haven't been analyzed before
@NikolajBjorner please check if this the right behavior for the other simplifiers. Thank you
2022-12-11 15:21:23 +00: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
Nikolaj Bjorner
ee307dd84f
Merge branch 'master' of https://github.com/z3prover/z3
2022-12-09 08:50:46 -08:00
Nikolaj Bjorner
1434c7d394
#6059
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-09 08:50:32 -08:00
Jakob Rath
8d13446537
Solve boolean skeleton first
2022-12-09 17:22:51 +01:00
Nuno Lopes
9ebacd87e2
fix buggy mask (typo in my last commit..)
2022-12-09 16:16:52 +00:00
Nikolaj Bjorner
e716e507d9
investigate bench4
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-09 08:14:42 -08:00
Nikolaj Bjorner
96a2c04026
fix bug reported by Nuno
...
qhead should not be changed after tactic execution. It should remain 0 so the same tactic can be applied repeatedly on the entire state
2022-12-09 07:57:06 -08:00
Nuno Lopes
a96f5a9b42
fix overflow in mpz::bitwise_not
2022-12-09 11:59:39 +00:00
Nuno Lopes
c6f9c09d70
cleanup more in dependent_expr_state_tactic to reduce mem consumption
2022-12-09 11:34:53 +00:00
Nikolaj Bjorner
a6b49d8b4e
provide access to saturation for selected constraints
2022-12-08 19:17:35 -08:00
Nuno Lopes
ca6fed8b25
minor code simplification
2022-12-08 18:20:46 +00:00
Nikolaj Bjorner
33902c7c9e
fix parity propagation code, add tail-spin unit tests. The unit tests diverge because conflict resolution removes conflicting literals from the conflict clause before the decision variable gets processed. We have to change how conflict resolution is processed for such conflict clauses
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-08 09:57:38 -08:00
Jakob Rath
3c8718615a
yes, no need for plugins to be mutually exclusive
2022-12-08 16:19:11 +01:00
Jakob Rath
5ad961029d
Rename revert_decision -> revert_pvar, and enable it.
...
Also rename resolve_with_assignment to resolve_evaluated
2022-12-08 16:19:11 +01:00
Jakob Rath
676aa81c5a
Fix test_ineq2
2022-12-08 16:19:11 +01:00
Jakob Rath
a81e05e660
We shouldn't assume that v is assigned
...
Happens if it is a viable conflict for v
2022-12-08 16:19:11 +01:00
