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