diff options
Diffstat (limited to 'src/include')
-rw-r--r-- | src/include/cvc4.h | 115 | ||||
-rw-r--r-- | src/include/cvc4_expr.h | 100 | ||||
-rw-r--r-- | src/include/theory.h | 81 |
3 files changed, 0 insertions, 296 deletions
diff --git a/src/include/cvc4.h b/src/include/cvc4.h deleted file mode 100644 index bbaffabb0..000000000 --- a/src/include/cvc4.h +++ /dev/null @@ -1,115 +0,0 @@ -/********************* -*- C++ -*- */ -/** 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 - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - **/ - -#ifndef __CVC4_H -#define __CVC4_H - -#include <vector> -#include "cvc4_expr.h" -#include "util/command.h" -#include "util/result.h" -#include "util/model.h" - -namespace CVC4 { - -class SmtEngine { - /** Current set of assertions. */ - // TODO: make context-aware to handle user-level push/pop. - std::vector<Expr> d_assertList; - - /** Our expression manager */ - ExprManager *d_em; - - /** User-level options */ - Options *opts; - - /** - * 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: - /* - * Construct an SmtEngine with the given expression manager and user options. - */ - SmtEngine(ExprManager*, Options*) throw(); - - /** - * Execute a command. - */ - void doCommand(Command*); - - /** - * 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 SmtEngine */ - -}/* CVC4 namespace */ - -#endif /* __CVC4_H */ diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h deleted file mode 100644 index 863097123..000000000 --- a/src/include/cvc4_expr.h +++ /dev/null @@ -1,100 +0,0 @@ -/********************* -*- C++ -*- */ -/** 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 - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Reference-counted encapsulation of a pointer to an expression. - **/ - -#ifndef __CVC4_EXPR_H -#define __CVC4_EXPR_H - -#include <vector> -#include <stdint.h> - -#include "cvc4_config.h" -#include "expr/kind.h" - -namespace CVC4 { - -namespace expr { - class ExprValue; -}/* CVC4::expr namespace */ - -using CVC4::expr::ExprValue; - -/** - * Encapsulation of an ExprValue pointer. The reference count is - * maintained in the ExprValue. - */ -class CVC4_PUBLIC Expr { - /** A convenient null-valued encapsulated pointer */ - static Expr s_null; - - /** The referenced ExprValue */ - ExprValue* d_ev; - - /** This constructor is reserved for use by the Expr package; one - * must construct an Expr using one of the build mechanisms of the - * Expr package. - * - * Increments the reference count. */ - explicit Expr(ExprValue*); - - typedef Expr* iterator; - typedef Expr const* const_iterator; - - friend class ExprBuilder; - -public: - CVC4_PUBLIC Expr(const Expr&); - - /** Destructor. Decrements the reference count and, if zero, - * collects the ExprValue. */ - CVC4_PUBLIC ~Expr(); - - Expr& operator=(const Expr&) CVC4_PUBLIC; - - /** Access to the encapsulated expression. - * @return the encapsulated expression. */ - ExprValue* operator->() const CVC4_PUBLIC; - - uint64_t hash() const; - - Expr eqExpr(const Expr& right) const; - Expr notExpr() const; - Expr negate() const; // avoid double-negatives - Expr andExpr(const Expr& right) const; - Expr orExpr(const Expr& right) const; - Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const; - Expr iffExpr(const Expr& right) const; - Expr impExpr(const Expr& right) const; - Expr xorExpr(const Expr& right) const; - - Expr plusExpr(const Expr& right) const; - Expr uMinusExpr() const; - Expr multExpr(const Expr& right) const; - - inline Kind getKind() const; - - static Expr null() { return s_null; } - -};/* class Expr */ - -}/* CVC4 namespace */ - -#include "expr/expr_value.h" - -namespace CVC4 { - -inline Kind Expr::getKind() const { - return Kind(d_ev->d_kind); -} - -}/* CVC4 namespace */ - -#endif /* __CVC4_EXPR_H */ diff --git a/src/include/theory.h b/src/include/theory.h deleted file mode 100644 index 47b4a2d92..000000000 --- a/src/include/theory.h +++ /dev/null @@ -1,81 +0,0 @@ -/********************* -*- 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 - -#include "expr.h" -#include "literal.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. - */ - // TODO design decisoin: instead of returning a set of literals - // here, perhaps we have an interface back into the prop engine - // where we assert directly. we might sometimes unknowingly assert - // something clearly inconsistent (esp. in a parallel context). - // This would allow the PropEngine to cancel our further work since - // we're already inconsistent---also could strategize dynamically on - // whether enough theory prop work has occurred. - virtual void propagate(Callback propagator, Effort level = FULL_EFFORT) = 0; - - /** - * 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 */ |