Skip to content

Commit

Permalink
Delete feature interleave
Browse files Browse the repository at this point in the history
  • Loading branch information
@shnarazk
shnarazk committed Dec 14, 2024
1 parent df09ded commit a992ed8
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 180 deletions.
2 changes: 0 additions & 2 deletions src/config.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -275,8 +275,6 @@ impl Config {
"EVSIDS rewarding",
#[cfg(feature = "incremental_solver")]
"incremental solver",
#[cfg(feature = "interleave")]
"interleaving slover",
#[cfg(feature = "just_used")]
"use 'just used' flag",
#[cfg(feature = "LRB_rewarding")]
Expand Down
178 changes: 0 additions & 178 deletions src/solver/search.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,184 +72,6 @@ impl SolveIF for Solver {
/// assert_ne!(res.unwrap(), Certificate::UNSAT);
/// }
///```
#[cfg(not(feature = "interleave"))]
fn solve(&mut self) -> SolverResult {
let Solver {
ref mut asg,
ref mut cdb,
ref mut state,
} = self;
if cdb.check_size().is_err() {
return Err(SolverError::OutOfMemory);
}
#[cfg(feature = "incremental_solver")]
{
// Reinitialize AssignStack::var_order with respect for assignments.
asg.rebuild_order();
}
state.progress_header();
state.progress(asg, cdb);
state.flush("");
state.flush("Preprocessing stage: ");

#[cfg(feature = "clause_vivification")]
{
state.flush("vivifying...");
if cdb.vivify(asg, state).is_err() {
#[cfg(feature = "support_user_assumption")]
analyze_final(asg, state, &cdb[ci]);

state.log(None, "By vivifier as a pre-possessor");
return Ok(Certificate::UNSAT);
}
debug_assert!(!asg.remains());
}
{
debug_assert_eq!(asg.decision_level(), asg.root_level());
let mut elim = Eliminator::instantiate(&state.config, &state.cnf);
if elim.simplify(asg, cdb, state, true).is_err() {
if cdb.check_size().is_err() {
return Err(SolverError::OutOfMemory);
}
state.log(None, "By eliminator");
return Ok(Certificate::UNSAT);
}

#[cfg(all(feature = "clause_elimination", not(feature = "incremental_solver")))]
{
//
//## Propagate all trivial literals (an essential step)
//
// Set appropriate phases and push all the unit clauses to assign stack.
// To do so, we use eliminator's occur list.
// Thus we have to call `activate` and `prepare` firstly, to build occur lists.
// Otherwise all literals are assigned wrongly.

state.flush("phasing...");
elim.prepare(asg, cdb, true);
for vi in 1..=asg.num_vars {
if asg.assign(vi).is_some() {
continue;
}
if let Some((p, m)) = elim.stats(vi) {
// We can't call `asg.assign_at_root_level(l)` even if p or m == 0.
// This means we can't pick `!l`.
// This becomes a problem in the case of incremental solving.
#[cfg(not(feature = "incremental_solver"))]
{
if m == 0 {
let l = Lit::from((vi, true));
debug_assert!(asg.assigned(l).is_none());
cdb.certificate_add_assertion(l);
if asg.assign_at_root_level(l).is_err() {
return Ok(Certificate::UNSAT);
}
} else if p == 0 {
let l = Lit::from((vi, false));
debug_assert!(asg.assigned(l).is_none());
cdb.certificate_add_assertion(l);
if asg.assign_at_root_level(l).is_err() {
return Ok(Certificate::UNSAT);
}
}
}
asg.var_mut(vi).set(FlagVar::PHASE, m < p);
elim.enqueue_var(asg, vi, false);
}
}
//
//## Run eliminator
//

state.flush("simplifying...");
if elim.simplify(asg, cdb, state, false).is_err() {
// Why inconsistent? Because the CNF contains a conflict, not an error!
// Or out of memory.
state.progress(asg, cdb);
if cdb.check_size().is_err() {
return Err(SolverError::OutOfMemory);
}
return Ok(Certificate::UNSAT);
}
for vi in 1..=asg.num_vars {
if asg.assign(vi).is_some() || asg.var(vi).is(FlagVar::ELIMINATED) {
continue;
}
match elim.stats(vi) {
Some((_, 0)) => (),
Some((0, _)) => (),
Some((p, m)) if m * 10 < p => asg.var_mut(vi).turn_on(FlagVar::PHASE),
Some((p, m)) if p * 10 < m => asg.var_mut(vi).turn_off(FlagVar::PHASE),
_ => (),
}
}
let act = 1.0 / (asg.num_vars as f64).powf(0.25);
for vi in 1..asg.num_vars {
if !asg.var(vi).is(FlagVar::ELIMINATED) {
asg.set_activity(vi, act);
}
}
asg.rebuild_order();
}
asg.eliminated.append(elim.eliminated_lits());
state[Stat::Simplify] += 1;
state[Stat::SubsumedClause] = elim.num_subsumed;
}
//
//## Search
//
state.progress(asg, cdb);
let answer = search(asg, cdb, state);
state.progress(asg, cdb);
match answer {
Ok(true) => {
#[cfg(feature = "trace_equivalency")]
asg.dump_cnf(cdb, "last-step.cnf");

// As a preparation for incremental solving, we need to backtrack to the
// root level. So all assignments, including assignments to eliminated vars,
// are stored in an extra storage. It has the same type of `AssignStack::assign`.
let model = asg.extend_model(cdb);

// Run validator on the extended model.
if cdb.validate(&model, false).is_some() {
state.log(None, "failed to validate the extended model");
state.progress(asg, cdb);
return Err(SolverError::SolverBug);
}

// map `Option<bool>` to `i32`, and remove the dummy var at the head.
let vals = asg
.var_iter()
.enumerate()
.skip(1)
.map(|(vi, _)| i32::from(Lit::from((vi, model[vi].unwrap()))))
.collect::<Vec<i32>>();

// As a preparation for incremental solving, turn flags off.
for v in asg.var_iter_mut().skip(1) {
if v.is(FlagVar::ELIMINATED) {
v.turn_off(FlagVar::ELIMINATED);
}
}
RESTART!(asg, cdb, state);
Ok(Certificate::SAT(vals))
}
Ok(false) | Err(SolverError::EmptyClause | SolverError::RootLevelConflict(_)) => {
#[cfg(feature = "support_user_assumption")]
analyze_final(asg, state, &cdb[ci]);

RESTART!(asg, cdb, state);
Ok(Certificate::UNSAT)
}
Err(e) => {
RESTART!(asg, cdb, state);
state.progress(asg, cdb);
Err(e)
}
}
}
#[cfg(feature = "interleave")]
fn solve(&mut self) -> SolverResult {
let mut sc = match self.prepare() {
Ok(sc) => sc,
Expand Down

0 comments on commit a992ed8

Please sign in to comment.