Remove deprecated SyGuS method evaluateWithUnfolding (#7155)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 9 Sep 2021 01:16:11 +0000 (20:16 -0500)
committerGitHub <noreply@github.com>
Thu, 9 Sep 2021 01:16:11 +0000 (20:16 -0500)
commit704fd545440023a0deaa328a9de9c11ac5fe963c
tree17b2466d420b958071cac579fe0353c12961b3af
parentb9dcd4d141cef256b4371aa103af4ee1aa7c61bd
Remove deprecated SyGuS method evaluateWithUnfolding (#7155)

This was a predecessor to the evaluator and TermDbSygus::rewriteNode that is no longer necessary.

This refactors the code so that evaluateWithUnfolding is replaced by rewriteNode as necessary throughout the SyGuS solver.

Note that in a few places, the extended rewriter was being used where TermDbSygus::rewriteNode (which also evaluates recursive function definitions) should have been used.
src/theory/quantifiers/sygus/cegis.cpp
src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
src/theory/quantifiers/sygus/sygus_eval_unfold.h
src/theory/quantifiers/sygus/sygus_invariance.cpp
src/theory/quantifiers/sygus/sygus_invariance.h
src/theory/quantifiers/sygus/sygus_repair_const.cpp
src/theory/quantifiers/sygus/sygus_unif_strat.cpp
src/theory/quantifiers/sygus/term_database_sygus.cpp
src/theory/quantifiers/sygus/term_database_sygus.h