luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

glucose2: Improvements and fixes for proof tracing 

This fills some gaps and fixes a few edge cases with the new proof
tracing callback API.
This commit is contained in:
Jannis Harder 2024-08-19 13:47:53 +02:00
parent e2749d5c90
commit f36e35f735
3 changed files with 24 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/sat/glucose2/Glucose2.cpp
View File

@ -285,7 +285,7 @@ bool Solver::addClause_(vec<Lit>& ps)
// Check if clause is satisfied and remove false/duplicate literals:
sort(ps);
vec<Lit> oc;
vec<Lit> oc, used_units;
oc.clear();
Lit p; int i, j, flag = 0;
@ -294,6 +294,8 @@ bool Solver::addClause_(vec<Lit>& ps)
oc.push(ps[i]);
if (value(ps[i]) == l_True || ps[i] == ~p || value(ps[i]) == l_False)
flag = 1;
if (trace_proof && value(ps[i]) == l_False)
used_units.push(~ps[i]);
}
}
@ -310,7 +312,14 @@ bool Solver::addClause_(vec<Lit>& ps)
printf( "\n" );
}
assert(!(flag && trace_proof)); // TODO implement this
uint32_t trace_tag = trace_default_tag;
if (flag && trace_proof) {
trace_tag = trace_proof_learnt_clause(trace_proof_callback_data,
(int *)(Lit *)ps, ps.size(),
&trace_tag, 1,
(int *)(Lit *)used_units, used_units.size());
}
if (flag && (certifiedUNSAT)) {
for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
@ -954,13 +963,17 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
if (decisionLevel() == 0) {
if (trace_proof) {
int p_int = toInt(p);
trace_proof_conflict(trace_proof_callback_data, NULL, 0, &p_int, 1);
trace_proof_conflict(trace_proof_callback_data,
(int *)(Lit *)out_conflict, out_conflict.size(), NULL, 0, &p_int, 1);
}
return;
}
seen[var(p)] = 1;
if (trace_proof && level(var(p)) == 0)
trace_units.push(p);
for (int i = trail.size()-1; i >= trail_lim[0]; i--){
Var x = var(trail[i]);
if (seen[x]){
@ -1005,10 +1018,9 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
}
}
assert(false);
trace_proof_conflict(
trace_proof_callback_data,
(int *)(Lit *)out_conflict, out_conflict.size(),
trace_tags, trace_tags.size(),
(int *)(Lit *)trace_units, trace_units.size());

2
src/sat/glucose2/Solver.h
View File

@ -201,7 +201,7 @@ public:
void *trace_proof_callback_data;
uint32_t (*trace_proof_learnt_clause)(void *data, const int *lits, int nlits, const uint32_t *tags, int ntags, const int *units, int nunits);
void (*trace_proof_learnt_unit)(void *data, int unit, uint32_t tag, const int *units, int nunits);
void (*trace_proof_conflict)(void *data, const uint32_t *tags, int ntags, const int *units, int nunits);
void (*trace_proof_conflict)(void *data, const int *lits, int nlits, const uint32_t *tags, int ntags, const int *units, int nunits);
// Statistics: (read-only member variable)

12
src/sat/glucose2/SolverTypes.h
View File

@ -274,13 +274,13 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
// Copy extra data-fields:
// (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
to[cr].mark(c.mark());
to[cr].header.trace_tag = c.header.trace_tag;
if (to[cr].learnt()) {
to[cr].activity() = c.activity();
to[cr].setLBD(c.lbd());
to[cr].setSizeWithoutSelectors(c.sizeWithoutSelectors());
to[cr].setCanBeDel(c.canBeDel());
to[cr].header.trace_tag = c.header.trace_tag;
}
to[cr].activity() = c.activity();
to[cr].setLBD(c.lbd());
to[cr].setSizeWithoutSelectors(c.sizeWithoutSelectors());
to[cr].setCanBeDel(c.canBeDel());
}
else if (to[cr].has_extra()) to[cr].calcAbstraction();
}
};