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

//! 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;
use crate::assumptions::Assumptions;
use crate::binary::BinaryClauses;
use crate::clause::{ClauseActivity, ClauseAlloc, ClauseDb};
use crate::config::{SolverConfig, SolverConfigUpdate};
use crate::decision::vsids::Vsids;
use crate::model::Model;
use crate::proof::Proof;
use crate::prop::{Assignment, ImplGraph, Trail, Watchlists};
use crate::schedule::Schedule;
use crate::state::SolverState;
use crate::tmp::{TmpData, TmpFlags};
use crate::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);
}