diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-16 18:06:27 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-16 18:06:27 +0200 |
commit | 7a36dd1e29c6d0160f949d5f805044768fb549d1 (patch) | |
tree | bb2fea5fac3879868895c2c1dfaf0f969d94dd1d /src/theory/quantifiers/term_database.cpp | |
parent | 9b32405be875e7d20289d8eabbe85d036a31f301 (diff) |
Avoid completion for large finite types. Fix bug for --fmf-fun.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 19 |
1 files changed, 19 insertions, 0 deletions
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 ) ){ |