diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 00351e968..145c1a3fc 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -4,13 +4,14 @@ z3_add_component(sat_smt ba_internalize.cpp ba_solver.cpp bv_internalize.cpp - xor_solver.cpp + bv_solver.cpp euf_ackerman.cpp euf_internalize.cpp euf_model.cpp euf_proof.cpp euf_solver.cpp sat_th.cpp + xor_solver.cpp COMPONENT_DEPENDENCIES sat ast diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 50b52534b..b290f7b16 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -23,53 +23,227 @@ Author: namespace bv { euf::theory_var solver::mk_var(euf::enode* n) { - theory_var r = euf::th_euf_solver::mk_var(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()); + 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)); + sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { + if (!visit_rec(m, e, sign, root, redundant)) + return sat::null_literal; return sat::null_literal; } bool solver::visit(expr* e) { - return false; + if (!bv.is_bv(e)) { + ctx.internalize(e, false, false, m_is_redundant); + return true; + } + m_args.reset(); + app* a = to_app(e); + for (expr* arg : *a) { + euf::enode* n = get_enode(arg); + if (n) + m_args.push_back(n); + else + m_stack.push_back(sat::eframe(arg)); + } + if (m_args.size() != a->get_num_args()) + return false; + if (!smt_params().m_bv_reflect) + m_args.reset(); + euf::enode* n = mk_enode(a, m_args); + SASSERT(n->interpreted()); + theory_var v = n->get_th_var(get_id()); + + switch (a->get_decl_kind()) { + case OP_BV_NUM: internalize_num(a, v); break; + default: break; + } + return true; } bool solver::visited(expr* e) { - return false; + return get_enode(e) != nullptr; + } + + euf::enode * solver::mk_enode(app * n, ptr_vector const& args) { + euf::enode * e = ctx.get_enode(n); + if (!e) { + e = ctx.mk_enode(n, args.size(), args.c_ptr()); + mk_var(e); + } + return e; + } + + void solver::register_true_false_bit(theory_var v, unsigned i) { + + } + + /** + \brief Add bit l to the given variable. + */ + void solver::add_bit(theory_var v, literal l) { + literal_vector & bits = m_bits[v]; + unsigned idx = bits.size(); + bits.push_back(l); +#if 0 + if (l.var() == true_bool_var) { + register_true_false_bit(v, idx); + } + else { + theory_id th_id = ctx.get_var_theory(l.var()); + if (th_id == get_id()) { + atom * a = get_bv2a(l.var()); + SASSERT(a && a->is_bit()); + bit_atom * b = static_cast(a); + find_new_diseq_axioms(b->m_occs, v, idx); + ctx.push(add_var_pos_trail(b)); + b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs); + } + else { + SASSERT(th_id == null_theory_id); + ctx.set_var_theory(l.var(), get_id()); + SASSERT(ctx.get_var_theory(l.var()) == get_id()); + bit_atom * b = new (get_region()) bit_atom(); + insert_bv2a(l.var(), b); + ctx.push(mk_atom_trail(l.var())); + SASSERT(b->m_occs == 0); + b->m_occs = new (get_region()) var_pos_occ(v, idx); + } + } +#endif + } + + void solver::init_bits(euf::enode * n, expr_ref_vector const & bits) { + SASSERT(get_bv_size(n) == bits.size()); + SASSERT(euf::null_theory_var != n->get_th_var(get_id())); + theory_var v = n->get_th_var(get_id()); + unsigned sz = bits.size(); + m_bits[v].reset(); + for (expr* bit : bits) + add_bit(v, get_literal(bit)); + find_wpos(v); + } + + unsigned solver::get_bv_size(euf::enode* n) { + return bv.get_bv_size(n->get_owner()); + } + + void solver::internalize_num(app* n, theory_var v) { + numeral val; + unsigned sz = 0; + VERIFY(bv.is_numeral(n, val, sz)); + expr_ref_vector bits(m); + m_bb.num2bits(val, sz, bits); + literal_vector & c_bits = m_bits[v]; + SASSERT(bits.size() == sz); + SASSERT(c_bits.empty()); + for (unsigned i = 0; i < sz; i++) { + expr * l = bits.get(i); + SASSERT(m.is_true(l) || m.is_false(l)); + c_bits.push_back(m.is_true(l) ? true_literal : false_literal); + register_true_false_bit(v, i); + } + fixed_var_eh(v); + } + + void solver::internalize_add(app* n) {} + void solver::internalize_sub(app* n) {} + void solver::internalize_mul(app* n) {} + void solver::internalize_udiv(app* n) {} + void solver::internalize_sdiv(app* n) {} + void solver::internalize_urem(app* n) {} + void solver::internalize_srem(app* n) {} + void solver::internalize_smod(app* n) {} + void solver::internalize_shl(app* n) {} + void solver::internalize_lshr(app* n) {} + void solver::internalize_ashr(app* n) {} + void solver::internalize_ext_rotate_left(app* n) {} + void solver::internalize_ext_rotate_right(app* n) {} + void solver::internalize_and(app* n) {} + void solver::internalize_or(app* n) {} + void solver::internalize_not(app* n) {} + void solver::internalize_nand(app* n) {} + void solver::internalize_nor(app* n) {} + void solver::internalize_xor(app* n) {} + void solver::internalize_xnor(app* n) {} + void solver::internalize_concat(app* n) {} + void solver::internalize_sign_extend(app* n) {} + void solver::internalize_zero_extend(app* n) {} + void solver::internalize_extract(app* n) {} + void solver::internalize_redand(app* n) {} + void solver::internalize_redor(app* n) {} + void solver::internalize_comp(app* n) {} + void solver::internalize_rotate_left(app* n) {} + void solver::internalize_rotate_right(app* n) {} + void solver::internalize_bv2int(app* n) {} + void solver::internalize_int2bv(app* n) {} + void solver::internalize_mkbv(app* n) {} + void solver::internalize_umul_no_overflow(app* n) {} + void solver::internalize_smul_no_overflow(app* n) {} + void solver::internalize_smul_no_underflow(app* n) {} + +} + + + +#if 0 + + case OP_BADD: internalize_add(term); return true; + case OP_BSUB: internalize_sub(term); return true; + case OP_BMUL: internalize_mul(term); return true; + case OP_BSDIV_I: internalize_sdiv(term); return true; + case OP_BUDIV_I: internalize_udiv(term); return true; + case OP_BSREM_I: internalize_srem(term); return true; + case OP_BUREM_I: internalize_urem(term); return true; + case OP_BSMOD_I: internalize_smod(term); return true; + case OP_BAND: internalize_and(term); return true; + case OP_BOR: internalize_or(term); return true; + case OP_BNOT: internalize_not(term); return true; + case OP_BXOR: internalize_xor(term); return true; + case OP_BNAND: internalize_nand(term); return true; + case OP_BNOR: internalize_nor(term); return true; + case OP_BXNOR: internalize_xnor(term); return true; + case OP_CONCAT: internalize_concat(term); return true; + case OP_SIGN_EXT: internalize_sign_extend(term); return true; + case OP_ZERO_EXT: internalize_zero_extend(term); return true; + case OP_EXTRACT: internalize_extract(term); return true; + case OP_BREDOR: internalize_redor(term); return true; + case OP_BREDAND: internalize_redand(term); return true; + case OP_BCOMP: internalize_comp(term); return true; + case OP_BSHL: internalize_shl(term); return true; + case OP_BLSHR: internalize_lshr(term); return true; + case OP_BASHR: internalize_ashr(term); return true; + case OP_ROTATE_LEFT: internalize_rotate_left(term); return true; + case OP_ROTATE_RIGHT: internalize_rotate_right(term); return true; + case OP_EXT_ROTATE_LEFT: internalize_ext_rotate_left(term); return true; + case OP_EXT_ROTATE_RIGHT: internalize_ext_rotate_right(term); return true; + case OP_BSDIV0: return false; + case OP_BUDIV0: return false; + case OP_BSREM0: return false; + case OP_BUREM0: return false; + case OP_BSMOD0: return false; + case OP_MKBV: internalize_mkbv(term); return true; + case OP_INT2BV: + if (params().m_bv_enable_int2bv2int) { + internalize_int2bv(term); + } + return params().m_bv_enable_int2bv2int; + case OP_BV2INT: + if (params().m_bv_enable_int2bv2int) { + internalize_bv2int(term); + } + return params().m_bv_enable_int2bv2int; + default: + TRACE("bv_op", tout << "unsupported operator: " << mk_ll_pp(term, m) << "\n";); + UNREACHABLE(); + return false; } } +#endif diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp new file mode 100644 index 000000000..b67fc90b8 --- /dev/null +++ b/src/sat/smt/bv_solver.cpp @@ -0,0 +1,56 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + bv_internalize.cpp + +Abstract: + + Internalize utilities for bit-vector solver plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2020-09-02 + +--*/ + +#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 { + + void solver::fixed_var_eh(theory_var v) { + + } + + /** + \brief Find an unassigned bit for m_wpos[v], if such bit cannot be found invoke fixed_var_eh + */ + void solver::find_wpos(theory_var v) { + literal_vector const & bits = m_bits[v]; + unsigned sz = bits.size(); + unsigned & wpos = m_wpos[v]; + unsigned init = wpos; + for (; wpos < sz; wpos++) { + TRACE("find_wpos", tout << "curr bit: " << bits[wpos] << "\n";); + if (s().value(bits[wpos]) == l_undef) { + TRACE("find_wpos", tout << "moved wpos of v" << v << " to " << wpos << "\n";); + return; + } + } + wpos = 0; + for (; wpos < init; wpos++) { + if (s().value(bits[wpos]) == l_undef) { + TRACE("find_wpos", tout << "moved wpos of v" << v << " to " << wpos << "\n";); + return; + } + } + TRACE("find_wpos", tout << "v" << v << " is a fixed variable.\n";); + fixed_var_eh(v); + } + + +} diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index f81467c57..393f3d40f 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -17,6 +17,7 @@ Author: #pragma once #include "sat/smt/sat_th.h" +#include "ast/rewriter/bit_blaster/bit_blaster.h" namespace bv { @@ -85,10 +86,9 @@ namespace bv { bool is_bit() const override { return false; } }; - euf::solver& ctx; - bv_util m_util; + bv_util bv; arith_util m_autil; -// bit_blaster m_bb; + 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; @@ -96,11 +96,59 @@ namespace bv { 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 }; + sat::solver& s() { return *m_solver; } + + // internalize: + sat::literal false_literal; + sat::literal true_literal; + bool visit(expr* e) override; + bool visited(expr* e) override; + bool post_visit(expr* e, bool sign, bool root) override; + unsigned get_bv_size(euf::enode* n); + euf::enode* mk_enode(app* n, ptr_vector const& args); + void fixed_var_eh(theory_var v); + void register_true_false_bit(theory_var v, unsigned i); + void add_bit(theory_var v, sat::literal lit); + void init_bits(euf::enode * n, expr_ref_vector const & bits); + void internalize_num(app * n, theory_var v); + void internalize_add(app * n); + void internalize_sub(app * n); + void internalize_mul(app * n); + void internalize_udiv(app * n); + void internalize_sdiv(app * n); + void internalize_urem(app * n); + void internalize_srem(app * n); + void internalize_smod(app * n); + void internalize_shl(app * n); + void internalize_lshr(app * n); + void internalize_ashr(app * n); + void internalize_ext_rotate_left(app * n); + void internalize_ext_rotate_right(app * n); + void internalize_and(app * n); + void internalize_or(app * n); + void internalize_not(app * n); + void internalize_nand(app * n); + void internalize_nor(app * n); + void internalize_xor(app * n); + void internalize_xnor(app * n); + void internalize_concat(app * n); + void internalize_sign_extend(app * n); + void internalize_zero_extend(app * n); + void internalize_extract(app * n); + void internalize_redand(app * n); + void internalize_redor(app * n); + void internalize_comp(app * n); + void internalize_rotate_left(app * n); + void internalize_rotate_right(app * n); + void internalize_bv2int(app* n); + void internalize_int2bv(app* n); + void internalize_mkbv(app* n); + void internalize_umul_no_overflow(app *n); + void internalize_smul_no_overflow(app *n); + void internalize_smul_no_underflow(app *n); + + void find_wpos(theory_var v); - bool visit(expr* e); - bool visited(expr* e); public: solver(euf::solver& ctx); ~solver() override {} diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 355d39872..30d8abc9a 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -17,56 +17,27 @@ Author: #include "ast/ast_pp.h" #include "ast/pb_decl_plugin.h" -#include "tactic/tactic_exception.h" #include "sat/smt/euf_solver.h" namespace euf { sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { - flet _is_learned(m_is_redundant, redundant); + if (si.is_bool_op(e)) + return si.internalize(e, redundant); auto* ext = get_solver(e); if (ext) return ext->internalize(e, sign, root, redundant); - IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(e, m) << "\n"); - SASSERT(!si.is_bool_op(e)); - sat::scoped_stack _sc(m_stack); - unsigned sz = m_stack.size(); - euf::enode* n = 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 (m_egraph.find(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++; - n = visit(arg); - if (!n) - goto loop; - } - m_args.reset(); - for (unsigned i = 0; i < num; ++i) - m_args.push_back(m_egraph.find(to_app(e)->get_arg(i))); - if (root && internalize_root(to_app(e), sign)) - return sat::null_literal; - n = m_egraph.mk(e, num, m_args.c_ptr()); - attach_node(n); - } + + if (!visit_rec(m, e, sign, root, redundant)) + return sat::null_literal; SASSERT(m_egraph.find(e)); return literal(m_expr2var.to_bool_var(e), sign); } - euf::enode* solver::visit(expr* e) { + bool solver::visit(expr* e) { euf::enode* n = m_egraph.find(e); if (n) - return n; + return true; if (si.is_bool_op(e)) { sat::literal lit = si.internalize(e, m_is_redundant); n = m_var2node.get(lit.var(), nullptr); @@ -77,15 +48,31 @@ namespace euf { attach_lit(lit, n); if (!m.is_true(e) && !m.is_false(e)) s().set_external(lit.var()); - return n; + return true; } if (is_app(e) && to_app(e)->get_num_args() > 0) { m_stack.push_back(sat::eframe(e)); - return nullptr; + return false; } n = m_egraph.mk(e, 0, nullptr); attach_node(n); - return n; + return true; + } + + bool solver::post_visit(expr* e, bool sign, bool root) { + unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0; + m_args.reset(); + for (unsigned i = 0; i < num; ++i) + m_args.push_back(m_egraph.find(to_app(e)->get_arg(i))); + if (root && internalize_root(to_app(e), sign)) + return false; + enode* n = m_egraph.mk(e, num, m_args.c_ptr()); + attach_node(n); + return true; + } + + bool solver::visited(expr* e) { + return m_egraph.find(e) != nullptr; } void solver::attach_node(euf::enode* n) { diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 46a504d2f..4dfe1f152 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -236,11 +236,13 @@ namespace euf { } enode* solver::mk_true() { - return visit(m.mk_true()); + VERIFY(visit(m.mk_true())); + return m_egraph.find(m.mk_true()); } enode* solver::mk_false() { - return visit(m.mk_false()); + VERIFY(visit(m.mk_false())); + return m_egraph.find(m.mk_false()); } sat::check_result solver::check() { diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index e125d2305..d7ed6f81d 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -20,12 +20,12 @@ Author: #include "util/trail.h" #include "ast/ast_translation.h" #include "ast/euf/euf_egraph.h" -#include "smt/params/smt_params.h" #include "tactic/model_converter.h" #include "sat/sat_extension.h" #include "sat/smt/atom2bool_var.h" #include "sat/smt/sat_th.h" #include "sat/smt/euf_ackerman.h" +#include "smt/params/smt_params.h" namespace euf { typedef sat::literal literal; @@ -83,8 +83,6 @@ namespace euf { ptr_vector m_var2node; ptr_vector m_explain; - euf::enode_vector m_args; - svector m_stack; unsigned m_num_scopes { 0 }; unsigned_vector m_var_trail; svector m_scopes; @@ -99,8 +97,10 @@ namespace euf { unsigned * base_ptr() { return reinterpret_cast(this); } // internalization - bool m_is_redundant { false }; - euf::enode* visit(expr* e); + + bool visit(expr* e) override; + bool visited(expr* e) override; + bool post_visit(expr* e, bool sign, bool root) override; void attach_node(euf::enode* n); void attach_lit(sat::literal lit, euf::enode* n); void add_distinct_axiom(app* e, euf::enode* const* args); @@ -109,6 +109,7 @@ namespace euf { bool internalize_root(app* e, bool sign); euf::enode* mk_true(); euf::enode* mk_false(); + // extensions th_solver* get_solver(func_decl* f); @@ -181,6 +182,11 @@ namespace euf { sat::sat_internalizer& get_si() { return si; } ast_manager& get_manager() { return m; } enode* get_enode(expr* e) { return m_egraph.find(e); } + sat::literal get_literal(expr* e) { return literal(m_expr2var.to_bool_var(e), false); } + smt_params const& get_config() { return m_config; } + region& get_region() { return m_region; } + template + void push(C const& c) { m_trail.push_back(new (m_region) C(c)); } void updt_params(params_ref const& p); void set_solver(sat::solver* s) override { m_solver = s; m_drat = s->get_config().m_drat; } @@ -214,12 +220,16 @@ namespace euf { bool check_model(sat::model const& m) const override; unsigned max_var(unsigned w) const override; + // decompile bool extract_pb(std::function& card, std::function& pb) override; bool to_formulas(std::function& l2e, expr_ref_vector& fmls) override; + + // internalize 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()); } + euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, n, args); } void update_model(model_ref& mdl); diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 4add216ce..435d330f5 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -17,15 +17,62 @@ Author: #include "sat/smt/sat_th.h" #include "sat/smt/euf_solver.h" +#include "tactic/tactic_exception.h" namespace euf { + bool th_internalizer::visit_rec(ast_manager& m, expr* a, bool sign, bool root, bool redundant) { + IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(a, m) << "\n"); + flet _is_learned(m_is_redundant, redundant); + sat::scoped_stack _sc(m_stack); + unsigned sz = m_stack.size(); + visit(a); + 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++; + if (!visit(arg)) + goto loop; + } + if (!post_visit(e, sign, root && a == e)) + return false; + m_stack.pop_back(); + } + return true; + } th_euf_solver::th_euf_solver(euf::solver& ctx, euf::theory_id id): th_solver(ctx.get_manager(), id), ctx(ctx) {} + smt_params const& th_euf_solver::get_config() const { + return ctx.get_config(); + } + + region& th_euf_solver::get_region() { + return ctx.get_region(); + } + + enode* th_euf_solver::get_enode(expr* e) const { + return ctx.get_enode(e); + } + + sat::literal th_euf_solver::get_literal(expr* e) const { + return ctx.get_literal(e); + } + theory_var th_euf_solver::mk_var(enode * n) { SASSERT(!is_attached_to_var(n)); euf::theory_var v = m_var2enode.size(); diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 4db1b873f..7770009c5 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -19,12 +19,23 @@ Author: #include "util/top_sort.h" #include "sat/smt/sat_smt.h" #include "ast/euf/euf_egraph.h" +#include "smt/params/smt_params.h" namespace euf { class solver; class th_internalizer { + protected: + euf::enode_vector m_args; + svector m_stack; + bool m_is_redundant { false }; + + bool visit_rec(ast_manager& m, expr* e, bool sign, bool root, bool redundant); + + virtual bool visit(expr* e) { return false; } + virtual bool visited(expr* e) { return false; } + virtual bool post_visit(expr* e, bool sign, bool root) { return false; } public: virtual ~th_internalizer() {} @@ -91,11 +102,16 @@ namespace euf { solver & ctx; euf::enode_vector m_var2enode; unsigned_vector m_var2enode_lim; + + smt_params const& get_config() const; + sat::literal get_literal(expr* e) const; + region& get_region(); public: th_euf_solver(euf::solver& ctx, euf::theory_id id); virtual ~th_euf_solver() {} virtual theory_var mk_var(enode * n); unsigned get_num_vars() const { return m_var2enode.size();} + enode* get_enode(expr* e) const; enode* get_enode(theory_var v) const { return m_var2enode[v]; } expr* get_expr(theory_var v) const { return get_enode(v)->get_owner(); } theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }