Skip to content

Commit

Permalink
update
Browse files Browse the repository at this point in the history
  • Loading branch information
@gipsyh
gipsyh committed Dec 20, 2024
1 parent 3e208f0 commit 8310cd1
Show file tree
Hide file tree
Showing 6 changed files with 47 additions and 96 deletions.
22 changes: 9 additions & 13 deletions src/gipsat/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -265,19 +265,18 @@ impl Solver {
assump: &[Lit],
constrain: Vec<Clause>,
bucket: bool,
limit: bool,
) -> Option<bool> {
) -> bool {
if self.trivial_unsat {
self.unsat_core.clear();
return Some(false);
return false;
}
assert!(!assump.is_empty());
self.statistic.num_solve += 1;
let mut assumption;
if self.propagate() != CREF_NONE {
self.trivial_unsat = true;
self.unsat_core.clear();
return Some(false);
return false;
}
let assump = if !constrain.is_empty() {
assumption = Cube::new();
Expand All @@ -295,7 +294,7 @@ impl Solver {
bucket,
) {
self.unsat_core.clear();
return Some(false);
return false;
};
&assumption
} else {
Expand All @@ -304,30 +303,27 @@ impl Solver {
};
self.clean_leanrt(true);
self.simplify();
self.search_with_restart(assump, limit)
self.search_with_restart(assump)
}

pub fn inductive_with_constrain(
&mut self,
cube: &[Lit],
strengthen: bool,
mut constrain: Vec<Clause>,
limit: bool,
) -> Option<bool> {
) -> bool {
let assump = self.ts.cube_next(cube);
if strengthen {
constrain.push(Clause::from_iter(cube.iter().map(|l| !*l)));
}
let res = self
.solve_with_domain(&assump, constrain.clone(), true, limit)
.map(|l| !l);
let res = !self.solve_with_domain(&assump, constrain.clone(), true);
self.assump = assump;
self.constrain = constrain;
res
}

pub fn inductive(&mut self, cube: &[Lit], strengthen: bool, limit: bool) -> Option<bool> {
self.inductive_with_constrain(cube, strengthen, vec![], limit)
pub fn inductive(&mut self, cube: &[Lit], strengthen: bool) -> bool {
self.inductive_with_constrain(cube, strengthen, vec![])
}

pub fn inductive_core(&mut self) -> Cube {
Expand Down
5 changes: 1 addition & 4 deletions src/gipsat/pred.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,7 @@ impl Solver {
target_constrain: &Clause,
) -> Option<Cube> {
let assump = Cube::from_iter(inputs.iter().chain(latchs.iter()).copied());
if self
.solve_with_domain(&assump, vec![target_constrain.clone()], true, false)
.unwrap()
{
if self.solve_with_domain(&assump, vec![target_constrain.clone()], true) {
return None;
}
Some(
Expand Down
7 changes: 2 additions & 5 deletions src/gipsat/search.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,12 +77,9 @@ impl Solver {
self.pos_in_trail.truncate(level);
}

pub fn search_with_restart(&mut self, assumption: &[Lit], limit: bool) -> Option<bool> {
pub fn search_with_restart(&mut self, assumption: &[Lit]) -> bool {
let mut restarts = 0;
loop {
if limit && restarts > 20 {
return None;
}
if restarts > 10 && self.vsids.enable_bucket {
self.vsids.enable_bucket = false;
self.vsids.heap.clear();
Expand All @@ -97,7 +94,7 @@ impl Solver {
None => {
restarts += 1;
}
r => return r,
Some(r) => return r,
}
}
}
Expand Down
41 changes: 13 additions & 28 deletions src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ impl IC3 {
fn push_lemma(&mut self, frame: usize, mut cube: Cube) -> (usize, Cube) {
let start = Instant::now();
for i in frame + 1..=self.level() {
if let Some(true) = self.solvers[i - 1].inductive(&cube, true, false) {
if self.solvers[i - 1].inductive(&cube, true) {
cube = self.solvers[i - 1].inductive_core();
} else {
return (i, cube);
Expand Down Expand Up @@ -160,9 +160,7 @@ impl IC3 {
return Some(false);
}
} else if self.options.ic3.inn && po.frame > 0 {
assert!(!self.solvers[0]
.solve_with_domain(&po.lemma, vec![], true, false)
.unwrap());
assert!(!self.solvers[0].solve_with_domain(&po.lemma, vec![], true));
} else {
self.add_obligation(po.clone());
assert!(po.frame == 0);
Expand All @@ -179,9 +177,7 @@ impl IC3 {
}
po.bump_act();
let blocked_start = Instant::now();
let blocked = self
.blocked_with_ordered(po.frame, &po.lemma, false, false, false)
.unwrap();
let blocked = self.blocked_with_ordered(po.frame, &po.lemma, false, false);
self.statistic.block_blocked_time += blocked_start.elapsed();
if blocked {
let mic_type = if self.options.ic3.dynamic {
Expand Down Expand Up @@ -256,17 +252,13 @@ impl IC3 {
}
*limit -= 1;
loop {
if self
.blocked_with_ordered_with_constrain(
frame,
&lemma,
false,
true,
constrain.to_vec(),
false,
)
.unwrap()
{
if self.blocked_with_ordered_with_constrain(
frame,
&lemma,
false,
true,
constrain.to_vec(),
) {
let mut mic = self.solvers[frame - 1].inductive_core();
mic = self.mic(frame, mic, constrain, MicType::DropVar(parameter));
let (frame, mic) = self.push_lemma(frame, mic);
Expand Down Expand Up @@ -305,10 +297,7 @@ impl IC3 {
continue;
}
for ctp in 0..3 {
if self
.blocked_with_ordered(frame_idx + 1, &lemma, false, false, false)
.unwrap()
{
if self.blocked_with_ordered(frame_idx + 1, &lemma, false, false) {
let core = if self.options.ic3.inn && self.ts.cube_subsume_init(&lemma) {
lemma.cube().clone()
} else {
Expand All @@ -329,9 +318,7 @@ impl IC3 {
}
let (ctp, _) = self.get_pred(frame_idx + 1, false);
if !self.ts.cube_subsume_init(&ctp)
&& self.solvers[frame_idx - 1]
.inductive(&ctp, true, false)
.unwrap()
&& self.solvers[frame_idx - 1].inductive(&ctp, true)
{
let core = self.solvers[frame_idx - 1].inductive_core();
let mic =
Expand Down Expand Up @@ -493,9 +480,7 @@ impl Engine for IC3 {
self.ts.bad.clone()
};
assump.extend_from_slice(&b.input);
assert!(self.solvers[0]
.solve_with_domain(&assump, vec![], false, false)
.unwrap());
assert!(self.solvers[0].solve_with_domain(&assump, vec![], false));
for l in self.ts.latchs.iter() {
let l = l.lit();
if let Some(v) = self.solvers[0].sat_value(l) {
Expand Down
35 changes: 14 additions & 21 deletions src/mic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,17 +71,13 @@ impl IC3 {
return None;
}
self.statistic.num_down_sat += 1;
if self
.blocked_with_ordered_with_constrain(
frame,
&cube,
false,
true,
constrain.to_vec(),
false,
)
.unwrap()
{
if self.blocked_with_ordered_with_constrain(
frame,
&cube,
false,
true,
constrain.to_vec(),
) {
return Some(self.solvers[frame - 1].inductive_core());
}
let mut ret = false;
Expand Down Expand Up @@ -137,10 +133,7 @@ impl IC3 {
return None;
}
self.statistic.num_down_sat += 1;
if self
.blocked_with_ordered(frame, &cube, false, true, false)
.unwrap()
{
if self.blocked_with_ordered(frame, &cube, false, true) {
return Some(self.solvers[frame - 1].inductive_core());
}
// for lit in cube.iter() {
Expand Down Expand Up @@ -341,9 +334,11 @@ impl IC3 {
j += 1;
continue;
}
let res = self.solvers[frame - 1]
.inductive_with_constrain(&try_gen, true, vec![!lemma.clone()], false)
.unwrap();
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();
Expand Down Expand Up @@ -394,9 +389,7 @@ impl IC3 {
}
}
if lemma.len() < o {
assert!(self.solvers[frame - 1]
.inductive(&lemma, true, false)
.unwrap());
assert!(self.solvers[frame - 1].inductive(&lemma, true));
self.add_lemma(frame, lemma.clone(), false, None);
}
}
Expand Down
33 changes: 8 additions & 25 deletions src/solver.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,7 @@ impl IC3 {
let solver = self.solvers.last_mut().unwrap();
solver.assump = self.ts.bad.clone();
solver.constrain = Default::default();
let res = solver
.solve_with_domain(&self.ts.bad, vec![], false, false)
.unwrap();
let res = solver.solve_with_domain(&self.ts.bad, vec![], false);
self.statistic.block_get_bad_time += start.elapsed();
if res {
let frame = self.solvers.len();
Expand All @@ -26,9 +24,7 @@ impl IC3 {
impl IC3 {
#[inline]
pub fn sat_contained(&mut self, frame: usize, lemma: &Lemma) -> bool {
!self.solvers[frame]
.solve_with_domain(lemma, vec![], true, false)
.unwrap()
!self.solvers[frame].solve_with_domain(lemma, vec![], true)
}

pub fn blocked_with_ordered(
Expand All @@ -37,11 +33,10 @@ impl IC3 {
cube: &Cube,
ascending: bool,
strengthen: bool,
limit: bool,
) -> Option<bool> {
) -> bool {
let mut ordered_cube = cube.clone();
self.activity.sort_by_activity(&mut ordered_cube, ascending);
self.solvers[frame - 1].inductive(&ordered_cube, strengthen, limit)
self.solvers[frame - 1].inductive(&ordered_cube, strengthen)
}

pub fn blocked_with_ordered_with_constrain(
Expand All @@ -51,16 +46,10 @@ impl IC3 {
ascending: bool,
strengthen: bool,
constrain: Vec<Clause>,
limit: bool,
) -> Option<bool> {
) -> bool {
let mut ordered_cube = cube.clone();
self.activity.sort_by_activity(&mut ordered_cube, ascending);
self.solvers[frame - 1].inductive_with_constrain(
&ordered_cube,
strengthen,
constrain,
limit,
)
self.solvers[frame - 1].inductive_with_constrain(&ordered_cube, strengthen, constrain)
}

pub fn get_pred(&mut self, frame: usize, strengthen: bool) -> (Cube, Cube) {
Expand Down Expand Up @@ -175,16 +164,10 @@ impl IC3 {
ts.init.push(!state.lit());
ts.init_map[state] = Some(false);
}
} else if !self.solvers[0]
.solve_with_domain(&[state.lit()], vec![], true, false)
.unwrap()
{
} else if !self.solvers[0].solve_with_domain(&[state.lit()], vec![], true) {
ts.init.push(!state.lit());
ts.init_map[state] = Some(false);
} else if !self.solvers[0]
.solve_with_domain(&[!state.lit()], vec![], true, false)
.unwrap()
{
} else if !self.solvers[0].solve_with_domain(&[!state.lit()], vec![], true) {
ts.init.push(state.lit());
ts.init_map[state] = Some(true);
}
Expand Down

0 comments on commit 8310cd1

Please sign in to comment.