diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.cpp | 4 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 2 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 38 | ||||
-rw-r--r-- | src/theory/bv/cd_set_collection.h | 18 | ||||
-rw-r--r-- | src/theory/datatypes/explanation_manager.h | 10 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 8 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 3 |
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; |