Report whether a file declared a c t track (#41)

`CnfMeta::mode` was a public field that resolved an absent `c t` line to
`Mc`, so `c t mc` and a file with no header at all read back
identically.
A consumer that varies its own defaults between a competition instance
and a
plain CNF had nothing to key on — and the show set and the weights
already
answer the same question with an `Option`.

The track is now stored as `Option<Mode>` behind two accessors:
`CnfMeta::declared_track` reports the line the file carried, and
`CnfMeta::mode` reports the track to read the file as, still resolving
an
absent line to `Mc`. `CnfMeta::from_parts` takes the option as well, so
metadata assembled in process can state absence the way a parsed file
does.

This replaces the public field, so a caller reading a track moves to
`mode()`, and one that needs to know whether the file said so moves to
`declared_track()`. Inside the crate only mode detection in
`resolve_mode`
read it.

Author: guyvdbroeck

src/cnf/dimacs.rs

@@ -225,7 +225,10 @@ impl CnfFormula {
         let mut clauses = Vec::new();
         let mut current_clause: Vec<Literal> = Vec::new();
         let mut line_num = 0usize;
-        let mut mode = Mode::default();
+        // Stays `None` until a `c t` line names a track, so that `c t mc` and a
+        // file carrying no such line remain distinguishable — see
+        // [`CnfMeta::declared_track`].
+        let mut track: Option<Mode> = None;
         // The show set and weight lines are collected as written and converted
         // to indexed form only once every id is known to fit the declared
         // count — both conversions subtract one from a written id, and the
@@ -260,9 +263,9 @@ impl CnfFormula {
                     let toks: Vec<&str> = line.split_whitespace().collect();
                     match toks.as_slice() {
                         ["c", "t", ty] => {
-                            mode = Mode::parse_track(ty).ok_or_else(|| {
+                            track = Some(Mode::parse_track(ty).ok_or_else(|| {
                                 format!("line {line_num}: unknown problem type: {ty}")
-                            })?;
+                            })?);
                         }
                         ["c", "p", "show", rest @ ..] => {
                             saw_show = true;
@@ -382,7 +385,7 @@ impl CnfFormula {
             )
         };
         let meta =
-            CnfMeta::from_parts(num_vars, mode, show_vars, weights).map_err(|e| e.to_string())?;
+            CnfMeta::from_parts(num_vars, track, show_vars, weights).map_err(|e| e.to_string())?;
 
         Ok((CnfFormula { num_vars, clauses }, meta))
     }

src/cnf/mod.rs

@@ -192,8 +192,10 @@ impl Mode {
 /// preprocessing renumbers variables.
 #[derive(Clone, Debug, Default)]
 pub struct CnfMeta {
-    /// The declared counting track; `Mode::Mc` if no `c t` line was seen.
-    pub mode: Mode,
+    /// The track a `c t` line named, read through [`CnfMeta::declared_track`],
+    /// or resolved to `Mode::Mc` through [`CnfMeta::mode`]. `None` when no
+    /// `c t` line is present.
+    track: Option<Mode>,
     /// The show set for projected counting, read through
     /// [`CnfMeta::declared_show_vars`]; the projected-out set is
     /// `all_vars \ show_vars`. `None` when no `c p show` line is present.
@@ -211,8 +213,9 @@ impl CnfMeta {
     /// therefore contains 0-based ids. `weights` remains the sparse table of
     /// explicit signed 1-based DIMACS literal declarations; omitted literals
     /// are not materialized. `None` means the corresponding declaration was
-    /// absent, while `Some(ShowSet::empty())` and `Some` of an empty
-    /// [`WeightTable`] preserve explicit empty declarations.
+    /// absent, for `track` as well as for the other two, while
+    /// `Some(ShowSet::empty())` and `Some` of an empty [`WeightTable`] preserve
+    /// explicit empty declarations.
     ///
     /// Passing the formula's declared count is mandatory: metadata assembled
     /// in-process is range-checked exactly as metadata read from DIMACS is.
@@ -224,7 +227,7 @@ impl CnfMeta {
     /// space.
     pub fn from_parts(
         num_vars: u32,
-        mode: Mode,
+        track: Option<Mode>,
         show_vars: Option<ShowSet<Original>>,
         weights: Option<WeightTable>,
     ) -> Result<Self, crate::error::VitriError> {
@@ -241,12 +244,31 @@ impl CnfMeta {
             weights.validate_num_vars(num_vars)?;
         }
         Ok(CnfMeta {
-            mode,
+            track,
             show_vars,
             weights,
         })
     }
 
+    /// The track this file's `c t` line named, or `None` when it carried no
+    /// such line.
+    ///
+    /// Declaring a track and counting under one are different questions, as
+    /// they are for the show set and the weights below. [`Self::mode`] answers
+    /// the second, resolving an absent line to [`Mode::Mc`]; this answers the
+    /// first, and is the only thing that tells `c t mc` apart from a file
+    /// carrying no header at all. A consumer whose own defaults differ between
+    /// a competition instance and a plain CNF reads this one, not `mode`.
+    pub fn declared_track(&self) -> Option<Mode> {
+        self.track
+    }
+
+    /// The counting track to read this file as: the one its `c t` line named,
+    /// or [`Mode::Mc`] when it carried no such line.
+    pub fn mode(&self) -> Mode {
+        self.track.unwrap_or_default()
+    }
+
     /// The show set this file declares, or `None` when it carried no
     /// `c p show` line.
     ///

src/config/mod.rs

@@ -984,11 +984,11 @@ impl RunConfig {
     /// instance.)
     pub fn resolve_mode(&self, meta: &crate::cnf::CnfMeta) -> Result<ResolvedMode, VitriError> {
         use crate::cnf::Mode;
-        let declares_weights = meta.mode.is_weighted() || meta.declared_weights().is_some();
+        let declares_weights = meta.mode().is_weighted() || meta.declared_weights().is_some();
         // Detection asks a wider question than "does the file carry a show set":
         // a `c t pmc` header asks for a projected count even before the
         // `c p show` line that must accompany it is read.
-        let declares_show = meta.mode.is_projected() || meta.declared_show_vars().is_some();
+        let declares_show = meta.mode().is_projected() || meta.declared_show_vars().is_some();
         let detected = match (declares_show, declares_weights) {
             (false, false) => Mode::Mc,
             (false, true) => Mode::Wmc,

src/tests/bundle/harness.rs

@@ -204,7 +204,8 @@ impl RoundTrip {
             self.mode
         };
         assert_eq!(
-            self.reparsed_meta.mode, expect_header,
+            self.reparsed_meta.mode(),
+            expect_header,
             "reduced.cnf's `c t` header must name the track the record does",
         );
         if self.mode == Mode::Compile {

src/tests/bundle/writer.rs

@@ -62,7 +62,7 @@ fn writer_round_trips_every_header() {
     .expect("write");
     let (reparsed, meta) = parse(&std::fs::read_to_string(&path).expect("read"));
     assert_eq!(reparsed, formula);
-    assert_eq!(meta.mode, Mode::Pwmc);
+    assert_eq!(meta.mode(), Mode::Pwmc);
     assert_eq!(
         meta.declared_show_vars().map(|s| s.to_dimacs()),
         Some(vec![1, 3]),

src/tests/cnf/meta_lines.rs

@@ -82,7 +82,7 @@ fn test_parse_mcc_weighted_meta() {
     let (formula, meta) = CnfFormula::from_dimacs(&input[..]).unwrap();
     assert_eq!(formula.num_vars, 2);
     assert_eq!(formula.clauses.len(), 1);
-    assert_eq!(meta.mode, Mode::Wmc);
+    assert_eq!(meta.mode(), Mode::Wmc);
     let wt = meta.weights.expect("weights parsed");
     let resolved: Weights<Original> = wt.resolve(2); // (w_neg, w_pos) per var
     let r = |n: i64, d: i64| {
@@ -96,7 +96,7 @@ fn test_parse_mcc_weighted_meta() {
 fn test_parse_show_set() {
     let input = b"c t pmc\np cnf 4 1\nc p show 1 3 0\n1 -2 3 0\n";
     let (_f, meta) = CnfFormula::from_dimacs(&input[..]).unwrap();
-    assert_eq!(meta.mode, Mode::Pmc);
+    assert_eq!(meta.mode(), Mode::Pmc);
     assert_eq!(
         meta.declared_show_vars(),
         Some(&ShowSet::from_zero_based([0, 2]))
@@ -107,11 +107,45 @@ fn test_parse_show_set() {
 fn test_plain_mc_meta_default() {
     let input = b"p cnf 2 1\n1 2 0\n";
     let (_f, meta) = CnfFormula::from_dimacs(&input[..]).unwrap();
-    assert_eq!(meta.mode, Mode::Mc);
+    assert_eq!(meta.mode(), Mode::Mc);
     assert!(meta.declared_show_vars().is_none());
     assert!(meta.weights.is_none());
 }
 
+/// A `c t` line is what makes a file DECLARE a track, and `c t mc` declares one
+/// as much as `c t pmc` does. `mode` cannot say so — it reads `Mc` for a file
+/// with no such line too — which is why the declaration is reported separately.
+#[test]
+fn declared_track_reports_the_line_not_the_resolved_mode() {
+    let (_, projected) =
+        CnfFormula::from_dimacs(&b"c t pmc\np cnf 6 1\nc p show 2 3 0\n1 -2 0\n"[..])
+            .expect("must parse");
+    assert_eq!(projected.declared_track(), Some(Mode::Pmc));
+    assert_eq!(projected.mode(), Mode::Pmc);
+
+    let (_, plain) =
+        CnfFormula::from_dimacs(&b"c t mc\np cnf 2 1\n1 2 0\n"[..]).expect("must parse");
+    assert_eq!(
+        plain.declared_track(),
+        Some(Mode::Mc),
+        "`c t mc` names a track, so the file declares one",
+    );
+    assert_eq!(plain.mode(), Mode::Mc);
+
+    let (_, bare) =
+        CnfFormula::from_dimacs(&b"c comment\np cnf 3 2\n1 -2 0\n2 3 0\n"[..]).expect("must parse");
+    assert_eq!(
+        bare.declared_track(),
+        None,
+        "no `c t` line means no declaration, however `mode` resolves",
+    );
+    assert_eq!(
+        bare.mode(),
+        Mode::Mc,
+        "an absent track still reads as plain model counting",
+    );
+}
+
 #[test]
 fn test_parse_c_p_show_accumulates_and_dedups() {
     let input = b"p cnf 4 1\nc p show 3 1 0\nc p show 1 2 0\n1 2 3 4 0\n";

src/tests/cnf/round_trip.rs

@@ -47,7 +47,7 @@ fn a_parsed_formula_reparses_from_the_dimacs_it_writes() {
     let declared = meta.weights.as_ref().expect("the fixture declares weights");
     let rows = declared_rows(declared);
     let header = DimacsHeader {
-        track: Some(meta.mode.token()),
+        track: meta.declared_track().map(Mode::token),
         show: meta.declared_show_vars(),
         weights: Some(&rows),
     };
@@ -56,7 +56,8 @@ fn a_parsed_formula_reparses_from_the_dimacs_it_writes() {
 
     assert_eq!(again, formula, "the clause set changed through write→read");
     assert_eq!(
-        again_meta.mode, meta.mode,
+        again_meta.declared_track(),
+        meta.declared_track(),
         "the track the file declared changed through write→read",
     );
     assert_eq!(
@@ -143,7 +144,8 @@ fn a_written_track_header_comes_back_as_the_mode_it_names() {
         };
         let (_, meta) = write_then_read("dimacs-track", &formula, &header);
         assert_eq!(
-            meta.mode, mode,
+            meta.declared_track(),
+            Some(mode),
             "the `c t` line written for {mode:?} read back as something else",
         );
     }

src/tests/cnf/types.rs

@@ -48,13 +48,20 @@ fn a_programmatic_weight_table_is_sparse_and_the_last_duplicate_wins() {
 
 /// Absence and an explicit empty declaration remain different values at the
 /// programmatic boundary, just as no `c p show` line differs from
-/// `c p show 0` in a file.
+/// `c p show 0` in a file. The track is the same kind of value: `None` is an
+/// undeclared track, not `mc`.
 #[test]
 fn programmatic_metadata_preserves_empty_declarations_and_absence() {
     let empty_weights = WeightTable::from_dimacs_pairs(Vec::new(), 3)
         .expect("an empty table has no out-of-range literal");
-    let declared = CnfMeta::from_parts(3, Mode::Pwmc, Some(ShowSet::empty()), Some(empty_weights))
-        .expect("empty declarations are valid");
+    let declared = CnfMeta::from_parts(
+        3,
+        Some(Mode::Pwmc),
+        Some(ShowSet::empty()),
+        Some(empty_weights),
+    )
+    .expect("empty declarations are valid");
+    assert_eq!(declared.declared_track(), Some(Mode::Pwmc));
     assert_eq!(declared.declared_show_vars(), Some(&ShowSet::empty()));
     assert_eq!(
         declared
@@ -64,8 +71,14 @@ fn programmatic_metadata_preserves_empty_declarations_and_absence() {
         Vec::new(),
     );
 
-    let absent = CnfMeta::from_parts(3, Mode::Pwmc, None, None)
+    let absent = CnfMeta::from_parts(3, None, None, None)
         .expect("absent declarations carry no ids to validate");
+    assert_eq!(absent.declared_track(), None);
+    assert_eq!(
+        absent.mode(),
+        Mode::Mc,
+        "an undeclared track still resolves to plain model counting",
+    );
     assert!(absent.declared_show_vars().is_none());
     assert!(absent.declared_weights().is_none());
 }
@@ -103,8 +116,13 @@ fn zero_and_out_of_range_programmatic_show_ids_are_input_errors() {
     );
     assert!(zero.to_string().contains('0'), "{zero} must name zero");
 
-    let err = CnfMeta::from_parts(3, Mode::Pmc, Some(ShowSet::from_zero_based([3])), None)
-        .expect_err("zero-based id 3 is DIMACS variable 4, above num_vars 3");
+    let err = CnfMeta::from_parts(
+        3,
+        Some(Mode::Pmc),
+        Some(ShowSet::from_zero_based([3])),
+        None,
+    )
+    .expect_err("zero-based id 3 is DIMACS variable 4, above num_vars 3");
     assert!(
         matches!(err, crate::error::VitriError::Input { .. }),
         "malformed metadata is input, got {err:?}",

tests/cli/output_bytes.rs

@@ -200,7 +200,7 @@ fn reduced_cnf_alone_states_the_problem_it_belongs_to() {
     let (_, meta) =
         CnfFormula::from_dimacs(std::io::BufReader::new(file)).expect("the emitted CNF must parse");
 
-    assert_eq!(meta.mode.token(), record["mode"]);
+    assert_eq!(meta.mode().token(), record["mode"]);
 
     let show_from_cnf: Vec<u64> = meta
         .declared_show_vars()