diff options
31 files changed, 256 insertions, 102 deletions
@@ -34,8 +34,9 @@ distclean maintainerclean: .PHONY: test test: check -.PHONY: doc +.PHONY: doc doc-internals doc: doc-builds +doc-internals: doc-internals-builds .PHONY: examples examples: all diff --git a/Makefile.builds.in b/Makefile.builds.in index 96dc8d3cf..dd2a394ae 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -22,6 +22,8 @@ include current @SET_MAKE@ # Set up some basic autoconf make vars +srcdir = @srcdir@ +builddir = @builddir@ install_sh = @install_sh@ mkinstalldirs = $(install_sh) -d exec_prefix = @exec_prefix@ @@ -213,7 +215,9 @@ TAGS tags: .PHONY: doc-builds doc-prereq doc-builds: doc-prereq - +(cd $(CURRENT_BUILD) && $(MAKE) doxygen-doc) + +(cd $(CURRENT_BUILD) && $(MAKE) doxygen-doc CVC4_DOXYGEN_INPUT="`builddir="$(builddir)" srcdir="$(srcdir)" "$(srcdir)/doc/find_public_interface.sh"`") +doc-internals-builds: doc-prereq + +(cd $(CURRENT_BUILD) && $(MAKE) doxygen-doc CVC4_DOXYGEN_INPUT="$(srcdir)/src src") doc-prereq: +(cd $(CURRENT_BUILD) && for dir in `find . -name Makefile | xargs grep -l BUILT_SOURCES`; do (cd `dirname "$$dir"`; (cat Makefile; echo 'doc-prereq: $$(BUILT_SOURCES)') | $(MAKE) -f- doc-prereq); done) diff --git a/config/doxygen.cfg b/config/doxygen.cfg index 78014290d..71d434959 100644 --- a/config/doxygen.cfg +++ b/config/doxygen.cfg @@ -568,8 +568,7 @@ WARN_LOGFILE = # directories like "/usr/src/myproject". Separate the files or directories # with spaces. -INPUT = $(SRCDIR)/src \ - src +INPUT = $(CVC4_DOXYGEN_INPUT) # This tag can be used to specify the character encoding of the source files # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is diff --git a/doc/find_public_interface.sh b/doc/find_public_interface.sh new file mode 100644 index 000000000..4609846f7 --- /dev/null +++ b/doc/find_public_interface.sh @@ -0,0 +1,20 @@ +#!/bin/bash +# +# Enumerates public interface headers, so that public-only documentation +# can be produced. +# + +cd "$(dirname "$0")" + +echo -n "\"$srcdir/src/include/cvc4.h\" " +echo -n "\"$srcdir/src/include/cvc4_public.h\" " +( (find "$builddir" -name '*.h' | xargs grep -l '^# *include *"cvc4.*_public\.h"'); \ + (find "$srcdir" -name '*.h' | xargs grep -l '^# *include *"cvc4.*_public\.h"'); \ +) | \ +while read f; do + if expr "$f" : ".*_\(template\|private\|test_utils\)\.h$" &>/dev/null; then + continue + fi + echo -n "\"$f\" " +done + diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 5129cd73a..dc82daec4 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -36,12 +36,13 @@ ${includes} #include "util/exception.h" #include "util/language.h" #include "util/hash.h" +#include "util/options.h" // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 45 "${template}" +#line 46 "${template}" namespace CVC4 { @@ -682,7 +683,12 @@ public: long& l = out.iword(s_iosIndex); if(l == 0) { // set the default print depth on this ostream - l = s_defaultPrintDepth; + if(Options::current() != NULL) { + l = Options::current()->defaultExprDepth; + } + if(l == 0) { + l = s_defaultPrintDepth; + } } return l; } @@ -877,9 +883,10 @@ class CVC4_PUBLIC ExprSetLanguage { /** * The default language to use, for ostreams that haven't yet had a - * setlanguage() applied to them. + * setlanguage() applied to them and where the current Options + * information isn't available. */ - static const int s_defaultLanguage = language::output::LANG_AST; + static const int s_defaultOutputLanguage = language::output::LANG_AST; /** * When this manipulator is used, the setting is stored here. @@ -902,7 +909,15 @@ public: if(l == 0) { // set the default language on this ostream // (offset by one to detect whether default has been set yet) - l = s_defaultLanguage + 1; + if(Options::current() != NULL) { + l = Options::current()->outputLanguage + 1; + } + if(l <= 0 || l > language::output::LANG_MAX) { + // if called from outside the library, we may not have options + // available to us at this point (or perhaps the output language + // is not set in Options). Default to something reasonable. + l = s_defaultOutputLanguage + 1; + } } return OutputLanguage(l - 1); } @@ -942,7 +957,7 @@ public: ${getConst_instantiations} -#line 946 "${template}" +#line 961 "${template}" namespace expr { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a2fddadfc..1abcf398b 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -336,8 +336,7 @@ TypeNode NodeManager::mkPredicateSubtype(Expr lambda) if(! tn.isPredicateLike() || tn.getArgTypes().size() != 1) { std::stringstream ss; - ss << Expr::setlanguage(Options::current()->outputLanguage) - << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; + ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; throw TypeCheckingExceptionPrivate(lambdan, ss.str()); } @@ -357,8 +356,7 @@ TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness) if(! tn.isPredicateLike() || tn.getArgTypes().size() != 1) { std::stringstream ss; - ss << Expr::setlanguage(Options::current()->outputLanguage) - << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; + ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; throw TypeCheckingExceptionPrivate(lambdan, ss.str()); } diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index 28aa2f884..1e983e86c 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -71,8 +71,6 @@ ${type_cardinalities} #line 72 "${template}" default: { std::stringstream ss; - ss << Expr::setlanguage(language::toOutputLanguage - ( Options::current()->inputLanguage )); ss << "A theory kinds file did not provide a cardinality " << "or cardinality computer for type:\n" << typeNode << "\nof kind " << k; @@ -84,7 +82,7 @@ ${type_cardinalities} inline bool isWellFounded(TypeConstant tc) { switch(tc) { ${type_constant_wellfoundednesses} -#line 88 "${template}" +#line 86 "${template}" default: { std::stringstream ss; ss << "No well-foundedness status known for type constant: " << tc; @@ -99,11 +97,9 @@ inline bool isWellFounded(TypeNode typeNode) { case TYPE_CONSTANT: return isWellFounded(typeNode.getConst<TypeConstant>()); ${type_wellfoundednesses} -#line 103 "${template}" +#line 101 "${template}" default: { std::stringstream ss; - ss << Expr::setlanguage(language::toOutputLanguage - ( Options::current()->inputLanguage )); ss << "A theory kinds file did not provide a well-foundedness " << "or well-foundedness computer for type:\n" << typeNode << "\nof kind " << k; @@ -115,7 +111,7 @@ ${type_wellfoundednesses} inline Node mkGroundTerm(TypeConstant tc) { switch(tc) { ${type_constant_groundterms} -#line 119 "${template}" +#line 115 "${template}" default: { std::stringstream ss; ss << "No ground term known for type constant: " << tc; @@ -130,11 +126,9 @@ inline Node mkGroundTerm(TypeNode typeNode) { case TYPE_CONSTANT: return mkGroundTerm(typeNode.getConst<TypeConstant>()); ${type_groundterms} -#line 134 "${template}" +#line 130 "${template}" default: { std::stringstream ss; - ss << Expr::setlanguage(language::toOutputLanguage - ( Options::current()->inputLanguage )); ss << "A theory kinds file did not provide a ground term " << "or ground term computer for type:\n" << typeNode << "\nof kind " << k; diff --git a/src/main/driver.cpp b/src/main/driver.cpp index 958175030..eda5df2ca 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -153,25 +153,9 @@ int runCvc4(int argc, char* argv[], Options& options) { } } - // Create the expression manager - ExprManager exprMgr(options); - - // Create the SmtEngine - SmtEngine smt(&exprMgr); - - // signal handlers need access - pStatistics = smt.getStatisticsRegistry(); - // Auto-detect input language by filename extension const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex]; - // Timer statistic - RegisterStatistic statTotalTime(exprMgr, &s_totalTime); - - // Filename statistics - ReferenceStat< const char* > s_statFilename("filename", filename); - RegisterStatistic statFilenameReg(exprMgr, &s_statFilename); - if(options.inputLanguage == language::input::LANG_AUTO) { if( inputFromStdin ) { // We can't do any fancy detection on stdin @@ -228,6 +212,15 @@ int runCvc4(int argc, char* argv[], Options& options) { << Expr::printtypes(false); } + // important even for muzzled builds (to get result output right) + *options.out << Expr::setlanguage(options.outputLanguage); + + // Create the expression manager + ExprManager exprMgr(options); + + // Create the SmtEngine + SmtEngine smt(&exprMgr); + Parser* replayParser = NULL; if( options.replayFilename != "" ) { ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options); @@ -245,8 +238,15 @@ int runCvc4(int argc, char* argv[], Options& options) { *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1); } - // important even for muzzled builds (to get result output right) - *options.out << Expr::setlanguage(options.outputLanguage); + // signal handlers need access + pStatistics = smt.getStatisticsRegistry(); + + // Timer statistic + RegisterStatistic statTotalTime(exprMgr, &s_totalTime); + + // Filename statistics + ReferenceStat< const char* > s_statFilename("filename", filename); + RegisterStatistic statFilenameReg(exprMgr, &s_statFilename); // Parse and execute commands until we are done Command* cmd; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 21f82f638..55e10724b 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -942,7 +942,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri i != i_end; ++i) { PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); - Expr func = EXPR_MANAGER->mkVar(*i, f.getType()); + Expr func = EXPR_MANAGER->mkVar(*i, t); PARSER_STATE->defineFunction(*i, f); Command* decl = new DefineFunctionCommand(*i, func, f); seq->addCommand(decl); @@ -2094,6 +2094,12 @@ NUMBER_OR_RANGEOP ) ; +// these empty fragments remove "no lexer rule corresponding to token" warnings +fragment INTEGER_LITERAL:; +fragment DECIMAL_LITERAL:; +fragment DOT:; +fragment DOTDOT:; + /** * Matches the hexidecimal digits (0-9, a-f, A-F) */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 07998b58f..84d75ceac 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -115,7 +115,11 @@ namespace CVC4 { #include "util/integer.h" #include "util/output.h" #include "util/rational.h" +#include "util/hash.h" #include <vector> +#include <set> +#include <string> +#include <sstream> using namespace CVC4; using namespace CVC4::parser; @@ -439,6 +443,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] std::string attr; Expr attexpr; std::vector<Expr> attexprs; + std::hash_set<std::string, StringHashFunction> names; + std::vector< std::pair<std::string, Expr> > binders; } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK @@ -540,8 +546,22 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK { PARSER_STATE->pushScope(); } - ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr, f2] RPAREN_TOK - { PARSER_STATE->defineVar(name,expr); } )+ + ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] term[expr, f2] RPAREN_TOK + // this is a parallel let, so we have to save up all the contributions + // of the let and define them only later on + { if(names.count(name) == 1) { + std::stringstream ss; + ss << "warning: symbol `" << name << "' bound multiple times by let; the last binding will be used, shadowing earlier ones"; + PARSER_STATE->warning(ss.str()); + } else { + names.insert(name); + } + binders.push_back(std::make_pair(name, expr)); } )+ + { // now implement these bindings + for(std::vector< std::pair<std::string, Expr> >::iterator i = binders.begin(); i != binders.end(); ++i) { + PARSER_STATE->defineVar((*i).first, (*i).second); + } + } RPAREN_TOK term[expr, f2] RPAREN_TOK diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 668b57b40..10d2aee8c 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -25,7 +25,8 @@ #include "theory/rewriter.h" #include "expr/expr_stream.h" #include "decision/decision_engine.h" - +#include "util/lemma_input_channel.h" +#include "util/lemma_output_channel.h" namespace CVC4 { namespace prop { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 97046a1ae..ddc45228e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -802,17 +802,32 @@ void SmtEngine::defineFunction(Expr func, Type formulaType = formula.getType(Options::current()->typeChecking); Type funcType = func.getType(); - Type rangeType = funcType.isFunction() ? - FunctionType(funcType).getRangeType() : funcType; - if(formulaType != rangeType) { - stringstream ss; - ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)) - << "Defined function's declared type does not match that of body\n" - << "The function : " << func << "\n" - << "Its range type: " << rangeType << "\n" - << "The body : " << formula << "\n" - << "Body type : " << formulaType; - throw TypeCheckingException(func, ss.str()); + // We distinguish here between definitions of constants and functions, + // because the type checking for them is subtly different. Perhaps we + // should instead have SmtEngine::defineFunction() and + // SmtEngine::defineConstant() for better clarity, although then that + // doesn't match the SMT-LIBv2 standard... + if(formals.size() > 0) { + Type rangeType = FunctionType(funcType).getRangeType(); + if(formulaType != rangeType) { + stringstream ss; + ss << "Type of defined function does not match its declaration\n" + << "The function : " << func << "\n" + << "Declared type : " << rangeType << "\n" + << "The body : " << formula << "\n" + << "Body type : " << formulaType; + throw TypeCheckingException(func, ss.str()); + } + } else { + if(formulaType != funcType) { + stringstream ss; + ss << "Declared type of defined constant does not match its definition\n" + << "The constant : " << func << "\n" + << "Declared type : " << funcType << "\n" + << "The definition : " << formula << "\n" + << "Definition type: " << formulaType; + throw TypeCheckingException(func, ss.str()); + } } TNode funcNode = func.getTNode(); vector<Node> formalsNodes; @@ -954,7 +969,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { Assert(Rewriter::rewrite(d_assertionsToPreprocess[i]) == d_assertionsToPreprocess[i]); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << endl; - d_propagator.assert(d_assertionsToPreprocess[i]); + d_propagator.assertTrue(d_assertionsToPreprocess[i]); } Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " @@ -1353,8 +1368,7 @@ bool SmtEnginePrivate::simplifyAssertions() // well-typed, and we don't want the C++ runtime to abort our // process without any error notice. stringstream ss; - ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)) - << "A bad expression was produced. Original exception follows:\n" + ss << "A bad expression was produced. Original exception follows:\n" << tcep; InternalError(ss.str().c_str()); } @@ -1573,8 +1587,7 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) { Type boolType = d_exprManager->booleanType(); if(type != boolType) { stringstream ss; - ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)) - << "Expected " << boolType << "\n" + ss << "Expected " << boolType << "\n" << "The assertion : " << e << "\n" << "Its type : " << type; throw TypeCheckingException(e, ss.str()); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 188f73c78..390ac280b 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1441,7 +1441,7 @@ void TheoryArith::check(Effort effortLevel){ while(!done()){ Constraint curr = constraintFromFactQueue(); if(curr != NullConstraint){ - bool res = assertionCases(curr); + bool res CVC4_UNUSED = assertionCases(curr); Assert(!res || inConflict()); } if(inConflict()){ break; } @@ -1453,7 +1453,7 @@ void TheoryArith::check(Effort effortLevel){ d_learnedBounds.pop(); Debug("arith::learned") << curr << endl; - bool res = assertionCases(curr); + bool res CVC4_UNUSED = assertionCases(curr); Assert(!res || inConflict()); if(inConflict()){ break; } diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 5f3f964de..63b44f7ca 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -29,11 +29,11 @@ namespace CVC4 { namespace theory { namespace booleans { -void CircuitPropagator::assert(TNode assertion) +void CircuitPropagator::assertTrue(TNode assertion) { if (assertion.getKind() == kind::AND) { for (unsigned i = 0; i < assertion.getNumChildren(); ++ i) { - assert(assertion[i]); + assertTrue(assertion[i]); } } else { // Analyze the assertion for back-edges and all that diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 04934b1fa..147a5927f 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -260,7 +260,7 @@ public: { d_context.pop(); } /** Assert for propagation */ - void assert(TNode assertion); + void assertTrue(TNode assertion); /** * Propagate through the asserted circuit propagator. New information discovered by the propagator diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 52d0defd1..9b0611ed8 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -51,7 +51,6 @@ class ApplyTypeRule { for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) { if((*argument_it).getType() != *argument_type_it) { std::stringstream ss; - ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)); ss << "argument types do not match the function type:\n" << "argument: " << *argument_it << "\n" << "has type: " << (*argument_it).getType() << "\n" @@ -81,7 +80,6 @@ class EqualityTypeRule { if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) { std::stringstream ss; - ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)); ss << "Subtypes must have a common type:" << std::endl; ss << "Equation: " << n << std::endl; ss << "Type 1: " << lhsType << std::endl; diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index bb6dfe40b..8cfdab5af 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -345,8 +345,10 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) { bits.push_back(utils::mkBitOf(node, i)); } - BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; - BVDebug("bitvector-bb") << " with bits " << toString(bits); + if(Debug.isOn("bitvector-bb")) { + BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << " with bits " << toString(bits); + } } void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) { @@ -363,7 +365,9 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) { bits.push_back(utils::mkTrue()); } } - BVDebug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; + if(Debug.isOn("bitvector-bb")) { + BVDebug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; + } } @@ -391,7 +395,9 @@ void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) { } } Assert (bits.size() == utils::getSize(node)); - BVDebug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; + if(Debug.isOn("bitvector-bb")) { + BVDebug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; + } } void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) { @@ -512,7 +518,9 @@ void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) { shiftAddMultiplier(res, current, newres); res = newres; } - BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + if(Debug.isOn("bitvector-bb")) { + BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + } } void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) { @@ -709,7 +717,9 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) { } } } - BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + if(Debug.isOn("bitvector-bb")) { + BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + } } void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) { @@ -740,7 +750,9 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) { } } } - BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + if(Debug.isOn("bitvector-bb")) { + BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + } } void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) { @@ -773,8 +785,9 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) { } } } - BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; - + if(Debug.isOn("bitvector-bb")) { + BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + } } void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) { @@ -791,9 +804,10 @@ void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) { } Assert (bits.size() == high - low + 1); - BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n"; - BVDebug("bitvector-bb") << " with bits " << toString(bits); - + if(Debug.isOn("bitvector-bb")) { + BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << " with bits " << toString(bits); + } } diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h index e43479381..1f15bffa8 100644 --- a/src/theory/bv/cd_set_collection.h +++ b/src/theory/bv/cd_set_collection.h @@ -72,8 +72,10 @@ class BacktrackableSetCollection { while (d_nodesInserted < d_memory.size()) { const tree_entry_type& node = d_memory.back(); - BVDebug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue() - << " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl; + if(Debug.isOn("cd_set_collection")) { + BVDebug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue() + << " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl; + } if (node.hasParent()) { if (node.isLeft()) { @@ -278,7 +280,9 @@ public: // Find the biggest node smaleer than value (it must exist) while (set != null) { - BVDebug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl; + if(Debug.isOn("set_collection")) { + BVDebug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl; + } const tree_entry_type& node = d_memory[set]; if (node.getValue() >= value) { // If the node is bigger than the value, we need a smaller one @@ -305,7 +309,9 @@ public: // Find the smallest node bigger than value (it must exist) while (set != null) { - BVDebug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl; + if(Debug.isOn("set_collection")) { + BVDebug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl; + } const tree_entry_type& node = d_memory[set]; if (node.getValue() <= value) { // If the node is smaller than the value, we need a bigger one @@ -372,7 +378,9 @@ public: backtrack(); Assert(isValid(set)); - BVDebug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl; + if(Debug.isOn("set_collection")) { + BVDebug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl; + } // Empty set no elements if (set == null) { diff --git a/src/theory/datatypes/explanation_manager.h b/src/theory/datatypes/explanation_manager.h index fa0d3f818..174b90ff5 100644 --- a/src/theory/datatypes/explanation_manager.h +++ b/src/theory/datatypes/explanation_manager.h @@ -104,7 +104,7 @@ class Explainer { public: /** assert that n is true */ - virtual void assert( Node n ) = 0; + virtual void assertTrue( Node n ) = 0; /** get the explanation for n. This should call pm->setExplanation( n1, jn1, r1 ) ... pm->setExplanation( nk, jnk, rk ) for some set of Nodes n1...nk. @@ -115,7 +115,7 @@ public: jni is the (at least informal) justification for ni. - Return value should be a (possibly empty) conjunction of nodes n'1...n'k, where each n'i occurs (as a conjunct) in jn1...jnk, but not in n1...nk. - For each of these literals n'i, assert( n'i ) was called. + For each of these literals n'i, assertTrue( n'i ) was called. - either pm->setExplanation( n, ... ) is called, or n is the return value. */ virtual Node explain( Node n, ProofManager* pm ) = 0; @@ -134,7 +134,7 @@ public: } ~CongruenceClosureExplainer(){} /** assert that n is true */ - void assert( Node n ){ + void assertTrue( Node n ){ Assert( n.getKind() == kind::EQUAL || n.getKind() == kind::IFF ); d_cc->addEquality( n ); } @@ -170,7 +170,7 @@ public: ~ExplanationManager(){} /** assert that n is true (n is an input) */ - void assert( Node n ) { + void assertTrue( Node n ) { //TODO: this can be optimized: // if the previous explanation for n was empty (n is a tautology), // then we should not claim it to be an input. @@ -219,4 +219,4 @@ public: } } -#endif
\ No newline at end of file +#endif diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 3b8efabb7..f9ef49c6b 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -124,7 +124,7 @@ void TheoryDatatypes::check(Effort e) { if( !hasConflict() ){ if( d_em.hasNode( assertion ) ){ Debug("datatypes") << "Assertion has already been derived" << endl; - d_em.assert( assertion ); + d_em.assertTrue( assertion ); } else { switch(assertion.getKind()) { case kind::EQUAL: @@ -949,7 +949,7 @@ void TheoryDatatypes::addEquality(TNode eq) { //setup merge pending list d_merge_pending.push_back( vector< pair< Node, Node > >() ); - d_cce.assert(eq); + d_cce.assertTrue(eq); d_cc.addTerm(eq[0]); d_cc.addTerm(eq[1]); @@ -979,7 +979,7 @@ void TheoryDatatypes::addEquality(TNode eq) { Debug("datatypes-ae") << " Find is " << find( eq[0] ) << " = " << find( eq[1] ) << std::endl; //merge original nodes merge( eq[0], eq[1] ); - d_cce.assert(eq); + d_cce.assertTrue(eq); d_cc.addTerm(eq[0]); d_cc.addTerm(eq[1]); #else @@ -987,7 +987,7 @@ void TheoryDatatypes::addEquality(TNode eq) { Debug("datatypes-ae") << " Find is " << find( eq[0] ) << " = " << find( eq[1] ) << std::endl; merge( eq[0], eq[1] ); if( !hasConflict() ){ - d_cce.assert(eq); + d_cce.assertTrue(eq); d_cc.addTerm(eq[0]); d_cc.addTerm(eq[1]); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4ab2c779c..50682f647 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -25,6 +25,7 @@ #include "expr/node.h" #include "expr/node_builder.h" #include "util/options.h" +#include "util/lemma_output_channel.h" #include "theory/theory.h" #include "theory/theory_engine.h" diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 2856e6a01..34a8a805b 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -46,8 +46,7 @@ public: TypeNode currentArgumentType = *argument_type_it; if(!currentArgument.isSubtypeOf(currentArgumentType)) { std::stringstream ss; - ss << Expr::setlanguage(Options::current()->outputLanguage) - << "argument type is not a subtype of the function's argument type:\n" + ss << "argument type is not a subtype of the function's argument type:\n" << "argument: " << *argument_it << "\n" << "has type: " << (*argument_it).getType() << "\n" << "not subtype: " << *argument_type_it; diff --git a/src/util/hash.h b/src/util/hash.h index fdfbf4087..6fb20dab0 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -26,6 +26,7 @@ namespace __gnu_cxx {} #include <ext/hash_map> +#include <ext/hash_set> namespace __gnu_cxx { diff --git a/src/util/options.cpp b/src/util/options.cpp index a10aae83d..2352ae503 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -87,6 +87,7 @@ Options::Options() : strictParsing(false), lazyDefinitionExpansion(false), printWinner(false), + defaultExprDepth(0), simplificationMode(SIMPLIFICATION_MODE_BATCH), simplificationModeSetByUser(false), decisionMode(DECISION_STRATEGY_INTERNAL), @@ -951,6 +952,7 @@ throw(OptionException) { Chat.getStream() << Expr::setdepth(depth); Message.getStream() << Expr::setdepth(depth); Warning.getStream() << Expr::setdepth(depth); + defaultExprDepth = depth; } break; diff --git a/src/util/options.h b/src/util/options.h index f3ae3b64e..f423260b0 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -27,8 +27,6 @@ #include "util/exception.h" #include "util/language.h" -#include "util/lemma_output_channel.h" -#include "util/lemma_input_channel.h" #include "util/tls.h" #include "theory/theoryof_mode.h" @@ -37,6 +35,8 @@ namespace CVC4 { class ExprStream; +class LemmaInputChannel; +class LemmaOutputChannel; /** Class representing an option-parsing exception. */ class CVC4_PUBLIC OptionException : public CVC4::Exception { @@ -112,6 +112,9 @@ struct CVC4_PUBLIC Options { /** Parallel Only: Whether the winner is printed at the end or not. */ bool printWinner; + /** The default expression depth to print on ostreams. */ + int defaultExprDepth; + /** Enumeration of simplification modes (when to simplify). */ typedef enum { /** Simplify the assertions as they come in */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 5eda230c3..58788c194 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -43,7 +43,8 @@ SMT2_TESTS = \ simple-lra.smt2 \ simple-rdl.smt2 \ simple-uf.smt2 \ - simplification_bug4.smt2 + simplification_bug4.smt2 \ + parallel-let.smt2 # Regression tests for PL inputs CVC_TESTS = \ @@ -115,7 +116,10 @@ BUG_TESTS = \ buggy-ite.smt2 \ bug303.smt2 \ bug310.cvc \ - bug339.smt2 + bug322.cvc \ + bug322b.cvc \ + bug339.smt2 \ + bug365.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug322.cvc b/test/regress/regress0/bug322.cvc new file mode 100644 index 000000000..c68fde795 --- /dev/null +++ b/test/regress/regress0/bug322.cvc @@ -0,0 +1,23 @@ +% EXPECT: sat +% EXIT: 10 +% Preamble -------------- +DATATYPE UNIT = Unit END; +DATATYPE BOOL = Truth | Falsity END; + +% Decls -------------- +node$type: TYPE; +value$type: TYPE; +Nodes$elem$type: TYPE = node$type; +Nodes$t$type: TYPE; +node_pair_set$type: TYPE = ARRAY node$type OF ARRAY node$type OF BOOL; +failure_pattern$type: TYPE = node_pair_set$type; +is_faulty:(node$type, failure_pattern$type) -> BOOL = (LAMBDA (p: node$type, + deliver: failure_pattern$type): + (IF (EXISTS (q: node$type): + (NOT ((((deliver)[ + (p)])[ + (q)]) = + (Truth)))) THEN + (Truth) ELSE (Falsity) ENDIF)); + +CHECKSAT; diff --git a/test/regress/regress0/bug322b.cvc b/test/regress/regress0/bug322b.cvc new file mode 100644 index 000000000..d10292dd5 --- /dev/null +++ b/test/regress/regress0/bug322b.cvc @@ -0,0 +1,12 @@ +% COMMAND-LINE: --incremental +% EXPECT: valid +% EXPECT: valid +% EXPECT: valid +% EXIT: 20 +x : INT; +y : INT = x + 1; +z : INT = -10; +identity : INT -> INT = LAMBDA(x:INT) : x; +QUERY identity(x) = x; +QUERY identity(y) > x; +QUERY identity(z) = -10; diff --git a/test/regress/regress0/bug365.smt2 b/test/regress/regress0/bug365.smt2 new file mode 100644 index 000000000..6dd48a849 --- /dev/null +++ b/test/regress/regress0/bug365.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_LIA) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(assert (let + ((a 2)) + (= a (let ((a 7)) a)))) +(check-sat) +(exit) + diff --git a/test/regress/regress0/datatypes/rec2.cvc b/test/regress/regress0/datatypes/rec2.cvc index 80aecfe25..49684241c 100644 --- a/test/regress/regress0/datatypes/rec2.cvc +++ b/test/regress/regress0/datatypes/rec2.cvc @@ -1,7 +1,7 @@ % EXPECT: valid % EXIT: 20 c : BOOLEAN; -a16 : [# _a : REAL, _b : REAL #] = ( +a16 : [# _a : INT, _b : INT #] = ( IF c THEN (# _a := 3, _b := 2 #) ELSE (# _a := 1, _b := 5 #) ENDIF WITH ._a := 2); diff --git a/test/regress/regress0/parallel-let.smt2 b/test/regress/regress0/parallel-let.smt2 new file mode 100644 index 000000000..1f12522ee --- /dev/null +++ b/test/regress/regress0/parallel-let.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_UF) +(set-info :status unsat) +(declare-sort U 0) +(declare-fun x () U) +(declare-fun y () U) +(assert (distinct x y)) +(assert (let ((x y) (y x)) (= x y))) +(check-sat) +(exit) |