diff options
Diffstat (limited to 'src')
59 files changed, 1293 insertions, 307 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index b505750d4..1dbf77451 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -137,7 +137,7 @@ gitinfo: gitinfo.tmp # .PHONY ensures the .tmp version is always rebuilt (to check for any changes) .PHONY: gitinfo.tmp gitinfo.tmp: - $(AM_V_GEN)(cd "$(top_srcdir)"; if ! grep -q '^ref: refs/heads/' .git/HEAD; then echo; fi; sed 's,^ref: refs/heads/,,' .git/HEAD; git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD`; echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`") >"$@" 2>/dev/null || true + $(AM_V_GEN)(cd "$(top_srcdir)"; if test -e .git/HEAD; then if ! grep -q '^ref: refs/heads/' .git/HEAD; then echo; fi; sed 's,^ref: refs/heads/,,' .git/HEAD; git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD`; echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`"; fi) >"$@" 2>/dev/null || true install-data-local: (echo include/cvc4.h; \ diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index 301150b12..dcc4bc858 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -163,7 +163,7 @@ CLEANFILES = \ EXTRA_DIST = \ swig.h \ java_iterator_adapter.h \ - java_output_stream_adapter.h + java_stream_adapters.h MOSTLYCLEANFILES = \ .swig_deps \ diff --git a/src/bindings/java_output_stream_adapter.h b/src/bindings/java_output_stream_adapter.h deleted file mode 100644 index 6830e508d..000000000 --- a/src/bindings/java_output_stream_adapter.h +++ /dev/null @@ -1,50 +0,0 @@ -/********************* */ -/*! \file java_output_stream_adapter.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief An OutputStream adapter for the Java bindings - ** - ** An OutputStream adapter for the Java bindings. This works with a lot - ** of help from SWIG, and custom typemaps in the ".i" SWIG interface files - ** for CVC4. The basic idea is that, when a CVC4 function with a - ** std::ostream& parameter is called, a Java-side binding is generated - ** taking a java.io.OutputStream. Now, the problem is that std::ostream - ** has no Java equivalent, and java.io.OutputStream has no C++ equivalent, - ** so we use this class (which exists on both sides) as the go-between. - ** The wrapper connecting the Java function (taking an OutputStream) and - ** the C++ function (taking an ostream) creates a JavaOutputStreamAdapter, - ** and call the C++ function with the stringstream inside. After the call, - ** the generated stream material is collected and output to the Java-side - ** OutputStream. - **/ - -// private to the bindings layer -#ifndef SWIGJAVA -# error This should only be included from the Java bindings layer. -#endif /* SWIGJAVA */ - -#ifndef __CVC4__BINDINGS__JAVA_OUTPUT_STREAM_ADAPTER_H -#define __CVC4__BINDINGS__JAVA_OUTPUT_STREAM_ADAPTER_H - -namespace CVC4 { - -class JavaOutputStreamAdapter { - std::stringstream d_ss; - -public: - JavaOutputStreamAdapter() { } - - std::string toString() { return d_ss.str(); } - -};/* class JavaOutputStreamAdapter */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__BINDINGS__JAVA_OUTPUT_STREAM_ADAPTER_H */ diff --git a/src/bindings/java_stream_adapters.h b/src/bindings/java_stream_adapters.h new file mode 100644 index 000000000..daeb06e18 --- /dev/null +++ b/src/bindings/java_stream_adapters.h @@ -0,0 +1,113 @@ +/********************* */ +/*! \file java_stream_adapters.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An OutputStream adapter for the Java bindings + ** + ** An OutputStream adapter for the Java bindings. This works with a lot + ** of help from SWIG, and custom typemaps in the ".i" SWIG interface files + ** for CVC4. The basic idea is that, when a CVC4 function with a + ** std::ostream& parameter is called, a Java-side binding is generated + ** taking a java.io.OutputStream. Now, the problem is that std::ostream + ** has no Java equivalent, and java.io.OutputStream has no C++ equivalent, + ** so we use this class (which exists on both sides) as the go-between. + ** The wrapper connecting the Java function (taking an OutputStream) and + ** the C++ function (taking an ostream) creates a JavaOutputStreamAdapter, + ** and call the C++ function with the stringstream inside. After the call, + ** the generated stream material is collected and output to the Java-side + ** OutputStream. + **/ + +// private to the bindings layer +#ifndef SWIGJAVA +# error This should only be included from the Java bindings layer. +#endif /* SWIGJAVA */ + +#include <sstream> +#include <set> +#include <cassert> +#include <iostream> +#include <string> +#include <jni.h> + +#ifndef __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H +#define __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H + +namespace CVC4 { + +class JavaOutputStreamAdapter { + std::stringstream d_ss; + +public: + JavaOutputStreamAdapter() { } + + std::string toString() { return d_ss.str(); } + +};/* class JavaOutputStreamAdapter */ + +class JavaInputStreamAdapter : public std::stringstream { + static std::set<JavaInputStreamAdapter*> s_adapters; + jobject inputStream; + + JavaInputStreamAdapter& operator=(const JavaInputStreamAdapter&); + JavaInputStreamAdapter(const JavaInputStreamAdapter&); + +public: + JavaInputStreamAdapter(jobject inputStream) : inputStream(inputStream) { + s_adapters.insert(this); + } + + ~JavaInputStreamAdapter() { + s_adapters.erase(this); + } + + static void pullAdapters(JNIEnv* jenv) { + for(std::set<JavaInputStreamAdapter*>::iterator i = s_adapters.begin(); + i != s_adapters.end(); + ++i) { + (*i)->pull(jenv); + } + } + + jobject getInputStream() const { + return inputStream; + } + + void pull(JNIEnv* jenv) { + if(fail() || eof()) { + clear(); + } + jclass clazz = jenv->FindClass("java/io/InputStream"); + assert(clazz != NULL && jenv->ExceptionOccurred() == NULL); + jmethodID method = jenv->GetMethodID(clazz, "available", "()I"); + assert(method != NULL && jenv->ExceptionOccurred() == NULL); + jint available = jenv->CallIntMethod(inputStream, method); + assert(jenv->ExceptionOccurred() == NULL); + jbyteArray bytes = jenv->NewByteArray(available); + assert(bytes != NULL && jenv->ExceptionOccurred() == NULL); + method = jenv->GetMethodID(clazz, "read", "([B)I"); + assert(method != NULL && jenv->ExceptionOccurred() == NULL); + jint nread = jenv->CallIntMethod(inputStream, method, bytes); + assert(jenv->ExceptionOccurred() == NULL); + jbyte* bptr = jenv->GetByteArrayElements(bytes, NULL); + assert(jenv->ExceptionOccurred() == NULL); + std::copy(bptr, bptr + nread, std::ostream_iterator<char>(*this)); + *this << std::flush; + jenv->ReleaseByteArrayElements(bytes, bptr, 0); + assert(jenv->ExceptionOccurred() == NULL); + assert(good()); + assert(!eof()); + } + +};/* class JavaInputStreamAdapter */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H */ diff --git a/src/cvc4.i b/src/cvc4.i index 3f11fafc2..925152248 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -54,6 +54,9 @@ using namespace CVC4; #include "expr/expr.h" #include "util/datatype.h" #include "expr/command.h" +#include "bindings/java_stream_adapters.h" + +std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %} %template(vectorCommandPtr) std::vector< CVC4::Command* >; @@ -72,7 +75,10 @@ using namespace CVC4; #ifdef SWIGJAVA -%exception { +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_stream_adapters.h" + +%exception %{ try { $action } catch(CVC4::Exception& e) { @@ -81,12 +87,19 @@ using namespace CVC4; std::string explanation = ss.str(); SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str()); } -} +%} // Create a mapping from C++ Exceptions to Java Exceptions. // This is in a couple of throws typemaps, simply because it's sensitive to SWIG's concept of which namespace we're in. %typemap(throws) Exception %{ - jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/$1_type"); + std::string name = "edu/nyu/acsys/$1_type"; + size_t i = name.find("::"); + if(i != std::string::npos) { + size_t j = name.rfind("::"); + assert(i <= j); + name.replace(i, j - i + 2, "/"); + } + jclass clazz = jenv->FindClass(name.c_str()); assert(clazz != NULL && jenv->ExceptionOccurred() == NULL); jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V"); assert(method != NULL && jenv->ExceptionOccurred() == NULL); @@ -97,8 +110,11 @@ using namespace CVC4; %} %typemap(throws) CVC4::Exception %{ std::string name = "edu/nyu/acsys/$1_type"; - for(size_t i = name.find("::"); i != std::string::npos; i = name.find("::")) { - name.replace(i, 2, "/"); + size_t i = name.find("::"); + if(i != std::string::npos) { + size_t j = name.rfind("::"); + assert(i <= j); + name.replace(i, j - i + 2, "/"); } jclass clazz = jenv->FindClass(name.c_str()); assert(clazz != NULL && jenv->ExceptionOccurred() == NULL); @@ -146,6 +162,76 @@ using namespace CVC4; post=" new java.io.PrintStream($javainput).print(temp$javainput.toString());") std::ostream& "edu.nyu.acsys.CVC4.JavaOutputStreamAdapter.getCPtr(temp$javainput)" +%typemap(jni) std::istream& "jlong" +%typemap(jtype) std::istream& "long" +%typemap(jstype) std::istream& "java.io.InputStream" +%typemap(javain, + pre=" edu.nyu.acsys.CVC4.JavaInputStreamAdapter temp$javainput = edu.nyu.acsys.CVC4.JavaInputStreamAdapter.get($javainput);", pgcppname="temp$javainput", + post="") + std::istream& "edu.nyu.acsys.CVC4.JavaInputStreamAdapter.getCPtr(temp$javainput)" +%typemap(in) jobject inputStream %{ + $1 = jenv->NewGlobalRef($input); +%} +%typemap(out) CVC4::JavaInputStreamAdapter* %{ + $1->pull(jenv); + *(CVC4::JavaInputStreamAdapter **)&$result = $1; +%} +%typemap(javacode) CVC4::JavaInputStreamAdapter %{ + private static java.util.HashMap streams = new java.util.HashMap(); + public static JavaInputStreamAdapter get(java.io.InputStream is) { + if(streams.containsKey(is)) { + return (JavaInputStreamAdapter) streams.get(is); + } + JavaInputStreamAdapter adapter = new JavaInputStreamAdapter(is); + streams.put(is, adapter); + return adapter; + } +%} +%typemap(javafinalize) CVC4::JavaInputStreamAdapter %{ + protected void finalize() { + streams.remove(getInputStream()); + delete(); + } +%} +%ignore CVC4::JavaInputStreamAdapter::init(JNIEnv*); +%ignore CVC4::JavaInputStreamAdapter::pullAdapters(JNIEnv*); +%javamethodmodifiers CVC4::JavaInputStreamAdapter::getInputStream() const "private"; +%javamethodmodifiers CVC4::JavaInputStreamAdapter::JavaInputStreamAdapter(jobject) "private"; + +%exception CVC4::parser::Parser::nextCommand() %{ + try { + CVC4::JavaInputStreamAdapter::pullAdapters(jenv); + $action + } catch(CVC4::Exception& e) { + std::stringstream ss; + ss << e.what() << ": " << e.getMessage(); + std::string explanation = ss.str(); + SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str()); + } +%} +%exception CVC4::parser::Parser::nextExpression() %{ + try { + CVC4::JavaInputStreamAdapter::pullAdapters(jenv); + $action + } catch(CVC4::Exception& e) { + std::stringstream ss; + ss << e.what() << ": " << e.getMessage(); + std::string explanation = ss.str(); + SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str()); + } +%} +%exception CVC4::JavaInputStreamAdapter::~JavaInputStreamAdapter() %{ + try { + jenv->DeleteGlobalRef(arg1->getInputStream()); + $action + } catch(CVC4::Exception& e) { + std::stringstream ss; + ss << e.what() << ": " << e.getMessage(); + std::string explanation = ss.str(); + SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str()); + } +%} + #endif /* SWIGJAVA */ %include "util/integer.i" diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp index 31963eee0..ecd31a4cc 100644 --- a/src/decision/relevancy.cpp +++ b/src/decision/relevancy.cpp @@ -28,6 +28,11 @@ // Relevancy stuff +const double Relevancy::secondsPerDecision = 0.001; +const double Relevancy::secondsPerExpense = 1e-7; +const double Relevancy::EPS = 1e-9; + + void Relevancy::setJustified(TNode n) { Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl; diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h index bfd30ddde..23d980a1b 100644 --- a/src/decision/relevancy.h +++ b/src/decision/relevancy.h @@ -109,9 +109,10 @@ class Relevancy : public RelevancyStrategy { bool d_multipleBacktrace; //bool d_computeRelevancy; // are we in a mode where we compute relevancy? - static const double secondsPerDecision = 0.001; - static const double secondsPerExpense = 1e-7; - static const double EPS = 1e-9; + static const double secondsPerDecision; + static const double secondsPerExpense; + static const double EPS; + /** Maximum time this algorithm should spent as part of whole algorithm */ double d_maxTimeAsPercentageOfTotalTime; diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 5159f6b5a..eab41ee38 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -936,7 +936,7 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr ("export of types belonging to theory of DATATYPES kinds unsupported"); } if(n.getMetaKind() == kind::metakind::PARAMETERIZED && - n.getKind() != kind::SORT_TYPE) { + n.getKind() != kind::SORT_TYPE) { throw ExportUnsupportedException ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported"); } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 5f813dbe8..bd3827f47 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -713,6 +713,10 @@ public: operator Node(); operator Node() const; + // similarly for TypeNode + operator TypeNode(); + operator TypeNode() const; + NodeBuilder<nchild_thresh>& operator&=(TNode); NodeBuilder<nchild_thresh>& operator|=(TNode); NodeBuilder<nchild_thresh>& operator+=(TNode); @@ -902,6 +906,16 @@ NodeBuilder<nchild_thresh>::operator Node() const { } template <unsigned nchild_thresh> +NodeBuilder<nchild_thresh>::operator TypeNode() { + return constructTypeNode(); +} + +template <unsigned nchild_thresh> +NodeBuilder<nchild_thresh>::operator TypeNode() const { + return constructTypeNode(); +} + +template <unsigned nchild_thresh> expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 236f48017..7522b8110 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -94,15 +94,32 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) { return true; } - if(isTuple() != t.isTuple() || isRecord() != t.isRecord() || - getNumChildren() != t.getNumChildren()) { + if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) { return false; } - // children must be subtypes of t's, in order - for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) { - if(!(*i).isSubtypeOf(*j)) { + if(isTuple()) { + if(getNumChildren() != t.getNumChildren()) { return false; } + // children must be subtypes of t's, in order + for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) { + if(!(*i).isSubtypeOf(*j)) { + return false; + } + } + } else { + const Record& r1 = getConst<Record>(); + const Record& r2 = t.getConst<Record>(); + if(r1.getNumFields() != r2.getNumFields()) { + return false; + } + // r1's fields must be subtypes of r2's, in order + // names must match also + for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) { + if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) { + return false; + } + } } return true; } @@ -125,15 +142,32 @@ bool TypeNode::isComparableTo(TypeNode t) const { NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) { return true; } - if(isTuple() != t.isTuple() || isRecord() != t.isRecord() || - getNumChildren() != t.getNumChildren()) { + if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) { return false; } - // children must be comparable to t's, in order - for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) { - if(!(*i).isComparableTo(*j)) { + if(isTuple()) { + if(getNumChildren() != t.getNumChildren()) { + return false; + } + // children must be comparable to t's, in order + for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) { + if(!(*i).isComparableTo(*j)) { + return false; + } + } + } else { + const Record& r1 = getConst<Record>(); + const Record& r2 = t.getConst<Record>(); + if(r1.getNumFields() != r2.getNumFields()) { return false; } + // r1's fields must be comparable to r2's, in order + // names must match also + for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) { + if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) { + return false; + } + } } return true; } else { diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 0e71e1539..45ee52121 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -123,17 +123,14 @@ void CommandExecutorPortfolio::lemmaSharingInit() } /* Output to string stream */ - if(d_options[options::verbosity] == 0 - || d_options[options::separateOutput]) { - assert(d_ostringstreams.size() == 0); - for(unsigned i = 0; i < d_numThreads; ++i) { - d_ostringstreams.push_back(new ostringstream); - d_threadOptions[i].set(options::out, d_ostringstreams[i]); - - // important even for muzzled builds (to get result output right) - *d_threadOptions[i][options::out] - << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]); - } + assert(d_ostringstreams.size() == 0); + for(unsigned i = 0; i < d_numThreads; ++i) { + d_ostringstreams.push_back(new ostringstream); + d_threadOptions[i].set(options::out, d_ostringstreams[i]); + + // important even for muzzled builds (to get result output right) + *d_threadOptions[i][options::out] + << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]); } } }/* CommandExecutorPortfolio::lemmaSharingInit() */ @@ -208,7 +205,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported, - d_threadOptions[d_lastWinner][options::out]); + d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL); if(d_lastWinner != 0) delete cmdExported; return ret; } else if(mode == 1) { // portfolio @@ -274,7 +271,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) fns[i] = boost::bind(smtEngineInvoke, d_smts[i], seqs[i], - d_threadOptions[i][options::out] + d_options[options::verbosity] >= -1 ? d_threadOptions[i][options::out] : NULL ); } @@ -332,7 +329,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported, - d_threadOptions[d_lastWinner][options::out]); + d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL); if(d_lastWinner != 0) delete cmdExported; return ret; } else { diff --git a/src/main/options b/src/main/options index caea63f5a..14a7a9f3f 100644 --- a/src/main/options +++ b/src/main/options @@ -31,8 +31,6 @@ option threadArgv std::vector<std::string> :include <vector> <string> Thread configuration (a string to be passed to parseOptions) option thread_id int :default -1 Thread ID, for internal use in case of multi-threaded run -option separateOutput bool :default false - In multi-threaded setting print output of each thread at the end of run, separated by a divider ("----"). option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write don't share (among portfolio threads) lemmas strictly longer than N option fallbackSequential --fallback-sequential bool :default false diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 020db0d50..89f6c8db5 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -185,8 +185,9 @@ public: std::string getUnparsedText(); /** Get the ANTLR3 lexer for this input. */ - pANTLR3_LEXER getAntlr3Lexer(){ return d_lexer; }; + pANTLR3_LEXER getAntlr3Lexer() { return d_lexer; } + pANTLR3_INPUT_STREAM getAntlr3InputStream() { return d_antlr3InputStream; } protected: /** Create an input. This input takes ownership of the given input stream, * and will delete it at destruction time. diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp index 8c4f1b0be..46853056b 100644 --- a/src/parser/antlr_line_buffered_input.cpp +++ b/src/parser/antlr_line_buffered_input.cpp @@ -21,15 +21,11 @@ #include <cassert> #include "util/output.h" +#include "parser/antlr_line_buffered_input.h" namespace CVC4 { namespace parser { -typedef struct ANTLR3_LINE_BUFFERED_INPUT_STREAM { - ANTLR3_INPUT_STREAM antlr; - std::istream* in; -} *pANTLR3_LINE_BUFFERED_INPUT_STREAM; - static pANTLR3_INPUT_STREAM antlr3CreateLineBufferedStream(std::istream& in); static void @@ -213,7 +209,9 @@ myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) { Debug("pipe") << "LA" << std::endl; if (( ((pANTLR3_UINT8)input->nextChar) + la - 1) >= (((pANTLR3_UINT8)input->data) + input->sizeBuf)) { - std::istream& in = *((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in; + std::istream& in = *((CVC4::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in; + //MGD + // in.clear(); if(!in) { Debug("pipe") << "EOF" << std::endl; return ANTLR3_CHARSTREAM_EOF; @@ -246,7 +244,7 @@ myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) { ++input->sizeBuf; } - Debug("pipe") << "READ POINTER[" << la << "] AT: >>" << std::string(((char*)input->nextChar), input->sizeBuf - (((char*)input->nextChar) - (char*)input->data) + 1) << "<< returning '" << (char)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << "' (" << (unsigned)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << ")" << std::endl; + Debug("pipe") << "READ POINTER[" << la << "] AT: >>" << std::string(((char*)input->nextChar), input->sizeBuf - (((char*)input->nextChar) - (char*)input->data)) << "<< returning '" << (char)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << "' (" << (unsigned)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << ")" << std::endl; return (ANTLR3_UCHAR)(*((pANTLR3_UINT8)input->nextChar + la - 1)); } @@ -356,7 +354,6 @@ antlr3CreateLineBufferedStream(std::istream& in) input->isAllocated = ANTLR3_FALSE; ((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in = ∈ - // Call the common 8 bit input stream handler // initialization. // diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h index 83df19a2d..fb0c16dbe 100644 --- a/src/parser/antlr_line_buffered_input.h +++ b/src/parser/antlr_line_buffered_input.h @@ -25,6 +25,11 @@ namespace CVC4 { namespace parser { +typedef struct ANTLR3_LINE_BUFFERED_INPUT_STREAM { + ANTLR3_INPUT_STREAM antlr; + std::istream* in; +} *pANTLR3_LINE_BUFFERED_INPUT_STREAM; + pANTLR3_INPUT_STREAM antlr3LineBufferedStreamNew(std::istream& in, ANTLR3_UINT32 encoding, pANTLR3_UINT8 name); diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index 6a6ae8609..108b67307 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -473,9 +473,11 @@ static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) { tokenStream = buffer->commonTstream; + /* if( buffer->done == ANTLR3_TRUE ) { return &(tokenStream->tstream->tokenSource->eofToken); } + */ /* Pick out the next token from the token source * Remember we just get a pointer (reference if you like) here diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 8b77362b2..90f17426b 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -446,26 +446,20 @@ Command* Parser::nextCommand() throw(ParserException) { if(!d_commandQueue.empty()) { cmd = d_commandQueue.front(); d_commandQueue.pop_front(); - if(cmd == NULL) { - setDone(); - } + setDone(cmd == NULL); } else { - if(!done()) { - try { - cmd = d_input->parseCommand(); - d_commandQueue.push_back(cmd); - cmd = d_commandQueue.front(); - d_commandQueue.pop_front(); - if(cmd == NULL) { - setDone(); - } - } catch(ParserException& e) { - setDone(); - throw; - } catch(exception& e) { - setDone(); - parseError(e.what()); - } + try { + cmd = d_input->parseCommand(); + d_commandQueue.push_back(cmd); + cmd = d_commandQueue.front(); + d_commandQueue.pop_front(); + setDone(cmd == NULL); + } catch(ParserException& e) { + setDone(); + throw; + } catch(exception& e) { + setDone(); + parseError(e.what()); } } Debug("parser") << "nextCommand() => " << cmd << std::endl; @@ -478,9 +472,7 @@ Expr Parser::nextExpression() throw(ParserException) { if(!done()) { try { result = d_input->parseExpr(); - if(result.isNull()) { - setDone(); - } + setDone(result.isNull()); } catch(ParserException& e) { setDone(); throw; diff --git a/src/parser/parser.i b/src/parser/parser.i index 5e10973d4..5b23555ea 100644 --- a/src/parser/parser.i +++ b/src/parser/parser.i @@ -9,14 +9,13 @@ namespace CVC4 { %ignore operator<<(std::ostream&, DeclarationCheck); %ignore operator<<(std::ostream&, SymbolType); - class ParserExprStream : public CVC4::ExprStream { - Parser* d_parser; - public: - ParserExprStream(Parser* parser) : d_parser(parser) {} - ~ParserExprStream() { delete d_parser; } - Expr nextExpr() { return d_parser->nextExpression(); } - };/* class Parser::ExprStream */ - + class ParserExprStream : public CVC4::ExprStream { + Parser* d_parser; + public: + ParserExprStream(Parser* parser) : d_parser(parser) {} + ~ParserExprStream() { delete d_parser; } + Expr nextExpr() { return d_parser->nextExpression(); } + };/* class Parser::ExprStream */ }/* namespace CVC4::parser */ }/* namespace CVC4 */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 2cfeaafc1..524344612 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -817,7 +817,7 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); if( options::modelUninterpDtEnum() && tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ - out << "DATATYPE " << std::endl; + out << "DATATYPE" << std::endl; out << " " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " = "; for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){ if (i>0) { @@ -1068,7 +1068,18 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr out << ',' << endl; } const Datatype& dt = (*i).getDatatype(); - out << " " << dt.getName() << " = "; + out << " " << dt.getName(); + if(dt.isParametric()) { + out << '['; + for(size_t j = 0; j < dt.getNumParameters(); ++j) { + if(j > 0) { + out << ','; + } + out << dt.getParameter(j); + } + out << ']'; + } + out << " = "; bool firstConstructor = true; for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) { if(! firstConstructor) { diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 35184e42e..09d8fcbd4 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -21,6 +21,8 @@ #include "smt/smt_engine.h" #include "theory/theory_engine.h" #include "theory/model.h" +#include "theory/booleans/boolean_term_conversion_mode.h" +#include "theory/booleans/options.h" #include "expr/kind.h" #include "util/hash.h" #include "util/bool.h" @@ -31,10 +33,56 @@ using namespace std; using namespace CVC4::theory; +using namespace CVC4::theory::booleans; namespace CVC4 { namespace smt { +BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) : + d_smt(smt), + d_ff(), + d_tt(), + d_ffDt(), + d_ttDt(), + d_termCache(), + d_typeCache() { + + // set up our "false" and "true" conversions based on command-line option + if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS || + options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_NATIVE) { + d_ff = NodeManager::currentNM()->mkConst(BitVector(1u, 0u)); + d_tt = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + } + if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS) { + d_ffDt = d_ff; + d_ttDt = d_tt; + } else { + Datatype spec("BooleanTerm"); + // don't change the order; false is assumed to come first by the model postprocessor + spec.addConstructor(DatatypeConstructor("BT_False")); + spec.addConstructor(DatatypeConstructor("BT_True")); + const Datatype& dt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(spec).getDatatype(); + d_ffDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_False"].getConstructor())); + d_ttDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_True"].getConstructor())); + // mark this datatype type as being special for Boolean term conversion + TypeNode::fromType(dt.getDatatypeType()).setAttribute(BooleanTermAttr(), Node::null()); + if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_DATATYPES) { + Assert(d_ff.isNull() && d_tt.isNull()); + d_ff = d_ffDt; + d_tt = d_ttDt; + } + } + + // assert that we set it up correctly + Assert(!d_ff.isNull() && !d_tt.isNull()); + Assert(!d_ffDt.isNull() && !d_ttDt.isNull()); + Assert(d_ff != d_tt); + Assert(d_ff.getType() == d_tt.getType()); + Assert(d_ffDt != d_ttDt); + Assert(d_ffDt.getType() == d_ttDt.getType()); + +}/* BooleanTermConverter::BooleanTermConverter() */ + static inline bool isBoolean(TNode top, unsigned i) { switch(top.getKind()) { case kind::NOT: @@ -63,27 +111,51 @@ static inline bool isBoolean(TNode top, unsigned i) { } } -const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype& dt) throw() { - return dt; - // boolean terms not supported in datatypes, yet +const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() { + const Datatype*& out = d_datatypeCache[&dt]; + if(out != NULL) { + return *out; + } - Debug("boolean-terms") << "booleanTermsConvertDatatype: considering " << dt.getName() << endl; + Debug("boolean-terms") << "convertDatatype: considering " << dt.getName() << endl; for(Datatype::const_iterator c = dt.begin(); c != dt.end(); ++c) { TypeNode t = TypeNode::fromType((*c).getConstructor().getType()); for(TypeNode::const_iterator a = t.begin(); a != t.end(); ++a) { - if((*a).isBoolean()) { - Datatype newDt(dt.getName() + "'"); + TypeNode converted = convertType(*a, true); + Debug("boolean-terms") << "GOT: " << converted << ":" << converted.getId() << endl; + if(*a != converted) { + SortConstructorType mySelfType; + set<Type> unresolvedTypes; + if(dt.isParametric()) { + mySelfType = NodeManager::currentNM()->toExprManager()->mkSortConstructor(dt.getName() + "'", dt.getNumParameters()); + unresolvedTypes.insert(mySelfType); + } + vector<Datatype> newDtVector; + if(dt.isParametric()) { + newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters())); + } else { + newDtVector.push_back(Datatype(dt.getName() + "'")); + } + Datatype& newDt = newDtVector.front(); Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl; for(c = dt.begin(); c != dt.end(); ++c) { DatatypeConstructor ctor((*c).getName() + "'", (*c).getTesterName() + "'"); t = TypeNode::fromType((*c).getConstructor().getType()); for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) { - if((*a).getType().getRangeType().isBoolean()) { - ctor.addArg((*a).getName() + "'", NodeManager::currentNM()->mkBitVectorType(1).toType()); - } else { - Type argType = (*a).getType().getRangeType(); - if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) { + Type argType = (*a).getType().getRangeType(); + if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) { + Debug("boolean-terms") << "argtype " << argType << " is self" << endl; + if(dt.isParametric()) { + Debug("boolean-terms") << "is-parametric self is " << mySelfType << endl; + ctor.addArg((*a).getName() + "'", mySelfType.instantiate(DatatypeType(argType).getDatatype().getParameters())); + } else { ctor.addArg((*a).getName() + "'", DatatypeSelfType()); + } + } else { + Debug("boolean-terms") << "argtype " << argType << " is NOT self" << endl; + converted = convertType(TypeNode::fromType(argType), true); + if(TypeNode::fromType(argType) != converted) { + ctor.addArg((*a).getName() + "'", converted.toType()); } else { ctor.addArg((*a).getName() + "'", argType); } @@ -91,22 +163,107 @@ const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype } newDt.addConstructor(ctor); } - DatatypeType newDtt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(newDt); + vector<DatatypeType> newDttVector = + NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes); + DatatypeType& newDtt = newDttVector.front(); const Datatype& newD = newDtt.getDatatype(); for(c = dt.begin(); c != dt.end(); ++c) { Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl; - d_booleanTermCache[make_pair(Node::fromExpr((*c).getConstructor()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()); - d_booleanTermCache[make_pair(Node::fromExpr((*c).getTester()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester()); + Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr? + Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl; + d_termCache[make_pair(Node::fromExpr((*c).getConstructor()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()); + d_termCache[make_pair(Node::fromExpr((*c).getTester()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester()); for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) { - d_booleanTermCache[make_pair(Node::fromExpr((*a).getSelector()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'")); + d_termCache[make_pair(Node::fromExpr((*a).getSelector()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'")); } } + out = &newD; return newD; } } } + + out = &dt; return dt; -}/* BooleanTermConverter::booleanTermsConvertDatatype() */ + +}/* BooleanTermConverter::convertDatatype() */ + +TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext) { + Debug("boolean-terms") << "CONVERT-TYPE[" << type << ":" << type.getId() << ", " << datatypesContext << "]" << endl; + // This function recursively converts the type. + if(type.isBoolean()) { + return datatypesContext ? d_ttDt.getType() : d_tt.getType(); + } + const pair<TypeNode, bool> cacheKey(type, datatypesContext); + if(d_typeCache.find(cacheKey) != d_typeCache.end()) { + TypeNode out = d_typeCache[cacheKey]; + return out.isNull() ? type : out; + } + TypeNode& outNode = d_typeCache[cacheKey]; + if(type.getKind() == kind::DATATYPE_TYPE || + type.getKind() == kind::PARAMETRIC_DATATYPE) { + bool parametric = (type.getKind() == kind::PARAMETRIC_DATATYPE); + const Datatype& dt = parametric ? type[0].getConst<Datatype>() : type.getConst<Datatype>(); + TypeNode out = TypeNode::fromType(convertDatatype(dt).getDatatypeType()); + Debug("boolean-terms") << "AFTER, got "<< out << " param:" << parametric << endl; + if(parametric) { + // re-parameterize the translation + vector<TypeNode> params = type.getParamTypes(); + for(size_t i = 0; i < params.size(); ++i) { + Debug("boolean-terms") << "in loop, got "<< params[i] << endl; + params[i] = convertType(params[i], true); + Debug("boolean-terms") << "in loop, convert to "<< params[i] << endl; + } + params.insert(params.begin(), out[0]); + out = NodeManager::currentNM()->mkTypeNode(kind::PARAMETRIC_DATATYPE, params); + Debug("boolean-terms") << "got OUT: " << out << endl; + } + if(out != type) { + outNode = out;// cache it + Debug("boolean-terms") << "OUT is same as TYPE" << endl; + } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl; + return out; + } + if(type.isRecord()) { + const Record& rec = type.getConst<Record>(); + vector< pair<string, Type> > flds; + for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) { + TypeNode converted = convertType(TypeNode::fromType((*i).second), true); + if(TypeNode::fromType((*i).second) != converted) { + flds.push_back(make_pair((*i).first, converted.toType())); + } else { + flds.push_back(*i); + } + } + TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds)); + Debug("tuprec") << "converted " << type << " to " << newRec << endl; + if(newRec != type) { + outNode = newRec;// cache it + } + return newRec; + } + if(type.getNumChildren() > 0) { + Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl; + // This should handle tuples and arrays ok. + // Might handle function types too, but they can't go + // in other types, so it doesn't matter. + NodeBuilder<> b(type.getKind()); + if(type.getMetaKind() == kind::metakind::PARAMETERIZED) { + b << type.getOperator(); + } + for(TypeNode::iterator i = type.begin(); i != type.end(); ++i) { + b << convertType(*i, false); + } + TypeNode out = b; + if(out != type) { + outNode = out;// cache it + } + Debug("boolean-terms") << "here at B, returning " << out << ":" << out.getId() << endl; + return out; + } + // leave the cache at Null + return type; +}/* BooleanTermConverter::convertType() */ // look for vars from "vars" that occur in a term-context in n; transfer them to output. static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TNode>& output, bool boolParent, std::hash_set< std::pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> >& alreadySeen) { @@ -134,11 +291,21 @@ static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TN } } -Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, std::map<TNode, Node>& quantBoolVars) throw() { - Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - boolParent=" << boolParent << endl; +Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw() { + Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl; + + // we only distinguish between datatypes, booleans, and "other", and we + // don't even distinguish datatypes except when in "native" conversion + // mode + if(parentTheory != theory::THEORY_BOOL) { + if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE || + parentTheory != theory::THEORY_DATATYPES) { + parentTheory = theory::THEORY_BUILTIN; + } + } - BooleanTermCache::iterator i = d_booleanTermCache.find(make_pair<Node, bool>(top, boolParent)); - if(i != d_booleanTermCache.end()) { + BooleanTermCache::iterator i = d_termCache.find(make_pair<Node, theory::TheoryId>(top, parentTheory)); + if(i != d_termCache.end()) { return (*i).second.isNull() ? Node(top) : (*i).second; } @@ -147,22 +314,24 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st NodeManager* nm = NodeManager::currentNM(); - Node one = nm->mkConst(BitVector(1u, 1u)); - Node zero = nm->mkConst(BitVector(1u, 0u)); - if(quantBoolVars.find(top) != quantBoolVars.end()) { // this Bool variable is quantified over and we're changing it to a BitVector var - if(boolParent) { - return quantBoolVars[top].eqNode(one); + if(parentTheory == theory::THEORY_BOOL) { + return quantBoolVars[top].eqNode(d_tt); } else { return quantBoolVars[top]; } } - if(!boolParent && top.getType().isBoolean()) { + if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) { // still need to rewrite e.g. function applications over boolean - Node topRewritten = rewriteBooleanTermsRec(top, true, quantBoolVars); - Node n = nm->mkNode(kind::ITE, topRewritten, one, zero); + Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars); + Node n; + if(parentTheory == theory::THEORY_DATATYPES) { + n = nm->mkNode(kind::ITE, topRewritten, d_ttDt, d_ffDt); + } else { + n = nm->mkNode(kind::ITE, topRewritten, d_tt, d_ff); + } Debug("boolean-terms") << "constructed ITE: " << n << endl; return n; } @@ -176,19 +345,19 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st if(constituentType.isBoolean()) { // we have store_all(true) or store_all(false) // just turn it into store_all(1) or store_all(0) - Node newConst = nm->mkConst(BitVector(1u, asa.getExpr().getConst<bool>() ? 1u : 0u)); if(indexType.isBoolean()) { // change index type to BV(1) also - indexType = nm->mkBitVectorType(1); + indexType = d_tt.getType(); } - ArrayStoreAll asaRepl(nm->mkArrayType(indexType, nm->mkBitVectorType(1)).toType(), newConst.toExpr()); + ArrayStoreAll asaRepl(nm->mkArrayType(indexType, d_tt.getType()).toType(), + (asa.getExpr().getConst<bool>() ? d_tt : d_ff).toExpr()); Node n = nm->mkConst(asaRepl); Debug("boolean-terms") << " returning new store_all: " << n << endl; return n; } if(indexType.isBoolean()) { // must change index type to BV(1) - indexType = nm->mkBitVectorType(1); + indexType = d_tt.getType(); ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr()); Node n = nm->mkConst(asaRepl); Debug("boolean-terms") << " returning new store_all: " << n << endl; @@ -200,9 +369,10 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st TypeNode t = top.getType(); if(t.isFunction()) { for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) { - if(t[i].isBoolean()) { + TypeNode newType = convertType(t[i], false); + if(newType != t[i]) { vector<TypeNode> argTypes = t.getArgTypes(); - replace(argTypes.begin(), argTypes.end(), t[i], nm->mkBitVectorType(1)); + replace(argTypes.begin(), argTypes.end(), t[i], d_tt.getType()); TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType()); Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__", newType, "a function introduced by Boolean-term conversion", @@ -216,7 +386,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st Node var = nm->mkBoundVar(t[j]); boundVarsBuilder << var; if(t[j].isBoolean()) { - bodyBuilder << nm->mkNode(kind::ITE, var, one, zero); + bodyBuilder << nm->mkNode(kind::ITE, var, d_tt, d_ff); } else { bodyBuilder << var; } @@ -226,105 +396,112 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st Node lam = nm->mkNode(kind::LAMBDA, boundVars, body); Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl; d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam); - d_booleanTermCache[make_pair(top, boolParent)] = n; + d_termCache[make_pair(top, parentTheory)] = n; return n; } } } else if(t.isArray()) { - TypeNode indexType = t.getArrayIndexType(); - TypeNode constituentType = t.getArrayConstituentType(); - bool rewrite = false; - if(indexType.isBoolean()) { - indexType = nm->mkBitVectorType(1); - rewrite = true; - } - if(constituentType.isBoolean()) { - constituentType = nm->mkBitVectorType(1); - rewrite = true; - } - if(rewrite) { + TypeNode indexType = convertType(t.getArrayIndexType(), false); + TypeNode constituentType = convertType(t.getArrayConstituentType(), false); + if(indexType != t.getArrayIndexType() || constituentType != t.getArrayConstituentType()) { TypeNode newType = nm->mkArrayType(indexType, constituentType); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()), + Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", newType, "an array variable introduced by Boolean-term conversion", NodeManager::SKOLEM_EXACT_NAME); top.setAttribute(BooleanTermAttr(), n); Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - Node n_zero = nm->mkNode(kind::SELECT, n, zero); - Node n_one = nm->mkNode(kind::SELECT, n, one); + Node n_ff = nm->mkNode(kind::SELECT, n, d_ff); + Node n_tt = nm->mkNode(kind::SELECT, n, d_tt); Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr())); Node repl = nm->mkNode(kind::STORE, nm->mkNode(kind::STORE, base, nm->mkConst(false), - nm->mkNode(kind::EQUAL, n_zero, one)), nm->mkConst(true), - nm->mkNode(kind::EQUAL, n_one, one)); + nm->mkNode(kind::EQUAL, n_ff, d_tt)), nm->mkConst(true), + nm->mkNode(kind::EQUAL, n_tt, d_tt)); Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl; d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl); - d_booleanTermCache[make_pair(top, boolParent)] = n; + d_termCache[make_pair(top, parentTheory)] = n; return n; } - d_booleanTermCache[make_pair(top, boolParent)] = Node::null(); + d_termCache[make_pair(top, parentTheory)] = Node::null(); return top; - } else if(t.isTuple()) { - return top; - } else if(t.isRecord()) { + } else if(t.isTuple() || t.isRecord()) { + TypeNode newType = convertType(t, true); + if(t != newType) { + Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", + newType, "a tuple/record variable introduced by Boolean-term conversion", + NodeManager::SKOLEM_EXACT_NAME); + top.setAttribute(BooleanTermAttr(), n); + n.setAttribute(BooleanTermAttr(), top); + Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl; + d_smt.d_theoryEngine->getModel()->addSubstitution(top, n); + Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; + d_termCache[make_pair(top, parentTheory)] = n; + return n; + } + d_termCache[make_pair(top, parentTheory)] = Node::null(); return top; - } else if(t.isDatatype()) { - return top;// no support for datatypes at present - const Datatype& dt = t.getConst<Datatype>(); - const Datatype& dt2 = booleanTermsConvertDatatype(dt); - if(dt != dt2) { - Assert(d_booleanTermCache.find(make_pair(top, boolParent)) == d_booleanTermCache.end(), + } else if(t.isDatatype() || t.isParametricDatatype()) { + Debug("boolean-terms") << "found a var of datatype type" << endl; + TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES); + if(t != newT) { + Assert(d_termCache.find(make_pair(top, parentTheory)) == d_termCache.end(), "Node `%s' already in cache ?!", top.toString().c_str()); - Assert(top.isVar()); - TypeNode newType = TypeNode::fromType(dt2.getDatatypeType()); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()), - newType, "an array variable introduced by Boolean-term conversion", + Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", + newT, "a datatype variable introduced by Boolean-term conversion", NodeManager::SKOLEM_EXACT_NAME); + Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl; top.setAttribute(BooleanTermAttr(), n); - Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - d_booleanTermCache[make_pair(top, boolParent)] = n; + d_smt.d_theoryEngine->getModel()->addSubstitution(top, n); + Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl; + d_termCache[make_pair(top, parentTheory)] = n; return n; } else { - d_booleanTermCache[make_pair(top, boolParent)] = Node::null(); + d_termCache[make_pair(top, parentTheory)] = Node::null(); return top; } } else if(t.isConstructor()) { - return top;// no support for datatypes at present - Assert(!boolParent); - const Datatype& dt = t[t.getNumChildren() - 1].getConst<Datatype>(); - const Datatype& dt2 = booleanTermsConvertDatatype(dt); + Assert(parentTheory != theory::THEORY_BOOL); + Assert(t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE || + t[t.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE); + const Datatype& dt = t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ? + t[t.getNumChildren() - 1].getConst<Datatype>() : + t[t.getNumChildren() - 1][0].getConst<Datatype>(); + TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); + const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>(); if(dt != dt2) { - Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(), + Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(), "constructor `%s' not in cache", top.toString().c_str()); - return d_booleanTermCache[make_pair(top, boolParent)]; - } else { - d_booleanTermCache[make_pair(top, boolParent)] = Node::null(); - return top; + return d_termCache[make_pair(top, parentTheory)]; } + d_termCache[make_pair(top, parentTheory)] = Node::null(); + return top; } else if(t.isTester() || t.isSelector()) { - return top;// no support for datatypes at present - Assert(!boolParent); - const Datatype& dt = t[0].getConst<Datatype>(); - const Datatype& dt2 = booleanTermsConvertDatatype(dt); + Assert(parentTheory != theory::THEORY_BOOL); + const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ? + t[0].getConst<Datatype>() : + t[0][0].getConst<Datatype>(); + TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); + const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>(); if(dt != dt2) { - Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(), + Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(), "tester or selector `%s' not in cache", top.toString().c_str()); - return d_booleanTermCache[make_pair(top, boolParent)]; + return d_termCache[make_pair(top, parentTheory)]; } else { - d_booleanTermCache[make_pair(top, boolParent)] = Node::null(); + d_termCache[make_pair(top, parentTheory)] = Node::null(); return top; } } else if(t.getNumChildren() > 0) { for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) { if((*i).isBoolean()) { vector<TypeNode> argTypes(t.begin(), t.end()); - replace(argTypes.begin(), argTypes.end(), *i, nm->mkBitVectorType(1)); + replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType()); TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes); Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()), newType, "a variable introduced by Boolean-term conversion", NodeManager::SKOLEM_EXACT_NAME); Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; top.setAttribute(BooleanTermAttr(), n); - d_booleanTermCache[make_pair(top, boolParent)] = n; + d_termCache[make_pair(top, parentTheory)] = n; return n; } } @@ -385,11 +562,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st } } Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars); - Node body = rewriteBooleanTermsRec(top[1], true, quantBoolVars); + Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars); Node quant = nm->mkNode(top.getKind(), boundVarList, body); Debug("bt") << "rewrote quantifier to -> " << quant << endl; - d_booleanTermCache[make_pair(top, true)] = quant; - d_booleanTermCache[make_pair(top, false)] = quant.iteNode(one, zero); + d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant; + d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff); + d_termCache[make_pair(top, theory::THEORY_DATATYPES)] = quant.iteNode(d_tt, d_ff); return quant; } } @@ -400,15 +578,20 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st NodeBuilder<> b(k); Debug("bt") << "looking at: " << top << endl; if(mk == kind::metakind::PARAMETERIZED) { - if(kindToTheoryId(k) != THEORY_BV && - k != kind::APPLY_TYPE_ASCRIPTION && - k != kind::TUPLE_SELECT && - k != kind::TUPLE_UPDATE && - k != kind::RECORD_SELECT && - k != kind::RECORD_UPDATE && - k != kind::RECORD) { + if(k == kind::RECORD) { + b << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES); + } else if(k == kind::APPLY_TYPE_ASCRIPTION) { + Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType())); + b << asc; + Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl; + asc.setAttribute(BooleanTermAttr(), top.getOperator()); + } else if(kindToTheoryId(k) != THEORY_BV && + k != kind::TUPLE_SELECT && + k != kind::TUPLE_UPDATE && + k != kind::RECORD_SELECT && + k != kind::RECORD_UPDATE) { Debug("bt") << "rewriting: " << top.getOperator() << endl; - b << rewriteBooleanTermsRec(top.getOperator(), false, quantBoolVars); + b << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars); Debug("bt") << "got: " << b.getOperator() << endl; } else { b << top.getOperator(); @@ -416,17 +599,21 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st } for(unsigned i = 0; i < top.getNumChildren(); ++i) { Debug("bt") << "rewriting: " << top[i] << endl; - b << rewriteBooleanTermsRec(top[i], isBoolean(top, i), quantBoolVars); + b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars); Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl; } Node n = b; Debug("boolean-terms") << "constructed: " << n << endl; - if(boolParent && - n.getType().isBitVector() && - n.getType().getBitVectorSize() == 1) { - n = nm->mkNode(kind::EQUAL, n, one); + if(parentTheory == theory::THEORY_BOOL) { + if(n.getType().isBitVector() && + n.getType().getBitVectorSize() == 1) { + n = nm->mkNode(kind::EQUAL, n, d_tt); + } else if(n.getType().isDatatype() && + n.getType().hasAttribute(BooleanTermAttr())) { + n = nm->mkNode(kind::EQUAL, n, d_ttDt); + } } - d_booleanTermCache[make_pair(top, boolParent)] = n; + d_termCache[make_pair(top, parentTheory)] = n; return n; } }/* BooleanTermConverter::rewriteBooleanTermsRec() */ diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index c53eadfa0..06f25f9ef 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -38,35 +38,64 @@ typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr; class BooleanTermConverter { /** The type of the Boolean term conversion cache */ - typedef std::hash_map< std::pair<Node, bool>, Node, + typedef std::hash_map< std::pair<Node, theory::TheoryId>, Node, PairHashFunction< Node, bool, - NodeHashFunction, std::hash<int> > > BooleanTermCache; + NodeHashFunction, std::hash<size_t> > > BooleanTermCache; + /** The type of the Boolean term conversion type cache */ + typedef std::hash_map< std::pair<TypeNode, bool>, TypeNode, + PairHashFunction< TypeNode, bool, + TypeNodeHashFunction, std::hash<int> > > BooleanTermTypeCache; + /** The type of the Boolean term conversion datatype cache */ + typedef std::hash_map<const Datatype*, const Datatype*, DatatypeHashFunction> BooleanTermDatatypeCache; /** The SmtEngine to which we're associated */ SmtEngine& d_smt; + /** The conversion for "false." */ + Node d_ff; + /** The conversion for "true." */ + Node d_tt; + /** The conversion for "false" when in datatypes contexts. */ + Node d_ffDt; + /** The conversion for "true" when in datatypes contexts. */ + Node d_ttDt; + /** The cache used during Boolean term conversion */ - BooleanTermCache d_booleanTermCache; + BooleanTermCache d_termCache; + /** The cache used during Boolean term type conversion */ + BooleanTermTypeCache d_typeCache; + /** The cache used during Boolean term datatype conversion */ + BooleanTermDatatypeCache d_datatypeCache; /** * Scan a datatype for and convert as necessary. */ - const Datatype& booleanTermsConvertDatatype(const Datatype& dt) throw(); + const Datatype& convertDatatype(const Datatype& dt) throw(); + + /** + * Convert a type. + */ + TypeNode convertType(TypeNode type, bool datatypesContext); - Node rewriteBooleanTermsRec(TNode n, bool boolParent, std::map<TNode, Node>& quantBoolVars) throw(); + Node rewriteBooleanTermsRec(TNode n, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw(); public: - BooleanTermConverter(SmtEngine& smt) : - d_smt(smt) { - } + /** + * Construct a Boolean-term converter associated to the given + * SmtEngine. + */ + BooleanTermConverter(SmtEngine& smt); /** - * We rewrite Boolean terms in assertions as bitvectors of length 1. + * Rewrite Boolean terms under a node. The node itself is not converted + * if boolParent is true, but its Boolean subterms appearing in a + * non-Boolean context will be rewritten. */ - Node rewriteBooleanTerms(TNode n, bool boolParent = true) throw() { + Node rewriteBooleanTerms(TNode n, bool boolParent = true, bool dtParent = false) throw() { std::map<TNode, Node> quantBoolVars; - return rewriteBooleanTermsRec(n, boolParent, quantBoolVars); + Assert(!(boolParent && dtParent)); + return rewriteBooleanTermsRec(n, boolParent ? theory::THEORY_BOOL : (dtParent ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars); } };/* class BooleanTermConverter */ diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index 26f5c9c60..fb80b27f7 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -17,37 +17,170 @@ #include "smt/model_postprocessor.h" #include "smt/boolean_terms.h" +using namespace std; using namespace CVC4; using namespace CVC4::smt; +Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { + if(n.getType().isSubtypeOf(asType)) { + // good to go, we have the right type + return n; + } + if(!n.isConst()) { + // we don't handle non-const right now + return n; + } + if(asType.isBoolean()) { + if(n.getType().isBitVector(1u)) { + // type mismatch: should only happen for Boolean-term conversion under + // datatype constructor applications; rewrite from BV(1) back to Boolean + bool tf = (n.getConst<BitVector>().getValue() == 1); + return NodeManager::currentNM()->mkConst(tf); + } + if(n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())) { + // type mismatch: should only happen for Boolean-term conversion under + // datatype constructor applications; rewrite from datatype back to Boolean + Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); + Assert(n.getNumChildren() == 0); + // we assume (by construction) false is first; see boolean_terms.cpp + bool tf = (Datatype::indexOf(n.getOperator().toExpr()) == 1); + Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << " ==> " << tf << endl; + return NodeManager::currentNM()->mkConst(tf); + } + } + Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl; + if(n.getType().isArray()) { + Assert(asType.isArray()); + if(n.getKind() == kind::STORE) { + return NodeManager::currentNM()->mkNode(kind::STORE, + rewriteAs(n[0], asType), + rewriteAs(n[1], asType[0]), + rewriteAs(n[2], asType[1])); + } + Assert(n.getKind() == kind::STORE_ALL); + const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>(); + Node val = rewriteAs(asa.getExpr(), asType[1]); + return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr())); + } + if(asType.getNumChildren() != n.getNumChildren() || + n.getMetaKind() == kind::metakind::CONSTANT) { + return n; + } + NodeBuilder<> b(n.getKind()); + TypeNode::iterator t = asType.begin(); + for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) { + Assert(t != asType.end()); + b << rewriteAs(*i, *t); + } + Assert(t == asType.end()); + Debug("boolean-terms") << "+++ constructing " << b << endl; + Node out = b; + return out; +} + void ModelPostprocessor::visit(TNode current, TNode parent) { - Debug("tuprec") << "visiting " << current << std::endl; + Debug("tuprec") << "visiting " << current << endl; Assert(!alreadyVisited(current, TNode::null())); if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) { Assert(current.getKind() == kind::APPLY_CONSTRUCTOR); + TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr()); NodeBuilder<> b(kind::TUPLE); - for(TNode::iterator i = current.begin(); i != current.end(); ++i) { + TypeNode::iterator t = expectType.begin(); + for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) { Assert(alreadyVisited(*i, TNode::null())); + Assert(t != expectType.end()); TNode n = d_nodes[*i]; - b << (n.isNull() ? *i : n); + n = n.isNull() ? *i : n; + if(!n.getType().isSubtypeOf(*t)) { + Assert(n.getType().isBitVector(1u) || + (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr()))); + Assert(n.isConst()); + Assert((*t).isBoolean()); + if(n.getType().isBitVector(1u)) { + b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1)); + } else { + // we assume (by construction) false is first; see boolean_terms.cpp + b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1)); + } + } else { + b << n; + } } + Assert(t == expectType.end()); d_nodes[current] = b; - Debug("tuprec") << "returning " << d_nodes[current] << std::endl; + Debug("tuprec") << "returning " << d_nodes[current] << endl; + Assert(d_nodes[current].getType() == expectType); } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) { Assert(current.getKind() == kind::APPLY_CONSTRUCTOR); + TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr()); + const Record& expectRec = expectType.getConst<Record>(); NodeBuilder<> b(kind::RECORD); b << current.getType().getAttribute(expr::DatatypeRecordAttr()); - for(TNode::iterator i = current.begin(); i != current.end(); ++i) { + Record::const_iterator t = expectRec.begin(); + for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) { Assert(alreadyVisited(*i, TNode::null())); + Assert(t != expectRec.end()); TNode n = d_nodes[*i]; - b << (n.isNull() ? *i : n); + n = n.isNull() ? *i : n; + if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) { + Assert(n.getType().isBitVector(1u) || + (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr()))); + Assert(n.isConst()); + Assert((*t).second.isBoolean()); + if(n.getType().isBitVector(1u)) { + b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1)); + } else { + // we assume (by construction) false is first; see boolean_terms.cpp + b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1)); + } + } else { + b << n; + } } + Assert(t == expectRec.end()); d_nodes[current] = b; - Debug("tuprec") << "returning " << d_nodes[current] << std::endl; + Debug("tuprec") << "returning " << d_nodes[current] << endl; + Assert(d_nodes[current].getType() == expectType); + } else if(current.getKind() == kind::APPLY_CONSTRUCTOR && + ( current.getOperator().hasAttribute(BooleanTermAttr()) || + ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION && + current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) { + NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); + Node realOp; + if(current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION) { + TNode oldAsc = current.getOperator().getOperator(); + Debug("boolean-terms") << "old asc: " << oldAsc << endl; + Node newCons = current.getOperator()[0].getAttribute(BooleanTermAttr()); + Node newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().toType())); + Debug("boolean-terms") << "new asc: " << newAsc << endl; + if(newCons.getType().getRangeType().isParametricDatatype()) { + vector<TypeNode> oldParams = TypeNode::fromType(oldAsc.getConst<AscriptionType>().getType()).getRangeType().getParamTypes(); + vector<TypeNode> newParams = newCons.getType().getRangeType().getParamTypes(); + Assert(oldParams.size() == newParams.size() && oldParams.size() > 0); + newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().substitute(newParams.begin(), newParams.end(), oldParams.begin(), oldParams.end()).toType())); + } + realOp = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, newAsc, newCons); + } else { + realOp = current.getOperator().getAttribute(BooleanTermAttr()); + } + b << realOp; + Debug("boolean-terms") << "+ op " << b.getOperator() << endl; + TypeNode::iterator j = realOp.getType().begin(); + for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++j) { + Assert(j != realOp.getType().end()); + Assert(alreadyVisited(*i, TNode::null())); + TNode repl = d_nodes[*i]; + repl = repl.isNull() ? *i : repl; + Debug("boolean-terms") << "+ adding " << repl << " expecting " << *j << endl; + b << rewriteAs(repl, *j); + } + Node n = b; + Debug("boolean-terms") << "model-post: " << current << endl + << "- returning " << n << endl; + d_nodes[current] = n; } else { - Debug("tuprec") << "returning self" << std::endl; + Debug("tuprec") << "returning self for kind " << current.getKind() << endl; // rewrite to self d_nodes[current] = Node::null(); } }/* ModelPostprocessor::visit() */ - diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h index 08e6168d9..f727a3483 100644 --- a/src/smt/model_postprocessor.h +++ b/src/smt/model_postprocessor.h @@ -25,9 +25,12 @@ namespace CVC4 { namespace smt { class ModelPostprocessor { + std::hash_map<TNode, Node, TNodeHashFunction> d_nodes; + public: typedef Node return_type; - std::hash_map<TNode, Node, TNodeHashFunction> d_nodes; + + Node rewriteAs(TNode n, TypeNode asType); bool alreadyVisited(TNode current, TNode parent) { return d_nodes.find(current) != d_nodes.end(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e98bffc1e..147cea85b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -63,6 +63,8 @@ #include "theory/logic_info.h" #include "theory/options.h" #include "theory/booleans/circuit_propagator.h" +#include "theory/booleans/boolean_term_conversion_mode.h" +#include "theory/booleans/options.h" #include "util/ite_removal.h" #include "theory/model.h" #include "printer/printer.h" @@ -586,11 +588,13 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_cumulativeTimeUsed(0), d_cumulativeResourceUsed(0), d_status(), - d_private(new smt::SmtEnginePrivate(*this)), - d_statisticsRegistry(new StatisticsRegistry()), + d_private(NULL), + d_statisticsRegistry(NULL), d_stats(NULL) { SmtScope smts(this); + d_private = new smt::SmtEnginePrivate(*this); + d_statisticsRegistry = new StatisticsRegistry(); d_stats = new SmtEngineStatistics(); // We have mutual dependency here, so we add the prop engine to the theory @@ -2636,10 +2640,26 @@ void SmtEnginePrivate::processAssertions() { TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime); for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) { Node n = d_booleanTermConverter.rewriteBooleanTerms(d_assertionsToPreprocess[i]); - if(n != d_assertionsToPreprocess[i] && !d_smt.d_logic.isTheoryEnabled(theory::THEORY_BV)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(theory::THEORY_BV); - d_smt.d_logic.lock(); + if(n != d_assertionsToPreprocess[i]) { + switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) { + case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: + case booleans::BOOLEAN_TERM_CONVERT_NATIVE: + if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_BV)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(theory::THEORY_BV); + d_smt.d_logic.lock(); + } + break; + case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: + if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(theory::THEORY_DATATYPES); + d_smt.d_logic.lock(); + } + break; + default: + Unhandled(mode); + } } d_assertionsToPreprocess[i] = n; } @@ -3046,10 +3066,14 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log return quickCheck().asValidityResult(); } -Node SmtEngine::postprocess(TNode node) { +Node SmtEngine::postprocess(TNode node, TypeNode expectedType) { ModelPostprocessor mpost; NodeVisitor<ModelPostprocessor> visitor; - return visitor.run(mpost, node); + Node value = visitor.run(mpost, node); + Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl; + Node realValue = mpost.rewriteAs(value, expectedType); + Debug("boolean-terms") << "postproc: realval " << realValue << " expect type " << expectedType << endl; + return realValue; } Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) { @@ -3071,7 +3095,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep // Make sure all preprocessing is done d_private->processAssertions(); Node n = d_private->simplify(Node::fromExpr(e)); - n = postprocess(n); + n = postprocess(n, TypeNode::fromType(e.getType())); return n.toExpr(); } @@ -3093,7 +3117,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L } hash_map<Node, Node, NodeHashFunction> cache; Node n = d_private->expandDefinitions(Node::fromExpr(e), cache); - n = postprocess(n); + n = postprocess(n, TypeNode::fromType(e.getType())); return n.toExpr(); } @@ -3140,8 +3164,10 @@ Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, TypeCheckingExcep resultNode = m->getValue(n); } Trace("smt") << "--- got value " << n << " = " << resultNode << endl; - resultNode = postprocess(resultNode); + resultNode = postprocess(resultNode, n.getType()); Trace("smt") << "--- model-post returned " << resultNode << endl; + Trace("smt") << "--- model-post returned " << resultNode.getType() << endl; + Trace("smt") << "--- model-post expected " << n.getType() << endl; // type-check the result we got Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType())); @@ -3356,7 +3382,9 @@ void SmtEngine::checkModel(bool hardFailure) { // function symbol (since then the definition is recursive) if (val.getKind() == kind::LAMBDA) { // first apply the model substitutions we have so far + Debug("boolean-terms") << "applying subses to " << val[1] << endl; Node n = substitutions.apply(val[1]); + Debug("boolean-terms") << "++ got " << n << endl; // now check if n contains func by doing a substitution // [func->func2] and checking equality of the Nodes. // (this just a way to check if func is in n.) @@ -3391,6 +3419,7 @@ void SmtEngine::checkModel(bool hardFailure) { } // (3) checks complete, add the substitution + Debug("boolean-terms") << "cm: adding subs " << func << " :=> " << val << endl; substitutions.addSubstitution(func, val); } } @@ -3408,7 +3437,9 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl; // Apply our model value substitutions. + Debug("boolean-terms") << "applying subses to " << n << endl; n = substitutions.apply(n); + Debug("boolean-terms") << "++ got " << n << endl; Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl; // Simplify the result. diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index fecfba14a..525f90ffe 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -249,7 +249,7 @@ class CVC4_PUBLIC SmtEngine { * like turning datatypes back into tuples, length-1-bitvectors back * into booleans, etc. */ - Node postprocess(TNode n); + Node postprocess(TNode n, TypeNode expectedType); /** * This is something of an "init" procedure, but is idempotent; call diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index b30a399e4..b3760b239 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -3,7 +3,7 @@ AM_CPPFLAGS = \ -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = builtin booleans uf arith arrays bv datatypes quantifiers rewriterules +SUBDIRS = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules DIST_SUBDIRS = $(SUBDIRS) example noinst_LTLIBRARIES = libtheory.la diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index 8cb32de18..9d58ffa75 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -13,7 +13,10 @@ libbooleans_la_SOURCES = \ theory_bool_rewriter.h \ theory_bool_rewriter.cpp \ circuit_propagator.h \ - circuit_propagator.cpp + circuit_propagator.cpp \ + boolean_term_conversion_mode.h \ + boolean_term_conversion_mode.cpp EXTRA_DIST = \ - kinds + kinds \ + options_handlers.h diff --git a/src/theory/booleans/boolean_term_conversion_mode.cpp b/src/theory/booleans/boolean_term_conversion_mode.cpp new file mode 100644 index 000000000..f9d80835c --- /dev/null +++ b/src/theory/booleans/boolean_term_conversion_mode.cpp @@ -0,0 +1,41 @@ +/********************* */ +/*! \file boolean_term_conversion_mode.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include <iostream> +#include "theory/booleans/boolean_term_conversion_mode.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) { + switch(mode) { + case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: + out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS"; + break; + case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: + out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES"; + break; + case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE: + out << "BOOLEAN_TERM_CONVERT_NATIVE"; + break; + default: + out << "BooleanTermConversionMode!UNKNOWN"; + } + + return out; +} + +}/* CVC4 namespace */ diff --git a/src/theory/booleans/boolean_term_conversion_mode.h b/src/theory/booleans/boolean_term_conversion_mode.h new file mode 100644 index 000000000..6ca908df4 --- /dev/null +++ b/src/theory/booleans/boolean_term_conversion_mode.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file boolean_term_conversion_mode.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H +#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H + +#include <iostream> + +namespace CVC4 { +namespace theory { +namespace booleans { + +typedef enum { + /** + * Convert Boolean terms to bitvectors of size 1. + */ + BOOLEAN_TERM_CONVERT_TO_BITVECTORS, + /** + * Convert Boolean terms to enumerations in the Datatypes theory. + */ + BOOLEAN_TERM_CONVERT_TO_DATATYPES, + /** + * Convert Boolean terms to enumerations in the Datatypes theory IF + * used in a datatypes context, otherwise to a bitvector of size 1. + */ + BOOLEAN_TERM_CONVERT_NATIVE + +} BooleanTermConversionMode; + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */ diff --git a/src/theory/booleans/options b/src/theory/booleans/options index ae14de58b..6c571f30e 100644 --- a/src/theory/booleans/options +++ b/src/theory/booleans/options @@ -5,4 +5,7 @@ module BOOLEANS "theory/booleans/options.h" Boolean theory +option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "theory/booleans/boolean_term_conversion_mode.h" :handler CVC4::theory::booleans::stringToBooleanTermConversionMode :handler-include "theory/booleans/options_handlers.h" + policy for converting Boolean terms + endmodule diff --git a/src/theory/booleans/options_handlers.h b/src/theory/booleans/options_handlers.h new file mode 100644 index 000000000..2bf53b3d2 --- /dev/null +++ b/src/theory/booleans/options_handlers.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \file options_handlers.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H +#define __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H + +#include <string> + +namespace CVC4 { +namespace theory { +namespace booleans { + +static const std::string booleanTermConversionModeHelp = "\ +Boolean term conversion modes currently supported by the\n\ +--boolean-term-conversion-mode option:\n\ +\n\ +bitvectors [default]\n\ ++ Boolean terms are converted to bitvectors of size 1.\n\ +\n\ +datatypes\n\ ++ Boolean terms are converted to enumerations in the Datatype theory.\n\ +\n\ +native\n\ ++ Boolean terms are converted in a \"natural\" way depending on where they\n\ + are used. If in a datatype context, they are converted to an enumeration.\n\ + Elsewhere, they are converted to a bitvector of size 1.\n\ +"; + +inline BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "bitvectors") { + return BOOLEAN_TERM_CONVERT_TO_BITVECTORS; + } else if(optarg == "datatypes") { + return BOOLEAN_TERM_CONVERT_TO_DATATYPES; + } else if(optarg == "native") { + return BOOLEAN_TERM_CONVERT_NATIVE; + } else if(optarg == "help") { + puts(booleanTermConversionModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") + + optarg + "'. Try --boolean-term-conversion-mode help."); + } +} + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H */ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 352868f7b..a369fb572 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -79,7 +79,7 @@ class EqualityTypeRule { if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) { std::stringstream ss; - ss << "Subtypes must have a common type:" << std::endl; + ss << "Subexpressions must have a common base type:" << std::endl; ss << "Equation: " << n << std::endl; ss << "Type 1: " << lhsType << std::endl; ss << "Type 2: " << rhsType << std::endl; diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index cc589c5c3..6da3b8efc 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -438,7 +438,7 @@ Node Bitblaster::getVarValue(TNode a) { if (d_cnfStream->hasLiteral(bits[i])) { SatLiteral bit = d_cnfStream->getLiteral(bits[i]); bit_value = d_satSolver->value(bit); - Assert (bit_value != SAT_VALUE_UNKNOWN); + Assert (bit_value != SAT_VALUE_UNKNOWN); } else { // the bit is unconstrainted so we can give it an arbitrary value bit_value = SAT_VALUE_FALSE; @@ -453,7 +453,7 @@ void Bitblaster::collectModelInfo(TheoryModel* m) { __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin(); for (; it!= d_variables.end(); ++it) { TNode var = *it; - if ((Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) && hasValue(var)) { + if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { Node const_value = getVarValue(var); Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " << var << " " diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index 3dfeba140..6d2ed0cf6 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -458,3 +458,15 @@ BitVector InequalityGraph::getValueInModel(TNode node) const { Assert (hasModelValue(id)); return getValue(id); } + +void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) { + for (ModelValues::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { + TermId id = (*it).first; + BitVector value = (*it).second.value; + TNode var = getTermNode(id); + Node constant = utils::mkConst(value); + Node assignment = utils::mkNode(kind::EQUAL, var, constant); + assignments.push_back(assignment); + Debug("bitvector-model") << " " << var <<" => " << constant << "\n"; + } +} diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index b23ea7704..860302aa4 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -88,11 +88,11 @@ class InequalityGraph : public context::ContextNotifyObj{ {} }; - typedef context::CDHashMap<TermId, ModelValue> Model; + typedef context::CDHashMap<TermId, ModelValue> ModelValues; struct QueueComparator { - const Model* d_model; - QueueComparator(const Model* model) + const ModelValues* d_model; + QueueComparator(const ModelValues* model) : d_model(model) {} bool operator() (TermId left, TermId right) const { @@ -128,7 +128,7 @@ class InequalityGraph : public context::ContextNotifyObj{ std::vector<TNode> d_conflict; bool d_signed; - Model d_modelValues; + ModelValues d_modelValues; void initializeModelValue(TNode node); void setModelValue(TermId term, const ModelValue& mv); ModelValue getModelValue(TermId term) const; @@ -290,7 +290,9 @@ public: * * @return */ - BitVector getValueInModel(TNode a) const; + BitVector getValueInModel(TNode a) const; + + void getAllValuesInModel(std::vector<Node>& assignments); }; } diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 4389dc50d..ed90e0ebe 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -91,6 +91,7 @@ public: virtual void preRegister(TNode node) {} virtual void propagate(Theory::Effort e) {} virtual void collectModelInfo(TheoryModel* m) = 0; + virtual Node getModelValue(TNode var) = 0; virtual bool isComplete() = 0; virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0; virtual void addSharedTerm(TNode node) {} diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index c7387daf8..9c4a5c5b6 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -64,6 +64,7 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) { bool BitblastSolver::check(Theory::Effort e) { + Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; ++(d_statistics.d_numCallstoCheck); //// Eager bit-blasting if (options::bitvectorEagerBitblast()) { @@ -87,7 +88,8 @@ bool BitblastSolver::check(Theory::Effort e) { // Processing assertions while (!done()) { - TNode fact = get(); + TNode fact = get(); + Debug("bv-bitblast") << " fact " << fact << ")\n"; if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) { // Some atoms have not been bit-blasted yet d_bitblaster->bbAtom(fact); @@ -137,3 +139,7 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) { void BitblastSolver::collectModelInfo(TheoryModel* m) { return d_bitblaster->collectModelInfo(m); } + +Node BitblastSolver::getModelValue(TNode node) { + return d_bitblaster->getVarValue(node); +} diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index b05ac74cd..b6be84df5 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -50,6 +50,7 @@ public: void explain(TNode literal, std::vector<TNode>& assumptions); EqualityStatus getEqualityStatus(TNode a, TNode b); void collectModelInfo(TheoryModel* m); + Node getModelValue(TNode node); bool isComplete() { return true; } }; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 112f73083..15720885d 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -222,9 +222,92 @@ bool CoreSolver::check(Theory::Effort e) { // if (!ok) // return false; // } + + // if we are sat and in full check attempt to construct a model + if (Theory::fullEffort(e) && isComplete()) { + buildModel(); + } + return true; } +void CoreSolver::buildModel() { + Debug("bv-core") << "CoreSolver::buildModel() \n"; + d_modelValues.clear(); + TNodeSet constants; + TNodeSet constants_in_eq_engine; + // collect constants in equality engine + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); + while (!eqcs_i.isFinished()) { + TNode repr = *eqcs_i; + if (repr.getKind() == kind::CONST_BITVECTOR) { + // must check if it's just the constant + eq::EqClassIterator it(repr, &d_equalityEngine); + if (!(++it).isFinished()) { + constants.insert(repr); + constants_in_eq_engine.insert(repr); + } + } + ++eqcs_i; + } + // build repr to value map + + eqcs_i = eq::EqClassesIterator(&d_equalityEngine); + while (!eqcs_i.isFinished()) { + TNode repr = *eqcs_i; + ++eqcs_i; + TypeNode type = repr.getType(); + if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) { + Debug("bv-core-model") << " processing " << repr <<"\n"; + // we need to assign a value for it + TypeEnumerator te(type); + Node val; + do { + val = *te; + ++te; + // Debug("bv-core-model") << " trying value " << val << "\n"; + // Debug("bv-core-model") << " is in set? " << constants.count(val) << "\n"; + // Debug("bv-core-model") << " enumerator done? " << te.isFinished() << "\n"; + } while (constants.count(val) != 0 && !(te.isFinished())); + + if (te.isFinished() && constants.count(val) != 0) { + // if we cannot enumerate anymore values we just return the lemma stating that + // at least two of the representatives are equal. + std::vector<TNode> representatives; + representatives.push_back(repr); + + for (TNodeSet::const_iterator it = constants_in_eq_engine.begin(); + it != constants_in_eq_engine.end(); ++it) { + TNode constant = *it; + if (utils::getSize(constant) == utils::getSize(repr)) { + representatives.push_back(constant); + } + } + for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { + representatives.push_back(it->first); + } + std::vector<Node> equalities; + for (unsigned i = 0; i < representatives.size(); ++i) { + for (unsigned j = i + 1; j < representatives.size(); ++j) { + TNode a = representatives[i]; + TNode b = representatives[j]; + if (utils::getSize(a) == utils::getSize(b)) { + equalities.push_back(utils::mkNode(kind::EQUAL, a, b)); + } + } + } + Node lemma = utils::mkOr(equalities); + d_bv->lemma(lemma); + Debug("bv-core") << " lemma: " << lemma << "\n"; + return; + } + Debug("bv-core-model") << " " << repr << " => " << val <<"\n" ; + constants.insert(val); + d_modelValues[repr] = val; + } + } +} + bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { // Notify the equality engine if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) { @@ -297,8 +380,6 @@ void CoreSolver::conflict(TNode a, TNode b) { d_bv->setConflict(conflict); } - - void CoreSolver::collectModelInfo(TheoryModel* m) { if (Debug.isOn("bitvector-model")) { context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin(); @@ -310,6 +391,20 @@ void CoreSolver::collectModelInfo(TheoryModel* m) { set<Node> termSet; d_bv->computeRelevantTerms(termSet); m->assertEqualityEngine(&d_equalityEngine, &termSet); + if (isComplete()) { + Debug("bitvector-model") << "CoreSolver::collectModelInfo complete."; + for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { + Node a = it->first; + Node b = it->second; + m->assertEquality(a, b, true); + } + } +} + +Node CoreSolver::getModelValue(TNode var) { + Assert (isComplete()); + Assert (d_modelValues.find(var) != d_modelValues.end()); + return d_modelValues[d_equalityEngine.getRepresentative(var)]; } CoreSolver::Statistics::Statistics() diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 4a9d84f79..d04dc164f 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -31,6 +31,9 @@ class Base; * Bitvector equality solver */ class CoreSolver : public SubtheorySolver { + typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + struct Statistics { IntStat d_numCallstoCheck; Statistics(); @@ -69,7 +72,9 @@ class CoreSolver : public SubtheorySolver { Slicer* d_slicer; context::CDO<bool> d_isCoreTheory; /** To make sure we keep the explanations */ - context::CDHashSet<Node, NodeHashFunction> d_reasons; + context::CDHashSet<Node, NodeHashFunction> d_reasons; + ModelValue d_modelValues; + void buildModel(); bool assertFactToEqualityEngine(TNode fact, TNode reason); bool decomposeFact(TNode fact); Node getBaseDecomposition(TNode a, std::vector<TNode>& explanation); @@ -83,6 +88,7 @@ public: bool check(Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); void collectModelInfo(TheoryModel* m); + Node getModelValue(TNode var); void addSharedTerm(TNode t) { d_equalityEngine.addTriggerTerm(t, THEORY_BV); } diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 3d7339e88..27047f6af 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -153,6 +153,23 @@ void InequalitySolver::propagate(Theory::Effort e) { Assert (false); } +void InequalitySolver::collectModelInfo(TheoryModel* m) { + Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n"; + std::vector<Node> model; + d_inequalityGraph.getAllValuesInModel(model); + for (unsigned i = 0; i < model.size(); ++i) { + Assert (model[i].getKind() == kind::EQUAL); + m->assertEquality(model[i][0], model[i][1], true); + } +} + +Node InequalitySolver::getModelValue(TNode var) { + Assert (isComplete()); + Assert (d_inequalityGraph.hasValueInModel(var)); + BitVector val = d_inequalityGraph.getValueInModel(var); + return utils::mkConst(val); +} + InequalitySolver::Statistics::Statistics() : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0) { diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index bcf94dc8b..b19ebb381 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -54,7 +54,8 @@ public: void propagate(Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); bool isComplete() { return d_isComplete; } - void collectModelInfo(TheoryModel* m) {} + void collectModelInfo(TheoryModel* m); + Node getModelValue(TNode var); EqualityStatus getEqualityStatus(TNode a, TNode b); void assertFact(TNode fact); }; diff --git a/src/theory/bv/options b/src/theory/bv/options index 72db63c09..8e01c6572 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -14,4 +14,6 @@ option bitvectorShareLemmas --bitblast-share-lemmas bool option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool check the bitblasting eagerly +option bitvectorInequalitySolver --bv-inequality-solver bool + turn on the inequality solver for the bit-vector theory endmodule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 43e290175..8245fdbdc 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -52,10 +52,12 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_subtheories.push_back(core_solver); d_subtheoryMap[SUB_CORE] = core_solver; - SubtheorySolver* ineq_solver = new InequalitySolver(c, this); - d_subtheories.push_back(ineq_solver); - d_subtheoryMap[SUB_INEQUALITY] = ineq_solver; - + if (options::bitvectorInequalitySolver()) { + SubtheorySolver* ineq_solver = new InequalitySolver(c, this); + d_subtheories.push_back(ineq_solver); + d_subtheoryMap[SUB_INEQUALITY] = ineq_solver; + } + SubtheorySolver* bb_solver = new BitblastSolver(c, this); d_subtheories.push_back(bb_solver); d_subtheoryMap[SUB_BITBLAST] = bb_solver; @@ -164,8 +166,21 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(!inConflict()); // Assert (fullModel); // can only query full model for (unsigned i = 0; i < d_subtheories.size(); ++i) { - d_subtheories[i]->collectModelInfo(m); + if (d_subtheories[i]->isComplete()) { + d_subtheories[i]->collectModelInfo(m); + return; + } + } +} + +Node TheoryBV::getModelValue(TNode var) { + Assert(!inConflict()); + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + if (d_subtheories[i]->isComplete()) { + return d_subtheories[i]->getModelValue(var); + } } + Unreachable(); } void TheoryBV::propagate(Effort e) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 5d139e11f..6bc4bdaf6 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -125,6 +125,8 @@ private: EqualityStatus getEqualityStatus(TNode a, TNode b); + Node getModelValue(TNode var); + inline std::string indent() { std::string indentStr(getSatContext()->getLevel(), ' '); diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 98bc8041d..f8b9f010e 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -249,6 +249,32 @@ inline unsigned isPow2Const(TNode node) { typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +inline Node mkOr(const std::vector<Node>& nodes) { + std::set<TNode> all; + all.insert(nodes.begin(), nodes.end()); + + if (all.size() == 0) { + return mkTrue(); + } + + if (all.size() == 1) { + // All the same, or just one + return nodes[0]; + } + + + NodeBuilder<> disjunction(kind::OR); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + disjunction << *it; + ++ it; + } + + return disjunction; +}/* mkOr() */ + + inline Node mkAnd(const std::vector<TNode>& conjunctions) { std::set<TNode> all; all.insert(conjunctions.begin(), conjunctions.end()); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9e4f0de75..a3bec7af0 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -24,6 +24,7 @@ #include "theory/datatypes/theory_datatypes_type_rules.h" #include "theory/model.h" #include "smt/options.h" +#include "smt/boolean_terms.h" #include "theory/quantifiers/options.h" #include <map> @@ -311,15 +312,28 @@ Node TheoryDatatypes::ppRewrite(TNode in) { return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]); } + TypeNode t = in.getType(); + // we only care about tuples and records here if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE && in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) { + if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) { + Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl; + Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl; + if(t.isTuple()) { + Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl; + Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl; + NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr())); + } else { + Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl; + Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl; + NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr())); + } + } // nothing to do return in; } - TypeNode t = in.getType(); - if(t.hasAttribute(expr::DatatypeTupleAttr())) { t = t.getAttribute(expr::DatatypeTupleAttr()); } else if(t.hasAttribute(expr::DatatypeRecordAttr())) { diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 2a74f6d15..a4facdefe 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -176,7 +176,7 @@ class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> { void newEnumerators() { d_enumerators = new TypeEnumerator*[getType().getNumChildren()]; for(size_t i = 0; i < getType().getNumChildren(); ++i) { - d_enumerators[i] = NULL; + d_enumerators[i] = new TypeEnumerator(getType()[i]); } } @@ -205,9 +205,7 @@ public: if(te.d_enumerators != NULL) { newEnumerators(); for(size_t i = 0; i < getType().getNumChildren(); ++i) { - if(te.d_enumerators[i] != NULL) { - d_enumerators[i] = new TypeEnumerator(*te.d_enumerators[i]); - } + *d_enumerators[i] = TypeEnumerator(*te.d_enumerators[i]); } } } @@ -292,9 +290,7 @@ public: if(re.d_enumerators != NULL) { newEnumerators(); for(size_t i = 0; i < getType().getNumChildren(); ++i) { - if(re.d_enumerators[i] != NULL) { - d_enumerators[i] = new TypeEnumerator(*re.d_enumerators[i]); - } + *d_enumerators[i] = TypeEnumerator(*re.d_enumerators[i]); } } } diff --git a/src/theory/model.cpp b/src/theory/model.cpp index bbc51c9e0..42a5380e4 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -57,7 +57,7 @@ Node TheoryModel::getValue( TNode n ) const{ Expr TheoryModel::getValue( Expr expr ) const{ Node n = Node::fromExpr( expr ); Node ret = getValue( n ); - return d_smt.postprocess(ret).toExpr(); + return d_smt.postprocess(ret, TypeNode::fromType(expr.getType())).toExpr(); } /** get cardinality for sort */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 5b2032430..94cf9accd 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -516,6 +516,11 @@ public: virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } /** + * Return the model value of the give shared term (or null if not avalilable. + */ + virtual Node getModelValue(TNode var) { return Node::null(); } + + /** * Check the current assignment's consistency. * * An implementation of check() is required to either: diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f7f689850..b89ca8fa4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1129,6 +1129,11 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); } +Node TheoryEngine::getModelValue(TNode var) { + Assert(d_sharedTerms.isShared(var)); + return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); +} + static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { std::set<TNode> all; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index a3779f0e8..a8fe52498 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -709,6 +709,12 @@ public: */ theory::EqualityStatus getEqualityStatus(TNode a, TNode b); + /** + * Retruns the value that a theory that owns the type of var currently + * has (or null if none); + */ + Node getModelValue(TNode var); + private: /** Default visitor for pre-registration */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 389a17461..c5d2845bd 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -83,6 +83,11 @@ EqualityStatus Valuation::getEqualityStatus(TNode a, TNode b) { return d_engine->getEqualityStatus(a, b); } +Node Valuation::getModelValue(TNode var) { + return d_engine->getModelValue(var); +} + + Node Valuation::ensureLiteral(TNode n) { Debug("ensureLiteral") << "rewriting: " << n << std::endl; Node rewritten = Rewriter::rewrite(n); diff --git a/src/theory/valuation.h b/src/theory/valuation.h index f69bacc19..36e62a402 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -97,6 +97,11 @@ public: EqualityStatus getEqualityStatus(TNode a, TNode b); /** + * Returns the model value of the shared term (or null if not available). + */ + Node getModelValue(TNode var); + + /** * Ensure that the given node will have a designated SAT literal * that is definitionally equal to it. The result of this function * is a Node that can be queried via getSatValue(). diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 18ecbc316..574a57f19 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -820,7 +820,18 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { // can only output datatypes in the CVC4 native language Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); - os << "DATATYPE " << dt.getName() << " =" << endl; + os << "DATATYPE " << dt.getName(); + if(dt.isParametric()) { + os << '['; + for(size_t i = 0; i < dt.getNumParameters(); ++i) { + if(i > 0) { + os << ','; + } + os << dt.getParameter(i); + } + os << ']'; + } + os << " =" << endl; Datatype::const_iterator i = dt.begin(), i_end = dt.end(); if(i != i_end) { os << " "; diff --git a/src/util/datatype.h b/src/util/datatype.h index de38d8835..4b6894ef8 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -450,7 +450,7 @@ public: * Create a new Datatype of the given name, with the given * parameterization. */ - inline Datatype(std::string name, std::vector<Type>& params); + inline Datatype(std::string name, const std::vector<Type>& params); /** * Add a constructor to this Datatype. Constructor names need not @@ -620,7 +620,7 @@ inline Datatype::Datatype(std::string name) : d_self() { } -inline Datatype::Datatype(std::string name, std::vector<Type>& params) : +inline Datatype::Datatype(std::string name, const std::vector<Type>& params) : d_name(name), d_params(params), d_constructors(), diff --git a/src/util/dense_map.h b/src/util/dense_map.h index 222a761c3..b7d690811 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -98,7 +98,7 @@ public: return false; }else{ Assert(x < allocated()); - return d_posVector[x] != POSITION_SENTINEL; + return d_posVector[x] != +POSITION_SENTINEL; } } @@ -160,7 +160,7 @@ public: void pop_back() { Assert(!empty()); Key atBack = back(); - d_posVector[atBack] = POSITION_SENTINEL; + d_posVector[atBack] = +POSITION_SENTINEL; d_image[atBack] = T(); d_list.pop_back(); } @@ -195,7 +195,7 @@ public: void increaseSize(Key max){ Assert(max >= allocated()); - d_posVector.resize(max+1, POSITION_SENTINEL); + d_posVector.resize(max+1, +POSITION_SENTINEL); d_image.resize(max+1); } diff --git a/src/util/hash.h b/src/util/hash.h index 4d4094143..913358512 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -48,7 +48,7 @@ namespace CVC4 { struct StringHashFunction { size_t operator()(const std::string& str) const { - return std::hash<const char*>()(str.c_str()); + return __gnu_cxx::hash<const char*>()(str.c_str()); } };/* struct StringHashFunction */ diff --git a/src/util/statistics.i b/src/util/statistics.i index 74cee5f37..7f3bbe526 100644 --- a/src/util/statistics.i +++ b/src/util/statistics.i @@ -4,7 +4,7 @@ #ifdef SWIGJAVA #include "bindings/java_iterator_adapter.h" -#include "bindings/java_output_stream_adapter.h" +#include "bindings/java_stream_adapters.h" #endif /* SWIGJAVA */ %} @@ -72,7 +72,7 @@ #ifdef SWIGJAVA %include "bindings/java_iterator_adapter.h" -%include "bindings/java_output_stream_adapter.h" +%include "bindings/java_stream_adapters.h" %template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>; |