anthem-rs/examples/example-exact-cover.spec

26 lines
1.1 KiB
RPMSpec
Raw Normal View History

2020-05-13 07:41:01 +02:00
# Auxiliary predicate to determine whether a variable is integer
2020-05-28 07:06:19 +02:00
#axiom: forall X (is_int(X) <-> exists N X = N).
2020-05-07 02:54:13 +02:00
2020-05-12 06:39:50 +02:00
# Perform the proofs under the assumption that n is a nonnegative integer input constant. n stands
# for the total number of input sets
input: n -> integer.
2020-05-29 12:09:28 +02:00
assume: n >= 0.
2020-05-12 06:39:50 +02:00
# s/2 is the input predicate defining the sets for which the program searches for exact covers
input: s/2.
2020-05-13 07:41:01 +02:00
# Only the in/1 predicate is an actual output, s/2 is an input and covered/1 and is_int/1 are
# auxiliary
output: in/1.
2020-05-12 06:39:50 +02:00
# Perform the proofs under the assumption that the second parameter of s/2 (the number of the set)
# is always an integer
2020-05-29 12:09:28 +02:00
assume: forall Y (exists X s(X, Y) -> exists N (Y = N and N >= 1 and N <= n)).
2020-05-07 02:54:13 +02:00
2020-05-12 06:39:50 +02:00
# Only valid sets can be included in the solution
2020-05-29 12:09:28 +02:00
spec: forall Y (in(Y) -> exists N (Y = N and N >= 1 and N <= n)).
2020-05-12 06:39:50 +02:00
# If an element is contained in an input set, it must be covered by all solutions
2020-05-29 12:09:28 +02:00
spec: forall X (exists Y s(X, Y) -> exists Y (in(Y) and s(X, Y))).
2020-05-12 06:39:50 +02:00
# Elements may not be covered by two input sets
2020-05-29 12:09:28 +02:00
spec: forall Y, Z (exists X (s(X, Y) and s(X, Z)) and in(Y) and in(Z) -> Y = Z).