Snapshot

Author: wsx-ucb

Diff for: src/main.rs

@@ -14,7 +14,7 @@ use env_logger::{Builder, Env, Target};
 use itertools::Itertools;
 use walkdir::WalkDir;
 
-use crate::pipeline::{unify, Input};
+use crate::pipeline::{unify, Input, Stats};
 
 mod pipeline;
 
@@ -32,8 +32,8 @@ fn visit<P: AsRef<Path>>(dir: P, mut cb: impl FnMut(usize, &Path)) -> io::Result
 
 #[derive(Debug)]
 enum CosetteResult {
-	Provable,
-	NotProvable,
+	Provable(Stats),
+	NotProvable(Stats),
 	ParseErr(serde_json::Error),
 	Panic(Box<dyn Any + Send>),
 }
@@ -51,21 +51,21 @@ fn main() -> io::Result<()> {
 			let mut buf_reader = BufReader::new(file);
 			let mut contents = String::new();
 			println!("#{}: {}", i, path.to_string_lossy().as_ref());
-			let old_time = Instant::now();
+			let start_time = Instant::now();
 			buf_reader.read_to_string(&mut contents).unwrap();
 			let result =
 				std::panic::catch_unwind(|| match serde_json::from_str::<Input>(&contents) {
 					Ok(rel) => {
-						let provable = unify(rel);
+						let (provable, case_stats) = unify(rel);
 						println!(
 							"Equivalence is {}provable for {}",
 							if provable { "" } else { "not " },
 							path.file_name().unwrap().to_str().unwrap(),
 						);
 						if provable {
-							Provable
+							Provable(case_stats)
 						} else {
-							NotProvable
+							NotProvable(case_stats)
 						}
 					},
 					Err(e) => {
@@ -80,20 +80,27 @@ fn main() -> io::Result<()> {
 					Panic(e)
 				},
 			};
-			let duration = Instant::now() - old_time;
-			let mut result_file = File::create(path.with_extension("res")).unwrap();
-			write!(
-				result_file,
-				"{}\n{}",
-				matches!(result, CosetteResult::Provable),
-				duration.as_secs_f32()
-			)
-			.unwrap();
+			let result_file = File::create(path.with_extension("result")).unwrap();
+			let case_stats = match &result {
+				Provable(stats) | NotProvable(stats) => {
+					let mut stats = stats.clone();
+					stats.provable = matches!(result, Provable(_));
+					stats.total_duration = start_time.elapsed();
+					stats
+				},
+				_ => {
+					let mut stats = Stats::default();
+					stats.panicked = true;
+					stats.total_duration = start_time.elapsed();
+					stats
+				},
+			};
+			serde_json::to_writer(result_file, &case_stats).unwrap();
 			stats.insert(path.to_string_lossy().to_string(), result);
 		})?;
 	}
 	println!("\n\nSTATISTICS");
-	let (a, b): (Vec<_>, _) = stats.values().partition(|v| matches!(v, CosetteResult::Provable));
+	let (a, b): (Vec<_>, _) = stats.values().partition(|v| matches!(v, CosetteResult::Provable(_)));
 	let (al, bl) = (a.len(), b.len());
 	for (name, result) in stats {
 		println!("{}\t{:?}", name, result);

Diff for: src/pipeline.rs

@@ -1,6 +1,5 @@
-use std::cell::RefCell;
-use std::collections::HashMap;
 use std::rc::Rc;
+use std::time::{Duration, Instant};
 
 use imbl::vector;
 use serde::{Deserialize, Serialize};
@@ -24,60 +23,84 @@ pub mod unify;
 #[derive(Serialize, Deserialize)]
 pub struct Input {
 	schemas: Vec<Schema>,
-	queries: (relation::Relation, relation::Relation),
+	pub queries: (relation::Relation, relation::Relation),
 	#[serde(default)]
 	help: (String, String),
 }
 
-pub fn unify(Input { schemas, queries: (rel1, rel2), help }: Input) -> bool {
+#[derive(Clone, Debug, Default, Serialize, Deserialize)]
+pub struct Stats {
+	pub provable: bool,
+	pub panicked: bool,
+	pub complete_fragment: bool,
+	pub equiv_class_duration: Duration,
+	pub equiv_class_timed_out: bool,
+	pub smt_duration: Duration,
+	pub smt_timed_out: bool,
+	pub nontrivial_perms: bool,
+	pub translate_duration: Duration,
+	pub normal_duration: Duration,
+	pub stable_duration: Duration,
+	pub unify_duration: Duration,
+	pub total_duration: Duration,
+}
+
+pub fn unify(Input { schemas, queries: (rel1, rel2), help }: Input) -> (bool, Stats) {
+	let mut stats = Stats::default();
 	let subst = vector![];
 	let env = relation::Env(&schemas, &subst, 0);
 	log::info!("Schemas:\n{:?}", schemas);
 	log::info!("Input:\n{}\n{}", help.0, help.1);
+	stats.complete_fragment = rel1.complete() && rel2.complete();
 	if rel1 == rel2 {
 		println!("Trivially true!");
-		return true;
+		return (true, stats);
 	}
+	let syn_start = Instant::now();
 	let rel1 = env.eval(rel1);
 	let rel2 = env.eval(rel2);
-	if rel1 == rel2 {
-		return true;
-	}
+	stats.translate_duration = syn_start.elapsed();
 	log::info!("Syntax left:\n{}", rel1);
 	log::info!("Syntax right:\n{}", rel2);
+	if rel1 == rel2 {
+		return (true, stats);
+	}
 	let nom_env = &vector![];
 	let eval_nom = |rel: syntax::Relation| -> normal::Relation {
 		let rel = (&partial::Env::default()).eval(rel);
 		nom_env.eval(rel)
 	};
+	let norm_start = Instant::now();
 	let rel1 = eval_nom(rel1);
 	let rel2 = eval_nom(rel2);
+	stats.normal_duration = norm_start.elapsed();
 	log::info!("Normal left:\n{}", rel1);
 	log::info!("Normal right:\n{}", rel2);
 	if rel1 == rel2 {
-		return true;
+		return (true, stats);
 	}
 	let config = Config::new();
 	let z3_ctx = &Context::new(&config);
-	let ctx = Rc::new(Ctx::new(Solver::new(z3_ctx)));
-	let h_ops = Rc::new(RefCell::new(HashMap::new()));
-	let agg_ops = Rc::new(RefCell::new(HashMap::new()));
-	let rel_h_ops = Rc::new(RefCell::new(HashMap::new()));
+	let ctx = Rc::new(Ctx::new_with_stats(Solver::new(z3_ctx), stats));
+	let z3_env = Z3Env::empty(ctx.clone());
 	let eval_stb = |nom: normal::Relation| -> normal::Relation {
-		let env = &stable::Env(vector![], {
-			let subst = vector![];
-			Z3Env(ctx.clone(), subst, h_ops.clone(), agg_ops.clone(), rel_h_ops.clone())
-		});
+		let env = &stable::Env(vector![], z3_env.clone());
 		let stb = env.eval(nom);
 		nom_env.eval(stb)
 	};
+	let stb_start = Instant::now();
 	let rel1 = eval_stb(rel1);
 	let rel2 = eval_stb(rel2);
+	ctx.stats.borrow_mut().stable_duration = stb_start.elapsed();
 	log::info!("Stable left:\n{}", rel1);
 	log::info!("Stable right:\n{}", rel2);
 	if rel1 == rel2 {
-		return true;
+		return (true, ctx.stats.borrow().clone());
 	}
-	let env = UnifyEnv(ctx, vector![], vector![]);
-	env.unify(&rel1, &rel2)
+	let env = UnifyEnv(ctx.clone(), vector![], vector![]);
+	let unify_start = Instant::now();
+	let res = env.unify(&rel1, &rel2);
+	ctx.stats.borrow_mut().unify_duration = unify_start.elapsed();
+	let stats = ctx.stats.borrow().clone();
+	(res, stats)
 }