diff options
40 files changed, 629 insertions, 629 deletions
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 7f4ce3c26..794f4706a 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -237,7 +237,7 @@ impliesFormula returns [CVC4::Expr f] } : f = orFormula ( IMPLIES e = impliesFormula - { f = mkExpr(CVC4::IFF, f, e); } + { f = mkExpr(CVC4::IMPLIES, f, e); } )? ; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index b4a0a297e..011d8ba5a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -27,36 +27,36 @@ using namespace std; 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 { @@ -64,328 +64,261 @@ 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 */ diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 0cc8cb425..9fb5858b3 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -25,7 +25,16 @@ #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 { @@ -40,69 +49,84 @@ class CnfStream { 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; @@ -122,47 +146,45 @@ class TseitinCnfStream : public CnfStream { 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 */ diff --git a/src/prop/minisat/CVC4-README b/src/prop/minisat/CVC4-README new file mode 100644 index 000000000..a36116451 --- /dev/null +++ b/src/prop/minisat/CVC4-README @@ -0,0 +1,68 @@ +* 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? diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 2383fd68c..5e51e5f5a 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -36,9 +36,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA 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: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 5889ba504..80a8819b9 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -31,94 +31,59 @@ namespace CVC4 { 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 */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index d60771e95..9aa1ecff8 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -19,118 +19,53 @@ #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. @@ -139,36 +74,34 @@ public: /** * 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 */ diff --git a/src/prop/sat.h b/src/prop/sat.h index 195323755..9375e37ec 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -20,6 +20,7 @@ #ifdef __CVC4_USE_MINISAT +#include "util/options.h" #include "prop/minisat/core/Solver.h" #include "prop/minisat/core/SolverTypes.h" @@ -65,6 +66,33 @@ inline std::ostream& operator << (std::ostream& out, const SatClause& clause) { 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 */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d30255e4f..8bca39df4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -24,25 +24,25 @@ using namespace CVC4::prop; 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); } @@ -52,16 +52,15 @@ Node SmtEngine::preprocess(const Node& e) { 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() { @@ -77,7 +76,7 @@ void SmtEngine::addFormula(const Node& e) { 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(); @@ -87,8 +86,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) { 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; @@ -97,7 +96,7 @@ Result SmtEngine::query(const BoolExpr& e) { 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(); @@ -110,9 +109,11 @@ Expr SmtEngine::simplify(const Expr& e) { } void SmtEngine::push() { + Debug("smt") << "SMT push()" << std::endl; } void SmtEngine::pop() { + Debug("smt") << "SMT pop()" << std::endl; } }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index eb9384ca5..d796959a9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -117,23 +117,22 @@ private: 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, @@ -141,12 +140,12 @@ private: * 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 diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index df0268f80..09be302af 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,19 +1,38 @@ 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 diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc new file mode 100644 index 000000000..d947d1a27 --- /dev/null +++ b/test/regress/regress0/logops.01.cvc @@ -0,0 +1,3 @@ +a, b, c: BOOLEAN; +% EXPECT: VALID +QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc new file mode 100644 index 000000000..ba2d55b4f --- /dev/null +++ b/test/regress/regress0/logops.02.cvc @@ -0,0 +1,3 @@ +a, b, c: BOOLEAN; +% EXPECT: INVALID +QUERY NOT c AND b; diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc new file mode 100644 index 000000000..85b23d2b0 --- /dev/null +++ b/test/regress/regress0/logops.03.cvc @@ -0,0 +1,3 @@ +a, b, c: BOOLEAN; +% EXPECT: VALID +QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc new file mode 100644 index 000000000..a71096542 --- /dev/null +++ b/test/regress/regress0/logops.04.cvc @@ -0,0 +1,3 @@ +a, b, c: BOOLEAN; +% EXPECT: VALID +QUERY (a => b) <=> (NOT a OR b); diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc new file mode 100644 index 000000000..19bbae5b4 --- /dev/null +++ b/test/regress/regress0/logops.05.cvc @@ -0,0 +1,4 @@ +a, b, c: BOOLEAN; +% EXPECT: VALID +QUERY TRUE XOR FALSE; + diff --git a/test/regress/regress0/logops.cvc b/test/regress/regress0/logops.cvc deleted file mode 100644 index 7bd2a356d..000000000 --- a/test/regress/regress0/logops.cvc +++ /dev/null @@ -1,17 +0,0 @@ -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; - diff --git a/test/regress/regress0/wiki.01.cvc b/test/regress/regress0/wiki.01.cvc new file mode 100644 index 000000000..57660b5a1 --- /dev/null +++ b/test/regress/regress0/wiki.01.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR (b OR c) <=> (a OR b) OR c; diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc new file mode 100644 index 000000000..baba45927 --- /dev/null +++ b/test/regress/regress0/wiki.02.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND (b AND c) <=> (a AND b) AND c; diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc new file mode 100644 index 000000000..791cc45c8 --- /dev/null +++ b/test/regress/regress0/wiki.03.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR b <=> b OR a; diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc new file mode 100644 index 000000000..f0f73ce1f --- /dev/null +++ b/test/regress/regress0/wiki.04.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND b <=> b AND a; diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc new file mode 100644 index 000000000..afb094dae --- /dev/null +++ b/test/regress/regress0/wiki.05.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR (a AND b) <=> a; diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc new file mode 100644 index 000000000..421bfbdfd --- /dev/null +++ b/test/regress/regress0/wiki.06.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND (a OR b) <=> a; diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc new file mode 100644 index 000000000..a28cbf553 --- /dev/null +++ b/test/regress/regress0/wiki.07.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR (b AND c) <=> (a OR b) AND (a OR c); diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc new file mode 100644 index 000000000..70fc5f430 --- /dev/null +++ b/test/regress/regress0/wiki.08.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND (b OR c) <=> (a AND b) OR (a AND c); diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc new file mode 100644 index 000000000..d3118536d --- /dev/null +++ b/test/regress/regress0/wiki.09.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR NOT a; diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc new file mode 100644 index 000000000..41a9bcd3f --- /dev/null +++ b/test/regress/regress0/wiki.10.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND NOT a <=> FALSE; diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc new file mode 100644 index 000000000..e9c0b9cce --- /dev/null +++ b/test/regress/regress0/wiki.11.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR a <=> a; diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc new file mode 100644 index 000000000..d5e7bd776 --- /dev/null +++ b/test/regress/regress0/wiki.12.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND a <=> a; diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc new file mode 100644 index 000000000..2674ba47b --- /dev/null +++ b/test/regress/regress0/wiki.13.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR FALSE <=> a; diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc new file mode 100644 index 000000000..378b84dcd --- /dev/null +++ b/test/regress/regress0/wiki.14.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND TRUE <=> a; diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc new file mode 100644 index 000000000..ca51c4632 --- /dev/null +++ b/test/regress/regress0/wiki.15.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR TRUE <=> TRUE; diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc new file mode 100644 index 000000000..af47433f8 --- /dev/null +++ b/test/regress/regress0/wiki.16.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND FALSE <=> FALSE; diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc new file mode 100644 index 000000000..dc7e7a1c3 --- /dev/null +++ b/test/regress/regress0/wiki.17.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY NOT FALSE <=> TRUE; diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc new file mode 100644 index 000000000..21a87f4b5 --- /dev/null +++ b/test/regress/regress0/wiki.18.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY NOT TRUE <=> FALSE; diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc new file mode 100644 index 000000000..c6081c200 --- /dev/null +++ b/test/regress/regress0/wiki.19.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY NOT (a OR b) <=> NOT a AND NOT b; diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc new file mode 100644 index 000000000..3bec9348b --- /dev/null +++ b/test/regress/regress0/wiki.20.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY NOT (a AND b) <=> NOT a OR NOT b; diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc new file mode 100644 index 000000000..e99ba2d68 --- /dev/null +++ b/test/regress/regress0/wiki.21.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY NOT NOT a <=> a; diff --git a/test/regress/regress0/wiki.cvc b/test/regress/regress0/wiki.cvc deleted file mode 100644 index b5894dbad..000000000 --- a/test/regress/regress0/wiki.cvc +++ /dev/null @@ -1,58 +0,0 @@ -% 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; - - diff --git a/test/regress/run_regression b/test/regress/run_regression index c141cf43a..2be776b3f 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -56,8 +56,8 @@ expfile=`mktemp -t cvc4_expected.XXXXXXXXXX` 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=$? |