From 1eef0f8d079e40cf9eac76e70399908d75dc11bc Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 22 Dec 2014 00:49:27 +0100 Subject: [PATCH] Add misc trigger options. --- src/theory/quantifiers/inst_match_generator.cpp | 15 ++++++++++++++- .../quantifiers/inst_strategy_e_matching.cpp | 4 ++-- src/theory/quantifiers/options | 4 ++++ src/theory/quantifiers/trigger.cpp | 5 ++++- 4 files changed, 24 insertions(+), 4 deletions(-) diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index cd24f9ac2..de8e45a84 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/candidate_generator.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/options.h" +#include "util/datatype.h" using namespace std; using namespace CVC4; @@ -92,6 +93,8 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat } } } + }else if( d_match_pattern.getKind()==APPLY_SELECTOR_TOTAL && d_match_pattern[0].getKind()==INST_CONSTANT && options::purifyDtTriggers() ){ + d_match_pattern = d_match_pattern[0]; } d_match_pattern_type = d_match_pattern.getType(); Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; @@ -121,7 +124,17 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat //create candidate generator if( d_match_pattern.getKind()==INST_CONSTANT ){ - d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); + if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){ + Expr selectorExpr = qe->getTermDatabase()->getOperator( d_pattern ).toExpr(); + size_t selectorIndex = Datatype::cindexOf(selectorExpr); + const Datatype& dt = Datatype::datatypeOf(selectorExpr); + const DatatypeConstructor& c = dt[selectorIndex]; + Node cOp = Node::fromExpr(c.getConstructor()); + Trace("inst-match-gen") << "Purify dt trigger " << d_pattern << ", will match terms of op " << cOp << std::endl; + d_cg = new inst::CandidateGeneratorQE( qe, cOp ); + }else{ + d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); + } }else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index b9e8aef09..fd5a3609f 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -249,7 +249,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() && !Trigger::isPureTheoryTrigger( it->first ) ){ + if( it->second.size()==f[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( it->first ) ) ){ d_patTerms[0][f].push_back( it->first ); d_is_single_trigger[ it->first ] = true; }else{ @@ -479,7 +479,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { } void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){ - + } int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index cac78af46..a48b009c2 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -74,6 +74,10 @@ option relationalTriggers --relational-triggers bool :default false choose relational triggers such as x = f(y), x >= f(y) option purifyTriggers --purify-triggers bool :default false :read-write purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 +option purifyDtTriggers --purify-dt-triggers bool :default false :read-write + purify dt triggers, match all constructors of correct form instead of selectors +option pureThTriggers --pure-th-triggers bool :default false :read-write + use pure theory terms as single triggers option multiTriggerWhenSingle --multi-trigger-when-single bool :default true never select multi-triggers when single triggers exist option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h" diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 65b976b4a..e953e90b2 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -318,6 +318,9 @@ bool Trigger::isSimpleTrigger( Node n ){ return false; } } + if( options::purifyDtTriggers() && n.getKind()==APPLY_SELECTOR_TOTAL ){ + return false; + } return true; }else{ return false; @@ -442,7 +445,7 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< for( unsigned i=0; i