Struct CompressionSddBuilder

pub struct CompressionSddBuilder<'a> { /* private fields */ }

Implementations

impl<'a> CompressionSddBuilder<'a>

pub fn new(vtree: VTree) -> CompressionSddBuilder<'a>

Trait Implementations

impl<'a> SddBuilder<'a> for CompressionSddBuilder<'a>

fn compress(&'a self, node: &mut Vec<SddAnd<'a>>)

Canonicalizes the list of (prime, sub) terms in-place node: a list of (prime, sub) pairs

fn canonicalize( &'a self, node: Vec<SddAnd<'a>>, table: VTreeIndex, ) -> SddPtr<'a>

Returns a canonicalized SDD pointer from a list of (prime, sub) pairs

fn vtree_manager(&self) -> &VTreeManager

fn app_cache_get(&self, and: &SddAnd<'a>) -> Option<SddPtr<'a>>

fn app_cache_insert(&self, and: SddAnd<'a>, ptr: SddPtr<'a>)

fn ite_cache_hash(&self, ite: &Ite<SddPtr<'_>>) -> u64

fn ite_cache_get(&self, ite: Ite<SddPtr<'a>>, hash: u64) -> Option<SddPtr<'_>>

fn ite_cache_insert(&self, ite: Ite<SddPtr<'a>>, res: SddPtr<'a>, hash: u64)

fn get_or_insert_bdd(&'a self, bdd: BinarySDD<'a>) -> SddPtr<'a>

fn get_or_insert_sdd(&'a self, or: SddOr<'a>) -> SddPtr<'a>

fn sdd_eq(&'a self, a: SddPtr<'a>, b: SddPtr<'a>) -> bool

fn set_compression(&mut self, b: bool)

fn node_iter(&self) -> Vec<SddPtr<'_>>

fn stats(&self) -> SddBuilderStats

fn log_recursive_call(&self)

fn is_true(&'a self, a: SddPtr<'a>) -> bool

fn is_false(&'a self, a: SddPtr<'a>) -> bool

fn unique_or(&'a self, node: Vec<SddAnd<'a>>, table: VTreeIndex) -> SddPtr<'a>

fn unique_bdd(&'a self, bdd: BinarySDD<'a>) -> SddPtr<'a>

fn and_indep( &'a self, a: SddPtr<'a>, b: SddPtr<'a>, lca: VTreeIndex, ) -> SddPtr<'a>

conjoin two SDDs that are in independent vtrees a is prime to b

fn and_sub_desc(&'a self, r: SddPtr<'a>, d: SddPtr<'a>) -> SddPtr<'a>

conjoin SDDs where d is a descendent of r, and d is sub to r i.e. for vtree 3 1 5 0 2 4 6 r might be wrt. node 3, and d wrt. node 5

fn and_prime_desc(&'a self, r: SddPtr<'a>, d: SddPtr<'a>) -> SddPtr<'a>

conjoin SDDs where d is a descendent of r, and r is sub to d i.e. for vtree 3 1 5 0 2 4 6 r might be wrt. node 3, and d wrt. node 1

fn and_cartesian( &'a self, a: SddPtr<'a>, b: SddPtr<'a>, lca: VTreeIndex, ) -> SddPtr<'a>

conjoin SDDs where a and b are wrt. the same vtree node

fn num_vars(&self) -> usize

fn vtree(&self, ptr: SddPtr<'_>) -> &VTree

fn vtree_index(&self, ptr: SddPtr<'_>) -> VTreeIndex

fn compile_cnf_helper(&'a self, vec: &[SddPtr<'a>]) -> Option<SddPtr<'a>>

fn print_sdd(&'a self, ptr: SddPtr<'a>) -> String