From f6968899de4d27c5bc986c3ac89972fbbe35c361 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 23 Nov 2009 16:42:12 +0000 Subject: [PATCH] fixups, file comments --- src/Makefile.am | 12 +++- src/context/Makefile.am | 1 + src/expr/Makefile.am | 1 + src/include/cvc4.h | 112 ++++++++++++++++++++++++++++----- src/include/cvc4_config.h | 41 +++++++++++++ src/include/cvc4_expr.h | 14 +++-- src/main/Makefile.am | 1 + src/main/about.h | 13 +++- src/main/getopt.cpp | 13 +++- src/main/main.cpp | 13 +++- src/main/main.h | 13 +++- src/main/usage.h | 13 +++- src/main/util.cpp | 13 +++- src/parser/Makefile.am | 1 + src/prop/Makefile.am | 5 ++ src/prop/minisat/Makefile.am | 1 + src/prop/prop_engine.h | 6 +- src/smt/Makefile.am | 1 + src/smt/smt_engine.h | 116 ----------------------------------- src/theory/Makefile.am | 1 + src/theory/theory.h | 4 +- src/util/Makefile.am | 1 + src/util/decision_engine.h | 2 +- src/util/options.h | 13 +++- test/{ => unit}/no_cxxtest | 0 25 files changed, 258 insertions(+), 153 deletions(-) create mode 100644 src/include/cvc4_config.h delete mode 100644 src/smt/smt_engine.h rename test/{ => unit}/no_cxxtest (100%) diff --git a/src/Makefile.am b/src/Makefile.am index f7404e514..ca22263fd 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -1,5 +1,6 @@ INCLUDES = -I@srcdir@/include -I@srcdir@ AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4LIB SUBDIRS = util expr context prop smt theory . parser main @@ -10,10 +11,19 @@ libcvc4_la_LIBADD = \ util/libutil.la \ expr/libexpr.la \ context/libcontext.la \ + prop/libprop.la \ prop/minisat/libminisat.la \ smt/libsmt.la \ theory/libtheory.la -EXTRA_DIST = \ +publicheaders = \ include/cvc4.h \ + include/cvc4_config.h \ include/cvc4_expr.h + +install-data-local: + $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4; \ + @for f in $(publicheaders); do + echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4" + $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4" + done diff --git a/src/context/Makefile.am b/src/context/Makefile.am index 87a4598c4..a906d2873 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -1,5 +1,6 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libcontext.la diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index da2839ad1..df3c34094 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -1,5 +1,6 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libexpr.la 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 #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 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 #include + +#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; diff --git a/src/main/Makefile.am b/src/main/Makefile.am index cf392f6b6..dddfb3219 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -1,5 +1,6 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4LIB bin_PROGRAMS = cvc4 diff --git a/src/main/about.h b/src/main/about.h index e02183ba7..458716842 100644 --- a/src/main/about.h +++ b/src/main/about.h @@ -1,4 +1,15 @@ -#ifndef __CVC4__MAIN__ABOUT_H +/********************* -*- C++ -*- */ +/** about.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 ]] + **/ + #define __CVC4__MAIN__ABOUT_H namespace CVC4 { diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 5f32ccd77..f1fe375b6 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -1,4 +1,15 @@ -#include +/********************* -*- C++ -*- */ +/** getopt.cpp + ** 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 ]] + **/ + #include #include #include diff --git a/src/main/main.cpp b/src/main/main.cpp index d2c6cb26d..44543a75f 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -1,4 +1,15 @@ -#include +/********************* -*- C++ -*- */ +/** main.cpp + ** 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 ]] + **/ + #include #include #include diff --git a/src/main/main.h b/src/main/main.h index d0a517967..5e0c68053 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -1,4 +1,15 @@ -#include +/********************* -*- C++ -*- */ +/** main.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 ]] + **/ + #include #include diff --git a/src/main/usage.h b/src/main/usage.h index edc9ad1d1..3326108ac 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -1,4 +1,15 @@ -#ifndef __CVC4__MAIN__USAGE_H +/********************* -*- C++ -*- */ +/** usage.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 ]] + **/ + #define __CVC4__MAIN__USAGE_H namespace CVC4 { diff --git a/src/main/util.cpp b/src/main/util.cpp index 63c8cc860..572aea00f 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -1,4 +1,15 @@ -#include +/********************* -*- C++ -*- */ +/** util.cpp + ** 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 ]] + **/ + #include #include #include diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 8ea47d140..e83605d29 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -1,5 +1,6 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@ AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libparser.la diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 941b0c653..87108cb5c 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -1,4 +1,9 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4LIB + +noinst_LTLIBRARIES = libprop.la + +libprop_la_SOURCES = SUBDIRS = minisat diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am index db646fef4..f2716ff56 100644 --- a/src/prop/minisat/Makefile.am +++ b/src/prop/minisat/Makefile.am @@ -1,5 +1,6 @@ INCLUDES = -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libminisat.la libminisat_la_SOURCES = \ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 5572b47f7..08d485882 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -12,9 +12,9 @@ #ifndef __CVC4__PROP__PROP_ENGINE_H #define __CVC4__PROP__PROP_ENGINE_H -#include "core/cvc4_expr.h" -#include "core/decision_engine.h" -#include "core/theory_engine.h" +#include "cvc4_expr.h" +#include "util/decision_engine.h" +#include "theory/theory_engine.h" namespace CVC4 { namespace prop { diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index c2967ad14..325999db2 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -1,5 +1,6 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libsmt.la diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h deleted file mode 100644 index 078bf9cde..000000000 --- a/src/smt/smt_engine.h +++ /dev/null @@ -1,116 +0,0 @@ -/********************* -*- C++ -*- */ -/** prover.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__SMT__SMT_ENGINE_H -#define __CVC4__SMT__SMT_ENGINE_H - -#include -#include "core/cvc4_expr.h" -#include "core/result.h" -#include "core/model.h" - -// In terms of abstraction, this is below (and provides services to) -// ValidityChecker and above (and requires the services of) -// PropEngine. - -namespace CVC4 { -namespace smt { - -// 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 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 SmtEngine */ - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__SMT__SMT_ENGINE_H */ diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 97cb116e0..803cc53b5 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -1,5 +1,6 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libtheory.la diff --git a/src/theory/theory.h b/src/theory/theory.h index 05e8e1b01..1369d5f0b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -12,8 +12,8 @@ #ifndef __CVC4__THEORY__THEORY_H #define __CVC4__THEORY__THEORY_H -#include "core/cvc4_expr.h" -#include "core/literal.h" +#include "cvc4_expr.h" +#include "util/literal.h" namespace CVC4 { namespace theory { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index f25f52ac0..4fe483c98 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -1,5 +1,6 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libutil.la diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index 2064e3687..a6f8596dd 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -12,7 +12,7 @@ #ifndef __CVC4__DECISION_ENGINE_H #define __CVC4__DECISION_ENGINE_H -#include "core/literal.h" +#include "util/literal.h" namespace CVC4 { diff --git a/src/util/options.h b/src/util/options.h index 6104470d2..490cd607b 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -1,4 +1,15 @@ -#ifndef __CVC4__OPTIONS_H +/********************* -*- C++ -*- */ +/** options.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 ]] + **/ + #define __CVC4__OPTIONS_H namespace CVC4 { diff --git a/test/no_cxxtest b/test/unit/no_cxxtest similarity index 100% rename from test/no_cxxtest rename to test/unit/no_cxxtest -- 2.30.2