diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-17 16:40:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-17 16:40:19 +0000 |
commit | 0201aa29bea8467e5cc07f2d0af68a4da3e86ec1 (patch) | |
tree | 548f42c4244176fb91956e9571451842fd85e482 /src | |
parent | 7293554b109742697d4d928ed7b58acadc6de947 (diff) |
fixes/redesign of source layout from meeting
Diffstat (limited to 'src')
-rw-r--r-- | src/Makefile.am | 18 | ||||
-rw-r--r-- | src/core/Makefile.am | 5 | ||||
-rw-r--r-- | src/core/assert.h (renamed from src/include/assert.h) | 0 | ||||
-rw-r--r-- | src/core/attr_type.h (renamed from src/include/attr_type.h) | 2 | ||||
-rw-r--r-- | src/core/command.h (renamed from src/include/command.h) | 0 | ||||
-rw-r--r-- | src/core/context.h (renamed from src/include/context.h) | 0 | ||||
-rw-r--r-- | src/core/debug.h (renamed from src/include/debug.h) | 0 | ||||
-rw-r--r-- | src/core/decision_engine.h (renamed from src/include/decision_engine.h) | 2 | ||||
-rw-r--r-- | src/core/exception.h (renamed from src/include/exception.h) | 0 | ||||
-rw-r--r-- | src/core/expr.cpp | 6 | ||||
-rw-r--r-- | src/core/expr_attribute.h (renamed from src/include/expr_attribute.h) | 6 | ||||
-rw-r--r-- | src/core/expr_builder.cpp | 152 | ||||
-rw-r--r-- | src/core/expr_builder.h (renamed from src/include/expr_builder.h) | 23 | ||||
-rw-r--r-- | src/core/expr_manager.cpp | 70 | ||||
-rw-r--r-- | src/core/expr_manager.h (renamed from src/include/expr_manager.h) | 4 | ||||
-rw-r--r-- | src/core/expr_value.cpp | 19 | ||||
-rw-r--r-- | src/core/expr_value.h (renamed from src/include/expr_value.h) | 6 | ||||
-rw-r--r-- | src/core/kind.h (renamed from src/include/kind.h) | 2 | ||||
-rw-r--r-- | src/core/literal.h (renamed from src/include/literal.h) | 0 | ||||
-rw-r--r-- | src/core/model.h (renamed from src/include/model.h) | 0 | ||||
-rw-r--r-- | src/core/parser.h (renamed from src/include/parser.h) | 4 | ||||
-rw-r--r-- | src/core/parser_exception.h (renamed from src/include/parser_exception.h) | 2 | ||||
-rw-r--r-- | src/core/prop_engine.h (renamed from src/include/prop_engine.h) | 6 | ||||
-rw-r--r-- | src/core/prover.h (renamed from src/include/prover.h) | 6 | ||||
-rw-r--r-- | src/core/result.h (renamed from src/include/result.h) | 0 | ||||
-rw-r--r-- | src/core/sat.h (renamed from src/include/sat.h) | 0 | ||||
-rw-r--r-- | src/core/theory.h (renamed from src/include/theory.h) | 4 | ||||
-rw-r--r-- | src/core/theory_engine.h (renamed from src/include/theory_engine.h) | 0 | ||||
-rw-r--r-- | src/core/unique_id.h (renamed from src/include/unique_id.h) | 0 | ||||
-rw-r--r-- | src/include/cvc4.h (renamed from src/include/vc.h) | 2 | ||||
-rw-r--r-- | src/include/cvc4_expr.h (renamed from src/include/expr.h) | 2 | ||||
-rw-r--r-- | src/parser/Makefile.am | 3 | ||||
-rw-r--r-- | src/parser/parser_state.h | 2 | ||||
-rw-r--r-- | src/sat/Makefile.am | 3 |
34 files changed, 264 insertions, 85 deletions
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 index a66503641..a66503641 100644 --- a/src/include/assert.h +++ b/src/core/assert.h diff --git a/src/include/attr_type.h b/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 index 944b9c621..944b9c621 100644 --- a/src/include/command.h +++ b/src/core/command.h diff --git a/src/include/context.h b/src/core/context.h index fce2f0b8d..fce2f0b8d 100644 --- a/src/include/context.h +++ b/src/core/context.h diff --git a/src/include/debug.h b/src/core/debug.h index 36942d1ae..36942d1ae 100644 --- a/src/include/debug.h +++ b/src/core/debug.h diff --git a/src/include/decision_engine.h b/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 index 792a98701..792a98701 100644 --- a/src/include/exception.h +++ b/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 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 <stdint.h> -#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<Expr>(); + 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<Expr>& oldTerms, + const std::vector<Expr>& newTerms) { +} + +// "Stream" expression constructor syntax +ExprBuilder& ExprBuilder::operator<<(const Kind& op) { +} + +ExprBuilder& ExprBuilder::operator<<(const Expr& child) { +} + +template <class Iterator> +ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) { +} + +void ExprBuilder::addChild(const Expr& e) { + if(d_nchildren == nchild_thresh) { + vector<Expr>* v = new vector<Expr>(); + v->reserve(nchild_thresh + 5); + + } + return *this; +} + +void ExprBuilder::collapse() { + if(d_nchildren == nchild_thresh) { + vector<Expr>* v = new vector<Expr>(); + 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 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 <vector> -#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<Expr>* 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 <vector> -#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<Expr> 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<Expr> children) { + return ExprBuilder(this, kind).append(children); +} } /* CVC4 namespace */ diff --git a/src/include/expr_manager.h b/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 <vector> -#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 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 <stdint.h> -#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 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 index 8b147c640..8b147c640 100644 --- a/src/include/literal.h +++ b/src/core/literal.h diff --git a/src/include/model.h b/src/core/model.h index c07b75dfa..c07b75dfa 100644 --- a/src/include/model.h +++ b/src/core/model.h diff --git a/src/include/parser.h b/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 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 <string> #include <iostream> diff --git a/src/include/prop_engine.h b/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 index de29f48c0..14eab7c03 100644 --- a/src/include/prover.h +++ b/src/core/prover.h @@ -13,9 +13,9 @@ #define __CVC4_PROVER_H #include <vector> -#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 index 50f488682..50f488682 100644 --- a/src/include/result.h +++ b/src/core/result.h diff --git a/src/include/sat.h b/src/core/sat.h index 00a94c142..00a94c142 100644 --- a/src/include/sat.h +++ b/src/core/sat.h diff --git a/src/include/theory.h b/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 index 2a0841d8d..2a0841d8d 100644 --- a/src/include/theory_engine.h +++ b/src/core/theory_engine.h diff --git a/src/include/unique_id.h b/src/core/unique_id.h index 1a6f3427a..1a6f3427a 100644 --- a/src/include/unique_id.h +++ b/src/core/unique_id.h diff --git a/src/include/vc.h b/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 index e92ece93d..17e7f4f82 100644 --- a/src/include/expr.h +++ b/src/include/cvc4_expr.h @@ -71,6 +71,8 @@ public: const std::vector<Expr>& 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 <iostream> #include <sstream> -#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 |