mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 11:37:54 +00:00
Code Activity

fix reset regression with mk_convex:

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-08-28 12:18:02 -07:00
parent 137339a2e1
commit 4597872be8
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/muz/pdr_generalizers.cpp
View file

@ -157,7 +157,7 @@ namespace pdr {
} }
void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) { void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) {
method3(n, core, uses_level, new_cores); // method3(n, core, uses_level, new_cores);
method1(n, core, uses_level, new_cores); method1(n, core, uses_level, new_cores);
} }
@ -180,18 +180,19 @@ 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); expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), fmls(m);
unsigned orig_size = new_cores.size(); unsigned orig_size = new_cores.size();
if (core.empty()) { if (core.empty()) {
new_cores.push_back(std::make_pair(core, uses_level)); new_cores.push_back(std::make_pair(core, uses_level));
return; return;
} }
add_variables(n, 2, conv1); add_variables(n, 2, fmls);
if (!mk_convex(core, 0, conv1)) { if (!mk_convex(core, 0, conv1)) {
new_cores.push_back(std::make_pair(core, uses_level)); 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;
} }
conv1.append(fmls);
expr_ref fml = n.pt().get_formulas(n.level(), false); expr_ref fml = n.pt().get_formulas(n.level(), false);
expr_ref_vector fmls(m); expr_ref_vector fmls(m);
qe::flatten_and(fml, fmls); qe::flatten_and(fml, fmls);