ipasir_loading/
lib.rs

1#![doc = include_str!("../README.md")]
2
3use anyhow::{anyhow, Result};
4use core::slice;
5use libloading::{Library, Symbol};
6use std::{
7    ffi::{CStr, OsStr},
8    ops::{Deref, DerefMut},
9    os::raw::{c_char, c_void},
10    rc::Rc,
11};
12
13/// A structure used to load a shared library and build new SAT solvers from it.
14///
15/// This structure takes as entry point a path to a shared library containing a SAT solver that conform to the IPASIR specification.
16/// An [`IpasirSolverLoader`] is built by passing this path to the [`from_path`](Self::from_path) function.
17/// This object can be used to create new solvers with the [`new_solver`](Self::new_solver) function.
18///
19/// The IPASIR interface provides two functions that take a function pointer as parameter.
20/// To use them on solvers created by this object,
21/// these functions must be enabled by calling [`enable_set_terminate`](Self::enable_set_terminate)
22/// and [`enable_set_learn`](Self::enable_set_learn) before creating the SAT solvers.
23///
24/// # Example
25///
26/// ```no_run
27/// # use ipasir_loading::IpasirSolverLoader;
28/// let mut loader = IpasirSolverLoader::from_path("path/to/lib.so").unwrap();
29/// loader.enable_set_terminate(true); // activate ipasir_set_terminate
30/// loader.enable_set_learn(Some(8)); // activate ipasir_set_learn for clause of sizes at most 8
31/// let sat_solver = loader.new_solver().unwrap(); // create the solver
32/// ```
33pub struct IpasirSolverLoader {
34    library: Rc<Library>,
35    enable_set_terminate: bool,
36    enable_set_learn: Option<i32>,
37}
38
39impl IpasirSolverLoader {
40    /// Builds a new [`IpasirSolverLoader`] given a path to a shared library containing a SAT solver that conform to the IPASIR specification.
41    ///
42    /// # Errors
43    ///
44    /// This function returns an error if the library cannot be loaded,
45    /// e.g. if the path does not point to a shared library.
46    pub fn from_path<P: AsRef<OsStr>>(path: P) -> Result<Self> {
47        let library = unsafe { Library::new(path)? };
48        Ok(Self {
49            library: Rc::new(library),
50            enable_set_terminate: false,
51            enable_set_learn: None,
52        })
53    }
54
55    /// Returns a string describing the name and the version of the library solver.
56    ///
57    /// # Errors
58    ///
59    /// This function returns an error if the library does not include the corresponding IPASIR function,
60    /// or if an error occurs when calling it.
61    pub fn ipasir_signature(&self) -> Result<String> {
62        let c_str_signature = unsafe {
63            let function: Symbol<unsafe extern "C" fn() -> *const c_char> =
64                self.library.get(b"ipasir_signature")?;
65            CStr::from_ptr(function())
66        };
67        Ok(c_str_signature.to_str()?.to_string())
68    }
69
70    /// Builds a new SAT solver from the shared library.
71    ///
72    /// The returned solver can accept callback functions on termination or when learning a clause
73    /// only if the appropriate activation functions ([`enable_set_terminate`](IpasirSolverLoader::enable_set_terminate) or [`enable_set_learn`](IpasirSolverLoader::enable_set_learn)) have been called before calling this function.
74    ///
75    /// # Errors
76    ///
77    /// This function returns an error if the library does not contain the `ipasir_init` function,
78    /// or if an error occurs when calling it.
79    /// In case some callback functions are enabled,
80    /// this function will also return an error if the corresponding IPASIR callback function (`ipasir_set_terminate` or `ipasir_set_learn`) is missing from the library or if an error occurs when calling it.
81    pub fn new_solver(&self) -> Result<IpasirSolverWrapper> {
82        let solver_ptr = unsafe {
83            let init_function: Symbol<unsafe extern "C" fn() -> *const c_void> =
84                self.library.get(b"ipasir_init")?;
85            init_function()
86        };
87        let mut ipasir_solver_box = Box::new(IpasirSolver {
88            library: Rc::clone(&self.library),
89            solver: solver_ptr,
90            enable_set_terminate: self.enable_set_terminate,
91            set_terminate_callbacks: vec![],
92            enable_set_learn: self.enable_set_learn,
93            set_learn_callbacks: vec![],
94            state: SolverState::Input,
95        });
96        if self.enable_set_terminate {
97            Self::enable_set_terminate_for_solver(self, solver_ptr, &mut ipasir_solver_box)?;
98        }
99        if let Some(bound) = self.enable_set_learn {
100            Self::enable_set_learn_for_solver(self, solver_ptr, &mut ipasir_solver_box, bound)?;
101        }
102        Ok(IpasirSolverWrapper(ipasir_solver_box))
103    }
104
105    /// Enables or disables the [`ipasir_set_terminate`](IpasirSolver::ipasir_set_terminate) for the solvers created after the call to this function.
106    pub fn enable_set_terminate(&mut self, v: bool) {
107        self.enable_set_terminate = v;
108    }
109
110    fn enable_set_terminate_for_solver(
111        loader: &IpasirSolverLoader,
112        solver_ptr: *const c_void,
113        ipasir_solver_box: &mut IpasirSolver,
114    ) -> Result<()> {
115        unsafe {
116            let set_terminate_function: Symbol<
117                unsafe extern "C" fn(
118                    *const c_void,
119                    *const c_void,
120                    *const fn(*const c_void) -> isize,
121                ),
122            > = loader.library.get(b"ipasir_set_terminate")?;
123            set_terminate_function(
124                solver_ptr,
125                std::ptr::addr_of_mut!(*ipasir_solver_box) as *const _,
126                ipasir_set_terminate_callback as *const _,
127            );
128        }
129        Ok(())
130    }
131
132    /// Enables or disables the [`ipasir_set_learn`](IpasirSolver::ipasir_set_learn) for the solvers created after the call to this function.
133    ///
134    /// To enable the function, pass `Some(n)` where `n` is the maximum length of the learned clauses you are interested in.
135    /// To disable the function, pass `None`.
136    pub fn enable_set_learn(&mut self, bound: Option<i32>) {
137        self.enable_set_learn = bound;
138    }
139
140    fn enable_set_learn_for_solver(
141        loader: &IpasirSolverLoader,
142        solver_ptr: *const c_void,
143        ipasir_solver_box: &mut IpasirSolver,
144        max_length: i32,
145    ) -> Result<()> {
146        unsafe {
147            let set_learn_function: Symbol<
148                unsafe extern "C" fn(
149                    *const c_void,
150                    *const c_void,
151                    i32,
152                    *const fn(*const c_void, *const i32),
153                ),
154            > = loader.library.get(b"ipasir_set_learn")?;
155            set_learn_function(
156                solver_ptr,
157                std::ptr::addr_of_mut!(*ipasir_solver_box) as *const _,
158                max_length,
159                ipasir_set_learn_callback as *const _,
160            );
161        }
162        Ok(())
163    }
164}
165
166impl AsRef<Library> for IpasirSolverLoader {
167    fn as_ref(&self) -> &Library {
168        &self.library
169    }
170}
171
172extern "C" fn ipasir_set_terminate_callback(solver_ptr: *const IpasirSolver) -> isize {
173    let must_terminate = unsafe {
174        (*solver_ptr)
175            .set_terminate_callbacks
176            .iter()
177            .any(|callback| callback())
178    };
179    isize::from(must_terminate)
180}
181
182extern "C" fn ipasir_set_learn_callback(solver_ptr: *const IpasirSolver, clause_ptr: *const i32) {
183    let clause = unsafe {
184        let mut p = clause_ptr;
185        while *p != 0 {
186            p = p.add(1);
187        }
188        slice::from_raw_parts(clause_ptr, p.offset_from(clause_ptr).unsigned_abs())
189    };
190    unsafe {
191        (*solver_ptr)
192            .set_learn_callbacks
193            .iter()
194            .for_each(|callback| callback(clause));
195    };
196}
197
198/// A wrapper around [`IpasirSolver`].
199pub struct IpasirSolverWrapper(Box<IpasirSolver>);
200
201impl Deref for IpasirSolverWrapper {
202    type Target = IpasirSolver;
203
204    fn deref(&self) -> &Self::Target {
205        &self.0
206    }
207}
208
209impl DerefMut for IpasirSolverWrapper {
210    fn deref_mut(&mut self) -> &mut Self::Target {
211        &mut self.0
212    }
213}
214
215type SetLearnCallbackType = Box<dyn Fn(&[i32])>;
216
217type SetTerminateCallbackType = Box<dyn Fn() -> bool>;
218
219#[derive(Debug, Copy, Clone, PartialEq)]
220enum SolverState {
221    Input,
222    Sat,
223    Unsat,
224}
225
226impl SolverState {
227    fn expect_status(self, expected: Self) -> Result<()> {
228        if self == expected {
229            Ok(())
230        } else {
231            Err(anyhow!("expected status {expected:?}, was {self:?}"))
232        }
233    }
234
235    fn update_from_status(&mut self, status: isize) {
236        *self = match status {
237            0 => *self,
238            10 => SolverState::Sat,
239            20 => SolverState::Unsat,
240            _ => unreachable!(),
241        }
242    }
243}
244
245/// A SAT solver conforming to the IPASIR specification.
246///
247/// All of the functions below, except the callback functions, are just safe interfaces to the IPASIR functions of the same name.
248/// For the two functions where the behavior differs from the specification, this is indicated in the function documentation.
249///
250/// When the [`IpasirSolver`] is dropped, the underlying data is automatically released by calling the `ipasir_release` function from the loaded library.
251/// Note that an error encountered in this function can lead to a panic.
252///
253/// ```no_run
254/// # use ipasir_loading::IpasirSolverLoader;
255/// // load the IPASIR library
256/// let loader = IpasirSolverLoader::from_path("path/to/lib.so").unwrap();
257///
258/// // create a solver from the library and populate it
259/// let mut solver = loader.new_solver().unwrap();
260/// solver.ipasir_add(-1).unwrap();
261/// solver.ipasir_add(-2).unwrap();
262/// solver.ipasir_add(0).unwrap();
263/// solver.ipasir_add(1).unwrap();
264/// solver.ipasir_add(2).unwrap();
265/// solver.ipasir_add(0).unwrap();
266///
267/// // check satisfiability and get back the model
268/// assert!(solver.ipasir_solve().unwrap().unwrap());
269/// let model = vec![solver.ipasir_val(1).unwrap(), solver.ipasir_val(2).unwrap()];
270/// let expected_1 = vec![Some(true), Some(false)];
271/// let expected_2 = vec![Some(false), Some(true)];
272/// assert!(model == expected_1 || model == expected_2);
273/// ```
274pub struct IpasirSolver {
275    library: Rc<Library>,
276    solver: *const c_void,
277    enable_set_terminate: bool,
278    set_terminate_callbacks: Vec<SetTerminateCallbackType>,
279    enable_set_learn: Option<i32>,
280    set_learn_callbacks: Vec<SetLearnCallbackType>,
281    state: SolverState,
282}
283
284impl IpasirSolver {
285    /// Add the given literal into the currently added clause or finalize the clause with a 0.
286    ///
287    /// # Errors
288    ///
289    /// This function returns an error if the library does not include the corresponding IPASIR function,
290    /// or if an error occurs when calling it.
291    pub fn ipasir_add(&mut self, lit: i32) -> Result<()> {
292        unsafe {
293            let function: Symbol<unsafe extern "C" fn(*const c_void, i32)> =
294                self.library.get(b"ipasir_add")?;
295            function(self.solver, lit);
296        }
297        self.state = SolverState::Input;
298        Ok(())
299    }
300
301    /// Solve the formula with specified clauses under the specified assumptions.
302    ///
303    /// The solver returns an `Option` containing `true` (resp. `false`) if the formula is satisfiable,
304    /// or `None` if the search was stopped before deciding the satisfiability.
305    ///
306    /// # Errors
307    ///
308    /// This function returns an error if the library does not include the corresponding IPASIR function,
309    /// or if an error occurs when calling it.
310    pub fn ipasir_solve(&mut self) -> Result<Option<bool>> {
311        let status = unsafe {
312            let function: Symbol<unsafe extern "C" fn(*const c_void) -> isize> =
313                self.library.get(b"ipasir_solve")?;
314            function(self.solver)
315        };
316        self.state.update_from_status(status);
317        match status {
318            0 => Ok(None),
319            10 => Ok(Some(true)),
320            20 => Ok(Some(false)),
321            _ => Err(anyhow!(
322                "ipasir_solve returned an unexpected value: {status}"
323            )),
324        }
325    }
326
327    /// Get the truth value of the given literal in the found satisfying assignment.
328    /// This function must not be called if the formula changed since the last time `ipasir_solve` found a model.
329    ///
330    /// This function returns an `Option` containing `true` (resp. `false`) if the variable was set to `true` (resp. `false`) in the last satisfying assignment.
331    /// In case the solver detected both polarities of the literal would lead to a model, `None` may be returned.
332    ///
333    /// # Errors
334    ///
335    /// This function returns an error if the library does not include the corresponding IPASIR function,
336    /// or if an error occurs when calling it.
337    pub fn ipasir_val(&mut self, lit: i32) -> Result<Option<bool>> {
338        self.state.expect_status(SolverState::Sat)?;
339        let value = unsafe {
340            let function: Symbol<unsafe extern "C" fn(*const c_void, i32) -> i32> =
341                self.library.get(b"ipasir_val")?;
342            function(self.solver, lit)
343        };
344        match value {
345            0 => Ok(None),
346            n if n == lit.abs() => Ok(Some(true)),
347            n if n == -lit.abs() => Ok(Some(false)),
348            _ => Err(anyhow!("ipasir_val returned an unexpected value: {value}")),
349        }
350    }
351
352    /// Add an assumption for the next SAT search (the next call of [`ipasir_solve`](Self::ipasir_solve)).
353    /// After calling [`ipasir_solve`](Self::ipasir_solve) all the previously added assumptions are cleared.
354    ///
355    /// # Errors
356    ///
357    /// This function returns an error if the library does not include the corresponding IPASIR function,
358    /// or if an error occurs when calling it.
359    pub fn ipasir_assume(&mut self, lit: i32) -> Result<()> {
360        unsafe {
361            let function: Symbol<unsafe extern "C" fn(*const c_void, i32)> =
362                self.library.get(b"ipasir_assume")?;
363            function(self.solver, lit);
364        }
365        self.state = SolverState::Input;
366        Ok(())
367    }
368
369    /// Check if the given assumption literal was used to prove the unsatisfiability of the formula under the assumptions used for the last SAT search.
370    /// This function must not be called if the formula changed since the last time `ipasir_solve` proved the unsatisfiability of the formula.
371    /// Return `true` if so, `false` otherwise.
372    ///
373    /// # Errors
374    ///
375    /// This function returns an error if the library does not include the corresponding IPASIR function,
376    /// or if an error occurs when calling it.
377    pub fn ipasir_failed(&mut self, lit: i32) -> Result<bool> {
378        self.state.expect_status(SolverState::Unsat)?;
379        let value = unsafe {
380            let function: Symbol<unsafe extern "C" fn(*const c_void, i32) -> isize> =
381                self.library.get(b"ipasir_failed")?;
382            function(self.solver, lit)
383        };
384        match value {
385            0 => Ok(false),
386            1 => Ok(true),
387            _ => Err(anyhow!(
388                "ipasir_failed returned an unexpected value: {value}"
389            )),
390        }
391    }
392
393    /// Add a callback function used to indicate a termination requirement to the solver.
394    /// The [`IpasirSolverLoader`] that created this solver must have enabled such callbacks with [`enable_set_terminate`](IpasirSolverLoader::enable_set_terminate).
395    ///
396    /// The solver will periodically call the callback function and check its return value during the search.
397    /// If the function returns `true`, the solver should terminate.
398    ///
399    /// Contrary to the IPASIR specification, more than one callback function can be set in this way.
400    ///
401    /// # Errors
402    ///
403    /// This function will return an error if the correct type of callback function has not been enabled prior to the creation of the solver.
404    pub fn ipasir_set_terminate(&mut self, callback: SetTerminateCallbackType) -> Result<()> {
405        if self.enable_set_terminate {
406            self.set_terminate_callbacks.push(callback);
407            Ok(())
408        } else {
409            Err(anyhow!("ipasir_set_terminate is not enabled; see ipasir-loading documentation for more information"))
410        }
411    }
412
413    /// Add a callback function to be called when a clause is learned by the solver.
414    /// The [`IpasirSolverLoader`] that created this solver must have enabled such callbacks with [`enable_set_learn`](IpasirSolverLoader::enable_set_learn).
415    ///
416    /// Contrary to the IPASIR specification, more than one callback function can be set in this way.
417    /// The maximum length of the clauses passed to the callbacks is defined when enabling the callbacks in [`IpasirSolverLoader`].
418    ///
419    /// # Errors
420    ///
421    /// This function will return an error if the correct type of callback function has not been enabled prior to the creation of the solver.
422    pub fn ipasir_set_learn(&mut self, callback: SetLearnCallbackType) -> Result<()> {
423        if self.enable_set_learn.is_some() {
424            self.set_learn_callbacks.push(callback);
425            Ok(())
426        } else {
427            Err(anyhow!("ipasir_set_learn is not enabled; see ipasir-loading documentation for more information"))
428        }
429    }
430}
431
432impl Drop for IpasirSolver {
433    fn drop(&mut self) {
434        unsafe {
435            let function: Symbol<unsafe extern "C" fn(*const c_void)> = self
436                .library
437                .get(b"ipasir_release")
438                .expect("cannot get function ipafair_release from IPSAIR solver library");
439            function(self.solver);
440        }
441    }
442}
443
444#[cfg(test)]
445#[allow(dead_code, unused_imports)]
446mod tests {
447    use super::*;
448    use std::{cell::RefCell, rc::Rc};
449
450    macro_rules! solver_loader_or_return {
451        () => {
452            if let Ok(path) = std::env::var("IPASIR_SOLVER") {
453                IpasirSolverLoader::from_path(path).unwrap()
454            } else {
455                return;
456            }
457        };
458    }
459
460    #[test]
461    fn test_signature() {
462        let loader = solver_loader_or_return!();
463        let signature = loader.ipasir_signature().unwrap();
464        assert!(!signature.is_empty());
465    }
466
467    #[test]
468    fn test_sat() {
469        let loader = solver_loader_or_return!();
470        let mut solver = loader.new_solver().unwrap();
471        solver.ipasir_add(1).unwrap();
472        solver.ipasir_add(0).unwrap();
473        assert!(solver.ipasir_solve().unwrap().unwrap());
474        assert!(solver.ipasir_val(1).unwrap().unwrap());
475        assert!(!solver.ipasir_val(-1).unwrap().unwrap());
476    }
477
478    #[test]
479    fn test_sat_neg_lit() {
480        let loader = solver_loader_or_return!();
481        let mut solver = loader.new_solver().unwrap();
482        solver.ipasir_add(-1).unwrap();
483        solver.ipasir_add(0).unwrap();
484        assert!(solver.ipasir_solve().unwrap().unwrap());
485        assert!(!solver.ipasir_val(1).unwrap().unwrap());
486        assert!(solver.ipasir_val(-1).unwrap().unwrap());
487    }
488
489    #[test]
490    fn test_unsat() {
491        let loader = solver_loader_or_return!();
492        let mut solver = loader.new_solver().unwrap();
493        solver.ipasir_add(1).unwrap();
494        solver.ipasir_add(0).unwrap();
495        solver.ipasir_add(-1).unwrap();
496        solver.ipasir_add(0).unwrap();
497        assert!(!solver.ipasir_solve().unwrap().unwrap());
498    }
499
500    #[test]
501    fn test_sat_then_unsat() {
502        let loader = solver_loader_or_return!();
503        let mut solver = loader.new_solver().unwrap();
504        solver.ipasir_add(1).unwrap();
505        solver.ipasir_add(0).unwrap();
506        assert!(solver.ipasir_solve().unwrap().unwrap());
507        assert!(solver.ipasir_val(1).unwrap().unwrap());
508        solver.ipasir_add(-1).unwrap();
509        solver.ipasir_add(0).unwrap();
510        assert!(!solver.ipasir_solve().unwrap().unwrap());
511    }
512
513    #[test]
514    fn test_assume() {
515        let loader = solver_loader_or_return!();
516        let mut solver = loader.new_solver().unwrap();
517        solver.ipasir_assume(1).unwrap();
518        assert!(solver.ipasir_solve().unwrap().unwrap());
519        assert!(solver.ipasir_val(1).unwrap().unwrap());
520        solver.ipasir_assume(-1).unwrap();
521        assert!(solver.ipasir_solve().unwrap().unwrap());
522        assert!(!solver.ipasir_val(1).unwrap().unwrap());
523        solver.ipasir_assume(1).unwrap();
524        solver.ipasir_assume(-1).unwrap();
525        assert!(!solver.ipasir_solve().unwrap().unwrap());
526    }
527
528    #[test]
529    fn test_failed() {
530        let loader = solver_loader_or_return!();
531        let mut solver = loader.new_solver().unwrap();
532        solver.ipasir_add(-1).unwrap();
533        solver.ipasir_add(0).unwrap();
534        solver.ipasir_assume(1).unwrap();
535        solver.ipasir_assume(2).unwrap();
536        assert!(!solver.ipasir_solve().unwrap().unwrap());
537        assert!(solver.ipasir_failed(1).unwrap());
538        assert!(!solver.ipasir_failed(2).unwrap());
539    }
540
541    #[allow(clippy::cast_possible_truncation, clippy::cast_possible_wrap)]
542    fn encode_php(solver: &mut IpasirSolver, n: usize) {
543        let n = n as i32;
544        let mut add_clause = |lits: &[i32]| {
545            for lit in lits {
546                solver.ipasir_add(*lit).unwrap();
547            }
548            solver.ipasir_add(0).unwrap();
549        };
550        for var0 in 1..=n {
551            let mut lit0 = -var0;
552            for i in 0..n {
553                let mut lit1 = lit0 - n;
554                for _ in 0..(n - i) {
555                    add_clause(&[lit0, lit1]);
556                    lit1 -= n;
557                }
558                lit0 -= n;
559            }
560        }
561        (0..=n)
562            .map(|i| (i * n + 1..=(i + 1) * n))
563            .for_each(|r| add_clause(&r.collect::<Vec<_>>()));
564    }
565
566    #[test]
567    fn test_set_terminate() {
568        let mut loader = solver_loader_or_return!();
569        loader.enable_set_terminate(true);
570        let mut solver = loader.new_solver().unwrap();
571        encode_php(&mut solver, 20);
572        let called = Rc::new(RefCell::new(false));
573        let called_cl = Rc::clone(&called);
574        let callback = Box::new(move || {
575            *called_cl.borrow_mut() = true;
576            true
577        });
578        solver.ipasir_set_terminate(callback).unwrap();
579        assert!(solver.ipasir_solve().unwrap().is_none());
580        assert!(*called.borrow());
581    }
582
583    #[test]
584    fn test_set_learn() {
585        let mut loader = solver_loader_or_return!();
586        loader.enable_set_learn(Some(i32::MAX));
587        let mut solver = loader.new_solver().unwrap();
588        encode_php(&mut solver, 3);
589        let n_lits = Rc::new(RefCell::new(0));
590        let n_lits_cl = Rc::clone(&n_lits);
591        let callback = Box::new(move |clause: &[i32]| {
592            *n_lits_cl.borrow_mut() += clause.len();
593        });
594        solver.ipasir_set_learn(callback).unwrap();
595        assert!(!solver.ipasir_solve().unwrap().unwrap());
596        assert_ne!(*n_lits.borrow(), 0);
597    }
598
599    #[test]
600    fn test_set_terminate_is_disabled() {
601        let loader = solver_loader_or_return!();
602        let mut solver = loader.new_solver().unwrap();
603        solver.ipasir_set_terminate(Box::new(|| true)).unwrap_err();
604    }
605
606    #[test]
607    fn test_set_learn_is_disabled() {
608        let loader = solver_loader_or_return!();
609        let mut solver = loader.new_solver().unwrap();
610        solver.ipasir_set_learn(Box::new(|_| {})).unwrap_err();
611    }
612
613    #[test]
614    fn test_forbidden_functions_on_input_state() {
615        let loader = solver_loader_or_return!();
616        let mut solver = loader.new_solver().unwrap();
617        solver.ipasir_add(-1).unwrap();
618        solver.ipasir_add(0).unwrap();
619        solver.ipasir_assume(1).unwrap();
620        solver.ipasir_val(1).unwrap_err();
621        solver.ipasir_failed(1).unwrap_err();
622    }
623
624    #[test]
625    fn test_forbidden_functions_on_sat_state() {
626        let loader = solver_loader_or_return!();
627        let mut solver = loader.new_solver().unwrap();
628        solver.ipasir_add(-1).unwrap();
629        solver.ipasir_add(0).unwrap();
630        assert!(solver.ipasir_solve().unwrap().unwrap());
631        solver.ipasir_failed(1).unwrap_err();
632    }
633
634    #[test]
635    fn test_forbidden_functions_on_unsat_state() {
636        let loader = solver_loader_or_return!();
637        let mut solver = loader.new_solver().unwrap();
638        solver.ipasir_add(-1).unwrap();
639        solver.ipasir_add(0).unwrap();
640        solver.ipasir_add(1).unwrap();
641        solver.ipasir_add(0).unwrap();
642        assert!(!solver.ipasir_solve().unwrap().unwrap());
643        solver.ipasir_val(1).unwrap_err();
644    }
645
646    #[test]
647    fn test_xor() {
648        let loader = solver_loader_or_return!();
649        let mut solver = loader.new_solver().unwrap();
650        solver.ipasir_add(-1).unwrap();
651        solver.ipasir_add(-2).unwrap();
652        solver.ipasir_add(0).unwrap();
653        solver.ipasir_add(1).unwrap();
654        solver.ipasir_add(2).unwrap();
655        solver.ipasir_add(0).unwrap();
656        assert!(solver.ipasir_solve().unwrap().unwrap());
657        let model = vec![solver.ipasir_val(1).unwrap(), solver.ipasir_val(2).unwrap()];
658        let expected_1 = vec![Some(true), Some(false)];
659        let expected_2 = vec![Some(false), Some(true)];
660        assert!(model == expected_1 || model == expected_2);
661    }
662}
ipasir_loading/lib.rs

ipasir_loading/
lib.rs
