z3 / src / solver / solver_na2as.cpp

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    solver_na2as.cpp

Abstract:

    Solver that implements "named" assertions using assumptions (aka answer literals).
    That is, a named assertion assert_expr(t, a) is mapped into
          a implies t
    and 'a' is used as an extra assumption for check_sat.

Author:

    Leonardo (leonardo) 2012-11-02

Notes:

--*/
#include"solver_na2as.h"
#include"ast_smt2_pp.h"

solver_na2as::solver_na2as() {
    m_manager = 0;
}

solver_na2as::~solver_na2as() {
    restore_assumptions(0);
}

void solver_na2as::assert_expr(expr * t, expr * a) {
    SASSERT(m_manager != 0);
    SASSERT(is_uninterp_const(a));
    SASSERT(m_manager->is_bool(a));
    TRACE("solver_na2as", tout << "asserting\n" << mk_ismt2_pp(t, *m_manager) << "\n" << mk_ismt2_pp(a, *m_manager) << "\n";);
    m_manager->inc_ref(a);
    m_assumptions.push_back(a);
    expr_ref new_t(*m_manager);
    new_t = m_manager->mk_implies(a, t);
    assert_expr(new_t);
}
    
void solver_na2as::init(ast_manager & m, symbol const & logic) {
    SASSERT(m_assumptions.empty());
    m_manager = &m;
    init_core(m, logic);
}

struct append_assumptions {
    ptr_vector<expr> & m_assumptions;
    unsigned           m_old_sz;
    append_assumptions(ptr_vector<expr> & _m_assumptions, 
                       unsigned num_assumptions, 
                       expr * const * assumptions):
        m_assumptions(_m_assumptions) {
        m_old_sz = m_assumptions.size();
        m_assumptions.append(num_assumptions, assumptions);
    }

    ~append_assumptions() {
        m_assumptions.shrink(m_old_sz);
    }
};

lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) {
    append_assumptions app(m_assumptions, num_assumptions, assumptions);
    return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr());
}

void solver_na2as::push() {
    m_scopes.push_back(m_assumptions.size());
    push_core();
}

void solver_na2as::pop(unsigned n) {
    pop_core(n);
    unsigned lvl = m_scopes.size();
    SASSERT(n <= lvl);
    unsigned new_lvl = lvl - n;
    restore_assumptions(m_scopes[new_lvl]);
    m_scopes.shrink(new_lvl);
}

void solver_na2as::restore_assumptions(unsigned old_sz) {
    SASSERT(old_sz == 0 || m_manager != 0);
    for (unsigned i = old_sz; i < m_assumptions.size(); i++) {
        m_manager->dec_ref(m_assumptions[i]);
    }
    m_assumptions.shrink(old_sz);
}

unsigned solver_na2as::get_scope_level() const {
    return m_scopes.size();
}

void solver_na2as::reset() {
    reset_core();
    restore_assumptions(0);
}
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.