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 220318b4c7a23684c3495e025bacb589705a9eed..98cc7813dd18745fb8ffc3ca529fe4af33107105 100644 (file)
--- 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 5b0fade71638623c8d87eceff4d985dfbe32fe5a..df7f06aff4387c25f49dd0c224cd238ff1288ea2 100644 (file)
--- 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 856ac782c2227d055b8de0b1e068892f9c6f7195..4a99852d102bc9428ce4ef5033057df8d6dc652e 100644 (file)
--- 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<BitVector>().toInteger()==1 &&
+          n[2].getConst<BitVector>().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<n.getNumChildren(); i++ ){
+      if( !isPureTheoryTrigger( n[i] ) ){
+        return false;
+      }
+    }
+    return true;
+  }
+}
+
 void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& 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<BitVector>().toInteger()==1 &&
-          n[2].getConst<BitVector>().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 42b7598eaee48270a753a0537873a59564a0f169..1a3ae3fcd8d0c0268a81c545fe5e367d062ae0b8 100644 (file)
--- 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 );