Type Definition splr::types::Lit

type Lit = u32;

Literal encoded on u32 as:

• the literal corresponding to a positive occurrence of *variable n is 2 * n and
• that for the negative one is 2 * n + 1.

Examples

use splr::traits::LitIF;
use splr::types::*;
assert_eq!(2, Lit::from_int( 1) as i32);
assert_eq!(3, Lit::from_int(-1) as i32);
assert_eq!(4, Lit::from_int( 2) as i32);
assert_eq!(5, Lit::from_int(-2) as i32);
assert_eq!( 1, Lit::from_int( 1).to_i32());
assert_eq!(-1, Lit::from_int(-1).to_i32());
assert_eq!( 2, Lit::from_int( 2).to_i32());
assert_eq!(-2, Lit::from_int(-2).to_i32());

Trait Implementations

impl LitIF for Lit

Examples

use splr::traits::LitIF;
use splr::types::*;
assert_eq!(Lit::from_int(1), Lit::from_var(1 as VarId, TRUE));
assert_eq!(Lit::from_int(2), Lit::from_var(2 as VarId, TRUE));
assert_eq!(1, Lit::from_var(1, TRUE).vi());
assert_eq!(1, Lit::from_var(1, FALSE).vi());
assert_eq!(2, Lit::from_var(2, TRUE).vi());
assert_eq!(2, Lit::from_var(2, FALSE).vi());
assert_eq!(Lit::from_int( 1), Lit::from_int(-1).negate());
assert_eq!(Lit::from_int(-1), Lit::from_int( 1).negate());
assert_eq!(Lit::from_int( 2), Lit::from_int(-2).negate());
assert_eq!(Lit::from_int(-2), Lit::from_int( 2).negate());

fn from_int(x: i32) -> Lit

convert from i32.

fn from_var(vi: VarId, p: Lbool) -> Lit

convert VarId to Lit. It returns a positive literal if p is TRUE or BOTTOM.

fn vi(self) -> VarId

convert to var index.

fn to_i32(self) -> i32

convert to i32.

fn lbool(self) -> Lbool

• positive Lit (= even u32) => TRUE (= 1 as u8)
• negative Lit (= odd u32) => LFASE (= 0 as u8)

fn is_positive(self) -> bool

return the sign or phase; return true if it is a positive literal.

fn negate(self) -> Lit

flip the sign.

fn to_cid(self) -> ClauseId

lift a literal to a virtual clause id.