Commits

Leonardo de Moura committed 95a2526

removed native low level parser

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

Comments (0)

Files changed (5)

src/api/api_parsers.cpp

 #include"cmd_context.h"
 #include"smt2parser.h"
 #include"smtparser.h"
-#include"z3_solver.h"
 
 extern "C" {
 
         return mk_c(c)->m_smtlib_error_buffer.c_str();
         Z3_CATCH_RETURN("");
     }
-    
-    Z3_ast parse_z3_stream(Z3_context c, std::istream& is) {
-        z3_solver parser(c, is, verbose_stream(), mk_c(c)->fparams(), false);
-        if (!parser.parse()) {
-            SET_ERROR_CODE(Z3_PARSER_ERROR);
-            return of_ast(mk_c(c)->m().mk_true());
-        }
-        expr_ref_vector assumptions(mk_c(c)->m());
-        parser.get_assumptions(assumptions);
-        return of_ast(mk_c(c)->mk_and(assumptions.size(), assumptions.c_ptr()));
-    }
-
-    Z3_ast Z3_API Z3_parse_z3_string(Z3_context c, Z3_string str) { 
-        Z3_TRY;
-        LOG_Z3_parse_z3_string(c, str);
-        std::string s(str);
-        std::istringstream is(s);
-        Z3_ast r = parse_z3_stream(c, is);
-        RETURN_Z3(r);
-        Z3_CATCH_RETURN(0);
-    }
-
-    Z3_ast Z3_API Z3_parse_z3_file(Z3_context c, Z3_string file_name) {
-        Z3_TRY;
-        LOG_Z3_parse_z3_file(c, file_name);
-        std::ifstream is(file_name);
-        if (!is) {
-            SET_ERROR_CODE(Z3_PARSER_ERROR);
-            return 0;
-        }
-        Z3_ast r = parse_z3_stream(c, is);
-        RETURN_Z3(r);
-        Z3_CATCH_RETURN(0);
-    }
 
     // ---------------
     // Support for SMTLIB2
     Z3_string Z3_API Z3_get_smtlib_error(__in Z3_context c);
 END_MLAPI_EXCLUDE
 
-    /**
-       \brief \mlh parse_z3_string c str \endmlh
-       Parse the given string using the Z3 native parser.
-       
-       Return the conjunction of asserts made in the input.
-
-       def_API('Z3_parse_z3_string', AST, (_in(CONTEXT), _in(STRING)))
-     */
-    Z3_ast Z3_API Z3_parse_z3_string(__in Z3_context c, __in Z3_string str);
-    
-    /**
-       \brief Similar to #Z3_parse_z3_string, but reads the benchmark from a file.
-
-       def_API('Z3_parse_z3_file', AST, (_in(CONTEXT), _in(STRING)))
-    */
-    Z3_ast Z3_API Z3_parse_z3_file(__in Z3_context c, __in Z3_string file_name);
-
     /*@}*/
 
 #ifdef CorML4

src/api/z3_solver.cpp

-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    z3_solver.cpp
-
-Abstract:
-
-    Native ast parser.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2007-07-17
-
-Revision History:
-
---*/
-
-#include "z3_solver.h"
-#include "z3_private.h"
-#include "warning.h"
-#include "ast_pp.h"
-#include "ast_ll_pp.h"
-#include "ast_smt_pp.h"
-#include "version.h"
-#include "array_decl_plugin.h"
-#include "bv_decl_plugin.h"
-#include "arith_decl_plugin.h"
-#include "lbool.h"
-#include <sstream>
-
-#define CHECK(_b_) if (!(_b_)) { return false; }
-
-#define CHECK_P(_b_,_m_) if (!(_b_)) { warning_msg(_m_); return false; }
-
-#define CHECK_CB(_b_,_cb_) if (!(_b_)) { _cb_; return false; }
-
-#define TRY_CHECK(_b_) if (!(_b_)) { return false; }
-
-
-ast_manager& Z3_get_manager(Z3_context c);
-Z3_context Z3_mk_context_from_params(front_end_params const& p);  
-void Z3_display_statistics(Z3_context c, std::ostream& s);
-void Z3_display_istatistics(Z3_context c, std::ostream& s);
-
-z3_solver::z3_solver(
-    Z3_context context,
-    std::istream& ins,
-    std::ostream& ous,
-    front_end_params & params,
-    bool is_active
-    )
-    : 
-    m_context(context?context:Z3_mk_context_from_params(params)),
-    m_owns_context(context?false:true),
-    m_manager(Z3_get_manager(m_context)),
-    m_params(params),
-    m_in(ins),
-    m_out(ous),
-    m_is_active(is_active),
-    m_assumptions(m_manager),
-    m_num_checks(0),
-    m_eof(false),
-    m_line(1),
-    m_arith(m_manager),
-    m_bv(m_manager),
-    m_pinned(m_manager),
-    m_last_check_result(Z3_L_UNDEF)
-{
-    add_builtins(m_manager.get_family_id("bv"));
-    add_builtins(m_manager.get_family_id("arith"));
-    add_builtins(m_manager.get_basic_family_id());
-    add_builtins(m_manager.get_family_id("array"));
-    add_builtins(m_manager.get_family_id("datatype"));
-}
-
-z3_solver::z3_solver(
-    ast_manager&  m,
-    std::istream& ins,
-    std::ostream& ous,
-    front_end_params & params
-    )
-    : 
-    m_context(0),
-    m_owns_context(true),
-    m_manager(m),
-    m_params(params),
-    m_in(ins),
-    m_out(ous),
-    m_is_active(false),
-    m_assumptions(m_manager),
-    m_num_checks(0),
-    m_eof(false),
-    m_line(1),
-    m_arith(m_manager),
-    m_bv(m_manager),
-    m_pinned(m_manager)
-{
-    add_builtins(m_manager.get_family_id("bv"));
-    add_builtins(m_manager.get_family_id("arith"));
-    add_builtins(m_manager.get_basic_family_id());
-    add_builtins(m_manager.get_family_id("array"));
-    add_builtins(m_manager.get_family_id("datatype"));
-
-}
-
-
-z3_solver::~z3_solver()
-{
-    m_assumptions.reset();
-    m_pinned.reset();
-    if (m_owns_context && m_context) {
-        Z3_del_context(m_context);
-    }
-}
-
-void z3_solver::skip_blank() {
-    while (*m_in == ' ' || *m_in == '\t' || *m_in == '\r') {
-        ++m_in;
-    }
-}
-
-bool z3_solver::next_token() {    
-    if (m_eof) {
-        warning_msg("line %d. EOF reached, expecting string", m_line);
-        return false;
-    }
-    skip_blank();
-    if (*m_in == EOF) {
-        m_eof = true;
-        return true;
-    }
-    m_string.clear();
-    while (*m_in != '\n' && *m_in != ' ' && 
-           *m_in != '\r' &&
-           *m_in != '\t' && *m_in != EOF) {
-        m_string.push_back(*m_in);
-        ++m_in;
-    }   
-    if (*m_in == '\n' && m_string.empty()) {
-        m_string = "\n";
-        ++m_in;
-    }
-    return true;
-}
-
-
-bool z3_solver::try_parse(char const* token) {
-    CHECK(!m_eof);
-    TRY_CHECK(strcmp(token, m_string.c_str()) == 0);
-    CHECK(next_token());
-    return true;
-}
-
-bool z3_solver::parse_int(int& i) {
-    if (m_eof) {
-        warning_msg("line %d. EOF reached, expecting numeral", m_line);
-        return false;
-    }
-    const char* s = m_string.c_str();    
-    i = 0;
-    bool negate = false;
-    if (*s == '-') {
-        negate = true;
-        ++s;
-    }
-    // NB: overflow checks are ignored.
-    while ('0' <= *s && *s <= '9') {
-        i = (i*10) + (*s - '0');
-        ++s;
-    }
-    if (negate) {
-        i = -i;
-    }
-    CHECK(next_token());    
-    return true;
-}
-
-bool z3_solver::check_int(int& i) {
-    if (m_eof) {
-        return false;
-    }
-    const char* s = m_string.c_str();    
-    bool negate = false;
-    i = 0;
-    if (!(('0' <= *s && *s <= '9') || *s == '-')) {
-        return false;
-    }
-    if (*s == '-') {
-        negate = true;
-        ++s;
-    }
-    while ('0' <= *s && *s <= '9') {
-        i = (i*10) + (*s - '0');
-        ++s;
-    }
-    if (negate) {
-        i = -i;
-    }
-    return true;
-}
-
-bool z3_solver::parse_unsigned(unsigned& i) {
-    if (m_eof) {
-        warning_msg("line %d. EOF reached, expecting numeral", m_line);
-        return false;
-    }
-    const char* s = m_string.c_str();    
-    i = 0;
-    // NB: overflow checks are ignored.
-    while ('0' <= *s && *s <= '9') {
-        i = (i*10) + (*s - '0');
-        ++s;
-    }
-    CHECK(next_token());    
-    return true;
-}
-
-bool z3_solver::check_unsigned(unsigned& i) {
-    if (m_eof) {
-        return false;
-    }
-    const char* s = m_string.c_str();    
-    i = 0;
-    if (!('0' <= *s && *s <= '9')) {
-        return false;
-    }
-    while ('0' <= *s && *s <= '9') {
-        i = (i*10) + (*s - '0');
-        ++s;
-    }
-    return true;
-}
-
-
-bool z3_solver::parse_id(symbol& id) {
-    size_t sz = m_string.size();
-    char const* str = m_string.c_str();
-    if (strcmp(str,"\"null\"") == 0) {
-        id = symbol();
-    }
-    else if (sz > 0 && str[0] == '"' && str[sz-1] == '"') {
-        std::string s(str,sz-1);
-        id = s.c_str();
-    }
-    else {
-        id = m_string.c_str();
-    }
-    CHECK(next_token());
-    return true;
-}
-
-
-bool z3_solver::parse_rational(rational& r) {
-    if (m_eof) {
-        warning_msg("line %d. EOF reached, expecting rational", m_line);
-        return false;
-    }
-    r = rational(m_string.c_str());
-    CHECK(next_token());
-    return true;
-}
-
-
-bool z3_solver::parse_eol() {
-    if (m_eof) {
-        warning_msg("line %d. EOF reached, expecting newline", m_line);
-        return false;
-    }
-    if (m_string[0] != '\n') {
-        warning_msg("line %d. Expecting newline, got '%s'\n", m_line, m_string.c_str());
-        return false;
-    }    
-    ++m_line;
-    CHECK(next_token());
-
-    return true;
-}
-
-
-z3_solver::kind z3_solver::parse_kind() {
- try_again:
-    if (m_eof) {
-        return T_EOF;
-    }
-    kind k = T_ERR;
-
-    switch(m_string[0]) {
-    case 'A':
-        if (strcmp(m_string.c_str(), "Assert") == 0) {
-            k = T_ASSERT;
-        }
-        else if (strcmp(m_string.c_str(), "App") == 0) {
-            k = T_BUILTIN_CONST;
-        }
-        break;
-    case 'C':
-        if (strcmp(m_string.c_str(), "Const") == 0) {
-            k = T_NULLARY_CONST;
-        }
-        else if (strcmp(m_string.c_str(), "Check") == 0) {
-            k = T_CHECK;
-        }
-        else if (strcmp(m_string.c_str(), "CheckAssumptions") == 0) {
-            k = T_CHECK_ASSUMPTIONS;
-        }
-        break;
-    case 'D':
-        if (strcmp(m_string.c_str(), "Dec") == 0) {
-            k = T_DEC;
-        }
-        else if (strcmp(m_string.c_str(), "DbgSat") == 0) {
-            k = T_DBG_SAT;
-        }
-        else if (strcmp(m_string.c_str(), "DbgUnsat") == 0) {
-            k = T_DBG_UNSAT;
-        }
-        break;
-    case 'E':
-        if (strcmp(m_string.c_str(), "Echo") == 0) {
-            k = T_ECHO;
-        }
-        break;
-    case 'F':
-        if (strcmp(m_string.c_str(), "Fun") == 0) {
-            k = T_FUNCTION_CONST;
-        }
-        break;
-    case 'G':
-        if (strcmp(m_string.c_str(), "GetImpliedEqualities") == 0) {
-            k = T_GET_IMPLIED_EQUALITIES;
-        }
-        break;
-    case 'L':
-        if (strcmp(m_string.c_str(), "Lab") == 0) {
-            k = T_LAB;
-        }
-        break;
-    case 'N':
-        if (strcmp(m_string.c_str(), "Num") == 0) {
-            k = T_NUM;
-        }
-        break;
-    case 'P':
-        if (strcmp(m_string.c_str(), "Pat") == 0) {
-            k = T_PAT;
-        }
-        else if (strcmp(m_string.c_str(), "Push") == 0) {
-            k = T_PUSH;
-        }
-        else if (strcmp(m_string.c_str(), "Pop") == 0) {
-            k = T_POP;
-        }
-        break;
-    case ';':
-        k = T_COMMENT;
-        break;
-    case '\n':
-        if (!next_token()) {
-            k = T_ERR;
-            break;
-        }
-        goto try_again;
-    case 'Q':
-        if (strcmp(m_string.c_str(), "Qua") == 0) {
-            k = T_QUA;
-        }
-        break;
-    case 'R':
-        if (strcmp(m_string.c_str(), "Reset") == 0) {
-            k = T_RESET;
-        }
-        break;
-    case 'S':
-        if (strcmp(m_string.c_str(), "Solver") == 0) {
-            k = T_SOLVER;
-        }
-        else if (strcmp(m_string.c_str(), "Simplify") == 0) {
-            k = T_SIMPLIFY;
-        }
-        break;
-    case 'T':
-        if (strcmp(m_string.c_str(), "Ty") == 0) {
-            k = T_TY;
-        }
-        else if (strcmp(m_string.c_str(), "Type") == 0) {
-            k = T_TYPE;
-        }
-        break;
-    case 'V':
-        if (strcmp(m_string.c_str(), "Var") == 0) {
-            k = T_VAR;
-        }
-        else if (strcmp(m_string.c_str(), "Version") == 0) {
-            k = T_VERSION;
-        }
-        break;
-    default:
-        break;
-    }
-    if (k == T_ERR) {
-        warning_msg("line %d. could not recognize token '%s'", m_line, m_string.c_str());
-    }
-    else if (!next_token()) {
-        k = T_ERR;
-        warning_msg("line %d. could not recognize token '%s'", m_line, m_string.c_str());
-    }
-    return k;
-    
-}
-
-bool z3_solver::parse_comment() {
-    while (m_string[0] != '\n') {
-        CHECK(next_token());
-    }
-    CHECK(parse_eol());
-    return true;
-}
-
-bool z3_solver::parse_numeral() {
-    symbol    id;
-    rational  r;
-    sort* s;
-    expr* n;
-    CHECK(parse_id(id));
-    CHECK(parse_rational(r));
-    CHECK(parse_ast<sort>(s, sort_coerce()));
-    CHECK(parse_eol());
-    if (m_arith.is_int(s)) {
-        n = m_arith.mk_numeral(r, true);
-    }
-    else if (m_arith.is_real(s)) {
-        n = m_arith.mk_numeral(r, false);
-    }
-    else if (m_bv.is_bv_sort(s)) {
-        n = m_bv.mk_numeral(r, s);
-    }
-    else {
-        return false;
-    }
-    add_id(id, n);
-    return true;
-}
-
-
-bool z3_solver::parse_var() {
-    symbol    id;
-    unsigned  n;
-    sort* ty;
-
-    CHECK(parse_id(id));
-    CHECK(parse_unsigned(n));
-    CHECK(parse_ast<sort>(ty,sort_coerce()));
-    CHECK(parse_eol());
-
-    var* v = m_manager.mk_var(n, ty);
-    add_id(id, v);
-    return true;
-}
-
-
-family_id z3_solver::get_family_id(char const* s) {
-    symbol sym(s);
-    if (sym == "null") {
-        return null_family_id;
-    }
-    else {
-        return m_manager.get_family_id(sym);
-    }
- 
-}
-
-bool z3_solver::parse_info(scoped_ptr<func_decl_info>& info) {
-    bool is_assoc = false;
-    bool is_comm = false;
-    bool is_inj = false;
-    vector<parameter> params;
-    family_id fid = null_family_id;
-    decl_kind kind = null_decl_kind;
-
-    if (!try_parse("BUILTIN")) {
-        info = 0;
-        return true;
-    }
-    
-    fid = get_family_id(m_string.c_str());
-
-    CHECK(next_token());
-    CHECK(parse_int(kind));
-    
-    while (m_string[0] != '\n') {
-        std::string s;
-
-        if (strcmp(m_string.c_str(), ":assoc") == 0) {
-            is_assoc = true;
-        }
-        else if (strcmp(m_string.c_str(), ":comm") == 0) {
-            is_comm = true;
-        }
-        else if (strcmp(m_string.c_str(), ":inj") == 0) {
-            is_inj = true;
-        }
-        else {
-            CHECK(parse_parameter(params));
-            continue;
-        }
-        CHECK(next_token());
-    }
-
-    
-    info = alloc(func_decl_info, fid, kind, params.size(), params.c_ptr());
-    info->set_associative(is_assoc);
-    info->set_commutative(is_comm);
-    info->set_injective(is_inj);
-    return true;
-}
-
-
-bool z3_solver::parse_info(scoped_ptr<sort_info>& info) {
-    vector<parameter> params;
-    bool is_infinite = true;
-    rational num_elems;
-    family_id fid = null_family_id;
-    decl_kind kind = null_decl_kind;
-
-    if (!try_parse("BUILTIN")) {
-        info = 0;
-        return true;
-    }
-
-    fid = get_family_id(m_string.c_str());
-    std::string th = m_string.c_str();
-
-    CHECK(next_token());
-    CHECK(parse_int(kind));
-
-    if (try_parse("Size")) {
-        CHECK(parse_rational(num_elems)); 
-        is_infinite = false;
-    }
-    
-    while (m_string[0] != '\n') {
-        CHECK(parse_parameter(params));
-    }
-    
-    if (!is_infinite && num_elems.is_uint64()) {
-        info = alloc(sort_info, fid, kind, num_elems.get_uint64(), params.size(), params.c_ptr());
-    }
-    else {
-        info = alloc(sort_info, fid, kind, params.size(), params.c_ptr());
-    }
-    return true;
-}
-
-
-bool z3_solver::parse_nullary_const() {
-    func_decl* d = 0;
-    app* n = 0;
-    symbol id;
-    CHECK(parse_func_decl(id, d));
-    SASSERT(d);
-    n = m_manager.mk_const(d);
-    CHECK(n);
-    add_id(id, n);
-    return true;
-
-}
-
-bool z3_solver::parse_func_decl() {
-    func_decl* d = 0;
-    symbol id;
-    CHECK(parse_func_decl(id, d));
-    CHECK(d);
-    add_id(id, d);
-    return true;
-}
-
-bool z3_solver::parse_func_decl(symbol& id, func_decl*& n) {
-    symbol name;
-    sort_ref_vector args(m_manager);
-    scoped_ptr<func_decl_info> info;
-    CHECK(parse_id(id));
-    CHECK(parse_id(name));
-    CHECK(parse_asts<sort>(args,sort_coerce()));
-    CHECK(parse_info(info));
-    CHECK(parse_eol());
-    if (args.size() == 0) {
-        warning_msg("line %d. Expecting more than 0 arguments", m_line);
-        return false;
-    }
-    unsigned dom_size = args.size()-1;
-    sort* rng = args[dom_size].get();
-
-    if (info.get()) {
-        n = m_manager.mk_func_decl(
-            info.get()->get_family_id(),
-            info.get()->get_decl_kind(),
-            info.get()->get_num_parameters(), 
-            info.get()->get_parameters(), 
-            dom_size, args.c_ptr());
-
-        // HACK: not all theories have name-less decl_kinds:
-        // constructors, tuples, marbles, etc.
-        if (!n) {
-            n = m_manager.mk_func_decl(name, dom_size, args.c_ptr(), rng, *info.get());
-        }
-    }
-    else {
-        n = m_manager.mk_func_decl(name, dom_size, args.c_ptr(), rng);
-    }
-    CHECK(n);
-    add_id(id, n);
-    return true;
-}
-
-bool z3_solver::parse_const() {
-    symbol id;
-    func_decl* d;
-    expr_ref_vector args(m_manager);
-    CHECK(parse_id(id));
-    CHECK(parse_ast<func_decl>(d,func_decl_coerce()));
-    CHECK(parse_asts<expr>(args, expr_coerce()));
-    CHECK(parse_eol());
-    app* n = m_manager.mk_app(d, args.size(), args.c_ptr());
-    CHECK(n);
-    if (!m_manager.check_sorts(n))
-        return false;
-    add_id(id, n);
-    return true;
-}
-
-
-// App n name [ params ] args 
-
-bool z3_solver::find_builtin_op(symbol name, family_id & fid, decl_kind& kind) {
-    builtin_info bi;
-    CHECK(m_builtin_ops.find(name, bi));
-    fid = bi.m_fid;
-    kind = bi.m_kind;
-    return true;
-}
-
-bool z3_solver::find_builtin_type(symbol name, family_id & fid, decl_kind& kind) {
-    builtin_info bi;
-    if (!m_builtin_types.find(name, bi)) {
-        return false;
-    }
-    fid = bi.m_fid;
-    kind = bi.m_kind;    
-    return true;
-}
-
-void z3_solver::add_builtins(family_id fid) {
-    decl_plugin* plugin = m_manager.get_plugin(fid);
-    SASSERT(plugin);
-    if (!plugin) {
-        return;
-    }
-    svector<builtin_name> op_names;
-    plugin->get_op_names(op_names);
-    for (unsigned i = 0; i < op_names.size(); ++i) {
-        m_builtin_ops.insert(op_names[i].m_name, builtin_info(fid, op_names[i].m_kind));
-    }
-    
-    svector<builtin_name> sort_names;
-    plugin->get_sort_names(sort_names);
-    for (unsigned i = 0; i < sort_names.size(); ++i) {
-        m_builtin_types.insert(sort_names[i].m_name, builtin_info(fid, sort_names[i].m_kind));
-    }
-}
-
-
-
-bool z3_solver::parse_parameter(vector<parameter>& params) {
-    ast* a = 0;
-    int n;
-    if (check_int(n)) {
-        params.push_back(parameter(n));
-    }
-    else if (m_table.find(symbol(m_string.c_str()), a)) {
-        params.push_back(parameter(a));
-    }
-    else {
-        symbol sym;
-        if (!parse_id(sym)) {
-            return false;
-        }
-        params.push_back(parameter(sym));
-        return true;
-    }
-    CHECK(next_token());
-    return true;
-}
-
-
-bool z3_solver::parse_params(vector<parameter>& params) {
-    if (strcmp(m_string.c_str(),"[") == 0) {
-        CHECK(next_token());
-        while (strcmp(m_string.c_str(),"]") != 0) {
-            CHECK(parse_parameter(params));
-        }
-        CHECK(next_token());
-    }
-    return true;
-}
-
-
-
-bool z3_solver::parse_builtin_const() {
-    symbol id, name;
-    vector<parameter> params;
-    family_id fid;
-    decl_kind kind;
-    app* n = 0;
-    expr_ref_vector args(m_manager);
-    CHECK(parse_id(id));
-    CHECK(parse_id(name));
-    CHECK(parse_params(params));
-    CHECK(parse_asts<expr>(args, expr_coerce()));
-    CHECK(parse_eol());
-
-    if (find_builtin_op(name, fid, kind)) {        
-        n = m_manager.mk_app(fid, kind, 
-                               params.size(), params.c_ptr(), 
-                               args.size(), args.c_ptr());
-    }
-    else {
-        func_decl* d = 0;
-        CHECK(parse_ast<func_decl>(name, d, func_decl_coerce()));
-        CHECK(d);
-        n = m_manager.mk_app(d, args.size(), args.c_ptr());
-    }
-
-    CHECK(n);
-    if (!m_manager.check_sorts(n))
-        return false;
-    add_id(id, n);
-    return true;
-}
-
-
-bool z3_solver::parse_type() {
-    symbol id, name;
-    scoped_ptr<sort_info> info;
-    CHECK(parse_id(id));
-    CHECK(parse_id(name));
-    CHECK(parse_info(info));
-    CHECK(parse_eol());
-    sort* ty;
-    if (info.get()) {
-        ty = m_manager.mk_sort(name, *info.get());
-    }
-    else {
-        ty = m_manager.mk_sort(name);
-    }
-    CHECK(ty);
-    add_id(id, ty);
-    return true;
-}
-
-
-bool z3_solver::parse_type_new() {
-    symbol id, name;
-    vector<parameter> params;
-    CHECK(parse_id(id));
-    CHECK(parse_id(name));
-    CHECK(parse_params(params));
-    CHECK(parse_eol());
-    sort* ty;
-    family_id fid;
-    decl_kind kind;
-    if (find_builtin_type(name, fid, kind)) {
-        ty = m_manager.mk_sort(fid, kind, params.size(), params.c_ptr());
-    }
-    else {
-        ty = m_manager.mk_sort(name);
-    }
-    CHECK(ty);
-    add_id(id, ty);
-    return true;
-}
-
-
-bool z3_solver::parse_label() {
-    symbol id, name;
-    std::string s;
-    expr* a;
-    CHECK(parse_id(id));
-    CHECK(next_token());
-    s = m_string;
-    CHECK(parse_id(name));
-    CHECK(parse_ast<expr>(a, expr_coerce()));
-    CHECK(parse_eol());
-    bool pos = (strcmp("LBLPOS",s.c_str()) == 0);
-    app* n = m_manager.mk_label(pos, name, a);
-    CHECK(n);
-    add_id(id, n);
-    return true;    
-}
-
-bool z3_solver::parse_quantifier() {
-    std::string s;
-    symbol id;
-    unsigned num_decls, num_patterns;
-    expr* body;
-    bool is_forall;
-    unsigned weight;
-    symbol skid, qid;
-    svector<symbol> names;
-    ptr_vector<sort> types;
-    ptr_vector<expr> patterns;
-
-    CHECK(parse_id(id));
-    s = m_string;
-    CHECK(next_token());
-    is_forall = (strcmp("FORALL",s.c_str()) == 0);
-    CHECK_P(parse_unsigned(weight), "Expected unsigned integer");
-    CHECK_P(parse_id(skid), "Expected symbol identifier");
-    CHECK_P(parse_id(qid), "Expected symbol identifier");
-    CHECK_P(parse_unsigned(num_decls), "Expected unsigned integer for number of declarations");
-    for (unsigned i = 0; i < num_decls; ++i) {
-        symbol name;
-        sort* ty;
-        CHECK_P(parse_id(name), "Expected identifier");
-        CHECK_P(parse_ast<sort>(ty, sort_coerce()), "Expected sort");
-        names.push_back(name);
-        types.push_back(ty);
-    }
-    CHECK_P(parse_unsigned(num_patterns), "Expected unsigned integer for number of patterns");
-    for (unsigned i = 0; i < num_patterns; ++i) {
-        app* p;
-        CHECK_P(parse_ast<app>(p, pattern_coerce(m_manager)), "Expected pattern");
-        patterns.push_back(p);
-    }
-    CHECK_P(parse_ast<expr>(body, expr_coerce()), "Expected expression");
-    CHECK(parse_eol());
-
-    CHECK_P(m_manager.is_bool(body), "Body of quantifier should be Boolean type");
-    CHECK_P(!m_manager.is_pattern(body), "Body of quantifier cannot be a pattern");
-
-
-#if 0
-    if (qid == symbol() && m_params.m_default_qid) {
-        qid = symbol(m_line);
-    }
-#endif
-    if (num_decls > 0) {
-        quantifier* n = m_manager.mk_quantifier(
-            is_forall, 
-            num_decls, types.c_ptr(), names.c_ptr(), body,
-            weight, qid, skid, 
-            num_patterns, patterns.c_ptr()
-            );
-        CHECK(n);
-        add_id(id, n);
-    }
-    else {
-        add_id(id, body);
-    }
-    return true;
-}
-
-
-
-bool z3_solver::parse_pattern() {
-    symbol id;
-    app_ref_vector patterns(m_manager);
-    CHECK(parse_id(id));
-    CHECK(parse_asts<app>(patterns, app_coerce()));
-    CHECK(parse_eol());
-    app* n = m_manager.mk_pattern(patterns.size(), patterns.c_ptr());
-    CHECK(n);
-    add_id(id, n);
-    return true;
-}
-
-
-
-bool z3_solver::parse_assert()
-{
-    expr* a = 0;
-    CHECK(parse_ast<expr>(a, expr_coerce()));
-    CHECK(parse_eol());
-    if (m_params.m_ast_ll_pp) {
-        ast_ll_pp(m_out, m_manager, a, true);
-        m_out.flush();
-    }
-    if (m_params.m_ast_smt_pp) {
-        for (unsigned i = 0; i < m_pinned_lim.size(); ++i) {
-            m_out << " ";
-        }
-        m_out << mk_pp(a, m_manager) << "\n";
-        m_out.flush();
-    }
-    if (m_is_active && m_context) {
-        Z3_assert_cnstr(m_context, reinterpret_cast<Z3_ast>(a));
-        if (m_params.m_smtlib_trace_path.size() > 0) {
-            m_assumptions.push_back(a);
-        }
-    }
-    else {
-        m_assumptions.push_back(a);
-    }
-    return true;
-}
-
-
-bool z3_solver::parse_simplify()
-{
-    expr* a = 0;
-    CHECK(parse_ast<expr>(a, expr_coerce()));
-    CHECK(parse_eol());
-    if (m_params.m_ast_ll_pp) {
-        ast_ll_pp(m_out, m_manager, a, true);
-        m_out.flush();
-    }
-    if (m_params.m_ast_smt_pp) {
-        for (unsigned i = 0; i < m_pinned_lim.size(); ++i) {
-            m_out << " ";
-        }
-        m_out << mk_pp(a, m_manager) << "\n";
-        m_out.flush();
-    }
-    if (m_is_active && m_context) {
-        Z3_ast r = Z3_simplify(m_context, reinterpret_cast<Z3_ast>(a));
-        m_out << mk_pp(reinterpret_cast<ast*>(r), m_manager) << "\n";
-        m_out.flush();        
-    }
-    return true;
-}
-
-
-
-bool z3_solver::parse_check()
-{
-    CHECK(parse_eol());
-
-    if (!m_context || !m_is_active) {
-        return true;
-    }
-    
-    Z3_model m = 0;    
-    Z3_ast pr  = 0;
-    Z3_lbool result = Z3_check_assumptions(m_context, 0, 0, &m, &pr, 0, 0);
-    m_last_check_result = result;
-    
-    // display the model.
-
-    if (m && m_params.m_model) {
-        char const* md = Z3_model_to_string(m_context, m);
-        if (md) {
-            m_out << md;
-        }
-    }
-    if (m) {
-        Z3_del_model(m_context, m);
-    }
-
-    if (result == Z3_L_FALSE && pr != 0 && m_params.m_display_proof) {
-        m_out << mk_ll_pp(reinterpret_cast<ast*>(pr), m_manager, true, false);
-    }
-
-    switch(result) {
-    case l_false: m_out << "unsat\n"; break;
-    case l_true: m_out << "sat\n"; break;
-    case l_undef: m_out << "unknown\n"; break;
-    }
-    m_out.flush();
-
-    dump_smtlib_benchmark(0, 0, result);    
-    return true;
-}
-
-void z3_solver::dump_smtlib_benchmark(unsigned num_assumptions, expr* const* assumptions, Z3_lbool result) {
-    //
-    // Generate SMT-LIB benchmark from current set of assertions.
-    // 
-    if (m_params.m_dump_goal_as_smt || m_params.m_smtlib_trace_path.size() > 0) {
-        ast_smt_pp pp(m_manager);
-        pp.set_logic(m_params.m_smtlib_logic.c_str());
-        pp.set_source_info(m_params.m_smtlib_source_info.c_str());
-        pp.set_category(m_params.m_smtlib_category.c_str());
-        for (unsigned i = 0; i < m_assumptions.size(); ++i) {
-            pp.add_assumption(m_assumptions[i].get());
-        }
-        for (unsigned i = 0; i < num_assumptions; ++i) {
-            pp.add_assumption_star(assumptions[i]);
-        }
-        char const* status = (result == Z3_L_FALSE)?"unsat":((result == Z3_L_TRUE)?"sat":"unknown");
-        pp.set_status(status);
-        std::ostringstream buffer;
-        if (m_params.m_smtlib_trace_path.size() > 0) {
-            buffer << m_params.m_smtlib_trace_path.c_str() << "_" << m_num_checks << ".smt2";
-        }
-        else {
-            buffer << "query." << m_num_checks << ".smts";
-        }
-        std::ofstream out(buffer.str().c_str());
-        if (!out.fail() && !out.bad()) {
-            pp.display_smt2(out, m_manager.mk_true());
-        }
-        m_num_checks++;
-        out.close();
-    }
-
-}
-
-
-bool z3_solver::parse_get_implied_equalities() 
-{
-    expr_ref_vector args(m_manager);    
-    unsigned_vector cls;
-    CHECK(parse_asts<expr>(args, expr_coerce()));
-    CHECK(parse_eol());
-    cls.resize(args.size());
-
-    if (!m_context) {
-        return true;
-    }
-    
-
-    TRACE("get_implied_equalities", tout << "checking assumptions...\n" << Z3_context_to_string(m_context) << "\n";);
-    Z3_lbool result = Z3_get_implied_equalities(m_context, args.size(), reinterpret_cast<Z3_ast*>(args.c_ptr()), cls.c_ptr());
-    TRACE("get_implied_equalities", tout << "after checking assumptions...\n" << Z3_context_to_string(m_context) << "\n";);
-    m_last_check_result = result;
-    
-    m_out << ";Implied Equality Classes: ";
-    for (unsigned i = 0; i < cls.size(); ++i) {
-        m_out << cls[i] << " ";
-    }
-    m_out << "\n";
-
-    m_out.flush();
-    
-    return true;    
-}
-
-
-bool z3_solver::parse_check_assumptions()
-{
-    expr_ref_vector args(m_manager);    
-    CHECK(parse_asts<expr>(args, expr_coerce()));
-    CHECK(parse_eol());
-
-    if (!m_context) {
-        return true;
-    }
-
-    Z3_model m = 0;
-    
-    Z3_ast pr  = 0;
-
-    TRACE("check_assumptions", tout << "checking assumptions...\n" << Z3_context_to_string(m_context) << "\n";);
-    Z3_lbool result = Z3_check_assumptions(m_context, args.size(), reinterpret_cast<Z3_ast*>(args.c_ptr()), &m, &pr, 0, 0);
-    TRACE("check_assumptions", tout << "after checking assumptions...\n" << Z3_context_to_string(m_context) << "\n";);
-    m_last_check_result = result;
-    
-    // display the model.
-
-    if (m && m_params.m_model) {
-        char const* md = Z3_model_to_string(m_context, m);
-        if (md) {
-            m_out << md;
-        }
-    }
-    if (m) {
-        Z3_del_model(m_context, m);
-    }
-
-    if (result == Z3_L_FALSE && pr != 0 && m_params.m_display_proof) {
-        m_out << mk_ll_pp(reinterpret_cast<ast*>(pr), m_manager, true, false);
-    }
-
-    switch(result) {
-    case l_false: m_out << "unsat\n"; break;
-    case l_true: m_out << "sat\n"; break;
-    case l_undef: m_out << "unknown\n"; break;
-    }
-    m_out.flush();
-
-    dump_smtlib_benchmark(args.size(), args.c_ptr(), result);
-    
-    return true;
-}
-
-bool z3_solver::parse_dbg(bool expected_sat) {
-    CHECK(parse_eol());
-    if (m_last_check_result == Z3_L_FALSE && expected_sat) {
-        m_out << "!!!!!!!!BUG FOUND!!!!!!!!!\n";
-        throw z3_error(ERR_UNSOUNDNESS);
-    }
-    if (m_last_check_result == Z3_L_TRUE && !expected_sat) {
-        m_out << "!!!!!!!!BUG FOUND!!!!!!!!!\n";
-        throw z3_error(ERR_INCOMPLETENESS);
-    } 
-    if (m_last_check_result == Z3_L_UNDEF) {
-        throw z3_error(ERR_UNKNOWN_RESULT);
-    }
-    return true;
-}
-
-bool z3_solver::parse_push()
-{
-    CHECK(parse_eol());
-    if (m_context) {
-        Z3_push(m_context);
-    }
-    m_pinned_lim.push_back(m_pinned.size());
-    m_assumptions_lim.push_back(m_assumptions.size());
-    return true;
-}
-
-
-bool z3_solver::parse_pop()
-{
-    CHECK(parse_eol());
-    if (m_context) {
-        Z3_pop(m_context, 1);
-    }
-    m_pinned.resize(m_pinned_lim.back());
-    m_pinned_lim.pop_back();
-    m_assumptions.resize(m_assumptions_lim.back());
-    m_assumptions_lim.pop_back();
-    return true;
-}
-
-
-bool z3_solver::parse_reset()
-{
-    CHECK(parse_eol());
-    if (m_context) {
-        Z3_del_context(m_context);
-        Z3_config m_config = 0; // TBD.
-        m_context = Z3_mk_context(m_config);
-    }
-    return true;
-}
-
-bool z3_solver::parse_echo()
-{
-    CHECK(parse_eol());
-    // TBD
-    return true;
-}
-
-bool z3_solver::parse_version()
-{
-    unsigned major, minor;
-    CHECK(parse_unsigned(major));
-    CHECK(parse_unsigned(minor));
-    CHECK(next_token()); // build date
-    CHECK(next_token()); // revision
-    CHECK(parse_eol());
-    if (major != Z3_MAJOR_VERSION) {
-        warning_msg("Parser is incompatible. Major version %d has changed to %d", major, Z3_MAJOR_VERSION);
-        return false;
-    }
-    if (minor > Z3_MINOR_VERSION) {
-        warning_msg("Parser is incompatible. Minor version %d of parser is younger than %d", Z3_MINOR_VERSION, minor);
-        return false;
-    }
-    return true;
-}
-
-
-bool z3_solver::parse_solver()
-{
-    std::string s;
-    const char * str;
-    s = m_string;
-    CHECK(next_token());
-    CHECK(parse_eol());
-    str = s.c_str();
-#if 0
-    if (!m_solver) {
-
-    }
-    else if (strcmp(str,"LIA") == 0) {
-        m_solver->register_arith(unmanaged_wrapper::LIA);
-    }
-    else if (strcmp(str,"LRA") == 0) {
-        m_solver->register_arith(unmanaged_wrapper::MIA);
-    }
-    else if (strcmp(str,"BV") == 0) {
-        m_solver->register_bv();
-    }
-#endif 
-    return true;
-}
-
-bool z3_solver::parse() 
-{
-    next_token();
-    bool ok = true;
-    while (ok) {
-        switch(parse_kind()) {
-        case T_NUM:
-            ok = parse_numeral();
-            break;
-        case T_VAR:
-            ok = parse_var();
-            break;
-        case T_DEC:
-            ok = parse_func_decl();
-            break;
-        case T_FUNCTION_CONST:
-            ok = parse_const();
-            break;
-        case T_GET_IMPLIED_EQUALITIES:
-            ok = parse_get_implied_equalities();
-            break;
-        case T_NULLARY_CONST:
-            ok = parse_nullary_const();
-            break;
-        case T_BUILTIN_CONST:
-            ok = parse_builtin_const();
-            break;
-        case T_TY:
-            ok = parse_type();
-            break;
-        case T_TYPE:
-            ok = parse_type_new();
-            break;
-        case T_QUA:
-            ok = parse_quantifier();
-            break;
-        case T_LAB:
-            ok = parse_label();
-            break;
-        case T_PAT:
-            ok = parse_pattern();
-            break;
-        case T_ASSERT:
-            ok = parse_assert();
-            break;
-        case T_SOLVER:
-            ok = parse_solver();
-            break;
-        case T_SIMPLIFY:
-            ok = parse_simplify();
-            break;
-        case T_PUSH:
-            ok = parse_push();
-            break;
-        case T_CHECK:
-            ok = parse_check();
-            break;
-        case T_CHECK_ASSUMPTIONS:
-            ok = parse_check_assumptions();
-            break;
-        case T_DBG_SAT:
-            ok = parse_dbg(true);
-            break;
-        case T_DBG_UNSAT:
-            ok = parse_dbg(false);
-            break;
-        case T_POP:
-            ok = parse_pop();
-            break;
-        case T_RESET:
-            ok = parse_reset();
-            break;
-        case T_COMMENT:
-            ok = parse_comment();
-            break;
-        case T_ECHO:
-            ok = parse_echo();
-            break;
-        case T_VERSION:
-            ok = parse_version();
-            break;
-        case T_EOF:
-            return true;
-        case T_ERR:
-            return false;
-        case T_CTX:
-            // [Leo]: this case is not handled.
-            break;
-        }
-    }
-    if (!ok) {
-        warning_msg("line %d. error encountered", m_line);
-    }
-    return ok;
-}
-
-void z3_solver::display_statistics(std::ostream& out, bool istats)
-{
-    if (m_context) {
-        if (istats) {
-            Z3_display_istatistics(m_context, out);
-        }
-        else {
-            Z3_display_statistics(m_context, out);
-        }
-    }
-}
-
-void z3_solver::add_id(symbol const& id, ast* n) {
-    m_table.insert(id, n);
-    m_pinned.push_back(n);
-}
-

src/api/z3_solver.h

-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    z3_solver.h
-
-Abstract:
-
-    Native ast parser.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2007-07-17
-
-Revision History:
-
---*/
-
-/**
-  \defgroup z3native Z3 low level input format 
-
-  This format is mainly used for generating logs. These logs
-  capture the expressions created using the Z3 API, and 
-  the main commands available there.
-  It is very low-level and follows 
-  some of the conventions found in the DIMACS format for SAT problems 
-  and by the <a class="el" href="http://www.cs.ubc.ca/~babic/index_spear.htm">Spear</a>
-  input format.
-
-  The format is extensible, as the grammar allows for 
-  selecting solvers and adding \emph{semantic attachments} 
-  with constructors. The <a class="el" href="http://www.smtlib.org">SMT-LIB</a> and Simplify text formats are easier to
-  write and read for a human consumer.
-
-  Every line consists of a command that gets interpreted
-  as a declaration of a node in anbstract syntax tree, or as
-  a control instruction to Z3, such as to augment the current
-  context with constraints or check for satisfiability.
-
-  \nicebox{
-    <i>command</i> := 
-      | <i>ast</i>
-      | <i>control </i>
-      | <i> ; commented line </i>      
-  }
-
-
-  White spaces are implicit in the production rules.
-  The legal white-spaces have the ASCII representations
-
-  \nicebox{
-     ' ' | \ t | \ r
-  }
-
-  Comment lines start with \c ;.
-  All characters up to the newline \ n are ignored.
-
-  We use <i>id</i> for identifiers in general. 
-  Identifiers associated with certain semantic categories,
-  such as \emph{ast} nodes, or \emph{type}s are 
-  prefixed by the category and suffixed by \emph{id}.
-  For example, we have:
-
-  \nicebox{
-   ast-id        - identifier for ast nodes 
-
-   type-id       - identifier for type nodes 
-
-   parameter-id  - identifier for ast 
-
-   name-id       - identifier for a function/type name 
-
-   decl-id       - identifier for declaration node 
-
-   context-id    - identifier for Boolean context
-  }   
-
-  Identifiers can be any sequence of non-whitespace 
-  and non-newline characters whose first character
-  is not one of the decimal digits.
-  Identifiers enclosed in quotes ''...''
-  are treated specially: the quotes are stripped.
-  Thus, the identifier consisting of zero characters
-  is written ''''. The identifier ''null'' 
-  is allowed for <em>skolem-id</em> and <em>quant-id</em>.
-  
-  \section nativecontrol Control commands
-
-  To load a theory solver for integer linear arithmetic, 
-  include a line of the form \ty{Solver LIA}. To load the
-  mixed integer/real solver include instead a line of the
-  form \ty{Solver LRA}
-
-  Use \ty{Push} and \ty{Pop} to push/pop contexts 
-  (constraints that are asserted 
-  under a \ty{Push} are removed after a \ty{Pop}).
-  To reset the state entirely, use \ty{Reset}.
-
-  To assert a constraint use \ty{Assert} \emph{ast-id},
-  where the \emph{ast-id} is an identifier declared
-  for a boolean typed term.
-
-  To check for satisfiability of all asserted constraints
-  use \ty{Check}.
-
-  \nicebox{
-  <i>control</i> :=
-     | Solver <i>solver</i>        - load specified theory solver 
-     | Assert <i>ast-id</i>        - assert constraint 
-     | Check                - check for satisfiability of asserts
-     | Push                 - push a context
-     | Pop                  - pop a context
-     | Version <i>major minor build-number revision</i> - specify Z3 version
-
-  <i>solver</i> :=
-     | LRA                  - mixed integer/real arithmetic 
-     | LIA                  - integer arithmetic}
-
-  \section z3nativeast Abstract syntax trees
-
-  Every node in the abstract syntax trees understood by Z3
-  is declared by using a syntax category identifier, followed
-  by a (unique) identifier that names the node. The
-  node identifier is followed by a description of the node.
-
-  In overview abstract syntax tree nodes are declared using the commands:
-
-  \nicebox{
-  <i>ast</i> :=
-     | Type <i>id</i> <i>type</i> 
-     | Dec <i>id</i> <i>declaration</i>
-     | Const <i>id</i> <i>constant</i>             
-     | Fun <i>id</i> <i>function</i>               
-     | App <i>id</i> <i>built-in</i>               
-     | Num <i>id</i> <i>numeral</i>                
-     | Qua <i>id</i> <i>quantifier</i>                     
-     | Var <i>id</i> <i>bound-variable</i>             
-     | Ctx <i>id</i> <i>local-context</i>          
-     | Lab <i>id</i> <i>label-term</i>         
-     | Pat <i>id</i> <i>pattern</i> 
- }
-
- \subsection z3nativetypes Types
-
- Types are created from a name and optional parameters.
- A number of names are reserved for built-in theories.
- These names are:
- \nicebox{
-    Int  Real  Bool  bv  array
- }
- When the name of a type is one of these, the type is automatically
- associated with the respective theory. 
- The \ty{bv} type takes one numeric parameter (the bit-width of the
- bit-vector), and \ty{array} takes <i>n+1</i> parameters (the <i>n</i> 
- types for the domain of the array and the last parameter for the
- range of the array.
-
- \nicebox{
- <i>type</i> := <i>name</i> '[' <i>parameter</i>* ']' 
-
- <i>parameter</i> := <i>number</i> | <i>ast-id</i> | <i>symbol</i>
- }
- A parameter can either be an integer, an identifier used for 
- another defined term or type, or a symbol. Symbols are given as
- strings. The parser first attempts to identify a parameter as
- a previously defined term or type, and if there is no 
- such previously defined term/type, then it treats the string
- as a symbol.
-
- \subsection nativez3Fuctions Function and constant declarations
- In Z3, functions are constants that take more than zero arguments,
- thus, everything is treated as a constant.
-
- Constant declarations comprise of a name, followed by
- a non-empty list of types, all but the first types
- are the domain of the function (there are no domain
- types for 0-ary constants), the last type is the range.
- A constant declaration is followed by optional 
- theory specific information.
-
- The codes used in the theory specific information is described under \ref theories 
-
- The theory specific information indicates
- whether the constant is associative/commutative/injective; 
- a list of parameters may also be used to indicate 
- auxiliary information for the constant declarations.
-
- \nicebox{
- <i>declaration</i> := <i>name-id</i> <i>type-id</i>* [<i>const-info</i>]
-
- <i>const-info</i> := BUILTIN <i>theory</i> <i>kind-num</i> (:assoc | :comm | :inj | <i>parameter</i>)*
-
- <i>theory</i> := 
-    | basic -  built-in types and operations 
-    | arith -  arithmetical 
-    | bv    -  bit-vectors 
-    | array -  arrays 
-    | datatype - datatypes
- }
-
-
- \subsection z3nativeterms Terms
-
-
- Terms are built from constants, function applications,
- labeling, context formation, quantification
- and bound variables.
-
- A constant consists of a declarations, functions consist of
- a declaration followed by a non-empty list of term identifiers.
- All constants and function applications can be constructed using
- the \ty{Fun} construct. However, two shortcuts are available.
-
- <ul>
- <li> \ty{Const}:
- Constants may be defined directly by supplying the name and the type of the constant.
- </li>
- <li> \ty{App}:
- Built-in arithmetic, array, bit-vector, and Boolean operations may be applied directly
- to their arguments without first providing function declarations.
- </li>
- </ul>
-
-  \nicebox{
-  <i>constant</i>  := <i>name-id</i> <i>type-id</i>
-
-  <i>function</i>  := <i>decl-id</i> <i>ast-id</i>* 
-
-  <i>built-in</i>  := <i>name-id</i> [<i> [</i> <i>parameter</i>* ]</i> </i>] <i>ast-id</i>*
-  }
-
- Labeled terms consist of a polarity (\ty{LBLPOS} for positive 
- context, \ty{LBLNEG} for negative contexts), a name, and a 
- term identifier.
-
- 
-  \nicebox{
-  <i>label-term</i>  :=  (LBLPOS | LBLNEG) <i>label-name</i> <i>ast-id</i> 
-  }
-
- Local contexts consist of an identifier for the underlying
- term, followed by a predicate summarizing the context in
- which the term is interpreted. 
-
-  \nicebox{
-  <i>local-context</i> :=  <i>ast-id</i> <i>context-id</i>
-  }
-
- A quantifier consists of 
-<ul>
-<li> 
-A number indiciating the
-weight of the quantifier (for matching precedence),
-<li> 
-A skolem identifier, used for Boogie quantifier instantiation,
-<li>
-A quantifier identifier, used for profiling instantiations, 
-<li>
-A number indicating how many variables are bound by the quantifier, followed
-by the bound variables, which are
-<ul>
-<li> A name for the bound variable.
-<li> An identifier for the type of the bound variable.
-</ul>
-<li>
-A number indicating how many patterns are associated with the quantifier,
-followed by the patterns, which are
-<ul>
-<li> An identifier for the pattern.
-</ul>
-<li> An identifier for the body of the quantifier.
-</ul>
-
-  \nicebox{
-  <i>quantifier</i>  :=  
-      (FORALL | EXISTS) 
-      <i>weight-num</i>  
-      <i>skolem-id</i>
-      <i>quant-id</i> 
-      <i>decls-num</i>
-      (<i>name-id</i> <i>type-id</i>)*
-      <i>pattern-num</i>
-      <i>pattern-id</i>*
-      <i>ast-id</i>
-  }
-
-A bound variable consists of a de-Brujin index for the bound
-variable together with the type of the bound variable.
-While the type can be computed by matching the index of
-the de-Brujin index with the associated quantifier, 
-
-Patterns comprise of a list of terms.
-
-
-  \nicebox{
-  <i>bound-variable</i>  :=  <i>index-num</i> <i>type-id</i>
-
-  <i>numeral</i>   :=  <i>rational</i> <i>type-id</i> 
-
-  <i>rational</i>  :=  <i>number</i> [/<i>number</i>] 
-
-  <i>number</i>    :=  [0-9]+
-
-  <i>pattern</i>   :=  <i>id</i> <i>ast-id</i>*
-  }
-
-
-\section z3nativeexamples Examples
-
-\subsection z3nativearithmetic Integer Arithmetic
-
-Suppose we wish to check whether 
-\nicebox{
-       z0 >= 0 && z1 >= 0 && z2 >= 1 && z1 >= z2 && z2 >= z0
-}
-is satisfiable for <pre>z0, z1, z2</pre> integers. 
-With the low-level input format, we may specify this by:
-
-\nicebox{
-   Type INT  Int
-   Type BOOL Bool
-   Const z0  z0 INT
-   Const z1  z1 INT
-   Const z2  z2 INT
-   Num   0   0 INT
-   Num   1   1 INT
-   App c0 >= z0 0
-   Assert c0
-   App c1 >= z1 0
-   Assert c1
-   App c2 >= z2 1
-   Assert c2
-   App c3 >= z1 z2
-   Assert c3
-   App c4 >= z2 z0
-   Assert c4
-   Check
-}
-
-
-Notice that the identifiers may be arbitrary strings, including numerals.
-So for instance, we used 1 to represent integer 1. 
-
-\subsection z3nativebv Bit-vectors
-
-We can check whether 32-bit addition is commutative. Z3 reports \ty{unsat}
-in for the first check. The second satisfiable check illustrates the use of parameters
-(\ty{extract} takes two integer parameters for the range of bits extracted
-from the bit-vectors). 
-
-\nicebox{
-   Type bool Bool 
-   Type bv32 bv [ 32 ]
-   Type bv64 bv [ 64 ]
-   Num 0 0 bv32
-   Num 1 1 bv32
-   Const x0 x0 bv32
-   Const x1 x1 bv32
-   Const x2 x2 bv64
-   App a bvadd x0 x1
-   App b bvadd x1 x0
-   App eq = a b
-   App constraint1 not eq
-   Push
-   Assert constraint1
-   Check
-   Pop
-   App c extract [ 31 0 ] x2
-   App eq2 = a c
-   App constraint2 not eq2
-   Push
-   Assert constraint2
-   Check
-   Pop
-}
-
-We added the declarations of bit-vector constants 0 and 1. Like integers, 
-these are also numerals, but with bit-vector type.
-
-
-\subsection z3nativeexarray Arrays
-
-The low-level version of:
-\nicebox{
-   store(f1,i1,v1) = store(f2,i2,v2) && i1 != i3 && i2 != i3 && select(f1,i3) != select(f2,i3)
-}
-is:
-
-\nicebox{
-  Type Index Index
-  Type Elem Elem
-  Type Array array [ Index Elem ]
-  Type bool Bool
-  Const i1 i1 Index
-  Const i2 i2 Index
-  Const i3 i3 Index
-  Const v1 v1 Elem
-  Const v2 v2 Elem
-  Const f1 f1 Array
-  Const f2 f2 Array
-  App n1 store f1 i1 v1
-  App n2 store f2 i2 v2
-  App n3 = n1 n2
-  App n4 = i1 i3
-  App n5 not n4
-  App n6 = i2 i3
-  App n7 not n6 
-  App n8 select f1 i3
-  App n9 select f2 i3
-  App n10 = n8 n9
-  App n11 not n10
-  Assert n3
-  Assert n5
-  Assert n7
-  Assert n11
-  Check
-}
-
-\subsection z3nativeexdatatype Data-types
-
-To check projection over tuples
-\nicebox{
-  (= x (first (mk_tuple x y)))
-}
-
-we write:
-\nicebox{
-  Type int Int
-  Type pair tuple [ mk_tuple first int second int ]
-  Const x x int
-  Const y y int
-  Const p p pair
-  App n1 mk_tuple x y
-  App n2 first n1
-  App n3 = n2 x
-  App n4 not n3
-  Assert n4
-  Check
-}
-
-
-*/
-
- /**
-
-  \defgroup theories Z3 theories
-
-
-  \section theorisbasics Basics
-
-There is a single basic sort, \ty{bool}, which has op-code 0.
-The basic operators are, listed with their codes in the table below.
-
-<table border cellspacing=5 cellpadding=10>
-<tr>
- <th>Op-code</th>
- <th>Mnmonics</th>
- <th>Description</th>
-</tr>
-<tr><td>0</td><td> \ty{true} </td><td> the constant \emph{true} </td></tr>
-<tr><td>1</td><td> \ty{false} </td><td> the constant \emph{false} </td></tr>
-<tr><td>2</td><td> \ty{=} </td><td> equality</td></tr>
-<tr><td>3</td><td> \ty{distinct} </td><td> distincinctness </td></tr>
-<tr><td>4</td><td> \ty{ite} </td><td> if-then-else </td></tr>
-<tr><td>5</td><td> \ty{and} </td><td> n-ary conjunction </td></tr>
-<tr><td>6</td><td> \ty{or} </td><td> n-ary disjunction </td></tr>
-<tr><td>7</td><td> \ty{iff} </td><td> bi-impliciation </td></tr>
-<tr><td>8</td><td> \ty{xor} </td><td> exclusive or </td></tr>
-<tr><td>9</td><td> \ty{not} </td><td> negation </td></tr>
-<tr><td>10</td><td> \ty{implies} </td><td> implication </td></tr>
-</table> 
-
-  \section theoriesarithmetic Arithmetic
-
-  \subsection tharithbuiltin Built-in operators
-
-  Arithmetical expression can be built from reals or integers.
-  The arithmetical sorts are listed below
-  and the supported operations are listed in the table thereafter.
-
-<table border cellspacing=5 cellpadding=10>
-<tr>
- <th>Op-code</th>
- <th>Mnmonics</th>
- <th>Description</th>
-</tr>
-<tr><td>0</td> <td>\ty{real}</td> <td> sort of reals</td></tr>
-<tr><td>1</td> <td>\ty{int}</td> <td> sort of integers</td></tr>
-</table>
-
-<table border cellspacing=5 cellpadding=10>
-<tr>
- <th>Op-code</th>
- <th>Mnmonics</th>
- <th>Description</th>
-</tr>
-<tr><td>0</td> <td> \ty{<=} </td><td> less-than or equal </td></tr>
-<tr><td>1</td> <td> \ty{>=} </td><td> greater-than or equal </td></tr>
-<tr><td>2</td> <td> \ty{<} </td><td> less-than </td></tr>
-<tr><td>3</td> <td> \ty{>} </td><td>  greater-than </td></tr>
-<tr><td>4</td> <td> \ty{+} </td><td>  n-ary addition </td></tr>
-<tr><td>5</td> <td> \ty{-} </td><td>  binary minus </td></tr>
-<tr><td>6</td> <td> \ty{~} </td><td> unary minus </td></tr>
-<tr><td>7</td> <td> \ty{*} </td><td>  n-ary multiplication </td></tr>
-<tr><td>8</td> <td> \ty{/} </td><td>  rational division </td></tr>
-<tr><td>9</td> <td> \ty{div} </td><td>  integer division </td></tr>
-<tr><td>10</td> <td> \ty{rem} </td><td>  integer remainder </td></tr>
-<tr><td>11</td> <td> \ty{mod} </td><td>  integer modulus </td></tr>
-</table>
-
-  \section theoriesbv Bit-vectors
-To indicate the bit-vector length one adds a numeral parameter
-with the number of bits the bit-vector holds.
-For instance, a declaration of the form:
-
-\nicebox{
-  Type $1 bv [ 32 ] 
-}
-
-declares a 32-bit bit-vector type.
-
-  
-<table border cellspacing=5 cellpadding=10>
-<tr>
- <th>Op-code</th>
- <th>Mnmonics</th>
- <th>Parameters</th>
- <th>Description</th>
-</tr>
-<tr><td>0</td> <td> \ty{bit1} </td> <td></td> <td>constant comprising of a single bit set to 1</td></tr>
-<tr><td>1 </td><td> \ty{bit0} </td><td> </td><td>  constant comprising of a single bit set to 0. </td></tr>
-<tr><td>2 </td><td> \ty{bvneg} </td><td> </td><td> Unary subtraction. </td></tr>
-<tr><td>3 </td><td> \ty{bvadd} </td><td> </td><td>  addition. </td></tr>
-<tr><td>4 </td><td> \ty{bvsub} </td><td> </td><td>  subtraction. </td></tr>
-<tr><td>5 </td><td> \ty{bvmul} </td><td> </td><td>  multiplication. </td></tr>
-<tr><td>6 </td><td> \ty{bvsdiv} </td><td> </td><td>  signed division. </td></tr>
-<tr><td>7 </td><td> \ty{bvudiv} </td><td> </td><td>  unsigned division. 
-The operands are treated as unsigned numbers. </td></tr> 
-<tr><td>8 </td><td> \ty{bvsrem} </td><td> </td><td>   signed remainder. </td></tr>
-<tr><td>9 </td><td> \ty{bvurem} </td><td> </td><td>   unsigned remainder. </td></tr>
-<tr><td>10 </td><td> \ty{bvsmod} </td><td> </td><td>   signed modulus. </td></tr>
-<tr><td>11 </td><td> \ty{bvule} </td><td> </td><td>   unsigned \ty{<=}. </td></tr>
-<tr><td>12 </td><td> \ty{bvsle} </td><td> </td><td>   signed \ty{<=}. </td></tr>
-<tr><td>13</td><td> \ty{bvuge} </td><td> </td><td>   unsigned \ty{>=}. </td></tr>
-<tr><td>14 </td><td> \ty{bvsge} </td><td> </td><td>  signed \ty{>=}. </td></tr>
-<tr><td>15 </td><td> \ty{bvult} </td><td> </td><td>  unsigned \ty{<}. </td></tr>
-<tr><td>16 </td><td> \ty{bvslt} </td><td> </td><td>  signed \ty{<}. </td></tr>
-<tr><td>17 </td><td> \ty{bvugt} </td><td> </td><td>  unsigned \ty{>}. </td></tr>
-<tr><td>18 </td><td> \ty{bvsgt} </td><td> </td><td>  signed \ty{>}. </td></tr>
-<tr><td>19 </td><td> \ty{bvand} </td><td> </td><td>  n-ary (associative/commutative) bit-wise and. </td></tr> 
-<tr><td>20 </td><td> \ty{bvor} </td><td> </td><td>  n-ary (associative/commutative) bit-wise or. </td></tr>
-<tr><td>21 </td><td> \ty{bvnot} </td><td> </td><td>  bit-wise not. </td></tr>
-<tr><td>22 </td><td> \ty{bvxor} </td><td> </td><td>  n-ary bit-wise xor. </td></tr>
-<tr><td>23 </td><td> \ty{bvnand} </td><td> </td><td>  bit-wise nand. </td></tr>
-<tr><td>24 </td><td> \ty{bvnor} </td><td> </td><td>  bit-wise nor. </td></tr>
-<tr><td>25 </td><td> \ty{bvxnor} </td><td> </td><td>  bit-wise exclusive nor. </td></tr>
-<tr><td>26 </td><td> \ty{concat} </td><td> </td><td>  bit-vector concatentaion. </td></tr>
-<tr><td>27 </td><td> \ty{sign\_extend} </td><td> \emph{n}</td><td>  \emph{n}-bit sign extension. </td></tr>
-<tr><td>28</td><td> \ty{zero\_extend} </td><td> \emph{n}</td><td>  \emph{n}-bit  zero extension. </td></tr>
-<tr><td>29 </td><td> \ty{extract} </td><td> \emph{hi:low} </td><td>  \emph{hi}-\emph{low} bit-extraction. </td></tr>
-<tr><td>30 </td><td> \ty{repeat} </td><td> \emph{n} </td><td>  repeat $n$ times. </td></tr>
-<tr><td>31 </td><td> \ty{bvredor} </td><td> </td><td>  or-reduction. </td></tr>
-<tr><td>32 </td><td> \ty{bvredand} </td><td> </td><td>  and-reducdtion. </td></tr>
-<tr><td>33 </td><td> \ty{bvcomp} </td><td> </td><td>  bit-vector comparison. </td></tr>
-<tr><td>34 </td><td> \ty{bvshl} </td><td> </td><td>  shift-left. </td></tr>
-<tr><td>35 </td><td> \ty{bvlshr} </td><td> </td><td>  logical shift-right. </td></tr>
-<tr><td>36 </td><td> \ty{bvrshr} </td><td> </td><td>  arithmetical shift-right. </td></tr>
-<tr><td>37 </td><td> \ty{bvrotate\_left} </td><td> \emph{n} </td><td>  \emph{n}-bit left rotation. </td></tr>
-<tr><td>38 </td><td> \ty{bvrotate\_right} </td><td>\emph{n} </td><td>  \emph{n}-bit right rotation.  </td></tr>
-</table>
-
-\section theoriesarrays Arrays
-
-\subsection tharraybuiltinops Built-in operators
-
-  There is a single built-in sort constructor for arrays with code 0.
-  It is followed by a sequence of parameters indicating the domain
-  sorts and the range of the array.
-
-<table border cellspacing=5 cellpadding=10>
-<tr>
- <th>Op-code</th>
- <th>Mnmonics</th>
- <th>Description</th>
-</tr>
-<tr><td>0</td><td> \ty{store} </td><td>  array store </td></tr>
-<tr><td>1</td><td> \ty{select} </td><td>  array select </td></tr>
-<!---
-<tr><td></td><td> \ty{const} </td><td> array returning constant value </td></tr>
-%\begin{internal}
-<tr><td></td><td> \ty{store\_ite} </td><td> ternary non-pointwise store</td></tr>
-<tr><td></td><td> \ty{set\_union} </td><td> set union A u B </td></tr>
-<tr><td></td><td> \ty{set\_intersect} </td><td> set intersection A n B </td></tr>
-<tr><td></td><td> \ty{set\_difference} </td><td> set difference A \ B </td></tr>
-<tr><td></td><td> \ty{set\_complement} </td><td> set complement C(A) </td></tr>
-<tr><td></td><td> \ty{is\_subset} </td><td> non-strict subset: A <= B </td></tr>
---->
-</table>
-
-  In the low-level input format, array types
-  are accompanied by a sequence of identifiers corresponding
-  to the domain and range of the array the operations operate
-  upon.
-  In more detail, the contract is that the supplied parameters
-  to the type declaration of an array are of the form:
-
-  <ul>
-  <li> parameter_0 - 1'st dimension 
-  <li> parameter_{n-1} - n'th dimension
-  <li> parameter_n - range
-  </ul>
-
- The constant array function symbol \ty{const} needs a parameter
- in order to infer the types of the indices of the constant array.
- We pass the array type as the parameter to \ty{const}. 
- The other array operations do not need parameters.
-
- We summarize the arities and semantics of the operators:
-
- <ul>
- <li> \ty{store} - 
-      
-Updates an array at a given index with a value:
- \ty{store}(A, i0, ... i_{n-1}, v) has the same contents as A, except on
-index i0, ... , i_{n-1}, where the value is v.
-
- <li> \ty{select} - 
-  
-  Selects the value from an array: 
-  \ty{select}(A, i0, ... , i_{n-}) selects the value stored at
-  index i0, ... , i_{n-1}.
- </ul>
-
-<!---
- 
-\\
-{\tt const} \\
-\> 
-\begin{minipage}[t]{5in}
-Creates a constant array: ${\tt const}(v)$ maps every index in the domain of the array to $v$.
-\end{minipage}
-\internalonly{
-\\
-{\tt store\_ite} \\
-\> 
-\begin{minipage}[t]{5in}
-Creates an array using a test and two other arrays: 
-\[
-\begin{array}{lll}
-        {\tt select}(A,\overline{i}) = {\tt select}(B, \overline{i}) & \rightarrow & 
-        {\tt select}({\tt store\_ite}(A,B,C), \overline{i}) = {\tt select}(C,\overline{i}) \ \
-        {\tt select}(A,\overline{i}) \neq {\tt select}(B, \overline{i}) & \rightarrow & 
-        {\tt select}({\tt store\_ite}(A,B,C), \overline{i}) = {\tt select}(B,\overline{i})
-\end{array}		
-\]
-\end{minipage}
-\\
-{\tt set\_union}, {\tt set\_intersect} \\
-\>
-\begin{minipage}[t]{5in}
-Creates the union, intersection of the list of arguments. Each argument must be declared as an array of the same type, 
-and the range type must be {\tt bool}.
-\end{minipage}
-\\
-{\tt set\_difference} \\
-\>
-\begin{minipage}[t]{5in}
-Creates the set difference of two arrays. The arguments must be declared as arrays of the same type with range type {\tt bool}
-\end{minipage}
-\\
-{\tt set\_complement}\\
-\>
-\begin{minipage}[t]{5in}
-Set complement of one Boolean valued array.
-\end{minipage}
-\\
-{\tt is\_subset} \\
-\>
-\begin{minipage}[t]{5in}
-Subset test of two Boolean valued arrays of the same type.
-\end{minipage}
-} % internalonly
-\end{tabbing}
---->
-
-
- */
-#ifndef _Z3_SOLVER_H_
-#define _Z3_SOLVER_H_
-
-#include "ast.h"
-#include "symbol_table.h"
-#include "stream_buffer.h"
-#include "warning.h"
-#include "front_end_params.h"
-#include "arith_decl_plugin.h"
-#include "bv_decl_plugin.h"
-#include "z3.h"
-
-
-class z3_solver {
-    
-    enum kind {
-        T_NUM,
-        T_VAR,
-        T_DEC,
-        T_FUNCTION_CONST,
-        T_GET_IMPLIED_EQUALITIES,
-        T_NULLARY_CONST,
-        T_BUILTIN_CONST,
-        T_TY,
-        T_TYPE,
-        T_QUA,
-        T_LAB,
-        T_CTX,
-        T_PAT,
-
-        T_SOLVER,
-        T_SIMPLIFY,
-
-        T_ASSERT,
-        T_CHECK,
-        T_CHECK_ASSUMPTIONS,
-        T_DBG_SAT,
-        T_DBG_UNSAT,
-        T_PUSH,
-        T_POP,
-        T_RESET,
-        T_ECHO,
-        T_VERSION,
-       
-        T_COMMENT,
-
-        T_EOF,
-        T_ERR
-    };
-
-    struct builtin_info {
-        family_id m_fid;
-        decl_kind m_kind;
-        builtin_info(family_id fid, decl_kind k) : m_fid(fid), m_kind(k) {}
-        builtin_info(): m_fid(null_family_id), m_kind(null_decl_kind) {}
-    };
-
-    Z3_context         m_context;
-    bool               m_owns_context;
-    ast_manager&       m_manager;
-    front_end_params&  m_params;
-    symbol_table<ast*> m_table;
-    stream_buffer      m_in;
-    std::ostream&      m_out;
-    bool               m_is_active;
-    expr_ref_vector    m_assumptions;
-    unsigned_vector    m_assumptions_lim;
-    unsigned           m_num_checks;
-    std::string        m_string;
-    bool               m_eof;
-    unsigned           m_line;
-    symbol_table<builtin_info> m_builtin_ops;
-    symbol_table<builtin_info> m_builtin_types;
-    arith_util         m_arith;
-    bv_util            m_bv;
-    ast_ref_vector     m_pinned;
-    unsigned_vector    m_pinned_lim;
-    Z3_lbool           m_last_check_result;
-    
-public:        
-
-    z3_solver(
-        Z3_context    c,
-        std::istream& is,
-        std::ostream& os,
-        front_end_params & params,
-        bool is_active = true
-        );
-
-    z3_solver(
-        ast_manager&  m,
-        std::istream& is,
-        std::ostream& os,
-        front_end_params & params
-        );
-
-    ~z3_solver();
-
-    bool parse();
-
-    void get_assumptions(expr_ref_vector& v) { v.append(m_assumptions); }
-
-    void display_statistics(std::ostream& out, bool istats);
-
-    void set_error_handler(Z3_error_handler h) {
-        Z3_set_error_handler(m_context, h);
-    }
-