}
: f = orFormula
( IMPLIES e = impliesFormula
- { f = mkExpr(CVC4::IFF, f, e); }
+ { f = mkExpr(CVC4::IMPLIES, f, e); }
)?
;
namespace CVC4 {
namespace prop {
-CnfStream::CnfStream(PropEngine *pe) :
- d_propEngine(pe) {
+CnfStream::CnfStream(SatSolver *satSolver) :
+ d_satSolver(satSolver) {
}
-TseitinCnfStream::TseitinCnfStream(PropEngine *pe) :
- CnfStream(pe) {
+TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver) :
+ CnfStream(satSolver) {
}
-void CnfStream::insertClauseIntoStream(SatClause& c) {
+void CnfStream::assertClause(SatClause& c) {
Debug("cnf") << "Inserting into stream " << c << endl;
- d_propEngine->assertClause(c);
+ d_satSolver->addClause(c);
}
-void CnfStream::insertClauseIntoStream(SatLiteral a) {
+void CnfStream::assertClause(SatLiteral a) {
SatClause clause(1);
clause[0] = a;
- insertClauseIntoStream(clause);
+ assertClause(clause);
}
-void CnfStream::insertClauseIntoStream(SatLiteral a, SatLiteral b) {
+void CnfStream::assertClause(SatLiteral a, SatLiteral b) {
SatClause clause(2);
clause[0] = a;
clause[1] = b;
- insertClauseIntoStream(clause);
+ assertClause(clause);
}
-void CnfStream::insertClauseIntoStream(SatLiteral a, SatLiteral b, SatLiteral c) {
+void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) {
SatClause clause(3);
clause[0] = a;
clause[1] = b;
clause[2] = c;
- insertClauseIntoStream(clause);
+ assertClause(clause);
}
bool CnfStream::isCached(const Node& n) const {
}
SatLiteral CnfStream::lookupInCache(const Node& n) const {
- Assert(isCached(n),
- "Node is not in cnf translation cache");
+ Assert(isCached(n), "Node is not in CNF translation cache");
return d_translationCache.find(n)->second;
}
-void CnfStream::flushCache() {
- Debug("cnf") << "flushing the translation cache" << endl;
- d_translationCache.clear();
-}
-
void CnfStream::cacheTranslation(const Node& node, SatLiteral lit) {
Debug("cnf") << "caching translation " << node << " to " << lit << endl;
d_translationCache.insert(make_pair(node, lit));
}
-SatLiteral CnfStream::aquireAndRegister(const Node& node, bool atom) {
- SatVariable var = atom ? d_propEngine->registerAtom(node)
- : d_propEngine->requestFreshVar();
- SatLiteral lit(var);
+SatLiteral CnfStream::newLiteral(const Node& node) {
+ SatLiteral lit = SatLiteral(d_satSolver->newVar());
cacheTranslation(node, lit);
return lit;
}
-bool CnfStream::isAtomMapped(const Node& n) const {
- return d_propEngine->isAtomMapped(n);
-}
-
-SatVariable CnfStream::lookupAtom(const Node& n) const {
- return d_propEngine->lookupAtom(n);
-}
-
-/***********************************************/
-/***********************************************/
-/************ End of CnfStream *****************/
-/***********************************************/
-/***********************************************/
+SatLiteral TseitinCnfStream::handleAtom(const Node& node) {
+ Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom");
+ Assert(!isCached(node), "atom already mapped!");
-SatLiteral TseitinCnfStream::handleAtom(const Node& n) {
- Assert(n.isAtomic(), "handleAtom(n) expects n to be an atom");
+ Debug("cnf") << "handleAtom(" << node << ")" << endl;
- Debug("cnf") << "handling atom" << endl;
+ SatLiteral lit = newLiteral(node);
- SatLiteral l = aquireAndRegister(n, true);
- switch(n.getKind()) { /* TRUE and FALSE are handled specially. */
+ switch(node.getKind()) {
case TRUE:
- insertClauseIntoStream(l);
+ assertClause(lit);
break;
case FALSE:
- insertClauseIntoStream(~l);
+ assertClause(~lit);
break;
- default: //Does nothing else
+ default:
break;
}
- return l;
+
+ return lit;
}
-SatLiteral TseitinCnfStream::handleXor(const Node& n) {
- // n: a XOR b
+SatLiteral TseitinCnfStream::handleXor(const Node& xorNode) {
+ Assert(!isCached(xorNode), "Atom already mapped!");
+ Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!");
+ Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!");
- SatLiteral a = recTransform(n[0]);
- SatLiteral b = recTransform(n[1]);
+ SatLiteral a = toCNF(xorNode[0]);
+ SatLiteral b = toCNF(xorNode[1]);
- SatLiteral l = aquireAndRegister(n);
+ SatLiteral xorLit = newLiteral(xorNode);
- insertClauseIntoStream(a, b, ~l);
- insertClauseIntoStream(a, ~b, l);
- insertClauseIntoStream(~a, b, l);
- insertClauseIntoStream(~a, ~b, ~l);
+ assertClause(a, b, ~xorLit);
+ assertClause(~a, ~b, ~xorLit);
+ assertClause(a, ~b, xorLit);
+ assertClause(~a, b, xorLit);
- return l;
+ return xorLit;
}
-/* 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,
- SatClause& target) {
- Assert((unsigned)target.size() == n.getNumChildren(),
- "Size of the children must be the same the constructed clause");
-
- int i = 0;
- Node::iterator subExprIter = n.begin();
-
- while(subExprIter != n.end()) {
- SatLiteral equivalentLit = recTransform(*subExprIter);
- target[i] = equivalentLit;
- ++subExprIter;
- ++i;
+SatLiteral TseitinCnfStream::handleOr(const Node& orNode) {
+ Assert(!isCached(orNode), "Atom already mapped!");
+ Assert(orNode.getKind() == OR, "Expecting an OR expression!");
+ Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!");
+
+ // Number of children
+ unsigned n_children = orNode.getNumChildren();
+
+ // Transform all the children first
+ Node::iterator node_it = orNode.begin();
+ Node::iterator node_it_end = orNode.end();
+ SatClause clause(n_children + 1);
+ for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
+ clause[i] = toCNF(*node_it);
}
-}
-SatLiteral TseitinCnfStream::handleOr(const Node& n) {
- //child_literals
- SatClause lits(n.getNumChildren());
- mapRecTransformOverChildren(n, lits);
-
- SatLiteral e = aquireAndRegister(n);
-
- /* e <-> (a1 | a2 | a3 | ...)
- *: e -> (a1 | a2 | a3 | ...)
- * : ~e | (
- * : ~e | a1 | a2 | a3 | ...
- * e <- (a1 | a2 | a3 | ...)
- * : e <- (a1 | a2 | a3 |...)
- * : e | ~(a1 | a2 | a3 |...)
- * :
- * : (e | ~a1) & (e |~a2) & (e & ~a3) & ...
- */
-
- SatClause c(1 + lits.size());
-
- for(int index = 0; index < lits.size(); ++index) {
- SatLiteral a = lits[index];
- c[index] = a;
- insertClauseIntoStream(e, ~a);
+ // Get the literal for this node
+ SatLiteral orLit = newLiteral(orNode);
+
+ // lit <- (a_1 | a_2 | a_3 | ... | a_n)
+ // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
+ // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
+ for(unsigned i = 0; i < n_children; ++i) {
+ assertClause(orLit, ~clause[i]);
}
- c[lits.size()] = ~e;
- insertClauseIntoStream(c);
- return e;
-}
+ // lit -> (a_1 | a_2 | a_3 | ... | a_n)
+ // ~lit | a_1 | a_2 | a_3 | ... | a_n
+ clause[n_children] = ~orLit;
+ // This needs to go last, as the clause might get modified by the SAT solver
+ assertClause(clause);
-/* TODO: this only supports 2-ary <=> nodes atm.
- * Should this be changed?
- */
-SatLiteral TseitinCnfStream::handleIff(const Node& n) {
- Assert(n.getKind() == IFF);
- Assert(n.getNumChildren() == 2);
- // n: a <=> b;
-
- SatLiteral a = recTransform(n[0]);
- SatLiteral b = recTransform(n[1]);
-
- SatLiteral l = aquireAndRegister(n);
-
- /* l <-> (a<->b)
- * : l -> ((a-> b) & (b->a))
- * : ~l | ((~a | b) & (~b |a))
- * : (~a | b | ~l ) & (~b | a | ~l)
- *
- * : (a<->b) -> l
- * : ~((a & b) | (~a & ~b)) | l
- * : (~(a & b)) & (~(~a & ~b)) | l
- * : ((~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);
-
- return l;
+ // Return the literal
+ return orLit;
}
-SatLiteral 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?
- SatClause lits(n.getNumChildren());
- mapRecTransformOverChildren(n, lits);
-
- SatLiteral e = aquireAndRegister(n);
-
- /* e <-> (a1 & a2 & a3 & ...)
- * : e -> (a1 & a2 & a3 & ...)
- * : ~e | (a1 & a2 & a3 & ...)
- * : (~e | a1) & (~e | a2) & ...
- * e <- (a1 & a2 & a3 & ...)
- * : e <- (a1 & a2 & a3 & ...)
- * : e | ~(a1 & a2 & a3 & ...)
- * : e | (~a1 | ~a2 | ~a3 | ...)
- * : e | ~a1 | ~a2 | ~a3 | ...
- */
-
- SatClause c(lits.size() + 1);
- for(int index = 0; index < lits.size(); ++index) {
- SatLiteral a = lits[index];
- c[index] = (~a);
- insertClauseIntoStream(~e, a);
+SatLiteral TseitinCnfStream::handleAnd(const Node& andNode) {
+ Assert(!isCached(andNode), "Atom already mapped!");
+ Assert(andNode.getKind() == AND, "Expecting an AND expression!");
+ Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!");
+
+ // Number of children
+ unsigned n_children = andNode.getNumChildren();
+
+ // Transform all the children first (remembering the negation)
+ Node::iterator node_it = andNode.begin();
+ Node::iterator node_it_end = andNode.end();
+ SatClause clause(n_children + 1);
+ for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
+ clause[i] = ~toCNF(*node_it);
}
- c[lits.size()] = e;
- insertClauseIntoStream(c);
+ // Get the literal for this node
+ SatLiteral andLit = newLiteral(andNode);
+
+ // lit -> (a_1 & a_2 & a_3 & ... & a_n)
+ // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
+ // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
+ for(unsigned i = 0; i < n_children; ++i) {
+ assertClause(~andLit, ~clause[i]);
+ }
+
+ // lit <- (a_1 & a_2 & a_3 & ... a_n)
+ // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
+ // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
+ clause[n_children] = andLit;
+ // This needs to go last, as the clause might get modified by the SAT solver
+ assertClause(clause);
+ return andLit;
+}
+
+SatLiteral TseitinCnfStream::handleImplies(const Node& impliesNode) {
+ Assert(!isCached(impliesNode), "Atom already mapped!");
+ Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!");
+ Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!");
+
+ // Convert the children to cnf
+ SatLiteral a = toCNF(impliesNode[0]);
+ SatLiteral b = toCNF(impliesNode[1]);
+
+ SatLiteral impliesLit = newLiteral(impliesNode);
+
+ // lit -> (a->b)
+ // ~lit | ~ a | b
+ assertClause(~impliesLit, ~a, b);
+
+ // (a->b) -> lit
+ // ~(~a | b) | lit
+ // (a | l) & (~b | l)
+ assertClause(a, impliesLit);
+ assertClause(~b, impliesLit);
- return e;
+ return impliesLit;
}
-SatLiteral TseitinCnfStream::handleImplies(const Node& n) {
- Assert(n.getKind() == IMPLIES);
- Assert(n.getNumChildren() == 2);
- // n: a => b;
-
- SatLiteral a = recTransform(n[0]);
- SatLiteral b = recTransform(n[1]);
-
- SatLiteral l = aquireAndRegister(n);
-
- /* l <-> (a->b)
- * (l -> (a->b)) & (l <- (a->b))
- * : l -> (a -> b)
- * : ~l | (~ a | b)
- * : (~l | ~a | b)
- * (~l | ~a | b) & (l<- (a->b))
- * : (a->b) -> l
- * : ~(~a | b) | l
- * : (a & ~b) | l
- * : (a | l) & (~b | l)
- * (~l | ~a | b) & (a | l) & (~b | l)
- */
-
- insertClauseIntoStream(a, l);
- insertClauseIntoStream(~b, l);
- insertClauseIntoStream(~l, ~a, b);
-
- return l;
+
+SatLiteral TseitinCnfStream::handleIff(const Node& iffNode) {
+ Assert(!isCached(iffNode), "Atom already mapped!");
+ Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
+ Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
+
+ // Convert the children to CNF
+ SatLiteral a = toCNF(iffNode[0]);
+ SatLiteral b = toCNF(iffNode[1]);
+
+ // Get the now literal
+ SatLiteral iffLit = newLiteral(iffNode);
+
+ // lit -> ((a-> b) & (b->a))
+ // ~lit | ((~a | b) & (~b | a))
+ // (~a | b | ~lit) & (~b | a | ~lit)
+ assertClause(~a, b, ~iffLit);
+ assertClause(a, ~b, ~iffLit);
+
+ // (a<->b) -> lit
+ // ~((a & b) | (~a & ~b)) | lit
+ // (~(a & b)) & (~(~a & ~b)) | lit
+ // ((~a | ~b) & (a | b)) | lit
+ // (~a | ~b | lit) & (a | b | lit)
+ assertClause(~a, ~b, iffLit);
+ assertClause(a, b, iffLit);
+
+ return iffLit;
}
-SatLiteral TseitinCnfStream::handleNot(const Node& n) {
- Assert(n.getKind() == NOT);
- Assert(n.getNumChildren() == 1);
- // n : NOT m
- Node m = n[0];
- SatLiteral equivM = recTransform(m);
+SatLiteral TseitinCnfStream::handleNot(const Node& notNode) {
+ Assert(!isCached(notNode), "Atom already mapped!");
+ Assert(notNode.getKind() == NOT, "Expecting a NOT expression!");
+ Assert(notNode.getNumChildren() == 1, "Expecting exactly 2 children!");
- SatLiteral equivN = ~equivM;
+ SatLiteral notLit = ~toCNF(notNode[0]);
- cacheTranslation(n, equivN);
+ // Since we don't introduce new variables, we need to cache the translation
+ cacheTranslation(notNode, notLit);
- return equivN;
+ return notLit;
}
-SatLiteral TseitinCnfStream::handleIte(const Node& n) {
- Assert(n.getKind() == ITE);
- Assert(n.getNumChildren() == 3);
-
- // n : IF c THEN t ELSE f ENDIF;
- SatLiteral c = recTransform(n[0]);
- SatLiteral t = recTransform(n[1]);
- SatLiteral f = recTransform(n[2]);
-
- // d <-> IF c THEN tB ELSE fb
- // : d -> (c & tB) | (~c & fB)
- // : ~d | ( (c & tB) | (~c & fB) )
- // : x | (y & z) = (x | y) & (x | z)
- // : ~d | ( ((c & t) | ~c ) & ((c & t) | f ) )
- // : ~d | ( (((c | ~c) & (~c | t))) & ((c | f) & (f | t)) )
- // : ~d | ( (~c | t) & (c | f) & (f | t) )
- // : (~d | ~c | t) & (~d | c | f) & (~d | f | t)
-
- // : ~d | (c & t & f)
- // : (~d | c) & (~d | t) & (~d | f)
- // ( IF c THEN tB ELSE fb) -> d
- // :~((c & tB) | (~c & fB)) | d
- // : ((~c | ~t)& ( c |~fb)) | d
- // : (~c | ~ t | d) & (c | ~f | d)
-
- SatLiteral d = aquireAndRegister(n);
-
- insertClauseIntoStream(~d, ~c, t);
- insertClauseIntoStream(~d, c, f);
- insertClauseIntoStream(~d, f, t);
- insertClauseIntoStream(~c, ~t, d);
- insertClauseIntoStream(c, ~f, d);
-
- return d;
+SatLiteral TseitinCnfStream::handleIte(const Node& iteNode) {
+ Assert(iteNode.getKind() == ITE);
+ Assert(iteNode.getNumChildren() == 3);
+
+ SatLiteral condLit = toCNF(iteNode[0]);
+ SatLiteral thenLit = toCNF(iteNode[1]);
+ SatLiteral elseLit = toCNF(iteNode[2]);
+
+ SatLiteral iteLit = newLiteral(iteNode);
+
+ // If ITE is true then one of the branches is true and the condition
+ // implies which one
+ assertClause(~iteLit, ~condLit, thenLit);
+ assertClause(~iteLit, condLit, elseLit);
+ assertClause(~iteLit, elseLit, thenLit);
+
+ // If ITE is false then one of the branches is false and the condition
+ // implies which one
+ assertClause(iteLit, ~condLit, ~thenLit);
+ assertClause(iteLit, condLit, ~elseLit);
+ assertClause(iteLit, ~thenLit, ~elseLit);
+
+ return iteLit;
}
-//TODO: The following code assumes everything is either
-// an atom or is a logical connective. This ignores quantifiers and lambdas.
-SatLiteral TseitinCnfStream::recTransform(const Node& n) {
- if(isCached(n)) {
- return lookupInCache(n);
+SatLiteral TseitinCnfStream::toCNF(const Node& node) {
+
+ // If the node has already been translated, return the previous translation
+ if(isCached(node)) {
+ return lookupInCache(node);
+ }
+
+ // Atomic nodes are treated specially
+ if(node.isAtomic()) {
+ return handleAtom(node);
}
- if(n.isAtomic()) {
-
- /* Unfortunately 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.
- */
- SatLiteral l(lookupAtom(n));
- cacheTranslation(n, l);
- return l;
- }
- return handleAtom(n);
- } else {
- //Assume n is a logical connective
- switch(n.getKind()) {
- case NOT:
- return handleNot(n);
- case XOR:
- return handleXor(n);
- case ITE:
- return handleIte(n);
- case IFF:
- return handleIff(n);
- case IMPLIES:
- return handleImplies(n);
- case OR:
- return handleOr(n);
- case AND:
- return handleAnd(n);
- default:
- Unreachable();
- }
+ // Handle each Boolean operator case
+ switch(node.getKind()) {
+ case NOT:
+ return handleNot(node);
+ case XOR:
+ return handleXor(node);
+ case ITE:
+ return handleIte(node);
+ case IFF:
+ return handleIff(node);
+ case IMPLIES:
+ return handleImplies(node);
+ case OR:
+ return handleOr(node);
+ case AND:
+ return handleAnd(node);
+ default:
+ Unreachable();
}
}
-void TseitinCnfStream::convertAndAssert(const Node& n) {
- SatLiteral e = recTransform(n);
- insertClauseIntoStream(e);
+void TseitinCnfStream::convertAndAssert(const Node& node) {
+ Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
+ assertClause(toCNF(node));
}
}/* CVC4::prop namespace */
#include "expr/node.h"
#include "prop/sat.h"
-#include <map>
+#include <ext/hash_map>
+
+namespace __gnu_cxx {
+template<>
+ struct hash<CVC4::Node> {
+ size_t operator()(const CVC4::Node& node) const {
+ return (size_t)node.hash();
+ }
+ };
+} /* __gnu_cxx namespace */
namespace CVC4 {
namespace prop {
private:
+ /** The SAT solver we will be using */
+ SatSolver *d_satSolver;
+
+ /** Cache of what literal have been registered to a node. */
+ __gnu_cxx::hash_map<Node, SatLiteral> d_translationCache;
+
+protected:
+
/**
- * d_propEngine is the PropEngine that the CnfStream interacts with directly
- * through the following functions:
- * - insertClauseIntoStream
- * - acquireFreshLit
- * - registerMapping
+ * Asserts the given clause to the sat solver.
+ * @param clause the clasue to assert
*/
- PropEngine *d_propEngine;
+ void assertClause(SatClause& clause);
/**
- * 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
+ * Asserts the unit clause to the sat solver.
+ * @param a the unit literal of the clause
*/
- std::map<Node, SatLiteral> d_translationCache;
-
-protected:
+ void assertClause(SatLiteral a);
- bool isAtomMapped(const Node& n) const;
-
- SatVariable lookupAtom(const Node& node) const;
+ /**
+ * Asserts the binary clause to the sat solver.
+ * @param a the first literal in the clause
+ * @param b the second literal in the clause
+ */
+ void assertClause(SatLiteral a, SatLiteral b);
/**
- * Uniform interface for sending a clause back to d_propEngine.
- * May want to have internal data-structures later on
+ * Asserts the ternary clause to the sat solver.
+ * @param a the first literal in the clause
+ * @param b the second literal in the clause
+ * @param c the thirs literal in the clause
*/
- void insertClauseIntoStream(SatClause& clause);
- void insertClauseIntoStream(SatLiteral a);
- void insertClauseIntoStream(SatLiteral a, SatLiteral b);
- void insertClauseIntoStream(SatLiteral a, SatLiteral b, SatLiteral c);
+ void assertClause(SatLiteral a, SatLiteral b, SatLiteral c);
- //utilities for the translation cache;
+ /**
+ * Returns true if the node has been cashed in the translation cache.
+ * @param node the node
+ * @return true if the node has been cached
+ */
bool isCached(const Node& node) const;
/**
- * Method comments...
- * @param n
- * @return returns ...
+ * Returns the cashed literal corresponding to the given node.
+ * @param node the node to lookup
+ * @return returns the corresponding literal
*/
SatLiteral lookupInCache(const Node& n) const;
- //negotiates the mapping of atoms to literals with PropEngine
+ /**
+ * Caches the pair of the node and the literal corresponding to the
+ * translation.
+ * @param node node
+ * @param lit
+ */
void cacheTranslation(const Node& node, SatLiteral lit);
- SatLiteral aquireAndRegister(const Node& node, bool atom = false);
-
-public:
-
/**
- * Constructs a CnfStream that sends constructs an equisatisfiable set of clauses
- * and sends them to the given PropEngine.
- * @param propEngine
+ * Acquires a new variable from the SAT solver to represent the node and
+ * inserts the necessary data it into the mapping tables.
+ * @param node a formula
+ * @return the literal corresponding to the formula
*/
- CnfStream(PropEngine* propEngine);
+ SatLiteral newLiteral(const Node& node);
+
+public:
/**
- * Empties the internal translation cache.
+ * 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
*/
- void flushCache();
+ CnfStream(SatSolver* satSolver);
/**
* Converts and asserts a formula.
* @param node node to convert and assert
+ * @param whether the sat solver can choose to remove this clause
*/
virtual void convertAndAssert(const Node& node) = 0;
public:
+ /**
+ * Convert a given formula to CNF and assert it to the SAT solver.
+ * @param node the formula to assert
+ */
void convertAndAssert(const Node& node);
- TseitinCnfStream(PropEngine* propEngine);
+ /**
+ * Constructs the stream to use the given sat solver.
+ * @param satSolver the sat solver to use
+ */
+ TseitinCnfStream(SatSolver* satSolver);
private:
- /* Each of these formulas handles takes care of a Node of each Kind.
- *
- * Each handleX(Node &n) is responsible for:
- * - constructing a new literal, l (if necessary)
- * - calling registerNode(n,l)
- * - 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
- */
+ // Each of these formulas handles takes care of a Node of each Kind.
+ //
+ // Each handleX(Node &n) is responsible for:
+ // - constructing a new literal, l (if necessary)
+ // - calling registerNode(n,l)
+ // - adding clauses assure that l is equivalent to the Node
+ // - calling toCNF on its children (if necessary)
+ // - returning l
+ //
+ // handleX( n ) can assume that n is not in d_translationCache
SatLiteral handleAtom(const Node& node);
SatLiteral handleNot(const Node& node);
SatLiteral handleXor(const Node& node);
SatLiteral handleImplies(const Node& node);
SatLiteral handleIff(const Node& node);
SatLiteral handleIte(const Node& node);
-
SatLiteral handleAnd(const Node& node);
SatLiteral handleOr(const Node& node);
/**
- * 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 ...
+ * Transforms the node into CNF recursively.
+ * @param node the formula to transform
+ * @return the literal representing the root of the formula
*/
- void mapRecTransformOverChildren(const Node& node, SatClause& target);
-
- //Recursively dispatches the various Kinds to the appropriate handler.
- SatLiteral recTransform(const Node& node);
+ SatLiteral toCNF(const Node& node);
}; /* class TseitinCnfStream */
--- /dev/null
+* Accessing the internals of the SAT solver
+
+The non-public parts of the SAT solver are accessed via the static methods in
+the SatSolverProxy class. SatSolverProxy is declared as a friend of the
+SatSolver and has all-privileges access to the internals -- use with care!!!
+
+* Clause Database and CNF
+
+The clause database consists of two parts:
+
+ vec<Clause*> clauses; // List of problem clauses.
+ vec<Clause*> learnts; // List of learnt clauses.
+
+Clauses is the original problem clauses, and learnts are the clauses learned
+during the search. I have disabled removal of satisfied problem clauses by
+setting the remove_satisfied flag to false.
+
+The learnt clauses get removed every once in a while by removing the half of
+clauses with the low activity (reduceDB())
+
+Since the clause database backtracks with the SMT solver, the CNF cache should
+be context dependent and everything will be in sync.
+
+* Adding a Clause
+
+The only method in the interface that allows addition of clauses in MiniSAT is
+
+ bool Solver::addClause(vec<Lit>& ps),
+
+but it only adds the problem clauses.
+
+In order to add the clauses to the removable database the interface is now
+
+ bool Solver::addClause(vec<Lit>& ps, bool removable).
+
+Clauses added with removable=true might get removed by the SAT solver when
+compacting the database.
+
+The question is whether to add the propagation/conflict lemmas as removable or
+not?
+
+* Making it Backtrackable
+
+First, whenever we push a context, we have to know which clauses to remove from
+the clauses vector (the problem clauses). For this we keep a CDO<int> that tells
+us how many clauses are in the database.
+
+We do the same for the learnt (removable) clauses, but this involves a little
+bit more work. When removing clauses, minisat will sort the learnt clauses and
+then remove the first half on non-locked clauses. We remember a CDO<int> for
+the current context and sort/remove from that index on in the vector.
+
+Also, each time we push a context, we need to remember the SAT solvers decision
+level in order to make it the "0" decision level. We also keep this in a
+CDO<int>, but the actual level has to be kept in the SAT solver and hard-coded
+in the routines.
+
+* Literal Activities
+
+We do not backtrack literal activities. This does not semantically change the
+equivalence of the context, but does change solve times if the same problem is
+run several times.
+
+* Conflict Analysis
+
+TODO
+
+* Do we need to assign literals that only appear in satisfied clauses?
namespace CVC4 {
namespace prop {
+
+class SatSolverProxy;
+
namespace minisat {
class Solver {
+
+ /** The only CVC4 entry point to the private solver data */
+ friend class CVC4::prop::SatSolverProxy;
+
public:
// Constructor/Destructor:
namespace prop {
PropEngine::PropEngine(const Options* opts, DecisionEngine* de,
- TheoryEngine* te) :
- d_opts(opts),
- d_de(de),
- d_te(te),
- d_restartMayBeNeeded(false) {
- d_sat = new SatSolver();
- d_cnfStream = new CVC4::prop::TseitinCnfStream(this);
+ TheoryEngine* te)
+: d_inCheckSat(false),
+ d_options(opts),
+ d_decisionEngine(de),
+ d_theoryEngine(te)
+{
+ Debug("prop") << "Constructing the PropEngine" << endl;
+ d_satSolver = new SatSolver();
+ SatSolverProxy::initSatSolver(d_satSolver, d_options);
+ d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver);
}
PropEngine::~PropEngine() {
+ Debug("prop") << "Destructing the PropEngine" << endl;
delete d_cnfStream;
- delete d_sat;
-}
-
-void PropEngine::assertClause(SatClause& clause) {
- /*we can also here add a context dependent queue of assertions
- *for restarting the sat solver
- */
- //TODO assert that each lit has been mapped to an atom or requested
- d_sat->addClause(clause);
-}
-
-SatVariable PropEngine::registerAtom(const Node & n) {
- SatVariable v = requestFreshVar();
- d_atom2var.insert(make_pair(n, v));
- d_var2atom.insert(make_pair(v, n));
- return v;
-}
-
-SatVariable PropEngine::requestFreshVar() {
- return d_sat->newVar();
+ delete d_satSolver;
}
void PropEngine::assertFormula(const Node& node) {
-
- Debug("prop") << "Asserting ";
- node.printAst(Debug("prop"));
- Debug("prop") << endl;
-
+ Assert(!d_inCheckSat, "Sat solver in solve()!");
+ Debug("prop") << "assertFormula(" << node << ")" << endl;
+ // Assert as non-removable
d_cnfStream->convertAndAssert(node);
- d_assertionList.push_back(node);
}
-void PropEngine::restart() {
- delete d_sat;
- d_sat = new SatSolver();
- d_cnfStream->flushCache();
- d_atom2var.clear();
- d_var2atom.clear();
-
- for(vector<Node>::iterator iter = d_assertionList.begin(); iter
- != d_assertionList.end(); ++iter) {
- d_cnfStream->convertAndAssert(*iter);
- }
+void PropEngine::assertLemma(const Node& node) {
+ Debug("prop") << "assertFormula(" << node << ")" << endl;
+ // Assert as removable
+ d_cnfStream->convertAndAssert(node);
}
-Result PropEngine::solve() {
- if(d_restartMayBeNeeded)
- restart();
-
- d_sat->verbosity = (d_opts->verbosity > 0) ? 1 : -1;
- bool result = d_sat->solve();
-
- if(!result) {
- d_restartMayBeNeeded = true;
- }
-
- Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
-
+Result PropEngine::checkSat() {
+ Assert(!d_inCheckSat, "Sat solver in solve()!");
+ Debug("prop") << "solve()" << endl;
+ // Mark that we are in the checkSat
+ d_inCheckSat = true;
+ // Check the problem
+ bool result = d_satSolver->solve();
+ // Not in checkSat any more
+ d_inCheckSat = false;
+ Debug("prop") << "solve() => " << (result ? "true" : "false") << endl;
return Result(result ? Result::SAT : Result::UNSAT);
}
-void PropEngine::assertLit(SatLiteral lit) {
- SatVariable var = literalToVariable(lit);
- if(isVarMapped(var)) {
- Node atom = lookupVar(var);
- //Theory* t = ...;
- //t must be the corresponding theory for the atom
-
- //Literal l(atom, sign(l));
- //t->assertLiteral(l );
- }
+void PropEngine::push() {
+ Assert(!d_inCheckSat, "Sat solver in solve()!");
+ Debug("prop") << "push()" << endl;
}
-void PropEngine::signalBooleanPropHasEnded() {
+void PropEngine::pop() {
+ Assert(!d_inCheckSat, "Sat solver in solve()!");
+ Debug("prop") << "pop()" << endl;
}
-//TODO decisionEngine should be told
-//TODO theoryEngine to call lightweight theory propogation
}/* prop namespace */
}/* CVC4 namespace */
#include "cvc4_config.h"
#include "expr/node.h"
-#include "util/decision_engine.h"
-#include "theory/theory_engine.h"
-#include "sat.h"
#include "util/result.h"
#include "util/options.h"
-
-#include <map>
+#include "util/decision_engine.h"
+#include "theory/theory_engine.h"
+#include "prop/sat.h"
namespace CVC4 {
namespace prop {
class CnfStream;
-// In terms of abstraction, this is below (and provides services to)
-// Prover and above (and requires the services of) a specific
-// propositional solver, DPLL or otherwise.
-
+/**
+ * PropEngine is the abstraction of a Sat Solver, providing methods for
+ * solving the SAT problem and conversion to CNF (via the CnfStream).
+ */
class PropEngine {
- friend class CnfStream;
-
- /** The global options */
- const Options *d_opts;
- /** The decision engine we will be using */
- DecisionEngine *d_de;
- /** The theory engine we will be using */
- TheoryEngine *d_te;
-
/**
- * The SAT solver.
+ * Indicates that the sat solver is currently solving something and we should
+ * not mess with it's internal state.
*/
- SatSolver* d_sat;
-
- std::map<Node, SatVariable> d_atom2var;
- std::map<SatVariable, Node> d_var2atom;
+ bool d_inCheckSat;
- /**
- * 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.
- */
- SatVariable registerAtom(const Node& node);
-
- /**
- * Requests a fresh variable from d_sat.
- */
- SatVariable 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& node) const;
+ /** The global options */
+ const Options *d_options;
- /**
- * Returns the variable mapped by the atom Node.
- * @param n the atom to do the lookup by
- * @return the corresponding variable
- */
- SatVariable lookupAtom(const Node& node) const;
+ /** The decision engine we will be using */
+ DecisionEngine *d_decisionEngine;
- /**
- * Flags whether the solver may need to have its state reset before
- * solving occurs
- */
- bool d_restartMayBeNeeded;
+ /** The theory engine we will be using */
+ TheoryEngine *d_theoryEngine;
- /**
- * Cleans existing state in the PropEngine and reinitializes the state.
- */
- void restart();
+ /** The SAT solver*/
+ SatSolver* d_satSolver;
- /**
- * Keeps track of all of the assertions that need to be made.
- */
+ /** List of all of the assertions that need to be made */
std::vector<Node> d_assertionList;
- /**
- * Returns true iff the variable from the sat solver has been mapped to
- * an atom.
- * @param var variable to check if it is mapped
- * @return returns true iff the minisat var has been mapped.
- */
- bool isVarMapped(SatVariable var) const;
-
- /**
- * Returns the atom mapped by the variable v.
- * @param var the variable to do the lookup by
- * @return an atom
- */
- Node lookupVar(SatVariable var) const;
-
- /**
- * Asserts an internally constructed clause. Each literal is assumed to be in
- * the 1-1 mapping contained in d_node2lit and d_lit2node.
- * @param clause the clause to be asserted.
- */
- void assertClause(SatClause& clause);
-
/** The CNF converter in use */
CnfStream* d_cnfStream;
- void assertLit(SatLiteral lit);
- void signalBooleanPropHasEnded();
-
public:
/**
* Create a PropEngine with a particular decision and theory engine.
*/
- PropEngine(const Options* opts, DecisionEngine*, TheoryEngine*);
+ PropEngine(const Options*, DecisionEngine*, TheoryEngine*);
/**
* Destructor.
/**
* Converts the given formula to CNF and assert the CNF to the sat solver.
+ * The formula is asserted permanently for the current context.
+ * @param node the formula to assert
*/
void assertFormula(const Node& node);
/**
- * Currently this takes a well-formed* Node,
- * converts it to a propositionally equisatisifiable formula for a sat solver,
- * and invokes the sat solver for a satisfying assignment.
- * TODO: what does well-formed mean here?
+ * Converts the given formula to CNF and assert the CNF to the sat solver.
+ * The formula can be removed by the sat solver.
+ * @param node the formula to assert
*/
- Result solve();
+ void assertLemma(const Node& node);
-};/* class PropEngine */
-
-inline bool PropEngine::isAtomMapped(const Node & n) const {
- return d_atom2var.find(n) != d_atom2var.end();
-}
+ /**
+ * Checks the current context for satisfiability.
+ */
+ Result checkSat();
-inline SatVariable PropEngine::lookupAtom(const Node & n) const {
- Assert(isAtomMapped(n));
- return d_atom2var.find(n)->second;
-}
+ /**
+ * Push the context level.
+ */
+ void push();
-inline bool PropEngine::isVarMapped(SatVariable v) const {
- return d_var2atom.find(v) != d_var2atom.end();
-}
+ /**
+ * Pop the context level.
+ */
+ void pop();
-inline Node PropEngine::lookupVar(SatVariable v) const {
- Assert(isVarMapped(v));
- return d_var2atom.find(v)->second;
-}
+};/* class PropEngine */
}/* prop namespace */
}/* CVC4 namespace */
#ifdef __CVC4_USE_MINISAT
+#include "util/options.h"
#include "prop/minisat/core/Solver.h"
#include "prop/minisat/core/SolverTypes.h"
return out;
}
+/**
+ * The proxy class that allows us to modify the internals of the SAT solver.
+ * It's only accessible from the PropEngine, and should be treated with major
+ * care.
+ */
+class SatSolverProxy {
+
+ /** Only the prop engine can modify the internals of the SAT solver */
+ friend class PropEngine;
+
+ private:
+
+ /**
+ * Initializes the given sat solver with the given options.
+ * @param satSolver the SAT solver
+ * @param options the options
+ */
+ inline static void initSatSolver(SatSolver* satSolver,
+ const Options* options) {
+ // Setup the verbosity
+ satSolver->verbosity = (options->verbosity > 0) ? 1 : -1;
+ // Do not delete the satisfied clauses, just the learnt ones
+ satSolver->remove_satisfied = false;
+ }
+};
+
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
namespace CVC4 {
-SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
+SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
d_assertions(),
- d_publicEm(em),
- d_nm(em->getNodeManager()),
- d_opts(opts)
+ d_exprManager(em),
+ d_nodeManager(em->getNodeManager()),
+ d_options(opts)
{
- d_de = new DecisionEngine();
- d_te = new TheoryEngine(this);
- d_prop = new PropEngine(opts, d_de, d_te);
+ d_decisionEngine = new DecisionEngine();
+ d_theoryEngine = new TheoryEngine(this);
+ d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine);
}
SmtEngine::~SmtEngine() {
- delete d_prop;
- delete d_te;
- delete d_de;
+ delete d_propEngine;
+ delete d_theoryEngine;
+ delete d_decisionEngine;
}
void SmtEngine::doCommand(Command* c) {
- NodeManagerScope nms(d_nm);
+ NodeManagerScope nms(d_nodeManager);
c->invoke(this);
}
void SmtEngine::processAssertionList() {
for(unsigned i = 0; i < d_assertions.size(); ++i) {
- d_prop->assertFormula(d_assertions[i]);
+ d_propEngine->assertFormula(d_assertions[i]);
}
d_assertions.clear();
}
-
Result SmtEngine::check() {
Debug("smt") << "SMT check()" << std::endl;
processAssertionList();
- return d_prop->solve();
+ return d_propEngine->checkSat();
}
Result SmtEngine::quickCheck() {
Result SmtEngine::checkSat(const BoolExpr& e) {
Debug("smt") << "SMT checkSat(" << e << ")" << std::endl;
- NodeManagerScope nms(d_nm);
+ NodeManagerScope nms(d_nodeManager);
Node node_e = preprocess(e.getNode());
addFormula(node_e);
Result r = check().asSatisfiabilityResult();
Result SmtEngine::query(const BoolExpr& e) {
Debug("smt") << "SMT query(" << e << ")" << std::endl;
- NodeManagerScope nms(d_nm);
- Node node_e = preprocess(d_nm->mkNode(NOT, e.getNode()));
+ NodeManagerScope nms(d_nodeManager);
+ Node node_e = preprocess(d_nodeManager->mkNode(NOT, e.getNode()));
addFormula(node_e);
Result r = check().asValidityResult();
Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl;
Result SmtEngine::assertFormula(const BoolExpr& e) {
Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl;
- NodeManagerScope nms(d_nm);
+ NodeManagerScope nms(d_nodeManager);
Node node_e = preprocess(e.getNode());
addFormula(node_e);
return quickCheck().asValidityResult();
}
void SmtEngine::push() {
+ Debug("smt") << "SMT push()" << std::endl;
}
void SmtEngine::pop() {
+ Debug("smt") << "SMT pop()" << std::endl;
}
}/* CVC4 namespace */
std::vector<Node> d_assertions;
/** Our expression manager */
- ExprManager* d_publicEm;
+ ExprManager* d_exprManager;
/** Out internal expression/node manager */
- NodeManager* d_nm;
+ NodeManager* d_nodeManager;
/** User-level options */
- const Options* d_opts;
+ const Options* d_options;
/** The decision engine */
- DecisionEngine* d_de;
+ DecisionEngine* d_decisionEngine;
/** The decision engine */
- TheoryEngine* d_te;
+ TheoryEngine* d_theoryEngine;
/** The propositional engine */
- prop::PropEngine* d_prop;
-
+ prop::PropEngine* d_propEngine;
/**
* Pre-process an Node. This is expected to be highly-variable,
* passes over the Node. TODO: may need to specify a LEVEL of
* preprocessing (certain contexts need more/less ?).
*/
- Node preprocess(const Node& e);
+ Node preprocess(const Node& node);
/**
* Adds a formula to the current context.
*/
- void addFormula(const Node& e);
+ void addFormula(const Node& node);
/**
* Full check of consistency in current context. Returns true iff
TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
-TESTS = boolean.cvc \
- bug1.cvc \
- hole6.cvc \
- logops.cvc \
- queries0.cvc \
+TESTS = hole6.cvc \
+ logops.01.cvc \
+ logops.02.cvc \
+ logops.03.cvc \
+ logops.04.cvc \
+ logops.05.cvc \
simple2.smt \
simple.cvc \
simple.smt \
- simple-uf.smt \
smallcnf.cvc \
test11.cvc \
- test12.cvc \
test9.cvc \
uf20-03.cvc \
- wiki.cvc
+ wiki.01.cvc \
+ wiki.02.cvc \
+ wiki.03.cvc \
+ wiki.04.cvc \
+ wiki.05.cvc \
+ wiki.06.cvc \
+ wiki.07.cvc \
+ wiki.08.cvc \
+ wiki.09.cvc \
+ wiki.10.cvc \
+ wiki.11.cvc \
+ wiki.12.cvc \
+ wiki.13.cvc \
+ wiki.14.cvc \
+ wiki.15.cvc \
+ wiki.16.cvc \
+ wiki.17.cvc \
+ wiki.18.cvc \
+ wiki.19.cvc \
+ wiki.20.cvc \
+ wiki.21.cvc
# synonyms for "check"
.PHONY: regress regress0 test
--- /dev/null
+a, b, c: BOOLEAN;
+% EXPECT: VALID
+QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
--- /dev/null
+a, b, c: BOOLEAN;
+% EXPECT: INVALID
+QUERY NOT c AND b;
--- /dev/null
+a, b, c: BOOLEAN;
+% EXPECT: VALID
+QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
--- /dev/null
+a, b, c: BOOLEAN;
+% EXPECT: VALID
+QUERY (a => b) <=> (NOT a OR b);
--- /dev/null
+a, b, c: BOOLEAN;
+% EXPECT: VALID
+QUERY TRUE XOR FALSE;
+
+++ /dev/null
-a, b, c: BOOLEAN;
-
-% EXPECT: VALID
-QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
-
-% EXPECT: INVALID
-QUERY NOT c AND b;
-
-% EXPECT: VALID
-QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
-
-% EXPECT: VALID
-QUERY (a => b) <=> (NOT a OR b);
-
-% EXPECT: VALID
-QUERY TRUE XOR FALSE;
-
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR (b OR c) <=> (a OR b) OR c;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND (b AND c) <=> (a AND b) AND c;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR b <=> b OR a;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND b <=> b AND a;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR (a AND b) <=> a;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND (a OR b) <=> a;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR (b AND c) <=> (a OR b) AND (a OR c);
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND (b OR c) <=> (a AND b) OR (a AND c);
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR NOT a;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND NOT a <=> FALSE;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR a <=> a;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND a <=> a;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR FALSE <=> a;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND TRUE <=> a;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR TRUE <=> TRUE;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND FALSE <=> FALSE;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY NOT FALSE <=> TRUE;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY NOT TRUE <=> FALSE;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY NOT (a OR b) <=> NOT a AND NOT b;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY NOT (a AND b) <=> NOT a OR NOT b;
--- /dev/null
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY NOT NOT a <=> a;
+++ /dev/null
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-
-a, b, c : BOOLEAN;
-
-QUERY a OR (b OR c) <=> (a OR b) OR c;
-QUERY a AND (b AND c) <=> (a AND b) AND c;
-
-QUERY a OR b <=> b OR a;
-QUERY a AND b <=> b AND a;
-
-QUERY a OR (a AND b) <=> a;
-QUERY a AND (a OR b) <=> a;
-
-QUERY a OR (b AND c) <=> (a OR b) AND (a OR c);
-QUERY a AND (b OR c) <=> (a AND b) OR (a AND c);
-
-QUERY a OR NOT a;
-QUERY a AND NOT a <=> FALSE;
-
-QUERY a OR a <=> a;
-QUERY a AND a <=> a;
-
-
-QUERY a OR FALSE <=> a;
-QUERY a AND TRUE <=> a;
-
-QUERY a OR TRUE <=> TRUE;
-QUERY a AND FALSE <=> FALSE;
-
-QUERY NOT FALSE <=> TRUE;
-QUERY NOT TRUE <=> FALSE;
-
-QUERY NOT (a OR b) <=> NOT a AND NOT b;
-QUERY NOT (a AND b) <=> NOT a OR NOT b;
-
-QUERY NOT NOT a <=> a;
-
-
outfile=`mktemp -t cvc4_output.XXXXXXXXXX`
echo "$expected_output" >"$expfile"
-echo "$cvc4" --segv-nospin "$benchmark"
-"$cvc4" --segv-nospin "$benchmark" | tee "$outfile"
+# echo "$cvc4" --segv-nospin "$benchmark"
+"$cvc4" --segv-nospin "$benchmark" > "$outfile"
diffs=`diff -u "$expfile" "$outfile"`
diffexit=$?
projects / cvc5.git / commitdiff