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

#6364

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-20 04:48:13 -07:00
parent f6595c161f
commit 2842c27e92
4 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/sat/smt/arith_diagnostics.cpp
View file

@ -152,7 +152,6 @@ namespace arith {
solver& a = dynamic_cast<solver&>(*s.fid2solver(fid));
char const* name;
expr_ref_vector args(m);
sort_ref_vector sorts(m);
switch (m_ty) {
case hint_type::farkas_h:
@ -182,11 +181,6 @@ namespace arith {
args.push_back(arith.mk_int(1));
args.push_back(eq);
}
for (expr* arg : args)
sorts.push_back(arg->get_sort());
sort* range = m.mk_proof_sort();
func_decl* d = m.mk_func_decl(symbol(name), args.size(), sorts.data(), range);
expr* r = m.mk_app(d, args);
return r;
return m.mk_app(symbol(name), args.size(), args.data(), m.mk_proof_sort());
}
}

2
src/sat/smt/euf_solver.cpp
View file

@ -674,7 +674,7 @@ namespace euf {
}
for (auto const& [e, v] : replay.m)
if (si.is_bool_op(e))
if (si.is_bool_op(e) && !si.is_cached(to_app(e), sat::literal(v, false)))
si.cache(to_app(e), sat::literal(v, false));
if (relevancy_enabled())

1
src/sat/smt/sat_internalizer.h
View file

@ -26,6 +26,7 @@ namespace sat {
virtual literal internalize(expr* e, bool learned) = 0;
virtual bool_var to_bool_var(expr* e) = 0;
virtual bool_var add_bool_var(expr* e) = 0;
virtual bool is_cached(app* t, literal l) const = 0;
virtual void cache(app* t, literal l) = 0;
virtual void uncache(literal l) = 0;
virtual void push() = 0;

7
src/sat/tactic/goal2sat.cpp
View file

@ -276,6 +276,13 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_lit2app.insert(l.index(), t);
m_cache_trail.push_back(t);
}
bool is_cached(app* t, sat::literal l) const override {
if (!m_app2lit.contains(t))
return false;
SASSERT(m_app2lit[t] == l);
return true;
}
void convert_atom(expr * t, bool root, bool sign) {
SASSERT(m.is_bool(t));