(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, 33 insertions, 28 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d703e8e83..1a35c9901 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -93,6 +93,7 @@
 #include "theory/quantifiers/fun_def_process.h"
 #include "theory/quantifiers/macros.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/single_inv_partition.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/sort_inference.h"
 #include "theory/strings/theory_strings.h"
@@ -4631,14 +4632,18 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) {
         Trace("smt-synth") << "Property is non-ground single invocation, run "
                               "QE to obtain single invocation."
                            << std::endl;
+        NodeManager* nm = NodeManager::currentNM();
         // partition variables
+        std::vector<Node> all_vars;
+        sip.getAllVariables(all_vars);
+        std::vector<Node> si_vars;
+        sip.getSingleInvocationVariables(si_vars);
         std::vector<Node> qe_vars;
         std::vector<Node> nqe_vars;
-        for (unsigned i = 0; i < sip.d_all_vars.size(); i++)
+        for (unsigned i = 0, size = all_vars.size(); i < size; i++)
         {
-          Node v = sip.d_all_vars[i];
-          if (std::find(sip.d_si_vars.begin(), sip.d_si_vars.end(), v)
-              == sip.d_si_vars.end())
+          Node v = all_vars[i];
+          if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end())
           {
             qe_vars.push_back(v);
           }
@@ -4652,27 +4657,29 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) {
         // skolemize non-qe variables
         for (unsigned i = 0; i < nqe_vars.size(); i++)
         {
-          Node k = NodeManager::currentNM()->mkSkolem(
-              "k",
-              nqe_vars[i].getType(),
-              "qe for non-ground single invocation");
+          Node k = nm->mkSkolem("k",
+                                nqe_vars[i].getType(),
+                                "qe for non-ground single invocation");
           orig.push_back(nqe_vars[i]);
           subs.push_back(k);
           Trace("smt-synth") << "  subs : " << nqe_vars[i] << " -> " << k
                              << std::endl;
         }
-        for (std::map<Node, bool>::iterator it = sip.d_funcs.begin();
-             it != sip.d_funcs.end();
-             ++it)
+        std::vector<Node> funcs;
+        sip.getFunctions(funcs);
+        for (unsigned i = 0, size = funcs.size(); i < size; i++)
         {
-          orig.push_back(sip.d_func_inv[it->first]);
-          Node k = NodeManager::currentNM()->mkSkolem(
-              "k",
-              sip.d_func_fo_var[it->first].getType(),
-              "qe for function in non-ground single invocation");
+          Node f = funcs[i];
+          Node fi = sip.getFunctionInvocationFor(f);
+          Node fv = sip.getFirstOrderVariableForFunction(f);
+          Assert(!fi.isNull());
+          orig.push_back(fi);
+          Node k =
+              nm->mkSkolem("k",
+                           fv.getType(),
+                           "qe for function in non-ground single invocation");
           subs.push_back(k);
-          Trace("smt-synth") << "  subs : " << sip.d_func_inv[it->first]
-                             << " -> " << k << std::endl;
+          Trace("smt-synth") << "  subs : " << fi << " -> " << k << std::endl;
         }
         Node conj_se_ngsi = sip.getFullSpecification();
         Trace("smt-synth") << "Full specification is " << conj_se_ngsi
@@ -4680,10 +4687,10 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) {
         Node conj_se_ngsi_subs = conj_se_ngsi.substitute(
             orig.begin(), orig.end(), subs.begin(), subs.end());
         Assert(!qe_vars.empty());
-        conj_se_ngsi_subs = NodeManager::currentNM()->mkNode(
-            kind::EXISTS,
-            NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qe_vars),
-            conj_se_ngsi_subs.negate());
+        conj_se_ngsi_subs =
+            nm->mkNode(kind::EXISTS,
+                       nm->mkNode(kind::BOUND_VAR_LIST, qe_vars),
+                       conj_se_ngsi_subs.negate());
 
         Trace("smt-synth") << "Run quantifier elimination on "
                            << conj_se_ngsi_subs << std::endl;
@@ -4697,14 +4704,12 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) {
             subs.begin(), subs.end(), orig.begin(), orig.end());
         if (!nqe_vars.empty())
         {
-          qe_res_n = NodeManager::currentNM()->mkNode(
-              kind::EXISTS,
-              NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, nqe_vars),
-              qe_res_n);
+          qe_res_n = nm->mkNode(kind::EXISTS,
+                                nm->mkNode(kind::BOUND_VAR_LIST, nqe_vars),
+                                qe_res_n);
         }
         Assert(conj.getNumChildren() == 3);
-        qe_res_n = NodeManager::currentNM()->mkNode(
-            kind::FORALL, conj[0], qe_res_n, conj[2]);
+        qe_res_n = nm->mkNode(kind::FORALL, conj[0], qe_res_n, conj[2]);
         Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n
                            << std::endl;
         e_check = qe_res_n.toExpr();