std::map<Node, std::vector<Node>>& exp)
{
// get the constant equivalence classes
- std::map<Node, std::vector<int>> 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);
}
else
{
- rep_to_subs_index[nr].push_back(i);
subs.push_back(n);
}
}
subs.push_back(n);
}
}
-
// return true if the substitution is non-trivial
return retVal;
}
bool NlExtTheoryCallback::isExtfReduced(
int effort, Node n, Node on, std::vector<Node>& 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)
}
}
}
- return false;
+ return true;
}
} // namespace nl
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<Node>& vars,
std::vector<Node>& subs,
std::map<Node, std::vector<Node>>& 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,
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
projects / cvc5.git / commitdiff