mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

created parsers folder

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-26 18:25:15 -07:00
parent 1492b81290
commit ad9bad9cc1
19 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

252
src/parsers/smt/smtlib.cpp Normal file
View file

@ -0,0 +1,252 @@
#include"smtlib.h"
#include"ast_pp.h"
#include"ast_smt2_pp.h"
#ifdef _WINDOWS
#ifdef ARRAYSIZE
#undef ARRAYSIZE
#endif
#include <windows.h>
#include <strsafe.h>
#endif
#include <iostream>
using namespace smtlib;
// --------------------------------------------------------------------------
// symtable
symtable::~symtable() {
reset();
}
void symtable::reset() {
svector<ptr_vector<func_decl>*> range;
m_ids.get_range(range);
for (unsigned i = 0; i < range.size(); ++i) {
ptr_vector<func_decl> const & v = *range[i];
for (unsigned j = 0; j < v.size(); ++j) {
m_manager.dec_ref(v[j]);
}
dealloc(range[i]);
}
m_ids.reset();
ptr_vector<sort> sorts;
m_sorts1.get_range(sorts);
for (unsigned i = 0; i < sorts.size(); ++i) {
m_manager.dec_ref(sorts[i]);
}
m_sorts1.reset();
ptr_vector<sort_builder> sort_builders;
m_sorts.get_range(sort_builders);
for (unsigned i = 0; i < sort_builders.size(); ++i) {
dealloc(sort_builders[i]);
}
m_sorts.reset();
}
void symtable::insert(symbol s, func_decl * d) {
ptr_vector<func_decl>* decls = 0;
m_manager.inc_ref(d);
if (!m_ids.find(s, decls)) {
SASSERT(!decls);
decls = alloc(ptr_vector<func_decl>);
decls->push_back(d);
m_ids.insert(s, decls);
}
else {
SASSERT(decls);
if ((*decls)[0] != d) {
decls->push_back(d);
}
else {
m_manager.dec_ref(d);
}
}
}
bool symtable::find1(symbol s, func_decl*& d) {
ptr_vector<func_decl>* decls = 0;
if (!m_ids.find(s, decls)) {
SASSERT(!decls);
return false;
}
SASSERT(decls && !decls->empty());
d = (*decls)[0];
return true;
}
bool symtable::find_overload(symbol s, ptr_vector<sort> const & dom, func_decl * & d) {
ptr_vector<func_decl>* decls = 0;
d = 0;
if (!m_ids.find(s, decls)) {
SASSERT(!decls);
return false;
}
SASSERT(decls);
for (unsigned i = 0; i < decls->size(); ++i) {
func_decl* decl = (*decls)[i];
if (decl->is_associative() && decl->get_arity() > 0) {
for (unsigned j = 0; j < dom.size(); ++j) {
if (dom[j] != decl->get_domain(0)) {
goto try_next;
}
}
d = decl;
return true;
}
if (decl->get_arity() != dom.size()) {
goto try_next;
}
for (unsigned j = 0; j < decl->get_arity(); ++j) {
if (decl->get_domain(j) != dom[j]) {
goto try_next;
}
}
d = decl;
return true;
try_next:
if (decl->get_family_id() == m_manager.get_basic_family_id() && decl->get_decl_kind() == OP_DISTINCT) {
// we skip type checking for 'distinct'
d = decl;
return true;
}
}
return false;
}
// Store in result the func_decl that are not attached to any family id.
// That is, the uninterpreted constants and function declarations.
void symtable::get_func_decls(ptr_vector<func_decl> & result) const {
svector<ptr_vector<func_decl>*> tmp;
m_ids.get_range(tmp);
svector<ptr_vector<func_decl>*>::const_iterator it = tmp.begin();
svector<ptr_vector<func_decl>*>::const_iterator end = tmp.end();
for (; it != end; ++it) {
ptr_vector<func_decl> * curr = *it;
if (curr) {
ptr_vector<func_decl>::const_iterator it2 = curr->begin();
ptr_vector<func_decl>::const_iterator end2 = curr->end();
for (; it2 != end2; ++it2) {
func_decl * d = *it2;
if (d && d->get_family_id() == null_family_id) {
result.push_back(d);
}
}
}
}
}
void symtable::insert(symbol s, sort_builder* sb) {
m_sorts.insert(s, sb);
}
bool symtable::lookup(symbol s, sort_builder*& sb) {
return m_sorts.find(s, sb);
}
void symtable::push_sort(symbol name, sort* srt) {
m_sorts.begin_scope();
sort_builder* sb = alloc(basic_sort_builder,srt);
m_sorts.insert(name, sb);
m_sorts_trail.push_back(sb);
}
void symtable::pop_sorts(unsigned num_sorts) {
while (num_sorts > 0) {
dealloc(m_sorts_trail.back());
m_sorts_trail.pop_back();
m_sorts.end_scope();
}
}
void symtable::get_sorts(ptr_vector<sort>& result) const {
vector<sort*,false> tmp;
m_sorts1.get_range(tmp);
for (unsigned i = 0; i < tmp.size(); ++i) {
if (tmp[i]->get_family_id() == null_family_id) {
result.push_back(tmp[i]);
}
}
}
// --------------------------------------------------------------------------
// theory
func_decl * theory::declare_func(symbol const & id, sort_ref_buffer & domain, sort * range,
bool is_assoc, bool is_comm, bool is_inj) {
func_decl * decl = m_ast_manager.mk_func_decl(id, domain.size(), domain.c_ptr(), range,
is_assoc, is_comm, is_inj);
m_symtable.insert(id, decl);
m_asts.push_back(decl);
return decl;
}
sort * theory::declare_sort(symbol const & id) {
sort * decl = m_ast_manager.mk_sort(id);
m_symtable.insert(id, decl);
m_asts.push_back(decl);
return decl;
}
bool theory::get_func_decl(symbol id, func_decl * & decl) {
return m_symtable.find1(id, decl);
}
bool theory::get_sort(symbol id, sort* & s) {
return m_symtable.find(id, s);
}
bool theory::get_const(symbol id, expr * & term) {
func_decl* decl = 0;
if (!get_func_decl(id,decl)) {
return false;
}
if (decl->get_arity() != 0) {
return false;
}
term = m_ast_manager.mk_const(decl);
m_asts.push_back(term);
return true;
}
void benchmark::display_as_smt2(std::ostream & out) const {
if (m_logic != symbol::null)
out << "(set-logic " << m_logic << ")\n";
out << "(set-info :smt-lib-version 2.0)\n";
out << "(set-info :status ";
switch (m_status) {
case SAT: out << "sat"; break;
case UNSAT: out << "unsat"; break;
default: out << "unknown"; break;
}
out << ")\n";
#if 0
ast_manager & m = m_ast_manager;
ptr_vector<func_decl> decls;
m_symtable.get_func_decls(decls);
ptr_vector<func_decl>::const_iterator it = decls.begin();
ptr_vector<func_decl>::const_iterator end = decls.end();
for (; it != end; ++it) {
func_decl * f = *it;
out << "(declare-fun " << f->get_name() << " (";
for (unsigned i = 0; i < f->get_arity(); i++) {
if (i > 0) out << " ";
out << mk_ismt2_pp(f->get_domain(i), m);
}
out << ") " << mk_ismt2_pp(f->get_range(), m);
out << ")\n";
}
#endif
}

232
src/parsers/smt/smtlib.h Normal file
View file

@ -0,0 +1,232 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtlib.h
Abstract:
SMT library utilities
Author:
Nikolaj Bjorner (nbjorner) 2006-09-29
Revision History:
--*/
#ifndef _SMTLIB_H_
#define _SMTLIB_H_
#include "ast.h"
#include "symbol_table.h"
#include "map.h"
#include "arith_decl_plugin.h"
namespace smtlib {
class sort_builder {
public:
virtual ~sort_builder() {}
virtual bool apply(unsigned num_params, parameter const* params, sort_ref& result) = 0;
virtual char const* error_message() { return ""; }
};
class basic_sort_builder : public sort_builder {
sort* m_sort;
public:
basic_sort_builder(sort* s) : m_sort(s) {}
virtual bool apply(unsigned np, parameter const*, sort_ref& result) {
result = m_sort;
return m_sort && np != 0;
}
};
class symtable {
ast_manager& m_manager;
symbol_table<sort*> m_sorts1;
symbol_table<sort_builder*> m_sorts;
ptr_vector<sort_builder> m_sorts_trail;
symbol_table<ptr_vector<func_decl>* > m_ids;
public:
symtable(ast_manager& m): m_manager(m) {}
~symtable();
void reset();
void insert(symbol s, func_decl * d);
bool find(symbol s, ptr_vector<func_decl> * & decls) {
return m_ids.find(s, decls);
}
bool find1(symbol s, func_decl * & d);
bool find_overload(symbol s, ptr_vector<sort> const & dom, func_decl * & d);
void insert(symbol s, sort * d) {
sort * d2;
if (m_sorts1.find(s, d2)) {
m_manager.dec_ref(d2);
}
m_manager.inc_ref(d);
m_sorts1.insert(s, d);
}
bool find(symbol s, sort * & d) {
return m_sorts1.find(s, d);
}
void insert(symbol s, sort_builder* sb);
bool lookup(symbol s, sort_builder*& sb);
void push_sort(symbol s, sort*);
void pop_sorts(unsigned num_sorts);
void get_func_decls(ptr_vector<func_decl> & result) const;
void get_sorts(ptr_vector<sort>& result) const;
};
class theory {
public:
typedef ptr_vector<expr>::const_iterator expr_iterator;
theory(ast_manager & ast_manager, symbol const& name):
m_name(name),
m_ast_manager(ast_manager),
m_symtable(ast_manager),
m_asts(ast_manager)
{}
virtual ~theory() {}
symtable * get_symtable() { return &m_symtable; }
void insert(sort * s) { m_symtable.insert(s->get_name(), s); }
void insert(func_decl * c) { m_symtable.insert(c->get_name(), c); }
func_decl * declare_func(symbol const & id, sort_ref_buffer & domain, sort * range,
bool is_assoc, bool is_comm, bool is_inj);
sort * declare_sort(symbol const & id);
void add_axiom(expr * axiom) {
m_asts.push_back(axiom);
m_axioms.push_back(axiom);
}
expr_iterator begin_axioms() const {
return m_axioms.begin();
}
unsigned get_num_axioms() const {
return m_axioms.size();
}
expr * const * get_axioms() const {
return m_axioms.c_ptr();
}
expr_iterator end_axioms() const {
return m_axioms.end();
}
void add_assumption(expr * axiom) {
m_asts.push_back(axiom);
m_assumptions.push_back(axiom);
}
unsigned get_num_assumptions() const {
return m_assumptions.size();
}
expr * const * get_assumptions() const {
return m_assumptions.c_ptr();
}
bool get_func_decl(symbol, func_decl*&);
bool get_sort(symbol, sort*&);
bool get_const(symbol, expr*&);
void set_name(symbol const& name) { m_name = name; }
symbol const get_name() const { return m_name; }
protected:
symbol m_name;
ast_manager& m_ast_manager;
ptr_vector<expr> m_axioms;
ptr_vector<expr> m_assumptions;
symtable m_symtable;
ast_ref_vector m_asts;
private:
theory& operator=(theory const&);
theory(theory const&);
};
class benchmark : public theory {
public:
enum status {
UNKNOWN,
SAT,
UNSAT
};
benchmark(ast_manager & ast_manager, symbol const & name) :
theory(ast_manager, name),
m_status(UNKNOWN) {}
virtual ~benchmark() {}
status get_status() const { return m_status; }
void set_status(status status) { m_status = status; }
symbol get_logic() const {
if (m_logic == symbol::null) {
return symbol("ALL");
}
return m_logic;
}
void set_logic(symbol const & s) { m_logic = s; }
unsigned get_num_formulas() const {
return m_formulas.size();
}
expr_iterator begin_formulas() const {
return m_formulas.begin();
}
expr_iterator end_formulas() const {
return m_formulas.end();
}
void add_formula(expr * formula) {
m_asts.push_back(formula);
m_formulas.push_back(formula);
}
void display_as_smt2(std::ostream & out) const;
private:
status m_status;
symbol m_logic;
ptr_vector<expr> m_formulas;
};
};
#endif

115
src/parsers/smt/smtlib_solver.cpp Normal file
View file

@ -0,0 +1,115 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtlib_solver.cpp
Abstract:
SMT based solver.
Author:
Nikolaj Bjorner (nbjorner) 2006-11-3.
Revision History:
--*/
#include"smtparser.h"
#include"smtlib_solver.h"
#include"warning.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"well_sorted.h"
#include"model.h"
#include"model_v2_pp.h"
#include"solver.h"
#include"smt_strategic_solver.h"
#include"cmd_context.h"
namespace smtlib {
solver::solver(front_end_params & params):
m_ast_manager(params.m_proof_mode, params.m_trace_stream),
m_params(params),
m_ctx(0),
m_parser(parser::create(m_ast_manager, params.m_ignore_user_patterns)),
m_error_code(0) {
m_parser->initialize_smtlib();
}
solver::~solver() {
if (m_ctx)
dealloc(m_ctx);
}
bool solver::solve_smt(char const * benchmark_file) {
IF_VERBOSE(100, verbose_stream() << "parsing...\n";);
if (!m_parser->parse_file(benchmark_file)) {
if (benchmark_file) {
warning_msg("could not parse file '%s'.", benchmark_file);
}
else {
warning_msg("could not parse input stream.");
}
m_error_code = ERR_PARSER;
return false;
}
benchmark * benchmark = m_parser->get_benchmark();
solve_benchmark(*benchmark);
return true;
}
bool solver::solve_smt_string(char const * benchmark_string) {
if (!m_parser->parse_string(benchmark_string)) {
warning_msg("could not parse string '%s'.", benchmark_string);
return false;
}
benchmark * benchmark = m_parser->get_benchmark();
solve_benchmark(*benchmark);
return true;
}
void solver::display_statistics() {
if (m_ctx)
m_ctx->display_statistics();
}
void solver::solve_benchmark(benchmark & benchmark) {
if (benchmark.get_num_formulas() == 0) {
// Hack: it seems SMT-LIB allow benchmarks without any :formula
benchmark.add_formula(m_ast_manager.mk_true());
}
m_ctx = alloc(cmd_context, m_params, true, &m_ast_manager, benchmark.get_logic());
m_ctx->set_solver(mk_smt_strategic_solver(*m_ctx));
theory::expr_iterator fit = benchmark.begin_formulas();
theory::expr_iterator fend = benchmark.end_formulas();
for (; fit != fend; ++fit)
solve_formula(benchmark, *fit);
}
void solver::solve_formula(benchmark const & benchmark, expr * f) {
IF_VERBOSE(100, verbose_stream() << "starting...\n";);
m_ctx->reset();
for (unsigned i = 0; i < benchmark.get_num_axioms(); i++)
m_ctx->assert_expr(benchmark.get_axioms()[i]);
m_ctx->assert_expr(f);
m_ctx->check_sat(benchmark.get_num_assumptions(), benchmark.get_assumptions());
check_sat_result * r = m_ctx->get_check_sat_result();
if (r != 0) {
proof * pr = r->get_proof();
if (pr != 0 && m_params.m_display_proof)
std::cout << mk_ll_pp(pr, m_ast_manager, false, false);
model_ref md;
if (r->status() != l_false) r->get_model(md);
if (md.get() != 0 && m_params.m_model) {
model_v2_pp(std::cout, *(md.get()), m_params.m_model_partial);
}
}
else {
m_error_code = ERR_UNKNOWN_RESULT;
}
}
};

48
src/parsers/smt/smtlib_solver.h Normal file
View file

@ -0,0 +1,48 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtlib_solver.h
Abstract:
SMT based solver.
Author:
Nikolaj Bjorner (nbjorner) 2006-11-3.
Revision History:
--*/
#ifndef _SMTLIB_SOLVER_H_
#define _SMTLIB_SOLVER_H_
#include"smtparser.h"
#include"front_end_params.h"
#include"lbool.h"
class cmd_context;
namespace smtlib {
class solver {
ast_manager m_ast_manager;
front_end_params & m_params;
cmd_context * m_ctx;
scoped_ptr<parser> m_parser;
unsigned m_error_code;
public:
solver(front_end_params & params);
~solver();
bool solve_smt(char const * benchmark_file);
bool solve_smt_string(char const * benchmark_string);
void display_statistics();
unsigned get_error_code() const { return m_error_code; }
private:
void solve_benchmark(benchmark & benchmark);
void solve_formula(benchmark const & benchmark, expr * f);
};
};
#endif

2759
src/parsers/smt/smtparser.cpp Normal file
View file

File diff suppressed because it is too large Load diff

48
src/parsers/smt/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

2491
src/parsers/smt2/smt2parser.cpp Normal file
View file

File diff suppressed because it is too large Load diff

26
src/parsers/smt2/smt2parser.h Normal file
View file

@ -0,0 +1,26 @@
/*++
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.h"
bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false);
#endif

355
src/parsers/smt2/smt2scanner.cpp Normal file
View file

@ -0,0 +1,355 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smt2scanner.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2011-03-09.
Revision History:
--*/
#include"smt2scanner.h"
namespace smt2 {
void scanner::next() {
if (m_cache_input)
m_cache.push_back(m_curr);
SASSERT(m_curr != EOF);
if (m_interactive) {
m_curr = m_stream.get();
}
else if (m_bpos < m_bend) {
m_curr = m_buffer[m_bpos];
m_bpos++;
}
else {
m_stream.read(m_buffer, SCANNER_BUFFER_SIZE);
m_bend = static_cast<unsigned>(m_stream.gcount());
m_bpos = 0;
if (m_bpos == m_bend) {
m_curr = EOF;
}
else {
m_curr = m_buffer[m_bpos];
m_bpos++;
}
}
m_spos++;
}
void scanner::read_comment() {
SASSERT(curr() == ';');
next();
while (true) {
char c = curr();
if (c == EOF)
return;
if (c == '\n') {
new_line();
next();
return;
}
next();
}
}
scanner::token scanner::read_quoted_symbol() {
SASSERT(curr() == '|');
bool escape = false;
m_string.reset();
next();
while (true) {
char c = curr();
if (c == EOF) {
throw scanner_exception("unexpected end of quoted symbol", m_line, m_spos);
}
else if (c == '\n') {
new_line();
}
else if (c == '|' && !escape) {
next();
m_string.push_back(0);
m_id = m_string.begin();
TRACE("scanner", tout << "new quoted symbol: " << m_id << "\n";);
return SYMBOL_TOKEN;
}
escape = (c == '\\');
m_string.push_back(c);
next();
}
}
scanner::token scanner::read_symbol_core() {
while (true) {
char c = curr();
char n = m_normalized[static_cast<unsigned char>(c)];
if (n == 'a' || n == '0' || n == '-') {
m_string.push_back(c);
next();
}
else {
m_string.push_back(0);
m_id = m_string.begin();
TRACE("scanner", tout << "new symbol: " << m_id << "\n";);
return SYMBOL_TOKEN;
}
}
}
scanner::token scanner::read_symbol() {
SASSERT(m_normalized[static_cast<unsigned>(curr())] == 'a' || curr() == ':' || curr() == '-');
m_string.reset();
m_string.push_back(curr());
next();
return read_symbol_core();
}
scanner::token scanner::read_number() {
SASSERT('0' <= curr() && curr() <= '9');
rational q(1);
m_number = rational(curr() - '0');
next();
bool is_float = false;
while (true) {
char c = curr();
if ('0' <= c && c <= '9') {
m_number = rational(10)*m_number + rational(c - '0');
if (is_float)
q *= rational(10);
next();
}
else if (c == '.') {
if (is_float)
break;
is_float = true;
next();
}
else {
break;
}
}
if (is_float)
m_number /= q;
TRACE("scanner", tout << "new number: " << m_number << "\n";);
return is_float ? FLOAT_TOKEN : INT_TOKEN;
}
scanner::token scanner::read_signed_number() {
SASSERT(curr() == '-');
next();
if ('0' <= curr() && curr() <= '9') {
scanner::token r = read_number();
m_number.neg();
return r;
}
else {
// it is a symbol.
m_string.reset();
m_string.push_back('-');
return read_symbol_core();
}
}
scanner::token scanner::read_string() {
SASSERT(curr() == '\"');
next();
m_string.reset();
while (true) {
char c = curr();
if (c == EOF)
throw scanner_exception("unexpected end of string", m_line, m_spos);
if (c == '\"') {
next();
m_string.push_back(0);
return STRING_TOKEN;
}
if (c == '\n')
new_line();
else if (c == '\\') {
next();
c = curr();
if (c == EOF)
throw scanner_exception("unexpected end of string", m_line, m_spos);
if (c != '\\' && c != '\"')
throw scanner_exception("invalid escape sequence", m_line, m_spos);
}
m_string.push_back(c);
next();
}
}
scanner::token scanner::read_bv_literal() {
SASSERT(curr() == '#');
next();
char c = curr();
if (c == 'x') {
next();
c = curr();
m_number = rational(0);
m_bv_size = 0;
while (true) {
if ('0' <= c && c <= '9') {
m_number *= rational(16);
m_number += rational(c - '0');
}
else if ('a' <= c && c <= 'f') {
m_number *= rational(16);
m_number += rational(10 + (c - 'a'));
}
else if ('A' <= c && c <= 'F') {
m_number *= rational(16);
m_number += rational(10 + (c - 'A'));
}
else {
if (m_bv_size == 0)
throw scanner_exception("invalid empty bit-vector literal", m_line, m_spos);
return BV_TOKEN;
}
m_bv_size += 4;
next();
c = curr();
}
}
else if (c == 'b') {
next();
c = curr();
m_number = rational(0);
m_bv_size = 0;
while (c == '0' || c == '1') {
m_number *= rational(2);
m_number += rational(c - '0');
m_bv_size++;
next();
c = curr();
}
if (m_bv_size == 0)
throw scanner_exception("invalid empty bit-vector literal", m_line, m_spos);
return BV_TOKEN;
}
else {
throw scanner_exception("invalid bit-vector literal, expecting 'x' or 'b'", m_line, m_spos);
}
}
scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
m_ctx(ctx),
m_interactive(interactive),
m_spos(0),
m_curr(0), // avoid Valgrind warning
m_line(1),
m_pos(0),
m_bv_size(UINT_MAX),
m_bpos(0),
m_bend(0),
m_stream(stream),
m_cache_input(false) {
for (int i = 0; i < 256; ++i) {
m_normalized[i] = (char) i;
}
m_normalized[static_cast<int>('\t')] = ' ';
m_normalized[static_cast<int>('\r')] = ' ';
// assert ('a' < 'z');
for (char ch = 'b'; ch <= 'z'; ++ch) {
m_normalized[static_cast<int>(ch)] = 'a';
}
for (char ch = 'A'; ch <= 'Z'; ++ch) {
m_normalized[static_cast<int>(ch)] = 'a';
}
// assert ('0' < '9', '9' - '0' == 9);
for (char ch = '1'; ch <= '9'; ++ch) {
m_normalized[static_cast<int>(ch)] = '0';
}
// SMT2 "Symbols": ~ ! @ $ % ^ & * _ - + = < > . ? /
m_normalized[static_cast<int>('~')] = 'a';
m_normalized[static_cast<int>('!')] = 'a';
m_normalized[static_cast<int>('@')] = 'a';
m_normalized[static_cast<int>('$')] = 'a';
m_normalized[static_cast<int>('%')] = 'a';
m_normalized[static_cast<int>('^')] = 'a';
m_normalized[static_cast<int>('&')] = 'a';
m_normalized[static_cast<int>('*')] = 'a';
m_normalized[static_cast<int>('_')] = 'a';
m_normalized[static_cast<int>('-')] = '-';
m_normalized[static_cast<int>('+')] = 'a';
m_normalized[static_cast<int>('=')] = 'a';
m_normalized[static_cast<int>('<')] = 'a';
m_normalized[static_cast<int>('>')] = 'a';
m_normalized[static_cast<int>('.')] = 'a';
m_normalized[static_cast<int>('?')] = 'a';
m_normalized[static_cast<int>('/')] = 'a';
next();
}
scanner::token scanner::scan() {
while (true) {
char c = curr();
m_pos = m_spos;
switch (m_normalized[(unsigned char) c]) {
case ' ':
next();
break;
case '\n':
next();
new_line();
break;
case ';':
read_comment();
break;
case ':':
read_symbol();
return KEYWORD_TOKEN;
case '(':
next();
return LEFT_PAREN;
case ')':
next();
return RIGHT_PAREN;
case '|':
return read_quoted_symbol();
case 'a':
return read_symbol();
case '"':
return read_string();
case '0':
return read_number();
case '#':
return read_bv_literal();
case '-':
if (m_ctx.is_smtlib2_compliant())
return read_symbol();
else
return read_signed_number();
case -1:
return EOF_TOKEN;
default: {
scanner_exception ex("unexpected character", m_line, m_spos);
next();
throw ex;
}}
}
}
char const * scanner::cached_str(unsigned begin, unsigned end) {
m_cache_result.reset();
while (isspace(m_cache[begin]) && begin < end)
begin++;
while (begin < end && isspace(m_cache[end-1]))
end--;
for (unsigned i = begin; i < end; i++)
m_cache_result.push_back(m_cache[i]);
m_cache_result.push_back(0);
return m_cache_result.begin();
}
};

108
src/parsers/smt2/smt2scanner.h Normal file
View file

@ -0,0 +1,108 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smt2scanner.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2011-03-09.
Revision History:
--*/
#ifndef _SMT2SCANNER_H_
#define _SMT2SCANNER_H_
#include<iostream>
#include"symbol.h"
#include"vector.h"
#include"rational.h"
#include"cmd_context.h"
namespace smt2 {
typedef cmd_exception scanner_exception;
class scanner {
private:
cmd_context & m_ctx;
bool m_interactive;
int m_spos; // position in the current line of the stream
char m_curr; // current char;
int m_line; // line
int m_pos; // start position of the token
// data
symbol m_id;
rational m_number;
unsigned m_bv_size;
// end of data
char m_normalized[256];
#define SCANNER_BUFFER_SIZE 1024
char m_buffer[SCANNER_BUFFER_SIZE];
unsigned m_bpos;
unsigned m_bend;
svector<char> m_string;
std::istream& m_stream;
bool m_cache_input;
svector<char> m_cache;
svector<char> m_cache_result;
char curr() const { return m_curr; }
void new_line() { m_line++; m_spos = 0; }
void next();
public:
enum token {
NULL_TOKEN = 0,
LEFT_PAREN = 1,
RIGHT_PAREN,
KEYWORD_TOKEN,
SYMBOL_TOKEN,
STRING_TOKEN,
INT_TOKEN,
BV_TOKEN,
FLOAT_TOKEN,
EOF_TOKEN
};
scanner(cmd_context & ctx, std::istream& stream, bool interactive = false);
~scanner() {}
int get_line() const { return m_line; }
int get_pos() const { return m_pos; }
symbol const & get_id() const { return m_id; }
rational get_number() const { return m_number; }
unsigned get_bv_size() const { return m_bv_size; }
char const * get_string() const { return m_string.begin(); }
token scan();
token read_symbol_core();
token read_symbol();
token read_quoted_symbol();
void read_comment();
token read_number();
token read_signed_number();
token read_string();
token read_bv_literal();
void start_caching() { m_cache_input = true; m_cache.reset(); }
void stop_caching() { m_cache_input = false; }
unsigned cache_size() const { return m_cache.size(); }
void reset_cache() { m_cache.reset(); }
char const * cached_str(unsigned begin, unsigned end);
};
};
#endif /* _SCANNER_H_ */

70
src/parsers/util/cost_parser.cpp Normal file
View file

@ -0,0 +1,70 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
cost_parser.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-06-14.
Revision History:
--*/
#include"cost_parser.h"
cost_parser::cost_parser(ast_manager & m):
simple_parser(m),
m_util(m),
m_vars(m) {
family_id fid;
fid = m.get_basic_family_id();
add_builtin_op("true", fid, OP_TRUE);
add_builtin_op("false", fid, OP_FALSE);
add_builtin_op("not", fid, OP_NOT);
add_builtin_op("and", fid, OP_AND);
add_builtin_op("implies", fid, OP_IMPLIES);
add_builtin_op("or", fid, OP_OR);
add_builtin_op("ite", fid, OP_ITE);
add_builtin_op("=", fid, OP_EQ);
add_builtin_op("iff", fid, OP_IFF);
add_builtin_op("xor", fid, OP_XOR);
fid = m_util.get_family_id();
add_builtin_op("+", fid, OP_ADD);
add_builtin_op("*", fid, OP_MUL);
add_builtin_op("-", fid, OP_SUB);
add_builtin_op("/", fid, OP_DIV);
add_builtin_op("<=", fid, OP_LE);
add_builtin_op(">=", fid, OP_GE);
add_builtin_op("<", fid, OP_LT);
add_builtin_op(">", fid, OP_GT);
}
expr * cost_parser::parse_int(rational const & r) {
return m_util.mk_numeral(r, false);
}
expr * cost_parser::parse_float(rational const & r) {
return m_util.mk_numeral(r, false);
}
unsigned cost_parser::add_var(symbol name) {
sort * real = m_util.mk_real();
unsigned r = m_vars.size();
var * v = m_manager.mk_var(r, real);
simple_parser::add_var(name, v);
m_vars.push_back(v);
return r;
}
void cost_parser::reset_vars() {
simple_parser::reset_vars();
m_vars.reset();
}

39
src/parsers/util/cost_parser.h Normal file
View file

@ -0,0 +1,39 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
cost_parser.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-06-14.
Revision History:
--*/
#ifndef _COST_PARSER_H_
#define _COST_PARSER_H_
#include"simple_parser.h"
#include"arith_decl_plugin.h"
class cost_parser : public simple_parser {
arith_util m_util;
var_ref_vector m_vars;
public:
cost_parser(ast_manager & m);
virtual ~cost_parser() {}
virtual expr * parse_int(rational const & r);
virtual expr * parse_float(rational const & r);
unsigned add_var(symbol name);
unsigned add_var(char const * name) { return add_var(symbol(name)); }
void reset_vars();
};
#endif /* _COST_PARSER_H_ */

105
src/parsers/util/pattern_validation.cpp Normal file
View file

@ -0,0 +1,105 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
pattern_validation.cpp
Abstract:
Code for checking whether a pattern is valid or not.
Author:
Leonardo de Moura (leonardo) 2006-12-08.
Revision History:
--*/
#include"pattern_validation.h"
#include"for_each_expr.h"
#include"warning.h"
#include"ast_pp.h"
struct pattern_validation_functor {
uint_set & m_found_vars;
unsigned m_num_bindings;
unsigned m_num_new_bindings;
bool m_result;
bool m_found_a_var;
family_id m_bfid;
family_id m_lfid;
pattern_validation_functor(uint_set & found_vars, unsigned num_bindings, unsigned num_new_bindings,
family_id bfid, family_id lfid):
m_found_vars(found_vars),
m_num_bindings(num_bindings),
m_num_new_bindings(num_new_bindings),
m_result(true),
m_found_a_var(false),
m_bfid(bfid),
m_lfid(lfid) {
}
bool is_forbidden(func_decl const * decl) {
family_id fid = decl->get_family_id();
if (fid == m_bfid && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE)
return true;
if (fid == m_lfid)
return true;
return false;
}
void operator()(app * n) {
func_decl * decl = to_app(n)->get_decl();
if (is_forbidden(decl)) {
warning_msg("'%s' cannot be used in patterns.", decl->get_name().str().c_str());
m_result = false;
}
}
void operator()(var * v) {
unsigned idx = to_var(v)->get_idx();
if (idx >= m_num_bindings) {
warning_msg("free variables cannot be used in patterns.");
m_result = false;
return;
}
if (idx < m_num_new_bindings) {
m_found_a_var = true;
m_found_vars.insert(idx);
}
}
void operator()(quantifier * q) { m_result = false; }
};
bool pattern_validator::process(uint_set & found_vars, unsigned num_bindings, unsigned num_new_bindings, expr * n) {
// I'm traversing the DAG as a tree, this is not a problem since pattern are supposed to be small ASTs.
if (n->get_kind() == AST_VAR) {
warning_msg("invalid pattern: variable.");
return false;
}
pattern_validation_functor f(found_vars, num_bindings, num_new_bindings, m_bfid, m_lfid);
for_each_expr(f, n);
if (!f.m_result)
return false;
if (!f.m_found_a_var) {
warning_msg("pattern does contain any variable.");
return false;
}
return true;
}
bool pattern_validator::operator()(unsigned num_bindings, unsigned num_new_bindings, expr * n) {
uint_set found_vars;
if (!process(found_vars, num_bindings, num_new_bindings, n))
return false;
bool r = found_vars.num_elems() == num_new_bindings;
if (!r)
warning_msg("pattern does not contain all quantified variables.");
return r;
}

44
src/parsers/util/pattern_validation.h Normal file
View file

@ -0,0 +1,44 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
pattern_validation.h
Abstract:
Code for checking whether a pattern is valid or not.
Author:
Leonardo de Moura (leonardo) 2006-12-08.
Revision History:
--*/
#ifndef _PATTERN_VALIDATION_H_
#define _PATTERN_VALIDATION_H_
#include"ast.h"
#include"uint_set.h"
#include"vector.h"
class pattern_validator {
family_id m_bfid;
family_id m_lfid;
bool process(uint_set & found_vars, unsigned num_bindings, unsigned num_new_bindings, expr * n);
public:
pattern_validator(ast_manager const & m):
m_bfid(m.get_basic_family_id()),
m_lfid(m.get_family_id("label")) {
}
bool operator()(unsigned num_bindings, unsigned num_new_bindings, expr * n);
bool operator()(unsigned num_new_bindings, expr * n) { return operator()(UINT_MAX, num_new_bindings, n); }
};
#endif /* _PATTERN_VALIDATION_H_ */

496
src/parsers/util/scanner.cpp Normal file
View file

@ -0,0 +1,496 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
scanner.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-03-31.
Revision History:
--*/
#include"scanner.h"
inline char scanner::read_char() {
if (m_is_interactive) {
++m_pos;
return m_stream.get();
}
if (m_bpos >= m_bend) {
m_buffer[0] = m_last_char;
m_stream.read(m_buffer.c_ptr()+1, m_buffer.size()-1);
m_bend = 1 + static_cast<unsigned>(m_stream.gcount());
m_bpos = 1;
m_last_char = m_buffer[m_bend-1];
}
++m_pos;
if (m_bpos < m_bend) {
return m_buffer[m_bpos++];
} else {
// increment m_bpos, so unread_char() will work properly
++m_bpos;
return -1;
}
}
inline void scanner::unread_char() {
--m_pos;
if (m_is_interactive) {
m_stream.unget();
} else {
// at most one character can be unread.
SASSERT(m_bpos > 0);
--m_bpos;
}
}
inline bool scanner::state_ok() {
return m_state != ERROR_TOKEN && m_state != EOF_TOKEN;
}
void scanner::comment(char delimiter) {
while(state_ok()) {
char ch = read_char();
if ('\n' == ch) {
++m_line;
}
if (delimiter == ch || -1 == ch) {
return;
}
}
}
scanner::token scanner::read_symbol(char ch) {
bool escape = false;
if (m_smt2)
m_string.pop_back(); // remove leading '|'
while (ch != '|' || escape) {
if (ch == EOF) {
// TODO: use error reporting
m_err << "ERROR: unexpected end of file.\n";
return EOF_TOKEN;
}
if (ch == '\n') {
++m_line;
}
escape = (ch == '\\');
m_string.push_back(ch);
ch = read_char();
}
if (!m_smt2)
m_string.push_back(ch); // don't add trailing '|'
m_string.push_back(0);
m_id = m_string.begin();
return ID_TOKEN;
}
scanner::token scanner::read_id(char first_char) {
char ch;
m_string.reset();
m_params.reset();
m_string.push_back(first_char);
bool is_arith = (m_normalized[(unsigned char) first_char] == '+');
bool is_alpha = (m_normalized[(unsigned char) first_char] == 'a');
ch = read_char();
// In SMT2 "-20" is an identifier.
if (!m_smt2 && state_ok() && first_char == '-' && m_normalized[(unsigned char) ch] == '0') {
return read_number(ch, false);
}
if (state_ok() && first_char == '|') {
return read_symbol(ch);
}
while (state_ok()) {
switch(m_normalized[(unsigned char) ch]) {
case '+':
if (is_arith) {
m_string.push_back(ch);
break;
}
// strings can have hyphens.
if (!is_alpha || ch != '-') {
goto bail_out;
}
case 'a':
case ':':
case '.':
case '0':
if (is_arith) {
goto bail_out;
}
m_string.push_back(ch);
break;
case '[':
m_string.push_back(0);
m_id = m_string.begin();
if (read_params()) {
return ID_TOKEN;
}
else {
return m_state;
}
default:
goto bail_out;
}
ch = read_char();
}
return m_state;
bail_out:
m_string.push_back(0);
m_id = m_string.begin();
unread_char();
return ID_TOKEN;
}
bool scanner::read_params() {
unsigned param_num = 0;
while (state_ok()) {
char ch = read_char();
switch (m_normalized[(unsigned char) ch]) {
case '0':
param_num = 10*param_num + (ch - '0');
break;
case ']':
m_params.push_back(parameter(param_num));
return true;
case ':':
m_params.push_back(parameter(param_num));
param_num = 0;
break;
default:
m_string.reset();
m_string.push_back(ch);
while (true) {
ch = read_char();
if (ch == ':' || ch == ']') {
m_string.push_back(0);
m_params.push_back(parameter(symbol(m_string.c_ptr())));
param_num = 0;
if (ch == ':') {
unread_char();
}
else {
return true;
}
break;
}
if (ch == EOF) {
// TODO: use error reporting
m_err << "ERROR: unexpected character: '" << ((int)ch) << " " << ch << "'.\n";
m_state = ERROR_TOKEN;
break;
}
m_string.push_back(ch);
}
break;
}
}
return false;
}
scanner::token scanner::read_number(char first_char, bool is_pos) {
unsigned divide_by = 0;
m_number = rational(first_char - '0');
m_state = INT_TOKEN;
while (true) {
char ch = read_char();
if (m_normalized[(unsigned char) ch] == '0') {
m_number = rational(10)*m_number + rational(ch - '0');
if (m_state == FLOAT_TOKEN) {
++divide_by;
}
}
else if (ch == '.') {
m_state = FLOAT_TOKEN;
}
else {
unread_char();
break;
}
}
if (!is_pos) {
m_number.neg();
}
if (m_state == FLOAT_TOKEN) {
m_number /= power(rational(10), divide_by);
}
return m_state;
}
scanner::token scanner::read_string(char delimiter, token result) {
m_string.reset();
m_params.reset();
while (true) {
char ch = read_char();
if (!state_ok()) {
return m_state;
}
if (ch == '\n') {
++m_line;
}
if (ch == delimiter || ch == EOF) {
m_string.push_back(0);
m_id = m_string.begin();
return result;
}
if (ch == '\\') {
m_string.push_back('\\');
ch = read_char();
}
m_string.push_back(ch);
}
return m_state;
}
scanner::token scanner::read_bv_literal() {
TRACE("scanner", tout << "read_bv_literal\n";);
if (m_bv_token) {
char ch = read_char();
if (ch == 'x') {
ch = read_char();
m_number = rational(0);
m_bv_size = 0;
while (true) {
if ('0' <= ch && ch <= '9') {
m_number *= rational(16);
m_number += rational(ch - '0');
}
else if ('a' <= ch && ch <= 'f') {
m_number *= rational(16);
m_number += rational(10 + (ch - 'a'));
}
else if ('A' <= ch && ch <= 'F') {
m_number *= rational(16);
m_number += rational(10 + (ch - 'A'));
}
else {
unread_char();
m_state = m_bv_size == 0 ? ERROR_TOKEN : BV_TOKEN;
TRACE("scanner", tout << m_state << ", bv-size: " << m_bv_size << ", INT_TOKEN: " << INT_TOKEN
<< ", BV_TOKEN: " << BV_TOKEN << "\n";);
return m_state;
}
m_bv_size += 4;
ch = read_char();
}
}
else if (ch == 'b') {
ch = read_char();
m_number = rational(0);
m_bv_size = 0;
while (ch == '0' || ch == '1') {
m_number *= rational(2);
m_number += rational(ch - '0');
m_bv_size++;
ch = read_char();
}
unread_char();
m_state = m_bv_size == 0 ? ERROR_TOKEN : BV_TOKEN;
return m_state;
}
else {
m_state = ERROR_TOKEN;
return m_state;
}
}
else {
// hack for the old parser
char ch = read_char();
bool is_hex = false;
m_state = ID_TOKEN;
m_string.reset();
m_params.reset();
// convert to SMT1 format
m_string.push_back('b');
m_string.push_back('v');
if (ch == 'x') {
m_string.push_back('h');
m_string.push_back('e');
m_string.push_back('x');
is_hex = true;
} else if (ch == 'b') {
m_string.push_back('b');
m_string.push_back('i');
m_string.push_back('n');
} else {
// TODO: use error reporting
m_err << "ERROR: unexpected character after '#': '" << ((int)ch) << " " << ch << "'.\n";
m_state = ERROR_TOKEN;
return m_state;
}
while (true) {
ch = read_char();
if (ch == '0' || ch == '1' ||
(is_hex &&
(('0' <= ch && ch <= '9') ||
('a' <= ch && ch <= 'f') ||
('A' <= ch && ch <= 'F')))) {
m_string.push_back(ch);
} else {
unread_char();
break;
}
}
m_string.push_back(0);
m_id = m_string.begin();
return m_state;
}
}
scanner::scanner(std::istream& stream, std::ostream& err, bool smt2, bool bv_token):
m_line(1),
m_pos(0),
m_id(""),
m_bv_size(UINT_MAX),
m_state(ID_TOKEN),
m_stream(stream),
m_err(err),
m_bpos(1 << 10),
m_bend(1 << 10),
m_last_char(0),
m_smt2(smt2),
m_bv_token(bv_token) {
char ch;
m_is_interactive = &stream == &std::cin;
m_buffer.resize(m_bpos);
for (int i = 0; i < 256; ++i) {
m_normalized[i] = (char) i;
}
m_normalized[static_cast<int>('\t')] = ' ';
m_normalized[static_cast<int>('\r')] = ' ';
// assert ('a' < 'z');
for (ch = 'b'; ch <= 'z'; ++ch) {
m_normalized[static_cast<int>(ch)] = 'a';
}
for (ch = 'A'; ch <= 'Z'; ++ch) {
m_normalized[static_cast<int>(ch)] = 'a';
}
// assert ('0' < '9', '9' - '0' == 9);
for (ch = '1'; ch <= '9'; ++ch) {
m_normalized[static_cast<int>(ch)] = '0';
}
if (m_smt2) {
// SMT2 3.1, "Symbols": ~ ! @ $ % ^ & * _ - + = < > . ? /
m_normalized[static_cast<int>('~')] = 'a';
m_normalized[static_cast<int>('!')] = 'a';
m_normalized[static_cast<int>('@')] = 'a';
m_normalized[static_cast<int>('$')] = 'a';
m_normalized[static_cast<int>('%')] = 'a';
m_normalized[static_cast<int>('^')] = 'a';
m_normalized[static_cast<int>('&')] = 'a';
m_normalized[static_cast<int>('*')] = 'a';
m_normalized[static_cast<int>('_')] = 'a';
m_normalized[static_cast<int>('-')] = 'a';
m_normalized[static_cast<int>('+')] = 'a';
m_normalized[static_cast<int>('=')] = 'a';
m_normalized[static_cast<int>('<')] = 'a';
m_normalized[static_cast<int>('>')] = 'a';
m_normalized[static_cast<int>('.')] = 'a';
m_normalized[static_cast<int>('?')] = 'a';
m_normalized[static_cast<int>('/')] = 'a';
// SMT2 3.1, "Hexadecimals", "Binaries"
m_normalized[static_cast<int>('#')] = '#';
m_normalized[static_cast<int>('|')] = '+';
} else {
m_normalized[static_cast<int>('=')] = '+';
m_normalized[static_cast<int>('<')] = '+';
m_normalized[static_cast<int>('>')] = '+';
m_normalized[static_cast<int>('+')] = '+';
m_normalized[static_cast<int>('-')] = '+';
m_normalized[static_cast<int>('*')] = '+';
m_normalized[static_cast<int>('/')] = '+';
m_normalized[static_cast<int>('%')] = '+';
m_normalized[static_cast<int>('~')] = '+';
m_normalized[static_cast<int>('&')] = '+';
m_normalized[static_cast<int>('@')] = '+';
m_normalized[static_cast<int>('#')] = '+';
m_normalized[static_cast<int>('|')] = '+';
m_normalized[static_cast<int>('\\')] = '+';
m_normalized[static_cast<int>('.')] = '.';
m_normalized[static_cast<int>('_')] = 'a';
m_normalized[static_cast<int>('\'')] = 'a';
m_normalized[static_cast<int>('!')] = 'a';
m_normalized[static_cast<int>('?')] = 'a';
}
}
scanner::token scanner::scan() {
while (state_ok()) {
char ch = read_char();
switch (m_normalized[(unsigned char) ch]) {
case ' ':
break;
case '\n':
m_pos = 0;
++m_line;
break;
case ';':
comment('\n');
break;
case ':':
return COLON;
case '(':
return LEFT_PAREN;
case ')':
return RIGHT_PAREN;
case '?':
case '$':
case 'a':
case '+':
case '.':
return read_id(ch);
case '{':
return read_string('}',COMMENT_TOKEN);
case '"':
return read_string('"',STRING_TOKEN);
case '0':
return read_number(ch, true);
case '#':
return read_bv_literal();
case -1:
m_state = EOF_TOKEN;
break;
default:
// TODO: use error reporting
m_err << "ERROR: unexpected character: '" << ((int)ch) << " " << ch << "'.\n";
m_state = ERROR_TOKEN;
break;
}
}
return m_state;
}

92
src/parsers/util/scanner.h Normal file
View file

@ -0,0 +1,92 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
scanner.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-03-31.
Revision History:
--*/
#ifndef _SCANNER_H_
#define _SCANNER_H_
#include"ast.h"
class scanner {
public:
enum token {
LEFT_PAREN = 1,
RIGHT_PAREN,
COLON,
ID_TOKEN,
STRING_TOKEN,
COMMENT_TOKEN,
INT_TOKEN,
BV_TOKEN,
FLOAT_TOKEN,
EOF_TOKEN,
ERROR_TOKEN
};
scanner(std::istream& stream, std::ostream& err, bool smt2, bool bv_token=false);
~scanner() {}
int get_line() const { return m_line; }
int get_pos() const { return m_pos; }
symbol const & get_id() const { return m_id; }
rational get_number() const { return m_number; }
unsigned get_bv_size() const { return m_bv_size; }
vector<parameter> const & get_params() const { return m_params; }
token scan();
private:
int m_line;
int m_pos;
symbol m_id;
rational m_number;
unsigned m_bv_size;
token m_state;
char m_normalized[256];
vector<char> m_string;
std::istream& m_stream;
std::ostream& m_err;
vector<parameter> m_params;
buffer<char> m_buffer;
unsigned m_bpos;
unsigned m_bend;
char m_last_char;
bool m_is_interactive;
bool m_smt2;
bool m_bv_token;
char read_char();
token read_symbol(char ch);
void unread_char();
void comment(char delimiter);
token read_id(char first_char);
bool read_params();
token read_number(char first_char, bool is_pos);
token read_string(char delimiter, token result);
token read_bv_literal();
bool state_ok();
};
#endif /* _SCANNER_H_ */

149
src/parsers/util/simple_parser.cpp Normal file
View file

@ -0,0 +1,149 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
simple_parser.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-03-31.
Revision History:
--*/
#include<fstream>
#include<sstream>
#include"simple_parser.h"
#include"warning.h"
#include"scanner.h"
simple_parser::simple_parser(ast_manager & m):
m_manager(m),
m_exprs(m) {
}
simple_parser::~simple_parser() {
}
void simple_parser::add_builtin_op(symbol const & s, family_id fid, decl_kind kind) {
SASSERT(!m_builtin.contains(s));
SASSERT(!m_vars.contains(s));
m_builtin.insert(s, builtin_op(fid, kind));
}
void simple_parser::add_builtin_op(char const * str, family_id fid, decl_kind kind) {
add_builtin_op(symbol(str), fid, kind);
}
void simple_parser::add_var(symbol const & s, var * v) {
SASSERT(!m_builtin.contains(s));
SASSERT(!m_vars.contains(s));
m_vars.insert(s, v);
}
void simple_parser::add_var(char const * str, var * v) {
add_var(symbol(str), v);
}
void simple_parser::reset() {
m_builtin.reset();
m_vars.reset();
m_exprs.reset();
}
void simple_parser::reset_vars() {
m_vars.reset();
}
expr * simple_parser::parse_expr(scanner & s) {
builtin_op op;
var * v;
expr * r;
scanner::token token;
token = s.scan();
switch (token) {
case scanner::LEFT_PAREN:
token = s.scan();
if (token != scanner::ID_TOKEN)
throw parser_error();
if (m_builtin.find(s.get_id(), op)) {
ptr_vector<expr> args;
while (true) {
expr * arg = parse_expr(s);
if (arg) {
args.push_back(arg);
}
else {
expr * r = m_manager.mk_app(op.m_family_id, op.m_kind, args.size(), args.c_ptr());
m_exprs.push_back(r);
return r;
}
}
}
throw parser_error();
case scanner::RIGHT_PAREN:
return 0;
case scanner::ID_TOKEN:
if (m_builtin.find(s.get_id(), op)) {
expr * r = m_manager.mk_const(op.m_family_id, op.m_kind);
m_exprs.push_back(r);
return r;
}
else if (m_vars.find(s.get_id(), v)) {
return v;
}
throw parser_error();
case scanner::INT_TOKEN:
r = parse_int(s.get_number());
m_exprs.push_back(r);
return r;
case scanner::FLOAT_TOKEN:
r = parse_float(s.get_number());
m_exprs.push_back(r);
return r;
default:
throw parser_error();
}
}
bool simple_parser::parse(std::istream & in, expr_ref & result) {
scanner s(in, std::cerr, false);
try {
result = parse_expr(s);
if (!result)
throw parser_error();
}
catch (parser_error) {
warning_msg("parser error");
return false;
}
m_exprs.reset();
return result.get() != 0;
}
bool simple_parser::parse_string(char const * str, expr_ref & result) {
std::string s = str;
std::istringstream is(s);
return parse(is, result);
}
bool simple_parser::parse_file(char const * file, expr_ref & result) {
if (file != 0) {
std::ifstream stream(file);
if (!stream) {
warning_msg("ERROR: could not open file '%s'.", file);
return false;
}
return parse(stream, result);
}
else {
return parse(std::cin, result);
}
}

64
src/parsers/util/simple_parser.h Normal file
View file

@ -0,0 +1,64 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
simple_parser.h
Abstract:
Simple sexpr parser
Author:
Leonardo de Moura (leonardo) 2008-03-31.
Revision History:
--*/
#ifndef _SIMPLE_PARSER_H_
#define _SIMPLE_PARSER_H_
#include"ast.h"
#include"map.h"
class scanner;
/**
\brief Simple sexpr parser.
This class is used to parse small expressions used for configuring Z3.
*/
class simple_parser {
protected:
struct parser_error {};
struct builtin_op {
family_id m_family_id;
decl_kind m_kind;
builtin_op() : m_family_id(null_family_id), m_kind(0) {}
builtin_op(family_id fid, decl_kind k) : m_family_id(fid), m_kind(k) {}
};
typedef map<symbol, builtin_op, symbol_hash_proc, symbol_eq_proc> op_map;
typedef map<symbol, var *, symbol_hash_proc, symbol_eq_proc> var_map;
ast_manager & m_manager;
op_map m_builtin;
var_map m_vars;
expr_ref_vector m_exprs;
expr * parse_expr(scanner & s);
public:
simple_parser(ast_manager & m);
virtual ~simple_parser();
void add_builtin_op(symbol const & s, family_id fid, decl_kind kind);
void add_builtin_op(char const * str, family_id fid, decl_kind kind);
void add_var(symbol const & s, var * v);
void add_var(char const * str, var * v);
void reset();
void reset_vars();
bool parse(std::istream & in, expr_ref & result);
bool parse_string(char const * str, expr_ref & result);
bool parse_file(char const * file, expr_ref & result);
virtual expr * parse_int(rational const & r) { throw parser_error(); }
virtual expr * parse_float(rational const & r) { throw parser_error(); }
};
#endif /* _SIMPLE_PARSER_H_ */