src/smt/smt_engine.h

   1 /*********************                                                        */
   2 /*! \file smt_engine.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: dejan
   6  ** Minor contributors (to current version): cconway
   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 SmtEngine: the main public entry point of libcvc4.
  15  **
  16  ** SmtEngine: the main public entry point of libcvc4.
  17  **/
  18
  19 #include "cvc4_public.h"
  20
  21 #ifndef __CVC4__SMT_ENGINE_H
  22 #define __CVC4__SMT_ENGINE_H
  23
  24 #include <vector>
  25
  26 #include "context/cdlist_forward.h"
  27 #include "context/cdmap_forward.h"
  28 #include "context/cdset_forward.h"
  29 #include "expr/expr.h"
  30 #include "expr/expr_manager.h"
  31 #include "smt/bad_option_exception.h"
  32 #include "smt/modal_exception.h"
  33 #include "smt/no_such_function_exception.h"
  34 #include "util/hash.h"
  35 #include "util/options.h"
  36 #include "util/result.h"
  37 #include "util/sexpr.h"
  38 #include "util/stats.h"
  39 #include "proof/proof_manager.h"
  40
  41 // In terms of abstraction, this is below (and provides services to)
  42 // ValidityChecker and above (and requires the services of)
  43 // PropEngine.
  44
  45 namespace CVC4 {
  46
  47
  48 template <bool ref_count> class NodeTemplate;
  49 typedef NodeTemplate<true> Node;
  50 typedef NodeTemplate<false> TNode;
  51 class NodeHashFunction;
  52
  53 class TheoryEngine;
  54
  55 class StatisticsRegistry;
  56
  57 namespace context {
  58   class Context;
  59   class UserContext;
  60 }/* CVC4::context namespace */
  61
  62 namespace prop {
  63   class PropEngine;
  64 }/* CVC4::prop namespace */
  65
  66 namespace smt {
  67   /**
  68    * Representation of a defined function.  We keep these around in
  69    * SmtEngine to permit expanding definitions late (and lazily), to
  70    * support getValue() over defined functions, to support user output
  71    * in terms of defined functions, etc.
  72    */
  73   class DefinedFunction;
  74
  75   class SmtEnginePrivate;
  76 }/* CVC4::smt namespace */
  77
  78 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
  79 // hood): use a type parameter and have check() delegate, or subclass
  80 // SmtEngine and override check()?
  81 //
  82 // Probably better than that is to have a configuration object that
  83 // indicates which passes are desired.  The configuration occurs
  84 // elsewhere (and can even occur at runtime).  A simple "pass manager"
  85 // of sorts determines check()'s behavior.
  86 //
  87 // The CNF conversion can go on in PropEngine.
  88
  89 class CVC4_PUBLIC SmtEngine {
  90
  91   /** The type of our internal map of defined functions */
  92   typedef context::CDMap<Node, smt::DefinedFunction, NodeHashFunction>
  93     DefinedFunctionMap;
  94   /** The type of our internal assertion list */
  95   typedef context::CDList<Expr> AssertionList;
  96   /** The type of our internal assignment set */
  97   typedef context::CDSet<Node, NodeHashFunction> AssignmentSet;
  98
  99   /** Expr manager context */
 100   context::Context* d_context;
 101
 102   /** The context levels of user pushes */
 103   std::vector<int> d_userLevels;
 104   /** User level context */
 105   context::UserContext* d_userContext;
 106
 107   /** Our expression manager */
 108   ExprManager* d_exprManager;
 109   /** Our internal expression/node manager */
 110   NodeManager* d_nodeManager;
 111   /** The decision engine */
 112   TheoryEngine* d_theoryEngine;
 113   /** The propositional engine */
 114   prop::PropEngine* d_propEngine;
 115   /** An index of our defined functions */
 116   DefinedFunctionMap* d_definedFunctions;
 117   /**
 118    * The assertion list (before any conversion) for supporting
 119    * getAssertions().  Only maintained if in interactive mode.
 120    */
 121   AssertionList* d_assertionList;
 122
 123   /**
 124    * List of items for which to retrieve values using getAssignment().
 125    */
 126   AssignmentSet* d_assignments;
 127
 128   /**
 129    * The logic we're in.
 130    */
 131   std::string d_logic;
 132
 133   /**
 134    * Whether or not we have added any assertions/declarations/definitions
 135    * since the last checkSat/query (and therefore we're not responsible
 136    * for an assignment).
 137    */
 138   bool d_problemExtended;
 139
 140   /**
 141    * Whether or not a query() or checkSat() has already been made through
 142    * this SmtEngine.  If true, and incrementalSolving is false, then
 143    * attempting an additional query() or checkSat() will fail with a
 144    * ModalException.
 145    */
 146   bool d_queryMade;
 147
 148   /** A user-imposed cumulative time budget, in milliseconds.  0 = no limit. */
 149   unsigned long d_timeBudgetCumulative;
 150   /** A user-imposed per-call time budget, in milliseconds.  0 = no limit. */
 151   unsigned long d_timeBudgetPerCall;
 152   /** A user-imposed cumulative resource budget.  0 = no limit. */
 153   unsigned long d_resourceBudgetCumulative;
 154   /** A user-imposed per-call resource budget.  0 = no limit. */
 155   unsigned long d_resourceBudgetPerCall;
 156
 157   /** The number of milliseconds used by this SmtEngine since its inception. */
 158   unsigned long d_cumulativeTimeUsed;
 159   /** The amount of resource used by this SmtEngine since its inception. */
 160   unsigned long d_cumulativeResourceUsed;
 161
 162   /**
 163    * Most recent result of last checkSat/query or (set-info :status).
 164    */
 165   Result d_status;
 166
 167   /**
 168    * A private utility class to SmtEngine.
 169    */
 170   smt::SmtEnginePrivate* d_private;
 171
 172   /**
 173    * This is called by the destructor, just before destroying the
 174    * PropEngine, TheoryEngine, and DecisionEngine (in that order).  It
 175    * is important because there are destruction ordering issues
 176    * between PropEngine and Theory.
 177    */
 178   void shutdown();
 179
 180   /**
 181    * Full check of consistency in current context.  Returns true iff
 182    * consistent.
 183    */
 184   Result check();
 185
 186   /**
 187    * Quick check of consistency in current context: calls
 188    * processAssertionList() then look for inconsistency (based only on
 189    * that).
 190    */
 191   Result quickCheck();
 192
 193   /**
 194    * Fully type-check the argument, and also type-check that it's
 195    * actually Boolean.
 196    */
 197   void ensureBoolean(const BoolExpr& e);
 198
 199   void internalPush();
 200
 201   void internalPop();
 202
 203   friend class ::CVC4::smt::SmtEnginePrivate;
 204
 205   // === STATISTICS ===
 206   /** time spent in definition-expansion */
 207   TimerStat d_definitionExpansionTime;
 208   /** time spent in non-clausal simplification */
 209   TimerStat d_nonclausalSimplificationTime;
 210   /** time spent in static learning */
 211   TimerStat d_staticLearningTime;
 212
 213 public:
 214
 215   /**
 216    * Construct an SmtEngine with the given expression manager.
 217    */
 218   SmtEngine(ExprManager* em) throw(AssertionException);
 219
 220   /**
 221    * Destruct the SMT engine.
 222    */
 223   ~SmtEngine();
 224
 225   /**
 226    * Set the logic of the script.
 227    */
 228   void setLogic(const std::string& logic) throw(ModalException);
 229
 230   /**
 231    * Set information about the script executing.
 232    */
 233   void setInfo(const std::string& key, const SExpr& value)
 234     throw(BadOptionException, ModalException);
 235
 236   /**
 237    * Query information about the SMT environment.
 238    */
 239   SExpr getInfo(const std::string& key) const
 240     throw(BadOptionException);
 241
 242   /**
 243    * Set an aspect of the current SMT execution environment.
 244    */
 245   void setOption(const std::string& key, const SExpr& value)
 246     throw(BadOptionException, ModalException);
 247
 248   /**
 249    * Get an aspect of the current SMT execution environment.
 250    */
 251   SExpr getOption(const std::string& key) const
 252     throw(BadOptionException);
 253
 254   /**
 255    * Add a formula to the current context: preprocess, do per-theory
 256    * setup, use processAssertionList(), asserting to T-solver for
 257    * literals and conjunction of literals.  Returns false iff
 258    * inconsistent.
 259    */
 260   void defineFunction(Expr func,
 261                       const std::vector<Expr>& formals,
 262                       Expr formula);
 263
 264   /**
 265    * Add a formula to the current context: preprocess, do per-theory
 266    * setup, use processAssertionList(), asserting to T-solver for
 267    * literals and conjunction of literals.  Returns false iff
 268    * inconsistent.
 269    */
 270   Result assertFormula(const BoolExpr& e);
 271
 272   /**
 273    * Check validity of an expression with respect to the current set
 274    * of assertions by asserting the query expression's negation and
 275    * calling check().  Returns valid, invalid, or unknown result.
 276    */
 277   Result query(const BoolExpr& e);
 278
 279   /**
 280    * Assert a formula (if provided) to the current context and call
 281    * check().  Returns sat, unsat, or unknown result.
 282    */
 283   Result checkSat(const BoolExpr& e = BoolExpr());
 284
 285   /**
 286    * Simplify a formula without doing "much" work.  Does not involve
 287    * the SAT Engine in the simplification, but uses the current
 288    * assertions and the current partial model, if one has been
 289    * constructed.
 290    *
 291    * @todo (design) is this meant to give an equivalent or an
 292    * equisatisfiable formula?
 293    */
 294   Expr simplify(const Expr& e);
 295
 296   /**
 297    * Get the assigned value of an expr (only if immediately preceded
 298    * by a SAT or INVALID query).  Only permitted if the SmtEngine is
 299    * set to operate interactively and produce-models is on.
 300    */
 301   Expr getValue(const Expr& e) throw(ModalException, AssertionException);
 302
 303   /**
 304    * Add a function to the set of expressions whose value is to be
 305    * later returned by a call to getAssignment().  The expression
 306    * should be a Boolean zero-ary defined function or a Boolean
 307    * variable.  Rather than throwing a ModalException on modal
 308    * failures (not in interactive mode or not producing assignments),
 309    * this function returns true if the expression was added and false
 310    * if this request was ignored.
 311    */
 312   bool addToAssignment(const Expr& e) throw(AssertionException);
 313
 314   /**
 315    * Get the assignment (only if immediately preceded by a SAT or
 316    * INVALID query).  Only permitted if the SmtEngine is set to
 317    * operate interactively and produce-assignments is on.
 318    */
 319   SExpr getAssignment() throw(ModalException, AssertionException);
 320
 321   /**
 322    * Get the current set of assertions.  Only permitted if the
 323    * SmtEngine is set to operate interactively.
 324    */
 325   std::vector<Expr> getAssertions() throw(ModalException, AssertionException);
 326
 327   /**
 328    * Get the current context level.
 329    */
 330   size_t getStackLevel() const;
 331
 332   /**
 333    * Push a user-level context.
 334    */
 335   void push();
 336
 337   /**
 338    * Pop a user-level context.  Throws an exception if nothing to pop.
 339    */
 340   void pop();
 341
 342   /**
 343    * Interrupt a running query.  This can be called from another thread
 344    * or from a signal handler.  Throws a ModalException if the SmtEngine
 345    * isn't currently in a query.
 346    */
 347   void interrupt() throw(ModalException);
 348
 349   /**
 350    * Set a resource limit for SmtEngine operations.  This is like a time
 351    * limit, but it's deterministic so that reproducible results can be
 352    * obtained.  However, please note that it may not be deterministic
 353    * between different versions of CVC4, or even the same version on
 354    * different platforms.
 355    *
 356    * A cumulative and non-cumulative (per-call) resource limit can be
 357    * set at the same time.  A call to setResourceLimit() with
 358    * cumulative==true replaces any cumulative resource limit currently
 359    * in effect; a call with cumulative==false replaces any per-call
 360    * resource limit currently in effect.  Time limits can be set in
 361    * addition to resource limits; the SmtEngine obeys both.  That means
 362    * that up to four independent limits can control the SmtEngine
 363    * at the same time.
 364    *
 365    * When an SmtEngine is first created, it has no time or resource
 366    * limits.
 367    *
 368    * Currently, these limits only cause the SmtEngine to stop what its
 369    * doing when the limit expires (or very shortly thereafter); no
 370    * heuristics are altered by the limits or the threat of them expiring.
 371    * We reserve the right to change this in the future.
 372    *
 373    * @param units the resource limit, or 0 for no limit
 374    * @param cumulative whether this resource limit is to be a cumulative
 375    * resource limit for all remaining calls into the SmtEngine (true), or
 376    * whether it's a per-call resource limit (false); the default is false
 377    */
 378   void setResourceLimit(unsigned long units, bool cumulative = false);
 379
 380   /**
 381    * Set a time limit for SmtEngine operations.
 382    *
 383    * A cumulative and non-cumulative (per-call) time limit can be
 384    * set at the same time.  A call to setTimeLimit() with
 385    * cumulative==true replaces any cumulative time limit currently
 386    * in effect; a call with cumulative==false replaces any per-call
 387    * time limit currently in effect.  Resource limits can be set in
 388    * addition to time limits; the SmtEngine obeys both.  That means
 389    * that up to four independent limits can control the SmtEngine
 390    * at the same time.
 391    *
 392    * Note that the cumulative timer only ticks away when one of the
 393    * SmtEngine's workhorse functions (things like assertFormula(),
 394    * query(), checkSat(), and simplify()) are running.  Between calls,
 395    * the timer is still.
 396    *
 397    * When an SmtEngine is first created, it has no time or resource
 398    * limits.
 399    *
 400    * Currently, these limits only cause the SmtEngine to stop what its
 401    * doing when the limit expires (or very shortly thereafter); no
 402    * heuristics are altered by the limits or the threat of them expiring.
 403    * We reserve the right to change this in the future.
 404    *
 405    * @param millis the time limit in milliseconds, or 0 for no limit
 406    * @param cumulative whether this time limit is to be a cumulative
 407    * time limit for all remaining calls into the SmtEngine (true), or
 408    * whether it's a per-call time limit (false); the default is false
 409    */
 410   void setTimeLimit(unsigned long millis, bool cumulative = false);
 411
 412   /**
 413    * Get the current resource usage count for this SmtEngine.  This
 414    * function can be used to ascertain reasonable values to pass as
 415    * resource limits to setResourceLimit().
 416    */
 417   unsigned long getResourceUsage() const;
 418
 419   /**
 420    * Get the current millisecond count for this SmtEngine.
 421    */
 422   unsigned long getTimeUsage() const;
 423
 424   /**
 425    * Get the remaining resources that can be consumed by this SmtEngine
 426    * according to the currently-set cumulative resource limit.  If there
 427    * is not a cumulative resource limit set, this function throws a
 428    * ModalException.
 429    */
 430   unsigned long getResourceRemaining() const throw(ModalException);
 431
 432   /**
 433    * Get the remaining number of milliseconds that can be consumed by
 434    * this SmtEngine according to the currently-set cumulative time limit.
 435    * If there is not a cumulative resource limit set, this function
 436    * throws a ModalException.
 437    */
 438   unsigned long getTimeRemaining() const throw(ModalException);
 439
 440   /**
 441    * Permit access to the underlying StatisticsRegistry.
 442    */
 443   StatisticsRegistry* getStatisticsRegistry() const;
 444
 445 };/* class SmtEngine */
 446
 447 }/* CVC4 namespace */
 448
 449 #endif /* __CVC4__SMT_ENGINE_H */