Add misc trigger options.

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index cd24f9ac2c93cb454abc907697312981fb80e059..de8e45a84efa3b60f14aa9bf162f0c8a3b9a9f0f 100644 (file)
--- 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 b9e8aef09c26270dab305019cde54db6a7e577ea..fd5a3609fb4444b26a096bc4f55406352f1f6720 100644 (file)
--- 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 cac78af46036a5966529634a9539a3188a6ab4d5..a48b009c27b60a1d4e57c4cddf1cc4de62963668 100644 (file)
--- 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 65b976b4a477a500623d9779db001ec3fed51ef3..e953e90b202948cc0823a442b26c1c3e02b2512b 100644 (file)
--- 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<n.getNumChildren(); i++ ){
       if( !isLocalTheoryExt( n[i], vars, patTerms ) ){
         return false;
-      } 
+      }
     }
   }
   return true;