Use choice when expanding definitions for inverse transcendental functions (#1742)

3 files changed, 10 insertions, 53 deletions

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 38b53e107..0d9eb3a5f 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -216,8 +216,7 @@ bool hasNewMonomials(Node n, const std::vector<Node>& existing) {
 
 NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                                        eq::EqualityEngine* ee)
-    : d_def_lemmas(containing.getUserContext()),
-      d_lemmas(containing.getUserContext()),
+    : d_lemmas(containing.getUserContext()),
       d_zero_split(containing.getUserContext()),
       d_skolem_atoms(containing.getUserContext()),
       d_containing(containing),
@@ -1905,22 +1904,9 @@ void NonlinearExtension::check(Theory::Effort e) {
   }
 }
 
-void NonlinearExtension::addDefinition(Node lem)
-{
-  Trace("nl-ext") << "NonlinearExtension::addDefinition : " << lem << std::endl;
-  d_def_lemmas.insert(lem);
-}
-
 void NonlinearExtension::presolve()
 {
-  Trace("nl-ext") << "NonlinearExtension::presolve, #defs = "
-                  << d_def_lemmas.size() << std::endl;
-  for (NodeSet::const_iterator it = d_def_lemmas.begin();
-       it != d_def_lemmas.end();
-       ++it)
-  {
-    flushLemma(*it);
-  }
+  Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl;
 }
 
 void NonlinearExtension::assignOrderIds(std::vector<Node>& vars,
@@ -2895,11 +2881,9 @@ std::vector<Node> NonlinearExtension::checkFactoring(
     }
     else
     {
-      // Only consider literals that evaluate to false in the model.
-      // this is a stronger restriction than the restriction that lit is in
-      // false_asserts.
-      // This excludes (most) literals that contain transcendental functions.
-      considerLit = computeModelValue(lit)==d_false;
+      // Only consider literals that are in false_asserts.
+      considerLit = std::find(false_asserts.begin(), false_asserts.end(), lit)
+                    != false_asserts.end();
     }
 
     if (considerLit)
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 8b1a320a2..1264a0fb8 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -121,15 +121,6 @@ class NonlinearExtension {
   void check(Theory::Effort e);
   /** Does this class need a call to check(...) at last call effort? */
   bool needsCheckLastEffort() const { return d_needsLastCall; }
-  /** add definition
-   *
-   * This function notifies this class that lem is a formula that defines or
-   * constrains an auxiliary variable. For example, during
-   * TheoryArith::expandDefinitions, we replace a term like arcsin( x ) with an
-   * auxiliary variable k. The lemmas 0 <= k < pi and sin( x ) = k are added as
-   * definitions to this class.
-   */
-  void addDefinition(Node lem);
   /** presolve
    *
    * This function is called during TheoryArith's presolve command.
@@ -419,8 +410,6 @@ class NonlinearExtension {
   // ( x*y, x*z, y ) for each pair of monomials ( x*y, x*z ) with common factors
   std::map<Node, std::map<Node, Node> > d_mono_diff;
 
-  /** cache of definition lemmas (user-context-dependent) */
-  NodeSet d_def_lemmas;
   /** cache of all lemmas sent on the output channel (user-context-dependent) */
   NodeSet d_lemmas;
   /** cache of terms t for which we have added the lemma ( t = 0 V t != 0 ). */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index a990e008c..0ae506b25 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4963,10 +4963,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
       NodeMap::const_iterator it = d_nlin_inverse_skolem.find(node);
       if (it == d_nlin_inverse_skolem.end())
       {
-        Node var = nm->mkSkolem("nonlinearInv",
-                                nm->realType(),
-                                "the result of a non-linear inverse function");
-        d_nlin_inverse_skolem[node] = var;
+        Node var = nm->mkBoundVar(nm->realType());
         Node lem;
         if (k == kind::SQRT)
         {
@@ -4994,10 +4991,6 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
                               nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
                               nm->mkNode(LT, var, pi));
           }
-          if (options::nlExt())
-          {
-            d_nonlinearExtension->addDefinition(rlem);
-          }
 
           Kind rk = k == kind::ARCSINE
                         ? kind::SINE
@@ -5011,21 +5004,12 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
                                                     ? kind::SECANT
                                                     : kind::COTANGENT))));
           Node invTerm = nm->mkNode(rk, var);
-          // since invTerm may introduce division,
-          // we must also call expandDefinition on the result
-          invTerm = expandDefinition(logicRequest, invTerm);
-          lem = invTerm.eqNode(node[0]);
+          lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
         }
         Assert(!lem.isNull());
-        if (options::nlExt())
-        {
-          d_nonlinearExtension->addDefinition(lem);
-        }
-        else
-        {
-          d_nlIncomplete = true;
-        }
-        return var;
+        Node ret = nm->mkNode(CHOICE, nm->mkNode(BOUND_VAR_LIST, var), lem);
+        d_nlin_inverse_skolem[node] = ret;
+        return ret;
       }
       return (*it).second;
       break;