1 files changed, 179 insertions, 0 deletions
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
new file mode 100644
index 000000000..c09994c06
--- /dev/null
+++ b/src/theory/bv/bv_quick_check.h
@@ -0,0 +1,179 @@
+/*********************                                                        */
+/*! \file bv_quick_check.h
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sandboxed sat solver for bv quickchecks.
+ **
+ ** Sandboxed sat solver for bv quickchecks.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BV_QUICK_CHECK_H
+#define __CVC4__BV_QUICK_CHECK_H
+
+#include <vector>
+#include <ext/hash_map>
+
+#include "expr/node.h"
+#include "context/cdo.h"
+#include "prop/sat_solver_types.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+
+class TheoryModel;
+
+namespace bv {
+
+
+
+typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+
+class TLazyBitblaster; 
+class TheoryBV;
+
+class BVQuickCheck {
+  context::Context* d_ctx;
+  TLazyBitblaster* d_bitblaster;
+  Node d_conflict;
+  context::CDO<bool> d_inConflict;
+  void setConflict();
+
+public:
+  BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv);
+  ~BVQuickCheck();
+  bool inConflict();
+  Node getConflict() { return d_conflict; }
+  /** 
+   * Checks the satisfiability for a given set of assumptions.
+   * 
+   * @param assumptions literals assumed true
+   * @param budget max number of conflicts
+   * 
+   * @return 
+   */
+  prop::SatValue checkSat(std::vector<Node>& assumptions, unsigned long budget);
+  /** 
+   * Checks the satisfiability of given assertions.
+   * 
+   * @param budget max number of conflicts
+   * 
+   * @return 
+   */
+  prop::SatValue checkSat(unsigned long budget);
+  
+  /** 
+   * Convert to CNF and assert the given literal.
+   * 
+   * @param assumption bv literal
+   * 
+   * @return false if a conflict has been found via bcp.
+   */
+  bool addAssertion(TNode assumption);
+
+  void push();
+  void pop();
+  void popToZero();
+  /** 
+   * Deletes the SAT solver and CNF stream, but maintains the
+   * bit-blasting term cache. 
+   * 
+   */
+  void clearSolver(); 
+
+  /** 
+   * Computes the size of the circuit required to bit-blast
+   * atom, by not recounting the nodes in seen. 
+   * 
+   * @param node 
+   * @param seen 
+   * 
+   * @return 
+   */
+  uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
+  void collectModelInfo(theory::TheoryModel* model, bool fullModel); 
+
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
+  vars_iterator beginVars(); 
+  vars_iterator endVars(); 
+
+  Node getVarValue(TNode var); 
+
+};
+
+
+class QuickXPlain {
+  struct Statistics {
+    TimerStat d_xplainTime;
+    IntStat d_numSolved;
+    IntStat d_numUnknown;
+    IntStat d_numUnknownWasUnsat;
+    IntStat d_numConflictsMinimized;
+    IntStat d_finalPeriod;
+    AverageStat d_avgMinimizationRatio;
+    Statistics(const std::string&);
+    ~Statistics();
+  };
+  BVQuickCheck* d_solver;
+  unsigned long d_budget;
+
+  // crazy heuristic variables
+  unsigned d_numCalled; // number of times called
+  double d_minRatioSum; // sum of minimization ratio for computing average min ratio  
+  unsigned d_numConflicts; // number of conflicts (including when minimization not applied)
+  unsigned d_period; // after how many conflicts to try minimizing again
+
+  double d_thresh; // if minimization ratio is less, increase period
+  double d_hardThresh; // decrease period if minimization ratio is greater than this
+  
+  
+  Statistics d_statistics;
+  /** 
+   * Uses solve with assumptions unsat core feature to
+   * further minimize a conflict. The minimized conflict
+   * will be between low and the returned value in conflict.
+   * 
+   * @param low 
+   * @param high 
+   * @param conflict 
+   * 
+   * @return 
+   */
+  unsigned selectUnsatCore(unsigned low, unsigned high,
+                           std::vector<TNode>& conflict);
+  /** 
+   * Internal conflict  minimization, attempts to minimize
+   * literals in conflict between low and high and adds the
+   * result in new_conflict. 
+   * 
+   * @param low 
+   * @param high 
+   * @param conflict 
+   * @param new_conflict 
+   */
+  void minimizeConflictInternal(unsigned low, unsigned high,
+                                std::vector<TNode>& conflict,
+                                std::vector<TNode>& new_conflict);
+
+  bool useHeuristic();
+public:
+  QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budged = 10000);
+  ~QuickXPlain();
+  Node minimizeConflict(TNode conflict); 
+};
+
+} /* bv namespace */
+} /* theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__BV_QUICK_CHECK_H */