3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-15 07:15:26 +00:00
z3/src/parsers/smt2/smt2parser.h
Nikolaj Bjorner f3b79087ee add default tactic as option to overwrite the behavior of strategic solver factory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-17 09:27:10 -07:00

28 lines
545 B
C++

/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt2parser.h
Abstract:
SMT 2.0 parser
Author:
Leonardo de Moura (leonardo) 2011-03-01
Revision History:
--*/
#ifndef SMT2_PARSER_H_
#define SMT2_PARSER_H_
#include "cmd_context/cmd_context.h"
bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false, params_ref const & p = params_ref(), char const * filename = nullptr);
sexpr_ref parse_sexpr(cmd_context& ctx, std::istream& is, params_ref const& ps, char const* filename);
#endif