mirror of
https://github.com/Z3Prover/z3
synced 2026-02-17 06:11:44 +00:00
78 lines
2.2 KiB
C++
78 lines
2.2 KiB
C++
/*++
|
|
Copyright (c) 2013 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
rule_properties.h
|
|
|
|
Abstract:
|
|
|
|
Collect properties of rules.
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner) 9-25-2014
|
|
|
|
Notes:
|
|
|
|
|
|
--*/
|
|
|
|
#pragma once
|
|
|
|
#include "ast/ast.h"
|
|
#include "ast/datatype_decl_plugin.h"
|
|
#include "ast/bv_decl_plugin.h"
|
|
#include "ast/array_decl_plugin.h"
|
|
#include "ast/arith_decl_plugin.h"
|
|
#include "ast/recfun_decl_plugin.h"
|
|
#include "muz/base/dl_rule.h"
|
|
#include "ast/expr_functors.h"
|
|
|
|
namespace datalog {
|
|
class rule_properties {
|
|
ast_manager& m;
|
|
rule_manager& rm;
|
|
context& m_ctx;
|
|
i_expr_pred& m_is_predicate;
|
|
datatype_util m_dt;
|
|
dl_decl_util m_dl;
|
|
arith_util m_a;
|
|
bv_util m_bv;
|
|
array_util m_ar;
|
|
recfun::util m_rec;
|
|
bool m_generate_proof;
|
|
rule* m_rule;
|
|
obj_map<quantifier, rule*> m_quantifiers;
|
|
obj_map<func_decl, rule*> m_uninterp_funs;
|
|
ptr_vector<rule> m_interp_pred;
|
|
ptr_vector<rule> m_negative_rules;
|
|
ptr_vector<rule> m_inf_sort;
|
|
bool m_collected;
|
|
bool m_is_monotone;
|
|
|
|
void insert(ptr_vector<rule>& rules, rule* r);
|
|
void check_sort(sort* s);
|
|
void visit_rules(expr_sparse_mark& visited, rule_set const& rules);
|
|
bool evaluates_to_numeral(expr * n, rational& val);
|
|
bool check_accessor(app* n);
|
|
public:
|
|
rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& is_predicate);
|
|
void set_generate_proof(bool generate_proof) { m_generate_proof = generate_proof; }
|
|
void collect(rule_set const& r);
|
|
void check_quantifier_free();
|
|
void check_quantifier_free(quantifier_kind qkind);
|
|
void check_uninterpreted_free();
|
|
void check_existential_tail();
|
|
void check_for_negated_predicates();
|
|
void check_nested_free();
|
|
void check_infinite_sorts();
|
|
void check_background_free();
|
|
bool is_monotone() { return m_is_monotone; }
|
|
void operator()(var* n);
|
|
void operator()(quantifier* n);
|
|
void operator()(app* n);
|
|
void reset();
|
|
};
|
|
}
|
|
|