summaryrefslogtreecommitdiff
path: root/test/regress/regress0
diff options
context:
space:
mode:
authorFrançois Bobot <francois@bobot.eu>2012-06-22 15:11:37 +0000
committerFrançois Bobot <francois@bobot.eu>2012-06-22 15:11:37 +0000
commit84c4269f3b9edb8de4134fe464dfc70679da2bb1 (patch)
treeb0c8f33e04d925064ffa9d85f1caeb6a3ff745b2 /test/regress/regress0
parenteda7d4df5481030d4e9cb6ef4a33d52afc8f7e0a (diff)
TPTP: add parser for cnf and fof
- include directive works - no keyword : 'fof', 'cnf', ... can be used for symbols name - real -> unsorted -> real (for the one that appear, so no bijection bitween real and unsorted) - same thing for string But: - string not distinct by projection to real, not sure if the current state of string theory make them distinct - filtering in include is not done - the result is not printed in the TPTP way (currently SMT2 way)
Diffstat (limited to 'test/regress/regress0')
-rw-r--r--test/regress/regress0/Makefile.am15
-rw-r--r--test/regress/regress0/tptp_parser.p17
-rw-r--r--test/regress/regress0/tptp_parser10.p10
-rw-r--r--test/regress/regress0/tptp_parser2.p14
-rw-r--r--test/regress/regress0/tptp_parser3.p14
-rw-r--r--test/regress/regress0/tptp_parser4.p14
-rw-r--r--test/regress/regress0/tptp_parser5.p16
-rw-r--r--test/regress/regress0/tptp_parser6.p16
-rw-r--r--test/regress/regress0/tptp_parser7.p16
-rw-r--r--test/regress/regress0/tptp_parser8.p11
-rw-r--r--test/regress/regress0/tptp_parser9.p14
11 files changed, 156 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index a1d960079..5eda230c3 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -85,6 +85,19 @@ CVC_TESTS = \
wiki.21.cvc \
simplification_bug3.cvc
+# Regression tests for TPTP inputs
+TPTP_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
+
# Regression tests derived from bug reports
BUG_TESTS = \
bug32.cvc \
@@ -104,7 +117,7 @@ BUG_TESTS = \
bug310.cvc \
bug339.smt2
-TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
+TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
EXTRA_DIST = $(TESTS) \
simplification_bug4.smt2.expect
diff --git a/test/regress/regress0/tptp_parser.p b/test/regress/regress0/tptp_parser.p
new file mode 100644
index 000000000..0be0adbbf
--- /dev/null
+++ b/test/regress/regress0/tptp_parser.p
@@ -0,0 +1,17 @@
+% EXPECT: unsat
+% EXIT: 20
+
+%--------------------------------------------------------------------------
+
+/*
+cnf(query_1,axiom,
+ $false | $false /* | $false).
+*/
+
+cnf(query_1,axiom,
+ $false | $false | $false).
+
+cnf(query_1,negated_conjecture, ~
+ $false | $false | $false).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser10.p b/test/regress/regress0/tptp_parser10.p
new file mode 100644
index 000000000..90db619e7
--- /dev/null
+++ b/test/regress/regress0/tptp_parser10.p
@@ -0,0 +1,10 @@
+% EXPECT: unsat
+% EXIT: 20
+
+%--------------------------------------------------------------------------
+
+fof(query_1,axiom, ![A,B]: (A != B => e(A) != e(B)) ).
+
+fof(query_1,conjecture, e(1.6) != e(1) ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser2.p b/test/regress/regress0/tptp_parser2.p
new file mode 100644
index 000000000..83a5f7b83
--- /dev/null
+++ b/test/regress/regress0/tptp_parser2.p
@@ -0,0 +1,14 @@
+% EXPECT: unsat
+% EXIT: 20
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, a | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~a | ~ 'c' ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser3.p b/test/regress/regress0/tptp_parser3.p
new file mode 100644
index 000000000..3677e6ffe
--- /dev/null
+++ b/test/regress/regress0/tptp_parser3.p
@@ -0,0 +1,14 @@
+% EXPECT: unsat
+% EXIT: 20
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( a, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(a, d) | ~ 'c' ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser4.p b/test/regress/regress0/tptp_parser4.p
new file mode 100644
index 000000000..6c5bd29da
--- /dev/null
+++ b/test/regress/regress0/tptp_parser4.p
@@ -0,0 +1,14 @@
+% EXPECT: unsat
+% EXIT: 20
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(A, d) | ~ 'c' ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser5.p b/test/regress/regress0/tptp_parser5.p
new file mode 100644
index 000000000..faacfdccc
--- /dev/null
+++ b/test/regress/regress0/tptp_parser5.p
@@ -0,0 +1,16 @@
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(A, e) | ~ 'c' ).
+
+cnf(query_1,axiom, e != d ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser6.p b/test/regress/regress0/tptp_parser6.p
new file mode 100644
index 000000000..0684a6a3d
--- /dev/null
+++ b/test/regress/regress0/tptp_parser6.p
@@ -0,0 +1,16 @@
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | cnf ).
+
+cnf(query_1,axiom, cnf | c ).
+
+cnf(query_1,axiom, ~p(A, axiom) | ~ 'c' ).
+
+cnf(query_1,axiom, axiom != d ).
+
+cnf(query_1,negated_conjecture, ~ cnf ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser7.p b/test/regress/regress0/tptp_parser7.p
new file mode 100644
index 000000000..ec90157e7
--- /dev/null
+++ b/test/regress/regress0/tptp_parser7.p
@@ -0,0 +1,16 @@
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(A, axiom) ).
+
+cnf(query_1,axiom, axiom != d ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser8.p b/test/regress/regress0/tptp_parser8.p
new file mode 100644
index 000000000..3bfd8efb6
--- /dev/null
+++ b/test/regress/regress0/tptp_parser8.p
@@ -0,0 +1,11 @@
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0
+
+%--------------------------------------------------------------------------
+include('tptp_parser7.p').
+
+cnf(query_1,axiom, include('A') | b ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser9.p b/test/regress/regress0/tptp_parser9.p
new file mode 100644
index 000000000..dab8065b5
--- /dev/null
+++ b/test/regress/regress0/tptp_parser9.p
@@ -0,0 +1,14 @@
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0
+
+%--------------------------------------------------------------------------
+
+fof(query_1,axiom, include(1) ).
+
+fof(query_1,axiom, ![E]: e(E,1.6) ).
+
+fof(query_1,axiom, ![A,E]: ~e(A,3.0E3) ).
+
+fof(query_1,conjecture, ![E]: e(E,2.6) ).
+
+%--------------------------------------------------------------------------
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback