diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-07 10:24:04 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-07 23:48:49 -0500 |
commit | d01269e2d5a02952fbda74dcd9629acfbf23dfd4 (patch) | |
tree | d8f2a90ddd94ade15edf84b48523e7ff76f78554 /src/theory/quantifiers | |
parent | 01cff049fac316d84ee05f747975a26b04e9c3a2 (diff) |
Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies; fix bug 551, improper ITE removal under quantifiers.
Diffstat (limited to 'src/theory/quantifiers')
-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 |
5 files changed, 10 insertions, 41 deletions
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 |