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

remove smtlib1 dependencies

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-28 10:37:30 -08:00
parent d7042c234f
commit 89971e2a98
18 changed files with 23 additions and 3918 deletions
Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_project.py
View file

@ -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)

1
src/CMakeLists.txt
View file

@ -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)

1
src/api/CMakeLists.txt
View file

@ -71,5 +71,4 @@ z3_add_component(api
opt
portfolio
realclosure
smtparser
)

37
src/api/api_context.cpp
View file

@ -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

12
src/api/api_context.h
View file

@ -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;
};

30
src/api/api_interp.cpp
View file

@ -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;

222
src/api/api_parsers.cpp
View file

@ -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("");
}

106
src/api/z3_api.h
View file

@ -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 */

8
src/parsers/smt/CMakeLists.txt
View file

@ -1,8 +0,0 @@
z3_add_component(smtparser
SOURCES
smtlib.cpp
smtlib_solver.cpp
smtparser.cpp
COMPONENT_DEPENDENCIES
portfolio
)

258
src/parsers/smt/smtlib.cpp
View file

@ -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
}

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

@ -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

119
src/parsers/smt/smtlib_solver.cpp
View file

@ -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;
}
}
};

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

@ -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

2760
src/parsers/smt/smtparser.cpp
View file

File diff suppressed because it is too large Load diff

48
src/parsers/smt/smtparser.h
View file

@ -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

11
src/shell/main.cpp
View file

@ -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);

38
src/shell/smtlib_frontend.cpp
View file

@ -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();

7
src/test/quant_elim.cpp
View file

@ -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");