mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'upstream-master' into develop

Browse source 
Conflicts:
	src/smt/smt_context.cpp
This commit is contained in:
Murphy Berzish 2017-04-24 12:28:16 -04:00
parent 06cd07e3c2 049cb957ea
commit 9e8a4e2a01
3 changed files with 16 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/c++/z3++.h
View file

@ -2244,7 +2244,7 @@ namespace z3 {
void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); } void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); } void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); } void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); to_check_result(r); } check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); return to_check_result(r); }
check_result query(func_decl_vector& relations) { check_result query(func_decl_vector& relations) {
array<Z3_func_decl> rs(relations); array<Z3_func_decl> rs(relations);
Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr()); Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());

27
src/smt/smt_context.cpp
View file

@ -3295,7 +3295,7 @@ namespace smt {
setup_context(m_fparams.m_auto_config); setup_context(m_fparams.m_auto_config);
expr_ref_vector theory_assumptions(m_manager); expr_ref_vector theory_assumptions(m_manager);
get_theory_assumptions(theory_assumptions); add_theory_assumptions(theory_assumptions);
if (!theory_assumptions.empty()) { if (!theory_assumptions.empty()) {
TRACE("search", tout << "Adding theory assumptions to context" << std::endl;); TRACE("search", tout << "Adding theory assumptions to context" << std::endl;);
return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true); return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true);
@ -3362,7 +3362,7 @@ namespace smt {
(*it)->setup(); (*it)->setup();
} }
void context::get_theory_assumptions(expr_ref_vector & theory_assumptions) { void context::add_theory_assumptions(expr_ref_vector & theory_assumptions) {
ptr_vector<theory>::iterator it = m_theory_set.begin(); ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end(); ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) { for (; it != end; ++it) {
@ -3382,16 +3382,9 @@ namespace smt {
if (!check_preamble(reset_cancel)) if (!check_preamble(reset_cancel))
return l_undef; return l_undef;
expr_ref_vector all_assumptions(m_manager); expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
for (unsigned i = 0; i < ext_num_assumptions; ++i) {
all_assumptions.push_back(ext_assumptions[i]);
}
if (!already_did_theory_assumptions) { if (!already_did_theory_assumptions) {
ptr_vector<theory>::iterator it = m_theory_set.begin(); add_theory_assumptions(all_assumptions);
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->add_theory_assumptions(all_assumptions);
}
} }
unsigned num_assumptions = all_assumptions.size(); unsigned num_assumptions = all_assumptions.size();
@ -3420,12 +3413,20 @@ namespace smt {
TRACE("after_internalization", display(tout);); TRACE("after_internalization", display(tout););
if (inconsistent()) { if (inconsistent()) {
VERIFY(!resolve_conflict()); // build the proof VERIFY(!resolve_conflict()); // build the proof
r = mk_unsat_core(); lbool result = mk_unsat_core();
if (result == l_undef) {
r = l_undef;
} else {
r = l_false;
}
} }
else { else {
r = search(); r = search();
if (r == l_false) { if (r == l_false) {
r = mk_unsat_core(); // validation may change an l_false to l_undef here lbool result = mk_unsat_core();
if (result == l_undef) {
r = l_undef;
}
} }
} }
} }

5
src/smt/smt_context.h
View file

@ -226,9 +226,6 @@ namespace smt {
literal2assumption m_literal2assumption; // maps an expression associated with a literal to the original assumption literal2assumption m_literal2assumption; // maps an expression associated with a literal to the original assumption
expr_ref_vector m_unsat_core; expr_ref_vector m_unsat_core;
// Unsat core assumption hint for theory_str
bool m_use_theory_str_overlap_assumption;
// ----------------------------------- // -----------------------------------
// //
// Theory case split // Theory case split
@ -1094,7 +1091,7 @@ namespace smt {
void reset_assumptions(); void reset_assumptions();
void get_theory_assumptions(expr_ref_vector & theory_assumptions); void add_theory_assumptions(expr_ref_vector & theory_assumptions);
lbool mk_unsat_core(); lbool mk_unsat_core();