From: Andrew Reynolds Date: Thu, 31 Mar 2022 18:05:53 +0000 (-0500) Subject: Fix check for whether PI is reduced (#8485) X-Git-Tag: cvc5-1.0.0~90 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c53479aab2d7bb086a9d25acd0417c60b98affc;p=cvc5.git Fix check for whether PI is reduced (#8485) Fixes cvc5/cvc5-projects#505. Also fixes a counter-intuitive behavior where 0 was not considered reduced and does minor cleanup. --- diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp index b1ec1061a..a027c7882 100644 --- a/src/theory/arith/nl/ext_theory_callback.cpp +++ b/src/theory/arith/nl/ext_theory_callback.cpp @@ -37,12 +37,9 @@ bool NlExtTheoryCallback::getCurrentSubstitution( std::map>& exp) { // get the constant equivalence classes - std::map> rep_to_subs_index; - bool retVal = false; - for (unsigned i = 0; i < vars.size(); i++) + for (const Node& n : vars) { - Node n = vars[i]; if (d_ee->hasTerm(n)) { Node nr = d_ee->getRepresentative(n); @@ -56,7 +53,6 @@ bool NlExtTheoryCallback::getCurrentSubstitution( } else { - rep_to_subs_index[nr].push_back(i); subs.push_back(n); } } @@ -65,7 +61,6 @@ bool NlExtTheoryCallback::getCurrentSubstitution( subs.push_back(n); } } - // return true if the substitution is non-trivial return retVal; } @@ -73,17 +68,29 @@ bool NlExtTheoryCallback::getCurrentSubstitution( bool NlExtTheoryCallback::isExtfReduced( int effort, Node n, Node on, std::vector& exp, ExtReducedId& id) { + if (isTranscendentalKind(on.getKind())) + { + // we do not handle reductions of transcendental functions here + return false; + } if (n != d_zero) { Kind k = n.getKind(); if (k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND && k != POW2) { + // we consider an extended function to be reduced if it simplifies to + // something that is not a non-linear term. For example, if we know + // that (= x 5), then (NONLINEAR_MULT x y) can be simplified to + // (MULT 5 y). We may consider (NONLINEAR_MULT x y) to be reduced. id = ExtReducedId::ARITH_SR_LINEAR; return true; } return false; } + // As an optimization, we minimize the explanation for why a term can be + // simplified to zero, for example, if (= x 0) ^ (= y 5) => (= (* x y) 0), + // we minimize the explanation to (= x 0) => (= (* x y) 0). Assert(n == d_zero); id = ExtReducedId::ARITH_SR_ZERO; if (on.getKind() == NONLINEAR_MULT) @@ -129,7 +136,7 @@ bool NlExtTheoryCallback::isExtfReduced( } } } - return false; + return true; } } // namespace nl diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h index 5226601a6..e8a64e920 100644 --- a/src/theory/arith/nl/ext_theory_callback.h +++ b/src/theory/arith/nl/ext_theory_callback.h @@ -32,43 +32,32 @@ class NlExtTheoryCallback : public ExtTheoryCallback public: NlExtTheoryCallback(eq::EqualityEngine* ee); ~NlExtTheoryCallback() {} - /** Get current substitution - * - * This function and the one below are - * used for context-dependent - * simplification, see Section 3.1 of - * "Designing Theory Solvers with Extensions" - * by Reynolds et al. FroCoS 2017. - * - * effort : an identifier indicating the stage where - * we are performing context-dependent simplification, - * vars : a set of arithmetic variables. - * - * This function populates subs and exp, such that for 0 <= i < vars.size(): - * ( exp[vars[i]] ) => vars[i] = subs[i] - * where exp[vars[i]] is a set of assertions - * that hold in the current context. We call { vars -> subs } a "derivable - * substituion" (see Reynolds et al. FroCoS 2017). + /** + * Gets the current substitution, which maps v in vars to a constant c + * if there is a constant in its equivalence class, or to v itself otherwise. + * In this case, it adds (= v c) as the explanation for the substitution of v. + * Returns true if the substitution is non-trivial. */ bool getCurrentSubstitution(int effort, const std::vector& vars, std::vector& subs, std::map>& exp) override; - /** Is the term n in reduced form? - * - * Used for context-dependent simplification. + /** + * Check whether the extended function `on` which can be simplified to `n` + * should be considered "reduced". Terms that are considered reduced are + * guaranteed to have the correct value in models and thus can be ignored + * if necessary by the theory solver. For example, if (= x 0) and + * (= (* x y) 0), then (* x y) may be considered reduced. The motivation is + * to minimize the number of terms that the non-linear solver must consider. * - * effort : an identifier indicating the stage where - * we are performing context-dependent simplification, - * on : the original term that we reduced to n, - * exp : an explanation such that ( exp => on = n ). + * This method returns true if + * (1) the extended term on is not a transcendental function, + * (2) the top symobl of n does not belong to non-linear arithmetic. * - * We return a pair ( b, exp' ) such that - * if b is true, then: - * n is in reduced form - * if exp' is non-null, then ( exp' => on = n ) - * The second part of the pair is used for constructing - * minimal explanations for context-dependent simplifications. + * For example, + * if on, n = (* x y), (* 5 y), we return true + * if on, n = (* x y), 6, we return true + * if on, n = (* x y z), (* y z), we return false */ bool isExtfReduced(int effort, Node n, diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 606f37d44..f20bc9edd 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -818,10 +818,12 @@ set(regress_0_tests regress0/nl/nta/issue8208-red-nred.smt2 regress0/nl/nta/issue8294-2-double-solve.smt2 regress0/nl/nta/issue8415-embed-arg.smt2 + regress0/nl/nta/pi-simplest.smt2 regress0/nl/nta/proj-issue376.smt2 regress0/nl/nta/proj-issue403.smt2 regress0/nl/nta/proj-issue460-pi-value.smt2 regress0/nl/nta/proj-issue483-arccos-oob.smt2 + regress0/nl/nta/proj-issue505-pi-red.smt2 regress0/nl/nta/real-pi.smt2 regress0/nl/nta/sin-sym.smt2 regress0/nl/nta/sin-sym-schema.smt2 diff --git a/test/regress/cli/regress0/nl/nta/pi-simplest.smt2 b/test/regress/cli/regress0/nl/nta/pi-simplest.smt2 new file mode 100644 index 000000000..6a88e6fe0 --- /dev/null +++ b/test/regress/cli/regress0/nl/nta/pi-simplest.smt2 @@ -0,0 +1,4 @@ +; EXPECT: unsat +(set-logic ALL) +(assert (= real.pi 1.0)) +(check-sat) diff --git a/test/regress/cli/regress0/nl/nta/proj-issue505-pi-red.smt2 b/test/regress/cli/regress0/nl/nta/proj-issue505-pi-red.smt2 new file mode 100644 index 000000000..323eb4d38 --- /dev/null +++ b/test/regress/cli/regress0/nl/nta/proj-issue505-pi-red.smt2 @@ -0,0 +1,5 @@ +; EXPECT: unsat +(set-logic ALL) +(assert (is_int (arcsin real.pi))) +(assert (= real.pi (cos real.pi))) +(check-sat)