otter_sat 0.1.0

A library for determining the satisfiability of boolean formulas written in conjunctive normal form, developed to support investigation into solvers by researchers, developers, or anyone curious.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

//! Implementation of clause trait for a slice of literals.

use crate::{
    config::LBD,
    db::{atom::AtomDB, clause::db_clause::dbClause},
    structures::{atom::Atom, clause::Clause, literal::CLiteral, valuation::Valuation},
};

impl Clause for dbClause {
    fn as_dimacs(&self, zero: bool) -> String {
        self.clause().as_dimacs(zero)
    }

    fn asserts(&self, val: &impl Valuation) -> Option<CLiteral> {
        self.clause().asserts(val)
    }

    fn lbd(&self, atom_db: &AtomDB) -> LBD {
        self.clause().lbd(atom_db)
    }

    fn literals(&self) -> impl std::iter::Iterator<Item = CLiteral> {
        self.clause().literals()
    }

    fn size(&self) -> usize {
        self.clause().len()
    }

    fn atoms(&self) -> impl Iterator<Item = Atom> {
        self.clause().atoms()
    }

    fn canonical(self) -> super::CClause {
        self.clause().to_vec()
    }

    fn unsatisfiable_on(&self, valuation: &impl Valuation) -> bool {
        self.clause().unsatisfiable_on(valuation)
    }

    unsafe fn unsatisfiable_on_unchecked(&self, valuation: &impl Valuation) -> bool {
        self.clause().unsatisfiable_on_unchecked(valuation)
    }
}