From 0201aa29bea8467e5cc07f2d0af68a4da3e86ec1 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 17 Nov 2009 16:40:19 +0000 Subject: [PATCH] fixes/redesign of source layout from meeting --- Makefile.am | 2 + src/Makefile.am | 18 +-- src/core/Makefile.am | 5 +- src/{include => core}/assert.h | 0 src/{include => core}/attr_type.h | 2 +- src/{include => core}/command.h | 0 src/{include => core}/context.h | 0 src/{include => core}/debug.h | 0 src/{include => core}/decision_engine.h | 2 +- src/{include => core}/exception.h | 0 src/core/expr.cpp | 6 +- src/{include => core}/expr_attribute.h | 6 +- src/core/expr_builder.cpp | 152 +++++++++++++++++++++++ src/{include => core}/expr_builder.h | 23 ++-- src/core/expr_manager.cpp | 70 +++++------ src/{include => core}/expr_manager.h | 4 +- src/core/expr_value.cpp | 19 ++- src/{include => core}/expr_value.h | 6 +- src/{include => core}/kind.h | 2 + src/{include => core}/literal.h | 0 src/{include => core}/model.h | 0 src/{include => core}/parser.h | 4 +- src/{include => core}/parser_exception.h | 2 +- src/{include => core}/prop_engine.h | 6 +- src/{include => core}/prover.h | 6 +- src/{include => core}/result.h | 0 src/{include => core}/sat.h | 0 src/{include => core}/theory.h | 4 +- src/{include => core}/theory_engine.h | 0 src/{include => core}/unique_id.h | 0 src/include/{vc.h => cvc4.h} | 2 +- src/include/{expr.h => cvc4_expr.h} | 2 + src/parser/Makefile.am | 3 +- src/parser/parser_state.h | 2 +- src/sat/Makefile.am | 3 +- 35 files changed, 266 insertions(+), 85 deletions(-) rename src/{include => core}/assert.h (100%) rename src/{include => core}/attr_type.h (96%) rename src/{include => core}/command.h (100%) rename src/{include => core}/context.h (100%) rename src/{include => core}/debug.h (100%) rename src/{include => core}/decision_engine.h (97%) rename src/{include => core}/exception.h (100%) rename src/{include => core}/expr_attribute.h (96%) create mode 100644 src/core/expr_builder.cpp rename src/{include => core}/expr_builder.h (89%) rename src/{include => core}/expr_manager.h (97%) rename src/{include => core}/expr_value.h (89%) rename src/{include => core}/kind.h (96%) rename src/{include => core}/literal.h (100%) rename src/{include => core}/model.h (100%) rename src/{include => core}/parser.h (97%) rename src/{include => core}/parser_exception.h (97%) rename src/{include => core}/prop_engine.h (91%) rename src/{include => core}/prover.h (97%) rename src/{include => core}/result.h (100%) rename src/{include => core}/sat.h (100%) rename src/{include => core}/theory.h (97%) rename src/{include => core}/theory_engine.h (100%) rename src/{include => core}/unique_id.h (100%) rename src/include/{vc.h => cvc4.h} (97%) rename src/include/{expr.h => cvc4_expr.h} (98%) diff --git a/Makefile.am b/Makefile.am index 451ef0e3a..5b0f8d11a 100644 --- a/Makefile.am +++ b/Makefile.am @@ -1,3 +1,5 @@ +AM_CXXFLAGS = -Wall + AUTOMAKE_OPTIONS = foreign ACLOCAL_AMFLAGS = -I config diff --git a/src/Makefile.am b/src/Makefile.am index 3f0d0b381..7b2141da3 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -1,4 +1,4 @@ -INCLUDES = -I@srcdir@/include +INCLUDES = -I@srcdir@/include -I@srcdir@ SUBDIRS = core parser sat @@ -10,17 +10,5 @@ libcvc4_la_LIBADD = \ sat/minisat/libminisat.a EXTRA_DIST = \ - include/assert.h \ - include/attr_type.h \ - include/command.h - include/expr_attribute.h \ - include/expr_builder.h \ - include/expr.h \ - include/expr_manager.h \ - include/expr_value.h \ - include/kind.h \ - include/parser.h \ - include/sat.h \ - include/unique_id.h \ - include/vc.h - + include/cvc4.h \ + include/cvc4_expr.h diff --git a/src/core/Makefile.am b/src/core/Makefile.am index 043882f36..d26a7483d 100644 --- a/src/core/Makefile.am +++ b/src/core/Makefile.am @@ -1,7 +1,10 @@ -INCLUDES = -I@srcdir@/../include +INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CXXFLAGS = -Wall noinst_LIBRARIES = libcore.a libcore_a_SOURCES = \ expr.cpp \ + expr_builder.cpp \ + expr_manager.cpp \ expr_value.cpp diff --git a/src/include/assert.h b/src/core/assert.h similarity index 100% rename from src/include/assert.h rename to src/core/assert.h diff --git a/src/include/attr_type.h b/src/core/attr_type.h similarity index 96% rename from src/include/attr_type.h rename to src/core/attr_type.h index d24385f8e..d76bd742d 100644 --- a/src/include/attr_type.h +++ b/src/core/attr_type.h @@ -12,7 +12,7 @@ #ifndef __CVC4_ATTR_TYPE_H #define __CVC4_ATTR_TYPE_H -#include "expr_attribute.h" +#include "core/expr_attribute.h" namespace CVC4 { diff --git a/src/include/command.h b/src/core/command.h similarity index 100% rename from src/include/command.h rename to src/core/command.h diff --git a/src/include/context.h b/src/core/context.h similarity index 100% rename from src/include/context.h rename to src/core/context.h diff --git a/src/include/debug.h b/src/core/debug.h similarity index 100% rename from src/include/debug.h rename to src/core/debug.h diff --git a/src/include/decision_engine.h b/src/core/decision_engine.h similarity index 97% rename from src/include/decision_engine.h rename to src/core/decision_engine.h index ec0172535..81d820eaa 100644 --- a/src/include/decision_engine.h +++ b/src/core/decision_engine.h @@ -12,7 +12,7 @@ #ifndef __CVC4_DECISION_ENGINE_H #define __CVC4_DECISION_ENGINE_H -#include "literal.h" +#include "core/literal.h" namespace CVC4 { diff --git a/src/include/exception.h b/src/core/exception.h similarity index 100% rename from src/include/exception.h rename to src/core/exception.h diff --git a/src/core/expr.cpp b/src/core/expr.cpp index cdc7e6775..5e422f349 100644 --- a/src/core/expr.cpp +++ b/src/core/expr.cpp @@ -10,9 +10,9 @@ ** Reference-counted encapsulation of a pointer to an expression. **/ -#include "expr.h" -#include "expr_value.h" -#include "expr_builder.h" +#include "cvc4_expr.h" +#include "core/expr_value.h" +#include "core/expr_builder.h" namespace CVC4 { diff --git a/src/include/expr_attribute.h b/src/core/expr_attribute.h similarity index 96% rename from src/include/expr_attribute.h rename to src/core/expr_attribute.h index 77700096e..b00882478 100644 --- a/src/include/expr_attribute.h +++ b/src/core/expr_attribute.h @@ -15,9 +15,9 @@ // TODO WARNING this file needs work ! #include -#include "config.h" -#include "context.h" -#include "expr.h" +#include "core/config.h" +#include "core/context.h" +#include "core/cvc4_expr.h" namespace CVC4 { diff --git a/src/core/expr_builder.cpp b/src/core/expr_builder.cpp new file mode 100644 index 000000000..6491b7d44 --- /dev/null +++ b/src/core/expr_builder.cpp @@ -0,0 +1,152 @@ +/********************* -*- C++ -*- */ +/** expr_builder.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. + ** + **/ + +#include "core/expr_builder.h" +#include "core/expr_manager.h" +#include "core/expr_value.h" + +using namespace std; + +namespace CVC4 { + +ExprBuilder::ExprBuilder() : d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {} + +ExprBuilder::ExprBuilder(Kind k) : d_em(ExprManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) {} + +ExprBuilder::ExprBuilder(const Expr& e) : d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { + ExprValue *v = e->inc(); + d_children.u_arr[0] = v; +} + +ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), d_nchildren(eb.d_nchildren) { + cvc4assert(!d_used); + + if(d_nchildren > nchild_thresh) { + d_children.u_vec = new vector(); + d_children.u_vec->reserve(d_nchildren + 5); + copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), back_inserter(*d_children.u_vec)); + } else { + iterator j = d_children.u_arr; + for(iterator i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j) + *j = i->inc(); + } +} + +ExprBuilder::ExprBuilder(ExprManager* em) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) { +} + +ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) { +} + +ExprBuilder::ExprBuilder(ExprManager* em, const Expr&) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { + ExprValue *v = e->inc(); + d_children.u_arr[0] = v; +} + +ExprBuilder::~ExprBuilder() { + if(d_nchildren > nchild_thresh) { + delete d_children.u_vec; + } else { + for(iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) { + *i + } + } +} + +// Compound expression constructors +ExprBuilder& ExprBuilder::eqExpr(const Expr& right) { + if(d_kind != UNDEFINED_KIND && d_kind != EQUAL) + collapse(); + d_kind = EQUAL; + return *this; +} + +ExprBuilder& ExprBuilder::notExpr() { +} + +// avoid double-negatives +ExprBuilder& ExprBuilder::negate() { +} + +ExprBuilder& ExprBuilder::andExpr(const Expr& right) { +} + +ExprBuilder& ExprBuilder::orExpr(const Expr& right) { +} + +ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) { +} + +ExprBuilder& ExprBuilder::iffExpr(const Expr& right) { +} + +ExprBuilder& ExprBuilder::impExpr(const Expr& right) { +} + +ExprBuilder& ExprBuilder::xorExpr(const Expr& right) { +} + +ExprBuilder& ExprBuilder::skolemExpr(int i) { +} + +ExprBuilder& ExprBuilder::substExpr(const std::vector& oldTerms, + const std::vector& newTerms) { +} + +// "Stream" expression constructor syntax +ExprBuilder& ExprBuilder::operator<<(const Kind& op) { +} + +ExprBuilder& ExprBuilder::operator<<(const Expr& child) { +} + +template +ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) { +} + +void ExprBuilder::addChild(const Expr& e) { + if(d_nchildren == nchild_thresh) { + vector* v = new vector(); + v->reserve(nchild_thresh + 5); + + } + return *this; +} + +void ExprBuilder::collapse() { + if(d_nchildren == nchild_thresh) { + vector* v = new vector(); + v->reserve(nchild_thresh + 5); + + } + return *this; +} + +// not const +ExprBuilder::operator Expr() { +} + +AndExprBuilder ExprBuilder::operator&&(Expr) { +} + +OrExprBuilder ExprBuilder::operator||(Expr) { +} + +PlusExprBuilder ExprBuilder::operator+ (Expr) { +} + +PlusExprBuilder ExprBuilder::operator- (Expr) { +} + +MultExprBuilder ExprBuilder::operator* (Expr) { +} + +} /* CVC4 namespace */ diff --git a/src/include/expr_builder.h b/src/core/expr_builder.h similarity index 89% rename from src/include/expr_builder.h rename to src/core/expr_builder.h index a95ecb2e3..fa08a3149 100644 --- a/src/include/expr_builder.h +++ b/src/core/expr_builder.h @@ -13,8 +13,8 @@ #define __CVC4_EXPR_BUILDER_H #include -#include "expr_manager.h" -#include "kind.h" +#include "core/expr_manager.h" +#include "core/kind.h" namespace CVC4 { @@ -29,26 +29,35 @@ class ExprBuilder { Kind d_kind; - // TODO: store some flags here and install into attribute map when - // the expr is created? (we'd have to do that since we don't know - // it's hash code yet) - // initially false, when you extract the Expr this is set and you can't // extract another bool d_used; + static const unsigned nchild_thresh = 10; + unsigned d_nchildren; union { - ExprValue* u_arr[10]; + ExprValue* u_arr[nchild_thresh]; std::vector* u_vec; } d_children; + void addChild(); + void collapse(); + public: ExprBuilder(); + ExprBuilder(Kind k); ExprBuilder(const Expr&); ExprBuilder(const ExprBuilder&); + ExprBuilder(ExprManager*); + ExprBuilder(ExprManager*, Kind k); + ExprBuilder(ExprManager*, const Expr&); + ExprBuilder(ExprManager*, const ExprBuilder&); + + ~ExprBuilder(); + // Compound expression constructors ExprBuilder& eqExpr(const Expr& right); ExprBuilder& notExpr(); diff --git a/src/core/expr_manager.cpp b/src/core/expr_manager.cpp index c18fd9652..90f10d8f7 100644 --- a/src/core/expr_manager.cpp +++ b/src/core/expr_manager.cpp @@ -10,43 +10,43 @@ ** Expression manager implementation. **/ -#include -#include "expr.h" -#include "kind.h" +#include "core/expr_builder.h" +#include "core/expr_manager.h" +#include "core/cvc4_expr.h" namespace CVC4 { -class ExprManager { - static __thread ExprManager* s_current; - -public: - static ExprManager* currentEM() { return s_current; } - - // general expression-builders - Expr mkExpr(Kind kind); - Expr mkExpr(Kind kind, Expr child1); - Expr mkExpr(Kind kind, Expr child1, Expr child2); - Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); - Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); - Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); - // N-ary version - Expr mkExpr(Kind kind, std::vector children); - - // TODO: these use the current EM (but must be renamed) - /* - static Expr mkExpr(Kind kind) - { currentEM()->mkExpr(kind); } - static Expr mkExpr(Kind kind, Expr child1); - { currentEM()->mkExpr(kind, child1); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2); - { currentEM()->mkExpr(kind, child1, child2); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); - { currentEM()->mkExpr(kind, child1, child2, child3); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); - { currentEM()->mkExpr(kind, child1, child2, child3, child4); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); - { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); } - */ -}; +__thread ExprManager* ExprManager::s_current = 0; + +// general expression-builders + +Expr ExprManager::mkExpr(Kind kind) { + return ExprBuilder(this, kind); +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1) { + return ExprBuilder(this, kind) << child1; +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) { + return ExprBuilder(this, kind) << child1 << child2; +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) { + return ExprBuilder(this, kind) << child1 << child2 << child3; +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4) { + return ExprBuilder(this, kind) << child1 << child2 << child3 << child4; +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5) { + return ExprBuilder(this, kind) << child1 << child2 << child3 << child4 << child5; +} + +// N-ary version +Expr ExprManager::mkExpr(Kind kind, std::vector children) { + return ExprBuilder(this, kind).append(children); +} } /* CVC4 namespace */ diff --git a/src/include/expr_manager.h b/src/core/expr_manager.h similarity index 97% rename from src/include/expr_manager.h rename to src/core/expr_manager.h index 59a3eb7a3..048250485 100644 --- a/src/include/expr_manager.h +++ b/src/core/expr_manager.h @@ -13,8 +13,8 @@ #define __CVC4_EXPR_MANAGER_H #include -#include "expr.h" -#include "kind.h" +#include "cvc4_expr.h" +#include "core/kind.h" namespace CVC4 { diff --git a/src/core/expr_value.cpp b/src/core/expr_value.cpp index b42773482..ce4177a09 100644 --- a/src/core/expr_value.cpp +++ b/src/core/expr_value.cpp @@ -14,7 +14,7 @@ ** reference count on ExprValue instances and **/ -#include "expr_value.h" +#include "core/expr_value.h" namespace CVC4 { @@ -27,6 +27,23 @@ uint64_t ExprValue::hash() const { return hash; } +ExprValue* ExprValue::inc() { + // FIXME multithreading + if(d_rc < MAX_RC) + ++d_rc; + return this; +} + +ExprValue* ExprValue::dec() { + // FIXME multithreading + if(d_rc < MAX_RC) + if(--d_rc == 0) { + // FIXME gc + return 0; + } + return this; +} + ExprValue::iterator ExprValue::begin() { return d_children; } diff --git a/src/include/expr_value.h b/src/core/expr_value.h similarity index 89% rename from src/include/expr_value.h rename to src/core/expr_value.h index ea14c3fa7..5f90533ed 100644 --- a/src/include/expr_value.h +++ b/src/core/expr_value.h @@ -18,7 +18,7 @@ #define __CVC4_EXPR_VALUE_H #include -#include "expr.h" +#include "cvc4_expr.h" namespace CVC4 { @@ -26,6 +26,10 @@ namespace CVC4 { * This is an ExprValue. */ class ExprValue { + /** Maximum reference count possible. Used for sticky + * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */ + static const unsigned MAX_RC = 255; + // this header fits into one 64-bit word /** The ID */ diff --git a/src/include/kind.h b/src/core/kind.h similarity index 96% rename from src/include/kind.h rename to src/core/kind.h index 5d99330ca..9c4e4d5ab 100644 --- a/src/include/kind.h +++ b/src/core/kind.h @@ -19,6 +19,8 @@ namespace CVC4 { // placeholder for design & development work. enum Kind { + UNDEFINED_KIND = -1, + EQUAL, AND, OR, XOR, diff --git a/src/include/literal.h b/src/core/literal.h similarity index 100% rename from src/include/literal.h rename to src/core/literal.h diff --git a/src/include/model.h b/src/core/model.h similarity index 100% rename from src/include/model.h rename to src/core/model.h diff --git a/src/include/parser.h b/src/core/parser.h similarity index 97% rename from src/include/parser.h rename to src/core/parser.h index e30b31b1c..967f20e95 100644 --- a/src/include/parser.h +++ b/src/core/parser.h @@ -13,8 +13,8 @@ #ifndef __CVC4_PARSER_H #define __CVC4_PARSER_H -#include "exception.h" -#include "lang.h" +#include "core/exception.h" +#include "core/lang.h" namespace CVC4 { diff --git a/src/include/parser_exception.h b/src/core/parser_exception.h similarity index 97% rename from src/include/parser_exception.h rename to src/core/parser_exception.h index debb75e70..18f027e44 100644 --- a/src/include/parser_exception.h +++ b/src/core/parser_exception.h @@ -13,7 +13,7 @@ #ifndef __CVC4_PARSER_EXCEPTION_H #define __CVC4_PARSER_EXCEPTION_H -#include "exception.h" +#include "core/exception.h" #include #include diff --git a/src/include/prop_engine.h b/src/core/prop_engine.h similarity index 91% rename from src/include/prop_engine.h rename to src/core/prop_engine.h index de25c5594..0febd2927 100644 --- a/src/include/prop_engine.h +++ b/src/core/prop_engine.h @@ -12,9 +12,9 @@ #ifndef __CVC4_PROP_ENGINE_H #define __CVC4_PROP_ENGINE_H -#include "expr.h" -#include "decision_engine.h" -#include "theory_engine.h" +#include "core/cvc4_expr.h" +#include "core/decision_engine.h" +#include "core/theory_engine.h" namespace CVC4 { diff --git a/src/include/prover.h b/src/core/prover.h similarity index 97% rename from src/include/prover.h rename to src/core/prover.h index de29f48c0..14eab7c03 100644 --- a/src/include/prover.h +++ b/src/core/prover.h @@ -13,9 +13,9 @@ #define __CVC4_PROVER_H #include -#include "expr.h" -#include "result.h" -#include "model.h" +#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) diff --git a/src/include/result.h b/src/core/result.h similarity index 100% rename from src/include/result.h rename to src/core/result.h diff --git a/src/include/sat.h b/src/core/sat.h similarity index 100% rename from src/include/sat.h rename to src/core/sat.h diff --git a/src/include/theory.h b/src/core/theory.h similarity index 97% rename from src/include/theory.h rename to src/core/theory.h index 935c23b08..eeaba58d1 100644 --- a/src/include/theory.h +++ b/src/core/theory.h @@ -12,8 +12,8 @@ #ifndef __CVC4_THEORY_H #define __CVC4_THEORY_H -#include "expr.h" -#include "literal.h" +#include "core/cvc4_expr.h" +#include "core/literal.h" namespace CVC4 { diff --git a/src/include/theory_engine.h b/src/core/theory_engine.h similarity index 100% rename from src/include/theory_engine.h rename to src/core/theory_engine.h diff --git a/src/include/unique_id.h b/src/core/unique_id.h similarity index 100% rename from src/include/unique_id.h rename to src/core/unique_id.h diff --git a/src/include/vc.h b/src/include/cvc4.h similarity index 97% rename from src/include/vc.h rename to src/include/cvc4.h index 845d1eb6d..109496001 100644 --- a/src/include/vc.h +++ b/src/include/cvc4.h @@ -13,7 +13,7 @@ #define __CVC4_VC_H #include "command.h" -#include "expr.h" +#include "cvc4_expr.h" /* TODO provide way of querying whether you fall into a fragment / * returning what fragment you're in */ diff --git a/src/include/expr.h b/src/include/cvc4_expr.h similarity index 98% rename from src/include/expr.h rename to src/include/cvc4_expr.h index e92ece93d..17e7f4f82 100644 --- a/src/include/expr.h +++ b/src/include/cvc4_expr.h @@ -71,6 +71,8 @@ public: const std::vector& newTerms) const; static Expr null() { return s_null; } + + friend class ExprBuilder; };/* class Expr */ } /* CVC4 namespace */ diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index a9560ab93..918ab2fb2 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -1,4 +1,5 @@ -INCLUDES = -I@srcdir@/../include +INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CXXFLAGS = -Wall noinst_LIBRARIES = libparser.a diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 6ab0ada49..f82980196 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -19,7 +19,7 @@ #include #include -#include "expr.h" +#include "cvc4_expr.h" #include "exception.h" namespace CVC4 { diff --git a/src/sat/Makefile.am b/src/sat/Makefile.am index 321507609..5051420a2 100644 --- a/src/sat/Makefile.am +++ b/src/sat/Makefile.am @@ -1,3 +1,4 @@ -INCLUDES = -I@srcdir@/../include +INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CXXFLAGS = -Wall SUBDIRS = minisat -- 2.30.2