mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00
Code Activity

update contract

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-05 14:15:08 -07:00
parent 2ce30019ee
commit 97c8fb15fa
1 changed files with 9 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/rewriter/finite_set_axioms.h
View file

@ -27,13 +27,8 @@ Abstract:
----------------------------------------------- -----------------------------------------------
x in v1 <=> x in v4 or x in v5 x in v1 <=> x in v4 or x in v5
set.in : S (FiniteSet S) -> Bool
set.size : (FiniteSet S) -> Int set.size : (FiniteSet S) -> Int
set.subset : (FiniteSet S) (FiniteSet S) -> Bool set.subset : (FiniteSet S) (FiniteSet S) -> Bool
set.map : (S -> T) (FiniteSet S) -> (FiniteSet T)
set.select : (S -> Bool) (FiniteSet S) -> (FiniteSet S)
set.range : Int Int -> (FiniteSet Int)
--*/ --*/
@ -75,11 +70,19 @@ public:
void in_range_axiom(expr *x, expr *a); void in_range_axiom(expr *x, expr *a);
// a := set.map(f, b) // a := set.map(f, b)
// (x in a) <=> set.map_inverse(f, x, b) // (x in a) <=> set.map_inverse(f, x, b) in b
void in_map_axiom(expr *x, expr *a); void in_map_axiom(expr *x, expr *a);
// a := set.map(f, b)
// (x in b) => f(x) in a
void in_map_image_axiom(expr *x, expr *a);
// a := set.select(p, b) // a := set.select(p, b)
// (x in a) <=> (x in b) and p(x) // (x in a) <=> (x in b) and p(x)
void in_select_axiom(expr *x, expr *a); void in_select_axiom(expr *x, expr *a);
// a := set.singleton(b)
// set.size(a) = 1
void size_singleton_axiom(expr *a);
}; };