Skip to content

Commit

Permalink
Add missing noaxioms_sets.vpr
Browse files Browse the repository at this point in the history
  • Loading branch information
dnezam authored Apr 13, 2024
1 parent b321539 commit ba80f9d
Showing 1 changed file with 19 additions and 0 deletions.
19 changes: 19 additions & 0 deletions evaluation/scripts/noaxioms_sets.vpr
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// This Source Code Form is subject to the terms of the Mozilla Public
// License, v. 2.0. If a copy of the MPL was not distributed with this
// file, You can obtain one at http://mozilla.org/MPL/2.0/.
//
// Copyright (c) 2011-2023 ETH Zurich.

domain $Set[E] {
function Set_in(e: E, s: $Set[E]): Bool
function Set_card(s: $Set[E]): Int
function Set_empty(): $Set[E]
function Set_singleton(e: E): $Set[E]
function Set_unionone(s: $Set[E], e: E): $Set[E]
function Set_union(s1: $Set[E], s2: $Set[E]): $Set[E]
function Set_disjoint(s1: $Set[E], s2: $Set[E]): Bool
function Set_difference(s1: $Set[E], s2: $Set[E]): $Set[E]
function Set_intersection(s1: $Set[E], s2: $Set[E]): $Set[E]
function Set_subset(s1: $Set[E], s2: $Set[E]): Bool
function Set_equal(s1: $Set[E], s2: $Set[E]): Bool
}

0 comments on commit ba80f9d

Please sign in to comment.