flussab_btor2/
btor2.rs

1//! Types for representing BTOR2.
2use std::{io::Write, mem::take, num::NonZeroU64};
3
4use bstr::BStr;
5use flussab::DeferredWriter;
6
7/// A single non-empty line of a BTOR2 file.
8#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
9pub enum Line<'a> {
10    /// A comment line.
11    Comment(&'a BStr),
12    /// A BTOR2 node.
13    Node(Node<'a>),
14}
15
16impl<'a> Line<'a> {
17    pub(crate) fn has_comment(&self) -> bool {
18        match self {
19            Line::Comment(_) => true,
20            Line::Node(node) => node.comment.is_some(),
21        }
22    }
23
24    pub(crate) fn update_comment(&mut self, comment: &'a BStr) {
25        match self {
26            Line::Comment(line_comment) => *line_comment = comment,
27            Line::Node(node) => node.comment = Some(comment),
28        }
29    }
30
31    pub(crate) fn update_bufs(&mut self, constant: &'a str, symbol: &'a BStr, nodes: &'a [NodeId]) {
32        if let Line::Node(node) = self {
33            if let Some(node_symbol) = &mut node.symbol {
34                *node_symbol = symbol
35            }
36            match &mut node.variant {
37                NodeVariant::Value(Value {
38                    variant:
39                        ValueVariant::Const(
40                            Const::Binary(BinaryConst(value_constant))
41                            | Const::Hex(HexConst(value_constant))
42                            | Const::Decimal(DecimalConst(value_constant)),
43                        ),
44                    ..
45                }) => *value_constant = constant,
46                NodeVariant::Output(Output::Justice(conditions)) => {
47                    *conditions = nodes;
48                }
49                _ => (),
50            }
51        }
52    }
53}
54
55/// Refers to a BTOR2 node.
56///
57/// Note that this is used for sort nodes, value nodes, state updates nodes and output nodes as they
58/// share a single id space in BTOR2.
59#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
60pub struct NodeId(pub NonZeroU64);
61
62impl NodeId {
63    /// Returns the node with the given id.
64    ///
65    /// This panics when the id is zero.
66    pub fn new(id: u64) -> Self {
67        Self(NonZeroU64::new(id).unwrap())
68    }
69}
70
71/// A BTOR2 node.
72#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
73pub struct Node<'a> {
74    /// The node id of this node.
75    pub id: NodeId,
76    /// The definition of this node.
77    pub variant: NodeVariant<'a>,
78    /// An optional name for this node.
79    pub symbol: Option<&'a BStr>,
80    /// An optional comment following the node definition.
81    pub comment: Option<&'a BStr>,
82}
83
84/// The definition of a BTOR2 node.
85#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
86pub enum NodeVariant<'a> {
87    /// The definition of a sort.
88    Sort(Sort),
89    /// The definition of a value.
90    Value(Value<'a>),
91    /// The definition of a state assignment.
92    Assignment(Assignment),
93    /// The definition of an output.
94    Output(Output<'a>),
95}
96
97/// A BTOR2 sort.
98#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
99pub enum Sort {
100    /// A bit-vector sort of a given positive width.
101    BitVec(NonZeroU64),
102    /// An array sort with a given domain and codomain.
103    Array(Array),
104}
105
106impl Sort {
107    /// Returns a bit-vector sort of the given width.
108    ///
109    /// Panics when the given width is zero.
110    pub fn bit_vec(width: u64) -> Self {
111        Self::BitVec(NonZeroU64::new(width).unwrap())
112    }
113}
114
115/// An array sort with a given domain and codomain.
116#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
117pub struct Array(pub NodeId, pub NodeId);
118
119/// A BTOR2 Value with of a known sort.
120#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
121pub struct Value<'a> {
122    /// The sort of the value.
123    pub sort: NodeId,
124    /// The definition of the value.
125    pub variant: ValueVariant<'a>,
126}
127
128/// A BTOR2 Value.
129#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
130pub enum ValueVariant<'a> {
131    /// A constant value.
132    Const(Const<'a>),
133    /// An input value.
134    Input,
135    /// A state value.
136    State,
137    /// A value defined by an operation.
138    Op(Op),
139}
140
141/// A value defined by an operation.
142#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
143pub enum Op {
144    /// A value resulting from applying an unary operation to a previously defined value.
145    Unary(UnaryOp, NodeId),
146    /// A value resulting from applying a binary operation to two previously defined values.
147    Binary(BinaryOp, [NodeId; 2]),
148    /// A value resulting from applying a ternary operation to three previously defined values.
149    Ternary(TernaryOp, [NodeId; 3]),
150}
151
152/// A unary BTOR2 operation.
153#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
154pub enum UnaryOp {
155    /// Unsigned width extension.
156    Uext(u64),
157    /// Signed width extension.
158    Sext(u64),
159    /// Bit-vector slicing.
160    Slice(u64, u64),
161    /// Bitwise negation.
162    Not,
163    /// Addition of constant 1.
164    Inc,
165    /// Subtraction of constant 1.
166    Dec,
167    /// Arithmetic negation.
168    Neg,
169    /// And-reduction.
170    Redand,
171    /// Or-reduction.
172    Redor,
173    /// Xor-reduction.
174    Redxor,
175}
176
177/// A binary BTOR2 operation.
178#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
179pub enum BinaryOp {
180    /// Boolean biimplication.
181    Iff,
182    /// Boolean implicaqtion.
183    Implies,
184    /// Equality.
185    Eq,
186    /// Inequality.
187    Neq,
188    /// Unsigned greater-than comparison.
189    Ugt,
190    /// Signed greater-than comparison.
191    Sgt,
192    /// Unsigned greater-than-or-equal-to comparison.
193    Ugte,
194    /// Signed greater-than-or-equal-to comparison.
195    Sgte,
196    /// Unsigned less-than comparison.
197    Ult,
198    /// Signed less-than comparison.
199    Slt,
200    /// Unsigned less-than-or-equal-to comparison.
201    Ulte,
202    /// Signed less-than-or-equal-to comparison.
203    Slte,
204    /// Bit-wise and.
205    And,
206    /// Bit-wise not-and.
207    Nand,
208    /// Bit-wise not-or.
209    Nor,
210    /// Bit-wise or.
211    Or,
212    /// Bit-wise not-xor.
213    Xnor,
214    /// Bit-wise xor.
215    Xor,
216    /// Left rotation.
217    Rol,
218    /// right rotation.
219    Ror,
220    /// Left shift.
221    Sll,
222    /// Arithmetic right shift.
223    Sra,
224    /// Logical right shift.
225    Srl,
226    /// Addition.
227    Add,
228    /// Multiplication.
229    Mul,
230    /// Unsigned division.
231    Udiv,
232    /// Signed division.
233    Sdiv,
234    /// Signed modulo.
235    Smod,
236    /// Unsigned remainder.
237    Urem,
238    /// Signed remainder.
239    Srem,
240    /// Subtraction.
241    Sub,
242    /// Overflow check for unsigned addition.
243    Uaddo,
244    /// Overflow check for signed addition.
245    Saddo,
246    /// Overflow check for signed division.
247    Sdivo,
248    /// Overflow check for unsigned multiplication.
249    Umulo,
250    /// Overflow check for signed multiplication.
251    Smulo,
252    /// Overflow check for unsigned subtraction.
253    Usubo,
254    /// Overflow check for signed subtraction.
255    Ssubo,
256    /// Bit-vector concatenation.
257    Concat,
258    /// Array lookup.
259    Read,
260}
261
262/// A ternary BTOR2 operation.
263#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
264pub enum TernaryOp {
265    /// If-then-else.
266    Ite,
267    /// Array update.
268    Write,
269}
270
271/// A BTOR2 constant.
272#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
273pub enum Const<'a> {
274    /// A constant represented in binary.
275    Binary(BinaryConst<'a>),
276    /// A constant represented in decimal.
277    Decimal(DecimalConst<'a>),
278    /// A constant represented in hexadecimal.
279    Hex(HexConst<'a>),
280    /// Constant one.
281    One,
282    /// Constant negative one, an all-ones bit-vector.
283    Ones,
284    /// Constant zero.
285    Zero,
286}
287
288/// Error of a string to bit-vector constant representation conversion.
289#[derive(Debug)]
290pub enum InvalidConstError {
291    /// The string contains a character that is not a valid digit for the target representation.
292    InvalidDigit(char),
293    /// The string is empty.
294    Empty,
295}
296
297/// A string of binary digits.
298#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
299pub struct BinaryConst<'a>(pub(crate) &'a str);
300
301impl std::fmt::Display for BinaryConst<'_> {
302    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
303        std::fmt::Display::fmt(&self.0, f)
304    }
305}
306
307impl<'a> TryFrom<&'a str> for BinaryConst<'a> {
308    type Error = InvalidConstError;
309
310    fn try_from(value: &'a str) -> Result<Self, Self::Error> {
311        if value.is_empty() {
312            return Err(InvalidConstError::Empty);
313        }
314        for c in value.chars() {
315            if !matches!(c, '0' | '1') {
316                return Err(InvalidConstError::InvalidDigit(c));
317            }
318        }
319        Ok(BinaryConst(value))
320    }
321}
322
323/// A string of hex digits.
324///
325/// This can contain lowercase and uppercase digits
326#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
327pub struct HexConst<'a>(pub(crate) &'a str);
328
329impl std::fmt::Display for HexConst<'_> {
330    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
331        std::fmt::Display::fmt(&self.0, f)
332    }
333}
334
335impl<'a> TryFrom<&'a str> for HexConst<'a> {
336    type Error = InvalidConstError;
337
338    fn try_from(value: &'a str) -> Result<Self, Self::Error> {
339        if value.is_empty() {
340            return Err(InvalidConstError::Empty);
341        }
342        for c in value.chars() {
343            if !c.is_ascii_hexdigit() {
344                return Err(InvalidConstError::InvalidDigit(c));
345            }
346        }
347        Ok(HexConst(value))
348    }
349}
350
351/// A string of decimal digits, optionally prefixed with a minus sign.
352#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
353pub struct DecimalConst<'a>(pub(crate) &'a str);
354
355impl std::fmt::Display for DecimalConst<'_> {
356    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
357        std::fmt::Display::fmt(&self.0, f)
358    }
359}
360
361impl<'a> TryFrom<&'a str> for DecimalConst<'a> {
362    type Error = InvalidConstError;
363
364    fn try_from(value: &'a str) -> Result<Self, Self::Error> {
365        if value.is_empty() {
366            return Err(InvalidConstError::Empty);
367        }
368        let mut first = true;
369        for c in value.chars() {
370            if !(take(&mut first) && c == '-' || c.is_ascii_hexdigit()) {
371                return Err(InvalidConstError::InvalidDigit(c));
372            }
373        }
374        Ok(DecimalConst(value))
375    }
376}
377
378/// Whether a state assignment is the initial assignment or the state update.
379#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
380pub enum AssignmentKind {
381    /// The assignment assigns an initial state value.
382    Init,
383    /// The assignment assigns the next state value.
384    Next,
385}
386
387/// A BTOR2 state assignemnt.
388#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
389pub struct Assignment {
390    /// The state to assign to.
391    pub state: NodeId,
392    /// The common sort of the state and assigned value.
393    pub sort: NodeId,
394    /// When to perform the assignment.
395    pub kind: AssignmentKind,
396    /// The value to assign.
397    pub value: NodeId,
398}
399
400/// A BTOR2 output.
401#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
402pub enum Output<'a> {
403    /// An output consisting of a single value.
404    SingleValue(SingleValueOutput),
405    /// An output representing a negated liveness property.
406    Justice(&'a [NodeId]),
407}
408
409/// The meaning of a single value output.
410#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
411pub enum SingleValueOutputKind {
412    /// A ciruit output.
413    Output,
414    /// An output representing a bad state property.
415    Bad,
416    /// An output representing an invariant constraint.
417    Constraint,
418    /// An output representing a fairness constraint.
419    Fair,
420}
421
422/// A BTOR2 output consisting of a single value.
423#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
424pub struct SingleValueOutput {
425    /// The meaning of this output.
426    pub kind: SingleValueOutputKind,
427    /// The value to output.
428    pub value: NodeId,
429}
430
431impl std::fmt::Display for Line<'_> {
432    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
433        let mut target = vec![];
434        {
435            let mut writer = DeferredWriter::from_write(&mut target);
436            self.write_into_unterminated(&mut writer);
437            writer.flush().unwrap();
438        }
439        std::fmt::Display::fmt(&String::from_utf8_lossy(&target), f)
440    }
441}
442
443impl Line<'_> {
444    /// Writes the BTOR2 line into a [`DeferredWriter`], includes the terminating newline.
445    pub fn write_into(&self, target: &mut DeferredWriter) {
446        self.write_into_unterminated(target);
447        target.write_all_defer_err(b"\n");
448    }
449
450    /// Writes the BTOR2 line into a [`DeferredWriter`], omits the terminating newline.
451    pub fn write_into_unterminated(&self, target: &mut DeferredWriter) {
452        match self {
453            Line::Comment(comment) => {
454                target.write_all_defer_err(b";");
455                target.write_all_defer_err(comment);
456            }
457            Line::Node(node) => {
458                node.write_into(target);
459            }
460        }
461    }
462}
463
464impl NodeId {
465    fn write_into(&self, target: &mut DeferredWriter) {
466        flussab::write::text::ascii_digits(target, self.0.get());
467    }
468}
469
470impl Node<'_> {
471    fn write_into(&self, target: &mut DeferredWriter) {
472        self.id.write_into(target);
473        target.write_all_defer_err(b" ");
474        self.variant.write_into(target);
475        if let Some(symbol) = self.symbol {
476            target.write_all_defer_err(b" ");
477            target.write_all_defer_err(symbol);
478        }
479        if let Some(comment) = self.comment {
480            target.write_all_defer_err(b" ;");
481            target.write_all_defer_err(comment);
482        }
483    }
484}
485
486impl NodeVariant<'_> {
487    fn write_into(&self, target: &mut DeferredWriter) {
488        match self {
489            NodeVariant::Sort(sort) => {
490                sort.write_into(target);
491            }
492            NodeVariant::Value(value) => {
493                value.write_into(target);
494            }
495            NodeVariant::Assignment(assignment) => {
496                assignment.write_into(target);
497            }
498            NodeVariant::Output(output) => {
499                output.write_into(target);
500            }
501        }
502    }
503}
504
505impl Sort {
506    fn write_into(&self, target: &mut DeferredWriter) {
507        match *self {
508            Sort::BitVec(width) => {
509                target.write_all_defer_err(b"sort bitvec ");
510                flussab::write::text::ascii_digits(target, width.get());
511            }
512            Sort::Array(Array(domain, codomain)) => {
513                target.write_all_defer_err(b"sort array ");
514                domain.write_into(target);
515                target.write_all_defer_err(b" ");
516                codomain.write_into(target);
517            }
518        }
519    }
520}
521
522impl Value<'_> {
523    fn write_into(&self, target: &mut DeferredWriter) {
524        match &self.variant {
525            ValueVariant::Const(Const::Binary(const_value)) => {
526                target.write_all_defer_err(b"const ");
527                self.sort.write_into(target);
528                target.write_all_defer_err(b" ");
529                target.write_all_defer_err(const_value.0.as_bytes());
530            }
531            ValueVariant::Const(Const::Hex(const_value)) => {
532                target.write_all_defer_err(b"consth ");
533                self.sort.write_into(target);
534                target.write_all_defer_err(b" ");
535                target.write_all_defer_err(const_value.0.as_bytes());
536            }
537            ValueVariant::Const(Const::Decimal(const_value)) => {
538                target.write_all_defer_err(b"constd ");
539                self.sort.write_into(target);
540                target.write_all_defer_err(b" ");
541                target.write_all_defer_err(const_value.0.as_bytes());
542            }
543            ValueVariant::Const(Const::One) => {
544                target.write_all_defer_err(b"one ");
545                self.sort.write_into(target);
546            }
547            ValueVariant::Const(Const::Ones) => {
548                target.write_all_defer_err(b"ones ");
549                self.sort.write_into(target);
550            }
551            ValueVariant::Const(Const::Zero) => {
552                target.write_all_defer_err(b"zero ");
553                self.sort.write_into(target);
554            }
555            ValueVariant::Input => {
556                target.write_all_defer_err(b"input ");
557                self.sort.write_into(target);
558            }
559            ValueVariant::State => {
560                target.write_all_defer_err(b"state ");
561                self.sort.write_into(target);
562            }
563            &ValueVariant::Op(Op::Unary(op, a0)) => {
564                target.write_all_defer_err(op.name().as_bytes());
565                target.write_all_defer_err(b" ");
566                self.sort.write_into(target);
567                target.write_all_defer_err(b" ");
568                a0.write_into(target);
569                op.write_indices_into(target);
570            }
571            &ValueVariant::Op(Op::Binary(op, [a0, a1])) => {
572                target.write_all_defer_err(op.name().as_bytes());
573                target.write_all_defer_err(b" ");
574                self.sort.write_into(target);
575                target.write_all_defer_err(b" ");
576                a0.write_into(target);
577                target.write_all_defer_err(b" ");
578                a1.write_into(target);
579            }
580            &ValueVariant::Op(Op::Ternary(op, [a0, a1, a2])) => {
581                target.write_all_defer_err(op.name().as_bytes());
582                target.write_all_defer_err(b" ");
583                self.sort.write_into(target);
584                target.write_all_defer_err(b" ");
585                a0.write_into(target);
586                target.write_all_defer_err(b" ");
587                a1.write_into(target);
588                target.write_all_defer_err(b" ");
589                a2.write_into(target);
590            }
591        }
592    }
593}
594
595impl UnaryOp {
596    fn name(&self) -> &'static str {
597        match self {
598            UnaryOp::Uext(_) => "uext",
599            UnaryOp::Sext(_) => "sext",
600            UnaryOp::Slice(_, _) => "slice",
601            UnaryOp::Not => "not",
602            UnaryOp::Inc => "inc",
603            UnaryOp::Dec => "dec",
604            UnaryOp::Neg => "neg",
605            UnaryOp::Redand => "redand",
606            UnaryOp::Redor => "redor",
607            UnaryOp::Redxor => "redxor",
608        }
609    }
610
611    fn write_indices_into(&self, target: &mut DeferredWriter) {
612        match self {
613            &UnaryOp::Uext(width) | &UnaryOp::Sext(width) => {
614                target.write_all_defer_err(b" ");
615                flussab::write::text::ascii_digits(target, width);
616            }
617            &UnaryOp::Slice(upper, lower) => {
618                target.write_all_defer_err(b" ");
619                flussab::write::text::ascii_digits(target, upper);
620                target.write_all_defer_err(b" ");
621                flussab::write::text::ascii_digits(target, lower);
622            }
623            _ => (),
624        }
625    }
626}
627
628impl BinaryOp {
629    fn name(&self) -> &'static str {
630        match self {
631            BinaryOp::Iff => "iff",
632            BinaryOp::Implies => "implies",
633            BinaryOp::Eq => "eq",
634            BinaryOp::Neq => "neq",
635            BinaryOp::Ugt => "ugt",
636            BinaryOp::Sgt => "sgt",
637            BinaryOp::Ugte => "ugte",
638            BinaryOp::Sgte => "sgte",
639            BinaryOp::Ult => "ult",
640            BinaryOp::Slt => "slt",
641            BinaryOp::Ulte => "ulte",
642            BinaryOp::Slte => "slte",
643            BinaryOp::And => "and",
644            BinaryOp::Nand => "nand",
645            BinaryOp::Nor => "nor",
646            BinaryOp::Or => "or",
647            BinaryOp::Xnor => "xnor",
648            BinaryOp::Xor => "xor",
649            BinaryOp::Rol => "rol",
650            BinaryOp::Ror => "ror",
651            BinaryOp::Sll => "sll",
652            BinaryOp::Sra => "sra",
653            BinaryOp::Srl => "srl",
654            BinaryOp::Add => "add",
655            BinaryOp::Mul => "mul",
656            BinaryOp::Udiv => "udiv",
657            BinaryOp::Sdiv => "sdiv",
658            BinaryOp::Smod => "smod",
659            BinaryOp::Urem => "urem",
660            BinaryOp::Srem => "srem",
661            BinaryOp::Sub => "sub",
662            BinaryOp::Uaddo => "uaddo",
663            BinaryOp::Saddo => "saddo",
664            BinaryOp::Sdivo => "sdivo",
665            BinaryOp::Umulo => "umulo",
666            BinaryOp::Smulo => "smulo",
667            BinaryOp::Usubo => "usubo",
668            BinaryOp::Ssubo => "ssubo",
669            BinaryOp::Concat => "concat",
670            BinaryOp::Read => "read",
671        }
672    }
673}
674
675impl TernaryOp {
676    fn name(&self) -> &'static str {
677        match self {
678            TernaryOp::Ite => "ite",
679            TernaryOp::Write => "write",
680        }
681    }
682}
683
684impl Assignment {
685    fn write_into(&self, target: &mut DeferredWriter) {
686        match self.kind {
687            AssignmentKind::Init => target.write_all_defer_err(b"init "),
688            AssignmentKind::Next => target.write_all_defer_err(b"next "),
689        }
690        self.sort.write_into(target);
691        target.write_all_defer_err(b" ");
692        self.state.write_into(target);
693        target.write_all_defer_err(b" ");
694        self.value.write_into(target);
695    }
696}
697
698impl Output<'_> {
699    fn write_into(&self, target: &mut DeferredWriter) {
700        match self {
701            Output::SingleValue(simple) => simple.write_into(target),
702            &Output::Justice(nodes) => {
703                target.write_all_defer_err(b"justice ");
704                flussab::write::text::ascii_digits(target, nodes.len());
705                for node in nodes {
706                    target.write_all_defer_err(b" ");
707                    node.write_into(target);
708                }
709            }
710        }
711    }
712}
713
714impl SingleValueOutput {
715    fn write_into(&self, target: &mut DeferredWriter) {
716        match self.kind {
717            SingleValueOutputKind::Output => target.write_all_defer_err(b"output "),
718            SingleValueOutputKind::Bad => target.write_all_defer_err(b"bad "),
719            SingleValueOutputKind::Constraint => target.write_all_defer_err(b"constraint "),
720            SingleValueOutputKind::Fair => target.write_all_defer_err(b"fair "),
721        }
722        self.value.write_into(target);
723    }
724}
flussab_btor2/btor2.rs

flussab_btor2/
btor2.rs
