Extend Solver Independent SMTLib2 Parser/Generator

.classpath

@@ -33,6 +33,7 @@ SPDX-License-Identifier: Apache-2.0
 	<classpathentry kind="lib" path="lib/java/runtime-cvc5/cvc5.jar"/>
 	<classpathentry kind="lib" path="lib/java/test/truth-java8-extension.jar" sourcepath="lib/java-contrib/truth-java8-extension-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/core/checker-qual.jar" sourcepath="lib/java-contrib/checker-qual-sources.jar"/>
+	<classpathentry kind="lib" path="lib/java/core/antlr4-runtime.jar"/>
 	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-11">
 		<attributes>
 			<attribute name="module" value="true"/>

build/Checkstyle.exclude.xml

@@ -0,0 +1,24 @@
+<?xml version="1.0"?>
+
+<!--
+This file is part of CPAchecker,
+a tool for configurable software verification:
+https://cpachecker.sosy-lab.org
+
+SPDX-FileCopyrightText: 2007-2025 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+<!DOCTYPE suppressions PUBLIC "-//Checkstyle//DTD SuppressionFilter Configuration 1.2//EN" "https://checkstyle.org/dtds/suppressions_1_2.dtd">
+
+<suppressions>
+  <!-- Generated code gets excluded -->
+  <suppress files="src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Visitor.java" checks=".*"/>
+  <suppress files="src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Smtlibv2Listener.java" checks=".*"/>
+  <suppress files="src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Smtlibv2Visitor.java" checks=".*"/>
+  <suppress files="src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Smtlibv2Lexer.java" checks=".*"/>
+  <suppress files="src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Smtlibv2Parser.java" checks=".*"/>
+  <suppress files="src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Smtlibv2BaseListener.java" checks=".*"/>
+  <suppress files="src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Smtlibv2BaseVisitor.java" checks=".*"/>
+</suppressions>

build/SpotBugs.exclude.xml

@@ -28,4 +28,6 @@ SPDX-License-Identifier: Apache-2.0
     <Match><Bug pattern="RV_RETURN_VALUE_IGNORED"/></Match>
     <!-- Exclude AutoValue classes -->
     <Match><Class name="~.*\.AutoValue_.*"/></Match>
+    <!-- Exclude autogenerated ANTLR files -->
+    <Match><Class name="~.*\.Smtlibv2.*"/></Match>
 </FindBugsFilter>

build/ivysettings.xml

@@ -10,7 +10,6 @@ SPDX-FileCopyrightText: 2018-2020 Dirk Beyer <https://www.sosy-lab.org>
 SPDX-License-Identifier: Apache-2.0
 -->
 
-<!DOCTYPE ivysettings> <!-- generic AcceptAllDTD to make the Eclipse Warning go away -->
 <ivysettings>
     <!-- DO NOT EDIT LOCALLY!
          Keep this file synchronized with

doc/Example-Maven-Project/src/main/java/org/sosy_lab/java_smt_example/SolverOverviewTable.java

@@ -32,7 +32,6 @@ public static void main(String[] args) throws SolverException, InterruptedExcept
     for (Solvers s : Solvers.values()) {
       infos.add(infoProvider.getSolverInformation(s));
     }
-
     infos.sort(Comparator.comparing(SolverInfo::getName)); // alphabetical ordering
 
     RowBuilder rowBuilder = new RowBuilder();

lib/ivy.xml

@@ -177,6 +177,9 @@ SPDX-License-Identifier: Apache-2.0
              As long as this is the case we need to provide the JAR, otherwise javac complains. -->
         <dependency org="org.codehaus.mojo" name="animal-sniffer-annotations" rev="1.18" conf="core->default;"/>
 
+        <!-- Antlr grammar support for our SMTLIB2 parser/generator -->
+        <dependency org="org.antlr" name="antlr4-runtime" rev="4.13.1" conf="core->default;"/>
+
         <!-- Guava has a dependency on error_prone_annotations without a revision number, need an override. -->
         <override org="com.google.errorprone" module="error_prone_annotations" rev="2.4.0"/>
 

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -26,10 +26,12 @@
 import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
 import org.sosy_lab.java_smt.api.SolverContext;
 import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
+import org.sosy_lab.java_smt.basicimpl.Generator;
 import org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverContext;
 import org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext;
 import org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext;
 import org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext;
+import org.sosy_lab.java_smt.solvers.SolverLess.SolverLessContext;
 import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaSolverContext;
 import org.sosy_lab.java_smt.solvers.boolector.BoolectorSolverContext;
 import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext;
@@ -60,7 +62,8 @@ public enum Solvers {
     CVC4,
     CVC5,
     YICES2,
-    BITWUZLA
+    SOLVERLESS,
+    BITWUZLA,
   }
 
   @Option(secure = true, description = "Export solver queries in SmtLib format into a file.")
@@ -113,6 +116,15 @@ public enum Solvers {
               + "This affects only the theories of integer and rational arithmetic.")
   private NonLinearArithmetic nonLinearArithmetic = NonLinearArithmetic.USE;
 
+  @Option(secure = true, description = "Enable SMTLIB2 script generation.")
+  private boolean generateSMTLIB2 = false;
+
+  @Option(secure = true, description = "Run the solver binary instead of using the library.")
+  private boolean useBinary = false;
+
+  @Option(secure = true, description = "Which Solver SolverLess should use to solve constraints")
+  private Solvers usedSolverBySolverLess = Solvers.Z3;
+
   private final LogManager logger;
   private final ShutdownNotifier shutdownNotifier;
   private final Configuration config;
@@ -158,6 +170,11 @@ public SolverContextFactory(
       Consumer<String> pLoader)
       throws InvalidConfigurationException {
     pConfig.inject(this);
+    if (useBinary && !generateSMTLIB2) {
+      throw new InvalidConfigurationException(
+          "Can't use option solver.useBinary without also enabling solver.generateSMTLIB2.");
+    }
+
     logger = pLogger.withComponentName("JavaSMT");
     shutdownNotifier = checkNotNull(pShutdownNotifier);
     config = pConfig;
@@ -208,7 +225,13 @@ public SolverContext generateContext() throws InvalidConfigurationException {
   @SuppressWarnings("resource") // returns unclosed context object
   public SolverContext generateContext(Solvers solverToCreate)
       throws InvalidConfigurationException {
-
+    if (useBinary && solverToCreate != Solvers.PRINCESS) {
+      throw new InvalidConfigurationException(
+          String.format(
+              "Can't use option solver.useBinary with solver %s. Currently only Princess is"
+                  + "supported in binary mode.",
+              solverToCreate));
+    }
     SolverContext context;
     try {
       context = generateContext0(solverToCreate);
@@ -234,7 +257,11 @@ public SolverContext generateContext(Solvers solverToCreate)
       // statistics need to be the most outer wrapping layer.
       context = new StatisticsSolverContext(context);
     }
-
+    if (solverToCreate == Solvers.SOLVERLESS) {
+      Generator.setIsLoggingEnabled(true);
+    } else {
+      Generator.setIsLoggingEnabled(generateSMTLIB2);
+    }
     return context;
   }
 
@@ -292,13 +319,15 @@ private SolverContext generateContext0(Solvers solverToCreate)
 
       case PRINCESS:
         return PrincessSolverContext.create(
-            config, shutdownNotifier, logfile, (int) randomSeed, nonLinearArithmetic);
+            config, useBinary, shutdownNotifier, logfile, (int) randomSeed, nonLinearArithmetic);
 
       case YICES2:
         return Yices2SolverContext.create(nonLinearArithmetic, shutdownNotifier, loader);
 
       case BOOLECTOR:
         return BoolectorSolverContext.create(config, shutdownNotifier, logfile, randomSeed, loader);
+      case SOLVERLESS:
+        return SolverLessContext.create(usedSolverBySolverLess);
 
       case BITWUZLA:
         return BitwuzlaSolverContext.create(

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

@@ -14,5 +14,22 @@ public enum FloatingPointRoundingMode {
   NEAREST_TIES_AWAY,
   TOWARD_POSITIVE,
   TOWARD_NEGATIVE,
-  TOWARD_ZERO
+  TOWARD_ZERO;
+
+  public String getSMTLIBFormat() {
+    switch (this) {
+      case NEAREST_TIES_TO_EVEN:
+        return "RNE";
+      case NEAREST_TIES_AWAY:
+        return "RNA";
+      case TOWARD_POSITIVE:
+        return "RTP";
+      case TOWARD_NEGATIVE:
+        return "RTN";
+      case TOWARD_ZERO:
+        return "RTZ";
+      default:
+        throw new IllegalArgumentException("Unknown rounding mode: " + this);
+    }
+  }
 }

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

@@ -10,16 +10,37 @@
 
 import com.google.common.collect.ImmutableMap;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import java.io.IOException;
 import java.util.List;
 import java.util.Map;
 import org.sosy_lab.common.Appender;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor;
 import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
 import org.sosy_lab.java_smt.api.visitors.TraversalProcess;
 
 /** FormulaManager class contains all operations which can be performed on formulas. */
 public interface FormulaManager {
 
+  /**
+   * Parses an SMT-LIB2 String and translates it into an equivalent BooleanFormula constraint.
+   *
+   * @param pString SMT-LIB2 formula as String that will be parsed
+   * @return BooleanFormula equivalent to the SMT-LIB2 string
+   */
+  // TODO Clean up exceptions?
+  BooleanFormula universalParseFromString(String pString)
+      throws IOException, SolverException, InterruptedException, InvalidConfigurationException;
+
+  /**
+   * Calls the dumpSMTLIB2 method from the Generator, which will write the assembled SMT-LIB2 to a
+   * file 'Out.smt2'.
+   *
+   * @throws IOException if writing to file fails
+   */
+  // TODO Return a String, instead of writing to a file
+  void dumpSMTLIB2() throws IOException;
+
   /**
    * Returns the Integer-Theory. Because most SAT-solvers support automatic casting between Integer-
    * and Rational-Theory, the Integer- and the RationalFormulaManager both return the same Formulas

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

@@ -274,8 +274,9 @@ public String toString() {
     }
 
     @Override
-    public String toSMTLIBString() {
-      return "(_ FloatingPoint " + exponentSize + " " + mantissaSize + ")";
+    public String toSMTLIBString() { // SMTLIB2 ALWAYS CONSIDERS SIGN BIT IN THE MANTISSA SIZE!
+      // returning (_ FloatingPoint 8 23) for single precision is incorrect.
+      return "(_ FloatingPoint " + exponentSize + " " + mantissaSize + 1 + ")";
     }
   }
 

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

@@ -53,7 +53,10 @@ enum ProverOptions {
     GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS,
 
     /** Whether the solver should enable support for formulae build in SL theory. */
-    ENABLE_SEPARATION_LOGIC
+    ENABLE_SEPARATION_LOGIC,
+
+    // TODO Document this option
+    USE_BINARY
   }
 
   /**

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

@@ -38,8 +38,11 @@ public <TI extends Formula, TE extends Formula> TE select(
     //    Rational
 
     final TFormulaInfo term = select(extractInfo(pArray), extractInfo(pIndex));
-
-    return (TE) getFormulaCreator().encapsulate(elementType, term);
+    TE result = (TE) getFormulaCreator().encapsulate(elementType, term);
+    if (Generator.isLoggingEnabled()) {
+      ArrayGenerator.logSelect(result, pArray, pIndex);
+    }
+    return result;
   }
 
   protected abstract TFormulaInfo select(TFormulaInfo pArray, TFormulaInfo pIndex);
@@ -52,7 +55,12 @@ public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> store(
     final FormulaType<TE> elementType = getFormulaCreator().getArrayFormulaElementType(pArray);
 
     final TFormulaInfo term = store(extractInfo(pArray), extractInfo(pIndex), extractInfo(pValue));
-    return getFormulaCreator().encapsulateArray(term, indexType, elementType);
+    ArrayFormula<TI, TE> result =
+        getFormulaCreator().encapsulateArray(term, indexType, elementType);
+    if (Generator.isLoggingEnabled()) {
+      ArrayGenerator.logStore(result, pArray, pIndex, pValue);
+    }
+    return result;
   }
 
   protected abstract TFormulaInfo store(
@@ -64,10 +72,16 @@ protected abstract TFormulaInfo store(
           TE extends Formula,
           FTI extends FormulaType<TI>,
           FTE extends FormulaType<TE>>
-      ArrayFormula<TI, TE> makeArray(String pName, FTI pIndexType, FTE pElementType) {
+      ArrayFormula<TI, TE> makeArray(String pName, FTI pIndexType, FTE pElementType)
+          throws GeneratorException {
     checkVariableName(pName);
     final TFormulaInfo namedArrayFormula = internalMakeArray(pName, pIndexType, pElementType);
-    return getFormulaCreator().encapsulateArray(namedArrayFormula, pIndexType, pElementType);
+    ArrayFormula<TI, TE> result =
+        getFormulaCreator().encapsulateArray(namedArrayFormula, pIndexType, pElementType);
+    if (Generator.isLoggingEnabled()) {
+      ArrayGenerator.logMakeArray(result, pName, pIndexType, pElementType);
+    }
+    return result;
   }
 
   @Override
@@ -101,8 +115,13 @@ public <TE extends Formula> FormulaType<TE> getElementType(ArrayFormula<?, TE> p
   @Override
   public <TI extends Formula, TE extends Formula> BooleanFormula equivalence(
       ArrayFormula<TI, TE> pArray1, ArrayFormula<TI, TE> pArray2) {
-    return getFormulaCreator()
-        .encapsulateBoolean(equivalence(extractInfo(pArray1), extractInfo(pArray2)));
+    BooleanFormula result =
+        getFormulaCreator()
+            .encapsulateBoolean(equivalence(extractInfo(pArray1), extractInfo(pArray2)));
+    if (Generator.isLoggingEnabled()) {
+      ArrayGenerator.logArrayEquivalence(result, pArray1, pArray2);
+    }
+    return result;
   }
 
   protected abstract TFormulaInfo equivalence(TFormulaInfo pArray1, TFormulaInfo pArray2);