Output for electrod,annotation use for services

AlloyTools · Mar 14, 2024 · 78664c5 · 78664c5
1 parent 051a0c4
commit 78664c5
Show file tree

Hide file tree

Showing 25 changed files with 463 additions and 220 deletions.
diff --git a/cnf/central.mvn b/cnf/central.mvn
@@ -1,4 +1,5 @@
 biz.aQute.bnd:aQute.libg:6.0.0
+biz.aQute.bnd:biz.aQute.bnd.annotation:6.0.0
 biz.aQute:biz.aQute.wrapper.hamcrest:1.3
 biz.aQute:biz.aQute.wrapper.junit:4.13.1
 com.google.code.gson:gson:2.8.9

diff --git a/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CLI.java b/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CLI.java
@@ -194,7 +194,7 @@ public void _exec(ExecOptions options) throws Exception {
 					info.command = c;
 					info.sequence = sequence++;
 					info.durationInMs = TimeUnit.NANOSECONDS.toMillis(finish - start);
-					if (opt.solver == SATFactory.CNF || opt.solver == SATFactory.KK)
+					if (opt.solver.isTransformer())
 						info.cnf = rep.output;
 					answers.put(info, s);
 					System.out.println("answers " + answers.size());
@@ -205,7 +205,7 @@ public void _exec(ExecOptions options) throws Exception {
 			stdout.println("no commands found " + cmd);
 		}
 
-		if (opt.solver == SATFactory.CNF || opt.solver == SATFactory.KK) {
+		if (opt.solver.isTransformer()) {
 			for (CommandInfo c : answers.keySet()) {
 				IO.copy(c.cnf, out);
 			}

diff --git a/org.alloytools.alloy.core/bnd.bnd b/org.alloytools.alloy.core/bnd.bnd
@@ -9,7 +9,8 @@
 	aQute.libg,\
 	org.alloytools.api,\
 	slf4j.api,\
-	org.alloytools.pardinus.core
+	org.alloytools.pardinus.core,\
+	biz.aQute.bnd.annotation
 
 -testpath: \
 	biz.aQute.wrapper.junit,\

diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Options.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Options.java
@@ -15,7 +15,10 @@
 
 package edu.mit.csail.sdg.translator;
 
+import java.io.File;
+import java.io.IOException;
 import java.io.Serializable;
+import java.nio.file.Files;
 
 import kodkod.engine.satlab.SATFactory;
 
@@ -163,4 +166,9 @@ public A4Options dup() {
         return x;
     }
 
+    public File tempFile(String extension) throws IOException {
+        File f = new File(tempDirectory);
+        return Files.createTempFile(f.toPath(), "alloy", extension).toFile();
+    }
+
 }
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java
@@ -1156,6 +1156,8 @@ void kr2typeCLEAR() throws Err {
     /** Caches a constant pair of Type.EMPTY and Pos.UNKNOWN */
     private Pair<Type,Pos> cachedPAIR = null;
 
+    private Formula        fgoal;
+
     /**
      * Maps a Kodkod variable to an Alloy Type and Alloy Pos (if no association
      * exists, it will return (Type.EMPTY , Pos.UNKNOWN)
@@ -1553,10 +1555,9 @@ A4Solution solve(final A4Reporter rep, Command cmd, Simplifier simp, boolean try
         if (opt.inferPartialInstance && simp != null && formulas.size() > 0 && !simp.simplify(rep, this, formulas))
             addFormula(Formula.FALSE, Pos.UNKNOWN);
         rep.translate(opt.solver.id(), bitwidth, maxseq, mintrace, maxtrace, solver.options().skolemDepth(), solver.options().symmetryBreaking(), A4Preferences.Decompose.values()[opt.decompose_mode].toString());
-        Formula fgoal = Formula.and(formulas);
+        fgoal = Formula.and(formulas);
         rep.debug("Generating the solution...\n");
         kEnumerator = null;
-        Solution sol = null;
         final Reporter oldReporter = solver.options().reporter();
         final boolean solved[] = new boolean[] {
                                                 true
@@ -1595,56 +1596,34 @@ public synchronized void solvingCNF(int step, int primaryVars, int vars, int cla
             }
 
         });
-        if (!opt.solver.equals(SATFactory.CNF) && !opt.solver.equals(SATFactory.KK) && tryBookExamples) { // try book examples
-            A4Reporter r = "yes".equals(System.getProperty("debug")) ? rep : null;
-            try {
-                sol = BookExamples.trial(r, this, fgoal, (AbstractKodkodSolver) solver.solver, cmd.check);
-            } catch (Throwable ex) {
-                sol = null;
-            }
-        }
 
         solved[0] = false; // this allows the reporter to report the # of
-                          // vars/clauses
+        // vars/clauses
         for (Relation r : bounds.relations()) {
             formulas.add(r.eq(r));
         } // Without this, kodkod refuses to grow unmentioned relations
+
         fgoal = Formula.and(formulas);
-        // Now pick the solver and solve it!
-        if (opt.solver.equals(SATFactory.KK)) {
-            File tmpCNF = File.createTempFile("tmp", ".java", new File(opt.tempDirectory));
-            String out = tmpCNF.getAbsolutePath();
-            Util.writeAll(out, debugExtractKInput());
-            rep.resultCNF(out);
-            return null;
-        }
-        if (opt.solver.equals(SATFactory.CNF)) {
-            File tmpCNF = File.createTempFile("tmp", ".cnf", new File(opt.tempDirectory));
-            String out = tmpCNF.getAbsolutePath();
-            solver.options().setSolver(WriteCNF.factory(out));
-            try {
-                sol = solver.solve(fgoal, bounds);
-            } catch (WriteCNF.WriteCNFCompleted ex) {
-                rep.resultCNF(out);
-                return null;
-            }
-            // The formula is trivial (otherwise, it would have thrown an
-            // exception)
-            // Since the user wants it in CNF format, we manually generate a
-            // trivially satisfiable (or unsatisfiable) CNF file.
-            Util.writeAll(out, sol.instance() != null ? "p cnf 1 1\n1 0\n" : "p cnf 1 2\n1 0\n-1 0\n");
-            rep.resultCNF(out);
-            return null;
-        }
-        if (/* solver.options().solver()==SATFactory.ZChaffMincost || */ !solver.options().solver().incremental()) {
+
+        Solution sol;
+        if (opt.solver instanceof KKTransformer) {
+            sol = doKK(rep, opt);
+        } else if (opt.solver instanceof CNFTransformer) {
+            sol = doCNF(rep, opt);
+        } else if (tryBookExamples && solver.solver instanceof AbstractKodkodSolver) {
+            sol = tryBook(rep, cmd);
+        } else if (!solver.options().solver().incremental()) {
             sol = solver.solve(fgoal, bounds);
-        } else {
+        } else
+            sol = null;
+
+        if (sol == null) {
             PardinusBounds b;
             if (solver.options().decomposed())
-                b = PardinusBounds.splitAtTemporal(bounds); // [electrum] split bounds on temporal
+                b = PardinusBounds.splitAtTemporal(bounds);
             else
                 b = bounds;
-            // [electrum] better handling of solving runtime errors
+
             try {
                 kEnumerator = new Peeker<Solution>(solver.solveAll(fgoal, b));
             } catch (InvalidMutableExpressionException e) {
@@ -1656,11 +1635,17 @@ public synchronized void solvingCNF(int step, int primaryVars, int vars, int cla
                 Pos p = ((Expr) k2pos(e.node())).pos;
                 throw new ErrorAPI(p, "Invalid specification for complete backend.\n" + e.getMessage());
             }
-            if (sol == null)
-                sol = kEnumerator.next();
+            sol = kEnumerator.next();
         }
+
+        if (sol.getOutput().isPresent()) {
+            rep.resultCNF(sol.getOutput().get().getAbsolutePath());
+            return null;
+        }
+
         if (!solved[0])
             rep.solve(0, 0, 0, 0);
+
         Instance inst = sol.instance();
         if (inst != null && !(inst instanceof TemporalInstance))
             inst = new TemporalInstance(Arrays.asList(inst), 0, 1);
@@ -1715,6 +1700,39 @@ public synchronized void solvingCNF(int step, int primaryVars, int vars, int cla
         return this;
     }
 
+    @SuppressWarnings({
+                       "rawtypes", "unchecked"
+    } )
+    private Solution tryBook(final A4Reporter rep, Command cmd) {
+        Solution sol;
+        A4Reporter r = "yes".equals(System.getProperty("debug")) ? rep : null;
+        try {
+            sol = BookExamples.trial(r, this, fgoal, (AbstractKodkodSolver) solver.solver, cmd.check);
+        } catch (Throwable ex) {
+            rep.debug("" + ex);
+            sol = null;
+        }
+        return sol;
+    }
+
+    private Solution doCNF(final A4Reporter rep, final A4Options opt) throws IOException {
+        File tmpCNF = opt.tempFile(".cnf");
+        String out = tmpCNF.getAbsolutePath();
+        solver.options().setSolver(WriteCNF.factory(out));
+        Solution solve = solver.solve(fgoal, bounds);
+        solve.setOutput(tmpCNF);
+        return solve;
+    }
+
+    private Solution doKK(final A4Reporter rep, final A4Options opt) throws IOException {
+        File tmpKK = opt.tempFile(".java");
+        String out = tmpKK.getAbsolutePath();
+        Util.writeAll(out, debugExtractKInput());
+        Solution s = Solution.unsatisfiable(null, null);
+        s.setOutput(tmpKK);
+        return s;
+    }
+
     // ===================================================================================================//
 
     /** This caches the toString() output. */
@@ -2167,4 +2185,18 @@ public InstanceDTO toDTO(int state) {
         return dto;
     }
 
+    public A4Reporter getReporter() {
+        return null;
+    }
+
+    /**
+     * Add default transformers
+     *
+     * @param extensions
+     */
+    public static void addTransformers(List<SATFactory> extensions) {
+        extensions.add(new KKTransformer());
+        extensions.add(new CNFTransformer());
+    }
+
 }
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/CNFTransformer.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/CNFTransformer.java
@@ -0,0 +1,40 @@
+package edu.mit.csail.sdg.translator;
+
+import java.util.Optional;
+
+import kodkod.engine.satlab.SATFactory;
+
+public class CNFTransformer extends SATFactory {
+
+    private static final long serialVersionUID = 1L;
+
+    @Override
+    public String id() {
+        return "CNF";
+    }
+
+    @Override
+    public String name() {
+        return "CNF output";
+    }
+
+    @Override
+    public Optional<String> getDescription() {
+        return Optional.of("CNF stands for Conjunctive Normal Form. It is specified by DIMACS. This is a standardized way of representing Boolean algebra expressions for processing by SAT solvers.");
+    }
+
+    @Override
+    public String type() {
+        return "transformer";
+    }
+
+    @Override
+    public boolean isTransformer() {
+        return true;
+    }
+
+    @Override
+    public boolean isPresent() {
+        return true;
+    }
+}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/KKTransformer.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/KKTransformer.java
@@ -0,0 +1,42 @@
+package edu.mit.csail.sdg.translator;
+
+import java.util.Optional;
+
+import kodkod.engine.satlab.SATFactory;
+
+public class KKTransformer extends SATFactory {
+
+    private static final long serialVersionUID = 1L;
+
+    @Override
+    public String id() {
+        return "KK";
+    }
+
+
+    @Override
+    public String type() {
+        return "transformer";
+    }
+
+    @Override
+    public String name() {
+        return "KodKod output";
+    }
+
+    @Override
+    public Optional<String> getDescription() {
+        return Optional.of("KK is the KodKod debug output format");
+    }
+
+    @Override
+    public boolean isTransformer() {
+        return true;
+    }
+
+    @Override
+    public boolean isPresent() {
+        return true;
+    }
+
+}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/WriteCNF.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/WriteCNF.java
@@ -27,7 +27,7 @@
  * an exception (this code is adapted from ExternalSolver from Kodkod).
  */
 
-final class WriteCNF implements SATSolver {
+final public class WriteCNF implements SATSolver {
 
     /**
      * This runtime exception is thrown when the CNF file has been written
@@ -131,6 +131,7 @@ public void free() {
         Util.close(cnf);
     }
 
+
     /** {@inheritDoc} */
     @Override
     public void addVariables(int numVars) {
@@ -173,10 +174,10 @@ public boolean solve() {
             cnf.seek(0);
             cnf.writeBytes("p cnf " + vars + " " + clauses);
             cnf.close();
+            return false;
         } catch (Exception ex) {
             throw new RuntimeException("WriteCNF failed.", ex);
         }
-        throw new WriteCNFCompleted();
     }
 
     /** {@inheritDoc} */

diff --git a/org.alloytools.alloy.core/src/main/java/org/alloytools/alloy/core/infra/AlloyDispatcher.java b/org.alloytools.alloy.core/src/main/java/org/alloytools/alloy/core/infra/AlloyDispatcher.java
@@ -42,6 +42,7 @@
 import aQute.service.reporter.Reporter;
 import edu.mit.csail.sdg.alloy4.A4Preferences;
 import edu.mit.csail.sdg.alloy4.A4Preferences.Pref;
+import edu.mit.csail.sdg.translator.A4Solution;
 import kodkod.engine.satlab.ExternalSolver;
 import kodkod.engine.satlab.SATFactory;
 import kodkod.engine.satlab.SATSolver;
@@ -533,6 +534,7 @@ public void setslf4j(Levels deflt, String... targets) {
      */
 
     void loadExtensions(File extensions) {
+        A4Solution.addTransformers(SATFactory.extensions);
         if (!extensions.isDirectory())
             return;