(Refactor) Split term util (#1303)

* Fix some documentation.

* Move model basis out of term db.

* Moving

* Finished moving.

* Document Skolemize and term enumeration.

* Minor

* Model basis to first order model.

* Change function name.

* Minor

* Clang format.

* Minor

* Format

* Minor

* Format

* Address review.

1 files changed, 385 insertions, 0 deletions

diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
new file mode 100644
index 000000000..2f210cc20
--- /dev/null
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -0,0 +1,385 @@
+/*********************                                                        */
+/*! \file skolemize.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of skolemization utility
+ **/
+
+#include "theory/quantifiers/skolemize.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/sort_inference.h"
+#include "theory/theory_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Skolemize::Skolemize(QuantifiersEngine* qe, context::UserContext* u)
+    : d_quantEngine(qe), d_skolemized(u)
+{
+}
+
+Node Skolemize::process(Node q)
+{
+  // do skolemization
+  if (d_skolemized.find(q) == d_skolemized.end())
+  {
+    Node body = getSkolemizedBody(q);
+    NodeBuilder<> nb(kind::OR);
+    nb << q << body.notNode();
+    Node lem = nb;
+    d_skolemized[q] = lem;
+    return lem;
+  }
+  return Node::null();
+}
+
+bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems)
+{
+  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
+      d_skolem_constants.find(q);
+  if (it != d_skolem_constants.end())
+  {
+    skolems.insert(skolems.end(), it->second.begin(), it->second.end());
+    return true;
+  }
+  return false;
+}
+
+Node Skolemize::getSkolemConstant(Node q, unsigned i)
+{
+  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
+      d_skolem_constants.find(q);
+  if (it != d_skolem_constants.end())
+  {
+    if (i < it->second.size())
+    {
+      return it->second[i];
+    }
+  }
+  return Node::null();
+}
+
+void Skolemize::getSelfSel(const Datatype& dt,
+                           const DatatypeConstructor& dc,
+                           Node n,
+                           TypeNode ntn,
+                           std::vector<Node>& selfSel)
+{
+  TypeNode tspec;
+  if (dt.isParametric())
+  {
+    tspec = TypeNode::fromType(
+        dc.getSpecializedConstructorType(n.getType().toType()));
+    Trace("sk-ind-debug") << "Specialized constructor type : " << tspec
+                          << std::endl;
+    Assert(tspec.getNumChildren() == dc.getNumArgs());
+  }
+  Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " "
+                        << dt.getName() << std::endl;
+  for (unsigned j = 0; j < dc.getNumArgs(); j++)
+  {
+    std::vector<Node> ssc;
+    if (dt.isParametric())
+    {
+      Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn
+                            << std::endl;
+      if (tspec[j] == ntn)
+      {
+        ssc.push_back(n);
+      }
+    }
+    else
+    {
+      TypeNode tn = TypeNode::fromType(dc[j].getRangeType());
+      Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
+      if (tn == ntn)
+      {
+        ssc.push_back(n);
+      }
+    }
+    /* TODO: more than weak structural induction
+    else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn
+    )==visited.end() ){
+      visited.push_back( tn );
+      const Datatype& dt =
+    ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
+      std::vector< Node > disj;
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        getSelfSel( dt[i], n, ntn, ssc );
+      }
+      visited.pop_back();
+    }
+    */
+    for (unsigned k = 0; k < ssc.size(); k++)
+    {
+      Node ss = NodeManager::currentNM()->mkNode(
+          APPLY_SELECTOR_TOTAL,
+          dc.getSelectorInternal(n.getType().toType(), j),
+          n);
+      if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
+      {
+        selfSel.push_back(ss);
+      }
+    }
+  }
+}
+
+Node Skolemize::mkSkolemizedBody(Node f,
+                                 Node n,
+                                 std::vector<TypeNode>& argTypes,
+                                 std::vector<TNode>& fvs,
+                                 std::vector<Node>& sk,
+                                 Node& sub,
+                                 std::vector<unsigned>& sub_vars)
+{
+  Assert(sk.empty() || sk.size() == f[0].getNumChildren());
+  // calculate the variables and substitution
+  std::vector<TNode> ind_vars;
+  std::vector<unsigned> ind_var_indicies;
+  std::vector<TNode> vars;
+  std::vector<unsigned> var_indicies;
+  for (unsigned i = 0; i < f[0].getNumChildren(); i++)
+  {
+    if (isInductionTerm(f[0][i]))
+    {
+      ind_vars.push_back(f[0][i]);
+      ind_var_indicies.push_back(i);
+    }
+    else
+    {
+      vars.push_back(f[0][i]);
+      var_indicies.push_back(i);
+    }
+    Node s;
+    // make the new function symbol or use existing
+    if (i >= sk.size())
+    {
+      if (argTypes.empty())
+      {
+        s = NodeManager::currentNM()->mkSkolem(
+            "skv", f[0][i].getType(), "created during skolemization");
+      }
+      else
+      {
+        TypeNode typ = NodeManager::currentNM()->mkFunctionType(
+            argTypes, f[0][i].getType());
+        Node op = NodeManager::currentNM()->mkSkolem(
+            "skop", typ, "op created during pre-skolemization");
+        // DOTHIS: set attribute on op, marking that it should not be selected
+        // as trigger
+        std::vector<Node> funcArgs;
+        funcArgs.push_back(op);
+        funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end());
+        s = NodeManager::currentNM()->mkNode(kind::APPLY_UF, funcArgs);
+      }
+      sk.push_back(s);
+    }
+    else
+    {
+      Assert(sk[i].getType() == f[0][i].getType());
+    }
+  }
+  Node ret;
+  if (vars.empty())
+  {
+    ret = n;
+  }
+  else
+  {
+    std::vector<Node> var_sk;
+    for (unsigned i = 0; i < var_indicies.size(); i++)
+    {
+      var_sk.push_back(sk[var_indicies[i]]);
+    }
+    Assert(vars.size() == var_sk.size());
+    ret = n.substitute(vars.begin(), vars.end(), var_sk.begin(), var_sk.end());
+  }
+  if (!ind_vars.empty())
+  {
+    Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
+    Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
+    Node n_str_ind;
+    TypeNode tn = ind_vars[0].getType();
+    Node k = sk[ind_var_indicies[0]];
+    Node nret = ret.substitute(ind_vars[0], k);
+    // note : everything is under a negation
+    // the following constructs ~( R( x, k ) => ~P( x ) )
+    if (options::dtStcInduction() && tn.isDatatype())
+    {
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      std::vector<Node> disj;
+      for (unsigned i = 0; i < dt.getNumConstructors(); i++)
+      {
+        std::vector<Node> selfSel;
+        getSelfSel(dt, dt[i], k, tn, selfSel);
+        std::vector<Node> conj;
+        conj.push_back(
+            NodeManager::currentNM()
+                ->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), k)
+                .negate());
+        for (unsigned j = 0; j < selfSel.size(); j++)
+        {
+          conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
+        }
+        disj.push_back(conj.size() == 1
+                           ? conj[0]
+                           : NodeManager::currentNM()->mkNode(OR, conj));
+      }
+      Assert(!disj.empty());
+      n_str_ind = disj.size() == 1
+                      ? disj[0]
+                      : NodeManager::currentNM()->mkNode(AND, disj);
+    }
+    else if (options::intWfInduction() && tn.isInteger())
+    {
+      Node icond = NodeManager::currentNM()->mkNode(
+          GEQ, k, NodeManager::currentNM()->mkConst(Rational(0)));
+      Node iret =
+          ret.substitute(
+                 ind_vars[0],
+                 NodeManager::currentNM()->mkNode(
+                     MINUS, k, NodeManager::currentNM()->mkConst(Rational(1))))
+              .negate();
+      n_str_ind = NodeManager::currentNM()->mkNode(OR, icond.negate(), iret);
+      n_str_ind = NodeManager::currentNM()->mkNode(AND, icond, n_str_ind);
+    }
+    else
+    {
+      Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0]
+                      << ", type = " << tn << std::endl;
+      Assert(false);
+    }
+    Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;
+
+    std::vector<Node> rem_ind_vars;
+    rem_ind_vars.insert(
+        rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end());
+    if (!rem_ind_vars.empty())
+    {
+      Node bvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, rem_ind_vars);
+      nret = NodeManager::currentNM()->mkNode(FORALL, bvl, nret);
+      nret = Rewriter::rewrite(nret);
+      sub = nret;
+      sub_vars.insert(
+          sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end());
+      n_str_ind = NodeManager::currentNM()
+                      ->mkNode(FORALL, bvl, n_str_ind.negate())
+                      .negate();
+    }
+    ret = NodeManager::currentNM()->mkNode(OR, nret, n_str_ind);
+  }
+  Trace("quantifiers-sk-debug") << "mkSkolem body for " << f
+                                << " returns : " << ret << std::endl;
+  // if it has an instantiation level, set the skolemized body to that level
+  if (f.hasAttribute(InstLevelAttribute()))
+  {
+    theory::QuantifiersEngine::setInstantiationLevelAttr(
+        ret, f.getAttribute(InstLevelAttribute()));
+  }
+
+  if (Trace.isOn("quantifiers-sk"))
+  {
+    Trace("quantifiers-sk") << "Skolemize : ";
+    for (unsigned i = 0; i < sk.size(); i++)
+    {
+      Trace("quantifiers-sk") << sk[i] << " ";
+    }
+    Trace("quantifiers-sk") << "for " << std::endl;
+    Trace("quantifiers-sk") << "   " << f << std::endl;
+  }
+
+  return ret;
+}
+
+Node Skolemize::getSkolemizedBody(Node f)
+{
+  Assert(f.getKind() == FORALL);
+  if (d_skolem_body.find(f) == d_skolem_body.end())
+  {
+    std::vector<TypeNode> fvTypes;
+    std::vector<TNode> fvs;
+    Node sub;
+    std::vector<unsigned> sub_vars;
+    d_skolem_body[f] = mkSkolemizedBody(
+        f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars);
+    // store sub quantifier information
+    if (!sub.isNull())
+    {
+      // if we are skolemizing one at a time, we already know the skolem
+      // constants of the sub-quantified formula, store them
+      Assert(d_skolem_constants[sub].empty());
+      for (unsigned i = 0; i < sub_vars.size(); i++)
+      {
+        d_skolem_constants[sub].push_back(d_skolem_constants[f][sub_vars[i]]);
+      }
+    }
+    Assert(d_skolem_constants[f].size() == f[0].getNumChildren());
+    if (options::sortInference())
+    {
+      for (unsigned i = 0; i < d_skolem_constants[f].size(); i++)
+      {
+        // carry information for sort inference
+        d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar(
+            f, f[0][i], d_skolem_constants[f][i]);
+      }
+    }
+  }
+  return d_skolem_body[f];
+}
+
+bool Skolemize::isInductionTerm(Node n)
+{
+  TypeNode tn = n.getType();
+  if (options::dtStcInduction() && tn.isDatatype())
+  {
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    return !dt.isCodatatype();
+  }
+  if (options::intWfInduction() && n.getType().isInteger())
+  {
+    return true;
+  }
+  return false;
+}
+
+bool Skolemize::printSkolemization(std::ostream& out)
+{
+  bool printed = false;
+  for (NodeNodeMap::iterator it = d_skolemized.begin();
+       it != d_skolemized.end();
+       ++it)
+  {
+    Node q = (*it).first;
+    printed = true;
+    out << "(skolem " << q << std::endl;
+    out << "  ( ";
+    for (unsigned i = 0; i < d_skolem_constants[q].size(); i++)
+    {
+      if (i > 0)
+      {
+        out << " ";
+      }
+      out << d_skolem_constants[q][i];
+    }
+    out << " )" << std::endl;
+    out << ")" << std::endl;
+  }
+  return printed;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */