mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
commit
8a49cf62f4
|
@ -43,6 +43,7 @@ Proof checker for clauses created during search.
|
|||
#include "util/small_object_allocator.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "smt/smt_solver.h"
|
||||
#include "sat/sat_solver.h"
|
||||
#include "sat/sat_drat.h"
|
||||
|
@ -132,7 +133,7 @@ public:
|
|||
clause1.push_back(hint);
|
||||
trim.assume(m_clauses.size());
|
||||
m_clauses.push_back(clause1);
|
||||
m_is_infer.push_back(false);
|
||||
m_is_infer.push_back(true);
|
||||
|
||||
if (clause.empty()) {
|
||||
mk_clause(clause);
|
||||
|
@ -167,12 +168,22 @@ public:
|
|||
trim.updt_params(p);
|
||||
}
|
||||
|
||||
expr_ref mk_dep(unsigned id, unsigned_vector const& deps) {
|
||||
arith_util a(m);
|
||||
expr_ref_vector args(m);
|
||||
args.push_back(a.mk_int(id));
|
||||
for (auto d : deps)
|
||||
args.push_back(a.mk_int(d));
|
||||
return expr_ref(m.mk_app(symbol("deps"), args.size(), args.data(), m.mk_proof_sort()), m);
|
||||
}
|
||||
|
||||
void do_trim(std::ostream& out) {
|
||||
ast_pp_util pp(m);
|
||||
auto ids = trim.trim();
|
||||
for (unsigned id : ids) {
|
||||
auto const& clause = m_clauses[id];
|
||||
for (auto const& [id, deps] : ids) {
|
||||
auto& clause = m_clauses[id];
|
||||
bool is_infer = m_is_infer[id];
|
||||
clause.push_back(mk_dep(id, deps));
|
||||
for (expr* e : clause)
|
||||
pp.collect(e);
|
||||
|
||||
|
@ -268,8 +279,10 @@ public:
|
|||
}
|
||||
|
||||
void add_literal(expr* e) override {
|
||||
if (m.is_proof(e))
|
||||
m_proof_hint = to_app(e);
|
||||
if (m.is_proof(e)) {
|
||||
if (!m_proof_hint)
|
||||
m_proof_hint = to_app(e);
|
||||
}
|
||||
else if (!m.is_bool(e))
|
||||
throw default_exception("literal should be either a Proof or Bool");
|
||||
else
|
||||
|
|
|
@ -29,19 +29,20 @@ namespace sat {
|
|||
Output: reduced trail - result
|
||||
*/
|
||||
|
||||
unsigned_vector proof_trim::trim() {
|
||||
unsigned_vector result;
|
||||
vector<std::pair<unsigned, unsigned_vector>> proof_trim::trim() {
|
||||
m_result.reset();
|
||||
m_core_literals.reset();
|
||||
m_propagated.resize(num_vars(), false);
|
||||
m_core_literals.insert(literal_vector());
|
||||
m_core_literals.insert(m_conflict);
|
||||
conflict_analysis_core(m_conflict, m_conflict_clause);
|
||||
|
||||
|
||||
IF_VERBOSE(10, s.display(verbose_stream() << "trim\n"));
|
||||
|
||||
auto const& [id, cl, clp, is_add, is_initial] = m_trail.back();
|
||||
SASSERT(cl.empty());
|
||||
result.push_back(id);
|
||||
m_result.push_back({id, unsigned_vector()});
|
||||
conflict_analysis_core(m_conflict, m_conflict_clause);
|
||||
m_trail.pop_back();
|
||||
|
||||
|
||||
|
@ -55,17 +56,17 @@ namespace sat {
|
|||
prune_trail(cl, clp);
|
||||
IF_VERBOSE(10, s.display(verbose_stream() << "\n"));
|
||||
del(cl, clp);
|
||||
if (!in_core(cl, clp))
|
||||
if (!in_core(cl))
|
||||
continue;
|
||||
IF_VERBOSE(4, verbose_stream() << cl << " in-core " << in_core(cl, clp) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} "; verbose_stream() << "\n");
|
||||
IF_VERBOSE(4, verbose_stream() << cl << " in-core " << in_core(cl) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} "; verbose_stream() << "\n");
|
||||
|
||||
result.push_back(id);
|
||||
m_result.push_back({id, unsigned_vector()});
|
||||
if (is_initial)
|
||||
continue;
|
||||
conflict_analysis_core(cl, clp);
|
||||
}
|
||||
result.reverse();
|
||||
return result;
|
||||
m_result.reverse();
|
||||
return m_result;
|
||||
}
|
||||
|
||||
void proof_trim::del(literal_vector const& cl, clause* cp) {
|
||||
|
@ -75,20 +76,6 @@ namespace sat {
|
|||
else
|
||||
del(cl);
|
||||
}
|
||||
|
||||
bool proof_trim::match_clause(literal_vector const& cl, literal l1, literal l2) const {
|
||||
return cl.size() == 2 && ((l1 == cl[0] && l2 == cl[1]) || (l1 == cl[1] && l2 == cl[0]));
|
||||
}
|
||||
|
||||
bool proof_trim::match_clause(literal_vector const& cl, literal l1, literal l2, literal l3) const {
|
||||
return cl.size() == 3 &&
|
||||
((l1 == cl[0] && l2 == cl[1] && l3 == cl[2]) ||
|
||||
(l1 == cl[0] && l2 == cl[2] && l3 == cl[1]) ||
|
||||
(l1 == cl[1] && l2 == cl[0] && l3 == cl[2]) ||
|
||||
(l1 == cl[1] && l2 == cl[2] && l3 == cl[0]) ||
|
||||
(l1 == cl[2] && l2 == cl[1] && l3 == cl[0]) ||
|
||||
(l1 == cl[2] && l2 == cl[0] && l3 == cl[1]));
|
||||
}
|
||||
|
||||
/**
|
||||
* cl is on the trail if there is some literal l that is implied by cl
|
||||
|
@ -294,6 +281,9 @@ namespace sat {
|
|||
}
|
||||
std::sort(m_clause.begin(), m_clause.end());
|
||||
IF_VERBOSE(3, verbose_stream() << "add core " << m_clause << "\n");
|
||||
unsigned id;
|
||||
VERIFY(m_clause2id.find(m_clause, id));
|
||||
m_result.back().second.push_back(id);
|
||||
m_core_literals.insert(m_clause);
|
||||
if (l != null_literal && s.lvl(l) == 0) {
|
||||
m_clause.reset();
|
||||
|
@ -302,7 +292,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
bool proof_trim::in_core(literal_vector const& cl, clause* cp) const {
|
||||
bool proof_trim::in_core(literal_vector const& cl) const {
|
||||
return m_core_literals.contains(cl);
|
||||
}
|
||||
|
||||
|
@ -346,10 +336,6 @@ namespace sat {
|
|||
s.set_trim();
|
||||
}
|
||||
|
||||
proof_trim::~proof_trim() {
|
||||
}
|
||||
|
||||
|
||||
void proof_trim::assume(unsigned id, bool is_initial) {
|
||||
std::sort(m_clause.begin(), m_clause.end());
|
||||
if (unit_or_binary_occurs())
|
||||
|
@ -360,6 +346,8 @@ namespace sat {
|
|||
return;
|
||||
|
||||
IF_VERBOSE(3, verbose_stream() << (is_initial?"assume ":"rup ") << m_clause << "\n");
|
||||
std::sort(m_clause.begin(), m_clause.end());
|
||||
m_clause2id.insert(m_clause, id);
|
||||
auto* cl = s.mk_clause(m_clause, status::redundant());
|
||||
|
||||
auto is_unit2 = [&]() {
|
||||
|
@ -393,7 +381,6 @@ namespace sat {
|
|||
else if (m_clause.size() > 2 && is_unit())
|
||||
s.propagate_clause(*cl, true, 0, s.cls_allocator().get_offset(cl));
|
||||
s.propagate(false);
|
||||
// verbose_stream() << m_clause << " - " << s.inconsistent() << "\n";
|
||||
if (s.inconsistent() || all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; }))
|
||||
set_conflict(m_clause, cl);
|
||||
|
||||
|
|
|
@ -35,7 +35,7 @@ namespace sat {
|
|||
uint_set m_in_coi;
|
||||
clause* m_conflict_clause = nullptr;
|
||||
vector<std::tuple<unsigned, literal_vector, clause*, bool, bool>> m_trail;
|
||||
|
||||
vector<std::pair<unsigned, unsigned_vector>> m_result;
|
||||
|
||||
struct hash {
|
||||
unsigned operator()(literal_vector const& v) const {
|
||||
|
@ -48,15 +48,13 @@ namespace sat {
|
|||
}
|
||||
};
|
||||
map<literal_vector, clause_vector, hash, eq> m_clauses;
|
||||
map<literal_vector, unsigned, hash, eq> m_clause2id;
|
||||
|
||||
hashtable<literal_vector, hash, eq> m_core_literals;
|
||||
bool_vector m_propagated;
|
||||
|
||||
void del(literal_vector const& cl, clause* cp);
|
||||
|
||||
bool match_clause(literal_vector const& cl, literal l1, literal l2) const;
|
||||
bool match_clause(literal_vector const& cl, literal l1, literal l2, literal l3) const;
|
||||
|
||||
void prune_trail(literal_vector const& cl, clause* cp);
|
||||
void conflict_analysis_core(literal_vector const& cl, clause* cp);
|
||||
|
||||
|
@ -64,7 +62,7 @@ namespace sat {
|
|||
void add_dependency(justification j);
|
||||
void add_core(bool_var v);
|
||||
void add_core(literal l, justification j);
|
||||
bool in_core(literal_vector const& cl, clause* cp) const;
|
||||
bool in_core(literal_vector const& cl) const;
|
||||
void revive(literal_vector const& cl, clause* cp);
|
||||
clause* del(literal_vector const& cl);
|
||||
void save(literal_vector const& lits, clause* cl);
|
||||
|
@ -76,7 +74,6 @@ namespace sat {
|
|||
public:
|
||||
|
||||
proof_trim(params_ref const& p, reslimit& lim);
|
||||
~proof_trim();
|
||||
|
||||
bool_var mk_var() { return s.mk_var(true, true); }
|
||||
void init_clause() { m_clause.reset(); }
|
||||
|
@ -88,7 +85,7 @@ namespace sat {
|
|||
void infer(unsigned id);
|
||||
void updt_params(params_ref const& p) { s.updt_params(p); }
|
||||
|
||||
unsigned_vector trim();
|
||||
vector<std::pair<unsigned, unsigned_vector>> trim();
|
||||
|
||||
};
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue