mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

fix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-06-08 09:04:41 -07:00
parent 9c4003d12e
commit e7065e3984
3 changed files with 20 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_context_pp.cpp
View file

@ -510,6 +510,9 @@ namespace smt {
#else #else
strm << "lemma_" << (++m_lemma_id) << ".smt2"; strm << "lemma_" << (++m_lemma_id) << ".smt2";
#endif #endif
if (m_lemma_id == 1303) {
verbose_stream() << "lemma\n";
}
return strm.str(); return strm.str();
} }

16
src/smt/theory_lra.cpp
View file

@ -354,6 +354,7 @@ class theory_lra::imp {
enode* e = mk_enode(n); enode* e = mk_enode(n);
theory_var v = e->get_th_var(get_id()); theory_var v = e->get_th_var(get_id());
TRACE("add_bug", tout << mk_pp(n, m) << " - v" << v << "\n");
if (v == null_theory_var) if (v == null_theory_var)
v = internalize_linearized_def(n, st); v = internalize_linearized_def(n, st);
return v; return v;
@ -372,8 +373,10 @@ class theory_lra::imp {
} }
} }
if (a.is_extended_numeral(arg, val)) if (a.is_extended_numeral(arg, val)) {
st.add(internalize_numeral(arg, val), sign); st.add(internalize_numeral(arg, val), sign);
return;
}
else if (a.is_mul(arg, arg1, arg2)) { else if (a.is_mul(arg, arg1, arg2)) {
if (a.is_extended_numeral(arg2, val)) if (a.is_extended_numeral(arg2, val))
std::swap(arg1, arg2); std::swap(arg1, arg2);
@ -386,8 +389,7 @@ class theory_lra::imp {
return; return;
} }
} }
else st.add(internalize_term_core(arg), sign);
st.add(internalize_term_core(arg), sign);
} }
theory_var internalize_numeral(app* n, rational const& val) { theory_var internalize_numeral(app* n, rational const& val) {
@ -508,7 +510,7 @@ class theory_lra::imp {
return mk_var(n); return mk_var(n);
ctx().internalize(n->get_arg(0), false); ctx().internalize(n->get_arg(0), false);
ctx().internalize(n->get_arg(1), false); ctx().internalize(n->get_arg(1), false);
enode* e = mk_enode(n); mk_enode(n);
return mk_var(n); return mk_var(n);
} }
@ -2852,9 +2854,9 @@ public:
CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
updt_unassigned_bounds(v, -1); updt_unassigned_bounds(v, -1);
TRACE("arith", TRACE("arith",
ctx().display_literals_verbose(tout, m_core); ctx().display_literals_smt2(tout, m_core);
tout << "\n --> "; tout << "\n --> ";
ctx().display_literal_verbose(tout, lit); ctx().display_literal_smt2(tout, lit);
tout << "\n"; tout << "\n";
display_evidence(tout, m_explanation); display_evidence(tout, m_explanation);
lp().print_implied_bound(be, tout); lp().print_implied_bound(be, tout);

11
src/smt/theory_special_relations.cpp
View file

@ -888,9 +888,14 @@ namespace smt {
func_decl* memf, *nextf, *connectedf; func_decl* memf, *nextf, *connectedf;
std::string member, next, connected_sym;
unsigned index = r.decl()->get_parameter(0).get_int();
member = "member" + std::to_string(index);
next = "next" + std::to_string(index);
connected_sym = "connected" + std::to_string(index);
{ {
sort* dom[2] = { s, listS }; sort* dom[2] = { s, listS };
recfun::promise_def mem = p.ensure_def(symbol("member"), 2, dom, m.mk_bool_sort(), true); recfun::promise_def mem = p.ensure_def(symbol(member), 2, dom, m.mk_bool_sort(), true);
memf = mem.get_def()->get_decl(); memf = mem.get_def()->get_decl();
var_ref xV(m.mk_var(1, s), m); var_ref xV(m.mk_var(1, s), m);
@ -913,7 +918,7 @@ namespace smt {
{ {
sort* dom[5] = { s, s, listS, listS, tup }; sort* dom[5] = { s, s, listS, listS, tup };
recfun::promise_def nxt = p.ensure_def(symbol("next"), 5, dom, tup, true); recfun::promise_def nxt = p.ensure_def(symbol(next), 5, dom, tup, true);
nextf = nxt.get_def()->get_decl(); nextf = nxt.get_def()->get_decl();
expr_ref next_body(m); expr_ref next_body(m);
@ -934,7 +939,7 @@ namespace smt {
{ {
sort* dom[3] = { listS, s, listS }; sort* dom[3] = { listS, s, listS };
recfun::promise_def connected = p.ensure_def(symbol("connected"), 3, dom, m.mk_bool_sort(), true); recfun::promise_def connected = p.ensure_def(symbol(connected_sym), 3, dom, m.mk_bool_sort(), true);
connectedf = connected.get_def()->get_decl(); connectedf = connected.get_def()->get_decl();
var_ref AV(m.mk_var(2, listS), m); var_ref AV(m.mk_var(2, listS), m);
var_ref dstV(m.mk_var(1, s), m); var_ref dstV(m.mk_var(1, s), m);