diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 58 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 7 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 32 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 8 |
4 files changed, 83 insertions, 22 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 1c327c5a8..961ef85c5 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -28,6 +28,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/sat.h" #include "util/output.h" #include "expr/command.h" +#include "proof/proof_manager.h" +#include "proof/sat_proof.h" using namespace Minisat; using namespace CVC4; @@ -121,7 +123,9 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bo , conflict_budget (-1) , propagation_budget (-1) , asynch_interrupt (false) -{} +{ + PROOF(ProofManager::initSatProof(this);) +} Solver::~Solver() @@ -233,6 +237,9 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) } else if (ps.size() == 1) { if(assigns[var(ps[0])] == l_Undef) { uncheckedEnqueue(ps[0]); + + PROOF( ProofManager::getSatProof()->registerUnitClause(ps[0], true); ) + if(assertionLevel > 0) { // remember to unset it on user pop Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl; @@ -244,6 +251,8 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) CRef cr = ca.alloc(assertionLevel, ps, false); clauses_persistent.push(cr); attachClause(cr); + + PROOF( ProofManager::getSatProof()->registerClause(cr, true); ) } } @@ -263,6 +272,8 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { + PROOF( ProofManager::getSatProof()->markDeleted(cr); ) + const Clause& c = ca[cr]; Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; assert(c.size() > 1); @@ -401,10 +412,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) int max_level = 0; // Maximal level of the resolved clauses + PROOF( ProofManager::getSatProof()->startResChain(confl); ) do{ assert(confl != CRef_Undef); // (otherwise should be UIP) Clause& c = ca[confl]; - if (c.level() > max_level) { max_level = c.level(); } @@ -422,6 +433,11 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) pathC++; else out_learnt.push(q); + } else { + // FIXME: can we do it lazily if we actually need the proof? + if (level(var(q)) == 0) { + PROOF( ProofManager::getSatProof()->resolveOutUnit(q); ) + } } } @@ -431,6 +447,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) confl = reason(var(p)); seen[var(p)] = 0; pathC--; + + if ( pathC > 0 && confl != CRef_Undef ) { + PROOF( ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); ) + } }while (pathC > 0); out_learnt[0] = ~p; @@ -442,7 +462,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) uint32_t abstract_level = 0; for (i = 1; i < out_learnt.size(); i++) abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) - + for (i = j = 1; i < out_learnt.size(); i++) { if (reason(var(out_learnt[i])) == CRef_Undef) { out_learnt[j++] = out_learnt[i]; @@ -453,6 +473,8 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) // Literal is not redundant out_learnt[j++] = out_learnt[i]; } else { + // + PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); ) // Literal is redundant, mark the level of the redundancy derivation if (max_level < red_level) { max_level = red_level; @@ -809,8 +831,13 @@ void Solver::removeSatisfied(vec<CRef>& cs) int i, j; for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; - if (satisfied(c)) + if (satisfied(c)) { + if (locked(c)) { + // store a resolution of the literal c propagated + PROOF( ProofManager::getSatProof()->storeUnitResolution(c[0]); ) + } removeClause(cs[i]); + } else cs[j++] = cs[i]; } @@ -908,7 +935,10 @@ lbool Solver::search(int nof_conflicts) conflicts++; conflictC++; - if (decisionLevel() == 0) return l_False; + if (decisionLevel() == 0) { + PROOF( ProofManager::getSatProof()->finalizeProof(confl); ) + return l_False; + } // Analyze the conflict learnt_clause.clear(); @@ -918,12 +948,17 @@ lbool Solver::search(int nof_conflicts) // Assert the conflict clause and the asserting literal if (learnt_clause.size() == 1) { uncheckedEnqueue(learnt_clause[0]); - } else { + + PROOF( ProofManager::getSatProof()->endResChain(learnt_clause[0]); ) + + } else { CRef cr = ca.alloc(max_level, learnt_clause, true); clauses_removable.push(cr); attachClause(cr); claBumpActivity(ca[cr]); uncheckedEnqueue(learnt_clause[0], cr); + + PROOF( ProofManager::getSatProof()->endResChain(cr); ) } varDecayActivity(); @@ -1211,7 +1246,7 @@ void Solver::relocAll(ClauseAllocator& to) // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1); vec<Watcher>& ws = watches[p]; for (int j = 0; j < ws.size(); j++) - ca.reloc(ws[j].cref, to); + ca.reloc(ws[j].cref, to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); } // All reasons: @@ -1220,18 +1255,19 @@ void Solver::relocAll(ClauseAllocator& to) Var v = var(trail[i]); if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) - ca.reloc(vardata[v].reason, to); + ca.reloc(vardata[v].reason, to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); } - // All learnt: // for (int i = 0; i < clauses_removable.size(); i++) - ca.reloc(clauses_removable[i], to); + ca.reloc(clauses_removable[i], to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); // All original: // for (int i = 0; i < clauses_persistent.size(); i++) - ca.reloc(clauses_persistent[i], to); + ca.reloc(clauses_persistent[i], to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); + + PROOF( ProofManager::getSatProof()->finishUpdateCRef(); ) } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index c5220997b..a3d449a36 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -37,9 +37,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "expr/command.h" namespace CVC4 { +class SatProof; + namespace prop { class SatSolver; }/* CVC4::prop namespace */ + }/* CVC4 namespace */ namespace Minisat { @@ -49,9 +52,9 @@ namespace Minisat { class Solver { - /** The only CVC4 entry point to the private solver data */ + /** The only two CVC4 entry points to the private solver data */ friend class CVC4::prop::SatSolver; - + friend class CVC4::SatProof; protected: /** The pointer to the proxy that provides interfaces to the SMT engine */ diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 1aff5094d..57ca95a41 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define Minisat_SolverTypes_h #include <assert.h> - +#include "util/output.h" #include "mtl/IntTypes.h" #include "mtl/Alg.h" #include "mtl/Vec.h" @@ -44,6 +44,7 @@ typedef int Var; #define var_Undef (-1) + struct Lit { int x; @@ -115,11 +116,26 @@ public: inline int toInt (lbool l) { return l.value; } inline lbool toLbool(int v) { return lbool((uint8_t)v); } -//================================================================================================= -// Clause -- a simple class for representing a clause: class Clause; typedef RegionAllocator<uint32_t>::Ref CRef; +} /* Minisat */ + + + +namespace CVC4 { +class ProofProxyAbstract { +public: + virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0; +}; +} + + + +namespace Minisat{ + +//================================================================================================= +// Clause -- a simple class for representing a clause: class Clause { struct { @@ -236,17 +252,21 @@ class ClauseAllocator : public RegionAllocator<uint32_t> RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra())); } - void reloc(CRef& cr, ClauseAllocator& to) + void reloc(CRef& cr, ClauseAllocator& to, CVC4::ProofProxyAbstract* proxy = NULL) { + + // FIXME what is this CRef_lazy if (cr == CRef_Lazy) return; + CRef old = cr; // save the old reference Clause& c = operator[](cr); - if (c.reloced()) { cr = c.relocation(); return; } cr = to.alloc(c.level(), c, c.removable()); c.relocate(cr); - + if (proxy) { + proxy->updateCRef(old, cr); + } // Copy extra data-fields: // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) to[cr].mark(c.mark()); diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 8c31dd377..6045fc881 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "mtl/Sort.h" #include "simp/SimpSolver.h" #include "utils/System.h" - +#include "proof/proof.h" using namespace Minisat; using namespace CVC4; @@ -57,7 +57,7 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con , asymm_lits (0) , eliminated_vars (0) , elimorder (1) - , use_simplification (!enableIncremental) + , use_simplification (!enableIncremental && !PROOF_ON()) // TODO: turn off simplifications if proofs are on initially , occurs (ClauseDeleted(ca)) , elim_heap (ElimLt(n_occ)) , bwdsub_assigns (0) @@ -702,10 +702,11 @@ void SimpSolver::relocAll(ClauseAllocator& to) // for (int i = 0; i < subsumption_queue.size(); i++) ca.reloc(subsumption_queue[i], to); - + // TODO reloc now takes the proof form the core solver // Temporary clause: // ca.reloc(bwdsub_tmpunit, to); + // TODO reloc now takes the proof form the core solver } @@ -723,4 +724,5 @@ void SimpSolver::garbageCollect() printf("| Garbage collection: %12d bytes => %12d bytes |\n", ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); + // TODO: proof.finalizeUpdateId(); } |