From c72745ec66a6328ab02350cd556a1ad82fb7d85c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 7 Dec 2009 23:14:15 +0000 Subject: big check-in of various fixes and adjustments --- src/Makefile.am | 4 +- src/context/Makefile.am | 3 +- src/expr/expr.h | 12 +- src/include/cvc4.h | 115 ----------- src/include/cvc4_expr.h | 100 --------- src/include/theory.h | 81 -------- src/parser/antlr_parser.h | 10 +- src/parser/cvc/Makefile.am | 25 +-- src/parser/cvc/Makefile.in | 502 --------------------------------------------- src/parser/smt/Makefile.am | 14 +- src/prop/Makefile.am | 3 +- src/prop/prop_engine.cpp | 0 src/smt/smt_engine.h | 2 +- src/util/command.cpp | 10 +- src/util/command.h | 6 +- src/util/exception.h | 2 + 16 files changed, 39 insertions(+), 850 deletions(-) delete mode 100644 src/include/cvc4.h delete mode 100644 src/include/cvc4_expr.h delete mode 100644 src/include/theory.h delete mode 100644 src/parser/cvc/Makefile.in create mode 100644 src/prop/prop_engine.cpp (limited to 'src') diff --git a/src/Makefile.am b/src/Makefile.am index afbb587a8..1db9d9ecf 100644 --- 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 a906d2873..d1e0d3c4b 100644 --- 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 0fcb5ea6a..a16ffee13 100644 --- 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 index bbaffabb0..000000000 --- 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 -#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 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 index 863097123..000000000 --- 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 -#include - -#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 index 47b4a2d92..000000000 --- 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 6bac079c8..0db12a0f0 100644 --- 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 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 9f548d656..2619b2dac 100644 --- 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 index 54c641bb6..000000000 --- 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 59782de7e..35b5bafd7 100644 --- 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 87108cb5c..4071197ad 100644 --- 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 index 000000000..e69de29bb diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3e33cc8af..ab3fc816a 100644 --- 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 961104585..190f794da 100644 --- 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 3d738ba45..501aa31e0 100644 --- 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 76eabe67e..164cda8b5 100644 --- 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 -- cgit v1.2.3