Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960use serde::{Deserialize, Serialize};use std::{ collections::{HashMap, HashSet}, rc::Rc,};
#[derive(PartialEq, Eq, Hash, Serialize, Deserialize)]pub struct UserQuantifier { pub span: String,}
#[derive(PartialEq, Eq, Hash, Serialize, Deserialize)]pub enum QuantifierKind { Internal, User(UserQuantifier),}
#[derive(PartialEq, Eq, Hash, Serialize, Deserialize)]pub struct QuantifierX { pub qid: String, pub module: Option<String>, pub kind: QuantifierKind,}pub type Quantifier = Rc<QuantifierX>;
#[derive(PartialEq, Eq, Hash, Serialize, Deserialize)]pub struct InstantiationX { pub quantifier: Quantifier, pub id: (u64, usize),}pub type Instantiation = Rc<InstantiationX>;
#[derive(Serialize, Deserialize)]pub struct Graph<N: PartialEq + Eq + std::hash::Hash, E: PartialEq + Eq + std::hash::Hash>( pub HashMap<N, HashSet<(E, N)>>,);
#[derive(Serialize, Deserialize)]pub struct InstantiationGraph { pub bucket_name: String, pub module: String, pub function: Option<String>, pub quantifiers: HashSet<Quantifier>, pub instantiations: HashSet<Instantiation>, pub graph: Graph<Instantiation, ()>,}
impl InstantiationGraph { pub fn serialize(&self, mut w: impl std::io::Write) -> Result<(), String> { bincode_next::serde::encode_into_std_write(self, &mut w, bincode_next::config::legacy()) .map_err(|x| x.to_string()) .map(|_| ()) }
pub fn deserialize(mut r: impl std::io::Read) -> Result<Self, String> { bincode_next::serde::decode_from_std_read(&mut r, bincode_next::config::legacy()) .map_err(|x| x.to_string()) }}