satif-cadical 0.2.2

Rust wrapper for the CaDiCaL SAT solver
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

use crate::tracer::Tracer;
use aig::{Aig, AigEdge};
use giputils::hash::{GHashMap, GHashSet};
use logicrs::{Lit, LitVec, Var};
use std::mem::take;

#[derive(Default)]
pub struct Interpolant {
    b_vars: GHashSet<Var>,
    var_edge: GHashMap<Var, Var>,
    cls_labels: GHashMap<usize, bool>,
    next_cls_label: Option<bool>,
    aig: Aig,
    itp: GHashMap<usize, AigEdge>,
    clauses: GHashMap<usize, LitVec>,
    mark: GHashSet<Lit>,
    handle_a: bool,
}

impl Interpolant {
    pub fn new() -> Self {
        Self::default()
    }

    pub fn label_clause(&mut self, k: bool) {
        self.next_cls_label = Some(k)
    }

    pub fn interpolant(self) -> (Aig, GHashMap<Var, Var>) {
        (self.aig, self.var_edge)
    }
}

impl Tracer for Interpolant {
    fn add_original_clause(&mut self, id: usize, _redundant: bool, c: &[Lit], restore: bool) {
        // println!("o {id}, {:?}", c);
        if !restore {
            assert!(
                self.cls_labels
                    .insert(id, take(&mut self.next_cls_label).unwrap())
                    .is_none()
            );
        }
        let itp = if self.cls_labels[&id] {
            assert!(!self.handle_a);
            for l in c.iter() {
                self.b_vars.insert(l.var());
            }
            AigEdge::constant(true)
        } else {
            self.handle_a = true;
            let mut itp = AigEdge::constant(false);
            for l in c.iter().filter(|l| self.b_vars.contains(&l.var())) {
                let e = if let Some(e) = self.var_edge.get(&l.var()) {
                    *e
                } else {
                    let e = Var::new(self.aig.new_input());
                    self.var_edge.insert(l.var(), e);
                    e
                };
                let e = AigEdge::new(e.into(), !l.polarity());
                itp = self.aig.new_or_node(itp, e);
            }
            itp
        };
        self.itp.insert(id, itp);
        self.clauses.insert(id, LitVec::from(c));
    }

    fn add_derived_clause(&mut self, id: usize, _redundant: bool, c: &[Lit], p: &[usize]) {
        // println!("d {id}, {:?}, {:?}", c, p);
        let conflict = p.last().unwrap();
        for l in self.clauses[conflict].iter() {
            self.mark.insert(*l);
        }
        let mut itp = self.itp[conflict];
        for pi in (0..p.len() - 1).rev() {
            for l in self.clauses[&p[pi]].iter() {
                if self.mark.contains(&!*l) {
                    itp = if self.b_vars.contains(&l.var()) {
                        self.aig.new_and_node(itp, self.itp[&p[pi]])
                    } else {
                        self.aig.new_or_node(itp, self.itp[&p[pi]])
                    };
                }
                self.mark.insert(*l);
            }
        }
        self.mark.clear();
        self.itp.insert(id, itp);
        self.clauses.insert(id, LitVec::from(c));
    }

    fn delete_clause(&mut self, id: usize, _redundant: bool, _c: &[Lit]) {
        self.itp.remove(&id);
        self.clauses.remove(&id);
    }

    fn conclude_unsat(&mut self, conclusion: i32, p: &[usize]) {
        if conclusion == 1 {
            assert!(p.len() == 1);
            self.aig.outputs.push(self.itp[&p[0]]);
            let (aig, map) = self.aig.coi_refine();
            self.aig = aig;
            let map = map.inverse();
            let ve = take(&mut self.var_edge);
            for (v, e) in ve {
                if let Some(e) = map.get(&e) {
                    self.var_edge.insert(v, *e);
                }
            }
        } else {
            todo!();
        }
    }
}