diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-23 16:42:12 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-23 16:42:12 +0000 |
commit | f6968899de4d27c5bc986c3ac89972fbbe35c361 (patch) | |
tree | dd3461b2e08e1568ca9aff97a56e93a0445b3abc /src/include | |
parent | 95e5ca98d4c22897c0192a78ebeeb05e4838db2b (diff) |
fixups, file comments
Diffstat (limited to 'src/include')
-rw-r--r-- | src/include/cvc4.h | 112 | ||||
-rw-r--r-- | src/include/cvc4_config.h | 41 | ||||
-rw-r--r-- | src/include/cvc4_expr.h | 14 |
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; |