mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-12-27 10:10:26 -08:00
commit 4c949cdbac
3 changed files with 33 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

59
src/smt/smt_context.cpp
View file

@ -3202,10 +3202,8 @@ namespace smt {
});
validate_unsat_core();
// theory validation of unsat core
ptr_vector<theory>::iterator th_it = m_theory_set.begin();
ptr_vector<theory>::iterator th_end = m_theory_set.end();
for (; th_it != th_end; ++th_it) {
lbool theory_result = (*th_it)->validate_unsat_core(m_unsat_core);
for (theory* th : m_theory_set) {
lbool theory_result = th->validate_unsat_core(m_unsat_core);
if (theory_result == l_undef) {
return l_undef;
}
@ -3296,10 +3294,8 @@ namespace smt {
#ifndef _EXTERNAL_RELEASE
if (m_fparams.m_display_installed_theories) {
std::cout << "(theories";
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
std::cout << " " << (*it)->get_name();
for (theory* th : m_theory_set) {
std::cout << " " << th->get_name();
}
std::cout << ")" << std::endl;
}
@ -3316,17 +3312,13 @@ namespace smt {
m_fparams.m_relevancy_lemma = false;
// setup all the theories
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it)
(*it)->setup();
for (theory* th : m_theory_set)
th->setup();
}
void context::add_theory_assumptions(expr_ref_vector & theory_assumptions) {
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->add_theory_assumptions(theory_assumptions);
for (theory* th : m_theory_set) {
th->add_theory_assumptions(theory_assumptions);
}
}
@ -3342,18 +3334,7 @@ namespace smt {
if (!check_preamble(reset_cancel))
return l_undef;
expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
if (!already_did_theory_assumptions) {
add_theory_assumptions(all_assumptions);
}
unsigned num_assumptions = all_assumptions.size();
expr * const * assumptions = all_assumptions.c_ptr();
if (!validate_assumptions(num_assumptions, assumptions))
return l_undef;
TRACE("check_bug", tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n";);
TRACE("unsat_core_bug", for (unsigned i = 0; i < num_assumptions; i++) { tout << mk_pp(assumptions[i], m_manager) << "\n";});
pop_to_base_lvl();
TRACE("before_search", display(tout););
SASSERT(at_base_level());
@ -3363,6 +3344,18 @@ namespace smt {
}
else {
setup_context(false);
expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
if (!already_did_theory_assumptions) {
add_theory_assumptions(all_assumptions);
}
unsigned num_assumptions = all_assumptions.size();
expr * const * assumptions = all_assumptions.c_ptr();
if (!validate_assumptions(num_assumptions, assumptions))
return l_undef;
TRACE("unsat_core_bug", tout << all_assumptions << "\n";);
internalize_assertions();
TRACE("after_internalize_assertions", display(tout););
if (m_asserted_formulas.inconsistent()) {
@ -3551,10 +3544,9 @@ namespace smt {
pop_scope(m_scope_lvl - curr_lvl);
SASSERT(at_search_level());
}
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end && !inconsistent(); ++it)
(*it)->restart_eh();
for (theory* th : m_theory_set) {
if (!inconsistent()) th->restart_eh();
}
TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";);
if (!inconsistent()) {
m_qmanager->restart_eh();
@ -4070,10 +4062,7 @@ namespace smt {
bool include = false;
if (at_lbls) {
// include if there is a label with the '@' sign.
buffer<symbol>::const_iterator it = lbls.begin();
buffer<symbol>::const_iterator end = lbls.end();
for (; it != end; ++it) {
symbol const & s = *it;
for (symbol const& s : lbls) {
if (s.contains('@')) {
include = true;
break;

1
src/tactic/smtlogics/qflia_tactic.cpp
View file

@ -24,7 +24,6 @@ Notes:
#include "tactic/core/solve_eqs_tactic.h"
#include "tactic/core/elim_uncnstr_tactic.h"
#include "smt/tactic/smt_tactic.h"
// include"mip_tactic.h"
#include "tactic/arith/add_bounds_tactic.h"
#include "tactic/arith/pb2bv_tactic.h"
#include "tactic/arith/lia2pb_tactic.h"

14
src/tactic/smtlogics/qfnia_tactic.cpp
View file

@ -102,13 +102,17 @@ static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) {
mk_fail_if_undecided_tactic());
}
tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) {
params_ref simp_p = p;
simp_p.set_bool("som", true); // expand into sums of monomials
return and_then(using_params(mk_simplify_tactic(m), simp_p), mk_smt_tactic());
}
tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
return and_then(mk_qfnia_premable(m, p),
or_else(mk_qfnia_nlsat_solver(m, p),
mk_qfnia_sat_solver(m, p),
and_then(using_params(mk_simplify_tactic(m), simp_p),
mk_smt_tactic())));
or_else(mk_qfnia_sat_solver(m, p),
try_for(mk_qfnia_smt_solver(m, p), 2000),
mk_qfnia_nlsat_solver(m, p),
mk_qfnia_smt_solver(m, p)));
}