additional headers

10 files changed, 421 insertions, 7 deletions

diff --git a/src/include/context.h b/src/include/context.h
new file mode 100644
index 000000000..845660ed7
--- /dev/null
+++ b/src/include/context.h
@@ -0,0 +1,29 @@
+/*********************                                           -*- C++ -*-  */
+/** context.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_CONTEXT_H
+#define __CVC4_CONTEXT_H
+
+namespace CVC4 {
+
+class ContextManager {
+public:
+  void switchContext(Context);
+  Context snapshot();
+};/* class ContextManager */
+
+class ContextObject {
+public:
+  void snapshot();
+  void restore();
+};/* class ContextObject */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_CONTEXT_H */
diff --git a/src/include/decision_engine.h b/src/include/decision_engine.h
new file mode 100644
index 000000000..6ff8d7f29
--- /dev/null
+++ b/src/include/decision_engine.h
@@ -0,0 +1,38 @@
+/*********************                                           -*- C++ -*-  */
+/** decision_engine.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_DECISION_ENGINE_H
+#define __CVC4_DECISION_ENGINE_H
+
+namespace CVC4 {
+
+// In terms of abstraction, this is below (and provides services to)
+// PropEngine.
+
+/**
+ * A decision mechanism for the next decision.
+ */
+class DecisionEngine {
+public:
+  /**
+   * Get the next decision.
+   */
+  virtual Literal nextDecision() = 0;
+
+  // TODO: design decision: decision engine should be notified of
+  // propagated lits, and also why(?) (so that it can make decisions
+  // based on the utility of various theories and various theory
+  // literals).  How?  Maybe TheoryEngine has a backdoor into
+  // DecisionEngine "behind the back" of the PropEngine?
+
+};/* class DecisionEngine */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_DECISION_ENGINE_H */
diff --git a/src/include/kind.h b/src/include/kind.h
index 26a3dd607..f45495bb0 100644
--- a/src/include/kind.h
+++ b/src/include/kind.h
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** expr_manager.h
+/** kind.h
  ** This file is part of the CVC4 prototype.
  **
  ** The Analysis of Computer Systems Group (ACSys)
@@ -7,18 +7,22 @@
  ** New York University
  **/
 
-#ifndef __CVC4_EXPR_MANAGER_H
-#define __CVC4_EXPR_MANAGER_H
+#ifndef __CVC4_KIND_H
+#define __CVC4_KIND_H
 
 namespace CVC4 {
 
+// TODO: create this file (?) from theory solver headers so that we
+// have a collection of kinds from all.  This file is mainly a
+// placeholder for design & development work.
+
 enum Kind {
   AND,
   OR,
   XOR,
   NOT,
   PLUS,
-  MINUS,
-  UMINUS,
-  
-};
+  MINUS
+};/* enum Kind */
+
+}/* CVC4 namespace */
diff --git a/src/include/parser.h b/src/include/parser.h
index 0cfc89a28..8f1032286 100644
--- a/src/include/parser.h
+++ b/src/include/parser.h
@@ -12,6 +12,31 @@
 
 namespace CVC4 {
 
+// In terms of abstraction, this is below (and provides services to)
+// the main CVC4 binary and above (and requires the services of)
+// ValidityChecker.
+
+class Parser {
+private:// maybe protected is better ?
+  ValidityChecker *d_vc;
+
+public:
+  Parser(ValidityChecker* vc);
+
+  /**
+   * Process a file.  Overridden in subclasses to support SMT-LIB
+   * format, CVC4 presentation language, etc.  In subclasses, this
+   * function should parse terms, build Command objects, and pass them
+   * to dispatch().
+   */
+  virtual Expr process(std::istream&) = 0;
+
+  /**
+   * Dispatch a command.
+   */
+  void dispatch(const Command&);
+};/* class Parser */
+
 } /* CVC4 namespace */
 
 #endif /* __CVC4_PARSER_H */
diff --git a/src/include/prop_engine.h b/src/include/prop_engine.h
new file mode 100644
index 000000000..1ec0316a9
--- /dev/null
+++ b/src/include/prop_engine.h
@@ -0,0 +1,37 @@
+/*********************                                           -*- C++ -*-  */
+/** prop_engine.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_PROP_ENGINE_H
+#define __CVC4_PROP_ENGINE_H
+
+namespace CVC4 {
+
+// In terms of abstraction, this is below (and provides services to)
+// Prover and above (and requires the services of) a specific
+// propositional solver, DPLL or otherwise.
+
+class PropEngine {
+  DecisionEngine* d_de;
+
+public:
+  /**
+   * Create a PropEngine with a particular decision and theory engine.
+   */
+  PropEngine(DecisionEngine*, TheoryEngine*);
+
+  /**
+   * Converts to CNF if necessary.
+   */
+  void solve(Expr);
+
+};/* class PropEngine */
+
+}
+
+#endif /* __CVC4_PROP_ENGINE_H */
diff --git a/src/include/prover.h b/src/include/prover.h
new file mode 100644
index 000000000..7abfafe63
--- /dev/null
+++ b/src/include/prover.h
@@ -0,0 +1,107 @@
+/*********************                                           -*- C++ -*-  */
+/** prover.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_PROVER_H
+#define __CVC4_PROVER_H
+
+// In terms of abstraction, this is below (and provides services to)
+// ValidityChecker and above (and requires the services of)
+// PropEngine.
+
+namespace CVC4 {
+
+// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
+// hood): use a type parameter and have check() delegate, or subclass
+// Prover 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 Prover {
+  /** 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:
+  /**
+   * 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();
+
+  /**
+   * Pop a user-level context.  Throws an exception if nothing to pop.
+   */
+  void pop();
+};/* class Prover */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_PROVER_H */
diff --git a/src/include/result.h b/src/include/result.h
new file mode 100644
index 000000000..1cecc5301
--- /dev/null
+++ b/src/include/result.h
@@ -0,0 +1,61 @@
+/*********************                                           -*- C++ -*-  */
+/** result.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_RESULT_H
+#define __CVC4_RESULT_H
+
+namespace CVC4 {
+
+// TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
+// but this requires doing the same for Prover and needs discussion.
+
+// TODO: subclass to provide models, etc.  This is really just
+// intended as a three-valued response code.
+
+/**
+ * Three-valued, immutable SMT result, with optional explanation.
+ */
+class Result {
+public:
+  enum {
+    UNSAT = 0,
+    SAT = 1,
+    UNKNOWN = 2
+  } SAT;
+
+  enum {
+    INVALID = 0,
+    VALID = 1,
+    UNKNOWN = 2
+  } Validity;
+
+  enum {
+    REQUIRES_FULL_CHECK,
+    INCOMPLETE,
+    TIMEOUT,
+    BAIL,
+    OTHER
+  } UnknownExplanation;
+
+private:
+  SAT      d_sat;
+  Validity d_validity;
+  enum { SAT, VALIDITY } d_which;
+
+public:
+  Result(SAT);
+  Result(Validity);
+
+  SAT isSAT();
+  Validity isValid();
+  UnknownExplanation whyUnknown();
+
+};/* class Result */
+
+}/* CVC4 namespace */
diff --git a/src/include/theory.h b/src/include/theory.h
new file mode 100644
index 000000000..b08e9e7ba
--- /dev/null
+++ b/src/include/theory.h
@@ -0,0 +1,71 @@
+/*********************                                           -*- C++ -*-  */
+/** theory.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_THEORY_H
+#define __CVC4_THEORY_H
+
+namespace CVC4 {
+
+/**
+ * Base class for T-solvers.  Abstract DPLL(T).
+ */
+class Theory {
+public:
+  /**
+   * Subclasses of Theory may add additional efforts.  DO NOT CHECK
+   * equality with one of these values (e.g. if STANDARD xxx) but
+   * rather use range checks (or use the helper functions below).
+   * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
+   * with MAX_EFFORT.
+   */
+  enum Effort {
+    MIN_EFFORT = 0,
+    QUICK_CHECK = 10,
+    STANDARD = 50,
+    FULL_EFFORT = 100
+  };/* enum Effort */
+
+  // TODO add compiler annotation "constant function" here
+  static bool minEffortOnly(Effort e)        { return e == MIN_EFFORT; }
+  static bool quickCheckOrMore(Effort e)     { return e >= QUICK_CHECK; }
+  static bool quickCheckOnly(Effort e)       { return e >= QUICK_CHECK && e < STANDARD; }
+  static bool standardEffortOrMore(Effort e) { return e >= STANDARD; }
+  static bool standardEffortOnly(Effort e)   { return e >= STANDARD && e < FULL_EFFORT; }
+  static bool fullEffort(Effort e)           { return e >= FULL_EFFORT; }
+
+  /**
+   * Prepare for an Expr.
+   */
+  virtual void setup(Expr) = 0;
+
+  /**
+   * Assert a literal in the current context.
+   */
+  virtual void assert(Literal) = 0;
+
+  /**
+   * Check the current assignment's consistency.  Return false iff inconsistent.
+   */
+  virtual bool check(Effort level = FULL_EFFORT) = 0;
+
+  /**
+   * T-propagate new literal assignments in the current context.
+   */
+  virtual LiteralSet propagate();
+
+  /**
+   * Return an explanation for the literal (which was previously propagated by this theory)..
+   */
+  virtual Expr explain(Literal) = 0;
+
+};/* class Theory */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_THEORY_H */
diff --git a/src/include/theory_engine.h b/src/include/theory_engine.h
new file mode 100644
index 000000000..f4e36f604
--- /dev/null
+++ b/src/include/theory_engine.h
@@ -0,0 +1,30 @@
+/*********************                                           -*- C++ -*-  */
+/** theory_engine.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_THEORY_ENGINE_H
+#define __CVC4_THEORY_ENGINE_H
+
+namespace CVC4 {
+
+// In terms of abstraction, this is below (and provides services to)
+// PropEngine.
+
+/**
+ * This is essentially an abstraction for a collection of theories.  A
+ * TheoryEngine provides services to a PropEngine, making various
+ * T-solvers look like a single unit to the propositional part of
+ * CVC4.
+ */
+class TheoryEngine {
+public:
+};/* class TheoryEngine */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_THEORY_ENGINE_H */
diff --git a/src/include/vc.h b/src/include/vc.h
index d4b293a28..a75aa0548 100644
--- a/src/include/vc.h
+++ b/src/include/vc.h
@@ -13,11 +13,23 @@
 /* TODO provide way of querying whether you fall into a fragment /
  * returning what fragment you're in */
 
+// 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.
+
 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.)
 public:
   void doCommand(Command);
+
+  void query(Expr);
 };
 
 } /* CVC4 namespace */