diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-11 11:58:53 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-12-11 11:58:53 -0600 |
| commit | 23eb6c0ab05b6607c14ee33b5c0101381aa0bc41 (patch) | |
| tree | ef91882b2bf83f66daa324428b8449bea146020a /src/theory/arith/arith_utilities.h | |
| parent | b12f67c710d359cd57d09dbff67f13bf26e10834 (diff) | |
Do not substitute beneath arithmetic terms in the non-linear solver (#3324)
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 */ |