From 541379b3d361e255cd664207f8b2e278a5b5e3eb Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 3 Nov 2009 03:07:58 +0000 Subject: [PATCH] additional headers --- DESIGN_QUESTIONS | 49 ++++++++++++++++ src/include/context.h | 29 +++++++++ src/include/decision_engine.h | 38 ++++++++++++ src/include/kind.h | 18 +++--- src/include/parser.h | 25 ++++++++ src/include/prop_engine.h | 37 ++++++++++++ src/include/prover.h | 107 ++++++++++++++++++++++++++++++++++ src/include/result.h | 61 +++++++++++++++++++ src/include/theory.h | 71 ++++++++++++++++++++++ src/include/theory_engine.h | 30 ++++++++++ src/include/vc.h | 12 ++++ 11 files changed, 470 insertions(+), 7 deletions(-) create mode 100644 DESIGN_QUESTIONS create mode 100644 src/include/context.h create mode 100644 src/include/decision_engine.h create mode 100644 src/include/prop_engine.h create mode 100644 src/include/prover.h create mode 100644 src/include/result.h create mode 100644 src/include/theory.h create mode 100644 src/include/theory_engine.h diff --git a/DESIGN_QUESTIONS b/DESIGN_QUESTIONS new file mode 100644 index 000000000..12704c6bf --- /dev/null +++ b/DESIGN_QUESTIONS @@ -0,0 +1,49 @@ +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 ?). + */ + 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 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 */ -- 2.30.2