fixups, file comments

3 files changed, 144 insertions, 23 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 */
 
diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h
new file mode 100644
index 000000000..e571f5969
--- /dev/null
+++ b/src/include/cvc4_config.h
@@ -0,0 +1,41 @@
+/*********************                                           -*- C++ -*-  */
+/** cvc4_config.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
+#ifdef __BUILDING_CVC4LIB
+
+#  if defined _WIN32 || defined __CYGWIN__
+#    ifdef BUILDING_DLL
+#      ifdef __GNUC__
+#        define CVC4_PUBLIC __attribute__((dllexport))
+#      else /* ! __GNUC__ */
+#        define CVC4_PUBLIC __declspec(dllexport)
+#      endif /* __GNUC__ */
+#    else /* BUILDING_DLL */
+#      ifdef __GNUC__
+#        define CVC4_PUBLIC __attribute__((dllimport))
+#      else /* ! __GNUC__ */
+#        define CVC4_PUBLIC __declspec(dllimport)
+#      endif /* __GNUC__ */
+#    endif /* BUILDING_DLL */
+#  else /* !( defined _WIN32 || defined __CYGWIN__ ) */
+#    if __GNUC__ >= 4
+#      define CVC4_PUBLIC __attribute__ ((visibility("default")))
+#    else /* !( __GNUC__ >= 4 ) */
+#      define CVC4_PUBLIC
+#    endif /* __GNUC__ >= 4 */
+#  endif /* defined _WIN32 || defined __CYGWIN__ */
+
+#else /* ! __BUILDING_CVC4LIB */
+
+#  define CVC4_PUBLIC
+
+#endif /* __BUILDING_CVC4LIB */
diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h
index 1f5ac659d..36d771647 100644
--- a/src/include/cvc4_expr.h
+++ b/src/include/cvc4_expr.h
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** expr.h
+/** cvc4_expr.h
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -15,6 +15,8 @@
 
 #include <vector>
 #include <stdint.h>
+
+#include "cvc4_config.h"
 #include "expr/kind.h"
 
 namespace CVC4 {
@@ -29,7 +31,7 @@ using CVC4::expr::ExprValue;
  * Encapsulation of an ExprValue pointer.  The reference count is
  * maintained in the ExprValue.
  */
-class Expr {
+class CVC4_PUBLIC Expr {
   /** A convenient null-valued encapsulated pointer */
   static Expr s_null;
 
@@ -49,17 +51,17 @@ class Expr {
   friend class ExprBuilder;
 
 public:
-  Expr(const Expr&);
+  CVC4_PUBLIC Expr(const Expr&);
 
   /** Destructor.  Decrements the reference count and, if zero,
    *  collects the ExprValue. */
-  ~Expr();
+  CVC4_PUBLIC ~Expr();
 
-  Expr& operator=(const Expr&);
+  Expr& operator=(const Expr&) CVC4_PUBLIC;
 
   /** Access to the encapsulated expression.
    *  @return the encapsulated expression. */
-  ExprValue* operator->() const;
+  ExprValue* operator->() const CVC4_PUBLIC;
 
   uint64_t hash() const;