mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

fixing #4670 (#4682)

Browse source 
* fixing #4670

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* init

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* arrays

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* arrays

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* arrays

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-10 04:35:11 -07:00 • committed by GitHub
parent ee00542e76
commit cfa7c733db
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
48 changed files with 1591 additions and 359 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_binspr.h
View file

@ -71,7 +71,7 @@ namespace sat {
void collect_candidates(literal lit, literal const* begin, literal const* end);
void strengthen_clause(literal lit, literal const* begin, literal const* end);
bool_var m_p, m_q, m_u, m_v;
bool_var m_p{ 0 }, m_q{ 0 }, m_u{ 0 }, m_v{ 0 };
lbool m_vals[4];
void algorithm2();

44
src/sat/sat_cut_simplifier.cpp
View file

@ -460,7 +460,7 @@ namespace sat {
return;
}
bin_rel q, p(~u, v);
if (m_bins.find(p, q) && q.op != none)
if (m_bins.find(p, q) && q.op != op_code::none)
return;
if (big.connected(u, v))
return;
@ -614,20 +614,16 @@ namespace sat {
*/
void cut_simplifier::cuts2bins(vector<cut_set> const& cuts) {
svector<bin_rel> dcs;
for (auto const& p : m_bins) {
if (p.op != none)
dcs.push_back(p);
}
for (auto const& p : m_bins)
if (p.op != op_code::none)
dcs.push_back(p);
m_bins.reset();
for (auto const& cs : cuts) {
for (auto const& c : cs) {
for (unsigned i = c.size(); i-- > 0; ) {
for (unsigned j = i; j-- > 0; ) {
for (auto const& cs : cuts)
for (auto const& c : cs)
for (unsigned i = c.size(); i-- > 0; )
for (unsigned j = i; j-- > 0; )
m_bins.insert(bin_rel(c[j],c[i]));
}
}
}
}
// don't lose previous don't cares
for (auto const& p : dcs) {
if (m_bins.contains(p)) {
@ -646,27 +642,27 @@ namespace sat {
big b(s.rand());
b.init(s, true);
for (auto& p : m_bins) {
if (p.op != none) continue;
if (p.op != op_code::none) continue;
literal u(p.u, false), v(p.v, false);
// u -> v, then u & ~v is impossible
if (b.connected(u, v)) {
p.op = pn;
p.op = op_code::pn;
}
else if (b.connected(u, ~v)) {
p.op = pp;
p.op = op_code::pp;
}
else if (b.connected(~u, v)) {
p.op = nn;
p.op = op_code::nn;
}
else if (b.connected(~u, ~v)) {
p.op = np;
p.op = op_code::np;
}
if (p.op != none) {
if (p.op != op_code::none) {
track_binary(p);
}
}
IF_VERBOSE(2, {
unsigned n = 0; for (auto const& p : m_bins) if (p.op != none) ++n;
unsigned n = 0; for (auto const& p : m_bins) if (p.op != op_code::none) ++n;
verbose_stream() << n << " / " << m_bins.size() << " don't cares\n";
});
}
@ -698,10 +694,10 @@ namespace sat {
*/
uint64_t cut_simplifier::op2dont_care(unsigned i, unsigned j, bin_rel const& p) {
SASSERT(i < j && j < 6);
if (p.op == none) return 0ull;
if (p.op == op_code::none) return 0ull;
// first position of mask is offset into output bits contributed by i and j
bool i_is_0 = (p.op == np || p.op == nn);
bool j_is_0 = (p.op == pn || p.op == nn);
bool i_is_0 = (p.op == op_code::np || p.op == op_code::nn);
bool j_is_0 = (p.op == op_code::pn || p.op == op_code::nn);
uint64_t first = (i_is_0 ? 0 : (1 << i)) + (j_is_0 ? 0 : (1 << j));
uint64_t inc = 1ull << (j + 1);
uint64_t r = 1ull << first;
@ -719,7 +715,7 @@ namespace sat {
for (unsigned i = 0; i < c.size(); ++i) {
for (unsigned j = i + 1; j < c.size(); ++j) {
bin_rel p(c[i], c[j]);
if (m_bins.find(p, p) && p.op != none) {
if (m_bins.find(p, p) && p.op != op_code::none) {
dc |= op2dont_care(i, j, p);
}
}

28
src/sat/sat_cut_simplifier.h
View file

@ -68,27 +68,27 @@ namespace sat {
*
*/
enum op_code { pp, pn, np, nn, none };
enum class op_code { pp, pn, np, nn, none };
struct bin_rel {
unsigned u, v;
op_code op;
bin_rel(unsigned _u, unsigned _v): u(_u), v(_v), op(none) {
bin_rel(unsigned _u, unsigned _v): u(_u), v(_v), op(op_code::none) {
if (u > v) std::swap(u, v);
}
// convert binary clause into a bin-rel
bin_rel(literal _u, literal _v): u(_u.var()), v(_v.var()), op(none) {
if (_u.sign() && _v.sign()) op = pp;
else if (_u.sign()) op = pn;
else if (_v.sign()) op = np;
else op = nn;
bin_rel(literal _u, literal _v): u(_u.var()), v(_v.var()), op(op_code::none) {
if (_u.sign() && _v.sign()) op = op_code::pp;
else if (_u.sign()) op = op_code::pn;
else if (_v.sign()) op = op_code::np;
else op = op_code::nn;
if (u > v) {
std::swap(u, v);
if (op == np) op = pn;
else if (op == pn) op = np;
if (op == op_code::np) op = op_code::pn;
else if (op == op_code::pn) op = op_code::np;
}
}
bin_rel(): u(UINT_MAX), v(UINT_MAX), op(none) {}
bin_rel(): u(UINT_MAX), v(UINT_MAX), op(op_code::none) {}
struct hash {
unsigned operator()(bin_rel const& p) const {
@ -102,10 +102,10 @@ namespace sat {
};
void to_binary(literal& lu, literal& lv) const {
switch (op) {
case pp: lu = literal(u, true); lv = literal(v, true); break;
case pn: lu = literal(u, true); lv = literal(v, false); break;
case np: lu = literal(u, false); lv = literal(v, true); break;
case nn: lu = literal(u, false); lv = literal(v, false); break;
case op_code::pp: lu = literal(u, true); lv = literal(v, true); break;
case op_code::pn: lu = literal(u, true); lv = literal(v, false); break;
case op_code::np: lu = literal(u, false); lv = literal(v, true); break;
case op_code::nn: lu = literal(u, false); lv = literal(v, false); break;
default: UNREACHABLE(); break;
}
}

32
src/sat/sat_extension.h
View file

@ -58,40 +58,40 @@ namespace sat {
virtual ~extension() {}
virtual unsigned get_id() const { return 0; }
virtual void set_solver(solver* s) = 0;
virtual void set_lookahead(lookahead* s) = 0;
virtual void set_lookahead(lookahead* s) {};
virtual void init_search() {}
virtual bool propagate(literal l, ext_constraint_idx idx) = 0;
virtual bool unit_propagate() = 0;
virtual bool is_external(bool_var v) = 0;
virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const = 0;
virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const { return 0; }
virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r, bool probing) = 0;
virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r) = 0;
virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r) { return false; }
virtual void asserted(literal l) = 0;
virtual check_result check() = 0;
virtual lbool resolve_conflict() { return l_undef; } // stores result in sat::solver::m_lemma
virtual void push() = 0;
void push_scopes(unsigned n) { for (unsigned i = 0; i < n; ++i) push(); }
virtual void pop(unsigned n) = 0;
virtual void pre_simplify() = 0;
virtual void simplify() = 0;
virtual void pre_simplify() {}
virtual void simplify() {}
// have a way to replace l by r in all constraints
virtual bool set_root(literal l, literal r) { return false; }
virtual void flush_roots() {}
virtual void clauses_modifed() = 0;
virtual lbool get_phase(bool_var v) = 0;
virtual void clauses_modifed() {}
virtual lbool get_phase(bool_var v) { return l_undef; }
virtual std::ostream& display(std::ostream& out) const = 0;
virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0;
virtual std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const = 0;
virtual void collect_statistics(statistics& st) const = 0;
virtual extension* copy(solver* s) = 0;
virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) = 0;
virtual void gc() = 0;
virtual void pop_reinit() = 0;
virtual bool validate() = 0;
virtual void init_use_list(ext_use_list& ul) = 0;
virtual bool is_blocked(literal l, ext_constraint_idx) = 0;
virtual bool check_model(model const& m) const = 0;
virtual unsigned max_var(unsigned w) const = 0;
virtual extension* copy(solver* s) { UNREACHABLE(); return nullptr; }
virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) {}
virtual void gc() {}
virtual void pop_reinit() {}
virtual bool validate() { return true; }
virtual void init_use_list(ext_use_list& ul) {}
virtual bool is_blocked(literal l, ext_constraint_idx) { return false; }
virtual bool check_model(model const& m) const { return true; }
virtual unsigned max_var(unsigned w) const { return w; }
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) {

31
src/sat/sat_local_search.h
View file

@ -88,33 +88,24 @@ namespace sat {
};
struct var_info {
bool m_value; // current solution
unsigned m_bias; // bias for current solution in percentage.
bool m_value{ true }; // current solution
unsigned m_bias{ 50 }; // bias for current solution in percentage.
// if bias is 0, then value is always false, if 100, then always true
bool m_unit; // is this a unit literal
bool m_unit{ false }; // is this a unit literal
literal m_explain; // explanation for unit assignment
bool m_conf_change; // whether its configure changes since its last flip
bool m_in_goodvar_stack;
int m_score;
int m_slack_score;
int m_time_stamp; // the flip time stamp
bool m_conf_change{ true }; // whether its configure changes since its last flip
bool m_in_goodvar_stack{ false };
int m_score{ 0 };
int m_slack_score{ 0 };
int m_time_stamp{ 0 }; // the flip time stamp
bool_var_vector m_neighbors; // neighborhood variables
coeff_vector m_watch[2];
literal_vector m_bin[2];
unsigned m_flips;
unsigned m_flips{ 0 };
ema m_slow_break;
double m_break_prob;
double m_break_prob{ 0 };
var_info():
m_value(true),
m_bias(50),
m_unit(false),
m_conf_change(true),
m_in_goodvar_stack(false),
m_score(0),
m_slack_score(0),
m_flips(0),
m_slow_break(1e-5),
m_break_prob(0)
m_slow_break(1e-5)
{}
};

4
src/sat/smt/CMakeLists.txt
View file

@ -1,5 +1,9 @@
z3_add_component(sat_smt
SOURCES
array_axioms.cpp
array_internalize.cpp
array_model.cpp
array_solver.cpp
atom2bool_var.cpp
ba_internalize.cpp
ba_solver.cpp

528
src/sat/smt/array_axioms.cpp Normal file
View file

@ -0,0 +1,528 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
array_axioms.cpp
Abstract:
Routines for instantiating array axioms
Author:
Nikolaj Bjorner (nbjorner) 2020-09-08
--*/
#include "ast/ast_trail.h"
#include "ast/ast_ll_pp.h"
#include "sat/smt/array_solver.h"
#include "sat/smt/euf_solver.h"
namespace array {
void solver::push_axiom(axiom_record const& r) {
unsigned idx = m_axiom_trail.size();
m_axiom_trail.push_back(r);
if (m_axioms.contains(idx))
m_axiom_trail.pop_back();
}
bool solver::assert_axiom(unsigned idx) {
axiom_record const& r = m_axiom_trail[idx];
if (m_axioms.contains(idx))
return false;
m_axioms.insert(idx);
ctx.push(insert_map<euf::solver, axiom_table_t, unsigned>(m_axioms, idx));
expr* child = r.n->get_expr();
app* select;
switch (r.m_kind) {
case axiom_record::kind_t::is_store:
return assert_store_axiom(to_app(child));
case axiom_record::kind_t::is_select:
select = r.select->get_app();
SASSERT(a.is_select(select));
if (a.is_const(child))
return assert_select_const_axiom(select, to_app(child));
else if (a.is_as_array(child))
return assert_select_as_array_axiom(select, to_app(child));
else if (a.is_store(child))
return assert_select_store_axiom(select, to_app(child));
else if (a.is_map(child))
return assert_select_map_axiom(select, to_app(child));
else if (is_lambda(child))
return assert_select_lambda_axiom(select, child);
else
UNREACHABLE();
break;
case axiom_record::kind_t::is_default:
if (a.is_const(child))
return assert_default_const_axiom(to_app(child));
else if (a.is_store(child))
return assert_default_store_axiom(to_app(child));
else if (a.is_map(child))
return assert_default_map_axiom(to_app(child));
else if (a.is_as_array(child))
return assert_default_as_array_axiom(to_app(child));
else
UNREACHABLE();
break;
case axiom_record::kind_t::is_extensionality:
return assert_extensionality(r.n->get_arg(0)->get_expr(), r.n->get_arg(1)->get_expr());
case axiom_record::kind_t::is_congruence:
return assert_congruent_axiom(child, r.select->get_expr());
default:
UNREACHABLE();
break;
}
return false;
}
/**
* Assert
* select(n, i) = v
* Where
* n := store(a, i, v)
*/
bool solver::assert_store_axiom(app* e) {
m_stats.m_num_store_axiom++;
SASSERT(a.is_store(e));
unsigned num_args = e->get_num_args();
ptr_vector<expr> sel_args(num_args - 1, e->get_args());
sel_args[0] = e;
expr_ref sel(a.mk_select(sel_args), m);
euf::enode* n1 = e_internalize(sel);
euf::enode* n2 = expr2enode(e->get_arg(num_args - 1));
return ctx.propagate(n1, n2, array_axiom());
}
/**
* Assert
* i_k = j_k or select(store(a, i, v), j) = select(a, j)
* where i = (i_1, ..., i_n), j = (j_1, .., j_n), k in 1..n
*/
bool solver::assert_select_store_axiom(app* select, app* store) {
m_stats.m_num_select_store_axiom++;
SASSERT(a.is_store(store));
SASSERT(a.is_select(select));
SASSERT(store->get_num_args() == 1 + select->get_num_args());
ptr_buffer<expr> sel1_args, sel2_args;
unsigned num_args = select->get_num_args();
sel1_args.push_back(store);
sel2_args.push_back(store->get_arg(0));
for (unsigned i = 1; i < num_args; i++) {
sel1_args.push_back(select->get_arg(i));
sel2_args.push_back(select->get_arg(i));
}
expr_ref sel1(a.mk_select(sel1_args), m);
expr_ref sel2(a.mk_select(sel2_args), m);
expr_ref sel_eq_e(m.mk_eq(sel1, sel2), m);
euf::enode* s1 = e_internalize(sel1);
euf::enode* s2 = e_internalize(sel2);
if (s1->get_root() == s2->get_root())
return false;
sat::literal sel_eq = b_internalize(sel_eq_e);
for (unsigned i = 1; i < num_args; i++) {
expr* idx1 = store->get_arg(i);
expr* idx2 = select->get_arg(i);
euf::enode* r1 = expr2enode(idx1)->get_root();
euf::enode* r2 = expr2enode(idx2)->get_root();
if (r1 == r2)
continue;
if (m.are_distinct(r1->get_expr(), r2->get_expr())) {
add_clause(sel_eq);
break;
}
sat::literal idx_eq = b_internalize(m.mk_eq(idx1, idx2));
add_clause(idx_eq, sel_eq);
}
return true;
}
/**
* Assert
* select(const(v), i) = v
*/
bool solver::assert_select_const_axiom(app* select, app* cnst) {
m_stats.m_num_select_const_axiom++;
expr* val = nullptr;
VERIFY(a.is_const(cnst, val));
SASSERT(a.is_select(select));
unsigned num_args = select->get_num_args();
ptr_vector<expr> sel_args(num_args, select->get_args());
sel_args[0] = cnst;
expr_ref sel(a.mk_select(sel_args), m);
euf::enode* n1 = e_internalize(sel);
euf::enode* n2 = expr2enode(val);
return ctx.propagate(n1, n2, array_axiom());
}
/**
* e1 = e2 or select(e1, diff(e1,e2)) != select(e2, diff(e1, e2))
*/
bool solver::assert_extensionality(expr* e1, expr* e2) {
m_stats.m_num_extensionality_axiom++;
func_decl_ref_vector* funcs = nullptr;
VERIFY(m_sort2diff.find(m.get_sort(e1), funcs));
expr_ref_vector args1(m), args2(m);
args1.push_back(e1);
args2.push_back(e2);
for (func_decl* f : *funcs) {
expr* k = m.mk_app(f, e1, e2);
args1.push_back(k);
args2.push_back(k);
}
expr_ref sel1(a.mk_select(args1), m);
expr_ref sel2(a.mk_select(args2), m);
expr_ref n1_eq_n2(m.mk_eq(e1, e2), m);
expr_ref sel1_eq_sel2(m.mk_eq(sel1, sel2), m);
literal lit1 = b_internalize(n1_eq_n2);
literal lit2 = b_internalize(sel1_eq_sel2);
if (s().value(lit1) == l_true || s().value(lit2) == l_false)
return false;
add_clause(lit1, ~lit2);
return true;
}
/**
* Assert axiom:
* select(map[f](a, ... d), i) = f(select(a,i),...,select(d,i))
*/
bool solver::assert_select_map_axiom(app* select, app* map) {
m_stats.m_num_select_map_axiom++;
SASSERT(a.is_map(map));
SASSERT(a.is_select(select));
SASSERT(map->get_num_args() > 0);
func_decl* f = a.get_map_func_decl(map);
TRACE("array",
tout << mk_bounded_pp(map, m) << "\n";
tout << mk_bounded_pp(select, m) << "\n";);
unsigned num_args = select->get_num_args();
unsigned num_arrays = map->get_num_args();
ptr_buffer<expr> args1, args2;
vector<ptr_vector<expr> > args2l;
args1.push_back(map);
for (expr* ar : *map) {
ptr_vector<expr> arg;
arg.push_back(ar);
args2l.push_back(arg);
}
for (unsigned i = 1; i < num_args; ++i) {
expr* arg = select->get_arg(i);
for (auto& args : args2l)
args.push_back(arg);
args1.push_back(arg);
}
for (auto const& args : args2l)
args2.push_back(a.mk_select(args));
expr_ref sel1(m), sel2(m);
sel1 = a.mk_select(args1);
sel2 = m.mk_app(f, args2);
rewrite(sel2);
euf::enode* n1 = e_internalize(sel1);
euf::enode* n2 = e_internalize(sel2);
return ctx.propagate(n1, n2, array_axiom());
}
/**
* Assert axiom:
* select(as-array f, i_1, ..., i_n) = (f i_1 ... i_n)
*/
bool solver::assert_select_as_array_axiom(app* select, app* arr) {
m_stats.m_num_select_as_array_axiom++;
SASSERT(a.is_as_array(arr));
SASSERT(a.is_select(select));
unsigned num_args = select->get_num_args();
func_decl* f = a.get_as_array_func_decl(arr);
ptr_vector<expr> sel_args(num_args, select->get_args());
sel_args[0] = arr;
expr_ref sel(a.mk_select(sel_args), m);
expr_ref val(m.mk_app(f, sel_args.size() - 1, sel_args.c_ptr() + 1), m);
euf::enode* n1 = e_internalize(sel);
euf::enode* n2 = e_internalize(val);
return ctx.propagate(n1, n2, array_axiom());
}
/**
* Assert:
* default(map[f](a,..,d)) = f(default(a),..,default(d))
*/
bool solver::assert_default_map_axiom(app* map) {
m_stats.m_num_default_map_axiom++;
SASSERT(a.is_map(map));
func_decl* f = a.get_map_func_decl(map);
SASSERT(map->get_num_args() == f->get_arity());
ptr_buffer<expr> args2;
for (expr* arg : *map)
args2.push_back(a.mk_default(arg));
expr_ref def1(a.mk_default(map), m);
expr_ref def2(m.mk_app(f, args2), m);
rewrite(def2);
return ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom());
}
/**
* Assert:
* default(const(e)) = e
*/
bool solver::assert_default_const_axiom(app* cnst) {
m_stats.m_num_default_const_axiom++;
expr* val = nullptr;
VERIFY(a.is_const(cnst, val));
TRACE("array", tout << mk_bounded_pp(cnst, m) << "\n";);
expr_ref def(a.mk_default(cnst), m);
return ctx.propagate(expr2enode(val), e_internalize(def), array_axiom());
}
bool solver::assert_default_as_array_axiom(app* as_array) {
// no-op
return false;
}
/**
* let n := store(a, i, v)
* Assert:
* - when sort(n) has exactly one element:
* default(n) = v
* - for small domains:
* default(n) = ite(epsilon1 = i, v, default(a))
n[diag(i)] = a[diag(i)]
* - for large domains:
* default(n) = default(a)
*/
bool solver::assert_default_store_axiom(app* store) {
m_stats.m_num_default_store_axiom++;
SASSERT(a.is_store(store));
SASSERT(store->get_num_args() >= 3);
expr_ref def1(m), def2(m);
bool prop = false;
unsigned num_args = store->get_num_args();
def1 = a.mk_default(store);
def2 = a.mk_default(store->get_arg(0));
bool is_new = false;
if (has_unitary_domain(store)) {
def2 = store->get_arg(num_args - 1);
}
else if (!has_large_domain(store)) {
//
// let A = store(B, i, v)
//
// Add:
// default(A) = ite(epsilon1 = i, v, default(B))
// A[diag(i)] = B[diag(i)]
//
expr_ref_vector eqs(m);
expr_ref_vector args1(m), args2(m);
args1.push_back(store->get_arg(0));
args2.push_back(store);
for (unsigned i = 1; i + 1 < num_args; ++i) {
expr* arg = store->get_arg(i);
sort* srt = m.get_sort(arg);
auto ep = mk_epsilon(srt);
eqs.push_back(m.mk_eq(ep.first, arg));
args1.push_back(m.mk_app(ep.second, arg));
args2.push_back(m.mk_app(ep.second, arg));
}
expr_ref eq(m.mk_and(eqs), m);
def2 = m.mk_ite(eq, store->get_arg(num_args - 1), def2);
app_ref sel1(m), sel2(m);
sel1 = a.mk_select(args1);
sel2 = a.mk_select(args2);
if (ctx.propagate(e_internalize(sel1), e_internalize(sel2), array_axiom()))
prop = true;
}
if (ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom()))
prop = true;
return prop;
}
/**
* Assert select(lambda xs . M, N1,.., Nk) -> M[N1/x1, ..., Nk/xk]
*/
bool solver::assert_select_lambda_axiom(app* select, expr* lambda) {
SASSERT(is_lambda(lambda));
SASSERT(a.is_select(select));
SASSERT(m.get_sort(lambda) == m.get_sort(select->get_arg(0)));
ptr_vector<expr> args(select->get_num_args(), select->get_args());
args[0] = lambda;
expr_ref alpha(a.mk_select(args), m);
expr_ref beta(alpha);
rewrite(beta);
return ctx.propagate(e_internalize(alpha), e_internalize(beta), array_axiom());
}
/**
\brief assert n1 = n2 => forall vars . (n1 vars) = (n2 vars)
*/
bool solver::assert_congruent_axiom(expr* e1, expr* e2) {
++m_stats.m_num_congruence_axiom;
sort* s = m.get_sort(e1);
unsigned dimension = get_array_arity(s);
expr_ref n1_eq_n2(m.mk_eq(e1, e2), m);
expr_ref_vector args1(m), args2(m);
args1.push_back(e1);
args2.push_back(e2);
svector<symbol> names;
sort_ref_vector sorts(m);
for (unsigned i = 0; i < dimension; i++) {
sort * srt = get_array_domain(s, i);
sorts.push_back(srt);
names.push_back(symbol(i));
expr * k = m.mk_var(dimension - i - 1, srt);
args1.push_back(k);
args2.push_back(k);
}
expr * sel1 = a.mk_select(dimension+1, args1.c_ptr());
expr * sel2 = a.mk_select(dimension+1, args2.c_ptr());
expr * eq = m.mk_eq(sel1, sel2);
expr_ref q(m.mk_forall(dimension, sorts.c_ptr(), names.c_ptr(), eq), m);
rewrite(q);
sat::literal fa_eq = b_internalize(q);
add_clause(~b_internalize(n1_eq_n2), fa_eq);
return true;
}
bool solver::has_unitary_domain(app* array_term) {
SASSERT(a.is_array(array_term));
sort* s = m.get_sort(array_term);
unsigned dim = get_array_arity(s);
for (unsigned i = 0; i < dim; ++i) {
sort* d = get_array_domain(s, i);
if (d->is_infinite() || d->is_very_big() || 1 != d->get_num_elements().size())
return false;
}
return true;
}
bool solver::has_large_domain(app* array_term) {
SASSERT(a.is_array(array_term));
sort* s = m.get_sort(array_term);
unsigned dim = get_array_arity(s);
rational sz(1);
for (unsigned i = 0; i < dim; ++i) {
sort* d = get_array_domain(s, i);
if (d->is_infinite() || d->is_very_big()) {
return true;
}
sz *= rational(d->get_num_elements().size(), rational::ui64());
if (sz >= rational(1 << 14)) {
return true;
}
}
return false;
}
std::pair<app*, func_decl*> solver::mk_epsilon(sort* s) {
app* eps = nullptr;
func_decl* diag = nullptr;
if (!m_sort2epsilon.find(s, eps)) {
eps = m.mk_fresh_const("epsilon", s);
ctx.push(ast2ast_trail<euf::solver, sort, app>(m_sort2epsilon, s, eps));
}
if (!m_sort2diag.find(s, diag)) {
diag = m.mk_fresh_func_decl("diag", 1, &s, s);
ctx.push(ast2ast_trail<euf::solver, sort, func_decl>(m_sort2diag, s, diag));
}
return std::make_pair(eps, diag);
}
void solver::push_parent_select_store_axioms(theory_var v) {
expr* e = var2expr(v);
if (!a.is_array(e))
return;
auto& d = get_var_data(v);
for (euf::enode* store : d.m_parents)
if (a.is_store(store->get_expr()))
for (euf::enode* sel : d.m_parents)
if (a.is_select(sel->get_expr()))
push_axiom(select_axiom(sel, store));
}
bool solver::add_delayed_axioms() {
if (!get_config().m_array_delay_exp_axiom)
return false;
unsigned num_vars = get_num_vars();
for (unsigned v = 0; v < num_vars; v++)
push_parent_select_store_axioms(v);
return unit_propagate();
}
bool solver::add_interface_equalities() {
sbuffer<theory_var> roots;
collect_shared_vars(roots);
bool prop = false;
for (unsigned i = roots.size(); i-- > 0; ) {
theory_var v1 = roots[i];
euf::enode* n1 = var2enode(v1);
for (unsigned j = i; j-- > 0; ) {
theory_var v2 = roots[j];
euf::enode* n2 = var2enode(v2);
if (m.get_sort(n1->get_expr()) != m.get_sort(n2->get_expr()))
continue;
expr_ref eq(m.mk_eq(n1->get_expr(), n2->get_expr()), m);
sat::literal lit = b_internalize(eq);
if (s().value(lit) == l_undef)
prop = true;
}
}
return prop;
}
void solver::collect_shared_vars(sbuffer<theory_var>& roots) {
ptr_buffer<euf::enode> to_unmark;
unsigned num_vars = get_num_vars();
for (unsigned i = 0; i < num_vars; i++) {
euf::enode * n = var2enode(i);
if (!a.is_array(n->get_expr())) {
continue;
}
euf::enode * r = n->get_root();
if (r->is_marked1()) {
continue;
}
// arrays used as indices in other arrays have to be treated as shared.
// issue #3532, #3529
//
if (ctx.is_shared(r) || is_select_arg(r)) {
TRACE("array", tout << "new shared var: #" << r->get_expr_id() << "\n";);
theory_var r_th_var = r->get_th_var(get_id());
SASSERT(r_th_var != euf::null_theory_var);
roots.push_back(r_th_var);
}
r->mark1();
to_unmark.push_back(r);
}
TRACE("array", tout << "collecting shared vars...\n" << unsigned_vector(roots.size(), (unsigned*)roots.c_ptr()) << "\n";);
for (auto* n : to_unmark)
n->unmark1();
}
bool solver::is_select_arg(euf::enode* r) {
for (euf::enode* n : euf::enode_parents(r))
if (a.is_select(n->get_expr()))
for (unsigned i = 1; i < n->num_args(); ++i)
if (r == n->get_arg(i)->get_root())
return true;
return false;
}
}

153
src/sat/smt/array_internalize.cpp Normal file
View file

@ -0,0 +1,153 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
array_internalize.cpp
Abstract:
Internalize routines for arrays
Author:
Nikolaj Bjorner (nbjorner) 2020-09-08
--*/
#include "sat/smt/array_solver.h"
#include "sat/smt/euf_solver.h"
namespace array {
sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
// TODO
return sat::null_literal;
}
void solver::internalize(expr* e, bool redundant) {
// TODO
}
euf::theory_var solver::mk_var(euf::enode* n) {
theory_var r = euf::th_euf_solver::mk_var(n);
m_find.mk_var();
ctx.attach_th_var(n, this, r);
m_var_data.push_back(alloc(var_data));
return r;
}
void solver::ensure_var(euf::enode* n) {
theory_var v = n->get_th_var(get_id());
if (v == euf::null_theory_var)
mk_var(n);
}
void solver::apply_sort_cnstr(euf::enode * n, sort * s) {
ensure_var(n);
}
void solver::internalize_store(euf::enode* n) {
if (get_config().m_array_laziness == 0)
add_parent(n->get_arg(0), n);
push_axiom(store_axiom(n));
}
void solver::internalize_select(euf::enode* n) {
if (get_config().m_array_laziness == 0)
add_parent(n->get_arg(0), n);
}
void solver::internalize_const(euf::enode* n) {
push_axiom(default_axiom(n));
set_prop_upward(n);
}
void solver::internalize_ext(euf::enode* n) {
push_axiom(extensionality_axiom(n));
}
void solver::internalize_default(euf::enode* n) {
add_parent(n->get_arg(0), n);
set_prop_upward(n);
}
void solver::internalize_map(euf::enode* n) {
for (auto* arg : euf::enode_args(n)) {
add_parent(arg, n);
set_prop_upward(arg);
}
push_axiom(default_axiom(n));
}
void solver::internalize_as_array(euf::enode* n) {
// TBD: delay verdict whether model is undetermined
ctx.unhandled_function(n->get_decl());
push_axiom(default_axiom(n));
}
bool solver::visited(expr* e) {
euf::enode* n = expr2enode(e);
return n && n->is_attached_to(get_id());
}
bool solver::visit(expr* e) {
if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
ctx.internalize(e, m_is_redundant);
ensure_var(expr2enode(e));
return true;
}
m_stack.push_back(sat::eframe(e));
return false;
}
bool solver::post_visit(expr* e, bool sign, bool root) {
euf::enode* n = expr2enode(e);
app* a = to_app(e);
SASSERT(!n || !n->is_attached_to(get_id()));
if (!n)
n = mk_enode(e, false);
SASSERT(!n->is_attached_to(get_id()));
theory_var v = mk_var(n);
for (auto* arg : euf::enode_args(n))
ensure_var(arg);
switch (a->get_decl_kind()) {
case OP_STORE:
internalize_store(n);
break;
case OP_SELECT:
internalize_select(n);
break;
case OP_CONST_ARRAY:
internalize_const(n);
break;
case OP_ARRAY_EXT:
internalize_ext(n);
break;
case OP_ARRAY_DEFAULT:
internalize_default(n);
break;
case OP_ARRAY_MAP:
internalize_map(n);
break;
case OP_AS_ARRAY:
internalize_as_array(n);
break;
case OP_SET_UNION:
case OP_SET_INTERSECT:
case OP_SET_DIFFERENCE:
case OP_SET_COMPLEMENT:
case OP_SET_SUBSET:
case OP_SET_HAS_SIZE:
case OP_SET_CARD:
ctx.unhandled_function(a->get_decl());
break;
default:
UNREACHABLE();
break;
}
return true;
}
}

77
src/sat/smt/array_model.cpp Normal file
View file

@ -0,0 +1,77 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
array_model.cpp
Abstract:
Theory plugin for arrays
Author:
Nikolaj Bjorner (nbjorner) 2020-09-08
--*/
#include "ast/ast_ll_pp.h"
#include "model/array_factory.h"
#include "sat/smt/array_solver.h"
#include "sat/smt/euf_solver.h"
namespace array {
void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
if (!a.is_array(n->get_expr())) {
dep.insert(n, nullptr);
return;
}
for (euf::enode* p : euf::enode_parents(n)) {
if (!a.is_select(p->get_expr()))
continue;
dep.add(n, p);
for (unsigned i = 1; i < p->num_args(); ++i)
dep.add(n, p->get_arg(i));
}
for (euf::enode* k : euf::enode_class(n))
if (a.is_const(k->get_expr()))
dep.add(n, k);
else if (a.is_default(k->get_expr()))
dep.add(n, k);
}
void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
SASSERT(a.is_array(n->get_expr()));
ptr_vector<expr> args;
sort* srt = m.get_sort(n->get_expr());
unsigned arity = get_array_arity(srt);
func_decl * f = mk_aux_decl_for_array_sort(m, srt);
func_interp * fi = alloc(func_interp, m, arity);
mdl.register_decl(f, fi);
for (euf::enode* p : euf::enode_parents(n)) {
if (!a.is_select(p->get_expr()))
continue;
args.reset();
for (unsigned i = 1; i < p->num_args(); ++i)
args.push_back(values.get(p->get_arg(i)->get_root_id()));
expr* value = values.get(p->get_root_id());
fi->insert_entry(args.c_ptr(), value);
}
if (!fi->get_else())
for (euf::enode* k : euf::enode_class(n))
if (a.is_const(k->get_expr()))
fi->set_else(k->get_arg(0)->get_root()->get_expr());
if (!fi->get_else())
for (euf::enode* k : euf::enode_parents(n))
if (a.is_default(k->get_expr()))
fi->set_else(k->get_root()->get_expr());
parameter p(f);
values.set(n->get_root_id(), m.mk_app(get_id(), OP_AS_ARRAY, 1, &p));
}
}

220
src/sat/smt/array_solver.cpp Normal file
View file

@ -0,0 +1,220 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
array_solver.h
Abstract:
Theory plugin for arrays
Author:
Nikolaj Bjorner (nbjorner) 2020-09-08
--*/
#include "ast/ast_ll_pp.h"
#include "sat/smt/array_solver.h"
#include "sat/smt/euf_solver.h"
namespace array {
solver::solver(euf::solver& ctx, theory_id id):
th_euf_solver(ctx, id),
a(m),
m_sort2epsilon(m),
m_sort2diag(m),
m_find(*this),
m_hash(*this),
m_eq(*this),
m_axioms(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_hash, m_eq)
{
m_constraint = alloc(sat::constraint_base);
m_constraint->initialize(m_constraint.get(), this);
}
sat::check_result solver::check() {
flet<bool> _is_redundant(m_is_redundant, true);
bool turn[2] = { false, false };
turn[s().rand()(2)] = true;
for (unsigned idx = 0; idx < 2; ++idx) {
if (turn[idx]) {
if (add_delayed_axioms())
return sat::CR_CONTINUE;
}
else {
if (add_interface_equalities())
return sat::CR_CONTINUE;
}
}
return sat::CR_DONE;
}
void solver::push() {
th_euf_solver::lazy_push();
}
void solver::pop(unsigned n) {
n = lazy_pop(n);
if (n == 0)
return;
m_var_data.resize(get_num_vars());
}
std::ostream& solver::display(std::ostream& out) const {
for (unsigned i = 0; i < get_num_vars(); ++i) {
out << var2enode(i)->get_expr_id() << " " << mk_bounded_pp(var2expr(i), m, 2) << "\n";
}
return out;
}
std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { return out; }
std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { return out; }
void solver::collect_statistics(statistics& st) const {
st.update("array store", m_stats.m_num_store_axiom);
st.update("array sel/store", m_stats.m_num_select_store_axiom);
st.update("array sel/const", m_stats.m_num_select_const_axiom);
st.update("array sel/map", m_stats.m_num_select_map_axiom);
st.update("array sel/as array", m_stats.m_num_select_as_array_axiom);
st.update("array def/map", m_stats.m_num_default_map_axiom);
st.update("array def/const", m_stats.m_num_default_const_axiom);
st.update("array def/store", m_stats.m_num_default_store_axiom);
st.update("array ext ax", m_stats.m_num_extensionality_axiom);
st.update("array cong ax", m_stats.m_num_congruence_axiom);
st.update("array exp ax2", m_stats.m_num_select_store_axiom_delayed);
st.update("array splits", m_stats.m_num_eq_splits);
}
euf::th_solver* solver::fresh(sat::solver* s, euf::solver& ctx) {
auto* result = alloc(solver, ctx, get_id());
ast_translation tr(m, ctx.get_manager());
for (unsigned i = 0; i < get_num_vars(); ++i) {
expr* e1 = var2expr(i);
expr* e2 = tr(e1);
euf::enode* n = ctx.get_enode(e2);
result->mk_var(n);
}
return result;
}
void solver::new_eq_eh(euf::th_eq const& eq) {
m_find.merge(eq.m_v1, eq.m_v2);
}
bool solver::unit_propagate() {
if (m_qhead == m_axiom_trail.size())
return false;
bool prop = false;
ctx.push(value_trail<euf::solver, unsigned>(m_qhead));
for (; m_qhead < m_axiom_trail.size() && !s().inconsistent(); ++m_qhead)
if (assert_axiom(m_qhead))
prop = true;
return prop;
}
void solver::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) {
euf::enode* n1 = var2enode(v1);
euf::enode* n2 = var2enode(v2);
SASSERT(n1->get_root() == n2->get_root());
SASSERT(n1->is_root() || n2->is_root());
SASSERT(v1 == find(v1));
expr* e1 = n1->get_expr();
expr* e2 = n2->get_expr();
auto& d1 = get_var_data(v1);
auto& d2 = get_var_data(v2);
if (d2.m_prop_upward && !d1.m_prop_upward)
set_prop_upward(v1);
if (a.is_array(e1))
for (euf::enode* parent : d2.m_parents) {
add_parent(v1, parent);
if (a.is_store(parent->get_expr()))
add_store(v1, parent);
}
if (is_lambda(e1) || is_lambda(e2))
push_axiom(congruence_axiom(n1, n2));
}
void solver::unmerge_eh(theory_var v1, theory_var v2) {
auto& p1 = get_var_data(v1).m_parents;
auto& p2 = get_var_data(v2).m_parents;
p1.shrink(p1.size() - p2.size());
}
void solver::add_store(theory_var v, euf::enode* store) {
SASSERT(a.is_store(store->get_expr()));
auto& d = get_var_data(v);
unsigned lambda_equiv_class_size = get_lambda_equiv_size(d);
if (get_config().m_array_always_prop_upward || lambda_equiv_class_size >= 1)
set_prop_upward(d);
for (euf::enode* n : d.m_parents)
if (a.is_select(n->get_expr()))
push_axiom(select_axiom(n, store));
if (get_config().m_array_always_prop_upward || lambda_equiv_class_size >= 1)
set_prop_upward(store);
}
void solver::add_parent(theory_var v_child, euf::enode* parent) {
SASSERT(parent->is_root());
get_var_data(v_child).m_parents.push_back(parent);
euf::enode* child = var2enode(v_child);
euf::enode* r = child->get_root();
expr* p = parent->get_expr();
expr* c = child->get_expr();
if (a.is_select(p) && parent->get_arg(0)->get_root() == r) {
if (a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c))
push_axiom(select_axiom(parent, child));
#if 0
if (!get_config().m_array_delay_exp_axiom && d.m_prop_upward) {
auto& d = get_var_data(v_child);
for (euf::enode* p2 : d.m_parents)
if (a.is_store(p2->get_expr()))
push_axiom(select_axiom(parent, p2));
}
#endif
}
else if (a.mk_default(p)) {
if (a.is_const(c) || a.is_store(c) || a.is_map(c) || a.is_as_array(c))
push_axiom(default_axiom(child));
}
}
void solver::set_prop_upward(theory_var v) {
auto& d = get_var_data(find(v));
if (!d.m_prop_upward) {
ctx.push(reset_flag_trail<euf::solver>(d.m_prop_upward));
d.m_prop_upward = true;
if (!get_config().m_array_delay_exp_axiom)
push_parent_select_store_axioms(v);
set_prop_upward(d);
}
}
void solver::set_prop_upward(euf::enode* n) {
if (a.is_store(n->get_expr()))
set_prop_upward(n->get_arg(0)->get_th_var(get_id()));
}
void solver::set_prop_upward(var_data& d) {
for (auto* p : d.m_parents)
set_prop_upward(p);
}
/**
\brief Return the size of the equivalence class for array terms
that can be expressed as \lambda i : Index . [.. (select a i) ..]
*/
unsigned solver::get_lambda_equiv_size(var_data const& d) {
unsigned sz = 0;
for (auto* p : d.m_parents)
if (a.is_store(p->get_expr()))
++sz;
return sz;
}
}

203
src/sat/smt/array_solver.h Normal file
View file

@ -0,0 +1,203 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
array_solver.h
Abstract:
Theory plugin for arrays
Author:
Nikolaj Bjorner (nbjorner) 2020-09-08
--*/
#pragma once
#include "ast/ast_trail.h"
#include "sat/smt/sat_th.h"
#include "ast/array_decl_plugin.h"
namespace euf {
class solver;
}
namespace array {
class solver : public euf::th_euf_solver {
typedef euf::theory_var theory_var;
typedef euf::theory_id theory_id;
typedef sat::literal literal;
typedef sat::bool_var bool_var;
typedef sat::literal_vector literal_vector;
typedef union_find<solver, euf::solver> array_union_find;
struct stats {
unsigned m_num_store_axiom, m_num_extensionality_axiom;
unsigned m_num_eq_splits, m_num_congruence_axiom;
unsigned m_num_select_store_axiom, m_num_select_as_array_axiom, m_num_select_map_axiom;
unsigned m_num_select_const_axiom, m_num_select_store_axiom_delayed;
unsigned m_num_default_store_axiom, m_num_default_map_axiom;
unsigned m_num_default_const_axiom, m_num_default_as_array_axiom;
void reset() { memset(this, 0, sizeof(*this)); }
stats() { reset(); }
};
// void log_drat(array_justification const& c);
struct var_data {
bool m_prop_upward{ false };
bool m_is_array{ false };
bool m_is_select{ false };
ptr_vector<euf::enode> m_parents;
var_data() {}
};
array_util a;
stats m_stats;
sat::solver* m_solver{ nullptr };
scoped_ptr_vector<var_data> m_var_data;
ast2ast_trailmap<sort, app> m_sort2epsilon;
ast2ast_trailmap<sort, func_decl> m_sort2diag;
obj_map<sort, func_decl_ref_vector*> m_sort2diff;
array_union_find m_find;
sat::solver& s() { return *m_solver; }
theory_var find(theory_var v) { return m_find.find(v); }
// internalize
bool visit(expr* e) override;
bool visited(expr* e) override;
bool post_visit(expr* e, bool sign, bool root) override;
void ensure_var(euf::enode* n);
void internalize_store(euf::enode* n);
void internalize_select(euf::enode* n);
void internalize_const(euf::enode* n);
void internalize_ext(euf::enode* n);
void internalize_default(euf::enode* n);
void internalize_map(euf::enode* n);
void internalize_as_array(euf::enode* n);
// axioms
struct axiom_record {
enum class kind_t {
is_store,
is_select,
is_extensionality,
is_default,
is_congruence
};
kind_t m_kind;
euf::enode* n;
euf::enode* select;
axiom_record(kind_t k, euf::enode* n, euf::enode* select = nullptr) : m_kind(k), n(n), select(select) {}
struct hash {
solver& s;
hash(solver& s) :s(s) {}
unsigned operator()(unsigned idx) const {
auto const& r = s.m_axiom_trail[idx];
return mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select ? r.select->get_expr_id() : 1);
}
};
struct eq {
solver& s;
eq(solver& s) :s(s) {}
unsigned operator()(unsigned a, unsigned b) const {
auto const& p = s.m_axiom_trail[a];
auto const& r = s.m_axiom_trail[b];
return p.n == r.n && p.select == r.select && p.m_kind == r.m_kind;
}
};
};
typedef hashtable<unsigned, axiom_record::hash, axiom_record::eq> axiom_table_t;
axiom_record::hash m_hash;
axiom_record::eq m_eq;
axiom_table_t m_axioms;
svector<axiom_record> m_axiom_trail;
unsigned m_qhead { 0 };
void push_axiom(axiom_record const& r);
bool assert_axiom(unsigned idx);
axiom_record select_axiom(euf::enode* s, euf::enode* n) { return axiom_record(axiom_record::kind_t::is_select, n, s); }
axiom_record default_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_default, n); }
axiom_record store_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_store, n); }
axiom_record extensionality_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_extensionality, n); }
axiom_record congruence_axiom(euf::enode* a, euf::enode* b) { return axiom_record(axiom_record::kind_t::is_congruence, a, b); }
scoped_ptr<sat::constraint_base> m_constraint;
sat::ext_justification_idx array_axiom() { return m_constraint->to_index(); }
bool assert_store_axiom(app* _e);
bool assert_select_store_axiom(app* select, app* store);
bool assert_select_const_axiom(app* select, app* cnst);
bool assert_select_as_array_axiom(app* select, app* arr);
bool assert_select_map_axiom(app* select, app* map);
bool assert_select_lambda_axiom(app* select, expr* lambda);
bool assert_extensionality(expr* e1, expr* e2);
bool assert_default_map_axiom(app* map);
bool assert_default_const_axiom(app* cnst);
bool assert_default_store_axiom(app* store);
bool assert_default_as_array_axiom(app* as_array);
bool assert_congruent_axiom(expr* e1, expr* e2);
bool add_delayed_axioms();
bool has_unitary_domain(app* array_term);
bool has_large_domain(app* array_term);
std::pair<app*, func_decl*> mk_epsilon(sort* s);
void collect_shared_vars(sbuffer<theory_var>& roots);
bool add_interface_equalities();
bool is_select_arg(euf::enode* r);
// solving
void add_parent(theory_var v_child, euf::enode* parent);
void add_parent(euf::enode* child, euf::enode* parent) { add_parent(child->get_th_var(get_id()), parent); }
void add_store(theory_var v, euf::enode* store);
void set_prop_upward(theory_var v);
void set_prop_upward(var_data& d);
void set_prop_upward(euf::enode* n);
void push_parent_select_store_axioms(theory_var v);
unsigned get_lambda_equiv_size(var_data const& d);
var_data& get_var_data(euf::enode* n) { return get_var_data(n->get_th_var(get_id())); }
var_data& get_var_data(theory_var v) { return *m_var_data[v]; }
// invariants
public:
solver(euf::solver& ctx, theory_id id);
~solver() override {}
void set_solver(sat::solver* s) override { m_solver = s; }
bool is_external(bool_var v) override { return false; }
bool propagate(literal l, sat::ext_constraint_idx idx) override { UNREACHABLE(); return false; }
void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override {}
void asserted(literal l) override {}
sat::check_result check() override;
void push() override;
void pop(unsigned n) override;
std::ostream& display(std::ostream& out) const override;
std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
void collect_statistics(statistics& st) const override;
euf::th_solver* fresh(sat::solver* s, euf::solver& ctx) override;
void new_eq_eh(euf::th_eq const& eq) override;
bool unit_propagate() override;
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
void add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
void internalize(expr* e, bool redundant) override;
euf::theory_var mk_var(euf::enode* n) override;
void apply_sort_cnstr(euf::enode* n, sort* s) override;
void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
void unmerge_eh(theory_var v1, theory_var v2);
};
}

22
src/sat/smt/bv_internalize.cpp
View file

@ -62,7 +62,7 @@ namespace bv {
m_zero_one_bits.push_back(zero_one_bits());
ctx.attach_th_var(n, this, r);
TRACE("bv", tout << "mk-var: " << r << " " << n->get_owner_id() << " " << mk_pp(n->get_owner(), m) << "\n";);
TRACE("bv", tout << "mk-var: " << r << " " << n->get_expr_id() << " " << mk_pp(n->get_expr(), m) << "\n";);
return r;
}
@ -100,17 +100,9 @@ namespace bv {
app* a = to_app(e);
SASSERT(!n || !n->is_attached_to(get_id()));
if (!n) {
m_args.reset();
if (get_config().m_bv_reflect || m.is_considered_uninterpreted(a->get_decl())) {
for (expr* arg : *a)
m_args.push_back(expr2enode(arg));
}
DEBUG_CODE(for (auto* n : m_args) VERIFY(n););
n = ctx.mk_enode(e, m_args.size(), m_args.c_ptr());
SASSERT(!n->is_attached_to(get_id()));
ctx.attach_node(n);
}
bool suppress_args = !get_config().m_bv_reflect && !m.is_considered_uninterpreted(a->get_decl());
if (!n)
n = mk_enode(e, suppress_args);
SASSERT(!n->is_attached_to(get_id()));
theory_var v = mk_var(n);
@ -196,14 +188,14 @@ namespace bv {
theory_var v = n->get_th_var(get_id());
if (v == euf::null_theory_var) {
v = mk_var(n);
if (bv.is_bv(n->get_owner()))
if (bv.is_bv(n->get_expr()))
mk_bits(v);
}
return v;
}
euf::enode* solver::get_arg(euf::enode* n, unsigned idx) {
app* o = to_app(n->get_owner());
app* o = to_app(n->get_expr());
return ctx.get_enode(o->get_arg(idx));
}
@ -280,7 +272,7 @@ namespace bv {
}
unsigned solver::get_bv_size(euf::enode* n) {
return bv.get_bv_size(n->get_owner());
return bv.get_bv_size(n->get_expr());
}
unsigned solver::get_bv_size(theory_var v) {

14
src/sat/smt/bv_solver.cpp
View file

@ -153,7 +153,7 @@ namespace bv {
out.width(4);
out << e->get_id() << " -> ";
out.width(4);
out << var2enode(find(v))->get_owner_id();
out << var2enode(find(v))->get_expr_id();
out << std::right;
out.flush();
atom* a = nullptr;
@ -168,7 +168,7 @@ namespace bv {
else if (m.is_bool(e) && (a = m_bool_var2atom.get(expr2literal(e).var(), nullptr))) {
if (a->is_bit()) {
for (var_pos vp : a->to_bit())
out << " " << var2enode(vp.first)->get_owner_id() << "[" << vp.second << "]";
out << " " << var2enode(vp.first)->get_expr_id() << "[" << vp.second << "]";
}
else
out << "def-atom";
@ -277,7 +277,7 @@ namespace bv {
literal bit1 = m_bits[v1][idx];
lbool val = s().value(bit1);
TRACE("bv", tout << "propagating v" << v1 << " #" << var2enode(v1)->get_owner_id() << "[" << idx << "] = " << val << "\n";);
TRACE("bv", tout << "propagating v" << v1 << " #" << var2enode(v1)->get_expr_id() << "[" << idx << "] = " << val << "\n";);
if (val == l_undef)
return;
@ -287,7 +287,7 @@ namespace bv {
for (theory_var v2 = m_find.next(v1); v2 != v1 && !s().inconsistent(); v2 = m_find.next(v2)) {
literal bit2 = m_bits[v2][idx];
SASSERT(m_bits[v1][idx] != ~m_bits[v2][idx]);
TRACE("bv", tout << "propagating #" << var2enode(v2)->get_owner_id() << "[" << idx << "] = " << s().value(bit2) << "\n";);
TRACE("bv", tout << "propagating #" << var2enode(v2)->get_expr_id() << "[" << idx << "] = " << s().value(bit2) << "\n";);
if (val == l_false)
bit2.neg();
@ -454,8 +454,8 @@ namespace bv {
bool solver::check_model(sat::model const& m) const { return true; }
unsigned solver::max_var(unsigned w) const { return w; }
void solver::add_value(euf::enode* n, expr_ref_vector& values) {
SASSERT(bv.is_bv(n->get_owner()));
void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
SASSERT(bv.is_bv(n->get_expr()));
theory_var v = n->get_th_var(get_id());
rational val;
unsigned i = 0;
@ -477,7 +477,7 @@ namespace bv {
}
void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_owner_id() << " v" << v2 << " #" << var2enode(v2)->get_owner_id() << "\n";);
TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_expr_id() << " v" << v2 << " #" << var2enode(v2)->get_expr_id() << "\n";);
if (!merge_zero_one_bits(r1, r2)) {
TRACE("bv", tout << "conflict detected\n";);
return; // conflict was detected

2
src/sat/smt/bv_solver.h
View file

@ -268,7 +268,7 @@ namespace bv {
void new_eq_eh(euf::th_eq const& eq) override;
bool unit_propagate() override;
void add_value(euf::enode* n, expr_ref_vector& values) override;
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
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 { return false; }

83
src/sat/smt/euf_internalize.cpp
View file

@ -23,7 +23,7 @@ namespace euf {
void solver::internalize(expr* e, bool redundant) {
if (si.is_bool_op(e))
attach_lit(si.internalize(e, redundant), e);
attach_lit(si.internalize(e, redundant), e);
else if (auto* ext = get_solver(e))
ext->internalize(e, redundant);
else
@ -32,8 +32,8 @@ namespace euf {
}
sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
if (si.is_bool_op(e))
return attach_lit(si.internalize(e, redundant), e);
if (si.is_bool_op(e))
return attach_lit(si.internalize(e, redundant), e);
if (auto* ext = get_solver(e))
return ext->internalize(e, sign, root, redundant);
if (!visit_rec(m, e, sign, root, redundant))
@ -82,11 +82,11 @@ namespace euf {
}
void solver::attach_node(euf::enode* n) {
expr* e = n->get_owner();
expr* e = n->get_expr();
if (!m.is_bool(e))
log_node(e);
else
attach_lit(literal(si.add_bool_var(e), false), e);
else
attach_lit(literal(si.add_bool_var(e), false), e);
if (!m.is_bool(e) && m.get_sort(e)->get_family_id() != null_family_id) {
auto* e_ext = get_solver(e);
@ -143,7 +143,7 @@ namespace euf {
sat::literal_vector lits;
for (unsigned i = 0; i < sz; ++i) {
for (unsigned j = i + 1; j < sz; ++j) {
expr_ref eq(m.mk_eq(args[i]->get_owner(), args[j]->get_owner()), m);
expr_ref eq(m.mk_eq(args[i]->get_expr(), args[j]->get_expr()), m);
sat::literal lit = internalize(eq, false, false, m_is_redundant);
lits.push_back(lit);
}
@ -184,11 +184,11 @@ namespace euf {
if (sz <= 1) {
s().mk_clause(0, nullptr, st);
return;
}
}
if (sz <= distinct_max_args) {
for (unsigned i = 0; i < sz; ++i) {
for (unsigned j = i + 1; j < sz; ++j) {
expr_ref eq(m.mk_eq(args[i]->get_owner(), args[j]->get_owner()), m);
expr_ref eq(m.mk_eq(args[i]->get_expr(), args[j]->get_expr()), m);
sat::literal lit = internalize(eq, true, false, m_is_redundant);
s().add_clause(1, &lit, st);
}
@ -213,9 +213,9 @@ namespace euf {
}
void solver::axiomatize_basic(enode* n) {
expr* e = n->get_owner();
expr* e = n->get_expr();
sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id());
if (m.is_ite(e)) {
if (m.is_ite(e)) {
app* a = to_app(e);
expr* c = a->get_arg(0);
expr* th = a->get_arg(1);
@ -237,7 +237,7 @@ namespace euf {
unsigned sz = n->num_args();
for (unsigned i = 0; i < sz; ++i) {
for (unsigned j = i + 1; j < sz; ++j) {
expr_ref eq(m.mk_eq(n->get_arg(i)->get_owner(), n->get_arg(j)->get_owner()), m);
expr_ref eq(m.mk_eq(n->get_arg(i)->get_expr(), n->get_arg(j)->get_expr()), m);
eqs.push_back(eq);
}
}
@ -247,8 +247,65 @@ namespace euf {
sat::literal lits1[2] = { ~dist, ~some_eq };
sat::literal lits2[2] = { dist, some_eq };
s().add_clause(2, lits1, st);
s().add_clause(2, lits2, st);
s().add_clause(2, lits2, st);
}
}
bool solver::is_shared(enode* n) const {
n = n->get_root();
if (m.is_ite(n->get_expr()))
return true;
theory_id th_id = null_theory_id;
for (auto p : euf::enode_th_vars(n)) {
if (th_id == null_theory_id)
th_id = p.get_id();
else
return true;
}
if (th_id == null_theory_id)
return false;
// the variable is shared if the equivalence class of n
// contains a parent application.
for (euf::enode* parent : euf::enode_parents(n)) {
app* p = to_app(parent->get_expr());
family_id fid = p->get_family_id();
if (fid != th_id && fid != m.get_basic_family_id())
return true;
}
// Some theories implement families of theories. Examples:
// Arrays and Tuples. For example, array theory is a
// parametric theory, that is, it implements several theories:
// (array int int), (array int (array int int)), ...
//
// Example:
//
// a : (array int int)
// b : (array int int)
// x : int
// y : int
// v : int
// w : int
// A : (array (array int int) int)
//
// assert (= b (store a x v))
// assert (= b (store a y w))
// assert (not (= x y))
// assert (not (select A a))
// assert (not (select A b))
// check
//
// In the example above, 'a' and 'b' are shared variables between
// the theories of (array int int) and (array (array int int) int).
// Remark: The inconsistency is not going to be detected if they are
// not marked as shared.
return true;
// TODO
// return get_theory(th_id)->is_shared(l->get_var());
}
}

4
src/sat/smt/euf_invariant.cpp
View file

@ -26,14 +26,14 @@ namespace euf {
void solver::check_eqc_bool_assignment() const {
for (enode* n : m_egraph.nodes()) {
VERIFY(!m.is_bool(n->get_owner()) ||
VERIFY(!m.is_bool(n->get_expr()) ||
s().value(get_literal(n)) == s().value(get_literal(n->get_root())));
}
}
void solver::check_missing_bool_enode_propagation() const {
for (enode* n : m_egraph.nodes())
if (m.is_bool(n->get_owner()) && l_undef == s().value(get_literal(n))) {
if (m.is_bool(n->get_expr()) && l_undef == s().value(get_literal(n))) {
if (!n->is_root()) {
VERIFY(l_undef == s().value(get_literal(n->get_root())));
}

12
src/sat/smt/euf_model.cpp
View file

@ -48,7 +48,7 @@ namespace euf {
deps.insert(n, nullptr);
continue;
}
auto* mb = get_solver(n->get_owner());
auto* mb = get_solver(n->get_expr());
if (mb)
mb->add_dep(n, deps);
else
@ -56,13 +56,13 @@ namespace euf {
}
}
void solver::dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref const& mdl) {
void solver::dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref& 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();
expr* e = n->get_expr();
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()));
@ -96,13 +96,13 @@ namespace euf {
}
auto* mb = get_solver(e);
if (mb)
mb->add_value(n, values);
mb->add_value(n, *mdl, 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 ((mb = get_solver(m.get_sort(e))))
mb->add_value(n, values);
mb->add_value(n, *mdl, values);
else {
IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n");
}
@ -112,7 +112,7 @@ namespace euf {
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();
expr* e = n->get_expr();
if (!is_app(e))
continue;
app* a = to_app(e);

12
src/sat/smt/euf_solver.cpp
View file

@ -138,8 +138,11 @@ namespace euf {
m_egraph.explain_eq<size_t>(m_explain, a, b);
}
void solver::propagate(enode* a, enode* b, ext_justification_idx idx) {
bool solver::propagate(enode* a, enode* b, ext_justification_idx idx) {
if (a->get_root() == b->get_root())
return false;
m_egraph.merge(a, b, to_ptr(idx));
return true;
}
@ -235,7 +238,7 @@ namespace euf {
euf::enode_bool_pair p = m_egraph.get_literal();
euf::enode* n = p.first;
bool is_eq = p.second;
expr* e = n->get_owner();
expr* e = n->get_expr();
expr* a = nullptr, *b = nullptr;
bool_var v = si.to_bool_var(e);
SASSERT(m.is_bool(e));
@ -247,7 +250,7 @@ namespace euf {
lit = literal(v, false);
}
else {
a = e, b = n->get_root()->get_owner();
a = e, b = n->get_root()->get_expr();
SASSERT(m.is_true(b) || m.is_false(b));
cnstr = lit_constraint().to_index();
lit = literal(v, m.is_false(b));
@ -548,7 +551,7 @@ namespace euf {
}
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()));
fmls.push_back(m.mk_eq(n->get_expr(), n->get_root()->get_expr()));
}
return true;
}
@ -560,4 +563,5 @@ namespace euf {
return false;
return true;
}
}

13
src/sat/smt/euf_solver.h
View file

@ -20,6 +20,7 @@ Author:
#include "util/trail.h"
#include "ast/ast_translation.h"
#include "ast/euf/euf_egraph.h"
#include "ast/rewriter/th_rewriter.h"
#include "tactic/model_converter.h"
#include "sat/sat_extension.h"
#include "sat/smt/atom2bool_var.h"
@ -83,6 +84,7 @@ namespace euf {
euf::egraph m_egraph;
euf_trail_stack m_trail;
stats m_stats;
th_rewriter m_rewriter;
func_decl_ref_vector m_unhandled_functions;
@ -129,13 +131,12 @@ namespace euf {
th_solver* get_solver(expr* e);
th_solver* get_solver(sat::bool_var v);
void add_solver(family_id fid, th_solver* th);
void unhandled_function(func_decl* f);
void init_ackerman();
// model building
bool include_func_interp(func_decl* f);
void register_macros(model& mdl);
void dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref const& mdl);
void dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref& mdl);
void collect_dependencies(deps_t& deps);
void values2model(deps_t const& deps, expr_ref_vector const& values, model_ref& mdl);
@ -166,6 +167,7 @@ namespace euf {
si(si),
m_egraph(m),
m_trail(*this),
m_rewriter(m),
m_unhandled_functions(m),
m_solver(nullptr),
m_lookahead(nullptr),
@ -201,7 +203,7 @@ namespace euf {
ast_manager& get_manager() { return m; }
enode* get_enode(expr* e) { return m_egraph.find(e); }
sat::literal get_literal(expr* e) const { return literal(si.to_bool_var(e), false); }
sat::literal get_literal(enode* e) const { return get_literal(e->get_owner()); }
sat::literal get_literal(enode* e) const { return get_literal(e->get_expr()); }
smt_params const& get_config() { return m_config; }
region& get_region() { return m_trail.get_region(); }
template <typename C>
@ -217,7 +219,7 @@ namespace euf {
bool is_external(bool_var v) override;
bool propagate(literal l, ext_constraint_idx idx) override;
bool unit_propagate() override;
void propagate(enode* a, enode* b, ext_justification_idx);
bool propagate(enode* a, enode* b, ext_justification_idx);
bool set_root(literal l, literal r) override;
void flush_roots() override;
@ -262,6 +264,9 @@ namespace euf {
void attach_node(euf::enode* n);
euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, n, args); }
expr* bool_var2expr(sat::bool_var v) { return m_var2expr.get(v, nullptr); }
void unhandled_function(func_decl* f);
th_rewriter& get_rewriter() { return m_rewriter; }
bool is_shared(euf::enode* n) const;
void update_model(model_ref& mdl);

19
src/sat/smt/sat_th.cpp
View file

@ -139,4 +139,23 @@ namespace euf {
ctx.s().add_clause(4, lits, sat::status::th(m_is_redundant, get_id()));
}
euf::enode* th_euf_solver::mk_enode(expr* e, bool suppress_args) {
m_args.reset();
if (!suppress_args)
for (expr* arg : *to_app(e))
m_args.push_back(expr2enode(arg));
euf::enode* n = ctx.mk_enode(e, m_args.size(), m_args.c_ptr());
ctx.attach_node(n);
if (m.is_bool(e)) {
sat::bool_var v = ctx.get_si().add_bool_var(e);
NOT_IMPLEMENTED_YET();
// TODO: ctx.attach_lit(literal(v, false), e);
}
return n;
}
void th_euf_solver::rewrite(expr_ref& a) {
ctx.get_rewriter()(a);
}
}

15
src/sat/smt/sat_th.h
View file

@ -19,6 +19,7 @@ Author:
#include "util/top_sort.h"
#include "sat/smt/sat_smt.h"
#include "ast/euf/euf_egraph.h"
#include "model/model.h"
#include "smt/params/smt_params.h"
namespace euf {
@ -44,6 +45,8 @@ namespace euf {
virtual void internalize(expr* e, bool redundant) = 0;
sat::literal b_internalize(expr* e) { return internalize(e, false, false, m_is_redundant); }
/**
\brief Apply (interpreted) sort constraints on the given enode.
*/
@ -55,7 +58,7 @@ namespace euf {
public:
virtual ~th_decompile() {}
virtual bool to_formulas(std::function<expr_ref(sat::literal)>& lit2expr, expr_ref_vector& fmls) = 0;
virtual bool to_formulas(std::function<expr_ref(sat::literal)>& lit2expr, expr_ref_vector& fmls) { return false; }
};
class th_model_builder {
@ -67,7 +70,7 @@ namespace euf {
\brief compute the value for enode \c n and store the value in \c values
for the root of the class of \c n.
*/
virtual void add_value(euf::enode* n, expr_ref_vector& values) {}
virtual void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {}
/**
\brief compute dependencies for node n
@ -113,10 +116,16 @@ namespace euf {
void add_unit(sat::literal lit);
void add_clause(sat::literal lit) { add_unit(lit); }
void add_clause(sat::literal a, sat::literal b);
void add_clause(sat::literal a, sat::literal b, sat::literal c);
void add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d);
euf::enode* e_internalize(expr* e) { internalize(e, m_is_redundant); return expr2enode(e); }
euf::enode* mk_enode(expr* e, bool suppress_args);
void rewrite(expr_ref& a);
public:
th_euf_solver(euf::solver& ctx, euf::theory_id id);
virtual ~th_euf_solver() {}
@ -124,7 +133,7 @@ namespace euf {
unsigned get_num_vars() const { return m_var2enode.size();}
enode* expr2enode(expr* e) const;
enode* var2enode(theory_var v) const { return m_var2enode[v]; }
expr* var2expr(theory_var v) const { return var2enode(v)->get_owner(); }
expr* var2expr(theory_var v) const { return var2enode(v)->get_expr(); }
expr* bool_var2expr(sat::bool_var v) const;
expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }