Move virtual term substitution utilities to own file and document (#3278)

10 files changed, 473 insertions, 257 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index db92d2b3f..20458219e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -463,6 +463,8 @@ libcvc4_add_sources(
   theory/quantifiers/cegqi/ceg_instantiator.h
   theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
   theory/quantifiers/cegqi/inst_strategy_cegqi.h
+  theory/quantifiers/cegqi/vts_term_cache.cpp
+  theory/quantifiers/cegqi/vts_term_cache.h
   theory/quantifiers/conjecture_generator.cpp
   theory/quantifiers/conjecture_generator.h
   theory/quantifiers/dynamic_rewrite.cpp
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index e71f2b157..0a3775807 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -32,7 +32,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-ArithInstantiator::ArithInstantiator(TypeNode tn) : Instantiator(tn)
+ArithInstantiator::ArithInstantiator(TypeNode tn, VtsTermCache* vtc)
+    : Instantiator(tn), d_vtc(vtc)
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
@@ -43,10 +44,8 @@ void ArithInstantiator::reset(CegInstantiator* ci,
                               Node pv,
                               CegInstEffort effort)
 {
-  d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity(
-      d_type, false, false);
-  d_vts_sym[1] =
-      ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta(false, false);
+  d_vts_sym[0] = d_vtc->getVtsInfinity(d_type, false, false);
+  d_vts_sym[1] = d_vtc->getVtsDelta(false, false);
   for (unsigned i = 0; i < 2; i++)
   {
     d_mbp_bounds[i].clear();
@@ -288,7 +287,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
       }
       else
       {
-        Node delta = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta();
+        Node delta = d_vtc->getVtsDelta();
         uval = nm->mkNode(
             uires == CEG_TT_UPPER_STRICT ? PLUS : MINUS, uval, delta);
         uval = Rewriter::rewrite(uval);
@@ -357,8 +356,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
             << "No " << (rr == 0 ? "lower" : "upper") << " bounds for " << pv
             << " (type=" << d_type << ")" << std::endl;
         // no bounds, we do +- infinity
-        Node val =
-            ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity(d_type);
+        Node val = d_vtc->getVtsInfinity(d_type);
         // could get rho value for infinity here
         if (rr == 0)
         {
@@ -1034,11 +1032,7 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci,
   {
     // create delta here if necessary
     val = nm->mkNode(
-        PLUS,
-        val,
-        nm->mkNode(MULT,
-                   delta_coeff,
-                   ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta()));
+        PLUS, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta()));
     val = Rewriter::rewrite(val);
   }
   return val;
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
index 8ae5383a5..94e674687 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
@@ -20,6 +20,7 @@
 #include <vector>
 #include "expr/node.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/cegqi/vts_term_cache.h"
 
 namespace CVC4 {
 namespace theory {
@@ -42,7 +43,7 @@ namespace quantifiers {
 class ArithInstantiator : public Instantiator
 {
  public:
-  ArithInstantiator(TypeNode tn);
+  ArithInstantiator(TypeNode tn, VtsTermCache* vtc);
   virtual ~ArithInstantiator() {}
   /** reset */
   void reset(CegInstantiator* ci,
@@ -129,6 +130,8 @@ class ArithInstantiator : public Instantiator
   std::string identify() const override { return "Arith"; }
 
  private:
+  /** pointer to the virtual term substitution term cache class */
+  VtsTermCache* d_vtc;
   /** zero/one */
   Node d_zero;
   Node d_one;
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 1713c21e2..63736b53c 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -477,7 +477,7 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index)
     TypeNode tn = v.getType();
     Instantiator * vinst;
     if( tn.isReal() ){
-      vinst = new ArithInstantiator(tn);
+      vinst = new ArithInstantiator(tn, d_parent->getVtsTermCache());
     }else if( tn.isSort() ){
       Assert( options::quantEpr() );
       vinst = new EprInstantiator(tn);
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 7ad7e6996..7f9c21a65 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -57,6 +57,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
       d_incomplete_check(false),
       d_added_cbqi_lemma(qe->getUserContext()),
       d_elim_quants(qe->getSatContext()),
+      d_vtsCache(new VtsTermCache(qe)),
       d_bv_invert(nullptr),
       d_nested_qe_waitlist_size(qe->getUserContext()),
       d_nested_qe_waitlist_proc(qe->getUserContext())
@@ -460,7 +461,7 @@ Node InstStrategyCegqi::rewriteInstantiation(Node q,
     // do virtual term substitution
     inst = Rewriter::rewrite(inst);
     Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl;
-    inst = d_quantEngine->getTermUtil()->rewriteVtsSymbols(inst);
+    inst = d_vtsCache->rewriteVtsSymbols(inst);
     Trace("quant-vts-debug") << "...got " << inst << std::endl;
   }
   if (options::cbqiNestedQE())
@@ -499,7 +500,7 @@ Node InstStrategyCegqi::doNestedQENode(
   if( doVts ){
     //do virtual term substitution
     ret = Rewriter::rewrite( ret );
-    ret = d_quantEngine->getTermUtil()->rewriteVtsSymbols( ret );
+    ret = d_vtsCache->rewriteVtsSymbols(ret);
   }
   Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl;
   Trace("cbqi-nqe") << "  " << n << std::endl; 
@@ -631,14 +632,14 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
       d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
       d_small_const = Rewriter::rewrite( d_small_const );
       //heuristic for now, until we know how to do nested quantification
-      Node delta = d_quantEngine->getTermUtil()->getVtsDelta( true, false );
+      Node delta = d_vtsCache->getVtsDelta(true, false);
       if( !delta.isNull() ){
         Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
         Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
         d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
       }
       std::vector< Node > inf;
-      d_quantEngine->getTermUtil()->getVtsTerms( inf, true, false, false );
+      d_vtsCache->getVtsTerms(inf, true, false, false);
       for( unsigned i=0; i<inf.size(); i++ ){
         Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
         Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
@@ -674,7 +675,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
     return true;
   }else{
     //check if we need virtual term substitution (if used delta or infinity)
-    bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false );
+    bool used_vts = d_vtsCache->containsVtsTerm(subs, false);
     if (d_quantEngine->getInstantiate()->addInstantiation(
             d_curr_quant, subs, false, false, used_vts))
     {
@@ -704,6 +705,11 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   return it->second.get();
 }
 
+VtsTermCache* InstStrategyCegqi::getVtsTermCache() const
+{
+  return d_vtsCache.get();
+}
+
 BvInverter* InstStrategyCegqi::getBvInverter() const
 {
   return d_bv_invert.get();
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index f3624d834..7abdf7d6d 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -21,6 +21,7 @@
 #include "theory/decision_manager.h"
 #include "theory/quantifiers/bv_inverter.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/cegqi/vts_term_cache.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_util.h"
 #include "util/statistics_registry.h"
@@ -89,6 +90,8 @@ class InstStrategyCegqi : public QuantifiersModule
   std::string identify() const override { return std::string("Cegqi"); }
   /** get instantiator for quantifier */
   CegInstantiator* getInstantiator(Node q);
+  /** get the virtual term substitution term cache utility */
+  VtsTermCache* getVtsTermCache() const;
   /** get the BV inverter utility */
   BvInverter* getBvInverter() const;
   /** pre-register quantifier */
@@ -149,6 +152,8 @@ class InstStrategyCegqi : public QuantifiersModule
    * This object is responsible for finding instantiatons for q.
    */
   std::map<Node, std::unique_ptr<CegInstantiator>> d_cinst;
+  /** virtual term substitution term cache for arithmetic instantiation */
+  std::unique_ptr<VtsTermCache> d_vtsCache;
   /** inversion utility for BV instantiation */
   std::unique_ptr<BvInverter> d_bv_invert;
   /**
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
new file mode 100644
index 000000000..11c126eaf
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -0,0 +1,298 @@
+/*********************                                                        */
+/*! \file vts_term_cache.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 virtual term substitution term cache.
+ **/
+
+#include "theory/quantifiers/cegqi/vts_term_cache.h"
+
+#include "expr/node_algorithm.h"
+#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+VtsTermCache::VtsTermCache(QuantifiersEngine* qe) : d_qe(qe)
+{
+  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+}
+
+void VtsTermCache::getVtsTerms(std::vector<Node>& t,
+                               bool isFree,
+                               bool create,
+                               bool inc_delta)
+{
+  if (inc_delta)
+  {
+    Node delta = getVtsDelta(isFree, create);
+    if (!delta.isNull())
+    {
+      t.push_back(delta);
+    }
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  for (unsigned r = 0; r < 2; r++)
+  {
+    TypeNode tn = r == 0 ? nm->realType() : nm->integerType();
+    Node inf = getVtsInfinity(tn, isFree, create);
+    if (!inf.isNull())
+    {
+      t.push_back(inf);
+    }
+  }
+}
+
+Node VtsTermCache::getVtsDelta(bool isFree, bool create)
+{
+  if (create)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    if (d_vts_delta_free.isNull())
+    {
+      d_vts_delta_free =
+          nm->mkSkolem("delta_free",
+                       nm->realType(),
+                       "free delta for virtual term substitution");
+      Node delta_lem = nm->mkNode(GT, d_vts_delta_free, d_zero);
+      d_qe->getOutputChannel().lemma(delta_lem);
+    }
+    if (d_vts_delta.isNull())
+    {
+      d_vts_delta = nm->mkSkolem(
+          "delta", nm->realType(), "delta for virtual term substitution");
+      // mark as a virtual term
+      VirtualTermSkolemAttribute vtsa;
+      d_vts_delta.setAttribute(vtsa, true);
+    }
+  }
+  return isFree ? d_vts_delta_free : d_vts_delta;
+}
+
+Node VtsTermCache::getVtsInfinity(TypeNode tn, bool isFree, bool create)
+{
+  if (create)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    if (d_vts_inf_free[tn].isNull())
+    {
+      d_vts_inf_free[tn] = nm->mkSkolem(
+          "inf_free", tn, "free infinity for virtual term substitution");
+    }
+    if (d_vts_inf[tn].isNull())
+    {
+      d_vts_inf[tn] =
+          nm->mkSkolem("inf", tn, "infinity for virtual term substitution");
+      // mark as a virtual term
+      VirtualTermSkolemAttribute vtsa;
+      d_vts_inf[tn].setAttribute(vtsa, true);
+    }
+  }
+  return isFree ? d_vts_inf_free[tn] : d_vts_inf[tn];
+}
+
+Node VtsTermCache::substituteVtsFreeTerms(Node n)
+{
+  std::vector<Node> vars;
+  getVtsTerms(vars, false, false);
+  std::vector<Node> vars_free;
+  getVtsTerms(vars_free, true, false);
+  Assert(vars.size() == vars_free.size());
+  if (vars.empty())
+  {
+    return n;
+  }
+  return n.substitute(
+      vars.begin(), vars.end(), vars_free.begin(), vars_free.end());
+}
+
+Node VtsTermCache::rewriteVtsSymbols(Node n)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if ((n.getKind() == EQUAL || n.getKind() == GEQ))
+  {
+    Trace("quant-vts-debug") << "VTS : process " << n << std::endl;
+    Node rew_vts_inf;
+    bool rew_delta = false;
+    // rewriting infinity always takes precedence over rewriting delta
+    for (unsigned r = 0; r < 2; r++)
+    {
+      TypeNode tn = r == 0 ? nm->realType() : nm->integerType();
+      Node inf = getVtsInfinity(tn, false, false);
+      if (!inf.isNull() && expr::hasSubterm(n, inf))
+      {
+        if (rew_vts_inf.isNull())
+        {
+          rew_vts_inf = inf;
+        }
+        else
+        {
+          // for mixed int/real with multiple infinities
+          Trace("quant-vts-debug") << "Multiple infinities...equate " << inf
+                                   << " = " << rew_vts_inf << std::endl;
+          std::vector<Node> subs_lhs;
+          subs_lhs.push_back(inf);
+          std::vector<Node> subs_rhs;
+          subs_lhs.push_back(rew_vts_inf);
+          n = n.substitute(subs_lhs.begin(),
+                           subs_lhs.end(),
+                           subs_rhs.begin(),
+                           subs_rhs.end());
+          n = Rewriter::rewrite(n);
+          // may have cancelled
+          if (!expr::hasSubterm(n, rew_vts_inf))
+          {
+            rew_vts_inf = Node::null();
+          }
+        }
+      }
+    }
+    if (rew_vts_inf.isNull())
+    {
+      if (!d_vts_delta.isNull() && expr::hasSubterm(n, d_vts_delta))
+      {
+        rew_delta = true;
+      }
+    }
+    if (!rew_vts_inf.isNull() || rew_delta)
+    {
+      std::map<Node, Node> msum;
+      if (ArithMSum::getMonomialSumLit(n, msum))
+      {
+        if (Trace.isOn("quant-vts-debug"))
+        {
+          Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl;
+          ArithMSum::debugPrintMonomialSum(msum, "quant-vts-debug");
+        }
+        Node vts_sym = !rew_vts_inf.isNull() ? rew_vts_inf : d_vts_delta;
+        Assert(!vts_sym.isNull());
+        Node iso_n;
+        Node nlit;
+        int res = ArithMSum::isolate(vts_sym, msum, iso_n, n.getKind(), true);
+        if (res != 0)
+        {
+          Trace("quant-vts-debug") << "VTS isolated :  -> " << iso_n
+                                   << ", res = " << res << std::endl;
+          Node slv = iso_n[res == 1 ? 1 : 0];
+          // ensure the vts terms have been eliminated
+          if (containsVtsTerm(slv))
+          {
+            Trace("quant-vts-warn")
+                << "Bad vts literal : " << n << ", contains " << vts_sym
+                << " but bad solved form " << slv << "." << std::endl;
+            // safe case: just convert to free symbols
+            nlit = substituteVtsFreeTerms(n);
+            Trace("quant-vts-debug") << "...return " << nlit << std::endl;
+            return nlit;
+          }
+          else
+          {
+            if (!rew_vts_inf.isNull())
+            {
+              nlit = nm->mkConst(n.getKind() == GEQ && res == 1);
+            }
+            else
+            {
+              Assert(iso_n[res == 1 ? 0 : 1] == d_vts_delta);
+              if (n.getKind() == EQUAL)
+              {
+                nlit = nm->mkConst(false);
+              }
+              else if (res == 1)
+              {
+                nlit = nm->mkNode(GEQ, d_zero, slv);
+              }
+              else
+              {
+                nlit = nm->mkNode(GT, slv, d_zero);
+              }
+            }
+          }
+          Trace("quant-vts-debug") << "Return " << nlit << std::endl;
+          return nlit;
+        }
+        else
+        {
+          Trace("quant-vts-warn")
+              << "Bad vts literal : " << n << ", contains " << vts_sym
+              << " but could not isolate." << std::endl;
+          // safe case: just convert to free symbols
+          nlit = substituteVtsFreeTerms(n);
+          Trace("quant-vts-debug") << "...return " << nlit << std::endl;
+          return nlit;
+        }
+      }
+    }
+    return n;
+  }
+  else if (n.getKind() == FORALL)
+  {
+    // cannot traverse beneath quantifiers
+    return substituteVtsFreeTerms(n);
+  }
+  bool childChanged = false;
+  std::vector<Node> children;
+  for (const Node& nc : n)
+  {
+    Node nn = rewriteVtsSymbols(nc);
+    children.push_back(nn);
+    childChanged = childChanged || nn != nc;
+  }
+  if (childChanged)
+  {
+    if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      children.insert(children.begin(), n.getOperator());
+    }
+    Node ret = nm->mkNode(n.getKind(), children);
+    Trace("quant-vts-debug") << "...make node " << ret << std::endl;
+    return ret;
+  }
+  return n;
+}
+
+bool VtsTermCache::containsVtsTerm(Node n, bool isFree)
+{
+  std::vector<Node> t;
+  getVtsTerms(t, isFree, false);
+  return expr::hasSubterm(n, t);
+}
+
+bool VtsTermCache::containsVtsTerm(std::vector<Node>& n, bool isFree)
+{
+  std::vector<Node> t;
+  getVtsTerms(t, isFree, false);
+  if (!t.empty())
+  {
+    for (const Node& nc : n)
+    {
+      if (expr::hasSubterm(nc, t))
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool VtsTermCache::containsVtsInfinity(Node n, bool isFree)
+{
+  std::vector<Node> t;
+  getVtsTerms(t, isFree, false, false);
+  return expr::hasSubterm(n, t);
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h
new file mode 100644
index 000000000..1c3ec0801
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.h
@@ -0,0 +1,145 @@
+/*********************                                                        */
+/*! \file vts_term_cache.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Virtual term substitution term cache.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
+#define CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
+
+#include <map>
+#include "expr/attribute.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+/** Attribute to mark Skolems as virtual terms */
+struct VirtualTermSkolemAttributeId
+{
+};
+typedef expr::Attribute<VirtualTermSkolemAttributeId, bool>
+    VirtualTermSkolemAttribute;
+
+namespace quantifiers {
+
+/** Virtual term substitution term cache
+ *
+ * This class stores skolems corresponding to virtual terms (e.g. delta and
+ * infinity) and has methods for performing virtual term substitution.
+ *
+ * In detail, there are three kinds of virtual terms:
+ * (1) delta, of Real type, representing a infinitesimally small real value,
+ * (2) infinity, of Real type, representing an infinitely large real value,
+ * (3) infinity, of Int type, representing an infinitely large integer value.
+ *
+ * For each of the above three virtual terms, we have 2 variants.
+ *
+ * The first variant we simply call "virtual terms". These terms are intended
+ * to never appear in assertions and are simply used by algorithms e.g. CEGQI
+ * for specifying instantiations. They are eliminated by the standard rules of
+ * virtual term substitution, e.g.:
+ *   t < s + delta ---> t <=s
+ *   t <= s + delta ---> t <= s
+ *   t < s - delta ----> t < s
+ *   t <= s - delta -----> t < s
+ *   t <= s + inf ----> true
+ *   t <= s - inf ----> false
+ *
+ * The second variant we call "free virtual terms". These terms are intended
+ * to appear in assertions and are constrained to have the semantics of the
+ * above virtual terms, e.g.:
+ *   0 < delta_free
+ *   forall x. x < inf_free
+ * We use free virtual terms for some instantiation strategies, e.g. those
+ * that combine instantiating quantified formulas with nested quantifiers
+ * with terms containing virtual terms.
+ */
+class VtsTermCache
+{
+ public:
+  VtsTermCache(QuantifiersEngine* qe);
+  ~VtsTermCache() {}
+  /**
+   * Get vts delta. The argument isFree indicates if we are getting the
+   * free variant of delta. If create is false, this method returns Node::null
+   * if the requested delta has not already been created.
+   */
+  Node getVtsDelta(bool isFree = false, bool create = true);
+  /**
+   * Get vts infinity of type tn, where tn should be Int or Real.
+   * The argument isFree indicates if we are getting the free variant of
+   * infinity. If create is false, this method returns Node::null if the
+   * requested infinity has not already been created.
+   */
+  Node getVtsInfinity(TypeNode tn, bool isFree = false, bool create = true);
+  /**
+   * Get all vts terms and add them to vector t.
+   * If the argument isFree is true, we return the free variant of all virtual
+   * terms. If create is false, we do not add virtual terms that have not
+   * already been created. If inc_delta is false, we do not include delta.
+   */
+  void getVtsTerms(std::vector<Node>& t,
+                   bool isFree = false,
+                   bool create = true,
+                   bool inc_delta = true);
+  /**
+   * Rewrite virtual terms in node n. This returns the rewritten form of n
+   * after virtual term substitution.
+   *
+   * This method ensures that the returned node is equivalent to n and does
+   * not contain free occurrences of the virtual terms.
+   */
+  Node rewriteVtsSymbols(Node n);
+  /**
+   * This method returns true iff n contains a virtual term. If isFree is true,
+   * if returns true iff n contains a free virtual term.
+   */
+  bool containsVtsTerm(Node n, bool isFree = false);
+  /**
+   * This method returns true iff any term in vector n contains a virtual term.
+   * If isFree is true, if returns true iff any term in vector n contains a
+   * free virtual term.
+   */
+  bool containsVtsTerm(std::vector<Node>& n, bool isFree = false);
+  /**
+   * This method returns true iff n contains an occurence of the virtual term
+   * infinity. If isFree is true, if returns true iff n contains the free
+   * virtual term infinity.
+   */
+  bool containsVtsInfinity(Node n, bool isFree = false);
+
+ private:
+  /** pointer to the quantifiers engine */
+  QuantifiersEngine* d_qe;
+  /** constants */
+  Node d_zero;
+  /** The virtual term substitution delta */
+  Node d_vts_delta;
+  /** The virtual term substitution "free delta" */
+  Node d_vts_delta_free;
+  /** The virtual term substitution infinities for int/real types */
+  std::map<TypeNode, Node> d_vts_inf;
+  /** The virtual term substitution "free infinities" for int/real types */
+  std::map<TypeNode, Node> d_vts_inf_free;
+  /** substitute vts terms with their corresponding vts free terms */
+  Node substituteVtsFreeTerms(Node n);
+}; /* class TermUtil */
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 6ffc50c97..c9c738eb3 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -304,215 +304,6 @@ void TermUtil::computeInstConstContainsForQuant(Node q,
   }
 }
 
-void TermUtil::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) {
-  if( inc_delta ){
-    Node delta = getVtsDelta( isFree, create );
-    if( !delta.isNull() ){
-      t.push_back( delta );
-    }
-  }
-  for( unsigned r=0; r<2; r++ ){
-    Node inf = getVtsInfinityIndex( r, isFree, create );
-    if( !inf.isNull() ){
-      t.push_back( inf );
-    }
-  }
-}
-
-Node TermUtil::getVtsDelta( bool isFree, bool create ) {
-  if( create ){
-    if( d_vts_delta_free.isNull() ){
-      d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" );
-      Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, d_zero );
-      d_quantEngine->getOutputChannel().lemma( delta_lem );
-    }
-    if( d_vts_delta.isNull() ){
-      d_vts_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for virtual term substitution" );
-      //mark as a virtual term
-      VirtualTermSkolemAttribute vtsa;
-      d_vts_delta.setAttribute(vtsa,true);
-    }
-  }
-  return isFree ? d_vts_delta_free : d_vts_delta;
-}
-
-Node TermUtil::getVtsInfinity( TypeNode tn, bool isFree, bool create ) {
-  if( create ){
-    if( d_vts_inf_free[tn].isNull() ){
-      d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf_free", tn, "free infinity for virtual term substitution" );
-    }
-    if( d_vts_inf[tn].isNull() ){
-      d_vts_inf[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "infinity for virtual term substitution" );
-      //mark as a virtual term
-      VirtualTermSkolemAttribute vtsa;
-      d_vts_inf[tn].setAttribute(vtsa,true);
-    }
-  }
-  return isFree ? d_vts_inf_free[tn] : d_vts_inf[tn];
-}
-
-Node TermUtil::getVtsInfinityIndex( int i, bool isFree, bool create ) {
-  if( i==0 ){
-    return getVtsInfinity( NodeManager::currentNM()->realType(), isFree, create );
-  }else if( i==1 ){
-    return getVtsInfinity( NodeManager::currentNM()->integerType(), isFree, create );
-  }else{
-    Assert( false );
-    return Node::null();
-  }
-}
-
-Node TermUtil::substituteVtsFreeTerms( Node n ) {
-  std::vector< Node > vars;
-  getVtsTerms( vars, false, false );
-  std::vector< Node > vars_free;
-  getVtsTerms( vars_free, true, false );
-  Assert( vars.size()==vars_free.size() );
-  if( !vars.empty() ){
-    return n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() );
-  }else{
-    return n;
-  }
-}
-
-Node TermUtil::rewriteVtsSymbols( Node n ) {
-  if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){
-    Trace("quant-vts-debug") << "VTS : process " << n << std::endl;
-    Node rew_vts_inf;
-    bool rew_delta = false;
-    //rewriting infinity always takes precedence over rewriting delta
-    for( unsigned r=0; r<2; r++ ){
-      Node inf = getVtsInfinityIndex( r, false, false );
-      if (!inf.isNull() && expr::hasSubterm(n, inf))
-      {
-        if( rew_vts_inf.isNull() ){
-          rew_vts_inf = inf;
-        }else{
-          //for mixed int/real with multiple infinities
-          Trace("quant-vts-debug") << "Multiple infinities...equate " << inf << " = " << rew_vts_inf << std::endl;
-          std::vector< Node > subs_lhs;
-          subs_lhs.push_back( inf );
-          std::vector< Node > subs_rhs;
-          subs_lhs.push_back( rew_vts_inf );
-          n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
-          n = Rewriter::rewrite( n );
-          // may have cancelled
-          if (!expr::hasSubterm(n, rew_vts_inf))
-          {
-            rew_vts_inf = Node::null();
-          }
-        }
-      }
-    }
-    if (rew_vts_inf.isNull())
-    {
-      if (!d_vts_delta.isNull() && expr::hasSubterm(n, d_vts_delta))
-      {
-        rew_delta = true;
-      }
-    }
-    if( !rew_vts_inf.isNull()  || rew_delta ){
-      std::map< Node, Node > msum;
-      if (ArithMSum::getMonomialSumLit(n, msum))
-      {
-        if( Trace.isOn("quant-vts-debug") ){
-          Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl;
-          ArithMSum::debugPrintMonomialSum(msum, "quant-vts-debug");
-        }
-        Node vts_sym = !rew_vts_inf.isNull() ? rew_vts_inf : d_vts_delta;
-        Assert( !vts_sym.isNull() );
-        Node iso_n;
-        Node nlit;
-        int res = ArithMSum::isolate(vts_sym, msum, iso_n, n.getKind(), true);
-        if( res!=0 ){
-          Trace("quant-vts-debug") << "VTS isolated :  -> " << iso_n << ", res = " << res << std::endl;
-          Node slv = iso_n[res==1 ? 1 : 0];
-          //ensure the vts terms have been eliminated
-          if( containsVtsTerm( slv ) ){
-            Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but bad solved form " << slv << "." << std::endl;
-            nlit = substituteVtsFreeTerms( n );
-            Trace("quant-vts-debug") << "...return " << nlit << std::endl;
-            //Assert( false );
-            //safe case: just convert to free symbols
-            return nlit;
-          }else{
-            if( !rew_vts_inf.isNull() ){
-              nlit = ( n.getKind()==GEQ && res==1 ) ? d_true : d_false;
-            }else{
-              Assert( iso_n[res==1 ? 0 : 1]==d_vts_delta );
-              if( n.getKind()==EQUAL ){
-                nlit = d_false;
-              }else if( res==1 ){
-                nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv );
-              }else{
-                nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero );
-              }
-            }
-          }
-          Trace("quant-vts-debug") << "Return " << nlit << std::endl;
-          return nlit;
-        }else{
-          Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but could not isolate." << std::endl;
-          //safe case: just convert to free symbols
-          nlit = substituteVtsFreeTerms( n );
-          Trace("quant-vts-debug") << "...return " << nlit << std::endl;
-          //Assert( false );
-          return nlit;
-        }
-      }
-    }
-    return n;
-  }else if( n.getKind()==FORALL ){
-    //cannot traverse beneath quantifiers
-    return substituteVtsFreeTerms( n );
-  }else{
-    bool childChanged = false;
-    std::vector< Node > children;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      Node nn = rewriteVtsSymbols( n[i] );
-      children.push_back( nn );
-      childChanged = childChanged || nn!=n[i];
-    }
-    if( childChanged ){
-      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.insert( children.begin(), n.getOperator() );
-      }
-      Node ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-      Trace("quant-vts-debug") << "...make node " << ret << std::endl;
-      return ret;
-    }else{
-      return n;
-    }
-  }
-}
-
-bool TermUtil::containsVtsTerm( Node n, bool isFree ) {
-  std::vector< Node > t;
-  getVtsTerms( t, isFree, false );
-  return expr::hasSubterm(n, t);
-}
-
-bool TermUtil::containsVtsTerm( std::vector< Node >& n, bool isFree ) {
-  std::vector< Node > t;
-  getVtsTerms( t, isFree, false );
-  if( !t.empty() ){
-    for (const Node& nc : n)
-    {
-      if (expr::hasSubterm(nc, t))
-      {
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-bool TermUtil::containsVtsInfinity( Node n, bool isFree ) {
-  std::vector< Node > t;
-  getVtsTerms( t, isFree, false, false );
-  return expr::hasSubterm(n, t);
-}
-
 Node TermUtil::ensureType( Node n, TypeNode tn ) {
   TypeNode ntn = n.getType();
   Assert( ntn.isComparableTo( tn ) );
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 52965d2fa..9906eef2f 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -76,10 +76,6 @@ typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
 struct QuantIdNumAttributeId {};
 typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
 
-/** Attribute to mark Skolems as virtual terms */
-struct VirtualTermSkolemAttributeId {};
-typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute;
-
 class QuantifiersEngine;
 
 namespace inst{
@@ -188,31 +184,7 @@ public:
                                                Node n,
                                                std::vector<Node>& vars);
 
-//for virtual term substitution
-private:
-  Node d_vts_delta;
-  std::map< TypeNode, Node > d_vts_inf;
-  Node d_vts_delta_free;
-  std::map< TypeNode, Node > d_vts_inf_free;
-  /** get vts infinity index */
-  Node getVtsInfinityIndex( int i, bool isFree = false, bool create = true  );
-  /** substitute vts free terms */
-  Node substituteVtsFreeTerms( Node n );
 public:
-  /** get vts delta */
-  Node getVtsDelta( bool isFree = false, bool create = true );
-  /** get vts infinity */
-  Node getVtsInfinity( TypeNode tn, bool isFree = false, bool create = true );
-  /** get all vts terms */
-  void getVtsTerms( std::vector< Node >& t, bool isFree = false, bool create = true, bool inc_delta = true );
-  /** rewrite delta */
-  Node rewriteVtsSymbols( Node n );
-  /** simple check for contains term */
-  bool containsVtsTerm( Node n, bool isFree = false );
-  /** simple check for contains term */
-  bool containsVtsTerm( std::vector< Node >& n, bool isFree = false );
-  /** simple check for contains term */
-  bool containsVtsInfinity( Node n, bool isFree = false );
   /** ensure type */
   static Node ensureType( Node n, TypeNode tn );