git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 22 Sep 2021 20:05:44 +0000 (15:05 -0500)
committer	GitHub <noreply@github.com>
	Wed, 22 Sep 2021 20:05:44 +0000 (20:05 +0000)
commit	ba259d66be877de3cc77e4f62083905ace942c82
tree	864bd79d72e52516bd9427a9f3d6907843f14b01	tree
parent	f9fd2f7a1e37540c0ac6a9ef33f9da91f69a8368	commit \| diff

Towards standard usage of evaluator (#7189)

This makes the evaluator accessible via EnvObj through the Rewriter. It furthermore removes Rewriter::rewrite from inside the evaluator itself.

Construction of Evaluator utilities is now discouraged.

The include dependencies were cleaned slightly in this PR, leading to more precise includes throughout.

This is work towards having a configurable cardinality for strings, as well as eliminating SmtEngineScope.

44 files changed:

src/smt/env.cpp		diff \| blob \| history
src/smt/env.h		diff \| blob \| history
src/smt/env_obj.cpp		diff \| blob \| history
src/smt/env_obj.h		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
src/theory/builtin/proof_checker.cpp		diff \| blob \| history
src/theory/datatypes/sygus_datatype_utils.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.h		diff \| blob \| history
src/theory/datatypes/sygus_simple_sym.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/evaluator.cpp		diff \| blob \| history
src/theory/evaluator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner_manager.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_evaluator.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_evaluator.h		diff \| blob \| history
src/theory/quantifiers/quant_bound_inference.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/solution_filter.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_value_manager.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_type_info.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.h		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.h		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/rewriter_tables_template.h		diff \| blob \| history
test/unit/theory/evaluator_white.cpp		diff \| blob \| history

RSS Atom