diff --git a/src/config.rs b/src/config.rs index 715278270..3d1aa9fbc 100644 --- a/src/config.rs +++ b/src/config.rs @@ -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")] diff --git a/src/solver/search.rs b/src/solver/search.rs index bf2b60153..cc5a4ce42 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -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` 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::>(); - - // 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,