From 166d4351fe55d182a4ed355ac729c5d40a1f9bc1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 3 Apr 2018 15:49:43 -0500 Subject: [PATCH] Use choice when expanding definitions for inverse transcendental functions (#1742) --- src/theory/arith/nonlinear_extension.cpp | 26 ++++---------------- src/theory/arith/nonlinear_extension.h | 11 --------- src/theory/arith/theory_arith_private.cpp | 26 ++++---------------- test/regress/Makefile.tests | 1 + test/regress/regress1/nl/arctan2-expdef.smt2 | 12 +++++++++ 5 files changed, 23 insertions(+), 53 deletions(-) create mode 100644 test/regress/regress1/nl/arctan2-expdef.smt2 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& 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& vars, @@ -2895,11 +2881,9 @@ std::vector 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 > 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; diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 7f333007a..c3d02bbd6 100644 --- 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 index 000000000..8a8494873 --- /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) -- 2.30.2