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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72

/*!
Callbacks associated with a context.

A context supports various callbacks, and
*/
use std::collections::HashSet;

use super::GenericContext;
use crate::{
    db::{clause::db_clause::dbClause, ClauseKey},
    structures::{clause::ClauseSource, literal::CLiteral},
};

/// The type of callback made on premises used during an instance of resolution.
pub type CallbackOnPremises = dyn FnMut(&HashSet<ClauseKey>);

/// The type of callback made on a clause and source of that clause.
pub type CallbackOnClauseSource = dyn FnMut(&dbClause, &ClauseSource);

/// The type of callback made on a clause.
pub type CallbackOnClause = dyn FnMut(&dbClause);

/// The type of callback made on a literal.
pub type CallbackOnLiteral = dyn FnMut(CLiteral);

/// The type of callback used to request termination of some procedure.
pub type CallbackTerminate = dyn FnMut() -> bool;

/// Methods to set general callbacks.
impl<R: rand::Rng + std::default::Default> GenericContext<R> {}

/// Methods to set callbacks called within the clause database.
impl<R: rand::Rng + std::default::Default> GenericContext<R> {
    /// Set a callback to be made when an original clause is added to the context.
    pub fn set_callback_original(&mut self, callback: Box<CallbackOnClauseSource>) {
        self.clause_db.set_callback_original(callback);
    }

    /// Set a callback to be made when an addition clause is added to the context.
    pub fn set_callback_addition(&mut self, callback: Box<CallbackOnClauseSource>) {
        self.clause_db.set_callback_addition(callback);
    }

    /// Set a callback to be made when the value of a literal is fixed within a solve.
    pub fn set_callback_fixed(&mut self, callback: Box<CallbackOnLiteral>) {
        self.clause_db.set_callback_fixed(callback);
    }

    /// Set a callback to be made when a clause is deleted from the context.
    pub fn set_callback_delete(&mut self, callback: Box<CallbackOnClause>) {
        self.clause_db.set_callback_delete(callback);
    }

    /// Set a callback to be made when the context is identified as unsatisfiable.
    pub fn set_callback_unsatisfiable(&mut self, callback: Box<CallbackOnClause>) {
        self.clause_db.set_callback_unsatisfiable(callback);
    }

    /// Set a callback to terminate a solve.
    pub fn set_callback_terminate_solve(&mut self, callback: Box<CallbackTerminate>) {
        self.callback_terminate = Some(callback);
    }

    /// Check whether the terminate callback has requested termination of a solve.
    pub fn check_callback_terminate_solve(&mut self) -> bool {
        if let Some(callback) = &mut self.callback_terminate {
            callback()
        } else {
            false
        }
    }
}