Skip to content

Commit

Permalink
update
Browse files Browse the repository at this point in the history
  • Loading branch information
@gipsyh
gipsyh committed Jan 6, 2025
1 parent 62cb0ba commit b460c43
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 230 deletions.
224 changes: 2 additions & 222 deletions src/ic3/mic.rs
View file
Original file line number Diff line number Diff line change
@@ -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 {
Expand Down Expand Up @@ -29,7 +29,6 @@ impl DropVarParameter {
pub enum MicType {
NoMic,
DropVar(DropVarParameter),
Xor(DropVarParameter),
}

impl MicType {
Expand Down Expand Up @@ -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<Lit> = HashSet::new();
let mut lemma_var_set: HashSet<Var> = HashSet::new();
let mut lemma_lit_set: HashSet<Lit> = 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
}
}
6 changes: 2 additions & 4 deletions src/ic3/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -36,7 +36,6 @@ pub struct IC3 {
bmc_solver: Option<(Box<dyn satif::Satif>, TransysUnroll)>,

auxiliary_var: Vec<Var>,
xor_var: HashMap<(Lit, Lit), Lit>,
}

impl IC3 {
Expand Down Expand Up @@ -343,7 +342,6 @@ impl IC3 {
abs_cst,
pre_lemmas,
auxiliary_var: Vec::new(),
xor_var: HashMap::new(),
bmc_solver: None,
};
res.extend();
Expand Down
4 changes: 0 additions & 4 deletions src/options.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down

0 comments on commit b460c43

Please sign in to comment.