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
}
}
-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);
add(s.d_vars, s.d_subs);
}
-Node Subs::apply(Node n) const
+Node Subs::apply(const Node& n) const
{
if (d_vars.empty())
{
class Subs
{
public:
+ Subs() {}
+ virtual ~Subs() {}
/** Is the substitution empty? */
bool empty() const;
/** The size of the substitution */
/** Add v -> k for fresh skolem of the same type as v for each v in vs */
void add(const std::vector<Node>& 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<Node>& vs, const std::vector<Node>& ss);
/** Add eq[0] -> eq[1] to the substitution */
/** 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 */
--- /dev/null
+/******************************************************************************
+ * 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<TNode, Node> visited;
+ std::vector<TNode> 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<Node> 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
--- /dev/null
+/******************************************************************************
+ * 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 <map>
+#include <optional>
+#include <vector>
+
+#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 */
* Implementation of common functions for dealing with nodes.
*/
-#include "arith_utilities.h"
+#include "theory/arith/arith_utilities.h"
#include <cmath>
}
}
-Node arithSubstitute(Node n, const Subs& sub)
-{
- NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, Node> visited;
- std::vector<TNode> 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<Node> 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();
/** 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);
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;
}
? 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?
Assert(boundn[0].getConst<Rational>()
<= boundn[1].getConst<Rational>());
Node s;
- qsub.add(v, Node());
+ qsub.addArith(v, Node());
if (cmp[0] != cmp[1])
{
Assert(!cmp[0] && cmp[1]);
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]);
}
if (!qsub.empty())
{
- Node slit = arithSubstitute(lit, qsub);
+ Node slit = qsub.applyArith(lit);
slit = rewrite(slit);
return simpleCheckModelLit(slit);
}
// no substitutions, just return s
return s;
}
- return rewrite(arithSubstitute(s, d_substitutions));
+ return rewrite(d_substitutions.applyArith(s));
}
} // namespace nl
#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;
* 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);
#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"
bool TranscendentalSolver::preprocessAssertionsCheckModel(
std::vector<Node>& 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
Node pa = a;
if (!subs.empty())
{
- pa = arithSubstitute(pa, subs);
+ pa = subs.applyArith(pa);
pa = rewrite(pa);
}
if (!pa.isConst() || !pa.getConst<bool>())
projects / cvc5.git / commitdiff