Struct splr::cdb::ClauseDB [−][src]
pub struct ClauseDB { pub bi_clause: Vec<HashMap<Lit, ClauseId>>, pub watch_cache: Vec<Vec<(ClauseId, Lit)>>, pub lbd_of_dp_ema: Ema, pub eliminated_permanent: Vec<Vec<Lit>>, // some fields omitted }
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
bi_clause: Vec<HashMap<Lit, ClauseId>>
hashed representation of binary clauses.
Note
This means a biclause [l0, l1] is stored at bi_clause[l0] instead of bi_clause[!l0].
watch_cache: Vec<Vec<(ClauseId, Lit)>>
container of watch literals
lbd_of_dp_ema: Ema
EMA of LBD of clauses used in conflict analysis (dependency graph)
eliminated_permanent: Vec<Vec<Lit>>
Trait Implementations
return average activity
set activity
modify one’s activity at conflict analysis in conflict_analyze
in solver
.
update internal counter.
modify one’s activity at value assignment in assign.
modify one’s activity at value assignment in unit propagation.
modify one’s activity at value un-assignment in cancel_until
.
update reward decay.
Warning
this function is the only function that makes dead clauses
replace the mutable watcher list with an empty one, and return the list
detach the watch_cache referred by the head of a watch_cache iterator
register the clause to the previous watch cache
restore detached watch cache
swap the first two literals in a clause.
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
. Read more
fn new_clause_sandbox<A>(
&mut self,
asg: &mut A,
vec: &mut Vec<Lit>
) -> RefClause where
A: AssignIF,
un-register a clause cid
from clause database and make the clause dead.
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
update watches of the clause
generic clause transformer (not in use)
check satisfied and nullified literals in a clause
swap i-th watch with j-th literal then update watch caches correctly
update LBD then convert a learnt clause to permanent if needed.
check the condition to reduce. Read more
record an asserted literal to unsat certification.
save the certification record to a file.
check the number of clauses Read more
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. Read more
minimize a clause.
complete bi-clause network
make and return an object from Config
and CNFDescription
.
update by a solver event.
Auto Trait Implementations
impl RefUnwindSafe for ClauseDB
impl UnwindSafe for ClauseDB
Blanket Implementations
Mutably borrows from an owned value. Read more