mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
14f3ff0b63
15 changed files with 875 additions and 94 deletions
|
|
@ -254,6 +254,15 @@ elseif (CYGWIN)
|
|||
elseif (WIN32)
|
||||
message(STATUS "Platform: Windows")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS")
|
||||
elseif (EMSCRIPTEN)
|
||||
message(STATUS "Platform: Emscripten")
|
||||
list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS
|
||||
"-Os"
|
||||
"-s ALLOW_MEMORY_GROWTH=1"
|
||||
"-s ASSERTIONS=0"
|
||||
"-s DISABLE_EXCEPTION_CATCHING=0"
|
||||
"-s ERROR_ON_UNDEFINED_SYMBOLS=1"
|
||||
)
|
||||
else()
|
||||
message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised")
|
||||
endif()
|
||||
|
|
|
|||
|
|
@ -394,76 +394,4 @@ test("data/horn2.smt2")
|
|||
test("data/horn3.smt2")
|
||||
test("data/horn4.smt2")
|
||||
test("data/horn5.smt2")
|
||||
test("data/horn6.smt2")
|
||||
|
||||
|
||||
|
||||
"""
|
||||
# TBD: Quip variant of IC3
|
||||
|
||||
must = True
|
||||
may = False
|
||||
|
||||
class QGoal:
|
||||
def __init__(self, cube, parent, level, must):
|
||||
self.level = level
|
||||
self.cube = cube
|
||||
self.parent = parent
|
||||
self.must = must
|
||||
|
||||
class Quip(MiniIC3):
|
||||
|
||||
# prev & tras -> r', such that r' intersects with cube
|
||||
def add_reachable(self, prev, cube):
|
||||
s = fd_solver()
|
||||
s.add(self.trans)
|
||||
s.add(prev)
|
||||
s.add(Or(cube))
|
||||
is_sat = s.check()
|
||||
assert is_sat == sat
|
||||
m = s.model();
|
||||
result = self.values2literals(m, cube)
|
||||
assert result
|
||||
self.reachable.add(result)
|
||||
|
||||
# A state s0 and level f0 such that
|
||||
# not(s0) is f0-1 inductive
|
||||
def quip_blocked(self, s0, f0):
|
||||
self.push_heap(QGoal(self.next(s0), None, f0, must))
|
||||
while self.goals:
|
||||
f, g = heapq.heappop(self.goals)
|
||||
sys.stdout.write("%d." % f)
|
||||
sys.stdout.flush()
|
||||
if f == 0:
|
||||
if g.must:
|
||||
print("")
|
||||
return g
|
||||
self.add_reachable(self.init, p.parent.cube)
|
||||
continue
|
||||
|
||||
# TBD
|
||||
return None
|
||||
|
||||
|
||||
def run(self):
|
||||
if not check_disjoint(self.init, self.bad):
|
||||
return "goal is reached in initial state"
|
||||
level = 0
|
||||
while True:
|
||||
inv = self.is_valid()
|
||||
if inv is not None:
|
||||
return inv
|
||||
is_sat, cube = self.unfold()
|
||||
if is_sat == unsat:
|
||||
level += 1
|
||||
print("Unfold %d" % level)
|
||||
sys.stdout.flush()
|
||||
self.add_solver()
|
||||
elif is_sat == sat:
|
||||
cex = self.quipie_blocked(cube, level)
|
||||
if cex is not None:
|
||||
return cex
|
||||
else:
|
||||
return is_sat
|
||||
|
||||
"""
|
||||
# test("data/horn6.smt2") # takes long time to finish
|
||||
|
|
|
|||
786
examples/python/mini_quip.py
Normal file
786
examples/python/mini_quip.py
Normal file
|
|
@ -0,0 +1,786 @@
|
|||
from z3 import *
|
||||
import heapq
|
||||
import numpy
|
||||
import time
|
||||
import random
|
||||
|
||||
verbose = True
|
||||
|
||||
# Simplistic (and fragile) converter from
|
||||
# a class of Horn clauses corresponding to
|
||||
# a transition system into a transition system
|
||||
# representation as <init, trans, goal>
|
||||
# It assumes it is given three Horn clauses
|
||||
# of the form:
|
||||
# init(x) => Invariant(x)
|
||||
# Invariant(x) and trans(x,x') => Invariant(x')
|
||||
# Invariant(x) and goal(x) => Goal(x)
|
||||
# where Invariant and Goal are uninterpreted predicates
|
||||
|
||||
class Horn2Transitions:
|
||||
def __init__(self):
|
||||
self.trans = True
|
||||
self.init = True
|
||||
self.inputs = []
|
||||
self.goal = True
|
||||
self.index = 0
|
||||
|
||||
def parse(self, file):
|
||||
fp = Fixedpoint()
|
||||
goals = fp.parse_file(file)
|
||||
for r in fp.get_rules():
|
||||
if not is_quantifier(r):
|
||||
continue
|
||||
b = r.body()
|
||||
if not is_implies(b):
|
||||
continue
|
||||
f = b.arg(0)
|
||||
g = b.arg(1)
|
||||
if self.is_goal(f, g):
|
||||
continue
|
||||
if self.is_transition(f, g):
|
||||
continue
|
||||
if self.is_init(f, g):
|
||||
continue
|
||||
|
||||
def is_pred(self, p, name):
|
||||
return is_app(p) and p.decl().name() == name
|
||||
|
||||
def is_goal(self, body, head):
|
||||
if not self.is_pred(head, "Goal"):
|
||||
return False
|
||||
pred, inv = self.is_body(body)
|
||||
if pred is None:
|
||||
return False
|
||||
self.goal = self.subst_vars("x", inv, pred)
|
||||
self.goal = self.subst_vars("i", self.goal, self.goal)
|
||||
self.inputs += self.vars
|
||||
self.inputs = list(set(self.inputs))
|
||||
return True
|
||||
|
||||
def is_body(self, body):
|
||||
if not is_and(body):
|
||||
return None, None
|
||||
fmls = [f for f in body.children() if self.is_inv(f) is None]
|
||||
inv = None
|
||||
for f in body.children():
|
||||
if self.is_inv(f) is not None:
|
||||
inv = f;
|
||||
break
|
||||
return And(fmls), inv
|
||||
|
||||
def is_inv(self, f):
|
||||
if self.is_pred(f, "Invariant"):
|
||||
return f
|
||||
return None
|
||||
|
||||
def is_transition(self, body, head):
|
||||
pred, inv0 = self.is_body(body)
|
||||
if pred is None:
|
||||
return False
|
||||
inv1 = self.is_inv(head)
|
||||
if inv1 is None:
|
||||
return False
|
||||
pred = self.subst_vars("x", inv0, pred)
|
||||
self.xs = self.vars
|
||||
pred = self.subst_vars("xn", inv1, pred)
|
||||
self.xns = self.vars
|
||||
pred = self.subst_vars("i", pred, pred)
|
||||
self.inputs += self.vars
|
||||
self.inputs = list(set(self.inputs))
|
||||
self.trans = pred
|
||||
return True
|
||||
|
||||
def is_init(self, body, head):
|
||||
for f in body.children():
|
||||
if self.is_inv(f) is not None:
|
||||
return False
|
||||
inv = self.is_inv(head)
|
||||
if inv is None:
|
||||
return False
|
||||
self.init = self.subst_vars("x", inv, body)
|
||||
return True
|
||||
|
||||
def subst_vars(self, prefix, inv, fml):
|
||||
subst = self.mk_subst(prefix, inv)
|
||||
self.vars = [ v for (k,v) in subst ]
|
||||
return substitute(fml, subst)
|
||||
|
||||
def mk_subst(self, prefix, inv):
|
||||
self.index = 0
|
||||
if self.is_inv(inv) is not None:
|
||||
return [(f, self.mk_bool(prefix)) for f in inv.children()]
|
||||
else:
|
||||
vars = self.get_vars(inv)
|
||||
return [(f, self.mk_bool(prefix)) for f in vars]
|
||||
|
||||
def mk_bool(self, prefix):
|
||||
self.index += 1
|
||||
return Bool("%s%d" % (prefix, self.index))
|
||||
|
||||
def get_vars(self, f, rs=[]):
|
||||
if is_var(f):
|
||||
return z3util.vset(rs + [f], str)
|
||||
else:
|
||||
for f_ in f.children():
|
||||
rs = self.get_vars(f_, rs)
|
||||
return z3util.vset(rs, str)
|
||||
|
||||
# Produce a finite domain solver.
|
||||
# The theory QF_FD covers bit-vector formulas
|
||||
# and pseudo-Boolean constraints.
|
||||
# By default cardinality and pseudo-Boolean
|
||||
# constraints are converted to clauses. To override
|
||||
# this default for cardinality constraints
|
||||
# we set sat.cardinality.solver to True
|
||||
|
||||
def fd_solver():
|
||||
s = SolverFor("QF_FD")
|
||||
s.set("sat.cardinality.solver", True)
|
||||
return s
|
||||
|
||||
|
||||
# negate, avoid double negation
|
||||
def negate(f):
|
||||
if is_not(f):
|
||||
return f.arg(0)
|
||||
else:
|
||||
return Not(f)
|
||||
|
||||
def cube2clause(cube):
|
||||
return Or([negate(f) for f in cube])
|
||||
|
||||
class State:
|
||||
def __init__(self, s):
|
||||
self.R = set([])
|
||||
self.solver = s
|
||||
|
||||
def add(self, clause):
|
||||
if clause not in self.R:
|
||||
self.R |= { clause }
|
||||
self.solver.add(clause)
|
||||
|
||||
def is_seq(f):
|
||||
return isinstance(f, list) or isinstance(f, tuple) or isinstance(f, AstVector)
|
||||
|
||||
# Check if the initial state is bad
|
||||
def check_disjoint(a, b):
|
||||
s = fd_solver()
|
||||
s.add(a)
|
||||
s.add(b)
|
||||
return unsat == s.check()
|
||||
|
||||
|
||||
# Remove clauses that are subsumed
|
||||
def prune(R):
|
||||
removed = set([])
|
||||
s = fd_solver()
|
||||
for f1 in R:
|
||||
s.push()
|
||||
for f2 in R:
|
||||
if f2 not in removed:
|
||||
s.add(Not(f2) if f1.eq(f2) else f2)
|
||||
if s.check() == unsat:
|
||||
removed |= { f1 }
|
||||
s.pop()
|
||||
return R - removed
|
||||
|
||||
# Quip variant of IC3
|
||||
|
||||
must = True
|
||||
may = False
|
||||
|
||||
class QLemma:
|
||||
def __init__(self, c):
|
||||
self.cube = c
|
||||
self.clause = cube2clause(c)
|
||||
self.bad = False
|
||||
|
||||
def __hash__(self):
|
||||
return hash(tuple(set(self.cube)))
|
||||
|
||||
def __eq__(self, qlemma2):
|
||||
if set(self.cube) == set(qlemma2.cube) and self.bad == qlemma2.bad:
|
||||
return True
|
||||
else:
|
||||
return False
|
||||
|
||||
def __ne__():
|
||||
if not self.__eq__(self, qlemma2):
|
||||
return True
|
||||
else:
|
||||
return False
|
||||
|
||||
|
||||
class QGoal:
|
||||
def __init__(self, cube, parent, level, must, encounter):
|
||||
self.level = level
|
||||
self.cube = cube
|
||||
self.parent = parent
|
||||
self.must = must
|
||||
|
||||
def __lt__(self, other):
|
||||
return self.level < other.level
|
||||
|
||||
|
||||
class QReach:
|
||||
|
||||
# it is assumed that there is a single initial state
|
||||
# with all latches set to 0 in hardware design, so
|
||||
# here init will always give a state where all variable are set to 0
|
||||
def __init__(self, init, xs):
|
||||
self.xs = xs
|
||||
self.constant_xs = [Not(x) for x in self.xs]
|
||||
s = fd_solver()
|
||||
s.add(init)
|
||||
is_sat = s.check()
|
||||
assert is_sat == sat
|
||||
m = s.model()
|
||||
# xs is a list, "for" will keep the order when iterating
|
||||
self.states = numpy.array([[False for x in self.xs]]) # all set to False
|
||||
assert not numpy.max(self.states) # since all element is False, so maximum should be False
|
||||
|
||||
# check if new state exists
|
||||
def is_exist(self, state):
|
||||
if state in self.states:
|
||||
return True
|
||||
return False
|
||||
|
||||
def enumerate(self, i, state_b, state):
|
||||
while i < len(state) and state[i] not in self.xs:
|
||||
i += 1
|
||||
if i >= len(state):
|
||||
if state_b.tolist() not in self.states.tolist():
|
||||
self.states = numpy.append(self.states, [state_b], axis = 0)
|
||||
return state_b
|
||||
else:
|
||||
return None
|
||||
state_b[i] = False
|
||||
if self.enumerate(i+1, state_b, state) is not None:
|
||||
return state_b
|
||||
else:
|
||||
state_b[i] = True
|
||||
return self.enumerate(i+1, state_b, state)
|
||||
|
||||
def is_full_state(self, state):
|
||||
for i in range(len(self.xs)):
|
||||
if state[i] in self.xs:
|
||||
return False
|
||||
return True
|
||||
|
||||
def add(self, cube):
|
||||
state = self.cube2partial_state(cube)
|
||||
assert len(state) == len(self.xs)
|
||||
if not self.is_exist(state):
|
||||
return None
|
||||
if self.is_full_state(state):
|
||||
self.states = numpy.append(self.states, [state], axis = 0)
|
||||
else:
|
||||
# state[i] is instance, state_b[i] is boolean
|
||||
state_b = numpy.array(state)
|
||||
for i in range(len(state)): # state is of same length as self.xs
|
||||
# i-th literal in state hasn't been assigned value
|
||||
# init un-assigned literals in state_b as True
|
||||
# make state_b only contain boolean value
|
||||
if state[i] in self.xs:
|
||||
state_b[i] = True
|
||||
else:
|
||||
state_b[i] = is_true(state[i])
|
||||
if self.enumerate(0, state_b, state) is not None:
|
||||
lits_to_remove = set([negate(f) for f in list(set(cube) - set(self.constant_xs))])
|
||||
self.constant_xs = list(set(self.constant_xs) - lits_to_remove)
|
||||
return state
|
||||
return None
|
||||
|
||||
|
||||
def cube2partial_state(self, cube):
|
||||
s = fd_solver()
|
||||
s.add(And(cube))
|
||||
is_sat = s.check()
|
||||
assert is_sat == sat
|
||||
m = s.model()
|
||||
state = numpy.array([m.eval(x) for x in self.xs])
|
||||
return state
|
||||
|
||||
|
||||
def state2cube(self, s):
|
||||
result = copy.deepcopy(self.xs) # x1, x2, ...
|
||||
for i in range(len(self.xs)):
|
||||
if not s[i]:
|
||||
result[i] = Not(result[i])
|
||||
return result
|
||||
|
||||
def intersect(self, cube):
|
||||
state = self.cube2partial_state(cube)
|
||||
mask = True
|
||||
for i in range(len(self.xs)):
|
||||
if is_true(state[i]) or is_false(state[i]):
|
||||
mask = (self.states[:, i] == state[i]) & mask
|
||||
intersects = numpy.reshape(self.states[mask], (-1, len(self.xs)))
|
||||
if intersects.size > 0:
|
||||
return And(self.state2cube(intersects[0])) # only need to return one single intersect
|
||||
return None
|
||||
|
||||
|
||||
class Quip:
|
||||
|
||||
def __init__(self, init, trans, goal, x0, inputs, xn):
|
||||
self.x0 = x0
|
||||
self.inputs = inputs
|
||||
self.xn = xn
|
||||
self.init = init
|
||||
self.bad = goal
|
||||
self.trans = trans
|
||||
self.min_cube_solver = fd_solver()
|
||||
self.min_cube_solver.add(Not(trans))
|
||||
self.goals = []
|
||||
s = State(fd_solver())
|
||||
s.add(init)
|
||||
s.solver.add(trans) # check if a bad state can be reached in one step from current level
|
||||
self.states = [s]
|
||||
self.s_bad = fd_solver()
|
||||
self.s_good = fd_solver()
|
||||
self.s_bad.add(self.bad)
|
||||
self.s_good.add(Not(self.bad))
|
||||
self.reachable = QReach(self.init, x0)
|
||||
self.frames = [] # frames is a 2d list, each row (representing level) is a set containing several (clause, bad) pairs
|
||||
self.count_may = 0
|
||||
|
||||
def next(self, f):
|
||||
if is_seq(f):
|
||||
return [self.next(f1) for f1 in f]
|
||||
return substitute(f, zip(self.x0, self.xn))
|
||||
|
||||
def prev(self, f):
|
||||
if is_seq(f):
|
||||
return [self.prev(f1) for f1 in f]
|
||||
return substitute(f, zip(self.xn, self.x0))
|
||||
|
||||
def add_solver(self):
|
||||
s = fd_solver()
|
||||
s.add(self.trans)
|
||||
self.states += [State(s)]
|
||||
|
||||
def R(self, i):
|
||||
return And(self.states[i].R)
|
||||
|
||||
def value2literal(self, m, x):
|
||||
value = m.eval(x)
|
||||
if is_true(value):
|
||||
return x
|
||||
if is_false(value):
|
||||
return Not(x)
|
||||
return None
|
||||
|
||||
def values2literals(self, m, xs):
|
||||
p = [self.value2literal(m, x) for x in xs]
|
||||
return [x for x in p if x is not None]
|
||||
|
||||
def project0(self, m):
|
||||
return self.values2literals(m, self.x0)
|
||||
|
||||
def projectI(self, m):
|
||||
return self.values2literals(m, self.inputs)
|
||||
|
||||
def projectN(self, m):
|
||||
return self.values2literals(m, self.xn)
|
||||
|
||||
|
||||
# Block a cube by asserting the clause corresponding to its negation
|
||||
def block_cube(self, i, cube):
|
||||
self.assert_clause(i, cube2clause(cube))
|
||||
|
||||
# Add a clause to levels 1 until i
|
||||
def assert_clause(self, i, clause):
|
||||
for j in range(1, i + 1):
|
||||
self.states[j].add(clause)
|
||||
assert str(self.states[j].solver) != str([False])
|
||||
|
||||
|
||||
# minimize cube that is core of Dual solver.
|
||||
# this assumes that props & cube => Trans
|
||||
# which means props & cube can only give us a Tr in Trans,
|
||||
# and it will never make !Trans sat
|
||||
def minimize_cube(self, cube, inputs, lits):
|
||||
# min_cube_solver has !Trans (min_cube.solver.add(!Trans))
|
||||
is_sat = self.min_cube_solver.check(lits + [c for c in cube] + [i for i in inputs])
|
||||
assert is_sat == unsat
|
||||
# unsat_core gives us some lits which make Tr sat,
|
||||
# so that we can ignore other lits and include more states
|
||||
core = self.min_cube_solver.unsat_core()
|
||||
assert core
|
||||
return [c for c in core if c in set(cube)]
|
||||
|
||||
# push a goal on a heap
|
||||
def push_heap(self, goal):
|
||||
heapq.heappush(self.goals, (goal.level, goal))
|
||||
|
||||
|
||||
# make sure cube to be blocked excludes all reachable states
|
||||
def check_reachable(self, cube):
|
||||
s = fd_solver()
|
||||
for state in self.reachable.states:
|
||||
s.push()
|
||||
r = self.reachable.state2cube(state)
|
||||
s.add(And(self.prev(r)))
|
||||
s.add(self.prev(cube))
|
||||
is_sat = s.check()
|
||||
s.pop()
|
||||
if is_sat == sat:
|
||||
# if sat, it means the cube to be blocked contains reachable states
|
||||
# so it is an invalid cube
|
||||
return False
|
||||
# if all fail, is_sat will be unsat
|
||||
return True
|
||||
|
||||
# Rudimentary generalization:
|
||||
# If the cube is already unsat with respect to transition relation
|
||||
# extract a core (not necessarily minimal)
|
||||
# otherwise, just return the cube.
|
||||
def generalize(self, cube, f):
|
||||
s = self.states[f - 1].solver
|
||||
if unsat == s.check(cube):
|
||||
core = s.unsat_core()
|
||||
if self.check_reachable(core):
|
||||
return core, f
|
||||
return cube, f
|
||||
|
||||
|
||||
def valid_reachable(self, level):
|
||||
s = fd_solver()
|
||||
s.add(self.init)
|
||||
for i in range(level):
|
||||
s.add(self.trans)
|
||||
for state in self.reachable.states:
|
||||
s.push()
|
||||
s.add(And(self.next(self.reachable.state2cube(state))))
|
||||
print self.reachable.state2cube(state)
|
||||
print s.check()
|
||||
s.pop()
|
||||
|
||||
def lemmas(self, level):
|
||||
return [(l.clause, l.bad) for l in self.frames[level]]
|
||||
|
||||
# whenever a new reachable state is found, we use it to mark some existing lemmas as bad lemmas
|
||||
def mark_bad_lemmas(self, new):
|
||||
s = fd_solver()
|
||||
reset = False
|
||||
for frame in self.frames:
|
||||
for lemma in frame:
|
||||
s.push()
|
||||
s.add(lemma.clause)
|
||||
is_sat = s.check(new)
|
||||
if is_sat == unsat:
|
||||
reset = True
|
||||
lemma.bad = True
|
||||
s.pop()
|
||||
if reset:
|
||||
self.states = [self.states[0]]
|
||||
for i in range(1, len(self.frames)):
|
||||
self.add_solver()
|
||||
for lemma in self.frames[i]:
|
||||
if not lemma.bad:
|
||||
self.states[i].add(lemma.clause)
|
||||
|
||||
# prev & tras -> r', such that r' intersects with cube
|
||||
def add_reachable(self, prev, cube):
|
||||
s = fd_solver()
|
||||
s.add(self.trans)
|
||||
s.add(prev)
|
||||
s.add(self.next(And(cube)))
|
||||
is_sat = s.check()
|
||||
assert is_sat == sat
|
||||
m = s.model()
|
||||
new = self.projectN(m)
|
||||
state = self.reachable.add(self.prev(new)) # always add as non-primed
|
||||
if state is not None: # if self.states do not have new state yet
|
||||
self.mark_bad_lemmas(self.prev(new))
|
||||
|
||||
|
||||
# Check if the negation of cube is inductive at level f
|
||||
def is_inductive(self, f, cube):
|
||||
s = self.states[f - 1].solver
|
||||
s.push()
|
||||
s.add(self.prev(Not(And(cube))))
|
||||
is_sat = s.check(cube)
|
||||
if is_sat == sat:
|
||||
m = s.model()
|
||||
s.pop()
|
||||
if is_sat == sat:
|
||||
cube = self.next(self.minimize_cube(self.project0(m), self.projectI(m), self.projectN(m)))
|
||||
elif is_sat == unsat:
|
||||
cube, f = self.generalize(cube, f)
|
||||
cube = self.next(cube)
|
||||
return cube, f, is_sat
|
||||
|
||||
|
||||
# Determine if there is a cube for the current state
|
||||
# that is potentially reachable.
|
||||
def unfold(self, level):
|
||||
core = []
|
||||
self.s_bad.push()
|
||||
R = self.R(level)
|
||||
self.s_bad.add(R) # check if current frame intersects with bad states, no trans
|
||||
is_sat = self.s_bad.check()
|
||||
if is_sat == sat:
|
||||
m = self.s_bad.model()
|
||||
cube = self.project0(m)
|
||||
props = cube + self.projectI(m)
|
||||
self.s_good.push()
|
||||
self.s_good.add(R)
|
||||
is_sat2 = self.s_good.check(props)
|
||||
assert is_sat2 == unsat
|
||||
core = self.s_good.unsat_core()
|
||||
assert core
|
||||
core = [c for c in core if c in set(cube)]
|
||||
self.s_good.pop()
|
||||
self.s_bad.pop()
|
||||
return is_sat, core
|
||||
|
||||
# A state s0 and level f0 such that
|
||||
# not(s0) is f0-1 inductive
|
||||
def quip_blocked(self, s0, f0):
|
||||
self.push_heap(QGoal(self.next(s0), None, f0, must, 0))
|
||||
while self.goals:
|
||||
f, g = heapq.heappop(self.goals)
|
||||
sys.stdout.write("%d." % f)
|
||||
if not g.must:
|
||||
self.count_may -= 1
|
||||
sys.stdout.flush()
|
||||
if f == 0:
|
||||
if g.must:
|
||||
s = fd_solver()
|
||||
s.add(self.init)
|
||||
s.add(self.prev(g.cube))
|
||||
# since init is a complete assignment, so g.cube must equal to init in sat solver
|
||||
assert is_sat == s.check()
|
||||
if verbose:
|
||||
print("")
|
||||
return g
|
||||
self.add_reachable(self.init, g.parent.cube)
|
||||
continue
|
||||
|
||||
r0 = self.reachable.intersect(self.prev(g.cube))
|
||||
if r0 is not None:
|
||||
if g.must:
|
||||
if verbose:
|
||||
print ""
|
||||
s = fd_solver()
|
||||
s.add(self.trans)
|
||||
# make it as a concrete reachable state
|
||||
# intersect returns an And(...), so use children to get cube list
|
||||
g.cube = r0.children()
|
||||
while True:
|
||||
is_sat = s.check(self.next(g.cube))
|
||||
assert is_sat == sat
|
||||
r = self.next(self.project0(s.model()))
|
||||
r = self.reachable.intersect(self.prev(r))
|
||||
child = QGoal(self.next(r.children()), g, 0, g.must, 0)
|
||||
g = child
|
||||
if not check_disjoint(self.init, self.prev(g.cube)):
|
||||
# g is init, break the loop
|
||||
break
|
||||
init = g
|
||||
while g.parent is not None:
|
||||
g.parent.level = g.level + 1
|
||||
g = g.parent
|
||||
return init
|
||||
if g.parent is not None:
|
||||
self.add_reachable(r0, g.parent.cube)
|
||||
continue
|
||||
|
||||
cube = None
|
||||
is_sat = sat
|
||||
f_1 = len(self.frames) - 1
|
||||
while f_1 >= f:
|
||||
for l in self.frames[f_1]:
|
||||
if not l.bad and len(l.cube) > 0 and set(l.cube).issubset(g.cube):
|
||||
cube = l.cube
|
||||
is_sat == unsat
|
||||
break
|
||||
f_1 -= 1
|
||||
if cube is None:
|
||||
cube, f_1, is_sat = self.is_inductive(f, g.cube)
|
||||
if is_sat == unsat:
|
||||
self.frames[f_1].add(QLemma(self.prev(cube)))
|
||||
self.block_cube(f_1, self.prev(cube))
|
||||
if f_1 < f0:
|
||||
# learned clause might also be able to block same bad states in higher level
|
||||
if set(list(cube)) != set(list(g.cube)):
|
||||
self.push_heap(QGoal(cube, None, f_1 + 1, may, 0))
|
||||
self.count_may += 1
|
||||
else:
|
||||
# re-queue g.cube in higher level, here g.parent is simply for tracking down the trace when output.
|
||||
self.push_heap(QGoal(g.cube, g.parent, f_1 + 1, g.must, 0))
|
||||
if not g.must:
|
||||
self.count_may += 1
|
||||
else:
|
||||
# qcube is a predecessor of g
|
||||
qcube = QGoal(cube, g, f_1 - 1, g.must, 0)
|
||||
if not g.must:
|
||||
self.count_may += 1
|
||||
self.push_heap(qcube)
|
||||
|
||||
if verbose:
|
||||
print("")
|
||||
return None
|
||||
|
||||
# Check if there are two states next to each other that have the same clauses.
|
||||
def is_valid(self):
|
||||
i = 1
|
||||
inv = None
|
||||
while True:
|
||||
# self.states[].R contains full lemmas
|
||||
# self.frames[] contains delta-encoded lemmas
|
||||
while len(self.states) <= i+1:
|
||||
self.add_solver()
|
||||
while len(self.frames) <= i+1:
|
||||
self.frames.append(set())
|
||||
duplicates = set([])
|
||||
for l in self.frames[i+1]:
|
||||
if l in self.frames[i]:
|
||||
duplicates |= {l}
|
||||
self.frames[i] = self.frames[i] - duplicates
|
||||
pushed = set([])
|
||||
for l in (self.frames[i] - self.frames[i+1]):
|
||||
if not l.bad:
|
||||
s = self.states[i].solver
|
||||
s.push()
|
||||
s.add(self.next(Not(l.clause)))
|
||||
s.add(l.clause)
|
||||
is_sat = s.check()
|
||||
s.pop()
|
||||
if is_sat == unsat:
|
||||
self.frames[i+1].add(l)
|
||||
self.states[i+1].add(l.clause)
|
||||
pushed |= {l}
|
||||
self.frames[i] = self.frames[i] - pushed
|
||||
if (not (self.states[i].R - self.states[i+1].R)
|
||||
and len(self.states[i].R) != 0):
|
||||
inv = prune(self.states[i].R)
|
||||
F_inf = self.frames[i]
|
||||
j = i + 1
|
||||
while j < len(self.states):
|
||||
for l in F_inf:
|
||||
self.states[j].add(l.clause)
|
||||
j += 1
|
||||
self.frames[len(self.states)-1] = F_inf
|
||||
self.frames[i] = set([])
|
||||
break
|
||||
elif (len(self.states[i].R) == 0
|
||||
and len(self.states[i+1].R) == 0):
|
||||
break
|
||||
i += 1
|
||||
|
||||
if inv is not None:
|
||||
self.s_bad.push()
|
||||
self.s_bad.add(And(inv))
|
||||
is_sat = self.s_bad.check()
|
||||
if is_sat == unsat:
|
||||
self.s_bad.pop()
|
||||
return And(inv)
|
||||
self.s_bad.pop()
|
||||
return None
|
||||
|
||||
def run(self):
|
||||
if not check_disjoint(self.init, self.bad):
|
||||
return "goal is reached in initial state"
|
||||
level = 0
|
||||
while True:
|
||||
inv = self.is_valid() # self.add_solver() here
|
||||
if inv is not None:
|
||||
return inv
|
||||
is_sat, cube = self.unfold(level)
|
||||
if is_sat == unsat:
|
||||
level += 1
|
||||
if verbose:
|
||||
print("Unfold %d" % level)
|
||||
sys.stdout.flush()
|
||||
elif is_sat == sat:
|
||||
cex = self.quip_blocked(cube, level)
|
||||
if cex is not None:
|
||||
return cex
|
||||
else:
|
||||
return is_sat
|
||||
|
||||
def test(file):
|
||||
h2t = Horn2Transitions()
|
||||
h2t.parse(file)
|
||||
if verbose:
|
||||
print("Test file: %s") % file
|
||||
mp = Quip(h2t.init, h2t.trans, h2t.goal, h2t.xs, h2t.inputs, h2t.xns)
|
||||
start_time = time.time()
|
||||
result = mp.run()
|
||||
end_time = time.time()
|
||||
if isinstance(result, QGoal):
|
||||
g = result
|
||||
if verbose:
|
||||
print("Trace")
|
||||
while g:
|
||||
if verbose:
|
||||
print(g.level, g.cube)
|
||||
g = g.parent
|
||||
print("--- used %.3f seconds ---" % (end_time - start_time))
|
||||
validate(mp, result, mp.trans)
|
||||
return
|
||||
if isinstance(result, ExprRef):
|
||||
if verbose:
|
||||
print("Invariant:\n%s " % result)
|
||||
print("--- used %.3f seconds ---" % (end_time - start_time))
|
||||
validate(mp, result, mp.trans)
|
||||
return
|
||||
print(result)
|
||||
|
||||
def validate(var, result, trans):
|
||||
if isinstance(result, QGoal):
|
||||
g = result
|
||||
s = fd_solver()
|
||||
s.add(trans)
|
||||
while g.parent is not None:
|
||||
s.push()
|
||||
s.add(var.prev(g.cube))
|
||||
s.add(var.next(g.parent.cube))
|
||||
assert sat == s.check()
|
||||
s.pop()
|
||||
g = g.parent
|
||||
if verbose:
|
||||
print "--- validation succeed ----"
|
||||
return
|
||||
if isinstance(result, ExprRef):
|
||||
inv = result
|
||||
s = fd_solver()
|
||||
s.add(trans)
|
||||
s.push()
|
||||
s.add(var.prev(inv))
|
||||
s.add(Not(var.next(inv)))
|
||||
assert unsat == s.check()
|
||||
s.pop()
|
||||
cube = var.prev(var.init)
|
||||
step = 0
|
||||
while True:
|
||||
step += 1
|
||||
# too many steps to reach invariant
|
||||
if step > 1000:
|
||||
if verbose:
|
||||
print "--- validation failed --"
|
||||
return
|
||||
if not check_disjoint(var.prev(cube), var.prev(inv)):
|
||||
# reach invariant
|
||||
break
|
||||
s.push()
|
||||
s.add(cube)
|
||||
assert s.check() == sat
|
||||
cube = var.projectN(s.model())
|
||||
s.pop()
|
||||
if verbose:
|
||||
print "--- validation succeed ----"
|
||||
return
|
||||
|
||||
|
||||
|
||||
test("data/horn1.smt2")
|
||||
test("data/horn2.smt2")
|
||||
test("data/horn3.smt2")
|
||||
test("data/horn4.smt2")
|
||||
test("data/horn5.smt2")
|
||||
# test("data/horn6.smt2") # not able to finish
|
||||
|
|
@ -8,6 +8,7 @@
|
|||
# You should **not** import ``mk_util`` here
|
||||
# to avoid having this code depend on the
|
||||
# of the Python build system.
|
||||
import io
|
||||
import os
|
||||
import pprint
|
||||
import logging
|
||||
|
|
@ -622,7 +623,7 @@ def mk_gparams_register_modules_internal(h_files_full_path, path):
|
|||
reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
|
||||
for h_file in sorted_headers_by_component(h_files_full_path):
|
||||
added_include = False
|
||||
with open(h_file, 'r') as fin:
|
||||
with io.open(h_file, encoding='utf-8', mode='r') as fin:
|
||||
for line in fin:
|
||||
m = reg_pat.match(line)
|
||||
if m:
|
||||
|
|
@ -696,7 +697,7 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path):
|
|||
for h_file in sorted_headers_by_component(h_files_full_path):
|
||||
added_include = False
|
||||
try:
|
||||
with open(h_file, 'r') as fin:
|
||||
with io.open(h_file, encoding='utf-8', mode='r') as fin:
|
||||
for line in fin:
|
||||
if tactic_pat.match(line):
|
||||
if not added_include:
|
||||
|
|
@ -764,7 +765,7 @@ def mk_mem_initializer_cpp_internal(h_files_full_path, path):
|
|||
finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
|
||||
for h_file in sorted_headers_by_component(h_files_full_path):
|
||||
added_include = False
|
||||
with open(h_file, 'r') as fin:
|
||||
with io.open(h_file, encoding='utf-8', mode='r') as fin:
|
||||
for line in fin:
|
||||
m = initializer_pat.match(line)
|
||||
if m:
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@
|
|||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
############################################
|
||||
import io
|
||||
import sys
|
||||
import os
|
||||
import re
|
||||
|
|
@ -806,7 +807,7 @@ def extract_c_includes(fname):
|
|||
# We should generate and error for any occurrence of #include that does not match the previous pattern.
|
||||
non_std_inc_pat = re.compile(".*#include.*")
|
||||
|
||||
f = open(fname, 'r')
|
||||
f = io.open(fname, encoding='utf-8', mode='r')
|
||||
linenum = 1
|
||||
for line in f:
|
||||
m1 = std_inc_pat.match(line)
|
||||
|
|
|
|||
|
|
@ -1720,6 +1720,10 @@ namespace z3 {
|
|||
m_vector = s.m_vector;
|
||||
return *this;
|
||||
}
|
||||
ast_vector_tpl& set(unsigned idx, ast& a) {
|
||||
Z3_ast_vector_set(ctx(), m_vector, idx, a);
|
||||
return *this;
|
||||
}
|
||||
/*
|
||||
Disabled pending C++98 build upgrade
|
||||
bool contains(T const& x) const {
|
||||
|
|
@ -1746,6 +1750,9 @@ namespace z3 {
|
|||
++m_index;
|
||||
return *this;
|
||||
}
|
||||
void set(T& arg) {
|
||||
Z3_ast_vector_set(m_vector->ctx(), *m_vector, m_index, arg);
|
||||
}
|
||||
iterator operator++(int) { iterator tmp = *this; ++m_index; return tmp; }
|
||||
T * operator->() const { return &(operator*()); }
|
||||
T operator*() const { return (*m_vector)[m_index]; }
|
||||
|
|
|
|||
|
|
@ -459,6 +459,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
case OP_SEQ_AT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_seq_at(args[0], args[1], result);
|
||||
case OP_SEQ_NTH:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_seq_nth(args[0], args[1], result);
|
||||
case OP_SEQ_PREFIX:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_seq_prefix(args[0], args[1], result);
|
||||
|
|
@ -877,6 +880,38 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
|
||||
zstring c;
|
||||
rational r;
|
||||
if (!m_autil.is_numeral(b, r) || !r.is_unsigned()) {
|
||||
return BR_FAILED;
|
||||
}
|
||||
unsigned len = r.get_unsigned();
|
||||
|
||||
expr_ref_vector as(m());
|
||||
m_util.str.get_concat_units(a, as);
|
||||
|
||||
for (unsigned i = 0; i < as.size(); ++i) {
|
||||
expr* a = as.get(i), *u = nullptr;
|
||||
if (m_util.str.is_unit(a, u)) {
|
||||
if (len == i) {
|
||||
result = u;
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
}
|
||||
else if (i > 0) {
|
||||
SASSERT(len >= i);
|
||||
result = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
|
||||
result = m().mk_app(m_util.get_family_id(), OP_SEQ_NTH, result, m_autil.mk_int(len - i));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
else {
|
||||
return BR_FAILED;
|
||||
}
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result) {
|
||||
zstring s1, s2;
|
||||
rational r;
|
||||
|
|
|
|||
|
|
@ -114,6 +114,7 @@ class seq_rewriter {
|
|||
br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result);
|
||||
br_status mk_seq_contains(expr* a, expr* b, expr_ref& result);
|
||||
br_status mk_seq_at(expr* a, expr* b, expr_ref& result);
|
||||
br_status mk_seq_nth(expr* a, expr* b, expr_ref& result);
|
||||
br_status mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result);
|
||||
br_status mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result);
|
||||
br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result);
|
||||
|
|
|
|||
|
|
@ -501,7 +501,7 @@ public:
|
|||
expr_ref val(m);
|
||||
model_evaluator eval(model);
|
||||
for (expr * f : fmls) {
|
||||
VERIFY(model.is_true(f));
|
||||
VERIFY(!model.is_false(f));
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
@ -657,7 +657,7 @@ public:
|
|||
other_vars.reset();
|
||||
}
|
||||
|
||||
SASSERT(eval.is_true(fml));
|
||||
SASSERT(!eval.is_false(fml));
|
||||
|
||||
vars.reset ();
|
||||
vars.append(other_vars);
|
||||
|
|
|
|||
|
|
@ -3537,7 +3537,7 @@ expr_ref theory_seq::digit2int(expr* ch) {
|
|||
|
||||
|
||||
|
||||
// n >= 0 & len(e) = k => is_digit(e_i) for i = 0..k-1
|
||||
// n >= 0 & len(e) >= i + 1 => is_digit(e_i) for i = 0..k-1
|
||||
// n >= 0 & len(e) = k => n = sum 10^i*digit(e_i)
|
||||
// n < 0 & len(e) = k => \/_i ~is_digit(e_i) for i = 0..k-1
|
||||
// 10^k <= n < 10^{k+1}-1 => len(e) = k
|
||||
|
|
@ -3557,7 +3557,9 @@ void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) {
|
|||
for (unsigned i = 0; i < k; ++i) {
|
||||
ith_char = mk_nth(e, m_autil.mk_int(i));
|
||||
literal isd = is_digit(ith_char);
|
||||
add_axiom(~len_eq_k, ~ge0, isd);
|
||||
literal len_ge_i1 = mk_literal(m_autil.mk_ge(len, m_autil.mk_int(i+1)));
|
||||
add_axiom(~len_ge_i1, ~ge0, isd);
|
||||
digits.push_back(~isd);
|
||||
chars.push_back(m_util.str.mk_unit(ith_char));
|
||||
nums.push_back(digit2int(ith_char));
|
||||
}
|
||||
|
|
@ -4585,7 +4587,12 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
|
|||
|
||||
IF_VERBOSE(11, verbose_stream() << mk_pp(s, m) << " in " << re << "\n");
|
||||
eautomaton* a = get_automaton(re);
|
||||
if (!a) return;
|
||||
if (!a) {
|
||||
std::stringstream strm;
|
||||
strm << "expression " << re << " does not correspond to a supported regular expression";
|
||||
TRACE("seq", tout << strm.str() << "\n";);
|
||||
throw default_exception(strm.str());
|
||||
}
|
||||
|
||||
m_s_in_re.push_back(s_in_re(lit, s, re, a));
|
||||
m_trail_stack.push(push_back_vector<theory_seq, vector<s_in_re>>(m_s_in_re));
|
||||
|
|
|
|||
|
|
@ -56,17 +56,17 @@ void finalize_debug() {
|
|||
|
||||
void enable_debug(const char * tag) {
|
||||
init_debug_table();
|
||||
g_enabled_debug_tags->insert(const_cast<char *>(tag));
|
||||
g_enabled_debug_tags->insert(tag);
|
||||
}
|
||||
|
||||
void disable_debug(const char * tag) {
|
||||
init_debug_table();
|
||||
g_enabled_debug_tags->erase(const_cast<char *>(tag));
|
||||
g_enabled_debug_tags->erase(tag);
|
||||
}
|
||||
|
||||
bool is_debug_enabled(const char * tag) {
|
||||
init_debug_table();
|
||||
return g_enabled_debug_tags->contains(const_cast<char *>(tag));
|
||||
return g_enabled_debug_tags->contains(tag);
|
||||
}
|
||||
|
||||
#if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER)
|
||||
|
|
|
|||
|
|
@ -44,6 +44,13 @@ bool assertions_enabled();
|
|||
#define DEBUG_CODE(CODE) ((void) 0)
|
||||
#endif
|
||||
|
||||
#ifdef __APPLE__
|
||||
#include <TargetConditionals.h>
|
||||
#if !TARGET_OS_OSX
|
||||
#define NO_Z3_DEBUGGER
|
||||
#endif
|
||||
#endif
|
||||
|
||||
#ifdef NO_Z3_DEBUGGER
|
||||
#define INVOKE_DEBUGGER() exit(ERR_INTERNAL_FATAL)
|
||||
#else
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ struct str_hash_proc {
|
|||
unsigned operator()(char const * s) const { return string_hash(s, static_cast<unsigned>(strlen(s)), 17); }
|
||||
};
|
||||
struct str_eq_proc { bool operator()(char const * s1, char const * s2) const { return strcmp(s1, s2) == 0; } };
|
||||
typedef ptr_hashtable<char, str_hash_proc, str_eq_proc> str_hashtable;
|
||||
typedef ptr_hashtable<const char, str_hash_proc, str_eq_proc> str_hashtable;
|
||||
|
||||
#endif /* STR_HASHTABLE_H_ */
|
||||
|
||||
|
|
|
|||
|
|
@ -35,20 +35,19 @@ class internal_symbol_table {
|
|||
public:
|
||||
|
||||
char const * get_str(char const * d) {
|
||||
char * result;
|
||||
const char * result;
|
||||
#pragma omp critical (cr_symbol)
|
||||
{
|
||||
char * r_d = const_cast<char *>(d);
|
||||
str_hashtable::entry * e;
|
||||
if (m_table.insert_if_not_there_core(r_d, e)) {
|
||||
if (m_table.insert_if_not_there_core(d, e)) {
|
||||
// new entry
|
||||
size_t l = strlen(d);
|
||||
// store the hash-code before the string
|
||||
size_t * mem = static_cast<size_t*>(m_region.allocate(l + 1 + sizeof(size_t)));
|
||||
*mem = e->get_hash();
|
||||
mem++;
|
||||
result = reinterpret_cast<char*>(mem);
|
||||
memcpy(result, d, l+1);
|
||||
result = reinterpret_cast<const char*>(mem);
|
||||
memcpy(mem, d, l+1);
|
||||
// update the entry with the new ptr.
|
||||
e->set_data(result);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@ void finalize_trace() {
|
|||
}
|
||||
|
||||
void enable_trace(const char * tag) {
|
||||
get_enabled_trace_tags().insert(const_cast<char *>(tag));
|
||||
get_enabled_trace_tags().insert(tag);
|
||||
}
|
||||
|
||||
void enable_all_trace(bool flag) {
|
||||
|
|
@ -46,12 +46,12 @@ void enable_all_trace(bool flag) {
|
|||
}
|
||||
|
||||
void disable_trace(const char * tag) {
|
||||
get_enabled_trace_tags().erase(const_cast<char *>(tag));
|
||||
get_enabled_trace_tags().erase(tag);
|
||||
}
|
||||
|
||||
bool is_trace_enabled(const char * tag) {
|
||||
return g_enable_all_trace_tags ||
|
||||
(g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast<char *>(tag)));
|
||||
(g_enabled_trace_tags && get_enabled_trace_tags().contains(tag));
|
||||
}
|
||||
|
||||
void close_trace() {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue