Fix bool_lit can be zero

viperproject · Dec 12, 2024 · 6e77282 · 6e77282
1 parent ef3b2c1
commit 6e77282
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 10 deletions.
diff --git a/smt-log-parser/src/error.rs b/smt-log-parser/src/error.rs
@@ -78,7 +78,7 @@ pub enum Error {
     // Enode
     UnknownEnode(TermIdx),
     EnodePoppedFrame(StackIdx),
-    InvalidGeneration(ParseIntError),
+    InvalidGeneration(nonmax::ParseIntError),
     EnodeRootMismatch(ENodeIdx, ENodeIdx),
 
     // Stack
@@ -90,7 +90,7 @@ pub enum Error {
     NoConflict,
     BoolLiteral,
     BoolLiteralNotP,
-    InvalidBoolLiteral(ParseIntError),
+    InvalidBoolLiteral(nonmax::ParseIntError),
     UnknownJustification(String),
     MissingColonJustification,
 

diff --git a/smt-log-parser/src/mem_dbg/mod.rs b/smt-log-parser/src/mem_dbg/mod.rs
@@ -110,6 +110,12 @@ macro_rules! derive_non_max {
                 self.0.fmt(f)
             }
         }
+        impl core::str::FromStr for $name {
+            type Err = <nonmax::$name as core::str::FromStr>::Err;
+            fn from_str(s: &str) -> Result<Self, Self::Err> {
+                nonmax::$name::from_str(s).map(Self)
+            }
+        }
     };
 }
 

diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs
@@ -1,7 +1,4 @@
-use core::{
-    num::{NonZeroU32, NonZeroUsize},
-    ops::Index,
-};
+use core::{num::NonZeroUsize, ops::Index};
 
 #[cfg(feature = "mem_dbg")]
 use mem_dbg::{MemDbg, MemSize};
@@ -102,8 +99,8 @@ impl Z3Parser {
         l: &mut impl Iterator<Item = &'a str>,
     ) -> Result<Option<NonMaxU32>> {
         if let Some(gen) = l.next() {
-            let gen = gen.parse::<u32>().map_err(E::InvalidGeneration)?;
-            Ok(Some(NonMaxU32::new(gen).unwrap()))
+            let gen = gen.parse::<NonMaxU32>().map_err(E::InvalidGeneration)?;
+            Ok(Some(gen))
         } else {
             Ok(None)
         }
@@ -386,7 +383,7 @@ impl Z3Parser {
     fn parse_bool_literal<'a>(
         &mut self,
         l: &mut impl Iterator<Item = &'a str>,
-    ) -> Result<Option<(Option<NonZeroU32>, bool)>> {
+    ) -> Result<Option<(Option<NonMaxU32>, bool)>> {
         let Some(lit) = l.next() else {
             return Ok(None);
         };
@@ -410,7 +407,7 @@ impl Z3Parser {
             };
             (lit.strip_prefix('p').ok_or(E::BoolLiteralNotP)?, value)
         };
-        let bool_lit = lit.parse::<NonZeroU32>().map_err(E::InvalidBoolLiteral)?;
+        let bool_lit = lit.parse::<NonMaxU32>().map_err(E::InvalidBoolLiteral)?;
         Ok(Some((Some(bool_lit), value)))
     }
 }