blob: 2945a8a24e154be713fa81f9aa50e23dbde4819b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(set-logic UFC)
(set-info :status unsat)
(declare-sort P 0)
(declare-sort H 0)
(declare-fun p () P)
(declare-fun h () H)
; pigeonhole using native cardinality constraints
(assert (_ fmf.card P 19))
(assert (not (_ fmf.card P 18)))
(assert (_ fmf.card H 18))
(assert (not (_ fmf.card H 17)))
; each pigeon has different holes
(declare-fun f (P) H)
(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2))))))
(check-sat)
|
