From 2fbab213d22b1fa4fb44ad9c50c0c357c5a52f06 Mon Sep 17 00:00:00 2001 From: Moritz Zwerger Date: Sat, 25 Apr 2026 14:50:22 +0200 Subject: [PATCH 1/3] boolean formular manager: horn api This makes it easy to create horn clauses in the form: `(constraint \/ body) => head`. --- .../java_smt/api/BooleanFormulaManager.java | 43 +++++++++++++++++++ .../AbstractBooleanFormulaManager.java | 7 +++ .../DebuggingBooleanFormulaManager.java | 7 +++ .../StatisticsBooleanFormulaManager.java | 8 ++++ .../SynchronizedBooleanFormulaManager.java | 31 +++++++++++++ .../trace/TraceBooleanFormulaManager.java | 13 ++++++ .../test/BooleanFormulaManagerTest.java | 29 +++++++++++++ 7 files changed, 138 insertions(+) diff --git a/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java b/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java index 3777fee198..677024fb1c 100644 --- a/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java @@ -203,4 +203,47 @@ BooleanFormula transformRecursively( * @param flatten If {@code true}, flatten recursively. */ Set 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 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 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 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 body, BooleanFormula constraint) { + return makeHornClause(makeTrue(), body, constraint); + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java index 8cbfa7f41d..3cdf1d364e 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java @@ -480,4 +480,11 @@ public Set visitFunction( return visitDefault(f); } }; + + @Override + public BooleanFormula makeHornClause(BooleanFormula head, Collection body, + BooleanFormula constraint) { + + return implication(and(constraint, and(body)), head); + } } diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBooleanFormulaManager.java index 9c14e185d4..077f698f91 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBooleanFormulaManager.java @@ -234,4 +234,11 @@ public Set toDisjunctionArgs(BooleanFormula f, boolean flatten) } return result; } + @Override + public BooleanFormula makeHornClause( + BooleanFormula head, + Collection body, + BooleanFormula constraint) { // TODO + return delegate.makeHornClause(head, body, constraint); + } } diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBooleanFormulaManager.java index 2a9b21840e..2fb6210e69 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBooleanFormulaManager.java @@ -154,4 +154,12 @@ public Set toConjunctionArgs(BooleanFormula pF, boolean pFlatten public Set toDisjunctionArgs(BooleanFormula pF, boolean pFlatten) { return delegate.toDisjunctionArgs(pF, pFlatten); } + + @Override + public BooleanFormula makeHornClause( + BooleanFormula head, + Collection body, + BooleanFormula constraint) { + return delegate.makeHornClause(head, body, constraint); + } } diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBooleanFormulaManager.java index 48d2551ce7..418a1b3f60 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBooleanFormulaManager.java @@ -183,4 +183,35 @@ public Set toDisjunctionArgs(BooleanFormula pF, boolean pFlatten return delegate.toDisjunctionArgs(pF, pFlatten); } } + + @Override + public BooleanFormula makeHornClause( + BooleanFormula head, + Collection body, + BooleanFormula constraint) { + synchronized (sync){ + return delegate.makeHornClause(head, body, constraint); + } + } + + @Override + public BooleanFormula makeHornClause(BooleanFormula head, Collection body) { + synchronized (sync){ + return delegate.makeHornClause(head, body); + } + } + + @Override + public BooleanFormula makeHornClause(Collection body) { + synchronized (sync){ + return delegate.makeHornClause(body); + } + } + + @Override + public BooleanFormula makeHornClause(Collection body, BooleanFormula constraint) { + synchronized (sync){ + return delegate.makeHornClause(body, constraint); + } + } } diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceBooleanFormulaManager.java index 8a422012b2..0f0c8a95c9 100644 --- a/src/org/sosy_lab/java_smt/delegate/trace/TraceBooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceBooleanFormulaManager.java @@ -200,4 +200,17 @@ public Set toDisjunctionArgs(BooleanFormula f, boolean flatten) "toDisjunctionArgs(%s, %s)".formatted(logger.toVariable(f), flatten), () -> delegate.toDisjunctionArgs(f, flatten))); } + + @Override + public BooleanFormula makeHornClause( + BooleanFormula head, + Collection 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))); + } } diff --git a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java index 594cbeddac..180569d042 100644 --- a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java +++ b/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,32 @@ 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 var1 = bmgr.makeVariable("var1"); + BooleanFormula var2 = bmgr.makeVariable("var2"); + BooleanFormula var3 = bmgr.makeVariable("var3"); + + assertThatFormula(bmgr.makeHornClause(var1, ImmutableList.of(var2, var3))).isEquisatisfiableTo( + bmgr.or(bmgr.not(bmgr.and(var2,var3)), var1)); + } + + @Test + public void hornBuildingConstraint() throws SolverException, InterruptedException { + assume() + .that(imgr) + .isNotNull(); + + BooleanFormula var1 = bmgr.makeVariable("var1"); + BooleanFormula var2 = bmgr.makeVariable("var2"); + BooleanFormula var3 = bmgr.makeVariable("var3"); + + IntegerFormula var4 = imgr.makeVariable("var4"); + IntegerFormula n1 = imgr.makeNumber(1); + BooleanFormula c1 = imgr.greaterThan(var4, n1); + + assertThatFormula(bmgr.makeHornClause(var1, ImmutableList.of(var2, var3), c1)).isEquisatisfiableTo(bmgr.or(c1, + bmgr.not(bmgr.and(var2, var3)), var1)); + } } From 2bee1acac2ce107a172c06893c0f20d0bd4b23b3 Mon Sep 17 00:00:00 2001 From: Moritz Zwerger Date: Sat, 25 Apr 2026 14:50:22 +0200 Subject: [PATCH 2/3] boolean formular manager: horn api This makes it easy to create horn clauses in the form: `(constraint \/ body) => head`. --- .../java_smt/api/BooleanFormulaManager.java | 65 +++++++++++++------ .../SynchronizedBooleanFormulaManager.java | 8 +-- .../test/BooleanFormulaManagerTest.java | 29 +++++---- 3 files changed, 65 insertions(+), 37 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java b/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java index 677024fb1c..32df5500a6 100644 --- a/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java +++ b/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 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 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 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 visit(BooleanFormula pFormula, BooleanFormulaVisitor visitor); @@ -205,45 +219,54 @@ BooleanFormula transformRecursively( Set toDisjunctionArgs(BooleanFormula f, boolean flatten); /** - * Creates a constrained horn clause + * Creates a constrained horn clause. * {@code (constraint \/ body) => head} - * @param head Head of horn clause - * @param body Body of horn clause + * + * @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 body, BooleanFormula constraint); + BooleanFormula makeHornClause( + BooleanFormula head, + Collection body, BooleanFormula constraint); /** - * Creates a constrained horn clause + * 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 body) { + default BooleanFormula makeHornClause( + BooleanFormula head, + Collection body) { return makeHornClause(head, body, makeTrue()); } /** - * Creates a horn clause + * Creates a horn clause. * {@code body => true} + * * @param body Body of horn clause * @return boolean formula representation of horn clause */ default BooleanFormula makeHornClause(Collection body) { return makeHornClause(makeTrue(), body); } + /** - * Creates a constrained horn clause + * Creates a constrained horn clause. * {@code (constraint \/ body) => true} - * @param body Body of horn clause + * + * @param body Body of horn clause * @param constraint Constraint of horn clause * @return boolean formula representation of horn clause */ - default BooleanFormula makeHornClause(Collection body, BooleanFormula constraint) { + default BooleanFormula makeHornClause( + Collection body, + BooleanFormula constraint) { return makeHornClause(makeTrue(), body, constraint); } } diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBooleanFormulaManager.java index 418a1b3f60..9c1f0ab72e 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBooleanFormulaManager.java @@ -189,28 +189,28 @@ public BooleanFormula makeHornClause( BooleanFormula head, Collection body, BooleanFormula constraint) { - synchronized (sync){ + synchronized (sync) { return delegate.makeHornClause(head, body, constraint); } } @Override public BooleanFormula makeHornClause(BooleanFormula head, Collection body) { - synchronized (sync){ + synchronized (sync) { return delegate.makeHornClause(head, body); } } @Override public BooleanFormula makeHornClause(Collection body) { - synchronized (sync){ + synchronized (sync) { return delegate.makeHornClause(body); } } @Override public BooleanFormula makeHornClause(Collection body, BooleanFormula constraint) { - synchronized (sync){ + synchronized (sync) { return delegate.makeHornClause(body, constraint); } } diff --git a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java index 180569d042..23f4f973e6 100644 --- a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java @@ -416,12 +416,14 @@ public void simplifiedIfThenElse() { @Test public void hornBuilding() throws SolverException, InterruptedException { - BooleanFormula var1 = bmgr.makeVariable("var1"); - BooleanFormula var2 = bmgr.makeVariable("var2"); - BooleanFormula var3 = bmgr.makeVariable("var3"); + BooleanFormula a = bmgr.makeVariable("a"); + BooleanFormula b = bmgr.makeVariable("b"); + BooleanFormula c = bmgr.makeVariable("c"); - assertThatFormula(bmgr.makeHornClause(var1, ImmutableList.of(var2, var3))).isEquisatisfiableTo( - bmgr.or(bmgr.not(bmgr.and(var2,var3)), var1)); + 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 @@ -430,15 +432,18 @@ public void hornBuildingConstraint() throws SolverException, InterruptedExceptio .that(imgr) .isNotNull(); - BooleanFormula var1 = bmgr.makeVariable("var1"); - BooleanFormula var2 = bmgr.makeVariable("var2"); - BooleanFormula var3 = bmgr.makeVariable("var3"); + BooleanFormula a = bmgr.makeVariable("a"); + BooleanFormula b = bmgr.makeVariable("b"); + BooleanFormula c = bmgr.makeVariable("c"); - IntegerFormula var4 = imgr.makeVariable("var4"); + IntegerFormula d = imgr.makeVariable("d"); IntegerFormula n1 = imgr.makeNumber(1); - BooleanFormula c1 = imgr.greaterThan(var4, n1); + 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(bmgr.makeHornClause(var1, ImmutableList.of(var2, var3), c1)).isEquisatisfiableTo(bmgr.or(c1, - bmgr.not(bmgr.and(var2, var3)), var1)); + assertThatFormula(horn).isEquivalentTo(expected); } } From 1bfacdefc9b83d31b0910bbbf712931d051bbb45 Mon Sep 17 00:00:00 2001 From: Moritz Zwerger Date: Tue, 28 Apr 2026 12:50:45 +0200 Subject: [PATCH 3/3] boolean formular manager: horn api This makes it easy to create horn clauses in the form: `(constraint \/ body) => head`. --- src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java index 23f4f973e6..0119d32e17 100644 --- a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java @@ -442,7 +442,7 @@ public void hornBuildingConstraint() throws SolverException, InterruptedExceptio var horn = bmgr.makeHornClause(a, ImmutableList.of(b, c), c1); - var expected = bmgr.or( a,bmgr.not(c1), bmgr.not(b), bmgr.not(c)); + var expected = bmgr.or(a, bmgr.not(c1), bmgr.not(b), bmgr.not(c)); assertThatFormula(horn).isEquivalentTo(expected); }