mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

fix logic for adding cores

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-08-11 09:43:17 -07:00
parent 0f83e7a251
commit 6a820adfed
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/muz_qe/pdr_generalizers.cpp
View file

@ -182,12 +182,14 @@ namespace pdr {
void core_convex_hull_generalizer::method1(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) { void core_convex_hull_generalizer::method1(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) {
manager& pm = n.pt().get_pdr_manager(); manager& pm = n.pt().get_pdr_manager();
expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), eqs(m); expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), eqs(m);
unsigned orig_size = new_cores.size();
if (core.empty()) { if (core.empty()) {
new_cores.push_back(std::make_pair(core, uses_level));
return; return;
} }
new_cores.push_back(std::make_pair(core, uses_level));
add_variables(n, eqs); add_variables(n, eqs);
if (!mk_convex(core, 0, conv1)) { if (!mk_convex(core, 0, conv1)) {
new_cores.push_back(std::make_pair(core, uses_level));
IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core), m) << "\n";); IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core), m) << "\n";);
return; return;
} }
@ -233,6 +235,10 @@ namespace pdr {
verbose_stream() << "Generalized to:\n" << mk_pp(state1, m) << "\n";); verbose_stream() << "Generalized to:\n" << mk_pp(state1, m) << "\n";);
} }
} }
if (!m_is_closure || new_cores.empty()) {
new_cores.push_back(std::make_pair(core, uses_level));
}
} }
// take as starting point two points from different regions. // take as starting point two points from different regions.