mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

replace __debug__ by Z3_DEBUG #2225

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-27 13:47:53 -07:00
parent 6af6617e36
commit 944ce1135b
4 changed files with 162 additions and 146 deletions
Download patch file Download diff file Expand all files Collapse all files

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

File diff suppressed because it is too large Load diff

18
src/api/python/z3/z3util.py
View file

@ -75,7 +75,7 @@ def ehash(v):
x_783810685_1 x_783810685_1 x_783810685_2 x_783810685_1 x_783810685_1 x_783810685_2
""" """
if __debug__: if Z3_DEBUG:
assert is_expr(v) assert is_expr(v)
return "{}_{}_{}".format(str(v),v.hash(),v.sort_kind()) return "{}_{}_{}".format(str(v),v.hash(),v.sort_kind())
@ -148,7 +148,7 @@ def get_vars(f,rs=[]):
[x, y, a, b] [x, y, a, b]
""" """
if __debug__: if Z3_DEBUG:
assert is_expr(f) assert is_expr(f)
if is_const(f): if is_const(f):
@ -228,13 +228,13 @@ def prove(claim,assume=None,verbose=0):
""" """
if __debug__: if Z3_DEBUG:
assert not assume or is_expr(assume) assert not assume or is_expr(assume)
to_prove = claim to_prove = claim
if assume: if assume:
if __debug__: if Z3_DEBUG:
is_proved,_ = prove(Not(assume)) is_proved,_ = prove(Not(assume))
def _f(): def _f():
@ -266,7 +266,7 @@ def prove(claim,assume=None,verbose=0):
elif models == False: #unsat elif models == False: #unsat
return True,None return True,None
else: #sat else: #sat
if __debug__: if Z3_DEBUG:
assert isinstance(models,list) assert isinstance(models,list)
if models: if models:
@ -312,7 +312,7 @@ def get_models(f,k):
""" """
if __debug__: if Z3_DEBUG:
assert is_expr(f) assert is_expr(f)
assert k>=1 assert k>=1
@ -448,13 +448,13 @@ def myBinOp(op,*L):
AssertionError AssertionError
""" """
if __debug__: if Z3_DEBUG:
assert op == Z3_OP_OR or op == Z3_OP_AND or op == Z3_OP_IMPLIES assert op == Z3_OP_OR or op == Z3_OP_AND or op == Z3_OP_IMPLIES
if len(L)==1 and (isinstance(L[0],list) or isinstance(L[0],tuple)): if len(L)==1 and (isinstance(L[0],list) or isinstance(L[0],tuple)):
L = L[0] L = L[0]
if __debug__: if Z3_DEBUG:
assert all(not isinstance(l,bool) for l in L) assert all(not isinstance(l,bool) for l in L)
L = [l for l in L if is_expr(l)] L = [l for l in L if is_expr(l)]
@ -493,7 +493,7 @@ def model_str(m,as_str=True):
see doctest exampels from function prove() see doctest exampels from function prove()
""" """
if __debug__: if Z3_DEBUG:
assert m is None or m == [] or isinstance(m,ModelRef) assert m is None or m == [] or isinstance(m,ModelRef)
if m : if m :

11
src/nlsat/nlsat_solver.cpp
View file

@ -1347,6 +1347,7 @@ namespace nlsat {
restore_order(); restore_order();
CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout);); CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout););
CTRACE("nlsat", r == l_false, display(tout);); CTRACE("nlsat", r == l_false, display(tout););
VERIFY(r != l_true || check_satisfied(m_clauses));
return r; return r;
} }
@ -1867,11 +1868,17 @@ namespace nlsat {
if (m_bk != null_bool_var) if (m_bk != null_bool_var)
num = m_bk; num = m_bk;
for (bool_var b = 0; b < num; b++) { for (bool_var b = 0; b < num; b++) {
SASSERT(check_satisfied(m_bwatches[b])); if (!check_satisfied(m_bwatches[b])) {
UNREACHABLE();
return false;
}
} }
if (m_xk != null_var) { if (m_xk != null_var) {
for (var x = 0; x < m_xk; x++) { for (var x = 0; x < m_xk; x++) {
SASSERT(check_satisfied(m_watches[x])); if (!check_satisfied(m_watches[x])) {
UNREACHABLE();
return false;
}
} }
} }
return true; return true;

7
src/nlsat/tactic/nlsat_tactic.cpp
View file

@ -85,6 +85,9 @@ class nlsat_tactic : public tactic {
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
if (!model.is_true(g.form(i))) { if (!model.is_true(g.form(i))) {
TRACE("nlsat", tout << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";); TRACE("nlsat", tout << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";);
IF_VERBOSE(0, verbose_stream() << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";);
IF_VERBOSE(1, verbose_stream() << model << "\n");
IF_VERBOSE(1, m_solver.display(verbose_stream()));
return false; return false;
} }
} }
@ -123,6 +126,7 @@ class nlsat_tactic : public tactic {
md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false()); md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false());
} }
DEBUG_CODE(eval_model(*md.get(), g);); DEBUG_CODE(eval_model(*md.get(), g););
// VERIFY(eval_model(*md.get(), g));
mc = model2model_converter(md.get()); mc = model2model_converter(md.get());
return ok; return ok;
} }
@ -149,6 +153,9 @@ class nlsat_tactic : public tactic {
t2x.mk_inv(m_display_var.m_var2expr); t2x.mk_inv(m_display_var.m_var2expr);
m_solver.set_display_var(m_display_var); m_solver.set_display_var(m_display_var);
IF_VERBOSE(10000, m_solver.display(verbose_stream()));
IF_VERBOSE(10000, g->display(verbose_stream()));
lbool st = m_solver.check(); lbool st = m_solver.check();
if (st == l_undef) { if (st == l_undef) {