fn visit_assert()

in smt2parser/src/visitors.rs [347:486]


    fn visit_assert(&mut self, term: Term) -> Result<Self::T, Self::E>;

    fn visit_check_sat(&mut self) -> Result<Self::T, Self::E>;

    fn visit_check_sat_assuming(
        &mut self,
        literals: Vec<(Symbol, bool)>,
    ) -> Result<Self::T, Self::E>;

    fn visit_declare_const(&mut self, symbol: Symbol, sort: Sort) -> Result<Self::T, Self::E>;

    fn visit_declare_datatype(
        &mut self,
        symbol: Symbol,
        datatype: DatatypeDec<Symbol, Sort>,
    ) -> Result<Self::T, Self::E>;

    fn visit_declare_datatypes(
        &mut self,
        datatypes: Vec<(Symbol, Numeral, DatatypeDec<Symbol, Sort>)>,
    ) -> Result<Self::T, Self::E>;

    fn visit_declare_fun(
        &mut self,
        symbol: Symbol,
        parameters: Vec<Sort>,
        sort: Sort,
    ) -> Result<Self::T, Self::E>;

    fn visit_declare_sort(&mut self, symbol: Symbol, arity: Numeral) -> Result<Self::T, Self::E>;

    fn visit_define_fun(
        &mut self,
        sig: FunctionDec<Symbol, Sort>,
        term: Term,
    ) -> Result<Self::T, Self::E>;

    fn visit_define_fun_rec(
        &mut self,
        sig: FunctionDec<Symbol, Sort>,
        term: Term,
    ) -> Result<Self::T, Self::E>;

    fn visit_define_funs_rec(
        &mut self,
        funs: Vec<(FunctionDec<Symbol, Sort>, Term)>,
    ) -> Result<Self::T, Self::E>;

    fn visit_define_sort(
        &mut self,
        symbol: Symbol,
        parameters: Vec<Symbol>,
        sort: Sort,
    ) -> Result<Self::T, Self::E>;

    fn visit_echo(&mut self, message: String) -> Result<Self::T, Self::E>;

    fn visit_exit(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_assertions(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_assignment(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_info(&mut self, flag: Keyword) -> Result<Self::T, Self::E>;

    fn visit_get_model(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_option(&mut self, keyword: Keyword) -> Result<Self::T, Self::E>;

    fn visit_get_proof(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_unsat_assumptions(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_unsat_core(&mut self) -> Result<Self::T, Self::E>;

    fn visit_get_value(&mut self, terms: Vec<Term>) -> Result<Self::T, Self::E>;

    fn visit_pop(&mut self, level: Numeral) -> Result<Self::T, Self::E>;

    fn visit_push(&mut self, level: Numeral) -> Result<Self::T, Self::E>;

    fn visit_reset(&mut self) -> Result<Self::T, Self::E>;

    fn visit_reset_assertions(&mut self) -> Result<Self::T, Self::E>;

    fn visit_set_info(
        &mut self,
        keyword: Keyword,
        value: AttributeValue<Constant, Symbol, SExpr>,
    ) -> Result<Self::T, Self::E>;

    fn visit_set_logic(&mut self, symbol: Symbol) -> Result<Self::T, Self::E>;

    fn visit_set_option(
        &mut self,
        keyword: Keyword,
        value: AttributeValue<Constant, Symbol, SExpr>,
    ) -> Result<Self::T, Self::E>;
}

/// A visitor for the entire SMT2 syntax.
pub trait Smt2Visitor:
    ConstantVisitor<T = <Self as Smt2Visitor>::Constant, E = <Self as Smt2Visitor>::Error>
    + SymbolVisitor<T = <Self as Smt2Visitor>::Symbol, E = <Self as Smt2Visitor>::Error>
    + KeywordVisitor<T = <Self as Smt2Visitor>::Keyword, E = <Self as Smt2Visitor>::Error>
    + SExprVisitor<
        <Self as Smt2Visitor>::Constant,
        <Self as Smt2Visitor>::Symbol,
        <Self as Smt2Visitor>::Keyword,
        T = <Self as Smt2Visitor>::SExpr,
        E = <Self as Smt2Visitor>::Error,
    > + QualIdentifierVisitor<
        Identifier<<Self as Smt2Visitor>::Symbol>,
        <Self as Smt2Visitor>::Sort,
        T = <Self as Smt2Visitor>::QualIdentifier,
        E = <Self as Smt2Visitor>::Error,
    > + SortVisitor<
        <Self as Smt2Visitor>::Symbol,
        T = <Self as Smt2Visitor>::Sort,
        E = <Self as Smt2Visitor>::Error,
    > + TermVisitor<
        <Self as Smt2Visitor>::Constant,
        <Self as Smt2Visitor>::QualIdentifier,
        <Self as Smt2Visitor>::Keyword,
        <Self as Smt2Visitor>::SExpr,
        <Self as Smt2Visitor>::Symbol,
        <Self as Smt2Visitor>::Sort,
        T = <Self as Smt2Visitor>::Term,
        E = <Self as Smt2Visitor>::Error,
    > + CommandVisitor<
        <Self as Smt2Visitor>::Term,
        <Self as Smt2Visitor>::Symbol,
        <Self as Smt2Visitor>::Sort,
        <Self as Smt2Visitor>::Keyword,
        <Self as Smt2Visitor>::Constant,
        <Self as Smt2Visitor>::SExpr,
        T = <Self as Smt2Visitor>::Command,
        E = <Self as Smt2Visitor>::Error,
    >
{