diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
commit | 7aa55e0d38e73a02b11ad0c5a60196b610674050 (patch) | |
tree | c59def0ed00dcde29a5a6498cf74ac87dc3a2a6f /src/prop/cnf_stream.h | |
parent | d8da6a3644d1cdbe62d44a8eb80068da4d1d2855 (diff) |
Refactored CnfStream to work with the bv theory Bitblaster:
* separated SatSolverInput interface class into two classes:
- TheoryProxy for the sat solver to communicate with the theories
- SatSolverInterface abstract class to communicate with the sat solver
* instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
* added abstract classes for DPLLSatSolver and BVSatSolver different interfaces
Replaced TheoryBV with bitblasting implementation:
* all operators bitblasted
* only operator elimination rewrite rules so far
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 4b16a02b9..c9306952b 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -29,7 +29,7 @@ #include "expr/node.h" #include "prop/sat.h" -#include "theory/registrar.h" +#include "prop/registrar.h" #include <ext/hash_map> @@ -48,7 +48,7 @@ class CnfStream { public: /** Cache of what nodes have been registered to a literal. */ - typedef __gnu_cxx::hash_map<SatLiteral, TNode, SatSolver::SatLiteralHashFunction> NodeCache; + typedef __gnu_cxx::hash_map<SatLiteral, TNode, SatLiteralHashFunction> NodeCache; /** Per node translation information */ struct TranslationInfo { @@ -64,7 +64,7 @@ public: protected: /** The SAT solver we will be using */ - SatInputInterface *d_satSolver; + SatSolverInterface *d_satSolver; TranslationCache d_translationCache; NodeCache d_nodeCache; @@ -77,7 +77,7 @@ protected: const bool d_fullLitToNodeMap; /** The "registrar" for pre-registration of terms */ - theory::Registrar d_registrar; + Registrar* d_registrar; /** Top level nodes that we translated */ std::vector<TNode> d_translationTrail; @@ -98,7 +98,7 @@ protected: * detection," when BIG FORMULA is later asserted, it is clausified * separately, and "lit" is never asserted as a unit clause. */ - KEEP_STATISTIC(IntStat, d_fortunateLiterals, "prop::CnfStream::fortunateLiterals", 0); + //KEEP_STATISTIC(IntStat, d_fortunateLiterals, "prop::CnfStream::fortunateLiterals", 0); /** Remove nots from the node */ TNode stripNot(TNode node) { @@ -189,7 +189,7 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - CnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false); + CnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -289,7 +289,7 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false); + TseitinCnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); private: |