Struct ExtendedResolution 

pub struct ExtendedResolution { /* private fields */ }

Extended resolution manager

Implementations

impl ExtendedResolution

pub fn new(num_vars: u32) -> Self

Create a new extended resolution manager

pub fn add_extension(&mut self, def: ExtensionType) -> Var

Add an extension variable

pub fn add_and(&mut self, x: Lit, y: Lit) -> Var

Add an AND extension: z ↔ (x ∧ y)

pub fn add_or(&mut self, x: Lit, y: Lit) -> Var

Add an OR extension: z ↔ (x ∨ y)

pub fn add_xor(&mut self, x: Lit, y: Lit) -> Var

Add an XOR extension: z ↔ (x ⊕ y)

pub fn add_ite(&mut self, cond: Lit, then_lit: Lit, else_lit: Lit) -> Var

Add an ITE extension: z ↔ (if c then t else e)

pub fn add_equiv(&mut self, x: Lit, y: Lit) -> Var

Add an EQUIV extension: z ↔ (x ↔ y)

pub fn get_all_cnf(&self) -> Vec<Vec<Lit>>

Get all CNF clauses for all extensions

pub fn get_extension(&self, var: Var) -> Option<&Extension>

Get extension definition for a variable

pub fn is_extension(&self, var: Var) -> bool

Check if a variable is an extension variable

pub fn num_vars(&self) -> u32

Get the current number of variables (including extensions)

pub fn num_extensions(&self) -> usize

Get the number of extension variables

pub fn get_extensions(&self) -> Vec<Var>

Get all extension variables

pub fn tseitin_and(&mut self, lits: &[Lit]) -> Var

Tseitin transformation for a formula Returns the top-level variable representing the formula

pub fn tseitin_or(&mut self, lits: &[Lit]) -> Var

Tseitin transformation for OR