mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix bug with model completion and remove spurious std::cout

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-06-24 09:02:12 -07:00
parent 67ea78a4a5
commit 017165c474
4 changed files with 5 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/array_decl_plugin.cpp
View file

@ -522,7 +522,7 @@ void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol
void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {
op_names.push_back(builtin_name("store",OP_STORE));
op_names.push_back(builtin_name("select",OP_SELECT));
if (true || logic == symbol::null) {
if (logic == symbol::null || logic == symbol("HORN")) {
// none of the SMT2 logics support these extensions
op_names.push_back(builtin_name("const",OP_CONST_ARRAY));
op_names.push_back(builtin_name("map",OP_ARRAY_MAP));

3
src/qe/qe_mbp.cpp
View file

@ -454,8 +454,7 @@ public:
(*p)(model, vars, fmls);
}
}
while (!vars.empty() && !fmls.empty()) {
std::cout << "mbp: " << var << "\n";
while (!vars.empty() && !fmls.empty()) {
var = vars.back();
vars.pop_back();
project_plugin* p = get_plugin(var);

4
src/qe/qsat.cpp
View file

@ -158,6 +158,8 @@ namespace qe {
return;
}
model_evaluator eval(*mdl);
eval.set_model_completion(true);
TRACE("qe", model_v2_pp(tout, *mdl););
expr_ref val(m);
for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) {
@ -169,7 +171,7 @@ namespace qe {
if (m.is_false(val)) {
m_asms.push_back(m.mk_not(p));
}
else {
else {
SASSERT(m.is_true(val));
m_asms.push_back(p);
}

12
src/solver/mus.cpp
View file

@ -475,18 +475,6 @@ lbool mus::get_mus(expr_ref_vector& mus) {
return m_imp->get_mus(mus);
}
lbool mus::get_mus(ptr_vector<expr>& mus) {
return m_imp->get_mus(mus);
}
lbool mus::get_mus(expr_ref_vector& mus) {
ptr_vector<expr> result;
lbool r = m_imp->get_mus(result);
mus.append(result.size(), result.c_ptr());
return r;
}
void mus::reset() {
m_imp->reset();
}