From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 13 Mar 2014 17:00:07 +0000 (-0400)
Subject: dos2unix on the proof signatures, and fix the makefile.
X-Git-Tag: cvc5-1.0.0~7017
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f0407e1c718050daf021c937708d779bdcc3b191;p=cvc5.git

dos2unix on the proof signatures, and fix the makefile.
---

diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am
index 610990ba2..42ba48262 100644
--- 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 edb6dc96e..0c6b16048 100755
--- a/proofs/signatures/th_arrays.plf
+++ b/proofs/signatures/th_arrays.plf
@@ -1,52 +1,51 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; 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)))))))
-               
\ 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 98b53e43d..d85b2115c 100755
--- a/proofs/signatures/th_quant.plf
+++ b/proofs/signatures/th_quant.plf
@@ -1,82 +1,82 @@
-(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))))))))))
\ 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))))))))))