From: Dejan Jovanović Date: Tue, 2 Feb 2010 22:36:57 +0000 (+0000) Subject: for tim X-Git-Tag: cvc5-1.0.0~9311 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6d65fe9fbd92f806651d9af13b1924067885446f;p=cvc5.git for tim --- diff --git a/src/prop/cnf_conversion.h b/src/prop/cnf_conversion.h index 924cae063..1d0ac50bb 100644 --- a/src/prop/cnf_conversion.h +++ b/src/prop/cnf_conversion.h @@ -19,11 +19,14 @@ namespace CVC4 { enum CnfConversion { + /** TODO: explanation of DIRECT_EXPONENTIAL (is this implemented?) */ CNF_DIRECT_EXPONENTIAL = 0, + /** Explanation of CNF_VAR_INTRODUCTION */ CNF_VAR_INTRODUCTION = 1 }; inline std::ostream& operator<<(std::ostream&, CVC4::CnfConversion) CVC4_PUBLIC; + inline std::ostream& operator<<(std::ostream& out, CVC4::CnfConversion c) { using namespace CVC4; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 73c3f6c01..0a7774129 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -24,33 +24,34 @@ 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 & c){ +void CnfStream::insertClauseIntoStream(vec & c) { d_propEngine->assertClause(c); } -void CnfStream::insertClauseIntoStream(minisat::Lit a){ +void CnfStream::insertClauseIntoStream(minisat::Lit a) { vec 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 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 clause(3); clause[0] = a; clause[1] = b; @@ -67,22 +68,22 @@ Lit CnfStream::lookupInCache(const Node & n) const { 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; @@ -94,14 +95,14 @@ Lit CnfStream::aquireAndRegister(const Node & node, bool atom){ /***********************************************/ /***********************************************/ -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; @@ -109,45 +110,47 @@ Lit TseitinCnfStream::handleAtom(const Node & n){ 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 & 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 & 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 lits(n.getNumChildren()); mapRecTransformOverChildren(n, lits); - + Lit e = aquireAndRegister(n); - + /* e <-> (a1 | a2 | a3 | ...) *: e -> (a1 | a2 | a3 | ...) * : ~e | ( @@ -161,31 +164,29 @@ Lit TseitinCnfStream::handleOr(const Node& n){ vec 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)) @@ -197,21 +198,21 @@ Lit TseitinCnfStream::handleIff(const Node& n){ * : ((~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 lits(n.getNumChildren()); mapRecTransformOverChildren(n, lits); - + Lit e = aquireAndRegister(n); /* e <-> (a1 & a2 & a3 & ...) @@ -227,25 +228,25 @@ Lit TseitinCnfStream::handleAnd(const Node& n){ vec 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) @@ -258,17 +259,17 @@ Lit TseitinCnfStream::handleImplies(const Node & n){ * : (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); @@ -280,14 +281,14 @@ Lit TseitinCnfStream::handleNot(const Node & n){ //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) ) @@ -306,20 +307,20 @@ Lit TseitinCnfStream::handleIte(const Node & n){ 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: @@ -334,16 +335,16 @@ bool atomic(const Node & n){ //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: @@ -361,61 +362,58 @@ Lit TseitinCnfStream::recTransform(const Node & n){ } } } - -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 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 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 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 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 */ diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index c0a70730a..131ac98dc 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -19,13 +19,9 @@ ** 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" @@ -34,45 +30,55 @@ #include namespace CVC4 { - class PropEngine; +class PropEngine; } - namespace CVC4 { namespace prop { +/** + * Comments for the behavior of the whole class... + * @author Tim King + */ 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 d_translationCache; - + std::map 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 & 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; /** @@ -88,11 +94,11 @@ protected: 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 @@ -101,13 +107,13 @@ public: }; /* 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. */ @@ -121,11 +127,11 @@ private: /* 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 @@ -140,19 +146,20 @@ private: 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 & target); + void mapRecTransformOverChildren(const Node& n, + minisat::vec & 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 */ @@ -160,6 +167,4 @@ private: }/* prop namespace */ }/* CVC4 namespace */ - - #endif /* __CVC4__CNF_STREAM_H */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 097500833..59eddccf0 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -59,7 +59,7 @@ public: SmtEngine(ExprManager* em, Options* opts) throw(); /** - * Destruct the smt engine. + * Destruct the SMT engine. */ ~SmtEngine();