1 files changed, 144 insertions, 0 deletions
diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h
new file mode 100644
index 000000000..9844cd982
--- /dev/null
+++ b/src/theory/bv/bv_sat.h
@@ -0,0 +1,144 @@
+/*********************                                                        */
+/*! \file bv_sat.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 Wrapper around the SAT solver used for bitblasting
+ **
+ ** Wrapper around the SAT solver used for bitblasting.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BV__SAT_H
+#define __CVC4__BV__SAT_H
+
+
+#include "expr/node.h"
+#include <vector>
+#include <list>
+#include <iostream>
+#include <math.h>
+#include <ext/hash_map>
+
+#include "context/cdo.h"
+#include "context/cdset.h"
+#include "context/cdlist.h"
+
+#include "theory_bv_utils.h"
+#include "util/stats.h"
+#include "bitblast_strategies.h"
+
+#include "prop/sat_module.h"
+
+namespace CVC4 {
+
+// forward declarations
+namespace prop {
+class CnfStream;
+class BVSatSolverInterface;
+}
+
+
+namespace theory {
+namespace bv {
+
+
+std::string toString (Bits& bits); 
+
+/** 
+ * The Bitblaster that manages the mapping between Nodes 
+ * and their bitwise definition 
+ * 
+ */
+
+typedef std::vector<Node> Bits; 
+
+class Bitblaster {
+  
+  typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction >              TermDefMap;
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      AtomSet; 
+  
+  typedef void   (*TermBBStrategy) (TNode, Bits&, Bitblaster*); 
+  typedef Node   (*AtomBBStrategy) (TNode, Bitblaster*); 
+
+  // sat solver used for bitblasting and associated CnfStream
+  prop::BVSatSolverInterface*        d_satSolver; 
+  prop::CnfStream*                   d_cnfStream;
+
+  // caches and mappings
+  TermDefMap                   d_termCache;
+  AtomSet                      d_bitblastedAtoms;
+  
+  context::CDList<prop::SatLiteral>  d_assertedAtoms; /**< context dependent list storing the atoms
+                                              currently asserted by the DPLL SAT solver. */
+
+  /// helper methods
+  bool          hasBBAtom(TNode node);    
+  bool          hasBBTerm(TNode node); 
+  void          getBBTerm(TNode node, Bits& bits);
+
+
+
+
+  /// function tables for the various bitblasting strategies indexed by node kind
+  TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
+  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; 
+
+  // helper methods to initialize function tables
+  void initAtomBBStrategies();
+  void initTermBBStrategies(); 
+
+  
+  void bbAtom(TNode node);
+  // division is bitblasted in terms of constraints
+  // so it needs to use private bitblaster interface
+  void bbUdiv(TNode node, Bits& bits);
+  void bbUrem(TNode node, Bits& bits); 
+public:
+  void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division
+  void bbTerm(TNode node, Bits&  bits);
+  
+public:
+  Bitblaster(context::Context* c); 
+  ~Bitblaster() {
+    delete d_cnfStream;
+    delete d_satSolver; 
+  }
+  
+  void assertToSat(TNode node);
+  bool solve();
+  void bitblast(TNode node);
+  void getConflict(std::vector<TNode>& conflict); 
+
+private:
+
+  
+  class Statistics {
+  public:
+    IntStat  d_numTermClauses, d_numAtomClauses;
+    TimerStat d_bitblastTimer;
+    Statistics();
+    ~Statistics(); 
+  }; 
+  
+  Statistics d_statistics;
+};
+
+
+
+} /* bv namespace */ 
+
+} /* theory namespace */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__BV__SAT_H */