3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-11 09:20:44 -07:00
parent 1197c4d416
commit 008f88ae1c
2 changed files with 23 additions and 10 deletions

View file

@ -151,7 +151,7 @@ def propagate_conflict(core):
sys.stdout.write("if (")
sys.stdout.write(core2pred(core))
sys.stdout.write(f")\n")
sys.stdout.write(f" return conflict({deps}), false;\n")
sys.stdout.write(f" return conflict(i, {deps}), false;\n")
sys.stdout.flush()
lows = [BitVecVal(0, nb), l, k, i, j, k + 1, i + 1]
@ -361,7 +361,7 @@ def test_le(ineq, lov, hiv, low, hiw):
bounds = [0, 1, 2, 3, 10, 2**nb - 3, 2**nb - 2, 2**nb - 1]
def search_dual(p):
def search_dual_loop(p):
for i in bounds:
for j in bounds:
for k in bounds:
@ -369,15 +369,17 @@ def search_dual(p):
test_le(p, i, j, k, l)
s0.push()
s1.push()
print("strict")
search_dual(ULT(v, w))
s0.pop()
s1.pop()
def search_dual():
s0.push()
s1.push()
print("strict")
search_dual_loop(ULT(v, w))
s0.pop()
s1.pop()
print("non-strict")
search_dual_loop(ULE(v, w))
print("non-strict")
search_dual(ULE(v, w))
search_dual()
# Sketch v-next approach that

View file

@ -1219,6 +1219,17 @@ namespace polysat {
* Explore an efficient way to propagate with the following idea:
* For odd c, multiply row by inverse of c and accumulate similar
* propagation.
*
* Conflicts spanning multiple rows are TBD:
* Idea could be similar to conflicts for inequality propagation.
* - create a stack of variables that get tightened.
* - walk over every row that contains the top variable on the stack
* - perform bounds propagation for the currently examined row
* - put newly tightened variables from row on the top of the stack
* - if a variable occurs already on the stack determine if the rows on the
* stack resolve into a conflict.
*
* TBD: Combination of inequality and row propagation?
*/
template<typename Ext>