logicrs 0.6.1

Rust library for logic expression
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

use super::DagCnf;
use crate::Lit;
use crate::{Var, VarMap};
use giputils::bitvec::BitVec;
use giputils::hash::GHashSet;
use rand::SeedableRng;
use rand::rngs::StdRng;
use std::ops::Index;

#[derive(Clone, Debug)]
pub struct DagCnfSimulation {
    pub(crate) sim: VarMap<BitVec>,
}

impl Index<Var> for DagCnfSimulation {
    type Output = BitVec;

    #[inline]
    fn index(&self, var: Var) -> &Self::Output {
        &self.sim[var]
    }
}

impl DagCnfSimulation {
    #[inline]
    pub fn val(&self, lit: Lit) -> BitVec {
        if !lit.polarity() {
            !&self.sim[lit.var()]
        } else {
            self.sim[lit.var()].clone()
        }
    }

    fn simulate_var(&mut self, v: Var, dc: &DagCnf) {
        for rel in dc.cnf[v].iter() {
            let mut sim = self.val(rel[0]);
            let mut vl = rel[0];
            for &l in &rel[1..] {
                if l.var() == v {
                    vl = l;
                }
                if l.polarity() {
                    sim |= &self[l.var()];
                } else {
                    sim |= &!&self[l.var()];
                }
            }
            assert!(vl.var() == v);
            if vl.polarity() {
                self.sim[v] |= &!&sim;
            } else {
                self.sim[v] &= &sim;
            }
        }
    }

    pub fn simulate(&mut self, dc: &DagCnf) {
        for v in Var(1)..=dc.max_var() {
            if dc.is_leaf(v) {
                continue;
            }
            self.simulate_var(v, dc);
        }
    }

    #[inline]
    pub fn add(&mut self, val: BitVec) {
        assert!(self.sim.len() == val.len());
        for v in 0..val.len() {
            self.sim[Var(v as u32)].push(val.get(v));
        }
    }
}

impl DagCnf {
    pub fn simulation(&self, num_word: usize) -> DagCnfSimulation {
        let mut rng = StdRng::seed_from_u64(0);
        let mut sim = VarMap::new_with(self.max_var());
        sim[Var::CONST] = BitVec::from_elem(num_word * BitVec::WORD_SIZE, false);
        let mut leafs = GHashSet::new();
        for v in Var(1)..=self.max_var() {
            if self.is_leaf(v) {
                loop {
                    let x = BitVec::new_rand(num_word, &mut rng);
                    if !leafs.contains(&x) {
                        leafs.insert(x.clone());
                        sim[v] = x;
                        break;
                    }
                }
            } else {
                sim[v] = BitVec::from_elem(num_word * BitVec::WORD_SIZE, false);
            }
        }
        let mut s = DagCnfSimulation { sim };
        s.simulate(self);
        s
    }
}