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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 24 Sep 2021 05:11:24 +0000 (00:11 -0500)
committer	GitHub <noreply@github.com>
	Fri, 24 Sep 2021 05:11:24 +0000 (05:11 +0000)
commit	7179be03b049d3046140316c4c5987efbdbd09b8
tree	194f889c2b8cb6c02fcd244818add0c365de96d9	tree
parent	421803a044faf8f17ebf6d44f94adbdfdbded4a6	commit \| diff

Eliminate calls to Rewriter::rewrite from strings entailment checks (#7203)

There are a few further circular references that prevent us from not passing Rewriter to the strings TheoryRewriter constructor, this can be cleaned in future PRs.

14 files changed:

src/preprocessing/passes/foreign_theory_rewrite.cpp		diff \| blob \| history
src/preprocessing/passes/foreign_theory_rewrite.h		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.cpp		diff \| blob \| history
src/theory/strings/arith_entail.cpp		diff \| blob \| history
src/theory/strings/arith_entail.h		diff \| blob \| history
src/theory/strings/sequences_rewriter.cpp		diff \| blob \| history
src/theory/strings/sequences_rewriter.h		diff \| blob \| history
src/theory/strings/strings_entail.cpp		diff \| blob \| history
src/theory/strings/strings_entail.h		diff \| blob \| history
src/theory/strings/strings_rewriter.cpp		diff \| blob \| history
src/theory/strings/strings_rewriter.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp		diff \| blob \| history
test/unit/theory/sequences_rewriter_white.cpp		diff \| blob \| history

RSS Atom