fixups, file comments

24 files changed, 258 insertions, 153 deletions

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 <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;
 
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 <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>
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 <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>
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 <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>
 
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 <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>
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 <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 */
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 {