Add support for eldarica horn solver

.classpath

@@ -23,6 +23,7 @@ SPDX-License-Identifier: Apache-2.0
 	<classpathentry kind="lib" path="lib/java/build/error_prone_annotations.jar" sourcepath="lib/java-contrib/error_prone_annotations-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/core/common.jar" sourcepath="lib/java-contrib/common-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime-smtinterpol/smtinterpol.jar" sourcepath="lib/java-contrib/smtinterpol-sources.jar"/>
+	<classpathentry kind="lib" path="lib/java/runtime-eldarica/eldarica_2.13.jar" sourcepath="lib/java-contrib/eldarica_2.13-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime-princess/princess_2.13.jar" sourcepath="lib/java-contrib/princess_2.13-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime-princess/scala-library.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime-princess/princess-smt-parser_2.13.jar"/>

.gitignore

@@ -81,3 +81,8 @@ pom.xml
 
 
 hs_err_*.log
+
+CPALog.txt
+CPALog.txt.lck
+CPALog.txt.*
+CPALog.txt.*.lck

README.md

@@ -75,6 +75,7 @@ JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.
 | [Yices2](https://yices.csl.sri.com/)                                    | :heavy_check_mark:  |                     | :heavy_check_mark: |                    | [maybe](https://github.com/sosy-lab/java-smt/pull/400)⁴ |                    |                                                                             |
 | [Z3](https://github.com/Z3Prover/z3)                                    | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                    | :heavy_check_mark: | mature and well-known solver                                                |
 | [Z3_WITH_INTERPOLATION](https://github.com/Z3Prover/z3)                 | :heavy_check_mark:  | :heavy_check_mark:  |                    |                    |                                                         |                    | an older version of Z3 that still provides interpolation support            |
+| [Eldarica](https://github.com/uuverifiers/eldarica)                     | :heavy_check_mark:  | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                    | :heavy_check_mark: | Java/Scala-based Horn solver                                                |
 
 We support a reasonable list of operating systems and versions.
 - Our main target is Linux (mainly Ubuntu or comparable Linux distributions).

build.xml

@@ -26,6 +26,7 @@ SPDX-License-Identifier: Apache-2.0
         runtime-boolector,
         runtime-cvc4,
         runtime-cvc5,
+        runtime-eldarica,
         runtime-mathsat,
         runtime-opensmt,
         runtime-optimathsat,
@@ -49,7 +50,7 @@ SPDX-License-Identifier: Apache-2.0
     <property name="errorprone.options" value="-Xep:Finally:OFF -Xep:MissingSummary:OFF -Xep:UnescapedEntity:OFF"/>
 
     <!-- Maven Central metadata -->
-    <property name="ivy.pom.description" value="Unified acccess layer to SMT solvers"/>
+    <property name="ivy.pom.description" value="Unified access layer to SMT solvers"/>
     <property name="ivy.pom.url" value="https://github.com/sosy-lab/java-smt"/>
     <property name="ivy.pom.name" value="java-smt"/>
     <property name="ivy.pom.groupId" value="org.sosy-lab"/>

build/ivysettings.xml

@@ -15,14 +15,19 @@ SPDX-License-Identifier: Apache-2.0
          Keep this file synchronized with
          https://gitlab.com/sosy-lab/software/java-project-template
     -->
-    <settings defaultResolver="Sosy-Lab"/>
+    <settings defaultResolver="chain"/>
     <property name="repo.dir" value="${basedir}/repository"/>
     <resolvers>
-        <!-- Resolver for downloading dependencies -->
-        <url name="Sosy-Lab" descriptor="required">
-            <ivy pattern="${ivy.repo.url}/[organisation]/[module]/ivy-[revision].xml" />
-            <artifact pattern="${ivy.repo.url}/[organisation]/[module]/([arch]/)[artifact]-[revision](-[classifier]).[ext]" />
-        </url>
+        <chain name="chain">
+            <!-- Resolver for downloading dependencies -->
+            <url name="Sosy-Lab" descriptor="required">
+                <ivy pattern="${ivy.repo.url}/[organisation]/[module]/ivy-[revision].xml" />
+                <artifact pattern="${ivy.repo.url}/[organisation]/[module]/([arch]/)[artifact]-[revision](-[classifier]).[ext]" />
+            </url>
+
+            <ibiblio name="local" m2compatible="true" root="https://eldarica.org/maven/"/>
+            <ibiblio name="local" m2compatible="true" root="https://repo1.maven.org/maven2/"/>
+        </chain>
 
         <!-- Resolver for publishing this project -->
         <filesystem name="Sosy-Lab-Publish">

doc/Example-Maven-Project/pom.xml

@@ -81,7 +81,7 @@ SPDX-License-Identifier: Apache-2.0
     <mathsat.version>5.6.15</mathsat.version>
     <opensmt.version>2.9.0-gef441e1c</opensmt.version>
     <smtinterpol.version>2.5-1242-g5c50fb6d</smtinterpol.version>
-    <princess.version>2025-11-17</princess.version>
+    <princess.version>2026-05-20</princess.version>
     <ostrich.version>2.0</ostrich.version>
     <javasmt-yices.version>5.0.1-1258-gdad634a69</javasmt-yices.version>
     <yices.version>2.6.4-264-g553897f5</yices.version>

doc/Example-Maven-Web-Project/pom.xml

@@ -82,7 +82,7 @@ SPDX-License-Identifier: Apache-2.0
     <mathsat.version>5.6.15</mathsat.version>
     <opensmt.version>2.9.0-gef441e1c</opensmt.version>
     <smtinterpol.version>2.5-1242-g5c50fb6d</smtinterpol.version>
-    <princess.version>2025-11-17</princess.version>
+    <princess.version>2026-05-20</princess.version>
     <ostrich.version>2.0</ostrich.version>
     <javasmt-yices.version>5.0.1-1258-gdad634a69</javasmt-yices.version>
     <yices.version>2.6.4-264-g553897f5</yices.version>

lib/ivy.xml

@@ -40,6 +40,7 @@ SPDX-License-Identifier: Apache-2.0
         <conf name="runtime-optimathsat" extends="core" description="only one solver included"/>
         <conf name="runtime-smtinterpol" extends="core" description="only one solver included"/>
         <conf name="runtime-princess" extends="core" description="only one solver included"/>
+        <conf name="runtime-eldarica" extends="core" description="only one solver included"/>
         <conf name="runtime-princess-with-javacup" extends="core" description="only one solver included"/>
         <conf name="runtime-z3" extends="runtime-z3-x64,runtime-z3-arm64" description="only one solver included"/>
         <conf name="runtime-z3-x64" extends="core" description="only one solver included"/>
@@ -171,11 +172,17 @@ SPDX-License-Identifier: Apache-2.0
         <!-- SmtInterpol -->
         <dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-1242-g5c50fb6d" conf="runtime-smtinterpol->master; contrib->sources,javadoc"/>
 
+        <!-- Eldarica -->
+        <dependency org="uuverifiers" name="eldarica_2.13" rev="2.3"
+                    conf="runtime-eldarica->master; contrib->sources"/>
+
         <!-- Princess and Ostrich for our Maven release -->
-        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2025-11-17" conf="runtime-princess-with-javacup->default; contrib->sources,javadoc"/>
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2025-05-20"
+                    conf="runtime-princess-with-javacup->default; contrib->sources,javadoc"/>
         <dependency org="io.github.uuverifiers" name="ostrich_2.13" rev="2.0" conf="runtime-princess-with-javacup->default; contrib->sources,javadoc"/>
         <!-- Princess and Ostrich for our Ivy release -->
-        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2025-11-17" conf="runtime-princess->default; contrib->sources,javadoc">
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2026-05-20"
+                    conf="runtime-princess->default; contrib->sources,javadoc">
             <!-- Exclude dependency on java-cup and replace it with java-cup-runtime, which is enough.
                We use the JAR that is published by us instead of the one from net.sf.squirrel-sql.thirdparty-non-maven
                because the latter does not provide a separate JAR for java-cup-runtime. -->

src/META-INF/MANIFEST.MF

@@ -0,0 +1,3 @@
+Manifest-Version: 1.0
+Main-Class: org.sosy_lab.java_smt.cmdline.JavaSMTMain
+

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -63,7 +63,8 @@ public enum Solvers {
     CVC4,
     CVC5,
     YICES2,
-    BITWUZLA
+    BITWUZLA,
+    ELDARICA,
   }
 
   @Option(secure = true, description = "Export solver queries in SmtLib format into a file.")
@@ -310,7 +311,7 @@ private SolverContext generateContext0(Solvers solverToCreate)
               nonLinearArithmetic,
               loader);
 
-      case PRINCESS ->
+      case PRINCESS, ELDARICA ->
           PrincessSolverContext.create(
               config, shutdownNotifier, logfile, (int) randomSeed, nonLinearArithmetic);
 

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

@@ -17,7 +17,9 @@
 import org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor;
 import org.sosy_lab.java_smt.api.visitors.TraversalProcess;
 
-/** Manager for dealing with boolean formulas. */
+/**
+ * Manager for dealing with boolean formulas.
+ */
 public interface BooleanFormulaManager {
 
   /**
@@ -30,10 +32,14 @@ default BooleanFormula makeBoolean(boolean value) {
     return value ? makeTrue() : makeFalse();
   }
 
-  /** Shortcut for {@code makeBoolean(true)}. */
+  /**
+   * Shortcut for {@code makeBoolean(true)}.
+   */
   BooleanFormula makeTrue();
 
-  /** Shortcut for {@code makeBoolean(false)}. */
+  /**
+   * Shortcut for {@code makeBoolean(false)}.
+   */
   BooleanFormula makeFalse();
 
   /**
@@ -81,8 +87,8 @@ default BooleanFormula makeBoolean(boolean value) {
    * Creates a formula representing {@code IF cond THEN f1 ELSE f2}.
    *
    * @param cond a Formula
-   * @param f1 a Formula
-   * @param f2 a Formula
+   * @param f1   a Formula
+   * @param f2   a Formula
    * @return (IF cond THEN f1 ELSE f2)
    */
   <T extends Formula> T ifThenElse(BooleanFormula cond, T f1, T f2);
@@ -116,7 +122,9 @@ default BooleanFormula and(BooleanFormula... bits) {
     return and(ImmutableList.copyOf(bits));
   }
 
-  /** Return a stream {@link Collector} that creates a conjunction of all elements in the stream. */
+  /**
+   * Return a stream {@link Collector} that creates a conjunction of all elements in the stream.
+   */
   Collector<BooleanFormula, ?, BooleanFormula> toConjunction();
 
   /**
@@ -140,13 +148,19 @@ default BooleanFormula or(BooleanFormula... bits) {
     return or(ImmutableList.copyOf(bits));
   }
 
-  /** Return a stream {@link Collector} that creates a disjunction of all elements in the stream. */
+  /**
+   * Return a stream {@link Collector} that creates a disjunction of all elements in the stream.
+   */
   Collector<BooleanFormula, ?, BooleanFormula> toDisjunction();
 
-  /** Creates a formula representing XOR of the two arguments. */
+  /**
+   * Creates a formula representing XOR of the two arguments.
+   */
   BooleanFormula xor(BooleanFormula bits1, BooleanFormula bits2);
 
-  /** Visit the formula with the given visitor. */
+  /**
+   * Visit the formula with the given visitor.
+   */
   @CanIgnoreReturnValue
   <R> R visit(BooleanFormula pFormula, BooleanFormulaVisitor<R> visitor);
 
@@ -203,4 +217,56 @@ BooleanFormula transformRecursively(
    * @param flatten If {@code true}, flatten recursively.
    */
   Set<BooleanFormula> toDisjunctionArgs(BooleanFormula f, boolean flatten);
+
+  /**
+   * Creates a constrained horn clause.
+   * {@code (constraint \/ body) => head}
+   *
+   * @param head       Head of horn clause
+   * @param body       Body of horn clause
+   * @param constraint Constraint of horn clause
+   * @return boolean formula representation of horn clause
+   */
+  BooleanFormula makeHornClause(
+      BooleanFormula head,
+      Collection<BooleanFormula> body, BooleanFormula constraint);
+
+  /**
+   * Creates a constrained horn clause.
+   * {@code body => head}
+   *
+   * @param head Head of horn clause
+   * @param body Body of horn clause
+   * @return boolean formula representation of horn clause
+   */
+  default BooleanFormula makeHornClause(
+      BooleanFormula head,
+      Collection<BooleanFormula> body) {
+    return makeHornClause(head, body, makeTrue());
+  }
+
+  /**
+   * Creates a horn clause.
+   * {@code body => true}
+   *
+   * @param body Body of horn clause
+   * @return boolean formula representation of horn clause
+   */
+  default BooleanFormula makeHornClause(Collection<BooleanFormula> body) {
+    return makeHornClause(makeTrue(), body);
+  }
+
+  /**
+   * Creates a constrained horn clause.
+   * {@code (constraint \/ body) => true}
+   *
+   * @param body       Body of horn clause
+   * @param constraint Constraint of horn clause
+   * @return boolean formula representation of horn clause
+   */
+  default BooleanFormula makeHornClause(
+      Collection<BooleanFormula> body,
+      BooleanFormula constraint) {
+    return makeHornClause(makeTrue(), body, constraint);
+  }
 }

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

@@ -0,0 +1,14 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.api;
+
+
+public interface HornProverEnvironment extends BasicProverEnvironment<Void>, AutoCloseable {
+
+}

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

@@ -90,6 +90,14 @@ enum ProverOptions {
    */
   OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options);
 
+  /**
+   * Create a fresh new {@link HornProverEnvironment} for solving horn clauses.
+   *
+   * @param options Options specified for the prover environment. All the options specified in
+   *     {@link ProverOptions} are turned off by default.
+   */
+  HornProverEnvironment newHornProverEnvironment(ProverOptions... options);
+
   /**
    * Get version information out of the solver.
    *

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

@@ -480,4 +480,11 @@ public Set<BooleanFormula> visitFunction(
           return visitDefault(f);
         }
       };
+
+  @Override
+  public BooleanFormula makeHornClause(BooleanFormula head, Collection<BooleanFormula> body,
+                                       BooleanFormula constraint) {
+
+    return implication(and(constraint, and(body)), head);
+  }
 }

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

@@ -151,7 +151,7 @@ protected final void checkEnableSeparationLogic() {
 
   protected abstract boolean hasPersistentModel();
 
-  private void setChanged() {
+  protected void setChanged() {
     wasLastSatCheckSatisfiable = false;
     if (!changedSinceLastSatQuery) {
       changedSinceLastSatQuery = true;

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

@@ -15,6 +15,7 @@
 import java.util.Set;
 import java.util.function.Consumer;
 import org.sosy_lab.java_smt.api.FormulaManager;
+import org.sosy_lab.java_smt.api.HornProverEnvironment;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
@@ -78,6 +79,18 @@ public final OptimizationProverEnvironment newOptimizationProverEnvironment(
   protected abstract OptimizationProverEnvironment newOptimizationProverEnvironment0(
       Set<ProverOptions> pSet);
 
+  @Override
+  public final HornProverEnvironment newHornProverEnvironment(
+      ProverOptions... options) {
+    return newHornProverEnvironment0(toSet(options));
+  }
+
+  protected HornProverEnvironment newHornProverEnvironment0(
+      Set<ProverOptions> pSet) {
+    // TODO: Fallback to normal ProverEnvironment?
+    throw new UnsupportedOperationException("Solver does not support horn clauses");
+  }
+
   /**
    * Whether the solver supports solving under some given assumptions (with all corresponding
    * features) by itself, i.e., whether {@link

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

@@ -125,7 +125,7 @@ public static boolean isSetInfoToken(String token) {
    * #toImmutableList()}.
    */
   public static boolean isDeclarationToken(String token) {
-    return matchesOneOf(token, "declare-const", "declare-fun");
+    return matchesOneOf(token, "declare-const", "declare-fun", "declare-datatypes");
   }
 
   /**