feat: ipasir-display feature

enabling this feature changes the behaviour of the `Var` and `Lit`
implementations of the `Display` trait to use IPASIR indexing

rustsat/Cargo.toml

@@ -39,6 +39,7 @@ multiopt = ["optimization"]
 compression = ["dep:bzip2", "dep:flate2", "dep:xz2"]
 rand = ["dep:rand"]
 bench = []
+ipasir-display = []
 all = ["multiopt", "compression", "rand", "fxhash"]
 
 [package.metadata.docs.rs]

rustsat/examples/print-lits.rs

@@ -0,0 +1,31 @@
+//! Example to showcase `ipasir-display` feature
+
+macro_rules! show_ipasir_var {
+    ($ipasir:expr) => {{
+        println!(
+            "`Display` IPASIR literal {:3}: {:>16}",
+            $ipasir,
+            format!("{}", rustsat::ipasir_lit![$ipasir])
+        );
+        println!(
+            "`Display` IPASIR literal {:3}: {:>16}",
+            -$ipasir,
+            format!("{}", rustsat::ipasir_lit![-$ipasir])
+        );
+        println!(
+            "  `Debug` IPASIR literal {:3}: {:>2?}",
+            $ipasir,
+            rustsat::ipasir_lit![$ipasir]
+        );
+        println!(
+            "  `Debug` IPASIR literal {:3}: {:>2?}",
+            -$ipasir,
+            rustsat::ipasir_lit![-$ipasir]
+        );
+    }};
+}
+
+fn main() {
+    show_ipasir_var![1];
+    show_ipasir_var![42];
+}

rustsat/src/lib.rs

@@ -47,13 +47,14 @@
 //!
 //! | Feature name | Description |
 //! | --- | --- |
-//! | `internals` | Make some internal data structures for e.g. encodings public. This is useful when basing a more complex encoding on the `rustsat` implementation of another encoding. Note that the internal API might change between releases. |
-//! | `fxhash` | Use the faster firefox hash function from `rustc-hash` in `rustsat`. |
 //! | `optimization` | Include optimization (MaxSAT) data structures etc. |
 //! | `multiopt` | Include data structures etc. for multi-objective optimization. |
 //! | `compression` | Enable parsing and writing compressed input. |
-//! | `bench` | Enable benchmark tests. Behind feature flag since it requires unstable Rust. |
+//! | `fxhash` | Use the faster firefox hash function from `rustc-hash` in `rustsat`. |
 //! | `rand` | Enable randomization features. (Shuffling clauses etc.) |
+//! | `ipasir-display` | Changes `Display` trait for `Lit` and `Var` types to follow IPASIR variables indexing. |
+//! | `bench` | Enable benchmark tests. Behind feature flag since it requires unstable Rust. |
+//! | `internals` | Make some internal data structures for e.g. encodings public. This is useful when basing a more complex encoding on the `rustsat` implementation of another encoding. Note that the internal API might change between releases. |
 //!
 //! ## Examples
 //!

rustsat/src/types.rs

@@ -204,7 +204,11 @@ impl ops::SubAssign<u32> for Var {
 /// Variables can be printed with the [`Display`](std::fmt::Display) trait
 impl fmt::Display for Var {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "x{}", self.idx)
+        if cfg!(feature = "ipasir-display") {
+            write!(f, "x{}", self.to_ipasir())
+        } else {
+            write!(f, "x{}", self.idx())
+        }
     }
 }
 
@@ -460,10 +464,7 @@ impl ops::Sub<u32> for Lit {
 /// Literals can be printed with the [`Display`](std::fmt::Display) trait
 impl fmt::Display for Lit {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        match self.is_neg() {
-            true => write!(f, "~x{}", self.vidx()),
-            false => write!(f, "x{}", self.vidx()),
-        }
+        write!(f, "{}{}", if self.is_neg() { "~" } else { "" }, self.var())
     }
 }