diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-07 14:09:58 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-07 19:09:58 +0000 |
| commit | 89641ef6aae22610cf544f1e7545178ee6418597 (patch) | |
| tree | 672e7991bbc1b7d2e1e5abf0a9b4a38c08b5baa2 /src/smt/preprocessor.h | |
| parent | 50ff9213e6e6d36cea5a745e5c85ecbf1ca1ab62 (diff) | |
Simplifications to expand definitions (#6487)
This removes the expandOnly flag from expandDefinitions.
The use of expandOnly = true is equivalent to applying top-level substitutions only, which should be done explicitly via Env::getTopLevelSubstitutions. It updates the trust substitutions utility to distinguish apply vs applyTrusted for convenience for this purpose.
This also breaks several dependencies in e.g. expand definitions module.
Diffstat (limited to 'src/smt/preprocessor.h')
| -rw-r--r-- | src/smt/preprocessor.h | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index e0ad2cc14..4c60a2898 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -85,16 +85,12 @@ class Preprocessor * simplification or normalization is done. * * @param n The node to expand - * @param expandOnly if true, then the expandDefinitions function of - * TheoryEngine is not called on subterms of n. * @return The expanded term. */ - Node expandDefinitions(const Node& n, bool expandOnly = false); + Node expandDefinitions(const Node& n); /** Same as above, with a cache of previous results. */ Node expandDefinitions( - const Node& n, - std::unordered_map<Node, Node, NodeHashFunction>& cache, - bool expandOnly = false); + const Node& n, std::unordered_map<Node, Node, NodeHashFunction>& cache); /** * Set proof node manager. Enables proofs in this preprocessor. */ |