Translation into Z3 expressions

latte/pom.xml

@@ -16,9 +16,23 @@
     <maven.compiler.source>1.8</maven.compiler.source>
     <maven.compiler.target>1.8</maven.compiler.target>
     <version.spoon>10.4.2</version.spoon>
+    <antlr4.version>4.13.1</antlr4.version>
   </properties>
 
   <dependencies>
+    <!-- Z3-Turnkey: Z3 with bundled native libraries -->
+    <dependency>
+        <groupId>tools.aqua</groupId>
+        <artifactId>z3-turnkey</artifactId>
+        <version>4.12.2.1</version>
+    </dependency>
+
+    <dependency>
+      <groupId>org.antlr</groupId>
+      <artifactId>antlr4-runtime</artifactId>
+      <version>${antlr4.version}</version>
+    </dependency>
+    <!-- REMOVED: antlr4-maven-plugin should not be a dependency -->
 
     <dependency>
       <groupId>com.google.code.gson</groupId>
@@ -35,23 +49,21 @@
     <dependency>
       <groupId>org.junit.jupiter</groupId>
       <artifactId>junit-jupiter-api</artifactId>
-      <version>5.11.4</version> <!-- Version is fine -->
+      <version>5.11.4</version>
       <scope>test</scope>
     </dependency>
 
-    <!-- JUnit Jupiter Params (for Parameterized tests) -->
     <dependency>
       <groupId>org.junit.jupiter</groupId>
       <artifactId>junit-jupiter-params</artifactId>
-      <version>5.11.4</version> <!-- Same version for consistency -->
+      <version>5.11.4</version>
       <scope>test</scope>
     </dependency>
 
-    <!-- JUnit Jupiter Engine (for running tests) -->
     <dependency>
       <groupId>org.junit.jupiter</groupId>
       <artifactId>junit-jupiter-engine</artifactId>
-      <version>5.11.4</version> <!-- Same version for consistency -->
+      <version>5.11.4</version>
       <scope>test</scope>
     </dependency>
 
@@ -89,7 +101,6 @@
       <scope>test</scope>
     </dependency>
 
-    <!-- Spoon Core Dependency -->
     <dependency>
       <groupId>fr.inria.gforge.spoon</groupId>
       <artifactId>spoon-core</artifactId>
@@ -115,7 +126,7 @@
         </plugin>
         <plugin>
           <artifactId>maven-surefire-plugin</artifactId>
-          <version>3.0.0-M5</version> <!-- Updated to newer version for better JUnit 5 support -->
+          <version>3.0.0-M5</version>
         </plugin>
         <plugin>
           <artifactId>maven-jar-plugin</artifactId>
@@ -139,5 +150,31 @@
         </plugin>
       </plugins>
     </pluginManagement>
+
+    <!-- MOVED ANTLR PLUGIN HERE - outside of pluginManagement -->
+    <plugins>
+      <plugin>
+        <groupId>org.antlr</groupId>
+        <artifactId>antlr4-maven-plugin</artifactId>
+        <version>${antlr4.version}</version>
+        <configuration>
+          <sourceDirectory>${basedir}/src/main/java/refinements</sourceDirectory>
+          <outputDirectory>${basedir}/src/main/java/refinements</outputDirectory>
+          <arguments>
+            <argument>-package</argument>
+            <argument>refinements</argument>
+          </arguments>
+          <visitor>true</visitor>
+          <listener>true</listener>
+        </configuration>
+        <executions>
+          <execution>
+            <goals>
+              <goal>antlr4</goal>
+            </goals>
+          </execution>
+        </executions>
+      </plugin>
+    </plugins>
   </build>
-</project>
+</project>

latte/src/main/java/refinements/.antlr/RefinementsLanguage.interp

@@ -0,0 +1,43 @@
+token literal names:
+null
+'('
+')'
+'!'
+'-'
+'.'
+null
+null
+null
+null
+null
+null
+null
+null
+
+token symbolic names:
+null
+null
+null
+null
+null
+null
+LOGOP
+BOOLOP
+ARITHOP
+BOOL
+ID_UPPER
+ID
+INT
+WS
+
+rule names:
+prog
+pred
+exp
+operand
+leafs
+literal
+
+
+atn:
+[4, 1, 13, 87, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 1, 0, 1, 0, 3, 0, 15, 8, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 25, 8, 1, 1, 1, 1, 1, 1, 1, 5, 1, 30, 8, 1, 10, 1, 12, 1, 33, 9, 1, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 3, 2, 41, 8, 2, 1, 2, 1, 2, 1, 2, 5, 2, 46, 8, 2, 10, 2, 12, 2, 49, 9, 2, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 3, 3, 59, 8, 3, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 5, 3, 67, 8, 3, 10, 3, 12, 3, 70, 9, 3, 1, 4, 1, 4, 1, 4, 1, 4, 1, 4, 1, 4, 1, 4, 1, 4, 1, 4, 3, 4, 81, 8, 4, 1, 5, 1, 5, 3, 5, 85, 8, 5, 1, 5, 0, 3, 2, 4, 6, 6, 0, 2, 4, 6, 8, 10, 0, 0, 94, 0, 14, 1, 0, 0, 0, 2, 24, 1, 0, 0, 0, 4, 40, 1, 0, 0, 0, 6, 58, 1, 0, 0, 0, 8, 80, 1, 0, 0, 0, 10, 84, 1, 0, 0, 0, 12, 15, 3, 2, 1, 0, 13, 15, 1, 0, 0, 0, 14, 12, 1, 0, 0, 0, 14, 13, 1, 0, 0, 0, 15, 1, 1, 0, 0, 0, 16, 17, 6, 1, -1, 0, 17, 18, 5, 1, 0, 0, 18, 19, 3, 2, 1, 0, 19, 20, 5, 2, 0, 0, 20, 25, 1, 0, 0, 0, 21, 22, 5, 3, 0, 0, 22, 25, 3, 2, 1, 3, 23, 25, 3, 4, 2, 0, 24, 16, 1, 0, 0, 0, 24, 21, 1, 0, 0, 0, 24, 23, 1, 0, 0, 0, 25, 31, 1, 0, 0, 0, 26, 27, 10, 2, 0, 0, 27, 28, 5, 6, 0, 0, 28, 30, 3, 2, 1, 3, 29, 26, 1, 0, 0, 0, 30, 33, 1, 0, 0, 0, 31, 29, 1, 0, 0, 0, 31, 32, 1, 0, 0, 0, 32, 3, 1, 0, 0, 0, 33, 31, 1, 0, 0, 0, 34, 35, 6, 2, -1, 0, 35, 36, 5, 1, 0, 0, 36, 37, 3, 4, 2, 0, 37, 38, 5, 2, 0, 0, 38, 41, 1, 0, 0, 0, 39, 41, 3, 6, 3, 0, 40, 34, 1, 0, 0, 0, 40, 39, 1, 0, 0, 0, 41, 47, 1, 0, 0, 0, 42, 43, 10, 2, 0, 0, 43, 44, 5, 7, 0, 0, 44, 46, 3, 4, 2, 3, 45, 42, 1, 0, 0, 0, 46, 49, 1, 0, 0, 0, 47, 45, 1, 0, 0, 0, 47, 48, 1, 0, 0, 0, 48, 5, 1, 0, 0, 0, 49, 47, 1, 0, 0, 0, 50, 51, 6, 3, -1, 0, 51, 59, 3, 8, 4, 0, 52, 53, 5, 3, 0, 0, 53, 59, 3, 6, 3, 2, 54, 55, 5, 1, 0, 0, 55, 56, 3, 6, 3, 0, 56, 57, 5, 2, 0, 0, 57, 59, 1, 0, 0, 0, 58, 50, 1, 0, 0, 0, 58, 52, 1, 0, 0, 0, 58, 54, 1, 0, 0, 0, 59, 68, 1, 0, 0, 0, 60, 61, 10, 4, 0, 0, 61, 62, 5, 8, 0, 0, 62, 67, 3, 6, 3, 5, 63, 64, 10, 3, 0, 0, 64, 65, 5, 4, 0, 0, 65, 67, 3, 6, 3, 4, 66, 60, 1, 0, 0, 0, 66, 63, 1, 0, 0, 0, 67, 70, 1, 0, 0, 0, 68, 66, 1, 0, 0, 0, 68, 69, 1, 0, 0, 0, 69, 7, 1, 0, 0, 0, 70, 68, 1, 0, 0, 0, 71, 72, 5, 1, 0, 0, 72, 73, 3, 8, 4, 0, 73, 74, 5, 2, 0, 0, 74, 81, 1, 0, 0, 0, 75, 81, 3, 10, 5, 0, 76, 81, 5, 11, 0, 0, 77, 78, 5, 11, 0, 0, 78, 79, 5, 5, 0, 0, 79, 81, 5, 11, 0, 0, 80, 71, 1, 0, 0, 0, 80, 75, 1, 0, 0, 0, 80, 76, 1, 0, 0, 0, 80, 77, 1, 0, 0, 0, 81, 9, 1, 0, 0, 0, 82, 85, 5, 9, 0, 0, 83, 85, 5, 12, 0, 0, 84, 82, 1, 0, 0, 0, 84, 83, 1, 0, 0, 0, 85, 11, 1, 0, 0, 0, 10, 14, 24, 31, 40, 47, 58, 66, 68, 80, 84]

latte/src/main/java/refinements/.antlr/RefinementsLanguage.tokens

@@ -0,0 +1,18 @@
+T__0=1
+T__1=2
+T__2=3
+T__3=4
+T__4=5
+LOGOP=6
+BOOLOP=7
+ARITHOP=8
+BOOL=9
+ID_UPPER=10
+ID=11
+INT=12
+WS=13
+'('=1
+')'=2
+'!'=3
+'-'=4
+'.'=5

latte/src/main/java/refinements/.antlr/RefinementsLanguageLexer.interp

@@ -0,0 +1,56 @@
+token literal names:
+null
+'('
+')'
+'!'
+'-'
+'.'
+null
+null
+null
+null
+null
+null
+null
+null
+
+token symbolic names:
+null
+null
+null
+null
+null
+null
+LOGOP
+BOOLOP
+ARITHOP
+BOOL
+ID_UPPER
+ID
+INT
+WS
+
+rule names:
+T__0
+T__1
+T__2
+T__3
+T__4
+LOGOP
+BOOLOP
+ARITHOP
+BOOL
+ID_UPPER
+ID
+INT
+WS
+
+channel names:
+DEFAULT_TOKEN_CHANNEL
+HIDDEN
+
+mode names:
+DEFAULT_MODE
+
+atn:
+[4, 0, 13, 113, 6, -1, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 2, 6, 7, 6, 2, 7, 7, 7, 2, 8, 7, 8, 2, 9, 7, 9, 2, 10, 7, 10, 2, 11, 7, 11, 2, 12, 7, 12, 1, 0, 1, 0, 1, 1, 1, 1, 1, 2, 1, 2, 1, 3, 1, 3, 1, 4, 1, 4, 1, 5, 1, 5, 1, 5, 1, 5, 3, 5, 42, 8, 5, 1, 6, 1, 6, 1, 6, 1, 6, 1, 6, 3, 6, 49, 8, 6, 1, 7, 1, 7, 1, 8, 1, 8, 1, 8, 1, 8, 1, 8, 1, 8, 1, 8, 1, 8, 1, 8, 3, 8, 62, 8, 8, 1, 9, 1, 9, 5, 9, 66, 8, 9, 10, 9, 12, 9, 69, 9, 9, 1, 10, 5, 10, 72, 8, 10, 10, 10, 12, 10, 75, 9, 10, 1, 10, 1, 10, 5, 10, 79, 8, 10, 10, 10, 12, 10, 82, 9, 10, 1, 11, 4, 11, 85, 8, 11, 11, 11, 12, 11, 86, 1, 11, 4, 11, 90, 8, 11, 11, 11, 12, 11, 91, 1, 11, 1, 11, 4, 11, 96, 8, 11, 11, 11, 12, 11, 97, 5, 11, 100, 8, 11, 10, 11, 12, 11, 103, 9, 11, 3, 11, 105, 8, 11, 1, 12, 4, 12, 108, 8, 12, 11, 12, 12, 12, 109, 1, 12, 1, 12, 0, 0, 13, 1, 1, 3, 2, 5, 3, 7, 4, 9, 5, 11, 6, 13, 7, 15, 8, 17, 9, 19, 10, 21, 11, 23, 12, 25, 13, 1, 0, 7, 2, 0, 42, 43, 47, 47, 1, 0, 65, 90, 3, 0, 48, 57, 65, 90, 97, 122, 3, 0, 65, 90, 95, 95, 97, 122, 5, 0, 35, 35, 48, 57, 65, 90, 95, 95, 97, 122, 1, 0, 48, 57, 3, 0, 9, 10, 13, 13, 32, 32, 125, 0, 1, 1, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 5, 1, 0, 0, 0, 0, 7, 1, 0, 0, 0, 0, 9, 1, 0, 0, 0, 0, 11, 1, 0, 0, 0, 0, 13, 1, 0, 0, 0, 0, 15, 1, 0, 0, 0, 0, 17, 1, 0, 0, 0, 0, 19, 1, 0, 0, 0, 0, 21, 1, 0, 0, 0, 0, 23, 1, 0, 0, 0, 0, 25, 1, 0, 0, 0, 1, 27, 1, 0, 0, 0, 3, 29, 1, 0, 0, 0, 5, 31, 1, 0, 0, 0, 7, 33, 1, 0, 0, 0, 9, 35, 1, 0, 0, 0, 11, 41, 1, 0, 0, 0, 13, 48, 1, 0, 0, 0, 15, 50, 1, 0, 0, 0, 17, 61, 1, 0, 0, 0, 19, 63, 1, 0, 0, 0, 21, 73, 1, 0, 0, 0, 23, 104, 1, 0, 0, 0, 25, 107, 1, 0, 0, 0, 27, 28, 5, 40, 0, 0, 28, 2, 1, 0, 0, 0, 29, 30, 5, 41, 0, 0, 30, 4, 1, 0, 0, 0, 31, 32, 5, 33, 0, 0, 32, 6, 1, 0, 0, 0, 33, 34, 5, 45, 0, 0, 34, 8, 1, 0, 0, 0, 35, 36, 5, 46, 0, 0, 36, 10, 1, 0, 0, 0, 37, 38, 5, 38, 0, 0, 38, 42, 5, 38, 0, 0, 39, 40, 5, 124, 0, 0, 40, 42, 5, 124, 0, 0, 41, 37, 1, 0, 0, 0, 41, 39, 1, 0, 0, 0, 42, 12, 1, 0, 0, 0, 43, 44, 5, 61, 0, 0, 44, 49, 5, 61, 0, 0, 45, 46, 5, 60, 0, 0, 46, 49, 5, 61, 0, 0, 47, 49, 5, 60, 0, 0, 48, 43, 1, 0, 0, 0, 48, 45, 1, 0, 0, 0, 48, 47, 1, 0, 0, 0, 49, 14, 1, 0, 0, 0, 50, 51, 7, 0, 0, 0, 51, 16, 1, 0, 0, 0, 52, 53, 5, 116, 0, 0, 53, 54, 5, 114, 0, 0, 54, 55, 5, 117, 0, 0, 55, 62, 5, 101, 0, 0, 56, 57, 5, 102, 0, 0, 57, 58, 5, 97, 0, 0, 58, 59, 5, 108, 0, 0, 59, 60, 5, 115, 0, 0, 60, 62, 5, 101, 0, 0, 61, 52, 1, 0, 0, 0, 61, 56, 1, 0, 0, 0, 62, 18, 1, 0, 0, 0, 63, 67, 7, 1, 0, 0, 64, 66, 7, 2, 0, 0, 65, 64, 1, 0, 0, 0, 66, 69, 1, 0, 0, 0, 67, 65, 1, 0, 0, 0, 67, 68, 1, 0, 0, 0, 68, 20, 1, 0, 0, 0, 69, 67, 1, 0, 0, 0, 70, 72, 5, 35, 0, 0, 71, 70, 1, 0, 0, 0, 72, 75, 1, 0, 0, 0, 73, 71, 1, 0, 0, 0, 73, 74, 1, 0, 0, 0, 74, 76, 1, 0, 0, 0, 75, 73, 1, 0, 0, 0, 76, 80, 7, 3, 0, 0, 77, 79, 7, 4, 0, 0, 78, 77, 1, 0, 0, 0, 79, 82, 1, 0, 0, 0, 80, 78, 1, 0, 0, 0, 80, 81, 1, 0, 0, 0, 81, 22, 1, 0, 0, 0, 82, 80, 1, 0, 0, 0, 83, 85, 7, 5, 0, 0, 84, 83, 1, 0, 0, 0, 85, 86, 1, 0, 0, 0, 86, 84, 1, 0, 0, 0, 86, 87, 1, 0, 0, 0, 87, 105, 1, 0, 0, 0, 88, 90, 7, 5, 0, 0, 89, 88, 1, 0, 0, 0, 90, 91, 1, 0, 0, 0, 91, 89, 1, 0, 0, 0, 91, 92, 1, 0, 0, 0, 92, 101, 1, 0, 0, 0, 93, 95, 5, 95, 0, 0, 94, 96, 7, 5, 0, 0, 95, 94, 1, 0, 0, 0, 96, 97, 1, 0, 0, 0, 97, 95, 1, 0, 0, 0, 97, 98, 1, 0, 0, 0, 98, 100, 1, 0, 0, 0, 99, 93, 1, 0, 0, 0, 100, 103, 1, 0, 0, 0, 101, 99, 1, 0, 0, 0, 101, 102, 1, 0, 0, 0, 102, 105, 1, 0, 0, 0, 103, 101, 1, 0, 0, 0, 104, 84, 1, 0, 0, 0, 104, 89, 1, 0, 0, 0, 105, 24, 1, 0, 0, 0, 106, 108, 7, 6, 0, 0, 107, 106, 1, 0, 0, 0, 108, 109, 1, 0, 0, 0, 109, 107, 1, 0, 0, 0, 109, 110, 1, 0, 0, 0, 110, 111, 1, 0, 0, 0, 111, 112, 6, 12, 0, 0, 112, 26, 1, 0, 0, 0, 13, 0, 41, 48, 61, 67, 73, 80, 86, 91, 97, 101, 104, 109, 1, 0, 1, 0]