big check-in of various fixes and adjustments

diff --git a/Makefile b/Makefile
index 74a1e169b0911df98f9e35d918094c888a3d00a0..33fed788a7113ddecc6b7a547cc8967bc02a93fd 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -11,3 +11,6 @@ _default_build_: all
                echo 'Run configure first, or type "make" in a configured build directory.'; \
                echo; \
        fi
+
+distclean:
+       rm -rf builds

diff --git a/configure.ac b/configure.ac
index e739f5ceecb8ab96e4170fc4933a04e0919566e3..8f844f75d5b370a802a6240875594cd3d1f32626 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -2,7 +2,7 @@
 # Process this file with autoconf to produce a configure script.
 
 AC_PREREQ([2.59])
-AC_INIT([src/include/cvc4.h])
+AC_INIT([src/include/cvc4_config.h])
 AC_CONFIG_AUX_DIR([config])
 #AC_CONFIG_LIBOBJ_DIR([lib])
 AC_CONFIG_MACRO_DIR([config])
@@ -95,7 +95,7 @@ AC_MSG_RESULT($build_type)
 AC_MSG_CHECKING([what dir to configure])
 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
   AC_MSG_RESULT([this one (in builds/)])
-elif test -e src/include/cvc4.h; then
+elif test -e src/include/cvc4_config.h; then
   AC_MSG_RESULT([builds/$target/$build_type])
   echo
   echo Setting up "builds/$target/$build_type"...
@@ -253,8 +253,8 @@ AC_PROG_CC
 AC_PROG_CXX
 AC_PROG_INSTALL
 AC_PROG_LIBTOOL
-AM_PROG_LEX
-AC_PROG_YACC
+#AM_PROG_LEX
+#AC_PROG_YACC
 
 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 AC_PROG_ANTLR

diff --git a/src/Makefile.am b/src/Makefile.am
index afbb587a8c8892ed8ff59762f0f7d85ec4e895bd..1db9d9ecf710c4effe40eb5abaf823d2c60bb365 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -36,9 +36,7 @@ libcvc4_la_LIBADD = \
        @builddir@/theory/libtheory.la
 
 publicheaders = \
-       include/cvc4.h \
-       include/cvc4_config.h \
-       include/cvc4_expr.h
+       include/cvc4_config.h
 
 install-data-local: $(publicheaders)
        $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4

diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index a906d28733165047b58e9bf69a3449d7f2795bfe..d1e0d3c4b70c65e43899889dd7fd2d0126bded02 100644 (file)
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -4,4 +4,5 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libcontext.la
 
-libcontext_la_SOURCES =
+libcontext_la_SOURCES = \
+       context.cpp

diff --git a/src/expr/expr.h b/src/expr/expr.h
index 0fcb5ea6a18d639ae50aeb7e4aa6bfefc31249c5..a16ffee139efd2e6a32cc1336e26b0e11b321f9f 100644 (file)
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -24,12 +24,10 @@ namespace CVC4 {
   class Expr;
 }/* CVC4 namespace */
 
-namespace std {
-inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC;
-}
-
 namespace CVC4 {
 
+inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC;
+
 class ExprManager;
 
 namespace expr {
@@ -116,13 +114,13 @@ public:
 
 #include "expr/expr_value.h"
 
-inline std::ostream& std::operator<<(std::ostream& out, CVC4::Expr e) {
+namespace CVC4 {
+
+inline std::ostream& operator<<(std::ostream& out, CVC4::Expr e) {
   e.toString(out);
   return out;
 }
 
-namespace CVC4 {
-
 inline Kind Expr::getKind() const {
   return Kind(d_ev->d_kind);
 }

diff --git a/src/include/cvc4.h b/src/include/cvc4.h
deleted file mode 100644 (file)
index bbaffab..0000000
--- 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 (file)
index 8630971..0000000
--- 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 (file)
index 47b4a2d..0000000
--- 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 */

diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 6bac079c8612e22c6cc9f9177071357903c78a21..0db12a0f04eb26f5499c2fb78e3b7ccb13d99f22 100644 (file)
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -22,7 +22,6 @@
 #include "parser/symbol_table.h"
 
 namespace CVC4 {
-
 namespace parser {
 
 /**
@@ -206,12 +205,9 @@ private:
   SymbolTable<Expr> d_var_symbol_table;
 };
 
-}
-
-}
+std::ostream& operator<<(std::ostream& out, AntlrParser::BenchmarkStatus status);
 
-namespace std {
-ostream& operator<<(ostream& out, CVC4::parser::AntlrParser::BenchmarkStatus status);
-}
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
 #endif /* CVC4_PARSER_H_ */

diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index 9f548d656d2acb1dfcc6af9b36e6873bd9502800..2619b2dacf305f171893593efe0287dce9fbcf83 100644 (file)
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -4,25 +4,20 @@ AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 
 noinst_LTLIBRARIES = libparsercvc.la
 
-libparsercvc_la_SOURCES = \
-       CvcLexer.g \
-       CvcParser.g \
-       AntlrCvcLexer.hpp \
-       AntlrCvcLexer.cpp \
-       AntlrCvcParser.hpp \
-       AntlrCvcParser.cpp   
-
-BUILT_SOURCES = \
+ANTLR_STUFF = \
        AntlrCvcLexer.hpp \
        AntlrCvcLexer.cpp \
        AntlrCvcParser.hpp \
        AntlrCvcParser.cpp 
 
+libparsercvc_la_SOURCES = \
+       CvcLexer.g \
+       CvcParser.g \
+       $(ANTLR_STUFF)
+
+BUILT_SOURCES = $(ANTLR_STUFF)
+CLEAN_FILES = $(ANTLR_STUFF)
 
-AntlrCvcLexer.hpp: CvcLexer.g
-AntlrCvcLexer.cpp: CvcLexer.g
-       $(ANTLR) @srcdir@/CvcLexer.g
+Antlr%.cpp Antlr%.hpp: %.g
+       $(ANTLR) -o "@builddir@" "@srcdir@/$<"
 
-AntlrCvcParser.hpp: CvcParser.g AntlrCvcLexer.cpp
-AntlrCvcParser.cpp: CvcParser.g AntlrCvcLexer.cpp
-       $(ANTLR) @srcdir@/CvcParser.g

diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in
deleted file mode 100644 (file)
index 54c641b..0000000
--- a/src/parser/cvc/Makefile.in
+++ /dev/null
@@ -1,502 +0,0 @@
-# Makefile.in generated by automake 1.9.6 from Makefile.am.
-# @configure_input@
-
-# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
-# 2003, 2004, 2005  Free Software Foundation, Inc.
-# This Makefile.in is free software; the Free Software Foundation
-# gives unlimited permission to copy and/or distribute it,
-# with or without modifications, as long as this notice is preserved.
-
-# This program is distributed in the hope that it will be useful,
-# but WITHOUT ANY WARRANTY, to the extent permitted by law; without
-# even the implied warranty of MERCHANTABILITY or FITNESS FOR A
-# PARTICULAR PURPOSE.
-
-@SET_MAKE@
-
-srcdir = @srcdir@
-top_srcdir = @top_srcdir@
-VPATH = @srcdir@
-pkgdatadir = $(datadir)/@PACKAGE@
-pkglibdir = $(libdir)/@PACKAGE@
-pkgincludedir = $(includedir)/@PACKAGE@
-top_builddir = ../../..
-am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd
-INSTALL = @INSTALL@
-install_sh_DATA = $(install_sh) -c -m 644
-install_sh_PROGRAM = $(install_sh) -c
-install_sh_SCRIPT = $(install_sh) -c
-INSTALL_HEADER = $(INSTALL_DATA)
-transform = $(program_transform_name)
-NORMAL_INSTALL = :
-PRE_INSTALL = :
-POST_INSTALL = :
-NORMAL_UNINSTALL = :
-PRE_UNINSTALL = :
-POST_UNINSTALL = :
-build_triplet = @build@
-host_triplet = @host@
-target_triplet = @target@
-subdir = src/parser/cvc
-DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in
-ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
-am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \
-       $(top_srcdir)/config/libtool.m4 \
-       $(top_srcdir)/config/ltoptions.m4 \
-       $(top_srcdir)/config/ltsugar.m4 \
-       $(top_srcdir)/config/ltversion.m4 \
-       $(top_srcdir)/config/lt~obsolete.m4 $(top_srcdir)/configure.ac
-am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
-       $(ACLOCAL_M4)
-mkinstalldirs = $(install_sh) -d
-CONFIG_HEADER = $(top_builddir)/config.h
-CONFIG_CLEAN_FILES =
-LTLIBRARIES = $(noinst_LTLIBRARIES)
-libparsercvc_la_LIBADD =
-am_libparsercvc_la_OBJECTS = AntlrCvcLexer.lo AntlrCvcParser.lo
-libparsercvc_la_OBJECTS = $(am_libparsercvc_la_OBJECTS)
-DEFAULT_INCLUDES = -I. -I$(srcdir) -I$(top_builddir)
-depcomp = $(SHELL) $(top_srcdir)/config/depcomp
-am__depfiles_maybe = depfiles
-CXXCOMPILE = $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
-       $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS)
-LTCXXCOMPILE = $(LIBTOOL) --tag=CXX --mode=compile $(CXX) $(DEFS) \
-       $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) \
-       $(AM_CXXFLAGS) $(CXXFLAGS)
-CXXLD = $(CXX)
-CXXLINK = $(LIBTOOL) --tag=CXX --mode=link $(CXXLD) $(AM_CXXFLAGS) \
-       $(CXXFLAGS) $(AM_LDFLAGS) $(LDFLAGS) -o $@
-COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
-       $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
-LTCOMPILE = $(LIBTOOL) --tag=CC --mode=compile $(CC) $(DEFS) \
-       $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) \
-       $(AM_CFLAGS) $(CFLAGS)
-CCLD = $(CC)
-LINK = $(LIBTOOL) --tag=CC --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) \
-       $(AM_LDFLAGS) $(LDFLAGS) -o $@
-SOURCES = $(libparsercvc_la_SOURCES)
-DIST_SOURCES = $(libparsercvc_la_SOURCES)
-ETAGS = etags
-CTAGS = ctags
-DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
-ACLOCAL = @ACLOCAL@
-AMDEP_FALSE = @AMDEP_FALSE@
-AMDEP_TRUE = @AMDEP_TRUE@
-AMTAR = @AMTAR@
-ANTLR = @ANTLR@
-ANTLR_INCLUDES = @ANTLR_INCLUDES@
-ANTLR_LDFLAGS = @ANTLR_LDFLAGS@
-AR = @AR@
-AS = @AS@
-AUTOCONF = @AUTOCONF@
-AUTOHEADER = @AUTOHEADER@
-AUTOMAKE = @AUTOMAKE@
-AWK = @AWK@
-CC = @CC@
-CCDEPMODE = @CCDEPMODE@
-CFLAGS = @CFLAGS@
-CPP = @CPP@
-CPPFLAGS = @CPPFLAGS@
-CVC4_LIBRARY_RELEASE_CODE = @CVC4_LIBRARY_RELEASE_CODE@
-CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@
-CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
-CXX = @CXX@
-CXXCPP = @CXXCPP@
-CXXDEPMODE = @CXXDEPMODE@
-CXXFLAGS = @CXXFLAGS@
-CXXTEST = @CXXTEST@
-CXXTESTGEN = @CXXTESTGEN@
-CYGPATH_W = @CYGPATH_W@
-DEFS = @DEFS@
-DEPDIR = @DEPDIR@
-DLLTOOL = @DLLTOOL@
-DOXYGEN = @DOXYGEN@
-DSYMUTIL = @DSYMUTIL@
-DUMPBIN = @DUMPBIN@
-ECHO_C = @ECHO_C@
-ECHO_N = @ECHO_N@
-ECHO_T = @ECHO_T@
-EGREP = @EGREP@
-EXEEXT = @EXEEXT@
-FGREP = @FGREP@
-GREP = @GREP@
-HAVE_CXXTESTGEN_FALSE = @HAVE_CXXTESTGEN_FALSE@
-HAVE_CXXTESTGEN_TRUE = @HAVE_CXXTESTGEN_TRUE@
-INSTALL_DATA = @INSTALL_DATA@
-INSTALL_PROGRAM = @INSTALL_PROGRAM@
-INSTALL_SCRIPT = @INSTALL_SCRIPT@
-INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@
-LD = @LD@
-LDFLAGS = @LDFLAGS@
-LEX = @LEX@
-LEXLIB = @LEXLIB@
-LEX_OUTPUT_ROOT = @LEX_OUTPUT_ROOT@
-LIBOBJS = @LIBOBJS@
-LIBS = @LIBS@
-LIBTOOL = @LIBTOOL@
-LIPO = @LIPO@
-LN_S = @LN_S@
-LTLIBOBJS = @LTLIBOBJS@
-MAKEINFO = @MAKEINFO@
-NM = @NM@
-NMEDIT = @NMEDIT@
-OBJDUMP = @OBJDUMP@
-OBJEXT = @OBJEXT@
-OTOOL = @OTOOL@
-OTOOL64 = @OTOOL64@
-PACKAGE = @PACKAGE@
-PACKAGE_BUGREPORT = @PACKAGE_BUGREPORT@
-PACKAGE_NAME = @PACKAGE_NAME@
-PACKAGE_STRING = @PACKAGE_STRING@
-PACKAGE_TARNAME = @PACKAGE_TARNAME@
-PACKAGE_URL = @PACKAGE_URL@
-PACKAGE_VERSION = @PACKAGE_VERSION@
-PATH_SEPARATOR = @PATH_SEPARATOR@
-PERL = @PERL@
-RANLIB = @RANLIB@
-SED = @SED@
-SET_MAKE = @SET_MAKE@
-SHELL = @SHELL@
-STRIP = @STRIP@
-TEST_CPPFLAGS = @TEST_CPPFLAGS@
-TEST_CXXFLAGS = @TEST_CXXFLAGS@
-TEST_LDFLAGS = @TEST_LDFLAGS@
-VERSION = @VERSION@
-YACC = @YACC@
-YFLAGS = @YFLAGS@
-ac_ct_CC = @ac_ct_CC@
-ac_ct_CXX = @ac_ct_CXX@
-ac_ct_DUMPBIN = @ac_ct_DUMPBIN@
-am__fastdepCC_FALSE = @am__fastdepCC_FALSE@
-am__fastdepCC_TRUE = @am__fastdepCC_TRUE@
-am__fastdepCXX_FALSE = @am__fastdepCXX_FALSE@
-am__fastdepCXX_TRUE = @am__fastdepCXX_TRUE@
-am__include = @am__include@
-am__leading_dot = @am__leading_dot@
-am__quote = @am__quote@
-am__tar = @am__tar@
-am__untar = @am__untar@
-bindir = @bindir@
-build = @build@
-build_alias = @build_alias@
-build_cpu = @build_cpu@
-build_os = @build_os@
-build_vendor = @build_vendor@
-datadir = @datadir@
-datarootdir = @datarootdir@
-docdir = @docdir@
-dvidir = @dvidir@
-exec_prefix = @exec_prefix@
-host = @host@
-host_alias = @host_alias@
-host_cpu = @host_cpu@
-host_os = @host_os@
-host_vendor = @host_vendor@
-htmldir = @htmldir@
-includedir = @includedir@
-infodir = @infodir@
-install_sh = @install_sh@
-libdir = @libdir@
-libexecdir = @libexecdir@
-localedir = @localedir@
-localstatedir = @localstatedir@
-lt_ECHO = @lt_ECHO@
-mandir = @mandir@
-mkdir_p = @mkdir_p@
-oldincludedir = @oldincludedir@
-pdfdir = @pdfdir@
-prefix = @prefix@
-program_transform_name = @program_transform_name@
-psdir = @psdir@
-sbindir = @sbindir@
-sharedstatedir = @sharedstatedir@
-sysconfdir = @sysconfdir@
-target = @target@
-target_alias = @target_alias@
-target_cpu = @target_cpu@
-target_os = @target_os@
-target_vendor = @target_vendor@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
-noinst_LTLIBRARIES = libparsercvc.la
-libparsercvc_la_SOURCES = \
-       CvcLexer.g \
-       CvcParser.g \
-       AntlrCvcLexer.hpp \
-       AntlrCvcLexer.cpp \
-       AntlrCvcParser.hpp \
-       AntlrCvcParser.cpp   
-
-BUILT_SOURCES = \
-       AntlrCvcLexer.hpp \
-       AntlrCvcLexer.cpp \
-       AntlrCvcParser.hpp \
-       AntlrCvcParser.cpp 
-
-all: $(BUILT_SOURCES)
-       $(MAKE) $(AM_MAKEFLAGS) all-am
-
-.SUFFIXES:
-.SUFFIXES: .cpp .lo .o .obj
-$(srcdir)/Makefile.in:  $(srcdir)/Makefile.am  $(am__configure_deps)
-       @for dep in $?; do \
-         case '$(am__configure_deps)' in \
-           *$$dep*) \
-             cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh \
-               && exit 0; \
-             exit 1;; \
-         esac; \
-       done; \
-       echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign  src/parser/cvc/Makefile'; \
-       cd $(top_srcdir) && \
-         $(AUTOMAKE) --foreign  src/parser/cvc/Makefile
-.PRECIOUS: Makefile
-Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status
-       @case '$?' in \
-         *config.status*) \
-           cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \
-         *) \
-           echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \
-           cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \
-       esac;
-
-$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES)
-       cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
-
-$(top_srcdir)/configure:  $(am__configure_deps)
-       cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
-$(ACLOCAL_M4):  $(am__aclocal_m4_deps)
-       cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
-
-clean-noinstLTLIBRARIES:
-       -test -z "$(noinst_LTLIBRARIES)" || rm -f $(noinst_LTLIBRARIES)
-       @list='$(noinst_LTLIBRARIES)'; for p in $$list; do \
-         dir="`echo $$p | sed -e 's|/[^/]*$$||'`"; \
-         test "$$dir" != "$$p" || dir=.; \
-         echo "rm -f \"$${dir}/so_locations\""; \
-         rm -f "$${dir}/so_locations"; \
-       done
-libparsercvc.la: $(libparsercvc_la_OBJECTS) $(libparsercvc_la_DEPENDENCIES) 
-       $(CXXLINK)  $(libparsercvc_la_LDFLAGS) $(libparsercvc_la_OBJECTS) $(libparsercvc_la_LIBADD) $(LIBS)
-
-mostlyclean-compile:
-       -rm -f *.$(OBJEXT)
-
-distclean-compile:
-       -rm -f *.tab.c
-
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcLexer.Plo@am__quote@
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcParser.Plo@am__quote@
-
-.cpp.o:
-@am__fastdepCXX_TRUE@  if $(CXXCOMPILE) -MT $@ -MD -MP -MF "$(DEPDIR)/$*.Tpo" -c -o $@ $<; \
-@am__fastdepCXX_TRUE@  then mv -f "$(DEPDIR)/$*.Tpo" "$(DEPDIR)/$*.Po"; else rm -f "$(DEPDIR)/$*.Tpo"; exit 1; fi
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@     source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@     DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
-@am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ $<
-
-.cpp.obj:
-@am__fastdepCXX_TRUE@  if $(CXXCOMPILE) -MT $@ -MD -MP -MF "$(DEPDIR)/$*.Tpo" -c -o $@ `$(CYGPATH_W) '$<'`; \
-@am__fastdepCXX_TRUE@  then mv -f "$(DEPDIR)/$*.Tpo" "$(DEPDIR)/$*.Po"; else rm -f "$(DEPDIR)/$*.Tpo"; exit 1; fi
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@     source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@     DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
-@am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ `$(CYGPATH_W) '$<'`
-
-.cpp.lo:
-@am__fastdepCXX_TRUE@  if $(LTCXXCOMPILE) -MT $@ -MD -MP -MF "$(DEPDIR)/$*.Tpo" -c -o $@ $<; \
-@am__fastdepCXX_TRUE@  then mv -f "$(DEPDIR)/$*.Tpo" "$(DEPDIR)/$*.Plo"; else rm -f "$(DEPDIR)/$*.Tpo"; exit 1; fi
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@     source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@     DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
-@am__fastdepCXX_FALSE@ $(LTCXXCOMPILE) -c -o $@ $<
-
-mostlyclean-libtool:
-       -rm -f *.lo
-
-clean-libtool:
-       -rm -rf .libs _libs
-
-distclean-libtool:
-       -rm -f libtool
-uninstall-info-am:
-
-ID: $(HEADERS) $(SOURCES) $(LISP) $(TAGS_FILES)
-       list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
-       unique=`for i in $$list; do \
-           if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
-         done | \
-         $(AWK) '    { files[$$0] = 1; } \
-              END { for (i in files) print i; }'`; \
-       mkid -fID $$unique
-tags: TAGS
-
-TAGS:  $(HEADERS) $(SOURCES)  $(TAGS_DEPENDENCIES) \
-               $(TAGS_FILES) $(LISP)
-       tags=; \
-       here=`pwd`; \
-       list='$(SOURCES) $(HEADERS)  $(LISP) $(TAGS_FILES)'; \
-       unique=`for i in $$list; do \
-           if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
-         done | \
-         $(AWK) '    { files[$$0] = 1; } \
-              END { for (i in files) print i; }'`; \
-       if test -z "$(ETAGS_ARGS)$$tags$$unique"; then :; else \
-         test -n "$$unique" || unique=$$empty_fix; \
-         $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \
-           $$tags $$unique; \
-       fi
-ctags: CTAGS
-CTAGS:  $(HEADERS) $(SOURCES)  $(TAGS_DEPENDENCIES) \
-               $(TAGS_FILES) $(LISP)
-       tags=; \
-       here=`pwd`; \
-       list='$(SOURCES) $(HEADERS)  $(LISP) $(TAGS_FILES)'; \
-       unique=`for i in $$list; do \
-           if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
-         done | \
-         $(AWK) '    { files[$$0] = 1; } \
-              END { for (i in files) print i; }'`; \
-       test -z "$(CTAGS_ARGS)$$tags$$unique" \
-         || $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \
-            $$tags $$unique
-
-GTAGS:
-       here=`$(am__cd) $(top_builddir) && pwd` \
-         && cd $(top_srcdir) \
-         && gtags -i $(GTAGS_ARGS) $$here
-
-distclean-tags:
-       -rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags
-
-distdir: $(DISTFILES)
-       @srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`; \
-       topsrcdirstrip=`echo "$(top_srcdir)" | sed 's|.|.|g'`; \
-       list='$(DISTFILES)'; for file in $$list; do \
-         case $$file in \
-           $(srcdir)/*) file=`echo "$$file" | sed "s|^$$srcdirstrip/||"`;; \
-           $(top_srcdir)/*) file=`echo "$$file" | sed "s|^$$topsrcdirstrip/|$(top_builddir)/|"`;; \
-         esac; \
-         if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \
-         dir=`echo "$$file" | sed -e 's,/[^/]*$$,,'`; \
-         if test "$$dir" != "$$file" && test "$$dir" != "."; then \
-           dir="/$$dir"; \
-           $(mkdir_p) "$(distdir)$$dir"; \
-         else \
-           dir=''; \
-         fi; \
-         if test -d $$d/$$file; then \
-           if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \
-             cp -pR $(srcdir)/$$file $(distdir)$$dir || exit 1; \
-           fi; \
-           cp -pR $$d/$$file $(distdir)$$dir || exit 1; \
-         else \
-           test -f $(distdir)/$$file \
-           || cp -p $$d/$$file $(distdir)/$$file \
-           || exit 1; \
-         fi; \
-       done
-check-am: all-am
-check: $(BUILT_SOURCES)
-       $(MAKE) $(AM_MAKEFLAGS) check-am
-all-am: Makefile $(LTLIBRARIES)
-installdirs:
-install: $(BUILT_SOURCES)
-       $(MAKE) $(AM_MAKEFLAGS) install-am
-install-exec: install-exec-am
-install-data: install-data-am
-uninstall: uninstall-am
-
-install-am: all-am
-       @$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am
-
-installcheck: installcheck-am
-install-strip:
-       $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
-         install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
-         `test -z '$(STRIP)' || \
-           echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install
-mostlyclean-generic:
-
-clean-generic:
-
-distclean-generic:
-       -test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES)
-
-maintainer-clean-generic:
-       @echo "This command is intended for maintainers to use"
-       @echo "it deletes files that may require special tools to rebuild."
-       -test -z "$(BUILT_SOURCES)" || rm -f $(BUILT_SOURCES)
-clean: clean-am
-
-clean-am: clean-generic clean-libtool clean-noinstLTLIBRARIES \
-       mostlyclean-am
-
-distclean: distclean-am
-       -rm -rf ./$(DEPDIR)
-       -rm -f Makefile
-distclean-am: clean-am distclean-compile distclean-generic \
-       distclean-libtool distclean-tags
-
-dvi: dvi-am
-
-dvi-am:
-
-html: html-am
-
-info: info-am
-
-info-am:
-
-install-data-am:
-
-install-exec-am:
-
-install-info: install-info-am
-
-install-man:
-
-installcheck-am:
-
-maintainer-clean: maintainer-clean-am
-       -rm -rf ./$(DEPDIR)
-       -rm -f Makefile
-maintainer-clean-am: distclean-am maintainer-clean-generic
-
-mostlyclean: mostlyclean-am
-
-mostlyclean-am: mostlyclean-compile mostlyclean-generic \
-       mostlyclean-libtool
-
-pdf: pdf-am
-
-pdf-am:
-
-ps: ps-am
-
-ps-am:
-
-uninstall-am: uninstall-info-am
-
-.PHONY: CTAGS GTAGS all all-am check check-am clean clean-generic \
-       clean-libtool clean-noinstLTLIBRARIES ctags distclean \
-       distclean-compile distclean-generic distclean-libtool \
-       distclean-tags distdir dvi dvi-am html html-am info info-am \
-       install install-am install-data install-data-am install-exec \
-       install-exec-am install-info install-info-am install-man \
-       install-strip installcheck installcheck-am installdirs \
-       maintainer-clean maintainer-clean-generic mostlyclean \
-       mostlyclean-compile mostlyclean-generic mostlyclean-libtool \
-       pdf pdf-am ps ps-am tags uninstall uninstall-am \
-       uninstall-info-am
-
-
-AntlrCvcLexer.hpp: CvcLexer.g
-AntlrCvcLexer.cpp: CvcLexer.g
-       $(ANTLR) @srcdir@/CvcLexer.g
-
-AntlrCvcParser.hpp: CvcParser.g AntlrCvcLexer.cpp
-AntlrCvcParser.cpp: CvcParser.g AntlrCvcLexer.cpp
-       $(ANTLR) @srcdir@/CvcParser.g
-# Tell versions [3.59,3.63) of GNU make to not export all variables.
-# Otherwise a system limit (for SysV at least) may be exceeded.
-.NOEXPORT:

diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 59782de7e73a1fd9d44f6df4248e5bb7fae27c44..35b5bafd787ba489025312b254bd9335d5dff6f2 100644 (file)
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -10,19 +10,17 @@ libparsersmt_la_SOURCES = \
        AntlrSmtLexer.hpp \
        AntlrSmtLexer.cpp \
        AntlrSmtParser.hpp \
-       AntlrSmtParser.cpp   
+       AntlrSmtParser.cpp 
 
 BUILT_SOURCES = \
        AntlrSmtLexer.hpp \
        AntlrSmtLexer.cpp \
        AntlrSmtParser.hpp \
        AntlrSmtParser.cpp 
+CLEAN_FILES = $(BUILT_SOURCES)
 
+AntlrSmtLexer.cpp AntlrSmtLexer.hpp: SmtLexer.g
+       $(ANTLR) -o "@builddir@" "@srcdir@/SmtLexer.g"
 
-AntlrSmtLexer.hpp: SmtLexer.g
-AntlrSmtLexer.cpp: SmtLexer.g
-       $(ANTLR) @srcdir@/SmtLexer.g
-
-AntlrSmtParser.hpp: SmtParser.g AntlrSmtLexer.cpp
-AntlrSmtParser.cpp: SmtParser.g AntlrSmtLexer.cpp
-       $(ANTLR) @srcdir@/SmtParser.g
+AntlrSmtParser.cpp AntlrSmtParser.hpp: SmtParser.g
+       $(ANTLR) -o "@builddir@" "@srcdir@/SmtParser.g"

diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 87108cb5cfce49914a1b86808d46b238f93ab77f..4071197ad567ab69916212856af830224e0eb1b7 100644 (file)
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -4,6 +4,7 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libprop.la
 
-libprop_la_SOURCES =
+libprop_la_SOURCES = \
+       prop_engine.cpp
 
 SUBDIRS = minisat

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3e33cc8af1ce944aa598b21b071dc67524fe88a2..ab3fc816a9281e23a143e32e1723fb6673065230 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** cvc4.h
+/** smt_engine.h
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/command.cpp b/src/util/command.cpp
index 9611045858c3ffb4486fb1d8bb17dff5f9513556..190f794da481b1aebf12b5df701d998841aaf1d9 100644 (file)
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -10,16 +10,16 @@
 #include "expr/expr.h"
 #include "util/result.h"
 
-namespace std {
+using namespace std;
+
+namespace CVC4 {
+
 ostream& operator<<(ostream& out, const CVC4::Command& c) {
   c.toString(out);
   return out;
 }
-}
-
-namespace CVC4 {
 
-EmptyCommand::EmptyCommand(std::string name) :
+EmptyCommand::EmptyCommand(string name) :
   d_name(name) {
 }
 

diff --git a/src/util/command.h b/src/util/command.h
index 3d738ba45851b03696fc66dc7d391ed17fdb8f07..501aa31e0d213deafc34a9eddd685928d143c7f7 100644 (file)
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -23,12 +23,10 @@ namespace CVC4 {
   class Expr;
 }/* CVC4 namespace */
 
-namespace std {
-  std::ostream& operator<<(std::ostream&, const CVC4::Command&) CVC4_PUBLIC;
-}
-
 namespace CVC4 {
 
+std::ostream& operator<<(std::ostream&, const CVC4::Command&) CVC4_PUBLIC;
+
 class CVC4_PUBLIC Command {
 public:
   virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;

diff --git a/src/util/exception.h b/src/util/exception.h
index 76eabe67e70321e4566f2bb9ee669328b12bc67c..164cda8b5765de5a65025e9b1cd7f50fa571ecf3 100644 (file)
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -8,6 +8,8 @@
  ** information.
  **
  ** Exception class.
+ **
+ ** As many paragraphs as you like.
  **/
 
 #ifndef __CVC4__EXCEPTION_H

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 0f9df5e2f4b2b865b591a00ac1fb02decde94590..acac06965402223264dc1b99db83a9e170628bdc 100644 (file)
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -12,7 +12,8 @@ libdummy_la_SOURCES = expr/expr_black.cpp
 libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
 
 $(TESTS:%=%.cpp): %.cpp: %.h
-       $(CXXTESTGEN) --have-eh --have-std --error-printer -o $@ $<
+       mkdir -p `dirname "$@"`
+       $(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<"
 $(TESTS): %: %.cpp
 #      get these in here somehow
 #      $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)

diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h
index 97746d1c457f2ee47eda2f2362bcda51f1a8c90c..5f1deee8acaf25a9f503c11f0998dc5f5281aee9 100644 (file)
--- a/test/unit/expr/expr_black.h
+++ b/test/unit/expr/expr_black.h
@@ -2,7 +2,7 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 
 using namespace CVC4;
 

diff --git a/test/unit/expr/expr_white.h b/test/unit/expr/expr_white.h
index b6bfdd394b29a25d32577bee91630da8b4b0e06b..3da360126e64545e23510ca7623c88ed8c730f4a 100644 (file)
--- a/test/unit/expr/expr_white.h
+++ b/test/unit/expr/expr_white.h
@@ -2,7 +2,7 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 
 using namespace CVC4;