mirror of
https://github.com/Z3Prover/z3
synced 2025-08-15 15:25:26 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4
This commit is contained in:
Christoph M. Wintersteiger
commit
8b47a84598
56 changed files with 5500 additions and 887 deletions
|
|
@ -1382,7 +1382,8 @@ namespace smt {
|
|||
bool_var v = l.var();
|
||||
bool_var_data & d = get_bdata(v);
|
||||
lbool val = get_assignment(v);
|
||||
TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode() << " " << l << "\n";);
|
||||
TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode()
|
||||
<< " tag: " << (d.is_eq()?"eq":"") << (d.is_theory_atom()?"th":"") << (d.is_quantifier()?"q":"") << " " << l << "\n";);
|
||||
SASSERT(val != l_undef);
|
||||
if (d.is_enode())
|
||||
propagate_bool_var_enode(v);
|
||||
|
|
|
|||
|
|
@ -90,7 +90,9 @@ namespace smt {
|
|||
sort * s = m_manager.get_sort(r->get_owner());
|
||||
model_value_proc * proc = 0;
|
||||
if (m_manager.is_bool(s)) {
|
||||
SASSERT(m_context->get_assignment(r) == l_true || m_context->get_assignment(r) == l_false);
|
||||
CTRACE("func_interp_bug", m_context->get_assignment(r) == l_undef,
|
||||
tout << mk_pp(r->get_owner(), m_manager) << "\n";);
|
||||
SASSERT(m_context->get_assignment(r) != l_undef);
|
||||
if (m_context->get_assignment(r) == l_true)
|
||||
proc = alloc(expr_wrapper_proc, m_manager.mk_true());
|
||||
else
|
||||
|
|
@ -359,6 +361,7 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
enode * child = d.get_enode();
|
||||
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_owner(), m_manager) << "): " << mk_pp(child->get_owner(), m_manager) << " " << mk_pp(child->get_root()->get_owner(), m_manager) << "\n";);
|
||||
child = child->get_root();
|
||||
app * val = 0;
|
||||
m_root2value.find(child, val);
|
||||
|
|
|
|||
|
|
@ -815,7 +815,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void setup::setup_seq() {
|
||||
m_context.register_plugin(alloc(theory_seq_empty, m_manager));
|
||||
m_context.register_plugin(alloc(theory_seq, m_manager));
|
||||
}
|
||||
|
||||
void setup::setup_card() {
|
||||
|
|
|
|||
|
|
@ -1056,6 +1056,10 @@ namespace smt {
|
|||
// -----------------------------------
|
||||
virtual bool get_value(enode * n, expr_ref & r);
|
||||
|
||||
bool get_lower(enode* n, expr_ref& r);
|
||||
bool get_upper(enode* n, expr_ref& r);
|
||||
bool to_expr(inf_numeral const& val, bool is_int, expr_ref& r);
|
||||
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
|
|
@ -1071,6 +1075,8 @@ namespace smt {
|
|||
unsigned num_eqs, enode_pair const * eqs,
|
||||
unsigned num_params, parameter* params);
|
||||
inf_eps_rational<inf_rational> conflict_minimize();
|
||||
|
||||
|
||||
private:
|
||||
virtual expr_ref mk_gt(theory_var v);
|
||||
|
||||
|
|
|
|||
|
|
@ -2157,6 +2157,7 @@ namespace smt {
|
|||
enode * r = n->get_root();
|
||||
enode_vector::const_iterator it = r->begin_parents();
|
||||
enode_vector::const_iterator end = r->end_parents();
|
||||
TRACE("shared", tout << get_context().get_scope_level() << " " << v << " " << r->get_num_parents() << "\n";);
|
||||
for (; it != end; ++it) {
|
||||
enode * parent = *it;
|
||||
app * o = parent->get_owner();
|
||||
|
|
|
|||
|
|
@ -3089,20 +3089,35 @@ namespace smt {
|
|||
// -----------------------------------
|
||||
|
||||
template<typename Ext>
|
||||
bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) {
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
if (v == null_theory_var) {
|
||||
// TODO: generate fresh value different from other get_value(v) for all v.
|
||||
return false;
|
||||
bool theory_arith<Ext>::to_expr(inf_numeral const& val, bool is_int, expr_ref & r) {
|
||||
if (val.get_infinitesimal().is_zero()) {
|
||||
numeral _val = val.get_rational();
|
||||
r = m_util.mk_numeral(_val.to_rational(), is_int);
|
||||
return true;
|
||||
}
|
||||
inf_numeral const & val = get_value(v);
|
||||
if (!val.get_infinitesimal().is_zero()) {
|
||||
// TODO: add support for infinitesimals
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
numeral _val = val.get_rational();
|
||||
r = m_util.mk_numeral(_val.to_rational(), is_int(v));
|
||||
return true;
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) {
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
return v != null_theory_var && to_expr(get_value(v), is_int(v), r);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool theory_arith<Ext>::get_lower(enode * n, expr_ref & r) {
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
bound* b = (v == null_theory_var) ? 0 : lower(v);
|
||||
return b && to_expr(b->get_value(), is_int(v), r);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool theory_arith<Ext>::get_upper(enode * n, expr_ref & r) {
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
bound* b = (v == null_theory_var) ? 0 : upper(v);
|
||||
return b && to_expr(b->get_value(), is_int(v), r);
|
||||
}
|
||||
|
||||
// -----------------------------------
|
||||
|
|
|
|||
|
|
@ -424,6 +424,39 @@ namespace smt {
|
|||
|
||||
};
|
||||
|
||||
void theory_bv::add_fixed_eq(theory_var v1, theory_var v2) {
|
||||
++m_stats.m_num_eq_dynamic;
|
||||
if (v1 > v2) {
|
||||
std::swap(v1, v2);
|
||||
}
|
||||
unsigned sz = get_bv_size(v1);
|
||||
ast_manager& m = get_manager();
|
||||
context & ctx = get_context();
|
||||
app* o1 = get_enode(v1)->get_owner();
|
||||
app* o2 = get_enode(v2)->get_owner();
|
||||
literal oeq = mk_eq(o1, o2, true);
|
||||
TRACE("bv",
|
||||
tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " "
|
||||
<< ctx.get_scope_level() << "\n";);
|
||||
literal_vector eqs;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
literal l1 = m_bits[v1][i];
|
||||
literal l2 = m_bits[v2][i];
|
||||
expr_ref e1(m), e2(m);
|
||||
e1 = mk_bit2bool(o1, i);
|
||||
e2 = mk_bit2bool(o2, i);
|
||||
literal eq = mk_eq(e1, e2, true);
|
||||
ctx.mk_th_axiom(get_id(), l1, ~l2, ~eq);
|
||||
ctx.mk_th_axiom(get_id(), ~l1, l2, ~eq);
|
||||
ctx.mk_th_axiom(get_id(), l1, l2, eq);
|
||||
ctx.mk_th_axiom(get_id(), ~l1, ~l2, eq);
|
||||
ctx.mk_th_axiom(get_id(), eq, ~oeq);
|
||||
eqs.push_back(~eq);
|
||||
}
|
||||
eqs.push_back(oeq);
|
||||
ctx.mk_th_axiom(get_id(), eqs.size(), eqs.c_ptr());
|
||||
}
|
||||
|
||||
void theory_bv::fixed_var_eh(theory_var v) {
|
||||
numeral val;
|
||||
bool r = get_fixed_value(v, val);
|
||||
|
|
@ -443,7 +476,9 @@ namespace smt {
|
|||
display_var(tout, v);
|
||||
display_var(tout, v2););
|
||||
m_stats.m_num_th2core_eq++;
|
||||
ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));
|
||||
add_fixed_eq(v, v2);
|
||||
ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));
|
||||
m_fixed_var_table.insert(key, v2);
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
|
@ -1177,6 +1212,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void theory_bv::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
|
||||
|
||||
m_stats.m_num_bit2core++;
|
||||
context & ctx = get_context();
|
||||
SASSERT(ctx.get_assignment(antecedent) == l_true);
|
||||
|
|
@ -1192,6 +1228,12 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
ctx.assign(consequent, mk_bit_eq_justification(v1, v2, consequent, antecedent));
|
||||
literal_vector lits;
|
||||
lits.push_back(~consequent);
|
||||
lits.push_back(antecedent);
|
||||
lits.push_back(~mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false));
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
|
||||
if (m_wpos[v2] == idx)
|
||||
find_wpos(v2);
|
||||
// REMARK: bit_eq_justification is marked as a theory_bv justification.
|
||||
|
|
@ -1601,6 +1643,7 @@ namespace smt {
|
|||
st.update("bv dynamic diseqs", m_stats.m_num_diseq_dynamic);
|
||||
st.update("bv bit2core", m_stats.m_num_bit2core);
|
||||
st.update("bv->core eq", m_stats.m_num_th2core_eq);
|
||||
st.update("bv dynamic eqs", m_stats.m_num_eq_dynamic);
|
||||
}
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
|
|
|
|||
|
|
@ -34,6 +34,7 @@ namespace smt {
|
|||
|
||||
struct theory_bv_stats {
|
||||
unsigned m_num_diseq_static, m_num_diseq_dynamic, m_num_bit2core, m_num_th2core_eq, m_num_conflicts;
|
||||
unsigned m_num_eq_dynamic;
|
||||
void reset() { memset(this, 0, sizeof(theory_bv_stats)); }
|
||||
theory_bv_stats() { reset(); }
|
||||
};
|
||||
|
|
@ -124,8 +125,9 @@ namespace smt {
|
|||
typedef std::pair<numeral, unsigned> value_sort_pair;
|
||||
typedef pair_hash<obj_hash<numeral>, unsigned_hash> value_sort_pair_hash;
|
||||
typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
|
||||
value2var m_fixed_var_table;
|
||||
|
||||
value2var m_fixed_var_table;
|
||||
|
||||
literal_vector m_tmp_literals;
|
||||
svector<var_pos> m_prop_queue;
|
||||
bool m_approximates_large_bvs;
|
||||
|
|
@ -166,6 +168,7 @@ namespace smt {
|
|||
void find_wpos(theory_var v);
|
||||
friend class fixed_eq_justification;
|
||||
void fixed_var_eh(theory_var v);
|
||||
void add_fixed_eq(theory_var v1, theory_var v2);
|
||||
bool get_fixed_value(theory_var v, numeral & result) const;
|
||||
void internalize_num(app * n);
|
||||
void internalize_add(app * n);
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -25,15 +25,24 @@ Revision History:
|
|||
#include "th_rewriter.h"
|
||||
#include "ast_trail.h"
|
||||
#include "scoped_vector.h"
|
||||
#include "scoped_ptr_vector.h"
|
||||
#include "automaton.h"
|
||||
#include "seq_rewriter.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
class theory_seq : public theory {
|
||||
typedef scoped_dependency_manager<enode_pair> enode_pair_dependency_manager;
|
||||
typedef enode_pair_dependency_manager::dependency enode_pair_dependency;
|
||||
|
||||
struct assumption {
|
||||
enode* n1, *n2;
|
||||
literal lit;
|
||||
assumption(enode* n1, enode* n2): n1(n1), n2(n2), lit(null_literal) {}
|
||||
assumption(literal lit): n1(0), n2(0), lit(lit) {}
|
||||
};
|
||||
typedef scoped_dependency_manager<assumption> dependency_manager;
|
||||
typedef dependency_manager::dependency dependency;
|
||||
|
||||
typedef trail_stack<theory_seq> th_trail_stack;
|
||||
typedef std::pair<expr*, enode_pair_dependency*> expr_dep;
|
||||
typedef std::pair<expr*, dependency*> expr_dep;
|
||||
typedef obj_map<expr, expr_dep> eqdep_map_t;
|
||||
|
||||
// cache to track evaluations under equalities
|
||||
|
|
@ -52,27 +61,30 @@ namespace smt {
|
|||
class solution_map {
|
||||
enum map_update { INS, DEL };
|
||||
ast_manager& m;
|
||||
enode_pair_dependency_manager& m_dm;
|
||||
dependency_manager& m_dm;
|
||||
eqdep_map_t m_map;
|
||||
eval_cache m_cache;
|
||||
expr_ref_vector m_lhs, m_rhs;
|
||||
ptr_vector<enode_pair_dependency> m_deps;
|
||||
ptr_vector<dependency> m_deps;
|
||||
svector<map_update> m_updates;
|
||||
unsigned_vector m_limit;
|
||||
|
||||
void add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d);
|
||||
void add_trail(map_update op, expr* l, expr* r, dependency* d);
|
||||
public:
|
||||
solution_map(ast_manager& m, enode_pair_dependency_manager& dm):
|
||||
solution_map(ast_manager& m, dependency_manager& dm):
|
||||
m(m), m_dm(dm), m_cache(m), m_lhs(m), m_rhs(m) {}
|
||||
bool empty() const { return m_map.empty(); }
|
||||
void update(expr* e, expr* r, enode_pair_dependency* d);
|
||||
bool empty() const { return m_map.empty(); }
|
||||
void update(expr* e, expr* r, dependency* d);
|
||||
void add_cache(expr* v, expr_dep& r) { m_cache.insert(v, r); }
|
||||
bool find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); }
|
||||
expr* find(expr* e, enode_pair_dependency*& d);
|
||||
void cache(expr* e, expr* r, enode_pair_dependency* d);
|
||||
void push_scope() { m_limit.push_back(m_updates.size()); }
|
||||
void pop_scope(unsigned num_scopes);
|
||||
void display(std::ostream& out) const;
|
||||
expr* find(expr* e, dependency*& d);
|
||||
expr* find(expr* e);
|
||||
bool is_root(expr* e) const;
|
||||
void cache(expr* e, expr* r, dependency* d);
|
||||
void reset_cache() { m_cache.reset(); }
|
||||
void push_scope() { m_limit.push_back(m_updates.size()); }
|
||||
void pop_scope(unsigned num_scopes);
|
||||
void display(std::ostream& out) const;
|
||||
};
|
||||
|
||||
// Table of current disequalities
|
||||
|
|
@ -97,52 +109,235 @@ namespace smt {
|
|||
struct eq {
|
||||
expr_ref m_lhs;
|
||||
expr_ref m_rhs;
|
||||
enode_pair_dependency* m_dep;
|
||||
eq(expr_ref& l, expr_ref& r, enode_pair_dependency* d):
|
||||
dependency* m_dep;
|
||||
eq(expr_ref& l, expr_ref& r, dependency* d):
|
||||
m_lhs(l), m_rhs(r), m_dep(d) {}
|
||||
eq(eq const& other): m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_dep(other.m_dep) {}
|
||||
eq& operator=(eq const& other) { m_lhs = other.m_lhs; m_rhs = other.m_rhs; m_dep = other.m_dep; return *this; }
|
||||
};
|
||||
|
||||
|
||||
// asserted or derived disqequality with dependencies
|
||||
struct ne {
|
||||
bool m_solved;
|
||||
expr_ref m_l, m_r;
|
||||
expr_ref_vector m_lhs;
|
||||
expr_ref_vector m_rhs;
|
||||
literal_vector m_lits;
|
||||
dependency* m_dep;
|
||||
ne(expr_ref& l, expr_ref& r):
|
||||
m_solved(false), m_l(l), m_r(r), m_lhs(l.get_manager()), m_rhs(r.get_manager()), m_dep(0) {
|
||||
m_lhs.push_back(l);
|
||||
m_rhs.push_back(r);
|
||||
}
|
||||
ne(ne const& other):
|
||||
m_solved(other.m_solved), m_l(other.m_l), m_r(other.m_r), m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {}
|
||||
ne& operator=(ne const& other) {
|
||||
m_solved = other.m_solved;
|
||||
m_l = other.m_l;
|
||||
m_r = other.m_r;
|
||||
m_lhs.reset(); m_lhs.append(other.m_lhs);
|
||||
m_rhs.reset(); m_rhs.append(other.m_rhs);
|
||||
m_lits.reset(); m_lits.append(other.m_lits);
|
||||
m_dep = other.m_dep;
|
||||
return *this;
|
||||
}
|
||||
bool is_solved() const { return m_solved; }
|
||||
};
|
||||
|
||||
class pop_lit : public trail<theory_seq> {
|
||||
unsigned m_idx;
|
||||
literal m_lit;
|
||||
public:
|
||||
pop_lit(theory_seq& th, unsigned idx): m_idx(idx), m_lit(th.m_nqs[idx].m_lits.back()) {
|
||||
th.m_nqs.ref(m_idx).m_lits.pop_back();
|
||||
}
|
||||
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.push_back(m_lit); }
|
||||
};
|
||||
class push_lit : public trail<theory_seq> {
|
||||
unsigned m_idx;
|
||||
public:
|
||||
push_lit(theory_seq& th, unsigned idx, literal lit): m_idx(idx) {
|
||||
th.m_nqs.ref(m_idx).m_lits.push_back(lit);
|
||||
}
|
||||
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.pop_back(); }
|
||||
};
|
||||
class set_lit : public trail<theory_seq> {
|
||||
unsigned m_idx;
|
||||
unsigned m_i;
|
||||
literal m_lit;
|
||||
public:
|
||||
set_lit(theory_seq& th, unsigned idx, unsigned i, literal lit):
|
||||
m_idx(idx), m_i(i), m_lit(th.m_nqs[idx].m_lits[i]) {
|
||||
th.m_nqs.ref(m_idx).m_lits[i] = lit;
|
||||
}
|
||||
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits[m_i] = m_lit; }
|
||||
};
|
||||
|
||||
class solved_ne : public trail<theory_seq> {
|
||||
unsigned m_idx;
|
||||
public:
|
||||
solved_ne(theory_seq& th, unsigned idx) : m_idx(idx) { th.m_nqs.ref(idx).m_solved = true; }
|
||||
virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_solved = false; }
|
||||
};
|
||||
void mark_solved(unsigned idx);
|
||||
|
||||
class push_ne : public trail<theory_seq> {
|
||||
unsigned m_idx;
|
||||
public:
|
||||
push_ne(theory_seq& th, unsigned idx, expr* l, expr* r) : m_idx(idx) {
|
||||
th.m_nqs.ref(m_idx).m_lhs.push_back(l);
|
||||
th.m_nqs.ref(m_idx).m_rhs.push_back(r);
|
||||
}
|
||||
virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_lhs.pop_back(); th.m_nqs.ref(m_idx).m_rhs.pop_back(); }
|
||||
};
|
||||
|
||||
class pop_ne : public trail<theory_seq> {
|
||||
expr_ref m_lhs;
|
||||
expr_ref m_rhs;
|
||||
unsigned m_idx;
|
||||
public:
|
||||
pop_ne(theory_seq& th, unsigned idx):
|
||||
m_lhs(th.m_nqs[idx].m_lhs.back(), th.m),
|
||||
m_rhs(th.m_nqs[idx].m_rhs.back(), th.m),
|
||||
m_idx(idx) {
|
||||
th.m_nqs.ref(idx).m_lhs.pop_back();
|
||||
th.m_nqs.ref(idx).m_rhs.pop_back();
|
||||
}
|
||||
virtual void undo(theory_seq& th) {
|
||||
th.m_nqs.ref(m_idx).m_lhs.push_back(m_lhs);
|
||||
th.m_nqs.ref(m_idx).m_rhs.push_back(m_rhs);
|
||||
m_lhs.reset();
|
||||
m_rhs.reset();
|
||||
}
|
||||
};
|
||||
|
||||
class set_ne : public trail<theory_seq> {
|
||||
expr_ref m_lhs;
|
||||
expr_ref m_rhs;
|
||||
unsigned m_idx;
|
||||
unsigned m_i;
|
||||
public:
|
||||
set_ne(theory_seq& th, unsigned idx, unsigned i, expr* l, expr* r):
|
||||
m_lhs(th.m_nqs[idx].m_lhs[i], th.m),
|
||||
m_rhs(th.m_nqs[idx].m_rhs[i], th.m),
|
||||
m_idx(idx),
|
||||
m_i(i) {
|
||||
th.m_nqs.ref(idx).m_lhs[i] = l;
|
||||
th.m_nqs.ref(idx).m_rhs[i] = r;
|
||||
}
|
||||
virtual void undo(theory_seq& th) {
|
||||
th.m_nqs.ref(m_idx).m_lhs[m_i] = m_lhs;
|
||||
th.m_nqs.ref(m_idx).m_rhs[m_i] = m_rhs;
|
||||
m_lhs.reset();
|
||||
m_rhs.reset();
|
||||
}
|
||||
};
|
||||
|
||||
class push_dep : public trail<theory_seq> {
|
||||
dependency* m_dep;
|
||||
unsigned m_idx;
|
||||
public:
|
||||
push_dep(theory_seq& th, unsigned idx, dependency* d): m_dep(th.m_nqs[idx].m_dep), m_idx(idx) {
|
||||
th.m_nqs.ref(idx).m_dep = d;
|
||||
}
|
||||
virtual void undo(theory_seq& th) {
|
||||
th.m_nqs.ref(m_idx).m_dep = m_dep;
|
||||
}
|
||||
};
|
||||
|
||||
class apply {
|
||||
public:
|
||||
virtual ~apply() {}
|
||||
virtual void operator()(theory_seq& th) = 0;
|
||||
};
|
||||
|
||||
class replay_length_coherence : public apply {
|
||||
expr_ref m_e;
|
||||
public:
|
||||
replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
|
||||
virtual void operator()(theory_seq& th) {
|
||||
th.check_length_coherence(m_e);
|
||||
}
|
||||
};
|
||||
|
||||
class replay_axiom : public apply {
|
||||
expr_ref m_e;
|
||||
public:
|
||||
replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
|
||||
virtual void operator()(theory_seq& th) {
|
||||
th.enque_axiom(m_e);
|
||||
}
|
||||
};
|
||||
|
||||
class push_replay : public trail<theory_seq> {
|
||||
apply* m_apply;
|
||||
public:
|
||||
push_replay(apply* app): m_apply(app) {}
|
||||
virtual void undo(theory_seq& th) {
|
||||
th.m_replay.push_back(m_apply);
|
||||
}
|
||||
};
|
||||
|
||||
void erase_index(unsigned idx, unsigned i);
|
||||
|
||||
struct stats {
|
||||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(stats)); }
|
||||
unsigned m_num_splits;
|
||||
unsigned m_num_reductions;
|
||||
unsigned m_propagate_automata;
|
||||
unsigned m_check_length_coherence;
|
||||
unsigned m_branch_variable;
|
||||
unsigned m_solve_nqs;
|
||||
unsigned m_solve_eqs;
|
||||
unsigned m_add_axiom;
|
||||
};
|
||||
ast_manager& m;
|
||||
enode_pair_dependency_manager m_dm;
|
||||
solution_map m_rep; // unification representative.
|
||||
scoped_vector<eq> m_eqs; // set of current equations.
|
||||
ast_manager& m;
|
||||
dependency_manager m_dm;
|
||||
solution_map m_rep; // unification representative.
|
||||
scoped_vector<eq> m_eqs; // set of current equations.
|
||||
scoped_vector<ne> m_nqs; // set of current disequalities.
|
||||
|
||||
seq_factory* m_factory; // value factory
|
||||
expr_ref_vector m_ineqs; // inequalities to check solution against
|
||||
exclusion_table m_exclude; // set of asserted disequalities.
|
||||
expr_ref_vector m_axioms; // list of axioms to add.
|
||||
unsigned m_axioms_head; // index of first axiom to add.
|
||||
unsigned m_branch_variable_head; // index of first equation to examine.
|
||||
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
|
||||
bool m_has_length; // is length applied
|
||||
bool m_model_completion; // during model construction, invent values in canonizer
|
||||
th_rewriter m_rewrite;
|
||||
seq_util m_util;
|
||||
arith_util m_autil;
|
||||
th_trail_stack m_trail_stack;
|
||||
stats m_stats;
|
||||
symbol m_prefix_sym;
|
||||
symbol m_suffix_sym;
|
||||
symbol m_contains_left_sym;
|
||||
symbol m_contains_right_sym;
|
||||
symbol m_left_sym; // split variable left part
|
||||
symbol m_right_sym; // split variable right part
|
||||
seq_factory* m_factory; // value factory
|
||||
exclusion_table m_exclude; // set of asserted disequalities.
|
||||
expr_ref_vector m_axioms; // list of axioms to add.
|
||||
obj_hashtable<expr> m_axiom_set;
|
||||
unsigned m_axioms_head; // index of first axiom to add.
|
||||
unsigned m_branch_variable_head; // index of first equation to examine.
|
||||
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
|
||||
obj_hashtable<expr> m_length; // is length applied
|
||||
scoped_ptr_vector<apply> m_replay; // set of actions to replay
|
||||
model_generator* m_mg;
|
||||
th_rewriter m_rewrite;
|
||||
seq_util m_util;
|
||||
arith_util m_autil;
|
||||
th_trail_stack m_trail_stack;
|
||||
stats m_stats;
|
||||
symbol m_prefix, m_suffix, m_contains_left, m_contains_right, m_accept, m_reject;
|
||||
symbol m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
|
||||
symbol m_extract_prefix, m_at_left, m_at_right;
|
||||
ptr_vector<expr> m_todo;
|
||||
expr_ref_vector m_ls, m_rs, m_lhs, m_rhs;
|
||||
|
||||
// maintain automata with regular expressions.
|
||||
scoped_ptr_vector<eautomaton> m_automata;
|
||||
obj_map<expr, eautomaton*> m_re2aut;
|
||||
|
||||
// queue of asserted atoms
|
||||
ptr_vector<expr> m_atoms;
|
||||
unsigned_vector m_atoms_lim;
|
||||
unsigned m_atoms_qhead;
|
||||
bool m_new_solution; // new solution added
|
||||
bool m_new_propagation; // new propagation to core
|
||||
|
||||
virtual final_check_status final_check_eh();
|
||||
virtual bool internalize_atom(app*, bool);
|
||||
virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); }
|
||||
virtual bool internalize_term(app*);
|
||||
virtual void internalize_eq_eh(app * atom, bool_var v);
|
||||
virtual void internalize_eq_eh(app * atom, bool_var v) {}
|
||||
virtual void new_eq_eh(theory_var, theory_var);
|
||||
virtual void new_diseq_eh(theory_var, theory_var);
|
||||
virtual void assign_eq(bool_var v, bool is_true);
|
||||
virtual void assign_eh(bool_var v, bool is_true);
|
||||
virtual bool can_propagate();
|
||||
virtual void propagate();
|
||||
virtual void push_scope_eh();
|
||||
|
|
@ -159,40 +354,56 @@ namespace smt {
|
|||
virtual void init_model(model_generator & mg);
|
||||
|
||||
// final check
|
||||
bool check_ineqs(); // check if inequalities are violated.
|
||||
bool simplify_and_solve_eqs(); // solve unitary equalities
|
||||
bool branch_variable(); // branch on a variable
|
||||
bool split_variable(); // split a variable
|
||||
bool is_solved();
|
||||
bool check_length_coherence();
|
||||
bool check_length_coherence_tbd();
|
||||
bool check_ineq_coherence();
|
||||
bool check_length_coherence();
|
||||
bool check_length_coherence(expr* e);
|
||||
bool propagate_length_coherence(expr* e);
|
||||
|
||||
bool pre_process_eqs(bool simplify_or_solve);
|
||||
bool simplify_eqs();
|
||||
bool simplify_eq(expr* l, expr* r, enode_pair_dependency* dep);
|
||||
bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* dep);
|
||||
bool solve_basic_eqs();
|
||||
bool solve_eqs(unsigned start);
|
||||
bool solve_eq(expr* l, expr* r, dependency* dep);
|
||||
bool simplify_eq(expr* l, expr* r, dependency* dep);
|
||||
bool solve_unit_eq(expr* l, expr* r, dependency* dep);
|
||||
bool is_binary_eq(expr* l, expr* r, expr*& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr*& y);
|
||||
bool solve_binary_eq(expr* l, expr* r, dependency* dep);
|
||||
bool propagate_max_length(expr* l, expr* r, dependency* dep);
|
||||
|
||||
bool solve_nqs(unsigned i);
|
||||
void solve_ne(unsigned i);
|
||||
bool unchanged(expr* e, expr_ref_vector& es) const { return es.size() == 1 && es[0] == e; }
|
||||
bool unchanged(expr* e, expr_ref_vector& es, expr* f, expr_ref_vector& fs) const {
|
||||
return
|
||||
(unchanged(e, es) && unchanged(f, fs)) ||
|
||||
(unchanged(e, fs) && unchanged(e, fs));
|
||||
}
|
||||
|
||||
// asserting consequences
|
||||
void propagate_lit(enode_pair_dependency* dep, literal lit);
|
||||
void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2);
|
||||
void propagate_eq(bool_var v, expr* e1, expr* e2);
|
||||
void set_conflict(enode_pair_dependency* dep);
|
||||
void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
|
||||
void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); }
|
||||
void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
|
||||
void propagate_eq(dependency* dep, enode* n1, enode* n2);
|
||||
void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs = false);
|
||||
void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
|
||||
|
||||
bool find_branch_candidate(expr* l, ptr_vector<expr> const& rs);
|
||||
bool assume_equality(expr* l, expr* r);
|
||||
bool find_branch_candidate(dependency* dep, expr* l, expr_ref_vector const& rs);
|
||||
lbool assume_equality(expr* l, expr* r);
|
||||
|
||||
// variable solving utilities
|
||||
bool occurs(expr* a, expr* b);
|
||||
bool is_var(expr* b);
|
||||
void add_solution(expr* l, expr* r, enode_pair_dependency* dep);
|
||||
bool is_left_select(expr* a, expr*& b);
|
||||
bool is_right_select(expr* a, expr*& b);
|
||||
expr_ref canonize(expr* e, enode_pair_dependency*& eqs);
|
||||
expr_ref expand(expr* e, enode_pair_dependency*& eqs);
|
||||
void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b);
|
||||
bool add_solution(expr* l, expr* r, dependency* dep);
|
||||
bool is_nth(expr* a) const;
|
||||
bool is_tail(expr* a, expr*& s, unsigned& idx) const;
|
||||
expr_ref mk_nth(expr* s, expr* idx);
|
||||
expr_ref mk_last(expr* e);
|
||||
expr_ref canonize(expr* e, dependency*& eqs);
|
||||
void canonize(expr* e, expr_ref_vector& es, dependency*& eqs);
|
||||
expr_ref expand(expr* e, dependency*& eqs);
|
||||
void add_dependency(dependency*& dep, enode* a, enode* b);
|
||||
|
||||
void get_concat(expr* e, ptr_vector<expr>& concats);
|
||||
|
||||
// terms whose meaning are encoded using axioms.
|
||||
void enque_axiom(expr* e);
|
||||
|
|
@ -202,28 +413,80 @@ namespace smt {
|
|||
void add_replace_axiom(expr* e);
|
||||
void add_extract_axiom(expr* e);
|
||||
void add_length_axiom(expr* n);
|
||||
void add_length_unit_axiom(expr* n);
|
||||
void add_length_empty_axiom(expr* n);
|
||||
void add_length_concat_axiom(expr* n);
|
||||
void add_length_string_axiom(expr* n);
|
||||
|
||||
bool has_length(expr *e) const { return m_length.contains(e); }
|
||||
void add_length(expr* e);
|
||||
void enforce_length(enode* n);
|
||||
void enforce_length_coherence(enode* n1, enode* n2);
|
||||
|
||||
void add_elim_string_axiom(expr* n);
|
||||
void add_at_axiom(expr* n);
|
||||
void add_in_re_axiom(expr* n);
|
||||
literal mk_literal(expr* n);
|
||||
literal mk_eq_empty(expr* n);
|
||||
literal mk_equals(expr* a, expr* b);
|
||||
void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
|
||||
expr* mk_sub(expr* a, expr* b);
|
||||
expr_ref mk_sub(expr* a, expr* b);
|
||||
enode* ensure_enode(expr* a);
|
||||
|
||||
// arithmetic integration
|
||||
bool lower_bound(expr* s, rational& lo);
|
||||
bool upper_bound(expr* s, rational& hi);
|
||||
bool get_length(expr* s, rational& val);
|
||||
|
||||
void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
|
||||
expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0, sort* range = 0);
|
||||
bool is_skolem(symbol const& s, expr* e) const;
|
||||
|
||||
void set_incomplete(app* term);
|
||||
|
||||
// automata utilities
|
||||
void propagate_in_re(expr* n, bool is_true);
|
||||
eautomaton* get_automaton(expr* e);
|
||||
literal mk_accept(expr* s, expr* idx, expr* re, expr* state);
|
||||
literal mk_accept(expr* s, expr* idx, expr* re, unsigned i) { return mk_accept(s, idx, re, m_autil.mk_int(i)); }
|
||||
bool is_accept(expr* acc) const { return is_skolem(m_accept, acc); }
|
||||
bool is_accept(expr* acc, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut) {
|
||||
return is_acc_rej(m_accept, acc, s, idx, re, i, aut);
|
||||
}
|
||||
literal mk_reject(expr* s, expr* idx, expr* re, expr* state);
|
||||
literal mk_reject(expr* s, expr* idx, expr* re, unsigned i) { return mk_reject(s, idx, re, m_autil.mk_int(i)); }
|
||||
bool is_reject(expr* rej) const { return is_skolem(m_reject, rej); }
|
||||
bool is_reject(expr* rej, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut) {
|
||||
return is_acc_rej(m_reject, rej, s, idx, re, i, aut);
|
||||
}
|
||||
bool is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut);
|
||||
expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* t);
|
||||
bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const;
|
||||
bool is_step(expr* e) const;
|
||||
void propagate_step(literal lit, expr* n);
|
||||
bool add_reject2reject(expr* rej);
|
||||
bool add_accept2step(expr* acc);
|
||||
bool add_step2accept(expr* step);
|
||||
bool add_prefix2prefix(expr* e);
|
||||
bool add_suffix2suffix(expr* e);
|
||||
bool add_contains2contains(expr* e);
|
||||
void ensure_nth(literal lit, expr* s, expr* idx);
|
||||
bool canonizes(bool sign, expr* e);
|
||||
void propagate_non_empty(literal lit, expr* s);
|
||||
void propagate_is_conc(expr* e, expr* conc);
|
||||
void propagate_acc_rej_length(literal lit, expr* acc_rej);
|
||||
bool propagate_automata();
|
||||
void add_atom(expr* e);
|
||||
void new_eq_eh(dependency* dep, enode* n1, enode* n2);
|
||||
|
||||
// diagnostics
|
||||
void display_equations(std::ostream& out) const;
|
||||
void display_deps(std::ostream& out, enode_pair_dependency* deps) const;
|
||||
void display_disequations(std::ostream& out) const;
|
||||
void display_disequation(std::ostream& out, ne const& e) const;
|
||||
void display_deps(std::ostream& out, dependency* deps) const;
|
||||
public:
|
||||
theory_seq(ast_manager& m);
|
||||
virtual ~theory_seq();
|
||||
|
||||
// model building
|
||||
app* mk_value(app* a);
|
||||
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -30,6 +30,7 @@ namespace smt {
|
|||
seq_util u;
|
||||
symbol_set m_strings;
|
||||
unsigned m_next;
|
||||
char m_char;
|
||||
std::string m_unique_prefix;
|
||||
obj_map<sort, expr*> m_unique_sequences;
|
||||
expr_ref_vector m_trail;
|
||||
|
|
@ -41,6 +42,7 @@ namespace smt {
|
|||
m_model(md),
|
||||
u(m),
|
||||
m_next(0),
|
||||
m_char(0),
|
||||
m_unique_prefix("#B"),
|
||||
m_trail(m)
|
||||
{
|
||||
|
|
@ -99,6 +101,11 @@ namespace smt {
|
|||
expr* v0 = get_fresh_value(seq);
|
||||
return u.re.mk_to_re(v0);
|
||||
}
|
||||
if (u.is_char(s)) {
|
||||
//char s[2] = { ++m_char, 0 };
|
||||
//return u.str.mk_char(zstring(s), 0);
|
||||
return u.str.mk_char(zstring("a"), 0);
|
||||
}
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue