Merge pull request #13 from alegnani/release-v0.4.0

Release v0.4.0

.github/workflows/publish.yml

@@ -16,10 +16,10 @@ jobs:
       matrix:
         include:
           - os: ubuntu-latest
-            artifact_name: verifactory
+            artifact_name: verifactory_app
             asset_name: VeriFactory-linux
           - os: windows-latest
-            artifact_name: verifactory.exe
+            artifact_name: verifactory_app.exe
             asset_name: VeriFactory-win.exe
 
     steps:
@@ -35,7 +35,7 @@ jobs:
           target/
         key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
     - name: Build
-      run: cargo build --release --features build_z3 --verbose
+      run: cargo build -p verifactory_app --release --features build_z3 --verbose
     - name: Upload binaries to release
       uses: svenstaro/upload-release-action@v2
       with:

.gitignore

@@ -13,12 +13,6 @@ Cargo.lock
 # MSVC Windows builds of rustc generate these, which store debugging information
 *.pdb
 
-# Remove generated graph svgs
-*.svg
-!img/*.svg
-
-imgs/rotate.sh
-
 *.log
 
 # Ignore direnv files

Cargo.toml

@@ -1,31 +1,7 @@
-[package]
-name = "verifactory"
-version = "0.1.0"
-edition = "2021"
+[workspace]
+resolver = "2"
+members = [ "verifactory_app","verifactory_lib"]
 
-# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
-
-[dependencies]
-anyhow = "<=1.0.171"
-base64 = "0.21.2"
-bitflags = "2.4.1"
-eframe = "0.24.1"
-egui = "0.24.1"
-egui-toast = "0.10.1"
-egui_extras = { version = "0.24.2", features = ["all_loaders"]}
-egui_file = "0.13.0"
-fraction = "0.13.1"
-graphviz-rust = "0.6.6"
-inflate = "0.4.5"
-num-bigint = "0.4.4"
-petgraph = "0.6.4"
-relations = "0.3.0"
-serde = { version = "1.0.164", features = ["derive"] }
-serde_json = "1.0.99"
-serde_repr = "0.1.12"
-tracing = "0.1.37"
-tracing-subscriber = "0.3.17"
-z3 = "0.12.1"
-
-[features]
-build_z3 = ["z3/static-link-z3"]
+[profile.release]
+lto = true
+strip = true

verifactory_app/Cargo.toml

@@ -0,0 +1,20 @@
+[package]
+name = "verifactory_app"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+anyhow = "1.0.79"
+eframe = "0.25.0"
+egui = "0.25.0"
+egui-toast = "0.10.2"
+egui_extras = { version = "0.25.0", features = ["all_loaders"]}
+egui_file = "0.14.0"
+tracing = "0.1.40"
+tracing-subscriber = "0.3.18"
+verifactory_lib = { path = "../verifactory_lib" }
+
+[features]
+build_z3 = ["verifactory_lib/build_z3"]

src/gui/app.rs → verifactory_app/src/gui/app.rs

@@ -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 crate::{
+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},
@@ -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>>>>;
@@ -144,12 +143,11 @@ impl MyApp {
         println!("Remove list: {:?}", removed);
 
         graph.simplify(&removed, CoalesceStrength::Aggressive);
-        let graph = if reversed {
+        if reversed {
             Reversable::reverse(&graph)
         } else {
             graph
-        };
-        graph
+        }
     }
 
     pub fn load_file(&mut self, file: PathBuf) -> anyhow::Result<()> {
@@ -268,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));
                 }
             });
 
@@ -284,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));
                 }
             });
 
@@ -302,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");
@@ -323,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));
                 }
             });
 

src/gui/grid.rs → verifactory_app/src/gui/grid.rs

@@ -2,7 +2,7 @@ use std::f32::consts::PI;
 
 use egui::{Color32, Image, Pos2, Rect, Sense, Vec2};
 
-use crate::{
+use verifactory_lib::{
     entities::{BeltType, FBBelt, FBEntity, FBSplitter, Priority},
     frontend::RelMap,
     utils::{Direction, Position, Rotation},
@@ -151,10 +151,7 @@ impl MyApp {
         /* if the entity is a splitter force the arrow to be drawn in the middle */
         if let FBEntity::Splitter(s) = entity {
             let size = self.grid_settings.size as f32;
-            let rot = s
-                .base
-                .direction
-                .rotate(crate::utils::Rotation::Clockwise, 1);
+            let rot = s.base.direction.rotate(Rotation::Clockwise, 1);
             rect = rect
                 .shrink_dir(rot, size / 2.)
                 .shrink_dir(rot.flip(), size / 2.);

src/main.rs → verifactory_app/src/main.rs

@@ -1,13 +1,4 @@
-#![doc = include_str!("../README.md")]
-
-mod backends;
-mod entities;
-mod frontend;
 mod gui;
-mod import;
-mod ir;
-mod utils;
-
 use std::{fs::File, sync::Arc};
 
 use eframe::NativeOptions;

verifactory_lib/Cargo.toml

@@ -0,0 +1,26 @@
+[package]
+name = "verifactory_lib"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+anyhow = "1.0.79"
+base64 = "0.21.6"
+bitflags = "2.4.1"
+fraction = "0.15.0"
+graphviz-rust = "0.7.0"
+inflate = "0.4.5"
+num-bigint = "0.4.4"
+petgraph = "0.6.4"
+relations = "0.3.0"
+serde = { version = "1.0.195", features = ["derive"] }
+serde_json = "1.0.111"
+serde_repr = "0.1.18"
+tracing = "0.1.40"
+tracing-subscriber = "0.3.18"
+z3 = "0.12.1"
+
+[features]
+build_z3 = ["z3/static-link-z3"]

src/backends/mod.rs → verifactory_lib/src/backends/mod.rs

@@ -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,