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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Sat, 6 Mar 2021 00:17:15 +0000 (16:17 -0800)
committer	GitHub <noreply@github.com>
	Sat, 6 Mar 2021 00:17:15 +0000 (00:17 +0000)
commit	c6fffe4fd328401f7f7e0757303e8dea5f6c14a4
tree	84bbb3f44fa7ffbeba0c0baf9b7b22f036d2e9f4	tree
parent	555e4b0b6b10e9170676c0a3ef9b778322f3327f	commit \| diff

Remove SMT-LIB 2.5 and 2.0 support. (#6068)

This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.

222 files changed:

src/options/language.cpp		diff \| blob \| history
src/options/language.h		diff \| blob \| history
src/options/options_template.cpp		diff \| blob \| history
src/options/set_language.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
src/printer/printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.h		diff \| blob \| history
src/printer/tptp/tptp_printer.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/arith/bug569.smt2		diff \| blob \| history
test/regress/regress0/arith/div.01.smt2		diff \| blob \| history
test/regress/regress0/arith/div.02.smt2		diff \| blob \| history
test/regress/regress0/arith/div.04.smt2		diff \| blob \| history
test/regress/regress0/arith/div.05.smt2		diff \| blob \| history
test/regress/regress0/arith/div.07.smt2		diff \| blob \| history
test/regress/regress0/arith/integers/ackermann4.smt2		diff \| blob \| history
test/regress/regress0/arith/integers/ackermann5.smt2		diff \| blob \| history
test/regress/regress0/arith/integers/ackermann6.smt2		diff \| blob \| history
test/regress/regress0/arith/mod.01.smt2		diff \| blob \| history
test/regress/regress0/arith/mult.01.smt2		diff \| blob \| history
test/regress/regress0/arrays/arrays0.smt2		diff \| blob \| history
test/regress/regress0/arrays/arrays1.smt2		diff \| blob \| history
test/regress/regress0/arrays/arrays2.smt2		diff \| blob \| history
test/regress/regress0/arrays/arrays3.smt2		diff \| blob \| history
test/regress/regress0/arrays/arrays4.smt2		diff \| blob \| history
test/regress/regress0/aufbv/bug580.delta.smt2		diff \| blob \| history
test/regress/regress0/auflia/bug336.smt2		diff \| blob \| history
test/regress/regress0/bt-test-00.smt2		diff \| blob \| history
test/regress/regress0/bt-test-01.smt2		diff \| blob \| history
test/regress/regress0/bug365.smt2		diff \| blob \| history
test/regress/regress0/bug578.smt2		diff \| blob \| history
test/regress/regress0/buggy-ite.smt2		diff \| blob \| history
test/regress/regress0/bv/ackermann1.smt2		diff \| blob \| history
test/regress/regress0/bv/ackermann2.smt2		diff \| blob \| history
test/regress/regress0/bv/ackermann3.smt2		diff \| blob \| history
test/regress/regress0/bv/ackermann4.smt2		diff \| blob \| history
test/regress/regress0/bv/bv-options4.smt2		diff \| blob \| history
test/regress/regress0/bv/core/constant_core.smt2		diff \| blob \| history
test/regress/regress0/bv/inequality00.smt2		diff \| blob \| history
test/regress/regress0/bv/inequality01.smt2		diff \| blob \| history
test/regress/regress0/bv/inequality02.smt2		diff \| blob \| history
test/regress/regress0/bv/inequality03.smt2		diff \| blob \| history
test/regress/regress0/bv/inequality04.smt2		diff \| blob \| history
test/regress/regress0/bv/inequality05.smt2		diff \| blob \| history
test/regress/regress0/decision/quant-ex1.smt2		diff \| blob \| history
test/regress/regress0/fmf/bug652.smt2	[deleted file]	blob \| history
test/regress/regress0/fp/down-cast-RNA.smt2		diff \| blob \| history
test/regress/regress0/fp/rti_3_5_bug.smt2		diff \| blob \| history
test/regress/regress0/get-value-incremental.smt2		diff \| blob \| history
test/regress/regress0/get-value-ints.smt2		diff \| blob \| history
test/regress/regress0/get-value-reals-ints.smt2		diff \| blob \| history
test/regress/regress0/get-value-reals.smt2		diff \| blob \| history
test/regress/regress0/hung10_itesdk_output1.smt2		diff \| blob \| history
test/regress/regress0/hung13sdk_output1.smt2		diff \| blob \| history
test/regress/regress0/lang_opts_2_5.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/magnitude-wrong-1020-m.smt2		diff \| blob \| history
test/regress/regress0/nl/very-easy-sat.smt2		diff \| blob \| history
test/regress/regress0/nl/very-simple-unsat.smt2		diff \| blob \| history
test/regress/regress0/parser/as.smt2		diff \| blob \| history
test/regress/regress0/parser/strings20.smt2		diff \| blob \| history
test/regress/regress0/parser/strings25.smt2		diff \| blob \| history
test/regress/regress0/push-pop/bug691.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/bug290.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/bug291.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/ex3.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/ex6.smt2		diff \| blob \| history
test/regress/regress0/strings/bug001.smt2		diff \| blob \| history
test/regress/regress0/strings/bug002.smt2		diff \| blob \| history
test/regress/regress0/strings/escchar.smt2		diff \| blob \| history
test/regress/regress0/uflia/check01.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith4.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith5.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith6.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith7.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/array1.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvbool.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvbool2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvbool3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvcmp.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvconcat.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvconcat2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvdiv.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvext.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvite.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvmul.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvmul2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvmul3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvnot.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvsle.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvsle2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvsle3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvsle4.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvsle5.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvslt.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvslt2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvslt3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvslt4.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvslt5.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvule.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvule2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvule3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvule4.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvule5.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvult.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvult2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvult3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvult4.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvult5.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/geq.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/gt.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/leq.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/lt.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/uf1.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/xor.smt2		diff \| blob \| history
test/regress/regress1/arith/bug716.0.smt2		diff \| blob \| history
test/regress/regress1/arith/div.03.smt2		diff \| blob \| history
test/regress/regress1/arith/div.06.smt2		diff \| blob \| history
test/regress/regress1/arith/div.08.smt2		diff \| blob \| history
test/regress/regress1/arith/mod.02.smt2		diff \| blob \| history
test/regress/regress1/arith/mod.03.smt2		diff \| blob \| history
test/regress/regress1/arith/problem__003.smt2		diff \| blob \| history
test/regress/regress1/aufbv/bug580.smt2		diff \| blob \| history
test/regress/regress1/auflia/bug330.smt2		diff \| blob \| history
test/regress/regress1/bug512.smt2		diff \| blob \| history
test/regress/regress1/bug521.smt2		diff \| blob \| history
test/regress/regress1/bug590.smt2		diff \| blob \| history
test/regress/regress1/bug800.smt2		diff \| blob \| history
test/regress/regress1/bv/decision-weight00.smt2		diff \| blob \| history
test/regress/regress1/bvdiv2.smt2		diff \| blob \| history
test/regress/regress1/datatypes/issue-variant-dt-zero.smt2		diff \| blob \| history
test/regress/regress1/datatypes/issue3266-small.smt2		diff \| blob \| history
test/regress/regress1/decision/quant-Arrays_Q1-noinfer.smt2		diff \| blob \| history
test/regress/regress1/fmf/issue916-fmf-or.smt2		diff \| blob \| history
test/regress/regress1/fmf/refcount24.cvc.smt2		diff \| blob \| history
test/regress/regress1/fp/rti_3_5_bug_report.smt2		diff \| blob \| history
test/regress/regress1/gensys_brn001.smt2		diff \| blob \| history
test/regress/regress1/nl/bug698.smt2		diff \| blob \| history
test/regress/regress1/nl/metitarski-1025.smt2		diff \| blob \| history
test/regress/regress1/nl/metitarski-3-4.smt2		diff \| blob \| history
test/regress/regress1/nl/metitarski_3_4_2e.smt2		diff \| blob \| history
test/regress/regress1/nl/nl-help-unsat-quant.smt2		diff \| blob \| history
test/regress/regress1/nl/nl-unk-quant.smt2		diff \| blob \| history
test/regress/regress1/nl/poly-1025.smt2		diff \| blob \| history
test/regress/regress1/nl/quant-nl.smt2		diff \| blob \| history
test/regress/regress1/proof00.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/AdditiveMethods_OwnedResults.Mz.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/Arrays_Q1-noinfer.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/array-unsat-simp3.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/bignum_quant.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/bug802.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/bug_743.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/burns13.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/burns4.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/gauss_init_0030.fof.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/issue3316.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/issue3317.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/issue3765.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/issue993.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/javafe.ast.StmtVec.009.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/opisavailable-12.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/rew-to-0211-dd.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/ricart-agrawala6.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/set3.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/set8.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/smtlib384a03.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/smtlib46f14a.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/smtlibf957ea.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/symmetric_unsat_7.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/var-eq-trigger.smt2		diff \| blob \| history
test/regress/regress1/sets/fuzz14418.smt2		diff \| blob \| history
test/regress/regress1/sets/fuzz15201.smt2		diff \| blob \| history
test/regress/regress1/sets/fuzz31811.smt2		diff \| blob \| history
test/regress/regress1/sets/sharingbug.smt2		diff \| blob \| history
test/regress/regress1/strings/bug686dd.smt2		diff \| blob \| history
test/regress/regress1/strings/issue1105.smt2		diff \| blob \| history
test/regress/regress1/strings/issue1684-regex.smt2		diff \| blob \| history
test/regress/regress1/strings/issue3272.smt2		diff \| blob \| history
test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2		diff \| blob \| history
test/regress/regress1/strings/pierre150331.smt2		diff \| blob \| history
test/regress/regress1/uf2.smt2		diff \| blob \| history
test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2		diff \| blob \| history
test/regress/regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2		diff \| blob \| history
test/regress/regress1/uflia/simple_cyclic2.smt2		diff \| blob \| history
test/regress/regress2/DTP_k2_n35_c175_s15.smt2		diff \| blob \| history
test/regress/regress2/arith/miplib-opt1217--27.smt2		diff \| blob \| history
test/regress/regress2/bug394.smt2		diff \| blob \| history
test/regress/regress2/bug812.smt2		diff \| blob \| history
test/regress/regress2/hash_sat_06_19.smt2		diff \| blob \| history
test/regress/regress2/hash_sat_07_17.smt2		diff \| blob \| history
test/regress/regress2/hash_sat_09_09.smt2		diff \| blob \| history
test/regress/regress2/hash_sat_10_09.smt2		diff \| blob \| history
test/regress/regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2		diff \| blob \| history
test/regress/regress2/javafe.ast.WhileStmt.447_no_forall.smt2		diff \| blob \| history
test/regress/regress2/nl/nt-lemmas-bad.smt2		diff \| blob \| history
test/regress/regress2/ooo.rf6.smt2		diff \| blob \| history
test/regress/regress2/ooo.tag10.smt2		diff \| blob \| history
test/regress/regress2/piVC_5581bd.smt2		diff \| blob \| history
test/regress/regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2		diff \| blob \| history
test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2		diff \| blob \| history
test/regress/regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2		diff \| blob \| history
test/regress/regress2/quantifiers/javafe.ast.WhileStmt.447.smt2		diff \| blob \| history
test/regress/regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2		diff \| blob \| history
test/regress/regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2		diff \| blob \| history
test/regress/regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2		diff \| blob \| history
test/regress/regress2/strings/cmu-dis-0707-3.smt2		diff \| blob \| history
test/regress/regress2/strings/issue918.smt2		diff \| blob \| history
test/regress/regress3/arith_prp-13-24.smt2		diff \| blob \| history
test/regress/regress3/lpsat-goal-9.smt2		diff \| blob \| history
test/regress/regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2		diff \| blob \| history
test/regress/regress4/bug337.smt2		diff \| blob \| history
test/regress/regress4/bug396.smt2		diff \| blob \| history
test/regress/regress4/miplib-pp08a-3000.smt2		diff \| blob \| history
test/regress/regress4/xs-11-20-5-2-5-3.smt2		diff \| blob \| history

RSS Atom