src/smt/smt_engine.h

   1 /*********************                                                        */
   2 /** smt_engine.h
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** SmtEngine: the main public entry point of libcvc4.
  14  **/
  15
  16 #ifndef __CVC4__SMT_ENGINE_H
  17 #define __CVC4__SMT_ENGINE_H
  18
  19 #include <vector>
  20
  21 #include "cvc4_config.h"
  22 #include "expr/expr.h"
  23 #include "expr/expr_manager.h"
  24 #include "util/result.h"
  25 #include "util/model.h"
  26 #include "util/decision_engine.h"
  27
  28 // In terms of abstraction, this is below (and provides services to)
  29 // ValidityChecker and above (and requires the services of)
  30 // PropEngine.
  31
  32 namespace CVC4 {
  33
  34 class Command;
  35 class Options;
  36 class TheoryEngine;
  37
  38 namespace prop {
  39   class PropEngine;
  40 }
  41
  42 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
  43 // hood): use a type parameter and have check() delegate, or subclass
  44 // SmtEngine and override check()?
  45 //
  46 // Probably better than that is to have a configuration object that
  47 // indicates which passes are desired.  The configuration occurs
  48 // elsewhere (and can even occur at runtime).  A simple "pass manager"
  49 // of sorts determines check()'s behavior.
  50 //
  51 // The CNF conversion can go on in PropEngine.
  52
  53 class CVC4_PUBLIC SmtEngine {
  54
  55 public:
  56
  57   /**
  58    * Construct an SmtEngine with the given expression manager and user options.
  59    */
  60   SmtEngine(ExprManager* em, const Options* opts) throw();
  61
  62   /**
  63    * Destruct the SMT engine.
  64    */
  65   ~SmtEngine();
  66
  67   /**
  68    * Execute a command.
  69    */
  70   void doCommand(Command*);
  71
  72   /**
  73    * Add a formula to the current context: preprocess, do per-theory
  74    * setup, use processAssertionList(), asserting to T-solver for
  75    * literals and conjunction of literals.  Returns false iff
  76    * inconsistent.
  77    */
  78   Result assertFormula(const BoolExpr& e);
  79
  80   /**
  81    * Add a formula to the current context and call check().  Returns
  82    * true iff consistent.
  83    */
  84   Result query(const BoolExpr& e);
  85
  86   /**
  87    * Add a formula to the current context and call check().  Returns
  88    * true iff consistent.
  89    */
  90   Result checkSat(const BoolExpr& e);
  91
  92   /**
  93    * Simplify a formula without doing "much" work.  Requires assist
  94    * from the SAT Engine.
  95    */
  96   Expr simplify(const Expr& e);
  97
  98   /**
  99    * Get a (counter)model (only if preceded by a SAT or INVALID query).
 100    */
 101   Model getModel();
 102
 103   /**
 104    * Push a user-level context.
 105    */
 106   void push();
 107
 108   /**
 109    * Pop a user-level context.  Throws an exception if nothing to pop.
 110    */
 111   void pop();
 112
 113 private:
 114
 115   /** Our Context */
 116   CVC4::context::Context* d_ctxt;
 117
 118   /** Our expression manager */
 119   ExprManager* d_exprManager;
 120
 121   /** Out internal expression/node manager */
 122   NodeManager* d_nodeManager;
 123
 124   /** User-level options */
 125   const Options* d_options;
 126
 127   /** The decision engine */
 128   DecisionEngine* d_decisionEngine;
 129
 130   /** The decision engine */
 131   TheoryEngine* d_theoryEngine;
 132
 133   /** The propositional engine */
 134   prop::PropEngine* d_propEngine;
 135
 136   /**
 137    * Pre-process an Node.  This is expected to be highly-variable,
 138    * with a lot of "source-level configurability" to add multiple
 139    * passes over the Node.  TODO: may need to specify a LEVEL of
 140    * preprocessing (certain contexts need more/less ?).
 141    */
 142   Node preprocess(TNode node);
 143
 144   /**
 145    * Adds a formula to the current context.
 146    */
 147   void addFormula(TNode node);
 148
 149   /**
 150    * Full check of consistency in current context.  Returns true iff
 151    * consistent.
 152    */
 153   Result check();
 154
 155   /**
 156    * Quick check of consistency in current context: calls
 157    * processAssertionList() then look for inconsistency (based only on
 158    * that).
 159    */
 160   Result quickCheck();
 161
 162 };/* class SmtEngine */
 163
 164 }/* CVC4 namespace */
 165
 166 #endif /* __CVC4__SMT_ENGINE_H */