diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp index 96e18b8bb..b4c6ee3d6 100644 --- a/src/sat/smt/ba_solver.cpp +++ b/src/sat/smt/ba_solver.cpp @@ -1734,6 +1734,7 @@ namespace sat { : m_solver(nullptr), m_lookahead(nullptr), m_constraint_id(0), m_ba(*this), m_sort(m_ba) { TRACE("ba", tout << this << "\n";); + std::cout << "mk " << this << "\n"; m_num_propagations_since_pop = 0; } diff --git a/src/sat/smt/ba_solver.h b/src/sat/smt/ba_solver.h index 05373d594..50d4fda47 100644 --- a/src/sat/smt/ba_solver.h +++ b/src/sat/smt/ba_solver.h @@ -81,8 +81,17 @@ namespace sat { public: constraint(extension* e, tag_t t, unsigned id, literal l, unsigned sz, size_t osz): index_base(e), - m_tag(t), m_removed(false), m_lit(l), m_watch(null_literal), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id), m_pure(false) {} - ext_constraint_idx index() const { return reinterpret_cast(this); } + m_tag(t), m_removed(false), m_lit(l), m_watch(null_literal), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id), m_pure(false) { + std::cout << "constraint ext: " << t << " " << e << "\n"; + size_t idx = reinterpret_cast(this); + std::cout << "index " << idx << "\n"; + std::cout << this << " " << index_base::from_index(idx) << "\n"; + std::cout << e << " " << index_base::to_extension(idx) << "\n"; + std::cout.flush(); + } + ext_constraint_idx index() const { + return reinterpret_cast(this); + } unsigned id() const { return m_id; } tag_t tag() const { return m_tag; } literal lit() const { return m_lit; } diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 1136e8d45..c666e5728 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -64,6 +64,7 @@ namespace euf { m_internalizers.push_back(bai); m_decompilers.push_back(alloc(sat::ba_decompile, *ba, s(), m)); ba->push_scopes(s().num_scopes()); + std::cout << "extension ba " << ba << "\n"; return ba; } } @@ -72,6 +73,7 @@ namespace euf { bool solver::propagate(literal l, ext_constraint_idx idx) { auto* ext = sat::index_base::to_extension(idx); + std::cout << "extension " << ext << " " << idx << "\n"; SASSERT(ext != this); return ext->propagate(l, idx); } @@ -275,8 +277,12 @@ namespace euf { sat::extension* solver::copy(sat::solver* s) { auto* r = copy_core(); r->set_solver(s); - for (auto* e : m_extensions) - r->m_extensions.push_back(e->copy(s)); + for (unsigned i = 0; i < m_id2extension.size(); ++i) { + auto* e = m_id2extension[i]; + if (e) + r->add_extension(i, e->copy(s)); + } + return r; } @@ -284,8 +290,11 @@ namespace euf { (void) learned; auto* r = copy_core(); r->set_lookahead(s); - for (auto* e : m_extensions) - r->m_extensions.push_back(e->copy(s, learned)); + for (unsigned i = 0; i < m_id2extension.size(); ++i) { + auto* e = m_id2extension[i]; + if (e) + r->add_extension(i, e->copy(s, learned)); + } return r; } @@ -378,6 +387,7 @@ namespace euf { m_true = visit(m.mk_true()); m_false = visit(m.mk_false()); } + std::cout << mk_pp(e, m) << "\n"; SASSERT(!si.is_bool_op(e)); sat::scoped_stack _sc(m_stack); unsigned sz = m_stack.size(); @@ -417,6 +427,11 @@ 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; + if (n) + return n; + n = m_egraph.mk(e, 0, nullptr); attach_bool_var(lit.var(), lit.sign(), n); if (!m.is_true(e) && !m.is_false(e)) @@ -436,6 +451,7 @@ namespace euf { expr* e = n->get_owner(); if (m.is_bool(e)) { sat::bool_var v = si.add_bool_var(e); + std::cout << "attach " << v << "\n"; attach_bool_var(v, false, n); } } diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h index ef0080f2a..4c5bdd246 100644 --- a/src/sat/smt/sat_smt.h +++ b/src/sat/smt/sat_smt.h @@ -19,6 +19,7 @@ Author: #pragma once #include "ast/ast.h" +#include "ast/ast_pp.h" #include "sat/sat_solver.h" namespace sat { @@ -50,9 +51,9 @@ namespace sat { class index_base { extension* ex; public: - index_base(extension* e): ex(e) {} - static extension* to_extension(size_t s) { return from_index(s)->ex; } + index_base(extension* e) : ex(e) { to_index(); } + static extension* to_extension(size_t s) { std::cout << "to_extension: " << from_index(s) << " " << from_index(s)->ex << " " << s << "\n"; return from_index(s)->ex; } static index_base* from_index(size_t s) { return reinterpret_cast(s); } - size_t to_index() const { return reinterpret_cast(this); } + size_t to_index() const { std::cout << "to_index " << this << " " << ex << " " << reinterpret_cast(this) << "\n"; return reinterpret_cast(this); } }; } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 1497ee6b5..659e6aeca 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -60,5 +60,27 @@ namespace sat { virtual bool include_func_interp(func_decl* f) const { return false; } }; + class th_solver : public extension, public th_model_builder, public th_decompile, public th_internalizer { + + virtual ~th_solver() {} + + /** + \brief compute the value for enode \c n and store the value in \c values + for the root of the class of \c n. + */ + virtual void add_value(euf::enode* n, expr_ref_vector& values) = 0; + + /** + \brief compute dependencies for node n + */ + virtual void add_dep(euf::enode* n, top_sort& dep) = 0; + + /** + \brief should function be included in model. + */ + virtual bool include_func_interp(func_decl* f) const { return false; } + + }; + } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index fbe26d3f9..2d4bbbead 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -95,6 +95,7 @@ struct goal2sat::imp : public sat::sat_internalizer { m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_xor_solver = p.get_bool("xor_solver", false); m_euf = false; + m_euf = true; } void throw_op_not_handled(std::string const& s) { @@ -194,7 +195,7 @@ struct goal2sat::imp : public sat::sat_internalizer { } bool convert_app(app* t, bool root, bool sign) { - if (pb.is_pb(t)) { + if (!m_euf && pb.is_pb(t)) { m_frame_stack.push_back(frame(to_app(t), root, sign, 0)); return false; } @@ -432,7 +433,7 @@ struct goal2sat::imp : public sat::sat_internalizer { void convert_iff(app * t, bool root, bool sign) { TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_bounded_pp(t, m, 2) << "\n";); - if (is_xor(t)) + if (!m_euf && is_xor(t)) convert_ba(t, root, sign); else convert_iff2(t, root, sign); @@ -443,6 +444,7 @@ struct goal2sat::imp : public sat::sat_internalizer { euf::solver* euf = nullptr; if (!ext) { euf = alloc(euf::solver, m, m_map, *this); + std::cout << "set euf\n"; m_solver.set_extension(euf); for (unsigned i = m_solver.num_scopes(); i-- > 0; ) euf->push(); @@ -464,6 +466,8 @@ struct goal2sat::imp : public sat::sat_internalizer { } void convert_ba(app* t, bool root, bool sign) { + SASSERT(!m_euf); + std::cout << "convert ba\n"; sat::extension* ext = m_solver.get_extension(); sat::ba_solver* ba = nullptr; if (!ext) { @@ -510,7 +514,7 @@ struct goal2sat::imp : public sat::sat_internalizer { } SASSERT(!root || m_result_stack.empty()); } - else if (pb.is_pb(t)) { + else if (!m_euf && pb.is_pb(t)) { convert_ba(t, root, sign); } else { @@ -571,7 +575,7 @@ struct goal2sat::imp : public sat::sat_internalizer { visit(t->get_arg(0), root, !sign); continue; } - if (is_xor(t)) { + if (!m_euf && is_xor(t)) { convert_ba(t, root, sign); m_frame_stack.pop_back(); continue; @@ -618,7 +622,7 @@ struct goal2sat::imp : public sat::sat_internalizer { return false; } } - else if (to_app(t)->get_family_id() == pb.get_family_id()) + else if (!m_euf && to_app(t)->get_family_id() == pb.get_family_id()) return true; else return false;