From e93aa6142aebf688b58f7bb2430d212e8ae9d1b0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Mon, 11 Nov 2024 17:19:40 +0100 Subject: [PATCH] Improve Synthetic term representation utilising niche optimisation --- smt-log-parser/src/analysis/generalise.rs | 2 +- smt-log-parser/src/display_with.rs | 9 +- smt-log-parser/src/parsers/z3/synthetic.rs | 192 ++++++++------------- smt-log-parser/src/parsers/z3/z3parser.rs | 4 +- 4 files changed, 75 insertions(+), 132 deletions(-) diff --git a/smt-log-parser/src/analysis/generalise.rs b/smt-log-parser/src/analysis/generalise.rs index 851247e5..9a173886 100644 --- a/smt-log-parser/src/analysis/generalise.rs +++ b/smt-log-parser/src/analysis/generalise.rs @@ -21,7 +21,7 @@ impl SynthTerms { let general_term = self.index(table, general); - let Some(general_kind) = general_term.kind().non_generalised() else { + let Some(general_kind) = general_term.kind().parsed() else { // if one of the terms is already generalised, no need to continue return self.new_generalised([general, larger.into()].into()); }; diff --git a/smt-log-parser/src/display_with.rs b/smt-log-parser/src/display_with.rs index 1460b3bb..7485b672 100644 --- a/smt-log-parser/src/display_with.rs +++ b/smt-log-parser/src/display_with.rs @@ -11,7 +11,7 @@ use crate::{ items::*, parsers::z3::{ stm2::EventKind, - synthetic::{SynthIdx, SynthTerm, SynthTermKind}, + synthetic::{AnyTerm, SynthIdx, SynthTermKind}, z3parser::Z3Parser, }, NonMaxU32, StringTable, @@ -423,11 +423,10 @@ impl<'a: 'b, 'b> DisplayWithCtxt, DisplayData<'b>> for &'a Term ctxt: &DisplayCtxt<'b>, data: &mut DisplayData<'b>, ) -> fmt::Result { - let sterm: &SynthTerm = self.into(); - sterm.fmt_with(f, ctxt, data) + self.as_any().fmt_with(f, ctxt, data) } } -impl<'a: 'b, 'b> DisplayWithCtxt, DisplayData<'b>> for &'a SynthTerm { +impl<'a: 'b, 'b> DisplayWithCtxt, DisplayData<'b>> for &'a AnyTerm { fn fmt_with( self, f: &mut fmt::Formatter<'_>, @@ -468,7 +467,7 @@ impl<'a, 'b> DisplayWithCtxt, DisplayData<'b>> for &'a SynthTerm ctxt: &DisplayCtxt<'b>, data: &mut DisplayData<'b>, ) -> fmt::Result { - match self.non_generalised() { + match self.parsed() { None => write!(f, "_"), Some(kind) => kind.fmt_with(f, ctxt, data), } diff --git a/smt-log-parser/src/parsers/z3/synthetic.rs b/smt-log-parser/src/parsers/z3/synthetic.rs index 22adf004..8e4fdfa0 100644 --- a/smt-log-parser/src/parsers/z3/synthetic.rs +++ b/smt-log-parser/src/parsers/z3/synthetic.rs @@ -11,141 +11,88 @@ use crate::{ use super::terms::Terms; +#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))] +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, PartialEq, Eq, Hash, Clone)] +pub enum AnyTerm { + Parsed(Term), + Synth(SynthTerm), +} + +#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))] +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, PartialEq, Eq, Hash, Clone)] +pub struct SynthTerm { + pub kind: SynthTermKind, + pub child_ids: BoxSlice, +} + #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))] #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] #[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)] #[repr(transparent)] -pub struct Synth(T); - -// #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))] -// #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] -// #[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)] -// pub enum MaybeSynth { -// Parsed(T), -// Synth(S), -// } +pub struct SynthIdx(TermIdx); -pub type SynthIdx = Synth; -pub type SynthTerm = Synth; -pub type SynthTermKind = Synth; +#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))] +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)] +pub enum SynthTermKind { + Parsed(TermKind), + Generalised, +} impl From for SynthIdx { fn from(tidx: TermIdx) -> Self { - Synth(tidx) + Self(tidx) } } -impl SynthTerm { +impl AnyTerm { pub fn id(&self) -> Option { - if self.0.id == TermId::default() { - None - } else { - Some(self.0.id) + match self { + AnyTerm::Parsed(term) => Some(term.id), + AnyTerm::Synth(_) => None, } } - pub fn kind<'a>(&'a self) -> &'a SynthTermKind { - let kind = &self.0.kind; - unsafe { std::mem::transmute::<&'a TermKind, &'a Synth>(kind) } + pub fn kind(&self) -> SynthTermKind { + match self { + AnyTerm::Parsed(term) => SynthTermKind::Parsed(term.kind), + AnyTerm::Synth(synth_term) => synth_term.kind, + } } pub fn child_ids<'a>(&'a self) -> &'a [SynthIdx] { - let child_ids = &*self.0.child_ids; - unsafe { std::mem::transmute::<&'a [TermIdx], &'a [Synth]>(child_ids) } - } -} - -impl<'a> From<&'a Term> for &'a SynthTerm { - fn from(term: &'a Term) -> Self { - unsafe { std::mem::transmute::<&'a Term, &'a Synth>(term) } + match self { + AnyTerm::Parsed(term) => { + let child_ids = &*term.child_ids; + unsafe { std::mem::transmute::<&'a [TermIdx], &'a [SynthIdx]>(child_ids) } + } + AnyTerm::Synth(synth_term) => &synth_term.child_ids, + } } } impl SynthTermKind { - pub fn non_generalised(&self) -> Option { - match self.0 { - TermKind::Var(u32::MAX) => None, - other => Some(other), + pub fn parsed(self) -> Option { + match self { + SynthTermKind::Parsed(p) => Some(p), + _ => None, } } } -// impl MaybeSynthKind { -// pub fn either_eq(self, other: Self) -> bool { -// match (self, other) { -// (Self::Parsed(TermKind::App(a)), Self::Synth(SynthTermKind::App(b))) -// | (Self::Synth(SynthTermKind::App(a)), Self::Parsed(TermKind::App(b))) => a == b, -// _ => self == other, -// } -// } -// } - -// impl<'a> MaybeSynthChildren<'a> { -// pub fn len(self) -> MaybeSynth { -// self.map(|t| t.len(), |t| t.len()) -// } -// pub fn get(self, idx: usize) -> MaybeSynthIdx { -// self.map(|t| t[idx].into(), |t| t[idx]).join() -// } - -// pub fn split_last(self) -> Option<(MaybeSynthIdx, MaybeSynthChildren<'a>)> { -// self.map( -// |t| { -// let (last, rest) = t.split_last()?; -// Some(( -// MaybeSynthIdx::Parsed(*last), -// MaybeSynthChildren::Parsed(rest), -// )) -// }, -// |t| { -// let (last, rest) = t.split_last()?; -// Some((*last, MaybeSynthChildren::Synth(rest))) -// }, -// ) -// .join() -// } - -// pub fn iter( -// self, -// ) -> MaybeSynth + 'a, impl Iterator + 'a> -// { -// self.map(|t| t.iter().copied(), |t| t.iter().copied()) -// } -// } -// impl<'a, T: Iterator + 'a, S: Iterator + 'a> Iterator -// for MaybeSynth -// { -// type Item = MaybeSynthIdx; -// fn next(&mut self) -> Option { -// match self { -// Self::Parsed(t) => t.next().map(MaybeSynthIdx::Parsed), -// Self::Synth(s) => s.next(), -// } -// } -// } - -// #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))] -// #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] -// #[derive(Debug, PartialEq, Eq, Hash, Clone)] -// pub struct SynthTerm { -// pub kind: SynthTermKind, -// pub child_ids: Box<[MaybeSynthIdx]>, -// } - -// #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))] -// #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] -// #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] -// pub enum SynthTermKind { -// App(IString), -// Generalised, -// } - -// impl SynthTermKind { -// pub fn new(kind: TermKind) -> Self { -// match kind { -// TermKind::App(name) => Self::App(name), -// other => panic!("Unexpected term kind: {:?}", other), -// } -// } -// } +impl Term { + const CHECK_REPR_EQ: bool = { + let sizeof_eq = core::mem::size_of::() == core::mem::size_of::(); + [(); 1][!sizeof_eq as usize]; + true + }; + pub fn as_any(&self) -> &AnyTerm { + assert!(Self::CHECK_REPR_EQ); + // SAFETY: `AnyTerm` and `Term` have the same memory layout since they + // have the same `size_of`. + unsafe { std::mem::transmute::<&Term, &AnyTerm>(self) } + } +} idx!(DefStIdx, "y{}"); @@ -153,7 +100,7 @@ idx!(DefStIdx, "y{}"); #[derive(Debug)] pub struct SynthTerms { start_idx: TermIdx, - synth_terms: TiVec, + synth_terms: TiVec, interned: FxHashMap, } @@ -182,7 +129,7 @@ impl SynthTerms { usize::from(dstidx) + usize::from(start_idx) < usize::MAX, "SynthIdx overflow {dstidx} + {start_idx}" ); - Synth(TermIdx::from(usize::from(dstidx) + usize::from(start_idx))) + SynthIdx(TermIdx::from(usize::from(dstidx) + usize::from(start_idx))) } pub fn eof(&mut self, start_idx: TermIdx) { @@ -193,18 +140,18 @@ impl SynthTerms { self.tidx_to_dstidx(sidx).err() } - pub(crate) fn index<'a>(&'a self, terms: &'a Terms, idx: SynthIdx) -> &SynthTerm { + pub(crate) fn index<'a>(&'a self, terms: &'a Terms, idx: SynthIdx) -> &AnyTerm { match self.tidx_to_dstidx(idx) { Ok(idx) => &self.synth_terms[idx], Err(tidx) => { let term = &terms[tidx]; - unsafe { std::mem::transmute::<&'a Term, &'a Synth>(term) } + term.as_any() } } } pub(crate) fn new_generalised(&mut self, child_ids: BoxSlice) -> Result { - self.insert(TermKind::Var(u32::MAX), child_ids) + self.insert(SynthTermKind::Generalised, child_ids) } pub(crate) fn new_synthetic( @@ -216,23 +163,20 @@ impl SynthTerms { child_ids.iter().any(|c| self.start_idx <= c.0), "Synthetic term must have at least one synthetic child" ); - self.insert(kind, child_ids) + self.insert(SynthTermKind::Parsed(kind), child_ids) } - fn insert(&mut self, kind: TermKind, child_ids: BoxSlice) -> Result { - let child_ids = - unsafe { std::mem::transmute::, BoxSlice>(child_ids) }; - let term = Synth(Term { + fn insert(&mut self, kind: SynthTermKind, child_ids: BoxSlice) -> Result { + let term = SynthTerm { kind, child_ids, - id: TermId::default(), - }); + }; self.interned.try_reserve(1)?; match self.interned.entry(term) { Entry::Occupied(entry) => Ok(*entry.get()), Entry::Vacant(entry) => { self.synth_terms.raw.try_reserve(1)?; - let idx = self.synth_terms.push_and_get_key(entry.key().clone()); + let idx = self.synth_terms.push_and_get_key(AnyTerm::Synth(entry.key().clone())); let idx = Self::dstidx_to_tidx(idx, self.start_idx); Ok(*entry.insert(idx)) } diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs index b43a0e7f..5be8ef0e 100644 --- a/smt-log-parser/src/parsers/z3/z3parser.rs +++ b/smt-log-parser/src/parsers/z3/z3parser.rs @@ -14,7 +14,7 @@ use super::{ inter_line::{InterLine, LineKind}, stack::Stack, stm2::EventLog, - synthetic::{SynthIdx, SynthTerm, SynthTerms}, + synthetic::{AnyTerm, SynthIdx, SynthTerms}, terms::Terms, }; @@ -892,7 +892,7 @@ impl std::ops::Index for Z3Parser { } } impl std::ops::Index for Z3Parser { - type Output = SynthTerm; + type Output = AnyTerm; fn index(&self, idx: SynthIdx) -> &Self::Output { self.synth_terms.index(&self.terms, idx) }