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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 7 Jan 2020 17:39:27 +0000 (11:39 -0600)
committer	GitHub <noreply@github.com>
	Tue, 7 Jan 2020 17:39:27 +0000 (11:39 -0600)
commit	53dc40ec71344d6cc8df9f009cbbba4dbefccb64
tree	c005676b3c59786652b3f816fe02b42f892316b9	tree
parent	e3e6f0dc62f0bb9d3fb8d752c5eb4600872fd806	commit \| diff

Update any-constant and normalization policies for sygus grammars (#3583)

src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.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
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/sygus/coeff-solve-inv.sy		diff \| blob \| history
test/regress/regress1/sygus/issue3580.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/ex23.sy		diff \| blob \| history