From 41ca9560126c2a19549b10eb7974683a6d4d0ccc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 17 Jul 2019 12:45:30 -0400
Subject: [PATCH] expose import model converter over Python, document it, add
partial order axioms for lex, disable linear order axioms, prepare ground for
re-adding clauses from reconstruction stack
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/python/z3/z3.py | 10 ++
src/api/z3_api.h | 8 ++
src/sat/sat_model_converter.cpp | 156 +++++++++++++++++++-------------
src/sat/sat_model_converter.h | 15 ++-
src/sat/sat_simplifier.cpp | 4 +-
src/sat/sat_solver.cpp | 10 +-
src/sat/sat_solver.h | 1 -
src/sat/tactic/goal2sat.cpp | 1 -
src/smt/smt_theory.cpp | 3 +
src/smt/theory_seq.cpp | 72 +++++++++++++--
src/smt/theory_seq.h | 3 +
11 files changed, 202 insertions(+), 81 deletions(-)
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index a3f63a696..cd3253495 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6646,6 +6646,10 @@ class Solver(Z3PPObject):
except Z3Exception:
raise Z3Exception("model is not available")
+ def import_model_converter(self, other):
+ """Import model converter from other into the current solver"""
+ Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
+
def unsat_core(self):
"""Return a subset (as an AST vector) of the assumptions provided to the last check().
@@ -8310,11 +8314,17 @@ def AtLeast(*args):
_args, sz = _to_ast_array(args1)
return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
+def _reorder_pb_arg(arg):
+ a, b = arg
+ if not _is_int(b) and _is_int(a):
+ return b, a
+ return arg
def _pb_args_coeffs(args, default_ctx = None):
args = _get_args_ast_list(args)
if len(args) == 0:
return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
+ args = [_reorder_pb_arg(arg) for arg in args]
args, coeffs = zip(*args)
if z3_debug():
_z3_assert(len(args) > 0, "Non empty list of arguments expected")
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 642c959cc..8acf35d2c 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6213,6 +6213,14 @@ extern "C" {
/**
\brief Ad-hoc method for importing model conversion from solver.
+
+ This method is used for scenarios where \c src has been used to solve a set
+ of formulas and was interrupted. The \c dst solver may be a strengthening of \c src
+ obtained from cubing (assigning a subset of literals or adding constraints over the
+ assertions available in \c src). If \c dst ends up being satisfiable, the model for \c dst
+ may not correspond to a model of the original formula due to inprocessing in \c src.
+ This method is used to take the side-effect of inprocessing into account when returning
+ a model for \c dst.
def_API('Z3_solver_import_model_converter', VOID, (_in(CONTEXT), _in(SOLVER), _in(SOLVER)))
*/
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index ddb7df74b..3a951025b 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -23,16 +23,12 @@ Revision History:
namespace sat {
- model_converter::model_converter(): m_solver(nullptr) {
+ model_converter::model_converter(): m_solver(nullptr), m_exposed_lim(0) {
}
model_converter::~model_converter() {
- reset();
}
- void model_converter::reset() {
- m_entries.finalize();
- }
model_converter& model_converter::operator=(model_converter const& other) {
copy(other);
@@ -40,21 +36,19 @@ namespace sat {
}
bool model_converter::legal_to_flip(bool_var v) const {
- // std::cout << "check " << v << " " << m_solver << "\n";
if (m_solver && m_solver->is_assumption(v)) {
- std::cout << "flipping assumption v" << v << "\n";
+ IF_VERBOSE(0, verbose_stream() << "flipping assumption v" << v << "\n";);
UNREACHABLE();
throw solver_exception("flipping assumption");
}
if (m_solver && m_solver->is_external(v) && m_solver->is_incremental()) {
- std::cout << "flipping external v" << v << "\n";
+ IF_VERBOSE(0, verbose_stream() << "flipping external v" << v << "\n";);
UNREACHABLE();
throw solver_exception("flipping external");
}
return !m_solver || !m_solver->is_assumption(v);
}
-
void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv const& stack) const {
SASSERT(!stack.empty());
unsigned sz = stack.size();
@@ -73,46 +67,33 @@ namespace sat {
}
void model_converter::operator()(model & m) const {
- vector<entry>::const_iterator begin = m_entries.begin();
- vector<entry>::const_iterator it = m_entries.end();
bool first = false;
- //SASSERT(!m_solver || m_solver->check_clauses(m));
- while (it != begin) {
- --it;
- bool_var v0 = it->var();
- SASSERT(it->get_kind() != ELIM_VAR || v0 == null_bool_var || m[v0] == l_undef);
- // if it->get_kind() == BCE, then it might be the case that m[v] != l_undef,
+ literal_vector clause;
+ for (unsigned i = m_entries.size(); i-- > m_exposed_lim; ) {
+ entry const& e = m_entries[i];
+ bool_var v0 = e.var();
+ SASSERT(e.get_kind() != ELIM_VAR || v0 == null_bool_var || m[v0] == l_undef);
+ // if e.get_kind() == BCE, then it might be the case that m[v] != l_undef,
// and the following procedure flips its value.
bool sat = false;
bool var_sign = false;
unsigned index = 0;
- literal_vector clause;
+ clause.reset();
VERIFY(v0 == null_bool_var || legal_to_flip(v0));
- for (literal l : it->m_clauses) {
+ for (literal l : e.m_clauses) {
if (l == null_literal) {
// end of clause
- if (!sat && it->get_kind() == ATE) {
- IF_VERBOSE(0, display(verbose_stream() << "violated ate\n", *it) << "\n");
- IF_VERBOSE(0, for (unsigned v = 0; v < m.size(); ++v) verbose_stream() << v << " := " << m[v] << "\n";);
- IF_VERBOSE(0, display(verbose_stream()));
- UNREACHABLE();
- first = false;
- }
- if (!sat && it->get_kind() != ATE && v0 != null_bool_var) {
+ VERIFY (sat || e.get_kind() != ATE);
+ if (!sat && e.get_kind() != ATE && v0 != null_bool_var) {
VERIFY(legal_to_flip(v0));
m[v0] = var_sign ? l_false : l_true;
- //IF_VERBOSE(0, verbose_stream() << "assign " << v0 << " "<< m[v0] << "\n");
}
- elim_stack* st = it->m_elim_stack[index];
+ elim_stack* st = e.m_elim_stack[index];
if (st) {
process_stack(m, clause, st->stack());
}
sat = false;
- if (first && m_solver && !m_solver->check_clauses(m)) {
- IF_VERBOSE(0, display(verbose_stream() << "after processing stack\n", *it) << "\n");
- IF_VERBOSE(0, display(verbose_stream()));
- first = false;
- }
+ VERIFY(!first || !m_solver || m_solver->check_clauses(m));
++index;
clause.reset();
continue;
@@ -123,7 +104,6 @@ namespace sat {
continue;
bool sign = l.sign();
bool_var v = l.var();
- if (v >= m.size()) std::cout << v << " model size: " << m.size() << "\n";
VERIFY(v < m.size());
if (v == v0)
var_sign = sign;
@@ -133,25 +113,21 @@ namespace sat {
VERIFY(legal_to_flip(v));
// clause can be satisfied by assigning v.
m[v] = sign ? l_false : l_true;
- // if (first) std::cout << "set: " << l << "\n";
sat = true;
- if (first && m_solver && !m_solver->check_clauses(m)) {
- IF_VERBOSE(0, display(verbose_stream() << "after flipping undef\n", *it) << "\n");
- first = false;
- }
+ VERIFY(!first || !m_solver || m_solver->check_clauses(m));
}
}
DEBUG_CODE({
// all clauses must be satisfied
bool sat = false;
bool undef = false;
- for (literal const& l : it->m_clauses) {
+ for (literal const& l : e.m_clauses) {
if (l == null_literal) {
CTRACE("sat", !sat,
if (m_solver) m_solver->display(tout);
display(tout);
for (unsigned v = 0; v < m.size(); ++v) tout << v << ": " << m[v] << "\n";
- for (literal const& l2 : it->m_clauses) {
+ for (literal const& l2 : e.m_clauses) {
if (l2 == null_literal) tout << "\n"; else tout << l2 << " ";
if (&l == &l2) break;
}
@@ -179,24 +155,21 @@ namespace sat {
*/
bool model_converter::check_model(model const & m) const {
bool ok = true;
- vector<entry>::const_iterator begin = m_entries.begin();
- vector<entry>::const_iterator it = m_entries.end();
- while (it != begin) {
- --it;
+ for (entry const & e : m_entries) {
bool sat = false;
- literal_vector::const_iterator it2 = it->m_clauses.begin();
- literal_vector::const_iterator itbegin = it2;
- literal_vector::const_iterator end2 = it->m_clauses.end();
- for (; it2 != end2; ++it2) {
- literal l = *it2;
+ literal_vector::const_iterator it = e.m_clauses.begin();
+ literal_vector::const_iterator itbegin = it;
+ literal_vector::const_iterator end = e.m_clauses.end();
+ for (; it != end; ++it) {
+ literal l = *it;
if (l == null_literal) {
// end of clause
if (!sat) {
- TRACE("sat_model_bug", tout << "failed eliminated: " << mk_lits_pp(static_cast<unsigned>(it2 - itbegin), itbegin) << "\n";);
+ TRACE("sat_model_bug", tout << "failed eliminated: " << mk_lits_pp(static_cast<unsigned>(it - itbegin), itbegin) << "\n";);
ok = false;
}
sat = false;
- itbegin = it2;
+ itbegin = it;
itbegin++;
continue;
}
@@ -239,6 +212,16 @@ namespace sat {
stackv().reset();
}
+ void model_converter::set_clause(entry & e, literal l1, literal l2) {
+ e.m_clause.push_back(l1);
+ e.m_clause.push_back(l2);
+ }
+
+ void model_converter::set_clause(entry & e, clause const & c) {
+ e.m_clause.append(c.size(), c.begin());
+ }
+
+
void model_converter::insert(entry & e, clause const & c) {
SASSERT(c.contains(e.var()));
SASSERT(m_entries.begin() <= &e);
@@ -349,27 +332,27 @@ namespace sat {
out << l;
}
out << ")";
- for (literal l : entry.m_clauses) {
- if (l != null_literal && l.var() != null_bool_var) {
- if (false && m_solver && m_solver->was_eliminated(l.var())) out << "\neliminated: " << l;
- }
- }
return out;
}
void model_converter::copy(model_converter const & src) {
- reset();
+ m_entries.reset();
m_entries.append(src.m_entries);
+ m_exposed_lim = src.m_exposed_lim;
}
void model_converter::flush(model_converter & src) {
VERIFY(this != &src);
m_entries.append(src.m_entries);
+ m_exposed_lim = src.m_exposed_lim;
src.m_entries.reset();
+ src.m_exposed_lim = 0;
}
void model_converter::collect_vars(bool_var_set & s) const {
- for (entry const & e : m_entries) s.insert(e.m_var);
+ for (entry const & e : m_entries) {
+ s.insert(e.m_var);
+ }
}
unsigned model_converter::max_var(unsigned min) const {
@@ -398,7 +381,8 @@ namespace sat {
void model_converter::expand(literal_vector& update_stack) {
sat::literal_vector clause;
- for (entry const& e : m_entries) {
+ for (unsigned i = m_exposed_lim; i < m_entries.size(); ++i) {
+ entry const& e = m_entries[i];
unsigned index = 0;
clause.reset();
for (literal l : e.m_clauses) {
@@ -427,6 +411,56 @@ namespace sat {
}
}
}
+ m_exposed_lim = m_entries.size();
+ }
+
+ void model_converter::init_search(solver& s) {
+#if 0
+ unsigned j = 0, k = 0;
+ literal_vector clause;
+ for (unsigned i = 0; i < m_entries.size(); ++i) {
+ entry & e = m_entries[i];
+ if (!m_mark[e.var()]) {
+ m_entries[j++] = e;
+ if (i < m_exposed_lim) k++;
+ continue;
+ }
+ clause.reset();
+ // For covered clauses we record the original clause. The role of m_clauses is to record ALA
+ // tautologies and are not part of the clause that is removed.
+
+ if (!e.m_clause.empty()) {
+ clause.append(e.m_clause);
+ s.mk_clause(clause.size(), clause.c_ptr(), false);
+ continue;
+ }
+ for (literal lit : e.m_clauses) {
+ if (lit == null_literal) {
+ s.mk_clause(clause.size(), clause.c_ptr(), false);
+ clause.reset();
+ }
+ else {
+ clause.push_back(lit);
+ }
+ }
+ }
+ m_entries.shrink(j);
+ m_exposed_lim = k;
+ for (bool& m : m_mark) {
+ m = false;
+ }
+#endif
+ }
+
+ void model_converter::add_clause(unsigned n, literal const* lits) {
+ if (m_entries.empty()) {
+ return;
+ }
+ // TBD: we just mark variables instead of literals because entries don't have directly literal information.
+ for (unsigned i = 0; i < n; ++i) {
+ m_mark.reserve(lits[i].var() + 1);
+ m_mark[lits[i].var()] = true;
+ }
}
};
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
index 2ca340e5d..585f8c312 100644
--- a/src/sat/sat_model_converter.h
+++ b/src/sat/sat_model_converter.h
@@ -72,20 +72,25 @@ namespace sat {
bool_var m_var;
kind m_kind;
literal_vector m_clauses; // the different clauses are separated by null_literal
+ literal_vector m_clause; // original clause in case of CCE
sref_vector<elim_stack> m_elim_stack;
entry(kind k, bool_var v): m_var(v), m_kind(k) {}
public:
entry(entry const & src):
m_var(src.m_var),
m_kind(src.m_kind),
- m_clauses(src.m_clauses) {
+ m_clauses(src.m_clauses),
+ m_clause(src.m_clause)
+ {
m_elim_stack.append(src.m_elim_stack);
}
bool_var var() const { return m_var; }
kind get_kind() const { return m_kind; }
};
private:
- vector<entry> m_entries;
+ vector<entry> m_entries; // entries accumulated during SAT search
+ unsigned m_exposed_lim; // last entry that was exposed to model converter.
+ svector<bool> m_mark; // literals that are used in asserted clauses.
solver const* m_solver;
elim_stackv m_elim_stack;
@@ -113,6 +118,8 @@ namespace sat {
void insert(entry & e, literal l1, literal l2);
void insert(entry & e, clause_wrapper const & c);
void insert(entry & c, literal_vector const& covered_clause);
+ void set_clause(entry & e, literal l1, literal l2);
+ void set_clause(entry & e, clause const & c);
void add_ate(literal_vector const& lits);
void add_ate(literal l1, literal l2);
@@ -121,7 +128,9 @@ namespace sat {
bool empty() const { return m_entries.empty(); }
unsigned size() const { return m_entries.size(); }
- void reset();
+ void init_search(solver& s);
+ void add_clause(unsigned n, literal const* lits);
+
bool check_invariant(unsigned num_vars) const;
void display(std::ostream & out) const;
bool check_model(model const & m) const;
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 95d60491c..d918f7459 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1223,8 +1223,6 @@ namespace sat {
}
for (unsigned i = idx; i > 0; --i) {
literal lit = m_covered_clause[i];
- //s.mark_visited(lit);
- //continue;
if (!s.is_marked(lit)) continue;
clause_ante const& ante = m_covered_antecedent[i];
if (ante.cls()) {
@@ -1591,6 +1589,7 @@ namespace sat {
}
}
m_mc.insert(new_entry, m_covered_clause);
+ m_mc.set_clause(new_entry, c);
}
void block_covered_binary(watched const& w, literal l1, literal blocked, model_converter::kind k) {
@@ -1600,6 +1599,7 @@ namespace sat {
TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";);
s.set_learned(l1, l2);
m_mc.insert(new_entry, m_covered_clause);
+ m_mc.set_clause(new_entry, l1, l2);
m_queue.decreased(~l2);
}
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 722b91b26..b88a3ec3c 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -357,6 +357,9 @@ namespace sat {
m_drat.add(m_lemma);
}
++m_stats.m_non_learned_generation;
+ if (!m_searching) {
+ m_mc.add_clause(num_lits, lits);
+ }
}
switch (num_lits) {
@@ -1832,8 +1835,8 @@ namespace sat {
m_min_core_valid = false;
m_min_core.reset();
m_simplifier.init_search();
+ m_mc.init_search(*this);
TRACE("sat", display(tout););
-
}
bool solver::should_simplify() const {
@@ -4485,13 +4488,14 @@ namespace sat {
lbool solver::get_bounded_consequences(literal_vector const& asms, bool_var_vector const& vars, vector<literal_vector>& conseq) {
bool_var_set unfixed_vars;
unsigned num_units = 0, num_iterations = 0;
- for (unsigned i = 0; i < vars.size(); ++i) {
- unfixed_vars.insert(vars[i]);
+ for (bool_var v : vars) {
+ unfixed_vars.insert(v);
}
TRACE("sat", tout << asms << "\n";);
m_antecedents.reset();
pop_to_base_level();
if (inconsistent()) return l_false;
+ flet<bool> _searching(m_searching, true);
init_search();
propagate(false);
if (inconsistent()) return l_false;
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index f817cb190..9532b4bb4 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -348,7 +348,6 @@ namespace sat {
bool limit_reached() {
if (!m_rlimit.inc()) {
- m_mc.reset();
m_model_is_current = false;
TRACE("sat", tout << "canceled\n";);
m_reason_unknown = "sat.canceled";
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index a53ed94a8..884b533cd 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -934,7 +934,6 @@ void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) {
void sat2goal::mc::flush_gmc() {
sat::literal_vector updates;
m_smc.expand(updates);
- m_smc.reset();
if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
// now gmc owns the model converter
sat::literal_vector clause;
diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
index 9fec0e1d3..642c0aca8 100644
--- a/src/smt/smt_theory.cpp
+++ b/src/smt/smt_theory.cpp
@@ -120,6 +120,9 @@ namespace smt {
}
literal theory::mk_eq(expr * a, expr * b, bool gate_ctx) {
+ if (a == b) {
+ return true_literal;
+ }
context & ctx = get_context();
app * eq = ctx.mk_eq_atom(a, b);
TRACE("mk_var_bug", tout << "mk_eq: " << eq->get_id() << " " << a->get_id() << " " << b->get_id() << "\n";
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 64ca608cd..c005a859c 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -268,6 +268,7 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
m_params(params),
m_rep(m, m_dm),
m_reset_cache(false),
+ m_lts_checked(false),
m_eq_id(0),
m_find(*this),
m_overlap(m),
@@ -336,12 +337,16 @@ final_check_status theory_seq::final_check_eh() {
++m_stats.m_solve_eqs;
TRACEFIN("solve_eqs");
return FC_CONTINUE;
- }
+ }
if (check_contains()) {
++m_stats.m_propagate_contains;
TRACEFIN("propagate_contains");
return FC_CONTINUE;
}
+ if (check_lts()) {
+ TRACEFIN("check_lts");
+ return FC_CONTINUE;
+ }
if (solve_nqs(0)) {
++m_stats.m_solve_nqs;
TRACEFIN("solve_nqs");
@@ -2147,6 +2152,57 @@ bool theory_seq::check_contains() {
}
return m_new_propagation || ctx.inconsistent();
}
+
+bool theory_seq::check_lts() {
+ context& ctx = get_context();
+ if (m_lts.empty() || m_lts_checked) {
+ return false;
+ }
+ unsigned sz = m_lts.size();
+ m_trail_stack.push(value_trail<theory_seq, bool>(m_lts_checked));
+ m_lts_checked = true;
+ expr* a = nullptr, *b = nullptr, *c = nullptr, *d = nullptr;
+ bool is_strict1, is_strict2;
+ for (unsigned i = 0; i + 1 < sz; ++i) {
+ expr* p1 = m_lts[i];
+ VERIFY(m_util.str.is_lt(p1, a, b) || m_util.str.is_le(p1, a, b));
+ literal r1 = ctx.get_literal(p1);
+ if (ctx.get_assignment(r1) == l_false) {
+ std::swap(a, b);
+ r1.neg();
+ is_strict1 = m_util.str.is_le(p1);
+ }
+ else {
+ is_strict1 = m_util.str.is_lt(p1);
+ }
+ for (unsigned j = i + 1; j < sz; ++j) {
+ expr* p2 = m_lts[j];
+ VERIFY(m_util.str.is_lt(p2, c, d) || m_util.str.is_le(p2, c, d));
+ literal r2 = ctx.get_literal(p2);
+ if (ctx.get_assignment(r2) == l_false) {
+ std::swap(c, d);
+ r2.neg();
+ is_strict2 = m_util.str.is_le(p2);
+ }
+ else {
+ is_strict2 = m_util.str.is_lt(p2);
+ }
+ if (ctx.get_enode(b)->get_root() == ctx.get_enode(c)->get_root()) {
+
+ literal eq = (b == c) ? true_literal : mk_eq(b, c, false);
+ bool is_strict = is_strict1 || is_strict2;
+ if (is_strict) {
+ add_axiom(~r1, ~r2, ~eq, mk_literal(m_util.str.mk_lex_lt(a, d)));
+ }
+ else {
+ add_axiom(~r1, ~r2, ~eq, mk_literal(m_util.str.mk_lex_le(a, d)));
+ }
+ }
+ }
+ }
+ return true;
+}
+
/*
- Eqs = 0
- Diseqs evaluate to false
@@ -5491,7 +5547,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
// no-op
}
else if (m_util.str.is_lt(e) || m_util.str.is_le(e)) {
- // no-op
+ m_lts.push_back(e);
}
else {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
@@ -5619,6 +5675,7 @@ void theory_seq::push_scope_eh() {
m_eqs.push_scope();
m_nqs.push_scope();
m_ncs.push_scope();
+ m_lts.push_scope();
m_internal_nth_lim.push_back(m_internal_nth_es.size());
}
@@ -5632,6 +5689,7 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) {
m_eqs.pop_scope(num_scopes);
m_nqs.pop_scope(num_scopes);
m_ncs.pop_scope(num_scopes);
+ m_lts.pop_scope(num_scopes);
m_rewrite.reset();
if (ctx.get_base_level() > ctx.get_scope_level() - num_scopes) {
m_replay.reset();
@@ -5927,10 +5985,10 @@ void theory_seq::propagate_not_suffix(expr* e) {
!(e1 < e2) => e1 = e2 or e2 = empty or e2 = xdz
!(e1 < e2) => e1 = e2 or e2 = empty or d < c
!(e1 < e2) => e1 = e2 or e1 = xcy
+ !(e1 = e2) or !(e1 < e2)
optional:
e1 < e2 or e1 = e2 or e2 < e1
- !(e1 = e2) or !(e1 < e2)
!(e1 = e2) or !(e2 < e1)
!(e1 < e2) or !(e2 < e1)
*/
@@ -5962,13 +6020,7 @@ void theory_seq::add_lt_axiom(expr* n) {
add_axiom(lt, eq, e1xcy);
add_axiom(lt, eq, emp2, ltdc);
add_axiom(lt, eq, emp2, e2xdz);
- if (e1->get_id() <= e2->get_id()) {
- literal gt = mk_literal(m_util.str.mk_lex_lt(e2, e1));
- add_axiom(lt, eq, gt);
- add_axiom(~eq, ~lt);
- add_axiom(~eq, ~gt);
- add_axiom(~lt, ~gt);
- }
+ add_axiom(~eq, ~lt);
}
/**
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index bfd982279..fd4b59e38 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -328,6 +328,8 @@ namespace smt {
scoped_vector<eq> m_eqs; // set of current equations.
scoped_vector<ne> m_nqs; // set of current disequalities.
scoped_vector<nc> m_ncs; // set of non-contains constraints.
+ scoped_vector<expr*> m_lts; // set of asserted str.<, str.<= literals
+ bool m_lts_checked;
unsigned m_eq_id;
th_union_find m_find;
@@ -460,6 +462,7 @@ namespace smt {
bool check_extensionality();
bool check_contains();
+ bool check_lts();
bool solve_eqs(unsigned start);
bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep, unsigned idx);
bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);