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

Allow bool_ind_generalizer to skip non-array literals

Browse source 
Currently a hack to skip generalizing some literals.
Used together with quic generalizer to remove all array terms if possible
before quic generalization
This commit is contained in:
Arie Gurfinkel 2017-12-26 16:49:48 -05:00
parent 46fb0d928a
commit 7dee36358d
2 changed files with 33 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/muz/spacer/spacer_generalizers.cpp
View file

@ -24,8 +24,15 @@ Revision History:
#include "ast/expr_abstract.h"
#include "ast/rewriter/var_subst.h"
#include "ast/for_each_expr.h"
#include "muz/spacer/spacer_term_graph.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/substitution/matcher.h"
#include "ast/expr_functors.h"
namespace spacer {
void lemma_sanity_checker::operator()(lemma_ref &lemma) {
unsigned uses_level;
@ -36,6 +43,19 @@ void lemma_sanity_checker::operator()(lemma_ref &lemma) {
lemma->weakness()));
}
namespace{
class contains_array_op_proc : public i_expr_pred {
ast_manager &m;
family_id m_array_fid;
public:
contains_array_op_proc(ast_manager &manager) :
m(manager), m_array_fid(m.mk_family_id("array"))
{}
virtual bool operator()(expr *e) {
return is_app(e) && to_app(e)->get_family_id() == m_array_fid;
}
};
}
// ------------------------
// lemma_bool_inductive_generalizer
@ -50,6 +70,9 @@ void lemma_bool_inductive_generalizer::operator()(lemma_ref &lemma) {
pred_transformer &pt = lemma->get_pob()->pt();
ast_manager &m = pt.get_ast_manager();
contains_array_op_proc has_array_op(m);
check_pred has_arrays(has_array_op, m);
expr_ref_vector cube(m);
cube.append(lemma->get_cube());
@ -65,6 +88,11 @@ void lemma_bool_inductive_generalizer::operator()(lemma_ref &lemma) {
(!m_failure_limit || num_failures < m_failure_limit)) {
expr_ref lit(m);
lit = cube.get(i);
if (m_array_only && !has_arrays(lit)) {
processed.push_back(lit);
++i;
continue;
}
cube[i] = true_expr;
if (cube.size() > 1 &&
pt.check_inductive(lemma->level(), cube, uses_level, weakness)) {

7
src/muz/spacer/spacer_generalizers.h
View file

@ -48,11 +48,14 @@ class lemma_bool_inductive_generalizer : public lemma_generalizer {
};
unsigned m_failure_limit;
bool m_array_only;
stats m_st;
public:
lemma_bool_inductive_generalizer(context& ctx, unsigned failure_limit) :
lemma_generalizer(ctx), m_failure_limit(failure_limit) {}
lemma_bool_inductive_generalizer(context& ctx, unsigned failure_limit,
bool array_only = false) :
lemma_generalizer(ctx), m_failure_limit(failure_limit),
m_array_only(array_only) {}
~lemma_bool_inductive_generalizer() override {}
void operator()(lemma_ref &lemma) override;