Add EncodingUtils class

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java

@@ -532,10 +532,9 @@ public BooleanFormula encodeDependencies() {
 
     public BooleanFormula encodeFilter() {
         final Expression filterSpec = context.getTask().getProgram().getFilterSpecification();
-        if (!ignoreFilterSpec && filterSpec != null) {
-            return context.getExpressionEncoder().encodeBooleanFinal(filterSpec).formula();
-        }
-        return context.getBooleanFormulaManager().makeTrue();
+        return ignoreFilterSpec
+                ? context.getBooleanFormulaManager().makeTrue()
+                : context.getExpressionEncoder().encodeBooleanFinal(filterSpec).formula();
     }
 
     public BooleanFormula encodeFinalRegisterValues() {

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java

@@ -5,13 +5,14 @@
 import com.dat3m.dartagnan.program.analysis.ThreadSymmetry;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent;
+import com.dat3m.dartagnan.smt.EncodingUtils;
 import com.dat3m.dartagnan.utils.equivalence.EquivalenceClass;
 import com.dat3m.dartagnan.wmm.Wmm;
 import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis;
 import com.dat3m.dartagnan.wmm.axiom.Axiom;
+import com.dat3m.dartagnan.wmm.utils.Tuple;
 import com.dat3m.dartagnan.wmm.utils.graph.EventGraph;
 import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph;
-import com.dat3m.dartagnan.wmm.utils.Tuple;
 import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph;
 import com.google.common.base.Preconditions;
 import org.apache.logging.log4j.LogManager;
@@ -72,12 +73,12 @@ private SymmetryEncoder(EncodingContext c, Configuration config) throws InvalidC
             c.getAnalysisContext().requires(BranchEquivalence.class);
             this.breakBySyncDegree = false; // We cannot break by sync degree here
         } else {
-            logger.info("Breaking symmetry on relation: " + symmBreakTarget);
+            logger.info("Breaking symmetry on relation: {}", symmBreakTarget);
             if (breakBySyncDegree && acycAxioms.isEmpty()) {
                 breakBySyncDegree = false;
                 logger.info("Disabled breaking by sync degree: Memory model has no acyclicity axioms.");
             }
-            logger.info("Breaking by sync degree: " + breakBySyncDegree);
+            logger.info("Breaking by sync degree: {}", breakBySyncDegree);
         }
     }
 
@@ -128,15 +129,17 @@ private BooleanFormula encodeSymmetryBreakingOnClass(EventGraph maySet, Encoding
 
         // Construct symmetric rows
         List<BooleanFormula> enc = new ArrayList<>();
+        final EncodingUtils utils = context.getFormulaManager().getEncodingUtils();
         for (int i = 1; i < symmThreads.size(); i++) {
-            Thread t2 = symmThreads.get(i);
-            Function<Event, Event> p = symm.createEventTransposition(t1, t2);
-            List<Tuple> t2Tuples = t1Tuples.stream().map(t -> new Tuple(p.apply(t.first()), p.apply(t.second()))).toList();
+            final Thread t2 = symmThreads.get(i);
+            final Function<Event, Event> p = symm.createEventTransposition(t1, t2);
+            final List<Tuple> t2Tuples = t1Tuples.stream().map(t -> new Tuple(p.apply(t.first()), p.apply(t.second()))).toList();
+
+            final List<BooleanFormula> r1 = t1Tuples.stream().map(t -> edge.encode(t.first(), t.second())).toList();
+            final List<BooleanFormula> r2 = t2Tuples.stream().map(t -> edge.encode(t.first(), t.second())).toList();
+            final String id = String.format("T%d_%d", rep.getId(), i);
+            enc.add(utils.encodeLexLeader(r2, r1, id)); // r1 >= r2
 
-            List<BooleanFormula> r1 = t1Tuples.stream().map(t -> edge.encode(t.first(), t.second())).toList();
-            List<BooleanFormula> r2 = t2Tuples.stream().map(t -> edge.encode(t.first(), t.second())).toList();
-            final String id = "_" + rep.getId() + "_" + i;
-            enc.add(encodeLexLeader(id, r2, r1, context)); // r1 >= r2
             t1 = t2;
             t1Tuples = t2Tuples;
         }
@@ -194,58 +197,6 @@ private void sort(List<Tuple> row) {
         row.sort(Comparator.<Tuple>comparingInt(t -> combinedInDegree.get(t.first()) * combinedOutDegree.get(t.second())).reversed());
     }
 
-    // ========================= Static utility ===========================
-
-    /*
-        Encodes that any assignment obeys "r1 <= r2" where the order is
-        the lexicographic order based on "false < true".
-        In other words, for all assignments to the variables of r1/r2,
-        the first time r1(i) and r2(i) get different truth values,
-        we will have r1(i) = FALSE and r2(i) = TRUE.
-
-        NOTE: Creates extra variables named "yi_<uniqueIdent>" which can cause conflicts if
-              <uniqueIdent> is not uniquely used.
-    */
-    public static BooleanFormula encodeLexLeader(String uniqueIdent, List<BooleanFormula> r1, List<BooleanFormula> r2, EncodingContext context) {
-        Preconditions.checkArgument(r1.size() == r2.size());
-        final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
-        // Return TRUE if there is nothing to encode
-        if(r1.isEmpty()) {
-            return bmgr.makeTrue();
-        }
-        final int size = r1.size();
-        final String suffix = "_" + uniqueIdent;
-
-        // We interpret the variables of <ri> as x1(ri), ..., xn(ri).
-        // We create helper variables y0_suffix, ..., y(n-1)_suffix (note the index shift compared to xi)
-        // xi gets related to y(i-1) and yi
-
-        BooleanFormula ylast = bmgr.makeVariable("y0" + suffix); // y(i-1)
-        List<BooleanFormula> enc = new ArrayList<>();
-        enc.add(ylast);
-        // From x1 to x(n-1)
-        for (int i = 1; i < size; i++) {
-            BooleanFormula y = bmgr.makeVariable("y" + i + suffix); // yi
-            BooleanFormula a = r1.get(i-1); // xi(r1)
-            BooleanFormula b = r2.get(i-1); // xi(r2)
-            enc.add(bmgr.or(y, bmgr.not(ylast), bmgr.not(a))); // (see below)
-            enc.add(bmgr.or(y, bmgr.not(ylast), b));           // "y(i-1) implies ((xi(r1) >= xi(r2))  =>  yi)"
-            enc.add(bmgr.or(bmgr.not(ylast), bmgr.not(a), b)); // "y(i-1) implies (xi(r1) <= xi(r2))"
-                    // NOTE: yi = TRUE means the prefixes (x1, x2, ..., xi) of the rows r1/r2 are equal
-                    //       yi = FALSE means that no conditions are imposed on xi
-                    // The first point, where y(i-1) is TRUE but yi is FALSE, is the breaking point
-                    // where xi(r1) < xi(r2) holds (afterwards all yj (j >= i+1) are unconstrained and can be set to
-                    // FALSE by the solver)
-            ylast = y;
-        }
-        // Final iteration for xn is handled differently as there is no variable yn anymore.
-        BooleanFormula a = r1.get(size-1);
-        BooleanFormula b = r2.get(size-1);
-        enc.add(bmgr.or(bmgr.not(ylast), bmgr.not(a), b));
-
-        return bmgr.and(enc);
-    }
-
     private EventGraph cfSet() {
         final BranchEquivalence branchEq = context.getAnalysisContext().requires(BranchEquivalence.class);
         MutableEventGraph cfSet = new MapEventGraph();

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java

@@ -7,6 +7,7 @@
 import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis;
 import com.dat3m.dartagnan.program.event.*;
 import com.dat3m.dartagnan.program.event.core.*;
+import com.dat3m.dartagnan.smt.EncodingUtils;
 import com.dat3m.dartagnan.smt.ModelExt;
 import com.dat3m.dartagnan.utils.Utils;
 import com.dat3m.dartagnan.utils.dependable.DependencyGraph;
@@ -25,6 +26,7 @@
 import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph;
 import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph;
 import com.google.common.collect.Iterables;
+import com.google.common.collect.Lists;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
@@ -41,7 +43,6 @@
 import static com.dat3m.dartagnan.configuration.OptionNames.*;
 import static com.dat3m.dartagnan.encoding.ExpressionEncoder.ConversionMode.LEFT_TO_RIGHT;
 import static com.dat3m.dartagnan.program.event.Tag.*;
-import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF;
 import static com.google.common.base.Verify.verify;
 
 @Options
@@ -635,40 +636,38 @@ public Void visitSameLocation(SameLocation locDef) {
         public Void visitReadFrom(ReadFrom rfDef) {
             final ExpressionEncoder exprEncoder = context.getExpressionEncoder();
             final Relation rf = rfDef.getDefinedRelation();
-            Map<MemoryEvent, List<BooleanFormula>> edgeMap = new HashMap<>();
             final EncodingContext.EdgeEncoder edge = context.edge(rf);
+            final EncodingUtils utils = context.getFormulaManager().getEncodingUtils();
+
+            final Map<MemoryEvent, List<BooleanFormula>> read2RfEdges = new HashMap<>();
+            // Encode the semantics of rf-edges
             ra.getKnowledge(rf).getMaySet().apply((e1, e2) -> {
                 final MemoryCoreEvent w = (MemoryCoreEvent) e1;
                 final MemoryCoreEvent r = (MemoryCoreEvent) e2;
 
-                BooleanFormula e = edge.encode(w, r);
-                BooleanFormula sameAddress = context.sameAddress(w, r);
-                BooleanFormula sameValue = context.sameValue(w, r, LEFT_TO_RIGHT);
-                edgeMap.computeIfAbsent(r, key -> new ArrayList<>()).add(e);
-                enc.add(bmgr.implication(e, bmgr.and(execution(w, r), sameAddress, sameValue)));
+                final BooleanFormula rfEdge = edge.encode(w, r);
+                final BooleanFormula sameAddress = context.sameAddress(w, r);
+                final BooleanFormula sameValue = context.sameValue(w, r, LEFT_TO_RIGHT);
+                enc.add(bmgr.implication(rfEdge, bmgr.and(execution(w, r), sameAddress, sameValue)));
+
+                read2RfEdges.computeIfAbsent(r, key -> new ArrayList<>()).add(rfEdge);
             });
+
+            // Encode the existence of rf-edges (+ semantics of uninit reads)
             for (Load r : program.getThreadEvents(Load.class)) {
                 final BooleanFormula uninit = getUninitReadVar(r);
                 if (memoryIsZeroed) {
                     final Expression zero = context.getExpressionFactory().makeGeneralZero(r.getAccessType());
                     enc.add(bmgr.implication(uninit, exprEncoder.equal(context.value(r), zero)));
                 }
 
-                final List<BooleanFormula> rfEdges = edgeMap.getOrDefault(r, List.of());
-                if (allowMultiReads) {
-                    enc.add(bmgr.implication(context.execution(r), bmgr.or(bmgr.or(rfEdges), uninit)));
-                    continue;
-                }
-
-                String rPrefix = "s(" + RF + ",E" + r.getGlobalId() + ",";
-                BooleanFormula lastSeqVar = uninit;
-                for (int i = 0; i < rfEdges.size(); i++) {
-                    BooleanFormula newSeqVar = bmgr.makeVariable(rPrefix + i + ")");
-                    enc.add(bmgr.equivalence(newSeqVar, bmgr.or(lastSeqVar, rfEdges.get(i))));
-                    enc.add(bmgr.not(bmgr.and(rfEdges.get(i), lastSeqVar)));
-                    lastSeqVar = newSeqVar;
-                }
-                enc.add(bmgr.implication(context.execution(r), lastSeqVar));
+                final List<BooleanFormula> rfChoices = Lists.newArrayList(Iterables.concat(
+                        List.of(uninit), read2RfEdges.getOrDefault(r, List.of())
+                ));
+                final BooleanFormula rfExistenceConstraint = allowMultiReads
+                        ? utils.atLeastOne(rfChoices)
+                        : utils.exactlyOneSequence(rfChoices, "rf_E" + r.getGlobalId());
+                enc.add(bmgr.implication(context.execution(r), rfExistenceConstraint));
             }
             return null;
         }

dartagnan/src/main/java/com/dat3m/dartagnan/smt/EncodingUtils.java

@@ -0,0 +1,113 @@
+package com.dat3m.dartagnan.smt;
+
+import com.google.common.base.Preconditions;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.BooleanFormulaManager;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.List;
+
+public class EncodingUtils {
+
+    private final FormulaManagerExt fmgr;
+
+    EncodingUtils(FormulaManagerExt fmgr) {
+        this.fmgr = fmgr;
+    }
+
+    // -----------------------------------------------------------------------------------------------
+    // Cardinality constraints
+
+    public BooleanFormula atLeastOne(Collection<BooleanFormula> formulas) {
+        return fmgr.getBooleanFormulaManager().or(formulas);
+    }
+
+    public BooleanFormula atMostOnePairwise(List<BooleanFormula> formulas) {
+        final BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager();
+        final List<BooleanFormula> enc = new ArrayList<>(formulas.size() * (formulas.size() - 1) / 2);
+        for (int i = 0; i < formulas.size(); i++) {
+            for (int j = i + 1; j < formulas.size(); j++) {
+                enc.add(bmgr.or(bmgr.not(formulas.get(i)), bmgr.not(formulas.get(j))));
+            }
+        }
+        return bmgr.and(enc);
+    }
+
+    // NOTE: This method generates helper variables using <uniqueIdent>, so the user must ensure
+    // that the identifier is unique.
+    public BooleanFormula exactlyOneSequence(List<BooleanFormula> formulas, String uniqueIdent) {
+        final BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager();
+        if (formulas.size() <= 1) {
+            return atLeastOne(formulas);
+        }
+
+        final String seqVarName = "seqVar_" + uniqueIdent + "#";
+        final List<BooleanFormula> enc = new ArrayList<>(2*formulas.size() - 1);
+        BooleanFormula lastSeqVar = formulas.get(0);
+        for (int i = 1; i < formulas.size(); i++) {
+            final BooleanFormula newSeqVar = bmgr.makeVariable(seqVarName + i);
+            enc.add(bmgr.equivalence(newSeqVar, bmgr.or(lastSeqVar, formulas.get(i))));
+            enc.add(bmgr.not(bmgr.and(formulas.get(i), lastSeqVar)));
+            lastSeqVar = newSeqVar;
+        }
+        enc.add(lastSeqVar); // NOTE: without this line, we get an at-most-one encoding
+
+        return bmgr.and(enc);
+    }
+
+    // -----------------------------------------------------------------------------------------------
+    // Symmetry constraints
+
+    /*
+        Encodes that any assignment obeys "r1 <= r2" where the order is
+        the lexicographic order based on "false < true".
+        In other words, for all assignments to the variables of r1/r2,
+        the first time r1(i) and r2(i) get different truth values,
+        we will have r1(i) = FALSE and r2(i) = TRUE.
+
+        NOTE: This method generates helper variables using <uniqueIdent>, so the user must ensure
+              that the identifier is unique.
+    */
+    public BooleanFormula encodeLexLeader(List<BooleanFormula> r1, List<BooleanFormula> r2, String uniqueIdent) {
+        Preconditions.checkArgument(r1.size() == r2.size());
+        final BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager();
+        // Return TRUE if there is nothing to encode
+        if (r1.isEmpty()) {
+            return bmgr.makeTrue();
+        }
+        final int size = r1.size();
+        final String helperVarName = "y_" + uniqueIdent + "#";
+
+        // We interpret the variables of <ri> as x1(ri), ..., xn(ri).
+        // We create helper variables y0, ..., y(n-1) (note the index shift compared to xi)
+        // xi gets related to y(i-1) and yi
+
+        final List<BooleanFormula> enc = new ArrayList<>(3 * size);
+        BooleanFormula ylast = bmgr.makeVariable(helperVarName + 0); // y(i-1)
+        enc.add(ylast);
+        // From x1 to x(n-1)
+        for (int i = 1; i < size; i++) {
+            final BooleanFormula y = bmgr.makeVariable(helperVarName + i); // yi
+            final BooleanFormula a = r1.get(i - 1); // xi(r1)
+            final BooleanFormula b = r2.get(i - 1); // xi(r2)
+            enc.add(bmgr.or(y, bmgr.not(ylast), bmgr.not(a))); // (see below)
+            enc.add(bmgr.or(y, bmgr.not(ylast), b));           // "y(i-1) implies ((xi(r1) >= xi(r2))  =>  yi)"
+            enc.add(bmgr.or(bmgr.not(ylast), bmgr.not(a), b)); // "y(i-1) implies (xi(r1) <= xi(r2))"
+            // NOTE: yi = TRUE means the prefixes (x1, x2, ..., xi) of the rows r1/r2 are equal
+            //       yi = FALSE means that no conditions are imposed on xi
+            // The first point, where y(i-1) is TRUE but yi is FALSE, is the breaking point
+            // where xi(r1) < xi(r2) holds (afterwards all yj (j >= i+1) are unconstrained and can be set to
+            // FALSE by the solver)
+            ylast = y;
+        }
+        // Final iteration for xn is handled differently as there is no variable yn anymore.
+        final BooleanFormula a = r1.get(size - 1);
+        final BooleanFormula b = r2.get(size - 1);
+        enc.add(bmgr.or(bmgr.not(ylast), bmgr.not(a), b));
+
+        return bmgr.and(enc);
+    }
+
+
+}

dartagnan/src/main/java/com/dat3m/dartagnan/smt/FormulaManagerExt.java

@@ -16,10 +16,12 @@ public class FormulaManagerExt {
 
     private final FormulaManager fmgr;
     private final TupleFormulaManager tmgr;
+    private final EncodingUtils encUtils;
 
     public FormulaManagerExt(FormulaManager fmgr) {
         this.fmgr = fmgr;
         this.tmgr = new TupleFormulaManager(this);
+        this.encUtils = new EncodingUtils(this);
     }
 
     public FormulaManager getUnderlyingFormulaManager() { return fmgr; }
@@ -38,6 +40,8 @@ public String escape(String varName) {
     // ====================================================================================================
     // Utility
 
+    public EncodingUtils getEncodingUtils() { return encUtils; }
+
     public boolean hasSameType(Formula left, Formula right) {
         if (left instanceof NumeralFormula.IntegerFormula && right instanceof NumeralFormula.IntegerFormula) {
             return true;

dartagnan/src/main/java/com/dat3m/dartagnan/utils/symmetry/CoSymmetryBreaking.java

@@ -1,12 +1,12 @@
 package com.dat3m.dartagnan.utils.symmetry;
 
 import com.dat3m.dartagnan.encoding.EncodingContext;
-import com.dat3m.dartagnan.encoding.SymmetryEncoder;
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.analysis.ThreadSymmetry;
 import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.core.Store;
+import com.dat3m.dartagnan.smt.EncodingUtils;
 import com.dat3m.dartagnan.utils.equivalence.EquivalenceClass;
 import com.dat3m.dartagnan.verification.VerificationTask;
 import com.dat3m.dartagnan.wmm.Relation;
@@ -223,6 +223,7 @@ public BooleanFormula encode(EquivalenceClass<Thread> symmClass) {
             r1.add(edge.encode(t.first(), t.second()));
         }
         // Construct symmetric rows
+        final EncodingUtils utils = context.getFormulaManager().getEncodingUtils();
         List<BooleanFormula> enc = new ArrayList<>();
         Thread rep = symmClass.getRepresentative();
         for (int i = 1; i < symmThreads.size(); i++) {
@@ -237,9 +238,8 @@ public BooleanFormula encode(EquivalenceClass<Thread> symmClass) {
                 r2.add(edge.encode(t.first(), t.second()));
             }
 
-            final String id = "_" + rep.getId() + "_" + i;
-            // NOTE: We want to have r1 >= r2 but lexLeader encodes r1 <= r2, so we swap r1 and r2.
-            enc.add(SymmetryEncoder.encodeLexLeader(id, r2, r1, context));
+            final String id = String.format("T%d_%d", rep.getId(), i);
+            enc.add(utils.encodeLexLeader(r2, r1, id)); // r1 >= r2
 
             t1 = t2;
             r1Tuples = r2Tuples;