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

add control over Farkas parameter for Arie

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-07-16 23:42:50 +04:00
parent f1d3a13b7f
commit 0cd3c3364b
6 changed files with 19 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz_qe/dl_context.cpp
View file

@ -434,7 +434,9 @@ namespace datalog {
void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
symbol const * relation_names) {
ensure_engine();
if (relation_name_cnt > 0) {
ensure_engine();
}
if (relation_name_cnt > 0 && m_rel) {
m_rel->set_predicate_representation(pred, relation_name_cnt, relation_names);
}

6
src/muz_qe/pdr_context.cpp
View file

@ -1556,13 +1556,13 @@ namespace pdr {
if (use_mc) {
m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0));
}
if (m_params.use_farkas() && !classify.is_bool()) {
if (!classify.is_bool()) {
m.toggle_proof_mode(PGM_FINE);
m_fparams.m_arith_bound_prop = BP_NONE;
m_fparams.m_arith_auto_config_simplex = true;
m_fparams.m_arith_propagate_eqs = false;
m_fparams.m_arith_eager_eq_axioms = false;
if (classify.is_dl()) {
if (classify.is_dl() && m_params.use_utvpi()) {
m_fparams.m_arith_mode = AS_DIFF_LOGIC;
m_fparams.m_arith_expand_eqs = true;
}
@ -1571,7 +1571,6 @@ namespace pdr {
m_fparams.m_arith_mode = AS_UTVPI;
m_fparams.m_arith_expand_eqs = true;
}
}
if (m_params.use_convex_hull_generalizer()) {
m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this));
@ -1800,6 +1799,7 @@ namespace pdr {
m_expanded_lvl = n.level();
}
n.pt().set_use_farkas(m_params.use_farkas());
if (n.pt().is_reachable(n.state())) {
TRACE("pdr", tout << "reachable\n";);
close_node(n);

2
src/muz_qe/pdr_context.h
View file

@ -166,6 +166,8 @@ namespace pdr {
prop_solver& get_solver() { return m_solver; }
void set_use_farkas(bool f) { get_solver().set_use_farkas(f); }
};

2
src/muz_qe/pdr_generalizers.cpp
View file

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

7
src/muz_qe/pdr_prop_solver.cpp
View file

@ -237,6 +237,7 @@ namespace pdr {
m_proxies(m),
m_core(0),
m_subset_based_core(false),
m_use_farkas(false),
m_in_level(false)
{
m_ctx->assert_expr(m_pm.get_background());
@ -328,7 +329,11 @@ namespace pdr {
}
}
if (result == l_false && m_core && m.proofs_enabled() && !m_subset_based_core) {
if (result == l_false &&
m_core &&
m.proofs_enabled() &&
m_use_farkas &&
!m_subset_based_core) {
extract_theory_core(safe);
}
else if (result == l_false && m_core) {

3
src/muz_qe/pdr_prop_solver.h
View file

@ -50,6 +50,7 @@ namespace pdr {
model_ref* m_model;
bool m_subset_based_core;
bool m_assumes_level;
bool m_use_farkas;
func_decl_set m_aux_symbols;
bool m_in_level;
unsigned m_current_level; // set when m_in_level
@ -97,6 +98,8 @@ namespace pdr {
~scoped_level() { m_lev = false; }
};
void set_use_farkas(bool f) { m_use_farkas = f; }
void add_formula(expr * form);
void add_level_formula(expr * form, unsigned level);