From 044329296028ad944b703929fad4d85aa6183472 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Tue, 9 Feb 2010 23:07:33 +0000 Subject: Changes to the CNF conversion and the SAT solver. All regression pass now, and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser. --- src/prop/cnf_stream.h | 146 +++++++++++++++++++++++++++++--------------------- 1 file changed, 84 insertions(+), 62 deletions(-) (limited to 'src/prop/cnf_stream.h') 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 +#include + +namespace __gnu_cxx { +template<> + struct hash { + 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 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 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 */ -- cgit v1.2.3