From: Morgan Deters Date: Fri, 29 Jan 2010 00:05:16 +0000 (+0000) Subject: fixed CNF conversion, and more modular; CNF conversion command line option; various... X-Git-Tag: cvc5-1.0.0~9331 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2a9e6970b971eb0a9ac4c216fe5f5f1542e195e0;p=cvc5.git fixed CNF conversion, and more modular; CNF conversion command line option; various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?) --- diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 6cbb41812..50c9edcd2 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -85,9 +85,9 @@ Kind Expr::getKind() const { return d_node->getKind(); } -size_t Expr::numChildren() const { +size_t Expr::getNumChildren() const { Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - return d_node->numChildren(); + return d_node->getNumChildren(); } std::string Expr::toString() const { diff --git a/src/expr/expr.h b/src/expr/expr.h index eb4d1ce03..6f7330ed0 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -104,7 +104,7 @@ public: * Returns the number of children of this expression. * @return the number of children */ - size_t numChildren() const; + size_t getNumChildren() const; /** * Returns the string representation of the expression. diff --git a/src/expr/kind.h b/src/expr/kind.h index ea9dbd662..8ba282f0f 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -88,7 +88,7 @@ inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) { case MINUS: out << "MINUS"; break; case MULT: out << "MULT"; break; - default: out << "UNKNOWNKIND!"; break; + default: out << "UNKNOWNKIND!" << int(k); break; } return out; diff --git a/src/expr/node.h b/src/expr/node.h index b40443923..67af6aa18 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -120,6 +120,7 @@ public: Node& operator=(const Node&); uint64_t hash() const; + uint64_t getId() const { return d_ev->getId(); } Node eqExpr(const Node& right) const; Node notExpr() const; @@ -136,7 +137,7 @@ public: inline Kind getKind() const; - inline size_t numChildren() const; + inline size_t getNumChildren() const; static Node null(); @@ -165,9 +166,7 @@ inline bool Node::operator<(const Node& e) const { return d_ev->d_id < e.d_ev->d_id; } -inline std::ostream& - -operator<<(std::ostream& out, const Node& e) { +inline std::ostream& operator<<(std::ostream& out, const Node& e) { e.toStream(out); return out; } @@ -216,7 +215,7 @@ inline Node::const_iterator Node::end() const { return d_ev->end(); } -inline size_t Node::numChildren() const { +inline size_t Node::getNumChildren() const { return d_ev->d_nchildren; } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 13aa0b0ff..7c6405ace 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -36,6 +36,9 @@ namespace CVC4 { namespace CVC4 { +template +inline std::ostream& operator<<(std::ostream&, const NodeBuilder&); + class AndNodeBuilder; class OrNodeBuilder; class PlusNodeBuilder; @@ -122,6 +125,10 @@ public: return d_ev->ev_end(); } + unsigned getNumChildren() const { + return d_ev->getNumChildren(); + } + // Compound expression constructors /* NodeBuilder& eqExpr(const Node& right); @@ -189,6 +196,10 @@ public: // not const operator Node(); + inline void toStream(std::ostream& out) const { + d_ev->toStream(out); + } + /* AndNodeBuilder operator&&(Node); OrNodeBuilder operator||(Node); @@ -440,7 +451,7 @@ inline NodeBuilder::NodeBuilder(NodeManager* nm, Kind k) : template inline NodeBuilder::~NodeBuilder() { Assert(d_used, "NodeBuilder unused at destruction"); - + return; /* for(iterator i = d_ev->ev_begin(); @@ -566,7 +577,7 @@ NodeBuilder::operator Node() {// not const // this inserts into the NodeManager; // return the result of lookup() in case another thread beat us to it - if(ev->numChildren()) { + if(ev->getNumChildren()) { Debug("prop") << "ev first child: " << *ev->ev_begin() << std::endl; } Node n = d_nm->lookup(d_hash, ev); @@ -574,6 +585,13 @@ NodeBuilder::operator Node() {// not const return n; } +template +inline std::ostream& operator<<(std::ostream& out, + const NodeBuilder& b) { + b.toStream(out); + return out; +} + }/* CVC4 namespace */ #endif /* __CVC4__NODE_BUILDER_H */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a307eb11f..0d3fecac6 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -40,7 +40,7 @@ Node NodeManager::lookup(uint64_t hash, NodeValue* ev) { continue; } - if(ev->numChildren() != j->numChildren()) { + if(ev->getNumChildren() != j->getNumChildren()) { continue; } @@ -81,7 +81,7 @@ NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) { continue; } - if(ev->numChildren() != j->numChildren()) { + if(ev->getNumChildren() != j->getNumChildren()) { continue; } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 84df5957a..847b6b153 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -170,7 +170,8 @@ public: unsigned getId() const { return d_id; } Kind getKind() const { return (Kind) d_kind; } - unsigned numChildren() const { return d_nchildren; } + unsigned getNumChildren() const { return d_nchildren; } + std::string toString() const; void toStream(std::ostream& out) const; }; diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 123bc3204..388e58a3b 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -46,9 +46,16 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt | smtlib SMT-LIB format\n\ "; +static const char cnf_help[] = "\ +CNF conversions currently supported as arguments to the --cnf option:\n\ + direct put in equiv. CNF directly (exp. blow up in # clauses, no new vars)\n\ + var variable-introduction method (new vars, no exp. blow up in # clauses)\n\ +"; + // FIXME add a comment here describing the purpose of this enum OptionValue { - SMTCOMP = 256, /* no clash with char options */ + CNF = 256, /* no clash with char options */ + SMTCOMP, STATS };/* enum OptionValue */ @@ -61,6 +68,7 @@ static struct option cmdlineOptions[] = { { "quiet" , no_argument , NULL, 'q' }, { "lang" , required_argument, NULL, 'L' }, { "debug" , required_argument, NULL, 'd' }, + { "cnf" , required_argument, NULL, CNF }, { "smtcomp", no_argument , NULL, SMTCOMP }, { "stats" , no_argument , NULL, STATS } };/* if you add things to the above, please remember to update usage.h! */ @@ -117,6 +125,21 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti fputs(lang_help, stdout); exit(1); + case CNF: + if(!strcmp(optarg, "direct")) { + opts->d_cnfConversion = CNF_DIRECT_EXPONENTIAL; + break; + } else if(!strcmp(optarg, "var")) { + opts->d_cnfConversion = CNF_VAR_INTRODUCTION; + break; + } else if(strcmp(optarg, "help")) { + throw OptionException(string("unknown CNF conversion for --cnf: `") + + optarg + "'. Try --cnf help."); + } + + fputs(cnf_help, stdout); + exit(1); + case 'd': Debug.on(optarg); /* fall-through */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index afc84a5b4..16b807904 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -56,7 +56,7 @@ static void doAtom(SimpSolver* minisat, map* vars, Node e, vec* return; } if(e.getKind() == NOT) { - Assert(e.numChildren() == 1); + Assert(e.getNumChildren() == 1); Node child = *e.begin(); Assert(child.getKind() == VARIABLE); map::iterator v = vars->find(child); diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index bd75bacab..fa7fed5f1 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -7,4 +7,7 @@ noinst_LTLIBRARIES = libsmt.la libsmt_la_SOURCES = \ smt_engine.cpp \ - smt_engine.h + smt_engine.h \ + cnf_converter.h \ + cnf_converter.cpp \ + cnf_conversion.h diff --git a/src/smt/Makefile.in b/src/smt/Makefile.in new file mode 100644 index 000000000..3eebba8e1 --- /dev/null +++ b/src/smt/Makefile.in @@ -0,0 +1,517 @@ +# Makefile.in generated by automake 1.11 from Makefile.am. +# @configure_input@ + +# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002, +# 2003, 2004, 2005, 2006, 2007, 2008, 2009 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@ + +VPATH = @srcdir@ +pkgdatadir = $(datadir)/@PACKAGE@ +pkgincludedir = $(includedir)/@PACKAGE@ +pkglibdir = $(libdir)/@PACKAGE@ +pkglibexecdir = $(libexecdir)/@PACKAGE@ +am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd +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/smt +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/cvc4.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 = +CONFIG_CLEAN_VPATH_FILES = +LTLIBRARIES = $(noinst_LTLIBRARIES) +libsmt_la_LIBADD = +am_libsmt_la_OBJECTS = smt_engine.lo cnf_converter.lo +libsmt_la_OBJECTS = $(am_libsmt_la_OBJECTS) +DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) +depcomp = $(SHELL) $(top_srcdir)/config/depcomp +am__depfiles_maybe = depfiles +am__mv = mv -f +CXXCOMPILE = $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \ + $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) +LTCXXCOMPILE = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --mode=compile $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \ + $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) +CXXLD = $(CXX) +CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --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 $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \ + $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) +CCLD = $(CC) +LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \ + $(LDFLAGS) -o $@ +SOURCES = $(libsmt_la_SOURCES) +DIST_SOURCES = $(libsmt_la_SOURCES) +ETAGS = etags +CTAGS = ctags +DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST) +ACLOCAL = @ACLOCAL@ +AMTAR = @AMTAR@ +ANTLR = @ANTLR@ +ANTLR_INCLUDES = @ANTLR_INCLUDES@ +ANTLR_LDFLAGS = @ANTLR_LDFLAGS@ +AR = @AR@ +AS = @AS@ +AUTOCONF = @AUTOCONF@ +AUTOHEADER = @AUTOHEADER@ +AUTOMAKE = @AUTOMAKE@ +AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ +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@ +INSTALL = @INSTALL@ +INSTALL_DATA = @INSTALL_DATA@ +INSTALL_PROGRAM = @INSTALL_PROGRAM@ +INSTALL_SCRIPT = @INSTALL_SCRIPT@ +INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@ +LD = @LD@ +LDFLAGS = @LDFLAGS@ +LIBOBJS = @LIBOBJS@ +LIBS = @LIBS@ +LIBTOOL = @LIBTOOL@ +LIPO = @LIPO@ +LN_S = @LN_S@ +LTLIBOBJS = @LTLIBOBJS@ +MAKEINFO = @MAKEINFO@ +MKDIR_P = @MKDIR_P@ +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@ +abs_builddir = @abs_builddir@ +abs_srcdir = @abs_srcdir@ +abs_top_builddir = @abs_top_builddir@ +abs_top_srcdir = @abs_top_srcdir@ +ac_ct_CC = @ac_ct_CC@ +ac_ct_CXX = @ac_ct_CXX@ +ac_ct_DUMPBIN = @ac_ct_DUMPBIN@ +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@ +builddir = @builddir@ +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@ +mk_include = @mk_include@ +mkdir_p = @mkdir_p@ +oldincludedir = @oldincludedir@ +pdfdir = @pdfdir@ +prefix = @prefix@ +program_transform_name = @program_transform_name@ +psdir = @psdir@ +sbindir = @sbindir@ +sharedstatedir = @sharedstatedir@ +srcdir = @srcdir@ +sysconfdir = @sysconfdir@ +target = @target@ +target_alias = @target_alias@ +target_cpu = @target_cpu@ +target_os = @target_os@ +target_vendor = @target_vendor@ +top_build_prefix = @top_build_prefix@ +top_builddir = @top_builddir@ +top_srcdir = @top_srcdir@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. + +AM_CXXFLAGS = -Wall -fvisibility=hidden +noinst_LTLIBRARIES = libsmt.la +libsmt_la_SOURCES = \ + smt_engine.cpp \ + smt_engine.h \ + cnf_converter.h \ + cnf_converter.cpp \ + cnf_conversion.h + +all: 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 ) \ + && { if test -f $@; then exit 0; else break; fi; }; \ + exit 1;; \ + esac; \ + done; \ + echo ' cd $(top_srcdir) && $(AUTOMAKE) --gnu src/smt/Makefile'; \ + $(am__cd) $(top_srcdir) && \ + $(AUTOMAKE) --gnu src/smt/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 +$(am__aclocal_m4_deps): + +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 +libsmt.la: $(libsmt_la_OBJECTS) $(libsmt_la_DEPENDENCIES) + $(CXXLINK) $(libsmt_la_OBJECTS) $(libsmt_la_LIBADD) $(LIBS) + +mostlyclean-compile: + -rm -f *.$(OBJEXT) + +distclean-compile: + -rm -f *.tab.c + +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cnf_converter.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/smt_engine.Plo@am__quote@ + +.cpp.o: +@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< +@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po +@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@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ `$(CYGPATH_W) '$<'` +@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po +@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@ $(LTCXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< +@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Plo +@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 + +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; nonempty = 1; } \ + END { if (nonempty) { for (i in files) print i; }; }'`; \ + mkid -fID $$unique +tags: TAGS + +TAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \ + $(TAGS_FILES) $(LISP) + set x; \ + 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; nonempty = 1; } \ + END { if (nonempty) { for (i in files) print i; }; }'`; \ + shift; \ + if test -z "$(ETAGS_ARGS)$$*$$unique"; then :; else \ + test -n "$$unique" || unique=$$empty_fix; \ + if test $$# -gt 0; then \ + $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \ + "$$@" $$unique; \ + else \ + $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \ + $$unique; \ + fi; \ + fi +ctags: CTAGS +CTAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \ + $(TAGS_FILES) $(LISP) + 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; nonempty = 1; } \ + END { if (nonempty) { for (i in files) print i; }; }'`; \ + test -z "$(CTAGS_ARGS)$$unique" \ + || $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \ + $$unique + +GTAGS: + here=`$(am__cd) $(top_builddir) && pwd` \ + && $(am__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)'; \ + dist_files=`for file in $$list; do echo $$file; done | \ + sed -e "s|^$$srcdirstrip/||;t" \ + -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \ + case $$dist_files in \ + */*) $(MKDIR_P) `echo "$$dist_files" | \ + sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \ + sort -u` ;; \ + esac; \ + for file in $$dist_files; do \ + if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \ + if test -d $$d/$$file; then \ + dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \ + if test -d "$(distdir)/$$file"; then \ + find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \ + fi; \ + if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \ + cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \ + find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \ + fi; \ + cp -fpR $$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: check-am +all-am: Makefile $(LTLIBRARIES) +installdirs: +install: 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) + -test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES) + +maintainer-clean-generic: + @echo "This command is intended for maintainers to use" + @echo "it deletes files that may require special tools to rebuild." +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-tags + +dvi: dvi-am + +dvi-am: + +html: html-am + +html-am: + +info: info-am + +info-am: + +install-data-am: + +install-dvi: install-dvi-am + +install-dvi-am: + +install-exec-am: + +install-html: install-html-am + +install-html-am: + +install-info: install-info-am + +install-info-am: + +install-man: + +install-pdf: install-pdf-am + +install-pdf-am: + +install-ps: install-ps-am + +install-ps-am: + +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: + +.MAKE: install-am install-strip + +.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-dvi \ + install-dvi-am install-exec install-exec-am install-html \ + install-html-am install-info install-info-am install-man \ + install-pdf install-pdf-am install-ps install-ps-am \ + 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 + + +# 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/smt/cnf_conversion.h b/src/smt/cnf_conversion.h new file mode 100644 index 000000000..924cae063 --- /dev/null +++ b/src/smt/cnf_conversion.h @@ -0,0 +1,46 @@ +/********************* -*- C++ -*- */ +/** cnf_conversion.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none + ** 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. + ** + ** A type for describing possible CNF conversions. + **/ + +#ifndef __CVC4__CNF_CONVERSION_H +#define __CVC4__CNF_CONVERSION_H + +namespace CVC4 { + +enum CnfConversion { + CNF_DIRECT_EXPONENTIAL = 0, + CNF_VAR_INTRODUCTION = 1 +}; + +inline std::ostream& operator<<(std::ostream&, CVC4::CnfConversion) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, CVC4::CnfConversion c) { + using namespace CVC4; + + switch(c) { + case CNF_DIRECT_EXPONENTIAL: + out << "CNF_DIRECT_EXPONENTIAL"; + break; + case CNF_VAR_INTRODUCTION: + out << "CNF_VAR_INTRODUCTION"; + break; + default: + out << "UNKNOWN-CONVERTER!" << int(c); + } + + return out; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__CNF_CONVERSION_H */ diff --git a/src/smt/cnf_converter.cpp b/src/smt/cnf_converter.cpp new file mode 100644 index 000000000..c94d62524 --- /dev/null +++ b/src/smt/cnf_converter.cpp @@ -0,0 +1,234 @@ +/********************* -*- C++ -*- */ +/** cnf_converter.cpp + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none + ** 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. + ** + ** A CNF converter for CVC4. + **/ + +#include "smt/cnf_converter.h" +#include "expr/node_builder.h" +#include "expr/node.h" +#include "util/output.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace smt { + + +static void printAST(std::ostream& out, const Node& n, int indent = 0) { + for(int i = 0; i < indent; ++i) { + out << " "; + } + if(n.getKind() == VARIABLE) { + out << "(VARIABLE " << n.getId(); + } else { + out << "(" << n.getKind(); + if(n.getNumChildren() > 0) { + out << std::endl; + } + for(Node::iterator i = n.begin(); i != n.end(); ++i) { + printAST(out, *i, indent + 1); + } + if(n.getNumChildren() > 0) { + for(int i = 0; i < indent; ++i) { + out << " "; + } + } + } + out << ")" << std::endl; +} + + +Node CnfConverter::convert(const Node& e) { + Node n; + + if(conversionMapped(e)) { + Debug("cnf") << "conversion for " << e << " with id " << e.getId() << " is cached!" << std::endl; + n = getConversionMap(e); + } else { + switch(d_conversion) { + case CNF_DIRECT_EXPONENTIAL: + n = directConvert(e); + break; + case CNF_VAR_INTRODUCTION: + n = varIntroductionConvert(e); + break; + default: + Unhandled(d_conversion); + } + + Debug("cnf") << "mapping conversion " << e << " with id " << e.getId() << " to " << n << " with id " << n.getId() << std::endl; + mapConversion(e, n); + Assert(conversionMapped(e)); + Assert(getConversionMap(e) == n); + } + + Debug("cnf") << "CONVERTED ================" << std::endl; + printAST(Debug("cnf"), e); + Debug("cnf") << "TO ================" << std::endl; + printAST(Debug("cnf"), n); + Debug("cnf") << "==========================" << std::endl; + + return n; +} + +Node CnfConverter::compressNOT(const Node& e) { + Assert(e.getKind() == NOT); + + // short-circuit trivial NOTs + 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 convert(e[0][0]); + } else { + Node f = convert(e[0]); + // push NOTs inside of ANDs and ORs + if(f.getKind() == AND) { + NodeBuilder<> n(OR); + for(Node::iterator i = f.begin(); i != f.end(); ++i) { + if((*i).getKind() == NOT) { + n << (*i)[0]; + } else { + n << d_nm->mkNode(NOT, *i); + } + } + return n; + } + if(f.getKind() == OR) { + NodeBuilder<> n(AND); + for(Node::iterator i = f.begin(); i != f.end(); ++i) { + if((*i).getKind() == NOT) { + n << (*i)[0]; + } else { + n << d_nm->mkNode(NOT, *i); + } + } + return n; + } + return e; + } +} + + +Node CnfConverter::directConvert(const Node& e) { + if(e.getKind() == NOT) { + return compressNOT(e); + } else if(e.getKind() == AND) { + return flatten(e); + } else if(e.getKind() == OR) { + Node n = flatten(e); + + NodeBuilder<> m(OR); + directOrHelper(n.begin(), n.end(), m); + + return m; + } + + return e; +} + +void CnfConverter::directOrHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result) { + while(p != end) { + if((*p).getKind() == AND) { + Debug("cnf") << "orHelper: p " << *p << std::endl; + Debug("cnf") << " end " << std::endl; + Debug("cnf") << " result " << result << std::endl; + + NodeBuilder<> resultPrefix = result; + result = NodeBuilder<>(AND); + + for(Node::iterator i = (*p).begin(); i != (*p).end(); ++i) { + NodeBuilder<> r = resultPrefix; + + // is this a double-convert since we did OR flattening before? + r << convert(*i); + Node::iterator p2 = p; + directOrHelper(++p2, end, r); + + result << r; + } + } else { + Debug("cnf") << "orHelper: passing through a conversion of " << *p << std::endl; + // is this a double-convert since we did OR flattening before? + result << convert(*p); + } + + Debug("cnf") << " ** result now " << result << std::endl; + + ++p; + } +} + +Node CnfConverter::varIntroductionConvert(const Node& e) { + if(e.getKind() == NOT) { + return compressNOT(e); + } else if(e.getKind() == AND) { + return flatten(e); + } else if(e.getKind() == OR) { + Node n = flatten(e); + + Debug("cnf") << "about to handle an OR:" << std::endl; + printAST(Debug("cnf"), n); + + NodeBuilder<> m(AND); + NodeBuilder<> extras(OR); + varIntroductionOrHelper(n.begin(), n.end(), m, extras); + + if(m.getNumChildren() > 0) { + return m << extras; + } else { + return extras; + } + } + + return e; +} + +void CnfConverter::varIntroductionOrHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result, NodeBuilder<>& extras) { + while(p != end) { + if((*p).getKind() == AND) { + Debug("cnf") << "orHelper: p " << *p << std::endl; + printAST(Debug("cnf"), *p); + Debug("cnf") << " end " << std::endl; + Debug("cnf") << " result " << result << std::endl; + Debug("cnf") << " extras " << extras << std::endl; + + Node var = d_nm->mkVar(); + extras << var; + + Debug("cnf") << " introduced var " << var << "(" << var.getId() << ")" << std::endl; + + Node notVar = d_nm->mkNode(NOT, var); + + for(Node::iterator i = (*p).begin(); i != (*p).end(); ++i) { + // is this a double-convert since we did OR flattening before? + result << d_nm->mkNode(OR, notVar, convert(*i)); + } + } else { + // is this a double-convert since we did OR flattening before? + Debug("cnf") << "orHelper: p " << *p << std::endl; + Debug("cnf") << " end " << std::endl; + Debug("cnf") << " result " << result << std::endl; + Debug("cnf") << " extras " << extras << std::endl; + Debug("cnf") << " passing through" << std::endl; + extras << convert(*p); + } + + Debug("cnf") << " ** result now " << result << std::endl; + Debug("cnf") << " ** extras now " << extras << std::endl; + ++p; + } +} + +}/* CVC4::smt namespace */ +}/* CVC4 namespace */ diff --git a/src/smt/cnf_converter.h b/src/smt/cnf_converter.h new file mode 100644 index 000000000..d045f4d64 --- /dev/null +++ b/src/smt/cnf_converter.h @@ -0,0 +1,152 @@ +/********************* -*- C++ -*- */ +/** cnf_converter.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none + ** 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. + ** + ** A CNF converter for CVC4. + **/ + +#ifndef __CVC4__SMT__CNF_CONVERTER_H +#define __CVC4__SMT__CNF_CONVERTER_H + +#include "expr/node_builder.h" +#include "expr/node.h" +#include "smt/cnf_conversion.h" + +#include + +namespace CVC4 { +namespace smt { + +class CnfConverter { + +private: + + /** Our node manager */ + NodeManager *d_nm; + + /** The type of conversion this converter performs */ + CVC4::CnfConversion d_conversion; + + /** Map of already-converted Nodes */ + std::map d_conversionMap; + + /** + * Returns true iff the CNF conversion for the Node was cached + * previously. + */ + bool conversionMapped(const Node& n) { + return d_conversionMap.find(n) != d_conversionMap.end(); + } + + /** + * Returns true iff the CNF conversion for the Node was cached + * previously. + */ + Node getConversionMap(const Node& n) { + return d_conversionMap[n]; + } + + /** + * Cache a new CNF conversion. + */ + void mapConversion(const Node& n, const Node& m) { + d_conversionMap[n] = m; + } + + /** + * Compress a NOT: do NNF transformation plus a bit. Does DNE, + * NOT FALSE ==> TRUE, NOT TRUE ==> FALSE, and pushes NOT inside + * of ANDs and ORs. Calls convert() on subnodes. + */ + Node compressNOT(const Node& e); + + /** + * Flatten a Node of kind K. K here is going to be AND or OR. + * "Flattening" means to take all children of the Node with the same + * kind and hoist their children to the top-level. So e.g. + * (AND (AND x y) (AND (AND z)) w) ==> (AND x y z w). + */ + template + Node flatten(const Node& e); + + /** + * Do a direct CNF conversion (with possible exponential blow-up in + * the number of clauses). No new variables are introduced. The + * output is equivalent to the input. + */ + Node directConvert(const Node& e); + + /** + * Helper method for "direct" CNF preprocessing. CNF-converts an OR. + */ + void directOrHelper(Node::iterator p, + Node::iterator end, + NodeBuilder<>& result); + + /** + * Do a satisfiability-preserving CNF conversion with variable + * introduction. Doesn't suffer from exponential blow-up in the + * number of clauses, but new variables are introduced and the + * output is equisatisfiable (but not equivalent) to the input. + */ + Node varIntroductionConvert(const Node& e); + + /** + * Helper method for "variable introduction" CNF preprocessing. + * CNF-converts an OR. + */ + void varIntroductionOrHelper(Node::iterator p, + Node::iterator end, + NodeBuilder<>& result, + NodeBuilder<>& extras); + +public: + + /** + * Construct a CnfConverter. + */ + CnfConverter(NodeManager* nm, CVC4::CnfConversion cnv = CNF_VAR_INTRODUCTION) : + d_nm(nm), + d_conversion(cnv) {} + + /** + * Convert an expression into CNF. If a conversion already exists + * for the Node, it is returned. If a conversion doesn't exist, it + * is computed and returned (caching the result). + */ + Node convert(const Node& e); + +};/* class CnfConverter */ + +template +Node CnfConverter::flatten(const Node& e) { + Assert(e.getKind() == K); + + NodeBuilder<> n(K); + + for(Node::iterator i = e.begin(); i != e.end(); ++i) { + Node f = convert(*i); + if(f.getKind() == K) { + for(Node::iterator j = f.begin(); j != f.end(); ++j) { + n << *j; + } + } else { + n << f; + } + } + + return n; +} + +}/* CVC4::smt namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT__CNF_CONVERTER_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index db9dc4edf..c0f825462 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -22,12 +22,13 @@ namespace CVC4 { SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() : d_assertions(), - d_public_em(em), + d_publicEm(em), d_nm(em->getNodeManager()), d_opts(opts), d_de(), d_te(), - d_prop(d_de, d_te) { + d_prop(d_de, d_te), + d_cnfConverter(d_nm, opts->d_cnfConversion) { } SmtEngine::~SmtEngine() { @@ -38,95 +39,7 @@ void SmtEngine::doCommand(Command* c) { c->invoke(this); } -void SmtEngine::orHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result) { - if(p == end) { - return; - } else if((*p).getKind() == AND) { - NodeBuilder<> resultPrefix = result; - result = NodeBuilder<>(AND); - - for(Node::iterator i = (*p).begin(); i != (*p).end(); ++i) { - NodeBuilder<> r = resultPrefix; - - r << preprocess(*i); - Node::iterator p2 = p; - orHelper(++p2, end, r); - - result << r; - } - } else { - result << preprocess(*p); - } -} - Node SmtEngine::preprocess(const Node& e) { - if(e.getKind() == NOT) { - // short-circuit trivial NOTs - 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]); - } else { - Node f = preprocess(e[0]); - // push NOTs inside of ANDs and ORs - if(f.getKind() == AND) { - NodeBuilder<> n(OR); - for(Node::iterator i = f.begin(); i != f.end(); ++i) { - if((*i).getKind() == NOT) { - n << (*i)[0]; - } else { - n << d_nm->mkNode(NOT, *i); - } - } - return n; - } - if(f.getKind() == OR) { - NodeBuilder<> n(AND); - for(Node::iterator i = f.begin(); i != f.end(); ++i) { - if((*i).getKind() == NOT) { - n << (*i)[0]; - } else { - n << d_nm->mkNode(NOT, *i); - } - } - return n; - } - } - } else if(e.getKind() == AND) { - NodeBuilder<> n(AND); - // flatten ANDs - for(Node::iterator i = e.begin(); i != e.end(); ++i) { - Node f = preprocess(*i); - if((*i).getKind() == AND) { - for(Node::iterator j = f.begin(); j != f.end(); ++j) { - n << *j; - } - } else { - n << *i; - } - } - return n; - } else if(e.getKind() == OR) { - NodeBuilder<> n(OR); - // flatten ORs - for(Node::iterator i = e.begin(); i != e.end(); ++i) { - if((*i).getKind() == OR) { - Node f = preprocess(*i); - for(Node::iterator j = f.begin(); j != f.end(); ++j) { - n << *j; - } - } - } - - Node nod = n; - NodeBuilder<> m(OR); - orHelper(nod.begin(), nod.end(), m); - - return m; - } - return e; } @@ -142,16 +55,55 @@ Node SmtEngine::processAssertionList() { asserts << *i; } - return asserts; + d_assertions.clear(); + d_assertions.push_back(asserts); + return d_assertions[0]; +} + +static void printAST(std::ostream& out, const Node& n, int indent = 0) { + for(int i = 0; i < indent; ++i) { + out << " "; + } + if(n.getKind() == VARIABLE) { + out << "(VARIABLE " << n.getId(); + } else { + out << "(" << n.getKind(); + if(n.getNumChildren() > 0) { + out << std::endl; + } + for(Node::iterator i = n.begin(); i != n.end(); ++i) { + printAST(out, *i, indent + 1); + } + if(n.getNumChildren() > 0) { + for(int i = 0; i < indent; ++i) { + out << " "; + } + } + } + out << ")" << std::endl; } Result SmtEngine::check() { + Debug("smt") << "SMT check()" << std::endl; Node asserts = processAssertionList(); - d_prop.solve(asserts); + + // CNF conversion + Debug("cnf") << "preprocessing " << asserts << std::endl; + Node assertsOut = d_cnfConverter.convert(asserts); + Debug("cnf") << " and got " << assertsOut << std::endl; + + Debug("smt") << "BEFORE CONVERSION ==" << std::endl; + printAST(Debug("smt"), asserts); + Debug("smt") << "AFTER CONVERSION ==" << std::endl; + printAST(Debug("smt"), assertsOut); + Debug("smt") << "===================" << std::endl; + + d_prop.solve(assertsOut); return Result(Result::VALIDITY_UNKNOWN); } Result SmtEngine::quickCheck() { + Debug("smt") << "SMT quickCheck()" << std::endl; processAssertionList(); return Result(Result::VALIDITY_UNKNOWN); } @@ -162,6 +114,7 @@ void SmtEngine::addFormula(const Node& e) { } Result SmtEngine::checkSat(const BoolExpr& e) { + Debug("smt") << "SMT checkSat(" << e << ")" << std::endl; NodeManagerScope nms(d_nm); Node node_e = preprocess(e.getNode()); addFormula(node_e); @@ -169,6 +122,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) { } Result SmtEngine::query(const BoolExpr& e) { + Debug("smt") << "SMT query(" << e << ")" << std::endl; NodeManagerScope nms(d_nm); Node node_e = preprocess(d_nm->mkNode(NOT, e.getNode())); addFormula(node_e); @@ -176,6 +130,7 @@ Result SmtEngine::query(const BoolExpr& e) { } Result SmtEngine::assertFormula(const BoolExpr& e) { + Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl; NodeManagerScope nms(d_nm); Node node_e = preprocess(e.getNode()); addFormula(node_e); @@ -183,6 +138,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) { } Expr SmtEngine::simplify(const Expr& e) { + Debug("smt") << "SMT simplify(" << e << ")" << std::endl; Expr simplify(const Expr& e); Unimplemented(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index e06a36128..65375ab65 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -29,6 +29,7 @@ #include "util/options.h" #include "prop/prop_engine.h" #include "util/decision_engine.h" +#include "smt/cnf_converter.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -116,7 +117,7 @@ private: std::vector d_assertions; /** Our expression manager */ - ExprManager *d_public_em; + ExprManager *d_publicEm; /** Out internal expression/node manager */ NodeManager *d_nm; @@ -133,6 +134,9 @@ private: /** The propositional engine */ PropEngine d_prop; + /** The CNF converter in use */ + CVC4::smt::CnfConverter d_cnfConverter; + /** * Pre-process an Node. This is expected to be highly-variable, * with a lot of "source-level configurability" to add multiple @@ -165,11 +169,6 @@ private: */ Node processAssertionList(); - /** - * Helper method for CNF preprocessing. CNF-converts an OR. - */ - void orHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result); - };/* class SmtEngine */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 1372616ec..f0db8a7ae 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -62,12 +62,12 @@ public: /** * Assert a literal in the current context. */ - virtual void assert(Literal) = 0; + void assert(Literal); /** - * Check the current assignment's consistency. Return false iff inconsistent. + * Check the current assignment's consistency. */ - virtual bool check(Effort level = FULL_EFFORT) = 0; + virtual void check(Effort level = FULL_EFFORT) = 0; /** * T-propagate new literal assignments in the current context. diff --git a/src/util/options.h b/src/util/options.h index d6c4e9009..57b20c47f 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -18,6 +18,7 @@ #include #include "parser/parser.h" +#include "smt/cnf_conversion.h" namespace CVC4 { @@ -38,26 +39,20 @@ struct Options { /* with 3, the solver is slowed down by all the scrolling */ int verbosity; - /** The input language option */ - enum InputLanguage { - /** The SMTLIB input language */ - LANG_SMTLIB, - /** The CVC4 input language */ - LANG_CVC4, - /** Auto-detect the language */ - LANG_AUTO - }; - /** The input language */ parser::Parser::InputLanguage lang; + /** The CNF conversion */ + CVC4::CnfConversion d_cnfConversion; + Options() : binary_name(), smtcomp_mode(false), statistics(false), out(0), err(0), verbosity(0), - lang(parser::Parser::LANG_AUTO) + lang(parser::Parser::LANG_AUTO), + d_cnfConversion(CVC4::CNF_DIRECT_EXPONENTIAL) {} };/* struct Options */ diff --git a/test/regress/simple.cvc b/test/regress/simple.cvc index c1a5dd840..3566053d9 100644 --- a/test/regress/simple.cvc +++ b/test/regress/simple.cvc @@ -2,5 +2,5 @@ x0, x1, x2, x3 : BOOLEAN; ASSERT x1 OR NOT x0; ASSERT x0 OR NOT x3; ASSERT x3 OR x2; -ASSERT NOT x1; +ASSERT x1 AND NOT x1; QUERY x2; diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 7cb744d02..5e4e1bb34 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -234,7 +234,7 @@ public: TS_ASSERT(EQUAL == eq.getKind()); - TS_ASSERT(2 == eq.numChildren()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); @@ -247,7 +247,7 @@ public: Node parent = child.notExpr(); TS_ASSERT(NOT == parent.getKind()); - TS_ASSERT(1 == parent.numChildren()); + TS_ASSERT(1 == parent.getNumChildren()); TS_ASSERT(*(parent.begin()) == child); @@ -261,7 +261,7 @@ public: TS_ASSERT(AND == eq.getKind()); - TS_ASSERT(2 == eq.numChildren()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); @@ -277,7 +277,7 @@ public: TS_ASSERT(OR == eq.getKind()); - TS_ASSERT(2 == eq.numChildren()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); @@ -294,7 +294,7 @@ public: TS_ASSERT(ITE == ite.getKind()); - TS_ASSERT(3 == ite.numChildren()); + TS_ASSERT(3 == ite.getNumChildren()); TS_ASSERT(*(ite.begin()) == cnd); TS_ASSERT(*(++ite.begin()) == thenBranch); @@ -310,7 +310,7 @@ public: TS_ASSERT(IFF == eq.getKind()); - TS_ASSERT(2 == eq.numChildren()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); @@ -325,7 +325,7 @@ public: TS_ASSERT(IMPLIES == eq.getKind()); - TS_ASSERT(2 == eq.numChildren()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); @@ -339,7 +339,7 @@ public: TS_ASSERT(XOR == eq.getKind()); - TS_ASSERT(2 == eq.numChildren()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); @@ -381,22 +381,22 @@ public: nbz << Node::null(); } Node result = nbz; - TS_ASSERT( N == result.numChildren()); + TS_ASSERT( N == result.getNumChildren()); } void testNumChildren(){ - /*inline size_t numChildren() const;*/ + /*inline size_t getNumChildren() const;*/ //test 0 - TS_ASSERT(0 == (Node::null()).numChildren()); + TS_ASSERT(0 == (Node::null()).getNumChildren()); //test 1 - TS_ASSERT(1 == (Node::null().notExpr()).numChildren()); + TS_ASSERT(1 == (Node::null().notExpr()).getNumChildren()); //test 2 - TS_ASSERT(2 == (Node::null().andExpr(Node::null())).numChildren() ); + TS_ASSERT(2 == (Node::null().andExpr(Node::null())).getNumChildren() ); //Bigger tests