Merge branch 'master' of https://github.com/opprop/checker-framework-…

…inference into unsat-verify

src/checkers/inference/model/serialization/CnfVecIntSerializer.java

@@ -8,6 +8,7 @@
 import checkers.inference.model.LubVariableSlot;
 import checkers.inference.model.ImplicationConstraint;
 import checkers.inference.model.VariableSlot;
+import org.checkerframework.javacutil.BugInCF;
 import org.sat4j.core.VecInt;
 
 import checkers.inference.SlotManager;
@@ -288,12 +289,37 @@ public VecInt[] serialize(ImplicationConstraint implicationConstraint) {
                 "MaxSAT backend. Use MaxSATSolver instead!");
     }
 
+    /**
+     * Convert all the given mandatory constraints into hard clauses. A BugInCF exception is
+     * raised if the given constraints contain any {@link PreferenceConstraint}.
+     *
+     * For conversion of constraints containing {@link PreferenceConstraint}, use
+     * {@link CnfVecIntSerializer#convertAll(Iterable, List, List)}
+     *
+     * @param constraints the constraints to convert
+     * @return the output clauses for the given constraints
+     */
     public List<VecInt> convertAll(Iterable<Constraint> constraints) {
         return convertAll(constraints, new LinkedList<VecInt>());
     }
 
+    /**
+     * Convert all the given mandatory constraints into hard clauses. A BugInCF exception is
+     * raised if the given constraints contains any {@link PreferenceConstraint}.
+     *
+     * For conversion of constraints containing {@link PreferenceConstraint}, use
+     * {@link CnfVecIntSerializer#convertAll(Iterable, List, List)}
+     *
+     * @param constraints the constraints to convert
+     * @param results the output clauses for the given constraints
+     * @return same as {@code results}
+     */
     public List<VecInt> convertAll(Iterable<Constraint> constraints, List<VecInt> results) {
         for (Constraint constraint : constraints) {
+            if (constraint instanceof PreferenceConstraint) {
+                throw new BugInCF("CnfVecIntSerializer: adding PreferenceConstraint ( " + constraint +
+                        " ) to hard clauses is forbidden");
+            }
             for (VecInt res : constraint.serialize(this)) {
                 if (res.size() != 0) {
                     results.add(res);
@@ -304,6 +330,28 @@ public List<VecInt> convertAll(Iterable<Constraint> constraints, List<VecInt> re
         return results;
     }
 
+    /**
+     * Convert all the given mandatory constraints to hard clauses, and preference constraints
+     * to soft clauses.
+     *
+     * @param constraints the constraints to convert
+     * @param hardClauses the output hard clauses for the mandatory constraints
+     * @param softClauses the output soft clauses for {@link PreferenceConstraint}
+     */
+    public void convertAll(Iterable<Constraint> constraints, List<VecInt> hardClauses, List<VecInt> softClauses) {
+        for (Constraint constraint : constraints) {
+            for (VecInt res : constraint.serialize(this)) {
+                if (res.size() != 0) {
+                    if (constraint instanceof PreferenceConstraint) {
+                        softClauses.add(res);
+                    } else {
+                        hardClauses.add(res);
+                    }
+                }
+            }
+        }
+    }
+
     protected abstract boolean isTop(ConstantSlot constantSlot);
 
     VecInt asVec(int ... vars) {

src/checkers/inference/solver/MaxSat2TypeSolver.java

@@ -7,6 +7,8 @@
 
 import java.util.Collection;
 import java.util.HashMap;
+import java.util.HashSet;
+import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
 
@@ -23,6 +25,8 @@
 import checkers.inference.model.Constraint;
 import checkers.inference.model.Slot;
 import checkers.inference.model.serialization.CnfVecIntSerializer;
+import org.sat4j.specs.ContradictionException;
+import org.sat4j.specs.TimeoutException;
 
 /**
  * This solver is used to convert any constraint set using a type system with only 2 types (Top/Bottom),
@@ -69,9 +73,10 @@ protected boolean isTop(ConstantSlot constantSlot) {
     }
 
     public InferenceResult solve() {
-        final Map<Integer, AnnotationMirror> solutions = new HashMap<>();
 
-        final List<VecInt> clauses = serializer.convertAll(constraints);
+        final List<VecInt> softClauses = new LinkedList<>();
+        final List<VecInt> hardClauses = new LinkedList<>();
+        serializer.convertAll(constraints, hardClauses, softClauses);
 
         // nextId describes the LARGEST id that might be found in a variable
         // if an exception occurs while creating a variable the id might be incremented
@@ -82,7 +87,7 @@ public InferenceResult solve() {
         // TODO: thus here the value of totalVars is the real slots number stored in slotManager, and plus the
         // TODO: "fake" slots number stored in existentialToPotentialVar
         final int totalVars = slotManager.getNumberOfSlots() + serializer.getExistentialToPotentialVar().size();
-        final int totalClauses =  clauses.size();
+        final int totalClauses = hardClauses.size() + softClauses.size();
 
 
         // When .newBoth is called, SAT4J will run two solvers and return the result of the first to halt
@@ -96,42 +101,69 @@ public InferenceResult solve() {
 
         VecInt lastClause = null;
         try {
-            for (VecInt clause : clauses) {
+            for (VecInt clause : hardClauses) {
+                lastClause = clause;
+                solver.addHardClause(clause);
+            }
+            for (VecInt clause : softClauses) {
 
                 lastClause = clause;
                 solver.addSoftClause(clause);
             }
 
-            // isSatisfiable launches the solvers and waits until one of them finishes
-            if (solver.isSatisfiable()) {
-                final Map<Integer, Integer> existentialToPotentialIds = serializer.getExistentialToPotentialVar();
-                int[] solution = solver.model();
-
-                for (Integer var : solution) {
-                    boolean isTop = var < 0;
-                    if (isTop) {
-                        var = -var;
-                    }
-
-                    Integer potential = existentialToPotentialIds.get(var);
-                    if (potential != null) {
-                        // idToExistence.put(potential, !isTop);
-                        // TODO: which AnnotationMirror should be used?
-                        solutions.put(potential, bottom);
-                    } else {
-                        solutions.put(var, isTop ? top : bottom );
-                    }
+        } catch (ContradictionException ce) {
+            // This happens when adding a clause causes trivial contradiction, such as adding -1 to {1}
+            System.out.println("Not solvable! Contradiction exception " +
+                    "when adding clause: " + lastClause + ".");
+
+            // pass empty set as the unsat explanation
+            // TODO: explain UNSAT possibly by reusing MaxSatSolver.MaxSATUnsatisfiableConstraintExplainer
+            return new DefaultInferenceResult(new HashSet<>());
+        }
 
+        boolean isSatisfiable;
+        try {
+            // isSatisfiable() launches the solvers and waits until one of them finishes
+            isSatisfiable = solver.isSatisfiable();
+
+        } catch(TimeoutException te) {
+            throw new RuntimeException("MAX-SAT solving timeout! ");
+        }
+
+        if (!isSatisfiable) {
+            System.out.println("Not solvable!");
+            // pass empty set as the unsat explanation
+            // TODO: explain UNSAT possibly by reusing MaxSatSolver.MaxSATUnsatisfiableConstraintExplainer
+            return new DefaultInferenceResult(new HashSet<>());
+        }
+
+        int[] solution = solver.model();
+        // The following code decodes VecInt solution to the slot-annotation mappings
+        final Map<Integer, AnnotationMirror> decodedSolution = new HashMap<>();
+        final Map<Integer, Integer> existentialToPotentialIds = serializer.getExistentialToPotentialVar();
+
+        for (Integer var : solution) {
+            Integer potential = existentialToPotentialIds.get(Math.abs(var));
+            if (potential != null) {
+                // Assume the 'solution' output by the solver is already sorted in the ascending order
+                // of their absolute values. So the existential variables come after the potential variables,
+                // which means the potential slot corresponding to the current existential variable is
+                // already inserted into 'solutions'
+                assert decodedSolution.containsKey(potential);
+                if (var < 0) {
+                    // The existential variable is false, so the potential variable should not be inserted.
+                    // Remove it from the solution.
+                    decodedSolution.remove(potential);
                 }
             } else {
-                System.out.println("Not solvable!");
+                boolean isTop = var < 0;
+                if (isTop) {
+                    var = -var;
+                }
+                decodedSolution.put(var, isTop ? top : bottom);
             }
-
-        } catch(Throwable th) {
-           throw new RuntimeException("Error MAX-SAT solving! " + lastClause, th);
         }
 
-
-        return new DefaultInferenceResult(solutions);
+        return new DefaultInferenceResult(decodedSolution);
     }
 }