Minor optimizations related to cbqi.

diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017
index 1a9f2400ff4a7fbd4294fd5df6b8f038ddcf8447..6a0ef54b2a30a2c7889d8f1100e5ba4a2b491caa 100644 (file)
--- a/contrib/run-script-smtcomp2017
+++ b/contrib/run-script-smtcomp2017
@@ -81,23 +81,27 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA)
   # finish 9min
   finishwith --full-saturate-quant
   ;;
-BV|UFBV)
+UFBV)
   # many problems in UFBV are essentially BV
   trywith 300 --full-saturate-quant
-  trywith 300 --finite-model-find
+  trywith 300 --full-saturate-quant --cbqi --decision=internal
+  finishwith --finite-model-find
+  ;;
+BV)
+  trywith 300 --full-saturate-quant
   finishwith --full-saturate-quant --cbqi --decision=internal
   ;;
 LIA|LRA)
   trywith 30 --full-saturate-quant
   trywith 300 --full-saturate-quant --cbqi-midpoint
   trywith 300 --full-saturate-quant --cbqi-nested-qe
-  finishwith  --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal
+  finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal
   ;;
 NIA|NRA)
   trywith 30 --full-saturate-quant
   trywith 300 --full-saturate-quant --nl-ext
   trywith 300 --full-saturate-quant --cbqi-nested-qe
-  finishwith  --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal
+  finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
   trywith 600

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 1f18377406ca4cf80ed89b54b4d103556404f133..88f8e24848eabb06099a682831743783c5559cd7 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -120,6 +120,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) {
           if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){
             d_parent_quant[q].push_back( qi );
             d_children_quant[qi].push_back( q );
+            Assert( hasAddedCbqiLemma( qi ) );
             Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi );
             dep.push_back( qi );
             dep.push_back( qicel );
@@ -594,8 +595,10 @@ Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool
 
 Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){
   std::map< Node, bool > proc;
-  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+  //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+  //  Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+  for( NodeSet::const_iterator it = d_added_cbqi_lemma.begin(); it != d_added_cbqi_lemma.end(); ++it ){
+    Node q = *it;
     Node d = getNextDecisionRequestProc( q, proc );
     if( !d.isNull() ){
       priority = 0;

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 01352217e2cec69760dc565faf2f111f6a4f700e..4c395f59d77f5b6b30b7b014ecd593b856a0dc1c 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1134,21 +1134,27 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s
   return body;
 }
 
-Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){
+Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited ){
+  unsigned tindex = topLevel ? 0 : 1;
+  std::map< Node, Node >::iterator itv = visited[tindex].find( n );
+  if( itv!=visited[tindex].end() ){
+    return itv->second;
+  }
   if( containsQuantifiers( n ) ){
+    Node ret = n;
     if( topLevel && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){
       std::vector< Node > children;
       Node nc = n.getKind()==NOT ? n[0] : n;
       for( unsigned i=0; i<nc.getNumChildren(); i++ ){
-        Node ncc = computePrenexAgg( nc[i], true );
+        Node ncc = computePrenexAgg( nc[i], true, visited );
         if( n.getKind()==NOT ){
           ncc = ncc.negate();        
         }
         children.push_back( ncc );
       }
-      return NodeManager::currentNM()->mkNode( AND, children );
+      ret = NodeManager::currentNM()->mkNode( AND, children );
     }else if( n.getKind()==NOT ){
-      return computePrenexAgg( n[0], false ).negate();
+      ret = computePrenexAgg( n[0], false, visited ).negate();
     }else if( n.getKind()==FORALL ){
     /*
       Node nn = computePrenexAgg( n[1], false );
@@ -1163,10 +1169,10 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){
       std::vector< Node > children;
       if( n[1].getKind()==OR && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL ){
         for( unsigned i=0; i<n[1].getNumChildren(); i++ ){
-          children.push_back( computePrenexAgg( n[1][i], false ) );
+          children.push_back( computePrenexAgg( n[1][i], false, visited ) );
         }
       }else{
-        children.push_back( computePrenexAgg( n[1], false ) );
+        children.push_back( computePrenexAgg( n[1], false, visited ) );
       }
       std::vector< Node > args;
       for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
@@ -1182,14 +1188,15 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){
           children[i] = children[i][1];
         }
       }
+      // TODO : keep the pattern
       Node nb = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
-      return mkForall( args, nb, true );
+      ret = mkForall( args, nb, true );
     }else{
       std::vector< Node > args;
       std::vector< Node > nargs;
       Node nn = computePrenex( n, args, nargs, true, true );
       if( n!=nn ){
-        Node nnn = computePrenexAgg( nn, false );
+        Node nnn = computePrenexAgg( nn, false, visited );
         //merge prenex
         if( nnn.getKind()==FORALL ){
           for( unsigned i=0; i<nnn[0].getNumChildren(); i++ ){
@@ -1213,12 +1220,14 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){
         if( !args.empty() ){
           nnn = mkForall( args, nnn, true );
         }
-        return nnn;
+        ret = nnn;
       }else{
         Assert( args.empty() );
         Assert( nargs.empty() );
       }
     }
+    visited[tindex][n] = ret;
+    return ret;
   }
   return n;
 }
@@ -1822,7 +1831,8 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
   //pull all quantifiers globally
   if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){
     Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl;
-    n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true );
+    std::map< unsigned, std::map< Node, Node > > visited;
+    n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true, visited );
     n = Rewriter::rewrite( n );
     Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl;
     //Assert( isPrenexNormalForm( n ) );

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index c61ca1fb0a7c3bae63ac3554328a1b0758c11b19..bb1d77dfe24e7eb53cd15c8069903ecc087267d0 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -60,7 +60,7 @@ public:
   static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa );
   static Node computeCondSplit( Node body, QAttributes& qa );
   static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg );
-  static Node computePrenexAgg( Node n, bool topLevel );
+  static Node computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited );
   static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa );
 private:

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 55b1af83c7a4407d168dbc6dbe50973cdcc880c5..501d77ecfd9dd8df0a4016eb00ec12c79f8f5e35 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -933,32 +933,37 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
   }
 }
 
-Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){
-  if( n.getKind()==INST_CONSTANT ){
-    Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
-    return terms[n.getAttribute(InstVarNumAttribute())];
-  }else{
-    //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
-      //Debug("check-inst") << "No inst const attr : " << n << std::endl;
-      //return n;
-    //}else{
-      //Debug("check-inst") << "Recurse on : " << n << std::endl;
-    std::vector< Node > cc;
-    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-      cc.push_back( n.getOperator() );
-    }
-    bool changed = false;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      Node c = getSubstitute( n[i], terms );
-      cc.push_back( c );
-      changed = changed || c!=n[i];
-    }
-    if( changed ){
-      Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cc );
-      return ret;
+Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited ){
+  std::map< Node, Node >::iterator itv = visited.find( n );
+  if( itv==visited.end() ){
+    Node ret = n;
+    if( n.getKind()==INST_CONSTANT ){
+      Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
+      ret = terms[n.getAttribute(InstVarNumAttribute())];
     }else{
-      return n;
+      //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
+        //Debug("check-inst") << "No inst const attr : " << n << std::endl;
+        //return n;
+      //}else{
+        //Debug("check-inst") << "Recurse on : " << n << std::endl;
+      std::vector< Node > cc;
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        cc.push_back( n.getOperator() );
+      }
+      bool changed = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node c = getSubstitute( n[i], terms, visited );
+        cc.push_back( c );
+        changed = changed || c!=n[i];
+      }
+      if( changed ){
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), cc );
+      }
     }
+    visited[n] = ret;
+    return ret;
+  }else{
+    return itv->second;
   }
 }
 
@@ -988,7 +993,8 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std
     }else{
       //do optimized version
       Node icb = d_term_db->getInstConstantBody( q );
-      body = getSubstitute( icb, terms );
+      std::map< Node, Node > visited;
+      body = getSubstitute( icb, terms, visited );
       if( Debug.isOn("check-inst") ){
         Node body2 = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
         if( body!=body2 ){

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 7405241b7cc278950c962694b77261403aee774e..fff446eda570acfbe2084a962e39e4b5049e701a 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -315,7 +315,7 @@ public:
   /** get instantiation */
   Node getInstantiation( Node q, std::vector< Node >& terms, bool doVts = false );
   /** do substitution */
-  Node getSubstitute( Node n, std::vector< Node >& terms );
+  Node getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited );
   /** add lemma lem */
   bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
   /** remove pending lemma */