3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-03 05:47:01 +00:00

moved smt 1.0 parser to its own module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-26 18:21:17 -07:00
parent 566ed44033
commit 1492b81290
7 changed files with 2 additions and 2 deletions

48
src/smtparser/smtparser.h Normal file
View file

@ -0,0 +1,48 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtparser.h
Abstract:
SMT parsing utilities
Author:
Nikolaj Bjorner (nbjorner) 2006-09-25
Revision History:
--*/
#ifndef _SMT_PARSER_H_
#define _SMT_PARSER_H_
#include<iostream>
#include"ast.h"
#include"vector.h"
#include"smtlib.h"
namespace smtlib {
class parser {
public:
static parser * create(ast_manager & ast_manager, bool ignore_user_patterns = false);
virtual ~parser() {}
virtual void add_builtin_op(char const *, family_id fid, decl_kind kind) = 0;
virtual void add_builtin_type(char const *, family_id fid, decl_kind kind) = 0;
virtual void initialize_smtlib() = 0;
virtual void set_error_stream(std::ostream& strm) = 0;
virtual bool parse_file(char const * path) = 0;
virtual bool parse_string(char const * string) = 0;
virtual benchmark * get_benchmark() = 0;
};
};
#endif