v1.3.3

gipsyh · Jan 12, 2025 · 853f217 · 853f217
1 parent 39041b0
commit 853f217
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 11 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "rIC3"
-version = "1.3.2"
+version = "1.3.3"
 edition = "2021"
 authors = ["Yuheng Su <[email protected]>"]
 repository = "https://github.com/gipsyh/rIC3"
@@ -12,7 +12,7 @@ rust-version = "1.85"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-aig = { path = "./deps/aig-rs", version = "0.2.4" }
+aig = { path = "./deps/aig-rs", version = "0.2.6" }
 satif-minisat = { path = "./deps/minisat-rs", version = "0.2" }
 satif-cadical = { path = "./deps/cadical-rs", version = "0.1" }
 satif-kissat = { path = "./deps/kissat-rs", version = "0.4" }

diff --git a/README.md b/README.md
@@ -20,19 +20,20 @@ To view the submission for HWMCC'24, please checkout the `HWMCC24` branch or dow
 ### Install From Crates.io
 ```cargo install rIC3```
 
-```rIC3 <aig model>```
-
-
 ### Install From Source
 Currently, some dependency libraries are linked through pre-compiled static files in the repository, and they have a dependency on the glibc version. Ubuntu 20.04 or later works fine.
 
 - Install the Rust compiler https://www.rust-lang.org/
-- Switch to nightly ````rustup default nightly````
-- ````git clone --recurse-submodules https://github.com/gipsyh/rIC3````
-- ```cd rIC3```
-- Build and Run ````cargo r --release -- <aig model>````
+- Switch to nightly ```rustup default nightly```
+- ```git clone --recurse-submodules https://github.com/gipsyh/rIC3```
+- Build ```cd rIC3 && cargo b --release```
+- Run ```cargo r --release -- <AIGER FILE>```
 - Install ```cargo install --path .```
 
+### Run
+- 16-threads Portfolio ```rIC3 <AIGER FILE>```
+- single-thread IC3 ```rIC3 -e ic3 <AIGER FILE>```
+
 Copyright (C) 2023 - Present, Yuheng Su ([email protected]). All rights reserved.
 
 Without obtaining authorization, rIC3 is not allowed to be used for any commercial purposes.
diff --git a/deps/aig-rs b/deps/aig-rs
diff --git a/src/transys/mod.rs b/src/transys/mod.rs
@@ -60,7 +60,7 @@ impl Transys {
                 new_var().lit().not_if(!l.next.to_lit().polarity())
             })
             .collect();
-        let init = aig.latch_init_cube().to_cube();
+        let init = aig.latch_init_cube();
         let mut init_map = VarMap::new();
         init_map.reserve(max_latch);
         for l in init.iter() {
+1 −1		Cargo.toml
+0 −17		src/aiger.rs
+1 −17		src/lib.rs
+0 −237		src/logic_form.rs
+5 −4		src/others.rs
+0 −11		src/simplify.rs