--- /dev/null
+vc.h
+
+/* TODO provide way of querying whether you fall into a fragment /
+ * returning what fragment you're in */
+
+decision_engine.h
+
+ // 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?
+
+result.h
+
+// 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.
+
+expr_builder.h
+
+ // TODO: store some flags here and install into attribute map when
+ // the expr is created? (we'd have to do that since we don't know
+ // it's hash code yet)
+
+prover.h
+
+// 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.
+
+prover.h
+
+ /** (preprocessing)
+ * 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 ?).
+ */
+
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
/********************* -*- C++ -*- */
-/** expr_manager.h
+/** kind.h
** This file is part of the CVC4 prototype.
**
** The Analysis of Computer Systems Group (ACSys)
** 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 */
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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
/* 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 */
projects / cvc5.git / commitdiff