Rerelease CVC4 to add JavaDocs and sources

build/build-publish-solvers/solver-cvc4.xml

@@ -12,15 +12,15 @@ SPDX-License-Identifier: Apache-2.0
 
 <!-- vim: set tabstop=8 shiftwidth=4 expandtab sts=4 filetype=ant fdm=marker: -->
 <project name="publish-solvers-cvc4" basedir="." xmlns:ivy="antlib:org.apache.ivy.ant">
-
     <import file="macros.xml"/>
 
-    <target name="package-cvc4" depends="">
-        <!-- Copy CVC4 binaries to the root folder along with the version postfix. -->
+    <property name="cvc4.distDir" value="${ivy.solver.dist.dir}/cvc4"/>
+
+    <target name="initialize-cvc4">
         <fail unless="cvc4.path">
             Please specify the path to CVC4 with the flag -Dcvc4.path=/path/to/cvc4.
             The path has to point to the root CVC4 folder, i.e.,
-            a checkout of the official git repository from 'https://github.com/CVC4/CVC4.git'.
+            a checkout of the official git repository from 'https://github.com/CVC4/CVC4-archived.git'.
             Note that shell substitutions do not work and a full absolute path has to be specified.
         </fail>
         <fail unless="cvc4.customRev">
@@ -36,56 +36,94 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="--format=%h"/>
         </exec>
         <property name="cvc4.version" value="${cvc4.customRev}-g${cvc4.revision}"/>
-        <echo message="Building CVC4 in version '${cvc4.version}'"/>
+    </target>
 
+    <target name="package-cvc4" depends="initialize-cvc4">
         <!-- build CVC4 -->
         <exec executable="rm" dir="${cvc4.path}" failonerror="true">
             <arg value="-rf"/>
-            <arg value="symfpu-CVC4"/>
+            <arg value="deps/symfpu-CVC4"/>
         </exec>
         <exec executable="./contrib/get-symfpu" dir="${cvc4.path}" failonerror="true"/>
         <exec executable="./configure.sh" dir="${cvc4.path}" failonerror="true">
             <arg value="--symfpu"/>
             <arg value="--language-bindings=java"/>
+            <arg value="--gmp-dir=/dependencies/gmp-6.3.0/install/x64-linux/"/>
+            <arg value="--prefix=${cvc4.path}/install"/>
         </exec>
         <exec executable="make" dir="${cvc4.path}/build/" failonerror="true">
-            <arg value="-j4" />
+            <arg value="-j8"/>
+            <arg value="install"/>
         </exec>
 
         <!-- remove unneeded symbols -->
-        <exec executable="strip" dir="${cvc4.path}/build/src/bindings/java/" failonerror="true">
+        <exec executable="strip" dir="${cvc4.path}/install/lib" failonerror="true">
             <arg value="libcvc4jni.so" />
-        </exec>
-        <exec executable="strip" dir="${cvc4.path}/build/src/" failonerror="true">
             <arg value="libcvc4.so" />
         </exec>
-        <exec executable="strip" dir="${cvc4.path}/build/src/parser/" failonerror="true">
-            <arg value="libcvc4parser.so" />
-        </exec>
 
         <!-- fix RPATH and library dependencies -->
-        <exec executable="patchelf" dir="${cvc4.path}/build/src/parser/" failonerror="true">
-            <arg value="--set-rpath"/><arg value="$ORIGIN"/>
-            <arg value="--replace-needed"/><arg value="libcvc4.so.6"/><arg value="libcvc4.so"/>
-            <arg value="libcvc4parser.so"/>
-        </exec>
-        <exec executable="patchelf" dir="${cvc4.path}/build/src/bindings/java/" failonerror="true">
+        <exec executable="patchelf" dir="${cvc4.path}/install/lib" failonerror="true">
             <arg value="--set-rpath"/><arg value="$ORIGIN"/>
-            <arg value="--replace-needed"/><arg value="libcvc4.so.6"/><arg value="libcvc4.so"/>
-            <arg value="--replace-needed"/><arg value="libcvc4parser.so.6"/><arg value="libcvc4parser.so"/>
+            <arg value="--replace-needed"/>
+            <arg value="libcvc4.so.7"/>
+            <arg value="libcvc4.so"/>
             <arg value="libcvc4jni.so"/>
         </exec>
 
         <!-- copy library files into directory to be published for IVY -->
-        <copy file="${cvc4.path}/build/src/libcvc4.so" tofile="libcvc4-${cvc4.version}.so"/>
-        <copy file="${cvc4.path}/build/src/parser/libcvc4parser.so" tofile="libcvc4parser-${cvc4.version}.so"/>
-        <copy file="${cvc4.path}/build/src/bindings/java/libcvc4jni.so" tofile="libcvc4jni-${cvc4.version}.so"/>
-        <copy file="${cvc4.path}/build/src/bindings/java/CVC4.jar" tofile="CVC4-${cvc4.version}.jar"/>
+        <mkdir dir="${cvc4.distDir}/x64"/>
+        <copy file="${cvc4.path}/install/lib/libcvc4.so" tofile="${cvc4.distDir}/x64/libcvc4-${cvc4.version}.so"/>
+        <copy file="${cvc4.path}/install/lib/libcvc4jni.so" tofile="${cvc4.distDir}/x64/libcvc4jni-${cvc4.version}.so"/>
+        <copy file="${cvc4.path}/install/share/java/cvc4/CVC4.jar" tofile="${cvc4.distDir}/CVC4-${cvc4.version}.jar"/>
+    </target>
+
+    <target name="package-cvc4-sources" depends="package-cvc4">
+        <jar destfile="${cvc4.distDir}/CVC4-${cvc4.version}-sources.jar" whenmanifestonly="fail">
+            <zipfileset dir="${cvc4.path}/build/src/bindings/java" includes="**/*.java" prefix="edu/stanford/CVC4"/>
+            <zipfileset dir="${cvc4.path}" includes="COPYING" prefix="META-INF"/>
+            <manifest>
+                <attribute name="Implementation-Title" value="cvc4"/>
+                <attribute name="Implementation-Version" value="${cvc4.version}"/>
+            </manifest>
+        </jar>
     </target>
 
-    <target name="publish-cvc4" depends="package-cvc4, load-ivy"
-        description="Publish CVC4 binaries to Ivy repository.">
-        <ivy:resolve conf="solver-cvc4" file="solvers_ivy_conf/ivy_cvc4.xml" />
-        <publishToRepository solverName="CVC4" solverVersion="${cvc4.version}"/>
+    <target name="package-cvc4-javadoc" depends="package-cvc4">
+        <javadoc destdir="${cvc4.path}/build/javadoc"
+                 classpathref="classpath"
+                 locale="en_US"
+                 encoding="utf-8"
+                 windowtitle="cvc4"
+                 failonerror="true"
+                 failonwarning="false">
+            <fileset dir="${cvc4.path}/build/src/bindings/java">
+                <include name="**/*.java"/>
+            </fileset>
+            <link href="https://docs.oracle.com/en/java/javase/11/docs/api/"/>
+            <doctitle><![CDATA[<h1>cvc4</h1>]]></doctitle>
+            <arg line="${javadoc.doclint}"/>
+        </javadoc>
+        <jar jarfile="${cvc4.distDir}/CVC4-${cvc4.version}-javadoc.jar" whenmanifestonly="fail">
+            <zipfileset dir="${cvc4.path}" includes="COPYING" prefix="META-INF"/>
+            <zipfileset dir="${cvc4.path}/build/javadoc"/>
+        </jar>
+    </target>
+
+    <target name="publish-cvc4" depends="package-cvc4, package-cvc4-sources, package-cvc4-javadoc, load-ivy" description="Publish CVC4 binaries to Ivy repository.">
+        <ivy:resolve conf="solver-cvc4" file="solvers_ivy_conf/ivy_cvc4.xml"/>
+        <publishToRepository solverName="CVC4" solverVersion="${cvc4.version}" distDir="${cvc4.distDir}"/>
+
+        <!--
+          We additionally provide x64-files without arch-attribute for backwards compatibility,
+          such that applications can load dependencies without changing their Ivy configuration.
+          Those files are not part of any direct configuration, but will be resolved if the
+          arch-attribute is not used.
+        -->
+        <copy todir="repository/${ivy.organisation}/${ivy.module}/">
+            <fileset dir="repository/${ivy.organisation}/${ivy.module}/x64/">
+                <include name="*-${cvc4.version}.*"/>
+            </fileset>
+        </copy>
     </target>
 </project>

doc/Developers-How-to-Release-into-Ivy.md

@@ -129,6 +129,21 @@ Example:
 ant publish-z3-legacy -Dz3.path=../solvers/z3/z3 -Dz3.customRev=4.5.0
 ```
 
+### Publishing CVC4
+
+We use the Docker image with Ubuntu 18.04 for publishing CVC4.
+Please manually add two additional dependencies before running the build script:
+
+```bash
+pip3 install toml
+apt-get install antlr3 libantlr3c-dev
+```
+
+Then run the build script to publish the bindings:
+
+```bash
+ant publish-cvc4 -Dcvc4.path=/workspace/CVC4-archived -Dcvc4.customRev=1.8.1
+```
 
 ### Publishing CVC5
 

lib/ivy.xml

@@ -190,7 +190,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.17.0-1009b13" conf="runtime-z3-x64->solver-z3-x64; runtime-z3-arm64->solver-z3-arm64; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.9.2-ge4c80308" conf="runtime-opensmt-x64->solver-opensmt-x64; runtime-opensmt-arm64->solver-opensmt-arm64; contrib->sources,javadoc"/>
         <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.3-sosy1" conf="runtime-optimathsat->solver-optimathsat" />
-        <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8.1-g40eac7f05" conf="runtime-cvc4->solver-cvc4; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="2026-02-26-d22638a" conf="runtime-cvc5-x64->solver-cvc5-x64; runtime-cvc5-arm64->solver-cvc5-arm64"/>
         <dependency org="org.sosy_lab" name="javasmt-solver-boolector" rev="3.2.2-g1a89c229" conf="runtime-boolector->solver-boolector" />
         <dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.9.0-gd13ef925" conf="runtime-bitwuzla-x64->solver-bitwuzla-x64; runtime-bitwuzla-arm64->solver-bitwuzla-arm64; contrib->sources,javadoc"/>

lib/native/x86_64-linux/libcvc4.so

@@ -1 +1 @@
-../../java/runtime-cvc4/libcvc4.so
+../../java/runtime-cvc4/x64/libcvc4.so

lib/native/x86_64-linux/libcvc4jni.so

@@ -1 +1 @@
-../../java/runtime-cvc4/libcvc4jni.so
+../../java/runtime-cvc4/x64/libcvc4jni.so

solvers_ivy_conf/ivy_cvc4.xml

@@ -23,14 +23,27 @@ SPDX-License-Identifier: Apache-2.0
     </info>
 
     <configurations>
-        <conf name="solver-cvc4" />
+        <!-- default config, provides only x64 for backwards-compatibility -->
+        <conf name="solver-cvc4" extends="solver-cvc4-x64"/>
+
+        <!-- main configurations -->
+        <conf name="solver-cvc4-x64" extends="solver-cvc4-linux-x64"/>
+        <conf name="sources"/>
+        <conf name="javadoc"/>
+
+        <!-- basic configurations -->
+        <conf name="solver-cvc4-linux-x64" extends="solver-cvc4-common"/>
+
+        <conf name="solver-cvc4-common" visibility="private"/>
     </configurations>
 
     <publications defaultconf="solver-cvc4">
-        <artifact name="libcvc4jni"    conf="solver-cvc4" type="shared-object" ext="so"/>
-        <artifact name="libcvc4"       conf="solver-cvc4" type="shared-object" ext="so"/>
-        <artifact name="libcvc4parser" conf="solver-cvc4" type="shared-object" ext="so"/>
-        <artifact name="CVC4" conf="solver-cvc4" />
+        <artifact name="libcvc4jni" conf="solver-cvc4-linux-x64" e:arch="x64" type="shared-object" ext="so"/>
+        <artifact name="libcvc4" conf="solver-cvc4-linux-x64" e:arch="x64" type="shared-object" ext="so"/>
+
+        <artifact name="CVC4" conf="solver-cvc4-common" ext="jar"/>
+        <artifact name="CVC4" conf="sources" e:classifier="sources" type="source" ext="jar"/>
+        <artifact name="CVC4" conf="javadoc" e:classifier="javadoc" type="javadoc" ext="jar"/>
     </publications>
 
     <dependencies></dependencies>

src/org/sosy_lab/java_smt/api/FormulaType.java

@@ -21,8 +21,10 @@
 import com.google.errorprone.annotations.Immutable;
 import java.util.List;
 import java.util.Set;
+import java.util.regex.Pattern;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
+import org.sosy_lab.java_smt.basicimpl.Tokenizer;
 
 /**
  * Type of a formula.
@@ -418,8 +420,7 @@ public String toString() {
 
     @Override
     public String toSMTLIBString() {
-      throw new UnsupportedOperationException(
-          "rounding mode is not expected in symbol declarations");
+      return "RoundingMode";
     }
   }
 
@@ -613,4 +614,37 @@ public static FormulaType<?> fromString(String t) {
       throw new AssertionError("unknown type:" + t);
     }
   }
+
+  public static FormulaType<?> fromSMTLIBString(String t) {
+    if (t.equals("Bool")) {
+      return BooleanType;
+    } else if (t.equals("Int")) {
+      return IntegerType;
+    } else if (t.equals("Real")) {
+      return RationalType;
+    } else if (t.equals("String")) {
+      return StringType;
+    } else if (t.equals("RegLan")) {
+      return RegexType;
+    } else if (t.equals("RoundingMode")) {
+      return FloatingPointRoundingModeType;
+    } else if (t.startsWith("(_ FloatingPoint")) {
+      var m = Pattern.compile("\\(\\s*_\\s+FloatingPoint\\s+(\\d+)\\s+(\\d+)\\s*\\)").matcher(t);
+      checkArgument(m.find());
+      return FormulaType.getFloatingPointTypeFromSizesWithHiddenBit(
+          Integer.parseInt(m.group(1)), Integer.parseInt(m.group(2)));
+    } else if (t.startsWith("(_ BitVec")) {
+      var m = Pattern.compile("\\(\\s*_\\s+BitVec\\s+(\\d+)\\s*\\)").matcher(t);
+      checkArgument(m.find());
+      return FormulaType.getBitvectorTypeWithSize(Integer.parseInt(m.group(1)));
+    } else if (t.startsWith("(Array")) {
+      var tokens = Tokenizer.tokenize(t.substring(1, t.length() - 1));
+      checkArgument(tokens.size() == 3);
+      var domain = fromSMTLIBString(tokens.get(1));
+      var range = fromSMTLIBString(tokens.get(2));
+      return FormulaType.getArrayType(domain, range);
+    } else {
+      throw new AssertionError("unknown type:" + t);
+    }
+  }
 }

src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java

@@ -121,9 +121,16 @@ public static List<String> tokenize(String input) {
               // Handle opening brackets
               token.append("(");
               level++;
+            } else if (c == ')') {
+              throw new IllegalArgumentException(
+                  "parentheses do not match, unexpected closing parenthesis");
             } else {
-              // Should be unreachable: all top-level expressions need parentheses around them
-              throw new IllegalArgumentException();
+              token.append(c);
+            }
+          } else {
+            if (!token.isEmpty()) {
+              builder.add(token.toString());
+              token = new StringBuilder();
             }
           }
         } else {
@@ -146,7 +153,10 @@ public static List<String> tokenize(String input) {
     }
     if (level != 0) {
       // Throw an exception if the brackets don't match
-      throw new IllegalArgumentException("brackets do not match, too many open brackets");
+      throw new IllegalArgumentException("parentheses do not match, too many open parentheses");
+    }
+    if (!token.isEmpty()) {
+      builder.add(token.toString());
     }
     return builder.build();
   }

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4ArrayFormulaManager.java

@@ -50,7 +50,8 @@ protected <TI extends Formula, TE extends Formula> Expr internalMakeArray(
   protected <TI extends Formula, TE extends Formula> Expr internalMakeArray(
       FormulaType<TI> pIndexType, FormulaType<TE> pElementType, Expr defaultElement) {
     final Type cvc4ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType));
-    return exprManager.mkConst(new ArrayStoreAll((ArrayType) cvc4ArrayType, defaultElement));
+    return exprManager.mkConst(
+        new ArrayStoreAll(exprManager, (ArrayType) cvc4ArrayType, defaultElement));
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java

@@ -13,7 +13,6 @@
 import edu.stanford.CVC4.BitVectorRotateLeft;
 import edu.stanford.CVC4.BitVectorRotateRight;
 import edu.stanford.CVC4.BitVectorSignExtend;
-import edu.stanford.CVC4.BitVectorType;
 import edu.stanford.CVC4.BitVectorZeroExtend;
 import edu.stanford.CVC4.Expr;
 import edu.stanford.CVC4.ExprManager;
@@ -235,7 +234,7 @@ protected Expr toIntegerFormulaImpl(Expr pBv, boolean pSigned) {
       // TODO check what is cheaper for the solver:
       // checking the first BV-bit or computing max-int-value for the given size
 
-      final int size = Math.toIntExact(new BitVectorType(pBv.getType()).getSize());
+      final int size = ((BitvectorType) formulaCreator.getFormulaType(pBv)).getSize();
       final BigInteger modulo = BigInteger.ONE.shiftLeft(size);
       final BigInteger maxInt = BigInteger.ONE.shiftLeft(size - 1).subtract(BigInteger.ONE);
       final Expr moduloExpr = exprManager.mkConst(new Rational(modulo.toString()));
@@ -254,8 +253,6 @@ protected Expr toIntegerFormulaImpl(Expr pBv, boolean pSigned) {
 
   @Override
   protected Expr distinctImpl(List<Expr> pParam) {
-    vectorExpr param = new vectorExpr();
-    pParam.forEach(param::add);
-    return exprManager.mkExpr(Kind.DISTINCT, param);
+    return exprManager.mkExpr(Kind.DISTINCT, new vectorExpr(exprManager, pParam));
   }
 }

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BooleanFormulaManager.java

@@ -87,11 +87,7 @@ protected Expr andImpl(Collection<Expr> pParams) {
     return switch (operands.size()) {
       case 0 -> cvc4True;
       case 1 -> Iterables.getOnlyElement(operands);
-      default -> {
-        vectorExpr vExpr = new vectorExpr();
-        operands.forEach(vExpr::add);
-        yield exprManager.mkExpr(Kind.AND, vExpr);
-      }
+      default -> exprManager.mkExpr(Kind.AND, new vectorExpr(exprManager, operands));
     };
   }
 
@@ -127,13 +123,7 @@ protected Expr orImpl(Collection<Expr> pParams) {
     return switch (operands.size()) {
       case 0 -> cvc4False;
       case 1 -> Iterables.getOnlyElement(operands);
-      default -> {
-        vectorExpr vExpr = new vectorExpr();
-        for (Expr e : operands) {
-          vExpr.add(e);
-        }
-        yield exprManager.mkExpr(Kind.OR, vExpr);
-      }
+      default -> exprManager.mkExpr(Kind.OR, new vectorExpr(exprManager, operands));
     };
   }