rustsat/
types.rs

1//! # Common Types for SAT Solving
2//!
3//! Common types used throughout the library to guarantee type safety.
4
5use core::ffi::c_int;
6use std::{
7    fmt,
8    ops::{self, Index, IndexMut},
9    path::Path,
10};
11
12use anyhow::Context;
13use thiserror::Error;
14
15pub mod constraints;
16pub use constraints::{Cl, Clause};
17
18use crate::instances::fio::{self, SolverOutput};
19
20/// The hash map to use throughout the library
21#[cfg(feature = "fxhash")]
22pub type RsHashMap<K, V> = rustc_hash::FxHashMap<K, V>;
23/// The hash map to use throughout the library
24#[cfg(not(feature = "fxhash"))]
25pub type RsHashMap<K, V> = std::collections::HashMap<K, V>;
26
27/// The hash set to use throughout the library
28#[cfg(feature = "fxhash")]
29pub type RsHashSet<V> = rustc_hash::FxHashSet<V>;
30/// The hash set to use throughout the library
31#[cfg(not(feature = "fxhash"))]
32pub type RsHashSet<V> = std::collections::HashSet<V>;
33
34/// The hasher to use throughout the library
35#[cfg(feature = "fxhash")]
36pub type RsHasher = rustc_hash::FxHasher;
37/// The hasher to use throughout the library
38#[cfg(not(feature = "fxhash"))]
39pub type RsHasher = std::collections::hash_map::DefaultHasher;
40
41/// [`u32`] with an upper bound, mainly used for safe `serde::Deserialize`
42#[derive(Hash, Eq, PartialEq, PartialOrd, Clone, Copy, Ord)]
43#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
44#[cfg_attr(feature = "serde", serde(try_from = "u32"))]
45#[repr(transparent)]
46struct LimitedU32<const U: u32>(u32);
47
48impl<const U: u32> TryFrom<u32> for LimitedU32<U> {
49    type Error = LimitedU32Error<U>;
50
51    fn try_from(value: u32) -> Result<Self, Self::Error> {
52        if value > U {
53            Err(LimitedU32Error(()))
54        } else {
55            Ok(Self(value))
56        }
57    }
58}
59
60/// Error when creating a limited range [`u32`] and the value exceeds the limit
61#[derive(thiserror::Error, Debug)]
62struct LimitedU32Error<const U: u32>(());
63
64impl<const U: u32> std::fmt::Display for LimitedU32Error<U> {
65    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
66        write!(f, "value must at most be {U}")
67    }
68}
69
70const MAX_VAR_IDX: u32 = (u32::MAX - 1) / 2;
71
72/// Type representing boolean variables in a SAT problem. Variables indexing in
73/// RustSAT starts from 0 and the maximum index is `(u32::MAX - 1) / 2`. This is
74/// because literals are represented as a single `u32` as well. The memory
75/// representation of variables is `u32`.
76#[derive(Hash, Eq, PartialEq, PartialOrd, Clone, Copy, Ord)]
77#[allow(clippy::unsafe_derive_deserialize)] // temporary, proper fix is in the works
78#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
79#[repr(transparent)]
80// this is fine because we are going through `LimitedU32`, which is deserialized via `try_from`
81#[allow(clippy::unsafe_derive_deserialize)]
82pub struct Var {
83    idx: LimitedU32<MAX_VAR_IDX>,
84}
85
86impl Var {
87    /// The maximum index that can be represented.
88    pub const MAX_IDX: u32 = MAX_VAR_IDX;
89
90    /// Creates a new variables with a given index.
91    /// Indices start from 0.
92    ///
93    /// # Panics
94    ///
95    /// If `idx > Var::MAX_IDX`.
96    #[must_use]
97    pub const fn new(idx: u32) -> Var {
98        assert!(idx <= Var::MAX_IDX, "variable index too high");
99        Var {
100            idx: LimitedU32(idx),
101        }
102    }
103
104    /// Creates a new variables with a given index.
105    /// Indices start from 0.
106    ///
107    /// # Errors
108    ///
109    /// `TypeError::IdxTooHigh(idx, Var::MAX_IDX)` if `idx > Var::MAX_IDX`.
110    pub fn new_with_error(idx: u32) -> Result<Var, TypeError> {
111        Ok(Var {
112            idx: idx
113                .try_into()
114                .map_err(|_| TypeError::IdxTooHigh(idx, Var::MAX_IDX))?,
115        })
116    }
117
118    /// Creates a new variables with a given index.
119    /// Indices start from 0.
120    /// Does not perform any check on the index, therefore might produce an inconsistent variable.
121    /// Only use this for performance reasons if you are sure that `idx <= Var::MAX_IDX`.
122    ///
123    /// # Safety
124    ///
125    /// `idx` must be guaranteed to be not higher than `Var::MAX_IDX`
126    #[inline]
127    #[must_use]
128    pub const unsafe fn new_unchecked(idx: u32) -> Var {
129        debug_assert!(idx <= Var::MAX_IDX);
130        Var {
131            idx: LimitedU32(idx),
132        }
133    }
134
135    /// Creates a literal with a given negation from the variable
136    ///
137    /// # Examples
138    ///
139    /// ```
140    /// # use rustsat::types::{Var,Lit};
141    /// let var = Var::new(5);
142    /// let lit = Lit::positive(5);
143    /// assert_eq!(lit, var.lit(false));
144    /// ```
145    #[inline]
146    #[must_use]
147    pub const fn lit(self, negated: bool) -> Lit {
148        unsafe { Lit::new_unchecked(self.idx.0, negated) }
149    }
150
151    /// Creates a literal that is not negated.
152    ///
153    /// # Examples
154    ///
155    /// ```
156    /// # use rustsat::types::{Var,Lit};
157    /// let var = Var::new(5);
158    /// let lit = Lit::positive(5);
159    /// assert_eq!(lit, var.pos_lit());
160    /// ```
161    #[inline]
162    #[must_use]
163    pub const fn pos_lit(self) -> Lit {
164        unsafe { Lit::positive_unchecked(self.idx.0) }
165    }
166
167    /// Creates a negated literal.
168    ///
169    /// # Examples
170    ///
171    /// ```
172    /// # use rustsat::types::{Var,Lit};
173    /// let var = Var::new(5);
174    /// let lit = Lit::negative(5);
175    /// assert_eq!(lit, var.neg_lit());
176    /// ```
177    #[inline]
178    #[must_use]
179    pub const fn neg_lit(self) -> Lit {
180        unsafe { Lit::negative_unchecked(self.idx.0) }
181    }
182
183    /// Returns the index of the variable. This is a `usize` to enable easier
184    /// indexing of data structures like vectors, even though the internal
185    /// representation of a variable is `u32`. For the 32 bit index use
186    /// [`Var::idx32`].
187    ///
188    /// # Examples
189    ///
190    /// ```
191    /// # use rustsat::types::Var;
192    /// let var = Var::new(5);
193    /// assert_eq!(5, var.idx());
194    /// ```
195    #[inline]
196    #[must_use]
197    pub fn idx(self) -> usize {
198        self.idx.0 as usize
199    }
200
201    /// Returns the 32 bit index of the variable.
202    ///
203    /// # Examples
204    ///
205    /// ```
206    /// # use rustsat::types::Var;
207    /// let var = Var::new(5);
208    /// assert_eq!(5, var.idx32());
209    /// ```
210    #[inline]
211    #[must_use]
212    pub fn idx32(self) -> u32 {
213        self.idx.0
214    }
215
216    /// Converts the variable to an integer as accepted by
217    /// [IPASIR](https://github.com/biotomas/ipasir) and the [DIMACS file
218    /// format](http://www.satcompetition.org/2011/format-benchmarks2011.html). The IPASIR variable
219    /// will have `idx+1`.
220    ///
221    /// # Panics
222    ///
223    /// If the variable index does not fit in `c_int`. As [`c_int` will almost always be
224    /// `i32`](https://doc.rust-lang.org/std/os/raw/type.c_int.html), this is only the case on very
225    /// esoteric platforms.
226    #[must_use]
227    pub fn to_ipasir(self) -> c_int {
228        (self.idx32() + 1)
229            .try_into()
230            .expect("variable index too high to fit in c_int")
231    }
232
233    /// Converts the variable to an integer as accepted by
234    /// [IPASIR](https://github.com/biotomas/ipasir) and the [DIMACS file
235    /// format](http://www.satcompetition.org/2011/format-benchmarks2011.html). The IPASIR literal
236    /// will have `idx+1` and be negative if the literal is negated.
237    ///
238    /// # Errors
239    ///
240    /// `TypeError::IdxTooHigh(_, _)` if the literal does not fit into a `c_int`. As [`c_int` will
241    /// almost always be `i32`](https://doc.rust-lang.org/std/os/raw/type.c_int.html), it is mostly
242    /// safe to simply use [`Self::to_ipasir`] instead.
243    pub fn to_ipasir_with_error(self) -> Result<c_int, TypeError> {
244        (self.idx32() + 1)
245            .try_into()
246            .map_err(|_| TypeError::IdxTooHigh(self.idx32() + 1, c_int::MAX as u32))
247    }
248}
249
250/// Incrementing variables
251impl ops::Add<u32> for Var {
252    type Output = Var;
253
254    fn add(self, rhs: u32) -> Self::Output {
255        let idx = self.idx.0 + rhs;
256        debug_assert!(idx <= Var::MAX_IDX, "variable index overflow");
257        Var {
258            idx: LimitedU32(idx),
259        }
260    }
261}
262
263impl ops::AddAssign<u32> for Var {
264    fn add_assign(&mut self, rhs: u32) {
265        debug_assert!(self.idx.0 + rhs <= Var::MAX_IDX, "variable index overflow");
266        self.idx.0 += rhs;
267    }
268}
269
270/// Decrementing variables
271impl ops::Sub<u32> for Var {
272    type Output = Var;
273
274    fn sub(self, rhs: u32) -> Self::Output {
275        Var {
276            idx: LimitedU32(self.idx.0 - rhs),
277        }
278    }
279}
280
281impl ops::SubAssign<u32> for Var {
282    fn sub_assign(&mut self, rhs: u32) {
283        self.idx.0 -= rhs;
284    }
285}
286
287/// Variables can be printed with the [`Display`](std::fmt::Display) trait
288impl fmt::Display for Var {
289    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
290        if cfg!(feature = "ipasir-display") {
291            write!(f, "x{}", self.to_ipasir())
292        } else {
293            write!(f, "x{}", self.idx())
294        }
295    }
296}
297
298/// Variables can be printed with the [`Debug`](std::fmt::Debug) trait
299impl fmt::Debug for Var {
300    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
301        write!(f, "x{}", self.idx.0)
302    }
303}
304
305#[cfg(kani)]
306impl kani::Arbitrary for Var {
307    fn any() -> Self {
308        let idx = u32::any();
309        kani::assume(idx <= Var::MAX_IDX);
310        Var::new(idx)
311    }
312}
313
314/// More easily creates variables. Mainly used in tests.
315///
316/// # Examples
317///
318/// ```
319/// # use rustsat::{var, types::Var};
320/// assert_eq!(var![42], Var::new(42));
321/// ```
322#[macro_export]
323macro_rules! var {
324    ($v:expr) => {
325        $crate::types::Var::new($v)
326    };
327}
328
329/// Type representing literals, possibly negated boolean variables.
330///
331/// # Representation in Memory
332///
333/// Literal representation is `idx << 1` with the last bit representing
334/// whether the literal is negated or not. This way the literal can directly
335/// be used to index data structures with the two literals of a variable
336/// being close together.
337#[derive(Hash, Eq, PartialEq, PartialOrd, Ord, Clone, Copy)]
338#[allow(clippy::unsafe_derive_deserialize)] // temporary, proper fix is in the works
339#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
340#[repr(transparent)]
341// this is fine because there aren't any invalid `Lit` representations, only invalid `Var` ones
342#[allow(clippy::unsafe_derive_deserialize)]
343pub struct Lit {
344    lidx: u32,
345}
346
347impl Lit {
348    /// Represents a literal in memory
349    #[inline]
350    const fn represent(idx: u32, negated: bool) -> u32 {
351        (idx << 1) + if negated { 1 } else { 0 }
352    }
353
354    /// Creates a new (negated or not) literal with a given index.
355    ///
356    /// # Panics
357    ///
358    /// If `idx > Var::MAX_IDX`.
359    #[must_use]
360    pub const fn new(idx: u32, negated: bool) -> Lit {
361        assert!(idx < Var::MAX_IDX, "variable index too high");
362        Lit {
363            lidx: Lit::represent(idx, negated),
364        }
365    }
366
367    /// Creates a new (negated or not) literal with a given index.
368    ///
369    /// # Errors
370    ///
371    /// `TypeError::IdxTooHigh(idx, Var::MAX_IDX)` if `idx > Var::MAX_IDX`.
372    pub fn new_with_error(idx: u32, negated: bool) -> Result<Lit, TypeError> {
373        if idx > Var::MAX_IDX {
374            return Err(TypeError::IdxTooHigh(idx, Var::MAX_IDX));
375        }
376        Ok(Lit {
377            lidx: Lit::represent(idx, negated),
378        })
379    }
380
381    /// Creates a new (negated or not) literal with a given index.
382    /// Does not perform any check on the index, therefore might produce an inconsistent variable.
383    /// Only use this for performance reasons if you are sure that `idx <= Var::MAX_IDX`.
384    ///
385    /// # Safety
386    ///
387    /// `idx` must be guaranteed to be not higher than `Var::MAX_IDX`
388    #[must_use]
389    pub const unsafe fn new_unchecked(idx: u32, negated: bool) -> Lit {
390        debug_assert!(idx <= Var::MAX_IDX);
391        Lit {
392            lidx: Lit::represent(idx, negated),
393        }
394    }
395
396    /// Creates a new positive literal with a given index.
397    /// Panics if `idx > Var::MAX_IDX`.
398    #[inline]
399    #[must_use]
400    pub const fn positive(idx: u32) -> Lit {
401        Lit::new(idx, false)
402    }
403
404    /// Creates a new negated literal with a given index.
405    /// Panics if `idx > Var::MAX_IDX`.
406    #[inline]
407    #[must_use]
408    pub const fn negative(idx: u32) -> Lit {
409        Lit::new(idx, true)
410    }
411
412    /// Creates a new positive literal with a given index.
413    ///
414    /// # Errors
415    ///
416    /// If `idx > Var::MAX_IDX`.
417    #[inline]
418    pub fn positive_with_error(idx: u32) -> Result<Lit, TypeError> {
419        Lit::new_with_error(idx, false)
420    }
421
422    /// Creates a new negated literal with a given index.
423    ///
424    /// # Errors
425    ///
426    /// If `idx > Var::MAX_IDX`.
427    #[inline]
428    pub fn negative_with_error(idx: u32) -> Result<Lit, TypeError> {
429        Lit::new_with_error(idx, true)
430    }
431
432    /// Creates a new positive literal with a given index.
433    /// Does not perform any check on the index, therefore might produce an inconsistent variable.
434    /// Only use this for performance reasons if you are sure that `idx <= Var::MAX_IDX`.
435    ///
436    /// # Safety
437    ///
438    /// `idx` must be guaranteed to be not higher than `Var::MAX_IDX`
439    #[inline]
440    #[must_use]
441    pub const unsafe fn positive_unchecked(idx: u32) -> Lit {
442        Lit::new_unchecked(idx, false)
443    }
444
445    /// Creates a new negated literal with a given index.
446    /// Does not perform any check on the index, therefore might produce an inconsistent variable.
447    /// Only use this for performance reasons if you are sure that `idx <= Var::MAX_IDX`.
448    ///
449    /// # Safety
450    ///
451    /// `idx` must be guaranteed to be not higher than `Var::MAX_IDX`
452    #[inline]
453    #[must_use]
454    pub const unsafe fn negative_unchecked(idx: u32) -> Lit {
455        Lit::new_unchecked(idx, true)
456    }
457
458    /// Create a literal from an
459    /// [IPASIR](https://github.com/biotomas/ipasir)/[DIMACS](http://www.satcompetition.org/2011/format-benchmarks2011.html)
460    /// integer value.
461    ///
462    /// # Errors
463    ///
464    /// If the value is zero or the index too high.
465    pub fn from_ipasir(val: c_int) -> Result<Lit, TypeError> {
466        if val == 0 {
467            return Err(TypeError::IpasirZero);
468        }
469        let negated = val < 0;
470        let idx = val.unsigned_abs();
471        Lit::new_with_error(idx - 1, negated)
472    }
473
474    /// Gets the variable index of the literal
475    #[inline]
476    #[must_use]
477    pub fn vidx(self) -> usize {
478        (self.lidx >> 1) as usize
479    }
480
481    /// Gets the 32-bit variable index of the literal
482    #[inline]
483    #[must_use]
484    pub fn vidx32(self) -> u32 {
485        self.lidx >> 1
486    }
487
488    /// Gets a literal representation for indexing data structures
489    #[inline]
490    #[must_use]
491    pub fn lidx(self) -> usize {
492        self.lidx as usize
493    }
494
495    /// Gets the variables that the literal corresponds to.
496    ///
497    /// # Examples
498    ///
499    /// ```
500    /// # use rustsat::types::{Var,Lit};
501    /// let var = Var::new(5);
502    /// let lit = Lit::negative(5);
503    /// assert_eq!(var, lit.var());
504    /// ```
505    #[inline]
506    #[must_use]
507    pub fn var(self) -> Var {
508        unsafe { Var::new_unchecked(self.vidx32()) }
509    }
510
511    /// True if the literal is positive.
512    #[inline]
513    #[must_use]
514    pub fn is_pos(self) -> bool {
515        (self.lidx & 1u32) == 0
516    }
517
518    /// True if the literal is negated.
519    #[inline]
520    #[must_use]
521    pub fn is_neg(self) -> bool {
522        (self.lidx & 1u32) == 1
523    }
524
525    /// Converts the literal to an integer as accepted by
526    /// [IPASIR](https://github.com/biotomas/ipasir) and the
527    /// [DIMACS file format](http://www.satcompetition.org/2011/format-benchmarks2011.html). The
528    /// IPASIR literal will have `idx+1` and be negative if the literal is negated. Panics if the
529    /// literal does not fit into a `c_int`.
530    ///
531    /// # Panics
532    ///
533    /// If the variable index does not fit in `c_int`. As [`c_int` will almost always be
534    /// `i32`](https://doc.rust-lang.org/std/os/raw/type.c_int.html), this is only the case on very
535    /// esoteric platforms.
536    #[must_use]
537    pub fn to_ipasir(self) -> c_int {
538        let negated = self.is_neg();
539        let idx: c_int = (self.vidx32() + 1)
540            .try_into()
541            .expect("variable index too high to fit in c_int");
542        if negated {
543            -idx
544        } else {
545            idx
546        }
547    }
548
549    /// Converts the literal to an integer as accepted by
550    /// [IPASIR](https://github.com/biotomas/ipasir) and the [DIMACS file
551    /// format](http://www.satcompetition.org/2011/format-benchmarks2011.html). The IPASIR literal
552    /// will have `idx+1` and be negative if the literal is negated.
553    ///
554    /// # Errors
555    ///
556    /// `TypeError::IdxTooHigh(_, _)` if the literal does not fit into a `c_int`. As [`c_int`
557    /// will almost always be `i32`](https://doc.rust-lang.org/std/os/raw/type.c_int.html), it is
558    /// mostly safe to simply use [`Self::to_ipasir`] instead.
559    pub fn to_ipasir_with_error(self) -> Result<c_int, TypeError> {
560        let negated = self.is_neg();
561        let idx: c_int = match (self.vidx() + 1).try_into() {
562            Ok(idx) => idx,
563            Err(_) => return Err(TypeError::IdxTooHigh(self.vidx32() + 1, c_int::MAX as u32)),
564        };
565        Ok(if negated { -idx } else { idx })
566    }
567}
568
569/// Trait implementation allowing for negating literals with the `!` operator.
570impl ops::Not for Lit {
571    type Output = Lit;
572
573    #[inline]
574    fn not(self) -> Lit {
575        Lit {
576            lidx: self.lidx ^ 1u32,
577        }
578    }
579}
580
581/// Trait implementation allowing for negating literals with the unary `-` operator.
582impl ops::Neg for Lit {
583    type Output = Lit;
584
585    #[inline]
586    fn neg(self) -> Lit {
587        Lit {
588            lidx: self.lidx ^ 1u32,
589        }
590    }
591}
592
593/// Incrementing literals. This preserves the sign of the literal.
594impl ops::Add<u32> for Lit {
595    type Output = Lit;
596
597    fn add(self, rhs: u32) -> Self::Output {
598        Lit {
599            lidx: self.lidx + 2 * rhs,
600        }
601    }
602}
603
604/// Decrementing literals. This preserves the sign of the literal.
605impl ops::Sub<u32> for Lit {
606    type Output = Lit;
607
608    fn sub(self, rhs: u32) -> Self::Output {
609        Lit {
610            lidx: self.lidx - 2 * rhs,
611        }
612    }
613}
614
615/// Literals can be printed with the [`Display`](std::fmt::Display) trait
616impl fmt::Display for Lit {
617    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
618        write!(f, "{}{}", if self.is_neg() { "~" } else { "" }, self.var())
619    }
620}
621
622/// Literals can be printed with the [`Debug`](std::fmt::Debug) trait
623impl fmt::Debug for Lit {
624    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
625        if self.is_neg() {
626            write!(f, "~x{}", self.vidx())
627        } else {
628            write!(f, "x{}", self.vidx())
629        }
630    }
631}
632
633#[cfg(kani)]
634impl kani::Arbitrary for Lit {
635    fn any() -> Self {
636        let var = Var::any();
637        var.lit(bool::any())
638    }
639}
640
641/// More easily creates literals. Mainly used in tests.
642///
643/// # Examples
644///
645/// ```
646/// # use rustsat::{lit, types::Lit};
647/// assert_eq!(lit![42], Lit::positive(42));
648/// assert_eq!(!lit![42], Lit::negative(42));
649/// ```
650#[macro_export]
651macro_rules! lit {
652    ($l:expr) => {
653        $crate::types::Lit::positive($l)
654    };
655}
656
657/// More easily creates literals with
658/// [IPASIR](https://github.com/biotomas/ipasir)/[DIMACS](http://www.satcompetition.org/2011/format-benchmarks2011.html)
659/// indexing (starts from 1) and negation (negative value is negation). Mainly used in tests.
660///
661/// # Examples
662///
663/// ```
664/// # use rustsat::{lit, ipasir_lit, types::Lit};
665/// assert_eq!(ipasir_lit![42], lit![41]);
666/// assert_eq!(ipasir_lit![-42], !lit![41]);
667/// ```
668#[macro_export]
669macro_rules! ipasir_lit {
670    ($l:expr) => {
671        $crate::types::Lit::from_ipasir($l).unwrap()
672    };
673}
674
675/// Ternary value assigned to a literal or variable, including possible "don't care"
676#[derive(Clone, Copy, PartialEq, Eq, Default)]
677#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
678#[repr(u8)]
679pub enum TernaryVal {
680    /// Positive assignment.
681    True,
682    /// Negative assignment.
683    False,
684    /// Formula is satisfied, no matter the assignment.
685    #[default]
686    DontCare,
687}
688
689impl TernaryVal {
690    /// Converts a [`TernaryVal`] to a [`bool`] with a default value for "don't cares"
691    #[must_use]
692    pub fn to_bool_with_def(self, def: bool) -> bool {
693        match self {
694            TernaryVal::True => true,
695            TernaryVal::False => false,
696            TernaryVal::DontCare => def,
697        }
698    }
699}
700
701/// Ternary values can be printed with the [`Display`](std::fmt::Display) trait
702impl fmt::Display for TernaryVal {
703    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
704        match self {
705            TernaryVal::True => write!(f, "1"),
706            TernaryVal::False => write!(f, "0"),
707            TernaryVal::DontCare => write!(f, "_"),
708        }
709    }
710}
711
712/// Ternary values can be printed with the [`Debug`](std::fmt::Debug) trait
713impl fmt::Debug for TernaryVal {
714    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
715        match self {
716            TernaryVal::True => write!(f, "1"),
717            TernaryVal::False => write!(f, "0"),
718            TernaryVal::DontCare => write!(f, "_"),
719        }
720    }
721}
722
723impl From<bool> for TernaryVal {
724    fn from(value: bool) -> Self {
725        if value {
726            return TernaryVal::True;
727        }
728        TernaryVal::False
729    }
730}
731
732impl ops::Not for TernaryVal {
733    type Output = TernaryVal;
734
735    fn not(self) -> Self::Output {
736        match self {
737            TernaryVal::True => TernaryVal::False,
738            TernaryVal::False => TernaryVal::True,
739            TernaryVal::DontCare => TernaryVal::DontCare,
740        }
741    }
742}
743
744impl ops::Neg for TernaryVal {
745    type Output = TernaryVal;
746
747    fn neg(self) -> Self::Output {
748        match self {
749            TernaryVal::True => TernaryVal::False,
750            TernaryVal::False => TernaryVal::True,
751            TernaryVal::DontCare => TernaryVal::DontCare,
752        }
753    }
754}
755
756#[cfg(kani)]
757impl kani::Arbitrary for TernaryVal {
758    fn any() -> Self {
759        let val: u8 = kani::any();
760        kani::assume(val < 3);
761        match val {
762            0 => TernaryVal::False,
763            1 => TernaryVal::True,
764            2 => TernaryVal::DontCare,
765            _ => panic!(),
766        }
767    }
768}
769
770/// Possible errors in parsing a SAT solver value (`v`) line
771#[derive(Error, Debug)]
772pub enum InvalidVLine {
773    /// The given `v` line starts with an invalid character
774    #[error("The value line does not start with 'v ' but with {0}")]
775    InvalidTag(char),
776    /// The `v` line contains a conflicting assignment on the given variable
777    #[error("The output of the SAT solver assigned different values to variable {0}")]
778    ConflictingAssignment(Var),
779    /// The given `v` line is empty
780    #[error("Empty value line")]
781    EmptyLine,
782}
783
784/// Different possible `v`-line formats
785enum VLineFormat {
786    /// Assignment specified as a space-separated sequence of IPASIR literals. This is the format
787    /// used in the SAT competition.
788    SatComp,
789    /// Assignment specified as a sequence of zeroes and ones. This is the format used in the
790    /// MaxSAT Evaluation.
791    MaxSatEval,
792    /// Assignment specified as a sequence of space-separated OPB literals. This is the format used
793    /// in the PB competition.
794    PbComp,
795}
796
797/// Type representing an assignment of variables.
798#[derive(Clone, PartialEq, Eq, Default)]
799#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
800#[repr(transparent)]
801pub struct Assignment {
802    assignment: Vec<TernaryVal>,
803}
804
805impl Assignment {
806    /// Gets the length of the assignment
807    #[must_use]
808    pub fn len(&self) -> usize {
809        self.assignment.len()
810    }
811
812    /// Checks whether the assignment is empty
813    #[must_use]
814    pub fn is_empty(&self) -> bool {
815        self.assignment.is_empty()
816    }
817
818    /// Get the value that the solution assigns to a variable.
819    /// If the variable is not included in the solution, will return `TernaryVal::DontCare`.
820    #[must_use]
821    pub fn var_value(&self, var: Var) -> TernaryVal {
822        if var.idx() >= self.assignment.len() {
823            TernaryVal::DontCare
824        } else {
825            self.assignment[var.idx()]
826        }
827    }
828
829    /// Same as [`Assignment::var_value`], but for literals.
830    #[must_use]
831    pub fn lit_value(&self, lit: Lit) -> TernaryVal {
832        if lit.is_neg() {
833            match self.var_value(lit.var()) {
834                TernaryVal::DontCare => TernaryVal::DontCare,
835                TernaryVal::True => TernaryVal::False,
836                TernaryVal::False => TernaryVal::True,
837            }
838        } else {
839            self.var_value(lit.var())
840        }
841    }
842
843    /// Replaces unassigned variables in the assignment with a default value
844    pub fn replace_dont_care(&mut self, def: bool) {
845        self.assignment.iter_mut().for_each(|tv| {
846            if tv == &TernaryVal::DontCare {
847                if def {
848                    *tv = TernaryVal::True;
849                } else {
850                    *tv = TernaryVal::False;
851                }
852            }
853        });
854    }
855
856    /// Assigns a variable in the assignment
857    pub fn assign_var(&mut self, variable: Var, value: TernaryVal) {
858        if self.assignment.len() < variable.idx() + 1 {
859            self.assignment
860                .resize(variable.idx() + 1, TernaryVal::DontCare);
861        }
862        self.assignment[variable.idx()] = value;
863    }
864
865    /// Assigns a literal to true
866    pub fn assign_lit(&mut self, lit: Lit) {
867        let val = if lit.is_pos() {
868            TernaryVal::True
869        } else {
870            TernaryVal::False
871        };
872        self.assign_var(lit.var(), val);
873    }
874
875    /// Truncates a solution to only include assignments up to a maximum variable
876    #[must_use]
877    pub fn truncate(mut self, max_var: Var) -> Self {
878        self.assignment.truncate(max_var.idx() + 1);
879        self
880    }
881
882    /// Get the maximum variable in the assignment
883    ///
884    /// # Panics
885    ///
886    /// If the assignment contains more then `u32::MAX` variables.
887    #[must_use]
888    pub fn max_var(&self) -> Option<Var> {
889        if self.assignment.is_empty() {
890            None
891        } else {
892            Some(var![
893                u32::try_from(self.assignment.len())
894                    .expect("assignment contains more than `u32::MAX` variables")
895                    - 1
896            ])
897        }
898    }
899
900    /// Reads a solution from SAT solver output given the path
901    ///
902    /// If it is unclear whether the SAT solver indicated satisfiability, use [`fio::parse_sat_solver_output`] instead.
903    ///
904    /// # Errors
905    ///
906    /// - IO error: [`std::io::Error`]
907    /// - Invalid solver output: [`fio::SatSolverOutputError`]
908    /// - Invalid v line: [`InvalidVLine`]
909    pub fn from_solver_output_path<P: AsRef<Path>>(path: P) -> anyhow::Result<Self> {
910        let mut reader = std::io::BufReader::new(
911            fio::open_compressed_uncompressed_read(path).context("failed to open reader")?,
912        );
913        let output = fio::parse_sat_solver_output(&mut reader)?;
914        match output {
915            SolverOutput::Sat(solution) => Ok(solution),
916            _ => anyhow::bail!("solver output does not indicate satisfiability"),
917        }
918    }
919
920    /// Creates an assignment from a SAT solver value line
921    ///
922    /// # Errors
923    ///
924    /// [`InvalidVLine`] or parsing error, or [`nom::error::Error`]
925    pub fn from_vline(line: &str) -> anyhow::Result<Self> {
926        let mut assignment = Assignment::default();
927        assignment.extend_from_vline(line)?;
928        Ok(assignment)
929    }
930
931    /// Parses an assignment from a value line returned by a solver
932    ///
933    /// The following value line formats are supported:
934    /// - [SAT Competition](https://satcompetition.github.io/2024/output.html): `v 1 -2 -3 4 0`
935    /// - [MaxSAT Evaluation](https://maxsat-evaluations.github.io/2024/rules.html): `v 1001`
936    /// - [PB Competition](https://www.cril.univ-artois.fr/PB24/competitionRequirements.pdf): `v x1 -x2 -x3 x4`
937    ///
938    /// # Errors
939    ///
940    /// Can return various parsing errors
941    pub fn extend_from_vline(&mut self, lines: &str) -> anyhow::Result<()> {
942        anyhow::ensure!(!lines.is_empty(), InvalidVLine::EmptyLine);
943        // determine line format
944        let format = if lines.contains('x') {
945            VLineFormat::PbComp
946        } else if !lines[1..].trim().contains(' ')
947            && lines[1..].trim() != "0"
948            && lines[1..]
949                .trim()
950                .chars()
951                .try_for_each(|c| {
952                    if c == '1' || c == '0' {
953                        Ok(())
954                    } else {
955                        Err(())
956                    }
957                })
958                .is_ok()
959        {
960            VLineFormat::MaxSatEval
961        } else {
962            VLineFormat::SatComp
963        };
964
965        for line in lines.lines() {
966            if let Some(tag) = line.chars().next() {
967                anyhow::ensure!(tag == 'v', InvalidVLine::InvalidTag(tag));
968            } else {
969                anyhow::bail!(InvalidVLine::EmptyLine);
970            }
971
972            match format {
973                VLineFormat::SatComp => self.extend_sat_comp_vline(line),
974                VLineFormat::MaxSatEval => self.extend_maxsat_eval_vline(line),
975                VLineFormat::PbComp => self.extend_pb_comp_vline(line),
976            }?;
977        }
978        Ok(())
979    }
980
981    /// Parses a single SAT Competition v-line
982    fn extend_sat_comp_vline(&mut self, line: &str) -> anyhow::Result<()> {
983        let line = &line[1..];
984        for number in line.split_whitespace() {
985            let number = number.parse::<i32>()?;
986
987            // End of the value lines
988            if number == 0 {
989                continue;
990            }
991
992            let literal = Lit::from_ipasir(number)?;
993            let val = self.lit_value(literal);
994            if val == TernaryVal::True && literal.is_neg()
995                || val == TernaryVal::False && literal.is_pos()
996            {
997                // Catch conflicting assignments
998                anyhow::bail!(InvalidVLine::ConflictingAssignment(literal.var()));
999            }
1000            self.assign_lit(literal);
1001        }
1002        Ok(())
1003    }
1004
1005    /// Parses a single MaxSAT Evaluation v-line
1006    fn extend_maxsat_eval_vline(&mut self, line: &str) -> anyhow::Result<()> {
1007        let line = line[1..].trim();
1008        self.assignment.reserve(line.len());
1009        for char in line.chars() {
1010            match char {
1011                '0' => self.assignment.push(TernaryVal::False),
1012                '1' => self.assignment.push(TernaryVal::True),
1013                _ => anyhow::bail!("unexpected character in MaxSAT Evaluation v-line"),
1014            }
1015        }
1016        Ok(())
1017    }
1018
1019    /// Parses a single PB Competition v-line
1020    fn extend_pb_comp_vline(&mut self, line: &str) -> anyhow::Result<()> {
1021        let line = &line[1..];
1022        for number in line.split_whitespace() {
1023            let (_, lit) = fio::opb::literal(number, fio::opb::Options::default())
1024                .map_err(nom::Err::<nom::error::Error<&str>>::to_owned)
1025                .with_context(|| format!("failed to parse pb literal '{number}'"))?;
1026            let val = self.lit_value(lit);
1027            if val == TernaryVal::True && lit.is_neg() || val == TernaryVal::False && lit.is_pos() {
1028                // Catch conflicting assignments
1029                anyhow::bail!(InvalidVLine::ConflictingAssignment(lit.var()));
1030            }
1031            self.assign_lit(lit);
1032        }
1033        Ok(())
1034    }
1035
1036    /// Gets an iterator over literals assigned to true
1037    #[allow(clippy::cast_possible_truncation)]
1038    pub fn iter(&self) -> impl Iterator<Item = Lit> + '_ {
1039        self.assignment
1040            .iter()
1041            .enumerate()
1042            .filter_map(|(idx, tv)| match tv {
1043                TernaryVal::True => Some(Lit::new(idx as u32, false)),
1044                TernaryVal::False => Some(Lit::new(idx as u32, true)),
1045                TernaryVal::DontCare => None,
1046            })
1047    }
1048}
1049
1050#[cfg(kani)]
1051impl Assignment {
1052    /// Generates a random assignment with the given number of variables
1053    pub fn arbitrary(n_vars: u32) -> Self {
1054        Self::from_iter((0..n_vars).map(|_| <bool as kani::Arbitrary>::any()))
1055    }
1056}
1057
1058impl fmt::Debug for Assignment {
1059    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1060        self.assignment.iter().try_for_each(|tv| write!(f, "{tv}"))
1061    }
1062}
1063
1064impl fmt::Display for Assignment {
1065    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1066        self.assignment.iter().try_for_each(|tv| write!(f, "{tv}"))
1067    }
1068}
1069
1070/// Turns the assignment into an iterator over all true literals
1071impl IntoIterator for Assignment {
1072    type Item = Lit;
1073
1074    type IntoIter = std::iter::FilterMap<
1075        std::iter::Enumerate<std::vec::IntoIter<TernaryVal>>,
1076        fn((usize, TernaryVal)) -> Option<Lit>,
1077    >;
1078
1079    fn into_iter(self) -> Self::IntoIter {
1080        self.assignment
1081            .into_iter()
1082            .enumerate()
1083            .filter_map(|(idx, tv)| match tv {
1084                TernaryVal::True => Some(Var::new(idx.try_into().unwrap()).pos_lit()),
1085                TernaryVal::False => Some(Var::new(idx.try_into().unwrap()).neg_lit()),
1086                TernaryVal::DontCare => None,
1087            })
1088    }
1089}
1090
1091/// Turns the assignment reference into an iterator over all true literals
1092impl<'a> IntoIterator for &'a Assignment {
1093    type Item = Lit;
1094
1095    type IntoIter = std::iter::FilterMap<
1096        std::iter::Enumerate<std::slice::Iter<'a, TernaryVal>>,
1097        fn((usize, &TernaryVal)) -> Option<Lit>,
1098    >;
1099
1100    fn into_iter(self) -> Self::IntoIter {
1101        self.assignment
1102            .iter()
1103            .enumerate()
1104            .filter_map(|(idx, tv)| match tv {
1105                TernaryVal::True => Some(Var::new(idx.try_into().unwrap()).pos_lit()),
1106                TernaryVal::False => Some(Var::new(idx.try_into().unwrap()).neg_lit()),
1107                TernaryVal::DontCare => None,
1108            })
1109    }
1110}
1111
1112impl FromIterator<Lit> for Assignment {
1113    fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self {
1114        let mut assignment = Assignment::default();
1115        iter.into_iter().for_each(|l| assignment.assign_lit(l));
1116        assignment
1117    }
1118}
1119
1120impl FromIterator<TernaryVal> for Assignment {
1121    fn from_iter<T: IntoIterator<Item = TernaryVal>>(iter: T) -> Self {
1122        Self::from(iter.into_iter().collect::<Vec<_>>())
1123    }
1124}
1125
1126impl FromIterator<bool> for Assignment {
1127    fn from_iter<T: IntoIterator<Item = bool>>(iter: T) -> Self {
1128        iter.into_iter().map(TernaryVal::from).collect()
1129    }
1130}
1131
1132impl From<Vec<TernaryVal>> for Assignment {
1133    fn from(assignment: Vec<TernaryVal>) -> Self {
1134        Self { assignment }
1135    }
1136}
1137
1138impl Index<Var> for Assignment {
1139    type Output = TernaryVal;
1140
1141    fn index(&self, index: Var) -> &Self::Output {
1142        &self.assignment[index.idx()]
1143    }
1144}
1145
1146impl IndexMut<Var> for Assignment {
1147    fn index_mut(&mut self, index: Var) -> &mut Self::Output {
1148        &mut self.assignment[index.idx()]
1149    }
1150}
1151
1152/// Errors related to types
1153#[derive(Error, Debug)]
1154pub enum TypeError {
1155    /// The requested index is too high.
1156    /// Contains the requested and the maximum index.
1157    #[error("index {0} is too high (maximum {1})")]
1158    IdxTooHigh(u32, u32),
1159    /// IPASIR/DIMACS index is zero
1160    #[error("zero is an invalid IPASIR/DIMACS literal")]
1161    IpasirZero,
1162}
1163
1164/// An iterator over literals
1165pub trait LitIter: IntoIterator<Item = Lit> {}
1166impl<I: IntoIterator<Item = Lit>> LitIter for I {}
1167/// An iterator over clauses
1168pub trait ClsIter: IntoIterator<Item = Clause> {}
1169impl<I: IntoIterator<Item = Clause>> ClsIter for I {}
1170
1171/// An iterator over weighted literals
1172pub trait WLitIter: IntoIterator<Item = (Lit, usize)> {}
1173impl<I: IntoIterator<Item = (Lit, usize)>> WLitIter for I {}
1174/// An iterator over weighted clauses
1175pub trait WClsIter: IntoIterator<Item = (Clause, usize)> {}
1176impl<I: IntoIterator<Item = (Clause, usize)>> WClsIter for I {}
1177/// An iterator over integer-weighted literals
1178pub trait IWLitIter: IntoIterator<Item = (Lit, isize)> {}
1179impl<I: IntoIterator<Item = (Lit, isize)>> IWLitIter for I {}
1180
1181#[cfg(feature = "proof-logging")]
1182mod pigeons {
1183    use std::fmt;
1184
1185    /// A formatter for [`super::Var`] for use with the [`pigeons`] library to ensure same
1186    /// variable formatting as in VeriPB
1187    #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
1188    #[repr(transparent)]
1189    pub struct PidgeonVarFormatter(super::Var);
1190
1191    impl From<super::Var> for PidgeonVarFormatter {
1192        fn from(value: super::Var) -> Self {
1193            PidgeonVarFormatter(value)
1194        }
1195    }
1196
1197    impl fmt::Display for PidgeonVarFormatter {
1198        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1199            write!(f, "x{}", self.0.idx() + 1)
1200        }
1201    }
1202
1203    impl pigeons::VarLike for super::Var {
1204        type Formatter = PidgeonVarFormatter;
1205    }
1206
1207    impl From<super::Lit> for pigeons::Axiom<super::Var> {
1208        fn from(value: super::Lit) -> Self {
1209            use pigeons::VarLike;
1210
1211            if value.is_pos() {
1212                value.var().pos_axiom()
1213            } else {
1214                value.var().neg_axiom()
1215            }
1216        }
1217    }
1218}
1219
1220#[cfg(test)]
1221mod tests {
1222    use std::{mem::size_of, num::ParseIntError};
1223
1224    use super::{Assignment, InvalidVLine, Lit, TernaryVal, Var};
1225
1226    #[test]
1227    fn var_index() {
1228        let idx = 5;
1229        let var = Var::new(idx);
1230        assert_eq!(var.idx(), idx as usize);
1231    }
1232
1233    #[test]
1234    fn var_index32() {
1235        let idx = 5;
1236        let var = Var::new(idx);
1237        assert_eq!(var.idx32(), idx);
1238    }
1239
1240    #[test]
1241    fn var_pos_lit() {
1242        let idx = 5;
1243        let var = Var::new(idx);
1244        let lit = Lit::positive(idx);
1245        assert_eq!(var.pos_lit(), lit);
1246    }
1247
1248    #[test]
1249    fn var_neg_lit() {
1250        let idx = 5;
1251        let var = Var::new(idx);
1252        let lit = Lit::negative(idx);
1253        assert_eq!(var.neg_lit(), lit);
1254    }
1255
1256    #[test]
1257    fn var_from_lit() {
1258        let idx = 0;
1259        let lit = Lit::positive(idx);
1260        let var = Var::new(idx);
1261        assert_eq!(lit.var(), var);
1262    }
1263
1264    #[cfg(feature = "proof-logging")]
1265    #[test]
1266    fn proof_log_var() {
1267        use pigeons::VarLike;
1268        let var = Var::new(3);
1269        assert_eq!(&format!("{}", <Var as VarLike>::Formatter::from(var)), "x4");
1270    }
1271
1272    #[test]
1273    #[should_panic(expected = "variable index overflow")]
1274    fn var_add_1_overflow() {
1275        let var = Var::new(Var::MAX_IDX);
1276        let _ = var + 1;
1277    }
1278
1279    #[test]
1280    #[should_panic(expected = "variable index overflow")]
1281    fn var_add_42_overflow() {
1282        let var = Var::new(Var::MAX_IDX - 41);
1283        let _ = var + 42;
1284    }
1285
1286    #[test]
1287    #[should_panic(expected = "variable index overflow")]
1288    fn var_addassign_1_overflow() {
1289        let mut var = Var::new(Var::MAX_IDX);
1290        var += 1;
1291    }
1292
1293    #[test]
1294    #[should_panic(expected = "variable index overflow")]
1295    fn var_addassign_overflow() {
1296        let mut var = Var::new(Var::MAX_IDX - 41);
1297        var += 42;
1298    }
1299
1300    #[test]
1301    fn lit_representation() {
1302        let lidx = Lit::represent(5, true);
1303        assert_eq!(lidx, 0b1011);
1304    }
1305
1306    #[test]
1307    fn lit_is_pos() {
1308        let lit = Lit::positive(0);
1309        assert!(lit.is_pos());
1310        assert!(!lit.is_neg());
1311    }
1312
1313    #[test]
1314    fn lit_is_neg() {
1315        let lit = Lit::negative(0);
1316        assert!(!lit.is_pos());
1317        assert!(lit.is_neg());
1318    }
1319
1320    #[test]
1321    fn lit_negation() {
1322        let lit1 = Lit::positive(0);
1323        let lit2 = !lit1;
1324        assert!(!lit2.is_pos());
1325        assert!(lit2.is_neg());
1326        assert_eq!(lit1.var(), lit2.var());
1327    }
1328
1329    #[test]
1330    fn ipasir_lit_not_zero() {
1331        let lit = Lit::positive(0);
1332        assert_ne!(lit.to_ipasir(), 0);
1333        let lit = !lit;
1334        assert_ne!(lit.to_ipasir(), 0);
1335    }
1336
1337    #[test]
1338    fn ipasir_lit_idx_plus_one() {
1339        let idx = 5;
1340        let lit = Lit::positive(idx);
1341        assert_eq!(lit.to_ipasir(), i32::try_from(idx).unwrap() + 1);
1342        let lit = !lit;
1343        assert_eq!(lit.to_ipasir(), -(i32::try_from(idx).unwrap() + 1));
1344    }
1345
1346    #[test]
1347    fn ternary_var_true() {
1348        let tv = TernaryVal::True;
1349        assert!(tv.to_bool_with_def(true));
1350        assert!(tv.to_bool_with_def(false));
1351    }
1352
1353    #[test]
1354    fn ternary_var_false() {
1355        let tv = TernaryVal::False;
1356        assert!(!tv.to_bool_with_def(true));
1357        assert!(!tv.to_bool_with_def(false));
1358    }
1359
1360    #[test]
1361    fn ternary_var_dnc() {
1362        let tv = TernaryVal::DontCare;
1363        assert!(tv.to_bool_with_def(true));
1364        assert!(!tv.to_bool_with_def(false));
1365    }
1366
1367    #[test]
1368    fn sol_var_val() {
1369        let sol = Assignment::from(vec![
1370            TernaryVal::True,
1371            TernaryVal::False,
1372            TernaryVal::DontCare,
1373        ]);
1374        let val = sol.var_value(Var::new(0));
1375        assert_eq!(val, TernaryVal::True);
1376        let val = sol.var_value(Var::new(1));
1377        assert_eq!(val, TernaryVal::False);
1378        let val = sol.var_value(Var::new(2));
1379        assert_eq!(val, TernaryVal::DontCare);
1380    }
1381
1382    #[test]
1383    fn sol_lit_val() {
1384        let sol = Assignment::from(vec![
1385            TernaryVal::True,
1386            TernaryVal::False,
1387            TernaryVal::DontCare,
1388        ]);
1389        let val = sol.lit_value(Lit::negative(0));
1390        assert_eq!(val, TernaryVal::False);
1391        let val = sol.lit_value(Lit::positive(0));
1392        assert_eq!(val, TernaryVal::True);
1393        let val = sol.lit_value(Lit::negative(1));
1394        assert_eq!(val, TernaryVal::True);
1395        let val = sol.lit_value(Lit::positive(1));
1396        assert_eq!(val, TernaryVal::False);
1397        let val = sol.lit_value(Lit::negative(2));
1398        assert_eq!(val, TernaryVal::DontCare);
1399        let val = sol.lit_value(Lit::positive(2));
1400        assert_eq!(val, TernaryVal::DontCare);
1401    }
1402
1403    #[test]
1404    fn sol_repl_dont_care() {
1405        let mut sol = Assignment::from(vec![
1406            TernaryVal::True,
1407            TernaryVal::False,
1408            TernaryVal::DontCare,
1409        ]);
1410        sol.replace_dont_care(true);
1411        let val = sol.var_value(Var::new(0));
1412        assert_eq!(val, TernaryVal::True);
1413        let val = sol.var_value(Var::new(1));
1414        assert_eq!(val, TernaryVal::False);
1415        let val = sol.var_value(Var::new(2));
1416        assert_eq!(val, TernaryVal::True);
1417    }
1418
1419    #[test]
1420    fn sol_from_lits() {
1421        let true_sol = Assignment::from(vec![
1422            TernaryVal::True,
1423            TernaryVal::DontCare,
1424            TernaryVal::False,
1425        ]);
1426        let sol = Assignment::from_iter(vec![lit![0], !lit![2]]);
1427        assert_eq!(true_sol, sol);
1428    }
1429
1430    #[test]
1431    fn var_mem_size() {
1432        assert_eq!(size_of::<Var>(), size_of::<u32>());
1433    }
1434
1435    #[test]
1436    fn lit_mem_size() {
1437        assert_eq!(size_of::<Lit>(), size_of::<u32>());
1438    }
1439
1440    #[test]
1441    fn ternary_val_size() {
1442        assert_eq!(size_of::<TernaryVal>(), 1);
1443    }
1444
1445    #[test]
1446    fn parse_sat_comp_vline() {
1447        let vline = "v 1 -2 4 -5 6 0";
1448        let ground_truth = Assignment::from(vec![
1449            TernaryVal::True,
1450            TernaryVal::False,
1451            TernaryVal::DontCare,
1452            TernaryVal::True,
1453            TernaryVal::False,
1454            TernaryVal::True,
1455        ]);
1456        assert_eq!(Assignment::from_vline(vline).unwrap(), ground_truth);
1457        assert_eq!(
1458            {
1459                let mut assign = Assignment::default();
1460                assign.extend_from_vline(vline).unwrap();
1461                assign
1462            },
1463            ground_truth
1464        );
1465    }
1466
1467    #[test]
1468    fn parse_maxsat_eval_vline() {
1469        let vline = "v 100101";
1470        let ground_truth = Assignment::from(vec![
1471            TernaryVal::True,
1472            TernaryVal::False,
1473            TernaryVal::False,
1474            TernaryVal::True,
1475            TernaryVal::False,
1476            TernaryVal::True,
1477        ]);
1478        assert_eq!(Assignment::from_vline(vline).unwrap(), ground_truth);
1479        assert_eq!(
1480            {
1481                let mut assign = Assignment::default();
1482                assign.extend_from_vline(vline).unwrap();
1483                assign
1484            },
1485            ground_truth
1486        );
1487    }
1488
1489    #[test]
1490    fn parse_pb_comp_vline() {
1491        let vline = "v x1 -x2 x4 -x5 x6";
1492        let ground_truth = Assignment::from(vec![
1493            TernaryVal::True,
1494            TernaryVal::False,
1495            TernaryVal::DontCare,
1496            TernaryVal::True,
1497            TernaryVal::False,
1498            TernaryVal::True,
1499        ]);
1500        assert_eq!(Assignment::from_vline(vline).unwrap(), ground_truth);
1501        assert_eq!(
1502            {
1503                let mut assign = Assignment::default();
1504                assign.extend_from_vline(vline).unwrap();
1505                assign
1506            },
1507            ground_truth
1508        );
1509    }
1510
1511    #[test]
1512    fn vline_invalid_lit_from() {
1513        let vline = "v 1 -2 4 foo -5 bar 6 0";
1514        let res = Assignment::from_vline(vline);
1515        res.unwrap_err().downcast::<ParseIntError>().unwrap();
1516    }
1517
1518    #[test]
1519    fn vline_invalid_lit_extend() {
1520        let vline = "v 1 -2 4 foo -5 bar 6 0";
1521        let mut assign = Assignment::default();
1522        let res = assign.extend_from_vline(vline);
1523        res.unwrap_err().downcast::<ParseIntError>().unwrap();
1524    }
1525
1526    #[test]
1527    fn vline_invalid_tag_from() {
1528        let vline = "b 1 -2 4 -5 6 0";
1529        let res = Assignment::from_vline(vline);
1530        assert!(matches!(
1531            res.unwrap_err().downcast::<InvalidVLine>(),
1532            Ok(InvalidVLine::InvalidTag('b'))
1533        ));
1534    }
1535
1536    #[test]
1537    fn vline_invalid_tag_extend() {
1538        let vline = "b 1 -2 4 -5 6 0";
1539        let mut assign = Assignment::default();
1540        let res = assign.extend_from_vline(vline);
1541        assert!(matches!(
1542            res.unwrap_err().downcast::<InvalidVLine>(),
1543            Ok(InvalidVLine::InvalidTag('b'))
1544        ));
1545    }
1546
1547    #[test]
1548    fn vline_invalid_empty() {
1549        let vline = "";
1550        let res = Assignment::from_vline(vline);
1551        assert!(matches!(
1552            res.unwrap_err().downcast::<InvalidVLine>(),
1553            Ok(InvalidVLine::EmptyLine)
1554        ));
1555    }
1556
1557    #[test]
1558    fn multi_vline() {
1559        let vline = "v 1 2 3\nv 4 5 6 0";
1560        let ground_truth = Assignment::from(vec![
1561            TernaryVal::True,
1562            TernaryVal::True,
1563            TernaryVal::True,
1564            TernaryVal::True,
1565            TernaryVal::True,
1566            TernaryVal::True,
1567        ]);
1568        let res = Assignment::from_vline(vline).unwrap();
1569        assert_eq!(res, ground_truth);
1570    }
1571
1572    #[cfg(feature = "serde")]
1573    #[test]
1574    fn serde_var() {
1575        let var = Var::new(5);
1576        let json = serde_json::to_string(&var).unwrap();
1577        assert_eq!(json, r#"{"idx":5}"#);
1578        let roundtrip: Var = serde_json::from_str(&json).unwrap();
1579        assert_eq!(roundtrip, var);
1580    }
1581
1582    #[cfg(feature = "serde")]
1583    #[test]
1584    fn serde_var_invalid() {
1585        let failure: Result<Var, _> = serde_json::from_str("");
1586        assert!(failure.is_err());
1587    }
1588
1589    #[cfg(feature = "serde")]
1590    #[test]
1591    fn serde_lit() {
1592        let lit = Lit::new(5, true);
1593        let json = serde_json::to_string(&lit).unwrap();
1594        assert_eq!(json, r#"{"lidx":11}"#);
1595        let roundtrip: Lit = serde_json::from_str(&json).unwrap();
1596        assert_eq!(roundtrip, lit);
1597    }
1598
1599    #[test]
1600    fn assign_into_iter() {
1601        let assign = Assignment::from(vec![
1602            TernaryVal::True,
1603            TernaryVal::False,
1604            TernaryVal::True,
1605            TernaryVal::DontCare,
1606            TernaryVal::True,
1607            TernaryVal::False,
1608        ]);
1609        let lits: Vec<_> = assign.into_iter().collect();
1610        assert_eq!(lits, vec![lit![0], !lit![1], lit![2], lit![4], !lit![5]]);
1611    }
1612
1613    #[test]
1614    fn assign_ref_into_iter() {
1615        let assign = Assignment::from(vec![
1616            TernaryVal::True,
1617            TernaryVal::False,
1618            TernaryVal::True,
1619            TernaryVal::DontCare,
1620            TernaryVal::True,
1621            TernaryVal::False,
1622        ]);
1623        let lits: Vec<_> = (&assign).into_iter().collect();
1624        assert_eq!(lits, vec![lit![0], !lit![1], lit![2], lit![4], !lit![5]]);
1625        // ensure assign is still around, so we actually used a reference
1626        assert_eq!(assign.len(), 6);
1627    }
1628}
1629
1630#[cfg(kani)]
1631mod proofs {
1632    #[kani::proof]
1633    fn pos_lit() {
1634        let var: super::Var = kani::any();
1635        let lit = var.pos_lit();
1636        assert_eq!(var, lit.var());
1637    }
1638
1639    #[kani::proof]
1640    fn neg_lit() {
1641        let var: super::Var = kani::any();
1642        let lit = var.neg_lit();
1643        assert_eq!(var, lit.var());
1644    }
1645}
rustsat/types.rs

rustsat/
types.rs
