#include "qe/qe.h"
#include "smt/smt_theory.h"
#include "ast/bv_decl_plugin.h"
#include "smt/smt_context.h"
#include "smt/theory_bv.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_smt_pp.h"
#include "ast/expr_abstract.h"
#include "ast/rewriter/var_subst.h"
#include "ast/for_each_expr.h"
#include "ast/dl_decl_plugin.h"
#include "qe/nlarith_util.h"
#include "ast/rewriter/expr_replacer.h"
#include "ast/rewriter/factor_rewriter.h"
#include "ast/expr_functors.h"
#include "ast/rewriter/quant_hoist.h"
#include "ast/rewriter/bool_rewriter.h"
#include "ast/rewriter/th_rewriter.h"
#include "smt/smt_kernel.h"
#include "model/model_evaluator.h"
#include "ast/has_free_vars.h"
#include "ast/rewriter/rewriter_def.h"
#include "tactic/tactical.h"
#include "model/model_v2_pp.h"
#include "util/obj_hashtable.h"
namespace qe {
class conjunctions {
ast_manager& m;
ptr_vector<qe_solver_plugin> m_plugins;
public:
conjunctions(ast_manager& m) : m(m) {}
void add_plugin(qe_solver_plugin* p) {
family_id fid = p->get_family_id();
if (static_cast<family_id>(m_plugins.size()) <= fid) {
m_plugins.resize(fid + 1);
}
m_plugins[fid] = p;
}
void get_partition(
expr* fml,
unsigned num_vars,
app* const* vars,
expr_ref& fml_closed, expr_ref& fml_mixed, expr_ref& fml_open )
{
expr_ref_vector conjs(m);
ast_mark visited;
ast_mark contains_var;
ast_mark contains_uf;
ptr_vector<expr> todo;
ptr_vector<expr> conjs_closed, conjs_mixed, conjs_open;
flatten_and(fml, conjs);
for (unsigned i = 0; i < conjs.size(); ++i) {
todo.push_back(conjs[i].get());
}
while (!todo.empty()) {
expr* e = todo.back();
if (visited.is_marked(e)) {
todo.pop_back();
continue;
}
if (is_var(to_app(e), num_vars, vars)) {
contains_var.mark(e, true);
visited.mark(e, true);
todo.pop_back();
continue;
}
if (!is_app(e)) {
visited.mark(e, true);
todo.pop_back();
continue;
}
bool all_visited = true;
app* a = to_app(e);
if (is_uninterpreted(a)) {
contains_uf.mark(e, true);
}
for (unsigned i = 0; i < a->get_num_args(); ++i) {
expr* arg = a->get_arg(i);
if (!visited.is_marked(arg)) {
all_visited = false;
todo.push_back(arg);
}
else {
if (contains_var.is_marked(arg)) {
contains_var.mark(e, true);
}
if (contains_uf.is_marked(arg)) {
contains_uf.mark(e, true);
}
}
}
if (all_visited) {
todo.pop_back();
visited.mark(e, true);
}
}
for (expr* e : conjs) {
bool cv = contains_var.is_marked(e);
bool cu = contains_uf.is_marked(e);
if (cv && cu) {
conjs_mixed.push_back(e);
conjs_open.push_back(e);
}
else if (cv) {
conjs_open.push_back(e);
}
else {
conjs_closed.push_back(e);
}
}
bool_rewriter rewriter(m);
rewriter.mk_and(conjs_closed.size(), conjs_closed.data(), fml_closed);
rewriter.mk_and(conjs_mixed.size(), conjs_mixed.data(), fml_mixed);
rewriter.mk_and(conjs_open.size(), conjs_open.data(), fml_open);
TRACE(qe,
tout << "closed\n" << mk_ismt2_pp(fml_closed, m) << "\n";
tout << "open\n" << mk_ismt2_pp(fml_open, m) << "\n";
tout << "mixed\n" << mk_ismt2_pp(fml_mixed, m) << "\n";
);
}
bool partition_vars(
unsigned num_vars,
contains_app** vars,
unsigned num_args,
expr* const* args,
vector<unsigned_vector>& partition
)
{
unsigned_vector contains_index;
unsigned_vector non_shared;
unsigned_vector non_shared_vars;
union_find_default_ctx df;
union_find<union_find_default_ctx> uf(df);
partition.reset();
for (unsigned v = 0; v < num_vars; ++v) {
contains_app& contains_x = *vars[v];
contains_index.reset();
for (unsigned i = 0; i < num_args; ++i) {
if (contains_x(args[i])) {
contains_index.push_back(i);
TRACE(qe_verbose, tout << "var " << v << " in " << i << "\n";);
}
}
if (2*contains_index.size() > num_args) {
if (partition.empty()) {
partition.push_back(unsigned_vector());
}
partition.back().push_back(v);
TRACE(qe_verbose, tout << "majority " << v << "\n";);
continue;
}
unsigned var_x = uf.mk_var();
SASSERT(var_x == non_shared_vars.size());
non_shared_vars.push_back(v);
for (unsigned i = 0; i < contains_index.size(); ++i) {
unsigned idx = contains_index[i];
if (non_shared.size() <= idx) {
non_shared.resize(idx+1,UINT_MAX);
}
unsigned var_y = non_shared[idx];
if (var_y != UINT_MAX) {
uf.merge(var_x, var_y);
}
else {
non_shared[idx] = var_x;
}
}
}
if (non_shared_vars.empty()) {
return false;
}
unsigned root0 = uf.find(0);
bool is_partitioned = false;
for (unsigned idx = 1; !is_partitioned && idx < non_shared_vars.size(); ++idx) {
is_partitioned = (uf.find(idx) != root0);
}
if (!is_partitioned) {
return false;
}
unsigned_vector roots;
if (!partition.empty()) {
roots.push_back(UINT_MAX);
}
for (unsigned idx = 0; idx < non_shared_vars.size(); ++idx) {
unsigned x = non_shared_vars[idx];
unsigned r = non_shared_vars[uf.find(idx)];
TRACE(qe_verbose, tout << "x: " << x << " r: " << r << "\n";);
bool found = false;
for (unsigned i = 0; !found && i < roots.size(); ++i) {
if (roots[i] == r) {
found = true;
partition[i].push_back(x);
}
}
if (!found) {
roots.push_back(r);
partition.push_back(unsigned_vector());
partition.back().push_back(x);
}
}
TRACE(qe_verbose,
for (unsigned i = 0; i < partition.size(); ++i) {
for (unsigned j = 0; j < partition[i].size(); ++j) {
tout << " " << mk_ismt2_pp(vars[partition[i][j]]->x(), m);;
}
tout << "\n";
});
SASSERT(partition.size() != 1);
SASSERT(!partition.empty() || roots.size() > 1);
return true;
}
private:
bool is_var(app* x, unsigned num_vars, app* const* vars) {
for (unsigned i = 0; i < num_vars; ++i) {
if (vars[i] == x) {
return true;
}
}
return false;
}
bool is_uninterpreted(app* a) {
family_id fid = a->get_family_id();
if (null_family_id == fid) {
return true;
}
if (static_cast<unsigned>(fid) >= m_plugins.size()) {
return true;
}
qe_solver_plugin* p = m_plugins[fid];
if (!p) {
return true;
}
return p->is_uninterpreted(a);
}
};
conj_enum::conj_enum(ast_manager& m, expr* e): m(m), m_conjs(m) {
flatten_and(e, m_conjs);
}
void conj_enum::extract_equalities(expr_ref_vector& eqs) {
arith_util arith(m);
obj_hashtable<expr> leqs;
expr_ref_vector trail(m);
expr_ref tmp1(m), tmp2(m);
expr *a0, *a1;
eqs.reset();
conj_enum::iterator it = begin();
for (; it != end(); ++it) {
expr* e = *it;
if (m.is_eq(e, a0, a1) && (arith.is_int(a0) || arith.is_real(a0))) {
tmp1 = arith.mk_sub(a0, a1);
eqs.push_back(tmp1);
}
else if (arith.is_le(e, a0, a1) || arith.is_ge(e, a1, a0)) {
tmp1 = arith.mk_sub(a0, a1);
tmp2 = arith.mk_sub(a1, a0);
if (leqs.contains(tmp2)) {
eqs.push_back(tmp1);
TRACE(qe, tout << "found: " << mk_ismt2_pp(tmp1, m) << "\n";);
}
else {
trail.push_back(tmp1);
leqs.insert(tmp1);
TRACE(qe_verbose, tout << "insert: " << mk_ismt2_pp(tmp1, m) << "\n";);
}
}
else {
}
}
}
class lift_ite {
ast_manager& m;
i_expr_pred& m_is_relevant;
th_rewriter m_rewriter;
scoped_ptr<expr_replacer> m_replace;
public:
lift_ite(ast_manager& m, i_expr_pred& is_relevant) :
m(m), m_is_relevant(is_relevant), m_rewriter(m), m_replace(mk_default_expr_replacer(m, false)) {}
bool operator()(expr* fml, expr_ref& result) {
if (m.is_ite(fml)) {
result = fml;
return true;
}
app* ite;
if (find_ite(fml, ite)) {
expr* cond = nullptr, *th = nullptr, *el = nullptr;
VERIFY(m.is_ite(ite, cond, th, el));
expr_ref tmp1(fml, m), tmp2(fml, m);
m_replace->apply_substitution(ite, th, tmp1);
m_replace->apply_substitution(ite, el, tmp2);
result = m.mk_ite(cond, tmp1, tmp2);
m_rewriter(result);
return result != fml;
}
else {
return false;
}
}
private:
bool find_ite(expr* e, app*& ite) {
ptr_vector<expr> todo;
ast_mark visited;
todo.push_back(e);
while(!todo.empty()) {
e = todo.back();
todo.pop_back();
if (visited.is_marked(e)) {
continue;
}
visited.mark(e, true);
if (!m_is_relevant(e)) {
continue;
}
if (m.is_ite(e)) {
ite = to_app(e);
return true;
}
if (is_app(e)) {
app* a = to_app(e);
unsigned num_args = a->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
todo.push_back(a->get_arg(i));
}
}
}
return false;
}
};
class nnf {
ast_manager& m;
i_expr_pred& m_is_relevant;
lift_ite m_lift_ite;
obj_map<expr, expr*> m_pos, m_neg; expr_ref_vector m_trail; expr_ref_vector m_args;
ptr_vector<expr> m_todo; bool_vector m_pols; bool_rewriter m_rewriter;
public:
nnf(ast_manager& m, i_expr_pred& is_relevant):
m(m),
m_is_relevant(is_relevant),
m_lift_ite(m, is_relevant),
m_trail(m),
m_args(m),
m_rewriter(m) {}
void operator()(expr_ref& fml) {
reset();
get_nnf(fml, true);
}
void reset() {
m_todo.reset();
m_trail.reset();
m_pols.reset();
m_pos.reset();
m_neg.reset();
}
private:
bool contains(expr* e, bool p) {
return p?m_pos.contains(e):m_neg.contains(e);
}
expr* lookup(expr* e, bool p) {
expr* r = nullptr;
if (p && m_pos.find(e, r)) {
return r;
}
if (!p && m_neg.find(e, r)) {
return r;
}
m_todo.push_back(e);
m_pols.push_back(p);
return nullptr;
}
void insert(expr* e, bool p, expr* r) {
if (p) {
m_pos.insert(e, r);
}
else {
m_neg.insert(e, r);
}
TRACE(nnf,
tout << mk_ismt2_pp(e, m) << " " << p << "\n";
tout << mk_ismt2_pp(r, m) << "\n";);
m_trail.push_back(r);
}
void pop() {
m_todo.pop_back();
m_pols.pop_back();
}
void nnf_iff(app* a, bool p) {
SASSERT(m.is_iff(a) || m.is_xor(a) || m.is_eq(a));
expr* a0 = a->get_arg(0);
expr* a1 = a->get_arg(1);
expr* r1 = lookup(a0, true);
expr* r2 = lookup(a0, false);
expr* p1 = lookup(a1, true);
expr* p2 = lookup(a1, false);
if (r1 && r2 && p1 && p2) {
expr_ref tmp1(m), tmp2(m), tmp(m);
pop();
if (p) {
m_rewriter.mk_and(r1, p1, tmp1);
m_rewriter.mk_and(r2, p2, tmp2);
m_rewriter.mk_or(tmp1, tmp2, tmp);
}
else {
m_rewriter.mk_or(r1, p1, tmp1);
m_rewriter.mk_or(r2, p2, tmp2);
m_rewriter.mk_and(tmp1, tmp2, tmp);
}
insert(a, p, tmp);
}
}
void nnf_ite(app* a, bool p) {
SASSERT(m.is_ite(a));
expr* r1 = lookup(a->get_arg(0), true);
expr* r2 = lookup(a->get_arg(0), false);
expr* th = lookup(a->get_arg(1), p);
expr* el = lookup(a->get_arg(2), p);
if (r1 && r2 && th && el) {
expr_ref tmp1(m), tmp2(m), tmp(m);
pop();
m_rewriter.mk_and(r1, th, tmp1);
m_rewriter.mk_and(r2, el, tmp2);
m_rewriter.mk_or(tmp1, tmp2, tmp);
TRACE(nnf,
tout << mk_ismt2_pp(a, m) << "\n";
tout << mk_ismt2_pp(tmp, m) << "\n";);
insert(a, p, tmp);
}
}
void nnf_implies(app* a, bool p) {
SASSERT(m.is_implies(a));
expr* r1 = lookup(a->get_arg(0), !p);
expr* r2 = lookup(a->get_arg(1), p);
if (r1 && r2) {
expr_ref tmp(m);
if (p) {
m_rewriter.mk_or(r1, r2, tmp);
}
else {
m_rewriter.mk_and(r1, r2, tmp);
}
insert(a, p, tmp);
}
}
void nnf_not(app* a, bool p) {
SASSERT(m.is_not(a));
expr* arg = a->get_arg(0);
expr* e = lookup(arg, !p);
if (e) {
insert(a, p, e);
}
}
void nnf_and_or(bool is_and, app* a, bool p) {
m_args.reset();
expr_ref tmp(m);
bool visited = true;
for (expr* arg : *a) {
expr* r = lookup(arg, p);
if (r) {
m_args.push_back(r);
}
else {
visited = false;
}
}
if (visited) {
pop();
if (p == is_and)
tmp = mk_and(m_args);
else
tmp = mk_or(m_args);
insert(a, p, tmp);
}
}
bool get_nnf(expr_ref& fml, bool p0) {
TRACE(nnf, tout << mk_ismt2_pp(fml.get(), m) << "\n";);
bool p = p0;
unsigned sz = m_todo.size();
expr_ref tmp(m);
expr* e = lookup(fml, p);
if (e) {
fml = e;
return true;
}
m_trail.push_back(fml);
while (sz < m_todo.size()) {
e = m_todo.back();
p = m_pols.back();
if (!m_is_relevant(e)) {
pop();
insert(e, p, p?e:mk_not(m, e));
continue;
}
if (!is_app(e)) {
return false;
}
if (contains(e, p)) {
pop();
continue;
}
app* a = to_app(e);
if (m.is_and(e) || m.is_or(e)) {
nnf_and_or(m.is_and(a), a, p);
}
else if (m.is_not(a)) {
nnf_not(a, p);
}
else if (m.is_ite(a)) {
nnf_ite(a, p);
}
else if (m.is_iff(a)) {
nnf_iff(a, p);
}
else if (m.is_xor(a)) {
nnf_iff(a, !p);
}
else if (m.is_implies(a)) {
nnf_implies(a, p);
}
else if (m_lift_ite(e, tmp)) {
if (!get_nnf(tmp, p)) {
return false;
}
pop();
insert(e, p, tmp);
}
else {
pop();
insert(e, p, p?e:mk_not(m, e));
}
}
fml = lookup(fml, p0);
SASSERT(fml.get());
return true;
}
};
class nnf_normalize_literals {
ast_manager& m;
i_expr_pred& m_is_relevant;
i_nnf_atom& m_mk_atom;
obj_map<expr, expr*> m_cache;
ptr_vector<expr> m_todo;
expr_ref_vector m_trail;
ptr_vector<expr> m_args;
public:
nnf_normalize_literals(ast_manager& m, i_expr_pred& is_relevant, i_nnf_atom& mk_atom):
m(m), m_is_relevant(is_relevant), m_mk_atom(mk_atom), m_trail(m) {}
void operator()(expr_ref& fml) {
SASSERT(m_todo.empty());
m_todo.push_back(fml);
while (!m_todo.empty()) {
expr* e = m_todo.back();
if (m_cache.contains(e)) {
m_todo.pop_back();
}
else if (!is_app(e)) {
m_todo.pop_back();
m_cache.insert(e, e);
}
else if (visit(to_app(e))) {
m_todo.pop_back();
}
}
fml = m_cache.find(fml);
reset();
}
void reset() {
m_cache.reset();
m_todo.reset();
m_trail.reset();
}
private:
bool visit(app* e) {
bool all_visit = true;
expr* f = nullptr;
expr_ref tmp(m);
if (!m_is_relevant(e)) {
m_cache.insert(e, e);
}
else if (m.is_and(e) || m.is_or(e)) {
m_args.reset();
for (expr* arg : *e) {
if (m_cache.find(arg, f)) {
m_args.push_back(f);
}
else {
all_visit = false;
m_todo.push_back(arg);
}
}
if (all_visit) {
m_cache.insert(e, m.mk_app(e->get_decl(), m_args.size(), m_args.data()));
}
}
else if (m.is_not(e, f)) {
SASSERT(!m.is_not(f) && !m.is_and(f) && !m.is_or(f));
m_mk_atom(f, false, tmp);
m_cache.insert(e, tmp);
m_trail.push_back(tmp);
}
else {
m_mk_atom(e, true, tmp);
m_trail.push_back(tmp);
m_cache.insert(e, tmp);
}
return all_visit;
}
};
void def_vector::normalize() {
ast_manager& m = m_vars.get_manager();
expr_substitution sub(m);
scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m);
if (size() <= 1) {
return;
}
for (unsigned i = size(); i > 0; ) {
--i;
expr_ref e(m);
e = def(i);
rep->set_substitution(&sub);
(*rep)(e);
sub.insert(m.mk_const(var(i)), e);
def_ref(i) = e;
}
}
void def_vector::project(unsigned num_vars, app* const* vars) {
obj_hashtable<func_decl> fns;
for (unsigned i = 0; i < num_vars; ++i) {
fns.insert(vars[i]->get_decl());
}
for (unsigned i = 0; i < size(); ++i) {
if (fns.contains(m_vars[i].get())) {
fns.remove(m_vars[i].get());
}
else {
for (unsigned j = i+1; j < size(); ++j) {
m_vars.set(j-1, m_vars.get(j));
m_defs.set(j-1, m_defs.get(j));
}
m_vars.pop_back();
m_defs.pop_back();
--i;
}
}
}
std::ostream& guarded_defs::display(std::ostream& out) const {
ast_manager& m = m_guards.get_manager();
for (unsigned i = 0; i < size(); ++i) {
for (unsigned j = 0; j < defs(i).size(); ++j) {
out << defs(i).var(j)->get_name() << " := " << mk_pp(defs(i).def(j), m) << "\n";
}
out << "if " << mk_pp(guard(i), m) << "\n";
}
return out;
}
bool guarded_defs::inv() {
return m_defs.size() == m_guards.size();
}
void guarded_defs::add(expr* guard, def_vector const& defs) {
SASSERT(inv());
m_defs.push_back(defs);
m_guards.push_back(guard);
m_defs.back().normalize();
SASSERT(inv());
}
void guarded_defs::project(unsigned num_vars, app* const* vars) {
for (unsigned i = 0; i < size(); ++i) {
m_defs[i].project(num_vars, vars);
}
}
class nnf_collect_atoms {
ast_manager& m;
i_expr_pred& m_is_relevant;
ptr_vector<expr> m_todo;
ast_mark m_visited;
public:
nnf_collect_atoms(ast_manager& m, i_expr_pred& is_relevant):
m(m), m_is_relevant(is_relevant) {}
void operator()(expr* fml, atom_set& pos, atom_set& neg) {
m_todo.push_back(fml);
while (!m_todo.empty()) {
expr* e = m_todo.back();
m_todo.pop_back();
if (m_visited.is_marked(e))
continue;
m_visited.mark(e, true);
if (!is_app(e) || !m_is_relevant(e))
continue;
app* a = to_app(e);
if (m.is_and(a) || m.is_or(a)) {
for (expr* arg : *a)
m_todo.push_back(arg);
}
else if (m.is_not(a, e) && is_app(e)) {
neg.insert(to_app(e));
}
else {
pos.insert(a);
}
}
SASSERT(m_todo.empty());
m_visited.reset();
}
};
class nnf_normalizer {
nnf m_nnf_core;
nnf_collect_atoms m_collect_atoms;
nnf_normalize_literals m_normalize_literals;
public:
nnf_normalizer(ast_manager& m, i_expr_pred& is_relevant, i_nnf_atom& mk_atom):
m_nnf_core(m, is_relevant),
m_collect_atoms(m, is_relevant),
m_normalize_literals(m, is_relevant, mk_atom)
{}
void operator()(expr_ref& fml, atom_set& pos, atom_set& neg) {
expr_ref orig(fml);
m_nnf_core(fml);
m_normalize_literals(fml);
m_collect_atoms(fml, pos, neg);
TRACE(qe,
ast_manager& m = fml.get_manager();
tout << mk_ismt2_pp(orig, m) << "\n-->\n" << mk_ismt2_pp(fml, m) << "\n";);
}
void reset() {
m_nnf_core.reset();
m_normalize_literals.reset();
}
};
void get_nnf(expr_ref& fml, i_expr_pred& pred, i_nnf_atom& mk_atom, atom_set& pos, atom_set& neg) {
nnf_normalizer nnf(fml.get_manager(), pred, mk_atom);
nnf(fml, pos, neg);
}
class quant_elim {
public:
virtual ~quant_elim() = default;
virtual lbool eliminate_exists(
unsigned num_vars, app* const* vars,
expr_ref& fml, app_ref_vector& free_vars, bool get_first, guarded_defs* defs) = 0;
virtual void set_assumption(expr* fml) = 0;
virtual void collect_statistics(statistics & st) const = 0;
virtual void eliminate(bool is_forall, unsigned num_vars, app* const* vars, expr_ref& fml) = 0;
virtual void updt_params(params_ref const& p) {}
};
class search_tree {
typedef map<rational, unsigned, rational::hash_proc, rational::eq_proc> branch_map;
ast_manager& m;
app_ref_vector m_vars; app_ref m_var; def_vector m_def; expr_ref m_fml; app_ref m_assignment; search_tree* m_parent; rational m_num_branches; ptr_vector<search_tree> m_children; branch_map m_branch_index; atom_set m_pos;
atom_set m_neg;
bool m_pure;
#define CHECK_COND(_cond_) if (!(_cond_)) { TRACE(qe, tout << "violated: " << #_cond_ << "\n";); return false; }
bool invariant() const {
CHECK_COND(assignment());
CHECK_COND(m_children.empty() || fml());
CHECK_COND(!is_root() || fml());
CHECK_COND(!fml() || has_var() || m_num_branches.is_zero() || is_unit());
for (auto const & kv : m_branch_index) {
CHECK_COND(kv.m_value < m_children.size());
CHECK_COND(kv.m_key < get_num_branches());
}
for (unsigned i = 0; i < m_children.size(); ++i) {
CHECK_COND(m_children[i]);
CHECK_COND(this == m_children[i]->m_parent);
CHECK_COND(m_children[i]->invariant());
}
return true;
}
#undef CHECKC_COND
public:
search_tree(search_tree* parent, ast_manager& m, app* assignment):
m(m),
m_vars(m),
m_var(m),
m_def(m),
m_fml(m),
m_assignment(assignment, m),
m_parent(parent),
m_pure(true)
{}
~search_tree() {
reset();
}
expr* fml() const { return m_fml; }
expr_ref& fml_ref() { return m_fml; }
def_vector const& def() const { return m_def; }
app* assignment() const { return m_assignment; }
app* var() const { SASSERT(has_var()); return m_var; }
bool has_var() const { return nullptr != m_var.get(); }
search_tree* parent() const { return m_parent; }
bool is_root() const { return !parent(); }
rational const& get_num_branches() const { SASSERT(has_var()); return m_num_branches; }
void get_leaves(expr_ref_vector& result) {
SASSERT(is_root());
ptr_vector<search_tree> todo;
todo.push_back(this);
while (!todo.empty()) {
search_tree* st = todo.back();
todo.pop_back();
if (st->m_children.empty() && st->fml() &&
st->m_vars.empty() && !st->has_var()) {
TRACE(qe, st->display(tout << "appending leaf\n"););
result.push_back(st->fml());
}
for (auto * ch : st->m_children)
todo.push_back(ch);
}
}
void get_leaves_rec(def_vector& defs, guarded_defs& gdefs) {
expr* f = this->fml();
unsigned sz = defs.size();
defs.append(def());
if (m_children.empty() && f && !m.is_false(f) &&
m_vars.empty() && !has_var()) {
gdefs.add(f, defs);
}
else {
for (unsigned i = 0; i < m_children.size(); ++i) {
m_children[i]->get_leaves_rec(defs, gdefs);
}
}
defs.shrink(sz);
}
void get_leaves(guarded_defs& gdefs) {
def_vector defs(m);
get_leaves_rec(defs, gdefs);
}
void reset() {
TRACE(qe,tout << "resetting\n";);
for (auto* ch : m_children) dealloc(ch);
m_pos.reset();
m_neg.reset();
m_children.reset();
m_vars.reset();
m_branch_index.reset();
m_var = nullptr;
m_def.reset();
m_num_branches = rational::zero();
m_pure = true;
}
void init(expr* fml) {
m_fml = fml;
SASSERT(invariant());
}
void add_def(app* v, expr* def) {
if (v && def) {
m_def.push_back(v->get_decl(), def);
}
}
unsigned num_free_vars() const { return m_vars.size(); }
app_ref_vector const& free_vars() const { return m_vars; }
app* free_var(unsigned i) const { return m_vars[i]; }
void reset_free_vars() { TRACE(qe, tout << m_vars << "\n";); m_vars.reset(); }
atom_set const& pos_atoms() const { return m_pos; }
atom_set const& neg_atoms() const { return m_neg; }
atom_set& pos_atoms() { return m_pos; }
atom_set& neg_atoms() { return m_neg; }
void set_var(app* x, rational const& num_branches) {
SASSERT(!m_var.get());
SASSERT(m_vars.contains(x));
m_var = x;
m_vars.erase(x);
m_num_branches = num_branches;
SASSERT(invariant());
}
void consume_vars(app_ref_vector& vars) {
while (!vars.empty()) {
m_vars.push_back(vars.back());
vars.pop_back();
}
}
bool is_pure() const {
search_tree const* node = this;
while (node) {
if (!node->m_pure) return false;
node = node->parent();
}
return true;
}
bool is_unit() const {
return m_children.size() == 1 &&
m_branch_index.empty();
}
bool has_branch(rational const& branch_id) const { return m_branch_index.contains(branch_id); }
search_tree* child(rational const& branch_id) const {
unsigned idx = m_branch_index.find(branch_id);
return m_children[idx];
}
search_tree* child() const {
SASSERT(is_unit());
return m_children[0];
}
void del_var(app* x) {
SASSERT(m_children.empty());
SASSERT(m_vars.contains(x));
m_vars.erase(x);
m_pure = false;
}
search_tree* add_child(expr* fml) {
SASSERT(m_branch_index.empty());
SASSERT(m_children.empty());
m_num_branches = rational(1);
search_tree* st = alloc(search_tree, this, m, m.mk_true());
m_children.push_back(st);
st->init(fml);
st->m_vars.append(m_vars.size(), m_vars.data());
SASSERT(invariant());
TRACE(qe, display_node(tout); st->display_node(tout););
return st;
}
search_tree* add_child(rational const& branch_id, app* assignment) {
SASSERT(!m_branch_index.contains(branch_id));
SASSERT(has_var());
SASSERT(branch_id.is_nonneg() && branch_id < m_num_branches);
unsigned index = m_children.size();
search_tree* st = alloc(search_tree, this, m, assignment);
m_children.push_back(st);
m_branch_index.insert(branch_id, index);
st->m_vars.append(m_vars.size(), m_vars.data());
SASSERT(invariant());
TRACE(qe, display_node(tout); st->display_node(tout););
return st;
}
void display(std::ostream& out) const {
display(out, "");
}
void display_node(std::ostream& out, char const* indent = "") const {
out << indent << "node " << std::hex << this << std::dec << "\n";
if (m_var) {
out << indent << " var: " << m_var << "\n";
}
for (app* v : m_vars) {
out << indent << " free: " << mk_pp(v, m) << "\n";
}
if (m_fml) {
out << indent << " fml: " << m_fml << "\n";
}
for (unsigned i = 0; i < m_def.size(); ++i) {
out << indent << " def: " << m_def.var(i)->get_name() << " = " << mk_ismt2_pp(m_def.def(i), m) << "\n";
}
out << indent << " branches: " << m_num_branches << "\n";
}
void display(std::ostream& out, char const* indent) const {
display_node(out, indent);
std::string new_indent(indent);
new_indent += " ";
for (auto * ch : m_children) {
ch->display(out, new_indent.c_str());
}
}
expr_ref abstract_variable(app* x, expr* fml) const {
expr_ref result(m);
expr* y = x;
expr_abstract(m, 0, 1, &y, fml, result);
symbol X(x->get_decl()->get_name());
sort* s = x->get_sort();
result = m.mk_exists(1, &s, &X, result);
return result;
}
void display_validate(std::ostream& out) const {
if (m_children.empty()) {
return;
}
expr_ref q(m);
expr* x = m_var;
if (x) {
q = abstract_variable(m_var, m_fml);
expr_ref_vector fmls(m);
expr_ref fml(m);
for (unsigned i = 0; i < m_children.size(); ++i) {
search_tree const& child = *m_children[i];
fml = child.fml();
if (fml) {
ptr_vector<app> child_vars, new_vars;
child_vars.append(child.m_vars.size(), child.m_vars.data());
if (child.m_var) {
child_vars.push_back(child.m_var);
}
for (unsigned j = 0; j < child_vars.size(); ++j) {
if (!m_vars.contains(child_vars[j]) &&
!new_vars.contains(child_vars[j])) {
fml = abstract_variable(child_vars[j], fml);
new_vars.push_back(child_vars[j]);
}
}
fmls.push_back(fml);
}
}
bool_rewriter(m).mk_or(fmls.size(), fmls.data(), fml);
fml = mk_not(m, m.mk_iff(q, fml));
ast_smt_pp pp(m);
out << "; eliminate " << mk_pp(m_var, m) << "\n";
out << "(push 1)\n";
pp.display_smt2(out, fml);
out << "(pop 1)\n\n";
#if 0#endif
}
for (unsigned i = 0; i < m_children.size(); ++i) {
if (m_children[i]->fml()) {
m_children[i]->display_validate(out);
}
}
}
};
i_solver_context::~i_solver_context() {
for (unsigned i = 0; i < m_plugins.size(); ++i) {
dealloc(m_plugins[i]);
}
}
bool i_solver_context::is_relevant::operator()(expr* e) {
for (unsigned i = 0; i < m_s.get_num_vars(); ++i) {
if (m_s.contains(i)(e)) {
return true;
}
}
TRACE(qe_verbose, tout << "Not relevant: " << mk_ismt2_pp(e, m_s.get_manager()) << "\n";);
return false;
}
bool i_solver_context::is_var(expr* x, unsigned& idx) const {
unsigned nv = get_num_vars();
for (unsigned i = 0; i < nv; ++i) {
if (get_var(i) == x) {
idx = i;
return true;
}
}
return false;
}
void i_solver_context::add_plugin(qe_solver_plugin* p) {
family_id fid = p->get_family_id();
SASSERT(fid != null_family_id);
if (static_cast<int>(m_plugins.size()) <= fid) {
m_plugins.resize(fid+1);
}
SASSERT(!m_plugins[fid]);
m_plugins[fid] = p;
}
bool i_solver_context::has_plugin(app* x) {
family_id fid = x->get_sort()->get_family_id();
return
0 <= fid &&
fid < static_cast<int>(m_plugins.size()) &&
m_plugins[fid] != 0;
}
qe_solver_plugin& i_solver_context::plugin(app* x) {
SASSERT(has_plugin(x));
return *(m_plugins[x->get_sort()->get_family_id()]);
}
void i_solver_context::mk_atom(expr* e, bool p, expr_ref& result) {
ast_manager& m = get_manager();
TRACE(qe_verbose, tout << mk_ismt2_pp(e, m) << "\n";);
for (unsigned i = 0; i < m_plugins.size(); ++i) {
qe_solver_plugin* pl = m_plugins[i];
if (pl && pl->mk_atom(e, p, result)) {
return;
}
}
TRACE(qe_verbose, tout << "No plugin for " << mk_ismt2_pp(e, m) << "\n";);
result = p?e:mk_not(m, e);
}
void i_solver_context::mk_atom_fn::operator()(expr* e, bool p, expr_ref& result) {
m_s.mk_atom(e, p, result);
}
void i_solver_context::collect_statistics(statistics& st) const {
}
typedef ref_vector_ptr_hash<expr, ast_manager> expr_ref_vector_hash;
typedef ref_vector_ptr_eq<expr, ast_manager> expr_ref_vector_eq;
typedef hashtable<expr_ref_vector*, expr_ref_vector_hash, expr_ref_vector_eq> clause_table;
typedef value_trail<unsigned> _value_trail;
class quant_elim_plugin : public i_solver_context {
ast_manager& m;
quant_elim& m_qe;
th_rewriter m_rewriter;
smt::kernel m_solver;
bv_util m_bv;
expr_ref_vector m_literals;
bool_rewriter m_bool_rewriter;
conjunctions m_conjs;
app_ref_vector m_free_vars; app_ref_vector m_trail;
expr_ref m_fml;
expr_ref m_subfml;
obj_map<app, app*> m_var2branch; obj_map<app, contains_app*> m_var2contains; obj_map<app, ptr_vector<app> > m_children; search_tree m_root;
search_tree* m_current;
vector<unsigned_vector> m_partition;
app_ref_vector m_new_vars; bool m_get_first; guarded_defs* m_defs;
nnf_normalizer m_nnf;
public:
quant_elim_plugin(ast_manager& m, quant_elim& qe, smt_params& p):
m(m),
m_qe(qe),
m_rewriter(m),
m_solver(m, p),
m_bv(m),
m_literals(m),
m_bool_rewriter(m),
m_conjs(m),
m_free_vars(m),
m_trail(m),
m_fml(m),
m_subfml(m),
m_root(nullptr, m, m.mk_true()),
m_current(nullptr),
m_new_vars(m),
m_get_first(false),
m_defs(nullptr),
m_nnf(m, get_is_relevant(), get_mk_atom())
{
params_ref params;
params.set_bool("gcd_rounding", true);
m_rewriter.updt_params(params);
}
~quant_elim_plugin() override {
reset();
}
void reset() {
m_free_vars.reset();
m_trail.reset();
for (auto & kv : m_var2contains) {
dealloc(kv.m_value);
}
m_var2contains.reset();
m_var2branch.reset();
m_root.reset();
m_new_vars.reset();
m_fml = nullptr;
m_defs = nullptr;
m_nnf.reset();
}
void add_plugin(qe_solver_plugin* p) {
i_solver_context::add_plugin(p);
m_conjs.add_plugin(p);
}
void check(unsigned num_vars, app* const* vars,
expr* assumption, expr_ref& fml, bool get_first,
app_ref_vector& free_vars, guarded_defs* defs) {
reset();
m_solver.push();
m_get_first = get_first;
m_defs = defs;
for (unsigned i = 0; i < num_vars; ++i) {
if (has_plugin(vars[i])) {
add_var(vars[i]);
}
else {
m_free_vars.push_back(vars[i]);
}
}
m_root.consume_vars(m_new_vars);
m_current = &m_root;
m_fml = fml;
normalize(m_fml, m_root.pos_atoms(), m_root.neg_atoms());
expr_ref f(m_fml);
get_max_relevant(get_is_relevant(), f, m_subfml);
if (f.get() != m_subfml.get()) {
m_fml = f;
f = m_subfml;
m_solver.assert_expr(f);
}
m_root.init(f);
TRACE(qe,
for (unsigned i = 0; i < num_vars; ++i) tout << mk_ismt2_pp(vars[i], m) << "\n";
tout << mk_ismt2_pp(f, m) << "\n";);
m_solver.assert_expr(m_fml);
if (assumption) m_solver.assert_expr(assumption);
bool is_sat = false;
lbool res = l_true;
while (res == l_true) {
res = m_solver.check();
if (res == l_true && has_uninterpreted(m, m_fml))
res = l_undef;
if (res == l_true)
res = final_check();
if (res == l_true)
is_sat = true;
else
break;
}
if (res == l_undef) {
free_vars.append(num_vars, vars);
reset();
m_solver.pop(1);
return;
}
if (!is_sat) {
fml = m.mk_false();
if (m_fml.get() != m_subfml.get()) {
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml);
fml = m_fml;
}
reset();
m_solver.pop(1);
return;
}
if (!get_first) {
expr_ref_vector result(m);
m_root.get_leaves(result);
m_bool_rewriter.mk_or(result.size(), result.data(), fml);
}
if (defs) {
m_root.get_leaves(*defs);
defs->project(num_vars, vars);
}
TRACE(qe,
tout << "result:" << mk_ismt2_pp(fml, m) << "\n";
tout << "input: " << mk_ismt2_pp(m_fml, m) << "\n";
tout << "subformula: " << mk_ismt2_pp(m_subfml, m) << "\n";
m_root.display(tout);
m_root.display_validate(tout);
tout << "free: " << m_free_vars << "\n";);
free_vars.append(m_free_vars);
if (m_fml.get() != m_subfml.get()) {
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml);
fml = m_fml;
}
reset();
m_solver.pop(1);
f = nullptr;
}
void collect_statistics(statistics& st) {
m_solver.collect_statistics(st);
}
private:
lbool final_check() {
model_ref model;
m_solver.get_model(model);
if (!model)
return l_undef;
scoped_ptr<model_evaluator> model_eval = alloc(model_evaluator, *model);
while (m.inc()) {
TRACE(qe, model_v2_pp(tout, *model););
while (can_propagate_assignment(*model_eval))
propagate_assignment(*model_eval);
VERIFY(CHOOSE_VAR == update_current(*model_eval, true));
SASSERT(m_current->fml());
if (l_true != m_solver.check())
return l_true;
m_solver.get_model(model);
if (!model)
return l_undef;
model_eval = alloc(model_evaluator, *model);
search_tree* st = m_current;
update_current(*model_eval, false);
if (st == m_current)
break;
}
if (!m.inc())
return l_undef;
pop(*model_eval);
return l_true;
}
ast_manager& get_manager() override { return m; }
atom_set const& pos_atoms() const override { return m_current->pos_atoms(); }
atom_set const& neg_atoms() const override { return m_current->neg_atoms(); }
unsigned get_num_vars() const override { return m_current->num_free_vars(); }
app* get_var(unsigned idx) const override { return m_current->free_var(idx); }
app_ref_vector const& get_vars() const override { return m_current->free_vars(); }
contains_app& contains(unsigned idx) override { return contains(get_var(idx)); }
void elim_var(unsigned idx, expr* _fml, expr* def) override {
app* x = get_var(idx);
expr_ref fml(_fml, m);
TRACE(qe, tout << mk_pp(x,m) << " " << mk_pp(def, m) << "\n";);
m_current->set_var(x, rational(1));
m_current = m_current->add_child(fml);
m_current->add_def(x, def);
m_current->consume_vars(m_new_vars);
normalize(*m_current);
}
void add_var(app* x) override {
m_new_vars.push_back(x);
if (m_var2branch.contains(x)) {
return;
}
contains_app* ca = alloc(contains_app, m, x);
m_var2contains.insert(x, ca);
app* bv = nullptr;
if (m.is_bool(x) || m_bv.is_bv(x)) {
bv = x;
}
else {
bv = m.mk_fresh_const("b", m_bv.mk_sort(20));
m_trail.push_back(bv);
}
TRACE(qe, tout << "Add branch var: " << mk_ismt2_pp(x, m) << " " << mk_ismt2_pp(bv, m) << "\n";);
m_var2branch.insert(x, bv);
}
void add_constraint(bool use_current_val, expr* l1 = nullptr, expr* l2 = nullptr, expr* l3 = nullptr) override {
search_tree* node = m_current;
expr_ref _l1(l1, m), _l2(l2, m), _l3(l3, m);
if (!use_current_val) {
node = m_current->parent();
}
m_literals.reset();
while (node) {
m_literals.push_back(mk_not(m, node->assignment()));
node = node->parent();
}
add_literal(l1);
add_literal(l2);
add_literal(l3);
expr_ref fml(m);
fml = m.mk_or(m_literals);
TRACE(qe, tout << fml << "\n";);
m_solver.assert_expr(fml);
}
void blast_or(app* var, expr_ref& fml) override {
m_qe.eliminate_exists(1, &var, fml, m_free_vars, false, nullptr);
}
lbool eliminate_exists(unsigned num_vars, app* const* vars, expr_ref& fml, bool get_first, guarded_defs* defs) {
return m_qe.eliminate_exists(num_vars, vars, fml, m_free_vars, get_first, defs);
}
private:
void add_literal(expr* l) {
if (l != nullptr) {
m_literals.push_back(l);
}
}
void get_max_relevant(i_expr_pred& is_relevant, expr_ref& fml, expr_ref& subfml) {
if (m.is_and(fml) || m.is_or(fml)) {
app* a = to_app(fml);
unsigned num_args = a->get_num_args();
ptr_buffer<expr> r_args;
ptr_buffer<expr> i_args;
for (unsigned i = 0; i < num_args; ++i) {
expr* arg = a->get_arg(i);
if (is_relevant(arg)) {
r_args.push_back(arg);
}
else {
i_args.push_back(arg);
}
}
if (r_args.empty() || i_args.empty()) {
subfml = fml;
}
else if (r_args.size() == 1) {
expr_ref tmp(r_args[0], m);
get_max_relevant(is_relevant, tmp, subfml);
i_args.push_back(tmp);
fml = m.mk_app(a->get_decl(), i_args.size(), i_args.data());
}
else {
subfml = m.mk_app(a->get_decl(), r_args.size(), r_args.data());
i_args.push_back(subfml);
fml = m.mk_app(a->get_decl(), i_args.size(), i_args.data());
}
}
else {
subfml = fml;
}
}
app* get_branch_id(app* x) {
return m_var2branch[x];
}
bool extract_partition(ptr_vector<app>& vars) {
if (m_partition.empty()) {
return false;
}
unsigned_vector& vec = m_partition.back();
for (auto v : vec)
vars.push_back(m_current->free_var(v));
m_partition.pop_back();
return true;
}
enum update_status { CHOOSE_VAR, NEED_PROPAGATION };
update_status update_current(model_evaluator& model_eval, bool apply) {
SASSERT(m_fml);
m_current = &m_root;
rational branch, nb;
while (true) {
SASSERT(m_current->fml());
if (m_current->is_unit()) {
m_current = m_current->child();
continue;
}
if (!m_current->has_var()) {
return CHOOSE_VAR;
}
app* x = m_current->var();
app* b = get_branch_id(x);
nb = m_current->get_num_branches();
expr_ref fml(m_current->fml(), m);
if (!eval(model_eval, b, branch) || branch >= nb) {
TRACE(qe, tout << "evaluation failed: setting branch to 0\n";);
branch = rational::zero();
}
SASSERT(!branch.is_neg());
if (!m_current->has_branch(branch)) {
if (apply) {
app_ref assignment(mk_eq_value(b, branch), m);
m_current = m_current->add_child(branch, assignment);
plugin(x).assign(contains(x), fml, branch);
m_current->consume_vars(m_new_vars);
}
return NEED_PROPAGATION;
}
m_current = m_current->child(branch);
if (m_current->fml() == nullptr) {
SASSERT(!m_current->has_var());
if (apply) {
expr_ref def(m);
plugin(x).subst(contains(x), branch, fml, m_defs?&def:nullptr);
SASSERT(!contains(x)(fml));
m_current->consume_vars(m_new_vars);
m_current->init(fml);
m_current->add_def(x, def);
normalize(*m_current);
}
return CHOOSE_VAR;
}
}
}
void pop(model_evaluator& model_eval) {
solve_vars();
expr* fml = m_current->fml();
if (m_current->num_free_vars() == 0) {
block_assignment();
return;
}
expr_ref fml_closed(m), fml_open(m), fml_mixed(m);
unsigned num_vars = m_current->num_free_vars();
ptr_vector<contains_app> cont;
ptr_vector<app> vars;
for (unsigned i = 0; i < num_vars; ++i) {
cont.push_back(&contains(i));
vars.push_back(m_current->free_var(i));
}
m_conjs.get_partition(fml, num_vars, vars.data(), fml_closed, fml_mixed, fml_open);
if (m.is_and(fml_open) &&
m_conjs.partition_vars(
num_vars, cont.data(),
to_app(fml_open)->get_num_args(), to_app(fml_open)->get_args(),
m_partition)) {
process_partition();
return;
}
if (m.is_true(fml_mixed)) {
SASSERT(l_false != m_solver.check());
m_current = m_current->add_child(fml_closed);
for (unsigned i = 0; m_defs && i < m_current->num_free_vars(); ++i) {
expr_ref val(m);
app* x = m_current->free_var(i);
model_eval(x, val);
if (val == x) {
model_ref model;
lbool is_sat = m_solver.check();
if (is_sat == l_undef) return;
m_solver.get_model(model);
SASSERT(is_sat == l_true);
model_evaluator model_eval2(*model);
model_eval2.set_model_completion(true);
model_eval2(x, val);
}
TRACE(qe, tout << mk_pp(x,m) << " " << mk_pp(val, m) << "\n";);
m_current->add_def(x, val);
}
m_current->reset_free_vars();
block_assignment();
return;
}
constrain_assignment();
}
void normalize(search_tree& st) {
normalize(st.fml_ref(), st.pos_atoms(), st.neg_atoms());
}
void normalize(expr_ref& result, atom_set& pos, atom_set& neg) {
m_rewriter(result);
bool simplified = true;
while (simplified) {
simplified = false;
for (unsigned i = 0; !simplified && i < m_plugins.size(); ++i) {
qe_solver_plugin* pl = m_plugins[i];
simplified = pl && pl->simplify(result);
}
}
TRACE(qe_verbose, tout << "simp: " << mk_ismt2_pp(result.get(), m) << "\n";);
m_nnf(result, pos, neg);
TRACE(qe, tout << "nnf: " << mk_ismt2_pp(result.get(), m) << "\n";);
}
bool get_propagate_value(model_evaluator& model_eval, search_tree* node, app*& b, rational& b_val) {
return node->has_var() && eval(model_eval, get_branch_id(node->var()), b_val);
}
bool can_propagate_assignment(model_evaluator& model_eval) {
return m_fml && NEED_PROPAGATION == update_current(model_eval, false);
}
void propagate_assignment(model_evaluator& model_eval) {
if (m_fml) {
update_current(model_eval, true);
}
}
bool eval(model_evaluator& model_eval, app* b, rational& val) {
unsigned bv_size;
expr_ref res(m);
model_eval(b, res);
SASSERT(m.is_bool(b) || m_bv.is_bv(b));
if (m.is_true(res)) {
val = rational::one();
return true;
}
else if (m.is_false(res)) {
val = rational::zero();
return true;
}
else if (m_bv.is_numeral(res, val, bv_size)) {
return true;
}
else {
return false;
}
}
app* mk_eq_value(app* b, rational const& vl) {
if (m.is_bool(b)) {
if (vl.is_zero()) return to_app(mk_not(m, b));
if (vl.is_one()) return b;
UNREACHABLE();
}
SASSERT(m_bv.is_bv(b));
app_ref value(m_bv.mk_numeral(vl, m_bv.get_bv_size(b)), m);
return m.mk_eq(b, value);
}
bool is_eq_value(app* e, app*& bv, rational& v) {
unsigned sz = 0;
if (!m.is_eq(e)) return false;
expr* e0 = e->get_arg(0), *e1 = e->get_arg(1);
if (!m_bv.is_bv(e0)) return false;
if (m_bv.is_numeral(e0, v, sz) && is_app(e1)) {
bv = to_app(e1);
return true;
}
if (m_bv.is_numeral(e1, v, sz) && is_app(e0)) {
bv = to_app(e0);
return true;
}
return false;
}
void block_assignment() {
TRACE(qe_verbose, m_solver.display(tout););
add_constraint(true);
}
void constrain_assignment() {
SASSERT(m_current->fml());
rational k;
app* x;
if (!find_min_weight(x, k)) {
return;
}
m_current->set_var(x, k);
TRACE(qe, tout << mk_pp(x, m) << " := " << k << "\n";);
if (m_bv.is_bv(x)) {
return;
}
app* b = get_branch_id(x);
if (m.is_bool(b)) {
SASSERT(k <= rational(2));
return;
}
SASSERT(m_bv.is_bv(b));
SASSERT(k.is_pos());
app_ref max_val(m_bv.mk_numeral(k-rational::one(), m_bv.get_bv_size(b)), m);
expr_ref ub(m_bv.mk_ule(b, max_val), m);
add_constraint(true, ub);
}
void process_partition() {
expr_ref fml(m_current->fml(), m);
ptr_vector<app> vars;
bool closed = true;
while (extract_partition(vars)) {
lbool r = m_qe.eliminate_exists(vars.size(), vars.data(), fml, m_free_vars, m_get_first, m_defs);
vars.reset();
closed = closed && (r != l_undef);
}
TRACE(qe, tout << fml << " free: " << m_current->free_vars() << "\n";);
m_current->add_child(fml)->reset_free_vars();
block_assignment();
}
contains_app& contains(app* x) {
return *m_var2contains[x];
}
bool find_min_weight(app*& x, rational& num_branches) {
SASSERT(!m_current->has_var());
while (m_current->num_free_vars() > 0) {
unsigned weight = UINT_MAX;
unsigned nv = m_current->num_free_vars();
expr* fml = m_current->fml();
unsigned index = 0;
for (unsigned i = 0; i < nv; ++i) {
x = get_var(i);
if (!has_plugin(x)) {
break;
}
unsigned weight1 = plugin(get_var(i)).get_weight(contains(i), fml);
if (weight1 < weight) {
index = i;
}
}
x = get_var(index);
if (has_plugin(x) &&
plugin(x).get_num_branches(contains(x), fml, num_branches)) {
return true;
}
TRACE(qe, tout << "setting variable " << mk_pp(x, m) << " free\n";);
m_free_vars.push_back(x);
m_current->del_var(x);
}
return false;
}
void solve_vars() {
bool solved = true;
while (solved) {
expr_ref fml(m_current->fml(), m);
TRACE(qe, tout << fml << "\n";);
conj_enum conjs(m, fml);
solved = false;
for (unsigned i = 0; !solved && i < m_plugins.size(); ++i) {
qe_solver_plugin* p = m_plugins[i];
solved = p && p->solve(conjs, fml);
SASSERT(m_new_vars.empty());
}
}
}
};
class quant_elim_new : public quant_elim {
ast_manager& m;
smt_params& m_fparams;
expr_ref m_assumption;
bool m_produce_models;
ptr_vector<quant_elim_plugin> m_plugins;
bool m_eliminate_variables_as_block;
public:
quant_elim_new(ast_manager& m, smt_params& p) :
m(m),
m_fparams(p),
m_assumption(m),
m_produce_models(m_fparams.m_model),
m_eliminate_variables_as_block(true)
{
}
~quant_elim_new() override {
reset();
}
void reset() {
for (unsigned i = 0; i < m_plugins.size(); ++i) {
dealloc(m_plugins[i]);
}
}
void checkpoint() {
if (!m.inc())
throw tactic_exception(m.limit().get_cancel_msg());
}
void collect_statistics(statistics & st) const override {
for (unsigned i = 0; i < m_plugins.size(); ++i) {
m_plugins[i]->collect_statistics(st);
}
}
void updt_params(params_ref const& p) override {
m_eliminate_variables_as_block = p.get_bool("eliminate_variables_as_block", m_eliminate_variables_as_block);
}
void eliminate(bool is_forall, unsigned num_vars, app* const* vars, expr_ref& fml) override {
if (is_forall) {
eliminate_forall_bind(num_vars, vars, fml);
}
else {
eliminate_exists_bind(num_vars, vars, fml);
}
}
virtual void bind_variables(unsigned num_vars, app* const* vars, expr_ref& fml) {
if (num_vars > 0) {
ptr_vector<sort> sorts;
vector<symbol> names;
app_ref_vector free_vars(m);
for (unsigned i = 0; i < num_vars; ++i) {
contains_app contains_x(m, vars[i]);
if (contains_x(fml)) {
sorts.push_back(vars[i]->get_sort());
names.push_back(vars[i]->get_decl()->get_name());
free_vars.push_back(vars[i]);
}
}
if (!free_vars.empty()) {
expr_ref tmp = expr_abstract(free_vars, fml);
fml = m.mk_exists(free_vars.size(), sorts.data(), names.data(), tmp, 1);
}
}
}
void set_assumption(expr* fml) override {
m_assumption = fml;
}
lbool eliminate_exists(
unsigned num_vars, app* const* vars, expr_ref& fml,
app_ref_vector& free_vars, bool get_first, guarded_defs* defs) override {
if (get_first) {
return eliminate_block(num_vars, vars, fml, free_vars, get_first, defs);
}
if (m_eliminate_variables_as_block) {
return eliminate_block(num_vars, vars, fml, free_vars, get_first, defs);
}
for (unsigned i = 0; i < num_vars; ++i) {
lbool r = eliminate_block(1, vars+i, fml, free_vars, get_first, defs);
switch(r) {
case l_false:
return l_false;
case l_undef:
free_vars.append(num_vars-i-1,vars+1+i);
return l_undef;
default:
break;
}
}
return l_true;
}
private:
lbool eliminate_block(
unsigned num_vars, app* const* vars, expr_ref& fml,
app_ref_vector& free_vars, bool get_first, guarded_defs* defs) {
checkpoint();
if (has_quantifiers(fml)) {
free_vars.append(num_vars, vars);
return l_undef;
}
flet<bool> fl1(m_fparams.m_model, true);
flet<bool> fl2(m_fparams.m_simplify_bit2int, true);
flet<bool> fl3(m_fparams.m_arith_enum_const_mod, true);
flet<bool> fl4(m_fparams.m_bv_enable_int2bv2int, true);
flet<bool> fl5(m_fparams.m_array_canonize_simplify, true);
flet<unsigned> fl6(m_fparams.m_relevancy_lvl, 0);
TRACE(qe,
for (unsigned i = 0; i < num_vars; ++i) {
tout << mk_ismt2_pp(vars[i], m) << " ";
}
tout << "\n";
tout << mk_ismt2_pp(fml, m) << "\n";
);
expr_ref fml0(fml, m);
scoped_ptr<quant_elim_plugin> th;
pop_context(th);
th->check(num_vars, vars, m_assumption, fml, get_first, free_vars, defs);
push_context(th.detach());
TRACE(qe,
for (unsigned i = 0; i < num_vars; ++i) {
tout << mk_ismt2_pp(vars[i], m) << " ";
}
tout << "\n";
tout << "Input:\n" << mk_ismt2_pp(fml0, m) << "\n";
tout << "Result:\n" << mk_ismt2_pp(fml, m) << "\n";);
if (m.is_false(fml)) {
return l_false;
}
if (free_vars.empty()) {
return l_true;
}
return l_undef;
}
void pop_context(scoped_ptr<quant_elim_plugin>& th) {
if (m_plugins.empty()) {
th = alloc(quant_elim_plugin, m, *this, m_fparams);
th->add_plugin(mk_bool_plugin(*th));
th->add_plugin(mk_bv_plugin(*th));
th->add_plugin(mk_arith_plugin(*th, m_produce_models, m_fparams));
th->add_plugin(mk_array_plugin(*th));
th->add_plugin(mk_datatype_plugin(*th));
th->add_plugin(mk_dl_plugin(*th));
}
else {
th = m_plugins.back();
m_plugins.pop_back();
}
}
void push_context(quant_elim_plugin* th) {
m_plugins.push_back(th);
th->reset();
}
void eliminate_exists_bind(unsigned num_vars, app* const* vars, expr_ref& fml) {
checkpoint();
app_ref_vector free_vars(m);
eliminate_exists(num_vars, vars, fml, free_vars, false, nullptr);
bind_variables(free_vars.size(), free_vars.data(), fml);
}
void eliminate_forall_bind(unsigned num_vars, app* const* vars, expr_ref& fml) {
expr_ref tmp(m);
bool_rewriter rw(m);
rw.mk_not(fml, tmp);
eliminate_exists_bind(num_vars, vars, tmp);
rw.mk_not(tmp, fml);
}
};
expr_quant_elim::expr_quant_elim(ast_manager& m, smt_params const& fp, params_ref const& p):
m(m),
m_fparams(fp),
m_params(p),
m_trail(m),
m_qe(nullptr),
m_assumption(m.mk_true())
{
}
expr_quant_elim::~expr_quant_elim() {
dealloc(m_qe);
}
void expr_quant_elim::operator()(expr* assumption, expr* fml, expr_ref& result) {
TRACE(qe,
if (assumption) tout << "elim assumption\n" << mk_ismt2_pp(assumption, m) << "\n";
tout << "elim input\n" << mk_ismt2_pp(fml, m) << "\n";);
expr_ref_vector bound(m);
result = fml;
m_assumption = assumption;
instantiate_expr(bound, result);
elim(result);
m_trail.reset();
m_visited.reset();
abstract_expr(bound.size(), bound.data(), result);
TRACE(qe, tout << "elim result\n" << mk_ismt2_pp(result, m) << "\n";);
}
void expr_quant_elim::updt_params(params_ref const& p) {
init_qe();
m_qe->updt_params(p);
}
void expr_quant_elim::collect_param_descrs(param_descrs& r) {
r.insert("eliminate_variables_as_block", CPK_BOOL,
"(default: true) eliminate variables as a block (true) or one at a time (false)");
}
void expr_quant_elim::init_qe() {
if (!m_qe) {
m_qe = alloc(quant_elim_new, m, const_cast<smt_params&>(m_fparams));
}
}
void expr_quant_elim::instantiate_expr(expr_ref_vector& bound, expr_ref& fml) {
expr_free_vars fv;
fv(fml);
fv.set_default_sort(m.mk_bool_sort());
if (!fv.empty()) {
expr_ref tmp(m);
for (unsigned i = fv.size(); i > 0;) {
--i;
bound.push_back(m.mk_fresh_const("bound", fv[i]));
}
var_subst subst(m);
fml = subst(fml, bound.size(), bound.data());
}
}
void expr_quant_elim::abstract_expr(unsigned sz, expr* const* bound, expr_ref& fml) {
if (sz > 0) {
fml = expr_abstract(m, 0, sz, bound, fml);
}
}
void extract_vars(quantifier* q, expr_ref& new_body, app_ref_vector& vars) {
ast_manager& m = new_body.get_manager();
expr_ref tmp(m);
unsigned nd = q->get_num_decls();
for (unsigned i = 0; i < nd; ++i) {
vars.push_back(m.mk_fresh_const("x",q->get_decl_sort(i)));
}
expr* const* exprs = (expr* const*)(vars.data());
var_subst subst(m);
tmp = subst(new_body, vars.size(), exprs);
inv_var_shifter shift(m);
shift(tmp, vars.size(), new_body);
}
void expr_quant_elim::elim(expr_ref& result) {
expr_ref tmp(m);
ptr_vector<expr> todo;
m_trail.push_back(result);
todo.push_back(result);
expr* e = nullptr, *r = nullptr;
while (!todo.empty()) {
e = todo.back();
if (m_visited.contains(e)) {
todo.pop_back();
continue;
}
switch(e->get_kind()) {
case AST_APP: {
app* a = to_app(e);
expr_ref_vector args(m);
bool all_visited = true;
for (expr* arg : *a) {
if (m_visited.find(arg, r)) {
args.push_back(r);
}
else {
todo.push_back(arg);
all_visited = false;
}
}
if (all_visited) {
r = m.mk_app(a->get_decl(), args.size(), args.data());
todo.pop_back();
m_trail.push_back(r);
m_visited.insert(e, r);
}
break;
}
case AST_QUANTIFIER: {
app_ref_vector vars(m);
quantifier* q = to_quantifier(e);
if (is_lambda(q)) {
tmp = e;
}
else {
bool is_fa = is_forall(q);
tmp = q->get_expr();
extract_vars(q, tmp, vars);
elim(tmp);
init_qe();
m_qe->set_assumption(m_assumption);
m_qe->eliminate(is_fa, vars.size(), vars.data(), tmp);
}
m_trail.push_back(tmp);
m_visited.insert(e, tmp);
todo.pop_back();
break;
}
default:
UNREACHABLE();
break;
}
}
VERIFY (m_visited.find(result, e));
result = e;
}
void expr_quant_elim::collect_statistics(statistics & st) const {
if (m_qe) {
m_qe->collect_statistics(st);
}
}
lbool expr_quant_elim::first_elim(unsigned num_vars, app* const* vars, expr_ref& fml, def_vector& defs) {
app_ref_vector fvs(m);
init_qe();
guarded_defs gdefs(m);
lbool res = m_qe->eliminate_exists(num_vars, vars, fml, fvs, true, &gdefs);
if (gdefs.size() > 0) {
defs.reset();
defs.append(gdefs.defs(0));
fml = gdefs.guard(0);
}
return res;
}
bool expr_quant_elim::solve_for_var(app* var, expr* fml, guarded_defs& defs) {
return solve_for_vars(1,&var, fml, defs);
}
bool expr_quant_elim::solve_for_vars(unsigned num_vars, app* const* vars, expr* _fml, guarded_defs& defs) {
app_ref_vector fvs(m);
expr_ref fml(_fml, m);
TRACE(qe, tout << mk_pp(fml, m) << "\n";);
init_qe();
lbool is_sat = m_qe->eliminate_exists(num_vars, vars, fml, fvs, false, &defs);
return is_sat != l_undef;
}
#if 0#endif
void hoist_exists(expr_ref& fml, app_ref_vector& vars) {
quantifier_hoister hoister(fml.get_manager());
hoister.pull_exists(fml, vars, fml);
}
void mk_exists(unsigned num_bound, app* const* vars, expr_ref& fml) {
ast_manager& m = fml.get_manager();
expr_ref tmp(m);
expr_abstract(m, 0, num_bound, (expr*const*)vars, fml, tmp);
ptr_vector<sort> sorts;
svector<symbol> names;
for (unsigned i = 0; i < num_bound; ++i) {
sorts.push_back(vars[i]->get_decl()->get_range());
names.push_back(vars[i]->get_decl()->get_name());
}
if (num_bound > 0) {
tmp = m.mk_exists(num_bound, sorts.data(), names.data(), tmp, 1);
}
fml = tmp;
}
bool has_quantified_uninterpreted(ast_manager& m, expr* fml) {
struct found : public std::exception {};
struct proc {
ast_manager& m;
proc(ast_manager& m):m(m) {}
void operator()(quantifier* q) {
if (has_uninterpreted(m, q->get_expr()))
throw found();
}
void operator()(expr*) {}
};
try {
proc p(m);
for_each_expr(p, fml);
return false;
}
catch (found const&) {
return true;
}
}
class simplify_solver_context : public i_solver_context {
ast_manager& m;
smt_params m_fparams;
app_ref_vector* m_vars;
expr_ref* m_fml;
ptr_vector<contains_app> m_contains;
atom_set m_pos;
atom_set m_neg;
public:
simplify_solver_context(ast_manager& m):
m(m),
m_vars(nullptr),
m_fml(nullptr)
{
add_plugin(mk_bool_plugin(*this));
add_plugin(mk_arith_plugin(*this, false, m_fparams));
}
void updt_params(params_ref const& p) {
m_fparams.updt_params(p);
}
~simplify_solver_context() override { reset(); }
void solve(expr_ref& fml, app_ref_vector& vars) {
init(fml, vars);
bool solved = true;
do {
conj_enum conjs(m, fml);
solved = false;
for (unsigned i = 0; !solved && i < m_plugins.size(); ++i) {
qe_solver_plugin* p = m_plugins[i];
solved = p && p->solve(conjs, fml);
}
TRACE(qe,
tout << (solved?"solved":"not solved") << "\n";
if (solved) tout << mk_ismt2_pp(fml, m) << "\n";
tout << *m_vars << "\n";
tout << "contains: " << m_contains.size() << "\n";
);
}
while (solved);
}
ast_manager& get_manager() override { return m; }
atom_set const& pos_atoms() const override { return m_pos; }
atom_set const& neg_atoms() const override { return m_neg; }
unsigned get_num_vars() const override { return m_vars->size(); }
app* get_var(unsigned idx) const override { return (*m_vars)[idx].get(); }
app_ref_vector const& get_vars() const override { return *m_vars; }
bool is_var(expr* e, unsigned& idx) const override {
for (unsigned i = 0; i < m_vars->size(); ++i) {
if ((*m_vars)[i].get() == e) {
idx = i;
return true;
}
}
return false;
}
contains_app& contains(unsigned idx) override {
return *m_contains[idx];
}
void elim_var(unsigned idx, expr* fml, expr* def) override {
TRACE(qe, tout << idx << ": " << mk_pp(m_vars->get(idx), m) << " " << mk_pp(fml, m) << " " << m_contains.size() << "\n";);
*m_fml = fml;
m_vars->set(idx, m_vars->get(m_vars->size()-1));
m_vars->pop_back();
dealloc(m_contains[idx]);
m_contains[idx] = m_contains[m_contains.size()-1];
m_contains.pop_back();
}
void add_var(app* x) override {
TRACE(qe, tout << "add var: " << mk_pp(x, m) << "\n";);
m_vars->push_back(x);
m_contains.push_back(alloc(contains_app, m, x));
}
void add_constraint(bool use_var, expr* l1 = nullptr, expr* l2 = nullptr, expr* l3 = nullptr) override {
UNREACHABLE();
}
void blast_or(app* var, expr_ref& fml) override {
UNREACHABLE();
}
private:
void reset() {
for (auto* c : m_contains)
dealloc (c);
m_contains.reset();
}
void init(expr_ref& fml, app_ref_vector& vars) {
reset();
m_fml = &fml;
m_vars = &vars;
TRACE(qe, tout << "Vars: " << vars << "\n";);
for (auto* v : vars) {
m_contains.push_back(alloc(contains_app, m, v));
}
}
};
class simplify_rewriter_cfg::impl {
ast_manager& m;
simplify_solver_context m_ctx;
public:
impl(ast_manager& m) : m(m), m_ctx(m) {}
void updt_params(params_ref const& p) {
m_ctx.updt_params(p);
}
void collect_statistics(statistics & st) const {
m_ctx.collect_statistics(st);
}
bool reduce_quantifier(
quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr
)
{
if (is_lambda(old_q)) {
return false;
}
app_ref_vector vars(m);
TRACE(qe, tout << "simplifying" << mk_pp(new_body, m) << "\n";);
result = new_body;
extract_vars(old_q, result, vars);
TRACE(qe, tout << "variables extracted" << mk_pp(result, m) << "\n";);
if (is_forall(old_q)) {
result = mk_not(m, result);
}
m_ctx.solve(result, vars);
if (is_forall(old_q)) {
expr* e = nullptr;
result = m.is_not(result, e)?e:mk_not(m, result);
}
var_shifter shift(m);
shift(result, vars.size(), result);
result = expr_abstract(vars, result);
TRACE(qe, tout << "abstracted" << mk_pp(result, m) << "\n";);
ptr_vector<sort> sorts;
svector<symbol> names;
for (app* v : vars) {
sorts.push_back(v->get_decl()->get_range());
names.push_back(v->get_decl()->get_name());
}
if (!vars.empty()) {
result = m.mk_quantifier(old_q->get_kind(), vars.size(), sorts.data(), names.data(), result, 1);
}
result_pr = nullptr;
return true;
}
};
simplify_rewriter_cfg::simplify_rewriter_cfg(ast_manager& m) {
imp = alloc(simplify_rewriter_cfg::impl, m);
}
simplify_rewriter_cfg::~simplify_rewriter_cfg() {
dealloc(imp);
}
bool simplify_rewriter_cfg::reduce_quantifier(
quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr
) {
return imp->reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr);
}
void simplify_rewriter_cfg::updt_params(params_ref const& p) {
imp->updt_params(p);
}
void simplify_rewriter_cfg::collect_statistics(statistics & st) const {
imp->collect_statistics(st);
}
bool simplify_rewriter_cfg::pre_visit(expr* e) {
if (!is_quantifier(e)) return true;
quantifier * q = to_quantifier(e);
return (q->get_num_patterns() == 0 && q->get_num_no_patterns() == 0);
}
void simplify_exists(app_ref_vector& vars, expr_ref& fml) {
ast_manager& m = fml.get_manager();
simplify_solver_context ctx(m);
ctx.solve(fml, vars);
}
}
template class rewriter_tpl<qe::simplify_rewriter_cfg>;