rust_formal_verification/models/finite_state_transition_system/
construction.rs

1// ************************************************************************************************
2// use
3// ************************************************************************************************
4
5// use std::collections::HashSet;
6
7use std::collections::{HashMap, HashSet};
8
9use crate::algorithms::formula_logic::get_all_variable_numbers_in_cnf;
10use crate::formulas::literal::VariableType;
11use crate::formulas::{Clause, Cube, Literal, CNF};
12use crate::models::and_inverter_graph::aig_wire::AIGWire;
13use crate::models::AndInverterGraph;
14use crate::solvers::sat::{stateless::VarisatSolver, SatResponse};
15
16use super::FiniteStateTransitionSystem;
17
18// ************************************************************************************************
19// impl
20// ************************************************************************************************
21
22impl FiniteStateTransitionSystem {
23    // ********************************************************************************************
24    // helper functions
25    // ********************************************************************************************
26
27    fn get_literal_from_aig_wire(aig_literal: AIGWire) -> Literal {
28        aig_literal.get_literal()
29    }
30
31    fn get_cnf_that_describes_wire_values_as_a_function_of_latch_values_for_specific_wires(
32        aig: &AndInverterGraph,
33        wires: &[AIGWire],
34    ) -> CNF {
35        let and_info = aig.get_and_information_in_cone_of_influence(wires);
36
37        let mut cnf = CNF::new();
38        // encode and gates into formula
39        for (lhs, rhs0, rhs1) in and_info {
40            // get variable numbers
41            let and_output = Self::get_literal_from_aig_wire(lhs);
42            assert!(!and_output.is_negated());
43
44            // cannot create variable with number 0.
45            if rhs0 == AIGWire::new(0) || rhs1 == AIGWire::new(0) {
46                cnf.add_clause(&Clause::new(&[!and_output]));
47            } else if rhs0 == AIGWire::new(1) && rhs1 == AIGWire::new(1) {
48                cnf.add_clause(&Clause::new(&[and_output]));
49            } else if rhs0 == AIGWire::new(1) {
50                let and_input_1 = Self::get_literal_from_aig_wire(rhs1);
51                cnf.add_clause(&Clause::new(&[!and_input_1, and_output]));
52                cnf.add_clause(&Clause::new(&[and_input_1, !and_output]));
53            } else if rhs1 == AIGWire::new(1) {
54                let and_input_0 = Self::get_literal_from_aig_wire(rhs0);
55                cnf.add_clause(&Clause::new(&[!and_input_0, and_output]));
56                cnf.add_clause(&Clause::new(&[and_input_0, !and_output]));
57            } else {
58                let and_input_1 = Self::get_literal_from_aig_wire(rhs1);
59                let and_input_0 = Self::get_literal_from_aig_wire(rhs0);
60                // lhs = rhs0 ^ rhs1 <=> (lhs -> rhs0 ^ rhs1) ^ (lhs <- rhs0 ^ rhs1)
61                // <=> (!lhs \/ (rhs0 ^ rhs1)) ^ (lhs \/ !(rhs0 ^ rhs1))
62                // <=> ((!lhs \/ rhs0) ^ (!lhs \/ rhs1)) ^ (lhs \/ !rhs0 \/ !rhs1)
63                cnf.add_clause(&Clause::new(&[!and_output, and_input_0]));
64                cnf.add_clause(&Clause::new(&[!and_output, and_input_1]));
65                cnf.add_clause(&Clause::new(&[and_output, !and_input_0, !and_input_1]));
66            }
67        }
68
69        cnf
70    }
71
72    fn create_initial_cnf(aig: &AndInverterGraph) -> Cube {
73        let mut cube_literals = Vec::<Literal>::new();
74
75        let latch_info = aig.get_latch_information();
76        for (latch_literal, _, latch_reset) in latch_info {
77            // if latch is initialized
78            if latch_reset != latch_literal {
79                let lit = Self::get_literal_from_aig_wire(latch_literal);
80                if latch_reset == AIGWire::new(0) {
81                    cube_literals.push(!lit);
82                } else if latch_reset == AIGWire::new(1) {
83                    cube_literals.push(lit);
84                } else {
85                    unreachable!();
86                }
87            }
88        }
89
90        Cube::new(&cube_literals)
91    }
92
93    fn get_wires_that_feed_into_latches(aig: &AndInverterGraph) -> Vec<AIGWire> {
94        let mut wires_we_care_about = Vec::new();
95        let latch_info = aig.get_latch_information();
96        for (_, latch_input, _) in latch_info {
97            wires_we_care_about.push(latch_input);
98        }
99        wires_we_care_about
100    }
101
102    fn get_wire_mappings_from_latch_to_latch_input(
103        aig: &AndInverterGraph,
104    ) -> HashMap<AIGWire, AIGWire> {
105        let mut wires_we_care_about = HashMap::new();
106        let latch_info = aig.get_latch_information();
107        for (latch_output, latch_input, _) in latch_info {
108            wires_we_care_about.insert(latch_output, latch_input);
109        }
110        wires_we_care_about
111    }
112
113    fn create_transition_cnf(aig: &AndInverterGraph, max_variable_number: VariableType) -> CNF {
114        // propagate new latch values
115        let mut latches_to_wires = CNF::new();
116
117        let latch_info = aig.get_latch_information();
118        // encode latch updates into formula
119        for (latch_literal, latch_input, _) in latch_info {
120            // debug_assert_eq!(latch_literal % 2, 0);
121            let latch_lit_before = Self::get_literal_from_aig_wire(latch_literal);
122            let latch_lit_after = Literal::new(latch_lit_before.get_number() + max_variable_number)
123                .negate_if_true(latch_lit_before.is_negated());
124
125            if latch_input == AIGWire::new(0) {
126                latches_to_wires.add_clause(&Clause::new(&[!latch_lit_after]));
127            } else if latch_input == AIGWire::new(1) {
128                latches_to_wires.add_clause(&Clause::new(&[latch_lit_after]));
129            } else {
130                let latch_input_lit = Self::get_literal_from_aig_wire(latch_input);
131
132                // latch_lit = latch_input_lit <=> (latch_lit -> latch_input_lit) ^ (latch_lit <- latch_input_lit)
133                // <=> (!latch_lit \/ latch_input_lit) ^ (latch_lit \/ !latch_input_lit)
134
135                latches_to_wires.add_clause(&Clause::new(&[!latch_lit_after, latch_input_lit]));
136                latches_to_wires.add_clause(&Clause::new(&[latch_lit_after, !latch_input_lit]));
137            }
138        }
139
140        latches_to_wires.append(
141            &Self::get_cnf_that_describes_wire_values_as_a_function_of_latch_values_for_specific_wires(
142                aig,
143                &Self::get_wires_that_feed_into_latches(aig),
144            )
145        );
146        latches_to_wires
147    }
148
149    fn get_bad_wires(aig: &AndInverterGraph, assume_output_is_bad: bool) -> Vec<AIGWire> {
150        let mut important_wires = Vec::new();
151        important_wires.append(&mut aig.get_bad_information());
152
153        // this should be empty because constrained problem are not supported as of now.
154        important_wires.append(&mut aig.get_constraints_information());
155
156        // this is here because sometimes we consider output to be bad
157        if assume_output_is_bad {
158            important_wires.append(&mut aig.get_output_information());
159        }
160        important_wires
161    }
162
163    fn create_state_to_safety_translation(
164        aig: &AndInverterGraph,
165        assume_output_is_bad: bool,
166    ) -> CNF {
167        let important_wires = Self::get_bad_wires(aig, assume_output_is_bad);
168
169        Self::get_cnf_that_describes_wire_values_as_a_function_of_latch_values_for_specific_wires(
170            aig,
171            &important_wires,
172        )
173    }
174
175    fn create_unsafety_property(aig: &AndInverterGraph, assume_output_is_bad: bool) -> Clause {
176        // take all bad into consideration
177        let mut bad_info = aig.get_bad_information();
178        if assume_output_is_bad {
179            bad_info.append(&mut aig.get_output_information());
180        }
181
182        // split to 2 cases, depending on if empty or not.
183        if !bad_info.is_empty() {
184            let mut unsafe_literals = Vec::new();
185            for bad_literal in bad_info {
186                let b_lit = Self::get_literal_from_aig_wire(bad_literal);
187                unsafe_literals.push(b_lit);
188            }
189            Clause::new(&unsafe_literals)
190        } else {
191            // the empty clause is un-sat when turned into cnf
192            let result = Clause::new(&[]);
193            debug_assert!(
194                VarisatSolver::default().solve_cnf(&result.to_cnf()) == SatResponse::UnSat
195            );
196            // debug_assert!(VarisatSolver::default().solve_cnf(&(!result.to_owned()).to_cnf()) == SatResponse::Sat { assignment: Assignment::from_dimacs_assignment });
197            // let p = (!result).to_cnf();
198            result
199        }
200    }
201
202    fn create_input_and_state_literal_numbers(
203        aig: &AndInverterGraph,
204    ) -> (Vec<VariableType>, Vec<VariableType>) {
205        let mut input_literals = Vec::new();
206        for input_literal in aig.get_input_information() {
207            let lit = Self::get_literal_from_aig_wire(input_literal);
208            assert!(!lit.is_negated());
209            input_literals.push(lit.get_number());
210        }
211
212        let mut state_literals = Vec::new();
213        for (latch_literal, _, _) in aig.get_latch_information() {
214            let lit = Self::get_literal_from_aig_wire(latch_literal);
215            assert!(!lit.is_negated());
216            state_literals.push(lit.get_number());
217        }
218        (input_literals, state_literals)
219    }
220
221    // ********************************************************************************************
222    // aig api functions
223    // ********************************************************************************************
224
225    /// Function that converts an AndInverterGraph into a FiniteStateTransitionSystem.
226    ///
227    /// # Arguments
228    ///
229    /// * `aig: &AndInverterGraph` - the AndInverterGraph desired.
230    ///
231    /// # Examples
232    /// ```
233    /// use rust_formal_verification::models::{AndInverterGraph, FiniteStateTransitionSystem};
234    /// let file_path = "tests/examples/ours/counter.aig";
235    /// let aig = AndInverterGraph::from_aig_path(file_path);
236    /// let fsts = FiniteStateTransitionSystem::from_aig(&aig, false);
237    /// assert_eq!(fsts.get_initial_relation().to_string(), "p cnf 3 3\n-1 0\n-2 0\n-3 0");
238    /// ```
239    pub fn from_aig(aig: &AndInverterGraph, assume_output_is_bad: bool) -> Self {
240        // perform some checks first
241        let max_wire_in_aig = aig.get_highest_non_negated_wire();
242        assert!(
243            max_wire_in_aig < AIGWire::new((u32::MAX).try_into().unwrap()),
244            "AIG has variables with numbers that are too high (too many variables)."
245        );
246        assert!(
247            aig.get_constraints_information().is_empty(),
248            "Making 'FiniteStateTransitionSystem' from aig with constraints is not supported.\nTry folding the AIG with another tool First"
249        );
250
251        // make formulas
252        let max_literal_number: VariableType = max_wire_in_aig.get_literal().get_number();
253        let (input_literals, state_literals) = Self::create_input_and_state_literal_numbers(aig);
254        let initial_states: Cube = Self::create_initial_cnf(aig);
255        let transition: CNF = Self::create_transition_cnf(aig, max_literal_number);
256        let state_to_safety_translation: CNF =
257            Self::create_state_to_safety_translation(aig, assume_output_is_bad);
258        let unsafety_property: Clause = Self::create_unsafety_property(aig, assume_output_is_bad);
259        let initial_literals = initial_states.iter().map(|l| l.to_owned()).collect();
260
261        let cone_of_safety = get_all_variable_numbers_in_cnf(&state_to_safety_translation);
262        let cone_of_transition = get_all_variable_numbers_in_cnf(&transition);
263
264        let cone_of_safety_only_latches: HashSet<VariableType> = cone_of_safety
265            .iter()
266            .filter(|v| state_literals.contains(v))
267            .map(|v| v.to_owned())
268            .collect();
269        let cone_of_transition_only_latches: HashSet<VariableType> = cone_of_transition
270            .iter()
271            .filter(|v| state_literals.contains(v))
272            .map(|v| v.to_owned())
273            .collect();
274
275        let bad_wires = Self::get_bad_wires(aig, assume_output_is_bad);
276        let wires_that_feed_into_latches = Self::get_wires_that_feed_into_latches(aig);
277
278        // get cone of bad
279        let mut and_information_in_cone_of_bad: Vec<(AIGWire, AIGWire, AIGWire)> = aig
280            .get_and_information_in_cone_of_influence(&bad_wires)
281            .into_iter()
282            .collect();
283
284        // sort by output
285        and_information_in_cone_of_bad
286            .sort_by(|first_and, second_and| first_and.0.cmp(&second_and.0));
287
288        // get cone of transition
289        let mut and_information_in_cone_of_transition: Vec<(AIGWire, AIGWire, AIGWire)> = aig
290            .get_and_information_in_cone_of_influence(&wires_that_feed_into_latches)
291            .into_iter()
292            .collect();
293
294        // sort by output
295        and_information_in_cone_of_transition
296            .sort_by(|first_and, second_and| first_and.0.cmp(&second_and.0));
297
298        // create object
299        Self {
300            initial_literals,
301            initial_states,
302            transition,
303            state_to_safety_translation,
304            unsafety_property,
305            max_literal_number,
306            state_literals,
307            input_literals,
308            // cone_of_safety,
309            // cone_of_transition,
310            cone_of_safety_only_latches,
311            cone_of_transition_only_latches,
312            wire_mappings_from_latch_to_latch_input:
313                Self::get_wire_mappings_from_latch_to_latch_input(aig),
314            bad_wires,
315            and_information_in_cone_of_bad_sorted_by_output: and_information_in_cone_of_bad,
316            and_information_in_cone_of_transition_sorted_by_output:
317                and_information_in_cone_of_transition,
318        }
319    }
320}
rust_formal_verification/models/finite_state_transition_system/construction.rs

rust_formal_verification/models/finite_state_transition_system/
construction.rs
