prepared mockup for miri

.github/workflows/rust.yml

@@ -2,16 +2,16 @@ name: Rust
 
 on:
   push:
-    branches: [ "test" ]
+    branches: [master, test]
   pull_request:
-    branches: [ "test" ]
+    branches: [master, test]
 
 env:
   CARGO_TERM_COLOR: always
 
 jobs:
   build:
-    runs-on: [ubuntu-latest, windows-latest, macos-latest]
+    runs-on: [ubuntu-latest]
     steps:
     - name: Checkout
       uses: actions/checkout@v4

src/lib.rs

@@ -15,6 +15,12 @@ use std::ptr::null_mut;
 use std::time::Instant;
 use std::{fmt, slice};
 
+#[cfg(miri)]
+mod mockup;
+#[cfg(miri)]
+use mockup::*;
+
+#[cfg(not(miri))]
 extern "C" {
     fn ccadical_signature() -> *const c_char;
     fn ccadical_init() -> *mut c_void;
@@ -448,6 +454,7 @@ mod tests {
     use std::thread;
 
     #[test]
+    #[cfg(not(miri))]
     fn solver() {
         let mut sat: Solver = Solver::new();
         assert!(sat.signature().starts_with("cadical-"));
@@ -564,6 +571,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg(not(miri))]
     fn fileio() {
         let mut path = std::env::temp_dir();
         path.push("pigeon5.cnf");
@@ -589,10 +597,10 @@ mod tests {
     #[test]
     fn test_reserve() {
         let mut s: Solver = Default::default();
-        assert!(s.solve().unwrap());
+        assert_eq!(s.solve(), Some(true));
         assert_eq!(s.max_variable(), 0);
         s.reserve(2);
-        assert!(s.solve().unwrap());
+        assert_eq!(s.solve(), Some(true));
         assert_eq!(s.max_variable(), 2);
     }
 }

src/mockup.rs

@@ -0,0 +1,191 @@
+//! This is a stand alone crate that contains both the C++ source code of the
+//! CaDiCaL incremental SAT solver together with its Rust binding. The C++
+//! files are compiled and statically linked during the build process. This
+//! crate works on Linux, Apple OSX, Windows, Android, iOS, Raspberry Pi,
+//! NetBSD and FreeBSD.
+//! CaDiCaL won first place in the SAT track of the SAT Race 2019 and second
+//! overall place. It was written by Armin Biere, and it is available under the
+//! MIT license.
+
+#![allow(unused)]
+
+use std::cmp::max;
+use std::ffi::CStr;
+use std::os::raw::{c_char, c_int, c_void};
+use std::ptr::{null, null_mut};
+
+struct Mockup {
+    vars: Vec<bool>,
+    clauses: i32,
+    conflicts: i32,
+    decisions: i32,
+    status: i32,
+    terminate_data: *mut c_void,
+    terminate_cbs: Option<extern "C" fn(*mut c_void) -> c_int>,
+}
+
+impl Mockup {
+    fn new() -> Self {
+        println!("created");
+        Self {
+            vars: Default::default(),
+            clauses: 0,
+            conflicts: -1,
+            decisions: -1,
+            status: 0,
+            terminate_data: null_mut(),
+            terminate_cbs: None,
+        }
+    }
+}
+
+impl Drop for Mockup {
+    fn drop(&mut self) {
+        println!("dropped");
+    }
+}
+
+pub unsafe fn ccadical_signature() -> *const c_char {
+    println!("signature");
+    "cadical-mockup\0".as_ptr() as *const c_char
+}
+
+pub unsafe fn ccadical_init() -> *mut c_void {
+    println!("init");
+    let mockup = Box::new(Mockup::new());
+    Box::into_raw(mockup) as *mut c_void
+}
+
+pub unsafe fn ccadical_release(ptr: *mut c_void) {
+    println!("release");
+    let mut mockup = Box::from_raw(ptr as *mut Mockup);
+    drop(mockup);
+}
+
+pub unsafe fn ccadical_add(ptr: *mut c_void, lit: c_int) {
+    let mockup = &mut *(ptr as *mut Mockup);
+    if lit == 0 {
+        mockup.clauses += 1;
+    } else {
+        let lit = lit.abs();
+        if (mockup.vars.len() as i32) < lit {
+            mockup.vars.resize(lit as usize, false);
+        }
+        mockup.vars[(lit - 1) as usize] = true;
+    }
+}
+
+pub unsafe fn ccadical_assume(ptr: *mut c_void, lit: c_int) {}
+
+pub unsafe fn ccadical_solve(ptr: *mut c_void) -> c_int {
+    println!("solve");
+    let mockup = &mut *(ptr as *mut Mockup);
+
+    if let Some(cbs) = mockup.terminate_cbs {
+        // let val = cbs(mockup.terminate_data);
+        // println!("{}", val);
+        return 0;
+    }
+
+    mockup.status = if mockup.clauses == 0 || mockup.clauses == 2 {
+        10
+    } else if mockup.conflicts >= 0 || mockup.decisions >= 0 {
+        0
+    } else {
+        20
+    };
+    mockup.status
+}
+
+pub unsafe fn ccadical_val(ptr: *mut c_void, lit: c_int) -> c_int {
+    if lit == 2 {
+        2
+    } else {
+        0
+    }
+}
+
+pub unsafe fn ccadical_failed(ptr: *mut c_void, lit: c_int) -> c_int {
+    0
+}
+
+pub unsafe fn ccadical_set_terminate(
+    ptr: *mut c_void,
+    data: *mut c_void,
+    cbs: Option<extern "C" fn(*mut c_void) -> c_int>,
+) {
+    let mockup = &mut *(ptr as *mut Mockup);
+    mockup.terminate_data = data;
+    mockup.terminate_cbs = cbs;
+}
+
+pub unsafe fn ccadical_set_learn(
+    ptr: *mut c_void,
+    data: *mut c_void,
+    max_len: c_int,
+    cbs: Option<extern "C" fn(*mut c_void, *const c_int)>,
+) {
+}
+
+pub unsafe fn ccadical_status(ptr: *mut c_void) -> c_int {
+    let mockup = &mut *(ptr as *mut Mockup);
+    mockup.status
+}
+
+pub unsafe fn ccadical_vars(ptr: *mut c_void) -> c_int {
+    let mockup = &mut *(ptr as *mut Mockup);
+    mockup.vars.len() as i32
+}
+
+pub unsafe fn ccadical_active(ptr: *mut c_void) -> i64 {
+    let mockup = &mut *(ptr as *mut Mockup);
+    mockup.vars.iter().filter(|v| **v).count() as i64
+}
+
+pub unsafe fn ccadical_irredundant(ptr: *mut c_void) -> i64 {
+    let mockup = &mut *(ptr as *mut Mockup);
+    mockup.clauses as i64
+}
+
+pub unsafe fn ccadical_read_dimacs(
+    ptr: *mut c_void,
+    path: *const c_char,
+    vars: *mut c_int,
+    strict: c_int,
+) -> *const c_char {
+    null::<c_char>()
+}
+
+pub unsafe fn ccadical_write_dimacs(
+    ptr: *mut c_void,
+    path: *const c_char,
+    min_max_var: c_int,
+) -> *const c_char {
+    null::<c_char>()
+}
+
+pub unsafe fn ccadical_configure(ptr: *mut c_void, name: *const c_char) -> c_int {
+    0
+}
+
+pub unsafe fn ccadical_limit2(ptr: *mut c_void, name: *const c_char, limit: c_int) -> c_int {
+    let mockup = &mut *(ptr as *mut Mockup);
+    let name = CStr::from_ptr(name).to_str().unwrap();
+    if name == "conflicts" {
+        mockup.conflicts = limit;
+        return 1;
+    } else if name == "decisions" {
+        mockup.decisions = limit;
+        return 1;
+    } else {
+        return 0;
+    }
+}
+
+pub unsafe fn ccadical_reserve(ptr: *mut c_void, min_max_var: c_int) {
+    println!("vars");
+    let mockup = &mut *(ptr as *mut Mockup);
+    if (mockup.vars.len() as i32) < min_max_var {
+        mockup.vars.resize(min_max_var as usize, false);
+    }
+}