summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/expr_template.h27
-rw-r--r--src/expr/node_manager.cpp6
-rw-r--r--src/expr/type_properties_template.h14
-rw-r--r--src/main/driver.cpp36
-rw-r--r--src/parser/cvc/Cvc.g8
-rw-r--r--src/parser/smt2/Smt2.g24
-rw-r--r--src/prop/theory_proxy.cpp3
-rw-r--r--src/smt/smt_engine.cpp45
-rw-r--r--src/theory/arith/theory_arith.cpp4
-rw-r--r--src/theory/booleans/circuit_propagator.cpp4
-rw-r--r--src/theory/booleans/circuit_propagator.h2
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h2
-rw-r--r--src/theory/bv/bitblast_strategies.cpp38
-rw-r--r--src/theory/bv/cd_set_collection.h18
-rw-r--r--src/theory/datatypes/explanation_manager.h10
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp8
-rw-r--r--src/theory/theory_engine.cpp1
-rw-r--r--src/theory/uf/theory_uf_type_rules.h3
-rw-r--r--src/util/hash.h1
-rw-r--r--src/util/options.cpp2
-rw-r--r--src/util/options.h7
21 files changed, 168 insertions, 95 deletions
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback