mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

placeholder for finite set signature

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-04 17:18:12 -07:00
parent c8bdbd2dc4
commit e0fca3ba25
2 changed files with 26 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

0
src/ast/finite_sets_decl_plugin.cpp Normal file
View file

26
src/ast/finite_sets_decl_plugin.h Normal file
View file

@ -0,0 +1,26 @@
/*++
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.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)
--*/