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
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
INCLUDES = -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libcontext.la
INCLUDES = -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libexpr.la
/********************* -*- 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
#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 */
--- /dev/null
+/********************* -*- 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 */
/********************* -*- 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
#include <vector>
#include <stdint.h>
+
+#include "cvc4_config.h"
#include "expr/kind.h"
namespace CVC4 {
* 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;
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;
INCLUDES = -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CPPFLAGS = -D__BUILDING_CVC4LIB
bin_PROGRAMS = cvc4
-#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 {
-#include <cstdio>
+/********************* -*- 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 <cstdlib>
#include <new>
#include <unistd.h>
-#include <cstdio>
+/********************* -*- 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 <cstdlib>
#include <cerrno>
#include <new>
-#include <iostream>
+/********************* -*- 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 <exception>
#include <string>
-#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 {
-#include <string>
+/********************* -*- 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 <cstdio>
#include <cstdlib>
#include <cerrno>
INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@
AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libparser.la
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
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 = \
#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 {
INCLUDES = -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libsmt.la
+++ /dev/null
-/********************* -*- 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 <vector>
-#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<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 SmtEngine */
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__SMT_ENGINE_H */
INCLUDES = -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libtheory.la
#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 {
INCLUDES = -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libutil.la
#ifndef __CVC4__DECISION_ENGINE_H
#define __CVC4__DECISION_ENGINE_H
-#include "core/literal.h"
+#include "util/literal.h"
namespace CVC4 {
-#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 {
+++ /dev/null
-#!/bin/sh
-
-echo
-echo '***************************************************************************'
-echo '* *'
-echo '* ERROR: CxxTest was not found at configure-time; tests cannot be run. *'
-echo '* *'
-echo '***************************************************************************'
-echo
-
-exit 1
-
--- /dev/null
+#!/bin/sh
+
+echo
+echo '***************************************************************************'
+echo '* *'
+echo '* ERROR: CxxTest was not found at configure-time; tests cannot be run. *'
+echo '* *'
+echo '***************************************************************************'
+echo
+
+exit 1
+
projects / cvc5.git / commitdiff