summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-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
10 files changed, 55 insertions, 35 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback