src/theory/bv/bv_quick_check.h

   1 /*********************                                                        */
   2 /*! \file bv_quick_check.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Tim King, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Sandboxed sat solver for bv quickchecks.
  13  **
  14  ** Sandboxed sat solver for bv quickchecks.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__BV_QUICK_CHECK_H
  20 #define __CVC4__BV_QUICK_CHECK_H
  21
  22 #include <vector>
  23 #include <ext/hash_map>
  24
  25 #include "context/cdo.h"
  26 #include "expr/node.h"
  27 #include "prop/sat_solver_types.h"
  28 #include "theory/bv/theory_bv_utils.h"
  29 #include "util/statistics_registry.h"
  30
  31 namespace CVC4 {
  32 namespace theory {
  33
  34 class TheoryModel;
  35
  36 namespace bv {
  37
  38 class TLazyBitblaster;
  39 class TheoryBV;
  40
  41 class BVQuickCheck {
  42   context::Context d_ctx;
  43   TLazyBitblaster* d_bitblaster;
  44   Node d_conflict;
  45   context::CDO<bool> d_inConflict;
  46   void setConflict();
  47
  48 public:
  49   BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv);
  50   ~BVQuickCheck();
  51   bool inConflict();
  52   Node getConflict() { return d_conflict; }
  53   /**
  54    * Checks the satisfiability for a given set of assumptions.
  55    *
  56    * @param assumptions literals assumed true
  57    * @param budget max number of conflicts
  58    *
  59    * @return
  60    */
  61   prop::SatValue checkSat(std::vector<Node>& assumptions, unsigned long budget);
  62   /**
  63    * Checks the satisfiability of given assertions.
  64    *
  65    * @param budget max number of conflicts
  66    *
  67    * @return
  68    */
  69   prop::SatValue checkSat(unsigned long budget);
  70
  71   /**
  72    * Convert to CNF and assert the given literal.
  73    *
  74    * @param assumption bv literal
  75    *
  76    * @return false if a conflict has been found via bcp.
  77    */
  78   bool addAssertion(TNode assumption);
  79
  80   void push();
  81   void pop();
  82   void popToZero();
  83   /**
  84    * Deletes the SAT solver and CNF stream, but maintains the
  85    * bit-blasting term cache.
  86    *
  87    */
  88   void clearSolver();
  89
  90   /**
  91    * Computes the size of the circuit required to bit-blast
  92    * atom, by not recounting the nodes in seen.
  93    *
  94    * @param node
  95    * @param seen
  96    *
  97    * @return
  98    */
  99   uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
 100   void collectModelInfo(theory::TheoryModel* model, bool fullModel);
 101
 102   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
 103   vars_iterator beginVars();
 104   vars_iterator endVars();
 105
 106   Node getVarValue(TNode var, bool fullModel);
 107
 108 };
 109
 110
 111 class QuickXPlain {
 112   struct Statistics {
 113     TimerStat d_xplainTime;
 114     IntStat d_numSolved;
 115     IntStat d_numUnknown;
 116     IntStat d_numUnknownWasUnsat;
 117     IntStat d_numConflictsMinimized;
 118     IntStat d_finalPeriod;
 119     AverageStat d_avgMinimizationRatio;
 120     Statistics(const std::string&);
 121     ~Statistics();
 122   };
 123   BVQuickCheck* d_solver;
 124   unsigned long d_budget;
 125
 126   // crazy heuristic variables
 127   unsigned d_numCalled; // number of times called
 128   double d_minRatioSum; // sum of minimization ratio for computing average min ratio
 129   unsigned d_numConflicts; // number of conflicts (including when minimization not applied)
 130   // unsigned d_period; // after how many conflicts to try minimizing again
 131
 132   // double d_thresh; // if minimization ratio is less, increase period
 133   // double d_hardThresh; // decrease period if minimization ratio is greater than this
 134
 135
 136   Statistics d_statistics;
 137   /**
 138    * Uses solve with assumptions unsat core feature to
 139    * further minimize a conflict. The minimized conflict
 140    * will be between low and the returned value in conflict.
 141    *
 142    * @param low
 143    * @param high
 144    * @param conflict
 145    *
 146    * @return
 147    */
 148   unsigned selectUnsatCore(unsigned low, unsigned high,
 149                            std::vector<TNode>& conflict);
 150   /**
 151    * Internal conflict  minimization, attempts to minimize
 152    * literals in conflict between low and high and adds the
 153    * result in new_conflict.
 154    *
 155    * @param low
 156    * @param high
 157    * @param conflict
 158    * @param new_conflict
 159    */
 160   void minimizeConflictInternal(unsigned low, unsigned high,
 161                                 std::vector<TNode>& conflict,
 162                                 std::vector<TNode>& new_conflict);
 163
 164   bool useHeuristic();
 165 public:
 166   QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budged = 10000);
 167   ~QuickXPlain();
 168   Node minimizeConflict(TNode conflict);
 169 };
 170
 171 } /* bv namespace */
 172 } /* theory namespace */
 173 } /* CVC4 namespace */
 174
 175 #endif /* __CVC4__BV_QUICK_CHECK_H */