Huge update of native code handling (#218)

* Added Pardinus source code back into Alloy. Required to cleanup the native code.

* Update to the pardinus core for the SATFactory usage as identifier

* Added native code project

* Update to the native code handling

* Just removed some files to test that were used as examples

* Adaptions to the new native code handling

* Needed for eclipse

* First batch of natives

* Added native code build

* Divide native builds in triggers and subflow

* Divide native builds in triggers and subflow

* Divide native builds in triggers and subflow

* Divide native builds in triggers and subflow

* Divide native builds in triggers and subflow

* Divide native builds in triggers and subflow

* Divide native builds in triggers and subflow

* Divide native builds in triggers and subflow

* Divide native builds in triggers and subflow

.github/workflows/subflow-native.yaml

@@ -0,0 +1,40 @@
+name: Native Code
+
+on:
+  workflow_call:
+
+
+jobs:
+  build:
+    runs-on: macos-latest
+
+    steps:
+      - name: Install GMP
+        run: brew install gmp
+
+      - name: Check out code
+        uses: actions/checkout@v2
+
+      - name: Run Shell Script
+        run: |
+          export HOMEBREW_NO_INSTALL_CLEANUP=true
+          brew install docker
+          colima start
+          ./gradlew --parallel compileJava
+          make -C org.alloytools.pardinus.native/satsolvers install
+          colima stop
+
+      - name: Commit and Push Changes
+        run: |
+          git config user.name github-actions
+          git config user.email [email protected]
+
+      - name: Create pull request
+        uses: peter-evans/create-pull-request@v3
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+          commit-message: "Native code update request"
+          title: "Native code update"
+          delete-branch: true
+          branch: native-code
+          base: master

.github/workflows/trigger-master-native.yaml

@@ -0,0 +1,13 @@
+name: Native Code on master branch
+
+on:
+  push:
+    branches:
+      - master
+    paths:
+      - 'org.alloytools.solvers.natv/satsolvers/**'
+
+jobs:
+  call-native:
+    uses: ./.github/workflows/subflow-native.yaml
+    secrets: inherit

.github/workflows/trigger-native.yaml

@@ -0,0 +1,11 @@
+name: Native code branch changed
+
+on:
+  push:
+    branches:
+      - native
+
+jobs:
+  call-native:
+     uses: ./.github/workflows/subflow-native.yaml
+     secrets: inherit

cnf/central.mvn

@@ -6,8 +6,6 @@ com.google.code.gson:gson:2.8.9
 commons-io:commons-io:jar:2.6
 commons-io:commons-io:jar:2.6
 de.jflex:jflex:1.6.1
-org.alloytools:pardinus.core:1.3.0
-org.alloytools:pardinus.nativesat:1.3.0
 org.eclipse.equinox:org.eclipse.equinox.common:jar:3.6.0
 org.eclipse.equinox:org.eclipse.equinox.common:jar:3.6.0
 org.eclipse.jdt:org.eclipse.jdt.annotation:2.1.100
@@ -20,7 +18,6 @@ org.sat4j:org.sat4j.maxsat:2.3.1
 org.sat4j:org.sat4j.pb:2.3.1
 org.slf4j:slf4j-api:1.7.28
 org.slf4j:slf4j-simple:1.7.5
-org.alloytools:pardinus.core:1.3.0
 org.alloytools:pardinus.nativesat:1.3.0
 biz.aQute:biz.aQute.wrapper.hamcrest:1.3
 biz.aQute:biz.aQute.wrapper.junit:4.13.1

org.alloytools.alloy.application/bnd.bnd

@@ -3,10 +3,10 @@
 
 -buildpath: \
 	lib/apple-osx-ui.jar;version=file,\
-	org.alloytools:pardinus.core;version='1.3.0',\
 	org.alloytools.alloy.core;version=latest,\
 	aQute.libg,\
-	org.alloytools.api
+	org.alloytools.api,\
+	org.alloytools.pardinus.core
 -testpath: \
 	biz.aQute.wrapper.junit, \
 	biz.aQute.wrapper.hamcrest, \

org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/PreferencesDialog.java

@@ -73,7 +73,7 @@
 import edu.mit.csail.sdg.alloy4.OurBorder;
 import edu.mit.csail.sdg.alloy4.OurUtil;
 import edu.mit.csail.sdg.alloy4.OurUtil.GridBagConstraintsBuilder;
-import edu.mit.csail.sdg.translator.A4Options.SatSolver;
+import kodkod.engine.satlab.SATFactory;
 
 /**
  * @modified [electrum] only log when debugging; load electrod binary
@@ -194,7 +194,8 @@ public int getExtent() {
         }
 
         @Override
-        public void setValueIsAdjusting(boolean b) {}
+        public void setValueIsAdjusting(boolean b) {
+        }
 
         @Override
         public boolean getValueIsAdjusting() {
@@ -254,26 +255,14 @@ public Component getListCellRendererComponent(JList list, Object value, int inde
     public PreferencesDialog(SwingLogPanel log, String binary) {
         this.log = log;
         if (log != null && binary != null) {
-            List<SatSolver> solvers = testSolvers();
-            Solver.setChoices(solvers, SatSolver.SAT4J);
+            List<SATFactory> solvers = SATFactory.getSolvers();
+            Solver.setChoices(solvers, SATFactory.DEFAULT);
             log.log("Available solvers on " + System.getProperty("os.name") + ":" + System.getProperty("os.arch") + "\n");
             solvers.forEach(s -> log.log(s.toString() + "\n"));
         }
         initUI();
     }
 
-    protected List<SatSolver> testSolvers() {
-        List<SatSolver> satChoices = SatSolver.values();
-        satChoices.removeIf(solver -> !solver.present());
-
-        SatSolver now = Solver.get();
-        if (!satChoices.contains(now)) {
-            Solver.set(SatSolver.SAT4J);
-        }
-
-        return satChoices;
-    }
-
 
 
     protected final void initUI() {
@@ -321,7 +310,7 @@ protected Component initSolverPane() {
 
             @Override
             public void stateChanged(ChangeEvent e) {
-                boolean enableCore = Solver.get() == SatSolver.MiniSatProverJNI;
+                boolean enableCore = Solver.get().prover();
                 pref2comp.get(CoreGranularity).setEnabled(enableCore);
                 pref2comp.get(CoreMinimization).setEnabled(enableCore);
             }
@@ -451,7 +440,8 @@ private void updatePref() {
                 String val = jtf.getText();
                 try {
                     pref.set(Integer.parseInt(val));
-                } catch (NumberFormatException ex) {}
+                } catch (NumberFormatException ex) {
+                }
             }
         });
         return OurUtil.makeH(pref.title + ": ", jtf);