Struct sat_rs::notation::Formula

pub struct Formula {
    pub clauses: Vec<Clause>,
    pub literals: Vec<i32>,
    pub num_clauses: i32,
    pub num_vars: i32,
}

Struct representing a Propositional Formula

Derives from Debug and Clone.

Contains a vector of Clauses, a vector of Literals, the number of clauses and the number of variables

Fields

clauses: Vec<Clause>

literals: Vec<i32>

num_clauses: i32

num_vars: i32

Implementations

impl Formula

pub fn new() -> Formula

Creates a new Formula with an empty vector of Clauses and Literals

Examples

use sat_rs::notation::Formula;

let formula = Formula::new();

pub fn evaluate(&mut self, interpretation: &HashMap<i32, bool>) -> bool

Evaluates a Formula given an interpretation

Arguments

• interpretation - A HashMap of i32 and bool representing the interpretation

Examples

Assuming the CNF file is in /bin/problem.cnf and contains the following:

p cnf 3 1
1 -3 0
2 3 -1 0

use sat_rs::cnfparser;
use std::collections::HashMap;

let buffer = include_str!("bin/problem.cnf");
let mut formula = cnfparser::parse_cnf(&buffer);

let mut interpretation: HashMap<i32, bool> = HashMap::new();
interpretation.insert(1, false);
interpretation.insert(2, false);
interpretation.insert(3, false);

assert_eq!(formula.unwrap().evaluate(&interpretation), true);

Trait Implementations

impl Clone for Formula

fn clone(&self) -> Formula

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Formula

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.