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
46
47
48
49

/*!
A combination of [clause activity](crate::config::Activity) and [lbd](LBD), used to sort clauses on an activity heap.
*/

use crate::config::{Activity, LBD};

/// A combination of [clause activity](crate::config::Activity) and [lbd](LBD), used to sort clauses on an activity heap.
pub struct ActivityLBD {
    /// The activity of a clause.
    pub activity: Activity,
    /// The lbd of a clause.
    pub lbd: LBD,
}

impl Default for ActivityLBD {
    fn default() -> Self {
        ActivityLBD {
            activity: 1.0,
            lbd: 0,
        }
    }
}

// `Revered` as max heap
use std::cmp::Ordering;
impl PartialOrd for ActivityLBD {
    /// [ActivityLBD] is ordered with precedence to lowest lbd and then least activity.
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        let lbd_comparison = match self.lbd.cmp(&other.lbd) {
            Ordering::Less => Ordering::Less,
            Ordering::Greater => Ordering::Greater,
            Ordering::Equal => match self.activity.partial_cmp(&other.activity) {
                None => Ordering::Equal,
                Some(comparison) => match comparison {
                    Ordering::Less => Ordering::Greater,
                    Ordering::Greater => Ordering::Less,
                    Ordering::Equal => Ordering::Equal,
                },
            },
        };
        Some(lbd_comparison)
    }
}

impl PartialEq for ActivityLBD {
    fn eq(&self, other: &Self) -> bool {
        self.lbd.eq(&other.lbd) && self.activity.eq(&other.activity)
    }
}