mirror of
https://github.com/Z3Prover/z3
synced 2025-10-08 00:41:56 +00:00
Rename finite_sets to finite_set everywhere including file names
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
parent
aa9cb71f6b
commit
495cdba9af
7 changed files with 46 additions and 46 deletions
|
|
@ -1,194 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2025 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
finite_sets_decl_plugin.h
|
||||
|
||||
Abstract:
|
||||
Declaration plugin for finite sets signatures
|
||||
|
||||
Sort:
|
||||
FiniteSet(S)
|
||||
|
||||
Operators:
|
||||
set.empty : (FiniteSet S)
|
||||
set.singleton : S -> (FiniteSet S)
|
||||
set.union : (FiniteSet S) (FiniteSet S) -> (FiniteSet S)
|
||||
set.intersect : (FiniteSet S) (FiniteSet S) -> (FiniteSet S)
|
||||
set.difference : (FiniteSet S) (FiniteSet S) -> (FiniteSet S)
|
||||
set.in : S (FiniteSet S) -> Bool
|
||||
set.size : (FiniteSet S) -> Int
|
||||
set.subset : (FiniteSet S) (FiniteSet S) -> Bool
|
||||
set.map : (S -> T) (FiniteSet S) -> (FiniteSet T)
|
||||
set.filter : (S -> Bool) (FiniteSet S) -> (FiniteSet S)
|
||||
set.range : Int Int -> (FiniteSet Int)
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "ast/ast.h"
|
||||
|
||||
enum finite_sets_sort_kind {
|
||||
FINITE_SET_SORT
|
||||
};
|
||||
|
||||
enum finite_sets_op_kind {
|
||||
OP_FINITE_SET_EMPTY,
|
||||
OP_FINITE_SET_SINGLETON,
|
||||
OP_FINITE_SET_UNION,
|
||||
OP_FINITE_SET_INTERSECT,
|
||||
OP_FINITE_SET_DIFFERENCE,
|
||||
OP_FINITE_SET_IN,
|
||||
OP_FINITE_SET_SIZE,
|
||||
OP_FINITE_SET_SUBSET,
|
||||
OP_FINITE_SET_MAP,
|
||||
OP_FINITE_SET_FILTER,
|
||||
OP_FINITE_SET_RANGE,
|
||||
LAST_FINITE_SET_OP
|
||||
};
|
||||
|
||||
class finite_sets_decl_plugin : public decl_plugin {
|
||||
struct psig {
|
||||
symbol m_name;
|
||||
unsigned m_num_params;
|
||||
sort_ref_vector m_dom;
|
||||
sort_ref m_range;
|
||||
psig(ast_manager& m, char const* name, unsigned n, unsigned dsz, sort* const* dom, sort* rng):
|
||||
m_name(name),
|
||||
m_num_params(n),
|
||||
m_dom(m),
|
||||
m_range(rng, m)
|
||||
{
|
||||
m_dom.append(dsz, dom);
|
||||
}
|
||||
};
|
||||
|
||||
ptr_vector<psig> m_sigs;
|
||||
ptr_vector<sort> m_binding;
|
||||
bool m_init;
|
||||
|
||||
void init();
|
||||
bool is_sort_param(sort* s, unsigned& idx);
|
||||
bool match(ptr_vector<sort>& binding, sort* s, sort* sP);
|
||||
void match(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out);
|
||||
func_decl * mk_empty(sort* element_sort);
|
||||
func_decl * mk_finite_set_op(decl_kind k, unsigned arity, sort * const * domain, sort* range);
|
||||
sort * get_element_sort(sort* finite_set_sort) const;
|
||||
|
||||
public:
|
||||
finite_sets_decl_plugin();
|
||||
~finite_sets_decl_plugin() override;
|
||||
|
||||
decl_plugin * mk_fresh() override {
|
||||
return alloc(finite_sets_decl_plugin);
|
||||
}
|
||||
|
||||
void finalize() override {
|
||||
for (psig* s : m_sigs)
|
||||
dealloc(s);
|
||||
m_sigs.reset();
|
||||
}
|
||||
|
||||
//
|
||||
// Contract for sort:
|
||||
// parameters[0] - element sort
|
||||
//
|
||||
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
|
||||
|
||||
//
|
||||
// Contract for func_decl:
|
||||
// For OP_FINITE_SET_MAP and OP_FINITE_SET_FILTER:
|
||||
// parameters[0] - function declaration
|
||||
// For others:
|
||||
// no parameters
|
||||
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) override;
|
||||
|
||||
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
|
||||
|
||||
void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) override;
|
||||
|
||||
expr * get_some_value(sort * s) override;
|
||||
|
||||
bool is_fully_interp(sort * s) const override;
|
||||
|
||||
bool is_value(app * e) const override;
|
||||
|
||||
bool is_unique_value(app* e) const override;
|
||||
};
|
||||
|
||||
class finite_sets_recognizers {
|
||||
protected:
|
||||
family_id m_fid;
|
||||
public:
|
||||
finite_sets_recognizers(family_id fid):m_fid(fid) {}
|
||||
family_id get_family_id() const { return m_fid; }
|
||||
bool is_finite_set(sort* s) const { return is_sort_of(s, m_fid, FINITE_SET_SORT); }
|
||||
bool is_finite_set(expr* n) const { return is_finite_set(n->get_sort()); }
|
||||
bool is_empty(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_EMPTY); }
|
||||
bool is_singleton(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_SINGLETON); }
|
||||
bool is_union(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_UNION); }
|
||||
bool is_intersect(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_INTERSECT); }
|
||||
bool is_difference(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_DIFFERENCE); }
|
||||
bool is_in(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_IN); }
|
||||
bool is_size(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_SIZE); }
|
||||
bool is_subset(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_SUBSET); }
|
||||
bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_MAP); }
|
||||
bool is_filter(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_FILTER); }
|
||||
bool is_range(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_RANGE); }
|
||||
};
|
||||
|
||||
class finite_sets_util : public finite_sets_recognizers {
|
||||
ast_manager& m_manager;
|
||||
public:
|
||||
finite_sets_util(ast_manager& m):
|
||||
finite_sets_recognizers(m.mk_family_id("finite_sets")), m_manager(m) {}
|
||||
|
||||
ast_manager& get_manager() const { return m_manager; }
|
||||
|
||||
app * mk_empty(sort* element_sort) {
|
||||
parameter param(element_sort);
|
||||
return m_manager.mk_app(m_fid, OP_FINITE_SET_EMPTY, 1, ¶m, 0, nullptr);
|
||||
}
|
||||
|
||||
app * mk_singleton(expr* elem) {
|
||||
return m_manager.mk_app(m_fid, OP_FINITE_SET_SINGLETON, elem);
|
||||
}
|
||||
|
||||
app * mk_union(expr* s1, expr* s2) {
|
||||
return m_manager.mk_app(m_fid, OP_FINITE_SET_UNION, s1, s2);
|
||||
}
|
||||
|
||||
app * mk_intersect(expr* s1, expr* s2) {
|
||||
return m_manager.mk_app(m_fid, OP_FINITE_SET_INTERSECT, s1, s2);
|
||||
}
|
||||
|
||||
app * mk_difference(expr* s1, expr* s2) {
|
||||
return m_manager.mk_app(m_fid, OP_FINITE_SET_DIFFERENCE, s1, s2);
|
||||
}
|
||||
|
||||
app * mk_in(expr* elem, expr* set) {
|
||||
return m_manager.mk_app(m_fid, OP_FINITE_SET_IN, elem, set);
|
||||
}
|
||||
|
||||
app * mk_size(expr* set) {
|
||||
return m_manager.mk_app(m_fid, OP_FINITE_SET_SIZE, set);
|
||||
}
|
||||
|
||||
app * mk_subset(expr* s1, expr* s2) {
|
||||
return m_manager.mk_app(m_fid, OP_FINITE_SET_SUBSET, s1, s2);
|
||||
}
|
||||
|
||||
app * mk_map(expr* arr, expr* set) {
|
||||
return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP, arr, set);
|
||||
}
|
||||
|
||||
app * mk_filter(expr* arr, expr* set) {
|
||||
return m_manager.mk_app(m_fid, OP_FINITE_SET_FILTER, arr, set);
|
||||
}
|
||||
|
||||
app * mk_range(expr* low, expr* high) {
|
||||
return m_manager.mk_app(m_fid, OP_FINITE_SET_RANGE, low, high);
|
||||
}
|
||||
};
|
||||
Loading…
Add table
Add a link
Reference in a new issue