diff options
author | Tim King <taking@cs.nyu.edu> | 2010-02-02 20:56:47 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-02-02 20:56:47 +0000 |
commit | a8588cb23c5257bb11a70348346476b55317faa3 (patch) | |
tree | 34bead7e2b760d813ee02d04a9dec091eedbc745 /src/prop/cnf_stream.h | |
parent | 86716e3782aae62a38987f7f89bdf5498eca534a (diff) |
Switched cnf conversion to go through CnfStream.
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 165 |
1 files changed, 165 insertions, 0 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h new file mode 100644 index 000000000..c0a70730a --- /dev/null +++ b/src/prop/cnf_stream.h @@ -0,0 +1,165 @@ +/********************* -*- C++ -*- */ +/** cnf_stream.h + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** This class takes a sequence of formulas. + ** It outputs a stream of clauses that is propositional + ** equisatisfiable with the conjunction of the formulas. + ** This stream is maintained in an online fashion. + ** + ** Unlike other parts of the system it is aware of the PropEngine's + ** internals such as the representation and translation of + **/ + + +#ifndef __CVC4__CNF_STREAM_H +#define __CVC4__CNF_STREAM_H + +//TODO: Why am i including this? Who knows... +#include "cvc4_config.h" + +#include "expr/node.h" +#include "prop/minisat/simp/SimpSolver.h" +#include "prop/minisat/core/SolverTypes.h" +#include "prop/prop_engine.h" + +#include <map> + +namespace CVC4 { + class PropEngine; +} + + +namespace CVC4 { +namespace prop { + +class CnfStream { + +private: + /** + * d_propEngine is the PropEngine that the CnfStream interacts with directly through + * the follwoing functions: + * - insertClauseIntoStream + * - acquireFreshLit + * - registerMapping + */ + PropEngine *d_propEngine; + + /**Cache of what literal have been registered to a node. + *Not strictly needed for correctness. + *This can be flushed when memory is under pressure. + */ + std::map<Node,minisat::Lit> d_translationCache; + +protected: + + /** + * Uniform interface for sending a clause back to d_propEngine. + * May want to have internal datastructures later on + */ + void insertClauseIntoStream(minisat::vec<minisat::Lit> & c); + void insertClauseIntoStream(minisat::Lit a); + void insertClauseIntoStream(minisat::Lit a,minisat::Lit b); + void insertClauseIntoStream(minisat::Lit a,minisat::Lit b, minisat::Lit c); + + + //utilities for the translation cache; + bool isCached(const Node & n) const; + minisat::Lit lookupInCache(const Node & n) const; + + /** + * Empties the internal translation cache. + */ + void flushCache(); + + //negotiates the mapping of atoms to literals with PropEngine + void registerMapping(const Node & node, minisat::Lit lit, bool atom = false); + minisat::Lit acquireFreshLit(const Node & n); + minisat::Lit aquireAndRegister(const Node & n, bool atom = false); + +public: + /** + * Constructs a CnfStream that sends constructs an equisatisfiable set of clauses + * and sends them to pe. + */ + CnfStream(CVC4::PropEngine *pe); + + + /** + * Converts and asserts a formula. + * @param n node to convert and assert + */ + virtual void convertAndAssert(const Node & n) = 0; + +}; /* class CnfStream */ + + +/** + * TseitinCnfStream is based on the following recursive algorithm + * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf + * The general gist of the algorithm is to introduce a new literal that + * will be equivalent to each subexpression in the constructed equisatisfiable formula + * then subsistute the new literal for the formula, and to do this recursively. + * + * This implementation does this in a single recursive pass. + */ +class TseitinCnfStream : public CnfStream { + +public: + void convertAndAssert(const Node & n); + TseitinCnfStream(CVC4::PropEngine *pe); + +private: + + /* Each of these formulas handles takes care of a Node of each Kind. + * + * Each handleX(Node &n) is responsibile for: + * - constructing a new literal, l (if nessecary) + * - calling registerNode(n,l) + * - adding clauses asure that l is equivalent to the Node + * - calling recTransform on its children (if nessecary) + * - returning l + * + * handleX( n ) can assume that n is not in d_translationCache + */ + minisat::Lit handleAtom(const Node & n); + minisat::Lit handleNot(const Node & n); + minisat::Lit handleXor(const Node & n); + minisat::Lit handleImplies(const Node & n); + minisat::Lit handleIff(const Node & n); + minisat::Lit handleIte(const Node & n); + + minisat::Lit handleAnd(const Node& n); + minisat::Lit handleOr(const Node& n); + + + /** + *Maps recTransform over the children of a node. + *This is very useful for n-ary Kinds (OR, AND). + * + *Non n-ary kinds (IMPLIES) should avoid using this as it requires a + *tiny bit of extra overhead, and it leads to less readable code. + * + * precondition: target.size() == n.getNumChildren() + */ + void mapRecTransformOverChildren(const Node& n, minisat::vec<minisat::Lit> & target); + + //Recurisively dispatches the various Kinds to the appropriate handler. + minisat::Lit recTransform(const Node & n); + +}; /* class TseitinCnfStream */ + +}/* prop namespace */ +}/* CVC4 namespace */ + + + +#endif /* __CVC4__CNF_STREAM_H */ |