diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-08 20:16:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-08 20:16:27 -0500 |
commit | 25a24a74b0765713e3b11df9b7ea891fdda9523e (patch) | |
tree | eaaae51ad04de4b3d66d006d5f30e8e3a469ff93 /src/theory/quantifiers/sygus/term_database_sygus.h | |
parent | 3daaf4c574aeb61cb0841f37c12051497a077dff (diff) | |
parent | 704fd545440023a0deaa328a9de9c11ac5fe963c (diff) |
Merge branch 'master' into rmStateOptionsrmStateOptions
Diffstat (limited to 'src/theory/quantifiers/sygus/term_database_sygus.h')
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index a44ebd297..7b05c70e4 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -271,21 +271,6 @@ class TermDbSygus : protected EnvObj Node bn, const std::vector<Node>& args, bool tryEval = true); - /** evaluate with unfolding - * - * n is any term that may involve sygus evaluation functions. This function - * returns the result of unfolding the evaluation functions within n and - * rewriting the result. For example, if eval_A is the evaluation function - * for the datatype: - * A -> C_0 | C_1 | C_x | C_+( C_A, C_A ) - * corresponding to grammar: - * A -> 0 | 1 | x | A + A - * then calling this function on eval( C_+( x, 1 ), 4 ) = y returns 5 = y. - * The node returned by this function is in (extended) rewritten form. - */ - Node evaluateWithUnfolding(Node n); - /** same as above, but with a cache of visited nodes */ - Node evaluateWithUnfolding(Node n, std::unordered_map<Node, Node>& visited); /** is evaluation point? * * Returns true if n is of the form eval( x, c1...cn ) for some variable x |