diff --git a/scripts/mk_util.py b/scripts/mk_util.py index fc0d3b5e0..e32c9c3dd 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2199,7 +2199,7 @@ def mk_config(): 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') elif VS_ARM: - print "ARM on VS is unsupported" + print("ARM on VS is unsupported") exit(1) else: config.write( @@ -2225,7 +2225,7 @@ def mk_config(): 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG)) elif VS_ARM: - print "ARM on VS is unsupported" + print("ARM on VS is unsupported") exit(1) else: config.write( diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index a26fcfe2c..f04d445e1 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -25,6 +25,8 @@ Notes: #include"automaton.h" #include"well_sorted.h" #include"var_subst.h" +#include"symbolic_automata_def.h" + expr_ref sym_expr::accept(expr* e) { ast_manager& m = m_t.get_manager(); @@ -37,6 +39,7 @@ expr_ref sym_expr::accept(expr* e) { } case t_char: SASSERT(m.get_sort(e) == m.get_sort(m_t)); + SASSERT(m.get_sort(e) == m_sort); result = m.mk_eq(e, m_t); break; case t_range: { @@ -67,8 +70,114 @@ struct display_expr1 { } }; +class sym_expr_boolean_algebra : public boolean_algebra { + ast_manager& m; + expr_solver& m_solver; + typedef sym_expr* T; +public: + sym_expr_boolean_algebra(ast_manager& m, expr_solver& s): + m(m), m_solver(s) {} + + virtual T mk_false() { + expr_ref fml(m.mk_false(), m); + return sym_expr::mk_pred(fml, m.mk_bool_sort()); // use of Bool sort for bound variable is arbitrary + } + virtual T mk_true() { + expr_ref fml(m.mk_true(), m); + return sym_expr::mk_pred(fml, m.mk_bool_sort()); + } + virtual T mk_and(T x, T y) { + if (x->is_char() && y->is_char()) { + if (x->get_char() == y->get_char()) { + return x; + } + if (m.are_distinct(x->get_char(), y->get_char())) { + expr_ref fml(m.mk_false(), m); + return sym_expr::mk_pred(fml, x->get_sort()); + } + } + var_ref v(m.mk_var(0, x->get_sort()), m); + expr_ref fml1 = x->accept(v); + expr_ref fml2 = y->accept(v); + if (m.is_true(fml1)) return y; + if (m.is_true(fml2)) return x; + expr_ref fml(m.mk_and(fml1, fml2), m); + return sym_expr::mk_pred(fml, x->get_sort()); + } + virtual T mk_or(T x, T y) { + if (x->is_char() && y->is_char() && + x->get_char() == y->get_char()) { + return x; + } + var_ref v(m.mk_var(0, x->get_sort()), m); + expr_ref fml1 = x->accept(v); + expr_ref fml2 = y->accept(v); + if (m.is_false(fml1)) return y; + if (m.is_false(fml2)) return x; + expr_ref fml(m.mk_or(fml1, fml2), m); + return sym_expr::mk_pred(fml, x->get_sort()); + } + + virtual T mk_and(unsigned sz, T const* ts) { + switch (sz) { + case 0: return mk_true(); + case 1: return ts[0]; + default: { + T t = ts[0]; + for (unsigned i = 1; i < sz; ++i) { + t = mk_and(t, ts[i]); + } + return t; + } + } + } + virtual T mk_or(unsigned sz, T const* ts) { + switch (sz) { + case 0: return mk_false(); + case 1: return ts[0]; + default: { + T t = ts[0]; + for (unsigned i = 1; i < sz; ++i) { + t = mk_or(t, ts[i]); + } + return t; + } + } + } + virtual lbool is_sat(T x) { + if (x->is_char()) { + return l_true; + } + if (x->is_range()) { + // TBD check lower is below upper. + } + expr_ref v(m.mk_fresh_const("x", x->get_sort()), m); + expr_ref fml = x->accept(v); + if (m.is_true(fml)) { + return l_true; + } + if (m.is_false(fml)) { + return l_false; + } + return m_solver.check_sat(fml); + } + virtual T mk_not(T x) { + var_ref v(m.mk_var(0, x->get_sort()), m); + expr_ref fml(m.mk_not(x->accept(v)), m); + return sym_expr::mk_pred(fml, x->get_sort()); + } +}; + +re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {} + +re2automaton::~re2automaton() {} + +void re2automaton::set_solver(expr_solver* solver) { + m_solver = solver; + m_ba = alloc(sym_expr_boolean_algebra, m, *solver); + m_sa = alloc(symbolic_automata_t, sm, *m_ba.get()); +} -re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m) {} eautomaton* re2automaton::operator()(expr* e) { eautomaton* r = re2aut(e); @@ -136,7 +245,7 @@ eautomaton* re2automaton::re2aut(expr* e) { expr_ref _start(bv.mk_numeral(start, nb), m); expr_ref _stop(bv.mk_numeral(stop, nb), m); expr_ref _pred(m.mk_not(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop))), m); - a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred)); + a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s)); return a.detach(); } else if (u.re.is_to_re(e0, e1) && u.str.is_string(e1, s1) && s1.length() == 1) { @@ -145,13 +254,14 @@ eautomaton* re2automaton::re2aut(expr* e) { expr_ref v(m.mk_var(0, s), m); expr_ref _ch(bv.mk_numeral(s1[0], nb), m); expr_ref _pred(m.mk_not(m.mk_eq(v, _ch)), m); - a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred)); + a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s)); return a.detach(); } else if (u.re.is_to_re(e0, e1) && u.str.is_unit(e1, e2)) { - expr_ref v(m.mk_var(0, m.get_sort(e2)), m); + sort* s = m.get_sort(e2); + expr_ref v(m.mk_var(0, s), m); expr_ref _pred(m.mk_not(m.mk_eq(v, e2)), m); - a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred)); + a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s)); return a.detach(); } else { @@ -187,14 +297,15 @@ eautomaton* re2automaton::re2aut(expr* e) { } else if (u.re.is_full(e)) { expr_ref tt(m.mk_true(), m); - sym_expr* _true = sym_expr::mk_pred(tt); + sort* seq_s, *char_s; + VERIFY (u.is_re(m.get_sort(e), seq_s)); + VERIFY (u.is_seq(seq_s, char_s)); + sym_expr* _true = sym_expr::mk_pred(tt, char_s); return eautomaton::mk_loop(sm, _true); } -#if 0 - else if (u.re.is_intersect(e, e1, e2)) { - // maybe later + else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) { + return m_sa->mk_product(*a, *b); } -#endif return 0; } diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 83dd8f653..040bae1b4 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -25,6 +25,7 @@ Notes: #include"params.h" #include"lbool.h" #include"automaton.h" +#include"symbolic_automata.h" class sym_expr { enum ty { @@ -33,21 +34,24 @@ class sym_expr { t_range }; ty m_ty; + sort* m_sort; expr_ref m_t; expr_ref m_s; unsigned m_ref; - sym_expr(ty ty, expr_ref& t, expr_ref& s) : m_ty(ty), m_t(t), m_s(s), m_ref(0) {} + sym_expr(ty ty, expr_ref& t, expr_ref& s, sort* srt) : m_ty(ty), m_sort(srt), m_t(t), m_s(s), m_ref(0) {} public: expr_ref accept(expr* e); - static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t); } + static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t, t.get_manager().get_sort(t)); } static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return mk_char(tr); } - static sym_expr* mk_pred(expr_ref& t) { return alloc(sym_expr, t_pred, t, t); } - static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi); } + static sym_expr* mk_pred(expr_ref& t, sort* s) { return alloc(sym_expr, t_pred, t, t, s); } + static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi, lo.get_manager().get_sort(hi)); } void inc_ref() { ++m_ref; } void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); } std::ostream& display(std::ostream& out) const; bool is_char() const { return m_ty == t_char; } bool is_pred() const { return !is_char(); } + bool is_range() const { return m_ty == t_range; } + sort* get_sort() const { return m_sort; } expr* get_char() const { SASSERT(is_char()); return m_t; } }; @@ -58,17 +62,31 @@ public: void dec_ref(sym_expr* s) { if (s) s->dec_ref(); } }; +class expr_solver { +public: + virtual ~expr_solver() {} + virtual lbool check_sat(expr* e) = 0; +}; + typedef automaton eautomaton; class re2automaton { + typedef boolean_algebra boolean_algebra_t; + typedef symbolic_automata symbolic_automata_t; ast_manager& m; sym_expr_manager sm; seq_util u; bv_util bv; + scoped_ptr m_solver; + scoped_ptr m_ba; + scoped_ptr m_sa; + eautomaton* re2aut(expr* e); eautomaton* seq2aut(expr* e); - public: +public: re2automaton(ast_manager& m); + ~re2automaton(); eautomaton* operator()(expr* e); + void set_solver(expr_solver* solver); }; /** diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index 54c969bbb..dd1ff87f5 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -178,15 +178,19 @@ public: return alloc(automaton, a.m, a.init(), final, mvs); } + automaton* clone() const { + return clone(*this); + } + // create the sum of disjoint automata static automaton* mk_union(automaton const& a, automaton const& b) { SASSERT(&a.m == &b.m); M& m = a.m; if (a.is_empty()) { - return clone(b); + return b.clone(); } if (b.is_empty()) { - return clone(a); + return a.clone(); } moves mvs; unsigned_vector final; @@ -213,7 +217,7 @@ public: mvs.push_back(move(m, 0, a.init() + offset)); } if (a.is_empty()) { - return clone(a); + return a.clone(); } mvs.push_back(move(m, init, a.final_state() + offset)); @@ -227,16 +231,16 @@ public: SASSERT(&a.m == &b.m); M& m = a.m; if (a.is_empty()) { - return clone(a); + return a.clone(); } if (b.is_empty()) { - return clone(b); + return b.clone(); } if (a.is_epsilon()) { - return clone(b); + return b.clone(); } if (b.is_epsilon()) { - return clone(a); + return a.clone(); } moves mvs; @@ -458,6 +462,7 @@ public: } unsigned init() const { return m_init; } + unsigned_vector const& final_states() const { return m_final_states; } unsigned in_degree(unsigned state) const { return m_delta_inv[state].size(); } unsigned out_degree(unsigned state) const { return m_delta[state].size(); } move const& get_move_from(unsigned state) const { SASSERT(m_delta[state].size() == 1); return m_delta[state][0]; } diff --git a/src/math/automata/boolean_algebra.h b/src/math/automata/boolean_algebra.h new file mode 100644 index 000000000..503878ef3 --- /dev/null +++ b/src/math/automata/boolean_algebra.h @@ -0,0 +1,46 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + boolean_algebra.h + +Abstract: + + Boolean Algebra, a la Margus Veanes Automata library. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-2-27 + +Revision History: + + +--*/ + +#ifndef BOOLEAN_ALGEBRA_H_ +#define BOOLEAN_ALGEBRA_H_ + +#include "util.h" + +template +class positive_boolean_algebra { +public: + virtual T mk_false() = 0; + virtual T mk_true() = 0; + virtual T mk_and(T x, T y) = 0; + virtual T mk_or(T x, T y) = 0; + virtual T mk_and(unsigned sz, T const* ts) = 0; + virtual T mk_or(unsigned sz, T const* ts) = 0; + virtual lbool is_sat(T x) = 0; +}; + +template +class boolean_algebra : public positive_boolean_algebra { +public: + virtual T mk_not(T x) = 0; + //virtual lbool are_equivalent(T x, T y) = 0; + //virtual T simplify(T x) = 0; +}; + +#endif diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h new file mode 100644 index 000000000..d77e0548d --- /dev/null +++ b/src/math/automata/symbolic_automata.h @@ -0,0 +1,104 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + symbolic_automata.h + +Abstract: + + Symbolic Automata over Boolean Algebras, a la Margus Veanes Automata library. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-02-27. + +Revision History: + + +--*/ + +#ifndef SYMBOLIC_AUTOMATA_H_ +#define SYMBOLIC_AUTOMATA_H_ + + +#include "automaton.h" +#include "boolean_algebra.h" + + +template > +class symbolic_automata { + typedef automaton automaton_t; + typedef boolean_algebra ba_t; + typedef typename automaton_t::move move_t; + typedef vector moves_t; + typedef obj_ref ref_t; + typedef ref_vector refs_t; + + M& m; + ba_t& m_ba; + + + class block { + uint_set m_set; + unsigned m_rep; + bool m_rep_chosen; + public: + + block(): m_rep(0), m_rep_chosen(false) {} + + block(uint_set const& s): + m_set(s), + m_rep(0), + m_rep_chosen(false) { + } + + block(unsigned_vector const& vs) { + for (unsigned i = 0; i < vs.size(); ++i) { + m_set.insert(vs[i]); + } + m_rep_chosen = false; + m_rep = 0; + } + + block& operator=(block const& b) { + m_set = b.m_set; + m_rep = 0; + m_rep_chosen = false; + return *this; + } + + unsigned get_representative() { + if (!m_rep_chosen) { + uint_set::iterator it = m_set.begin(); + if (m_set.end() != it) { + m_rep = *it; + } + m_rep_chosen = true; + } + return m_rep; + } + + void add(unsigned i) { m_set.insert(i); } + bool contains(unsigned i) const { return m_set.contains(i); } + bool is_empty() const { return m_set.empty(); } + unsigned size() const { return m_set.num_elems(); } + void remove(unsigned i) { m_set.remove(i); m_rep_chosen = false; } + void clear() { m_set.reset(); m_rep_chosen = false; } + uint_set::iterator begin() { return m_set.begin(); } + uint_set::iterator end() { return m_set.end(); } + }; + +public: + symbolic_automata(M& m, ba_t& ba): m(m), m_ba(ba) {} + automaton_t* mk_determinstic(automaton_t& a); + automaton_t* mk_complement(automaton_t& a); + automaton_t* remove_epsilons(automaton_t& a); + automaton_t* mk_total(automaton_t& a); + automaton_t* mk_minimize(automaton_t& a); + automaton_t* mk_product(automaton_t& a, automaton_t& b); +}; + + + +#endif diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h new file mode 100644 index 000000000..db6172d49 --- /dev/null +++ b/src/math/automata/symbolic_automata_def.h @@ -0,0 +1,228 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + symbolic_automata_def.h + +Abstract: + + Symbolic Automata over Boolean Algebras, a la Margus Veanes Automata library. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-02-27. + +Revision History: + + +--*/ + +#ifndef SYMBOLIC_AUTOMATA_DEF_H_ +#define SYMBOLIC_AUTOMATA_DEF_H_ + + +#include "symbolic_automata.h" +#include "hashtable.h" + +typedef std::pair unsigned_pair; + + + +template +typename symbolic_automata::automaton_t* symbolic_automata::mk_total(automaton_t& a) { + unsigned dead_state = a.num_states(); + moves_t mvs, new_mvs; + for (unsigned i = 0; i < dead_state; ++i) { + mvs.reset(); + a.get_moves(i, mvs, true); + refs_t vs(m); + + for (unsigned j = 0; j < mvs.size(); ++j) { + vs.push_back(mvs[j].t()); + } + ref_t cond(m_ba.mk_not(m_ba.mk_or(vs.size(), vs.c_ptr())), m); + lbool is_sat = m_ba.is_sat(cond); + if (is_sat == l_undef) { + return 0; + } + if (is_sat == l_true) { + new_mvs.push_back(move_t(m, i, dead_state, cond)); + } + } + if (new_mvs.empty()) { + return a.clone(); + } + new_mvs.push_back(move_t(m, dead_state, dead_state, m_ba.mk_true())); + automaton_t::append_moves(0, a, new_mvs); + + return alloc(automaton_t, m, a.init(), a.final_states(), new_mvs); +} + +template +typename symbolic_automata::automaton_t* symbolic_automata::mk_minimize(automaton_t& a) { + if (a.is_empty()) { + return a.clone(); + } + + if (a.is_epsilon()) { + return a.clone(); + } + // SASSERT(a.is_deterministic()); + + scoped_ptr fa = mk_total(a); + if (!fa) { + return 0; + } + + block final_block(fa->final_states()); + block non_final_block(fa->non_final_states()); + vector blocks; + for (unsigned i = 0; i < fa->num_states(); ++i) { + if (fa->is_final_state(i)) { + blocks.push_back(final_block); + } + else { + blocks.push_back(non_final_block); + } + } + vector W; + if (final_block.size() > non_final_block.size()) { + W.push_back(non_final_block); + } + else { + W.push_back(final_block); + } + +#if 0 + + refs_t trail(m); + u_map gamma; + moves_t mvs; + while (!W.empty()) { + block R(W.back()); + W.pop_back(); + block Rcopy(R); + gamma.reset(); + uint_set::iterator it = Rcopy.begin(), end = Rcopy.end(); + for (; it != end; ++it) { + unsigned q = *it; + mvs.reset(); + fa->get_moves_to(q, mvs); + for (unsigned i = 0; i < mvs.size(); ++i) { + unsigned src = mvs[i].src(); + if (blocks[src].size() > 1) { + T* t = mvs[i](); + if (gamma.find(src, t1)) { + t = m_ba.mk_or(t, t1); + trail.push_back(t); + } + gamma.insert(src, t); + } + } + } + hashtable relevant; + u_map::iterator end = gamma.end(); + for (u_map::iterator it = gamma.begin(); it != end; ++it) { + relevant.insert(blocks[it->m_key]); + } + + } +#endif + + return 0; + +} + +template +typename symbolic_automata::automaton_t* symbolic_automata::mk_product(automaton_t& a, automaton_t& b) { + map, default_eq > state_ids; + unsigned_pair init_pair(a.init(), b.init()); + svector todo; + todo.push_back(init_pair); + state_ids.insert(init_pair, 0); + moves_t mvs; + unsigned_vector final; + if (a.is_final_state(a.init()) && b.is_final_state(b.init())) { + final.push_back(0); + } + unsigned n = 1; + moves_t mvsA, mvsB; + while (!todo.empty()) { + unsigned_pair curr_pair = todo.back(); + todo.pop_back(); + unsigned src = state_ids[curr_pair]; + mvsA.reset(); mvsB.reset(); + a.get_moves_from(curr_pair.first, mvsA, true); + b.get_moves_from(curr_pair.second, mvsB, true); + for (unsigned i = 0; i < mvsA.size(); ++i) { + for (unsigned j = 0; j < mvsB.size(); ++j) { + ref_t ab(m_ba.mk_and(mvsA[i].t(), mvsB[j].t()), m); + lbool is_sat = m_ba.is_sat(ab); + if (is_sat == l_false) { + continue; + } + else if (is_sat == l_undef) { + return 0; + } + unsigned_pair tgt_pair(mvsA[i].dst(), mvsB[j].dst()); + unsigned tgt; + if (!state_ids.find(tgt_pair, tgt)) { + tgt = n++; + state_ids.insert(tgt_pair, tgt); + todo.push_back(tgt_pair); + if (a.is_final_state(tgt_pair.first) && b.is_final_state(tgt_pair.second)) { + final.push_back(tgt); + } + } + mvs.push_back(move_t(m, src, tgt, ab)); + } + } + } + + if (final.empty()) { + return alloc(automaton_t, m); + } + vector inv(n, moves_t()); + for (unsigned i = 0; i < mvs.size(); ++i) { + move_t const& mv = mvs[i]; + inv[mv.dst()].push_back(move_t(m, mv.dst(), mv.src(), mv.t())); + } + + svector back_reachable(n, false); + for (unsigned i = 0; i < final.size(); ++i) { + back_reachable[final[i]] = true; + } + + unsigned_vector stack(final); + while (!stack.empty()) { + unsigned state = stack.back(); + stack.pop_back(); + moves_t const& mv = inv[state]; + for (unsigned i = 0; i < mv.size(); ++i) { + state = mv[i].dst(); + if (!back_reachable[state]) { + back_reachable[state] = true; + stack.push_back(state); + } + } + } + + moves_t mvs1; + for (unsigned i = 0; i < mvs.size(); ++i) { + move_t const& mv = mvs[i]; + if (back_reachable[mv.dst()]) { + mvs1.push_back(mv); + } + } + if (mvs1.empty()) { + return alloc(automaton_t, m); + } + else { + return alloc(automaton_t, m, 0, final, mvs1); + } +} + + + +#endif diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 33889e4ef..bc57a4099 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -425,7 +425,7 @@ private: DEBUG_CODE( for (unsigned i = 0; i < m_fmls.size(); ++i) { expr_ref tmp(m); - VERIFY(m_model->eval(m_fmls[i].get(), tmp)); + VERIFY(m_model->eval(m_fmls[i].get(), tmp, true)); CTRACE("sat", !m.is_true(tmp), tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m) << " to " << tmp << "\n"; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index cfd043895..551e80c85 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -25,6 +25,7 @@ Revision History: #include "theory_seq.h" #include "ast_trail.h" #include "theory_arith.h" +#include "smt_kernel.h" using namespace smt; @@ -36,6 +37,21 @@ struct display_expr { } }; +class seq_expr_solver : public expr_solver { + kernel m_kernel; +public: + seq_expr_solver(ast_manager& m, smt_params& fp): + m_kernel(m, fp) + {} + + virtual lbool check_sat(expr* e) { + m_kernel.push(); + m_kernel.assert_expr(e); + lbool r = m_kernel.check(); + m_kernel.pop(1); + return r; + } +}; void theory_seq::solution_map::update(expr* e, expr* r, dependency* d) { @@ -182,6 +198,7 @@ theory_seq::theory_seq(ast_manager& m): m(m), m_rep(m, m_dm), m_eq_id(0), + m_find(*this), m_factory(0), m_exclude(m), m_axioms(m), @@ -198,28 +215,31 @@ theory_seq::theory_seq(ast_manager& m): m_new_solution(false), m_new_propagation(false), m_mk_aut(m) { - m_prefix = "seq.prefix.suffix"; - m_suffix = "seq.suffix.prefix"; - m_contains_left = "seq.contains.left"; - m_contains_right = "seq.contains.right"; - m_accept = "aut.accept"; - m_reject = "aut.reject"; + m_prefix = "seq.p.suffix"; + m_suffix = "seq.s.prefix"; + m_accept = "aut.accept"; + m_reject = "aut.reject"; m_tail = "seq.tail"; m_nth = "seq.nth"; m_seq_first = "seq.first"; m_seq_last = "seq.last"; - m_indexof_left = "seq.indexof.left"; - m_indexof_right = "seq.indexof.right"; + m_indexof_left = "seq.idx.left"; + m_indexof_right = "seq.idx.right"; m_aut_step = "aut.step"; m_pre = "seq.pre"; // (seq.pre s l): prefix of string s of length l m_post = "seq.post"; // (seq.post s l): suffix of string s of length l m_eq = "seq.eq"; + } theory_seq::~theory_seq() { m_trail_stack.reset(); } +void theory_seq::init(context* ctx) { + theory::init(ctx); + m_mk_aut.set_solver(alloc(seq_expr_solver, m, get_context().get_fparams())); +} final_check_status theory_seq::final_check_eh() { TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n");); @@ -585,7 +605,6 @@ bool theory_seq::fixed_length(expr* e) { } if (is_skolem(m_tail, e) || is_skolem(m_seq_first, e) || is_skolem(m_indexof_left, e) || is_skolem(m_indexof_right, e) || - is_skolem(m_contains_left, e) || is_skolem(m_contains_right, e) || m_fixed.contains(e)) { return false; } @@ -885,8 +904,8 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) { enode_pair_vector eqs; linearize(dep, eqs, lits); TRACE("seq", - tout << "assert:" << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <- \n"; - display_deps(tout, dep); + tout << "assert: " << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <-\n"; + display_deps(tout, dep); ); justification* js = ctx.mk_justification( @@ -944,6 +963,7 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc // no-op } else if (m_util.is_seq(li) || m_util.is_re(li)) { + TRACE("seq", tout << "inserting " << li << " = " << ri << "\n";); m_eqs.push_back(mk_eqdep(li, ri, deps)); } else { @@ -1101,6 +1121,7 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de return true; } if (!ctx.inconsistent() && change) { + TRACE("seq", tout << "inserting equality\n";); m_eqs.push_back(eq(m_eq_id++, ls, rs, deps)); return true; } @@ -2096,6 +2117,7 @@ theory_var theory_seq::mk_var(enode* n) { } else { theory_var v = theory::mk_var(n); + m_find.mk_var(); get_context().attach_th_var(n, this, v); get_context().mark_as_relevant(n); return v; @@ -2897,8 +2919,8 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp new_eq_eh(deps, n1, n2); } TRACE("seq", - tout << "assert: " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "<- \n"; - ctx.display_literals_verbose(tout, lits);); + tout << "assert: " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << " <- \n"; + if (!lits.empty()) { ctx.display_literals_verbose(tout, lits); tout << "\n"; }); justification* js = ctx.mk_justification( ext_theory_eq_propagation_justification( @@ -2963,14 +2985,14 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { } else if (m_util.str.is_contains(e, e1, e2)) { if (is_true) { - expr_ref f1 = mk_skolem(m_contains_left, e1, e2); - expr_ref f2 = mk_skolem(m_contains_right, e1, e2); + expr_ref f1 = mk_skolem(m_indexof_left, e1, e2); + expr_ref f2 = mk_skolem(m_indexof_right, e1, e2); f = mk_concat(f1, e2, f2); propagate_eq(lit, f, e1, true); } else if (!canonizes(false, e)) { propagate_non_empty(lit, e2); -#if 0 +#if 1 dependency* dep = m_dm.mk_leaf(assumption(lit)); m_ncs.push_back(nc(expr_ref(e, m), dep)); #else @@ -3030,6 +3052,12 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { if (n1 != n2 && m_util.is_seq(n1->get_owner())) { + theory_var v1 = n1->get_th_var(get_id()); + theory_var v2 = n2->get_th_var(get_id()); + if (m_find.find(v1) == m_find.find(v2)) { + return; + } + m_find.merge(v1, v2); expr_ref o1(n1->get_owner(), m); expr_ref o2(n2->get_owner(), m); TRACE("seq", tout << o1 << " = " << o2 << "\n";); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index c600e443f..8206eeca4 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -28,6 +28,7 @@ Revision History: #include "scoped_ptr_vector.h" #include "automaton.h" #include "seq_rewriter.h" +#include "union_find.h" namespace smt { @@ -44,6 +45,7 @@ namespace smt { typedef trail_stack th_trail_stack; typedef std::pair expr_dep; typedef obj_map eqdep_map_t; + typedef union_find th_union_find; class seq_value_proc; @@ -292,7 +294,8 @@ namespace smt { scoped_vector m_eqs; // set of current equations. scoped_vector m_nqs; // set of current disequalities. scoped_vector m_ncs; // set of non-contains constraints. - unsigned m_eq_id; + unsigned m_eq_id; + th_union_find m_find; seq_factory* m_factory; // value factory exclusion_table m_exclude; // set of asserted disequalities. @@ -309,7 +312,7 @@ namespace smt { 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_prefix, m_suffix, 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_pre, m_post, m_eq; ptr_vector m_todo; @@ -329,6 +332,7 @@ namespace smt { obj_hashtable m_fixed; // string variables that are fixed length. + virtual void init(context* ctx); virtual final_check_status final_check_eh(); virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); } virtual bool internalize_term(app*); @@ -539,6 +543,11 @@ namespace smt { // model building app* mk_value(app* a); + th_trail_stack& get_trail_stack() { return m_trail_stack; } + 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) {} + }; }; diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 16154c7ef..15bfa69d2 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -20,9 +20,11 @@ Author: #include "ctx_simplify_tactic.h" #include "bv_decl_plugin.h" #include "ast_pp.h" +#include -static rational uMaxInt(unsigned sz) { - return rational::power_of_two(sz) - rational::one(); +static uint64_t uMaxInt(unsigned sz) { + SASSERT(sz <= 64); + return ULLONG_MAX >> (64u - sz); } namespace { @@ -30,26 +32,26 @@ namespace { struct interval { // l < h: [l, h] // l > h: [0, h] U [l, UMAX_INT] - rational l, h; + uint64_t l, h; unsigned sz; bool tight; interval() {} - interval(const rational& l, const rational& h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { + interval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { // canonicalize full set - if (is_wrapped() && l == h + rational::one()) { - this->l = rational::zero(); + if (is_wrapped() && l == h + 1) { + this->l = 0; this->h = uMaxInt(sz); } SASSERT(invariant()); } bool invariant() const { - return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz) && - (!is_wrapped() || l != h+rational::one()); + return l <= uMaxInt(sz) && h <= uMaxInt(sz) && + (!is_wrapped() || l != h+1); } - bool is_full() const { return l.is_zero() && h == uMaxInt(sz); } + bool is_full() const { return l == 0 && h == uMaxInt(sz); } bool is_wrapped() const { return l > h; } bool is_singleton() const { return l == h; } @@ -129,18 +131,18 @@ struct interval { /// return false if negation is empty bool negate(interval& result) const { if (!tight) { - result = interval(rational::zero(), uMaxInt(sz), true); + result = interval(0, uMaxInt(sz), true); return true; } if (is_full()) return false; - if (l.is_zero()) { - result = interval(h + rational::one(), uMaxInt(sz), sz); + if (l == 0) { + result = interval(h + 1, uMaxInt(sz), sz); } else if (uMaxInt(sz) == h) { - result = interval(rational::zero(), l - rational::one(), sz); + result = interval(0, l - 1, sz); } else { - result = interval(h + rational::one(), l - rational::one(), sz); + result = interval(h + 1, l - 1, sz); } return true; } @@ -152,59 +154,76 @@ std::ostream& operator<<(std::ostream& o, const interval& I) { } +struct undo_bound { + expr* e; + interval b; + bool fresh; + undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {} +}; + class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { typedef obj_map map; typedef obj_map expr_set; typedef obj_map expr_list_map; - ast_manager& m; - params_ref m_params; - bool m_propagate_eq; - bv_util m_bv; - vector m_scopes; - map *m_bound; - expr_list_map m_expr_vars; + ast_manager& m; + params_ref m_params; + bool m_propagate_eq; + bv_util m_bv; + vector m_scopes; + map m_bound; + expr_list_map m_expr_vars; + expr_set m_bound_exprs; - bool is_bound(expr *e, expr*& v, interval& b) { - rational n; + bool is_number(expr *e, uint64_t& n, unsigned& sz) const { + rational r; + if (m_bv.is_numeral(e, r, sz) && sz <= 64) { + n = r.get_uint64(); + return true; + } + return false; + } + + bool is_bound(expr *e, expr*& v, interval& b) const { + uint64_t n; expr *lhs, *rhs; unsigned sz; if (m_bv.is_bv_ule(e, lhs, rhs)) { - if (m_bv.is_numeral(lhs, n, sz)) { // C ule x <=> x uge C + if (is_number(lhs, n, sz)) { // C ule x <=> x uge C if (m_bv.is_numeral(rhs)) return false; b = interval(n, uMaxInt(sz), sz, true); v = rhs; return true; } - if (m_bv.is_numeral(rhs, n, sz)) { // x ule C - b = interval(rational::zero(), n, sz, true); + if (is_number(rhs, n, sz)) { // x ule C + b = interval(0, n, sz, true); v = lhs; return true; } } else if (m_bv.is_bv_sle(e, lhs, rhs)) { - if (m_bv.is_numeral(lhs, n, sz)) { // C sle x <=> x sge C + if (is_number(lhs, n, sz)) { // C sle x <=> x sge C if (m_bv.is_numeral(rhs)) return false; - b = interval(n, rational::power_of_two(sz-1) - rational::one(), sz, true); + b = interval(n, (1ull << (sz-1)) - 1, sz, true); v = rhs; return true; } - if (m_bv.is_numeral(rhs, n, sz)) { // x sle C - b = interval(rational::power_of_two(sz-1), n, sz, true); + if (is_number(rhs, n, sz)) { // x sle C + b = interval(1ull << (sz-1), n, sz, true); v = lhs; return true; } } else if (m.is_eq(e, lhs, rhs)) { - if (m_bv.is_numeral(lhs, n, sz)) { + if (is_number(lhs, n, sz)) { if (m_bv.is_numeral(rhs)) return false; b = interval(n, n, sz, true); v = rhs; return true; } - if (m_bv.is_numeral(rhs, n, sz)) { + if (is_number(rhs, n, sz)) { b = interval(n, n, sz, true); v = lhs; return true; @@ -238,27 +257,29 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { } bool expr_has_bounds(expr* t) { + bool has_bounds = false; + if (m_bound_exprs.find(t, has_bounds)) + return has_bounds; + app* a = to_app(t); if ((m_bv.is_bv_ule(t) || m_bv.is_bv_sle(t) || m.is_eq(t)) && - (m_bv.is_numeral(a->get_arg(0)) || m_bv.is_numeral(a->get_arg(1)))) - return true; - - for (unsigned i = 0; i < a->get_num_args(); ++i) { - if (expr_has_bounds(a->get_arg(i))) - return true; + (m_bv.is_numeral(a->get_arg(0)) || m_bv.is_numeral(a->get_arg(1)))) { + has_bounds = true; } - return false; + + for (unsigned i = 0; !has_bounds && i < a->get_num_args(); ++i) { + has_bounds = expr_has_bounds(a->get_arg(i)); + } + + m_bound_exprs.insert(t, has_bounds); + return has_bounds; } public: - bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { - m_scopes.push_back(map()); - m_bound = &m_scopes.back(); updt_params(p); } - virtual void updt_params(params_ref const & p) { m_propagate_eq = p.get_bool("propagate_eq", false); } @@ -285,10 +306,21 @@ public: if (sign) VERIFY(b.negate(b)); - push(); TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); - interval& r = m_bound->insert_if_not_there2(t1, b)->get_data().m_value; - return r.intersect(b, r); + map::obj_map_entry* e = m_bound.find_core(t1); + if (e) { + interval& old = e->get_data().m_value; + interval intr; + if (!old.intersect(b, intr)) + return false; + if (old == intr) + return true; + m_scopes.insert(undo_bound(t1, old, false)); + old = intr; + } else { + m_bound.insert(t1, b); + m_scopes.insert(undo_bound(t1, interval(), true)); + } } return true; } @@ -297,7 +329,7 @@ public: expr* t1; interval b; - if (m_bound->find(t, b) && b.is_singleton()) { + if (m_bound.find(t, b) && b.is_singleton()) { result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); return true; } @@ -324,16 +356,17 @@ public: interval ctx, intr; result = 0; - if (m_bound->find(t1, ctx)) { + if (b.is_full() && b.tight) { + result = m.mk_true(); + } else if (m_bound.find(t1, ctx)) { if (ctx.implies(b)) { result = m.mk_true(); } else if (!b.intersect(ctx, intr)) { result = m.mk_false(); } else if (m_propagate_eq && intr.is_singleton()) { - result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1))); + result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), + m.get_sort(t1))); } - } else if (b.is_full() && b.tight) { - result = m.mk_true(); } CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";); @@ -346,36 +379,43 @@ public: if (m_bv.is_numeral(t)) return false; + while (m.is_not(t, t)); + expr_set* used_exprs = get_expr_vars(t); - for (map::iterator I = m_bound->begin(), E = m_bound->end(); I != E; ++I) { + for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) return true; } - while (m.is_not(t, t)); - expr* t1; interval b; // skip common case: single bound constraint without any context for simplification if (is_bound(t, t1, b)) { - return m_bound->contains(t1); + return b.is_full() || m_bound.contains(t1); } return expr_has_bounds(t); } - virtual void push() { - TRACE("bv", tout << "push\n";); - unsigned sz = m_scopes.size(); - m_scopes.resize(sz + 1); - m_bound = &m_scopes.back(); - m_bound->~map(); - new (m_bound) map(m_scopes[sz - 1]); - } - virtual void pop(unsigned num_scopes) { TRACE("bv", tout << "pop: " << num_scopes << "\n";); - m_scopes.shrink(m_scopes.size() - num_scopes); - m_bound = &m_scopes.back(); + if (m_scopes.empty()) + return; + unsigned target = m_scopes.size() - num_scopes; + if (target == 0) { + m_bound.reset(); + m_scopes.reset(); + return; + } + for (unsigned i = m_scopes.size()-1; i >= target; --i) { + undo_bound& undo = m_scopes[i]; + SASSERT(m_bound.contains(undo.e)); + if (undo.fresh) { + m_bound.erase(undo.e); + } else { + m_bound.insert(undo.e, undo.b); + } + } + m_scopes.shrink(target); } virtual simplifier * translate(ast_manager & m) { @@ -383,7 +423,7 @@ public: } virtual unsigned scope_level() const { - return m_scopes.size() - 1; + return m_scopes.size(); } }; diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index f127614aa..1cda9cc6f 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -36,7 +36,7 @@ public: virtual ~ctx_propagate_assertions() {} virtual bool assert_expr(expr * t, bool sign); virtual bool simplify(expr* t, expr_ref& result); - virtual void push(); + void push(); virtual void pop(unsigned num_scopes); virtual unsigned scope_level() const { return m_scopes.size(); } virtual simplifier * translate(ast_manager & m); @@ -260,10 +260,6 @@ struct ctx_simplify_tactic::imp { return m_simp->scope_level(); } - void push() { - m_simp->push(); - } - void restore_cache(unsigned lvl) { if (lvl >= m_cache_undo.size()) return; diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index 7b1507f67..d6ebf5cbd 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -31,7 +31,6 @@ public: virtual bool assert_expr(expr * t, bool sign) = 0; virtual bool simplify(expr* t, expr_ref& result) = 0; virtual bool may_simplify(expr* t) { return true; } - virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0; virtual simplifier * translate(ast_manager & m) = 0; virtual unsigned scope_level() const = 0;