pub struct ClauseDB {
pub eliminated_permanent: Vec<Vec<Lit>>,
/* private fields */
}
Expand description
Clause database
use crate::{splr::config::Config, splr::types::*};
use crate::splr::cdb::ClauseDB;
let cdb = ClauseDB::instantiate(&Config::default(), &CNFDescription::default());
Fields§
§eliminated_permanent: Vec<Vec<Lit>>
Trait Implementations§
source§impl ClauseDBIF for ClauseDB
impl ClauseDBIF for ClauseDB
source§fn remove_clause(&mut self, cid: ClauseId)
fn remove_clause(&mut self, cid: ClauseId)
§Warning
this function is the only function that makes dead clauses
source§fn reduce(&mut self, asg: &mut impl AssignIF, setting: ReductionType)
fn reduce(&mut self, asg: &mut impl AssignIF, setting: ReductionType)
reduce the number of ‘learnt’ or removable clauses.
source§fn dump_cnf(&self, asg: &impl AssignIF, fname: &Path)
fn dump_cnf(&self, asg: &impl AssignIF, fname: &Path)
dump all active clauses and assertions as a CNF file.
source§fn binary_links(&self, l: Lit) -> &BinaryLinkList
fn binary_links(&self, l: Lit) -> &BinaryLinkList
return binary links:
BinaryLinkList
connected with a Lit
.fn fetch_watch_cache_entry(&self, lit: Lit, wix: usize) -> (ClauseId, Lit)
source§fn watch_cache_iter(&mut self, l: Lit) -> WatchCacheIterator
fn watch_cache_iter(&mut self, l: Lit) -> WatchCacheIterator
replace the mutable watcher list with an empty one, and return the list
source§fn detach_watch_cache(&mut self, l: Lit, iter: &mut WatchCacheIterator)
fn detach_watch_cache(&mut self, l: Lit, iter: &mut WatchCacheIterator)
detach the watch_cache referred by the head of a watch_cache iterator
source§fn swap_watch(&mut self, cid: ClauseId)
fn swap_watch(&mut self, cid: ClauseId)
swap the first two literals in a clause.
source§fn new_clause(
&mut self,
asg: &mut impl AssignIF,
vec: &mut Vec<Lit>,
learnt: bool
) -> RefClause
fn new_clause( &mut self, asg: &mut impl AssignIF, vec: &mut Vec<Lit>, learnt: bool ) -> RefClause
allocate a new clause and return its id.
Note this removes an eliminated Lit
p
from a clause. This is an O(n) function!
This returns true
if the clause became a unit clause.
And this is called only from Eliminator::strengthen_clause
.fn new_clause_sandbox( &mut self, asg: &mut impl AssignIF, vec: &mut Vec<Lit> ) -> RefClause
source§fn remove_clause_sandbox(&mut self, cid: ClauseId)
fn remove_clause_sandbox(&mut self, cid: ClauseId)
un-register a clause
cid
from clause database and make the clause dead.source§fn transform_by_restoring_watch_cache(
&mut self,
l: Lit,
iter: &mut WatchCacheIterator,
op: Option<Lit>
)
fn transform_by_restoring_watch_cache( &mut self, l: Lit, iter: &mut WatchCacheIterator, op: Option<Lit> )
push back a watch literal cache by adjusting the iterator for
lit
source§fn transform_by_elimination(&mut self, cid: ClauseId, p: Lit) -> RefClause
fn transform_by_elimination(&mut self, cid: ClauseId, p: Lit) -> RefClause
update watches of the clause
source§fn transform_by_replacement(
&mut self,
cid: ClauseId,
new_lits: &mut Vec<Lit>
) -> RefClause
fn transform_by_replacement( &mut self, cid: ClauseId, new_lits: &mut Vec<Lit> ) -> RefClause
generic clause transformer (not in use)
source§fn transform_by_simplification(
&mut self,
asg: &mut impl AssignIF,
cid: ClauseId
) -> RefClause
fn transform_by_simplification( &mut self, asg: &mut impl AssignIF, cid: ClauseId ) -> RefClause
check satisfied and nullified literals in a clause
source§fn transform_by_updating_watch(
&mut self,
cid: ClauseId,
old: usize,
new: usize,
removed: bool
)
fn transform_by_updating_watch( &mut self, cid: ClauseId, old: usize, new: usize, removed: bool )
swap i-th watch with j-th literal then update watch caches correctly
source§fn update_at_analysis(&mut self, asg: &impl AssignIF, cid: ClauseId) -> bool
fn update_at_analysis(&mut self, asg: &impl AssignIF, cid: ClauseId) -> bool
update flags.
return
true
if it’s learnt.source§fn certificate_add_assertion(&mut self, lit: Lit)
fn certificate_add_assertion(&mut self, lit: Lit)
record an asserted literal to unsat certification.
source§fn certificate_save(&mut self)
fn certificate_save(&mut self)
save the certification record to a file.
source§fn check_size(&self) -> Result<bool, SolverError>
fn check_size(&self) -> Result<bool, SolverError>
check the number of clauses Read more
source§fn validate(&self, model: &[Option<bool>], strict: bool) -> Option<ClauseId>
fn validate(&self, model: &[Option<bool>], strict: bool) -> Option<ClauseId>
returns None if the given assignment is a model of a problem.
Otherwise returns a clause which is not satisfiable under a given assignment.
Clauses with an unassigned literal are treated as falsified in
strict
mode.source§fn minimize_with_bi_clauses(&mut self, asg: &impl AssignIF, vec: &mut Vec<Lit>)
fn minimize_with_bi_clauses(&mut self, asg: &impl AssignIF, vec: &mut Vec<Lit>)
minimize a clause.
source§fn complete_bi_clauses(&mut self, asg: &mut impl AssignIF)
fn complete_bi_clauses(&mut self, asg: &mut impl AssignIF)
complete bi-clause network
source§impl Instantiate for ClauseDB
impl Instantiate for ClauseDB
source§fn instantiate(config: &Config, cnf: &CNFDescription) -> ClauseDB
fn instantiate(config: &Config, cnf: &CNFDescription) -> ClauseDB
make and return an object from
Config
and CNFDescription
.source§fn handle(&mut self, e: SolverEvent)
fn handle(&mut self, e: SolverEvent)
update by a solver event.
source§impl StochasticLocalSearchIF for ClauseDB
impl StochasticLocalSearchIF for ClauseDB
source§fn stochastic_local_search(
&mut self,
_asg: &impl AssignIF,
assignment: &mut HashMap<VarId, bool>,
limit: usize
) -> (usize, usize)
fn stochastic_local_search( &mut self, _asg: &impl AssignIF, assignment: &mut HashMap<VarId, bool>, limit: usize ) -> (usize, usize)
returns the decision level of the given assignment and the one of the final assignment.
Note: the lower level a set of clauses make a conflict at,
the higher learning rate a solver can keep and the better learnt clauses we will have.
This would be a better criteria that can be used in CDCL solvers.
source§impl VivifyIF for ClauseDB
impl VivifyIF for ClauseDB
source§fn vivify(
&mut self,
asg: &mut AssignStack,
state: &mut State
) -> MaybeInconsistent
fn vivify( &mut self, asg: &mut AssignStack, state: &mut State ) -> MaybeInconsistent
vivify clauses under asg
Auto Trait Implementations§
impl RefUnwindSafe for ClauseDB
impl Send for ClauseDB
impl Sync for ClauseDB
impl Unpin for ClauseDB
impl UnwindSafe for ClauseDB
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more