fn test_assert_term()

in smt2parser/src/parser.rs [393:501]

• 102 lines of code
• 1 McCabe index (conditional complexity)

    fn test_assert_term() {
        let value = parse_tokens(Lexer::new(&b"(assert 12)"[..])).unwrap();
        assert_eq!(
            value,
            Command::Assert {
                term: Term::Constant(Constant::Numeral(num::BigUint::from(12u32))),
            }
        );

        let value = parse_tokens(Lexer::new(&b"(assert (as A B))"[..])).unwrap();
        assert_eq!(
            value,
            Command::Assert {
                term: Term::QualIdentifier(QualIdentifier::Sorted {
                    identifier: Identifier::Simple {
                        symbol: Symbol("A".into())
                    },
                    sort: Sort::Simple {
                        identifier: Identifier::Simple {
                            symbol: Symbol("B".into())
                        }
                    },
                })
            },
        );

        let value = parse_tokens(Lexer::new(&b"(assert (let ((x (f x 2))) (= x 3)))"[..])).unwrap();
        assert_eq!(
            value,
            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)))
                        ]
                    }),
                }
            }
        );

        let value = parse_tokens(Lexer::new(
            &b"(assert (forall ((x Bool) (y Int)) (f x y))\n ; dfg \n )"[..],
        ))
        .unwrap();
        assert!(matches!(
            value,
            Command::Assert {
                term: Term::Forall { .. }
            }
        ));

        let result = parse_tokens(Lexer::new(&b"(assert (forall () (f x y)))"[..]));
        assert!(result.is_err());

        let value = parse_tokens(Lexer::new(
            &b"(assert ( ;foo\n match 3 ( (x (+ x 2)) ) ))"[..],
        ))
        .unwrap();
        assert!(matches!(
            value,
            Command::Assert {
                term: Term::Match { .. }
            }
        ));

        let value = parse_tokens(Lexer::new(&b"(assert ( ! 3 :f 1 :g (a 3) ))"[..])).unwrap();
        assert!(matches!(
            value,
            Command::Assert {
                term: Term::Attributes { .. }
            }
        ));

        let value = parse_tokens(Lexer::new(&b"(assert ( f 1 2 3 ))"[..])).unwrap();
        assert!(matches!(
            value,
            Command::Assert {
                term: Term::Application { .. }
            }
        ));
    }