src/smt/smt_engine.h

   1 /*********************                                           -*- C++ -*-  */
   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 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/node.h"
  23 #include "expr/expr.h"
  24 #include "expr/node_manager.h"
  25 #include "expr/expr_manager.h"
  26 #include "util/result.h"
  27 #include "util/model.h"
  28 #include "util/options.h"
  29 #include "prop/prop_engine.h"
  30 #include "util/decision_engine.h"
  31
  32 // In terms of abstraction, this is below (and provides services to)
  33 // ValidityChecker and above (and requires the services of)
  34 // PropEngine.
  35
  36 namespace CVC4 {
  37
  38 class Command;
  39
  40 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
  41 // hood): use a type parameter and have check() delegate, or subclass
  42 // SmtEngine and override check()?
  43 //
  44 // Probably better than that is to have a configuration object that
  45 // indicates which passes are desired.  The configuration occurs
  46 // elsewhere (and can even occur at runtime).  A simple "pass manager"
  47 // of sorts determines check()'s behavior.
  48 //
  49 // The CNF conversion can go on in PropEngine.
  50
  51 class CVC4_PUBLIC SmtEngine {
  52
  53 public:
  54
  55   /**
  56    * Construct an SmtEngine with the given expression manager and user options.
  57    */
  58   SmtEngine(ExprManager* em, Options* opts) throw();
  59
  60   /**
  61    * Destruct the smt engine.
  62    */
  63   ~SmtEngine();
  64
  65   /**
  66    * Execute a command.
  67    */
  68   void doCommand(Command*);
  69
  70   /**
  71    * Add a formula to the current context: preprocess, do per-theory
  72    * setup, use processAssertionList(), asserting to T-solver for
  73    * literals and conjunction of literals.  Returns false iff
  74    * inconsistent.
  75    */
  76   Result assertFormula(const BoolExpr& e);
  77
  78   /**
  79    * Add a formula to the current context and call check().  Returns
  80    * true iff consistent.
  81    */
  82   Result query(const BoolExpr& e);
  83
  84   /**
  85    * Add a formula to the current context and call check().  Returns
  86    * true iff consistent.
  87    */
  88   Result checkSat(const BoolExpr& e);
  89
  90   /**
  91    * Simplify a formula without doing "much" work.  Requires assist
  92    * from the SAT Engine.
  93    */
  94   Expr simplify(const Expr& e);
  95
  96   /**
  97    * Get a (counter)model (only if preceded by a SAT or INVALID query.
  98    */
  99   Model getModel();
 100
 101   /**
 102    * Push a user-level context.
 103    */
 104   void push();
 105
 106   /**
 107    * Pop a user-level context.  Throws an exception if nothing to pop.
 108    */
 109   void pop();
 110
 111 private:
 112
 113   /** Current set of assertions. */
 114   // TODO: make context-aware to handle user-level push/pop.
 115   std::vector<Node> d_assertions;
 116
 117   /** Our expression manager */
 118   ExprManager *d_public_em;
 119
 120   /** Out internal expression/node manager */
 121   NodeManager *d_nm;
 122
 123   /** User-level options */
 124   Options *d_opts;
 125
 126   /** The decision engine */
 127   DecisionEngine d_de;
 128
 129   /** The decision engine */
 130   TheoryEngine d_te;
 131
 132   /** The propositional engine */
 133   PropEngine d_prop;
 134
 135   /**
 136    * Pre-process an Node.  This is expected to be highly-variable,
 137    * with a lot of "source-level configurability" to add multiple
 138    * passes over the Node.  TODO: may need to specify a LEVEL of
 139    * preprocessing (certain contexts need more/less ?).
 140    */
 141   Node preprocess(const Node& e);
 142
 143   /**
 144    * Adds a formula to the current context.
 145    */
 146   void addFormula(const Node& e);
 147
 148   /**
 149    * Full check of consistency in current context.  Returns true iff
 150    * consistent.
 151    */
 152   Result check();
 153
 154   /**
 155    * Quick check of consistency in current context: calls
 156    * processAssertionList() then look for inconsistency (based only on
 157    * that).
 158    */
 159   Result quickCheck();
 160
 161   /**
 162    * Process the assertion list: for literals and conjunctions of
 163    * literals, assert to T-solver.
 164    */
 165   Node processAssertionList();
 166
 167
 168 };/* class SmtEngine */
 169
 170 }/* CVC4 namespace */
 171
 172 #endif /* __CVC4__SMT_ENGINE_H */