Use the proper evaluator for optimized SyGuS datatype rewriting (#7266)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 1 Oct 2021 04:49:08 +0000 (23:49 -0500)
committerGitHub <noreply@github.com>
Fri, 1 Oct 2021 04:49:08 +0000 (04:49 +0000)
commitbb0e6dcde2e7267e391a46b868b990d7cb7e42bd
tree5445dfc53c9310ca2a445d4d78ad0ea128fe4a55
parent19f223e580b527bc17add2ea4e61e85df2977c87
Use the proper evaluator for optimized SyGuS datatype rewriting (#7266)

This updates the datatypes rewriter to use the evaluator from Env instead of creating local copies of Evaluator. This makes all uses of the Evaluator dependent on the proper options (e.g. which will be based later on the cardinality of the alphabet for strings).

This moves one utility method (sygusToBuiltinEval) to the datatypes rewriter, as it uses an Evaluator that will be dependent on options.

Notice that this is another instance where it is important for us to make the cache for the rewriter local. The same issue occurs for other places where rewriting is dependent on options. This issue will be revisited when the option for strings alphabet cardinality is added.
src/smt/env.cpp
src/smt/env.h
src/theory/datatypes/datatypes_rewriter.cpp
src/theory/datatypes/datatypes_rewriter.h
src/theory/datatypes/sygus_datatype_utils.cpp
src/theory/datatypes/sygus_datatype_utils.h
src/theory/datatypes/theory_datatypes.cpp