Update Z3 library jar; Move constraint deserializer out of knarr. Con…

…straintSerializer now writes directly to stream, uses references by offset instead of making a separate table. Add some hacks to reduce duplicate constraint generation
gmu-swe · Aug 11, 2021 · 6e63b91 · 6e63b91
1 parent aacb943
commit 6e63b91
Show file tree

Hide file tree

Showing 5 changed files with 359 additions and 474 deletions.
diff --git a/knarr-server/pom.xml b/knarr-server/pom.xml
@@ -89,11 +89,10 @@
             <artifactId>choco-solver</artifactId>
             <version>3.3.0</version>
         </dependency>
-		<!-- https://mvnrepository.com/artifact/org.sosy-lab/javasmt-solver-z3 -->
         <dependency>
-            <groupId>org.sosy-lab</groupId>
-            <artifactId>javasmt-solver-z3</artifactId>
-            <version>4.8.9-sosy1</version>
+            <groupId>edu.gmu.swe.z3</groupId>
+            <artifactId>z3</artifactId>
+            <version>4.8.12-SNAPSHOT</version>
         </dependency>
     </dependencies>
     <distributionManagement>

diff --git a/knarr/src/main/java/edu/gmu/swe/knarr/internal/ConstraintDeserializer.java b/knarr/src/main/java/edu/gmu/swe/knarr/internal/ConstraintDeserializer.java