From 7a36dd1e29c6d0160f949d5f805044768fb549d1 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 16 Jun 2015 18:06:27 +0200 Subject: [PATCH] Avoid completion for large finite types. Fix bug for --fmf-fun. --- src/theory/quantifiers/quant_util.cpp | 5 ++--- src/theory/quantifiers/term_database.cpp | 19 +++++++++++++++++ src/theory/quantifiers/term_database.h | 4 ++++ src/theory/rep_set.cpp | 27 ++++++++++++++++++------ src/theory/rep_set.h | 2 +- src/theory/theory_model.h | 6 ------ 6 files changed, 47 insertions(+), 16 deletions(-) diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index c10f1db53..2c65b62b3 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -313,12 +313,11 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int } void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { - Assert( n.getKind()!=IMPLIES && n.getKind()!=XOR ); newHasPol = hasPol; newPol = pol; - if( n.getKind()==NOT ){ + if( n.getKind()==NOT || ( n.getKind()==IMPLIES && child==0 ) ){ newPol = !pol; - }else if( n.getKind()==IFF ){ + }else if( n.getKind()==IFF || n.getKind()==XOR ){ newHasPol = false; }else if( n.getKind()==ITE ){ if( child==0 ){ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index eba080a0e..2671f616b 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -409,6 +409,25 @@ bool TermDb::isInstClosure( Node r ) { return d_iclosure_processed.find( r )!=d_iclosure_processed.end(); } +//checks whether a type is reasonably small enough such that all of its domain elements can be enumerated +bool TermDb::mayComplete( TypeNode tn ) { + std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn ); + if( it==d_may_complete.end() ){ + bool mc = false; + if( !tn.isArray() && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){ + Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) ); + Node oth = NodeManager::currentNM()->mkConst( Rational(1000) ); + Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth ); + eq = Rewriter::rewrite( eq ); + mc = eq==d_true; + } + d_may_complete[tn] = mc; + return mc; + }else{ + return it->second; + } +} + void TermDb::setHasTerm( Node n ) { Trace("term-db-debug2") << "hasTerm : " << n << std::endl; //if( inst::Trigger::isAtomicTrigger( n ) ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 455287feb..b7fa4e999 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -137,6 +137,8 @@ private: NodeIntMap d_op_ccount; /** set has term */ void setHasTerm( Node n ); + /** may complete */ + std::map< TypeNode, bool > d_may_complete; public: TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); ~TermDb(){} @@ -191,6 +193,8 @@ public: Node getEligibleTermInEqc( TNode r ); /** is inst closure */ bool isInstClosure( Node r ); + /** may complete */ + bool mayComplete( TypeNode tn ); //for model basis private: //map from types to model basis terms diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 454fe8971..eb05564e5 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -15,6 +15,7 @@ #include "theory/rep_set.h" #include "theory/type_enumerator.h" #include "theory/quantifiers/bounded_integers.h" +#include "theory/quantifiers/term_database.h" using namespace std; using namespace CVC4; @@ -86,8 +87,15 @@ int RepSet::getIndexFor( Node n ) const { } } -void RepSet::complete( TypeNode t ){ - if( d_type_complete.find( t )==d_type_complete.end() ){ +bool RepSet::complete( TypeNode t ){ + std::map< TypeNode, bool >::iterator it = d_type_complete.find( t ); + if( it==d_type_complete.end() ){ + //remove all previous + for( unsigned i=0; isecond; } } @@ -165,6 +176,7 @@ bool RepSetIterator::setFunctionDomain( Node op ){ } bool RepSetIterator::initialize(){ + Trace("rsi") << "Initialize rep set iterator..." << std::endl; for( size_t i=0; ihasType( tn ) ){ Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" ); @@ -184,7 +197,7 @@ bool RepSetIterator::initialize(){ //check if it is bound if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){ if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){ - Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded integer." << std::endl; + Trace("rsi") << " variable is bounded integer." << std::endl; d_enum_type.push_back( ENUM_RANGE ); }else{ inc = true; @@ -195,18 +208,20 @@ bool RepSetIterator::initialize(){ if( inc ){ //check if it is otherwise bound if( d_bounds[0].find(i)!=d_bounds[0].end() && d_bounds[1].find(i)!=d_bounds[1].end() ){ - Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded." << std::endl; + Trace("rsi") << " variable is bounded." << std::endl; d_enum_type.push_back( ENUM_RANGE ); }else{ + Trace("rsi") << " variable cannot be bounded." << std::endl; Trace("fmf-incomplete") << "Incomplete because of integer quantification of " << d_owner[0][i] << "." << std::endl; d_incomplete = true; } } //enumerate if the sort is reasonably small, not an Array, the upper bound of 1000 is chosen arbitrarily for now - }else if( !tn.isArray() && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() && - tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=1000 ){ + }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){ + Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; d_rep_set->complete( tn ); }else{ + Trace("rsi") << " variable cannot be bounded." << std::endl; Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl; d_incomplete = true; } diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 4aab230e6..f1114edcf 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -48,7 +48,7 @@ public: /** returns index in d_type_reps for node n */ int getIndexFor( Node n ) const; /** complete all values */ - void complete( TypeNode t ); + bool complete( TypeNode t ); /** debug print */ void toStream(std::ostream& out); };/* class RepSet */ diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 4e5c84f42..be202fb69 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -77,12 +77,6 @@ public: * If it cannot find such a node, it returns null. */ Node getNewDomainValue( TypeNode tn ); - /** complete all values for type - * Calling this function ensures that all terms of type tn exist in d_rep_set.d_type_reps[tn] - */ - void completeDomainValues( TypeNode tn ){ - d_rep_set.complete( tn ); - } public: /** Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, bool invalidateCache = true); -- 2.30.2