From a34b66437f97f66d9dcd1caa0919f66cf316e238 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 4 Feb 2010 21:03:07 +0000 Subject: [PATCH] Changed mapping from atoms to literals in the prop engine to be atoms to vars. --- src/prop/cnf_stream.cpp | 79 +++++++++++++++++++++++++++++----------- src/prop/cnf_stream.h | 5 ++- src/prop/prop_engine.cpp | 62 ++++++++++++++----------------- src/prop/prop_engine.h | 77 +++++++++++++++++++++++++++++++-------- 4 files changed, 149 insertions(+), 74 deletions(-) diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 79182617e..cf013363b 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -30,22 +30,19 @@ namespace prop { bool atomic(const Node & n); -CnfStream::CnfStream(PropEngine *pe) : - d_propEngine(pe) { -} -TseitinCnfStream::TseitinCnfStream(PropEngine *pe) : - CnfStream(pe) { +static void printVar(ostream & out, Var v){ + out << v; } static void printLit(ostream & out, Lit l) { const char * s = (sign(l))?"~":" "; out << s << var(l); - } + static void printClause(ostream & out, vec & c) { - out << "clause :"; + out << "clause:"; for(int i=0;i & c) { out << ";" << endl; } + + +CnfStream::CnfStream(PropEngine *pe) : + d_propEngine(pe) { +} + +TseitinCnfStream::TseitinCnfStream(PropEngine *pe) : + CnfStream(pe) { +} + + + void CnfStream::insertClauseIntoStream(vec & c) { Debug("cnf") << "Inserting into stream "; printClause(Debug("cnf"),c); @@ -95,28 +104,31 @@ void CnfStream::flushCache() { d_translationCache.clear(); } -void CnfStream::registerMapping(const Node & node, Lit lit, bool atom) { - - Debug("cnf") << "Mapping Node "<< node << " to "; +void CnfStream::cacheTranslation(const Node & node, Lit lit) { + Debug("cnf") << "cacheing translation "<< node << " to "; printLit(Debug("cnf"),lit); Debug("cnf") << endl; - //Prop engine does not need to know this mapping d_translationCache.insert(make_pair(node, lit)); - if(atom) - d_propEngine->registerAtom(node, lit); -} - -Lit CnfStream::acquireFreshLit(const Node & n) { - return d_propEngine->requestFreshLit(); } Lit CnfStream::aquireAndRegister(const Node & node, bool atom) { - Lit l = acquireFreshLit(node); - registerMapping(node, l, atom); + Var v = atom ? + d_propEngine->registerAtom(node) + : d_propEngine->requestFreshVar(); + Lit l(v); + cacheTranslation(node, l); return l; } +bool CnfStream::isAtomMapped(const Node & n) const{ + return d_propEngine->isAtomMapped(n); +} + +Var CnfStream::lookupAtom(const Node & n) const{ + return d_propEngine->lookupAtom(n); +} + /***********************************************/ /***********************************************/ /************ End of CnfStream *****************/ @@ -213,7 +225,8 @@ Lit TseitinCnfStream::handleOr(const Node& n) { * Should this be changed? */ Lit TseitinCnfStream::handleIff(const Node& n) { - Assert(n.getKind() == IFF); Assert(n.getNumChildren() == 2); + Assert(n.getKind() == IFF); + Assert(n.getNumChildren() == 2); // n: a <=> b; Lit a = recTransform(n[0]); @@ -241,7 +254,10 @@ Lit TseitinCnfStream::handleIff(const Node& n) { return l; } -Lit TseitinCnfStream::handleAnd(const Node& n) { +Lit TseitinCnfStream::handleAnd(const Node& n) { + Assert(n.getKind() == AND); + Assert(n.getNumChildren() >= 1); + //TODO: we know the exact size of the this. //Dynamically allocated array would have less overhead no? vec lits(n.getNumChildren()); @@ -275,6 +291,7 @@ Lit TseitinCnfStream::handleAnd(const Node& n) { Lit TseitinCnfStream::handleImplies(const Node & n) { Assert(n.getKind() == IMPLIES); + Assert(n.getNumChildren() == 2); // n: a => b; Lit a = recTransform(n[0]); @@ -304,6 +321,7 @@ Lit TseitinCnfStream::handleImplies(const Node & n) { Lit TseitinCnfStream::handleNot(const Node & n) { Assert(n.getKind() == NOT); + Assert(n.getNumChildren() == 1); // n : NOT m Node m = n[0]; @@ -311,7 +329,7 @@ Lit TseitinCnfStream::handleNot(const Node & n) { Lit equivN = ~equivM; - registerMapping(n, equivN, false); + cacheTranslation(n, equivN); return equivN; } @@ -320,6 +338,7 @@ Lit TseitinCnfStream::handleNot(const Node & n) { //Assumes binary no else if branchs, and that ITEs Lit TseitinCnfStream::handleIte(const Node & n) { Assert(n.getKind() == ITE); + Assert(n.getNumChildren() == 3); // n : IF c THEN t ELSE f ENDIF; Lit c = recTransform(n[0]); @@ -379,6 +398,22 @@ Lit TseitinCnfStream::recTransform(const Node & n) { } if(atomic(n)) { + + /* Unforunately we need to potentially allow + * for n to be to the Atom <-> Var map but not the + * translation cache. + * This is because the translation cache can be flushed. + * It is really not clear where this check should go, but + * it needs to be done. + */ + if(isAtomMapped(n)){ + /* Puts the atom in the translation cache after looking it up. + * Avoids doing 2 map lookups for this atom in the future. + */ + Lit l(lookupAtom(n)); + cacheTranslation(n, l); + return l; + } return handleAtom(n); } else { //Assume n is a logical connective diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 9be5efcd3..ca2e6dedd 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -61,6 +61,8 @@ private: std::map d_translationCache; protected: + bool isAtomMapped(const Node & n) const; + minisat::Var lookupAtom(const Node & n) const; /** * Uniform interface for sending a clause back to d_propEngine. @@ -83,8 +85,7 @@ protected: //negotiates the mapping of atoms to literals with PropEngine - void registerMapping(const Node & node, minisat::Lit lit, bool atom = false); - minisat::Lit acquireFreshLit(const Node & n); + void cacheTranslation(const Node & node, minisat::Lit lit); minisat::Lit aquireAndRegister(const Node & n, bool atom = false); public: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index f4b10414c..a206a8343 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -58,15 +58,15 @@ void PropEngine::assertClause(vec & c){ d_sat->addClause(c); } -void PropEngine::registerAtom(const Node & n, Lit l){ - d_atom2lit.insert(make_pair(n,l)); - d_lit2atom.insert(make_pair(l,n)); +Var PropEngine::registerAtom(const Node & n){ + Var v = requestFreshVar(); + d_atom2var.insert(make_pair(n,v)); + d_var2atom.insert(make_pair(v,n)); + return v; } -Lit PropEngine::requestFreshLit(){ - Var v = d_sat->newVar(); - Lit l(v,false); - return l; +Var PropEngine::requestFreshVar(){ + return d_sat->newVar(); } void PropEngine::assertFormula(const Node& node) { @@ -83,8 +83,8 @@ void PropEngine::restart(){ delete d_sat; d_sat = new Solver(); d_cnfStream->flushCache(); - d_atom2lit.clear(); - d_lit2atom.clear(); + d_atom2var.clear(); + d_var2atom.clear(); for(vector::iterator iter = d_assertionList.begin(); iter != d_assertionList.end(); ++iter){ @@ -92,11 +92,6 @@ void PropEngine::restart(){ } } -static void printLit(ostream & out, Lit l) { - const char * s = (sign(l))?"~":" "; - out << s << var(l); - -} Result PropEngine::solve() { if(d_restartMayBeNeeded) @@ -110,29 +105,26 @@ Result PropEngine::solve() { } Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl; - - if(result){ - for(map::iterator atomIter = d_atom2lit.begin(); - atomIter != d_atom2lit.end(); - ++atomIter){ - Node n = (*atomIter).first; - Lit l = (*atomIter).second; - - lbool lb = d_sat->modelValue(l); - - Notice() << n << "->" << lb.toInt() << endl; - } - }else{ - // unsat case - Notice() << "Conflict {"; - for(int i=0; i< d_sat->conflict.size(); i++){ - Notice() << endl << " "; - printLit(Notice(), d_sat->conflict[i]); - } - Notice() << endl << "}" << endl; - } return Result(result ? Result::SAT : Result::UNSAT); } + + void PropEngine::assertLit(Lit l){ + Var v = var(l); + if(isVarMapped(v)){ + Node atom = lookupVar(v); + //Theory* t = ...; + //t must be the corresponding theory for the atom + + //Literal l(atom, sign(l)); + //t->assertLiteral(l ); + } + } + + void PropEngine::signalBooleanPropHasEnded(){} + //TODO decisionEngine should be told + //TODO theoryEngine to call lightweight theory propogation + + }/* CVC4 namespace */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 15664be75..b2355ee38 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -54,14 +54,36 @@ class PropEngine { */ CVC4::prop::minisat::Solver* d_sat; - std::map d_atom2lit; - std::map d_lit2atom; + std::map d_atom2var; + std::map d_var2atom; + /** - * Adds mapping of n -> l to d_node2lit, and - * a mapping of l -> n to d_lit2node. + * Requests a fresh variable from d_sat, v. + * Adds mapping of n -> v to d_node2var, and + * a mapping of v -> n to d_var2node. + */ + CVC4::prop::minisat::Var registerAtom(const Node & n); + + /** + * Requests a fresh variable from d_sat. + */ + CVC4::prop::minisat::Var requestFreshVar(); + + + /** + * Returns true iff this Node is in the atom to variable mapping. + * @param n the Node to lookup + * @return true iff this Node is in the atom to variable mapping. + */ + bool isAtomMapped(const Node & n) const; + + /** + * Returns the variable mapped by the atom Node. + * @param n the atom to do the lookup by + * @return the corresponding variable */ - void registerAtom(const Node & n, CVC4::prop::minisat::Lit l); + CVC4::prop::minisat::Var lookupAtom(const Node & n) const; /** * Flags whether the solver may need to have its state reset before @@ -79,11 +101,22 @@ class PropEngine { */ std::vector d_assertionList; - - CVC4::prop::minisat::Lit requestFreshLit(); - bool isNodeMapped(const Node & n) const; - CVC4::prop::minisat::Lit lookupLit(const Node & n) const; + /** + * Returns true iff the minisat var has been mapped to an atom. + * @param v variable to check if it is mapped + * @return returns true iff the minisat var has been mapped. + */ + bool isVarMapped(CVC4::prop::minisat::Var v) const; + + /** + * Returns the atom mapped by the variable v. + * @param v the variable to do the lookup by + * @return an atom + */ + Node lookupVar(CVC4::prop::minisat::Var v) const; + + /** * Asserts an internally constructed clause. @@ -94,9 +127,15 @@ class PropEngine { /** The CNF converter in use */ - //CVC4::prop::CnfConverter d_cnfConverter; CVC4::prop::CnfStream *d_cnfStream; + + + void assertLit(CVC4::prop::minisat::Lit l); + void signalBooleanPropHasEnded(); + public: + + /** * Create a PropEngine with a particular decision and theory engine. */ @@ -118,19 +157,27 @@ public: */ Result solve(); + };/* class PropEngine */ -inline bool PropEngine::isNodeMapped(const Node & n) const{ - return d_atom2lit.find(n) != d_atom2lit.end(); +inline bool PropEngine::isAtomMapped(const Node & n) const{ + return d_atom2var.find(n) != d_atom2var.end(); } -inline CVC4::prop::minisat::Lit PropEngine::lookupLit(const Node & n) const{ - Assert(isNodeMapped(n)); - return d_atom2lit.find(n)->second; +inline CVC4::prop::minisat::Var PropEngine::lookupAtom(const Node & n) const{ + Assert(isAtomMapped(n)); + return d_atom2var.find(n)->second; } +inline bool PropEngine::isVarMapped(CVC4::prop::minisat::Var v) const { + return d_var2atom.find(v) != d_var2atom.end(); +} +inline Node PropEngine::lookupVar(CVC4::prop::minisat::Var v) const { + Assert(isVarMapped(v)); + return d_var2atom.find(v)->second; +} }/* CVC4 namespace */ -- 2.30.2