From 969b144a5f9630d646afdf0ff0a053df38d0ed1a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 10 Apr 2011 00:44:20 +0000 Subject: merge from replay branch --- src/prop/cnf_stream.cpp | 19 ++++++++++++++----- src/prop/cnf_stream.h | 2 ++ src/prop/minisat/core/Solver.cc | 11 +++++++++++ src/prop/sat.cpp | 36 ++++++++++++++++++++++++++++++------ src/prop/sat.h | 11 ++++++++--- 5 files changed, 65 insertions(+), 14 deletions(-) (limited to 'src/prop') diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index fc7fa600a..6732b09bc 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -31,11 +31,18 @@ using namespace std; using namespace CVC4::kind; +#ifdef CVC4_REPLAY +# define CVC4_USE_REPLAY true +#else /* CVC4_REPLAY */ +# define CVC4_USE_REPLAY false +#endif /* CVC4_REPLAY */ + namespace CVC4 { namespace prop { CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar) : - d_satSolver(satSolver), d_registrar(registrar) { + d_satSolver(satSolver), + d_registrar(registrar) { } void CnfStream::recordTranslation(TNode node) { @@ -46,7 +53,6 @@ void CnfStream::recordTranslation(TNode node) { } } - TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar) : CnfStream(satSolver, registrar) { } @@ -88,7 +94,7 @@ bool CnfStream::hasLiteral(TNode n) const { } SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { - Debug("cnf") << "newLiteral(" << node << ")" << endl; + Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl; // Get the literal for this node SatLiteral lit; @@ -108,14 +114,16 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { d_translationCache[node].level = level; d_translationCache[node.notNode()].level = level; - // If it's a theory literal, store it for back queries - if (theoryLiteral) { + // If it's a theory literal, need to store it for back queries + if ( theoryLiteral || + ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ) { d_nodeCache[lit] = node; d_nodeCache[~lit] = node.notNode(); } // Here, you can have it Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl; + // have to keep track of this, because with the call to preRegister(), // the cnf stream is re-entrant! bool wasAssertingLemma = d_assertingLemma; @@ -155,6 +163,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { SatLiteral CnfStream::getLiteral(TNode node) { TranslationCache::iterator find = d_translationCache.find(node); + Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node"); Assert(find != d_translationCache.end(), "Literal not in the CNF Cache: %s\n", node.toString().c_str()); SatLiteral literal = find->second.literal; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 28b2cfb03..ef75e635b 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -180,6 +180,7 @@ public: * Constructs a CnfStream that sends constructs an equi-satisfiable * set of clauses and sends them to the given sat solver. * @param satSolver the sat solver to use + * @param registrar the entity that takes care of preregistration of Nodes */ CnfStream(SatInputInterface* satSolver, theory::Registrar registrar); @@ -255,6 +256,7 @@ public: /** * Constructs the stream to use the given sat solver. * @param satSolver the sat solver to use + * @param registrar the entity that takes care of pre-registration of Nodes */ TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar); diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index fd4b18222..10cd02f94 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -395,6 +395,13 @@ void Solver::popTrail() { Lit Solver::pickBranchLit() { +#ifdef CVC4_REPLAY + Lit nextLit = proxy->getNextReplayDecision(); + if (nextLit != lit_Undef) { + return nextLit; + } +#endif /* CVC4_REPLAY */ + Var next = var_Undef; // Random decision: @@ -1051,6 +1058,10 @@ lbool Solver::search(int nof_conflicts) check_type = CHECK_WITHOUTH_PROPAGATION_FINAL; continue; } + +#ifdef CVC4_REPLAY + proxy->logDecision(next); +#endif /* CVC4_REPLAY */ } // Increase decision level and enqueue 'next' diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 1db7bf446..a6adecb1d 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -2,10 +2,10 @@ /*! \file sat.cpp ** \verbatim ** Original author: cconway - ** Major contributors: mdeters, taking - ** Minor contributors (to current version): dejan + ** Major contributors: dejan, mdeters, taking + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -17,11 +17,12 @@ ** \todo document this file **/ -#include "cnf_stream.h" -#include "prop_engine.h" -#include "sat.h" +#include "prop/cnf_stream.h" +#include "prop/prop_engine.h" +#include "prop/sat.h" #include "context/context.h" #include "theory/theory_engine.h" +#include "expr/expr_stream.h" namespace CVC4 { namespace prop { @@ -106,5 +107,28 @@ void SatSolver::notifyRestart() { d_theoryEngine->notifyRestart(); } +SatLiteral SatSolver::getNextReplayDecision() { +#ifdef CVC4_REPLAY + if(Options::current()->replayStream != NULL) { + Expr e = Options::current()->replayStream->nextExpr(); + if(!e.isNull()) { // we get null node when out of decisions to replay + // convert & return + return d_cnfStream->getLiteral(e); + } + } + return Minisat::lit_Undef; +#endif /* CVC4_REPLAY */ +} + +void SatSolver::logDecision(SatLiteral lit) { +#ifdef CVC4_REPLAY + if(Options::current()->replayLog != NULL) { + Assert(lit != Minisat::lit_Undef, "logging an `undef' decision ?!"); + *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl; + } +#endif /* CVC4_REPLAY */ +} + + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/sat.h b/src/prop/sat.h index b80b0f705..c00115cd8 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -5,7 +5,7 @@ ** Major contributors: taking, cconway, dejan ** Minor contributors (to current version): barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -250,14 +250,19 @@ public: void notifyRestart(); + SatLiteral getNextReplayDecision(); + + void logDecision(SatLiteral lit); + };/* class SatSolver */ /* Functions that delegate to the concrete SAT solver. */ #ifdef __CVC4_USE_MINISAT -inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, - context::Context* context) : +inline SatSolver::SatSolver(PropEngine* propEngine, + TheoryEngine* theoryEngine, + context::Context* context) : d_propEngine(propEngine), d_cnfStream(NULL), d_theoryEngine(theoryEngine), -- cgit v1.2.3