From: ajreynol Date: Fri, 29 Aug 2014 13:03:00 +0000 (+0200) Subject: Do not use pure theory terms as single triggers. Minor cleanup. X-Git-Tag: cvc5-1.0.0~6640 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4397bf2a96fabe124ebd18e9ae9957689852afb3;p=cvc5.git Do not use pure theory terms as single triggers. Minor cleanup. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 220318b4c..98cc7813d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1299,6 +1299,11 @@ void SmtEngine::setDefaults() { options::intWfInduction.set( true ); } } + if( options::dtStcInduction() ){ + if( !options::dtForceAssignment.wasSetByUser() ){ + options::dtForceAssignment.set( true ); + } + } if( options::intWfInduction() ){ if( !options::purifyTriggers.wasSetByUser() ){ options::purifyTriggers.set( true ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 5b0fade71..df7f06aff 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -206,7 +206,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor std::map< Node, std::vector< Node > > varContains; d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains ); for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){ - if( it->second.size()==f[0].getNumChildren() ){ + if( it->second.size()==f[0].getNumChildren() && !Trigger::isPureTheoryTrigger( it->first ) ){ d_patTerms[0][f].push_back( it->first ); d_is_single_trigger[ it->first ] = true; }else{ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 856ac782c..4a99852d1 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -188,19 +188,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } //check for duplicate? - if( trOption==TR_MAKE_NEW ){ - //static int trNew = 0; - //static int trOld = 0; - //Trigger* t = qe->getTermDatabase()->getTrigger( trNodes ); - //if( t ){ - // trOld++; - //}else{ - // trNew++; - //} - //if( (trNew+trOld)%100==0 ){ - // Notice() << "Trigger new old = " << trNew << " " << trOld << std::endl; - //} - }else{ + if( trOption!=TR_MAKE_NEW ){ Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes ); if( t ){ if( trOption==TR_GET_OLD ){ @@ -215,6 +203,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& qe->getTriggerDatabase()->addTrigger( trNodes, t ); return t; } + Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){ std::vector< Node > nodes; nodes.push_back( n ); @@ -243,11 +232,9 @@ bool Trigger::isUsable( Node n, Node f ){ return true; }else{ std::map< Node, Node > coeffs; - if( isArithmeticTrigger( f, n, coeffs ) ){ - return true; - }else if( isBooleanTermTrigger( n ) ){ + if( isBooleanTermTrigger( n ) ){ return true; - } + } } return false; }else{ @@ -401,6 +388,35 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< } } +bool Trigger::isBooleanTermTrigger( Node n ) { + if( n.getKind()==ITE ){ + //check for boolean term converted to ITE + if( n[0].getKind()==INST_CONSTANT && + n[1].getKind()==CONST_BITVECTOR && + n[2].getKind()==CONST_BITVECTOR ){ + if( ((BitVectorType)n[1].getType().toType()).getSize()==1 && + n[1].getConst().toInteger()==1 && + n[2].getConst().toInteger()==0 ){ + return true; + } + } + } + return false; +} + +bool Trigger::isPureTheoryTrigger( Node n ) { + if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermDb::hasInstConstAttr( n ) ){ + return false; + }else{ + for( unsigned i=0; i& patTerms, int tstrt, bool filterInst ){ std::map< Node, bool > patMap; if( filterInst ){ @@ -442,67 +458,6 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } -bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs ){ - if( n.getKind()==PLUS ){ - Assert( coeffs.empty() ); - NodeBuilder<> t(kind::PLUS); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){ - if( n[i].getKind()==INST_CONSTANT ){ - if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){ - coeffs[ n[i] ] = Node::null(); - }else{ - coeffs.clear(); - return false; - } - }else if( !isArithmeticTrigger( f, n[i], coeffs ) ){ - coeffs.clear(); - return false; - } - }else{ - t << n[i]; - } - } - if( t.getNumChildren()==0 ){ - coeffs[ Node::null() ] = NodeManager::currentNM()->mkConst( Rational(0) ); - }else if( t.getNumChildren()==1 ){ - coeffs[ Node::null() ] = t.getChild( 0 ); - }else{ - coeffs[ Node::null() ] = t; - } - return true; - }else if( n.getKind()==MULT ){ - if( n[0].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[0])==f ){ - if( !quantifiers::TermDb::hasInstConstAttr(n[1]) ){ - coeffs[ n[0] ] = n[1]; - return true; - } - }else if( n[1].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[1])==f ){ - if( !quantifiers::TermDb::hasInstConstAttr(n[0]) ){ - coeffs[ n[1] ] = n[0]; - return true; - } - } - } - return false; -} - -bool Trigger::isBooleanTermTrigger( Node n ) { - if( n.getKind()==ITE ){ - //check for boolean term converted to ITE - if( n[0].getKind()==INST_CONSTANT && - n[1].getKind()==CONST_BITVECTOR && - n[2].getKind()==CONST_BITVECTOR ){ - if( ((BitVectorType)n[1].getType().toType()).getSize()==1 && - n[1].getConst().toInteger()==1 && - n[2].getConst().toInteger()==0 ){ - return true; - } - } - } - return false; -} - Node Trigger::getInversionVariable( Node n ) { if( n.getKind()==INST_CONSTANT ){ return n; diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 42b7598ea..1a3ae3fcd 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -110,9 +110,8 @@ public: static bool isAtomicTrigger( Node n ); static bool isAtomicTriggerKind( Kind k ); static bool isSimpleTrigger( Node n ); - /** get pattern arithmetic */ - static bool isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs ); static bool isBooleanTermTrigger( Node n ); + static bool isPureTheoryTrigger( Node n ); /** return data structure for producing matches for this trigger. */ static InstMatchGenerator* getInstMatchGenerator( Node n ); static Node getInversionVariable( Node n );