mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

tidy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-04-22 11:36:03 -07:00
parent 4f455c7a3c
commit 5068d2083d
2 changed files with 5 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/smt/smt_context.cpp
View file

@ -3156,7 +3156,7 @@ namespace smt {
setup_context(m_fparams.m_auto_config);
expr_ref_vector theory_assumptions(m_manager);
get_theory_assumptions(theory_assumptions);
add_theory_assumptions(theory_assumptions);
if (!theory_assumptions.empty()) {
TRACE("search", tout << "Adding theory assumptions to context" << std::endl;);
return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true);
@ -3223,7 +3223,7 @@ namespace smt {
(*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 end = m_theory_set.end();
for (; it != end; ++it) {
@ -3243,16 +3243,9 @@ namespace smt {
if (!check_preamble(reset_cancel))
return l_undef;
expr_ref_vector all_assumptions(m_manager);
for (unsigned i = 0; i < ext_num_assumptions; ++i) {
all_assumptions.push_back(ext_assumptions[i]);
}
expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
if (!already_did_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(all_assumptions);
}
add_theory_assumptions(all_assumptions);
}
unsigned num_assumptions = all_assumptions.size();

2
src/smt/smt_context.h
View file

@ -1059,7 +1059,7 @@ namespace smt {
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();