smt_scope/analysis/
cdcl.rs

1use crate::{
2    items::{CdclIdx, TermIdx},
3    FxHashMap, TiVec, Z3Parser,
4};
5
6#[derive(Default)]
7pub struct CdclAnalysis {
8    pub assignments: FxHashMap<TermIdx, (AssignData, AssignData)>,
9}
10
11#[derive(Clone, Copy, Default)]
12pub struct AssignData {
13    pub count: u32,
14    pub cost: u32,
15}
16
17impl CdclAnalysis {
18    pub fn new(parser: &Z3Parser) -> Self {
19        let mut self_ = Self::default();
20        let mut cdcl_size: TiVec<CdclIdx, _> = parser.cdcls().iter().map(|_| 1u32).collect();
21
22        for (cidx, data) in parser.cdcls().iter_enumerated().rev() {
23            let Some(parent) = data.backlink(cidx).to_root() else {
24                continue;
25            };
26            let size = cdcl_size[cidx];
27            cdcl_size[parent] += size;
28
29            for a in data.get_assignments() {
30                let a = parser.lits[a].term;
31                let (true_data, false_data) = self_.assignments.entry(a.literal).or_default();
32                if a.value {
33                    true_data.count += 1;
34                    true_data.cost += size;
35                } else {
36                    false_data.count += 1;
37                    false_data.cost += size;
38                }
39            }
40        }
41        self_
42    }
43}
smt_scope/analysis/cdcl.rs

smt_scope/analysis/
cdcl.rs
