boolean formular manager: horn api

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/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/delegate/debugging/DebuggingBooleanFormulaManager.java

@@ -234,4 +234,11 @@ public Set<BooleanFormula> toDisjunctionArgs(BooleanFormula f, boolean flatten)
     }
     return result;
   }
+  @Override
+  public BooleanFormula makeHornClause(
+      BooleanFormula head,
+      Collection<BooleanFormula> body,
+      BooleanFormula constraint) { // TODO
+    return delegate.makeHornClause(head, body, constraint);
+  }
 }

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBooleanFormulaManager.java

@@ -154,4 +154,12 @@ public Set<BooleanFormula> toConjunctionArgs(BooleanFormula pF, boolean pFlatten
   public Set<BooleanFormula> toDisjunctionArgs(BooleanFormula pF, boolean pFlatten) {
     return delegate.toDisjunctionArgs(pF, pFlatten);
   }
+
+  @Override
+  public BooleanFormula makeHornClause(
+      BooleanFormula head,
+      Collection<BooleanFormula> body,
+      BooleanFormula constraint) {
+      return delegate.makeHornClause(head, body, constraint);
+  }
 }

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBooleanFormulaManager.java

@@ -183,4 +183,35 @@ public Set<BooleanFormula> toDisjunctionArgs(BooleanFormula pF, boolean pFlatten
       return delegate.toDisjunctionArgs(pF, pFlatten);
     }
   }
+
+  @Override
+  public BooleanFormula makeHornClause(
+      BooleanFormula head,
+      Collection<BooleanFormula> body,
+      BooleanFormula constraint) {
+    synchronized (sync) {
+      return delegate.makeHornClause(head, body, constraint);
+    }
+  }
+
+  @Override
+  public BooleanFormula makeHornClause(BooleanFormula head, Collection<BooleanFormula> body) {
+    synchronized (sync) {
+      return delegate.makeHornClause(head, body);
+    }
+  }
+
+  @Override
+  public BooleanFormula makeHornClause(Collection<BooleanFormula> body) {
+    synchronized (sync) {
+      return delegate.makeHornClause(body);
+    }
+  }
+
+  @Override
+  public BooleanFormula makeHornClause(Collection<BooleanFormula> body, BooleanFormula constraint) {
+    synchronized (sync) {
+      return delegate.makeHornClause(body, constraint);
+    }
+  }
 }

src/org/sosy_lab/java_smt/delegate/trace/TraceBooleanFormulaManager.java

@@ -200,4 +200,17 @@ public Set<BooleanFormula> toDisjunctionArgs(BooleanFormula f, boolean flatten)
             "toDisjunctionArgs(%s, %s)".formatted(logger.toVariable(f), flatten),
             () -> delegate.toDisjunctionArgs(f, flatten)));
   }
+
+  @Override
+  public BooleanFormula makeHornClause(
+      BooleanFormula head,
+      Collection<BooleanFormula> body,
+      BooleanFormula constraint) {
+    return mgr.rebuild(
+        logger.logDefDiscard(
+            "mgr.getBooleanFormulaManager()",
+            "makeHornClause(%s, %s, %s)".formatted(logger.toVariable(head),
+                logger.toVariable(body), logger.toVariable(constraint)),
+            () -> delegate.makeHornClause(head, body, constraint)));
+  }
 }

src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java

@@ -18,6 +18,7 @@
 import org.junit.Test;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.SolverException;
 
 /**
@@ -412,4 +413,37 @@ public void simplifiedIfThenElse() {
     assertThat(bmgr.ifThenElse(var1, fTrue, fFalse)).isEqualTo(var1);
     assertThat(bmgr.ifThenElse(var1, fFalse, fTrue)).isEqualTo(bmgr.not(var1));
   }
+
+  @Test
+  public void hornBuilding() throws SolverException, InterruptedException {
+    BooleanFormula a = bmgr.makeVariable("a");
+    BooleanFormula b = bmgr.makeVariable("b");
+    BooleanFormula c = bmgr.makeVariable("c");
+
+    var horn = bmgr.makeHornClause(a, ImmutableList.of(b, c));
+    var expected = bmgr.or(a, bmgr.not(b), bmgr.not(c));
+
+    assertThatFormula(horn).isEquivalentTo(expected);
+  }
+
+  @Test
+  public void hornBuildingConstraint() throws SolverException, InterruptedException {
+    assume()
+        .that(imgr)
+        .isNotNull();
+
+    BooleanFormula a = bmgr.makeVariable("a");
+    BooleanFormula b = bmgr.makeVariable("b");
+    BooleanFormula c = bmgr.makeVariable("c");
+
+    IntegerFormula d = imgr.makeVariable("d");
+    IntegerFormula n1 = imgr.makeNumber(1);
+    BooleanFormula c1 = imgr.greaterThan(d, n1);
+
+
+    var horn = bmgr.makeHornClause(a, ImmutableList.of(b, c), c1);
+    var expected = bmgr.or(a, bmgr.not(c1), bmgr.not(b), bmgr.not(c));
+
+    assertThatFormula(horn).isEquivalentTo(expected);
+  }
 }