projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 79af28a) | patch
Parsing THF and adding several regressions (#3131)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Wed, 31 Jul 2019 17:17:29 +0000 (12:17 -0500)
committerGitHub <noreply@github.com>
Wed, 31 Jul 2019 17:17:29 +0000 (12:17 -0500)
commit7537ff075dbb2d814d722d2d72586ce78235467c
tree4adca4f03007da65ddfc2a313f6ecfaf9477626ctree
parent79af28acb3bdd16d18f325c7a4fab36604232ab0commit | diff
Parsing THF and adding several regressions (#3131)
38 files changed:
src/options/options.h diff | blob | history
src/parser/parser.cpp diff | blob | history
src/parser/tptp/Tptp.g diff | blob | history
src/parser/tptp/tptp.cpp diff | blob | history
src/parser/tptp/tptp.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p [new file with mode: 0644] blob
test/regress/regress0/ho/fta0210.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-std-fmf.smt2 [new file with mode: 0644] blob
test/regress/regress0/ho/hoa0008.smt2 [new file with mode: 0644] blob
test/regress/regress0/ho/match-middle.smt2 [new file with mode: 0644] blob
test/regress/regress1/ho/NUM638^1.smt2 [new file with mode: 0644] blob
test/regress/regress1/ho/NUM925^1.p [new file with mode: 0644] blob
test/regress/regress1/ho/SYO056^1.p [new file with mode: 0644] blob
test/regress/regress1/ho/auth0068.smt2 [deleted file] blob | history
test/regress/regress1/ho/bound_var_bug.p [new file with mode: 0644] blob
test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p [new file with mode: 0644] blob
test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 [new file with mode: 0644] blob
test/regress/regress1/ho/fta0210.smt2 [deleted file] blob | history
test/regress/regress1/ho/fta0328.lfho.p [new file with mode: 0644] blob
test/regress/regress1/ho/fta0409.smt2 [deleted file] blob | history
test/regress/regress1/ho/ho-exponential-model.smt2 [deleted file] blob | history
test/regress/regress1/ho/ho-matching-enum-2.smt2 [deleted file] blob | history
test/regress/regress1/ho/ho-std-fmf.smt2 [deleted file] blob | history
test/regress/regress1/ho/hoa0008.smt2 [deleted file] blob | history
test/regress/regress1/ho/match-middle.smt2 [deleted file] blob | history
test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 [new file with mode: 0644] blob
test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 [new file with mode: 0644] blob
test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p [new file with mode: 0644] blob
test/regress/regress1/ho/store-ax-min.p [new file with mode: 0644] blob
test/regress/regress2/ho/SYO362^5.p [new file with mode: 0644] blob
test/regress/regress2/ho/auth0068.smt2 [new file with mode: 0644] blob
test/regress/regress2/ho/bug_instfalse_SEU882^5.p [new file with mode: 0644] blob
test/regress/regress2/ho/fta0409.smt2 [new file with mode: 0644] blob
test/regress/regress2/ho/involved_parsing_ALG248^3.p [new file with mode: 0644] blob
test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p [new file with mode: 0644] blob