Skip to content

Commit

Permalink
removed z3 from app dependencies
Browse files Browse the repository at this point in the history
  • Loading branch information
@alegnani
alegnani committed Jan 15, 2024
1 parent bfb6622 commit c5a6595
Show file tree
Hide file tree
Showing 5 changed files with 112 additions and 77 deletions.
1 change: 0 additions & 1 deletion verifactory_app/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,6 @@ egui_extras = { version = "0.25.0", features = ["all_loaders"]}
egui_file = "0.14.0"
tracing = "0.1.40"
tracing-subscriber = "0.3.18"
z3 = "0.12.1"
verifactory_lib = { path = "../verifactory_lib" }

[features]
Expand Down
48 changes: 19 additions & 29 deletions verifactory_app/src/gui/app.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,14 @@ use std::{
path::PathBuf,
};

use egui::{Align2, Direction, Event, Key};
use egui::{Align2, Direction, Event};
use egui_file::FileDialog;
use egui_toast::{Toast, ToastOptions, Toasts};
use z3::{Config, Context, SatResult};

use verifactory_lib::{
backends::{
belt_balancer_f, equal_drain_f, model_f, throughput_unlimited, universal_balancer,
ModelFlags, Printable,
belt_balancer_f, equal_drain_f, throughput_unlimited, universal_balancer,
BlueprintProofEntity, ModelFlags, ProofResult,
},
entities::{EntityId, FBEntity},
frontend::{Compiler, RelMap},
Expand Down Expand Up @@ -78,10 +77,10 @@ impl IOState {

#[derive(Default)]
pub struct ProofState {
balancer: Option<SatResult>,
equal_drain: Option<SatResult>,
throughput_unlimited: Option<SatResult>,
universal: Option<SatResult>,
balancer: Option<ProofResult>,
equal_drain: Option<ProofResult>,
throughput_unlimited: Option<ProofResult>,
universal: Option<ProofResult>,
}

pub type EntityGrid = Vec<Vec<Option<FBEntity<i32>>>>;
Expand Down Expand Up @@ -267,13 +266,12 @@ impl eframe::App for MyApp {
ui.horizontal(|ui| {
if ui.button("Prove").clicked() {
let graph = self.generate_graph(false);
let cfg = Config::new();
let ctx = Context::new(&cfg);
let res = model_f(&graph, &ctx, belt_balancer_f, ModelFlags::empty());
let mut proof = BlueprintProofEntity::new(graph);
let res = proof.model(belt_balancer_f, ModelFlags::empty());
self.proof_state.balancer = Some(res);
}
if let Some(proof_res) = self.proof_state.balancer {
ui.label(format!("Proof result: {}", proof_res.to_str()));
ui.label(format!("Proof result: {}", proof_res));
}
});

Expand All @@ -283,13 +281,12 @@ impl eframe::App for MyApp {
ui.horizontal(|ui| {
if ui.button("Prove").clicked() {
let graph = self.generate_graph(true);
let cfg = Config::new();
let ctx = Context::new(&cfg);
let res = model_f(&graph, &ctx, equal_drain_f, ModelFlags::empty());
let mut proof = BlueprintProofEntity::new(graph);
let res = proof.model(equal_drain_f, ModelFlags::empty());
self.proof_state.equal_drain = Some(res);
}
if let Some(proof_res) = self.proof_state.equal_drain {
ui.label(format!("Proof result: {}", proof_res.to_str()));
ui.label(format!("Proof result: {}", proof_res));
}
});

Expand All @@ -301,19 +298,13 @@ impl eframe::App for MyApp {
ui.horizontal(|ui| {
if ui.button("Prove").clicked() {
let graph = self.generate_graph(false);
let cfg = Config::new();
let ctx = Context::new(&cfg);
let mut proof = BlueprintProofEntity::new(graph);
let entities = self.grid.iter().flatten().flatten().cloned().collect();
let res = model_f(
&graph,
&ctx,
throughput_unlimited(entities),
ModelFlags::Relaxed,
);
let res = proof.model(throughput_unlimited(entities), ModelFlags::Relaxed);
self.proof_state.throughput_unlimited = Some(res);
}
if let Some(proof_res) = self.proof_state.throughput_unlimited {
ui.label(format!("Proof result: {}", proof_res.to_str()));
ui.label(format!("Proof result: {}", proof_res));
}
});
ui.label("\n");
Expand All @@ -322,13 +313,12 @@ impl eframe::App for MyApp {
ui.horizontal(|ui| {
if ui.button("Prove").clicked() {
let graph = self.generate_graph(false);
let cfg = Config::new();
let ctx = Context::new(&cfg);
let res = model_f(&graph, &ctx, universal_balancer, ModelFlags::Blocked);
let mut proof = BlueprintProofEntity::new(graph);
let res = proof.model(universal_balancer, ModelFlags::Blocked);
self.proof_state.universal = Some(res);
}
if let Some(proof_res) = self.proof_state.universal {
ui.label(format!("Proof result: {}", proof_res.to_str()));
ui.label(format!("Proof result: {}", proof_res));
}
});

Expand Down
2 changes: 1 addition & 1 deletion verifactory_lib/src/backends/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ mod model_entities;
mod model_graph;
mod proofs;

pub use self::proofs::{Printable, Z3Proofs};
pub use self::proofs::{BlueprintProofEntity, ProofResult};

pub use model_graph::{
belt_balancer_f, equal_drain_f, model_f, throughput_unlimited, universal_balancer, ModelFlags,
Expand Down
56 changes: 30 additions & 26 deletions verifactory_lib/src/backends/model_graph.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,12 @@ use petgraph::prelude::{EdgeIndex, NodeIndex};
use std::{collections::HashMap, mem};
use z3::{
ast::{exists_const, forall_const, Ast, Bool, Int, Real},
Context, SatResult, Solver,
Context, Solver,
};

use crate::{entities::FBEntity, ir::FlowGraph};

use super::proofs::Negatable;
use super::proofs::ProofResult;

use super::model_entities::{Z3Edge, Z3Node};

Expand Down Expand Up @@ -59,7 +59,12 @@ bitflags! {
}
}

pub fn model_f<'a, F>(graph: &'a FlowGraph, ctx: &'a Context, f: F, flags: ModelFlags) -> SatResult
pub fn model_f<'a, F>(
graph: &'a FlowGraph,
ctx: &'a Context,
f: F,
flags: ModelFlags,
) -> ProofResult
where
F: FnOnce(ProofPrimitives<'a>) -> Bool<'a>,
{
Expand Down Expand Up @@ -109,7 +114,7 @@ where
};

solver.assert(&f(primitives.clone()));
let res = solver.check().not();
let res: ProofResult = solver.check().into();
// TODO: move to tracing
// println!("Solver:\n{:?}", solver);
// println!("Model:\n{:?}", solver.get_model());
Expand All @@ -119,7 +124,7 @@ where
println!("{:?}: {:?}", &input, a);
}
}
res
res.not()
}

/// Conjunction of a slice of `Bool`s.
Expand Down Expand Up @@ -333,7 +338,6 @@ mod tests {
use z3::Config;

use super::*;
use crate::backends::Printable;
use crate::ir::CoalesceStrength;
use crate::{frontend::Compiler, import::file_to_entities, ir::FlowGraphFun};

Expand All @@ -346,8 +350,8 @@ mod tests {
let cfg = Config::new();
let ctx = Context::new(&cfg);
let res = model_f(&graph, &ctx, belt_balancer_f, ModelFlags::empty());
println!("Result: {}", res.to_str());
assert!(matches!(res, SatResult::Unsat));
println!("Result: {}", res);
assert!(matches!(res, ProofResult::Unsat));
}

#[test]
Expand All @@ -358,8 +362,8 @@ mod tests {
let cfg = Config::new();
let ctx = Context::new(&cfg);
let res = model_f(&graph, &ctx, belt_balancer_f, ModelFlags::empty());
println!("Result: {}", res.to_str());
assert!(matches!(res, SatResult::Sat));
println!("Result: {}", res);
assert!(matches!(res, ProofResult::Sat));
}

#[test]
Expand All @@ -375,8 +379,8 @@ mod tests {
throughput_unlimited(entities),
ModelFlags::Relaxed,
);
println!("Result: {}", res.to_str());
assert!(matches!(res, SatResult::Sat));
println!("Result: {}", res);
assert!(matches!(res, ProofResult::Sat));
}

#[test]
Expand All @@ -392,8 +396,8 @@ mod tests {
throughput_unlimited(entities),
ModelFlags::Relaxed,
);
println!("Result: {}", res.to_str());
assert!(matches!(res, SatResult::Unsat));
println!("Result: {}", res);
assert!(matches!(res, ProofResult::Unsat));
}

#[test]
Expand All @@ -409,8 +413,8 @@ mod tests {
throughput_unlimited(entities),
ModelFlags::Relaxed,
);
println!("Result: {}", res.to_str());
assert!(matches!(res, SatResult::Sat));
println!("Result: {}", res);
assert!(matches!(res, ProofResult::Sat));
}

#[test]
Expand All @@ -426,8 +430,8 @@ mod tests {
throughput_unlimited(entities),
ModelFlags::Relaxed,
);
println!("Result: {}", res.to_str());
assert!(matches!(res, SatResult::Unsat));
println!("Result: {}", res);
assert!(matches!(res, ProofResult::Unsat));
}

#[test]
Expand All @@ -441,8 +445,8 @@ mod tests {
let cfg = Config::new();
let ctx = Context::new(&cfg);
let res = model_f(&graph, &ctx, universal_balancer, ModelFlags::Blocked);
println!("Result: {}", res.to_str());
assert!(matches!(res, SatResult::Sat));
println!("Result: {}", res);
assert!(matches!(res, ProofResult::Sat));
}

#[test]
Expand All @@ -453,8 +457,8 @@ mod tests {
let cfg = Config::new();
let ctx = Context::new(&cfg);
let res = model_f(&graph, &ctx, universal_balancer, ModelFlags::Blocked);
println!("Result: {}", res.to_str());
assert!(matches!(res, SatResult::Unsat));
println!("Result: {}", res);
assert!(matches!(res, ProofResult::Unsat));
}

#[test]
Expand All @@ -465,7 +469,7 @@ mod tests {
let cfg = Config::new();
let ctx = Context::new(&cfg);
let res = model_f(&graph, &ctx, belt_balancer_f, ModelFlags::empty());
assert!(matches!(res, SatResult::Sat));
assert!(matches!(res, ProofResult::Sat));
}

#[test]
Expand All @@ -476,7 +480,7 @@ mod tests {
let cfg = Config::new();
let ctx = Context::new(&cfg);
let res = model_f(&graph, &ctx, equal_drain_f, ModelFlags::empty());
assert!(matches!(res, SatResult::Sat));
assert!(matches!(res, ProofResult::Sat));
}

#[test]
Expand All @@ -492,7 +496,7 @@ mod tests {
throughput_unlimited(entities),
ModelFlags::Relaxed,
);
assert!(matches!(res, SatResult::Sat));
assert!(matches!(res, ProofResult::Sat));
}

#[test]
Expand All @@ -503,6 +507,6 @@ mod tests {
let cfg = Config::new();
let ctx = Context::new(&cfg);
let res = model_f(&graph, &ctx, equal_drain_f, ModelFlags::Blocked);
assert!(matches!(res, SatResult::Sat));
assert!(matches!(res, ProofResult::Sat));
}
}
Loading

0 comments on commit c5a6595

Please sign in to comment.