mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-16 07:45:27 +00:00
Code Activity

seq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-08 21:03:28 -08:00
parent 24de0a9b90
commit 94bd2fdbe4
7 changed files with 285 additions and 78 deletions
Download patch file Download diff file Expand all files Collapse all files

207
src/smt/theory_seq.cpp
View file

@ -72,6 +72,14 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) {
m_limit.resize(m_limit.size() - num_scopes);
}
void theory_seq::solution_map::display(std::ostream& out) const {
map_t::iterator it = m_map.begin(), end = m_map.end();
for (; it != end; ++it) {
out << mk_pp(it->m_key, m) << " |-> " << mk_pp(it->m_value.first, m) << "\n";
}
}
theory_seq::theory_seq(ast_manager& m):
theory(m.mk_family_id("seq")),
m(m),
@ -88,10 +96,17 @@ theory_seq::theory_seq(ast_manager& m):
m_lhs.push_back(expr_array());
m_rhs.push_back(expr_array());
m_deps.push_back(enode_pair_dependency_array());
m_prefix_sym = "prefix";
m_suffix_sym = "suffix";
m_left_sym = "left";
m_right_sym = "right";
m_contains_left_sym = "contains_left";
m_contains_right_sym = "contains_right";
}
final_check_status theory_seq::final_check_eh() {
context & ctx = get_context();
TRACE("seq", display(tout););
if (!check_ineqs()) {
return FC_CONTINUE;
}
@ -111,44 +126,50 @@ bool theory_seq::check_ineqs() {
enode_pair_dependency* eqs = 0;
expr_ref b = canonize(a, eqs);
if (m.is_true(b)) {
TRACE("seq", tout << "Evaluates to false: " << a << "\n";);
ctx.internalize(a, false);
literal lit(ctx.get_literal(a));
ctx.mark_as_relevant(lit);
vector<enode_pair, false> _eqs;
m_dm.linearize(eqs, _eqs);
ctx.assign(
lit,
ctx.mk_justification(
ext_theory_propagation_justification(
get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), lit)));
propagate(lit, eqs);
return false;
}
}
return true;
}
void theory_seq::propagate(literal lit, enode_pair_dependency* dep) {
context& ctx = get_context();
ctx.mark_as_relevant(lit);
vector<enode_pair, false> _eqs;
m_dm.linearize(dep, _eqs);
TRACE("seq",
ctx.display_detailed_literal(tout, lit);
tout << " <- ";
for (unsigned i = 0; i < _eqs.size(); ++i) {
tout << mk_pp(_eqs[i].first->get_owner(), m) << " = "
<< mk_pp(_eqs[i].second->get_owner(), m) << "\n";
}
);
ctx.assign(
lit,
ctx.mk_justification(
ext_theory_propagation_justification(
get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), lit)));
}
bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) {
context& ctx = get_context();
seq_rewriter rw(m);
expr_ref_vector lhs(m), rhs(m);
SASSERT(ctx.e_internalized(l));
SASSERT(ctx.e_internalized(r));
expr_ref lh = canonize(l, deps);
expr_ref rh = canonize(r, deps);
if (!rw.reduce_eq(l, r, lhs, rhs)) {
// equality is inconsistent.
// create conflict assignment.
expr_ref a(m);
a = m.mk_eq(l, r);
literal lit(ctx.get_literal(a));
vector<enode_pair, false> _eqs;
m_dm.linearize(deps, _eqs);
ctx.assign(
~lit,
ctx.mk_justification(
ext_theory_propagation_justification(
get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), ~lit)));
literal lit(mk_eq(l, r, false));
propagate(~lit, deps);
return true;
}
if (lhs.size() == 1 && l == lhs[0].get() &&
@ -161,6 +182,13 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) {
m.push_back(m_rhs.back(), rhs[i].get());
m_dam.push_back(m_deps.back(), deps);
}
TRACE("seq",
tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " => ";
for (unsigned i = 0; i < lhs.size(); ++i) {
tout << mk_pp(lhs[i].get(), m) << " = " << mk_pp(rhs[i].get(), m) << "; ";
}
tout << "\n";
);
return true;
}
@ -187,31 +215,36 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps) {
}
bool theory_seq::occurs(expr* a, expr* b) {
// true if a occurs under an interpreted function or under left/right selector.
SASSERT(is_var(a));
// true if a occurs under an interpreted function or under left/right selector.
if (a == b) {
return true;
}
expr* e1, *e2;
while (is_left_select(a, e1) || is_right_select(a, e1)) {
a = e1;
}
if (m_util.str.is_concat(b, e1, e2)) {
return occurs(a, e1) || occurs(a, e2);
}
if (is_left_select(b, e1) || is_right_select(b, e1)) {
return occurs(a, e1);
}
while (is_left_select(b, e1) || is_right_select(b, e1)) {
b = e1;
}
if (a == b) {
return true;
}
return false;
}
bool theory_seq::is_var(expr* a) {
return is_uninterp(a);
return is_uninterp(a) || m_util.is_skolem(a);
}
bool theory_seq::is_left_select(expr* a, expr*& b) {
return false;
return m_util.is_skolem(a) &&
to_app(a)->get_decl()->get_parameter(0).get_symbol() == m_left_sym && (b = to_app(a)->get_arg(0), true);
}
bool theory_seq::is_right_select(expr* a, expr*& b) {
return false;
return m_util.is_skolem(a) &&
to_app(a)->get_decl()->get_parameter(0).get_symbol() == m_right_sym && (b = to_app(a)->get_arg(0), true);
}
@ -224,10 +257,18 @@ void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) {
enode* n2 = ctx.get_enode(r);
vector<enode_pair, false> _eqs;
m_dm.linearize(deps, _eqs);
// alloc?
ctx.assign_eq(n1, n2, eq_justification(
alloc(ext_theory_eq_propagation_justification,
get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2)));
TRACE("seq",
tout << mk_pp(n1->get_owner(), m) << " " << mk_pp(n2->get_owner(), m) << " <- ";
for (unsigned i = 0; i < _eqs.size(); ++i) {
tout << mk_pp(_eqs[i].first->get_owner(), m) << " = "
<< mk_pp(_eqs[i].second->get_owner(), m) << "\n";
}
);
justification* js = ctx.mk_justification(
ext_theory_eq_propagation_justification(
get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2));
ctx.assign_eq(n1, n2, eq_justification(js));
}
}
@ -254,6 +295,7 @@ bool theory_seq::pre_process_eqs(bool simplify_or_solve) {
m.set(rhs, i, m.get(rhs, m.size(rhs)-1));
m_dam.set(deps, i, m_dam.get(deps, m_dam.size(deps)-1));
--i;
++m_stats.m_num_reductions;
change = true;
}
m.pop_back(lhs);
@ -312,7 +354,8 @@ bool theory_seq::internalize_term(app* term) {
!m_util.str.is_unit(term) &&
!m_util.str.is_suffix(term) &&
!m_util.str.is_prefix(term) &&
!m_util.str.is_contains(term)) {
!m_util.str.is_contains(term) &&
!m_util.is_skolem(term)) {
set_incomplete(term);
}
@ -326,6 +369,70 @@ void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
}
}
void theory_seq::display(std::ostream & out) const {
expr_array const& lhs = m_lhs.back();
expr_array const& rhs = m_rhs.back();
enode_pair_dependency_array const& deps = m_deps.back();
out << "Equations:\n";
for (unsigned i = 0; i < m.size(lhs); ++i) {
out << mk_pp(m.get(lhs, i), m) << " = " << mk_pp(m.get(rhs, i), m) << " <-\n";
enode_pair_dependency* dep = m_dam.get(deps, i);
if (dep) {
vector<enode_pair, false> _eqs;
const_cast<enode_pair_dependency_manager&>(m_dm).linearize(dep, _eqs);
for (unsigned i = 0; i < _eqs.size(); ++i) {
out << " " << mk_pp(_eqs[i].first->get_owner(), m) << " = " << mk_pp(_eqs[i].second->get_owner(), m) << "\n";
}
}
}
out << "Negative constraints:\n";
for (unsigned i = 0; i < m_ineqs.size(); ++i) {
out << mk_pp(m_ineqs[i], m) << "\n";
}
out << "Solved equations:\n";
m_rep.display(out);
}
void theory_seq::collect_statistics(::statistics & st) const {
st.update("seq num splits", m_stats.m_num_splits);
st.update("seq num reductions", m_stats.m_num_reductions);
}
void theory_seq::init_model(model_generator & mg) {
m_factory = alloc(seq_factory, get_manager(),
get_family_id(), mg.get_model());
mg.register_factory(m_factory);
// TBD: this is still unsound model generation.
// disequalities are not guaranteed. we need to
// prime the factory with a prefix that cannot be
// constructed using any existing combinations of the
// strings (or units) that are used.
for (unsigned i = 0; i < get_num_vars(); ++i) {
expr* e = get_enode(i)->get_owner();
if (m_util.is_seq(e)) {
enode_pair_dependency* deps = 0;
e = m_rep.find(e, deps);
if (is_var(e)) {
expr* val = m_factory->get_fresh_value(m.get_sort(e));
m_rep.update(e, val, 0);
}
}
else if (m_util.is_re(e)) {
// TBD
}
}
}
model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
enode_pair_dependency* deps = 0;
expr_ref e(m);
canonize(e, deps);
SASSERT(is_app(e));
m_factory->add_trail(e);
return alloc(expr_wrapper_proc, to_app(e));
}
void theory_seq::set_incomplete(app* term) {
TRACE("seq", tout << "No support for: " << mk_pp(term, m) << "\n";);
@ -413,27 +520,29 @@ void theory_seq::assert_axiom(expr_ref& e) {
literal lit(ctx.get_literal(e));
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit);
}
expr_ref theory_seq::mk_skolem(char const* name, expr* e1, expr* e2) {
expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2) {
expr_ref result(m);
sort* s = m.get_sort(e1);
SASSERT(s == m.get_sort(e2));
sort* ss[2] = { s, s };
result = m.mk_app(m.mk_func_decl(symbol("#prefix_eq"), 2, ss, s), e1, e2);
expr* es[2] = { e1, e2 };
result = m_util.mk_skolem(name, 2, es, m.get_sort(e1));
return result;
}
void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) {
context& ctx = get_context();
TRACE("seq",
tout << mk_pp(ctx.bool_var2enode(v)->get_owner(), m) << " => "
<< mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";);
ctx.internalize(e1, false);
enode* n1 = ctx.get_enode(e1);
enode* n2 = ctx.get_enode(e2);
literal lit(v);
ctx.assign_eq(n1, n2, eq_justification(
alloc(ext_theory_eq_propagation_justification,
get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2)));
justification* js = ctx.mk_justification(ext_theory_eq_propagation_justification(
get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2));
ctx.assign_eq(n1, n2, eq_justification(js));
}
void theory_seq::assign_eq(bool_var v, bool is_true) {
@ -445,18 +554,18 @@ void theory_seq::assign_eq(bool_var v, bool is_true) {
expr* e1, *e2;
expr_ref f(m);
if (m_util.str.is_prefix(e, e1, e2)) {
f = mk_skolem("#prefix_eq", e1, e2);
f = mk_skolem(m_prefix_sym, e1, e2);
f = m_util.str.mk_concat(e1, f);
propagate_eq(v, f, e2);
}
else if (m_util.str.is_suffix(e, e1, e2)) {
f = mk_skolem("#suffix_eq", e1, e2);
f = mk_skolem(m_suffix_sym, e1, e2);
f = m_util.str.mk_concat(f, e1);
propagate_eq(v, f, e2);
}
else if (m_util.str.is_contains(e, e1, e2)) {
expr_ref f1 = mk_skolem("#contains_eq1", e1, e2);
expr_ref f2 = mk_skolem("#contains_eq2", e1, e2);
expr_ref f1 = mk_skolem(m_contains_left_sym, e1, e2);
expr_ref f2 = mk_skolem(m_contains_right_sym, e1, e2);
f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e1), f2);
propagate_eq(v, f, e2);
}
@ -485,7 +594,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
expr* e1 = get_enode(v1)->get_owner();
expr* e2 = get_enode(v2)->get_owner();
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_ineqs));
m_ineqs.push_back(m.mk_eq(e1, e2));
m_ineqs.push_back(mk_eq_atom(e1, e2));
}
void theory_seq::push_scope_eh() {

49
src/smt/theory_seq.h
View file

@ -49,25 +49,28 @@ namespace smt {
class solution_map {
enum map_update { INS, DEL };
ast_manager& m;
enode_pair_dependency_manager& m_dm;
obj_map<expr, std::pair<expr*, enode_pair_dependency*> > m_map;
expr_ref_vector m_lhs, m_rhs;
typedef obj_map<expr, std::pair<expr*, enode_pair_dependency*> > map_t;
ast_manager& m;
enode_pair_dependency_manager& m_dm;
map_t m_map;
expr_ref_vector m_lhs, m_rhs;
ptr_vector<enode_pair_dependency> m_deps;
svector<map_update> m_updates;
unsigned_vector m_limit;
svector<map_update> m_updates;
unsigned_vector m_limit;
public:
solution_map(ast_manager& m, enode_pair_dependency_manager& dm): m(m), m_dm(dm), m_lhs(m), m_rhs(m) {}
void update(expr* e, expr* r, enode_pair_dependency* d);
expr* find(expr* e, 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;
};
struct stats {
stats() { reset(); }
void reset() { memset(this, 0, sizeof(stats)); }
unsigned m_num_splits;
unsigned m_num_reductions;
};
ast_manager& m;
small_object_allocator m_alloc;
@ -78,7 +81,7 @@ namespace smt {
vector<expr_array> m_lhs, m_rhs; // persistent sets of equalities.
vector<enode_pair_dependency_array> m_deps; // persistent sets of dependencies.
seq_factory* m_factory; // value factory
expr_ref_vector m_ineqs; // inequalities to check
expr_ref_vector m_axioms;
unsigned m_axioms_head;
@ -88,13 +91,19 @@ namespace smt {
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;
symbol m_right_sym;
virtual final_check_status final_check_eh();
virtual bool internalize_atom(app*, bool);
virtual bool internalize_term(app*);
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_eq(bool_var v, bool is_true);
virtual bool can_propagate();
virtual void propagate();
virtual void push_scope_eh();
@ -105,21 +114,25 @@ namespace smt {
virtual char const * get_name() const { return "seq"; }
virtual theory_var mk_var(enode* n);
virtual void apply_sort_cnstr(enode* n, sort* s);
virtual void display(std::ostream & out) const;
virtual void collect_statistics(::statistics & st) const;
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
virtual void init_model(model_generator & mg);
bool check_ineqs();
bool pre_process_eqs(bool simplify_or_solve);
bool simplify_eqs();
bool simplify_eq(expr* l, expr* r, enode_pair_dependency* deps);
bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps);
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 simplify_and_solve_eqs();
void propagate(literal lit, enode_pair_dependency* dep);
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);
final_check_status add_axioms();
void assert_axiom(expr_ref& e);
@ -131,21 +144,11 @@ namespace smt {
enode_pair_dependency* join(enode_pair_dependency* a, enode_pair_dependency* b);
void propagate_eq(bool_var v, expr* e1, expr* e2);
expr_ref mk_skolem(char const* name, expr* e1, expr* e2);
expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2);
void set_incomplete(app* term);
public:
theory_seq(ast_manager& m);
virtual void init_model(model_generator & mg) {
mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()));
}
#if 0
th_trail_stack & get_trail_stack() { return m_trail_stack; }
virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var);
static 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);
#endif
};
};

26
src/smt/theory_seq_empty.h
View file

@ -25,22 +25,44 @@ Revision History:
namespace smt {
class seq_factory : public value_factory {
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
ast_manager& m;
proto_model& m_model;
seq_util u;
symbol_set m_strings;
unsigned m_next;
std::string m_unique_prefix;
obj_map<sort, expr*> m_unique_sequences;
expr_ref_vector m_trail;
public:
seq_factory(ast_manager & m, family_id fid, proto_model & md):
value_factory(m, fid),
m(m),
m_model(md),
u(m),
m_next(0)
m_next(0),
m_unique_prefix("#B"),
m_trail(m)
{
m_strings.insert(symbol(""));
m_strings.insert(symbol("a"));
m_strings.insert(symbol("b"));
}
void add_trail(expr* e) {
m_trail.push_back(e);
}
void set_prefix(char const* p) {
m_unique_prefix = p;
}
// generic method for setting unique sequences
void set_prefix(expr* uniq) {
m_trail.push_back(uniq);
m_unique_sequences.insert(m.get_sort(uniq), uniq);
}
virtual expr* get_some_value(sort* s) {
if (u.is_string(s))
return u.str.mk_string(symbol(""));
@ -60,7 +82,7 @@ namespace smt {
if (u.is_string(s)) {
while (true) {
std::ostringstream strm;
strm << "S" << m_next++;
strm << m_unique_prefix << m_next++;
symbol sym(strm.str().c_str());
if (m_strings.contains(sym)) continue;
m_strings.insert(sym);