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<Lit> & c) {
- out << "clause :";
+ out << "clause:";
for(int i=0;i<c.size();i++){
out << " ";
printLit(out, c[i]) ;
out << ";" << endl;
}
+
+
+CnfStream::CnfStream(PropEngine *pe) :
+ d_propEngine(pe) {
+}
+
+TseitinCnfStream::TseitinCnfStream(PropEngine *pe) :
+ CnfStream(pe) {
+}
+
+
+
void CnfStream::insertClauseIntoStream(vec<Lit> & c) {
Debug("cnf") << "Inserting into stream ";
printClause(Debug("cnf"),c);
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 *****************/
* 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]);
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<Lit> lits(n.getNumChildren());
Lit TseitinCnfStream::handleImplies(const Node & n) {
Assert(n.getKind() == IMPLIES);
+ Assert(n.getNumChildren() == 2);
// n: a => b;
Lit a = recTransform(n[0]);
Lit TseitinCnfStream::handleNot(const Node & n) {
Assert(n.getKind() == NOT);
+ Assert(n.getNumChildren() == 1);
// n : NOT m
Node m = n[0];
Lit equivN = ~equivM;
- registerMapping(n, equivN, false);
+ cacheTranslation(n, equivN);
return equivN;
}
//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]);
}
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
std::map<Node, minisat::Lit> 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.
//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:
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) {
delete d_sat;
d_sat = new Solver();
d_cnfStream->flushCache();
- d_atom2lit.clear();
- d_lit2atom.clear();
+ d_atom2var.clear();
+ d_var2atom.clear();
for(vector<Node>::iterator iter = d_assertionList.begin();
iter != d_assertionList.end(); ++iter){
}
}
-static void printLit(ostream & out, Lit l) {
- const char * s = (sign(l))?"~":" ";
- out << s << var(l);
-
-}
Result PropEngine::solve() {
if(d_restartMayBeNeeded)
}
Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
-
- if(result){
- for(map<Node,Lit>::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 */
*/
CVC4::prop::minisat::Solver* d_sat;
- std::map<Node, CVC4::prop::minisat::Lit> d_atom2lit;
- std::map<CVC4::prop::minisat::Lit, Node> d_lit2atom;
+ std::map<Node, CVC4::prop::minisat::Var> d_atom2var;
+ std::map<CVC4::prop::minisat::Var, Node> 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
*/
std::vector<Node> 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.
/** 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.
*/
*/
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 */
projects / cvc5.git / commitdiff