From: Andrew Reynolds Date: Fri, 13 May 2022 23:07:49 +0000 (-0500) Subject: Make arith substitute its own utility (#8765) X-Git-Tag: cvc5-1.0.1~132 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c8b193f93369e042bf768d8ba567d6dc4ba01e7e;p=cvc5.git Make arith substitute its own utility (#8765) Arithmetic substitutions behave differently in two ways: (1) they traverse only symbols belonging to arithmetic (2) they allow mixing Int/Real This makes ArithSubs derive from the more general Subs class with these two behavior changes. This is one of the last remaining non-trivial steps towards for eliminating TypeNode::isSubtypeOf. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6facce4e8..3b3069723 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -363,6 +363,8 @@ libcvc5_add_sources( theory/arith/arith_rewriter.h theory/arith/arith_state.cpp theory/arith/arith_state.h + theory/arith/arith_subs.cpp + theory/arith/arith_subs.h theory/arith/arith_utilities.cpp theory/arith/arith_utilities.h theory/arith/bound_inference.cpp diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp index c5aa7edcb..cebff11c5 100644 --- a/src/expr/subs.cpp +++ b/src/expr/subs.cpp @@ -69,7 +69,7 @@ void Subs::add(const std::vector& vs) } } -void Subs::add(Node v, Node s) +void Subs::add(const Node& v, const Node& s) { Assert(s.isNull() || v.getType().isComparableTo(s.getType())); d_vars.push_back(v); @@ -97,7 +97,7 @@ void Subs::append(Subs& s) add(s.d_vars, s.d_subs); } -Node Subs::apply(Node n) const +Node Subs::apply(const Node& n) const { if (d_vars.empty()) { diff --git a/src/expr/subs.h b/src/expr/subs.h index 7761f3e77..ad3f3aa13 100644 --- a/src/expr/subs.h +++ b/src/expr/subs.h @@ -35,6 +35,8 @@ namespace cvc5::internal { class Subs { public: + Subs() {} + virtual ~Subs() {} /** Is the substitution empty? */ bool empty() const; /** The size of the substitution */ @@ -50,7 +52,7 @@ class Subs /** Add v -> k for fresh skolem of the same type as v for each v in vs */ void add(const std::vector& vs); /** Add v -> s to the substitution */ - void add(Node v, Node s); + void add(const Node& v, const Node& s); /** Add vs -> ss to the substitution */ void add(const std::vector& vs, const std::vector& ss); /** Add eq[0] -> eq[1] to the substitution */ @@ -58,7 +60,7 @@ class Subs /** Append the substitution s to this */ void append(Subs& s); /** Return the result of this substitution on n */ - Node apply(Node n) const; + Node apply(const Node& n) const; /** Return the result of the reverse of this substitution on n */ Node rapply(Node n) const; /** Apply this substitution to all nodes in the range of s */ diff --git a/src/theory/arith/arith_subs.cpp b/src/theory/arith/arith_subs.cpp new file mode 100644 index 000000000..9e62736ad --- /dev/null +++ b/src/theory/arith/arith_subs.cpp @@ -0,0 +1,110 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Arithmetic substitution utility. + */ + +#include "theory/arith/arith_subs.h" + +#include "theory/arith/arith_utilities.h" + +namespace cvc5::internal { +namespace theory { +namespace arith { + +void ArithSubs::addArith(const Node& v, const Node& s) +{ + Assert(v.getType().isRealOrInt()); + Assert(s.getType().isRealOrInt()); + d_vars.push_back(v); + d_subs.push_back(s); +} + +Node ArithSubs::applyArith(const Node& n) const +{ + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map visited; + std::vector visit; + visit.push_back(n); + do + { + TNode cur = visit.back(); + visit.pop_back(); + auto it = visited.find(cur); + + if (it == visited.end()) + { + visited[cur] = Node::null(); + Kind ck = cur.getKind(); + auto s = find(cur); + if (s) + { + visited[cur] = *s; + } + else if (cur.getNumChildren() == 0) + { + visited[cur] = cur; + } + else + { + TheoryId ctid = theory::kindToTheoryId(ck); + if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL + && ctid != THEORY_BUILTIN) + || isTranscendentalKind(ck)) + { + // Do not traverse beneath applications that belong to another theory + // besides (core) arithmetic. Notice that transcendental function + // applications are also not traversed here. + visited[cur] = cur; + } + else + { + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + +} // namespace arith +} // namespace theory +} // namespace cvc5::internal diff --git a/src/theory/arith/arith_subs.h b/src/theory/arith/arith_subs.h new file mode 100644 index 000000000..2aff9f62e --- /dev/null +++ b/src/theory/arith/arith_subs.h @@ -0,0 +1,52 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Arithmetic substitution utility. + */ + +#ifndef CVC5__THEORY__ARITH__SUBS_H +#define CVC5__THEORY__ARITH__SUBS_H + +#include +#include +#include + +#include "expr/subs.h" + +namespace cvc5::internal { +namespace theory { +namespace arith { + +/** + * applyArith computes the substitution n { subs }, but with the caveat + * that subterms of n that belong to a theory other than arithmetic are + * not traversed. In other words, terms that belong to other theories are + * treated as atomic variables. For example: + * (5*f(x) + 7*x ){ x -> 3 } returns 5*f(x) + 7*3. + * + * Note that in contrast to the ordinary substitution class, this class allows + * mixing integers and reals via addArith. + */ +class ArithSubs : public Subs +{ + public: + /** Add v -> s to the substitution */ + void addArith(const Node& v, const Node& s); + /** Return the result of this substitution on n */ + Node applyArith(const Node& n) const; +}; + +} // namespace arith +} // namespace theory +} // namespace cvc5::internal + +#endif /* CVC5__THEORY__ARITH__SUBS_H */ diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index 76ca33ce1..02fda5156 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -13,7 +13,7 @@ * Implementation of common functions for dealing with nodes. */ -#include "arith_utilities.h" +#include "theory/arith/arith_utilities.h" #include @@ -219,82 +219,6 @@ void printRationalApprox(const char* c, Node cr, unsigned prec) } } -Node arithSubstitute(Node n, const Subs& sub) -{ - NodeManager* nm = NodeManager::currentNM(); - std::unordered_map visited; - std::vector visit; - visit.push_back(n); - do - { - TNode cur = visit.back(); - visit.pop_back(); - auto it = visited.find(cur); - - if (it == visited.end()) - { - visited[cur] = Node::null(); - Kind ck = cur.getKind(); - auto s = sub.find(cur); - if (s) - { - visited[cur] = *s; - } - else if (cur.getNumChildren() == 0) - { - visited[cur] = cur; - } - else - { - TheoryId ctid = theory::kindToTheoryId(ck); - if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL - && ctid != THEORY_BUILTIN) - || isTranscendentalKind(ck)) - { - // Do not traverse beneath applications that belong to another theory - // besides (core) arithmetic. Notice that transcendental function - // applications are also not traversed here. - visited[cur] = cur; - } - else - { - visit.push_back(cur); - for (const Node& cn : cur) - { - visit.push_back(cn); - } - } - } - } - else if (it->second.isNull()) - { - Node ret = cur; - bool childChanged = false; - std::vector children; - if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) - { - children.push_back(cur.getOperator()); - } - for (const Node& cn : cur) - { - it = visited.find(cn); - Assert(it != visited.end()); - Assert(!it->second.isNull()); - childChanged = childChanged || cn != it->second; - children.push_back(it->second); - } - if (childChanged) - { - ret = nm->mkNode(cur.getKind(), children); - } - visited[cur] = ret; - } - } while (!visit.empty()); - Assert(visited.find(n) != visited.end()); - Assert(!visited.find(n)->second.isNull()); - return visited[n]; -} - Node mkBounded(Node l, Node a, Node u) { NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 92151d688..c08dbff0b 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -312,16 +312,6 @@ Node getApproximateConstant(Node c, bool isLower, unsigned prec); /** print rational approximation of cr with precision prec on trace c */ void printRationalApprox(const char* c, Node cr, unsigned prec = 5); -/** Arithmetic substitute - * - * This computes the substitution n { subs }, but with the caveat - * that subterms of n that belong to a theory other than arithmetic are - * not traversed. In other words, terms that belong to other theories are - * treated as atomic variables. For example: - * (5*f(x) + 7*x ){ x -> 3 } returns 5*f(x) + 7*3. - */ -Node arithSubstitute(Node n, const Subs& sub); - /** Make the node u >= a ^ a >= l */ Node mkBounded(Node l, Node a, Node u); diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 1fbbabaab..f2e6a5dd7 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -309,17 +309,17 @@ bool NlModel::addSubstitution(TNode v, TNode s) return false; } } - Subs tmp; - tmp.add(v, s); + ArithSubs tmp; + tmp.addArith(v, s); for (auto& sub : d_substitutions.d_subs) { - Node ms = arithSubstitute(sub, tmp); + Node ms = tmp.applyArith(sub); if (ms != sub) { sub = rewrite(ms); } } - d_substitutions.add(v, s); + d_substitutions.addArith(v, s); return true; } @@ -625,7 +625,7 @@ bool NlModel::simpleCheckModelLit(Node lit) ? vs_invalid[0] : nm->mkNode(ADD, vs_invalid)); // substitution to try - Subs qsub; + ArithSubs qsub; for (const Node& v : vs) { // is it a valid variable? @@ -677,7 +677,7 @@ bool NlModel::simpleCheckModelLit(Node lit) Assert(boundn[0].getConst() <= boundn[1].getConst()); Node s; - qsub.add(v, Node()); + qsub.addArith(v, Node()); if (cmp[0] != cmp[1]) { Assert(!cmp[0] && cmp[1]); @@ -695,7 +695,7 @@ bool NlModel::simpleCheckModelLit(Node lit) for (unsigned r = 0; r < 2; r++) { qsub.d_subs.back() = boundn[r]; - Node ts = arithSubstitute(t, qsub); + Node ts = qsub.applyArith(t); tcmpn[r] = rewrite(ts); } Node tcmp = nm->mkNode(LT, tcmpn[0], tcmpn[1]); @@ -734,7 +734,7 @@ bool NlModel::simpleCheckModelLit(Node lit) } if (!qsub.empty()) { - Node slit = arithSubstitute(lit, qsub); + Node slit = qsub.applyArith(lit); slit = rewrite(slit); return simpleCheckModelLit(slit); } @@ -1129,7 +1129,7 @@ Node NlModel::getSubstitutedForm(TNode s) const // no substitutions, just return s return s; } - return rewrite(arithSubstitute(s, d_substitutions)); + return rewrite(d_substitutions.applyArith(s)); } } // namespace nl diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index eee16ed9d..5b9fe11af 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -22,8 +22,8 @@ #include "expr/kind.h" #include "expr/node.h" -#include "expr/subs.h" #include "smt/env_obj.h" +#include "theory/arith/arith_subs.h" namespace cvc5::context { class Context; @@ -201,7 +201,7 @@ class NlModel : protected EnvObj * A substitution from variables that appear in assertions to a solved form * term. */ - Subs d_substitutions; + ArithSubs d_substitutions; /** Get the model value of n from the model object above */ Node getValueInternal(TNode n); diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 72e1b4cd1..11e432159 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -23,6 +23,7 @@ #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_state.h" +#include "theory/arith/arith_subs.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" @@ -96,10 +97,10 @@ void TranscendentalSolver::initLastCall(const std::vector& xts) bool TranscendentalSolver::preprocessAssertionsCheckModel( std::vector& assertions) { - Subs subs; + ArithSubs subs; for (const auto& sub : d_tstate.d_trPurify) { - subs.add(sub.first, sub.second); + subs.addArith(sub.first, sub.second); } // initialize representation of assertions @@ -110,7 +111,7 @@ bool TranscendentalSolver::preprocessAssertionsCheckModel( Node pa = a; if (!subs.empty()) { - pa = arithSubstitute(pa, subs); + pa = subs.applyArith(pa); pa = rewrite(pa); } if (!pa.isConst() || !pa.getConst())