Rebase master onto Scala 2.13

.github/workflows/scala.yml

@@ -2,9 +2,9 @@ name: Scala CI
 
 on:
   push:
-    branches: [ master ]
+    branches: [ master, scala-2.13 ]
   pull_request:
-    branches: [ master ]
+    branches: [ master, scala-2.13 ]
 
 jobs:
   build:

build.sbt

@@ -173,6 +173,9 @@ lazy val root = (project in file(".")).
     }}).value,
 //
     assembly / test := None,
+//
+    libraryDependencies +=
+      "org.scala-lang.modules" %% "scala-parser-combinators" % "2.3.0",
 //
     libraryDependencies +=
       "net.sf.squirrel-sql.thirdparty-non-maven" % "java-cup" % "0.11a",

regression-tests/horn-accel/Answers

@@ -311,9 +311,13 @@ unsat
 booleans.smt2
 Warning: ignoring exit
 sat
-(define-fun main_1 ((A Int) (B Int) (C Int) (D Int) (E Bool) (F Int)) Bool (or (= A 0) (and (= A 1) (and (= E true) (and (and (and (and (and (and (and (and (>= (+ (* 2 C) (+ (* (- 2) D) F)) B) (<= B 999999)) (>= B 0)) (<= C 499998)) (<= D 499999)) (>= D 1)) (<= F 999999)) (>= F 4)) (or (>= (- F B) 3) (and (= (+ B (+ (* (- 2) C) (- (* 2 D) F))) 0) (>= (- D C) 1))))))))
+(
+    (define-fun main_1 ((A Int) (B Int) (C Int) (D Int) (E Bool) (F Int)) Bool (or (= A 0) (and (= A 1) (and (= E true) (and (and (and (and (and (and (and (and (>= (+ (* 2 C) (+ (* (- 2) D) F)) B) (<= B 999999)) (>= B 0)) (<= C 499998)) (<= D 499999)) (>= D 1)) (<= F 999999)) (>= F 4)) (or (>= (- F B) 3) (and (= (+ B (+ (* (- 2) C) (- (* 2 D) F))) 0) (>= (- D C) 1))))))))
+)
 
 chc-LIA-Lin_421.smt2
 Warning: ignoring exit
 sat
-(define-fun predh11_1 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 Int) (L1 Int) (M1 Int) (N1 Int) (O1 Int) (P1 Int) (Q1 Int) (R1 Int) (S1 Int) (T1 Int) (U1 Int) (V1 Int) (W1 Int) (X1 Int) (Y1 Int) (Z1 Int) (A2 Int) (B2 Int) (C2 Int) (D2 Int) (E2 Int) (F2 Int) (G2 Int) (H2 Int)) Bool (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= H2 D1) (= G2 C1)) (= (- F2 F) 1)) (= E2 1)) (= D2 F)) (= C2 1)) (= (- B2 F) 1)) (= A2 1)) (= Z1 F)) (= Y1 1)) (= X1 F)) (= W1 1)) (= V1 R)) (= U1 Q)) (= T1 P)) (= (+ S1 (- L R1)) 0)) (= Q1 1)) (= P1 L)) (= O1 K)) (= N1 J)) (= M1 I)) (= L1 H)) (= K1 G)) (= J1 F)) (= I1 E)) (= H1 D)) (= G1 C)) (= F1 B)) (= E1 A)) (and (>= (- F J) (- 1)) (>= J 1))))
+(
+    (define-fun predh11_1 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 Int) (L1 Int) (M1 Int) (N1 Int) (O1 Int) (P1 Int) (Q1 Int) (R1 Int) (S1 Int) (T1 Int) (U1 Int) (V1 Int) (W1 Int) (X1 Int) (Y1 Int) (Z1 Int) (A2 Int) (B2 Int) (C2 Int) (D2 Int) (E2 Int) (F2 Int) (G2 Int) (H2 Int)) Bool (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= H2 D1) (= G2 C1)) (= (- F2 F) 1)) (= E2 1)) (= D2 F)) (= C2 1)) (= (- B2 F) 1)) (= A2 1)) (= Z1 F)) (= Y1 1)) (= X1 F)) (= W1 1)) (= V1 R)) (= U1 Q)) (= T1 P)) (= (+ S1 (- L R1)) 0)) (= Q1 1)) (= P1 L)) (= O1 K)) (= N1 J)) (= M1 I)) (= L1 H)) (= K1 G)) (= J1 F)) (= I1 E)) (= H1 D)) (= G1 C)) (= F1 B)) (= E1 A)) (and (>= (- F J) (- 1)) (>= J 1))))
+)

regression-tests/horn-adt/Answers

@@ -1,12 +1,16 @@
 
 simple-adt-horn.smt2
 sat
-(define-fun I1 ((A Pair)) Bool (and (= (right A) true) (>= (left A) 0)))
-(define-fun I2 ((A Pair)) Bool (and (not (= (right A) true)) (>= (left A) 1)))
+(
+    (define-fun I1 ((A Pair)) Bool (and (= (right A) true) (>= (left A) 0)))
+    (define-fun I2 ((A Pair)) Bool (and (not (= (right A) true)) (>= (left A) 1)))
+)
 
 bool.smt2
 sat
-(define-fun Inv ((A Bool) (B Bool)) Bool (or (and (= A true) (= B true)) (and (not (= A true)) (not (= B true)))))
+(
+    (define-fun Inv ((A Bool) (B Bool)) Bool (or (and (= A true) (= B true)) (and (not (= A true)) (not (= B true)))))
+)
 
 bool-unsat.smt2
 unsat
@@ -17,10 +21,14 @@ unsat
 
 list-synasc.smt2
 sat
-(define-fun Concat ((A IList) (B IList) (C IList)) Bool (or (and (and (= (+ (_size A) (- (_size B) (_size C))) 1) (and (>= (_size C) (_size B)) (>= (_size B) 1))) (= (head C) (head A))) (and (and (and (and (= (_size A) 1) (or (and (is-Nil B) (is-Nil C)) (and (is-Cons B) (is-Cons C)))) (= (_size B) (_size C))) (>= (_size C) 1)) (or (not (is-Cons C)) (= (head C) (head B))))))
+(
+    (define-fun Concat ((A IList) (B IList) (C IList)) Bool (or (and (and (= (+ (_size A) (- (_size B) (_size C))) 1) (and (>= (_size C) (_size B)) (>= (_size B) 1))) (= (head C) (head A))) (and (and (and (and (= (_size A) 1) (or (and (is-Nil B) (is-Nil C)) (and (is-Cons B) (is-Cons C)))) (= (_size B) (_size C))) (>= (_size C) 1)) (or (not (is-Cons C)) (= (head C) (head B))))))
+)
 
 unbounded-tree.smt2
 sat
+(
+)
 
 record-cex.smt2
 unsat
@@ -58,11 +66,15 @@ unsat
 
 testers.smt2
 sat
-(define-fun p1 ((A XS)) Bool (is-XS_cons A))
+(
+    (define-fun p1 ((A XS)) Bool (is-XS_cons A))
+)
 
 tuple.smt2
 sat
-(define-fun p1 ((A Pair) (B Int)) Bool (and (and (>= (first A) 1) (<= (second A) 2)) (>= B 42)))
+(
+    (define-fun p1 ((A Pair) (B Int)) Bool (and (and (>= (first A) 1) (<= (second A) 2)) (>= B 42)))
+)
 
 tuple2.smt2
 unsat
@@ -77,17 +89,23 @@ unsat
 
 polymorphicTuple.smt2
 sat
-(define-fun p1 ((A (Pair Int Int)) (B Int)) Bool (and (and (>= (first A) 1) (<= (second A) 2)) (>= B 42)))
+(
+    (define-fun p1 ((A (Pair Int Int)) (B Int)) Bool (and (and (>= (first A) 1) (<= (second A) 2)) (>= B 42)))
+)
 
 adt-bug.smt2
 sat
-(define-fun pred1 ((A Int) (B abi_type) (C f_type) (D f_type)) Bool (or (not (= B a)) (and (= D C) (= A 0))))
+(
+    (define-fun pred1 ((A Int) (B abi_type) (C f_type) (D f_type)) Bool (or (not (= B a)) (and (= D C) (= A 0))))
+)
 
 de-brujin-bug.smt2
 sat
-(define-fun mmin ((A f)) Bool (= (h 0 g) A))
-(define-fun n ((A f)) Bool (= (_size A) 1))
-(define-fun p ((A f) (B d1) (C f)) Bool (or (or (and (and (= (_size A) (_size C)) (= (_size B) 1)) (>= (_size C) 1)) (and (and (and (is-b B) (= (_size B) 3)) (and (>= (_size A) 1) (>= (_size C) 1))) (is-b B))) (and (and (and (is-b B) (and (and (and (and (or (and (is-g A) (>= (_size B) 4)) (and (is-h A) (>= (+ (- 1) (_size B)) 4))) (or (and (is-g A) (>= (_size B) 5)) (and (is-h A) (>= (+ 1 (_size B)) 5)))) (>= (+ (_size A) (_size B)) 6)) (>= (_size A) 1)) (>= (_size C) 1))) (is-b B)) (= (mod (+ 1 (_size B)) 2) 0))))
+(
+    (define-fun mmin ((A f)) Bool (= (h 0 g) A))
+    (define-fun n ((A f)) Bool (= (_size A) 1))
+    (define-fun p ((A f) (B d1) (C f)) Bool (or (or (and (and (= (_size A) (_size C)) (= (_size B) 1)) (>= (_size C) 1)) (and (and (and (is-b B) (= (_size B) 3)) (and (>= (_size A) 1) (>= (_size C) 1))) (is-b B))) (and (and (and (is-b B) (and (and (and (and (or (and (is-g A) (>= (_size B) 4)) (and (is-h A) (>= (+ (- 1) (_size B)) 4))) (or (and (is-g A) (>= (_size B) 5)) (and (is-h A) (>= (+ 1 (_size B)) 5)))) (>= (+ (_size A) (_size B)) 6)) (>= (_size A) 1)) (>= (_size C) 1))) (is-b B)) (= (mod (+ 1 (_size B)) 2) 0))))
+)
 
 list-synasc-unsat.smt2
 unsat