src/prop/prop_engine.h

   1 /*********************                                                        */
   2 /*! \file prop_engine.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: taking, dejan
   6  ** Minor contributors (to current version): cconway, barrett, kshitij
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief The PropEngine (propositional engine); main interface point
  15  ** between CVC4's SMT infrastructure and the SAT solver
  16  **
  17  ** The PropEngine (propositional engine); main interface point
  18  ** between CVC4's SMT infrastructure and the SAT solver.
  19  **/
  20
  21 #include "cvc4_private.h"
  22
  23 #ifndef __CVC4__PROP_ENGINE_H
  24 #define __CVC4__PROP_ENGINE_H
  25
  26 #include "expr/node.h"
  27 #include "util/options.h"
  28 #include "util/result.h"
  29 #include "smt/modal_exception.h"
  30 #include <sys/time.h>
  31
  32 namespace CVC4 {
  33
  34 class DecisionEngine;
  35 class TheoryEngine;
  36
  37 namespace prop {
  38
  39 class CnfStream;
  40 class DPLLSatSolverInterface;
  41
  42 class PropEngine;
  43
  44 /**
  45  * A helper class to keep track of a time budget and signal
  46  * the PropEngine when the budget expires.
  47  */
  48 class SatTimer {
  49
  50   PropEngine& d_propEngine;
  51   unsigned long d_ms;
  52   timeval d_limit;
  53
  54 public:
  55
  56   /** Construct a SatTimer attached to the given PropEngine. */
  57   SatTimer(PropEngine& propEngine) :
  58     d_propEngine(propEngine),
  59     d_ms(0) {
  60   }
  61
  62   /** Is the timer currently active? */
  63   bool on() const {
  64     return d_ms != 0;
  65   }
  66
  67   /** Set a millisecond timer (0==off). */
  68   void set(unsigned long millis) {
  69     d_ms = millis;
  70     // keep track of when it was set, even if it's disabled (i.e. == 0)
  71     Trace("limit") << "SatTimer::set(" << d_ms << ")" << std::endl;
  72     gettimeofday(&d_limit, NULL);
  73     Trace("limit") << "SatTimer::set(): it's " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
  74     d_limit.tv_sec += millis / 1000;
  75     d_limit.tv_usec += (millis % 1000) * 1000;
  76     if(d_limit.tv_usec > 1000000) {
  77       ++d_limit.tv_sec;
  78       d_limit.tv_usec -= 1000000;
  79     }
  80     Trace("limit") << "SatTimer::set(): limit is at " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
  81   }
  82
  83   /** Return the milliseconds elapsed since last set(). */
  84   unsigned long elapsed() {
  85     timeval tv;
  86     gettimeofday(&tv, NULL);
  87     Trace("limit") << "SatTimer::elapsed(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl;
  88     tv.tv_sec -= d_limit.tv_sec - d_ms / 1000;
  89     tv.tv_usec -= d_limit.tv_usec - (d_ms % 1000) * 1000;
  90     Trace("limit") << "SatTimer::elapsed(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
  91     return tv.tv_sec * 1000 + tv.tv_usec / 1000;
  92   }
  93
  94   bool expired() {
  95     if(on()) {
  96       timeval tv;
  97       gettimeofday(&tv, NULL);
  98       Trace("limit") << "SatTimer::expired(): current time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
  99       Trace("limit") << "SatTimer::expired(): limit time is " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
 100       if(d_limit.tv_sec < tv.tv_sec ||
 101          (d_limit.tv_sec == tv.tv_sec && d_limit.tv_usec <= tv.tv_usec)) {
 102         Trace("limit") << "SatTimer::expired(): OVER LIMIT!" << std::endl;
 103         return true;
 104       } else {
 105         Trace("limit") << "SatTimer::expired(): within limit" << std::endl;
 106       }
 107     }
 108     return false;
 109   }
 110
 111   /** Check the current time and signal the PropEngine if over-time. */
 112   void check();
 113
 114 };/* class SatTimer */
 115
 116 /**
 117  * PropEngine is the abstraction of a Sat Solver, providing methods for
 118  * solving the SAT problem and conversion to CNF (via the CnfStream).
 119  */
 120 class PropEngine {
 121
 122   /**
 123    * Indicates that the SAT solver is currently solving something and we should
 124    * not mess with it's internal state.
 125    */
 126   bool d_inCheckSat;
 127
 128   /** The theory engine we will be using */
 129   TheoryEngine *d_theoryEngine;
 130
 131   /** The decision engine we will be using */
 132   DecisionEngine *d_decisionEngine;
 133
 134   /** The context */
 135   context::Context* d_context;
 136
 137   /** The SAT solver proxy */
 138   DPLLSatSolverInterface* d_satSolver;
 139
 140   /** List of all of the assertions that need to be made */
 141   std::vector<Node> d_assertionList;
 142
 143   /** The CNF converter in use */
 144   CnfStream* d_cnfStream;
 145
 146   /** A timer for SAT calls */
 147   SatTimer d_satTimer;
 148
 149   /** Whether we were just interrupted (or not) */
 150   bool d_interrupted;
 151
 152   /** Dump out the satisfying assignment (after SAT result) */
 153   void printSatisfyingAssignment();
 154
 155 public:
 156
 157   /**
 158    * Create a PropEngine with a particular decision and theory engine.
 159    */
 160   PropEngine(TheoryEngine*, DecisionEngine*, context::Context*);
 161
 162   /**
 163    * Destructor.
 164    */
 165   CVC4_PUBLIC ~PropEngine();
 166
 167   /**
 168    * This is called by SmtEngine, at shutdown time, just before
 169    * destruction.  It is important because there are destruction
 170    * ordering issues between some parts of the system (notably between
 171    * PropEngine and Theory).  For now, there's nothing to do here in
 172    * the PropEngine.
 173    */
 174   void shutdown() { }
 175
 176   /**
 177    * Converts the given formula to CNF and assert the CNF to the SAT solver.
 178    * The formula is asserted permanently for the current context.
 179    * @param node the formula to assert
 180    */
 181   void assertFormula(TNode node);
 182
 183   /**
 184    * Converts the given formula to CNF and assert the CNF to the SAT solver.
 185    * The formula can be removed by the SAT solver after backtracking lower
 186    * than the (SAT and SMT) level at which it was asserted.
 187    *
 188    * @param node the formula to assert
 189    * @param negated whether the node should be considered to be negated
 190    * at the top level (or not)
 191    * @param removable whether this lemma can be quietly removed based
 192    * on an activity heuristic (or not)
 193    */
 194   void assertLemma(TNode node, bool negated, bool removable);
 195
 196   /**
 197    * Checks the current context for satisfiability.
 198    *
 199    * @param millis the time limit for this call in milliseconds
 200    * (0==off); on output, it is set to the milliseconds used
 201    * @param on input, resource the number of resource units permitted
 202    * for this call (0==off); on output, it is set to the resource used
 203    */
 204   Result checkSat(unsigned long& millis, unsigned long& resource);
 205
 206   /**
 207    * Get the value of a boolean variable.
 208    *
 209    * @return mkConst<true>, mkConst<false>, or Node::null() if
 210    * unassigned.
 211    */
 212   Node getValue(TNode node) const;
 213
 214   /**
 215    * Return true if node has an associated SAT literal.
 216    */
 217   bool isSatLiteral(TNode node) const;
 218
 219   /**
 220    * Return true if node has an associated SAT literal that is
 221    * currently translated (i.e., it's relevant to the current
 222    * user push/pop level).
 223    */
 224   bool isTranslatedSatLiteral(TNode node) const;
 225
 226   /**
 227    * Check if the node has a value and return it if yes.
 228    */
 229   bool hasValue(TNode node, bool& value) const;
 230
 231   /**
 232    * Ensure that the given node will have a designated SAT literal
 233    * that is definitionally equal to it.  The result of this function
 234    * is that the Node can be queried via getSatValue().
 235    */
 236   void ensureLiteral(TNode n);
 237
 238   /**
 239    * Push the context level.
 240    */
 241   void push();
 242
 243   /**
 244    * Pop the context level.
 245    */
 246   void pop();
 247
 248   /**
 249    * Return true if we are currently searching (either in this or
 250    * another thread).
 251    */
 252   bool isRunning() const;
 253
 254   /**
 255    * Check the current time budget.
 256    */
 257   void checkTime();
 258
 259   /**
 260    * Interrupt a running solver (cause a timeout).
 261    */
 262   void interrupt() throw(ModalException);
 263
 264   /**
 265    * "Spend" a "resource."  If the sum of these externally-counted
 266    * resources and SAT-internal resources exceed the current limit,
 267    * SAT should terminate.
 268    */
 269   void spendResource() throw();
 270
 271   /**
 272    * For debugging.  Return true if "expl" is a well-formed
 273    * explanation for "node," meaning:
 274    *
 275    * 1. expl is either a SAT literal or an AND of SAT literals
 276    *    currently assigned true;
 277    * 2. node is assigned true;
 278    * 3. node does not appear in expl; and
 279    * 4. node was assigned after all of the literals in expl
 280    */
 281   bool properExplanation(TNode node, TNode expl) const;
 282
 283 };/* class PropEngine */
 284
 285
 286 inline void SatTimer::check() {
 287   if(d_propEngine.isRunning() && expired()) {
 288     Trace("limit") << "SatTimer::check(): interrupt!" << std::endl;
 289     d_propEngine.interrupt();
 290   }
 291 }
 292
 293 inline void PropEngine::checkTime() {
 294   d_satTimer.check();
 295 }
 296
 297 }/* CVC4::prop namespace */
 298 }/* CVC4 namespace */
 299
 300 #endif /* __CVC4__PROP_ENGINE_H */