Skip to content

Commit

Permalink
start btor2 serialization testing
Browse files Browse the repository at this point in the history
  • Loading branch information
ekiwi committed Nov 14, 2023
1 parent 47cce29 commit 840fc74
Show file tree
Hide file tree
Showing 4 changed files with 29 additions and 3 deletions.
7 changes: 4 additions & 3 deletions src/btor2/serialize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,11 @@
// author: Kevin Laeufer <[email protected]>

use crate::ir::*;
use std::io::Write;

pub fn serialize(
ctx: &Context,
writer: &mut impl (std::io::Write),
writer: &mut impl Write,
sys: &TransitionSystem,
) -> std::io::Result<()> {
Serializer::new(ctx, writer).serialize_sys(sys)
Expand All @@ -20,12 +21,12 @@ pub fn serialize_to_str(ctx: &Context, sys: &TransitionSystem) -> String {
String::from_utf8(buf).expect("Failed to read string we wrote!")
}

struct Serializer<'a, W: std::io::Write> {
struct Serializer<'a, W: Write> {
ctx: &'a Context,
writer: &'a mut W,
}

impl<'a, W: std::io::Write> Serializer<'a, W> {
impl<'a, W: Write> Serializer<'a, W> {
fn new(ctx: &'a Context, writer: &'a mut W) -> Self {
Serializer { ctx, writer }
}
Expand Down
13 changes: 13 additions & 0 deletions tests/btor2_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,22 @@ fn parse_count2() {
insta::assert_snapshot!(sys.serialize_to_str(&ctx));
}

#[test]
fn serialize_count2() {
let mut ctx = Context::default();
let sys = btor2::parse_str(&mut ctx, COUNT_2, Some("count2")).unwrap();
insta::assert_snapshot!(btor2::serialize_to_str(&ctx, &sys));
}


#[test]
fn parse_quiz1() {
let (ctx, sys) = btor2::parse_file("inputs/Quiz1.btor").unwrap();
insta::assert_snapshot!(sys.serialize_to_str(&ctx));
}

#[test]
fn serialize_quiz1() {
let (ctx, sys) = btor2::parse_file("inputs/Quiz1.btor").unwrap();
insta::assert_snapshot!(btor2::serialize_to_str(&ctx, &sys));
}
6 changes: 6 additions & 0 deletions tests/snapshots/btor2_test__serialize_count2.snap
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
---
source: tests/btor2_test.rs
expression: "btor2::serialize_to_str(&ctx, &sys)"
---
; btor2 description of `count2` generated by patron 0.2.0

6 changes: 6 additions & 0 deletions tests/snapshots/btor2_test__serialize_quiz1.snap
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
---
source: tests/btor2_test.rs
expression: "btor2::serialize_to_str(&ctx, &sys)"
---
; btor2 description of `Quiz1` generated by patron 0.2.0

0 comments on commit 840fc74

Please sign in to comment.