dos2unix on the proof signatures, and fix the makefile.

diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am
index 610990ba28d48fbe6ec2eed6e7a020ce138e30de..42ba4826233f317dab20b90d3754f3ed6c72f0e7 100644 (file)
--- a/proofs/signatures/Makefile.am
+++ b/proofs/signatures/Makefile.am
@@ -3,7 +3,7 @@
 # add support for more theories, just list them here in the same order
 # you would to the LFSC proof-checker binary.
 #
-CORE_PLFS = sat.plf smt.plf th_base.plf
+CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf
 
 noinst_LTLIBRARIES = libsignatures.la
 
@@ -31,4 +31,7 @@ signatures.cpp: $(CORE_PLFS)
        ) > $@
 
 EXTRA_DIST = \
-       example.plf
+       example.plf \
+       example-arrays.plf \
+       example-quant.plf \
+       th_quant.plf

diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf
index edb6dc96ee069641f05dfee44406c9a42c1f27e3..0c6b16048eff63a9b5197b82d05bf9ce9cc64003 100755 (executable)
--- a/proofs/signatures/th_arrays.plf
+++ b/proofs/signatures/th_arrays.plf
@@ -1,52 +1,51 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
-;\r
-; Theory of Arrays\r
-;\r
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
-; depdends on : th_base.plf\r
-\r
-; sorts\r
-\r
-(declare array (! s1 sort (! s2 sort sort)))   ; s1 is index, s2 is element\r
-\r
-; functions\r
-(declare write (! s1 sort\r
-               (! s2 sort\r
-                 (term (arrow (array s1 s2) \r
-                       (arrow s1 \r
-                       (arrow s2 (array s1 s2))))))))\r
-                 \r
-(declare read (! s1 sort\r
-              (! s2 sort\r
-               (term (arrow (array s1 s2)\r
-                             (arrow s1 s2))))))\r
-                \r
-; inference rules\r
-(declare row1 (! s1 sort\r
-              (! s2 sort\r
-              (! t1 (term (array s1 s2))\r
-              (! t2 (term s1)\r
-              (! t3 (term s2)\r
-               (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2) \r
-                              t3))))))))\r
-               \r
-\r
-(declare row (! s1 sort\r
-             (! s2 sort\r
-             (! t2 (term s1)\r
-             (! t3 (term s1)\r
-             (! t1 (term (array s1 s2))\r
-             (! t4 (term s2)\r
-             (! u (th_holds (not (= _ t2 t3)))\r
-               (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3) \r
-                                     (apply _ _ (apply _ _ (read s1 s2) t1) t3)))))))))))\r
-\r
-(declare ext (! s1 sort\r
-             (! s2 sort\r
-             (! t1 (term (array s1 s2))\r
-             (! t2 (term (array s1 s2))\r
-             (! u1 (! k (term s1)\r
-                   (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k)))))\r
-                     (holds cln)))\r
-               (holds cln)))))))\r
-               
\ No newline at end of file
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Theory of Arrays
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; depdends on : th_base.plf
+
+; sorts
+
+(declare array (! s1 sort (! s2 sort sort)))   ; s1 is index, s2 is element
+
+; functions
+(declare write (! s1 sort
+               (! s2 sort
+                 (term (arrow (array s1 s2)
+                       (arrow s1
+                       (arrow s2 (array s1 s2))))))))
+
+(declare read (! s1 sort
+              (! s2 sort
+               (term (arrow (array s1 s2)
+                             (arrow s1 s2))))))
+
+; inference rules
+(declare row1 (! s1 sort
+              (! s2 sort
+              (! t1 (term (array s1 s2))
+              (! t2 (term s1)
+              (! t3 (term s2)
+               (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2)
+                              t3))))))))
+               
+
+(declare row (! s1 sort
+             (! s2 sort
+             (! t2 (term s1)
+             (! t3 (term s1)
+             (! t1 (term (array s1 s2))
+             (! t4 (term s2)
+             (! u (th_holds (not (= _ t2 t3)))
+               (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3)
+                                     (apply _ _ (apply _ _ (read s1 s2) t1) t3)))))))))))
+
+(declare ext (! s1 sort
+             (! s2 sort
+             (! t1 (term (array s1 s2))
+             (! t2 (term (array s1 s2))
+             (! u1 (! k (term s1)
+                   (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k)))))
+                     (holds cln)))
+               (holds cln)))))))

diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf
index 98b53e43d21e6439091113c5fbb935e9202a3d3d..d85b2115ca18c9090f7cffb65df8ea4c1d8b6ccf 100755 (executable)
--- a/proofs/signatures/th_quant.plf
+++ b/proofs/signatures/th_quant.plf
@@ -1,82 +1,82 @@
-(declare forall (! s sort\r
-                (! t (term s)\r
-                (! f formula\r
-                  formula))))\r
-\r
-(program eqterm ((n1 term) (n2 term)) bool\r
-    (do (markvar n1)\r
-        (let s (ifmarked n2 tt ff)\r
-           (do (markvar n1) s))))\r
-\r
-(program is_inst_t ((ti term) (t term) (k term)) bool\r
-  (match t\r
-    ((apply s1 s2 t1 t2) \r
-      (match ti\r
-        ((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))\r
-        (default ff)))\r
-    (default \r
-      (match ti\r
-        ((apply si1 si2 ti1 ti2) ff)\r
-        (default (eqterm ti (ifmarked t k t)))))))\r
-\r
-(program is_inst_f ((fi formula) (f formula) (k term)) bool\r
-  (match f \r
-    ((and f1 f2) (match fi\r
-                  ((and fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))\r
-                  (default ff)))\r
-    ((or f1 f2) (match fi\r
-                  ((or fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))\r
-                  (default ff)))\r
-    ((impl f1 f2) (match fi\r
-                  ((impl fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))\r
-                  (default ff)))\r
-    ((not f1) (match fi\r
-                  ((not fi1) (is_inst_f fi1 f1 k))\r
-                  (default ff)))\r
-    ((iff f1 f2) (match fi\r
-                  ((iff fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))\r
-                  (default ff)))\r
-    ((xor f1 f2) (match fi\r
-                  ((xor fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))\r
-                  (default ff)))\r
-    ((ifte f1 f2 f3) (match fi\r
-                      ((ifte fi1 fi2 fi3) (match (is_inst_f fi1 f1 k) \r
-                                            (tt (match (is_inst_f fi2 f2 k) (tt (is_inst_f fi3 f3 k)) (ff ff))) \r
-                                            (ff ff)))\r
-                      (default ff)))\r
-    ((= s t1 t2) (match fi\r
-                  ((= s ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))\r
-                  (default ff)))\r
-    ((forall s t1 f1) (match fi\r
-                     ((forall s ti1 fi1) (is_inst_f fi1 f1 k))\r
-                     (default ff)))\r
-    (default ff)))\r
-\r
-(program is_inst ((fi formula) (f formula) (t term) (k term)) bool\r
-  (do (markvar t) \r
-     (let f1 (is_inst_f fi f k)\r
-        (do (markvar t) f1))))\r
-\r
-(declare skolem\r
-  (! s sort\r
-  (! t (term s)\r
-  (! f formula\r
-  (! p (th_holds (not (forall s t f)))\r
-  (! u (! k (term s)\r
-       (! fi formula\r
-       (! p1 (th_holds (not fi))\r
-       (! r (^ (is_inst fi f t k) tt)\r
-         (holds cln)))))\r
-    (holds cln)))))))\r
-    \r
-(declare inst\r
-  (! s sort\r
-  (! t (term s)\r
-  (! f formula\r
-  (! k (term s)\r
-  (! fi formula\r
-  (! p (th_holds (forall s t f))\r
-  (! r (^ (is_inst fi f t k) tt)\r
-  (! u (! p1 (th_holds fi)\r
-            (holds cln))\r
-    (holds cln))))))))))
\ No newline at end of file
+(declare forall (! s sort
+                (! t (term s)
+                (! f formula
+                  formula))))
+
+(program eqterm ((n1 term) (n2 term)) bool
+    (do (markvar n1)
+        (let s (ifmarked n2 tt ff)
+           (do (markvar n1) s))))
+
+(program is_inst_t ((ti term) (t term) (k term)) bool
+  (match t
+    ((apply s1 s2 t1 t2)
+      (match ti
+        ((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
+        (default ff)))
+    (default
+      (match ti
+        ((apply si1 si2 ti1 ti2) ff)
+        (default (eqterm ti (ifmarked t k t)))))))
+
+(program is_inst_f ((fi formula) (f formula) (k term)) bool
+  (match f
+    ((and f1 f2) (match fi
+                  ((and fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
+                  (default ff)))
+    ((or f1 f2) (match fi
+                  ((or fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
+                  (default ff)))
+    ((impl f1 f2) (match fi
+                  ((impl fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
+                  (default ff)))
+    ((not f1) (match fi
+                  ((not fi1) (is_inst_f fi1 f1 k))
+                  (default ff)))
+    ((iff f1 f2) (match fi
+                  ((iff fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
+                  (default ff)))
+    ((xor f1 f2) (match fi
+                  ((xor fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
+                  (default ff)))
+    ((ifte f1 f2 f3) (match fi
+                      ((ifte fi1 fi2 fi3) (match (is_inst_f fi1 f1 k)
+                                            (tt (match (is_inst_f fi2 f2 k) (tt (is_inst_f fi3 f3 k)) (ff ff)))
+                                            (ff ff)))
+                      (default ff)))
+    ((= s t1 t2) (match fi
+                  ((= s ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
+                  (default ff)))
+    ((forall s t1 f1) (match fi
+                     ((forall s ti1 fi1) (is_inst_f fi1 f1 k))
+                     (default ff)))
+    (default ff)))
+
+(program is_inst ((fi formula) (f formula) (t term) (k term)) bool
+  (do (markvar t)
+     (let f1 (is_inst_f fi f k)
+        (do (markvar t) f1))))
+
+(declare skolem
+  (! s sort
+  (! t (term s)
+  (! f formula
+  (! p (th_holds (not (forall s t f)))
+  (! u (! k (term s)
+       (! fi formula
+       (! p1 (th_holds (not fi))
+       (! r (^ (is_inst fi f t k) tt)
+         (holds cln)))))
+    (holds cln)))))))
+
+(declare inst
+  (! s sort
+  (! t (term s)
+  (! f formula
+  (! k (term s)
+  (! fi formula
+  (! p (th_holds (forall s t f))
+  (! r (^ (is_inst fi f t k) tt)
+  (! u (! p1 (th_holds fi)
+            (holds cln))
+    (holds cln))))))))))