diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 19:58:37 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-11 17:15:59 -0400 |
| commit | e80b93ca958bdbeb28959029868f6193b39a3f19 (patch) | |
| tree | 92218adf47348cb8011a41599e158b371f5659de /test/regress/regress0/tptp/Makefile.am | |
| parent | b76afedab3a23525da478ba4a8687c882793ea81 (diff) | |
Support for TPTP's TFF0 (with arithmetic)
This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).
This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made. These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.
Diffstat (limited to 'test/regress/regress0/tptp/Makefile.am')
| -rw-r--r-- | test/regress/regress0/tptp/Makefile.am | 79 |
1 files changed, 79 insertions, 0 deletions
diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am new file mode 100644 index 000000000..130a9dc7c --- /dev/null +++ b/test/regress/regress0/tptp/Makefile.am @@ -0,0 +1,79 @@ +BINARY = cvc4 +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +# escape the `=' in file names +equals = = + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + tptp_parser.p \ + tptp_parser2.p \ + tptp_parser3.p \ + tptp_parser4.p \ + tptp_parser5.p \ + tptp_parser6.p \ + tptp_parser7.p \ + tptp_parser8.p \ + tptp_parser9.p \ + tptp_parser10.p \ + tff0.p \ + tff0-arith.p \ + ARI086$(equals)1.p \ + BOO003-4.p \ + DAT001$(equals)1.p \ + KRS018+1.p \ + KRS063+1.p \ + MGT019+2.p \ + MGT041-2.p \ + PUZ131_1.p \ + SYN000+1.p \ + SYN000+2.p \ + SYN000-1.p \ + SYN000-2.p \ + SYN000$(equals)2.p \ + SYN000_1.p \ + SYN000_2.p \ + SYN075-1.p + +# axiom files required for the above tests +TEST_DEPS_DIST = \ + Axioms/BOO004-0.ax \ + Axioms/SYN000_0.ax \ + Axioms/SYN000-0.ax \ + Axioms/SYN000+0.ax + +# these take too long at present +EXTRA_DIST = $(TESTS) \ + $(TEST_DEPS_DIST) \ + BOO027-1.p \ + MGT031-1.p \ + NLP114-1.p \ + SYN075+1.p + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: |