mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

add scoped class for controlling Farkas generalization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-08-07 19:58:21 -07:00
parent 327b2bbe9c
commit 5b9ec3dec7
4 changed files with 15 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/pdr_context.cpp
View file

@ -1801,7 +1801,7 @@ namespace pdr {
m_expanded_lvl = n.level(); m_expanded_lvl = n.level();
} }
n.pt().set_use_farkas(m_params.use_farkas()); pred_transformer::scoped_farkas sf (n.pt(), m_params.use_farkas());
if (n.pt().is_reachable(n.state())) { if (n.pt().is_reachable(n.state())) {
TRACE("pdr", tout << "reachable\n";); TRACE("pdr", tout << "reachable\n";);
close_node(n); close_node(n);

11
src/muz_qe/pdr_context.h
View file

@ -165,8 +165,19 @@ namespace pdr {
void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars); void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars);
prop_solver& get_solver() { return m_solver; } prop_solver& get_solver() { return m_solver; }
prop_solver const& get_solver() const { return m_solver; }
void set_use_farkas(bool f) { get_solver().set_use_farkas(f); } void set_use_farkas(bool f) { get_solver().set_use_farkas(f); }
bool get_use_farkas() const { return get_solver().get_use_farkas(); }
class scoped_farkas {
bool m_old;
pred_transformer& m_p;
public:
scoped_farkas(pred_transformer& p, bool v): m_old(p.get_use_farkas()), m_p(p) {
p.set_use_farkas(v);
}
~scoped_farkas() { m_p.set_use_farkas(m_old); }
};
}; };

4
src/muz_qe/pdr_generalizers.cpp
View file

@ -196,7 +196,7 @@ namespace pdr {
); );
model_node nd(0, state, n.pt(), n.level()); model_node nd(0, state, n.pt(), n.level());
n.pt().set_use_farkas(true); pred_transformer::scoped_farkas sf(n.pt(), true);
if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) { if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
TRACE("pdr", TRACE("pdr",
tout << mk_pp(state, m) << "\n"; tout << mk_pp(state, m) << "\n";
@ -261,7 +261,7 @@ namespace pdr {
expr_ref state = pm.mk_and(conv1); expr_ref state = pm.mk_and(conv1);
TRACE("pdr", tout << "Try:\n" << mk_pp(state, m) << "\n";); TRACE("pdr", tout << "Try:\n" << mk_pp(state, m) << "\n";);
model_node nd(0, state, n.pt(), n.level()); model_node nd(0, state, n.pt(), n.level());
n.pt().set_use_farkas(true); pred_transformer::scoped_farkas sf(n.pt(), true);
if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) { if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
IF_VERBOSE(0, IF_VERBOSE(0,
verbose_stream() << mk_pp(state, m) << "\n"; verbose_stream() << mk_pp(state, m) << "\n";

1
src/muz_qe/pdr_prop_solver.h
View file

@ -99,6 +99,7 @@ namespace pdr {
}; };
void set_use_farkas(bool f) { m_use_farkas = f; } void set_use_farkas(bool f) { m_use_farkas = f; }
bool get_use_farkas() const { return m_use_farkas; }
void add_formula(expr * form); void add_formula(expr * form);
void add_level_formula(expr * form, unsigned level); void add_level_formula(expr * form, unsigned level);