Use non-zero ints to allow Option optimisations

viperproject · Jan 15, 2024 · 5d19387 · 5d19387
1 parent 44da0bb
commit 5d19387
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 11 deletions.
diff --git a/smt-log-parser/src/error.rs b/smt-log-parser/src/error.rs
@@ -1,6 +1,6 @@
 use std::{collections::TryReserveError, num::ParseIntError};
 
-use crate::items::{TermId, TermIdx, StackIdx, ENodeIdx, BlameKind};
+use crate::items::{TermId, TermIdx, StackIdx, ENodeIdx, BlameKind, Fingerprint};
 
 pub type Result<T> = std::result::Result<T, Error>;
 pub type FResult<T> = std::result::Result<T, FatalError>;
@@ -44,6 +44,7 @@ pub enum Error {
 
     // Fingerprint
     InvalidFingerprint(ParseIntError),
+    UnknownFingerprint(Fingerprint),
 
     // Enode
     UnknownEnode(TermIdx),

diff --git a/smt-log-parser/src/items.rs b/smt-log-parser/src/items.rs
@@ -2,7 +2,7 @@ use fxhash::FxHashMap;
 use serde::{Deserialize, Serialize};
 use std::borrow::Cow;
 use std::fmt;
-use std::num::NonZeroU32;
+use std::num::{NonZeroU32, NonZeroUsize};
 use crate::{Result, Error};
 
 pub type StringTable = lasso::Rodeo<lasso::Spur, fxhash::FxBuildHasher>;
@@ -12,17 +12,17 @@ pub type IString = lasso::Spur;
 macro_rules! idx {
     ($struct:ident, $prefix:tt) => {
         #[derive(
-            Clone, Copy, Default, Eq, PartialEq, Serialize, Deserialize, PartialOrd, Ord, Hash,
+            Clone, Copy, Eq, PartialEq, Serialize, Deserialize, PartialOrd, Ord, Hash,
         )]
-        pub struct $struct(usize);
+        pub struct $struct(NonZeroUsize);
         impl From<usize> for $struct {
             fn from(value: usize) -> Self {
-                Self(value)
+                Self(NonZeroUsize::new(value.checked_add(1).unwrap()).unwrap())
             }
         }
         impl From<$struct> for usize {
             fn from(value: $struct) -> Self {
-                value.0
+                value.0.get() - 1
             }
         }
         impl fmt::Debug for $struct {

diff --git a/smt-log-parser/src/parsers/z3/inst.rs b/smt-log-parser/src/parsers/z3/inst.rs
@@ -25,12 +25,14 @@ impl Insts {
         Ok(idx)
     }
 
-    pub fn new_inst(&mut self, fingerprint: Fingerprint, mut inst: Instantiation) -> Result<InstIdx> {
-        let (match_idx, inst_idx) = self
+    pub fn get_match(&self, fingerprint: Fingerprint) -> Option<MatchIdx> {
+        self.fingerprint_to_match.get(&fingerprint).map(|(idx, _)| *idx)
+    }
+    pub fn new_inst(&mut self, fingerprint: Fingerprint, inst: Instantiation) -> Result<InstIdx> {
+        let (_, inst_idx) = self
             .fingerprint_to_match
             .get_mut(&fingerprint)
             .expect(&format!("{:x}", fingerprint.0));
-        inst.match_ = *match_idx;
         self.insts.raw.try_reserve(1)?;
         let idx = self.insts.push_and_get_key(inst);
         debug_assert!(inst_idx.is_none(), "duplicate fingerprint");

diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs
@@ -503,9 +503,9 @@ impl Z3LogParser for Z3Parser {
         Self::expect_completed(proof)?;
         let z3_generation = Self::parse_z3_generation(&mut l)?;
 
+        let match_ = self.insts.get_match(fingerprint).ok_or(Error::UnknownFingerprint(fingerprint))?;
         let inst = Instantiation {
-            // Will be filled in by `new_inst`
-            match_: MatchIdx::default(),
+            match_,
             fingerprint,
             proof_id,
             z3_generation,