small changes

README.md

@@ -1,6 +1,6 @@
 CaDiCaL SAT solver
 ==================
-[![Build Status](https://app.travis-ci.com/mmaroti/cadical-rs.svg?branch=master)](https://app.travis-ci.com/github/mmaroti/cadical-rs)
+[![Build Status](https://github.com/mmaroti/cadical-rs/actions/workflows/rust.yml/badge.svg)](https://github.com/mmaroti/cadical-rs/actions)
 [![Crate](https://img.shields.io/crates/v/cadical)](https://crates.io/crates/cadical)
 [![Documentation](https://docs.rs/cadical/badge.svg)](https://docs.rs/cadical)
 [![GitHub](https://img.shields.io/github/license/mmaroti/cadical-rs)](LICENSE)
@@ -28,5 +28,5 @@ assert_eq!(sat.value(2), Some(true));
 ```
 
 The C++ library is build with assertions disabled and with optimization level
-3 by default. C++ assertions are enabled only when cargo is building a debug 
+3 by default. C++ assertions are enabled only when cargo is building a debug
 version and the `cpp-debug` feature of the library is enabled.

src/ccadical.cpp

@@ -1,5 +1,9 @@
 #include "../cadical/src/ccadical.cpp"
 
+// This files converts some of the C++ interface of cadical to C.
+// These functions are not available in the C interface of cadical.
+// The C interface that cadical provides is in: cadical/src/ccadical.h
+
 extern "C"
 {
   int ccadical_status(CCaDiCaL *wrapper)

src/lib.rs

@@ -62,7 +62,7 @@ extern "C" {
     fn ccadical_reserve(ptr: *mut c_void, min_max_var: c_int);
 }
 
-/// The CaDiCaL incremental SAT solver. The literals are unwrapped positive
+/// The `CaDiCaL` incremental SAT solver. The literals are unwrapped positive
 /// and negative integers, exactly as in the DIMACS format. The common IPASIR
 /// operations are presented in a safe Rust interface.
 /// # Examples
@@ -163,7 +163,7 @@ impl<C: Callbacks> Solver<C> {
     /// assumptions.
     pub fn solve_with<I>(&mut self, assumptions: I) -> Option<bool>
     where
-        I: Iterator<Item = i32>,
+        I: IntoIterator<Item = i32>,
     {
         for lit in assumptions {
             debug_assert!(lit != 0 && lit != i32::MIN);
@@ -196,9 +196,9 @@ impl<C: Callbacks> Solver<C> {
         debug_assert!(self.status() == Some(true));
         debug_assert!(lit != 0 && lit != i32::MIN);
         let val = unsafe { ccadical_val(self.ptr, lit) };
-        if val == lit {
+        if val == lit.abs() {
             Some(true)
-        } else if val == -lit {
+        } else if val == -lit.abs() {
             Some(false)
         } else {
             None
@@ -382,8 +382,8 @@ impl<C: Callbacks> Drop for Solver<C> {
     }
 }
 
-/// CaDiCaL does not use thread local variables, so it is possible to
-/// move it between threads. However it cannot be used queried concurrently
+/// `CaDiCaL`` does not use thread local variables, so it is possible to
+/// move it between threads. However it cannot be used concurrently
 /// (for example getting the value from multiple threads at once), so we
 /// do not implement `Sync`.
 unsafe impl<C: Callbacks + Send> Send for Solver<C> {}
@@ -441,8 +441,10 @@ impl Callbacks for Timeout {
     }
 }
 
-#[derive(Clone, Debug, PartialEq, Eq)]
+unsafe impl Send for Timeout {}
+
 /// Error type for configuration and DIMACS reading and writing errors.
+#[derive(Clone, Debug, PartialEq, Eq)]
 pub struct Error {
     pub msg: String,
 }
@@ -479,7 +481,9 @@ mod tests {
         assert_eq!(sat.solve(), Some(true));
         assert_eq!(sat.solve_with([-1].iter().copied()), Some(true));
         assert_eq!(sat.value(1), Some(false));
+        assert_eq!(sat.value(-1), Some(true));
         assert_eq!(sat.value(2), Some(true));
+        assert_eq!(sat.value(-2), Some(false));
         assert_eq!(sat.solve_with([-2].iter().copied()), Some(true));
         assert_eq!(sat.value(1), Some(true));
         assert_eq!(sat.value(2), Some(false));

src/mockup.rs

@@ -104,6 +104,8 @@ pub unsafe fn ccadical_solve(ptr: *mut c_void) -> c_int {
 pub unsafe fn ccadical_val(ptr: *mut c_void, lit: c_int) -> c_int {
     if lit == 2 {
         2
+    } else if lit == -2 {
+        -2
     } else {
         0
     }
@@ -177,12 +179,12 @@ pub unsafe fn ccadical_limit2(ptr: *mut c_void, name: *const c_char, limit: c_in
     let name = CStr::from_ptr(name).to_str().unwrap();
     if name == "conflicts" {
         mockup.conflicts = limit;
-        return 1;
+        1
     } else if name == "decisions" {
         mockup.decisions = limit;
-        return 1;
+        1
     } else {
-        return 0;
+        0
     }
 }