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

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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-17 12:45:30 -04:00
parent 7ed5ca05e3
commit 41ca956012
11 changed files with 202 additions and 81 deletions
Download patch file Download diff file Expand all files Collapse all files

156
src/sat/sat_model_converter.cpp
View file

@ -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;
}
}
};

15
src/sat/sat_model_converter.h
View file

@ -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;

4
src/sat/sat_simplifier.cpp
View file

@ -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);
}

10
src/sat/sat_solver.cpp
View file

@ -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;

1
src/sat/sat_solver.h
View file

@ -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";

1
src/sat/tactic/goal2sat.cpp
View file

@ -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;