diff --git a/src/checkers/inference/model/Constraint.java b/src/checkers/inference/model/Constraint.java index 2e14115e5..faaefea08 100644 --- a/src/checkers/inference/model/Constraint.java +++ b/src/checkers/inference/model/Constraint.java @@ -42,7 +42,7 @@ public Constraint(List slots) { public AnnotationLocation getLocation() { return location; } - + public abstract T serialize(Serializer serializer); /** diff --git a/src/checkers/inference/model/ConstraintManager.java b/src/checkers/inference/model/ConstraintManager.java index e03682d8b..aa54a2257 100644 --- a/src/checkers/inference/model/ConstraintManager.java +++ b/src/checkers/inference/model/ConstraintManager.java @@ -62,6 +62,19 @@ private void add(Constraint constraint) { } } + /** + * Allows {@link ImplicationConstraint} to add its component assumptions + * directly to the manager as part of one of its normalization cases. + * + * @param constraints + * a collection of (possibly normalized) constraints + */ + protected void addAll(Iterable constraints) { + for (Constraint c : constraints) { + add(c); + } + } + public void startIgnoringConstraints() { ignoreConstraints = true; } @@ -130,6 +143,10 @@ public ExistentialConstraint createExistentialConstraint(Slot slot, ifNotExistsConstraints, getCurrentLocation()); } + public Constraint createImplicationConstraint(List assumptions, Constraint conclusion) { + return ImplicationConstraint.create(assumptions, conclusion, getCurrentLocation()); + } + /** * Create an {@link ArithmeticConstraint} for the given operation and slots. */ @@ -259,4 +276,8 @@ public void addArithmeticConstraint(ArithmeticOperationKind operation, Slot left Slot rightOperand, ArithmeticVariableSlot result) { add(createArithmeticConstraint(operation, leftOperand, rightOperand, result)); } + + public void addImplicationConstraint(List assumptions, Constraint conclusion) { + add(createImplicationConstraint(assumptions, conclusion)); + } } diff --git a/src/checkers/inference/model/ImplicationConstraint.java b/src/checkers/inference/model/ImplicationConstraint.java new file mode 100644 index 000000000..6df6ea7f6 --- /dev/null +++ b/src/checkers/inference/model/ImplicationConstraint.java @@ -0,0 +1,163 @@ +package checkers.inference.model; + +import org.checkerframework.dataflow.util.HashCodeUtils; +import org.checkerframework.javacutil.BugInCF; + +import checkers.inference.InferenceMain; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +/** + * Constraint that models implication logic. If all the assumptions are + * satisfied, then conclusion should also be satisfied. + *

+ * Suppose one needs to enforce this restriction: if {@code @A} is inferred as + * on declaration of class {@code MyClass}, then every usage of class + * {@code MyClass} needs to be inferred to {@code @A}. + * {@link ImplicationConstraint} can express this restriction: + *

+ * {@code @1 == @A -> @2 == @A}, in which {@code @1} is the slot inserted on the + * class tree and {@code @2} is the slot that represents one usage of + * {@code MyClass}. + */ +public class ImplicationConstraint extends Constraint { + + /** + * An immutable set of {@link Constraint}s that are conjuncted together. + */ + private final Set assumptions; + + /** + * A single {@link Constraint} that is implicated by the + * {@link #assumptions}. + */ + private final Constraint conclusion; + + public ImplicationConstraint(Set assumptions, + Constraint conclusion, AnnotationLocation location) { + super(extractAllSlots(assumptions, conclusion), location); + + this.assumptions = Collections.unmodifiableSet(assumptions); + this.conclusion = conclusion; + } + + private static List extractAllSlots(Iterable assumptions, + Constraint conclusion) { + List slots = new ArrayList<>(); + for (Constraint a : assumptions) { + slots.addAll(a.getSlots()); + } + slots.addAll(conclusion.getSlots()); + return slots; + } + + // TODO: the input should be a set of constraints instead of a list. This + // requires modifying the constraint manager and PICO. + public static Constraint create(List assumptions, + Constraint conclusion, AnnotationLocation currentLocation) { + if (assumptions == null || conclusion == null) { + throw new BugInCF( + "Adding implication constraint with null argument. assumptions: " + + assumptions + " conclusion: " + conclusion); + } + + // Normalization cases: + // 1) assumptions == empty ==> return conclusion + // 2) any assumption == FALSE ==> return TRUE + // 3) refinedAssumptions == empty ==> return conclusion + // 4) refinedAssumptions != empty && conclusion == TRUE ==> return TRUE + // 5) refinedAssumptions != empty && conclusion == FALSE ==> return + // conjunction of refinedAssumptions + // 6) refinedAssumptions != empty && conclusion != TRUE && conclusion != + // FALSE ==> CREATE_REAL_IMPLICATION_CONSTRAINT + + // 1) assumptions == empty ==> return conclusion + // Optimization for trivial cases when there are no preconditions for + // the conclusion to be true, meaning conclusion is a hard constraint + // that must be satisfied. + if (assumptions.isEmpty()) { + return conclusion; + } + + // Otherwise, assumptions list is not empty + Set refinedAssumptions = new HashSet<>(); + // Iterate over assumptions: if any assumption is false, directly return + // AlwaysTrueConstraint; + // If any assumption is true, don't add it to the refined assumptions + // set and continue the iteration. + for (Constraint assumption : assumptions) { + // 2) any assumption == FALSE ==> return TRUE + if (assumption instanceof AlwaysFalseConstraint) { + // assumption is false, the whole implication is true + return AlwaysTrueConstraint.create(); + } else if (!(assumption instanceof AlwaysTrueConstraint)) { + // current assumption is not statically known to true or false. + refinedAssumptions.add(assumption); + } + } + + // 3) refinedAssumptions == empty ==> return conclusion + if (refinedAssumptions.isEmpty()) { + // This covers the case where original assumptions list is not empty + // and every assumption is AlwaysTrueConstraint + return conclusion; + } + + // 4) refinedAssumptions != empty && conclusion == TRUE ==> return TRUE + if (conclusion instanceof AlwaysTrueConstraint) { + return AlwaysTrueConstraint.create(); + } + + // 5) refinedAssumptions != empty && conclusion == FALSE ==> return + // conjunction of refinedAssumptions + if (conclusion instanceof AlwaysFalseConstraint) { + // Instead of creating a "conjunction constraint", here we directly + // add the set of constraints to the constraint manager + InferenceMain.getInstance().getConstraintManager() + .addAll(refinedAssumptions); + // since all assumptions are added to the constraint manager, we + // return a dummy always true constraint as the normalized result + return AlwaysTrueConstraint.create(); + } + + // 6) refinedAssumptions != empty && conclusion != TRUE && conclusion != + // FALSE ==> CREATE_REAL_IMPLICATION_CONSTRAINT + return new ImplicationConstraint(refinedAssumptions, conclusion, + currentLocation); + } + + @Override + public T serialize(Serializer serializer) { + return serializer.serialize(this); + } + + public Set getAssumptions() { + return assumptions; + } + + public Constraint getConclusion() { + return conclusion; + } + + @Override + public int hashCode() { + return HashCodeUtils.hash(assumptions, conclusion); + } + + @Override + public boolean equals(Object obj) { + if (this == obj) { + return true; + } + if (obj == null || this.getClass() != obj.getClass()) { + return false; + } + ImplicationConstraint other = (ImplicationConstraint) obj; + return assumptions.equals(other.assumptions) + && conclusion.equals(other.conclusion); + } +} diff --git a/src/checkers/inference/model/Serializer.java b/src/checkers/inference/model/Serializer.java index 80386d0d0..8fd10b6c2 100644 --- a/src/checkers/inference/model/Serializer.java +++ b/src/checkers/inference/model/Serializer.java @@ -44,5 +44,8 @@ public interface Serializer { T serialize(PreferenceConstraint preferenceConstraint); + T serialize(ImplicationConstraint implicationConstraint); + T serialize(ArithmeticConstraint arithmeticConstraint); + } diff --git a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java index 759b80c90..0d4297f17 100644 --- a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java +++ b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java @@ -6,6 +6,7 @@ import java.util.Map; import checkers.inference.model.LubVariableSlot; +import checkers.inference.model.ImplicationConstraint; import org.sat4j.core.VecInt; import checkers.inference.SlotManager; @@ -273,6 +274,12 @@ public VecInt[] serialize(PreferenceConstraint preferenceConstraint) { throw new UnsupportedOperationException("APPLY WEIGHTING FOR WEIGHTED MAX-SAT"); } + @Override + public VecInt[] serialize(ImplicationConstraint implicationConstraint) { + throw new UnsupportedOperationException("ImplicationConstraint is supported in more-advanced" + + "MaxSAT backend. Use MaxSATSolver instead!"); + } + public List convertAll(Iterable constraints) { return convertAll(constraints, new LinkedList()); } diff --git a/src/checkers/inference/model/serialization/JsonSerializer.java b/src/checkers/inference/model/serialization/JsonSerializer.java index e39d76fa2..485059545 100644 --- a/src/checkers/inference/model/serialization/JsonSerializer.java +++ b/src/checkers/inference/model/serialization/JsonSerializer.java @@ -1,11 +1,14 @@ package checkers.inference.model.serialization; +import java.util.ArrayList; import java.util.Collection; +import java.util.List; import java.util.Map; import javax.lang.model.element.AnnotationMirror; import checkers.inference.model.LubVariableSlot; +import checkers.inference.model.ImplicationConstraint; import org.json.simple.JSONArray; import org.json.simple.JSONObject; import checkers.inference.model.ArithmeticConstraint; @@ -139,6 +142,10 @@ public class JsonSerializer implements Serializer { protected static final String EXISTENTIAL_THEN = "then"; protected static final String EXISTENTIAL_ELSE = "else"; + protected static final String IMPLICATION_CONSTRAINT_KEY = "implication"; + protected static final String IMPLICATION_ASSUMPTIONS = "assumptions"; + protected static final String IMPLICATION_CONCLUSTION = "conclusion"; + protected static final String ARITH_LEFT_OPERAND = "left_operand"; protected static final String ARITH_RIGHT_OPERAND = "right_operand"; protected static final String ARITH_RESULT = "result"; @@ -335,6 +342,21 @@ public JSONObject serialize(PreferenceConstraint constraint) { return obj; } + @Override + public JSONObject serialize(ImplicationConstraint implicationConstraint) { + // If either assumptions or conclusion is null, the program would have been terminated + // when trying to create that ImplicationConstraint instance. + JSONObject obj = new JSONObject(); + obj.put(CONSTRAINT_KEY, IMPLICATION_CONSTRAINT_KEY); + List serializedAssumptions = new ArrayList<>(); + for (Constraint assumption : implicationConstraint.getAssumptions()) { + serializedAssumptions.add(assumption.serialize(this)); + } + obj.put(IMPLICATION_ASSUMPTIONS, serializedAssumptions); + obj.put(IMPLICATION_CONCLUSTION, implicationConstraint.getConclusion().serialize(this)); + return obj; + } + @SuppressWarnings("unchecked") @Override public JSONObject serialize(ArithmeticConstraint constraint) { diff --git a/src/checkers/inference/model/serialization/ToStringSerializer.java b/src/checkers/inference/model/serialization/ToStringSerializer.java index 0d3559ff4..25434499c 100644 --- a/src/checkers/inference/model/serialization/ToStringSerializer.java +++ b/src/checkers/inference/model/serialization/ToStringSerializer.java @@ -20,6 +20,7 @@ import checkers.inference.model.EqualityConstraint; import checkers.inference.model.ExistentialConstraint; import checkers.inference.model.ExistentialVariableSlot; +import checkers.inference.model.ImplicationConstraint; import checkers.inference.model.InequalityConstraint; import checkers.inference.model.LubVariableSlot; import checkers.inference.model.PreferenceConstraint; @@ -267,6 +268,39 @@ public String serialize(ArithmeticConstraint arithmeticConstraint) { return sb.toString(); } + @Override + public String serialize(ImplicationConstraint implicationConstraint) { + boolean prevShowVerboseVars = showVerboseVars; + showVerboseVars = false; + // format(non-empty): assumption1 & assumption 2 & ... & assumption n -> conclusion + // format(empty): [ ] -> conclusion + final StringBuilder sb = new StringBuilder(); + sb.append(getCurrentIndentString()); + int oldIndentationLevel = indentationLevel; + // This is to avoid indentation for each sub constraint that comprises the implicationConstraint + indentationLevel = 0; + String assumptions = getAssumptionsString(implicationConstraint); + String conclusion = implicationConstraint.getConclusion().serialize(this); + sb.append(assumptions).append(" -> ").append(conclusion); + // Recover the previous indentation level to not affect further serializations + indentationLevel = oldIndentationLevel; + showVerboseVars = prevShowVerboseVars; + return sb.toString(); + } + + private String getAssumptionsString(ImplicationConstraint implicationConstraint) { + if (implicationConstraint.getAssumptions().isEmpty()) { + return "[ ]"; + } + + List serializedAssumptions = new ArrayList<>(); + for (Constraint assumption : implicationConstraint.getAssumptions()) { + serializedAssumptions.add(assumption.serialize(this)); + } + + return String.join(" & ", serializedAssumptions); + } + // variables @Override public String serialize(VariableSlot slot) { @@ -279,9 +313,9 @@ public String serialize(VariableSlot slot) { @Override public String serialize(RefinementVariableSlot slot) { final StringBuilder sb = new StringBuilder(); - sb.append(slot.getId()) - .append(": refines ") - .append(Arrays.asList(slot.getRefined())); + sb.append(slot.getId()); + // "↧" sign is \u21A7 + sb.append("[ \u21A7 "+ slot.getRefined() + " ]"); optionallyShowVerbose(slot, sb); return sb.toString(); } diff --git a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java index 3554e1e00..b84f82c7f 100644 --- a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java +++ b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java @@ -8,6 +8,7 @@ import checkers.inference.model.EqualityConstraint; import checkers.inference.model.ExistentialConstraint; import checkers.inference.model.ExistentialVariableSlot; +import checkers.inference.model.ImplicationConstraint; import checkers.inference.model.InequalityConstraint; import checkers.inference.model.LubVariableSlot; import checkers.inference.model.PreferenceConstraint; @@ -23,6 +24,7 @@ import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; import checkers.inference.solver.backend.encoder.existential.ExistentialConstraintEncoder; +import checkers.inference.solver.backend.encoder.implication.ImplicationConstraintEncoder; import checkers.inference.solver.backend.encoder.preference.PreferenceConstraintEncoder; import checkers.inference.solver.frontend.Lattice; @@ -112,6 +114,8 @@ public abstract class AbstractFormatTranslator existentialConstraintEncoder; + protected ImplicationConstraintEncoder implicationConstraintEncoder; + /** * {@code ArithmeticConstraintEncoder} to which encoding of {@link ArithmeticConstraint} is delegated. */ @@ -137,6 +141,7 @@ protected void finishInitializingEncoders() { preferenceConstraintEncoder = encoderFactory.createPreferenceConstraintEncoder(); combineConstraintEncoder = encoderFactory.createCombineConstraintEncoder(); existentialConstraintEncoder = encoderFactory.createExistentialConstraintEncoder(); + implicationConstraintEncoder = encoderFactory.createImplicationConstraintEncoder(); arithmeticConstraintEncoder = encoderFactory.createArithmeticConstraintEncoder(); } @@ -190,6 +195,12 @@ public ConstraintEncodingT serialize(ExistentialConstraint constraint) { ConstraintEncoderCoordinator.redirect(constraint, existentialConstraintEncoder); } + @Override + public ConstraintEncodingT serialize(ImplicationConstraint constraint) { + return implicationConstraintEncoder == null ? null : + ConstraintEncoderCoordinator.redirect(constraint, implicationConstraintEncoder); + } + @Override public ConstraintEncodingT serialize(ArithmeticConstraint constraint) { return arithmeticConstraintEncoder == null ? null : diff --git a/src/checkers/inference/solver/backend/encoder/AbstractConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/encoder/AbstractConstraintEncoderFactory.java index ed1f40d5e..d4a148768 100644 --- a/src/checkers/inference/solver/backend/encoder/AbstractConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/encoder/AbstractConstraintEncoderFactory.java @@ -1,22 +1,33 @@ package checkers.inference.solver.backend.encoder; +import checkers.inference.solver.backend.FormatTranslator; import checkers.inference.solver.frontend.Lattice; /** * Abstract base class for all concrete {@link ConstraintEncoderFactory}. Subclasses of {@code AbstractConstraintEncoderFactory} * should override corresponding createXXXEncoder methods to return concrete implementations if the - * {@link checkers.inference.solver.backend.SolverType} that the subclasses belong to support encoding such constraints. + * solver backend that the subclasses belong to support encoding such constraints. * * @see ConstraintEncoderFactory */ -public abstract class AbstractConstraintEncoderFactory implements ConstraintEncoderFactory{ +public abstract class AbstractConstraintEncoderFactory> + implements ConstraintEncoderFactory{ /** * {@link Lattice} instance that every constraint encoder needs */ protected final Lattice lattice; - public AbstractConstraintEncoderFactory(Lattice lattice) { + /** + * {@link FormatTranslator} instance that concrete subclass of {@link AbstractConstraintEncoder} might need. + * For example, {@link checkers.inference.solver.backend.z3.encoder.Z3BitVectorSubtypeConstraintEncoder} needs + * it to format translate {@SubtypeConstraint}. {@link checkers.inference.solver.backend.maxsat.encoder.MaxSATImplicationConstraintEncoder} + * needs it to delegate format translation task of non-{@code ImplicationConstraint}s. + */ + protected final FormatTranslatorT formatTranslator; + + public AbstractConstraintEncoderFactory(Lattice lattice, FormatTranslatorT formatTranslator) { this.lattice = lattice; + this.formatTranslator = formatTranslator; } } diff --git a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java index 2a3803fd0..5cb031b97 100644 --- a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java +++ b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java @@ -6,11 +6,13 @@ import checkers.inference.model.CombineConstraint; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialConstraint; +import checkers.inference.model.ImplicationConstraint; import checkers.inference.model.PreferenceConstraint; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.BinaryConstraintEncoder; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; import checkers.inference.solver.backend.encoder.existential.ExistentialConstraintEncoder; +import checkers.inference.solver.backend.encoder.implication.ImplicationConstraintEncoder; import checkers.inference.solver.backend.encoder.preference.PreferenceConstraintEncoder; /** @@ -112,4 +114,8 @@ public static ConstraintEncodingT redirect( ExistentialConstraintEncoder encoder) { return encoder.encode(constraint); } + + public static ConstraintEncodingT redirect(ImplicationConstraint constraint, ImplicationConstraintEncoder encoder) { + return encoder.encode(constraint); + } } diff --git a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java index 2755d07f4..a0c451c34 100644 --- a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderFactory.java @@ -6,6 +6,7 @@ import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; import checkers.inference.solver.backend.encoder.existential.ExistentialConstraintEncoder; +import checkers.inference.solver.backend.encoder.implication.ImplicationConstraintEncoder; import checkers.inference.solver.backend.encoder.preference.PreferenceConstraintEncoder; /** @@ -21,6 +22,7 @@ *

  • {@link PreferenceConstraintEncoder}
    • *
  • {@link CombineConstraintEncoder}
    • *
  • {@link ExistentialConstraintEncoder}
    • + *
  • {@link ImplicationConstraintEncoder}
    • *
  • {@link ArithmeticConstraintEncoder}
    • * *

    @@ -45,5 +47,7 @@ public interface ConstraintEncoderFactory { ExistentialConstraintEncoder createExistentialConstraintEncoder(); + ImplicationConstraintEncoder createImplicationConstraintEncoder(); + ArithmeticConstraintEncoder createArithmeticConstraintEncoder(); } diff --git a/src/checkers/inference/solver/backend/encoder/implication/ImplicationConstraintEncoder.java b/src/checkers/inference/solver/backend/encoder/implication/ImplicationConstraintEncoder.java new file mode 100644 index 000000000..6c2301910 --- /dev/null +++ b/src/checkers/inference/solver/backend/encoder/implication/ImplicationConstraintEncoder.java @@ -0,0 +1,13 @@ +package checkers.inference.solver.backend.encoder.implication; + +import checkers.inference.model.ImplicationConstraint; + +/** + * Interface that defines operations to encode a {@link ImplicationConstraint}. + * + * @param solver encoding type for {@link ImplicationConstraint} + */ +public interface ImplicationConstraintEncoder { + + ConstraintEncodingT encode(ImplicationConstraint constraint); +} diff --git a/src/checkers/inference/solver/backend/logiql/LogiQLFormatTranslator.java b/src/checkers/inference/solver/backend/logiql/LogiQLFormatTranslator.java index d7e3b8a75..fb88c0f7e 100644 --- a/src/checkers/inference/solver/backend/logiql/LogiQLFormatTranslator.java +++ b/src/checkers/inference/solver/backend/logiql/LogiQLFormatTranslator.java @@ -10,7 +10,7 @@ /** * LogiQLFormatTranslator converts constraint into string as logiQL data. - * + * * @author jianchu * */ @@ -23,7 +23,7 @@ public LogiQLFormatTranslator(Lattice lattice) { @Override protected ConstraintEncoderFactory createConstraintEncoderFactory() { - return new LogiQLConstraintEncoderFactory(lattice); + return new LogiQLConstraintEncoderFactory(lattice, this); } @Override diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java index fecbf43da..adcfe0ed5 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLConstraintEncoderFactory.java @@ -8,7 +8,9 @@ import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; import checkers.inference.solver.backend.encoder.existential.ExistentialConstraintEncoder; +import checkers.inference.solver.backend.encoder.implication.ImplicationConstraintEncoder; import checkers.inference.solver.backend.encoder.preference.PreferenceConstraintEncoder; +import checkers.inference.solver.backend.logiql.LogiQLFormatTranslator; import checkers.inference.solver.frontend.Lattice; /** @@ -16,10 +18,10 @@ * * @see checkers.inference.solver.backend.encoder.ConstraintEncoderFactory */ -public class LogiQLConstraintEncoderFactory extends AbstractConstraintEncoderFactory { +public class LogiQLConstraintEncoderFactory extends AbstractConstraintEncoderFactory { - public LogiQLConstraintEncoderFactory(Lattice lattice) { - super(lattice); + public LogiQLConstraintEncoderFactory(Lattice lattice, LogiQLFormatTranslator formatTranslator) { + super(lattice, formatTranslator); } @Override @@ -57,6 +59,11 @@ public ExistentialConstraintEncoder createExistentialConstraintEncoder() return null; } + @Override + public ImplicationConstraintEncoder createImplicationConstraintEncoder() { + return null; + } + @Override public ArithmeticConstraintEncoder createArithmeticConstraintEncoder() { return null; diff --git a/src/checkers/inference/solver/backend/maxsat/MaxSatFormatTranslator.java b/src/checkers/inference/solver/backend/maxsat/MaxSatFormatTranslator.java index 010e42111..0725cd54b 100644 --- a/src/checkers/inference/solver/backend/maxsat/MaxSatFormatTranslator.java +++ b/src/checkers/inference/solver/backend/maxsat/MaxSatFormatTranslator.java @@ -58,7 +58,7 @@ public MaxSatFormatTranslator(Lattice lattice) { @Override protected ConstraintEncoderFactory createConstraintEncoderFactory() { - return new MaxSATConstraintEncoderFactory(lattice, typeToInt); + return new MaxSATConstraintEncoderFactory(lattice, typeToInt, this); } /** diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java index bbc232fce..4dcfaf12f 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATConstraintEncoderFactory.java @@ -4,6 +4,8 @@ import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; import checkers.inference.solver.backend.encoder.existential.ExistentialConstraintEncoder; +import checkers.inference.solver.backend.encoder.implication.ImplicationConstraintEncoder; +import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; import checkers.inference.solver.frontend.Lattice; import org.sat4j.core.VecInt; @@ -15,12 +17,13 @@ * * @see checkers.inference.solver.backend.encoder.ConstraintEncoderFactory */ -public class MaxSATConstraintEncoderFactory extends AbstractConstraintEncoderFactory { +public class MaxSATConstraintEncoderFactory extends AbstractConstraintEncoderFactory { private final Map typeToInt; - public MaxSATConstraintEncoderFactory(Lattice lattice, Map typeToInt) { - super(lattice); + public MaxSATConstraintEncoderFactory(Lattice lattice, Map typeToInt, + MaxSatFormatTranslator formatTranslator) { + super(lattice, formatTranslator); this.typeToInt = typeToInt; } @@ -49,6 +52,11 @@ public MaxSATPreferenceConstraintEncoder createPreferenceConstraintEncoder() { return new MaxSATPreferenceConstraintEncoder(lattice, typeToInt); } + @Override + public MaxSATImplicationConstraintEncoder createImplicationConstraintEncoder() { + return new MaxSATImplicationConstraintEncoder(lattice, typeToInt, formatTranslator); + } + @Override public CombineConstraintEncoder createCombineConstraintEncoder() { return null; diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATImplicationConstraintEncoder.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATImplicationConstraintEncoder.java new file mode 100644 index 000000000..1e7a7d4f8 --- /dev/null +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATImplicationConstraintEncoder.java @@ -0,0 +1,152 @@ +package checkers.inference.solver.backend.maxsat.encoder; + +import checkers.inference.model.Constraint; +import checkers.inference.model.ImplicationConstraint; +import checkers.inference.solver.backend.encoder.implication.ImplicationConstraintEncoder; +import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; +import checkers.inference.solver.frontend.Lattice; +import org.sat4j.core.VecInt; + +import javax.lang.model.element.AnnotationMirror; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.Map; + +public class MaxSATImplicationConstraintEncoder + extends MaxSATAbstractConstraintEncoder + implements ImplicationConstraintEncoder { + + /** + * {@link MaxSatFormatTranslator} instance to delegate format translating + * base {@link Constraint}s ({@code Constraint}s that are not + * {@link ImplicationConstraint}). + */ + private final MaxSatFormatTranslator formatTranslator; + + public MaxSATImplicationConstraintEncoder(Lattice lattice, + Map typeToInt, + MaxSatFormatTranslator formatTranslator) { + super(lattice, typeToInt); + this.formatTranslator = formatTranslator; + } + + // High level procedures: + // 1) Format translate all Constraint from assumptions to a list of VecInt: + // [(a|b),(c|d)] + // + // 2) Convert the list in step 1 to a list of list. The sublist is + // essentially a set (should have no duplicates) of variables: [[a,b],[c,d]] + // + // 3) Get the cartesian set(use list for implementation): + // [[a,c],[a,d],[b,c],[b,d]] + // + // 4) Iterate over cartesian set in step 3, create a new VecInt, which is + // composed by this way: negate each variable from each set from cartesian + // set, combine it with every VecInt from conclusion clauses. + // For example, (~a | ~c | h | i), (~a | ~c | j | k), + // (~a | ~d | h | i), (~a | ~d | j | k), (~b | ~c | h | i), + // (~b | ~c | j | k), (~b | ~d | h | i), (~b | ~d | j | k) + // + // 5) Convert the list of VecInt in step 4 to array of VecInt and return it + // as final format translated result. + // + // Note: + // (a | b) & (c | d) => (h | i) & (j | k) is equivalent to cnf form: + // (~a | ~c | h | i) & (~a | ~c | j | k) & (~a | ~d | h | i) & + // (~a | ~d | j | k) & (~b | ~c | h | i) & (~b | ~c | j | k) & + // (~b | ~d | h | i) & (~b | ~d | j | k) + @Override + public VecInt[] encode(ImplicationConstraint constraint) { + + // Step 1 + // A list of VecInts/clauses from lhs of implication, which are + // conjuncted together in cnf + List assumptions = new ArrayList<>(); + for (Constraint a : constraint.getAssumptions()) { + assumptions.addAll(Arrays.asList(a.serialize(formatTranslator))); + } + + // Step 2 + // l is a set of set, in which each subset contains every variable that + // a VecInt contains, for example, l = {{a,b}, {c,d}} + List> l = new ArrayList<>(); + for (VecInt clause : assumptions) { + int[] a = clause.toArray(); + List list = new ArrayList<>(); + for (int each : a) { + list.add(each); + } + l.add(list); + } + + // Step 3 + // cartesian is cartesian set of every variable from different VecInt, + // for example, cartesian = {{a,c}, {a,d}, {b,c}, {b,d}} + // cartesian should have the same length as target array + List> cartesian = cartesianProduct(l); + + // Concatenate with every pair at the end + VecInt[] conclusionClauses = constraint.getConclusion() + .serialize(formatTranslator); + + int expectedSize = cartesian.size() * conclusionClauses.length; + + List serializedTemp = new ArrayList<>(); + + // Step 4 + for (int i = 0; i < cartesian.size(); i++) { + for (int j = 0; j < conclusionClauses.length; j++) { + List toNegate = cartesian.get(i); + VecInt targetClause = new VecInt(); + for (Integer var : toNegate) { + // Push the negation, of variable because it's from lhs + // assumption for example, they are {!a, !c} and {!a,!d} and + // {!b, !c} and {!b, !d} + targetClause.push(-var); + } + targetClause.pushAll(conclusionClauses[j]); + serializedTemp.add(targetClause); + } + } + + assert serializedTemp.size() == expectedSize; + + // Step 5 + VecInt[] finalSerializedResult = new VecInt[expectedSize]; + return serializedTemp.toArray(finalSerializedResult); + } + + /** + * Method to get cartesian set of input set. + * + * For example, if the input is [[1,2], [3,4,5]], this method returns + * [[1,3],[1,4],[1,5],[2,3],[2,4],[2,5]] + * + * @param lists + * a set of set of elements + * @param + * type of element + * @return cartesian set of elements + */ + protected List> cartesianProduct(List> lists) { + List> resultLists = new ArrayList>(); + if (lists.size() == 0) { + resultLists.add(new ArrayList()); + return resultLists; + } else { + List firstList = lists.get(0); + List> remainingLists = cartesianProduct( + lists.subList(1, lists.size())); + for (T condition : firstList) { + for (List remainingList : remainingLists) { + ArrayList resultList = new ArrayList(); + resultList.add(condition); + resultList.addAll(remainingList); + resultLists.add(resultList); + } + } + } + return resultLists; + } +} diff --git a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java index c775494e9..3d8c3dc1d 100644 --- a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java +++ b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorConstraintEncoderFactory.java @@ -7,6 +7,7 @@ import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; import checkers.inference.solver.backend.encoder.existential.ExistentialConstraintEncoder; +import checkers.inference.solver.backend.encoder.implication.ImplicationConstraintEncoder; import checkers.inference.solver.backend.encoder.preference.PreferenceConstraintEncoder; import checkers.inference.solver.backend.z3.Z3BitVectorFormatTranslator; import checkers.inference.solver.frontend.Lattice; @@ -18,26 +19,24 @@ * * @see checkers.inference.solver.backend.encoder.ConstraintEncoderFactory */ -public class Z3BitVectorConstraintEncoderFactory extends AbstractConstraintEncoderFactory{ +public class Z3BitVectorConstraintEncoderFactory extends AbstractConstraintEncoderFactory{ protected final Context context; - protected final Z3BitVectorFormatTranslator z3BitVectorFormatTranslator; public Z3BitVectorConstraintEncoderFactory(Lattice lattice, Context context, - Z3BitVectorFormatTranslator z3BitVectorFormatTranslator) { - super(lattice); + Z3BitVectorFormatTranslator formatTranslator) { + super(lattice, formatTranslator); this.context = context; - this.z3BitVectorFormatTranslator = z3BitVectorFormatTranslator; } @Override public Z3BitVectorSubtypeConstraintEncoder createSubtypeConstraintEncoder() { - return new Z3BitVectorSubtypeConstraintEncoder(lattice, context, z3BitVectorFormatTranslator); + return new Z3BitVectorSubtypeConstraintEncoder(lattice, context, formatTranslator); } @Override public EqualityConstraintEncoder createEqualityConstraintEncoder() { - return new Z3BitVectorEqualityConstraintEncoder(lattice, context, z3BitVectorFormatTranslator); + return new Z3BitVectorEqualityConstraintEncoder(lattice, context, formatTranslator); } @Override @@ -53,7 +52,7 @@ public ComparableConstraintEncoder createComparableConstraintEncoder() @Override public PreferenceConstraintEncoder createPreferenceConstraintEncoder() { - return new Z3BitVectorPreferenceConstraintEncoder(lattice, context, z3BitVectorFormatTranslator); + return new Z3BitVectorPreferenceConstraintEncoder(lattice, context, formatTranslator); } @Override @@ -66,6 +65,11 @@ public ExistentialConstraintEncoder createExistentialConstraintEncoder return null; } + @Override + public ImplicationConstraintEncoder createImplicationConstraintEncoder() { + return null; + } + @Override public ArithmeticConstraintEncoder createArithmeticConstraintEncoder() { return null; diff --git a/src/checkers/inference/solver/util/PrintUtils.java b/src/checkers/inference/solver/util/PrintUtils.java index 84e6a9668..b4c07852f 100644 --- a/src/checkers/inference/solver/util/PrintUtils.java +++ b/src/checkers/inference/solver/util/PrintUtils.java @@ -24,6 +24,7 @@ import checkers.inference.model.EqualityConstraint; import checkers.inference.model.ExistentialConstraint; import checkers.inference.model.ExistentialVariableSlot; +import checkers.inference.model.ImplicationConstraint; import checkers.inference.model.InequalityConstraint; import checkers.inference.model.LubVariableSlot; import checkers.inference.model.PreferenceConstraint; @@ -286,6 +287,15 @@ public Void serialize(PreferenceConstraint constraint) { return null; } + @Override + public Void serialize(ImplicationConstraint constraint) { + for (Constraint assumption : constraint.getAssumptions()) { + assumption.serialize(this); + } + constraint.getConclusion().serialize(this); + return null; + } + @Override public Void serialize(ArithmeticConstraint constraint) { constraint.getLeftOperand().serialize(this);