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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 14 Feb 2020 23:09:59 +0000 (17:09 -0600)
committer	GitHub <noreply@github.com>
	Fri, 14 Feb 2020 23:09:59 +0000 (17:09 -0600)
commit	528e801343c692b0ce8123f8754e069e6523f5dc
tree	517c86381e7a0535c376d244c830365d04e3aa62	tree
parent	08289dd911aff28110baf0fd815fd912f8b76fd3	commit \| diff

Remove quantifiers rewrite rules infrastructure (#3754)

56 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/api/cvc4cppkind.h		diff \| blob \| history
src/bindings/java/CMakeLists.txt		diff \| blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/smt2/smt2.h		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/quantifiers/kinds		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.h		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.cpp	[deleted file]	blob \| history
src/theory/quantifiers/rewrite_engine.h	[deleted file]	blob \| history
src/theory/quantifiers/theory_quantifiers_type_rules.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/term_registration_visitor.cpp		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/rewriterules/datatypes.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/datatypes_clark.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_n.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_n_lemma.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_trick.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_trick2.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/native_arrays.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/native_datatypes.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/relation.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/simulate_rewriting.smt2	[deleted file]	blob \| history
test/regress/regress1/push-pop/bug326.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/datatypes2.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/datatypes3.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/datatypes_sat.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_gen.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_gen_010.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_gen_010_lemma.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_gen_020.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_gen_020_sat.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_gen_040.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_gen_040_lemma.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_gen_080.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_gen_160_lemma.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_gen_inv_160.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_trick3.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/length_trick3_int.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/read5.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/test_guards.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2	[deleted file]	blob \| history

RSS Atom