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
  

1 files changed, 112 insertions, 0 deletions

diff --git a/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h
new file mode 100644
index 000000000..504755e6c
--- /dev/null
+++ b/src/theory/bv/bitblast_strategies.h
@@ -0,0 +1,112 @@
+/*********************                                                        */
+/*! \file bitblast_strategies.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief Implementation of bitblasting functions for various operators. 
+ **
+ ** Implementation of bitblasting functions for various operators. 
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BITBLAST__STRATEGIES_H
+#define __CVC4__BITBLAST__STRATEGIES_H
+
+
+#include "expr/node.h"
+#include "prop/sat_module.h"
+
+namespace CVC4 {
+
+
+namespace theory {
+namespace bv {
+
+class Bitblaster;
+
+
+typedef std::vector<Node>    Bits; 
+
+
+/** 
+ * Default Atom Bitblasting strategies: 
+ * 
+ * @param node the atom to be bitblasted
+ * @param markerLit the marker literal corresponding to the atom
+ * @param bb the bitblaster
+ */
+
+Node UndefinedAtomBBStrategy (TNode node, Bitblaster* bb);                               
+Node DefaultEqBB(TNode node, Bitblaster* bb);
+
+Node DefaultUltBB(TNode node, Bitblaster* bb);
+Node DefaultUleBB(TNode node, Bitblaster* bb);
+Node DefaultUgtBB(TNode node, Bitblaster* bb);
+Node DefaultUgeBB(TNode node, Bitblaster* bb);
+
+Node DefaultSltBB(TNode node, Bitblaster* bb);
+Node DefaultSleBB(TNode node, Bitblaster* bb);
+Node DefaultSgtBB(TNode node, Bitblaster* bb);
+Node DefaultSgeBB(TNode node, Bitblaster* bb);
+
+/// other modes
+Node AdderUltBB(TNode node, Bitblaster* bb);
+
+
+
+/** 
+ * Default Term Bitblasting strategies
+ * 
+ * @param node the term to be bitblasted
+ * @param bb the bitblaster in which the clauses are added
+ * 
+ * @return the bits representing the new term 
+ */
+
+void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb); 
+
+void DefaultVarBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultConstBB       (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultNotBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultConcatBB      (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultAndBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultOrBB          (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultXorBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultXnorBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultNandBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultNorBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultCompBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultMultBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultPlusBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultSubBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultNegBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultUdivBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultUremBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultSdivBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultSremBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultSmodBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultShlBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultLshrBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultAshrBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultExtractBB     (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultRepeatBB      (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultZeroExtendBB  (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultSignExtendBB  (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultRotateRightBB (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultRotateLeftBB  (TNode node, Bits& bits, Bitblaster* bb);
+
+
+}
+}
+}
+
+#endif