diff --git a/src/ic3/mic.rs b/src/ic3/mic.rs index 6d57419..f5a6822 100644 --- a/src/ic3/mic.rs +++ b/src/ic3/mic.rs @@ -1,7 +1,7 @@ use super::IC3; use crate::options::Options; -use logic_form::{Clause, Cube, Lemma, Lit, Var}; -use std::{collections::HashSet, mem::swap, time::Instant}; +use logic_form::{Clause, Cube, Lemma, Lit}; +use std::{collections::HashSet, time::Instant}; #[derive(Clone, Copy, Debug, Default)] pub struct DropVarParameter { @@ -29,7 +29,6 @@ impl DropVarParameter { pub enum MicType { NoMic, DropVar(DropVarParameter), - Xor(DropVarParameter), } impl MicType { @@ -269,225 +268,6 @@ impl IC3 { match mic_type { MicType::NoMic => cube, MicType::DropVar(parameter) => self.mic_by_drop_var(frame, cube, constrain, parameter), - MicType::Xor(mut parameter) => { - assert!(constrain.is_empty()); - let cube = self.mic_by_drop_var(frame, cube, constrain, parameter); - parameter = DropVarParameter::new(5, 3, 0); - self.xor_mic(frame, cube, parameter) - } - } - } - - // pub fn lazy_mic(&mut self, frame: usize, mut cube: Cube, level: usize) -> Cube { - // let start = Instant::now(); - // self.statistic.avg_mic_cube_len += cube.len(); - // self.statistic.num_mic += 1; - // let mut cex = Vec::new(); - // let keep = HashSet::new(); - // for similar in self.frame.similar(&cube, frame) { - // let mic = if level > 0 { - // self.ctg_down(frame, &similar, &keep, &cube, level) - // } else { - // self.down(frame, &similar, &keep, &cube, &[], &mut cex) - // }; - // if let Some(new_cube) = mic { - // cube = new_cube; - // break; - // } - // } - // self.activity.bump_cube_activity(&cube); - // self.statistic.block_mic_time += start.elapsed(); - // cube - // } - - pub fn xor_generalize(&mut self, frame: usize, mut lemma: Cube) { - let o = lemma.len(); - for xor_round in 0..=1 { - let mut i = 0; - while i < lemma.len() { - let mut j = i + 1; - while j < lemma.len() { - let mut a = lemma[i]; - let mut b = lemma[j]; - if a.var() > b.var() { - swap(&mut a, &mut b); - } - if !a.polarity() { - a = !a; - b = !b; - } - if xor_round == 0 && !self.xor_var.contains_key(&(a, b)) { - j += 1; - continue; - } - let mut try_gen = lemma.clone(); - let c = self.xor_var.get(&(a, b)); - if let Some(c) = c { - assert!(i < j); - try_gen[i] = *c; - try_gen.remove(j); - } else { - try_gen[i] = !try_gen[i]; - try_gen[j] = !try_gen[j]; - }; - if self.ts.cube_subsume_init(&try_gen) { - j += 1; - continue; - } - let res = self.solvers[frame - 1].inductive_with_constrain( - &try_gen, - true, - vec![!lemma.clone()], - ); - self.statistic.xor_gen.statistic(res); - if res { - let core = self.solvers[frame - 1].inductive_core(); - if c.is_some() { - // if core.len() < try_gen.len() { - // println!("{:?} {:?}", &try_gen[i], &try_gen[j]); - // println!("c {:?}", core); - // println!("t {:?}", try_gen); - // } - } - lemma = if c.is_some() { - try_gen - } else { - let xor_var = self.new_var(); - let xor_var_next = self.new_var(); - let c = xor_var.lit(); - self.xor_var.insert((a, b), c); - let trans = vec![ - Clause::from([!a, !b, c]), - Clause::from([a, b, c]), - Clause::from([!a, b, !c]), - Clause::from([a, !b, !c]), - ]; - let dep = vec![a.var(), b.var()]; - self.add_latch(xor_var, xor_var_next.lit(), None, trans, dep); - let mut new_lemma = lemma.clone(); - new_lemma[i] = c; - new_lemma.remove(j); - if core.len() < lemma.len() { - let mic = self.mic( - frame, - core, - &[], - MicType::DropVar(Default::default()), - ); - self.add_lemma(frame, mic, true, None); - } - new_lemma - }; - // assert!(self.solvers[frame - 1] - // .inductive(&lemma, true, false) - // .unwrap()); - continue; - } - j += 1; - } - i += 1; - } - } - if lemma.len() < o { - assert!(self.solvers[frame - 1].inductive(&lemma, true)); - self.add_lemma(frame, lemma.clone(), false, None); - } - } - - pub fn xor_mic(&mut self, frame: usize, mut cube: Cube, parameter: DropVarParameter) -> Cube { - // dbg!("begin xor mic"); - let mut cand_lits: HashSet = HashSet::new(); - let mut lemma_var_set: HashSet = HashSet::new(); - let mut lemma_lit_set: HashSet = HashSet::new(); - for l in cube.iter() { - lemma_var_set.insert(l.var()); - lemma_lit_set.insert(*l); } - for fm in &self.frame[frame..] { - for fl in fm.iter() { - if fl.iter().all(|l| lemma_var_set.contains(&l.var())) { - for l in fl.iter() { - if lemma_lit_set.contains(&!*l) { - cand_lits.insert(!*l); - } - } - } - } - } - for xor_round in 0..=1 { - let mut i = 0; - while i < cube.len() { - if !cand_lits.contains(&cube[i]) { - i += 1; - continue; - } - let mut j = i + 1; - while j < cube.len() { - if xor_round == 1 && !cand_lits.contains(&cube[j]) { - j += 1; - continue; - } - let mut a = cube[i]; - let mut b = cube[j]; - if a.var() > b.var() { - swap(&mut a, &mut b); - } - if !a.polarity() { - a = !a; - b = !b; - } - if xor_round == 0 && !self.xor_var.contains_key(&(a, b)) { - j += 1; - continue; - } - let mut try_gen = cube.clone(); - let c = self.xor_var.get(&(a, b)).cloned(); - if let Some(c) = c { - try_gen[i] = c; - try_gen.remove(j); - } else { - try_gen[i] = !try_gen[i]; - try_gen[j] = !try_gen[j]; - }; - if self.ts.cube_subsume_init(&try_gen) { - j += 1; - continue; - } - let res = self.trivial_block( - frame, - Lemma::new(try_gen.clone()), - &[!cube.clone()], - parameter, - ); - self.statistic.xor_gen.statistic(res); - if res { - cube = if c.is_some() { - try_gen - } else { - let xor_var = self.new_var(); - let xor_var_next = self.new_var(); - let c = xor_var.lit(); - self.xor_var.insert((a, b), c); - let trans = vec![ - Clause::from([!a, !b, c]), - Clause::from([a, b, c]), - Clause::from([!a, b, !c]), - Clause::from([a, !b, !c]), - ]; - let dep = vec![a.var(), b.var()]; - self.add_latch(xor_var, xor_var_next.lit(), None, trans, dep); - let mut new_lemma = cube.clone(); - new_lemma[i] = c; - new_lemma.remove(j); - new_lemma - }; - continue; - } - j += 1; - } - i += 1; - } - } - cube } } diff --git a/src/ic3/mod.rs b/src/ic3/mod.rs index 72c7a44..7b7ed82 100644 --- a/src/ic3/mod.rs +++ b/src/ic3/mod.rs @@ -8,11 +8,11 @@ use activity::Activity; use aig::{Aig, AigEdge}; use frame::{Frame, Frames}; use giputils::grc::Grc; -use logic_form::{Clause, Cube, Lemma, Lit, Var}; +use logic_form::{Clause, Cube, Lemma, Var}; use mic::{DropVarParameter, MicType}; use proofoblig::{ProofObligation, ProofObligationQueue}; use statistic::Statistic; -use std::{collections::HashMap, time::Instant}; +use std::time::Instant; mod activity; mod frame; @@ -36,7 +36,6 @@ pub struct IC3 { bmc_solver: Option<(Box, TransysUnroll)>, auxiliary_var: Vec, - xor_var: HashMap<(Lit, Lit), Lit>, } impl IC3 { @@ -343,7 +342,6 @@ impl IC3 { abs_cst, pre_lemmas, auxiliary_var: Vec::new(), - xor_var: HashMap::new(), bmc_solver: None, }; res.extend(); diff --git a/src/options.rs b/src/options.rs index 9212f71..80078ee 100644 --- a/src/options.rs +++ b/src/options.rs @@ -97,10 +97,6 @@ pub struct IC3Options { #[arg(long = "ic3-inn", default_value_t = false)] pub inn: bool, - /// ic3 with backward - #[arg(long = "ic3-bwd", default_value_t = false)] - pub bwd: bool, - /// ic3 with abstract constrains #[arg(long = "ic3-abs-cst", default_value_t = false)] pub abs_cst: bool,