mirror of
https://github.com/Z3Prover/z3
synced 2025-10-09 01:11:55 +00:00
add outline of axiomatization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
522be5d8c2
commit
ad7b248956
3 changed files with 86 additions and 1 deletions
85
src/ast/rewriter/finite_set_axioms.h
Normal file
85
src/ast/rewriter/finite_set_axioms.h
Normal file
|
@ -0,0 +1,85 @@
|
|||
/*++
|
||||
Copyright (c) 2025 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
finite_set_axioms.h
|
||||
|
||||
Abstract:
|
||||
Axiom schemas for finite sets.
|
||||
|
||||
Axiom schemars for finite sets are instantiated based on the state of the
|
||||
congruence closure and existing assertions in for finite sets.
|
||||
This module implements axiom schemas that are invoked by saturating constraints
|
||||
with respect to the semantics of set operations.
|
||||
|
||||
Let v1 ~ v2 mean that v1 and v2 are congruent
|
||||
|
||||
The set-based decision procedure relies on saturating with respect
|
||||
to rules of the form:
|
||||
|
||||
x in v1 == v2, v1 ~ set.empty
|
||||
--------------------------------
|
||||
not (x in set.empty)
|
||||
|
||||
|
||||
x in v1 == v2, v1 ~ v3, v3 == (set.union v4 v5)
|
||||
-----------------------------------------------
|
||||
x in v1 <=> x in v4 or x in v5
|
||||
|
||||
|
||||
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.select : (S -> Bool) (FiniteSet S) -> (FiniteSet S)
|
||||
set.range : Int Int -> (FiniteSet Int)
|
||||
|
||||
--*/
|
||||
|
||||
class finite_set_axioms {
|
||||
ast_manager& m;
|
||||
finite_set_util u;
|
||||
|
||||
std::function<void(expr_ref_vector const &)> m_add_clause;
|
||||
|
||||
public:
|
||||
|
||||
finite_set_axioms(ast_manager &m) : m(m), u(m) {}
|
||||
|
||||
void set_add_clause(std::function<void(expr_ref_vector const &)> &ac) {
|
||||
m_add_clause = ac;
|
||||
}
|
||||
|
||||
// a ~ set.empty => not (x in a)
|
||||
void in_empty_axiom(expr *x);
|
||||
|
||||
// a := set.union(b, c)
|
||||
// (x in a) <=> (x in b) or (x in c)
|
||||
void in_union_axiom(expr *x, expr *a);
|
||||
|
||||
// a := set.intersect(b, c)
|
||||
// (x in a) <=> (x in b) and (x in c)
|
||||
void in_intersect_axiom(expr *x, expr *a);
|
||||
|
||||
// a := set.difference(b, c)
|
||||
// (x in a) <=> (x in b) and not (x in c)
|
||||
void in_difference_axiom(expr *x, expr *a);
|
||||
|
||||
// a := set.singleton(b)
|
||||
// (x in a) <=> (x == b)
|
||||
void in_singleton_axiom(expr *x, expr *a);
|
||||
|
||||
// a := set.range(lo, hi)
|
||||
// (x in a) <=> (lo <= x <= hi)
|
||||
void in_range_axiom(expr *x, expr *a);
|
||||
|
||||
// a := set.map(f, b)
|
||||
// (x in a) <=> set.map_inverse(f, x, b)
|
||||
void in_map_axiom(expr *x, expr *a);
|
||||
|
||||
// a := set.select(p, b)
|
||||
// (x in a) <=> (x in b) and p(x)
|
||||
void in_select_axiom(expr *x, expr *a);
|
||||
|
||||
};
|
|
@ -3,7 +3,7 @@ Copyright (c) 2025 Microsoft Corporation
|
|||
|
||||
Module Name:
|
||||
|
||||
finite_sets_rewriter.h
|
||||
finite_set_rewriter.h
|
||||
|
||||
Abstract:
|
||||
Rewriting Simplification for finite sets
|
Loading…
Add table
Add a link
Reference in a new issue