From 89971e2a98e513a7516d84b09609dd8997337b5b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Nov 2017 10:37:30 -0800
Subject: [PATCH] remove smtlib1 dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_project.py | 3 +-
src/CMakeLists.txt | 1 -
src/api/CMakeLists.txt | 1 -
src/api/api_context.cpp | 37 -
src/api/api_context.h | 12 +-
src/api/api_interp.cpp | 30 +-
src/api/api_parsers.cpp | 222 +--
src/api/z3_api.h | 106 +-
src/parsers/smt/CMakeLists.txt | 8 -
src/parsers/smt/smtlib.cpp | 258 ---
src/parsers/smt/smtlib.h | 232 ---
src/parsers/smt/smtlib_solver.cpp | 119 --
src/parsers/smt/smtlib_solver.h | 48 -
src/parsers/smt/smtparser.cpp | 2760 -----------------------------
src/parsers/smt/smtparser.h | 48 -
src/shell/main.cpp | 11 +-
src/shell/smtlib_frontend.cpp | 38 +-
src/test/quant_elim.cpp | 7 +-
18 files changed, 23 insertions(+), 3918 deletions(-)
delete mode 100644 src/parsers/smt/CMakeLists.txt
delete mode 100644 src/parsers/smt/smtlib.cpp
delete mode 100644 src/parsers/smt/smtlib.h
delete mode 100644 src/parsers/smt/smtlib_solver.cpp
delete mode 100644 src/parsers/smt/smtlib_solver.h
delete mode 100644 src/parsers/smt/smtparser.cpp
delete mode 100644 src/parsers/smt/smtparser.h
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 05190f217..5ab56d1c7 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -75,10 +75,9 @@ def init_project_def():
add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
- add_lib('smtparser', ['portfolio'], 'parsers/smt')
add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt')
API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_interp.h', 'z3_fpa.h', 'z3_spacer.h']
- add_lib('api', ['portfolio', 'smtparser', 'realclosure', 'interp', 'opt'],
+ add_lib('api', ['portfolio', 'realclosure', 'interp', 'opt'],
includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')
add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cfe6e5265..7cde89ae2 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -98,7 +98,6 @@ add_subdirectory(sat/sat_solver)
add_subdirectory(tactic/smtlogics)
add_subdirectory(tactic/fpa)
add_subdirectory(tactic/portfolio)
-add_subdirectory(parsers/smt)
add_subdirectory(opt)
add_subdirectory(api)
add_subdirectory(api/dll)
diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt
index a413376ac..fcdbb1651 100644
--- a/src/api/CMakeLists.txt
+++ b/src/api/CMakeLists.txt
@@ -71,5 +71,4 @@ z3_add_component(api
opt
portfolio
realclosure
- smtparser
)
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 1e3f7a0a4..73fb2c212 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -19,7 +19,6 @@ Revision History:
--*/
#include<typeinfo>
#include "api/api_context.h"
-#include "parsers/smt/smtparser.h"
#include "util/version.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
@@ -89,8 +88,6 @@ namespace api {
m_print_mode = Z3_PRINT_SMTLIB_FULL;
m_searching = false;
- m_smtlib_parser = 0;
- m_smtlib_parser_has_decls = false;
m_interruptable = 0;
m_error_handler = &default_error_handler;
@@ -111,7 +108,6 @@ namespace api {
context::~context() {
- reset_parser();
m_last_obj = 0;
u_map<api::object*>::iterator it = m_allocated_objects.begin();
while (it != m_allocated_objects.end()) {
@@ -304,39 +300,6 @@ namespace api {
}
}
-
- // ------------------------
- //
- // Parser interface for backward compatibility
- //
- // ------------------------
-
- void context::reset_parser() {
- if (m_smtlib_parser) {
- dealloc(m_smtlib_parser);
- m_smtlib_parser = 0;
- m_smtlib_parser_has_decls = false;
- m_smtlib_parser_decls.reset();
- m_smtlib_parser_sorts.reset();
- }
- SASSERT(!m_smtlib_parser_has_decls);
- }
-
- void context::extract_smtlib_parser_decls() {
- if (m_smtlib_parser) {
- if (!m_smtlib_parser_has_decls) {
- smtlib::symtable * table = m_smtlib_parser->get_benchmark()->get_symtable();
- table->get_func_decls(m_smtlib_parser_decls);
- table->get_sorts(m_smtlib_parser_sorts);
- m_smtlib_parser_has_decls = true;
- }
- }
- else {
- m_smtlib_parser_decls.reset();
- m_smtlib_parser_sorts.reset();
- }
- }
-
// ------------------------
//
// RCF manager
diff --git a/src/api/api_context.h b/src/api/api_context.h
index 6f8dc43f6..58893d1c1 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -220,19 +220,11 @@ namespace api {
// ------------------------
//
- // Parser interface for backward compatibility
+ // Parser interface
//
// ------------------------
- // TODO: move to a "parser" object visible to the external world.
- std::string m_smtlib_error_buffer;
- smtlib::parser * m_smtlib_parser;
- bool m_smtlib_parser_has_decls;
- ptr_vector<func_decl> m_smtlib_parser_decls;
- ptr_vector<sort> m_smtlib_parser_sorts;
-
- void reset_parser();
- void extract_smtlib_parser_decls();
+ std::string m_parser_error_buffer;
};
diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 416c71adf..d6f4e1128 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -510,31 +510,15 @@ extern "C" {
read_error.clear();
try {
std::string foo(filename);
- if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){
- Z3_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
- Z3_app app = Z3_to_app(ctx, assrts);
- int nconjs = Z3_get_app_num_args(ctx, app);
- assertions.resize(nconjs);
- for (int k = 0; k < nconjs; k++)
- assertions[k] = Z3_get_app_arg(ctx, app, k);
- }
- else {
- Z3_parse_smtlib_file(ctx, filename, 0, 0, 0, 0, 0, 0);
- int numa = Z3_get_smtlib_num_assumptions(ctx);
- int numf = Z3_get_smtlib_num_formulas(ctx);
- int num = numa + numf;
-
- assertions.resize(num);
- for (int j = 0; j < num; j++){
- if (j < numa)
- assertions[j] = Z3_get_smtlib_assumption(ctx, j);
- else
- assertions[j] = Z3_get_smtlib_formula(ctx, j - numa);
- }
- }
+ Z3_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
+ Z3_app app = Z3_to_app(ctx, assrts);
+ int nconjs = Z3_get_app_num_args(ctx, app);
+ assertions.resize(nconjs);
+ for (int k = 0; k < nconjs; k++)
+ assertions[k] = Z3_get_app_arg(ctx, app, k);
}
catch (...) {
- read_error << "SMTLIB parse error: " << Z3_get_smtlib_error(ctx);
+ read_error << "SMTLIB parse error: " << Z3_get_parser_error(ctx);
read_msg = read_error.str();
*error = read_msg.c_str();
return false;
diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index b3252281b..867117984 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -22,232 +22,16 @@ Revision History:
#include "api/api_util.h"
#include "cmd_context/cmd_context.h"
#include "parsers/smt2/smt2parser.h"
-#include "parsers/smt/smtparser.h"
#include "solver/solver_na2as.h"
extern "C" {
- void init_smtlib_parser(Z3_context c,
- unsigned num_sorts,
- Z3_symbol const sort_names[],
- Z3_sort const types[],
- unsigned num_decls,
- Z3_symbol const decl_names[],
- Z3_func_decl const decls[]) {
- mk_c(c)->reset_parser();
- mk_c(c)->m_smtlib_parser = smtlib::parser::create(mk_c(c)->m());
- mk_c(c)->m_smtlib_parser->initialize_smtlib();
- smtlib::symtable * table = mk_c(c)->m_smtlib_parser->get_benchmark()->get_symtable();
- for (unsigned i = 0; i < num_sorts; i++) {
- table->insert(to_symbol(sort_names[i]), to_sort(types[i]));
- }
- for (unsigned i = 0; i < num_decls; i++) {
- table->insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
- }
- }
-
- void Z3_API Z3_parse_smtlib_string(Z3_context c,
- const char * str,
- unsigned num_sorts,
- Z3_symbol const sort_names[],
- Z3_sort const sorts[],
- unsigned num_decls,
- Z3_symbol const decl_names[],
- Z3_func_decl const decls[]) {
- Z3_TRY;
- LOG_Z3_parse_smtlib_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
- scoped_ptr<std::ostringstream> outs = alloc(std::ostringstream);
- bool ok = false;
- RESET_ERROR_CODE();
- init_smtlib_parser(c, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
- mk_c(c)->m_smtlib_parser->set_error_stream(*outs);
- try {
- ok = mk_c(c)->m_smtlib_parser->parse_string(str);
- }
- catch (...) {
- ok = false;
- }
- mk_c(c)->m_smtlib_error_buffer = outs->str();
- outs = nullptr;
- if (!ok) {
- mk_c(c)->reset_parser();
- SET_ERROR_CODE(Z3_PARSER_ERROR);
- }
- Z3_CATCH;
- }
-
- void Z3_API Z3_parse_smtlib_file(Z3_context c,
- const char * file_name,
- unsigned num_sorts,
- Z3_symbol const sort_names[],
- Z3_sort const types[],
- unsigned num_decls,
- Z3_symbol const decl_names[],
- Z3_func_decl const decls[]) {
+ Z3_string Z3_API Z3_get_parser_error(Z3_context c) {
Z3_TRY;
- LOG_Z3_parse_smtlib_file(c, file_name, num_sorts, sort_names, types, num_decls, decl_names, decls);
- bool ok = false;
- RESET_ERROR_CODE();
- scoped_ptr<std::ostringstream> outs = alloc(std::ostringstream);
- init_smtlib_parser(c, num_sorts, sort_names, types, num_decls, decl_names, decls);
- mk_c(c)->m_smtlib_parser->set_error_stream(*outs);
- try {
- ok = mk_c(c)->m_smtlib_parser->parse_file(file_name);
- }
- catch(...) {
- ok = false;
- }
- mk_c(c)->m_smtlib_error_buffer = outs->str();
- outs = nullptr;
- if (!ok) {
- mk_c(c)->reset_parser();
- SET_ERROR_CODE(Z3_PARSER_ERROR);
- }
- Z3_CATCH;
- }
-
- unsigned Z3_API Z3_get_smtlib_num_formulas(Z3_context c) {
- Z3_TRY;
- LOG_Z3_get_smtlib_num_formulas(c);
- RESET_ERROR_CODE();
- if (mk_c(c)->m_smtlib_parser) {
- return mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_formulas();
- }
- SET_ERROR_CODE(Z3_NO_PARSER);
- return 0;
- Z3_CATCH_RETURN(0);
- }
-
- Z3_ast Z3_API Z3_get_smtlib_formula(Z3_context c, unsigned i) {
- Z3_TRY;
- LOG_Z3_get_smtlib_formula(c, i);
- RESET_ERROR_CODE();
- if (mk_c(c)->m_smtlib_parser) {
- if (i < mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_formulas()) {
- ast * f = mk_c(c)->m_smtlib_parser->get_benchmark()->begin_formulas()[i];
- mk_c(c)->save_ast_trail(f);
- RETURN_Z3(of_ast(f));
- }
- else {
- SET_ERROR_CODE(Z3_IOB);
- }
- }
- else {
- SET_ERROR_CODE(Z3_NO_PARSER);
- }
- RETURN_Z3(0);
- Z3_CATCH_RETURN(0);
- }
-
- unsigned Z3_API Z3_get_smtlib_num_assumptions(Z3_context c) {
- Z3_TRY;
- LOG_Z3_get_smtlib_num_assumptions(c);
- RESET_ERROR_CODE();
- if (mk_c(c)->m_smtlib_parser) {
- return mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_axioms();
- }
- SET_ERROR_CODE(Z3_NO_PARSER);
- return 0;
- Z3_CATCH_RETURN(0);
- }
-
- Z3_ast Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i) {
- Z3_TRY;
- LOG_Z3_get_smtlib_assumption(c, i);
- RESET_ERROR_CODE();
- if (mk_c(c)->m_smtlib_parser) {
- if (i < mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_axioms()) {
- ast * a = mk_c(c)->m_smtlib_parser->get_benchmark()->begin_axioms()[i];
- mk_c(c)->save_ast_trail(a);
- RETURN_Z3(of_ast(a));
- }
- else {
- SET_ERROR_CODE(Z3_IOB);
- }
- }
- else {
- SET_ERROR_CODE(Z3_NO_PARSER);
- }
- RETURN_Z3(0);
- Z3_CATCH_RETURN(0);
- }
-
- unsigned Z3_API Z3_get_smtlib_num_decls(Z3_context c) {
- Z3_TRY;
- LOG_Z3_get_smtlib_num_decls(c);
- RESET_ERROR_CODE();
- if (mk_c(c)->m_smtlib_parser) {
- mk_c(c)->extract_smtlib_parser_decls();
- return mk_c(c)->m_smtlib_parser_decls.size();
- }
- SET_ERROR_CODE(Z3_NO_PARSER);
- return 0;
- Z3_CATCH_RETURN(0);
- }
-
- Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i) {
- Z3_TRY;
- LOG_Z3_get_smtlib_decl(c, i);
+ LOG_Z3_get_parser_error(c);
RESET_ERROR_CODE();
- mk_c(c)->extract_smtlib_parser_decls();
- if (mk_c(c)->m_smtlib_parser) {
- if (i < mk_c(c)->m_smtlib_parser_decls.size()) {
- func_decl * d = mk_c(c)->m_smtlib_parser_decls[i];
- mk_c(c)->save_ast_trail(d);
- RETURN_Z3(of_func_decl(d));
- }
- else {
- SET_ERROR_CODE(Z3_IOB);
- }
- }
- else {
- SET_ERROR_CODE(Z3_NO_PARSER);
- }
- RETURN_Z3(0);
- Z3_CATCH_RETURN(0);
- }
-
- unsigned Z3_API Z3_get_smtlib_num_sorts(Z3_context c) {
- Z3_TRY;
- LOG_Z3_get_smtlib_num_sorts(c);
- RESET_ERROR_CODE();
- if (mk_c(c)->m_smtlib_parser) {
- mk_c(c)->extract_smtlib_parser_decls();
- return mk_c(c)->m_smtlib_parser_sorts.size();
- }
- SET_ERROR_CODE(Z3_NO_PARSER);
- return 0;
- Z3_CATCH_RETURN(0);
- }
-
- Z3_sort Z3_API Z3_get_smtlib_sort(Z3_context c, unsigned i) {
- Z3_TRY;
- LOG_Z3_get_smtlib_sort(c, i);
- RESET_ERROR_CODE();
- if (mk_c(c)->m_smtlib_parser) {
- mk_c(c)->extract_smtlib_parser_decls();
- if (i < mk_c(c)->m_smtlib_parser_sorts.size()) {
- sort* s = mk_c(c)->m_smtlib_parser_sorts[i];
- mk_c(c)->save_ast_trail(s);
- RETURN_Z3(of_sort(s));
- }
- else {
- SET_ERROR_CODE(Z3_IOB);
- }
- }
- else {
- SET_ERROR_CODE(Z3_NO_PARSER);
- }
- RETURN_Z3(0);
- Z3_CATCH_RETURN(0);
- }
-
- Z3_string Z3_API Z3_get_smtlib_error(Z3_context c) {
- Z3_TRY;
- LOG_Z3_get_smtlib_error(c);
- RESET_ERROR_CODE();
- return mk_c(c)->m_smtlib_error_buffer.c_str();
+ return mk_c(c)->m_parser_error_buffer.c_str();
Z3_CATCH_RETURN("");
}
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index cf1c8fca7..56d9f69b7 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -5228,115 +5228,13 @@ extern "C" {
Z3_symbol const decl_names[],
Z3_func_decl const decls[]);
- /**
- \brief Parse the given string using the SMT-LIB parser.
-
- The symbol table of the parser can be initialized using the given sorts and declarations.
- The symbols in the arrays \c sort_names and \c decl_names don't need to match the names
- of the sorts and declarations in the arrays \c sorts and \c decls. This is an useful feature
- since we can use arbitrary names to reference sorts and declarations defined using the C API.
-
- The formulas, assumptions and declarations defined in \c str can be extracted using the functions:
- #Z3_get_smtlib_num_formulas, #Z3_get_smtlib_formula, #Z3_get_smtlib_num_assumptions, #Z3_get_smtlib_assumption,
- #Z3_get_smtlib_num_decls, and #Z3_get_smtlib_decl.
-
- def_API('Z3_parse_smtlib_string', VOID, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL)))
- */
- void Z3_API Z3_parse_smtlib_string(Z3_context c,
- Z3_string str,
- unsigned num_sorts,
- Z3_symbol const sort_names[],
- Z3_sort const sorts[],
- unsigned num_decls,
- Z3_symbol const decl_names[],
- Z3_func_decl const decls[]
- );
-
- /**
- \brief Similar to #Z3_parse_smtlib_string, but reads the benchmark from a file.
-
- def_API('Z3_parse_smtlib_file', VOID, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL)))
- */
- void Z3_API Z3_parse_smtlib_file(Z3_context c,
- Z3_string file_name,
- unsigned num_sorts,
- Z3_symbol const sort_names[],
- Z3_sort const sorts[],
- unsigned num_decls,
- Z3_symbol const decl_names[],
- Z3_func_decl const decls[]
- );
-
- /**
- \brief Return the number of SMTLIB formulas parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
-
- def_API('Z3_get_smtlib_num_formulas', UINT, (_in(CONTEXT), ))
- */
- unsigned Z3_API Z3_get_smtlib_num_formulas(Z3_context c);
-
- /**
- \brief Return the i-th formula parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
-
- \pre i < Z3_get_smtlib_num_formulas(c)
-
- def_API('Z3_get_smtlib_formula', AST, (_in(CONTEXT), _in(UINT)))
- */
- Z3_ast Z3_API Z3_get_smtlib_formula(Z3_context c, unsigned i);
-
- /**
- \brief Return the number of SMTLIB assumptions parsed by #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
-
- def_API('Z3_get_smtlib_num_assumptions', UINT, (_in(CONTEXT), ))
- */
- unsigned Z3_API Z3_get_smtlib_num_assumptions(Z3_context c);
-
- /**
- \brief Return the i-th assumption parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
-
- \pre i < Z3_get_smtlib_num_assumptions(c)
-
- def_API('Z3_get_smtlib_assumption', AST, (_in(CONTEXT), _in(UINT)))
- */
- Z3_ast Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i);
-
- /**
- \brief Return the number of declarations parsed by #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
-
- def_API('Z3_get_smtlib_num_decls', UINT, (_in(CONTEXT), ))
- */
- unsigned Z3_API Z3_get_smtlib_num_decls(Z3_context c);
-
- /**
- \brief Return the i-th declaration parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
-
- \pre i < Z3_get_smtlib_num_decls(c)
-
- def_API('Z3_get_smtlib_decl', FUNC_DECL, (_in(CONTEXT), _in(UINT)))
- */
- Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i);
-
- /**
- \brief Return the number of sorts parsed by #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
-
- def_API('Z3_get_smtlib_num_sorts', UINT, (_in(CONTEXT), ))
- */
- unsigned Z3_API Z3_get_smtlib_num_sorts(Z3_context c);
-
- /**
- \brief Return the i-th sort parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
-
- \pre i < Z3_get_smtlib_num_sorts(c)
-
- def_API('Z3_get_smtlib_sort', SORT, (_in(CONTEXT), _in(UINT)))
- */
- Z3_sort Z3_API Z3_get_smtlib_sort(Z3_context c, unsigned i);
/**
\brief Retrieve that last error message information generated from parsing.
- def_API('Z3_get_smtlib_error', STRING, (_in(CONTEXT), ))
+ def_API('Z3_get_parser_error', STRING, (_in(CONTEXT), ))
*/
- Z3_string Z3_API Z3_get_smtlib_error(Z3_context c);
+ Z3_string Z3_API Z3_get_parser_error(Z3_context c);
/*@}*/
/** @name Error Handling */
diff --git a/src/parsers/smt/CMakeLists.txt b/src/parsers/smt/CMakeLists.txt
deleted file mode 100644
index 2edf7b679..000000000
--- a/src/parsers/smt/CMakeLists.txt
+++ /dev/null
@@ -1,8 +0,0 @@
-z3_add_component(smtparser
- SOURCES
- smtlib.cpp
- smtlib_solver.cpp
- smtparser.cpp
- COMPONENT_DEPENDENCIES
- portfolio
-)
diff --git a/src/parsers/smt/smtlib.cpp b/src/parsers/smt/smtlib.cpp
deleted file mode 100644
index 71dd48156..000000000
--- a/src/parsers/smt/smtlib.cpp
+++ /dev/null
@@ -1,258 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-
-#include "parsers/smt/smtlib.h"
-#include "ast/ast_pp.h"
-#include "ast/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_uninterpreted_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
-}
diff --git a/src/parsers/smt/smtlib.h b/src/parsers/smt/smtlib.h
deleted file mode 100644
index f037e3d74..000000000
--- a/src/parsers/smt/smtlib.h
+++ /dev/null
@@ -1,232 +0,0 @@
-/*++
-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/ast.h"
-#include "util/symbol_table.h"
-#include "util/map.h"
-#include "ast/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
diff --git a/src/parsers/smt/smtlib_solver.cpp b/src/parsers/smt/smtlib_solver.cpp
deleted file mode 100644
index 339be2ddd..000000000
--- a/src/parsers/smt/smtlib_solver.cpp
+++ /dev/null
@@ -1,119 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
- smtlib_solver.cpp
-
-Abstract:
-
- SMT based solver.
-
-Author:
-
- Nikolaj Bjorner (nbjorner) 2006-11-3.
-
-Revision History:
-
---*/
-
-#include "parsers/smt/smtparser.h"
-#include "parsers/smt/smtlib_solver.h"
-#include "util/warning.h"
-#include "ast/ast_pp.h"
-#include "ast/ast_ll_pp.h"
-#include "ast/well_sorted.h"
-#include "model/model.h"
-#include "model/model_v2_pp.h"
-#include "solver/solver.h"
-#include "tactic/portfolio/smt_strategic_solver.h"
-#include "cmd_context/cmd_context.h"
-#include "model/model_params.hpp"
-#include "parsers/util/parser_params.hpp"
-
-namespace smtlib {
-
- solver::solver():
- m_ast_manager(m_params.m_proof ? PGM_ENABLED : PGM_DISABLED,
- m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0),
- m_ctx(0),
- m_error_code(0) {
- parser_params ps;
- m_parser = parser::create(m_ast_manager, ps.ignore_user_patterns());
- 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, true, &m_ast_manager, benchmark.get_logic());
- m_ctx->set_solver_factory(mk_smt_strategic_solver_factory());
- 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_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_params p;
- model_v2_pp(std::cout, *(md.get()), p.partial());
- }
- }
- else {
- m_error_code = ERR_UNKNOWN_RESULT;
- }
- }
-};
diff --git a/src/parsers/smt/smtlib_solver.h b/src/parsers/smt/smtlib_solver.h
deleted file mode 100644
index 6288c360b..000000000
--- a/src/parsers/smt/smtlib_solver.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*++
-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 "parsers/smt/smtparser.h"
-#include "cmd_context/context_params.h"
-#include "util/lbool.h"
-
-class cmd_context;
-
-namespace smtlib {
- class solver {
- context_params m_params;
- ast_manager m_ast_manager;
- cmd_context * m_ctx;
- scoped_ptr<parser> m_parser;
- unsigned m_error_code;
- public:
- solver();
- ~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
diff --git a/src/parsers/smt/smtparser.cpp b/src/parsers/smt/smtparser.cpp
deleted file mode 100644
index 15f094e33..000000000
--- a/src/parsers/smt/smtparser.cpp
+++ /dev/null
@@ -1,2760 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
- smtparser.cpp
-
-Abstract:
-
- SMT parser into ast.
-
-Author:
-
- Nikolaj Bjorner (nbjorner) 2006-10-4.
- Leonardo de Moura (leonardo)
-
-Revision History:
---*/
-#include<iostream>
-#include<istream>
-#include<fstream>
-#include<sstream>
-#include<signal.h>
-#include "util/region.h"
-#include "parsers/util/scanner.h"
-#include "util/symbol.h"
-#include "util/vector.h"
-#include "util/symbol_table.h"
-#include "parsers/smt/smtlib.h"
-#include "parsers/smt/smtparser.h"
-#include "ast/ast_pp.h"
-#include "ast/bv_decl_plugin.h"
-#include "ast/array_decl_plugin.h"
-#include "util/warning.h"
-#include "util/error_codes.h"
-#include "parsers/util/pattern_validation.h"
-#include "ast/rewriter/var_subst.h"
-#include "ast/well_sorted.h"
-#include "util/str_hashtable.h"
-#include "util/stopwatch.h"
-
-class id_param_info {
- symbol m_string;
- unsigned m_num_params;
- parameter m_params[0];
-public:
- id_param_info(symbol const& s, unsigned n, parameter const* p) : m_string(s), m_num_params(n) {
- for (unsigned i = 0; i < n; ++i) {
- new (&(m_params[i])) parameter();
- m_params[i] = p[i];
- }
- }
- symbol string() const { return m_string; }
- parameter * params() { return m_params; }
- unsigned num_params() const { return m_num_params; }
-};
-
-class proto_region {
- ptr_vector<rational> m_rationals;
- ptr_vector<id_param_info> m_id_infos;
- region m_region;
-public:
- proto_region() { }
-
- ~proto_region() { reset(); }
-
- rational* allocate(rational const & n) {
- rational* r = alloc(rational, n);
- m_rationals.push_back(r);
- return r;
- }
-
- id_param_info* allocate(vector<parameter> const& params, symbol const & s) {
- unsigned size = sizeof(id_param_info) + sizeof(parameter)*(params.size());
- id_param_info* r = static_cast<id_param_info*>(m_region.allocate(size));
- new (r) id_param_info(s, params.size(), params.c_ptr());
- m_id_infos.push_back(r);
- return r;
- }
-
- void* allocate(size_t s) { return m_region.allocate(s); }
-
- void reset() {
- for (unsigned i = 0; i < m_rationals.size(); ++i) {
- dealloc(m_rationals[i]);
- }
- for (unsigned i = 0; i < m_id_infos.size(); ++i) {
- unsigned n = m_id_infos[i]->num_params();
- for (unsigned j = 0; j < n; ++j) {
- m_id_infos[i]->params()[j].~parameter();
- }
- }
- m_rationals.reset();
- m_id_infos.reset();
- m_region.reset();
- }
-
-private:
-
-};
-
-inline void * operator new(size_t s, proto_region& r) { return r.allocate(s); }
-inline void * operator new[](size_t s, proto_region & r) { return r.allocate(s); }
-inline void operator delete(void*, proto_region& r) {}
-inline void operator delete[](void *, proto_region& r) {}
-
-class proto_expr {
-public:
-
- enum kind_t {
- ID,
- STRING,
- COMMENT,
- ANNOTATION,
- INT,
- FLOAT,
- CONS
- };
-private:
-
- int m_kind:8;
- int m_line:24;
- int m_pos;
- union {
- id_param_info* m_id_info;
- rational* m_number;
- proto_expr** m_children;
- };
-
-public:
-
- symbol string() {
- if (m_kind == INT || m_kind == FLOAT) {
- std::string s = m_number->to_string();
- return symbol(s.c_str());
- }
- if (m_kind == CONS) {
- return symbol("");
- }
- SASSERT(m_kind == STRING || m_kind == COMMENT || m_kind == ID || m_kind == ANNOTATION);
- return m_id_info->string();
- }
-
- rational const& number() {
- SASSERT(m_kind == INT || m_kind == FLOAT);
- return *m_number;
- }
-
- proto_expr* const* children() const {
- if (m_kind == CONS) {
- return m_children;
- }
- else {
- return 0;
- }
- }
-
- int line() { return m_line; }
- int pos() { return m_pos; }
- kind_t kind() { return static_cast<kind_t>(m_kind); }
-
- unsigned num_params() const {
- SASSERT(m_kind == ID);
- return m_id_info->num_params();
- }
-
- parameter * params() {
- SASSERT(m_kind == ID);
- return m_id_info->params();
- }
-
- proto_expr(proto_region & region, kind_t kind, symbol const & s, vector<parameter> const & params, int line, int pos):
- m_kind(kind),
- m_line(line),
- m_pos(pos),
- m_id_info(region.allocate(params, s)) {
- SASSERT(kind != CONS);
- SASSERT(kind != INT);
- SASSERT(kind != FLOAT);
- }
-
- proto_expr(proto_region& region, bool is_int, rational const & n, int line, int pos):
- m_kind(is_int?INT:FLOAT),
- m_line(line),
- m_pos(pos),
- m_number(region.allocate(n))
- {}
-
- proto_expr(proto_region& region, ptr_vector<proto_expr>& proto_exprs, int line, int pos):
- m_kind(CONS),
- m_line(line),
- m_pos(pos) {
- //
- // null terminated list of proto_expression pointers.
- //
- unsigned num_children = proto_exprs.size();
- m_children = new (region) proto_expr*[num_children+1];
- for (unsigned i = 0; i < num_children; ++i) {
- m_children[i] = proto_exprs[i];
- }
- m_children[num_children] = 0;
- }
-
- ~proto_expr() {}
-
-
- static proto_expr* copy(proto_region& r, proto_expr* e) {
- switch(e->kind()) {
- case proto_expr::CONS: {
- ptr_vector<proto_expr> args;
- proto_expr* const* children = e->children();
- while (children && *children) {
- args.push_back(copy(r, *children));
- ++children;
- }
- return new (r) proto_expr(r, args, e->line(), e->pos());
- }
- case proto_expr::INT: {
- return new (r) proto_expr(r, true, e->number(), e->line(), e->pos());
- }
- case proto_expr::FLOAT: {
- return new (r) proto_expr(r, false, e->number(), e->line(), e->pos());
- }
- case proto_expr::ID: {
- vector<parameter> params;
- for (unsigned i = 0; i < e->num_params(); ++i) {
- params.push_back(e->params()[i]);
- }
- return new (r) proto_expr(r, e->kind(), e->string(), params, e->line(), e->pos());
- }
- default: {
- vector<parameter> params;
- return new (r) proto_expr(r, e->kind(), e->string(), params, e->line(), e->pos());
- }
- }
- }
-
-private:
-
- proto_expr(proto_expr const & other);
- proto_expr& operator=(proto_expr const & other);
-};
-
-
-//
-// build up proto_expr tree from token stream.
-//
-
-class proto_expr_parser {
- proto_region& m_region;
- scanner& m_scanner;
- std::ostream& m_err;
- bool m_at_eof;
-public:
- proto_expr_parser(proto_region& region, scanner& scanner, std::ostream& err):
- m_region(region),
- m_scanner(scanner),
- m_err(err),
- m_at_eof(false) {
- }
-
- ~proto_expr_parser() {}
-
- bool parse(ptr_vector<proto_expr> & proto_exprs, bool parse_single_expr = false) {
- scanner::token token;
- vector<frame> stack;
- proto_expr* result = 0;
-
- stack.push_back(frame(PROTO_EXPRS_PRE));
-
- token = m_scanner.scan();
-
- if (token == scanner::EOF_TOKEN) {
- proto_exprs.reset();
- return true;
- }
-
- while (!stack.empty()) {
-
- if (token == scanner::EOF_TOKEN) {
- break;
- }
-
- if (token == scanner::ERROR_TOKEN) {
- print_error("unexpected token");
- goto done;
- }
-
- switch(stack.back().m_state) {
-
- case PROTO_EXPR:
- switch (token) {
- case scanner::LEFT_PAREN:
- stack.back().m_state = PROTO_EXPRS_PRE;
- token = m_scanner.scan();
- break;
- default:
- stack.back().m_state = ATOM;
- break;
- }
- break;
-
- case ATOM:
- SASSERT(!result);
- switch(token) {
- case scanner::ID_TOKEN:
- result = new (m_region) proto_expr(m_region, proto_expr::ID, m_scanner.get_id(), m_scanner.get_params(),
- m_scanner.get_line(), m_scanner.get_pos());
- break;
- case scanner::INT_TOKEN:
- result = new (m_region) proto_expr(m_region, true, m_scanner.get_number(), m_scanner.get_line(),
- m_scanner.get_pos());
- break;
- case scanner::FLOAT_TOKEN:
- result = new (m_region) proto_expr(m_region, false, m_scanner.get_number(), m_scanner.get_line(),
- m_scanner.get_pos());
- break;
- case scanner::STRING_TOKEN:
- result = new (m_region) proto_expr(m_region, proto_expr::STRING, m_scanner.get_id(), m_scanner.get_params(),
- m_scanner.get_line(), m_scanner.get_pos());
- break;
- case scanner::COMMENT_TOKEN:
- result = new (m_region) proto_expr(m_region, proto_expr::COMMENT, m_scanner.get_id(), m_scanner.get_params(),
- m_scanner.get_line(), m_scanner.get_pos());
- break;
- case scanner::COLON:
- token = m_scanner.scan();
- if (token == scanner::ID_TOKEN) {
- result = new (m_region) proto_expr(m_region, proto_expr::ANNOTATION, m_scanner.get_id(),
- m_scanner.get_params(), m_scanner.get_line(), m_scanner.get_pos());
- }
- else {
- print_error("unexpected identifier ':'");
- token = scanner::ERROR_TOKEN;
- goto done;
- }
- break;
- default:
- print_error("unexpected token");
- token = scanner::ERROR_TOKEN;
- goto done;
- }
- stack.pop_back();
- SASSERT(!stack.empty());
- stack.back().m_proto_exprs.push_back(result);
- result = 0;
- if (parse_single_expr && stack.size() == 1) {
- goto done;
- }
- token = m_scanner.scan();
- break;
-
- case PROTO_EXPRS_PRE:
- SASSERT(!result);
- switch(token) {
- case scanner::RIGHT_PAREN:
- result = new (m_region) proto_expr(m_region, stack.back().m_proto_exprs, m_scanner.get_line(),
- m_scanner.get_pos());
- stack.pop_back();
-
- if (stack.empty()) {
- print_error("unexpected right parenthesis");
- token = scanner::ERROR_TOKEN;
- result = 0;
- goto done;
- }
- stack.back().m_proto_exprs.push_back(result);
- if (parse_single_expr && stack.size() == 1) {
- goto done;
- }
- result = 0;
- token = m_scanner.scan();
- break;
-
- case scanner::EOF_TOKEN:
- m_at_eof = true;
- break;
-
- case scanner::ERROR_TOKEN:
- print_error("could not parse expression");
- goto done;
-
- default:
- stack.back().m_state = PROTO_EXPRS_POST;
- stack.push_back(frame(PROTO_EXPR));
- break;
- }
- break;
-
- case PROTO_EXPRS_POST:
- stack.back().m_state = PROTO_EXPRS_PRE;
- break;
- }
- }
-
- done:
-
- if (stack.size() == 1) {
- for (unsigned i = 0; i < stack.back().m_proto_exprs.size(); ++i) {
- proto_exprs.push_back(stack.back().m_proto_exprs[i]);
- }
- return true;
- }
-
- if (stack.size() == 2) {
- proto_exprs.push_back(new (m_region) proto_expr(m_region, stack.back().m_proto_exprs, m_scanner.get_line(),
- m_scanner.get_pos()));
- return true;
- }
-
- print_error("unexpected nesting of parenthesis: ", stack.size());
- return false;
- }
-
- int get_line() {
- return m_scanner.get_line();
- }
-
- bool at_eof() const {
- return m_at_eof;
- }
-
-private:
-
- template<typename T>
- void print_error(char const* msg1, T msg2) {
- m_err << "ERROR: line " << m_scanner.get_line()
- << " column " << m_scanner.get_pos() << ": "
- << msg1 << msg2 << "\n";
- }
-
- void print_error(char const* msg) {
- print_error(msg, "");
- }
-
- // stack frame:
- enum frame_state {
- PROTO_EXPR,
- PROTO_EXPRS_PRE,
- PROTO_EXPRS_POST,
- ATOM
- };
-
- class frame {
- public:
- frame_state m_state;
- ptr_vector<proto_expr> m_proto_exprs;
- frame(frame_state state):
- m_state(state){
- }
- frame(frame const & other):
- m_state(other.m_state),
- m_proto_exprs(other.m_proto_exprs) {
- }
- private:
- frame& operator=(frame const &);
- };
-
-};
-
-using namespace smtlib;
-
-class idbuilder {
-public:
- virtual ~idbuilder() {}
- virtual bool apply(expr_ref_vector const & args, expr_ref & result) = 0;
-};
-
-class builtin_sort_builder : public sort_builder {
- ast_manager& m_manager;
- family_id m_fid;
- decl_kind m_kind;
-public:
- builtin_sort_builder(ast_manager& m, family_id fid, decl_kind k) :
- m_manager(m), m_fid(fid), m_kind(k) {}
-
- virtual bool apply(unsigned num_params, parameter const* params, sort_ref & result) {
- result = m_manager.mk_sort(m_fid, m_kind, num_params, params);
- return result.get() != 0;
- }
-};
-
-class array_sort : public builtin_sort_builder {
-public:
- array_sort(ast_manager& m) :
- builtin_sort_builder(m, m.mk_family_id("array"), ARRAY_SORT) {}
-};
-
-class bv_sort : public builtin_sort_builder {
-public:
- bv_sort(ast_manager& m) :
- builtin_sort_builder(m, m.mk_family_id("bv"), BV_SORT) {}
-};
-
-class user_sort : public sort_builder {
- user_sort_plugin * m_plugin;
- decl_kind m_kind;
- symbol m_name;
- unsigned m_num_args;
- std::string m_error_message;
-public:
- user_sort(ast_manager& m, unsigned num_args, symbol name):
- m_name(name),
- m_num_args(num_args) {
- m_plugin = m.get_user_sort_plugin();
- m_kind = m_plugin->register_name(name);
- }
-
- ~user_sort() {}
-
- virtual bool apply(unsigned num_params, parameter const* params, sort_ref & result) {
- if (num_params != m_num_args) {
- std::ostringstream strm;
- strm << "wrong number of arguments passed to " << m_name << " "
- << m_num_args << " expected, but " << num_params << " given";
- m_error_message = strm.str();
- return false;
- }
- result = m_plugin->mk_sort(m_kind, num_params, params);
- return true;
- }
-
- virtual char const* error_message() {
- return m_error_message.c_str();
- }
-};
-
-class smtparser : public parser {
- 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) {}
- };
-
- class add_plugins {
-
- public:
- add_plugins(ast_manager& m) {
-#define REGISTER_PLUGIN(NAME, MK) { \
- family_id fid = m.mk_family_id(symbol(NAME)); \
- if (!m.has_plugin(fid)) { \
- m.register_plugin(fid, MK); \
- } \
- } ((void) 0)
-
- REGISTER_PLUGIN("arith", alloc(arith_decl_plugin));
- REGISTER_PLUGIN("bv", alloc(bv_decl_plugin));
- REGISTER_PLUGIN("array", alloc(array_decl_plugin));
-
- };
- };
-
- ast_manager& m_manager;
- add_plugins m_plugins;
- arith_util m_anum_util;
- bv_util m_bvnum_util;
- pattern_validator m_pattern_validator;
- bool m_ignore_user_patterns;
- unsigned m_binding_level; // scope level for bound vars
- benchmark m_benchmark; // currently parsed benchmark
-
- typedef map<symbol, builtin_op, symbol_hash_proc, symbol_eq_proc> op_map;
- op_map m_builtin_ops;
- op_map m_builtin_sorts;
-
- symbol m_let; // commonly used symbols.
- symbol m_flet;
- symbol m_forall;
- symbol m_exists;
- symbol m_lblneg;
- symbol m_lblpos;
- symbol m_associative;
- symbol m_commutative;
- symbol m_injective;
- symbol m_sorts;
- symbol m_funs;
- symbol m_preds;
- symbol m_axioms;
- symbol m_notes;
- symbol m_array;
- symbol m_bang;
- symbol m_underscore;
- sort* m_int_sort;
- sort* m_real_sort;
- family_id m_bv_fid;
- family_id m_arith_fid;
- family_id m_array_fid;
- family_id m_rel_fid;
- func_decl * m_sk_hack;
- std::ostream* m_err;
- bool m_display_error_for_vs;
-
-
-public:
-
- smtparser(ast_manager& m, bool ignore_user_patterns):
- m_manager(m),
- m_plugins(m),
- m_anum_util(m),
- m_bvnum_util(m),
- m_pattern_validator(m),
- m_ignore_user_patterns(ignore_user_patterns),
- m_binding_level(0),
- m_benchmark(m_manager, symbol("")),
- m_let("let"),
- m_flet("flet"),
- m_forall("forall"),
- m_exists("exists"),
- m_lblneg("lblneg"),
- m_lblpos("lblpos"),
- m_associative("assoc"),
- m_commutative("comm"),
- m_injective("injective"),
- m_sorts("sorts"),
- m_funs("funs"),
- m_preds("preds"),
- m_axioms("axioms"),
- m_notes("notes"),
- m_array("array"),
- m_bang("!"),
- m_underscore("_"),
- m_err(0),
- m_display_error_for_vs(false)
- {
- family_id bfid = m_manager.get_basic_family_id();
-
- add_builtin_type("bool", bfid, BOOL_SORT);
- m_benchmark.get_symtable()->insert(symbol("Array"), alloc(array_sort, m));
- m_benchmark.get_symtable()->insert(symbol("BitVec"), alloc(bv_sort, m));
-
-
- add_builtins(bfid);
- }
-
- ~smtparser() {
- }
-
- void set_error_stream(std::ostream& strm) { m_err = &strm; }
-
- std::ostream& get_err() { return m_err?(*m_err):std::cerr; }
-
- bool ignore_user_patterns() const { return m_ignore_user_patterns; }
-
- bool parse_stream(std::istream& stream) {
- proto_region region;
- scanner scanner(stream, get_err(), false);
- proto_expr_parser parser(region, scanner, get_err());
- return parse(parser);
- }
-
- bool parse_file(char const * filename) {
- if (filename != 0) {
- std::ifstream stream(filename);
- if (!stream) {
- get_err() << "ERROR: could not open file '" << filename << "'.\n";
- return false;
- }
- return parse_stream(stream);
- }
- else {
- return parse_stream(std::cin);
- }
- }
-
- bool parse_string(char const * str) {
- std::string s = str;
- std::istringstream is(s);
- return parse_stream(is);
- }
-
- void add_builtin_op(char const * s, family_id fid, decl_kind k) {
- m_builtin_ops.insert(symbol(s), builtin_op(fid, k));
- }
-
- void add_builtin_type(char const * s, family_id fid, decl_kind k) {
- m_builtin_sorts.insert(symbol(s), builtin_op(fid, k));
- }
-
- void initialize_smtlib() {
- smtlib::symtable* table = m_benchmark.get_symtable();
-
- symbol arith("arith");
- family_id afid = m_manager.mk_family_id(arith);
- m_arith_fid = afid;
-
- add_builtin_type("Int", afid, INT_SORT);
- add_builtin_type("Real", afid, REAL_SORT);
- add_builtin_type("Bool", m_manager.get_basic_family_id(), BOOL_SORT);
-
- m_int_sort = m_manager.mk_sort(m_arith_fid, INT_SORT);
- m_real_sort = m_manager.mk_sort(m_arith_fid, REAL_SORT);
-
- add_builtins(afid);
-
- symbol bv("bv");
- family_id bfid = m_manager.mk_family_id(bv);
- m_bv_fid = bfid;
-
- add_builtins(bfid);
-
- add_builtin_type("BitVec", bfid, BV_SORT);
-
- symbol array("array");
- afid = m_manager.mk_family_id(array);
- m_array_fid = afid;
-
- add_builtins(afid);
-
- sort* a1, *a2;
- func_decl* store1, *sel1, *store2, *sel2;
-
- // Array
- parameter params0[2] = { parameter(m_int_sort), parameter(m_int_sort) };
- a1 = m_manager.mk_sort(afid, ARRAY_SORT, 2, params0);
- table->insert(symbol("Array"), a1);
- parameter param0(a1);
- sort * args0[3] = { a1, m_int_sort, m_int_sort };
- store1 = m_manager.mk_func_decl(afid, OP_STORE, 0, 0, 3, args0);
- table->insert(symbol("store"), store1);
- sel1 = m_manager.mk_func_decl(afid, OP_SELECT, 0, 0, 2, args0);
- table->insert(symbol("select"), sel1);
-
- // Array1
- parameter params1[2] = { parameter(m_int_sort), parameter(m_real_sort) };
- a1 = m_manager.mk_sort(afid, ARRAY_SORT, 2, params1);
- table->insert(symbol("Array1"), a1);
- parameter param1(a1);
- sort * args1[3] = { a1, m_int_sort, m_real_sort };
- store1 = m_manager.mk_func_decl(afid, OP_STORE, 0, 0, 3, args1);
- table->insert(symbol("store"), store1);
- sel1 = m_manager.mk_func_decl(afid, OP_SELECT, 0, 0, 2, args1);
- table->insert(symbol("select"), sel1);
-
- // Array2
- parameter params2[2] = { parameter(m_int_sort), parameter(a1) };
- a2 = m_manager.mk_sort(afid, ARRAY_SORT, 2, params2);
- table->insert(symbol("Array2"), a2);
- parameter param2(a2);
- sort * args2[3] = { a2, m_int_sort, a1 };
- store2 = m_manager.mk_func_decl(afid, OP_STORE, 0, 0, 3, args2);
- table->insert(symbol("store"), store2);
- sel2 = m_manager.mk_func_decl(afid, OP_SELECT, 0, 0, 2, args2);
- table->insert(symbol("select"), sel2);
-
- m_benchmark.declare_sort(symbol("U"));
-
- sort * bool_sort = m_manager.mk_bool_sort();
- m_sk_hack = m_manager.mk_func_decl(symbol("sk_hack"), 1, &bool_sort, bool_sort);
- table->insert(symbol("sk_hack"), m_sk_hack);
- }
-
-
- void add_builtins(family_id fid) {
- decl_plugin * plugin = m_manager.get_plugin(fid);
- SASSERT(plugin);
- svector<builtin_name> op_names;
- plugin->get_op_names(op_names);
- for (unsigned i = 0; i < op_names.size(); ++i) {
- add_builtin_op(op_names[i].m_name.bare_str(), fid, op_names[i].m_kind);
- }
- }
-
- smtlib::benchmark* get_benchmark() { return &m_benchmark; }
-
-private:
-
-
- bool parse(proto_expr_parser& parser) {
- symbol benchmark("benchmark");
- symbol name("");
- proto_expr* const* rest = 0;
- ptr_vector<proto_expr> proto_exprs;
- bool result = parser.parse(proto_exprs);
- proto_expr* proto_expr = 0;
-
- if (!result) {
- get_err() << "ERROR: parse error at line " << parser.get_line() << ".\n";
- }
-
- for (unsigned i = 0; result && i < proto_exprs.size(); ++i) {
-
- proto_expr = proto_exprs[i];
-
- if (match_cons(proto_expr, benchmark, name, rest)) {
- result = make_benchmark(name, rest);
- }
- else if (proto_expr && proto_expr->kind() != proto_expr::COMMENT) {
- set_error("could not match expression to benchmark ", proto_expr);
- }
- else {
- // proto_expr->kind() == proto_expr::COMMENT.
- }
- }
- return result;
- }
-
- void error_prefix(proto_expr* e) {
- if (m_display_error_for_vs) {
- if (e) {
- get_err() << "Z3(" << e->line() << "," << e->pos() << "): ERROR: ";
- }
- }
- else {
- get_err() << "ERROR: ";
- if (e) {
- get_err() << "line " << e->line() << " column " << e->pos() << ": ";
- }
- }
- }
-
- void set_error(char const * str, proto_expr* e) {
- error_prefix(e);
- if (e->kind() == proto_expr::ID) {
- get_err() << str << " '" << e->string() << "'.\n";
- }
- else {
- get_err() << str << ".\n";
- }
- }
-
- template<typename T1, typename T2>
- void set_error(T1 str1, T2 str2, proto_expr* e) {
- error_prefix(e);
- get_err() << str1 << " " << str2 << ".\n";
- }
-
- template<typename T1, typename T2, typename T3>
- void set_error(T1 str1, T2 str2, T3 str3, proto_expr* e) {
- error_prefix(e);
- get_err() << str1 << str2 << str3 << ".\n";
- }
-
- bool match_cons(proto_expr * e, symbol const & sym, symbol & name, proto_expr* const*& proto_exprs) {
- if (e &&
- e->kind() == proto_expr::CONS &&
- e->children() &&
- e->children()[0] &&
- e->children()[0]->string() == sym &&
- e->children()[1]) {
- proto_exprs = e->children() + 2;
- name = e->children()[1]->string();
- return true;
- }
-
- return false;
- }
-
- bool make_benchmark(symbol & name, proto_expr * const* proto_exprs) {
- symbol extrasorts("extrasorts");
- symbol extrafuns("extrafuns");
- symbol extrapreds("extrapreds");
- symbol assumption("assumption");
- symbol assumption_core("assumption-core");
- symbol define_sorts_sym("define_sorts");
- symbol logic("logic");
- symbol formula("formula");
- symbol status("status");
- symbol sat("sat");
- symbol unsat("unsat");
- symbol unknown("unknown");
- symbol empty("");
- symbol source("source");
- symbol difficulty("difficulty");
- symbol category("category");
- bool success = true;
-
- push_benchmark(name);
-
- while (proto_exprs && *proto_exprs) {
- proto_expr* e = *proto_exprs;
- ++proto_exprs;
- proto_expr* e1 = *proto_exprs;
-
- if (logic == e->string() && e1) {
- name = e1->string();
- m_benchmark.set_logic(name);
-
- set_default_num_sort(name);
-
- if (name == symbol("QF_AX")) {
- // Hack for supporting new QF_AX theory...
- sort * index = m_manager.mk_uninterpreted_sort(symbol("Index"));
- sort * element = m_manager.mk_uninterpreted_sort(symbol("Element"));
- parameter params[2] = { parameter(index), parameter(element) };
- sort * array = m_manager.mk_sort(m_array_fid, ARRAY_SORT, 2, params);
- smtlib::symtable* table = m_benchmark.get_symtable();
- table->insert(symbol("Index"), index);
- table->insert(symbol("Element"), element);
- // overwrite Array definition...
- table->insert(symbol("Array"), array);
- sort * args[3] = { array, index, element };
- func_decl * store = m_manager.mk_func_decl(m_array_fid, OP_STORE, 0, 0, 3, args);
- table->insert(symbol("store"), store);
- func_decl * sel = m_manager.mk_func_decl(m_array_fid, OP_SELECT, 0, 0, 2, args);
- table->insert(symbol("select"), sel);
- }
-
- ++proto_exprs;
- continue;
- }
-
- if (assumption == e->string() && e1) {
- expr_ref t(m_manager);
- if (!make_expression(e1, t) ||
- !push_assumption(t.get())) {
- return false;
- }
- ++proto_exprs;
- continue;
- }
-
- if (assumption_core == e->string() && e1) {
- expr_ref t(m_manager);
- if (!make_expression(e1, t))
- return false;
- m_benchmark.add_assumption(t.get());
- ++proto_exprs;
- continue;
- }
-
- if (define_sorts_sym == e->string() && e1) {
- if (!define_sorts(e1)) {
- return false;
- }
- ++proto_exprs;
- continue;
- }
-
- if (formula == e->string() && e1) {
- expr_ref t(m_manager);
- if (!make_expression(e1, t) ||
- !push_formula(t.get())) {
- return false;
- }
- ++proto_exprs;
- continue;
- }
-
- if (status == e->string() && e1) {
- if (sat == e1->string()) {
- if (!push_status(smtlib::benchmark::SAT)) {
- set_error("could not push status ", e1->string(),e1);
- return false;
- }
- }
- else if (unsat == e1->string()) {
- if (!push_status(smtlib::benchmark::UNSAT)) {
- set_error("could not push status ", e1->string(),e1);
- return false;
- }
- }
- else if (unknown == e1->string()) {
- if (!push_status(smtlib::benchmark::UNKNOWN)) {
- set_error("could not push status ", e1->string(),e1);
- return false;
- }
- }
- else {
- set_error("could not recognize status ", e1->string(),e1);
- return false;
- }
- ++proto_exprs;
- continue;
- }
-
- if (extrasorts == e->string() && e1) {
- if (!declare_sorts(e1)) {
- return false;
- }
- ++proto_exprs;
- continue;
- }
- if (extrafuns == e->string() && e1) {
- if (!declare_funs(e1)) {
- return false;
- }
- ++proto_exprs;
- continue;
- }
- if (extrapreds == e->string() && e1) {
- if (!declare_preds(e1)) {
- return false;
- }
- ++proto_exprs;
- continue;
- }
- if (m_notes == e->string() && e1) {
- ++proto_exprs;
- continue;
- }
-
- if ((source == e->string() || difficulty == e->string() || category == e->string()) && e1) {
- ++proto_exprs;
- continue;
- }
-
- if (e->string() != empty) {
- set_error("ignoring unknown attribute '", e->string().bare_str(), "'", e);
- if (e1) {
- ++proto_exprs;
- }
- // do not fail.
- // success = false;
- continue;
- }
-
- TRACE("smtparser",
- tout << "skipping: " << e->string() << " " <<
- e->line() << " " <<
- e->pos() << ".\n";);
- continue;
- }
- return success;
- }
-
- bool is_id_token(proto_expr* expr) {
- return
- expr &&
- (expr->kind() == proto_expr::ID ||
- expr->kind() == proto_expr::STRING ||
- expr->kind() == proto_expr::ANNOTATION);
- }
-
- bool check_id(proto_expr* e) {
- return is_id_token(e);
- }
-
- bool make_expression(proto_expr * e, expr_ref & result) {
- m_binding_level = 0;
- symbol_table<idbuilder*> local_scope;
- return make_expression(local_scope, e, result);
- }
-
- bool make_func_decl(proto_expr* e, func_decl_ref& result) {
- func_decl* f;
- if (m_benchmark.get_symtable()->find1(e->string(), f)) {
- result = f;
- return true;
- }
- else {
- return false;
- }
- }
-
- bool make_bool_expression(symbol_table<idbuilder*>& local_scope, proto_expr * e, expr_ref & result) {
- if (!make_expression(local_scope, e, result)) {
- return false;
- }
- if (!m_manager.is_bool(result)) {
- set_error("expecting Boolean expression", e);
- return false;
- }
- return true;
- }
-
- bool make_bool_expressions(symbol_table<idbuilder*>& local_scope, proto_expr * const* chs, expr_ref_vector & exprs) {
- while (chs && *chs) {
- expr_ref result(m_manager);
- m_binding_level = 0;
- if (!make_bool_expression(local_scope, *chs, result)) {
- return false;
- }
- exprs.push_back(result);
- ++chs;
- }
- return true;
- }
-
- bool make_expression(symbol_table<idbuilder*>& local_scope, proto_expr * e, expr_ref & result) {
- //
- // Walk proto_expr by using the zipper.
- // That is, maintain a stack of what's
- // . left - already processed.
- // . right - to be processed.
- // . up - above the processed node.
- //
-
- region region;
-
- expr_ref_vector * left = alloc(expr_ref_vector, m_manager);
- proto_expr* const* right = 0;
- ptr_vector<parse_frame> up;
- proto_expr* current = e;
- bool success = false;
- idbuilder* builder = 0;
-
- while (true) {
-
- if (!current && right && *right) {
- //
- // pull the current from right.
- //
- current = *right;
- ++right;
- }
-
- if (!current && up.empty()) {
- //
- // we are done.
- //
- if (left->size() == 0) {
- // set_error();
- set_error("there are no expressions to return", e);
- goto cleanup;
- }
- if (left->size() != 1) {
- set_error("there are too many expressions to return", e);
- goto cleanup;
- }
- result = left->back();
- success = true;
- goto cleanup;
- }
-
- if (!current && !up.empty()) {
- //
- // There is nothing more to process at this level.
- //
- // Apply the operator on the stack to the
- // current 'left' vector.
- // Adjust the stack by popping the left and right
- // work-lists.
- //
- expr_ref term(m_manager);
- parse_frame* above = up.back();
- // symbol sym = above->get_proto_expr()->string();
-
- if (above->make_term()) {
- if (!above->make_term()->apply(*left, term)) {
- set_error("Could not create application",
- above->get_proto_expr());
- success = false;
- goto cleanup;
- }
- }
- else if (!make_app(above->get_proto_expr(), *left, term)) {
- success = false;
- goto cleanup;
- }
- dealloc(left);
- left = above->detach_left();
- left->push_back(term.get());
- right = above->right();
- m_binding_level = above->binding_level();
- up.pop_back();
- continue;
- }
-
- while (current &&
- current->kind() == proto_expr::CONS &&
- current->children() &&
- current->children()[0] &&
- !current->children()[1]) {
- current = current->children()[0];
- }
-
- switch(current->kind()) {
-
- case proto_expr::ANNOTATION:
- // ignore
- current = 0;
- break;
-
- case proto_expr::ID: {
- symbol const& id = current->string();
- expr_ref term(m_manager);
- expr * const_term = 0;
- bool ok = true;
-
- if (local_scope.find(id, builder)) {
- expr_ref_vector tmp(m_manager);
- if (!builder->apply(tmp, term)) {
- set_error("identifier supplied with the wrong number of arguments ", id, current);
- goto cleanup;
-
- }
- }
- else if (m_benchmark.get_const(id, const_term)) {
- // found.
- term = const_term;
- }
- else if (is_builtin_const(id, current, current->num_params(), current->params(), ok, term)) {
- if (!ok) goto cleanup;
- }
- else if (is_bvconst(id, current->num_params(), current->params(), term)) {
- // found
- }
- else {
- set_error("could not locate id ", id, current);
- goto cleanup;
- }
-
- left->push_back(term.get());
- current = 0;
- break;
- }
-
- case proto_expr::STRING:
- //
- // Ignore strings.
- //
- current = 0;
- break;
-
- case proto_expr::COMMENT:
- //
- // Ignore comments.
- //
- current = 0;
- break;
-
- case proto_expr::INT:
-
- left->push_back(mk_number(current->number(), true));
- current = 0;
- break;
-
- case proto_expr::FLOAT:
- left->push_back(mk_number(current->number(), false));
- current = 0;
- break;
-
- case proto_expr::CONS:
-
- if (!current->children() ||
- !current->children()[0]) {
- set_error("cons does not have children", current);
- current = 0;
- goto cleanup;
- }
-
- //
- // expect the head to be a symbol
- // which can be used to build a term of
- // the subterms.
- //
-
- symbol const& head_symbol = current->children()[0]->string();
-
- if (head_symbol == m_underscore) {
-
- expr_ref term(m_manager);
-
- proto_expr * const* chs = current->children() + 1;
- symbol const& id = chs[0]->string();
- sort_ref_vector sorts(m_manager);
- vector<parameter> params;
- bool ok = true;
- if (!parse_params(chs+1, params, sorts)) {
- goto cleanup;
- }
- if (is_builtin_const(id, current, params.size(), params.c_ptr(), ok, term)) {
- if (!ok) goto cleanup;
- }
- else if (is_bvconst(id, params.size(), params.c_ptr(), term)) {
- // ok
- }
- else {
- set_error("Could not parse _ term", current);
- goto cleanup;
- }
- left->push_back(term.get());
- current = 0;
- break;
- }
-
- if ((head_symbol == m_let) ||
- (head_symbol == m_flet)) {
-
- if (!current->children()[1] ||
- !current->children()[2]) {
- set_error("let does not have two arguments", current);
- goto cleanup;
- }
-
- proto_expr * let_binding = current->children()[1];
- proto_expr * const* let_body = current->children()+2;
-
- //
- // Collect bound variables and definitions for the bound variables
- // into vectors 'vars' and 'bound'.
- //
- svector<symbol> vars;
- ptr_vector<proto_expr> bound_vec;
- if (is_binary_let_binding(let_binding)) {
- vars.push_back(let_binding->children()[0]->string());
- bound_vec.push_back(let_binding->children()[1]);
- }
- else {
- proto_expr* const* children = let_binding->children();
- if (!children) {
- set_error("let binding does not have two arguments", let_binding);
- goto cleanup;
- }
- while (*children) {
- proto_expr* ch = *children;
- if (!is_binary_let_binding(ch)) {
- set_error("let binding does not have two arguments", ch);
- goto cleanup;
- }
- vars.push_back(ch->children()[0]->string());
- bound_vec.push_back(ch->children()[1]);
- ++children;
- }
- }
- bound_vec.push_back(0);
-
- proto_expr** bound = new (region) proto_expr*[bound_vec.size()];
- for (unsigned i = 0; i < bound_vec.size(); ++i) {
- bound[i] = bound_vec[i];
- }
-
- //
- // Let's justify the transformation that
- // pushes push_let and pop_let on the stack.
- // and how it processes the let declaration.
- //
- // walk up left ((let ((v1 x1) (v2 x2)) z)::right)
- //
- // =
- //
- // walk (up::(pop_let(),left,right)::(bind(v1,v2),[],[z])) [] [x1;x2]
- //
- // = (* assume x1 -> y1, x2 -> y2 *)
- //
- // walk (up::(pop_let(),left,right)::(bind(v1,v2),[],[z])) [y1;y2] []
- //
- // = (* apply binding *)
- //
- // walk (up::(pop_let(),left,right)) [] [z]
- //
- // = (* assume z -> u *)
- //
- // walk up {left::u] right
- //
- // so if pop_let(v) [a,b] has the effect of removing v from the environment
- // and projecting the second element "b", we obtain the effect of a let-binding.
- //
-
- expr_ref_vector * pinned = alloc(expr_ref_vector, m_manager);
- pop_let * popl = new (region) pop_let(local_scope, pinned);
- up.push_back(new (region) parse_frame(let_binding, popl, left, right, m_binding_level));
-
-
- push_let_and * pushl = new (region) push_let_and(this, region, local_scope, pinned, vars.size(), vars.c_ptr());
- expr_ref_vector * tmp = alloc(expr_ref_vector, m_manager);
- up.push_back(new (region) parse_frame(let_binding, pushl, tmp, let_body, m_binding_level));
-
-
- left = alloc(expr_ref_vector, m_manager);
- right = bound;
- current = 0;
- break;
- }
-
- if (head_symbol == m_lblneg ||
- head_symbol == m_lblpos) {
- if (!current->children()[1] ||
- !current->children()[2]) {
- set_error("labels require two arguments", current);
- goto cleanup;
- }
-
- bool is_pos = head_symbol == m_lblpos;
- idbuilder* lbl = new (region) build_label(this, is_pos, current->children()[1]);
-
- up.push_back(new (region) parse_frame(current, lbl, left, right, m_binding_level));
-
- //
- // process the body.
- //
- left = alloc(expr_ref_vector, m_manager);
- right = 0;
- current = current->children()[2];
- break;
- }
-
- if (head_symbol == m_bang) {
- proto_expr* const* children = current->children();
- proto_expr* body = children[1];
- proto_expr* lblname = 0;
- bool is_pos = false;
-
- children += 2;
-
- while (children[0] &&
- children[0]->kind() == proto_expr::ANNOTATION &&
- children[1]) {
- symbol id = children[0]->string();
-
- if ((id == m_lblneg) ||
- (id == m_lblpos)) {
- is_pos = id == m_lblpos;
- lblname = children[1];
- }
-
- children += 2;
- }
-
- if (lblname) {
- idbuilder* lbl = new (region) build_label(this, is_pos, lblname);
- up.push_back(new (region) parse_frame(current, lbl, left, right, m_binding_level));
- left = alloc(expr_ref_vector, m_manager);
- right = 0;
- }
-
- //
- // process the body.
- //
- current = body;
- break;
- }
-
- if ((head_symbol == m_forall) ||
- (head_symbol == m_exists)) {
-
- expr_ref_buffer patterns(m_manager);
- expr_ref_buffer no_patterns(m_manager);
- sort_ref_buffer sorts(m_manager);
- svector<symbol> vars;
- int weight = 1;
-
- proto_expr* const* children = current->children();
- proto_expr* body = 0;
-
- ++children;
-
- if (!children[0] || !children[1]) {
- set_error("quantifier should have at least two arguments", current);
- goto cleanup;
- }
-
- //
- // restore 'left' and 'right' working set and m_binding_level.
- //
- up.push_back(new (region) parse_frame(current, new (region) identity(), left, right, m_binding_level));
- left = alloc(expr_ref_vector, m_manager);
-
- //
- // declare the bound variables.
- //
-
- local_scope.begin_scope();
-
- while (children[0] && children[1] &&
- (children[1]->kind() != proto_expr::ANNOTATION)) {
-
- if (!parse_bound(local_scope, region, *children, vars, sorts)) {
- goto cleanup;
- }
- ++children;
- }
-
- body = children[0];
-
- if (is_annotated_cons(body)) {
- children = body->children()+1;
- body = body->children()[1];
- }
-
- ++children;
-
- symbol qid = symbol(current->line());
- symbol skid = symbol();
-
- read_patterns(vars.size(), local_scope, children, patterns, no_patterns, weight, qid, skid);
-
- //
- // push a parse_frame to undo the scope of the quantifier.
- //
-
- SASSERT(sorts.size() > 0);
-
- idbuilder* pop_q = new (region) pop_quantifier(this, (head_symbol == m_forall), weight, qid, skid, patterns, no_patterns, sorts, vars, local_scope);
-
- expr_ref_vector * empty_v = alloc(expr_ref_vector, m_manager);
- up.push_back(new (region) parse_frame(current, pop_q, empty_v, 0, m_binding_level));
-
- //
- // process the body.
- //
- right = 0;
- current = body;
- break;
- }
-
- if (is_underscore_op(region, current->children()[0], builder)) {
- up.push_back(new (region) parse_frame(current, builder, left, right, m_binding_level));
- }
- else if (local_scope.find(head_symbol, builder)) {
- up.push_back(new (region) parse_frame(current, builder, left, right, m_binding_level));
- }
- else {
- up.push_back(new (region) parse_frame(current->children()[0], left, right, m_binding_level));
- }
- left = alloc(expr_ref_vector, m_manager);
- right = current->children() + 1;
- current = 0;
- break;
- }
- }
-
- cleanup:
-
- if (success && !is_well_sorted(m_manager, result)) {
- set_error("expression is not well sorted", e);
- success = false;
- }
-
- dealloc(left);
- while (!up.empty()) {
- dealloc(up.back()->detach_left());
- up.pop_back();
- }
- return success;
- }
-
- bool read_patterns(unsigned num_bindings, symbol_table<idbuilder*> & local_scope, proto_expr * const * & children,
- expr_ref_buffer & patterns, expr_ref_buffer & no_patterns, int& weight, symbol& qid, symbol& skid) {
- proto_region region;
- while (children[0] &&
- children[0]->kind() == proto_expr::ANNOTATION &&
- children[1]) {
-
- if (children[0]->string() == symbol("qid") ||
- children[0]->string() == symbol("named")) {
- qid = children[1]->string();
- children += 2;
- continue;
- }
-
- if (children[0]->string() == symbol("skolemid")) {
- skid = children[1]->string();
- children += 2;
- continue;
- }
-
- ptr_vector<proto_expr> proto_exprs;
-
- if (children[1]->kind() == proto_expr::COMMENT) {
- std::string s = children[1]->string().str();
- std::istringstream stream(s);
- scanner scanner(stream, get_err(), false);
- proto_expr_parser parser(region, scanner, get_err());
-
- if (!parser.parse(proto_exprs)) {
- set_error("could not parse expression", children[1]);
- return false;
- }
- } else if (children[1]->kind() == proto_expr::CONS) {
- for (proto_expr* const* pexpr = children[1]->children(); *pexpr; pexpr++)
- proto_exprs.push_back(*pexpr);
- } else {
- proto_exprs.push_back(children[1]);
- }
-
- expr_ref_buffer ts(m_manager);
- for (unsigned i = 0; i < proto_exprs.size(); ++i) {
- expr_ref t(m_manager);
- if (!make_expression(local_scope, proto_exprs[i], t)) {
- return false;
- }
- ts.push_back(t.get());
- }
-
- if (children[0]->string() == symbol("pat") ||
- children[0]->string() == symbol("pats") ||
- children[0]->string() == symbol("pattern")) {
- for (unsigned i = 0; i < ts.size(); ++i) {
- if (!is_app(ts[i])) {
- set_error("invalid pattern", children[0]);
- return false;
- }
- }
- expr_ref p(m_manager);
- p = m_manager.mk_pattern(ts.size(), (app*const*)(ts.c_ptr()));
- if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) {
- set_error("invalid pattern", children[0]);
- return false;
- }
- patterns.push_back(p);
- }
- else if (children[0]->string() == symbol("ex_act") && ts.size() == 1) {
- app_ref sk_hack(m_manager);
- sk_hack = m_manager.mk_app(m_sk_hack, 1, ts.c_ptr());
- app * sk_hackp = sk_hack.get();
- expr_ref p(m_manager);
- p = m_manager.mk_pattern(1, &sk_hackp);
- if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) {
- set_error("invalid pattern", children[0]);
- return false;
- }
- patterns.push_back(p);
- }
- else if ((children[0]->string() == symbol("nopat") ||
- children[0]->string() == symbol("no-pattern"))
- && ts.size() == 1) {
- no_patterns.push_back(ts[0]);
- }
- else if (children[0]->string() == symbol("weight") && ts.size() == 1 &&
- proto_exprs[0]->kind() == proto_expr::INT &&
- proto_exprs[0]->number().is_unsigned()) {
- weight = proto_exprs[0]->number().get_unsigned();
- }
- else {
- // TODO: this should be a warning, perferably once per unknown kind of annotation
- set_error("could not understand annotation '",
- children[0]->string().bare_str(), "'", children[0]);
- }
-
- children += 2;
- }
- return true;
- }
-
- void set_default_num_sort(symbol const& name) {
- if (name == symbol("QF_RDL") ||
- name == symbol("QF_LRA") ||
- name == symbol("LRA") ||
- name == symbol("RDL") ||
- name == symbol("QF_NRA") ||
- name == symbol("QF_UFNRA") ||
- name == symbol("QF_UFLRA")) {
- m_int_sort = m_real_sort;
- }
- }
-
- bool get_sort(theory* th, char const * s, sort_ref& sort) {
- return make_sort(symbol(s), 0, 0, sort);
- }
-
-
- bool make_sort(symbol const & id, unsigned num_params, parameter const* params, sort_ref& s) {
- builtin_op info;
- if (m_builtin_sorts.find(id, info)) {
- s = m_manager.mk_sort(info.m_family_id, info.m_kind, num_params, params);
- return true;
- }
-
- if (num_params == 2 && symbol("Array") == id) {
- // Old HACK to accomodate bit-vector arrays.
-
- if (!params[0].is_int()) {
- throw default_exception("Non-integer parameter to array");
- return false;
- }
- if (!params[1].is_int()) {
- throw default_exception("Non-integer parameter to array");
- return false;
- }
- parameter bv_params0[1] = { parameter(params[0].get_int()) };
- parameter bv_params1[1] = { parameter(params[1].get_int()) };
-
- sort * t1 = m_manager.mk_sort(m_bv_fid, BV_SORT, 1, bv_params0);
- sort * t2 = m_manager.mk_sort(m_bv_fid, BV_SORT, 1, bv_params1);
- parameter params[2] = { parameter(t1), parameter(t2) };
- s = m_manager.mk_sort(m_array_fid, ARRAY_SORT, 2, params);
- return true;
- }
-
- sort* srt = 0;
- if (m_benchmark.get_sort(id, srt)) {
- s = srt;
- return true;
- }
- return false;
- }
-
- bool make_sort(proto_expr * e, sort_ref& s) {
- SASSERT(can_be_sort(e));
- symtable& env = *m_benchmark.get_symtable();
- sort_builder* mk_sort;
- switch(e->kind()) {
- case proto_expr::ID: {
- if (make_sort(e->string(), e->num_params(), e->params(), s)) {
- return true;
- }
- if (env.lookup(e->string(), mk_sort)) {
- if (!mk_sort->apply(e->num_params(), e->params(), s)) {
- set_error(mk_sort->error_message(), e);
- return false;
- }
- return true;
- }
- set_error("could not find sort ", e);
- return false;
- }
- case proto_expr::CONS: {
- if (!can_be_sort(e)) {
- set_error("expression cannot be a sort", e);
- return false;
- }
- proto_expr *const* chs = e->children();
- if (is_underscore(e)) {
- ++chs;
- }
- symbol name = (*chs)->string();
- if (!env.lookup(name, mk_sort)) {
- set_error("could not find sort symbol '", name.str(), "'", e);
- return false;
- }
- sort_ref_vector sorts(m_manager);
- vector<parameter> params;
- if (!parse_params(chs+1, params, sorts)) {
- return false;
- }
-
- if (!mk_sort->apply(params.size(), params.c_ptr(), s)) {
- set_error(mk_sort->error_message(), e);
- return false;
- }
- return true;
- }
- default:
- set_error("could not create sort ", e);
- return false;
- }
- }
-
- bool parse_params(proto_expr* const* chs,vector<parameter>& params, sort_ref_vector& sorts) {
- while (*chs) {
- if ((*chs)->kind() == proto_expr::INT) {
- rational const& num = (*chs)->number();
- if (num.is_unsigned()) {
- params.push_back(parameter(num.get_unsigned()));
- }
- else {
- params.push_back(parameter(num));
- }
- }
- else {
- sort_ref s1(m_manager);
- if (!make_sort(*chs, s1)) {
- return false;
- }
- sorts.push_back(s1);
- params.push_back(parameter((ast*)s1.get()));
- }
- ++chs;
- }
- return true;
- }
-
- bool parse_bound(
- symbol_table<idbuilder*>& local_scope,
- region& region,
- proto_expr* bound,
- svector<symbol>& vars,
- sort_ref_buffer& sorts
- )
- {
- if (is_cons_list(bound)) {
- proto_expr *const* children = bound->children();
- while (*children) {
- if (!parse_bound(local_scope, region, *children, vars, sorts)) {
- return false;
- }
- ++children;
- }
- return true;
- }
- if (!can_be_sorted_var(bound)) {
- set_error("bound variable should contain a list of pairs", bound);
- return false;
- }
- proto_expr* var = bound->children()[0];
- proto_expr* sort_proto_expr = bound->children()[1];
-
- sort_ref sort(m_manager);
- if (!make_sort(sort_proto_expr, sort)) {
- return false;
- }
- sorts.push_back(sort);
- vars.push_back(var->string());
-
- local_scope.insert(
- var->string(),
- new (region) bound_var(this, sort)
- );
-
- ++m_binding_level;
-
- return true;
- }
-
- bool can_be_sort(proto_expr* e) {
- if (e && e->kind() == proto_expr::ID) {
- return true;
- }
- if (is_underscore(e)) {
- return true;
- }
-
- if (e &&
- e->kind() == proto_expr::CONS &&
- e->children() &&
- e->children()[0] &&
- e->children()[1]) {
- proto_expr* const* ch = e->children();
- while(*ch) {
- if (!can_be_sort(*ch)) {
- return false;
- }
- ++ch;
- }
- return true;
- }
- return false;
- }
-
- bool declare_sorts(proto_expr* e) {
- proto_expr* const * children = e->children();
-
- while (children && *children) {
- proto_expr* ch = *children;
- switch(ch->kind()) {
-
- case proto_expr::ID:
- m_benchmark.declare_sort(ch->string());
- break;
-
- case proto_expr::CONS:
- //
- // The declaration of type constructors
- // consists of an identifier together with
- // a number indicating the arity of the
- // constructor.
- //
- if (ch->children() &&
- ch->children()[0] &&
- ch->children()[0]->kind() == proto_expr::ID &&
- ch->children()[1] &&
- ch->children()[1]->kind() == proto_expr::INT) {
-
- // unsigned num = (unsigned) ch->children()[1]->number().get_uint64();
- m_benchmark.declare_sort(ch->children()[0]->string());
- }
- break;
-
- case proto_expr::ANNOTATION:
- break;
-
- default:
- set_error("unexpected argument to sorts",ch);
- return false;
- }
- ++children;
- }
- return true;
- }
-
- bool define_sorts(proto_expr* e) {
- proto_expr* const * children = e->children();
-
- while (children && *children) {
- if (!define_sort(*children)) {
- return false;
- }
- ++children;
- }
- return true;
- }
-
- bool define_sort(proto_expr* e) {
- proto_expr* const * children = e->children();
- sort_ref_buffer domain(m_manager);
-
- //
- // First element in list must be an identifier.
- // there should be just two elements.
- //
- if (!children ||
- !children[0] ||
- !(children[0]->kind() == proto_expr::ID) ||
- !children[1] ||
- children[2]) {
- set_error("unexpected arguments to function declaration", e);
- return false;
- }
- symbol name = children[0]->string();
- sort_ref s(m_manager);
- if (!can_be_sort(children[1]) ||
- !make_sort(children[1], s)) {
- set_error("unexpected arguments to function declaration", e);
- return false;
- }
-
- m_benchmark.get_symtable()->insert(name, s);
-
- return true;
- }
-
- bool declare_funs(proto_expr* e) {
- proto_expr* const * children = e->children();
-
- while (children && *children) {
- if (!declare_fun(*children)) {
- return false;
- }
- ++children;
- }
- return true;
- }
- class define_sort_cls : public sort_builder {
- smtparser& m_parser;
- proto_region m_region;
- proto_expr* m_expr;
- svector<symbol> m_params;
- symbol m_name;
- std::string m_error_message;
-
- public:
- define_sort_cls(smtparser& p, symbol const& name, proto_expr* e, unsigned num_params, symbol* params) :
- m_parser(p),
- m_name(name) {
- for (unsigned i = 0; i < num_params; ++i) {
- m_params.push_back(params[i]);
- }
- m_expr = proto_expr::copy(m_region, e);
- }
-
- virtual bool apply(unsigned num_params, parameter const* params, sort_ref & result) {
- smtlib::symtable * symtable = m_parser.m_benchmark.get_symtable();
- if (m_params.size() != num_params) {
- std::ostringstream strm;
- strm << "wrong number of arguments passed to " << m_name << " "
- << m_params.size() << " expected, but " << num_params << " given";
- m_error_message = strm.str();
- return false;
- }
- for (unsigned i = 0; i < num_params; ++i) {
- parameter p(params[i]);
- if (!p.is_ast() || !is_sort(p.get_ast())) {
- symtable->pop_sorts(i);
- std::ostringstream strm;
- strm << "argument " << i << " is not a sort";
- m_error_message = strm.str();
- return false;
- }
- symtable->push_sort(m_params[i], to_sort(p.get_ast()));
- }
- bool success = m_parser.make_sort(m_expr, result);
-
- symtable->pop_sorts(num_params);
- return success;
- }
-
- virtual char const* error_message() {
- return m_error_message.c_str();
- }
-
- };
-
- // (define-sort name (<symbol>*) <sort>)
- bool define_sort(proto_expr* id, proto_expr* sorts, proto_expr* srt) {
- symbol name = id->string();
- proto_expr* const * children = sorts->children();
- svector<symbol> names;
-
- if (!children) {
- set_error("Sort definition expects a list of sort symbols",id);
- return false;
- }
-
- while (children[0]) {
- id = children[0];
- if(id->kind() != proto_expr::ID) {
- set_error("unexpected argument, expected ID", id);
- return false;
- }
- names.push_back(id->string());
- ++children;
- }
-
- m_benchmark.get_symtable()->insert(name, alloc(define_sort_cls, *this, name, srt, names.size(), names.c_ptr()));
- return true;
- }
-
- bool declare_fun(proto_expr* id, proto_expr* sorts, proto_expr* srt) {
- proto_expr* const * children = sorts?sorts->children():0;
- sort_ref_buffer domain(m_manager);
- symbol name = id->string();
-
- if (sorts && !children) {
- set_error("Function declaration expects a list of sorts", id);
- return false;
- }
- //
- // parse domain.
- //
- while (sorts && children[0]) {
- sort_ref s(m_manager);
- if (!make_sort(children[0], s)) {
- return false;
- }
- domain.push_back(s);
- ++children;
- }
-
- sort_ref range(m_manager);
- if (!make_sort(srt, range)) {
- return false;
- }
- bool is_associative = false;
- bool is_commutative = false;
- bool is_injective = false;
- m_benchmark.declare_func(name, domain, range, is_associative, is_commutative, is_injective);
- return true;
- }
-
- bool declare_fun(proto_expr* e) {
- proto_expr* const * children = e->children();
- sort_ref_buffer domain(m_manager);
- //
- // Skip declaration of numbers.
- //
- if (children &&
- children[0] &&
- children[0]->kind() == proto_expr::INT) {
- return true;
- }
-
- //
- // First element in list must be an identifier.
- //
- if (!children ||
- !children[0] ||
- !(children[0]->kind() == proto_expr::ID)) {
- set_error("unexpected arguments to function declaration", e);
- return false;
- }
-
- symbol name = children[0]->string();
-
- ++children;
-
-
- if (!can_be_sort(children[0])) {
- set_error("unexpected arguments to function declaration", e);
- return false;
- }
-
- //
- // parse domain.
- //
- while (can_be_sort(children[1])) {
- sort_ref s(m_manager);
- if (!make_sort(children[0], s)) {
- return false;
- }
- domain.push_back(s);
- ++children;
- }
-
- //
- // parse range.
- //
- SASSERT(can_be_sort(children[0]));
-
- sort_ref range(m_manager);
- if (!make_sort(children[0], range)) {
- return false;
- }
- ++children;
-
- //
- // parse attributes.
- //
- bool is_associative = false;
- bool is_commutative = false;
- bool is_injective = false;
-
- while(children[0] && children[0]->kind() == proto_expr::ANNOTATION) {
-
- if (m_associative == children[0]->string()) {
- is_associative = true;
- }
- else if (m_commutative == children[0]->string()) {
- is_commutative = true;
- }
- else if (m_injective == children[0]->string()) {
- is_injective = true;
- }
- ++children;
- }
-
- m_benchmark.declare_func(name, domain, range, is_associative, is_commutative, is_injective);
-
- return true;
- }
-
- bool declare_preds(proto_expr* e) {
- proto_expr* const * children = e->children();
-
- while (children && *children) {
- if (!declare_pred(*children)) {
- return false;
- }
- ++children;
- }
- return true;
- }
-
-
- bool declare_pred(proto_expr* e) {
- proto_expr* const * children = e->children();
- if (!children || !children[0] || !(children[0]->kind() == proto_expr::ID)) {
- set_error("unexpected arguments to predicate declaration", e);
- return false;
- }
- symbol const & name = children[0]->string();
- sort_ref_buffer domain(m_manager);
- sort * bool_sort = m_manager.mk_bool_sort();
-
- ++children;
-
- while (can_be_sort(children[0])) {
- sort_ref s(m_manager);
- if (!make_sort(children[0], s)) {
- return false;
- }
- domain.push_back(s);
- ++children;
- }
-
- m_benchmark.declare_func(name, domain, bool_sort, false, false, false);
-
- return true;
- }
-
- bool can_be_sorted_var(proto_expr* e) {
- return
- e &&
- (e->kind() == proto_expr::CONS) &&
- e->children() &&
- e->children()[0] &&
- (e->children()[0]->kind() == proto_expr::ID) &&
- can_be_sort(e->children()[1]);
- }
-
- bool is_cons_list(proto_expr* e) {
- return
- e &&
- (e->kind() == proto_expr::CONS) &&
- e->children() &&
- e->children()[0] &&
- e->children()[0]->kind() == proto_expr::CONS;
- }
-
- bool is_prefixed(proto_expr* e, symbol const& s) {
- return
- e &&
- (e->kind() == proto_expr::CONS) &&
- e->children() &&
- e->children()[0] &&
- e->children()[1] &&
- e->children()[0]->string() == s;
-
- }
-
- bool is_underscore(proto_expr* e) {
- return
- is_prefixed(e, m_underscore) &&
- e->children()[1]->kind() == proto_expr::ID;
- }
-
- bool is_annotated_cons(proto_expr* e) {
- return is_prefixed(e, m_bang);
- }
-
- bool is_builtin_const(symbol const& id, proto_expr* current, unsigned num_params, parameter * params, bool& ok, expr_ref& term) {
- builtin_op info;
- ok = true;
- if (!m_builtin_ops.find(id, info)) {
- return false;
- }
- fix_parameters(num_params, params);
- func_decl* d = m_manager.mk_func_decl(info.m_family_id, info.m_kind, num_params, params, 0, (expr * const *)0);
- if (!d) {
- set_error("could not create a term from constant ", id, current);
- ok = false;
- }
- else if (d->get_arity() != 0) {
- set_error("identifier expects arguments ", id, current);
- ok = false;
- }
- else {
- term = m_manager.mk_const(d);
- }
- return true;
- }
-
- bool is_underscore_op(region& r, proto_expr* e, idbuilder*& builder) {
- if (!is_underscore(e)) {
- return false;
- }
- builtin_op info;
- proto_expr *const* chs = e->children()+1;
- symbol const& id = (*chs)->string();
- sort_ref_vector sorts(m_manager);
- vector<parameter> params;
-
- if (!m_builtin_ops.find(id, info)) {
- return false;
- }
- if (!parse_params(chs+1, params, sorts)) {
- return false;
- }
-
- builder = new (r) builtin_builder(this, info.m_family_id, info.m_kind, params);
- return true;
- }
-
- void fix_parameters(unsigned num_params, parameter* params) {
- for (unsigned i = 0; i < num_params; ++i) {
- func_decl* d = 0;
- sort* s = 0;
- builtin_op info;
- if (params[i].is_symbol() && m_benchmark.get_symtable()->find1(params[i].get_symbol(), d)) {
- params[i] = parameter(d);
- }
- else if (params[i].is_symbol() && m_benchmark.get_symtable()->find(params[i].get_symbol(), s)) {
- params[i] = parameter(s);
- }
- else if (params[i].is_symbol() && m_builtin_sorts.find(params[i].get_symbol(), info)) {
- params[i] = parameter(m_manager.mk_sort(info.m_family_id, info.m_kind, 0, 0));
- }
- }
- }
-
- bool make_app(proto_expr * proto_expr, expr_ref_vector const & args, expr_ref & result) {
- symbol const& name = proto_expr->string();
- ptr_vector<sort> sorts;
- func_decl * d = 0;
- smtlib::symtable * symtable = m_benchmark.get_symtable();
-
- for (unsigned i = 0; i < args.size(); ++i) {
- sorts.push_back(m_manager.get_sort(args.get(i)));
- }
-
- if (symtable->find_overload(name, sorts, d)) {
- result = m_manager.mk_app(d, args.size(), args.c_ptr());
- return true;
- }
-
- builtin_op info;
- if (m_builtin_ops.find(name, info)) {
- unsigned num_params = proto_expr->num_params();
- parameter * params = proto_expr->params();
- fix_parameters(num_params, params);
- d = m_manager.mk_func_decl(info.m_family_id, info.m_kind, num_params, params, args.size(), args.c_ptr());
- if (d) {
- result = m_manager.mk_app(d, args.size(), args.c_ptr());
- return true;
- }
- }
-
- rational arg2_value;
- bool arg2_is_int;
-
- if (name == symbol("store") &&
- args.size() == 3 &&
- m_anum_util.is_numeral(args.get(2), arg2_value, arg2_is_int) &&
- arg2_is_int) {
- expr_ref_vector new_args(m_manager);
- new_args.push_back(args.get(0));
- new_args.push_back(args.get(1));
- new_args.push_back(m_anum_util.mk_numeral(arg2_value, false));
- sorts.reset();
- for (unsigned i = 0; i < args.size(); ++i) {
- sorts.push_back(m_manager.get_sort(new_args.get(i)));
- }
- if (symtable->find_overload(name, sorts, d)) {
- result = m_manager.mk_app(d, new_args.size(), new_args.c_ptr());
- return true;
- }
- }
-
- error_prefix(proto_expr);
- get_err() << "could not find overload for '" << name << "' ";
- for (unsigned i = 0; i < sorts.size(); ++i) {
- get_err() << "Argument: "
- << mk_pp(args.get(i), m_manager)
- << " has type "
- << mk_pp(sorts[i], m_manager)
- << ".\n";
- }
- return false;
- }
-
- class nullary : public idbuilder {
- expr* m_expr;
- smtparser* m_parser;
- unsigned m_decl_level_save;
- public:
- nullary(expr* e, smtparser* p) : m_expr(e), m_parser(p), m_decl_level_save(p->m_binding_level) {}
-
- virtual bool apply(expr_ref_vector const& args, expr_ref & result) {
- unsigned decl_level = m_parser->m_binding_level;
- SASSERT(decl_level >= m_decl_level_save);
- shift_vars shifty(m_parser->m_manager);
- shifty(m_expr, decl_level - m_decl_level_save, result);
- return (args.size() == 0);
- }
- };
-
- class identity : public idbuilder {
- public:
- identity() {}
-
- virtual bool apply(expr_ref_vector const & args, expr_ref & result) {
- if (args.size() == 1) {
- result = args.back();
- return true;
- }
- else {
- return false;
- }
- }
- };
-
- class parse_frame {
- public:
-
- parse_frame(proto_expr * e, idbuilder * make, expr_ref_vector * left, proto_expr * const* right, unsigned binding_level):
- m_proto_expr(e),
- m_make_term(make),
- m_left(left),
- m_right(right),
- m_binding_level(binding_level) {
- }
-
- parse_frame(proto_expr * e, expr_ref_vector * left, proto_expr * const* right, unsigned binding_level):
- m_proto_expr(e),
- m_make_term(0),
- m_left(left),
- m_right(right),
- m_binding_level(binding_level) {
- }
-
- expr_ref_vector * detach_left() {
- expr_ref_vector * result = m_left;
- SASSERT(m_left);
- m_left = 0;
- return result;
- }
-
- unsigned binding_level() const { return m_binding_level; }
-
- proto_expr* const * right() const { return m_right; }
-
- idbuilder* make_term() { return m_make_term; }
-
- proto_expr* get_proto_expr() const { return m_proto_expr; }
-
- ~parse_frame() { dealloc(m_left); }
-
- private:
-
- proto_expr* m_proto_expr;
- idbuilder* m_make_term;
- expr_ref_vector * m_left;
- proto_expr* const * m_right;
- unsigned m_binding_level;
-
- parse_frame & operator=(parse_frame const & other);
-
- parse_frame(parse_frame const & other);
-
- };
-
- class build_label : public idbuilder {
- bool m_pos;
- symbol m_sym;
- smtparser * m_smt;
- public:
- build_label(smtparser * smt, bool is_pos, proto_expr * sym): m_pos(is_pos), m_smt(smt) {
- switch(sym->kind()) {
- case proto_expr::ID:
- case proto_expr::STRING:
- m_sym = sym->string();
- break;
- case proto_expr::INT:
- m_sym = symbol(sym->number().to_string().c_str());
- break;
- default:
- UNREACHABLE();
- break;
- }
- }
-
- virtual bool apply(expr_ref_vector const & args, expr_ref & result) {
- if (args.size() >= 1) {
- result = m_smt->m_manager.mk_label(m_pos, m_sym, args.get(0));
- return true;
- }
- else {
- return false;
- }
- }
- };
-
- class pop_let : public idbuilder {
- public:
- pop_let(symbol_table<idbuilder*> & local_scope, expr_ref_vector* pinned = 0):
- m_local_scope(local_scope),
- m_pinned(pinned) {
- }
-
- virtual ~pop_let() {}
-
- virtual bool apply(expr_ref_vector const & args, expr_ref & result) {
- dealloc(m_pinned);
- if (args.size() == 2) {
- m_local_scope.end_scope();
- result = args.get(1);
- return true;
- }
- else {
- return false;
- }
- }
- private:
- symbol_table<idbuilder*> & m_local_scope;
- expr_ref_vector* m_pinned;
- };
-
- class push_let : public idbuilder {
- smtparser* m_parser;
- region & m_region;
- symbol_table<idbuilder*> & m_local_scope;
- symbol m_let_var;
-
- public:
- push_let(smtparser* p, region & region, symbol_table<idbuilder*> & local_scope, symbol const & let_var):
- m_parser(p),
- m_region(region),
- m_local_scope(local_scope),
- m_let_var(let_var) {
- }
-
- virtual bool apply(expr_ref_vector const & args, expr_ref & result) {
- //
- // . push a scope,
- // . create a nullary function using the variable/term association.
- // . return the (first) argument.
- //
- //
- if (args.size() == 1) {
- m_local_scope.begin_scope();
- m_local_scope.insert(m_let_var, new (m_region) nullary(args.back(), m_parser));
- result = args.back();
- return true;
- }
- else {
- return false;
- }
- }
- };
-
- // push multiple let bound variables.
- class push_let_and : public idbuilder {
- smtparser* m_parser;
- region & m_region;
- symbol_table<idbuilder*> & m_local_scope;
- unsigned m_num_vars;
- symbol* m_vars;
- expr_ref_vector* m_pinned;
-
- public:
- push_let_and(smtparser* p, region & region, symbol_table<idbuilder*> & local_scope, expr_ref_vector* pinned, unsigned num_vars, symbol const* vars):
- m_parser(p),
- m_region(region),
- m_local_scope(local_scope),
- m_num_vars(num_vars),
- m_vars(new (region) symbol[num_vars]),
- m_pinned(pinned) {
- for (unsigned i = 0; i < num_vars; ++i) {
- m_vars[i] = vars[i];
- }
- }
-
- virtual bool apply(expr_ref_vector const & args, expr_ref & result) {
- if (args.size() != m_num_vars) {
- return false;
- }
-
- //
- // . push a scope,
- // . create a nullary function using the variable/term association.
- // . return the last argument (arbitrary).
- //
-
- m_local_scope.begin_scope();
- for (unsigned i = 0; i < m_num_vars; ++i) {
- m_local_scope.insert(m_vars[i], new (m_region) nullary(args[i], m_parser));
- m_pinned->push_back(args[i]);
- }
- result = args.back();
- return true;
- }
- };
-
- class bound_var : public idbuilder {
- public:
- bound_var(smtparser * smt, sort * sort):
- m_smt(smt),
- m_decl_level(smt->m_binding_level),
- m_sort(sort) {
- }
-
- virtual bool apply(expr_ref_vector const & args, expr_ref & result) {
- SASSERT(m_smt->m_binding_level > m_decl_level);
- unsigned idx = m_smt->m_binding_level - m_decl_level - 1;
- result = m_smt->m_manager.mk_var(idx, m_sort);
- return args.empty();
- }
-
- private:
- smtparser * m_smt;
- unsigned m_decl_level;
- sort * m_sort;
- };
-
- class pop_quantifier : public idbuilder {
- public:
- pop_quantifier(smtparser * smt, bool is_forall, int weight, symbol const& qid, symbol const& skid, expr_ref_buffer & patterns, expr_ref_buffer & no_patterns, sort_ref_buffer & sorts,
- svector<symbol>& vars, symbol_table<idbuilder*> & local_scope):
- m_smt(smt),
- m_is_forall(is_forall),
- m_weight(weight),
- m_qid(qid),
- m_skid(skid),
- m_patterns(m_smt->m_manager),
- m_no_patterns(m_smt->m_manager),
- m_sorts(m_smt->m_manager),
- m_local_scope(local_scope) {
- SASSERT(sorts.size() == vars.size());
-
- m_vars.append(vars);
- m_sorts.append(sorts);
- m_patterns.append(patterns);
- m_no_patterns.append(no_patterns);
- }
-
- virtual bool apply(expr_ref_vector const & args, expr_ref & result) {
- if (args.size() != 1) {
- return false;
- }
-
- m_local_scope.end_scope();
-
- expr * body = args.back();
-
- if (m_smt->ignore_user_patterns()) {
- TRACE("pat_bug", tout << "ignoring user patterns...: " << m_patterns.size() << "\n";);
- result = m_smt->m_manager.mk_quantifier(m_is_forall,
- m_sorts.size(), // num_decls
- m_sorts.c_ptr(), // decl_sorts
- m_vars.begin(), // decl_names
- body,
- m_weight,
- m_qid,
- m_skid,
- 0,
- 0,
- 0,
- 0);
- }
- else if (!m_patterns.empty()) {
- if (!m_no_patterns.empty()) {
- m_smt->set_error("patterns were provided, ignoring :nopat attribute.", ((proto_expr*)0));
- }
- result = m_smt->m_manager.mk_quantifier(m_is_forall,
- m_sorts.size(), // num_decls
- m_sorts.c_ptr(), // decl_sorts
- m_vars.begin(), // decl_names
- body,
- m_weight,
- m_qid,
- m_skid,
- m_patterns.size(),
- m_patterns.c_ptr(),
- 0,
- 0);
- }
- else {
- result = m_smt->m_manager.mk_quantifier(m_is_forall,
- m_sorts.size(), // num_decls
- m_sorts.c_ptr(), // decl_sorts
- m_vars.begin(), // decl_names
- body,
- m_weight,
- m_qid,
- m_skid,
- 0,
- 0,
- m_no_patterns.size(),
- m_no_patterns.c_ptr());
- }
-
- //
- // reclaim memory resources on application.
- //
-
- m_vars.finalize();
- m_sorts.finalize();
- m_patterns.finalize();
- m_no_patterns.finalize();
- return true;
- }
-
- private:
- smtparser* m_smt;
- bool m_is_forall;
- int m_weight;
- symbol m_qid;
- symbol m_skid;
- expr_ref_buffer m_patterns;
- expr_ref_buffer m_no_patterns;
- sort_ref_buffer m_sorts;
- svector<symbol> m_vars;
- symbol_table<idbuilder*>& m_local_scope;
- };
-
- class builtin_builder : public idbuilder {
- smtparser* m_smt;
- family_id m_fid;
- decl_kind m_kind;
- vector<parameter> m_params;
-
- public:
- builtin_builder(smtparser* smt, family_id fid, decl_kind k,vector<parameter> const& p):
- m_smt(smt),
- m_fid(fid),
- m_kind(k),
- m_params(p)
- {
- }
-
- virtual bool apply(expr_ref_vector const& args, expr_ref& result) {
- ast_manager& m = m_smt->m_manager;
- func_decl* d = m.mk_func_decl(m_fid, m_kind, m_params.size(), m_params.c_ptr(), args.size(), args.c_ptr());
- if (d) {
- result = m.mk_app(d, args.size(), args.c_ptr());
- }
- m_params.finalize();
- return d != 0;
- }
- };
-
- bool push_status(smtlib::benchmark::status status) {
- m_benchmark.set_status( status);
- return true;
- }
-
- expr * mk_number(rational const & r, bool is_int){
- if (m_int_sort == m_real_sort) // integer constants should be mapped to real
- is_int = false;
- return m_anum_util.mk_numeral(r, is_int);
- }
-
- void push_benchmark(symbol const & name) {
- m_benchmark.set_name(name);
- }
-
- bool push_assumption(expr * t) {
- m_benchmark.add_axiom(t);
- return true;
- }
-
- bool push_formula(expr * t) {
- m_benchmark.add_formula(t);
- return true;
- }
-
- bool is_binary_let_binding(proto_expr* let_binding) {
- return
- let_binding &&
- let_binding->children() &&
- let_binding->children()[0] &&
- (let_binding->children()[0]->kind() == proto_expr::ID) &&
- let_binding->children()[1] &&
- !let_binding->children()[2];
- }
-
- bool is_bvconst(symbol const & fname, unsigned num_params, parameter const* params, expr_ref & term) {
- rational n;
- char const * str = fname.bare_str();
- unsigned sz = 0;
-
- if (strncmp(str, "bvbin", 5) == 0) {
- str += 5;
- n = rational(0);
- while (*str == '1' || *str == '0') {
- n *= rational(2);
- n += rational(*str - '0');
- ++sz;
- ++str;
- }
- if (sz == 0) {
- return false;
- }
- }
- else if (strncmp(str, "bvhex", 5) == 0) {
- n = rational(0);
- str += 5;
- while (('0' <= *str && *str <= '9') ||
- ('a' <= *str && *str <= 'f') ||
- ('A' <= *str && *str <= 'F')) {
- n *= rational(16);
- if ('0' <= *str && *str <= '9') {
- n += rational(*str - '0');
- }
- else if ('a' <= *str && *str <= 'f') {
- n += rational(10);
- n += rational(*str - 'a');
- }
- else {
- SASSERT('A' <= *str && *str <= 'F');
- n += rational(10);
- n += rational(*str - 'A');
- }
- sz += 4;
- ++str;
- }
- if (sz == 0) {
- return false;
- }
- }
- else if (strncmp(str, "bv", 2) == 0 && '0' <= *(str + 2) && *(str + 2) <= '9') {
- n = rational(0);
- str += 2;
- while ('0' <= *str && *str <= '9') {
- n *= rational(10);
- n += rational(*str - '0');
- ++str;
- }
- if (num_params == 1) {
- sz = params[0].get_int();
- }
- else {
- sz = 32;
- }
- }
- else {
- return false;
- }
-
- term = m_bvnum_util.mk_numeral(n, sz);
-
- return true;
- }
-};
-
-
-parser * parser::create(ast_manager& ast_manager, bool ignore_user_patterns) {
- return alloc(smtparser, ast_manager, ignore_user_patterns);
-}
diff --git a/src/parsers/smt/smtparser.h b/src/parsers/smt/smtparser.h
deleted file mode 100644
index d8999e8ab..000000000
--- a/src/parsers/smt/smtparser.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*++
-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/ast.h"
-#include "util/vector.h"
-#include "parsers/smt/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
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 3d2609c4f..8b719681c 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -37,7 +37,7 @@ Revision History:
#include "util/env_params.h"
#include "shell/lp_frontend.h"
-typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_Z3_LOG, IN_MPS } input_kind;
+typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_Z3_LOG, IN_MPS } input_kind;
std::string g_aux_input_file;
char const * g_input_file = 0;
@@ -169,9 +169,6 @@ void parse_cmd_line_args(int argc, char ** argv) {
std::cout << "\n";
exit(0);
}
- else if (strcmp(opt_name, "smt") == 0) {
- g_input_kind = IN_SMTLIB;
- }
else if (strcmp(opt_name, "smt2") == 0) {
g_input_kind = IN_SMTLIB_2;
}
@@ -340,9 +337,6 @@ int STD_CALL main(int argc, char ** argv) {
else if (strcmp(ext, "smt2") == 0) {
g_input_kind = IN_SMTLIB_2;
}
- else if (strcmp(ext, "smt") == 0) {
- g_input_kind = IN_SMTLIB;
- }
else if (strcmp(ext, "mps") == 0 || strcmp(ext, "sif") == 0 ||
strcmp(ext, "MPS") == 0 || strcmp(ext, "SIF") == 0) {
g_input_kind = IN_MPS;
@@ -350,9 +344,6 @@ int STD_CALL main(int argc, char ** argv) {
}
}
switch (g_input_kind) {
- case IN_SMTLIB:
- return_value = read_smtlib_file(g_input_file);
- break;
case IN_SMTLIB_2:
memory::exit_when_out_of_memory(true, "(error \"out of memory\")");
return_value = read_smtlib2_commands(g_input_file);
diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index 666a1e1fe..8c716a81a 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -21,7 +21,6 @@ Revision History:
#include<iostream>
#include<time.h>
#include<signal.h>
-#include "parsers/smt/smtlib_solver.h"
#include "util/timeout.h"
#include "parsers/smt2/smt2parser.h"
#include "muz/fp/dl_cmds.h"
@@ -35,20 +34,14 @@ Revision History:
extern bool g_display_statistics;
static clock_t g_start_time;
-static smtlib::solver* g_solver = 0;
static cmd_context * g_cmd_context = 0;
static void display_statistics() {
clock_t end_time = clock();
- if ((g_solver || g_cmd_context) && g_display_statistics) {
+ if (g_cmd_context && g_display_statistics) {
std::cout.flush();
std::cerr.flush();
- if (g_solver) {
- g_solver->display_statistics();
- memory::display_max_usage(std::cout);
- std::cout << "time: " << ((static_cast<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC) << " secs\n";
- }
- else if (g_cmd_context) {
+ if (g_cmd_context) {
g_cmd_context->set_regular_stream("stdout");
g_cmd_context->display_statistics(true, ((static_cast<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC));
}
@@ -72,33 +65,6 @@ static void STD_CALL on_ctrl_c(int) {
raise(SIGINT);
}
-unsigned read_smtlib_file(char const * benchmark_file) {
- g_start_time = clock();
- register_on_timeout_proc(on_timeout);
- signal(SIGINT, on_ctrl_c);
- smtlib::solver solver;
- g_solver = &solver;
-
- bool ok = true;
-
- ok = solver.solve_smt(benchmark_file);
- if (!ok) {
- if (benchmark_file) {
- std::cerr << "ERROR: solving '" << benchmark_file << "'.\n";
- }
- else {
- std::cerr << "ERROR: solving input stream.\n";
- }
- }
-
- #pragma omp critical (g_display_stats)
- {
- display_statistics();
- register_on_timeout_proc(0);
- g_solver = 0;
- }
- return solver.get_error_code();
-}
unsigned read_smtlib2_commands(char const * file_name) {
g_start_time = clock();
diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp
index 3674e6b70..12fca706d 100644
--- a/src/test/quant_elim.cpp
+++ b/src/test/quant_elim.cpp
@@ -8,8 +8,6 @@ Copyright (c) 2015 Microsoft Corporation
#include "smt/params/smt_params.h"
#include "qe/qe.h"
#include "ast/ast_pp.h"
-#include "parsers/smt/smtlib.h"
-#include "parsers/smt/smtparser.h"
#include "util/lbool.h"
#include <sstream>
#include "ast/reg_decl_plugins.h"
@@ -54,6 +52,9 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons
static void test_formula(lbool expected_outcome, char const* fml) {
ast_manager m;
reg_decl_plugins(m);
+ // No-op requires SMTLIB2
+
+#if 0
scoped_ptr<smtlib::parser> parser = smtlib::parser::create(m);
parser->initialize_smtlib();
@@ -73,8 +74,10 @@ static void test_formula(lbool expected_outcome, char const* fml) {
for (; it != end; ++it) {
test_qe(m, expected_outcome, *it, 0);
}
+#endif
}
+
void tst_quant_elim() {
disable_debug("heap");