mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

add dependency tracking to proof from trim

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-04 16:24:09 +02:00
parent abf5aff0b3
commit f0d3cbe39d
3 changed files with 38 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/cmd_context/extra_cmds/proof_cmds.cpp
View file

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

26
src/sat/sat_proof_trim.cpp
View file

@ -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) {
@ -280,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();
@ -288,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);
}
@ -342,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 = [&]() {

8
src/sat/sat_proof_trim.h
View file

@ -35,7 +35,8 @@ 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 {
return string_hash((char const*)v.begin(), v.size()*sizeof(literal), 3);
@ -47,6 +48,7 @@ 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;
@ -60,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);
@ -83,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();
};
}