diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/ite_utilities.cpp | 20 | ||||
-rw-r--r-- | src/theory/ite_utilities.h | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 22 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 7 |
7 files changed, 29 insertions, 62 deletions
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp index 1b4e096f2..a4af4f26f 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -28,6 +28,7 @@ namespace CVC4 { namespace theory { namespace ite { + inline static bool isTermITE(TNode e) { return (e.getKind() == kind::ITE && !e.getType().isBoolean()); } @@ -77,9 +78,7 @@ struct CTIVStackElement { } /* CVC4::theory::ite */ - - -ITEUtilities::ITEUtilities(ContainsTermITEVistor* containsVisitor) +ITEUtilities::ITEUtilities(ContainsTermITEVisitor* containsVisitor) : d_containsVisitor(containsVisitor) , d_compressor(NULL) , d_simplifier(NULL) @@ -144,11 +143,11 @@ void ITEUtilities::clear(){ } /********************* */ -/* ContainsTermITEVistor +/* ContainsTermITEVisitor */ -ContainsTermITEVistor::ContainsTermITEVistor(): d_cache() {} -ContainsTermITEVistor::~ContainsTermITEVistor(){} -bool ContainsTermITEVistor::containsTermITE(TNode e){ +ContainsTermITEVisitor::ContainsTermITEVisitor(): d_cache() {} +ContainsTermITEVisitor::~ContainsTermITEVisitor(){} +bool ContainsTermITEVisitor::containsTermITE(TNode e){ /* throughout execution skip through NOT nodes. */ e = (e.getKind() == kind::NOT) ? e[0] : e; if(ite::triviallyContainsNoTermITEs(e)){ return false; } @@ -197,7 +196,7 @@ bool ContainsTermITEVistor::containsTermITE(TNode e){ } return foundTermIte; } -void ContainsTermITEVistor::garbageCollect() { +void ContainsTermITEVisitor::garbageCollect() { d_cache.clear(); } @@ -249,7 +248,7 @@ void IncomingArcCounter::clear() { /********************* */ /* ITECompressor */ -ITECompressor::ITECompressor(ContainsTermITEVistor* contains) +ITECompressor::ITECompressor(ContainsTermITEVisitor* contains) : d_contains(contains) , d_assertions(NULL) , d_incoming(true, true) @@ -547,7 +546,7 @@ uint32_t TermITEHeightCounter::termITEHeight(TNode e){ -ITESimplifier::ITESimplifier(ContainsTermITEVistor* contains) +ITESimplifier::ITESimplifier(ContainsTermITEVisitor* contains) : d_containsVisitor(contains) , d_termITEHeight() , d_constantLeaves() @@ -1608,6 +1607,5 @@ Node ITECareSimplifier::simplifyWithCare(TNode e) return substitute(e, substTable, cache); } - } /* namespace theory */ } /* namespace CVC4 */ diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h index d9e6120aa..7f0986ecb 100644 --- a/src/theory/ite_utilities.h +++ b/src/theory/ite_utilities.h @@ -31,7 +31,7 @@ namespace CVC4 { namespace theory { -class ContainsTermITEVistor; +class ContainsTermITEVisitor; class IncomingArcCounter; class TermITEHeightCounter; class ITECompressor; @@ -40,7 +40,7 @@ class ITECareSimplifier; class ITEUtilities { public: - ITEUtilities(ContainsTermITEVistor* containsVisitor); + ITEUtilities(ContainsTermITEVisitor* containsVisitor); ~ITEUtilities(); Node simpITE(TNode assertion); @@ -55,7 +55,7 @@ public: void clear(); private: - ContainsTermITEVistor* d_containsVisitor; + ContainsTermITEVisitor* d_containsVisitor; ITECompressor* d_compressor; ITESimplifier* d_simplifier; ITECareSimplifier* d_careSimp; @@ -64,10 +64,10 @@ private: /** * A caching visitor that computes whether a node contains a term ite. */ -class ContainsTermITEVistor { +class ContainsTermITEVisitor { public: - ContainsTermITEVistor(); - ~ContainsTermITEVistor(); + ContainsTermITEVisitor(); + ~ContainsTermITEVisitor(); /** returns true if a node contains a term ite. */ bool containsTermITE(TNode n); @@ -140,7 +140,7 @@ private: */ class ITECompressor { public: - ITECompressor(ContainsTermITEVistor* contains); + ITECompressor(ContainsTermITEVisitor* contains); ~ITECompressor(); /* returns false if an assertion is discovered to be equal to false. */ @@ -153,7 +153,7 @@ private: Node d_true; /* Copy of true. */ Node d_false; /* Copy of false. */ - ContainsTermITEVistor* d_contains; + ContainsTermITEVisitor* d_contains; std::vector<Node>* d_assertions; IncomingArcCounter d_incoming; @@ -180,7 +180,7 @@ private: class ITESimplifier { public: - ITESimplifier(ContainsTermITEVistor* d_containsVisitor); + ITESimplifier(ContainsTermITEVisitor* d_containsVisitor); ~ITESimplifier(); Node simpITE(TNode assertion); @@ -192,7 +192,7 @@ private: Node d_true; Node d_false; - ContainsTermITEVistor* d_containsVisitor; + ContainsTermITEVisitor* d_containsVisitor; inline bool containsTermITE(TNode n) { return d_containsVisitor->containsTermITE(n); } diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 78f989807..e59874429 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -274,7 +274,7 @@ void BoundedIntegers::registerQuantifier( Node f ) { for( unsigned i=0; i<d_set[f].size(); i++) { Node v = d_set[f][i]; Node r = d_range[f][v]; - if( quantifiers::TermDb::hasBoundVarAttr(r) ){ + if( r.hasBoundVar() ){ //introduce a new bound Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" ); d_nground_range[f][v] = d_range[f][v]; @@ -384,5 +384,5 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node } bool BoundedIntegers::isGroundRange(Node f, Node v) { - return isBoundVar(f,v) && !quantifiers::TermDb::hasBoundVarAttr(getLowerBound(f,v)) && !quantifiers::TermDb::hasBoundVarAttr(getUpperBound(f,v)); + return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar(); } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 6d333521b..2967c77c8 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -42,8 +42,6 @@ option clauseSplit --clause-split bool :default false # forall x. P( x ) => f( S( x ) ) = x option preSkolemQuant --pre-skolem-quant bool :read-write :default false apply skolemization eagerly to bodies of quantified formulas -option iteRemoveQuant --ite-remove-quant bool :default false - apply ite removal to bodies of quantifiers # Whether to perform agressive miniscoping option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false perform aggressive miniscoping for quantifiers diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index ced4e1997..ae5a35a00 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -128,7 +128,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) registerNode( n[1], hasPol, pol, true );
}else{
if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){
- if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
+ if( n.hasBoundVar() ){
//literals
if( n.getKind()==EQUAL ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
@@ -162,7 +162,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) void QuantInfo::flatten( Node n, bool beneathQuant ) {
Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
- if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
+ if( n.hasBoundVar() ){
if( d_var_num.find( n )==d_var_num.end() ){
Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
d_var_num[n] = d_vars.size();
@@ -647,7 +647,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ d_type = typ_invalid;
}
}else{
- if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
+ if( n.hasBoundVar() ){
d_type_not = false;
d_n = n;
if( d_n.getKind()==NOT ){
@@ -693,7 +693,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ //literals
if( d_n.getKind()==EQUAL ){
for( unsigned i=0; i<2; i++ ){
- if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){
+ if( d_n[i].hasBoundVar() ){
if( !qi->isVar( d_n[i] ) ){
Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl;
}else if( d_n[i].getKind()==BOUND_VARIABLE && !beneathQuant ){
@@ -844,7 +844,7 @@ void MatchGen::reset_round( QuantConflictFind * p ) { }
}else if( d_type==typ_eq ){
for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
- if( !quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){
+ if( !d_n[i].hasBoundVar() ){
d_ground_eval[i] = p->evaluateTerm( d_n[i] );
}
}
@@ -1904,7 +1904,7 @@ void QuantConflictFind::computeRelevantEqr() { eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );
while( !eqc_i.isFinished() ){
TNode n = (*eqc_i);
- if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
+ if( n.hasBoundVar() ){
std::cout << "BAD TERM IN DB : " << n << std::endl;
exit( 199 );
}
@@ -1945,7 +1945,7 @@ void QuantConflictFind::computeRelevantEqr() { // std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;
// }
//}
- if( !quantifiers::TermDb::hasBoundVarAttr( n ) ){ //temporary
+ if( !n.hasBoundVar() ){ //temporary
bool isRedundant;
std::map< TNode, std::vector< TNode > >::iterator it_na;
@@ -2095,4 +2095,4 @@ QuantConflictFind::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_partial_inst);
}
-}
\ No newline at end of file +}
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 39ba3e8af..9a912130f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -348,28 +348,6 @@ bool TermDb::hasInstConstAttr( Node n ) { return !getInstConstAttr(n).isNull(); } -bool TermDb::hasBoundVarAttr( Node n ) { - if( !n.getAttribute(HasBoundVarComputedAttribute()) ){ - bool hasBv = false; - if( n.getKind()==BOUND_VARIABLE ){ - hasBv = true; - }else{ - for (unsigned i=0; i<n.getNumChildren(); i++) { - if( hasBoundVarAttr(n[i]) ){ - hasBv = true; - break; - } - } - } - HasBoundVarAttribute hbva; - n.setAttribute(hbva, hasBv); - HasBoundVarComputedAttribute hbvca; - n.setAttribute(hbvca, true); - Trace("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttribute()) << std::endl; - } - return n.getAttribute(HasBoundVarAttribute()); -} - void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) { if (n.getKind()==BOUND_VARIABLE ){ if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 860f087dd..66b45be2f 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -60,11 +60,6 @@ typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute; struct ModelBasisArgAttributeId {}; typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute; -struct HasBoundVarAttributeId {}; -typedef expr::Attribute<HasBoundVarAttributeId, bool> HasBoundVarAttribute; -struct HasBoundVarComputedAttributeId {}; -typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarComputedAttribute; - //for rewrite rules struct QRewriteRuleAttributeId {}; typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute; @@ -210,8 +205,6 @@ public: static bool hasInstConstAttr( Node n ); //for bound variables public: - //does n have bound variables? - static bool hasBoundVarAttr( Node n ); //get bound variables in n static void getBoundVars( Node n, std::vector< Node >& bvs); //for skolem |