smt_scope/analysis/graph/analysis/
proof.rs

1use petgraph::Direction;
2
3use crate::{
4    analysis::raw::{Node, ProofReach},
5    Z3Parser,
6};
7
8use super::run::{CollectInitialiser, Initialiser};
9
10const FORWARD_MASK: ProofReach = ProofReach::ProvesFalse.or(ProofReach::UnderHypothesis);
11const REVERSE_MASK: ProofReach = ProofReach::ReachesProof
12    .or(ProofReach::ReachesNonTrivialProof)
13    .or(ProofReach::ReachesFalse);
14
15pub struct ProofInitialiser<const FORWARD: bool>;
16
17impl<const FORWARD: bool> Initialiser<FORWARD, 3> for ProofInitialiser<FORWARD> {
18    type Value = ProofReach;
19    fn direction() -> Direction {
20        if FORWARD {
21            Direction::Incoming
22        } else {
23            Direction::Outgoing
24        }
25    }
26    fn base(&mut self, node: &Node, parser: &Z3Parser) -> Self::Value {
27        let Some(proof) = node.kind().proof() else {
28            return ProofReach::default();
29        };
30        let kind = parser[proof].kind;
31        let under_hypothesis = ProofReach::UnderHypothesis.if_(kind.is_hypothesis());
32        let reaches_non_trivial_proof = ProofReach::ReachesNonTrivialProof.if_(!kind.is_trivial());
33
34        let proves_false = parser.proves_false(proof);
35        let reaches_false = ProofReach::ReachesFalse.if_(proves_false);
36        let proves_false = ProofReach::ProvesFalse.if_(proves_false);
37        proves_false
38            | under_hypothesis
39            | ProofReach::ReachesProof
40            | reaches_non_trivial_proof
41            | reaches_false
42    }
43    fn assign(&mut self, node: &mut Node, value: Self::Value) {
44        if FORWARD {
45            node.proof = (value & FORWARD_MASK) | (node.proof & FORWARD_MASK.not());
46        } else {
47            node.proof = (value & REVERSE_MASK) | (node.proof & REVERSE_MASK.not());
48        }
49    }
50}
51
52impl<const FORWARD: bool> CollectInitialiser<FORWARD, false, 3> for ProofInitialiser<FORWARD> {
53    fn collect<'n, T: Iterator<Item = &'n Node>>(
54        &mut self,
55        node: &Node,
56        from_all: impl Fn() -> T,
57    ) -> Self::Value {
58        let mut reach = node.proof;
59        for from in from_all() {
60            if FORWARD {
61                let proves_false = from.proof.proves_false();
62                let under_hypothesis =
63                    (from.proof & ProofReach::UnderHypothesis).if_(!proves_false);
64                reach |= under_hypothesis;
65            } else {
66                reach |= from.proof & REVERSE_MASK;
67            }
68        }
69        reach
70    }
71}
smt_scope/analysis/graph/analysis/proof.rs

smt_scope/analysis/graph/analysis/
proof.rs
