diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-13 11:37:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-13 11:37:03 -0500 |
| commit | 68174dedcb4bf9d91241585ab1cc876d2fa83d62 (patch) | |
| tree | 851787c7b22ac16564840512aa61811698cd3abc /src/theory/quantifiers/candidate_rewrite_database.h | |
| parent | 1b8ee921760d15492c0c0492ce6a4da07186699a (diff) | |
Remove spurious data member. (#2857)
Diffstat (limited to 'src/theory/quantifiers/candidate_rewrite_database.h')
| -rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.h | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 3fa9d989a..35c08f43f 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -97,11 +97,6 @@ class CandidateRewriteDatabase : public ExprMiner bool d_using_sygus; /** candidate rewrite filter */ CandidateRewriteFilter d_crewrite_filter; - /** - * Cache of skolems for each free variable that appears in a synthesis check - * (for --sygus-rr-synth-check). - */ - std::map<Node, Node> d_fv_to_skolem; /** the cache for results of addTerm */ std::unordered_map<Node, bool, NodeHashFunction> d_add_term_cache; /** if true, we silence the output of candidate rewrites */ |