(Refactor) Document and clean single invocation partition. (#1364)

* Documenting single invocation partiion.

* More

* More encapsulation.

* More, documentation complete.

* Split to own file.

* Format

* Fully encapsulate.

* Format

* Improvements to doc.

* Format

* Address

* Format

* Missed comment

* Newline

* Address

* Format

1 files changed, 27 insertions, 11 deletions

diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index 681c168f2..1303b7627 100644
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -116,9 +116,15 @@ void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e)
         }
         if( success ){
           //sort the argument variables
-          d_ask_types[q].insert( d_ask_types[q].end(), d_quant_sip[q].d_arg_types.begin(), d_quant_sip[q].d_arg_types.end() );
+          std::vector<Node> sivars;
+          d_quant_sip[q].getSingleInvocationVariables(sivars);
+          for (const Node& v : sivars)
+          {
+            d_ask_types[q].push_back(v.getType());
+          }
           std::map< TypeNode, std::vector< unsigned > > indices;
-          for( unsigned j=0; j<d_ask_types[q].size(); j++ ){
+          for (unsigned j = 0, size = d_ask_types[q].size(); j < size; j++)
+          {
             indices[d_ask_types[q][j]].push_back( j );
           }
           sortTypeOrder sto;
@@ -165,8 +171,10 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool
       for( unsigned i=0; i<quants.size(); i++ ){
         Node q = quants[i];
         std::vector< int > eqcs;
-        for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){
-          Node f = it->first;
+        std::vector<Node> funcs;
+        d_quant_sip[q].getFunctions(funcs);
+        for (const Node& f : funcs)
+        {
           std::map< Node, int >::iterator itf = func_to_eqc.find( f );
           if( itf == func_to_eqc.end() ){
             if( eqcs.empty() ){
@@ -222,7 +230,8 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool
     std::vector< Node > outer_vars;
     std::vector< Node > inner_vars;
     Node q = quants[0];
-    for( unsigned i=0; i<d_ask_types[q].size(); i++ ){
+    for (unsigned i = 0, size = d_ask_types[q].size(); i < size; i++)
+    {
       Node v = NodeManager::currentNM()->mkBoundVar( d_ask_types[q][i] );
       Trace("anti-sk-debug") << "Outer var " << i << " : " << v << std::endl;
       outer_vars.push_back( v );
@@ -237,15 +246,22 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool
       std::vector< Node > subs_rhs;
       //get outer variable substitution
       Assert( d_ask_types_index[q].size()==d_ask_types[q].size() );
-      for( unsigned j=0; j<d_ask_types_index[q].size(); j++ ){
-        Trace("anti-sk-debug") << " o_subs : " << d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] << " -> " << outer_vars[j] << std::endl;
-        subs_lhs.push_back( d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] );
+      std::vector<Node> sivars;
+      d_quant_sip[q].getSingleInvocationVariables(sivars);
+      for (unsigned j = 0, size = d_ask_types_index[q].size(); j < size; j++)
+      {
+        Trace("anti-sk-debug")
+            << " o_subs : " << sivars[d_ask_types_index[q][j]] << " -> "
+            << outer_vars[j] << std::endl;
+        subs_lhs.push_back(sivars[d_ask_types_index[q][j]]);
         subs_rhs.push_back( outer_vars[j] );
       }
       //get function substitution
-      for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){
-        Node f = it->first;
-        Node fv = d_quant_sip[q].d_func_fo_var[it->first];
+      std::vector<Node> funcs;
+      d_quant_sip[q].getFunctions(funcs);
+      for (const Node& f : funcs)
+      {
+        Node fv = d_quant_sip[q].getFirstOrderVariableForFunction(f);
         if( func_to_var.find( f )==func_to_var.end() ){
           Node v = NodeManager::currentNM()->mkBoundVar( fv.getType() );
           Trace("anti-sk-debug") << "Inner var for " << f << " : " << v << std::endl;