varisat 0.2.2

A CDCL based SAT solver (library)
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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131

//! Central solver data structure.
//!
//! This module defines the `Context` data structure which holds all data used by the solver. It
//! also contains global notification functions that likely need to be extended when new parts are
//! added to the solver.
use partial_ref::{part, partial, PartialRef, PartialRefTarget};

use crate::{
    analyze_conflict::AnalyzeConflict,
    assumptions::Assumptions,
    binary::BinaryClauses,
    clause::{ClauseActivity, ClauseAlloc, ClauseDb},
    config::{SolverConfig, SolverConfigUpdate},
    decision::vsids::Vsids,
    model::Model,
    proof::Proof,
    prop::{Assignment, ImplGraph, Trail, Watchlists},
    schedule::Schedule,
    state::SolverState,
    tmp::{TmpData, TmpFlags},
    variables::Variables,
};

/// Part declarations for the [`Context`] struct.
pub mod parts {
    use super::*;

    part!(pub AnalyzeConflictP: AnalyzeConflict);
    part!(pub AssignmentP: Assignment);
    part!(pub BinaryClausesP: BinaryClauses);
    part!(pub ClauseActivityP: ClauseActivity);
    part!(pub ClauseAllocP: ClauseAlloc);
    part!(pub ClauseDbP: ClauseDb);
    part!(pub ImplGraphP: ImplGraph);
    part!(pub AssumptionsP: Assumptions);
    part!(pub ModelP: Model);
    part!(pub ProofP<'a>: Proof<'a>);
    part!(pub ScheduleP: Schedule);
    part!(pub SolverConfigP: SolverConfig);
    part!(pub SolverStateP: SolverState);
    part!(pub TmpDataP: TmpData);
    part!(pub TmpFlagsP: TmpFlags);
    part!(pub TrailP: Trail);
    part!(pub VariablesP: Variables);
    part!(pub VsidsP: Vsids);
    part!(pub WatchlistsP: Watchlists);
}

use parts::*;

/// Central solver data structure.
///
/// This struct contains all data kept by the solver. Most functions operating on multiple fields of
/// the context use partial references provided by the `partial_ref` crate. This documents the data
/// dependencies and makes the borrow checker happy without the overhead of passing individual
/// references.
#[derive(PartialRefTarget, Default)]
pub struct Context<'a> {
    #[part(AnalyzeConflictP)]
    pub analyze_conflict: AnalyzeConflict,
    #[part(AssignmentP)]
    pub assignment: Assignment,
    #[part(BinaryClausesP)]
    pub binary_clauses: BinaryClauses,
    #[part(ClauseActivityP)]
    pub clause_activity: ClauseActivity,
    #[part(ClauseAllocP)]
    pub clause_alloc: ClauseAlloc,
    #[part(ClauseDbP)]
    pub clause_db: ClauseDb,
    #[part(ImplGraphP)]
    pub impl_graph: ImplGraph,
    #[part(AssumptionsP)]
    pub assumptions: Assumptions,
    #[part(ModelP)]
    pub model: Model,
    #[part(ProofP<'a>)]
    pub proof: Proof<'a>,
    #[part(ScheduleP)]
    pub schedule: Schedule,
    #[part(SolverConfigP)]
    pub solver_config: SolverConfig,
    #[part(SolverStateP)]
    pub solver_state: SolverState,
    #[part(TmpDataP)]
    pub tmp_data: TmpData,
    #[part(TmpFlagsP)]
    pub tmp_flags: TmpFlags,
    #[part(TrailP)]
    pub trail: Trail,
    #[part(VariablesP)]
    pub variables: Variables,
    #[part(VsidsP)]
    pub vsids: Vsids,
    #[part(WatchlistsP)]
    pub watchlists: Watchlists,
}

/// Update structures for a new variable count.
pub fn set_var_count(
    mut ctx: partial!(
        Context,
        mut AnalyzeConflictP,
        mut AssignmentP,
        mut BinaryClausesP,
        mut ImplGraphP,
        mut TmpFlagsP,
        mut VsidsP,
        mut WatchlistsP,
    ),
    count: usize,
) {
    ctx.part_mut(AnalyzeConflictP).set_var_count(count);
    ctx.part_mut(AssignmentP).set_var_count(count);
    ctx.part_mut(BinaryClausesP).set_var_count(count);
    ctx.part_mut(ImplGraphP).set_var_count(count);
    ctx.part_mut(TmpFlagsP).set_var_count(count);
    ctx.part_mut(VsidsP).set_var_count(count);
    ctx.part_mut(WatchlistsP).set_var_count(count);
}

/// The solver configuration has changed.
pub fn config_changed(
    mut ctx: partial!(Context, mut VsidsP, mut ClauseActivityP, SolverConfigP),
    _update: &SolverConfigUpdate,
) {
    let (config, mut ctx) = ctx.split_part(SolverConfigP);
    ctx.part_mut(VsidsP).set_decay(config.vsids_decay);
    ctx.part_mut(ClauseActivityP)
        .set_decay(config.clause_activity_decay);
}