mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

categorize theory axioms as inferences in output to capture justifications

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-04 09:12:58 +02:00
parent 47fc0cf75c
commit ae29a54876
3 changed files with 2 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -132,7 +132,7 @@ public:
clause1.push_back(hint); clause1.push_back(hint);
trim.assume(m_clauses.size()); trim.assume(m_clauses.size());
m_clauses.push_back(clause1); m_clauses.push_back(clause1);
m_is_infer.push_back(false); m_is_infer.push_back(true);
if (clause.empty()) { if (clause.empty()) {
mk_clause(clause); mk_clause(clause);

19
src/sat/sat_proof_trim.cpp
View file

@ -76,20 +76,6 @@ namespace sat {
del(cl); 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 * cl is on the trail if there is some literal l that is implied by cl
* Remove all clauses after cl that are in the cone of influence of cl. * Remove all clauses after cl that are in the cone of influence of cl.
@ -346,10 +332,6 @@ namespace sat {
s.set_trim(); s.set_trim();
} }
proof_trim::~proof_trim() {
}
void proof_trim::assume(unsigned id, bool is_initial) { void proof_trim::assume(unsigned id, bool is_initial) {
std::sort(m_clause.begin(), m_clause.end()); std::sort(m_clause.begin(), m_clause.end());
if (unit_or_binary_occurs()) if (unit_or_binary_occurs())
@ -393,7 +375,6 @@ namespace sat {
else if (m_clause.size() > 2 && is_unit()) else if (m_clause.size() > 2 && is_unit())
s.propagate_clause(*cl, true, 0, s.cls_allocator().get_offset(cl)); s.propagate_clause(*cl, true, 0, s.cls_allocator().get_offset(cl));
s.propagate(false); 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; })) if (s.inconsistent() || all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; }))
set_conflict(m_clause, cl); set_conflict(m_clause, cl);

5
src/sat/sat_proof_trim.h
View file

@ -36,7 +36,6 @@ namespace sat {
clause* m_conflict_clause = nullptr; clause* m_conflict_clause = nullptr;
vector<std::tuple<unsigned, literal_vector, clause*, bool, bool>> m_trail; vector<std::tuple<unsigned, literal_vector, clause*, bool, bool>> m_trail;
struct hash { struct hash {
unsigned operator()(literal_vector const& v) const { unsigned operator()(literal_vector const& v) const {
return string_hash((char const*)v.begin(), v.size()*sizeof(literal), 3); return string_hash((char const*)v.begin(), v.size()*sizeof(literal), 3);
@ -54,9 +53,6 @@ namespace sat {
void del(literal_vector const& cl, clause* cp); 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 prune_trail(literal_vector const& cl, clause* cp);
void conflict_analysis_core(literal_vector const& cl, clause* cp); void conflict_analysis_core(literal_vector const& cl, clause* cp);
@ -76,7 +72,6 @@ namespace sat {
public: public:
proof_trim(params_ref const& p, reslimit& lim); proof_trim(params_ref const& p, reslimit& lim);
~proof_trim();
bool_var mk_var() { return s.mk_var(true, true); } bool_var mk_var() { return s.mk_var(true, true); }
void init_clause() { m_clause.reset(); } void init_clause() { m_clause.reset(); }