mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

sketch vnext

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-10 12:25:30 -07:00
parent c1365b6ba8
commit 1197c4d416
1 changed files with 15 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

16
scripts/fixplex.py
View file

@ -380,4 +380,18 @@ print("non-strict")
search_dual(ULE(v, w))
# Sketch v-next approach that
# Maintain a transition relation T(B0, B1)
# where B := (lo(v), hi(v), lo(w), hi(w)) are variables.
# Initially T is B0 = B1
# Enumerate representative values of B0
# Enumerate solutions for T(B0, B1) given value for B0
# Check if B & v < w and v = lo(v) is unsat (similar to w = lo(w), v = hi(v)-1, )
# If it is unsat then find predicate cover P for B1
# B1 |= P,
# * P & v < w & not in_bounds(v, lo(v)', hi(v)') is unsat
# where lo(v)', hi(v)' is a tightest bound under B1
# Update T by adding transition (P => B2 = lo(v)', hi(v)', lo(w), hi(w)) & (~P => B2 = B1)
# * P & v < w is unsat
# Update T by adding not P
#