using namespace CVC4::prop::minisat;
using namespace std;
-
namespace CVC4 {
namespace prop {
CnfStream::CnfStream(PropEngine *pe) :
- d_propEngine(pe){}
-
-TseitinCnfStream::TseitinCnfStream(PropEngine *pe):
- CnfStream(pe){}
+ d_propEngine(pe) {
+}
+TseitinCnfStream::TseitinCnfStream(PropEngine *pe) :
+ CnfStream(pe) {
+}
-void CnfStream::insertClauseIntoStream(vec<Lit> & c){
+void CnfStream::insertClauseIntoStream(vec<Lit> & c) {
d_propEngine->assertClause(c);
}
-void CnfStream::insertClauseIntoStream(minisat::Lit a){
+void CnfStream::insertClauseIntoStream(minisat::Lit a) {
vec<Lit> clause(1);
clause[0] = a;
insertClauseIntoStream(clause);
}
-void CnfStream::insertClauseIntoStream(minisat::Lit a,minisat::Lit b){
+void CnfStream::insertClauseIntoStream(minisat::Lit a, minisat::Lit b) {
vec<Lit> clause(2);
clause[0] = a;
clause[1] = b;
insertClauseIntoStream(clause);
}
-void CnfStream::insertClauseIntoStream(minisat::Lit a,minisat::Lit b, minisat::Lit c){
+void CnfStream::insertClauseIntoStream(minisat::Lit a, minisat::Lit b,
+ minisat::Lit c) {
vec<Lit> clause(3);
clause[0] = a;
clause[1] = b;
return d_translationCache.find(n)->second;
}
-void CnfStream::flushCache(){
+void CnfStream::flushCache() {
d_translationCache.clear();
}
-void CnfStream::registerMapping(const Node & node, Lit lit, bool atom){
+void CnfStream::registerMapping(const Node & node, Lit lit, bool atom) {
//Prop engine does not need to know this mapping
- d_translationCache.insert(make_pair(node,lit));
+ d_translationCache.insert(make_pair(node, lit));
if(atom)
d_propEngine->registerAtom(node, lit);
}
-Lit CnfStream::acquireFreshLit(const Node & n){
+Lit CnfStream::acquireFreshLit(const Node & n) {
return d_propEngine->requestFreshLit();
}
-Lit CnfStream::aquireAndRegister(const Node & node, bool atom){
+Lit CnfStream::aquireAndRegister(const Node & node, bool atom) {
Lit l = acquireFreshLit(node);
registerMapping(node, l, atom);
return l;
/***********************************************/
/***********************************************/
-Lit TseitinCnfStream::handleAtom(const Node & n){
+Lit TseitinCnfStream::handleAtom(const Node & n) {
Lit l = aquireAndRegister(n, true);
- switch(n.getKind()){ /* TRUE and FALSE are handled specially. */
+ switch(n.getKind()) { /* TRUE and FALSE are handled specially. */
case TRUE:
- insertClauseIntoStream( l );
+ insertClauseIntoStream(l);
break;
case FALSE:
- insertClauseIntoStream( ~l );
+ insertClauseIntoStream(~l);
break;
default: //Does nothing else
break;
return l;
}
-Lit TseitinCnfStream::handleXor(const Node & n){
+Lit TseitinCnfStream::handleXor(const Node & n) {
// n: a XOR b
-
+
Lit a = recTransform(n[0]);
Lit b = recTransform(n[1]);
-
+
Lit l = aquireAndRegister(n);
-
- insertClauseIntoStream( a, b, ~l);
- insertClauseIntoStream( a, ~b, l);
- insertClauseIntoStream(~a, b, l);
+
+ insertClauseIntoStream(a, b, ~l);
+ insertClauseIntoStream(a, ~b, l);
+ insertClauseIntoStream(~a, b, l);
insertClauseIntoStream(~a, ~b, ~l);
-
+
return l;
}
- /* For a small efficiency boost target needs to already be allocated to have
- size of the number of children of n.
- */
-void TseitinCnfStream::mapRecTransformOverChildren(const Node& n, vec<Lit> & target){
+/* For a small efficiency boost target needs to already be allocated to have
+ size of the number of children of n.
+ */
+void TseitinCnfStream::mapRecTransformOverChildren(const Node& n,
+ vec<Lit> & target) {
Assert(target.size() == n.getNumChildren());
int i = 0;
Node::iterator subExprIter = n.begin();
-
- while(subExprIter != n.end()){
+
+ while(subExprIter != n.end()) {
Lit equivalentLit = recTransform(*subExprIter);
target[i] = equivalentLit;
- ++subExprIter; ++i;
+ ++subExprIter;
+ ++i;
}
}
-Lit TseitinCnfStream::handleOr(const Node& n){
+Lit TseitinCnfStream::handleOr(const Node& n) {
//child_literals
vec<Lit> lits(n.getNumChildren());
mapRecTransformOverChildren(n, lits);
-
+
Lit e = aquireAndRegister(n);
-
+
/* e <-> (a1 | a2 | a3 | ...)
*: e -> (a1 | a2 | a3 | ...)
* : ~e | (
vec<Lit> c;
c.push(~e);
-
- for( int index = 0; index < lits.size(); ++index){
+
+ for(int index = 0; index < lits.size(); ++index) {
Lit a = lits[index];
c.push(a);
- insertClauseIntoStream( e, ~a);
+ insertClauseIntoStream(e, ~a);
}
insertClauseIntoStream(c);
-
+
return e;
}
-
/* TODO: this only supports 2-ary <=> nodes atm.
* Should this be changed?
*/
-Lit TseitinCnfStream::handleIff(const Node& n){
- Assert(n.getKind() == IFF);
- Assert(n.getNumChildren() == 2);
+Lit TseitinCnfStream::handleIff(const Node& n) {
+ Assert(n.getKind() == IFF); Assert(n.getNumChildren() == 2);
// n: a <=> b;
Lit a = recTransform(n[0]);
Lit b = recTransform(n[1]);
-
+
Lit l = aquireAndRegister(n);
-
+
/* l <-> (a<->b)
* : l -> ((a-> b) & (b->a))
* : ~l | ((~a | b) & (~b |a))
* : ((~a | ~b) & (a | b)) | l
* : (~a | ~b | l) & (a | b | l)
*/
-
- insertClauseIntoStream( ~a, b,~l);
- insertClauseIntoStream( a,~b,~l);
- insertClauseIntoStream( ~a,~b, l);
- insertClauseIntoStream( a, b, l);
-
+
+ insertClauseIntoStream(~a, b, ~l);
+ insertClauseIntoStream(a, ~b, ~l);
+ insertClauseIntoStream(~a, ~b, l);
+ insertClauseIntoStream(a, b, l);
+
return l;
}
-Lit TseitinCnfStream::handleAnd(const Node& n){
+Lit TseitinCnfStream::handleAnd(const Node& n) {
//TODO: we know the exact size of the this.
//Dynamically allocated array would have less overhead no?
vec<Lit> lits(n.getNumChildren());
mapRecTransformOverChildren(n, lits);
-
+
Lit e = aquireAndRegister(n);
/* e <-> (a1 & a2 & a3 & ...)
vec<Lit> c;
c.push(e);
- for(int index = 0; index < lits.size(); ++index){
+ for(int index = 0; index < lits.size(); ++index) {
Lit a = lits[index];
c.push(~a);
- insertClauseIntoStream( ~e, a );
+ insertClauseIntoStream(~e, a);
}
insertClauseIntoStream(c);
-
+
return e;
}
-Lit TseitinCnfStream::handleImplies(const Node & n){
+Lit TseitinCnfStream::handleImplies(const Node & n) {
Assert(n.getKind() == IMPLIES);
// n: a => b;
Lit a = recTransform(n[0]);
Lit b = recTransform(n[1]);
-
+
Lit l = aquireAndRegister(n);
-
+
/* l <-> (a->b)
* (l -> (a->b)) & (l <- (a->b))
* : l -> (a -> b)
* : (a | l) & (~b | l)
* (~l | ~a | b) & (a | l) & (~b | l)
*/
-
- insertClauseIntoStream( a, l);
- insertClauseIntoStream( ~b, l);
- insertClauseIntoStream( ~l, ~a, b);
-
+
+ insertClauseIntoStream(a, l);
+ insertClauseIntoStream(~b, l);
+ insertClauseIntoStream(~l, ~a, b);
+
return l;
}
-Lit TseitinCnfStream::handleNot(const Node & n){
+Lit TseitinCnfStream::handleNot(const Node & n) {
Assert(n.getKind() == NOT);
-
+
// n : NOT m
Node m = n[0];
Lit equivM = recTransform(m);
//FIXME: This function is a major hack! Should be changed ASAP
//Assumes binary no else if branchs, and that ITEs
-Lit TseitinCnfStream::handleIte(const Node & n){
+Lit TseitinCnfStream::handleIte(const Node & n) {
Assert(n.getKind() == ITE);
-
+
// n : IF c THEN t ELSE f ENDIF;
Lit c = recTransform(n[0]);
Lit t = recTransform(n[1]);
Lit f = recTransform(n[2]);
-
+
// d <-> IF c THEN tB ELSE fb
// : d -> (c & tB) | (~c & fB)
// : ~d | ( (c & tB) | (~c & fB) )
Lit d = aquireAndRegister(n);
- insertClauseIntoStream(~d , ~c , t);
- insertClauseIntoStream(~d , c , f);
- insertClauseIntoStream(~d , f , t);
- insertClauseIntoStream(~c , ~t , d);
- insertClauseIntoStream( c , ~f , d);
+ insertClauseIntoStream(~d, ~c, t);
+ insertClauseIntoStream(~d, c, f);
+ insertClauseIntoStream(~d, f, t);
+ insertClauseIntoStream(~c, ~t, d);
+ insertClauseIntoStream(c, ~f, d);
return d;
}
//FIXME: This function is a major hack! Should be changed ASAP
//TODO: Should be moved. Not sure where...
-//TODO: Should use positive defintion, i.e. what kinds are atomic.
-bool atomic(const Node & n){
- switch(n.getKind()){
+//TODO: Should use positive definition, i.e. what kinds are atomic.
+bool atomic(const Node & n) {
+ switch(n.getKind()) {
case NOT:
case XOR:
case ITE:
//TODO: The following code assumes everthing is either
// an atom or is a logical connective. This ignores quantifiers and lambdas.
-Lit TseitinCnfStream::recTransform(const Node & n){
- if(isCached(n)){
+Lit TseitinCnfStream::recTransform(const Node & n) {
+ if(isCached(n)) {
return lookupInCache(n);
}
-
- if(atomic(n)){
+
+ if(atomic(n)) {
return handleAtom(n);
- }else{
+ } else {
//Assume n is a logical connective
- switch(n.getKind()){
+ switch(n.getKind()) {
case NOT:
return handleNot(n);
case XOR:
}
}
}
-
-void TseitinCnfStream::convertAndAssert(const Node & n){
+
+void TseitinCnfStream::convertAndAssert(const Node & n) {
//n has already been mapped so use the previous result
- if(isCached(n)){
+ if(isCached(n)) {
Lit l = lookupInCache(n);
insertClauseIntoStream(l);
return;
}
-
+
Lit e = recTransform(n);
- insertClauseIntoStream( e );
+ insertClauseIntoStream(e);
//I've commented the following section out because it uses a bit too much intelligence.
/*
- if(n.getKind() == AND){
- // this code is required to efficiently flatten and
- // assert each part of the node.
- // This would be rendered unnessecary if the input was given differently
- queue<Node> and_queue;
- and_queue.push(n);
-
- //This was changed to use a queue due to pressure on the C stack.
-
- //TODO: this does no cacheing of what has been asserted.
- //Low hanging fruit
- while(!and_queue.empty()){
- Node curr = and_queue.front();
- and_queue.pop();
- if(curr.getKind() == AND){
- for(Node::iterator i = curr.begin(); i != curr.end(); ++i){
- and_queue.push(*i);
- }
- }else{
- convertAndAssert(curr);
- }
- }
- }else if(n.getKind() == OR){
- //This is special cased so minimal translation is done for things that
- //are already in CNF so minimal work is done on clauses.
- vec<Lit> c;
- for(Node::iterator i = n.begin(); i != n.end(); ++i){
- Lit cl = recTransform(*i);
- c.push(cl);
- }
- insertClauseIntoStream(c);
- }else{
- Lit e = recTransform(n);
- insertClauseIntoStream( e );
- }
- */
+ if(n.getKind() == AND){
+ // this code is required to efficiently flatten and
+ // assert each part of the node.
+ // This would be rendered unnessecary if the input was given differently
+ queue<Node> and_queue;
+ and_queue.push(n);
+
+ //This was changed to use a queue due to pressure on the C stack.
+
+ //TODO: this does no cacheing of what has been asserted.
+ //Low hanging fruit
+ while(!and_queue.empty()){
+ Node curr = and_queue.front();
+ and_queue.pop();
+ if(curr.getKind() == AND){
+ for(Node::iterator i = curr.begin(); i != curr.end(); ++i){
+ and_queue.push(*i);
+ }
+ }else{
+ convertAndAssert(curr);
+ }
+ }
+ }else if(n.getKind() == OR){
+ //This is special cased so minimal translation is done for things that
+ //are already in CNF so minimal work is done on clauses.
+ vec<Lit> c;
+ for(Node::iterator i = n.begin(); i != n.end(); ++i){
+ Lit cl = recTransform(*i);
+ c.push(cl);
+ }
+ insertClauseIntoStream(c);
+ }else{
+ Lit e = recTransform(n);
+ insertClauseIntoStream( e );
+ }
+ */
}
-
-
-
}/* CVC4::prop namespace */
}/* CVC4 namespace */
** internals such as the representation and translation of
**/
-
#ifndef __CVC4__CNF_STREAM_H
#define __CVC4__CNF_STREAM_H
-//TODO: Why am i including this? Who knows...
-#include "cvc4_config.h"
-
#include "expr/node.h"
#include "prop/minisat/simp/SimpSolver.h"
#include "prop/minisat/core/SolverTypes.h"
#include <map>
namespace CVC4 {
- class PropEngine;
+class PropEngine;
}
-
namespace CVC4 {
namespace prop {
+/**
+ * Comments for the behavior of the whole class...
+ * @author Tim King <taking@cs.nyu.edu>
+ */
class CnfStream {
private:
+
/**
- * d_propEngine is the PropEngine that the CnfStream interacts with directly through
- * the follwoing functions:
+ * d_propEngine is the PropEngine that the CnfStream interacts with directly
+ * through the following functions:
* - insertClauseIntoStream
* - acquireFreshLit
* - registerMapping
*/
PropEngine *d_propEngine;
- /**Cache of what literal have been registered to a node.
- *Not strictly needed for correctness.
- *This can be flushed when memory is under pressure.
+ /**
+ * Cache of what literal have been registered to a node. Not strictly needed
+ * for correctness. This can be flushed when memory is under pressure.
+ * TODO: Use attributes when they arrive
*/
- std::map<Node,minisat::Lit> d_translationCache;
-
+ std::map<Node, minisat::Lit> d_translationCache;
+
protected:
/**
* Uniform interface for sending a clause back to d_propEngine.
- * May want to have internal datastructures later on
+ * May want to have internal data-structures later on
*/
void insertClauseIntoStream(minisat::vec<minisat::Lit> & c);
void insertClauseIntoStream(minisat::Lit a);
- void insertClauseIntoStream(minisat::Lit a,minisat::Lit b);
- void insertClauseIntoStream(minisat::Lit a,minisat::Lit b, minisat::Lit c);
-
+ void insertClauseIntoStream(minisat::Lit a, minisat::Lit b);
+ void insertClauseIntoStream(minisat::Lit a, minisat::Lit b, minisat::Lit c);
//utilities for the translation cache;
bool isCached(const Node & n) const;
+
+ /**
+ * Method comments...
+ * @param n
+ * @return returns ...
+ */
minisat::Lit lookupInCache(const Node & n) const;
/**
public:
/**
* Constructs a CnfStream that sends constructs an equisatisfiable set of clauses
- * and sends them to pe.
+ * and sends them to the given PropEngine.
+ * @param pe
*/
CnfStream(CVC4::PropEngine *pe);
-
/**
* Converts and asserts a formula.
* @param n node to convert and assert
}; /* class CnfStream */
-
/**
* TseitinCnfStream is based on the following recursive algorithm
* http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
* The general gist of the algorithm is to introduce a new literal that
- * will be equivalent to each subexpression in the constructed equisatisfiable formula
- * then subsistute the new literal for the formula, and to do this recursively.
+ * will be equivalent to each subexpression in the constructed equisatisfiable
+ * formula then substitute the new literal for the formula, and to do this
+ * recursively.
*
* This implementation does this in a single recursive pass.
*/
/* Each of these formulas handles takes care of a Node of each Kind.
*
- * Each handleX(Node &n) is responsibile for:
- * - constructing a new literal, l (if nessecary)
+ * Each handleX(Node &n) is responsible for:
+ * - constructing a new literal, l (if necessary)
* - calling registerNode(n,l)
- * - adding clauses asure that l is equivalent to the Node
- * - calling recTransform on its children (if nessecary)
+ * - adding clauses assure that l is equivalent to the Node
+ * - calling recTransform on its children (if necessary)
* - returning l
*
* handleX( n ) can assume that n is not in d_translationCache
minisat::Lit handleAnd(const Node& n);
minisat::Lit handleOr(const Node& n);
-
/**
- *Maps recTransform over the children of a node.
- *This is very useful for n-ary Kinds (OR, AND).
- *
- *Non n-ary kinds (IMPLIES) should avoid using this as it requires a
- *tiny bit of extra overhead, and it leads to less readable code.
+ * Maps recTransform over the children of a node. This is very useful for
+ * n-ary Kinds (OR, AND). Non n-ary kinds (IMPLIES) should avoid using this
+ * as it requires a tiny bit of extra overhead, and it leads to less readable
+ * code.
*
* precondition: target.size() == n.getNumChildren()
+ * @param n ...
+ * @param target ...
*/
- void mapRecTransformOverChildren(const Node& n, minisat::vec<minisat::Lit> & target);
+ void mapRecTransformOverChildren(const Node& n,
+ minisat::vec<minisat::Lit> & target);
- //Recurisively dispatches the various Kinds to the appropriate handler.
+ //Recursively dispatches the various Kinds to the appropriate handler.
minisat::Lit recTransform(const Node & n);
}; /* class TseitinCnfStream */
}/* prop namespace */
}/* CVC4 namespace */
-
-
#endif /* __CVC4__CNF_STREAM_H */
projects / cvc5.git / commitdiff