From aa66be9406069ee59e54dd04f4cc93ef985c7500 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 Sep 2020 07:16:59 -0700
Subject: [PATCH] na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/smt/CMakeLists.txt | 3 +-
src/sat/smt/bv_internalize.cpp | 240 +++++++++++++++++++++++++++-----
src/sat/smt/bv_solver.cpp | 56 ++++++++
src/sat/smt/bv_solver.h | 62 ++++++++-
src/sat/smt/euf_internalize.cpp | 65 ++++-----
src/sat/smt/euf_solver.cpp | 6 +-
src/sat/smt/euf_solver.h | 20 ++-
src/sat/smt/sat_th.cpp | 47 +++++++
src/sat/smt/sat_th.h | 16 +++
9 files changed, 428 insertions(+), 87 deletions(-)
create mode 100644 src/sat/smt/bv_solver.cpp
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<bool> _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<euf::enode> 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<bit_atom*>(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<literal_vector> m_bits; // per var, the bits of a given variable.
ptr_vector<expr> m_bits_expr;
@@ -96,11 +96,59 @@ namespace bv {
vector<zero_one_bits> m_zero_one_bits; // per var, see comment in the struct zero_one_bit
// bool_var2atom m_bool_var2atom;
sat::solver* m_solver;
- svector<sat::eframe> 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<euf::enode> 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<bool> _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<euf::enode> m_var2node;
ptr_vector<unsigned> m_explain;
- euf::enode_vector m_args;
- svector<sat::eframe> m_stack;
unsigned m_num_scopes { 0 };
unsigned_vector m_var_trail;
svector<scope> m_scopes;
@@ -99,8 +97,10 @@ namespace euf {
unsigned * base_ptr() { return reinterpret_cast<unsigned*>(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 <typename C>
+ 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<void(unsigned sz, literal const* c, unsigned k)>& card,
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override;
bool to_formulas(std::function<expr_ref(sat::literal)>& 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<bool> _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<sat::eframe> 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()); }