From: Morgan Deters Date: Tue, 26 Jan 2010 07:29:41 +0000 (+0000) Subject: fixes to build structure, util classes, lots of fixes to Node and NodeBuilder. outst... X-Git-Tag: cvc5-1.0.0~9340 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=21e01d42ed4c0b6d9fa5855c2e0cfc1a3765d14f;p=cvc5.git fixes to build structure, util classes, lots of fixes to Node and NodeBuilder. outstanding SEGVs fixed --- diff --git a/Makefile.builds.in b/Makefile.builds.in index 00551ea6f..789fb0bae 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -11,6 +11,8 @@ prefix = @prefix@ bindir = @bindir@ libdir = @libdir@ abs_builddir = @abs_builddir@ +BUILDING_STATIC = @BUILDING_STATIC@ +BUILDING_SHARED = @BUILDING_SHARED@ .PHONY: _default_build_ all _default_build_: all @@ -19,17 +21,27 @@ all: $(mkinstalldirs) "$(CURRENT_BUILD)$(bindir)" "$(CURRENT_BUILD)$(libdir)" $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "$(abs_builddir)$(libdir)" +ifeq ($(BUILDING_SHARED),1) thelibdir="$(abs_builddir)$(libdir)"; progdir="$(abs_builddir)$(bindir)"; file=cvc4; \ eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \ eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)" +endif +ifeq ($(BUILDING_STATIC),1) + install -v $(CURRENT_BUILD)/src/main/cvc4 "$(abs_builddir)$(bindir)" +endif test -e $(CURRENT_BUILD)/lib || ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib test -e $(CURRENT_BUILD)/bin || ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin mkdir -pv ".$(bindir)" ".$(libdir)" $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)" $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)" +ifeq ($(BUILDING_SHARED),1) thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; file=cvc4; \ eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \ eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)" +endif +ifeq ($(BUILDING_STATIC),1) + install -v $(CURRENT_BUILD)/src/main/cvc4 "`pwd`$(bindir)" +endif test -e lib || ln -sfv ".$(libdir)" lib test -e bin || ln -sfv ".$(bindir)" bin diff --git a/Makefile.in b/Makefile.in index 139f43cc0..c67c877a1 100644 --- a/Makefile.in +++ b/Makefile.in @@ -120,6 +120,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/configure b/configure index 16c2aa0b9..8e60591d9 100755 --- a/configure +++ b/configure @@ -713,6 +713,8 @@ mk_include CVC4_PARSER_LIBRARY_VERSION CVC4_LIBRARY_VERSION CVC4_LIBRARY_RELEASE_CODE +BUILDING_STATIC +BUILDING_SHARED ANTLR_LDFLAGS ANTLR_INCLUDES PERL @@ -5456,13 +5458,13 @@ if test "${lt_cv_nm_interface+set}" = set; then : else lt_cv_nm_interface="BSD nm" echo "int some_variable = 0;" > conftest.$ac_ext - (eval echo "\"\$as_me:5459: $ac_compile\"" >&5) + (eval echo "\"\$as_me:5461: $ac_compile\"" >&5) (eval "$ac_compile" 2>conftest.err) cat conftest.err >&5 - (eval echo "\"\$as_me:5462: $NM \\\"conftest.$ac_objext\\\"\"" >&5) + (eval echo "\"\$as_me:5464: $NM \\\"conftest.$ac_objext\\\"\"" >&5) (eval "$NM \"conftest.$ac_objext\"" 2>conftest.err > conftest.out) cat conftest.err >&5 - (eval echo "\"\$as_me:5465: output\"" >&5) + (eval echo "\"\$as_me:5467: output\"" >&5) cat conftest.out >&5 if $GREP 'External.*some_variable' conftest.out > /dev/null; then lt_cv_nm_interface="MS dumpbin" @@ -6665,7 +6667,7 @@ ia64-*-hpux*) ;; *-*-irix6*) # Find out which ABI we are using. - echo '#line 6668 "configure"' > conftest.$ac_ext + echo '#line 6670 "configure"' > conftest.$ac_ext if { { eval echo "\"\$as_me\":${as_lineno-$LINENO}: \"$ac_compile\""; } >&5 (eval $ac_compile) 2>&5 ac_status=$? @@ -8133,11 +8135,11 @@ else -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \ -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \ -e 's:$: $lt_compiler_flag:'` - (eval echo "\"\$as_me:8136: $lt_compile\"" >&5) + (eval echo "\"\$as_me:8138: $lt_compile\"" >&5) (eval "$lt_compile" 2>conftest.err) ac_status=$? cat conftest.err >&5 - echo "$as_me:8140: \$? = $ac_status" >&5 + echo "$as_me:8142: \$? = $ac_status" >&5 if (exit $ac_status) && test -s "$ac_outfile"; then # The compiler can only warn and ignore the option if not recognized # So say no if there are warnings other than the usual output. @@ -8472,11 +8474,11 @@ else -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \ -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \ -e 's:$: $lt_compiler_flag:'` - (eval echo "\"\$as_me:8475: $lt_compile\"" >&5) + (eval echo "\"\$as_me:8477: $lt_compile\"" >&5) (eval "$lt_compile" 2>conftest.err) ac_status=$? cat conftest.err >&5 - echo "$as_me:8479: \$? = $ac_status" >&5 + echo "$as_me:8481: \$? = $ac_status" >&5 if (exit $ac_status) && test -s "$ac_outfile"; then # The compiler can only warn and ignore the option if not recognized # So say no if there are warnings other than the usual output. @@ -8577,11 +8579,11 @@ else -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \ -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \ -e 's:$: $lt_compiler_flag:'` - (eval echo "\"\$as_me:8580: $lt_compile\"" >&5) + (eval echo "\"\$as_me:8582: $lt_compile\"" >&5) (eval "$lt_compile" 2>out/conftest.err) ac_status=$? cat out/conftest.err >&5 - echo "$as_me:8584: \$? = $ac_status" >&5 + echo "$as_me:8586: \$? = $ac_status" >&5 if (exit $ac_status) && test -s out/conftest2.$ac_objext then # The compiler can only warn and ignore the option if not recognized @@ -8632,11 +8634,11 @@ else -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \ -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \ -e 's:$: $lt_compiler_flag:'` - (eval echo "\"\$as_me:8635: $lt_compile\"" >&5) + (eval echo "\"\$as_me:8637: $lt_compile\"" >&5) (eval "$lt_compile" 2>out/conftest.err) ac_status=$? cat out/conftest.err >&5 - echo "$as_me:8639: \$? = $ac_status" >&5 + echo "$as_me:8641: \$? = $ac_status" >&5 if (exit $ac_status) && test -s out/conftest2.$ac_objext then # The compiler can only warn and ignore the option if not recognized @@ -11015,7 +11017,7 @@ else lt_dlunknown=0; lt_dlno_uscore=1; lt_dlneed_uscore=2 lt_status=$lt_dlunknown cat > conftest.$ac_ext <<_LT_EOF -#line 11018 "configure" +#line 11020 "configure" #include "confdefs.h" #if HAVE_DLFCN_H @@ -11111,7 +11113,7 @@ else lt_dlunknown=0; lt_dlno_uscore=1; lt_dlneed_uscore=2 lt_status=$lt_dlunknown cat > conftest.$ac_ext <<_LT_EOF -#line 11114 "configure" +#line 11116 "configure" #include "confdefs.h" #if HAVE_DLFCN_H @@ -14666,11 +14668,11 @@ else -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \ -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \ -e 's:$: $lt_compiler_flag:'` - (eval echo "\"\$as_me:14669: $lt_compile\"" >&5) + (eval echo "\"\$as_me:14671: $lt_compile\"" >&5) (eval "$lt_compile" 2>conftest.err) ac_status=$? cat conftest.err >&5 - echo "$as_me:14673: \$? = $ac_status" >&5 + echo "$as_me:14675: \$? = $ac_status" >&5 if (exit $ac_status) && test -s "$ac_outfile"; then # The compiler can only warn and ignore the option if not recognized # So say no if there are warnings other than the usual output. @@ -14765,11 +14767,11 @@ else -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \ -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \ -e 's:$: $lt_compiler_flag:'` - (eval echo "\"\$as_me:14768: $lt_compile\"" >&5) + (eval echo "\"\$as_me:14770: $lt_compile\"" >&5) (eval "$lt_compile" 2>out/conftest.err) ac_status=$? cat out/conftest.err >&5 - echo "$as_me:14772: \$? = $ac_status" >&5 + echo "$as_me:14774: \$? = $ac_status" >&5 if (exit $ac_status) && test -s out/conftest2.$ac_objext then # The compiler can only warn and ignore the option if not recognized @@ -14817,11 +14819,11 @@ else -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \ -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \ -e 's:$: $lt_compiler_flag:'` - (eval echo "\"\$as_me:14820: $lt_compile\"" >&5) + (eval echo "\"\$as_me:14822: $lt_compile\"" >&5) (eval "$lt_compile" 2>out/conftest.err) ac_status=$? cat out/conftest.err >&5 - echo "$as_me:14824: \$? = $ac_status" >&5 + echo "$as_me:14826: \$? = $ac_status" >&5 if (exit $ac_status) && test -s out/conftest2.$ac_objext then # The compiler can only warn and ignore the option if not recognized @@ -16444,6 +16446,11 @@ fi # Prepare configure output +if test "$enable_shared" = yes; then BUILDING_SHARED=1; fi +if test "$enable_static" = yes; then BUILDING_STATIC=1; fi + + + diff --git a/configure.ac b/configure.ac index 80fc73fdd..2937f62d7 100644 --- a/configure.ac +++ b/configure.ac @@ -399,6 +399,11 @@ AC_TYPE_SIZE_T # Prepare configure output +if test "$enable_shared" = yes; then BUILDING_SHARED=1; fi +if test "$enable_static" = yes; then BUILDING_STATIC=1; fi +AC_SUBST(BUILDING_SHARED) +AC_SUBST(BUILDING_STATIC) + AC_SUBST(CVC4_LIBRARY_RELEASE_CODE) AC_SUBST(CVC4_LIBRARY_VERSION) AC_SUBST(CVC4_PARSER_LIBRARY_VERSION) diff --git a/contrib/Makefile.in b/contrib/Makefile.in index a86658b70..8df42980b 100644 --- a/contrib/Makefile.in +++ b/contrib/Makefile.in @@ -63,6 +63,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/doc/Makefile.in b/doc/Makefile.in index 99ff59b1c..745314a39 100644 --- a/doc/Makefile.in +++ b/doc/Makefile.in @@ -63,6 +63,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/Makefile.in b/src/Makefile.in index 9099b92be..08f7c6421 100644 --- a/src/Makefile.in +++ b/src/Makefile.in @@ -159,6 +159,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/context/Makefile.in b/src/context/Makefile.in index c4f82d42a..5428ba8b9 100644 --- a/src/context/Makefile.in +++ b/src/context/Makefile.in @@ -92,6 +92,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in index 4892220d8..848d8d72b 100644 --- a/src/expr/Makefile.in +++ b/src/expr/Makefile.in @@ -93,6 +93,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/expr/node.h b/src/expr/node.h index fd2603ffa..b40443923 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -25,6 +25,7 @@ #include "cvc4_config.h" #include "expr/kind.h" +#include "util/Assert.h" namespace CVC4 { class Node; @@ -105,6 +106,11 @@ public: bool operator==(const Node& e) const { return d_ev == e.d_ev; } bool operator!=(const Node& e) const { return d_ev != e.d_ev; } + Node operator[](int i) const { + Assert(i >= 0 && i < d_ev->d_nchildren); + return Node(d_ev->d_children[i]); + } + /** * We compare by expression ids so, keeping things deterministic and having * that subexpressions have to be smaller than the enclosing expressions. diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 1dee91735..747854d23 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -168,6 +168,7 @@ public: NodeBuilder& append(const Node& n) { Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Debug("prop") << "append: " << this << " " << n << "[" << n.d_ev << "]" << std::endl; allocateEvIfNecessaryForAppend(); NodeValue* ev = n.d_ev; d_hash = NodeValue::computeHash(d_hash, ev); @@ -364,7 +365,7 @@ inline NodeBuilder::NodeBuilder() : d_used(false), d_ev(&d_inlineEv), d_inlineEv(0), - d_childrenStorage(0) {} + d_childrenStorage() {} template inline NodeBuilder::NodeBuilder(Kind k) : @@ -373,9 +374,9 @@ inline NodeBuilder::NodeBuilder(Kind k) : d_used(false), d_ev(&d_inlineEv), d_inlineEv(0), - d_childrenStorage(0) { + d_childrenStorage() { - Message() << "kind " << k << std::endl; + //Message() << "kind " << k << std::endl; d_inlineEv.d_kind = k; } @@ -386,13 +387,13 @@ inline NodeBuilder::NodeBuilder(const NodeBuilder& d_used(nb.d_used), d_ev(&d_inlineEv), d_inlineEv(0), - d_childrenStorage(0) { + d_childrenStorage() { if(evIsAllocated(nb)) { realloc(nb->d_size, false); - std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end()); + std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin()); } else { - std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end()); + std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin()); } } @@ -404,13 +405,13 @@ inline NodeBuilder::NodeBuilder(const NodeBuilder& nb) : d_used(nb.d_used), d_ev(&d_inlineEv), d_inlineEv(0), - d_childrenStorage(0) { + d_childrenStorage() { if(nb.d_ev->d_nchildren > nchild_thresh) { realloc(nb.d_size, false); - std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end()); + std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin()); } else { - std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end()); + std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin()); } } @@ -421,7 +422,7 @@ inline NodeBuilder::NodeBuilder(NodeManager* nm) : d_used(false), d_ev(&d_inlineEv), d_inlineEv(0), - d_childrenStorage(0) {} + d_childrenStorage() {} template inline NodeBuilder::NodeBuilder(NodeManager* nm, Kind k) : @@ -432,7 +433,7 @@ inline NodeBuilder::NodeBuilder(NodeManager* nm, Kind k) : d_inlineEv(0), d_childrenStorage() { - Message() << "kind " << k << std::endl; + //Message() << "kind " << k << std::endl; d_inlineEv.d_kind = k; } @@ -466,9 +467,9 @@ void NodeBuilder::realloc() { d_ev->d_rc = 0; d_ev->d_kind = d_inlineEv.d_kind; d_ev->d_nchildren = nchild_thresh; - std::copy(d_ev->d_children, - d_inlineEv.d_children, - d_inlineEv.d_children + nchild_thresh); + std::copy(d_inlineEv.d_children, + d_inlineEv.d_children + nchild_thresh, + d_ev->d_children); } } @@ -489,9 +490,9 @@ void NodeBuilder::realloc(size_t toSize, bool copy) { d_ev->d_kind = d_inlineEv.d_kind; d_ev->d_nchildren = nchild_thresh; if(copy) { - std::copy(d_ev->d_children, - d_inlineEv.d_children, - d_inlineEv.d_children + nchild_thresh); + std::copy(d_inlineEv.d_children, + d_inlineEv.d_children + nchild_thresh, + d_ev->d_children); } } } @@ -502,6 +503,21 @@ NodeBuilder::operator Node() {// not const Assert(d_ev->d_kind != UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); + if(d_ev->d_kind == VARIABLE) { + Assert(d_ev->d_nchildren == 0); + NodeValue *ev = (NodeValue*) + std::malloc(sizeof(NodeValue) + + ( sizeof(NodeValue*) * d_inlineEv.d_nchildren )); + ev->d_nchildren = 0; + ev->d_kind = VARIABLE; + ev->d_id = NodeValue::next_id++;// FIXME multithreading + ev->d_rc = 0; + d_used = true; + d_ev = NULL; + Debug("prop") << "result: " << Node(ev) << std::endl; + return Node(ev); + } + // implementation differs depending on whether the expression value // was malloc'ed or not @@ -510,6 +526,7 @@ NodeBuilder::operator Node() {// not const if(ev != NULL) { // expression already exists in node manager d_used = true; + Debug("prop") << "result: " << Node(ev) << std::endl; return Node(ev); } @@ -520,30 +537,41 @@ NodeBuilder::operator Node() {// not const // this inserts into the NodeManager; // return the result of lookup() in case another thread beat us to it d_used = true; - return d_nm->lookup(d_hash, ev); + Node n = d_nm->lookup(d_hash, ev); + Debug("prop") << "result: " << n << std::endl; + return n; } NodeValue *ev = d_nm->lookupNoInsert(d_hash, &d_inlineEv); if(ev != NULL) { // expression already exists in node manager d_used = true; + Debug("prop") << "result: " << Node(ev) << std::endl; return Node(ev); } // otherwise create the canonical expression value for this node ev = (NodeValue*) std::malloc(sizeof(NodeValue) + - ( sizeof(NodeValue*) * d_inlineEv.d_nchildren) ); - ev->d_nchildren = d_ev->d_nchildren; - ev->d_kind = d_ev->d_kind; + ( sizeof(NodeValue*) * d_inlineEv.d_nchildren )); + ev->d_nchildren = d_inlineEv.d_nchildren; + ev->d_kind = d_inlineEv.d_kind; ev->d_id = NodeValue::next_id++;// FIXME multithreading ev->d_rc = 0; + std::copy(d_inlineEv.d_children, + d_inlineEv.d_children + d_inlineEv.d_nchildren, + ev->d_children); d_used = true; d_ev = NULL; // this inserts into the NodeManager; // return the result of lookup() in case another thread beat us to it - return d_nm->lookup(d_hash, ev); + if(ev->numChildren()) { + Debug("prop") << "ev first child: " << *ev->ev_begin() << std::endl; + } + Node n = d_nm->lookup(d_hash, ev); + Debug("prop") << "result: " << n << std::endl; + return n; } }/* CVC4 namespace */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index eba8c4d18..a307eb11f 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -58,6 +58,7 @@ Node NodeManager::lookup(uint64_t hash, NodeValue* ev) { return *j; } + // didn't find it, insert std::vector v; Node e(ev); @@ -99,6 +100,7 @@ NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) { return j->d_ev; } + // didn't find it, don't insert return 0; } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 954fe0aaa..985ad15a7 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -177,7 +177,7 @@ namespace CVC4 { namespace expr { inline Node NodeValue::node_iterator::operator*() { - return Node((NodeValue*) d_i); + return Node(*d_i); } }/* CVC4::expr namespace */ diff --git a/src/main/Makefile.in b/src/main/Makefile.in index 8e2c49989..6a2677109 100644 --- a/src/main/Makefile.in +++ b/src/main/Makefile.in @@ -94,6 +94,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 81cbc2df8..123bc3204 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -110,7 +110,8 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti } if(strcmp(optarg, "help")) { - throw OptionException(string("unknown language for --lang: `") + argv[optind] + "'. Try --lang help."); + throw OptionException(string("unknown language for --lang: `") + + optarg + "'. Try --lang help."); } fputs(lang_help, stdout); @@ -132,13 +133,13 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti break; case '?': - throw OptionException(string("can't understand option: `") + argv[optind] + "'"); + throw OptionException(string("can't understand option"));// + argv[optind - 1] + "'"); case ':': - throw OptionException(string("option `") + argv[optind] + "' missing its required argument"); + throw OptionException(string("option missing its required argument"));// + argv[optind - 1] + "' missing its required argument"); default: - throw OptionException(string("can't understand option: `") + argv[optind] + "'"); + throw OptionException(string("can't understand option"));//: `") + argv[optind - 1] + "'"); } } diff --git a/src/parser/Makefile.in b/src/parser/Makefile.in index 31ae05da5..b6c6ae102 100644 --- a/src/parser/Makefile.in +++ b/src/parser/Makefile.in @@ -163,6 +163,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in index 28b80800e..e63b15e26 100644 --- a/src/parser/cvc/Makefile.in +++ b/src/parser/cvc/Makefile.in @@ -96,6 +96,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in index 6145b4c4e..a65d62c88 100644 --- a/src/parser/smt/Makefile.in +++ b/src/parser/smt/Makefile.in @@ -96,6 +96,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/prop/Makefile.in b/src/prop/Makefile.in index c6538df38..e5ac92c61 100644 --- a/src/prop/Makefile.in +++ b/src/prop/Makefile.in @@ -130,6 +130,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in index 1dbc8da9f..278d68790 100644 --- a/src/prop/minisat/Makefile.in +++ b/src/prop/minisat/Makefile.in @@ -92,6 +92,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index ffd335453..afc84a5b4 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -64,7 +64,13 @@ static void doAtom(SimpSolver* minisat, map* vars, Node e, vec* c->push(Lit(v->second, true)); return; } - Unhandled(); + if(e.getKind() == OR) { + for(Node::iterator i = e.begin(); i != e.end(); ++i) { + doAtom(minisat, vars, *i, c); + } + return; + } + Unhandled(e.getKind()); } static void doClause(SimpSolver* minisat, map* vars, map* varsReverse, Node e) { @@ -72,6 +78,20 @@ static void doClause(SimpSolver* minisat, map* vars, map* Debug("prop") << " " << e << endl; if(e.getKind() == VARIABLE || e.getKind() == NOT) { doAtom(minisat, vars, e, &c); + } else if(e.getKind() == FALSE) { + // inconsistency + Notice() << "adding FALSE clause" << endl; + Var v = minisat->newVar(); + c.push(Lit(v, true)); + minisat->addClause(c); + Notice() << "added unit clause " << v << " [[ " << (*varsReverse)[v] << " ]]" << endl; + c.clear(); + c.push(Lit(v, false)); + minisat->addClause(c); + Notice() << "added unit clause -" << v << " [[ -" << (*varsReverse)[v] << " ]]" << endl; + } else if(e.getKind() == TRUE) { + Notice() << "adding TRUE clause (do nothing)" << endl; + // do nothing } else { Assert(e.getKind() == OR); for(Node::iterator i = e.begin(); i != e.end(); ++i) { @@ -101,7 +121,7 @@ void PropEngine::solve(Node e) { d_sat.verbosity = 1; bool result = d_sat.solve(); - Notice() << "result is " << (result ? "sat" : "unsat") << endl; + Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl; if(result) { Notice() << "model:" << endl; for(int i = 0; i < d_sat.model.size(); ++i) diff --git a/src/smt/Makefile.in b/src/smt/Makefile.in index 35126e382..aa00d5e25 100644 --- a/src/smt/Makefile.in +++ b/src/smt/Makefile.in @@ -92,6 +92,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4c7f6a156..018936f7c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -15,37 +15,55 @@ #include "smt/smt_engine.h" #include "util/exception.h" #include "util/command.h" +#include "util/output.h" +#include "expr/node_builder.h" namespace CVC4 { SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() : - d_public_em(em), - d_em(em->getNodeManager()), - d_opts(opts), - d_de(), - d_te(), - d_prop(d_de, d_te) { - } + d_assertions(), + d_public_em(em), + d_nm(em->getNodeManager()), + d_opts(opts), + d_de(), + d_te(), + d_prop(d_de, d_te) { +} SmtEngine::~SmtEngine() { } void SmtEngine::doCommand(Command* c) { + NodeManagerScope nms(d_nm); c->invoke(this); } Node SmtEngine::preprocess(const Node& e) { + if(e.getKind() == NOT) { + if(e[0].getKind() == TRUE) { + return d_nm->mkNode(FALSE); + } else if(e[0].getKind() == FALSE) { + return d_nm->mkNode(TRUE); + } else if(e[0].getKind() == NOT) { + return preprocess(e[0][0]); + } + } return e; } Node SmtEngine::processAssertionList() { - Node asserts; + if(d_assertions.size() == 1) { + return d_assertions[0]; + } + + NodeBuilder<> asserts(AND); for(std::vector::iterator i = d_assertions.begin(); i != d_assertions.end(); ++i) { - asserts = asserts.isNull() ? *i : d_em->mkNode(AND, asserts, *i); + asserts << *i; } + return asserts; } @@ -61,25 +79,34 @@ Result SmtEngine::quickCheck() { } void SmtEngine::addFormula(const Node& e) { + Debug("smt") << "push_back assertion " << e << std::endl; d_assertions.push_back(e); } Result SmtEngine::checkSat(const BoolExpr& e) { + NodeManagerScope nms(d_nm); Node node_e = preprocess(e.getNode()); addFormula(node_e); return check(); } Result SmtEngine::query(const BoolExpr& e) { - Node node_e = preprocess(e.getNode()); + NodeManagerScope nms(d_nm); + Node node_e = preprocess(d_nm->mkNode(NOT, e.getNode())); addFormula(node_e); return check(); } Result SmtEngine::assertFormula(const BoolExpr& e) { + NodeManagerScope nms(d_nm); Node node_e = preprocess(e.getNode()); addFormula(node_e); return quickCheck(); } +Expr SmtEngine::simplify(const Expr& e) { + Expr simplify(const Expr& e); + Unimplemented(); +} + }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 98cffb6de..027d3d603 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -118,7 +118,7 @@ private: ExprManager *d_public_em; /** Out internal expression/node manager */ - NodeManager *d_em; + NodeManager *d_nm; /** User-level options */ Options *d_opts; diff --git a/src/theory/Makefile.in b/src/theory/Makefile.in index dafd68b6c..379d1171b 100644 --- a/src/theory/Makefile.in +++ b/src/theory/Makefile.in @@ -130,6 +130,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/theory/uf/Makefile.in b/src/theory/uf/Makefile.in index 3b3cd6bbb..b1a6081d2 100644 --- a/src/theory/uf/Makefile.in +++ b/src/theory/uf/Makefile.in @@ -78,6 +78,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/util/Assert.h b/src/util/Assert.h index 49c97e9b6..d8e881613 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -113,6 +113,28 @@ public: } };/* class UnhandledCaseException */ +class CVC4_PUBLIC UnimplementedOperationException : public AssertionException { +protected: + UnimplementedOperationException() : AssertionException() {} + +public: + UnimplementedOperationException(const char* function, const char* file, + unsigned line, const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Unimplemented code encountered", + NULL, function, file, line, fmt, args); + va_end(args); + } + + UnimplementedOperationException(const char* function, const char* file, + unsigned line) : + AssertionException() { + construct("Unimplemented code encountered", NULL, function, file, line); + } +};/* class UnimplementedOperationException */ + class CVC4_PUBLIC IllegalArgumentException : public AssertionException { protected: IllegalArgumentException() : AssertionException() {} @@ -172,6 +194,8 @@ public: throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define Unhandled(msg...) \ throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) +#define Unimplemented(msg...) \ + throw UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define IllegalArgument(arg, msg...) \ throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define CheckArgument(cond, arg, msg...) \ diff --git a/src/util/Makefile.in b/src/util/Makefile.in index 3ac892aba..686f4cc33 100644 --- a/src/util/Makefile.in +++ b/src/util/Makefile.in @@ -93,6 +93,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/util/output.h b/src/util/output.h index 57ce5f3ca..c1e513703 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -55,7 +55,7 @@ public: // Yeting option not possible here std::ostream& operator()(const char* tag) { - if(d_tags.find(tag) != d_tags.end()) + if(d_tags.find(std::string(tag)) != d_tags.end()) return *d_os; else return null_os; } diff --git a/test/Makefile.in b/test/Makefile.in index c2eabd8a4..6e8fff2a7 100644 --- a/test/Makefile.in +++ b/test/Makefile.in @@ -103,6 +103,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index bee3e3a85..c5e6ec676 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4 +TESTS_ENVIRONMENT = @top_builddir@/../../bin/cvc4 TESTS = \ simple.cvc \ simple.smt \ diff --git a/test/regress/Makefile.in b/test/regress/Makefile.in index 4ba824928..2670ecd65 100644 --- a/test/regress/Makefile.in +++ b/test/regress/Makefile.in @@ -65,6 +65,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ @@ -190,7 +192,7 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4 +TESTS_ENVIRONMENT = @top_builddir@/../../bin/cvc4 TESTS = \ simple.cvc \ simple.smt \ diff --git a/test/regress/simple2.smt b/test/regress/simple2.smt index c8db8c13f..e917d1b64 100644 --- a/test/regress/simple2.smt +++ b/test/regress/simple2.smt @@ -5,9 +5,9 @@ :extrapreds ((x1)) :extrapreds ((x2)) :extrapreds ((x3)) -:assumption (or x1 (not x0)) :formula -(and (or x0 (not x3)) +(and (or x1 (not x0)) + (or x0 (not x3)) (or x3 x2) (not x1)) ) diff --git a/test/system/Makefile.in b/test/system/Makefile.in index 14e1ac9c7..4b457a954 100644 --- a/test/system/Makefile.in +++ b/test/system/Makefile.in @@ -65,6 +65,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index df85ba805..fcaa2cc5d 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -4,6 +4,8 @@ UNIT_TESTS = \ expr/node_black \ parser/parser_black +TESTS_DEPENDENCIES = $(abs_top_builddir)/src/libcvc4.la $(abs_top_builddir)/src/parser/libcvc4parser.la + # things that aren't tests but that tests rely on and need to # go into the distribution TEST_DEPS = diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in index 4d20d59de..49912b26c 100644 --- a/test/unit/Makefile.in +++ b/test/unit/Makefile.in @@ -88,6 +88,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ @@ -220,6 +222,7 @@ UNIT_TESTS = \ expr/node_black \ parser/parser_black +TESTS_DEPENDENCIES = $(abs_top_builddir)/src/libcvc4.la $(abs_top_builddir)/src/parser/libcvc4parser.la # things that aren't tests but that tests rely on and need to # go into the distribution