in smt2parser/src/rewriter.rs [924:1044]
fn test_term_rewriter() {
use crate::concrete::*;
// (assert (let ((x (f x 2))) (= x 3)))
let command = Command::Assert {
term: Term::Let {
var_bindings: vec![(
Symbol("x".into()),
Term::Application {
qual_identifier: QualIdentifier::Simple {
identifier: Identifier::Simple {
symbol: Symbol("f".into()),
},
},
arguments: vec![
Term::QualIdentifier(QualIdentifier::Simple {
identifier: Identifier::Simple {
symbol: Symbol("x".into()),
},
}),
Term::Constant(Constant::Numeral(num::BigUint::from(2u32))),
],
},
)],
term: Box::new(Term::Application {
qual_identifier: QualIdentifier::Simple {
identifier: Identifier::Simple {
symbol: Symbol("=".into()),
},
},
arguments: vec![
Term::QualIdentifier(QualIdentifier::Simple {
identifier: Identifier::Simple {
symbol: Symbol("x".into()),
},
}),
Term::Constant(Constant::Numeral(num::BigUint::from(3u32))),
],
}),
},
};
#[derive(Default)]
struct Builder(crate::concrete::SyntaxBuilder);
impl Rewriter for Builder {
type V = crate::concrete::SyntaxBuilder;
type Error = crate::concrete::Error;
fn visitor(&mut self) -> &mut Self::V {
&mut self.0
}
fn process_symbol(&mut self, s: Symbol) -> Result<Symbol, Self::Error> {
Ok(Symbol(s.0 + "__"))
}
}
let mut builder = Builder::default();
let command2 = command.clone().accept(&mut builder).unwrap();
let command3 = Command::Assert {
term: Term::Let {
var_bindings: vec![(
Symbol("x__".into()),
Term::Application {
qual_identifier: QualIdentifier::Simple {
identifier: Identifier::Simple {
symbol: Symbol("f__".into()),
},
},
arguments: vec![
Term::QualIdentifier(QualIdentifier::Simple {
identifier: Identifier::Simple {
symbol: Symbol("x__".into()),
},
}),
Term::Constant(Constant::Numeral(num::BigUint::from(2u32))),
],
},
)],
term: Box::new(Term::Application {
qual_identifier: QualIdentifier::Simple {
identifier: Identifier::Simple {
symbol: Symbol("=__".into()),
},
},
arguments: vec![
Term::QualIdentifier(QualIdentifier::Simple {
identifier: Identifier::Simple {
symbol: Symbol("x__".into()),
},
}),
Term::Constant(Constant::Numeral(num::BigUint::from(3u32))),
],
}),
},
};
assert_eq!(command2, command3);
#[derive(Default)]
struct Builder2(crate::concrete::SyntaxBuilder);
impl Rewriter for Builder2 {
type V = crate::concrete::SyntaxBuilder;
type Error = crate::concrete::Error;
fn visitor(&mut self) -> &mut Self::V {
&mut self.0
}
fn visit_assert(&mut self, _: Term) -> Result<Command, Self::Error> {
Ok(Command::Exit)
}
}
let mut builder = Builder2::default();
let command2 = command.accept(&mut builder).unwrap();
let command3 = Command::Exit;
assert_eq!(command2, command3);
}