diff --git a/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java b/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java index 3777fee198..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); @@ -203,4 +217,56 @@ 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..9c1f0ab72e 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..0119d32e17 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,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); + } }