Merge pull request #7 from lixitrixi/main

Kissat bindings

.github/workflows/kissat-tests.yml

@@ -0,0 +1,87 @@
+# https://doc.rust-lang.org/cargo/guide/continuous-integration.html
+# https://ectobit.com/blog/speed-up-github-actions-rust-pipelines/
+name: 'solvers/kissat'
+on:
+  push:
+    paths: 
+      - 'solvers/kissat/**'
+  pull_request:
+    paths: 
+      - 'solvers/kissat/**'
+  workflow_dispatch:
+
+jobs:
+  ubuntu:
+    name: 'solvers/kissat: Ubuntu Build'
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: Set up cache
+        uses: actions/cache@v3
+        with:
+          path: |
+            ~/.cargo/bin/
+            ~/.cargo/registry/index/
+            ~/.cargo/registry/cache/
+            ~/.cargo/git/db/
+            target/
+          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
+          restore-keys: ${{ runner.os }}-cargo-
+
+      - working-directory: ./solvers/kissat
+        run: rustup update stable && rustup default stable
+
+      - working-directory: ./solvers/kissat
+        run: cargo build -vv
+
+  mac:
+    name: 'solvers/kissat: Mac Build'
+    runs-on: macos-latest
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: Set up cache
+        uses: actions/cache@v3
+        with:
+          path: |
+            ~/.cargo/bin/
+            ~/.cargo/registry/index/
+            ~/.cargo/registry/cache/
+            ~/.cargo/git/db/
+            target/
+          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
+          restore-keys: ${{ runner.os }}-cargo-
+
+      - working-directory: ./solvers/kissat
+        run: rustup update stable && rustup default stable
+
+      - working-directory: ./solvers/kissat 
+        run: rustup target add aarch64-apple-darwin
+
+      - working-directory: ./solvers/kissat
+        run: cargo build -vv
+
+  tests:
+    name: 'solvers/kissat: Tests'
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: Set up cache
+        uses: actions/cache@v3
+        with:
+          path: |
+            ~/.cargo/bin/
+            ~/.cargo/registry/index/
+            ~/.cargo/registry/cache/
+            ~/.cargo/git/db/
+            target/
+          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
+          restore-keys: ${{ runner.os }}-cargo-
+
+      - working-directory: ./solvers/kissat
+        run: rustup update stable && rustup default stable
+
+      - working-directory: ./solvers/kissat
+        run: cargo test

.gitignore

@@ -1 +1,3 @@
 target
+
+solvers/**/vendor/build

Cargo.toml

@@ -1,3 +1,4 @@
 [workspace]
 
-members = ["solvers/minion", "solvers/chuffed"]
+members = ["solvers/*"]
+exclude = []

solvers/kissat/Cargo.toml

@@ -0,0 +1,10 @@
+[package]
+name = "kissat_rs"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+kissat-rs = { git = "https://github.com/firefighterduck/kissat-rs", branch = "main", version = "0.1" }
+kissat-sys = { git = "https://github.com/firefighterduck/kissat-rs", branch = "main", version = "0.1" }

solvers/kissat/src/lib.rs

@@ -0,0 +1,31 @@
+
+#[cfg(test)]
+fn test1() {
+    use kissat_rs::Solver;
+    use kissat_rs::Assignment;
+
+    // Define three literals used in both formulae.
+    let x = 1;
+    let y = 2;
+    let z = 3;
+
+    // Construct a formula from clauses (i.e. an iterator over literals).
+    // (~x || y) && (~y || z) && (x || ~z) && (x || y || z)
+    let formula1 = vec![vec![-x, y], vec![-y, z], vec![x, -z], vec![x, y, z]];
+    let satisfying_assignment = Solver::solve_formula(formula1).unwrap();
+
+    // The formula from above is satisfied by the assignment: x -> True, y -> True, z -> True
+    if let Some(assignments) = satisfying_assignment {
+        assert_eq!(assignments.get(&x).unwrap(), &Some(Assignment::True));
+        assert_eq!(assignments.get(&y).unwrap(), &Some(Assignment::True));
+        assert_eq!(assignments.get(&z).unwrap(), &Some(Assignment::True));
+    }
+
+    // (x || y || ~z) && ~x && (x || y || z) && (x || ~y)
+    let formula2 = vec![vec![x, y, -z], vec![-x], vec![x, y, z], vec![x, -y]];
+    let unsat_result = Solver::solve_formula(formula2).unwrap();
+
+    // The second formula is unsatisfiable. 
+    // This can for example be proved by resolution.
+    assert_eq!(unsat_result, None);
+}