From d83d0a83d6b12a1411f42cb3fbb560cbc638952b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Sep 2020 14:43:49 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_egraph.cpp | 2 +- src/sat/sat_drat.cpp | 32 +++---- src/sat/sat_drat.h | 5 +- src/sat/sat_types.h | 24 ++---- src/sat/smt/CMakeLists.txt | 1 + src/sat/smt/ba_solver.cpp | 24 +++--- src/sat/smt/bv_internalize.cpp | 75 ++++++++++++++++ src/sat/smt/bv_solver.h | 147 ++++++++++++++++++++++++++++++++ src/sat/smt/euf_ackerman.cpp | 4 +- src/sat/smt/euf_internalize.cpp | 10 +-- src/sat/smt/euf_proof.cpp | 2 +- src/sat/smt/euf_solver.cpp | 4 + src/sat/smt/euf_solver.h | 2 + src/sat/smt/sat_th.h | 1 - 14 files changed, 274 insertions(+), 59 deletions(-) create mode 100644 src/sat/smt/bv_internalize.cpp create mode 100644 src/sat/smt/bv_solver.h diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 6d22083dd0f..4f1e3d10979 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -245,7 +245,7 @@ namespace euf { std::swap(n1, n2); } if ((m.is_true(r2->get_owner()) || m.is_false(r2->get_owner())) && j.is_congruence()) { - m_new_lits.push_back(enode_pair(n1, false)); + m_new_lits.push_back(enode_bool_pair(n1, false)); ++m_stats.m_num_lits; } for (enode* p : enode_parents(n1)) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index f3557c14f4c..b1de72147aa 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -68,7 +68,7 @@ namespace sat { m_activity = s.get_config().m_drat_activity; } - std::ostream& operator<<(std::ostream& out, status st) { + std::ostream& drat::pp(std::ostream& out, status st) const { if (st.is_redundant()) out << "l"; else if (st.is_deleted()) @@ -76,10 +76,8 @@ namespace sat { else if (st.is_asserted()) out << "a"; - if (st.is_ba()) - out << " ba"; - else if (st.is_euf()) - out << " euf"; + if (!st.is_sat()) + out << " " << m_theory[st.get_th()]; return out; } @@ -103,15 +101,9 @@ namespace sat { buffer[len++] = ' '; } - if (st.is_euf()) { - buffer[len++] = 'e'; - buffer[len++] = 'u'; - buffer[len++] = 'f'; - buffer[len++] = ' '; - } - else if (st.is_ba()) { - buffer[len++] = 'b'; - buffer[len++] = 'a'; + if (!st.is_sat()) { + for (char ch : m_theory[st.get_th()]) + buffer[len++] = ch; buffer[len++] = ' '; } for (unsigned i = 0; i < n; ++i) { @@ -139,8 +131,6 @@ namespace sat { buffer[len++] = '\n'; m_out->write(buffer, len); - m_out->flush(); - } void drat::dump_activity() { @@ -192,7 +182,7 @@ namespace sat { } void drat::trace(std::ostream& out, unsigned n, literal const* c, status st) { - out << st << " "; + pp(out, st) << " "; literal last = null_literal; for (unsigned i = 0; i < n; ++i) { if (c[i] != last) { @@ -204,7 +194,7 @@ namespace sat { } void drat::append(literal l, status st) { - TRACE("sat_drat", tout << st << " " << l << "\n";); + TRACE("sat_drat", pp(tout, st) << " " << l << "\n";); declare(l); IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st);); @@ -222,7 +212,7 @@ namespace sat { } void drat::append(literal l1, literal l2, status st) { - TRACE("sat_drat", tout << st << " " << l1 << " " << l2 << "\n";); + TRACE("sat_drat", pp(tout, st) << " " << l1 << " " << l2 << "\n";); declare(l1); declare(l2); literal lits[2] = { l1, l2 }; @@ -305,7 +295,7 @@ namespace sat { #endif void drat::append(clause& c, status st) { - TRACE("sat_drat", tout << st << " " << c << "\n";); + TRACE("sat_drat", pp(tout, st) << " " << c << "\n";); for (literal lit : c) declare(lit); unsigned n = c.size(); IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st);); @@ -609,7 +599,7 @@ namespace sat { if (num_true == 0 && num_undef == 1) { out << "Unit "; } - out << m_status[i] << " " << i << ": " << *c << "\n"; + pp(out, m_status[i]) << " " << i << ": " << *c << "\n"; } } for (unsigned i = 0; i < m_assignment.size(); ++i) { diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h index 5ca47d010c3..f41d5b103d8 100644 --- a/src/sat/sat_drat.h +++ b/src/sat/sat_drat.h @@ -64,6 +64,7 @@ namespace sat { literal_vector m_units; vector m_watches; svector m_assignment; + svector m_theory; bool m_inconsistent; unsigned m_num_add, m_num_del; bool m_check_unsat, m_check_sat, m_check, m_activity; @@ -77,7 +78,7 @@ namespace sat { bool is_clause(clause& c, literal l1, literal l2, literal l3, status st1, status st2); - friend std::ostream& operator<<(std::ostream & out, status st); + std::ostream& pp(std::ostream & out, status st) const; status get_status(bool learned) const; void declare(literal l); @@ -99,6 +100,8 @@ namespace sat { ~drat(); void updt_config(); + + void add_theory(int id, symbol const& s) { m_theory.setx(id, s.str(), std::string()); } void add(); void add(literal l, bool learned); void add(literal l1, literal l2, status st); diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 18bc0e90b66..82d1c23aed4 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -255,30 +255,24 @@ namespace sat { class status { public: enum class st { asserted, redundant, deleted }; - enum class orig { sat, ba, euf }; + int m_orig; st m_st; - orig m_orig; public: - status(enum st s, enum orig o) : m_st(s), m_orig(o) {}; + status(enum st s, int o) : m_st(s), m_orig(o) {}; status(status const& s) : m_st(s.m_st), m_orig(s.m_orig) {} - status(status&& s) noexcept { m_st = st::asserted; m_orig = orig::sat; std::swap(m_st, s.m_st); std::swap(m_orig, s.m_orig); } - static status redundant() { return status(status::st::redundant, status::orig::sat); } - static status asserted() { return status(status::st::asserted, status::orig::sat); } - static status deleted() { return status(status::st::deleted, status::orig::sat); } + status(status&& s) noexcept { m_st = st::asserted; m_orig = -1; std::swap(m_st, s.m_st); std::swap(m_orig, s.m_orig); } + static status redundant() { return status(status::st::redundant, -1); } + static status asserted() { return status(status::st::asserted, -1); } + static status deleted() { return status(status::st::deleted, -1); } - static status euf(bool redundant) { return status(redundant ? st::redundant : st::asserted, orig::euf); } - - static status ba(bool redundant) { return redundant ? ba_redundant() : ba_asserted(); } - static status ba_redundant() { return status(status::st::redundant, status::orig::ba); } - static status ba_asserted() { return status(status::st::asserted, status::orig::ba); } + static status th(bool redundant, int id) { return status(redundant ? st::redundant : st::asserted, id); } bool is_redundant() const { return st::redundant == m_st; } bool is_asserted() const { return st::asserted == m_st; } bool is_deleted() const { return st::deleted == m_st; } - bool is_sat() const { return orig::sat == m_orig; } - bool is_ba() const { return orig::ba == m_orig; } - bool is_euf() const { return orig::euf == m_orig; } + bool is_sat() const { return -1 == m_orig; } + int get_th() const { return m_orig; } }; diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index e9468b4158a..00351e968be 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(sat_smt atom2bool_var.cpp ba_internalize.cpp ba_solver.cpp + bv_internalize.cpp xor_solver.cpp euf_ackerman.cpp euf_internalize.cpp diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp index 642a6fb882c..ec2e2554cf0 100644 --- a/src/sat/smt/ba_solver.cpp +++ b/src/sat/smt/ba_solver.cpp @@ -360,7 +360,7 @@ namespace sat { } if (p.k() == 1 && p.lit() == null_literal) { literal_vector lits(p.literals()); - s().mk_clause(lits.size(), lits.c_ptr(), status::ba(p.learned())); + s().mk_clause(lits.size(), lits.c_ptr(), status::th(p.learned(), get_id())); IF_VERBOSE(100, display(verbose_stream() << "add clause: " << lits << "\n", p, true);); remove_constraint(p, "implies clause"); } @@ -412,7 +412,7 @@ namespace sat { if (k == 1 && p.lit() == null_literal) { literal_vector lits(sz, p.literals().c_ptr()); - s().mk_clause(sz, lits.c_ptr(), status::ba(p.learned())); + s().mk_clause(sz, lits.c_ptr(), status::th(p.learned(), get_id())); remove_constraint(p, "is clause"); return; } @@ -795,7 +795,7 @@ namespace sat { else if (k == 1 && p.lit() == null_literal) { literal_vector lits(sz, p.literals().c_ptr()); - s().mk_clause(sz, lits.c_ptr(), status::ba(p.learned())); + s().mk_clause(sz, lits.c_ptr(), status::th(p.learned(), get_id())); remove_constraint(p, "recompiled to clause"); return; } @@ -1598,7 +1598,7 @@ namespace sat { TRACE("ba", tout << m_lemma << "\n";); if (get_config().m_drat && m_solver) { - s().m_drat.add(m_lemma, sat::status::ba(true)); + s().m_drat.add(m_lemma, sat::status::th(true, get_id())); } s().m_lemma.reset(); @@ -1750,7 +1750,7 @@ namespace sat { ba_solver::constraint* ba_solver::add_at_least(literal lit, literal_vector const& lits, unsigned k, bool learned) { if (k == 1 && lit == null_literal) { literal_vector _lits(lits); - s().mk_clause(_lits.size(), _lits.c_ptr(), status::ba(learned)); + s().mk_clause(_lits.size(), _lits.c_ptr(), status::th(learned, get_id())); return nullptr; } if (!learned && clausify(lit, lits.size(), lits.c_ptr(), k)) { @@ -2140,7 +2140,7 @@ namespace sat { for (literal lit : r) lits.push_back(~lit); lits.push_back(l); - s().m_drat.add(lits, sat::status::ba(true)); + s().m_drat.add(lits, sat::status::th(true, get_id())); } } @@ -2899,7 +2899,7 @@ namespace sat { if (k == 1 && c.lit() == null_literal) { literal_vector lits(sz, c.literals().c_ptr()); - s().mk_clause(sz, lits.c_ptr(), sat::status::ba(c.learned())); + s().mk_clause(sz, lits.c_ptr(), sat::status::th(c.learned(), get_id())); remove_constraint(c, "recompiled to clause"); return; } @@ -2907,27 +2907,27 @@ namespace sat { if (sz == 0) { if (c.lit() == null_literal) { if (k > 0) { - s().mk_clause(0, nullptr, status::ba_asserted()); + s().mk_clause(0, nullptr, status::th(false, get_id())); } } else if (k > 0) { literal lit = ~c.lit(); - s().mk_clause(1, &lit, status::ba(c.learned())); + s().mk_clause(1, &lit, status::th(c.learned(), get_id())); } else { literal lit = c.lit(); - s().mk_clause(1, &lit, status::ba(c.learned())); + s().mk_clause(1, &lit, status::th(c.learned(), get_id())); } remove_constraint(c, "recompiled to clause"); return; } if (all_units && sz < k) { if (c.lit() == null_literal) { - s().mk_clause(0, nullptr, status::ba(c.learned())); + s().mk_clause(0, nullptr, status::th(c.learned(), get_id())); } else { literal lit = ~c.lit(); - s().mk_clause(1, &lit, status::ba(c.learned())); + s().mk_clause(1, &lit, status::th(c.learned(), get_id())); } remove_constraint(c, "recompiled to clause"); return; diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp new file mode 100644 index 00000000000..50b52534b80 --- /dev/null +++ b/src/sat/smt/bv_internalize.cpp @@ -0,0 +1,75 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + bv_internalize.cpp + +Abstract: + + Internalize utilities for bit-vector solver plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-30 + +--*/ + +#include "sat/smt/bv_solver.h" +#include "sat/smt/euf_solver.h" +#include "sat/smt/sat_th.h" +#include "tactic/tactic_exception.h" + +namespace bv { + + euf::theory_var solver::mk_var(euf::enode* n) { + theory_var r = euf::th_euf_solver::mk_var(n); + m_find.mk_var(); + m_bits.push_back(sat::literal_vector()); + m_wpos.push_back(0); + m_zero_one_bits.push_back(zero_one_bits()); + ctx.attach_th_var(n, this, r); + return r; + } + + sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) { + flet _is_learned(m_is_redundant, learned); + sat::scoped_stack _sc(m_stack); + unsigned sz = m_stack.size(); + visit(e); + while (m_stack.size() > sz) { + loop: + if (!m.inc()) + throw tactic_exception(m.limit().get_cancel_msg()); + sat::eframe & fr = m_stack.back(); + expr* e = fr.m_e; + if (visited(e)) { + m_stack.pop_back(); + continue; + } + unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0; + + while (fr.m_idx < num) { + expr* arg = to_app(e)->get_arg(fr.m_idx); + fr.m_idx++; + visit(arg); + if (!visited(arg)) + goto loop; + } + visit(e); + SASSERT(visited(e)); + m_stack.pop_back(); + } + SASSERT(visited(e)); + return sat::null_literal; + } + + bool solver::visit(expr* e) { + return false; + } + + bool solver::visited(expr* e) { + return false; + } + +} diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h new file mode 100644 index 00000000000..f81467c57df --- /dev/null +++ b/src/sat/smt/bv_solver.h @@ -0,0 +1,147 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + bv_solver.h + +Abstract: + + Theory plugin for bit-vectors + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-30 + +--*/ +#pragma once + +#include "sat/smt/sat_th.h" + +namespace bv { + + class solver : public euf::th_euf_solver { + typedef rational numeral; + typedef euf::theory_var theory_var; + typedef euf::theory_id theory_id; + typedef sat::literal literal; + typedef sat::bool_var bool_var; + typedef sat::literal_vector literal_vector; + typedef svector vars; + typedef std::pair value_sort_pair; + typedef pair_hash, unsigned_hash> value_sort_pair_hash; + typedef map > value2var; + typedef union_find th_union_find; + + /** + \brief Structure used to store the position of a bitvector variable that + contains the true_literal/false_literal. + + Remark: the implementation assumes that bitvector variables containing + complementary bits are never merged. I assert a disequality (not (= x y)) + whenever x and y contain complementary bits. However, this is too expensive + when the bit is the true_literal or false_literal. The number of disequalities + is too big. To avoid this problem, each equivalence class has a set + of its true_literal and false_literal bits in the form of svector. + + Before merging two classes we just check if the merge is valid by traversing these + vectors. + */ + struct zero_one_bit { + theory_var m_owner; //!< variable that owns the bit: useful for backtracking + unsigned m_idx:31; + unsigned m_is_true:1; + zero_one_bit(theory_var v = euf::null_theory_var, unsigned idx = UINT_MAX, bool is_true = false): + m_owner(v), m_idx(idx), m_is_true(is_true) {} + }; + + typedef svector zero_one_bits; + + class atom { + public: + virtual ~atom() {} + virtual bool is_bit() const = 0; + }; + + struct var_pos_occ { + theory_var m_var; + unsigned m_idx; + var_pos_occ * m_next; + var_pos_occ(theory_var v = euf::null_theory_var, unsigned idx = 0, var_pos_occ * next = nullptr):m_var(v), m_idx(idx), m_next(next) {} + }; + + struct bit_atom : public atom { + var_pos_occ * m_occs; + bit_atom():m_occs(nullptr) {} + ~bit_atom() override {} + bool is_bit() const override { return true; } + }; + + struct le_atom : public atom { + literal m_var; + literal m_def; + le_atom(literal v, literal d):m_var(v), m_def(d) {} + ~le_atom() override {} + bool is_bit() const override { return false; } + }; + + euf::solver& ctx; + bv_util m_util; + arith_util m_autil; +// bit_blaster m_bb; + th_union_find m_find; + vector m_bits; // per var, the bits of a given variable. + ptr_vector m_bits_expr; + svector m_wpos; // per var, watch position for fixed variable detection. + vector m_zero_one_bits; // per var, see comment in the struct zero_one_bit +// bool_var2atom m_bool_var2atom; + sat::solver* m_solver; + svector m_stack; + bool m_is_redundant{ false }; + + bool visit(expr* e); + bool visited(expr* e); + public: + solver(euf::solver& ctx); + ~solver() override {} + void set_solver(sat::solver* s) override { m_solver = s; } + void set_lookahead(sat::lookahead* s) override { } + void init_search() override {} + double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override; + bool is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) override; + bool is_external(bool_var v) override; + bool propagate(literal l, sat::ext_constraint_idx idx) override; + void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r) override; + void asserted(literal l) override; + sat::check_result check() override; + void push() override; + void pop(unsigned n) override; + void pre_simplify() override; + void simplify() override; + void clauses_modifed() override; + lbool get_phase(bool_var v) override; + std::ostream& display(std::ostream& out) const override; + std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override; + std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override; + void collect_statistics(statistics& st) const override; + extension* copy(sat::solver* s) override; + void find_mutexes(literal_vector& lits, vector & mutexes) override {} + void gc() override {} + void pop_reinit() override; + bool validate() override; + void init_use_list(sat::ext_use_list& ul) override; + bool is_blocked(literal l, sat::ext_constraint_idx) override; + bool check_model(sat::model const& m) const override; + unsigned max_var(unsigned w) const override; + + bool extract_pb(std::function& card, + std::function& pb) override { return false; } + + bool to_formulas(std::function& l2e, expr_ref_vector& fmls) override { return false; } + sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; + euf::theory_var mk_var(euf::enode* n) override; + + }; + + +} diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp index ba85fb8c375..77d5866554d 100644 --- a/src/sat/smt/euf_ackerman.cpp +++ b/src/sat/smt/euf_ackerman.cpp @@ -194,7 +194,7 @@ namespace euf { } expr_ref eq(m.mk_eq(a, b), m); lits.push_back(s.internalize(eq, false, false, true)); - s.s().mk_clause(lits, sat::status::euf(true)); + s.s().mk_clause(lits, sat::status::th(true, m.get_basic_family_id())); } void ackerman::add_eq(expr* a, expr* b, expr* c) { @@ -205,6 +205,6 @@ namespace euf { lits[0] = s.internalize(eq1, true, false, true); lits[1] = s.internalize(eq2, true, false, true); lits[2] = s.internalize(eq3, false, false, true); - s.s().mk_clause(3, lits, sat::status::euf(true)); + s.s().mk_clause(3, lits, sat::status::th(true, m.get_basic_family_id())); } } diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 8514d87eea1..355d3987220 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -103,8 +103,8 @@ namespace euf { if (lit.sign()) { sat::bool_var v = si.add_bool_var(n->get_owner()); sat::literal lit2 = literal(v, false); - s().mk_clause(~lit, lit2, sat::status::euf(false)); - s().mk_clause(lit, ~lit2, sat::status::euf(false)); + s().mk_clause(~lit, lit2, sat::status::th(false, m.get_basic_family_id())); + s().mk_clause(lit, ~lit2, sat::status::th(false, m.get_basic_family_id())); lit = lit2; } sat::bool_var v = lit.var(); @@ -132,7 +132,7 @@ namespace euf { if (sz <= 1) return; - sat::status st = sat::status::euf(m_is_redundant); + sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id()); static const unsigned distinct_max_args = 32; if (sz <= distinct_max_args) { sat::literal_vector lits; @@ -175,7 +175,7 @@ namespace euf { SASSERT(m.is_distinct(e)); static const unsigned distinct_max_args = 32; unsigned sz = e->get_num_args(); - sat::status st = sat::status::euf(m_is_redundant); + sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id()); if (sz <= 1) { s().mk_clause(0, nullptr, st); return; @@ -209,7 +209,7 @@ namespace euf { void solver::axiomatize_basic(enode* n) { expr* e = n->get_owner(); - sat::status st = sat::status::euf(m_is_redundant); + sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id()); if (m.is_ite(e)) { app* a = to_app(e); expr* c = a->get_arg(0); diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 9e983eb55f8..930da2c3625 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -49,7 +49,7 @@ namespace euf { for (literal lit : r) lits.push_back(~lit); if (l != sat::null_literal) lits.push_back(l); - s().get_drat().add(lits, sat::status::euf(true)); + s().get_drat().add(lits, sat::status::th(true, m.get_basic_family_id())); } } diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 8b0003ece88..46a504d2f8f 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -27,6 +27,8 @@ namespace euf { void solver::updt_params(params_ref const& p) { m_config.updt_params(p); m_drat = m_solver && m_solver->get_config().m_drat; + if (m_drat) + m_solver->get_drat().add_theory(m.get_basic_family_id(), symbol("euf")); } /** @@ -59,6 +61,8 @@ namespace euf { pb_util pb(m); if (pb.get_family_id() == fid) { ext = alloc(sat::ba_solver, *this, fid); + if (m_drat) + m_solver->get_drat().add_theory(fid, symbol("ba")); } if (ext) { ext->set_solver(m_solver); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 7dfb70e270d..e125d230583 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -219,6 +219,8 @@ namespace euf { bool to_formulas(std::function& l2e, expr_ref_vector& fmls) override; sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; + void attach_th_var(enode* n, th_solver* th, theory_var v) { m_egraph.add_th_var(n, v, th->get_id()); } + void update_model(model_ref& mdl); func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 03617bc6384..4db1b873fd0 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -84,7 +84,6 @@ namespace euf { */ virtual bool is_shared(theory_var v) const { return false; } - }; class th_euf_solver : public th_solver {