mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Add notes from discussion

Browse source
This commit is contained in:
Jakob Rath 2021-09-14 15:45:17 +02:00
parent 34631d972d
commit 4b3af1d0a4
1 changed files with 11 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/test/polysat.cpp
View file

@ -706,6 +706,17 @@ namespace polysat {
* *
* The original version had signed comparisons but that doesn't matter for the UNSAT result. * The original version had signed comparisons but that doesn't matter for the UNSAT result.
* UNSAT can be seen easily by substituting the equality. * UNSAT can be seen easily by substituting the equality.
*
* Possible ways to solve:
* - Integrate AC congruence closure
* See: Deepak Kapur. A Modular Associative Commutative (AC) Congruence Closure Algorithm, FSCD 2021. https://doi.org/10.4230/LIPIcs.FSCD.2021.15
* - Propagate equalities as substitutions
* x=t /\ p(x) ==> p(t)
* Ackermann-like reduction
* (index, watch lists over boolean literals)
* - Augment explain:
* conflict: y=x+1 /\ y^2 > z
* explain could then derive (x+1)^2 > z
*/ */
static void test_subst(unsigned bw = 32) { static void test_subst(unsigned bw = 32) {
scoped_solver s(__func__); scoped_solver s(__func__);