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

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 38b53e1070bdcb7a6f9e2c974901a746be746f3b..0d9eb3a5fd839ad9724462382d6a107f2f08656f 100644 (file)
--- 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 8b1a320a2cce9c10c0a0bb5b0972b305ee2f64fd..1264a0fb87a0f751eaa3ecc7192079edb87e2e5f 100644 (file)
--- 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 a990e008cd863a4f83bc3951a425f6653c4d28eb..0ae506b252ceb7d7638f8eca8586f636c0693d50 100644 (file)
--- 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;

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 7f333007a754b363649c1549cd305e95ce2d45ea..c3d02bbd6e0ae978f7e45e45d62fb6c2c1818a78 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1087,6 +1087,7 @@ REG1_TESTS = \
        regress1/lemmas/pursuit-safety-8.smt \
        regress1/lemmas/simple_startup_9nodes.abstract.base.smt \
        regress1/nl/NAVIGATION2.smt2 \
+       regress1/nl/arctan2-expdef.smt2 \
        regress1/nl/arrowsmith-050317.smt2 \
        regress1/nl/bad-050217.smt2 \
        regress1/nl/bug698.smt2 \

diff --git a/test/regress/regress1/nl/arctan2-expdef.smt2 b/test/regress/regress1/nl/arctan2-expdef.smt2
new file mode 100644 (file)
index 0000000..8a84948
--- /dev/null
+++ b/test/regress/regress1/nl/arctan2-expdef.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_NRA)
+(set-info :status unsat)
+(set-option :arith-no-partial-fun true)
+(declare-fun lat1 () Real)
+(declare-fun lat2 () Real)
+
+(declare-fun arctan2u () Real)
+(define-fun arctan2 ((x Real) (y Real)) Real
+  (arctan (/ y x)))
+      
+(assert (= (arctan2 lat1 lat2) 3))
+(check-sat)