[−][src]Trait splr::traits::LitIF

pub trait LitIF {
    fn from_int(x: i32) -> Self;

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

    fn vi(self) -> VarId;

    fn to_i32(self) -> i32;

    fn lbool(self) -> Lbool;

    fn is_positive(self) -> bool;

    fn negate(self) -> Lit;

    fn to_cid(self) -> ClauseId;
}

API for Literal like from_int, from_var, to_cid and so on.

Required methods

fn from_int(x: i32) -> Self

convert from i32.

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

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

convert to Lbool.

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.

Loading content...

Implementors

impl LitIF for Lit[src]

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 lbool(self) -> Lbool[src]

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