From 25106866b52eea709561024c9bfca0a59e3ee867 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 30 Aug 2020 14:46:31 -0700
Subject: [PATCH] fix dotnet build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/dotnet/Goal.cs | 2 +-
src/ast/euf/euf_egraph.cpp | 51 ++++++++++---------
src/ast/euf/euf_egraph.h | 12 ++++-
src/sat/smt/euf_solver.cpp | 96 +++++++++++++++++++----------------
src/sat/smt/euf_solver.h | 32 +++++++-----
src/sat/smt/sat_smt.h | 6 ++-
src/sat/tactic/goal2sat.cpp | 35 ++++++++++---
src/sat/tactic/goal2sat.h | 4 +-
src/sat/tactic/sat_tactic.cpp | 14 ++---
9 files changed, 153 insertions(+), 99 deletions(-)
diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs
index 05edb36b1..c31f649f7 100644
--- a/src/api/dotnet/Goal.cs
+++ b/src/api/dotnet/Goal.cs
@@ -227,7 +227,7 @@ namespace Microsoft.Z3
/// <returns>A string representation of the Goal.</returns>
public string ToDimacs(bool include_names = true)
{
- return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject, include_names);
+ return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject, (byte)(include_names ? 1 : 0));
}
/// <summary>
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 1bb193e86..c12815bfa 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -341,6 +341,28 @@ namespace euf {
n->invariant();
}
+ std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
+ out << std::setw(5)
+ << n->get_owner_id() << " := ";
+ out << n->get_root()->get_owner_id() << " ";
+ expr* f = n->get_owner();
+ if (is_app(f))
+ out << to_app(f)->get_decl()->get_name() << " ";
+ else if (is_quantifier(f))
+ out << "q ";
+ else
+ out << "v ";
+ for (enode* arg : enode_args(n))
+ out << arg->get_owner_id() << " ";
+ for (unsigned i = n->num_args(); i < max_args; ++i)
+ out << " ";
+ out << "\t";
+ for (enode* p : enode_parents(n))
+ out << p->get_owner_id() << " ";
+ out << "\n";
+ return out;
+ }
+
std::ostream& egraph::display(std::ostream& out) const {
m_table.display(out);
unsigned max_args = 0;
@@ -348,24 +370,7 @@ namespace euf {
max_args = std::max(max_args, n->num_args());
for (enode* n : m_nodes) {
- out << std::setw(5)
- << n->get_owner_id() << " := ";
- out << n->get_root()->get_owner_id() << " ";
- expr* f = n->get_owner();
- if (is_app(f))
- out << to_app(f)->get_decl()->get_name() << " ";
- else if (is_quantifier(f))
- out << "q ";
- else
- out << "v ";
- for (enode* arg : enode_args(n))
- out << arg->get_owner_id() << " ";
- for (unsigned i = n->num_args(); i < max_args; ++i)
- out << " ";
- out << "\t";
- for (enode* p : enode_parents(n))
- out << p->get_owner_id() << " ";
- out << "\n";
+ display(out, max_args, n);
}
return out;
}
@@ -392,16 +397,16 @@ namespace euf {
}
expr* e2 = tr(e1);
enode* n2 = mk(e2, args.size(), args.c_ptr());
- m_exprs.push_back(e2);
- m_nodes.push_back(n2);
old_expr2new_enode.setx(e1->get_id(), n2, nullptr);
}
- for (unsigned i = 0; i < src.m_nodes.size(); ++i) {
+ for (unsigned i = 0; i < src.m_nodes.size(); ++i) {
enode* n1 = src.m_nodes[i];
- enode* n1t = n1->m_target;
+ enode* n1t = n1->m_target;
enode* n2 = m_nodes[i];
- enode* n2t = n1t ? old_expr2new_enode[n1t->get_owner_id()] : nullptr;
+ enode* n2t = n1t ? old_expr2new_enode[n1->get_owner_id()] : nullptr;
SASSERT(!n1t || n2t);
+ SASSERT(!n1t || src.m.get_sort(n1->get_owner()) == src.m.get_sort(n1t->get_owner()));
+ SASSERT(!n1t || m.get_sort(n2->get_owner()) == m.get_sort(n2t->get_owner()));
if (n1t && n2->get_root() != n2t->get_root()) {
merge(n2, n2t, n1->m_justification.copy(copy_justification));
}
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 76f946ee1..b68ee0b20 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -101,6 +101,8 @@ namespace euf {
}
template <typename T>
void explain_todo(ptr_vector<T>& justifications);
+
+ std::ostream& display(std::ostream& out, unsigned max_args, enode* n) const;
public:
egraph(ast_manager& m): m(m), m_table(m), m_exprs(m) {}
@@ -140,9 +142,17 @@ namespace euf {
enode_vector const& nodes() const { return m_nodes; }
void invariant();
void copy_from(egraph const& src, std::function<void*(void*)>& copy_justification);
- std::ostream& display(std::ostream& out) const;
+ struct e_pp {
+ egraph const& g;
+ enode* n;
+ e_pp(egraph const& g, enode* n) : g(g), n(n) {}
+ std::ostream& display(std::ostream& out) const { return g.display(out, 0, n); }
+ };
+ e_pp pp(enode* n) const { return e_pp(*this, n); }
+ std::ostream& display(std::ostream& out) const;
void collect_statistics(statistics& st) const;
};
inline std::ostream& operator<<(std::ostream& out, egraph const& g) { return g.display(out); }
+ inline std::ostream& operator<<(std::ostream& out, egraph::e_pp const& p) { return p.display(out); }
}
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 119abeead..264f087c4 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -32,9 +32,10 @@ namespace euf {
* retrieve extension that is associated with Boolean variable.
*/
sat::th_solver* solver::get_solver(sat::bool_var v) {
- if (v >= m_var2node.size())
+ unsigned idx = literal(v, false).index();
+ if (idx >= m_lit2node.size())
return nullptr;
- euf::enode* n = m_var2node[v].first;
+ euf::enode* n = m_lit2node[idx];
if (!n)
return nullptr;
return get_solver(n->get_owner());
@@ -53,6 +54,8 @@ namespace euf {
auto* ext = m_id2solver.get(fid, nullptr);
if (ext)
return ext;
+ if (fid == m.get_basic_family_id())
+ return nullptr;
pb_util pb(m);
if (pb.get_family_id() == fid) {
ext = alloc(sat::ba_solver, m, si);
@@ -74,8 +77,11 @@ namespace euf {
}
void solver::unhandled_function(func_decl* f) {
+ if (m_unhandled_functions.contains(f))
+ return;
+ m_unhandled_functions.push_back(f);
+ m_trail.push_back(new (m_region) push_back_vector<solver, func_decl_ref_vector>(m_unhandled_functions));
IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
- // TBD: set some state with the unhandled function.
}
bool solver::propagate(literal l, ext_constraint_idx idx) {
@@ -88,7 +94,7 @@ namespace euf {
void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r) {
auto* ext = sat::constraint_base::to_extension(idx);
if (ext == this)
- get_antecedents(l, *constraint::from_idx(idx), r);
+ get_antecedents(l, constraint::from_idx(idx), r);
else
ext->get_antecedents(l, idx, r);
}
@@ -96,8 +102,6 @@ namespace euf {
void solver::get_antecedents(literal l, constraint& j, literal_vector& r) {
m_explain.reset();
euf::enode* n = nullptr;
- bool sign = false;
- enode_bool_pair p;
// init_ackerman();
@@ -107,20 +111,19 @@ namespace euf {
m_egraph.explain<unsigned>(m_explain);
break;
case constraint::kind_t::eq:
- n = m_var2node[l.var()].first;
+ n = m_lit2node[l.index()];
SASSERT(n);
SASSERT(m_egraph.is_equality(n));
m_egraph.explain_eq<unsigned>(m_explain, n->get_arg(0), n->get_arg(1), n->commutative());
break;
case constraint::kind_t::lit:
- p = m_var2node[l.var()];
- n = p.first;
- sign = l.sign() != p.second;
+ n = m_lit2node[l.index()];
SASSERT(n);
SASSERT(m.is_bool(n->get_owner()));
- m_egraph.explain_eq<unsigned>(m_explain, n, (sign ? mk_false() : mk_true()), false);
+ m_egraph.explain_eq<unsigned>(m_explain, n, (l.sign() ? mk_false() : mk_true()), false);
break;
default:
+ std::cout << (unsigned)j.kind() << "\n";
UNREACHABLE();
}
for (unsigned* idx : m_explain)
@@ -135,20 +138,22 @@ namespace euf {
return;
}
- auto p = m_var2node.get(l.var(), enode_bool_pair(nullptr, false));
- if (!p.first)
+ bool sign = l.sign();
+ unsigned idx = sat::literal(l.var(), false).index();
+ auto n = m_lit2node.get(idx, nullptr);
+ if (!n)
return;
force_push();
- bool sign = p.second != l.sign();
- euf::enode* n = p.first;
+
expr* e = n->get_owner();
if (m.is_eq(e) && !sign) {
euf::enode* na = n->get_arg(0);
euf::enode* nb = n->get_arg(1);
m_egraph.merge(na, nb, base_ptr() + l.index());
}
- else {
+ else {
euf::enode* nb = sign ? mk_false() : mk_true();
+ std::cout << "merge " << n->get_owner_id() << " " << sign << " " << nb->get_owner_id() << "\n";
m_egraph.merge(n, nb, base_ptr() + l.index());
}
// TBD: delay propagation?
@@ -216,39 +221,36 @@ namespace euf {
}
void solver::push() {
- ++m_num_scopes;
+ scope s;
+ s.m_lit_lim = m_lit_trail.size();
+ s.m_trail_lim = m_trail.size();
+ m_scopes.push_back(s);
+ m_region.push_scope();
+ for (auto* e : m_solvers)
+ e->push();
+ m_egraph.push();
}
void solver::force_push() {
for (; m_num_scopes > 0; --m_num_scopes) {
- scope s;
- s.m_bool_var_lim = m_bool_var_trail.size();
- s.m_trail_lim = m_trail.size();
- m_scopes.push_back(s);
- for (auto* e : m_solvers)
- e->push();
- m_egraph.push();
+
}
}
void solver::pop(unsigned n) {
- if (n <= m_num_scopes) {
- m_num_scopes -= n;
- return;
- }
- n -= m_num_scopes;
m_egraph.pop(n);
for (auto* e : m_solvers)
e->pop(n);
- scope & s = m_scopes[m_scopes.size() - n];
+ scope const & s = m_scopes[m_scopes.size() - n];
- for (unsigned i = m_bool_var_trail.size(); i-- > s.m_bool_var_lim; )
- m_var2node[m_bool_var_trail[i]] = enode_bool_pair(nullptr, false);
- m_bool_var_trail.shrink(s.m_bool_var_lim);
+ for (unsigned i = m_lit_trail.size(); i-- > s.m_lit_lim; )
+ m_lit2node[m_lit_trail[i]] = nullptr;
+ m_lit_trail.shrink(s.m_lit_lim);
undo_trail_stack(*this, m_trail, s.m_trail_lim);
-
+
+ m_region.pop_scope(n);
m_scopes.shrink(m_scopes.size() - n);
}
@@ -278,6 +280,10 @@ namespace euf {
std::ostream& solver::display(std::ostream& out) const {
m_egraph.display(out);
+ for (unsigned idx : m_lit_trail) {
+ euf::enode* n = m_lit2node[idx];
+ out << sat::to_literal(idx) << ": " << m_egraph.pp(n);
+ }
for (auto* e : m_solvers)
e->display(out);
return out;
@@ -363,8 +369,8 @@ namespace euf {
unsigned solver::max_var(unsigned w) const {
for (auto* e : m_solvers)
w = e->max_var(w);
- for (unsigned sz = m_var2node.size(); sz-- > 0; ) {
- euf::enode* n = m_var2node[sz].first;
+ for (unsigned sz = m_lit2node.size(); sz-- > 0; ) {
+ euf::enode* n = m_lit2node[sz];
if (n && m.is_bool(n->get_owner())) {
w = std::max(w, sz);
break;
@@ -452,13 +458,12 @@ namespace euf {
return n;
if (si.is_bool_op(e)) {
sat::literal lit = si.internalize(e);
- enode_bool_pair bp(nullptr, false);
- n = m_var2node.get(lit.var(), bp).first;
+ n = m_lit2node.get(lit.index(), nullptr);
if (n)
return n;
n = m_egraph.mk(e, 0, nullptr);
- attach_bool_var(lit.var(), lit.sign(), n);
+ attach_lit(lit, n);
if (!m.is_true(e) && !m.is_false(e))
s().set_external(lit.var());
return n;
@@ -476,15 +481,16 @@ namespace euf {
expr* e = n->get_owner();
if (m.is_bool(e)) {
sat::bool_var v = si.add_bool_var(e);
- attach_bool_var(v, false, n);
+ attach_lit(literal(v, false), n);
}
}
- void solver::attach_bool_var(sat::bool_var v, bool sign, euf::enode* n) {
- m_var2node.reserve(v + 1, enode_bool_pair(nullptr, false));
- SASSERT(m_var2node[v].first == nullptr);
- m_var2node[v] = euf::enode_bool_pair(n, sign);
- m_bool_var_trail.push_back(v);
+ void solver::attach_lit(literal lit, euf::enode* n) {
+ unsigned v = lit.index();
+ m_lit2node.reserve(v + 1, nullptr);
+ SASSERT(m_lit2node[v] == nullptr);
+ m_lit2node[v] = n;
+ m_lit_trail.push_back(v);
}
bool solver::to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) {
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index f5fe6170f..8bc69644b 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -42,7 +42,9 @@ namespace euf {
public:
constraint(kind_t k) : m_kind(k) {}
kind_t kind() const { return m_kind; }
- static constraint* from_idx(size_t z) { return reinterpret_cast<constraint*>(z); }
+ static constraint& from_idx(size_t z) {
+ return *reinterpret_cast<constraint*>(sat::constraint_base::idx2mem(z));
+ }
size_t to_index() const { return sat::constraint_base::mem2base(this); }
};
@@ -54,11 +56,11 @@ namespace euf {
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
- struct scope {
- unsigned m_bool_var_lim;
- unsigned m_trail_lim;
- };
- typedef ptr_vector<trail<solver> > trail_stack;
+ struct scope {
+ unsigned m_lit_lim;
+ unsigned m_trail_lim;
+ };
+ typedef ptr_vector<trail<solver> > trail_stack;
ast_manager& m;
atom2bool_var& m_expr2var;
@@ -66,8 +68,9 @@ namespace euf {
smt_params m_config;
euf::egraph m_egraph;
stats m_stats;
-
- trail_stack m_trail;
+ region m_region;
+ func_decl_ref_vector m_unhandled_functions;
+ trail_stack m_trail;
sat::solver* m_solver { nullptr };
sat::lookahead* m_lookahead { nullptr };
@@ -76,13 +79,13 @@ namespace euf {
sat::sat_internalizer* m_to_si;
scoped_ptr<euf::ackerman> m_ackerman;
- svector<euf::enode_bool_pair> m_var2node;
+ ptr_vector<euf::enode> m_lit2node;
ptr_vector<unsigned> m_explain;
euf::enode_vector m_args;
svector<sat::frame> m_stack;
unsigned m_num_scopes { 0 };
- unsigned_vector m_bool_var_trail;
- svector<scope> m_scopes;
+ unsigned_vector m_lit_trail;
+ svector<scope> m_scopes;
scoped_ptr_vector<sat::th_solver> m_solvers;
ptr_vector<sat::th_solver> m_id2solver;
@@ -96,7 +99,7 @@ namespace euf {
// internalization
euf::enode* visit(expr* e);
void attach_bool_var(euf::enode* n);
- void attach_bool_var(sat::bool_var v, bool sign, euf::enode* n);
+ void attach_lit(sat::literal lit, euf::enode* n);
euf::enode* mk_true();
euf::enode* mk_false();
@@ -118,7 +121,7 @@ namespace euf {
// solving
void propagate();
void get_antecedents(literal l, constraint& j, literal_vector& r);
- void force_push();
+ void force_push();
constraint& mk_constraint(constraint*& c, constraint::kind_t k);
constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
@@ -131,6 +134,7 @@ namespace euf {
m_expr2var(expr2var),
si(si),
m_egraph(m),
+ m_unhandled_functions(m),
m_solver(nullptr),
m_lookahead(nullptr),
m_to_m(&m),
@@ -197,6 +201,8 @@ namespace euf {
bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
sat::literal internalize(expr* e, bool sign, bool root) override;
void update_model(model_ref& mdl);
+
+ func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }
};
};
diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h
index 37e447ab4..2762d9664 100644
--- a/src/sat/smt/sat_smt.h
+++ b/src/sat/smt/sat_smt.h
@@ -88,7 +88,11 @@ namespace sat {
static void* ptr2mem(void* ptr) {
return reinterpret_cast<void*>(((unsigned char*) ptr) + ext_size());
- }
+ }
+
+ static void* idx2mem(size_t idx) {
+ return ptr2mem(from_index(idx));
+ }
};
}
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 26fdc3485..004919386 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -66,7 +66,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
bool m_ite_extra;
unsigned long long m_max_memory;
expr_ref_vector m_trail;
- func_decl_ref_vector m_interpreted_funs;
+ func_decl_ref_vector m_unhandled_funs;
bool m_default_external;
bool m_xor_solver;
bool m_euf;
@@ -80,7 +80,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_map(map),
m_dep2asm(dep2asm),
m_trail(m),
- m_interpreted_funs(m),
+ m_unhandled_funs(m),
m_default_external(default_external) {
updt_params(p);
m_true = sat::null_literal;
@@ -174,7 +174,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
return;
}
else
- m_interpreted_funs.push_back(to_app(t)->get_decl());
+ m_unhandled_funs.push_back(to_app(t)->get_decl());
}
}
}
@@ -398,8 +398,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
SASSERT(t->get_num_args() == 2);
unsigned sz = m_result_stack.size();
SASSERT(sz >= 2);
- sat::literal l1 = m_result_stack[sz - 1];
- sat::literal l2 = m_result_stack[sz - 2];
+ sat::literal l2 = m_result_stack[sz - 1];
+ sat::literal l1 = m_result_stack[sz - 2];
if (root) {
SASSERT(sz == 2);
if (sign) {
@@ -469,6 +469,13 @@ struct goal2sat::imp : public sat::sat_internalizer {
convert_iff2(t, root, sign);
}
+ func_decl_ref_vector const& interpreted_funs() {
+ auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
+ if (ext)
+ return ext->unhandled_functions();
+ return m_unhandled_funs;
+ }
+
void convert_euf(expr* e, bool root, bool sign) {
sat::extension* ext = m_solver.get_extension();
euf::solver* euf = nullptr;
@@ -693,6 +700,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
void operator()(goal const & g) {
+ g.display(std::cout);
struct scoped_reset {
imp& i;
scoped_reset(imp& i) :i(i) {}
@@ -741,6 +749,12 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
}
+ void update_model(model_ref& mdl) {
+ auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
+ if (ext)
+ ext->update_model(mdl);
+ }
+
};
struct unsupported_bool_proc {
@@ -792,7 +806,7 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core
(*m_imp)(g);
- if (!t.get_extension() && m_imp->m_interpreted_funs.empty()) {
+ if (!t.get_extension() && m_imp->interpreted_funs().empty()) {
dealloc(m_imp);
m_imp = nullptr;
}
@@ -801,12 +815,17 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core
void goal2sat::get_interpreted_funs(func_decl_ref_vector& atoms) {
if (m_imp) {
- atoms.append(m_imp->m_interpreted_funs);
+ atoms.append(m_imp->interpreted_funs());
}
}
bool goal2sat::has_interpreted_funs() const {
- return m_imp && !m_imp->m_interpreted_funs.empty();
+ return m_imp && !m_imp->interpreted_funs().empty();
+}
+
+void goal2sat::update_model(model_ref& mdl) {
+ if (m_imp)
+ m_imp->update_model(mdl);
}
diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h
index 1576b10a9..298e9dc36 100644
--- a/src/sat/tactic/goal2sat.h
+++ b/src/sat/tactic/goal2sat.h
@@ -61,12 +61,14 @@ public:
*/
void operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
- void get_interpreted_funs(func_decl_ref_vector& atoms);
+ void get_interpreted_funs(func_decl_ref_vector& funs);
bool has_interpreted_funs() const;
sat::sat_internalizer& si(ast_manager& m, params_ref const& p, sat::solver_core& t, atom2bool_var& a2b, dep2asm_map& dep2asm, bool default_external = false);
+ void update_model(model_ref& mdl);
+
};
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index 455df100e..8249bd865 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -50,11 +50,12 @@ class sat_tactic : public tactic {
obj_map<expr, sat::literal> dep2asm;
sat::literal_vector assumptions;
m_goal2sat(*g, m_params, *m_solver, map, dep2asm);
- TRACE("sat", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n";
- for (auto const& kv : map) {
- if (!is_uninterp_const(kv.m_key))
- tout << mk_ismt2_pp(kv.m_key, m) << "\n";
- });
+ TRACE("sat", tout << "interpreted_atoms: " << m_goal2sat.has_interpreted_funs() << "\n";
+ func_decl_ref_vector funs(m);
+ m_goal2sat.get_interpreted_funs(funs);
+ for (func_decl* f : funs)
+ tout << mk_ismt2_pp(f, m) << "\n";
+ );
g->reset();
g->m().compact_memory();
@@ -78,7 +79,7 @@ class sat_tactic : public tactic {
}
g->assert_expr(m.mk_false(), nullptr, lcore);
}
- else if (r == l_true && !map.interpreted_atoms()) {
+ else if (r == l_true && !m_goal2sat.has_interpreted_funs()) {
// register model
if (produce_models) {
model_ref md = alloc(model, m);
@@ -99,6 +100,7 @@ class sat_tactic : public tactic {
break;
}
}
+ m_goal2sat.update_model(md);
TRACE("sat_tactic", model_v2_pp(tout, *md););
g->add(model2model_converter(md.get()));
}