mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master'

Browse source
This commit is contained in:
Yatao Li 2019-01-12 15:01:28 +08:00
parent ffd26e5a56 63d480fd92
commit 17596fcc17
47 changed files with 1440 additions and 375 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
CMakeLists.txt
View file

@ -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()

74
examples/python/mini_ic3.py
View file

@ -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
View 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

7
scripts/mk_genfile_common.py
View file

@ -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:

8
scripts/mk_nuget_release.py
View file

@ -38,7 +38,7 @@ def download_installs():
urllib.request.urlretrieve(url, "packages/%s" % name)
os_info = {"z64-ubuntu-14" : ('so', 'ubuntu.14.04-x64'),
'ubuntu-16' : ('so', 'ubuntu.16.04-x64'),
'ubuntu-16' : ('so', 'ubuntu-x64'),
'x64-win' : ('dll', 'win-x64'),
'x86-win' : ('dll', 'win-x86'),
'osx' : ('dylib', 'macos'),
@ -91,11 +91,7 @@ def create_nuget_spec():
<iconUrl>https://raw.githubusercontent.com/Z3Prover/z3/master/package/icon.jpg</iconUrl>
<projectUrl>https://github.com/Z3Prover/z3</projectUrl>
<licenseUrl>https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt</licenseUrl>
<repository
type="git"
url="https://github.com/Z3Prover/z3.git"
branch="master"
/>
<repository type="git" url="https://github.com/Z3Prover/z3.git" />
<requireLicenseAcceptance>true</requireLicenseAcceptance>
<language>en</language>
</metadata>

3
scripts/mk_util.py
View file

@ -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)

2
src/api/api_solver.cpp
View file

@ -181,7 +181,7 @@ extern "C" {
if (!is) {
SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr);
}
else if (ext && std::string("dimacs") == ext) {
else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) {
ast_manager& m = to_solver_ref(s)->get_manager();
std::stringstream err;
sat::solver solver(to_solver_ref(s)->get_params(), m.limit());

7
src/api/c++/z3++.h
View file

@ -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]; }

31
src/api/python/z3/z3.py
View file

@ -482,6 +482,7 @@ def _to_ast_ref(a, ctx):
else:
return _to_expr_ref(a, ctx)
#########################################
#
# Sorts
@ -6664,17 +6665,11 @@ class Solver(Z3PPObject):
def from_file(self, filename):
"""Parse assertions from a file"""
try:
Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
def from_string(self, s):
"""Parse assertions from a string"""
try:
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
def cube(self, vars = None):
"""Get set of cubes
@ -7063,17 +7058,11 @@ class Fixedpoint(Z3PPObject):
def parse_string(self, s):
"""Parse rules and queries from a string"""
try:
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
def parse_file(self, f):
"""Parse rules and queries from a file"""
try:
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
def get_rules(self):
"""retrieve rules that have been added to fixedpoint context"""
@ -7410,17 +7399,11 @@ class Optimize(Z3PPObject):
def from_file(self, filename):
"""Parse assertions and objectives from a file"""
try:
Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
def from_string(self, s):
"""Parse assertions and objectives from a string"""
try:
Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
def assertions(self):
"""Return an AST vector containing all added constraints."""

83
src/ast/datatype_decl_plugin.cpp
View file

@ -143,7 +143,77 @@ namespace datatype {
}
return r;
}
size* size::mk_power(size* a1, size* a2) { return alloc(power, a1, a2); }
size* size::mk_power(size* a1, size* a2) {
return alloc(power, a1, a2);
}
sort_size plus::eval(obj_map<sort, sort_size> const& S) {
rational r(0);
ptr_vector<size> todo;
todo.push_back(m_arg1);
todo.push_back(m_arg2);
while (!todo.empty()) {
size* s = todo.back();
todo.pop_back();
plus* p = dynamic_cast<plus*>(s);
if (p) {
todo.push_back(p->m_arg1);
todo.push_back(p->m_arg2);
}
else {
sort_size sz = s->eval(S);
if (sz.is_infinite()) return sz;
if (sz.is_very_big()) return sz;
r += rational(sz.size(), rational::ui64());
}
}
return sort_size(r);
}
size* plus::subst(obj_map<sort,size*>& S) {
return mk_plus(m_arg1->subst(S), m_arg2->subst(S));
}
sort_size times::eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64());
return sort_size(r);
}
size* times::subst(obj_map<sort,size*>& S) {
return mk_times(m_arg1->subst(S), m_arg2->subst(S));
}
sort_size power::eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
// s1^s2
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
if (s1.size() == 1) return s1;
if (s2.size() == 1) return s1;
if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big();
rational r = ::power(rational(s1.size(), rational::ui64()), static_cast<unsigned>(s2.size()));
return sort_size(r);
}
size* power::subst(obj_map<sort,size*>& S) {
return mk_power(m_arg1->subst(S), m_arg2->subst(S));
}
size* sparam::subst(obj_map<sort, size*>& S) {
return S[m_param];
}
}
namespace decl {
@ -584,13 +654,14 @@ namespace datatype {
param_size::size* sz;
obj_map<sort, param_size::size*> S;
unsigned n = get_datatype_num_parameter_sorts(s);
def & d = get_def(s->get_name());
SASSERT(n == d.params().size());
for (unsigned i = 0; i < n; ++i) {
sort* ps = get_datatype_parameter_sort(s, i);
sz = get_sort_size(params, ps);
sz->inc_ref();
S.insert(ps, sz);
}
def & d = get_def(s->get_name());
sz->inc_ref();
S.insert(d.params().get(i), sz);
}
sz = d.sort_size()->subst(S);
for (auto & kv : S) {
kv.m_value->dec_ref();
@ -667,7 +738,7 @@ namespace datatype {
continue;
}
ptr_vector<param_size::size> s_add;
ptr_vector<param_size::size> s_add;
for (constructor const* c : d) {
ptr_vector<param_size::size> s_mul;
for (accessor const* a : *c) {

57
src/ast/datatype_decl_plugin.h
View file

@ -132,71 +132,28 @@ namespace datatype {
size* m_arg1, *m_arg2;
plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();}
~plus() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
size* subst(obj_map<sort,size*>& S) override { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); }
sort_size eval(obj_map<sort, sort_size> const& S) override {
rational r(0);
ptr_vector<size> todo;
todo.push_back(m_arg1);
todo.push_back(m_arg2);
while (!todo.empty()) {
size* s = todo.back();
todo.pop_back();
plus* p = dynamic_cast<plus*>(s);
if (p) {
todo.push_back(p->m_arg1);
todo.push_back(p->m_arg2);
}
else {
sort_size sz = s->eval(S);
if (sz.is_infinite()) return sz;
if (sz.is_very_big()) return sz;
r += rational(sz.size(), rational::ui64());
}
}
return sort_size(r);
}
size* subst(obj_map<sort,size*>& S) override;
sort_size eval(obj_map<sort, sort_size> const& S) override;
};
struct times : public size {
size* m_arg1, *m_arg2;
times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
~times() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
size* subst(obj_map<sort,size*>& S) override { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); }
sort_size eval(obj_map<sort, sort_size> const& S) override {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64());
return sort_size(r);
}
size* subst(obj_map<sort,size*>& S) override;
sort_size eval(obj_map<sort, sort_size> const& S) override;
};
struct power : public size {
size* m_arg1, *m_arg2;
power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
~power() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
size* subst(obj_map<sort,size*>& S) override { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); }
sort_size eval(obj_map<sort, sort_size> const& S) override {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
// s1^s2
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
if (s1.size() == 1) return s1;
if (s2.size() == 1) return s1;
if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big();
rational r = ::power(rational(s1.size(), rational::ui64()), static_cast<unsigned>(s2.size()));
return sort_size(r);
}
size* subst(obj_map<sort,size*>& S) override;
sort_size eval(obj_map<sort, sort_size> const& S) override;
};
struct sparam : public size {
sort_ref m_param;
sparam(sort_ref& p): m_param(p) {}
~sparam() override {}
size* subst(obj_map<sort,size*>& S) override { return S[m_param]; }
size* subst(obj_map<sort, size*>& S) override;
sort_size eval(obj_map<sort, sort_size> const& S) override { return S[m_param]; }
};
};

47
src/ast/expr2var.cpp
View file

@ -29,8 +29,17 @@ void expr2var::insert(expr * n, var v) {
TRACE("expr2var", tout << "interpreted:\n" << mk_ismt2_pp(n, m()) << "\n";);
m_interpreted_vars = true;
}
m().inc_ref(n);
m_mapping.insert(n, v);
unsigned idx = m_id2map.get(n->get_id(), UINT_MAX);
if (idx == UINT_MAX) {
m().inc_ref(n);
idx = m_mapping.size();
m_mapping.push_back(key_value(n, v));
m_id2map.setx(n->get_id(), idx, UINT_MAX);
}
else {
m_mapping[idx] = key_value(n, v);
}
m_recent_exprs.push_back(n);
}
@ -40,20 +49,22 @@ expr2var::expr2var(ast_manager & m):
}
expr2var::~expr2var() {
dec_ref_map_keys(m(), m_mapping);
for (auto & kv : m_mapping) {
m().dec_ref(kv.m_key);
}
}
expr2var::var expr2var::to_var(expr * n) const {
var v = UINT_MAX;
m_mapping.find(n, v);
var v = m_id2map.get(n->get_id(), UINT_MAX);
if (v != UINT_MAX) {
v = m_mapping[v].m_value;
}
return v;
}
void expr2var::display(std::ostream & out) const {
obj_map<expr, var>::iterator it = m_mapping.begin();
obj_map<expr, var>::iterator end = m_mapping.end();
for (; it != end; ++it) {
out << mk_ismt2_pp(it->m_key, m()) << " -> " << it->m_value << "\n";
for (auto const& kv : m_mapping) {
out << mk_ismt2_pp(kv.m_key, m()) << " -> " << kv.m_value << "\n";
}
}
@ -68,8 +79,11 @@ void expr2var::mk_inv(expr_ref_vector & var2expr) const {
}
void expr2var::reset() {
dec_ref_map_keys(m(), m_mapping);
SASSERT(m_mapping.empty());
for (auto & kv : m_mapping) {
m().dec_ref(kv.m_key);
}
m_mapping.reset();
m_id2map.reset();
m_recent_exprs.reset();
m_recent_lim.reset();
m_interpreted_vars = false;
@ -83,8 +97,15 @@ void expr2var::pop(unsigned num_scopes) {
if (num_scopes > 0) {
unsigned sz = m_recent_lim[m_recent_lim.size() - num_scopes];
for (unsigned i = sz; i < m_recent_exprs.size(); ++i) {
m_mapping.erase(m_recent_exprs[i]);
m().dec_ref(m_recent_exprs[i]);
expr* n = m_recent_exprs[i];
unsigned idx = m_id2map[n->get_id()];
if (idx + 1 != m_mapping.size()) {
m_id2map[m_mapping.back().m_key->get_id()] = idx;
m_mapping[idx] = m_mapping.back();
}
m_id2map[n->get_id()] = UINT_MAX;
m_mapping.pop_back();
m().dec_ref(n);
}
m_recent_exprs.shrink(sz);
m_recent_lim.shrink(m_recent_lim.size() - num_scopes);

10
src/ast/expr2var.h
View file

@ -32,12 +32,14 @@ Notes:
class expr2var {
public:
typedef unsigned var;
typedef obj_map<expr, var> expr2var_mapping;
typedef expr2var_mapping::iterator iterator;
typedef obj_map<expr, var>::key_data key_value;
typedef key_value const* iterator;
typedef ptr_vector<expr>::const_iterator recent_iterator;
protected:
ast_manager & m_manager;
expr2var_mapping m_mapping;
unsigned_vector m_id2map;
svector<key_value> m_mapping;
ptr_vector<expr> m_recent_exprs;
unsigned_vector m_recent_lim;
bool m_interpreted_vars;
@ -51,7 +53,7 @@ public:
var to_var(expr * n) const;
bool is_var(expr * n) const { return m_mapping.contains(n); }
bool is_var(expr * n) const { return m_id2map.get(n->get_id(), UINT_MAX) != UINT_MAX; }
void display(std::ostream & out) const;

16
src/ast/rewriter/bv_rewriter.cpp
View file

@ -196,6 +196,9 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
return mk_bv_comp(args[0], args[1], result);
case OP_MKBV:
return mk_mkbv(num_args, args, result);
case OP_BIT2BOOL:
SASSERT(num_args == 1);
return mk_bit2bool(args[0], f->get_parameter(0).get_int(), result);
case OP_BSMUL_NO_OVFL:
return mk_bvsmul_no_overflow(num_args, args, result);
case OP_BUMUL_NO_OVFL:
@ -2203,6 +2206,19 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
return st;
}
br_status bv_rewriter::mk_bit2bool(expr * n, int idx, expr_ref & result) {
rational v, bit;
unsigned sz = 0;
if (!is_numeral(n, v, sz))
return BR_FAILED;
if (idx < 0 || idx >= static_cast<int>(sz))
return BR_FAILED;
div(v, rational::power_of_two(idx), bit);
mod(bit, rational(2), bit);
result = m().mk_bool_val(bit.is_one());
return BR_DONE;
}
br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
unsigned sz = get_bv_size(lhs);
if (sz != 1)

1
src/ast/rewriter/bv_rewriter.h
View file

@ -134,6 +134,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
br_status mk_bv_redand(expr * arg, expr_ref & result);
br_status mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result);
br_status mk_bit2bool(expr * lhs, int idx, expr_ref & result);
br_status mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & result);
br_status mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result);
br_status mk_mkbv(unsigned num, expr * const * args, expr_ref & result);

31
src/ast/rewriter/seq_rewriter.cpp
View file

@ -459,6 +459,11 @@ 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);
#if 0
case OP_SEQ_NTH:
SASSERT(num_args == 2);
return mk_seq_nth(args[0], args[1], result);
#endif
case OP_SEQ_PREFIX:
SASSERT(num_args == 2);
return mk_seq_prefix(args[0], args[1], result);
@ -877,6 +882,32 @@ 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_DONE;
}
}
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;

1
src/ast/rewriter/seq_rewriter.h
View file

@ -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);

20
src/ast/shared_occs.cpp
View file

@ -21,13 +21,11 @@ Revision History:
#include "util/ref_util.h"
inline void shared_occs::insert(expr * t) {
obj_hashtable<expr>::entry * dummy;
if (m_shared.insert_if_not_there_core(t, dummy))
m.inc_ref(t);
m_shared.reserve(t->get_id() + 1);
m_shared[t->get_id()] = t;
}
void shared_occs::reset() {
dec_ref_collection_values(m, m_shared);
m_shared.reset();
}
@ -132,9 +130,15 @@ void shared_occs::operator()(expr * t) {
}
void shared_occs::display(std::ostream & out, ast_manager & m) const {
iterator it = begin_shared();
iterator end = end_shared();
for (; it != end; ++it) {
out << mk_ismt2_pp(*it, m) << "\n";
for (expr* s : m_shared) {
if (s) {
out << mk_ismt2_pp(s, m) << "\n";
}
}
}
unsigned shared_occs::num_shared() const{
unsigned count = 0;
for (expr* s : m_shared) if (s) count++;
return count;
}

11
src/ast/shared_occs.h
View file

@ -53,7 +53,7 @@ class shared_occs {
bool m_track_atomic;
bool m_visit_quantifiers;
bool m_visit_patterns;
obj_hashtable<expr> m_shared;
expr_ref_vector m_shared;
typedef std::pair<expr*, unsigned> frame;
svector<frame> m_stack;
bool process(expr * t, shared_occs_mark & visited);
@ -64,15 +64,14 @@ public:
m(_m),
m_track_atomic(track_atomic),
m_visit_quantifiers(visit_quantifiers),
m_visit_patterns(visit_patterns) {
m_visit_patterns(visit_patterns),
m_shared(m) {
}
~shared_occs();
void operator()(expr * t);
void operator()(expr * t, shared_occs_mark & visited);
bool is_shared(expr * t) const { return m_shared.contains(t); }
unsigned num_shared() const { return m_shared.size(); }
iterator begin_shared() const { return m_shared.begin(); }
iterator end_shared() const { return m_shared.end(); }
bool is_shared(expr * t) const { return m_shared.get(t->get_id(), nullptr) != nullptr; }
unsigned num_shared() const;
void reset();
void cleanup();
void display(std::ostream & out, ast_manager & mgr) const;

40
src/cmd_context/extra_cmds/dbg_cmds.cpp
View file

@ -77,30 +77,12 @@ BINARY_SYM_CMD(shift_vars_cmd,
store_expr_ref(ctx, m_sym, r.get());
});
UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "<term>", "display shared subterms of the given term", CPK_EXPR, expr *, {
shared_occs s(ctx.m());
s(arg);
ctx.regular_stream() << "(shared";
shared_occs::iterator it = s.begin_shared();
shared_occs::iterator end = s.end_shared();
for (; it != end; ++it) {
expr * curr = *it;
ctx.regular_stream() << std::endl << " ";
ctx.display(ctx.regular_stream(), curr, 2);
}
ctx.regular_stream() << ")" << std::endl;
});
UNARY_CMD(assert_not_cmd, "assert-not", "<term>", "assert negation", CPK_EXPR, expr *, {
expr_ref ne(ctx.m().mk_not(arg), ctx.m());
ctx.assert_expr(ne);
});
UNARY_CMD(num_shared_cmd, "dbg-num-shared", "<term>", "return the number of shared subterms", CPK_EXPR, expr *, {
shared_occs s(ctx.m());
s(arg);
ctx.regular_stream() << s.num_shared() << std::endl;
});
UNARY_CMD(size_cmd, "dbg-size", "<term>", "return the size of the given term", CPK_EXPR, expr *, {
ctx.regular_stream() << get_num_exprs(arg) << std::endl;
@ -524,11 +506,21 @@ public:
for (func_decl* v : m_vars) vars.push_back(v);
for (expr* e : m_lits) lits.push_back(e);
flatten_and(lits);
qe::term_graph tg(m);
tg.set_vars(vars, false);
tg.add_lits(lits);
expr_ref_vector p = tg.project();
ctx.regular_stream() << p << "\n";
solver_factory& sf = ctx.get_solver_factory();
params_ref pa;
solver_ref s = sf(m, pa, false, true, true, symbol::null);
solver_ref se = sf(m, pa, false, true, true, symbol::null);
s->assert_expr(lits);
lbool r = s->check_sat();
if (r != l_true) {
ctx.regular_stream() << "sat check " << r << "\n";
return;
}
model_ref mdl;
s->get_model(mdl);
qe::euf_arith_mbi_plugin plugin(s.get(), se.get());
plugin.project(mdl, lits);
ctx.regular_stream() << lits << "\n";
}
};
@ -540,8 +532,6 @@ void install_dbg_cmds(cmd_context & ctx) {
ctx.insert(alloc(set_cmd));
ctx.insert(alloc(pp_var_cmd));
ctx.insert(alloc(shift_vars_cmd));
ctx.insert(alloc(pp_shared_cmd));
ctx.insert(alloc(num_shared_cmd));
ctx.insert(alloc(assert_not_cmd));
ctx.insert(alloc(size_cmd));
ctx.insert(alloc(subst_cmd));

2
src/opt/opt_context.cpp
View file

@ -361,7 +361,7 @@ namespace opt {
mdl = m_model;
fix_model(mdl);
if (mdl) mdl->set_model_completion(true);
TRACE("opt", tout << *mdl;);
CTRACE("opt", mdl, tout << *mdl;);
}
void context::get_box_model(model_ref& mdl, unsigned index) {

4
src/qe/qe_arrays.cpp
View file

@ -798,7 +798,7 @@ namespace qe {
*/
expr* reduce_core (app *a) {
if (!m_arr_u.is_store (a->get_arg (0))) return a;
expr* array = a->get_arg(0);
expr* array = a->get_arg(0);
unsigned arity = get_array_arity(m.get_sort(array));
expr* const* js = a->get_args() + 1;
@ -810,7 +810,7 @@ namespace qe {
if (is_equals (arity, idxs, js)) {
add_idx_cond (cond);
return a->get_arg (2);
return a->get_arg (a->get_num_args() - 1);
}
else {
cond = m.mk_not (cond);

52
src/qe/qe_mbi.cpp
View file

@ -126,30 +126,29 @@ namespace qe {
struct euf_arith_mbi_plugin::is_arith_var_proc {
ast_manager& m;
app_ref_vector& m_avars;
arith_util arith;
app_ref_vector& m_proxies;
arith_util m_arith;
obj_hashtable<expr> m_seen;
is_arith_var_proc(app_ref_vector& avars):
m(avars.m()), m_avars(avars), arith(m) {
is_arith_var_proc(app_ref_vector& avars, app_ref_vector& proxies):
m(avars.m()), m_avars(avars), m_proxies(proxies), m_arith(m) {
}
void operator()(app* a) {
if (is_arith_op(a) || a->get_family_id() == m.get_basic_family_id()) {
// no-op
return;
}
else if (!arith.is_int_real(a)) {
for (expr* arg : *a) {
if (is_app(arg) && !m_seen.contains(arg) && is_arith_op(to_app(arg))) {
m_avars.push_back(to_app(arg));
m_seen.insert(arg);
}
}
}
else if (!m_seen.contains(a)) {
m_seen.insert(a);
if (m_arith.is_int_real(a)) {
m_avars.push_back(a);
}
for (expr* arg : *a) {
if (is_app(arg) && !m_seen.contains(arg) && m_arith.is_int_real(arg)) {
m_proxies.push_back(to_app(arg));
m_seen.insert(arg);
}
}
}
bool is_arith_op(app* a) {
return a->get_family_id() == arith.get_family_id();
return a->get_family_id() == m_arith.get_family_id();
}
void operator()(expr*) {}
};
@ -221,9 +220,9 @@ namespace qe {
/**
* \brief extract arithmetical variables and arithmetical terms in shared positions.
*/
app_ref_vector euf_arith_mbi_plugin::get_arith_vars(model_ref& mdl, expr_ref_vector& lits) {
app_ref_vector euf_arith_mbi_plugin::get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies) {
app_ref_vector avars(m);
is_arith_var_proc _proc(avars);
is_arith_var_proc _proc(avars, proxies);
for_each_expr(_proc, lits);
return avars;
}
@ -257,16 +256,19 @@ namespace qe {
void euf_arith_mbi_plugin::project(model_ref& mdl, expr_ref_vector& lits) {
TRACE("qe", tout << lits << "\n" << *mdl << "\n";);
TRACE("qe", tout << m_solver->get_assertions() << "\n";);
// 1. arithmetical variables - atomic and in purified positions
app_ref_vector avars = get_arith_vars(mdl, lits);
TRACE("qe", tout << "vars: " << avars << "\nlits: " << lits << "\n";);
app_ref_vector proxies(m);
app_ref_vector avars = get_arith_vars(mdl, lits, proxies);
TRACE("qe", tout << "vars: " << avars << "\nproxies: " << proxies << "\nlits: " << lits << "\n";);
// 2. project private non-arithmetical variables from lits
project_euf(mdl, lits, avars);
// 3. Order arithmetical variables and purified positions
order_avars(mdl, lits, avars);
order_avars(mdl, lits, avars, proxies);
TRACE("qe", tout << "ordered: " << lits << "\n";);
// 4. Perform arithmetical projection
@ -307,15 +309,14 @@ namespace qe {
/**
* \brief Order arithmetical variables:
* 1. add literals that order the variable according to the model.
* 2. remove non-atomic arithmetical terms from projection.
* 1. add literals that order the proxies according to the model.
* 2. sort arithmetical terms, such that deepest terms are first.
*/
void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars) {
void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies) {
arith_util a(m);
model_evaluator mev(*mdl.get());
vector<std::pair<rational, app*>> vals;
for (app* v : avars) {
for (app* v : proxies) {
rational val;
expr_ref tmp = mev(v);
VERIFY(a.is_numeral(tmp, val));
@ -327,7 +328,7 @@ namespace qe {
return x.first < y.first;
}
};
// add linear order between avars
// add linear order between proxies
compare_first cmp;
std::sort(vals.begin(), vals.end(), cmp);
for (unsigned i = 1; i < vals.size(); ++i) {
@ -338,6 +339,7 @@ namespace qe {
lits.push_back(a.mk_lt(vals[i-1].second, vals[i].second));
}
}
// filter out only private variables
filter_private_arith(avars);

6
src/qe/qe_mbi.h
View file

@ -103,18 +103,18 @@ namespace qe {
struct is_atom_proc;
struct is_arith_var_proc;
app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits);
app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies);
bool get_literals(model_ref& mdl, expr_ref_vector& lits);
void collect_atoms(expr_ref_vector const& fmls);
void project(model_ref& mdl, expr_ref_vector& lits);
void project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars);
void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars);
void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies);
void substitute(vector<def> const& defs, expr_ref_vector& lits);
void filter_private_arith(app_ref_vector& avars);
public:
euf_arith_mbi_plugin(solver* s, solver* emptySolver);
~euf_arith_mbi_plugin() override {}
mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
void project(model_ref& mdl, expr_ref_vector& lits);
void block(expr_ref_vector const& lits) override;
};

4
src/qe/qe_mbp.cpp
View file

@ -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);

65
src/sat/sat_cleaner.cpp
View file

@ -78,6 +78,7 @@ namespace sat {
}
void cleaner::cleanup_clauses(clause_vector & cs) {
tmp_clause tmp;
clause_vector::iterator it = cs.begin();
clause_vector::iterator it2 = it;
clause_vector::iterator end = cs.end();
@ -88,12 +89,10 @@ namespace sat {
CTRACE("sat_cleaner_frozen", c.frozen(), tout << c << "\n";);
unsigned sz = c.size();
unsigned i = 0, j = 0;
bool sat = false;
m_cleanup_counter += sz;
for (; i < sz; i++) {
switch (s.value(c[i])) {
case l_true:
sat = true;
goto end_loop;
case l_false:
m_elim_literals++;
@ -108,9 +107,9 @@ namespace sat {
}
end_loop:
CTRACE("sat_cleaner_frozen", c.frozen(),
tout << "sat: " << sat << ", new_size: " << j << "\n";
tout << "sat: " << (i < sz) << ", new_size: " << j << "\n";
tout << mk_lits_pp(j, c.begin()) << "\n";);
if (sat) {
if (i < sz) {
m_elim_clauses++;
s.del_clause(c);
}
@ -119,33 +118,37 @@ namespace sat {
CTRACE("sat_cleaner_bug", new_sz < 2, tout << "new_sz: " << new_sz << "\n";
if (c.size() > 0) tout << "unit: " << c[0] << "\n";
s.display_watches(tout););
if (new_sz == 0) {
switch (new_sz) {
case 0:
s.set_conflict(justification());
s.del_clause(c);
}
else if (new_sz == 1) {
break;
case 1:
s.assign(c[0], justification());
s.del_clause(c);
}
else {
break;
case 2:
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
if (new_sz == 2) {
TRACE("cleanup_bug", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
s.mk_bin_clause(c[0], c[1], c.is_learned());
s.del_clause(c);
TRACE("cleanup_bug", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
s.mk_bin_clause(c[0], c[1], c.is_learned());
s.del_clause(c);
break;
default:
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
if (s.m_config.m_drat && new_sz < i) {
tmp.set(c.size(), c.begin(), c.is_learned());
}
else {
c.shrink(new_sz);
*it2 = *it;
it2++;
if (!c.frozen()) {
s.attach_clause(c);
}
if (s.m_config.m_drat) {
// for optimization, could also report deletion
// of previous version of clause.
s.m_drat.add(c, true);
}
c.shrink(new_sz);
*it2 = *it;
it2++;
if (!c.frozen()) {
s.attach_clause(c);
}
if (s.m_config.m_drat && new_sz < i) {
// for optimization, could also report deletion
// of previous version of clause.
s.m_drat.add(c, true);
s.m_drat.del(*tmp.get());
}
}
}
@ -192,10 +195,14 @@ namespace sat {
report rpt(*this);
m_last_num_units = trail_sz;
m_cleanup_counter = 0;
cleanup_watches();
cleanup_clauses(s.m_clauses);
cleanup_clauses(s.m_learned);
s.propagate(false);
do {
trail_sz = s.m_trail.size();
cleanup_watches();
cleanup_clauses(s.m_clauses);
cleanup_clauses(s.m_learned);
s.propagate(false);
}
while (trail_sz < s.m_trail.size());
CASSERT("cleaner_bug", s.check_invariant());
return true;
}

85
src/sat/sat_drat.cpp
View file

@ -143,7 +143,7 @@ namespace sat {
IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st););
if (st == status::learned) {
verify(n, c.begin());
verify(c);
}
m_status.push_back(st);
@ -225,6 +225,55 @@ namespace sat {
m_units.resize(num_units);
bool ok = m_inconsistent;
m_inconsistent = false;
if (!ok) {
literal_vector lits(n, c);
IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n");
for (unsigned v = 0; v < m_assignment.size(); ++v) {
lbool val = m_assignment[v];
if (val != l_undef) {
IF_VERBOSE(0, verbose_stream() << literal(v, false) << " |-> " << val << "\n");
}
}
for (clause* cp : s.m_clauses) {
clause& cl = *cp;
bool found = false;
for (literal l : cl) {
if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) {
found = true;
break;
}
}
if (!found) {
IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n");
}
}
for (clause* cp : s.m_learned) {
clause& cl = *cp;
bool found = false;
for (literal l : cl) {
if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) {
found = true;
break;
}
}
if (!found) {
IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n");
}
}
svector<sat::solver::bin_clause> bin;
s.collect_bin_clauses(bin, true);
for (auto & b : bin) {
bool found = false;
if (m_assignment[b.first.var()] != (b.first.sign() ? l_true : l_false)) found = true;
if (m_assignment[b.second.var()] != (b.second.sign() ? l_true : l_false)) found = true;
if (!found) {
IF_VERBOSE(0, verbose_stream() << "Bin clause is false under assignment: " << b.first << " " << b.second << "\n");
}
}
IF_VERBOSE(0, s.display(verbose_stream()));
exit(0);
}
return ok;
}
@ -280,7 +329,10 @@ namespace sat {
void drat::verify(unsigned n, literal const* c) {
if (m_check_unsat && !is_drup(n, c) && !is_drat(n, c)) {
std::cout << "Verification failed\n";
literal_vector lits(n, c);
std::cout << "Verification of " << lits << " failed\n";
s.display(std::cout);
exit(0);
UNREACHABLE();
//display(std::cout);
TRACE("sat",
@ -291,6 +343,35 @@ namespace sat {
}
}
bool drat::contains(unsigned n, literal const* lits) {
for (unsigned i = m_proof.size(); i-- > 0; ) {
clause& c = *m_proof[i];
status st = m_status[i];
if (match(n, lits, c)) {
return st != status::deleted;
}
}
return false;
}
bool drat::match(unsigned n, literal const* lits, clause const& c) const {
if (n == c.size()) {
for (unsigned i = 0; i < n; ++i) {
literal lit1 = lits[i];
bool found = false;
for (literal lit2 : c) {
if (lit1 == lit2) {
found = true;
break;
}
}
if (!found) return false;
}
return true;
}
return false;
}
void drat::display(std::ostream& out) const {
out << "units: " << m_units << "\n";
for (unsigned i = 0; i < m_assignment.size(); ++i) {

12
src/sat/sat_drat.h
View file

@ -67,7 +67,6 @@ namespace sat {
void propagate(literal l);
void assign_propagate(literal l);
void del_watch(clause& c, literal l);
void verify(unsigned n, literal const* c);
bool is_drup(unsigned n, literal const* c);
bool is_drat(unsigned n, literal const* c);
bool is_drat(unsigned n, literal const* c, unsigned pos);
@ -75,6 +74,7 @@ namespace sat {
void trace(std::ostream& out, unsigned n, literal const* c, status st);
void display(std::ostream& out) const;
void validate_propagation() const;
bool match(unsigned n, literal const* lits, clause const& c) const;
public:
drat(solver& s);
@ -93,6 +93,16 @@ namespace sat {
void del(literal l1, literal l2);
void del(clause& c);
void verify(clause const& c) { verify(c.size(), c.begin()); }
void verify(unsigned n, literal const* c);
void verify(literal l1, literal l2) { literal lits[2] = {l1, l2}; verify(2, lits); }
void verify(literal l1, literal l2, literal l3) { literal lits[3] = {l1, l2, l3}; verify(3, lits); }
bool contains(clause const& c) { return contains(c.size(), c.begin()); }
bool contains(unsigned n, literal const* c);
bool contains(literal l1, literal l2) { literal lits[2] = {l1, l2}; return contains(2, lits); }
bool contains(literal l1, literal l2, literal l3) { literal lits[3] = {l1, l2, l3}; return contains(3, lits); }
void check_model(model const& m);
};

77
src/sat/sat_elim_eqs.cpp
View file

@ -23,9 +23,15 @@ Revision History:
namespace sat {
elim_eqs::elim_eqs(solver & s):
m_solver(s) {
m_solver(s),
m_to_delete(nullptr) {
}
elim_eqs::~elim_eqs() {
dealloc(m_to_delete);
}
inline literal norm(literal_vector const & roots, literal l) {
if (l.sign())
return ~roots[l.var()];
@ -86,6 +92,12 @@ namespace sat {
m_new_bin.reset();
}
void elim_eqs::drat_delete_clause() {
if (m_solver.m_config.m_drat) {
m_solver.m_drat.del(*m_to_delete->get());
}
}
void elim_eqs::cleanup_clauses(literal_vector const & roots, clause_vector & cs) {
clause_vector::iterator it = cs.begin();
clause_vector::iterator it2 = it;
@ -107,8 +119,16 @@ namespace sat {
it2++;
continue;
}
if (!c.frozen())
if (!c.frozen()) {
m_solver.detach_clause(c);
}
// save clause to be deleted for drat
if (m_solver.m_config.m_drat) {
if (!m_to_delete) m_to_delete = alloc(tmp_clause);
m_to_delete->set(sz, c.begin(), c.is_learned());
}
// apply substitution
for (i = 0; i < sz; i++) {
literal lit = c[i];
@ -124,60 +144,69 @@ namespace sat {
CTRACE("sat", l != norm(roots, l), tout << l << " " << norm(roots, l) << "\n"; tout.flush(););
SASSERT(l == norm(roots, l));
} });
// remove duplicates, and check if it is a tautology
literal l_prev = null_literal;
unsigned j = 0;
literal l_prev = null_literal;
for (i = 0; i < sz; i++) {
literal l = c[i];
if (l == l_prev)
continue;
if (l == ~l_prev)
if (l == ~l_prev) {
break;
}
if (l == l_prev) {
continue;
}
SASSERT(l != ~l_prev);
l_prev = l;
lbool val = m_solver.value(l);
if (val == l_true)
break; // clause was satisfied
if (val == l_false)
if (val == l_true) {
break;
}
if (val == l_false) {
continue; // skip
}
c[j] = l;
j++;
}
TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";);
if (i < sz) {
// clause is a tautology or was simplified to true
m_solver.del_clause(c);
drat_delete_clause();
m_solver.del_clause(c, false);
continue;
}
if (j == 0) {
// empty clause
switch (j) {
case 0:
m_solver.set_conflict(justification());
for (; it != end; ++it) {
*it2 = *it;
it2++;
}
cs.set_end(it2);
return;
}
TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";);
SASSERT(j >= 1);
switch (j) {
return;
case 1:
m_solver.assign(c[0], justification());
m_solver.del_clause(c);
m_solver.del_clause(c, false);
drat_delete_clause();
break;
case 2:
m_solver.mk_bin_clause(c[0], c[1], c.is_learned());
m_solver.del_clause(c);
m_solver.del_clause(c, false);
drat_delete_clause();
break;
default:
SASSERT(*it == &c);
if (j < sz) {
if (m_solver.m_config.m_drat) m_solver.m_drat.del(c);
c.shrink(j);
if (m_solver.m_config.m_drat) m_solver.m_drat.add(c, true);
}
else
else {
c.update_approx();
}
if (m_solver.m_config.m_drat) {
m_solver.m_drat.add(c, true);
drat_delete_clause();
}
DEBUG_CODE(for (literal l : c) VERIFY(l == norm(roots, l)););

4
src/sat/sat_elim_eqs.h
View file

@ -23,6 +23,7 @@ Revision History:
namespace sat {
class solver;
class tmp_clause;
class elim_eqs {
struct bin {
@ -32,6 +33,8 @@ namespace sat {
};
svector<bin> m_new_bin;
solver & m_solver;
tmp_clause* m_to_delete;
void drat_delete_clause();
void save_elim(literal_vector const & roots, bool_var_vector const & to_elim);
void cleanup_clauses(literal_vector const & roots, clause_vector & cs);
void cleanup_bin_watches(literal_vector const & roots);
@ -39,6 +42,7 @@ namespace sat {
bool check_clause(clause const& c, literal_vector const& roots) const;
public:
elim_eqs(solver & s);
~elim_eqs();
void operator()(literal_vector const & roots, bool_var_vector const & to_elim);
};

23
src/sat/sat_simplifier.cpp
View file

@ -349,7 +349,7 @@ namespace sat {
}
if (sz == 2) {
s.mk_bin_clause(c[0], c[1], c.is_learned());
s.del_clause(c);
s.del_clause(c, false);
continue;
}
*it2 = *it;
@ -611,10 +611,15 @@ namespace sat {
break;
}
}
if (j < sz) {
if (s.m_config.m_drat) s.m_drat.del(c);
if (j < sz && !r) {
if (s.m_config.m_drat) {
m_dummy.set(c.size(), c.begin(), c.is_learned());
}
c.shrink(j);
if (s.m_config.m_drat) s.m_drat.add(c, true);
if (s.m_config.m_drat) {
s.m_drat.add(c, true);
s.m_drat.del(*m_dummy.get());
}
}
return r;
}
@ -1272,7 +1277,8 @@ namespace sat {
* unless C contains lit, and it is a tautology.
*/
bool add_ala() {
for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) {
unsigned init_size = m_covered_clause.size();
for (; m_ala_qhead < m_covered_clause.size() && m_ala_qhead < 5*init_size; ++m_ala_qhead) {
literal l = m_covered_clause[m_ala_qhead];
for (watched & w : s.get_wlist(~l)) {
if (w.is_binary_non_learned_clause()) {
@ -1282,7 +1288,6 @@ namespace sat {
return true;
}
if (!s.is_marked(~lit)) {
// if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << l << " " << lit << "\n");
m_covered_clause.push_back(~lit);
m_covered_antecedent.push_back(clause_ante(l, false));
s.mark_visited(~lit);
@ -1312,7 +1317,6 @@ namespace sat {
if (lit1 == null_literal) {
return true;
}
// if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << c << " " << lit1 << "\n");
m_covered_clause.push_back(~lit1);
m_covered_antecedent.push_back(clause_ante(c));
s.mark_visited(~lit1);
@ -1527,6 +1531,7 @@ namespace sat {
block_covered_binary(w, l, blocked, k);
break;
}
s.checkpoint();
}
}
@ -1552,6 +1557,7 @@ namespace sat {
s.set_learned(c);
break;
}
s.checkpoint();
}
}
@ -2019,8 +2025,7 @@ namespace sat {
for (auto & c2 : m_neg_cls) {
m_new_cls.reset();
if (!resolve(c1, c2, pos_l, m_new_cls))
continue;
if (false && v == 767) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n");
continue;
TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";);
if (cleanup_clause(m_new_cls))
continue; // clause is already satisfied.

4
src/sat/sat_solver.cpp
View file

@ -298,14 +298,14 @@ namespace sat {
mk_clause(3, ls, learned);
}
void solver::del_clause(clause& c) {
void solver::del_clause(clause& c, bool enable_drat) {
if (!c.is_learned()) {
m_stats.m_non_learned_generation++;
}
if (c.frozen()) {
--m_num_frozen;
}
if (m_config.m_drat && !m_drat.is_cleaned(c)) {
if (enable_drat && m_config.m_drat && !m_drat.is_cleaned(c)) {
m_drat.del(c);
}
dealloc_clause(&c);

2
src/sat/sat_solver.h
View file

@ -232,7 +232,7 @@ namespace sat {
void defrag_clauses();
bool should_defrag();
bool memory_pressure();
void del_clause(clause & c);
void del_clause(clause & c, bool enable_drat = true);
clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.c_ptr()); }
clause * mk_clause_core(unsigned num_lits, literal * lits) { return mk_clause_core(num_lits, lits, false); }

46
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -60,6 +60,7 @@ class inc_sat_solver : public solver {
atom2bool_var m_map;
scoped_ptr<bit_blaster_rewriter> m_bb_rewriter;
tactic_ref m_preprocess;
bool m_is_cnf;
unsigned m_num_scopes;
sat::literal_vector m_asms;
goal_ref_buffer m_subgoals;
@ -88,6 +89,7 @@ public:
m_fmls_head(0),
m_core(m),
m_map(m),
m_is_cnf(true),
m_num_scopes(0),
m_unknown("no reason given"),
m_internalized_converted(false),
@ -262,7 +264,19 @@ public:
void assert_expr_core2(expr * t, expr * a) override {
if (a) {
m_asmsf.push_back(a);
assert_expr_core(m.mk_implies(a, t));
if (m_is_cnf && is_literal(t) && is_literal(a)) {
assert_expr_core(m.mk_or(::mk_not(m, a), t));
}
else if (m_is_cnf && m.is_or(t) && is_clause(t) && is_literal(a)) {
expr_ref_vector args(m);
args.push_back(::mk_not(m, a));
args.append(to_app(t)->get_num_args(), to_app(t)->get_args());
assert_expr_core(m.mk_or(args.size(), args.c_ptr()));
}
else {
m_is_cnf = false;
assert_expr_core(m.mk_implies(a, t));
}
}
else {
assert_expr_core(t);
@ -272,6 +286,7 @@ public:
ast_manager& get_manager() const override { return m; }
void assert_expr_core(expr * t) override {
TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
m_is_cnf &= is_clause(t);
m_fmls.push_back(t);
}
void set_produce_models(bool f) override {}
@ -545,7 +560,12 @@ private:
SASSERT(!g->proofs_enabled());
TRACE("sat", m_solver.display(tout); g->display(tout););
try {
(*m_preprocess)(g, m_subgoals);
if (m_is_cnf) {
m_subgoals.push_back(g.get());
}
else {
(*m_preprocess)(g, m_subgoals);
}
}
catch (tactic_exception & ex) {
IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
@ -705,6 +725,25 @@ private:
}
}
bool is_literal(expr* n) {
return is_uninterp_const(n) || (m.is_not(n, n) && is_uninterp_const(n));
}
bool is_clause(expr* fml) {
if (is_literal(fml)) {
return true;
}
if (!m.is_or(fml)) {
return false;
}
for (expr* n : *to_app(fml)) {
if (!is_literal(n)) {
return false;
}
}
return true;
}
lbool internalize_formulas() {
if (m_fmls_head == m_fmls.size()) {
return l_true;
@ -712,7 +751,8 @@ private:
dep2asm_t dep2asm;
goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) {
g->assert_expr(m_fmls[i].get());
expr* fml = m_fmls.get(i);
g->assert_expr(fml);
}
lbool res = internalize_goal(g, dep2asm, false);
if (res != l_undef) {

10
src/sat/tactic/atom2bool_var.cpp
View file

@ -38,9 +38,13 @@ void atom2bool_var::mk_var_inv(app_ref_vector & var2expr) const {
}
sat::bool_var atom2bool_var::to_bool_var(expr * n) const {
sat::bool_var v = sat::null_bool_var;
m_mapping.find(n, v);
return v;
unsigned idx = m_id2map.get(n->get_id(), UINT_MAX);
if (idx == UINT_MAX) {
return sat::null_bool_var;
}
else {
return m_mapping[idx].m_value;
}
}
struct collect_boolean_interface_proc {

1
src/smt/smt_context_pp.cpp
View file

@ -200,6 +200,7 @@ namespace smt {
out << "current assignment:\n";
for (literal lit : m_assigned_literals) {
display_literal(out, lit);
if (!is_relevant(lit)) out << " n ";
out << ": ";
display_verbose(out, m_manager, 1, &lit, m_bool_var2expr.c_ptr());
out << "\n";

14
src/smt/theory_arith_core.h
View file

@ -482,12 +482,12 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::mk_idiv_mod_axioms(expr * dividend, expr * divisor) {
th_rewriter & s = get_context().get_rewriter();
if (!m_util.is_zero(divisor)) {
ast_manager & m = get_manager();
// if divisor is zero, then idiv and mod are uninterpreted functions.
expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m);
expr_ref eqz(m), eq(m), lower(m), upper(m);
th_rewriter & s = get_context().get_rewriter();
div = m_util.mk_idiv(dividend, divisor);
mod = m_util.mk_mod(dividend, divisor);
zero = m_util.mk_int(0);
@ -508,6 +508,17 @@ namespace smt {
mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
rational k;
context& ctx = get_context();
if (!m_util.is_numeral(divisor)) {
// (=> (> y 0) (<= (* y (div x y)) x))
// (=> (< y 0) ???)
expr_ref div_ge(m), div_non_pos(m);
div_ge = m_util.mk_ge(m_util.mk_sub(dividend, m_util.mk_mul(divisor, div)), zero);
s(div_ge);
div_non_pos = m_util.mk_le(divisor, zero);
mk_axiom(div_non_pos, div_ge, false);
}
(void)ctx;
if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&
k.is_pos() && k < rational(8)) {
@ -542,6 +553,7 @@ namespace smt {
}
#endif
}
#if 0
// e-matching is too restrictive for multiplication.
// also suffers from use-after free so formulas have to be pinned in solver.

39
src/smt/theory_bv.cpp
View file

@ -53,6 +53,7 @@ namespace smt {
unsigned bv_size = get_bv_size(n);
context & ctx = get_context();
literal_vector & bits = m_bits[v];
TRACE("bv", tout << "v" << v << "\n";);
bits.reset();
for (unsigned i = 0; i < bv_size; i++) {
app * bit = mk_bit2bool(owner, i);
@ -77,6 +78,7 @@ namespace smt {
context & ctx = get_context();
SASSERT(!ctx.b_internalized(n));
TRACE("bv", tout << "bit2bool: " << mk_pp(n, ctx.get_manager()) << "\n";);
expr* first_arg = n->get_arg(0);
if (!ctx.e_internalized(first_arg)) {
@ -94,23 +96,30 @@ namespace smt {
// This will also force the creation of all bits for x.
enode * first_arg_enode = ctx.get_enode(first_arg);
get_var(first_arg_enode);
#if 0
// constant axiomatization moved to catch all case in the end of function.
// numerals are not blasted into bit2bool, so we do this directly.
rational val;
unsigned sz;
if (!ctx.b_internalized(n) && m_util.is_numeral(first_arg, val, sz)) {
TRACE("bv", tout << "bit2bool constants\n";);
theory_var v = first_arg_enode->get_th_var(get_id());
app* owner = first_arg_enode->get_owner();
for (unsigned i = 0; i < sz; ++i) {
ctx.internalize(mk_bit2bool(owner, i), true);
app* e = mk_bit2bool(owner, i);
ctx.internalize(e, true);
}
m_bits[v].reset();
rational bit;
for (unsigned i = 0; i < sz; ++i) {
div(val, rational::power_of_two(i), bit);
mod(bit, rational(2), bit);
m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);
m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);
}
}
#endif
}
enode * arg = ctx.get_enode(first_arg);
@ -135,6 +144,19 @@ namespace smt {
SASSERT(a->m_occs == 0);
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
}
// axiomatize bit2bool on constants.
rational val;
unsigned sz;
if (m_util.is_numeral(first_arg, val, sz)) {
rational bit;
unsigned idx = n->get_decl()->get_parameter(0).get_int();
div(val, rational::power_of_two(idx), bit);
mod(bit, rational(2), bit);
literal lit = ctx.get_literal(n);
if (bit.is_zero()) lit.neg();
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit);
}
}
void theory_bv::process_args(app * n) {
@ -602,8 +624,8 @@ namespace smt {
num *= numeral(2);
}
expr_ref sum(m_autil.mk_add(sz, args.c_ptr()), m);
arith_rewriter arw(m);
ctx.get_rewriter()(sum);
th_rewriter rw(m);
rw(sum);
literal l(mk_eq(n, sum, false));
TRACE("bv",
tout << mk_pp(n, m) << "\n";
@ -622,7 +644,9 @@ namespace smt {
context& ctx = get_context();
process_args(n);
mk_enode(n);
mk_bits(ctx.get_enode(n)->get_th_var(get_id()));
theory_var v = ctx.get_enode(n)->get_th_var(get_id());
mk_bits(v);
if (!ctx.relevancy()) {
assert_int2bv_axiom(n);
}
@ -1179,7 +1203,7 @@ namespace smt {
m_prop_queue.push_back(var_pos(curr->m_var, curr->m_idx));
curr = curr->m_next;
}
TRACE("bv", tout << m_prop_queue.size() << "\n";);
TRACE("bv", tout << "prop queue size: " << m_prop_queue.size() << "\n";);
propagate_bits();
}
}
@ -1196,7 +1220,7 @@ namespace smt {
literal_vector & bits = m_bits[v];
literal bit = bits[idx];
lbool val = ctx.get_assignment(bit);
lbool val = ctx.get_assignment(bit);
if (val == l_undef) {
continue;
}
@ -1213,6 +1237,7 @@ namespace smt {
SASSERT(bit != ~bit2);
lbool val2 = ctx.get_assignment(bit2);
TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";);
TRACE("bv", tout << bit << " " << bit2 << "\n";);
if (val != val2) {
literal consequent = bit2;

24
src/smt/theory_pb.cpp
View file

@ -723,10 +723,11 @@ namespace smt {
ineqs = alloc(ptr_vector<ineq>);
m_var_infos[lit.var()].m_lit_watch[lit.sign()] = ineqs;
}
for (auto* c1 : *ineqs) {
//if (c1 == c) return;
SASSERT (c1 != c);
}
DEBUG_CODE(
for (auto* c1 : *ineqs) {
//if (c1 == c) return;
SASSERT (c1 != c);
});
ineqs->push_back(c);
}
@ -965,9 +966,9 @@ namespace smt {
justification* js = nullptr;
c.inc_propagations(*this);
if (!resolve_conflict(c, lits)) {
if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
}
if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
}
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
}
SASSERT(ctx.inconsistent());
@ -1194,10 +1195,15 @@ namespace smt {
// perform unit propagation
if (maxsum >= c.mpz_k() && maxsum - mininc < c.mpz_k()) {
literal_vector& lits = get_unhelpful_literals(c, true);
// for (literal lit : lits) SASSERT(ctx.get_assignment(lit) == l_true);
lits.push_back(c.lit());
// SASSERT(ctx.get_assignment(c.lit()) == l_true);
for (unsigned i = 0; i < sz; ++i) {
DEBUG_CODE(validate_assign(c, lits, c.lit(i)););
add_assign(c, lits, c.lit(i));
literal lit = c.lit(i);
if (ctx.get_assignment(lit) == l_undef) {
DEBUG_CODE(validate_assign(c, lits, lit););
add_assign(c, lits, c.lit(i));
}
}
}
}

52
src/smt/theory_seq.cpp
View file

@ -251,7 +251,7 @@ void theory_seq::init(context* ctx) {
m_arith_value.init(ctx);
}
#define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(10, verbose_stream() << s << "\n"); }
#define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(11, verbose_stream() << s << "\n"); }
final_check_status theory_seq::final_check_eh() {
@ -262,6 +262,7 @@ final_check_status theory_seq::final_check_eh() {
m_new_propagation = false;
TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
TRACE("seq_verbose", get_context().display(tout););
if (simplify_and_solve_eqs()) {
++m_stats.m_solve_eqs;
TRACEFIN("solve_eqs");
@ -3495,12 +3496,11 @@ bool theory_seq::add_itos_val_axiom(expr* e) {
}
bool theory_seq::add_stoi_val_axiom(expr* e) {
context& ctx = get_context();
expr* n = nullptr;
rational val, val2;
VERIFY(m_util.str.is_stoi(e, n));
TRACE("seq", tout << mk_pp(e, m) << " " << ctx.get_scope_level () << " " << get_length(n, val) << " " << val << "\n";);
TRACE("seq", tout << mk_pp(e, m) << " " << get_context().get_scope_level () << " " << get_length(n, val) << " " << val << "\n";);
if (m_util.str.is_itos(n)) {
return false;
@ -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));
}
@ -3951,7 +3953,6 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
app* theory_seq::mk_value(app* e) {
expr_ref result(m);
context& ctx = get_context();
e = get_ite_value(e);
result = m_rep.find(e);
@ -4260,6 +4261,9 @@ void theory_seq::deque_axiom(expr* n) {
else if (m_util.str.is_at(n)) {
add_at_axiom(n);
}
else if (m_util.str.is_nth(n)) {
add_nth_axiom(n);
}
else if (m_util.str.is_string(n)) {
add_elim_string_axiom(n);
}
@ -4586,7 +4590,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));
@ -4705,7 +4714,6 @@ bool theory_seq::lower_bound2(expr* _e, rational& lo) {
bool theory_seq::get_length(expr* e, rational& val) const {
context& ctx = get_context();
rational val1;
expr_ref len(m), len_val(m);
expr* e1 = nullptr, *e2 = nullptr;
@ -4960,6 +4968,17 @@ void theory_seq::add_at_axiom(expr* e) {
add_axiom(~i_ge_len_s, mk_eq(e, emp, false));
}
void theory_seq::add_nth_axiom(expr* e) {
expr* s = nullptr, *i = nullptr;
rational n;
zstring str;
VERIFY(m_util.str.is_nth(e, s, i));
if (m_util.str.is_string(s, str) && m_autil.is_numeral(i, n) && n.is_unsigned() && n.get_unsigned() < str.length()) {
app_ref ch(m_util.str.mk_char(str[n.get_unsigned()]), m);
add_axiom(mk_eq(ch, e, false));
}
}
/*
lit => s = (nth s 0) ++ (nth s 1) ++ ... ++ (nth s idx) ++ (tail s idx)
@ -5426,6 +5445,7 @@ void theory_seq::relevant_eh(app* n) {
m_util.str.is_replace(n) ||
m_util.str.is_extract(n) ||
m_util.str.is_at(n) ||
m_util.str.is_nth(n) ||
m_util.str.is_empty(n) ||
m_util.str.is_string(n) ||
m_util.str.is_itos(n) ||
@ -5562,14 +5582,9 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
propagate_lit(nullptr, 1, &lit, false_literal);
return;
}
if (_idx.get_unsigned() > m_max_unfolding_depth &&
m_max_unfolding_lit != null_literal && ctx.get_scope_level() > 0) {
propagate_lit(nullptr, 1, &lit, ~m_max_unfolding_lit);
return;
}
expr_ref len = mk_len(e);
literal_vector lits;
lits.push_back(~lit);
if (aut->is_final_state(src)) {
@ -5579,9 +5594,11 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
else {
propagate_lit(nullptr, 1, &lit, ~mk_literal(m_autil.mk_le(len, idx)));
}
eautomaton::moves mvs;
aut->get_moves_from(src, mvs);
TRACE("seq", tout << mvs.size() << "\n";);
TRACE("seq", tout << mk_pp(acc, m) << " #moves " << mvs.size() << "\n";);
for (auto const& mv : mvs) {
expr_ref nth = mk_nth(e, idx);
expr_ref t = mv.t()->accept(nth);
@ -5590,6 +5607,11 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
lits.push_back(step);
}
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
if (_idx.get_unsigned() > m_max_unfolding_depth &&
m_max_unfolding_lit != null_literal && ctx.get_scope_level() > 0) {
propagate_lit(nullptr, 1, &lit, ~m_max_unfolding_lit);
}
}
void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {

1
src/smt/theory_seq.h
View file

@ -575,6 +575,7 @@ namespace smt {
expr_ref add_elim_string_axiom(expr* n);
void add_at_axiom(expr* n);
void add_nth_axiom(expr* n);
void add_in_re_axiom(expr* n);
void add_itos_axiom(expr* n);
void add_stoi_axiom(expr* n);

10
src/smt/theory_str.cpp
View file

@ -1682,10 +1682,10 @@ namespace smt {
expr_ref i1(mk_int_var("i1"), m);
expr_ref result(mk_str_var("result"), m);
expr * replaceS;
expr * replaceT;
expr * replaceTPrime;
u.str.is_replace(ex, replaceS, replaceT, replaceTPrime);
expr * replaceS = nullptr;
expr * replaceT = nullptr;
expr * replaceTPrime = nullptr;
VERIFY(u.str.is_replace(ex, replaceS, replaceT, replaceTPrime));
// t empty => result = (str.++ t' s)
expr_ref emptySrcAst(ctx.mk_eq_atom(replaceT, mk_string("")), m);
@ -4851,6 +4851,7 @@ namespace smt {
bool theory_str::get_arith_value(expr* e, rational& val) const {
context& ctx = get_context();
ast_manager & m = get_manager();
(void)m;
if (!ctx.e_internalized(e)) {
return false;
}
@ -8255,6 +8256,7 @@ namespace smt {
void theory_str::check_eqc_concat_concat(std::set<expr*> & eqc_concat_lhs, std::set<expr*> & eqc_concat_rhs) {
ast_manager & m = get_manager();
(void)m;
int hasCommon = 0;
if (!eqc_concat_lhs.empty() && !eqc_concat_rhs.empty()) {

6
src/util/debug.cpp
View file

@ -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)

11
src/util/debug.h
View file

@ -44,6 +44,17 @@ 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 __EMSCRIPTEN__
#define NO_Z3_DEBUGGER
#endif
#ifdef NO_Z3_DEBUGGER
#define INVOKE_DEBUGGER() exit(ERR_INTERNAL_FATAL)
#else

2
src/util/str_hashtable.h
View file

@ -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_ */

9
src/util/symbol.cpp
View file

@ -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);
}

6
src/util/trace.cpp
View file

@ -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() {