fixups, file comments

1 files changed, 95 insertions, 17 deletions

diff --git a/src/include/cvc4.h b/src/include/cvc4.h
index c5e3bb013..7b068228f 100644
--- a/src/include/cvc4.h
+++ b/src/include/cvc4.h
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** vc.h
+/** cvc4.h
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -12,30 +12,108 @@
 #ifndef __CVC4_H
 #define __CVC4_H
 
-#include "util/command.h"
+#include <vector>
 #include "cvc4_expr.h"
-
-/* TODO provide way of querying whether you fall into a fragment /
- * returning what fragment you're in */
+#include "util/command.h"
+#include "util/result.h"
+#include "util/model.h"
 
 // In terms of abstraction, this is below (and provides services to)
-// users using the library interface, and also the parser for the main
-// CVC4 binary.  It is above (and requires the services of) the Prover
-// class.
+// ValidityChecker and above (and requires the services of)
+// PropEngine.
 
 namespace CVC4 {
 
-/**
- * User-visible (library) interface to CVC4.
- */
-class ValidityChecker {
-  // on entry to the validity checker interface, need to set up
-  // current state (ExprManager::d_current etc.)
+// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
+// hood): use a type parameter and have check() delegate, or subclass
+// SmtEngine and override check()?
+//
+// Probably better than that is to have a configuration object that
+// indicates which passes are desired.  The configuration occurs
+// elsewhere (and can even occur at runtime).  A simple "pass manager"
+// of sorts determines check()'s behavior.
+//
+// The CNF conversion can go on in PropEngine.
+
+class SmtEngine {
+  /** Current set of assertions. */
+  // TODO: make context-aware to handle user-level push/pop.
+  std::vector<Expr> d_assertList;
+
+private:
+  /**
+   * Pre-process an Expr.  This is expected to be highly-variable,
+   * with a lot of "source-level configurability" to add multiple
+   * passes over the Expr.  TODO: may need to specify a LEVEL of
+   * preprocessing (certain contexts need more/less ?).
+   */
+  void preprocess(Expr);
+
+  /**
+   * Adds a formula to the current context.
+   */
+  void addFormula(Expr);
+
+  /**
+   * Full check of consistency in current context.  Returns true iff
+   * consistent.
+   */
+  Result check();
+
+  /**
+   * Quick check of consistency in current context: calls
+   * processAssertionList() then look for inconsistency (based only on
+   * that).
+   */
+  Result quickCheck();
+
+  /**
+   * Process the assertion list: for literals and conjunctions of
+   * literals, assert to T-solver.
+   */
+  void processAssertionList();
+
 public:
-  void doCommand(Command);
+  /**
+   * Execute a command
+   */
+  void doCommand(Command c);
+
+  /**
+   * Add a formula to the current context: preprocess, do per-theory
+   * setup, use processAssertionList(), asserting to T-solver for
+   * literals and conjunction of literals.  Returns false iff
+   * inconsistent.
+   */
+  Result assert(Expr);
+
+  /**
+   * Add a formula to the current context and call check().  Returns
+   * true iff consistent.
+   */
+  Result query(Expr);
+
+  /**
+   * Simplify a formula without doing "much" work.  Requires assist
+   * from the SAT Engine.
+   */
+  Expr simplify(Expr);
+
+  /**
+   * Get a (counter)model (only if preceded by a SAT or INVALID query.
+   */
+  Model getModel();
+
+  /**
+   * Push a user-level context.
+   */
+  void push();
 
-  void query(Expr);
-};
+  /**
+   * Pop a user-level context.  Throws an exception if nothing to pop.
+   */
+  void pop();
+};/* class SmtEngine */
 
 }/* CVC4 namespace */