gateconvert 0.1.2

The library to convert Gate circuit from/to foreign logic format.
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

#![cfg_attr(docsrs, feature(doc_cfg))]
//! Module to conversion between Gate circuit and the BTOR2 logic format.

use crate::gatesim::*;

use std::collections::HashMap;
use std::io::{self, BufWriter, Write};

use crate::vcircuit::*;

/// Converts circuit to BTOR2 format.
///
/// Function writes Gate circuit logic in BTOR2 format to `out`. `circuit` is circuit
/// to convert. `state_len` is length of state.
///
/// The circuit inputs are organized in form: `[state,inputs]`.
/// The circuit outputs are organized in form: `[state,outputs]`.
pub fn to_btor2(circuit: Circuit<usize>, state_len: usize, out: impl Write) -> io::Result<()> {
    let input_len = circuit.input_len();
    let output_len = circuit.outputs().len();
    assert!(state_len <= input_len);
    assert!(state_len <= output_len);
    let circuit = VCircuit::to_op_and_ximpl_circuit(circuit, false);

    let mut out = BufWriter::new(out);
    out.write(b"1 sort bitvec 1\n")?;
    // write states
    for i in 0..state_len {
        writeln!(out, "{} state 1", i + 2)?;
    }
    for i in state_len..input_len {
        writeln!(out, "{} input 1", i + 2)?;
    }
    // write gates
    let gate_num = circuit.gates.len();
    for (i, g) in circuit.gates.iter().enumerate() {
        let op = match g.func {
            VGateFunc::And => "and",
            VGateFunc::Nand => "nand",
            VGateFunc::Or => "or",
            VGateFunc::Nor => "nor",
            VGateFunc::Impl => "implies",
            VGateFunc::Xor => "xor",
            _ => {
                panic!("Unsupported gate function");
            }
        };
        let index = input_len + 2 + i;
        writeln!(out, "{} {} 1 {} {}", index, op, g.i0 + 2, g.i1 + 2)?;
    }
    // to collect negations
    let mut neg_map = HashMap::new();
    // write nexts
    let mut index = input_len + 2 + gate_num;
    for (i, (o, n)) in circuit.outputs[0..state_len].iter().enumerate() {
        if *n {
            let neg = if let Some(neg_nid) = neg_map.get(o) {
                *neg_nid
            } else {
                writeln!(out, "{} not 1 {}", index, o + 2)?;
                neg_map.insert(*o, index);
                index += 1;
                neg_map[o]
            };
            writeln!(out, "{} next 1 {} {}", index, i + 2, neg)?;
        } else {
            writeln!(out, "{} next 1 {} {}", index, i + 2, o + 2)?;
        }
        index += 1;
    }
    // write outputs
    for (o, n) in &circuit.outputs[state_len..] {
        if *n {
            let neg = if let Some(neg_nid) = neg_map.get(o) {
                *neg_nid
            } else {
                writeln!(out, "{} not 1 {}", index, o + 2)?;
                neg_map.insert(*o, index);
                index += 1;
                neg_map[o]
            };
            writeln!(out, "{} output {}", index, neg)?;
        } else {
            writeln!(out, "{} output {}", index, o + 2)?;
        }
        index += 1;
    }
    Ok(())
}