From 4244ce4aade3b4b5e1e8bd477ac364baed86bafb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 28 Aug 2020 12:55:31 -0700
Subject: [PATCH] adding ack/model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_project.py | 6 +-
src/CMakeLists.txt | 2 -
src/ast/euf/euf_egraph.cpp | 45 ++-
src/ast/euf/euf_egraph.h | 9 +-
src/ast/euf/euf_enode.h | 18 +
src/sat/ba/CMakeLists.txt | 8 -
src/sat/euf/CMakeLists.txt | 9 -
src/sat/euf/euf_model.cpp | 72 ----
src/sat/sat_extension.h | 2 +-
src/sat/sat_solver.h | 2 +
src/sat/sat_solver/inc_sat_solver.cpp | 8 +-
src/sat/smt/CMakeLists.txt | 7 +-
src/sat/{ba => smt}/ba_internalize.cpp | 90 ++++-
src/sat/{ba => smt}/ba_internalize.h | 30 +-
src/sat/{ba => smt}/ba_solver.cpp | 533 +------------------------
src/sat/{ba => smt}/ba_solver.h | 0
src/sat/smt/euf_ackerman.cpp | 211 ++++++++++
src/sat/smt/euf_ackerman.h | 89 +++++
src/sat/smt/euf_model.cpp | 138 +++++++
src/sat/{euf => smt}/euf_solver.cpp | 92 +++--
src/sat/{euf => smt}/euf_solver.h | 121 +++---
src/sat/smt/sat_th.cpp | 37 --
src/sat/smt/sat_th.h | 38 +-
src/sat/tactic/CMakeLists.txt | 2 -
src/sat/tactic/goal2sat.cpp | 135 ++-----
src/sat/tactic/goal2sat.h | 7 +-
src/shell/dimacs_frontend.cpp | 1 -
src/smt/params/CMakeLists.txt | 2 -
src/smt/params/smt_params.h | 1 -
src/smt/qi_queue.h | 2 +-
src/util/top_sort.h | 28 +-
31 files changed, 831 insertions(+), 914 deletions(-)
delete mode 100644 src/sat/ba/CMakeLists.txt
delete mode 100644 src/sat/euf/CMakeLists.txt
delete mode 100644 src/sat/euf/euf_model.cpp
rename src/sat/{ba => smt}/ba_internalize.cpp (76%)
rename src/sat/{ba => smt}/ba_internalize.h (58%)
rename src/sat/{ba => smt}/ba_solver.cpp (89%)
rename src/sat/{ba => smt}/ba_solver.h (100%)
create mode 100644 src/sat/smt/euf_ackerman.cpp
create mode 100644 src/sat/smt/euf_ackerman.h
create mode 100644 src/sat/smt/euf_model.cpp
rename src/sat/{euf => smt}/euf_solver.cpp (83%)
rename src/sat/{euf => smt}/euf_solver.h (55%)
delete mode 100644 src/sat/smt/sat_th.cpp
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 07fa172f6..dd2b190d4 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -39,9 +39,7 @@ def init_project_def():
add_lib('solver', ['model', 'tactic', 'proofs'])
add_lib('cmd_context', ['solver', 'rewriter'])
add_lib('sat_smt', ['sat', 'euf', 'tactic'], 'sat/smt')
- add_lib('sat_ba', ['sat', 'sat_smt'], 'sat/ba')
- add_lib('sat_euf', ['sat', 'euf', 'sat_ba'], 'sat/euf')
- add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_euf'], 'sat/tactic')
+ add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic')
add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
@@ -83,7 +81,7 @@ def init_project_def():
includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'arith_tactics'], 'cmd_context/extra_cmds')
add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')
- add_exe('test', ['api', 'fuzzing', 'simplex', 'sat_euf'], exe_name='test-z3', install=False)
+ add_exe('test', ['api', 'fuzzing', 'simplex', 'sat_smt'], exe_name='test-z3', install=False)
_libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
reexports=['api'],
dll_name='libz3',
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index df9d6acaf..0274f28a6 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -60,8 +60,6 @@ add_subdirectory(math/subpaving/tactic)
add_subdirectory(tactic/aig)
add_subdirectory(solver)
add_subdirectory(sat/smt)
-add_subdirectory(sat/ba)
-add_subdirectory(sat/euf)
add_subdirectory(sat/tactic)
add_subdirectory(tactic/arith)
add_subdirectory(nlsat/tactic)
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 5f073a877..1bb193e86 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -255,7 +255,10 @@ namespace euf {
explanations up to the least common ancestors.
*/
void egraph::push_congruence(enode* n1, enode* n2, bool comm) {
+ SASSERT(is_app(n1->get_owner()));
SASSERT(n1->get_decl() == n2->get_decl());
+ if (m_used_cc)
+ m_used_cc(to_app(n1->get_owner()), to_app(n2->get_owner()));
if (comm &&
n1->get_arg(0)->get_root() == n2->get_arg(1)->get_root() &&
n1->get_arg(1)->get_root() == n2->get_arg(0)->get_root()) {
@@ -268,30 +271,28 @@ namespace euf {
push_lca(n1->get_arg(i), n2->get_arg(i));
}
- void egraph::push_lca(enode* a, enode* b) {
+ enode* egraph::find_lca(enode* a, enode* b) {
SASSERT(a->get_root() == b->get_root());
- enode* n = a;
- while (n) {
- n->mark2();
- n = n->m_target;
- }
- n = b;
- while (n) {
- if (n->is_marked2())
- n->unmark2();
- else if (!n->is_marked1())
- m_todo.push_back(n);
- n = n->m_target;
- }
- n = a;
- while (n->is_marked2()) {
- n->unmark2();
- if (!n->is_marked1())
- m_todo.push_back(n);
+ a->mark2_targets<true>();
+ while (!b->is_marked2())
+ b = b->m_target;
+ a->mark2_targets<false>();
+ return b;
+ }
+
+ void egraph::push_to_lca(enode* n, enode* lca) {
+ while (n != lca) {
+ m_todo.push_back(n);
n = n->m_target;
}
}
+ void egraph::push_lca(enode* a, enode* b) {
+ enode* lca = find_lca(a, b);
+ push_to_lca(a, lca);
+ push_to_lca(b, lca);
+ }
+
void egraph::push_todo(enode* n) {
while (n) {
m_todo.push_back(n);
@@ -313,7 +314,11 @@ namespace euf {
void egraph::explain_eq(ptr_vector<T>& justifications, enode* a, enode* b, bool comm) {
SASSERT(m_todo.empty());
SASSERT(a->get_root() == b->get_root());
- push_lca(a, b);
+ enode* lca = find_lca(a, b);
+ push_to_lca(a, lca);
+ push_to_lca(b, lca);
+ if (m_used_eq)
+ m_used_eq(a->get_owner(), b->get_owner(), lca->get_owner());
explain_todo(justifications);
}
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 4988ebb32..76f946ee1 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -70,7 +70,8 @@ namespace euf {
enode_vector m_new_lits;
enode_vector m_todo;
stats m_stats;
-
+ std::function<void(expr*,expr*,expr*)> m_used_eq;
+ std::function<void(app*,app*)> m_used_cc;
void push_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
m_eqs.push_back(add_eq_record(r1, n1, r2_num_parents));
@@ -87,6 +88,8 @@ namespace euf {
void reinsert_equality(enode* p);
void update_children(enode* n);
void push_lca(enode* a, enode* b);
+ enode* find_lca(enode* a, enode* b);
+ void push_to_lca(enode* a, enode* lca);
void push_congruence(enode* n1, enode* n2, bool commutative);
void push_todo(enode* n);
template <typename T>
@@ -126,6 +129,10 @@ namespace euf {
bool inconsistent() const { return m_inconsistent; }
enode_vector const& new_eqs() const { return m_new_eqs; }
enode_vector const& new_lits() const { return m_new_lits; }
+
+ void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; }
+ void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; }
+
template <typename T>
void explain(ptr_vector<T>& justifications);
template <typename T>
diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h
index 776747db2..59166df31 100644
--- a/src/ast/euf/euf_enode.h
+++ b/src/ast/euf/euf_enode.h
@@ -104,11 +104,29 @@ namespace euf {
void mark2() { m_mark2 = true; }
void unmark2() { m_mark2 = false; }
bool is_marked2() { return m_mark2; }
+
+ template<bool m> void mark1_targets() {
+ enode* n = this;
+ while (n) {
+ if (m) n->mark1(); else n->unmark1();
+ n = n->m_target;
+ }
+ }
+ template<bool m> void mark2_targets() {
+ enode* n = this;
+ while (n) {
+ if (m) n->mark2(); else n->unmark2();
+ n = n->m_target;
+ }
+ }
+
void add_parent(enode* p) { m_parents.push_back(p); }
unsigned class_size() const { return m_class_size; }
+ bool is_root() const { return m_root == this; }
enode* get_root() const { return m_root; }
expr* get_owner() const { return m_owner; }
unsigned get_owner_id() const { return m_owner->get_id(); }
+ unsigned get_root_id() const { return m_root->m_owner->get_id(); }
void inc_class_size(unsigned n) { m_class_size += n; }
void dec_class_size(unsigned n) { m_class_size -= n; }
diff --git a/src/sat/ba/CMakeLists.txt b/src/sat/ba/CMakeLists.txt
deleted file mode 100644
index fc94b42f8..000000000
--- a/src/sat/ba/CMakeLists.txt
+++ /dev/null
@@ -1,8 +0,0 @@
-z3_add_component(sat_ba
- SOURCES
- ba_solver.cpp
- ba_internalize.cpp
- COMPONENT_DEPENDENCIES
- sat
-)
-
diff --git a/src/sat/euf/CMakeLists.txt b/src/sat/euf/CMakeLists.txt
deleted file mode 100644
index b716ea015..000000000
--- a/src/sat/euf/CMakeLists.txt
+++ /dev/null
@@ -1,9 +0,0 @@
-z3_add_component(sat_euf
- SOURCES
- euf_solver.cpp
- euf_model.cpp
- COMPONENT_DEPENDENCIES
- sat
- sat_smt
- euf
-)
diff --git a/src/sat/euf/euf_model.cpp b/src/sat/euf/euf_model.cpp
deleted file mode 100644
index 9c789140e..000000000
--- a/src/sat/euf/euf_model.cpp
+++ /dev/null
@@ -1,72 +0,0 @@
-/*++
-Copyright (c) 2020 Microsoft Corporation
-
-Module Name:
-
- euf_model.cpp
-
-Abstract:
-
- Model building for EUF solver plugin.
-
-Author:
-
- Nikolaj Bjorner (nbjorner) 2020-08-25
-
---*/
-
-#include "ast/ast_pp.h"
-#include "sat/euf/euf_solver.h"
-#include "model/value_factory.h"
-
-namespace euf {
-
- model_converter* solver::get_model() {
- sat::th_dependencies deps;
- collect_dependencies(deps);
- // deps.sort();
- expr_ref_vector values(m);
- dependencies2values(deps, values);
- return nullptr;
- }
-
- void solver::collect_dependencies(sat::th_dependencies& deps) {
-
- }
-
-
- void solver::dependencies2values(sat::th_dependencies& deps, expr_ref_vector& values) {
-
- user_sort_factory user_sort(m);
- for (enode* n : deps) {
- unsigned id = n->get_root()->get_owner_id();
- if (values.get(id) != nullptr)
- continue;
- expr* e = n->get_owner();
- values.reserve(id + 1);
- if (m.is_bool(e)) {
- switch (s().value(m_expr2var.to_bool_var(e))) {
- case l_true:
- values.set(id, m.mk_true());
- break;
- default:
- values.set(id, m.mk_false());
- break;
- }
- continue;
- }
- auto* mb = get_model_builder(e);
- if (mb)
- mb->add_value(n, values);
- else if (m.is_uninterp(m.get_sort(e))) {
- expr* v = user_sort.get_fresh_value(m.get_sort(e));
- values.set(id, v);
- }
- else {
- IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n");
- }
-
- }
- NOT_IMPLEMENTED_YET();
- }
-}
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index 1493044ca..9ab1fcd0c 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -86,7 +86,7 @@ namespace sat {
virtual unsigned max_var(unsigned w) const = 0;
virtual 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) {
+ std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) {
return false;
}
};
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index c52bf4d7c..06b843b44 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -454,6 +454,8 @@ namespace sat {
void display_lookahead_scores(std::ostream& out);
+ stats const& stats() const { return m_stats; }
+
protected:
unsigned m_conflicts_since_init;
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 4bb9563e9..ef020d3de 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -615,7 +615,7 @@ public:
private:
- lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
+ lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm) {
m_solver.pop_to_base_level();
if (m_solver.inconsistent())
return l_false;
@@ -662,7 +662,7 @@ private:
// ensure that if goal is already internalized, then import mc from m_solver.
- m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, is_incremental(), is_lemma);
+ m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, is_incremental());
m_goal2sat.get_interpreted_atoms(atoms);
if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m);
m_sat_mc->flush_smc(m_solver, m_map);
@@ -690,7 +690,7 @@ private:
for (unsigned i = 0; i < get_num_assumptions(); ++i) {
g->assert_expr(get_assumption(i), m.mk_leaf(get_assumption(i)));
}
- lbool res = internalize_goal(g, dep2asm, false);
+ lbool res = internalize_goal(g, dep2asm);
if (res == l_true) {
extract_assumptions(sz, asms, dep2asm);
}
@@ -831,7 +831,7 @@ private:
expr* fml = m_fmls.get(i);
g->assert_expr(fml);
}
- lbool res = internalize_goal(g, dep2asm, false);
+ lbool res = internalize_goal(g, dep2asm);
if (res != l_undef) {
m_fmls_head = m_fmls.size();
}
diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt
index a4c9e363a..e90730620 100644
--- a/src/sat/smt/CMakeLists.txt
+++ b/src/sat/smt/CMakeLists.txt
@@ -1,7 +1,12 @@
z3_add_component(sat_smt
SOURCES
atom2bool_var.cpp
- sat_th.cpp
+ ba_solver.cpp
+ xor_solver.cpp
+ ba_internalize.cpp
+ euf_ackerman.cpp
+ euf_solver.cpp
+ euf_model.cpp
COMPONENT_DEPENDENCIES
sat
ast
diff --git a/src/sat/ba/ba_internalize.cpp b/src/sat/smt/ba_internalize.cpp
similarity index 76%
rename from src/sat/ba/ba_internalize.cpp
rename to src/sat/smt/ba_internalize.cpp
index 27606ff55..00ebd0d19 100644
--- a/src/sat/ba/ba_internalize.cpp
+++ b/src/sat/smt/ba_internalize.cpp
@@ -7,7 +7,7 @@ Module Name:
Abstract:
- INternalize methods for Boolean algebra operators.
+ Internalize methods for Boolean algebra operators.
Author:
@@ -16,12 +16,11 @@ Author:
--*/
-#include "sat/ba/ba_internalize.h"
+#include "sat/smt/ba_internalize.h"
namespace sat {
- literal ba_internalize::internalize(sat_internalizer& si, expr* e, bool sign, bool root) {
- m_si = &si;
+ literal ba_internalize::internalize(expr* e, bool sign, bool root) {
if (pb.is_pb(e))
return internalize_pb(e, sign, root);
if (m.is_xor(e))
@@ -35,7 +34,7 @@ namespace sat {
sat::bool_var v = m_solver.add_var(true);
lits.push_back(literal(v, true));
auto add_expr = [&](expr* a) {
- literal lit = m_si->internalize(a);
+ literal lit = si.internalize(a);
m_solver.set_external(lit.var());
lits.push_back(lit);
};
@@ -100,7 +99,7 @@ namespace sat {
void ba_internalize::convert_pb_args(app* t, literal_vector& lits) {
for (expr* arg : *t) {
- lits.push_back(m_si->internalize(arg));
+ lits.push_back(si.internalize(arg));
m_solver.set_external(lits.back().var());
}
}
@@ -192,10 +191,10 @@ namespace sat {
literal l1(v1, false), l2(v2, false);
bool_var v = m_solver.add_var(false);
literal l(v, false);
- m_si->mk_clause(~l, l1);
- m_si->mk_clause(~l, l2);
- m_si->mk_clause(~l1, ~l2, l);
- m_si->cache(t, l);
+ si.mk_clause(~l, l1);
+ si.mk_clause(~l, l2);
+ si.mk_clause(~l1, ~l2, l);
+ si.cache(t, l);
if (sign) l.neg();
return l;
}
@@ -218,7 +217,7 @@ namespace sat {
bool_var v = m_solver.add_var(true);
literal lit(v, false);
ba.add_at_least(v, lits, k.get_unsigned());
- m_si->cache(t, lit);
+ si.cache(t, lit);
if (sign) lit.neg();
TRACE("ba", tout << "root: " << root << " lit: " << lit << "\n";);
return lit;
@@ -245,7 +244,7 @@ namespace sat {
bool_var v = m_solver.add_var(true);
literal lit(v, false);
ba.add_at_least(v, lits, k2);
- m_si->cache(t, lit);
+ si.cache(t, lit);
if (sign) lit.neg();
return lit;
}
@@ -267,10 +266,10 @@ namespace sat {
literal l1(v1, false), l2(v2, false);
bool_var v = m_solver.add_var(false);
literal l(v, false);
- m_si->mk_clause(~l, l1);
- m_si->mk_clause(~l, l2);
- m_si->mk_clause(~l1, ~l2, l);
- m_si->cache(t, l);
+ si.mk_clause(~l, l1);
+ si.mk_clause(~l, l2);
+ si.mk_clause(~l1, ~l2, l);
+ si.cache(t, l);
if (sign) l.neg();
return l;
}
@@ -278,4 +277,63 @@ namespace sat {
return null_literal;
}
}
+
+ expr_ref ba_decompile::get_card(std::function<expr_ref(sat::literal)>& lit2expr, ba_solver::card const& c) {
+ ptr_buffer<expr> lits;
+ for (sat::literal l : c) {
+ lits.push_back(lit2expr(l));
+ }
+ expr_ref fml(pb.mk_at_least_k(c.size(), lits.c_ptr(), c.k()), m);
+
+ if (c.lit() != sat::null_literal) {
+ fml = m.mk_eq(lit2expr(c.lit()), fml);
+ }
+ return fml;
+ }
+
+ expr_ref ba_decompile::get_pb(std::function<expr_ref(sat::literal)>& lit2expr, ba_solver::pb const& p) {
+ ptr_buffer<expr> lits;
+ vector<rational> coeffs;
+ for (auto const& wl : p) {
+ lits.push_back(lit2expr(wl.second));
+ coeffs.push_back(rational(wl.first));
+ }
+ rational k(p.k());
+ expr_ref fml(pb.mk_ge(p.size(), coeffs.c_ptr(), lits.c_ptr(), k), m);
+
+ if (p.lit() != sat::null_literal) {
+ fml = m.mk_eq(lit2expr(p.lit()), fml);
+ }
+ return fml;
+ }
+
+ expr_ref ba_decompile::get_xor(std::function<expr_ref(sat::literal)>& lit2expr, ba_solver::xr const& x) {
+ ptr_buffer<expr> lits;
+ for (sat::literal l : x) {
+ lits.push_back(lit2expr(l));
+ }
+ expr_ref fml(m.mk_xor(x.size(), lits.c_ptr()), m);
+
+ if (x.lit() != sat::null_literal) {
+ fml = m.mk_eq(lit2expr(x.lit()), fml);
+ }
+ return fml;
+ }
+
+ bool ba_decompile::to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) {
+ for (auto* c : ba.constraints()) {
+ switch (c->tag()) {
+ case ba_solver::card_t:
+ fmls.push_back(get_card(l2e, c->to_card()));
+ break;
+ case sat::ba_solver::pb_t:
+ fmls.push_back(get_pb(l2e, c->to_pb()));
+ break;
+ case sat::ba_solver::xr_t:
+ fmls.push_back(get_xor(l2e, c->to_xr()));
+ break;
+ }
+ }
+ return true;
+ }
}
diff --git a/src/sat/ba/ba_internalize.h b/src/sat/smt/ba_internalize.h
similarity index 58%
rename from src/sat/ba/ba_internalize.h
rename to src/sat/smt/ba_internalize.h
index 71ab20614..39864acae 100644
--- a/src/sat/ba/ba_internalize.h
+++ b/src/sat/smt/ba_internalize.h
@@ -19,7 +19,7 @@ Author:
#pragma once
#include "sat/smt/sat_th.h"
-#include "sat/ba/ba_solver.h"
+#include "sat/smt/ba_solver.h"
#include "ast/pb_decl_plugin.h"
@@ -31,7 +31,7 @@ namespace sat {
pb_util pb;
ba_solver& ba;
solver_core& m_solver;
- sat_internalizer* m_si;
+ sat_internalizer& si;
literal convert_eq_k(app* t, rational const& k, bool root, bool sign);
literal convert_at_most_k(app* t, rational const& k, bool root, bool sign);
literal convert_at_least_k(app* t, rational const& k, bool root, bool sign);
@@ -44,10 +44,30 @@ namespace sat {
void convert_pb_args(app* t, literal_vector& lits);
literal internalize_pb(expr* e, bool sign, bool root);
literal internalize_xor(expr* e, bool sign, bool root);
+
public:
- ba_internalize(ba_solver& ba, solver_core& s, ast_manager& m) : m(m), pb(m), ba(ba), m_solver(s) {}
+ ba_internalize(ba_solver& ba, solver_core& s, sat_internalizer& si, ast_manager& m) :
+ m(m), pb(m), ba(ba), m_solver(s), si(si) {}
~ba_internalize() override {}
- literal internalize(sat_internalizer& si, expr* e, bool sign, bool root) override;
-
+ literal internalize(expr* e, bool sign, bool root) override;
+
+ };
+
+ class ba_decompile : public sat::th_decompile {
+ ast_manager& m;
+ ba_solver& ba;
+ solver_core& m_solver;
+ pb_util pb;
+
+ expr_ref get_card(std::function<expr_ref(sat::literal)>& l2e, ba_solver::card const& c);
+ expr_ref get_pb(std::function<expr_ref(sat::literal)>& l2e, ba_solver::pb const& p);
+ expr_ref get_xor(std::function<expr_ref(sat::literal)>& l2e, ba_solver::xr const& x);
+ public:
+ ba_decompile(ba_solver& ba, solver_core& s, ast_manager& m) :
+ m(m), ba(ba), m_solver(s), pb(m) {}
+
+ ~ba_decompile() override {}
+
+ bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
};
}
diff --git a/src/sat/ba/ba_solver.cpp b/src/sat/smt/ba_solver.cpp
similarity index 89%
rename from src/sat/ba/ba_solver.cpp
rename to src/sat/smt/ba_solver.cpp
index 646cb6534..96e18b8bb 100644
--- a/src/sat/ba/ba_solver.cpp
+++ b/src/sat/smt/ba_solver.cpp
@@ -7,7 +7,7 @@ Module Name:
Abstract:
- Extension for cardinality and xr reasoning.
+ Extension for cardinality and xor reasoning.
Author:
@@ -18,9 +18,9 @@ Revision History:
--*/
#include <cmath>
-#include "sat/ba/ba_solver.h"
-#include "sat/sat_types.h"
#include "util/mpz.h"
+#include "sat/sat_types.h"
+#include "sat/smt/ba_solver.h"
#include "sat/sat_simplifier_params.hpp"
#include "sat/sat_xor_finder.h"
@@ -55,15 +55,6 @@ namespace sat {
return static_cast<pb_base const&>(*this);
}
- ba_solver::xr& ba_solver::constraint::to_xr() {
- SASSERT(is_xr());
- return static_cast<xr&>(*this);
- }
-
- ba_solver::xr const& ba_solver::constraint::to_xr() const{
- SASSERT(is_xr());
- return static_cast<xr const&>(*this);
- }
unsigned ba_solver::constraint::fold_max_var(unsigned w) const {
if (lit() != null_literal) w = std::max(w, lit().var());
@@ -205,32 +196,7 @@ namespace sat {
}
- // -----------------------------------
- // xr
- ba_solver::xr::xr(extension* e, unsigned id, literal_vector const& lits):
- constraint(e, xr_t, id, null_literal, lits.size(), get_obj_size(lits.size())) {
- for (unsigned i = 0; i < size(); ++i) {
- m_lits[i] = lits[i];
- }
- }
-
- bool ba_solver::xr::is_watching(literal l) const {
- return
- l == (*this)[0] || l == (*this)[1] ||
- ~l == (*this)[0] || ~l == (*this)[1];
- }
-
- bool ba_solver::xr::well_formed() const {
- uint_set vars;
- if (lit() != null_literal) vars.insert(lit().var());
- for (literal l : *this) {
- bool_var v = l.var();
- if (vars.contains(v)) return false;
- vars.insert(v);
- }
- return true;
- }
// ----------------------------
// card
@@ -908,107 +874,6 @@ namespace sat {
out << ">= " << p.k() << "\n";
}
- // --------------------
- // xr:
-
- void ba_solver::clear_watch(xr& x) {
- x.clear_watch();
- unwatch_literal(x[0], x);
- unwatch_literal(x[1], x);
- unwatch_literal(~x[0], x);
- unwatch_literal(~x[1], x);
- }
-
- bool ba_solver::parity(xr const& x, unsigned offset) const {
- bool odd = false;
- unsigned sz = x.size();
- for (unsigned i = offset; i < sz; ++i) {
- SASSERT(value(x[i]) != l_undef);
- if (value(x[i]) == l_true) {
- odd = !odd;
- }
- }
- return odd;
- }
-
- bool ba_solver::init_watch(xr& x) {
- clear_watch(x);
- VERIFY(x.lit() == null_literal);
- TRACE("ba", display(tout, x, true););
- unsigned sz = x.size();
- unsigned j = 0;
- for (unsigned i = 0; i < sz && j < 2; ++i) {
- if (value(x[i]) == l_undef) {
- x.swap(i, j);
- ++j;
- }
- }
- switch (j) {
- case 0:
- if (!parity(x, 0)) {
- unsigned l = lvl(x[0]);
- j = 1;
- for (unsigned i = 1; i < sz; ++i) {
- if (lvl(x[i]) > l) {
- j = i;
- l = lvl(x[i]);
- }
- }
- set_conflict(x, x[j]);
- }
- return false;
- case 1:
- SASSERT(x.lit() == null_literal || value(x.lit()) == l_true);
- assign(x, parity(x, 1) ? ~x[0] : x[0]);
- return false;
- default:
- SASSERT(j == 2);
- watch_literal(x[0], x);
- watch_literal(x[1], x);
- watch_literal(~x[0], x);
- watch_literal(~x[1], x);
- return true;
- }
- }
-
-
- lbool ba_solver::add_assign(xr& x, literal alit) {
- // literal is assigned
- unsigned sz = x.size();
- TRACE("ba", tout << "assign: " << ~alit << "@" << lvl(~alit) << " " << x << "\n"; display(tout, x, true); );
-
- VERIFY(x.lit() == null_literal);
- SASSERT(value(alit) != l_undef);
- unsigned index = (x[1].var() == alit.var()) ? 1 : 0;
- VERIFY(x[index].var() == alit.var());
-
- // find a literal to swap with:
- for (unsigned i = 2; i < sz; ++i) {
- literal lit = x[i];
- if (value(lit) == l_undef) {
- x.swap(index, i);
- unwatch_literal(~alit, x);
- // alit gets unwatched by propagate_core because we return l_undef
- watch_literal(lit, x);
- watch_literal(~lit, x);
- TRACE("ba", tout << "swap in: " << lit << " " << x << "\n";);
- return l_undef;
- }
- }
- if (index == 0) {
- x.swap(0, 1);
- }
- // alit resides at index 1.
- VERIFY(x[1].var() == alit.var());
- if (value(x[0]) == l_undef) {
- bool p = parity(x, 1);
- assign(x, p ? ~x[0] : x[0]);
- }
- else if (!parity(x, 0)) {
- set_conflict(x, ~x[1]);
- }
- return inconsistent() ? l_false : l_true;
- }
// ---------------------------
// conflict resolution
@@ -1977,116 +1842,7 @@ namespace sat {
add_pb_ge(lit, wlits, k, false);
}
- void ba_solver::add_xr(literal_vector const& lits) {
- add_xr(lits, false);
- }
- bool ba_solver::all_distinct(literal_vector const& lits) {
- return s().all_distinct(lits);
- }
-
- bool ba_solver::all_distinct(clause const& c) {
- return s().all_distinct(c);
- }
-
- bool ba_solver::all_distinct(xr const& x) {
- init_visited();
- for (literal l : x) {
- if (is_visited(l.var())) {
- return false;
- }
- mark_visited(l.var());
- }
- return true;
- }
-
- literal ba_solver::add_xor_def(literal_vector& lits, bool learned) {
- unsigned sz = lits.size();
- SASSERT (sz > 1);
- VERIFY(all_distinct(lits));
- init_visited();
- bool parity1 = true;
- for (literal l : lits) {
- mark_visited(l.var());
- parity1 ^= l.sign();
- }
- for (auto const & w : get_wlist(lits[0])) {
- if (w.get_kind() != watched::EXT_CONSTRAINT) continue;
- constraint& c = index2constraint(w.get_ext_constraint_idx());
- if (!c.is_xr()) continue;
- xr& x = c.to_xr();
- if (sz + 1 != x.size()) continue;
- bool is_match = true;
- literal l0 = null_literal;
- bool parity2 = true;
- for (literal l : x) {
- if (!is_visited(l.var())) {
- if (l0 == null_literal) {
- l0 = l;
- }
- else {
- is_match = false;
- break;
- }
- }
- else {
- parity2 ^= l.sign();
- }
- }
- if (is_match) {
- SASSERT(all_distinct(x));
- if (parity1 == parity2) l0.neg();
- if (!learned && x.learned()) {
- set_non_learned(x);
- }
- return l0;
- }
- }
- bool_var v = s().mk_var(true, true);
- literal lit(v, false);
- lits.push_back(~lit);
- add_xr(lits, learned);
- return lit;
- }
-
-
- ba_solver::constraint* ba_solver::add_xr(literal_vector const& _lits, bool learned) {
- literal_vector lits;
- u_map<bool> var2sign;
- bool sign = false, odd = false;
- for (literal lit : _lits) {
- if (var2sign.find(lit.var(), sign)) {
- var2sign.erase(lit.var());
- odd ^= (sign ^ lit.sign());
- }
- else {
- var2sign.insert(lit.var(), lit.sign());
- }
- }
-
- for (auto const& kv : var2sign) {
- lits.push_back(literal(kv.m_key, kv.m_value));
- }
- if (odd && !lits.empty()) {
- lits[0].neg();
- }
- switch (lits.size()) {
- case 0:
- if (!odd)
- s().set_conflict(justification(0));
- return nullptr;
- case 1:
- s().assign_scoped(lits[0]);
- return nullptr;
- default:
- break;
- }
- void * mem = m_allocator.allocate(xr::get_obj_size(lits.size()));
- xr* x = new (mem) xr(this, next_id(), lits);
- x->set_learned(learned);
- add_constraint(x);
- return x;
- }
/*
\brief return true to keep watching literal.
@@ -2178,89 +1934,6 @@ namespace sat {
m_parity_marks[v] = 0;
}
- /**
- \brief perform parity resolution on xr premises.
- The idea is to collect premises based on xr resolvents.
- Variables that are repeated an even number of times cancel out.
- */
-
- void ba_solver::get_xr_antecedents(literal l, unsigned index, justification js, literal_vector& r) {
- unsigned level = lvl(l);
- bool_var v = l.var();
- SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION);
- TRACE("ba", tout << l << ": " << js << "\n";
- for (unsigned i = 0; i <= index; ++i) tout << s().m_trail[i] << " "; tout << "\n";
- s().display_units(tout);
- );
-
-
- unsigned num_marks = 0;
- while (true) {
- TRACE("ba", tout << "process: " << l << " " << js << "\n";);
- if (js.get_kind() == justification::EXT_JUSTIFICATION) {
- constraint& c = index2constraint(js.get_ext_justification_idx());
- TRACE("ba", tout << c << "\n";);
- if (!c.is_xr()) {
- r.push_back(l);
- }
- else {
- xr& x = c.to_xr();
- if (x[1].var() == l.var()) {
- x.swap(0, 1);
- }
- VERIFY(x[0].var() == l.var());
- for (unsigned i = 1; i < x.size(); ++i) {
- literal lit(value(x[i]) == l_true ? x[i] : ~x[i]);
- inc_parity(lit.var());
- if (lvl(lit) == level) {
- TRACE("ba", tout << "mark: " << lit << "\n";);
- ++num_marks;
- }
- else {
- m_parity_trail.push_back(lit);
- }
- }
- }
- }
- else {
- r.push_back(l);
- }
- bool found = false;
- while (num_marks > 0) {
- l = s().m_trail[index];
- v = l.var();
- unsigned n = get_parity(v);
- if (n > 0 && lvl(l) == level) {
- reset_parity(v);
- num_marks -= n;
- if (n % 2 == 1) {
- found = true;
- break;
- }
- }
- --index;
- }
- if (!found) {
- break;
- }
- --index;
- js = s().m_justification[v];
- }
-
- // now walk the defined literals
-
- for (literal lit : m_parity_trail) {
- if (get_parity(lit.var()) % 2 == 1) {
- r.push_back(lit);
- }
- else {
- // IF_VERBOSE(2, verbose_stream() << "skip even parity: " << lit << "\n";);
- }
- reset_parity(lit.var());
- }
- m_parity_trail.reset();
- TRACE("ba", tout << r << "\n";);
- }
/**
\brief retrieve a sufficient set of literals from p that imply l.
@@ -2400,12 +2073,6 @@ namespace sat {
}
}
- void ba_solver::simplify(xr& x) {
- if (x.learned()) {
- x.set_removed();
- m_constraint_removed = true;
- }
- }
void ba_solver::get_antecedents(literal l, card const& c, literal_vector& r) {
if (l == ~c.lit()) {
@@ -2431,24 +2098,6 @@ namespace sat {
}
}
- void ba_solver::get_antecedents(literal l, xr const& x, literal_vector& r) {
- if (x.lit() != null_literal) r.push_back(x.lit());
- // TRACE("ba", display(tout << l << " ", x, true););
- SASSERT(x.lit() == null_literal || value(x.lit()) == l_true);
- SASSERT(x[0].var() == l.var() || x[1].var() == l.var());
- if (x[0].var() == l.var()) {
- SASSERT(value(x[1]) != l_undef);
- r.push_back(value(x[1]) == l_true ? x[1] : ~x[1]);
- }
- else {
- SASSERT(value(x[0]) != l_undef);
- r.push_back(value(x[0]) == l_true ? x[0] : ~x[0]);
- }
- for (unsigned i = 2; i < x.size(); ++i) {
- SASSERT(value(x[i]) != l_undef);
- r.push_back(value(x[i]) == l_true ? x[i] : ~x[i]);
- }
- }
// ----------------------------
// constraint generic methods
@@ -2617,31 +2266,6 @@ namespace sat {
return l_undef;
}
- lbool ba_solver::eval(xr const& x) const {
- bool odd = false;
-
- for (auto l : x) {
- switch (value(l)) {
- case l_true: odd = !odd; break;
- case l_false: break;
- default: return l_undef;
- }
- }
- return odd ? l_true : l_false;
- }
-
- lbool ba_solver::eval(model const& m, xr const& x) const {
- bool odd = false;
-
- for (auto l : x) {
- switch (value(m, l)) {
- case l_true: odd = !odd; break;
- case l_false: break;
- default: return l_undef;
- }
- }
- return odd ? l_true : l_false;
- }
bool ba_solver::validate() {
if (!validate_watch_literals()) {
@@ -2940,52 +2564,9 @@ namespace sat {
}
}
- void ba_solver::pre_simplify() {
- VERIFY(s().at_base_lvl());
- if (s().inconsistent())
- return;
- m_constraint_removed = false;
- xor_finder xf(s());
- for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) pre_simplify(xf, *m_constraints[i]);
- for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) pre_simplify(xf, *m_learned[i]);
- bool change = m_constraint_removed;
- cleanup_constraints();
- if (change) {
- // remove non-used variables.
- init_use_lists();
- remove_unused_defs();
- set_non_external();
- }
- }
-
- void ba_solver::pre_simplify(xor_finder& xf, constraint& c) {
- if (c.is_xr() && c.size() <= xf.max_xor_size()) {
- unsigned sz = c.size();
- literal_vector lits;
- bool parity = false;
- xr const& x = c.to_xr();
- for (literal lit : x) {
- parity ^= lit.sign();
- }
-
- // IF_VERBOSE(0, verbose_stream() << "blast: " << c << "\n");
- for (unsigned i = 0; i < (1ul << sz); ++i) {
- if (xf.parity(sz, i) == parity) {
- lits.reset();
- for (unsigned j = 0; j < sz; ++j) {
- lits.push_back(literal(x[j].var(), (0 != (i & (1 << j)))));
- }
- // IF_VERBOSE(0, verbose_stream() << lits << "\n");
- s().mk_clause(lits);
- }
- }
- c.set_removed();
- m_constraint_removed = true;
- }
- }
-
void ba_solver::simplify() {
- if (!s().at_base_lvl()) s().pop_to_base_level();
+ if (!s().at_base_lvl())
+ s().pop_to_base_level();
if (s().inconsistent())
return;
unsigned trail_sz, count = 0;
@@ -3381,9 +2962,6 @@ namespace sat {
return false;
}
- bool ba_solver::clausify(xr& x) {
- return false;
- }
bool ba_solver::clausify(card& c) {
return false;
@@ -3771,82 +3349,6 @@ namespace sat {
}
}
- // merge xors that contain cut variable
- void ba_solver::merge_xor() {
- unsigned sz = s().num_vars();
- for (unsigned i = 0; i < sz; ++i) {
- literal lit(i, false);
- unsigned index = lit.index();
- if (m_cnstr_use_list[index].size() == 2) {
- constraint& c1 = *m_cnstr_use_list[index][0];
- constraint& c2 = *m_cnstr_use_list[index][1];
- if (c1.is_xr() && c2.is_xr() &&
- m_clause_use_list.get(lit).empty() &&
- m_clause_use_list.get(~lit).empty()) {
- bool unique = true;
- for (watched w : get_wlist(lit)) {
- if (w.is_binary_clause()) unique = false;
- }
- for (watched w : get_wlist(~lit)) {
- if (w.is_binary_clause()) unique = false;
- }
- if (!unique) continue;
- xr const& x1 = c1.to_xr();
- xr const& x2 = c2.to_xr();
- literal_vector lits, dups;
- bool parity = false;
- init_visited();
- for (literal l : x1) {
- mark_visited(l.var());
- lits.push_back(l);
- }
- for (literal l : x2) {
- if (is_visited(l.var())) {
- dups.push_back(l);
- }
- else {
- lits.push_back(l);
- }
- }
- init_visited();
- for (literal l : dups) mark_visited(l);
- unsigned j = 0;
- for (unsigned i = 0; i < lits.size(); ++i) {
- literal l = lits[i];
- if (is_visited(l)) {
- // skip
- }
- else if (is_visited(~l)) {
- parity ^= true;
- }
- else {
- lits[j++] = l;
- }
- }
- lits.shrink(j);
- if (!parity) lits[0].neg();
- IF_VERBOSE(1, verbose_stream() << "binary " << lits << " : " << c1 << " " << c2 << "\n");
- c1.set_removed();
- c2.set_removed();
- add_xr(lits, !c1.learned() && !c2.learned());
- m_constraint_removed = true;
- }
- }
- }
- }
-
- void ba_solver::extract_xor() {
- xor_finder xf(s());
- std::function<void (literal_vector const&)> f = [this](literal_vector const& l) { add_xr(l, false); };
- xf.set(f);
- clause_vector clauses(s().clauses());
- xf(clauses);
- for (clause* cp : xf.removed_clauses()) {
- cp->set_removed(true);
- m_clause_removed = true;
- }
- }
-
void ba_solver::init_visited() { s().init_visited(); }
void ba_solver::mark_visited(literal l) { s().mark_visited(l); }
void ba_solver::mark_visited(bool_var v) { s().mark_visited(v); }
@@ -3915,6 +3417,7 @@ namespace sat {
cs.set_end(it2);
}
+
/*
\brief subsumption between two cardinality constraints
- A >= k subsumes A + B >= k' for k' <= k
@@ -4380,23 +3883,6 @@ namespace sat {
out << ">= " << ineq.m_k << "\n";
}
- void ba_solver::display(std::ostream& out, xr const& x, bool values) const {
- out << "xr: ";
- for (literal l : x) {
- out << l;
- if (values) {
- out << "@(" << value(l);
- if (value(l) != l_undef) {
- out << ":" << lvl(l);
- }
- out << ") ";
- }
- else {
- out << " ";
- }
- }
- out << "\n";
- }
void ba_solver::display_lit(std::ostream& out, literal lit, unsigned sz, bool values) const {
if (lit != null_literal) {
@@ -4555,13 +4041,6 @@ namespace sat {
return false;
}
- bool ba_solver::validate_unit_propagation(xr const& x, literal alit) const {
- if (value(x.lit()) != l_true) return false;
- for (unsigned i = 1; i < x.size(); ++i) {
- if (value(x[i]) == l_undef) return false;
- }
- return true;
- }
bool ba_solver::validate_lemma() {
int64_t bound64 = m_bound;
diff --git a/src/sat/ba/ba_solver.h b/src/sat/smt/ba_solver.h
similarity index 100%
rename from src/sat/ba/ba_solver.h
rename to src/sat/smt/ba_solver.h
diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp
new file mode 100644
index 000000000..bc6f36e6d
--- /dev/null
+++ b/src/sat/smt/euf_ackerman.cpp
@@ -0,0 +1,211 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+ euf_ackerman.cpp
+
+Abstract:
+
+ Ackerman reduction plugin for EUF
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2020-08-28
+
+--*/
+#pragma once
+
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/euf_ackerman.h"
+
+namespace euf {
+
+ ackerman::ackerman(solver& s, ast_manager& m): s(s), m(m) {
+ new_tmp();
+ }
+
+ ackerman::~ackerman() {
+ reset();
+ dealloc(m_tmp_inference);
+ }
+
+ void ackerman::reset() {
+ for (inference* inf : m_table) {
+ m.dec_ref(inf->a);
+ m.dec_ref(inf->b);
+ m.dec_ref(inf->c);
+ }
+ m_table.reset();
+ m_queue = nullptr;
+ }
+
+ void ackerman::insert(expr* a, expr* b, expr* lca) {
+ if (a->get_id() > b->get_id())
+ std::swap(a, b);
+ inference& inf = *m_tmp_inference;
+ inf.a = a;
+ inf.b = b;
+ inf.c = lca;
+ inf.is_cc = false;
+ insert();
+ }
+
+ void ackerman::insert(app* a, app* b) {
+ if (a->get_id() > b->get_id())
+ std::swap(a, b);
+ inference& inf = *m_tmp_inference;
+ inf.a = a;
+ inf.b = b;
+ inf.c = nullptr;
+ inf.is_cc = true;
+ insert();
+ }
+
+ void ackerman::remove_from_queue(inference* inf) {
+ if (m_queue->m_next == m_queue) {
+ SASSERT(inf == m_queue);
+ m_queue = nullptr;
+ return;
+ }
+ if (m_queue == inf)
+ m_queue = inf->m_next;
+ auto* next = inf->m_next;
+ auto* prev = inf->m_prev;
+ prev->m_next = next;
+ next->m_prev = prev;
+ }
+
+ void ackerman::push_to_front(inference* inf) {
+ if (!m_queue) {
+ m_queue = inf;
+ }
+ else if (m_queue != inf) {
+ auto* next = inf->m_next;
+ auto* prev = inf->m_prev;
+ prev->m_next = next;
+ next->m_prev = prev;
+ inf->m_prev = m_queue->m_prev;
+ inf->m_next = m_queue;
+ m_queue->m_prev = inf;
+ }
+ }
+
+ void ackerman::insert() {
+ inference* inf = m_tmp_inference;
+ inference* other = m_table.insert_if_not_there(inf);
+ if (other == inf) {
+ m.inc_ref(inf->a);
+ m.inc_ref(inf->b);
+ m.inc_ref(inf->c);
+ }
+ else
+ new_tmp();
+ other->m_count++;
+ push_to_front(other);
+ }
+
+ void ackerman::remove(inference* inf) {
+ remove_from_queue(inf);
+ m_table.erase(inf);
+ m.dec_ref(inf->a);
+ m.dec_ref(inf->b);
+ m.dec_ref(inf->c);
+ dealloc(inf);
+ }
+
+ void ackerman::new_tmp() {
+ m_tmp_inference = alloc(inference);
+ m_tmp_inference->m_next = m_tmp_inference->m_prev = m_tmp_inference;
+ m_tmp_inference->m_count = 0;
+ }
+
+ void ackerman::cg_conflict_eh(expr * n1, expr * n2) {
+ if (s.m_config.m_dack != DACK_ROOT)
+ return;
+ if (!is_app(n1) || !is_app(n2))
+ return;
+ app* a = to_app(n1);
+ app* b = to_app(n2);
+ if (a->get_decl() != b->get_decl() || a->get_num_args() != b->get_num_args())
+ return;
+ insert(a, b);
+ gc();
+ }
+
+ void ackerman::used_eq_eh(expr* a, expr* b, expr* c) {
+ if (!s.m_config.m_dack_eq)
+ return;
+ if (a == b || a == c || b == c)
+ return;
+ insert(a, b, c);
+ gc();
+ }
+
+ void ackerman::used_cc_eh(app* a, app* b) {
+ if (s.m_config.m_dack != DACK_CR)
+ return;
+ SASSERT(a->get_decl() == b->get_decl());
+ SASSERT(a->get_num_args() == b->get_num_args());
+ insert(a, b);
+ gc();
+ }
+
+ void ackerman::gc() {
+ m_num_propagations_since_last_gc++;
+ if (m_num_propagations_since_last_gc <= s.m_config.m_dack_gc)
+ return;
+ m_num_propagations_since_last_gc = 0;
+
+ while (m_table.size() > m_gc_threshold)
+ remove(m_queue->m_prev);
+
+ m_gc_threshold *= 110;
+ m_gc_threshold /= 100;
+ m_gc_threshold++;
+ }
+
+ void ackerman::propagate() {
+ SASSERT(s.s().at_base_lvl());
+ auto* n = m_queue;
+ inference* k = nullptr;
+ unsigned num_prop = static_cast<unsigned>(s.s().stats().m_conflict * s.m_config.m_dack_factor);
+ num_prop = std::min(num_prop, m_table.size());
+ for (unsigned i = 0; i < num_prop; ++i, n = k) {
+ k = n->m_next;
+ if (n->m_count < s.m_config.m_dack_threshold)
+ continue;
+ if (n->is_cc)
+ add_cc(n->a, n->b);
+ else
+ add_eq(n->a, n->b, n->c);
+ remove(n);
+ }
+ }
+
+ void ackerman::add_cc(expr* _a, expr* _b) {
+ app* a = to_app(_a);
+ app* b = to_app(_b);
+ sat::literal_vector lits;
+ unsigned sz = a->get_num_args();
+ for (unsigned i = 0; i < sz; ++i) {
+ expr_ref eq(m.mk_eq(a->get_arg(i), b->get_arg(i)), m);
+ sat::literal lit = s.internalize(eq, true, false);
+ lits.push_back(~lit);
+ }
+ expr_ref eq(m.mk_eq(a, b), m);
+ lits.push_back(s.internalize(eq, false, false));
+ s.s().mk_clause(lits, true);
+ }
+
+ void ackerman::add_eq(expr* a, expr* b, expr* c) {
+ sat::literal lits[3];
+ expr_ref eq1(m.mk_eq(a, c), m);
+ expr_ref eq2(m.mk_eq(b, c), m);
+ expr_ref eq3(m.mk_eq(a, b), m);
+ lits[0] = s.internalize(eq1, true, false);
+ lits[1] = s.internalize(eq2, true, false);
+ lits[2] = s.internalize(eq3, false, false);
+ s.s().mk_clause(3, lits, true);
+ }
+}
diff --git a/src/sat/smt/euf_ackerman.h b/src/sat/smt/euf_ackerman.h
new file mode 100644
index 000000000..eeed7639c
--- /dev/null
+++ b/src/sat/smt/euf_ackerman.h
@@ -0,0 +1,89 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+ euf_ackerman.h
+
+Abstract:
+
+ Ackerman reduction plugin for EUF
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+#pragma once
+
+#include "ast/euf/euf_egraph.h"
+#include "sat/smt/atom2bool_var.h"
+#include "sat/smt/sat_th.h"
+
+namespace euf {
+
+ class solver;
+
+ class ackerman {
+
+ struct inference {
+ bool is_cc;
+ expr* a, *b, *c;
+ inference* m_next{ nullptr };
+ inference* m_prev{ nullptr };
+ unsigned m_count{ 0 };
+ inference():is_cc(false), a(nullptr), b(nullptr), c(nullptr) {}
+ inference(app* a, app* b):is_cc(true), a(a), b(b), c(nullptr) {}
+ inference(expr* a, expr* b, expr* c):is_cc(false), a(a), b(b), c(c) {}
+ };
+
+ struct inference_eq {
+ bool operator()(inference const* a, inference const* b) const {
+ return a->is_cc == b->is_cc && a->a == b->a && a->b == b->b && a->c == b->c;
+ }
+ };
+
+ struct inference_hash {
+ unsigned operator()(inference const* a) const {
+ SASSERT(a->a && a->b);
+ return mk_mix(a->a->get_id(), a->b->get_id(), a->c ? a->c->get_id() : 0);
+ }
+ };
+
+ typedef hashtable<inference*, inference_hash, inference_eq> table_t;
+
+ solver& s;
+ ast_manager& m;
+ table_t m_table;
+ inference* m_queue { nullptr };
+ inference* m_tmp_inference { nullptr };
+ unsigned m_gc_threshold { 1 };
+ unsigned m_propagate_threshold { 0 };
+ unsigned m_num_propagations_since_last_gc { 0 };
+
+ void reset();
+ void new_tmp();
+ void insert(expr* a, expr* b, expr* lca);
+ void insert(app* a, app* b);
+ void insert();
+ void remove(inference* inf);
+ void add_cc(expr* a, expr* b);
+ void add_eq(expr* a, expr* b, expr* c);
+ void gc();
+ void push_to_front(inference* inf);
+ void remove_from_queue(inference* inf);
+
+ public:
+ ackerman(solver& s, ast_manager& m);
+ ~ackerman();
+
+ void cg_conflict_eh(expr * n1, expr * n2);
+
+ void used_eq_eh(expr* a, expr* b, expr* lca);
+
+ void used_cc_eh(app* a, app* b);
+
+ void propagate();
+ };
+
+};
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
new file mode 100644
index 000000000..048030636
--- /dev/null
+++ b/src/sat/smt/euf_model.cpp
@@ -0,0 +1,138 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+ euf_model.cpp
+
+Abstract:
+
+ Model building for EUF solver plugin.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "sat/smt/euf_solver.h"
+#include "model/value_factory.h"
+
+namespace euf {
+
+ void solver::update_model(model_ref& mdl) {
+ deps_t deps;
+ expr_ref_vector values(m);
+ collect_dependencies(deps);
+ deps.topological_sort();
+ dependencies2values(deps, values, mdl);
+ values2model(deps, values, mdl);
+ }
+
+ sat::th_model_builder* solver::get_model_builder(expr* e) const {
+ if (is_app(e))
+ return get_model_builder(to_app(e)->get_decl());
+ return nullptr;
+ }
+
+ sat::th_model_builder* solver::get_model_builder(func_decl* f) const {
+ return m_id2model_builder.get(f->get_family_id(), nullptr);
+ }
+
+ bool solver::include_func_interp(func_decl* f) const {
+ if (f->get_family_id() == null_family_id)
+ return true;
+ sat::th_model_builder* mb = get_model_builder(f);
+ return mb && mb->include_func_interp(f);
+ }
+
+ void solver::collect_dependencies(deps_t& deps) {
+ for (enode* n : m_egraph.nodes()) {
+ if (n->num_args() == 0) {
+ deps.insert(n, nullptr);
+ continue;
+ }
+ auto* mb = get_model_builder(n->get_owner());
+ if (mb)
+ mb->add_dep(n, deps);
+ else
+ deps.insert(n, nullptr);
+ }
+ }
+
+ void solver::dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref const& mdl) {
+ user_sort_factory user_sort(m);
+ for (enode* n : deps.top_sorted()) {
+ unsigned id = n->get_root_id();
+ if (values.get(id, nullptr))
+ continue;
+ expr* e = n->get_owner();
+ values.reserve(id + 1);
+ if (m.is_bool(e) && is_uninterp_const(e) && mdl->get_const_interp(to_app(e)->get_decl())) {
+ values.set(id, mdl->get_const_interp(to_app(e)->get_decl()));
+ continue;
+ }
+ // model of s() must have been fixed.
+ if (m.is_bool(e)) {
+ switch (s().value(m_expr2var.to_bool_var(e))) {
+ case l_true:
+ values.set(id, m.mk_true());
+ break;
+ case l_false:
+ values.set(id, m.mk_false());
+ break;
+ default:
+ break;
+ }
+ continue;
+ }
+ auto* mb = get_model_builder(e);
+ if (mb)
+ mb->add_value(n, values);
+ else if (m.is_uninterp(m.get_sort(e))) {
+ expr* v = user_sort.get_fresh_value(m.get_sort(e));
+ values.set(id, v);
+ }
+ else {
+ IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n");
+ }
+ }
+ }
+
+ void solver::values2model(deps_t const& deps, expr_ref_vector const& values, model_ref& mdl) {
+ ptr_vector<expr> args;
+ for (enode* n : deps.top_sorted()) {
+ expr* e = n->get_owner();
+ if (!is_app(e))
+ continue;
+ app* a = to_app(e);
+ func_decl* f = a->get_decl();
+ if (!include_func_interp(f))
+ continue;
+ if (m.is_bool(e) && is_uninterp_const(e) && mdl->get_const_interp(f))
+ continue;
+ expr* v = values.get(n->get_root_id());
+ unsigned arity = f->get_arity();
+ if (arity == 0)
+ mdl->register_decl(f, v);
+ else {
+ auto* fi = mdl->get_func_interp(f);
+ if (!fi) {
+ fi = alloc(func_interp, m, arity);
+ mdl->register_decl(f, fi);
+ }
+ args.reset();
+ for (enode* arg : enode_args(n))
+ args.push_back(values.get(arg->get_root_id()));
+ if (!fi->get_entry(args.c_ptr()))
+ fi->insert_new_entry(args.c_ptr(), v);
+ }
+ }
+ }
+
+ void solver::register_macros(model& mdl) {
+ // TODO
+ }
+
+}
diff --git a/src/sat/euf/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
similarity index 83%
rename from src/sat/euf/euf_solver.cpp
rename to src/sat/smt/euf_solver.cpp
index ed5129a52..7846a6436 100644
--- a/src/sat/euf/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -16,15 +16,19 @@ Author:
--*/
#include "ast/pb_decl_plugin.h"
-#include "sat/smt/sat_smt.h"
-#include "sat/ba/ba_solver.h"
-#include "sat/ba/ba_internalize.h"
-#include "sat/euf/euf_solver.h"
-#include "sat/sat_solver.h"
#include "tactic/tactic_exception.h"
+#include "sat/sat_solver.h"
+#include "sat/smt/sat_smt.h"
+#include "sat/smt/ba_solver.h"
+#include "sat/smt/ba_internalize.h"
+#include "sat/smt/euf_solver.h"
namespace euf {
+ void solver::updt_params(params_ref const& p) {
+ m_config.updt_params(p);
+ }
+
/**
* retrieve extension that is associated with Boolean variable.
*/
@@ -55,9 +59,10 @@ namespace euf {
auto* ba = alloc(sat::ba_solver);
ba->set_solver(m_solver);
add_extension(pb.get_family_id(), ba);
- auto* bai = alloc(sat::ba_internalize, *ba, s(), m);
+ auto* bai = alloc(sat::ba_internalize, *ba, s(), si, m);
m_id2internalize.setx(pb.get_family_id(), bai, nullptr);
m_internalizers.push_back(bai);
+ m_decompilers.push_back(alloc(sat::ba_decompile, *ba, s(), m));
ba->push_scopes(s().num_scopes());
return ba;
}
@@ -74,12 +79,12 @@ namespace euf {
void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r) {
auto* ext = sat::index_base::to_extension(idx);
if (ext == this)
- get_antecedents(l, *euf_base::from_idx(idx), r);
+ get_antecedents(l, *constraint::from_idx(idx), r);
else
ext->get_antecedents(l, idx, r);
}
- void solver::get_antecedents(literal l, euf_base& j, literal_vector& r) {
+ void solver::get_antecedents(literal l, constraint& j, literal_vector& r) {
m_explain.reset();
euf::enode* n = nullptr;
bool sign = false;
@@ -90,6 +95,8 @@ namespace euf {
sign = l.sign() != p.second;
}
+ // init_ackerman();
+
switch (j.id()) {
case 0:
SASSERT(m_egraph.inconsistent());
@@ -144,6 +151,9 @@ namespace euf {
}
for (euf::enode* eq : m_egraph.new_eqs()) {
bool_var v = m_expr2var.to_bool_var(eq->get_owner());
+ expr* a = nullptr, *b = nullptr;
+ if (s().value(v) == l_false && m_ackerman && m.is_eq(eq->get_owner(), a, b))
+ m_ackerman->cg_conflict_eh(a, b);
s().assign(literal(v, false), sat::justification::mk_ext_justification(s().scope_lvl(), m_eq_idx.to_index()));
}
for (euf::enode* p : m_egraph.new_lits()) {
@@ -152,7 +162,10 @@ namespace euf {
SASSERT(m.is_bool(e));
SASSERT(m.is_true(p->get_root()->get_owner()) || sign);
bool_var v = m_expr2var.to_bool_var(e);
- s().assign(literal(v, sign), sat::justification::mk_ext_justification(s().scope_lvl(), m_lit_idx.to_index()));
+ literal lit(v, sign);
+ if (s().value(lit) == l_false && m_ackerman)
+ m_ackerman->cg_conflict_eh(p->get_owner(), p->get_root()->get_owner());
+ s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), m_lit_idx.to_index()));
}
}
@@ -204,6 +217,8 @@ namespace euf {
void solver::simplify() {
for (auto* e : m_extensions)
e->simplify();
+ if (m_ackerman)
+ m_ackerman->propagate();
}
void solver::clauses_modifed() {
@@ -243,12 +258,14 @@ namespace euf {
m_egraph.collect_statistics(st);
for (auto* e : m_extensions)
e->collect_statistics(st);
+ st.update("euf dynack", m_stats.m_num_dynack);
}
solver* solver::copy_core() {
ast_manager& to = m_translate ? m_translate->to() : m;
atom2bool_var& a2b = m_translate_expr2var ? *m_translate_expr2var : m_expr2var;
- auto* r = alloc(solver, to, a2b);
+ auto* r = alloc(solver, to, a2b, si);
+ r->m_config = m_config;
std::function<void*(void*)> copy_justification = [&](void* x) { return (void*)(r->base_ptr() + ((unsigned*)x - base_ptr())); };
r->m_egraph.copy_from(m_egraph, copy_justification);
return r;
@@ -325,6 +342,23 @@ namespace euf {
return w;
}
+ void solver::init_ackerman() {
+ if (m_ackerman)
+ return;
+ if (m_config.m_dack == DACK_DISABLED)
+ return;
+ m_ackerman = alloc(ackerman, *this, m);
+ std::function<void(expr*,expr*,expr*)> used_eq = [&](expr* a, expr* b, expr* lca) {
+ m_ackerman->used_eq_eh(a, b, lca);
+ };
+ std::function<void(app*,app*)> used_cc = [&](app* a, app* b) {
+ m_ackerman->used_cc_eh(a, b);
+ };
+ m_egraph.set_used_eq(used_eq);
+ m_egraph.set_used_cc(used_cc);
+ }
+
+
sat::th_internalizer* solver::get_internalizer(expr* e) {
if (is_app(e))
return m_id2internalize.get(to_app(e)->get_family_id(), nullptr);
@@ -334,25 +368,19 @@ namespace euf {
}
return nullptr;
}
-
- sat::th_model_builder* solver::get_model_builder(expr* e) {
- if (is_app(e))
- return m_id2model_builder.get(to_app(e)->get_family_id(), nullptr);
- return nullptr;
- }
- sat::literal solver::internalize(sat::sat_internalizer& si, expr* e, bool sign, bool root) {
+ sat::literal solver::internalize(expr* e, bool sign, bool root) {
auto* ext = get_internalizer(e);
if (ext)
- return ext->internalize(si, e, sign, root);
+ return ext->internalize(e, sign, root);
if (!m_true) {
- m_true = visit(si, m.mk_true());
- m_false = visit(si, m.mk_false());
+ m_true = visit(m.mk_true());
+ m_false = visit(m.mk_false());
}
SASSERT(!si.is_bool_op(e));
sat::scoped_stack _sc(m_stack);
unsigned sz = m_stack.size();
- euf::enode* n = visit(si, e);
+ euf::enode* n = visit(e);
while (m_stack.size() > sz) {
loop:
if (!m.inc())
@@ -368,7 +396,7 @@ namespace euf {
while (fr.m_idx < num) {
expr* arg = to_app(e)->get_arg(fr.m_idx);
fr.m_idx++;
- n = visit(si, arg);
+ n = visit(arg);
if (!n)
goto loop;
}
@@ -376,13 +404,13 @@ namespace euf {
for (unsigned i = 0; i < num; ++i)
m_args.push_back(m_egraph.find(to_app(e)->get_arg(i)));
n = m_egraph.mk(e, num, m_args.c_ptr());
- attach_bool_var(si, n);
+ attach_bool_var(n);
}
SASSERT(m_egraph.find(e));
return literal(m_expr2var.to_bool_var(e), sign);
}
- euf::enode* solver::visit(sat::sat_internalizer& si, expr* e) {
+ euf::enode* solver::visit(expr* e) {
euf::enode* n = m_egraph.find(e);
if (n)
return n;
@@ -399,11 +427,11 @@ namespace euf {
return nullptr;
}
n = m_egraph.mk(e, 0, nullptr);
- attach_bool_var(si, n);
+ attach_bool_var(n);
return n;
}
- void solver::attach_bool_var(sat::sat_internalizer& si, euf::enode* n) {
+ void solver::attach_bool_var(euf::enode* n) {
expr* e = n->get_owner();
if (m.is_bool(e)) {
sat::bool_var v = si.add_bool_var(e);
@@ -420,6 +448,18 @@ namespace euf {
m_bool_var_trail.push_back(v);
}
+ bool solver::to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) {
+ for (auto* th : m_decompilers) {
+ if (!th->to_formulas(l2e, fmls))
+ return false;
+ }
+ for (euf::enode* n : m_egraph.nodes()) {
+ if (!n->is_root())
+ fmls.push_back(m.mk_eq(n->get_owner(), n->get_root()->get_owner()));
+ }
+ return true;
+ }
+
bool solver::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) {
if (m_true)
diff --git a/src/sat/euf/euf_solver.h b/src/sat/smt/euf_solver.h
similarity index 55%
rename from src/sat/euf/euf_solver.h
rename to src/sat/smt/euf_solver.h
index f2aa26059..537a0b665 100644
--- a/src/sat/euf/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -17,12 +17,14 @@ Author:
#pragma once
#include "util/scoped_ptr_vector.h"
-#include "sat/sat_extension.h"
-#include "ast/euf/euf_egraph.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 "tactic/model_converter.h"
+#include "sat/smt/euf_ackerman.h"
namespace euf {
typedef sat::literal literal;
@@ -31,66 +33,89 @@ namespace euf {
typedef sat::literal_vector literal_vector;
typedef sat::bool_var bool_var;
- class euf_base : public sat::index_base {
+ class constraint : public sat::index_base {
unsigned m_id;
public:
- euf_base(sat::extension* e, unsigned id) :
+ constraint(sat::extension* e, unsigned id) :
index_base(e), m_id(id)
{}
unsigned id() const { return m_id; }
- static euf_base* from_idx(size_t z) { return reinterpret_cast<euf_base*>(z); }
+ static constraint* from_idx(size_t z) { return reinterpret_cast<constraint*>(z); }
};
- class solver : public sat::extension, public sat::th_internalizer {
- ast_manager& m;
- atom2bool_var& m_expr2var;
- euf::egraph m_egraph;
- sat::solver* m_solver;
- sat::lookahead* m_lookahead;
- ast_translation* m_translate;
- atom2bool_var* m_translate_expr2var;
+ class solver : public sat::extension, public sat::th_internalizer, public sat::th_decompile {
+ typedef top_sort<euf::enode> deps_t;
+ friend class ackerman;
+ struct stats {
+ unsigned m_num_dynack;
+ stats() { reset(); }
+ void reset() { memset(this, 0, sizeof(*this)); }
+ };
- euf::enode* m_true;
- euf::enode* m_false;
- svector<euf::enode_bool_pair> m_var2node;
- 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;
- unsigned_vector m_bool_var_lim;
- scoped_ptr_vector<sat::extension> m_extensions;
- ptr_vector<sat::extension> m_id2extension;
- ptr_vector<sat::th_internalizer> m_id2internalize;
- scoped_ptr_vector<sat::th_internalizer> m_internalizers;
- scoped_ptr_vector<sat::th_model_builder> m_model_builders;
- ptr_vector<sat::th_model_builder> m_id2model_builder;
- euf_base m_conflict_idx, m_eq_idx, m_lit_idx;
+ ast_manager& m;
+ atom2bool_var& m_expr2var;
+ sat::sat_internalizer& si;
+ smt_params m_config;
+ euf::egraph m_egraph;
+ stats m_stats;
+ sat::solver* m_solver { nullptr };
+ sat::lookahead* m_lookahead { nullptr };
+ ast_translation* m_translate { nullptr };
+ atom2bool_var* m_translate_expr2var { nullptr };
+ scoped_ptr<ackerman> m_ackerman;
+
+ euf::enode* m_true { nullptr };
+ euf::enode* m_false { nullptr };
+ svector<euf::enode_bool_pair> m_var2node;
+ 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;
+ unsigned_vector m_bool_var_lim;
+ scoped_ptr_vector<sat::extension> m_extensions;
+ ptr_vector<sat::extension> m_id2extension;
+ ptr_vector<sat::th_internalizer> m_id2internalize;
+ scoped_ptr_vector<sat::th_internalizer> m_internalizers;
+ scoped_ptr_vector<sat::th_model_builder> m_model_builders;
+ ptr_vector<sat::th_model_builder> m_id2model_builder;
+ scoped_ptr_vector<sat::th_decompile> m_decompilers;
+ constraint m_conflict_idx, m_eq_idx, m_lit_idx;
sat::solver& s() { return *m_solver; }
unsigned * base_ptr() { return reinterpret_cast<unsigned*>(this); }
- euf::enode* visit(sat::sat_internalizer& si, expr* e);
- void attach_bool_var(sat::sat_internalizer& si, euf::enode* n);
+
+ // internalization
+ sat::th_internalizer* get_internalizer(expr* e);
+ 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);
solver* copy_core();
+
+ // extensions
sat::extension* get_extension(sat::bool_var v);
sat::extension* get_extension(expr* e);
void add_extension(family_id fid, sat::extension* e);
- sat::th_internalizer* get_internalizer(expr* e);
+ void init_ackerman();
- sat::th_model_builder* get_model_builder(expr* e);
+ // model building
+ bool include_func_interp(func_decl* f) const;
+ sat::th_model_builder* get_model_builder(expr* e) const;
+ sat::th_model_builder* get_model_builder(func_decl* f) const;
+ void register_macros(model& mdl);
+ void dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref const& mdl);
+ void collect_dependencies(deps_t& deps);
+ void values2model(deps_t const& deps, expr_ref_vector const& values, model_ref& mdl);
+ // solving
void propagate();
- void get_antecedents(literal l, euf_base& j, literal_vector& r);
-
- void dependencies2values(sat::th_dependencies& deps, expr_ref_vector& values);
- void collect_dependencies(sat::th_dependencies& deps);
- void sort_dependencies(sat::th_dependencies& deps);
+ void get_antecedents(literal l, constraint& j, literal_vector& r);
public:
- solver(ast_manager& m, atom2bool_var& expr2var):
+ solver(ast_manager& m, atom2bool_var& expr2var, sat::sat_internalizer& si, params_ref const& p = params_ref()):
m(m),
m_expr2var(expr2var),
+ si(si),
m_egraph(m),
m_solver(nullptr),
m_lookahead(nullptr),
@@ -101,9 +126,13 @@ namespace euf {
m_conflict_idx(this, 0),
m_eq_idx(this, 1),
m_lit_idx(this, 2)
- {}
+ {
+ updt_params(p);
+ }
+
~solver() override {}
+ void updt_params(params_ref const& p);
void set_solver(sat::solver* s) override { m_solver = s; }
void set_lookahead(sat::lookahead* s) override { m_lookahead = s; }
struct scoped_set_translate {
@@ -143,11 +172,9 @@ namespace euf {
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;
-
- sat::literal internalize(sat::sat_internalizer& si, expr* e, bool sign, bool root) override;
- model_converter* get_model();
-
-
-
+ bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls);
+ sat::literal internalize(expr* e, bool sign, bool root) override;
+ void update_model(model_ref& mdl);
+
};
};
diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
deleted file mode 100644
index 22c59fd2e..000000000
--- a/src/sat/smt/sat_th.cpp
+++ /dev/null
@@ -1,37 +0,0 @@
-/*++
-Copyright (c) 2020 Microsoft Corporation
-
-Module Name:
-
- sat_th.cpp
-
-Abstract:
-
- Theory plugins
-
-Author:
-
- Nikolaj Bjorner (nbjorner) 2020-08-25
-
---*/
-#include "sat/smt/sat_th.h"
-#include "util/top_sort.h"
-
-namespace sat {
-
- /*
- * \brief add dependency: dst depends on src.
- */
- void th_dependencies::add(euf::enode* src, euf::enode* dst) {
-
- }
-
- /*
- * \brief sort dependencies.
- */
- void th_dependencies::sort() {
- top_sort<euf::enode> top;
-
- }
-
-}
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index 9c0f92dd7..1497ee6b5 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -16,33 +16,26 @@ Author:
--*/
#pragma once
+#include "util/top_sort.h"
#include "sat/smt/sat_smt.h"
#include "ast/euf/euf_egraph.h"
namespace sat {
-
- class th_dependencies {
- public:
- th_dependencies() {}
- euf::enode * const* begin() const { return nullptr; }
- euf::enode * const* end() const { return nullptr; }
-
- /*
- * \brief add dependency: dst depends on src.
- */
- void add(euf::enode* src, euf::enode* dst);
-
- /*
- * \brief sort dependencies.
- */
- void sort();
- };
-
class th_internalizer {
public:
- virtual literal internalize(sat_internalizer& si, expr* e, bool sign, bool root) = 0;
virtual ~th_internalizer() {}
+
+ virtual literal internalize(expr* e, bool sign, bool root) = 0;
+
+
+ };
+
+ class th_decompile {
+ public:
+ virtual ~th_decompile() {}
+
+ virtual bool to_formulas(std::function<expr_ref(sat::literal)>& lit2expr, expr_ref_vector& fmls) = 0;
};
class th_model_builder {
@@ -59,7 +52,12 @@ namespace sat {
/**
\brief compute dependencies for node n
*/
- virtual void add_dep(euf::enode* n, th_dependencies& dep) = 0;
+ virtual void add_dep(euf::enode* n, top_sort<euf::enode>& 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/CMakeLists.txt b/src/sat/tactic/CMakeLists.txt
index 434fe854c..d1924d679 100644
--- a/src/sat/tactic/CMakeLists.txt
+++ b/src/sat/tactic/CMakeLists.txt
@@ -7,8 +7,6 @@ z3_add_component(sat_tactic
tactic
solver
sat_smt
- sat_ba
- sat_euf
TACTIC_HEADERS
sat_tactic.h
)
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 8dcf2f0ee..c1c3343b1 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -35,9 +35,9 @@ Notes:
#include "ast/for_each_expr.h"
#include "sat/tactic/goal2sat.h"
#include "sat/sat_cut_simplifier.h"
-#include "sat/ba/ba_internalize.h"
-#include "sat/ba/ba_solver.h"
-#include "sat/euf/euf_solver.h"
+#include "sat/smt/ba_internalize.h"
+#include "sat/smt/ba_solver.h"
+#include "sat/smt/euf_solver.h"
#include "model/model_evaluator.h"
#include "model/model_v2_pp.h"
#include "tactic/tactic.h"
@@ -71,7 +71,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
bool m_default_external;
bool m_xor_solver;
bool m_euf;
- bool m_is_lemma;
imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
@@ -83,8 +82,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_dep2asm(dep2asm),
m_trail(m),
m_interpreted_atoms(m),
- m_default_external(default_external),
- m_is_lemma(false) {
+ m_default_external(default_external) {
updt_params(p);
m_true = sat::null_literal;
m_aig = s.get_cut_simplifier();
@@ -107,21 +105,19 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_solver.add_clause(1, &l, false);
}
- void set_lemma_mode(bool f) { m_is_lemma = f; }
-
void mk_clause(sat::literal l1, sat::literal l2) override {
TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";);
- m_solver.add_clause(l1, l2, m_is_lemma);
+ m_solver.add_clause(l1, l2, false);
}
void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3, bool is_lemma = false) override {
TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
- m_solver.add_clause(l1, l2, l3, m_is_lemma || is_lemma);
+ m_solver.add_clause(l1, l2, l3, is_lemma);
}
void mk_clause(unsigned num, sat::literal * lits) {
TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";);
- m_solver.add_clause(num, lits, m_is_lemma);
+ m_solver.add_clause(num, lits, false);
}
sat::literal mk_true() {
@@ -444,7 +440,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
sat::extension* ext = m_solver.get_extension();
euf::solver* euf = nullptr;
if (!ext) {
- euf = alloc(euf::solver, m, m_map);
+ euf = alloc(euf::solver, m, m_map, *this);
m_solver.set_extension(euf);
for (unsigned i = m_solver.num_scopes(); i-- > 0; )
euf->push();
@@ -454,7 +450,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
if (!euf)
throw default_exception("cannot convert to euf");
- sat::literal lit = euf->internalize(*this, e, sign, root);
+ sat::literal lit = euf->internalize(e, sign, root);
if (root)
m_result_stack.reset();
if (lit == sat::null_literal)
@@ -478,8 +474,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
if (!ba)
throw default_exception("cannot convert to pb");
- sat::ba_internalize internalize(*ba, m_solver, m);
- sat::literal lit = internalize.internalize(*this, t, sign, root);
+ sat::ba_internalize internalize(*ba, m_solver, *this, m);
+ sat::literal lit = internalize.internalize(t, sign, root);
if (root)
m_result_stack.reset();
else
@@ -735,7 +731,13 @@ bool goal2sat::has_unsupported_bool(goal const & g) {
return test<unsupported_bool_proc>(g);
}
-goal2sat::goal2sat():m_imp(nullptr), m_interpreted_atoms(nullptr) {
+goal2sat::goal2sat():
+ m_imp(nullptr),
+ m_interpreted_atoms(nullptr) {
+}
+
+goal2sat::~goal2sat() {
+ dealloc(m_imp);
}
void goal2sat::collect_param_descrs(param_descrs & r) {
@@ -743,25 +745,18 @@ void goal2sat::collect_param_descrs(param_descrs & r) {
r.insert("ite_extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas");
}
-struct goal2sat::scoped_set_imp {
- goal2sat * m_owner;
- scoped_set_imp(goal2sat * o, goal2sat::imp * i):m_owner(o) {
- m_owner->m_imp = i;
- }
- ~scoped_set_imp() {
- m_owner->m_imp = nullptr;
- }
-};
-
-void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external, bool is_lemma) {
- imp proc(g.m(), p, t, m, dep2asm, default_external);
- scoped_set_imp set(this, &proc);
- proc.set_lemma_mode(is_lemma);
- proc(g);
- dealloc(m_interpreted_atoms);
+void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) {
+ if (!m_imp)
+ m_imp = alloc(imp, g.m(), p, t, m, dep2asm, default_external);
+
+ (*m_imp)(g);
m_interpreted_atoms = alloc(expr_ref_vector, g.m());
- m_interpreted_atoms->append(proc.m_interpreted_atoms);
+ m_interpreted_atoms->append(m_imp->m_interpreted_atoms);
+ if (!t.get_extension()) {
+ dealloc(m_imp);
+ m_imp = nullptr;
+ }
}
void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) {
@@ -948,50 +943,6 @@ struct sat2goal::imp {
return m_lit2expr.get(l.index());
}
- void assert_pb(ref<mc>& mc, goal& r, sat::ba_solver::pb const& p) {
- pb_util pb(m);
- ptr_buffer<expr> lits;
- vector<rational> coeffs;
- for (auto const& wl : p) {
- lits.push_back(lit2expr(mc, wl.second));
- coeffs.push_back(rational(wl.first));
- }
- rational k(p.k());
- expr_ref fml(pb.mk_ge(p.size(), coeffs.c_ptr(), lits.c_ptr(), k), m);
-
- if (p.lit() != sat::null_literal) {
- fml = m.mk_eq(lit2expr(mc, p.lit()), fml);
- }
- r.assert_expr(fml);
- }
-
- void assert_card(ref<mc>& mc, goal& r, sat::ba_solver::card const& c) {
- pb_util pb(m);
- ptr_buffer<expr> lits;
- for (sat::literal l : c) {
- lits.push_back(lit2expr(mc, l));
- }
- expr_ref fml(pb.mk_at_least_k(c.size(), lits.c_ptr(), c.k()), m);
-
- if (c.lit() != sat::null_literal) {
- fml = m.mk_eq(lit2expr(mc, c.lit()), fml);
- }
- r.assert_expr(fml);
- }
-
- void assert_xor(ref<mc>& mc, goal & r, sat::ba_solver::xr const& x) {
- ptr_buffer<expr> lits;
- for (sat::literal l : x) {
- lits.push_back(lit2expr(mc, l));
- }
- expr_ref fml(m.mk_xor(x.size(), lits.c_ptr()), m);
-
- if (x.lit() != sat::null_literal) {
- fml = m.mk_eq(lit2expr(mc, x.lit()), fml);
- }
- r.assert_expr(fml);
- }
-
void assert_clauses(ref<mc>& mc, sat::solver_core const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
ptr_buffer<expr> lits;
unsigned small_lbd = 3; // s.get_config().m_gc_small_lbd;
@@ -1008,10 +959,6 @@ struct sat2goal::imp {
}
}
- sat::ba_solver* get_ba_solver(sat::solver_core const& s) {
- return dynamic_cast<sat::ba_solver*>(s.get_extension());
- }
-
void operator()(sat::solver_core & s, atom2bool_var const & map, goal & r, ref<mc> & mc) {
if (s.at_base_lvl() && s.inconsistent()) {
r.assert_expr(m.mk_false());
@@ -1039,21 +986,21 @@ struct sat2goal::imp {
// collect clauses
assert_clauses(mc, s, s.clauses(), r, true);
- sat::ba_solver* ext = get_ba_solver(s);
+ auto* ext = s.get_extension();
if (ext) {
- for (auto* c : ext->constraints()) {
- switch (c->tag()) {
- case sat::ba_solver::card_t:
- assert_card(mc, r, c->to_card());
- break;
- case sat::ba_solver::pb_t:
- assert_pb(mc, r, c->to_pb());
- break;
- case sat::ba_solver::xr_t:
- assert_xor(mc, r, c->to_xr());
- break;
- }
+ std::function<expr_ref(sat::literal)> l2e = [&](sat::literal lit) {
+ return expr_ref(lit2expr(mc, lit), m);
+ };
+ expr_ref_vector fmls(m);
+ sat::ba_solver* ba = dynamic_cast<sat::ba_solver*>(ext);
+ if (ba) {
+ sat::ba_decompile decompile(*ba, s, m);
+ decompile.to_formulas(l2e, fmls);
}
+ else
+ dynamic_cast<euf::solver*>(ext)->to_formulas(l2e, fmls);
+ for (expr* f : fmls)
+ r.assert_expr(f);
}
}
diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h
index a4c9b90b0..40ccb2e9c 100644
--- a/src/sat/tactic/goal2sat.h
+++ b/src/sat/tactic/goal2sat.h
@@ -38,12 +38,11 @@ Notes:
class goal2sat {
struct imp;
imp * m_imp;
- struct scoped_set_imp;
- expr_ref_vector* m_interpreted_atoms;
+ scoped_ptr<expr_ref_vector> m_interpreted_atoms;
public:
goal2sat();
- ~goal2sat() { dealloc(m_interpreted_atoms); }
+ ~goal2sat();
typedef obj_map<expr, sat::literal> dep2asm_map;
@@ -61,7 +60,7 @@ public:
\warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory).
*/
- void operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false, bool is_lemma = false);
+ 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_atoms(expr_ref_vector& atoms);
diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp
index 3b82fbd52..9bc723f82 100644
--- a/src/shell/dimacs_frontend.cpp
+++ b/src/shell/dimacs_frontend.cpp
@@ -25,7 +25,6 @@ Revision History:
#include "sat/dimacs.h"
#include "sat/sat_params.hpp"
#include "sat/sat_solver.h"
-#include "sat/ba/ba_solver.h"
#include "sat/tactic/goal2sat.h"
#include "ast/reg_decl_plugins.h"
#include "tactic/tactic.h"
diff --git a/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt
index 4beec80f0..31b9b203d 100644
--- a/src/smt/params/CMakeLists.txt
+++ b/src/smt/params/CMakeLists.txt
@@ -11,8 +11,6 @@ z3_add_component(smt_params
theory_seq_params.cpp
theory_str_params.cpp
COMPONENT_DEPENDENCIES
- ast
- bit_blaster
pattern
PYG_FILES
smt_params_helper.pyg
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 01d83403c..844a9a9b6 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -18,7 +18,6 @@ Revision History:
--*/
#pragma once
-#include "ast/ast.h"
#include "smt/params/dyn_ack_params.h"
#include "smt/params/qi_params.h"
#include "smt/params/theory_arith_params.h"
diff --git a/src/smt/qi_queue.h b/src/smt/qi_queue.h
index e79b0cfb5..50ba2e1b9 100644
--- a/src/smt/qi_queue.h
+++ b/src/smt/qi_queue.h
@@ -22,8 +22,8 @@ Revision History:
#include "smt/smt_quantifier_stat.h"
#include "smt/smt_checker.h"
#include "smt/smt_quantifier.h"
-#include "smt/params/qi_params.h"
#include "smt/fingerprints.h"
+#include "smt/params/qi_params.h"
#include "parsers/util/cost_parser.h"
#include "smt/cost_evaluator.h"
#include "smt/cached_var_subst.h"
diff --git a/src/util/top_sort.h b/src/util/top_sort.h
index ec9ee4668..0e4f97af1 100644
--- a/src/util/top_sort.h
+++ b/src/util/top_sort.h
@@ -18,11 +18,11 @@ Revision History:
#pragma once
-#include "util/obj_hashtable.h"
-#include "util/vector.h"
#include<algorithm>
#include<type_traits>
#include<memory.h>
+#include "util/obj_hashtable.h"
+#include "util/vector.h"
#include "util/memory_manager.h"
@@ -52,12 +52,13 @@ class top_sort {
else {
m_dfs_num.insert(f, m_next_preorder++);
m_stack_S.push_back(f);
- m_stack_P.push_back(f);
- for (T* g : *m_deps[f]) {
- traverse(g);
- }
- if (f == m_stack_P.back()) {
-
+ m_stack_P.push_back(f);
+ if (m_deps[f]) {
+ for (T* g : *m_deps[f]) {
+ traverse(g);
+ }
+ }
+ if (f == m_stack_P.back()) {
p_id = m_top_sorted.size();
T* s_f;
do {
@@ -94,7 +95,16 @@ public:
m_deps.insert(t, s);
}
- ptr_vector<T> const& top_sorted() { return m_top_sorted; }
+ void add(T* t, T* s) {
+ T_set* tb = nullptr;
+ if (!m_deps.find(t, tb)) {
+ tb = alloc(T_set);
+ insert(s, tb);
+ }
+ t->insert(s);
+ }
+
+ ptr_vector<T> const& top_sorted() const { return m_top_sorted; }
obj_map<T, unsigned> const& partition_ids() const { return m_partition_id; }