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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 24 Nov 2017 02:07:19 +0000 (20:07 -0600)
committer	GitHub <noreply@github.com>
	Fri, 24 Nov 2017 02:07:19 +0000 (20:07 -0600)
commit	612509379a1417f8d4a5e001ff143ba819f5516f
tree	764c379a42fa29ec36d9c83d448901c975e2fa29	tree
parent	c9ae6b9812e737ae7932df91fa5f334d6d2588d4	commit \| diff

Ho parsing and regressions (#1350)

34 files changed:

src/parser/parser.cpp		diff \| blob \| history
src/parser/parser.h		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
test/Makefile.am		diff \| blob \| history
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/ho/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress0/ho/apply-collapse-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/apply-collapse-unsat.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/auth0068.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/cong-full-apply.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/cong.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/declare-fun-variants.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/def-fun-flatten.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/ext-finite-unsat.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/ext-ho.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/ext-sat-partial-eval.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/ext-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/fta0409.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/ho-exponential-model.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/ho-matching-enum-2.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/ho-matching-enum.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/ho-matching-nested-app.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/ho-std-fmf.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/hoa0102.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/ite-apply-eq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/lambda-equality-non-canon.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/modulo-func-equality.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/simple-matching-partial.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/simple-matching.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ho/trans.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rec-fun-const-parse-bug.smt2	[new file with mode: 0644]	blob

RSS Atom