Fix parantheses in clause args

althelf/rules.smt3

@@ -26,7 +26,7 @@
     )
 )
 (declare-rule not_not ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_not_not CL) true)
   :conclusion CL
 )
@@ -42,7 +42,7 @@
 ;TRUST
 (declare-rule th_resolution ((Cs Bool) (CL Bool))
   :premise-list Cs and
-  :args ((CL))
+  :args (CL)
   :requires ((check_resolution Cs CL) true)
   :conclusion CL
 )
@@ -50,7 +50,7 @@
 ;TRUST
 (declare-rule resolution ((Cs Bool) (CL Bool))
   :premise-list Cs and
-  :args ((CL))
+  :args (CL)
   :requires ((check_resolution Cs CL) true)
   :conclusion CL
 )
@@ -82,7 +82,7 @@
 ;TRUST
 (declare-rule contraction ((CL1 Bool) (CL Bool))
   :premises (CL1)
-  :args ((CL))
+  :args (CL)
   :requires ((check_contraction CL1 CL) true)
   :conclusion CL
 )
@@ -105,7 +105,7 @@
 ;TRUST
 (declare-rule la_generic ((CL Bool) (coeffs Real :int))
   :args (coeffs)
-  :args ((CL))
+  :args (CL)
   :requires ((check_la_generic coeffs CL) true)
   :conclusion CL
 )
@@ -120,7 +120,7 @@
 
 ;TRUST
 (declare-rule lia_generic ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_lia_generic CL) true)
   :conclusion CL
 )
@@ -145,7 +145,7 @@
 
 ;TRUST
 (declare-rule la_tautology ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_la_tautology CL) true)
   :conclusion CL
 )
@@ -270,7 +270,7 @@
 
 ;TRUST
 (declare-rule eq_transitive ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_eq_transitive CL) true)
   :conclusion CL
 )
@@ -285,7 +285,7 @@
 
 ;TRUST
 (declare-rule eq_congruent ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_eq_congruent CL) true)
   :conclusion CL
 )
@@ -300,7 +300,7 @@
 
 ;TRUST
 (declare-rule eq_congruent_pred ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_eq_congruent_pred CL) true)
   :conclusion CL
 )
@@ -373,7 +373,7 @@
 ;TODO implement transform_not_and
 (declare-rule not_and ((CL Bool) (C Bool) (CN Bool :list))
   :premises ((cl (not (and C CN))))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (transform_not_and (and C CN)) CL) true)
   :conclusion CL
 )
@@ -381,7 +381,7 @@
 ;TRUST
 (declare-rule xor1 ((CL Bool) (phi1 Bool) (phi2 Bool))
   :premises ((cl (xor phi1 phi2)))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl phi1 phi2) CL) true)
   :conclusion CL
 )
@@ -389,7 +389,7 @@
 ;TRUST
 (declare-rule xor2 ((CL Bool) (phi1 Bool) (phi2 Bool))
   :premises ((cl (xor phi1 phi2)))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl (not phi1) (not phi2)) CL) true)
   :conclusion CL
 )
@@ -397,7 +397,7 @@
 ;TRUST
 (declare-rule not_xor1 ((CL Bool) (phi1 Bool) (phi2 Bool))
   :premises ((cl (not (xor phi1 phi2))))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl phi1 (not phi2)) CL) true)
   :conclusion CL
 )
@@ -405,7 +405,7 @@
 ;TRUST
 (declare-rule not_xor2 ((CL Bool) (phi1 Bool) (phi2 Bool))
   :premises ((cl (not (xor phi1 phi2))))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl (not phi1) phi2) CL) true)
   :conclusion CL
 )
@@ -413,7 +413,7 @@
 ;TRUST
 (declare-rule implies ((CL Bool) (phi1 Bool) (phi2 Bool))
   :premises ((cl (=> phi1 phi2)))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl (not phi1) phi2) CL) true)
   :conclusion CL
 )
@@ -433,7 +433,7 @@
 ;TRUST
 (declare-rule equiv1 ((CL Bool) (phi1 Bool) (phi2 Bool))
   :premises ((cl (= phi1 phi2)))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl (not phi1) phi2) CL) true)
   :conclusion CL
 )
@@ -441,7 +441,7 @@
 ;TRUST
 (declare-rule equiv2 ((CL Bool) (phi1 Bool) (phi2 Bool))
   :premises ((cl (= phi1 phi2)))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl phi1 (not phi2)) CL) true)
   :conclusion CL
 )
@@ -449,7 +449,7 @@
 ;TRUST
 (declare-rule not_equiv1 ((CL Bool) (phi1 Bool) (phi2 Bool))
   :premises ((cl (not (= phi1 phi2))))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl phi1 phi2) CL) true)
   :conclusion CL
 )
@@ -457,7 +457,7 @@
 ;TRUST
 (declare-rule not_equiv1 ((CL Bool) (phi1 Bool) (phi2 Bool))
   :premises ((cl (not (= phi1 phi2))))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl (not phi1) (not phi2)) CL) true)
   :conclusion CL
 )
@@ -472,7 +472,7 @@
 
 ;TRUST
 (declare-rule and_pos ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_and_pos CL) true)
   :conclusion CL
 )
@@ -487,7 +487,7 @@
 
 ;TRUST
 (declare-rule and_neg ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_and_neg CL) true)
   :conclusion CL
 )
@@ -502,7 +502,7 @@
 
 ;TRUST
 (declare-rule or_pos ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_or_pos CL) true)
   :conclusion CL
 )
@@ -517,140 +517,140 @@
 
 ;TRUST
 (declare-rule or_neg ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_or_neg CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule xor_pos1 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_xor_pos1 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule xor_pos2 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_xor_pos2 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule xor_neg1 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_xor_neg1 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule xor_neg2 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_xor_neg2 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule implies_pos ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_implies_pos CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule implies_neg1 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_implies_neg1 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule implies_neg2 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_implies_neg2 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule equiv_pos1 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_equiv_pos1 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule equiv_pos2 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_equiv_pos2 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule equiv_neg1 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_equiv_neg1 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule equiv_neg2 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_equiv_neg2 CL) true)
   :conclusion CL
 )
 
 (declare-rule ite1 ((phi1 Bool) (phi2 Bool) (phi3 Bool) (CL Bool)
   :premises ((cl (ite phi1 phi2 phi3)))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl phi1 phi3) CL) true)
   :conclusion CL
 )
 
 (declare-rule ite2 ((phi1 Bool) (phi2 Bool) (phi3 Bool) (CL Bool)
   :premises ((cl (ite phi1 phi2 phi3)))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl (not phi1) phi2) CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule ite_pos1 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_ite_pos1 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule ite_pos2 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_ite_pos2 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule ite_neg1 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_ite_neg1 CL) true)
   :conclusion CL
 )
 
 ; TODO: sidecondition
 (declare-rule ite_neg2 ((CL Bool))
-  :args ((CL))
+  :args (CL)
   :requires ((check_ite_neg2 CL) true)
   :conclusion CL
 )
 
 (declare-rule not_ite1 ((phi1 Bool) (phi2 Bool) (phi3 Bool) (CL Bool))
   :premises ((cl (not (ite phi1 phi2 phi3))))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl phi1 (not phi3)) CL) true)
   :conclusion CL
 )
 
 (declare-rule not_ite2 ((phi1 Bool) (phi2 Bool) (phi3 Bool) (CL Bool))
   :premises ((cl (not (ite phi1 phi2 phi3))))
-  :args ((CL))
+  :args (CL)
   :requires ((clEqual (cl (not phi1) (not phi2)) CL) true)
   :conclusion CL
 )