diff options
Diffstat (limited to 'src/theory/arith/arith_utilities.h')
| -rw-r--r-- | src/theory/arith/arith_utilities.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index d737fefeb..f87a908b4 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -325,6 +325,16 @@ 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 { vars -> 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, std::vector<Node>& vars, std::vector<Node>& subs); + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |