src/smt/smt_engine.h

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