(set-option :backend none)
(declare-datatype man (
(m1) (m2) (m3)
))
(declare-datatype woman (
(w1) (w2) (w3)
))
(declare-fun manOf (woman) man)
(declare-fun womanOf ( man) woman)
(declare-fun manPrefers ( man woman woman) Bool)
(declare-fun womanPrefers (woman man man) Bool)
(declare-fun manAssignsScore ( man woman) Int)
(declare-fun womanAssignsScore (woman man) Int)
; !x in man: !y in woman: womanOf(x)=y <=> manOf(y)=x.
;(assert (forall ((M man) (W woman))
; (= (= (womanOf M) W)
; (= ( manOf W) M))))
; ! M in man, W in woman: ~manPrefers(M,W,womanOf(M)) | ~womanPrefers(W,M,manOf(W))
;(assert (forall ((M man) (W woman))
; (or (not ( manPrefers M W (womanOf M)))
; (not (womanPrefers W M ( manOf W))))))
; ! M in man, W in woman, W1 in woman : manPrefers(M,W,W1) <=> manAssignsScore(M, W) > manAssignsScore(M, W1)
(assert (forall ((M man) (W woman) (W1 woman))
(= ( manPrefers M W W1)
(> ( manAssignsScore M W) ( manAssignsScore M W1)))))
; ! M in man, W in woman, M1 in man : womanPrefers(W,M,M1) <=> womanAssignsScore(W, M) > womanAssignsScore(W, M1)
;(assert (forall ((M man) (W woman) (M1 man))
; (= (womanPrefers W M M1)
; (> (womanAssignsScore W M) (womanAssignsScore W M1)))))
(x-interpret-fun manAssignsScore (x-mapping
((m1 w1) 16) ((m1 w2) 8) ((m1 w3) 7)
((m2 w1) 2) ((m2 w2) 12) ((m2 w3) 3)
((m3 w1) 17) ((m3 w2) 11) ((m3 w3) 1)
))
(x-interpret-fun womanAssignsScore (x-mapping
((w1 m1) 16) ((w1 m2) 8) ((w1 m3) 7)
((w2 m1) 2) ((w2 m2) 12) ((w2 m3) 3)
((w3 m1) 17) ((w3 m2) 11) ((w3 m3) 1)
))
(x-ground :debug :sql)
(x-debug solver functions)
(x-debug solver groundings)
------- RESULTS ------------------
(declare-datatype man ((m1) (m2) (m3)))
(declare-datatype woman ((w1) (w2) (w3)))
(declare-fun manOf (woman) man)
(declare-fun womanOf (man) woman)
(declare-fun manPrefers (man woman woman) Bool)
(declare-fun womanPrefers (woman man man) Bool)
(declare-fun manAssignsScore (man woman) Int)
(declare-fun womanAssignsScore (woman man) Int)
; ==== Query =============================
;-- Agg (0)
;SELECT G as G
; FROM (-- Join(7)
; SELECT _xmt_interp_manassignsscore_G_4.a_1 AS M,
; _xmt_interp_manassignsscore_G_4.a_2 AS W,
; _xmt_interp_manassignsscore_G_5.a_2 AS W1,
; apply("=", apply("manPrefers", _xmt_interp_manassignsscore_G_4.a_1, _xmt_interp_manassignsscore_G_4.a_2, _xmt_interp_manassignsscore_G_5.a_2), compare_(">", _xmt_interp_manassignsscore_G_4.G, _xmt_interp_manassignsscore_G_5.G)) AS G
; FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_4
; JOIN _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_5
; ON _xmt_interp_manassignsscore_G_4.a_1 = _xmt_interp_manassignsscore_G_5.a_1)(assert (= (manPrefers m1 w1 w1) false))
(assert (= (manPrefers m1 w1 w2) true))
(assert (= (manPrefers m1 w1 w3) true))
(assert (= (manPrefers m1 w2 w1) false))
(assert (= (manPrefers m1 w2 w2) false))
(assert (= (manPrefers m1 w2 w3) true))
(assert (= (manPrefers m1 w3 w1) false))
(assert (= (manPrefers m1 w3 w2) false))
(assert (= (manPrefers m1 w3 w3) false))
(assert (= (manPrefers m2 w1 w1) false))
(assert (= (manPrefers m2 w1 w2) false))
(assert (= (manPrefers m2 w1 w3) false))
(assert (= (manPrefers m2 w2 w1) true))
(assert (= (manPrefers m2 w2 w2) false))
(assert (= (manPrefers m2 w2 w3) true))
(assert (= (manPrefers m2 w3 w1) true))
(assert (= (manPrefers m2 w3 w2) false))
(assert (= (manPrefers m2 w3 w3) false))
(assert (= (manPrefers m3 w1 w1) false))
(assert (= (manPrefers m3 w1 w2) true))
(assert (= (manPrefers m3 w1 w3) true))
(assert (= (manPrefers m3 w2 w1) false))
(assert (= (manPrefers m3 w2 w2) false))
(assert (= (manPrefers m3 w2 w3) true))
(assert (= (manPrefers m3 w3 w1) false))
(assert (= (manPrefers m3 w3 w2) false))
(assert (= (manPrefers m3 w3 w3) false))
Functions2:
- true ()->Bool : Constructor
- false ()->Bool : Constructor
- not ()->Bool : Predefined (true)
- => ()->Bool : Predefined (true)
- and ()->Bool : Predefined (true)
- or ()->Bool : Predefined (true)
- xor ()->Bool : Predefined (true)
- = ()->Bool : Predefined (true)
- distinct ()->Bool : Predefined (true)
- <= ()->Bool : Predefined (true)
- < ()->Bool : Predefined (true)
- >= ()->Bool : Predefined (true)
- > ()->Bool : Predefined (true)
- ite ()->Bool : Predefined (?)
- let ()->Bool : Predefined (?)
- + ()->Real : Predefined (false)
- - ()->Real : Predefined (false)
- * ()->Real : Predefined (false)
- div ()->Real : Predefined (false)
- mod ()->Real : Predefined (false)
- abs ()->Real : Predefined (false)
- m1 ()->man : Constructor
- m2 ()->man : Constructor
- m3 ()->man : Constructor
- (_ is m1) (man)->Bool : Predefined (true)
- (_ is m2) (man)->Bool : Predefined (true)
- (_ is m3) (man)->Bool : Predefined (true)
- w1 ()->woman : Constructor
- w2 ()->woman : Constructor
- w3 ()->woman : Constructor
- (_ is w1) (woman)->Bool : Predefined (true)
- (_ is w2) (woman)->Bool : Predefined (true)
- (_ is w3) (woman)->Bool : Predefined (true)
- manOf (woman)->man : Not interpreted
- womanOf (man)->woman : Not interpreted
- manPrefers (man, woman, woman)->Bool : Not interpreted
- womanPrefers (woman, man, man)->Bool : Not interpreted
- manAssignsScore (man, woman)->Int : Non Boolean (_xmt_interp_manassignsscore_G Complete)
- womanAssignsScore (woman, man)->Int : Non Boolean (_xmt_interp_womanassignsscore_G Complete)
Groundings:
=== M ======================================
-- Join(0)
SELECT _xmt_sort_man.G AS M,
_xmt_sort_man.G AS G
FROM _xmt_sort_man
=== W ======================================
-- Join(0)
SELECT _xmt_sort_woman_1.G AS W,
_xmt_sort_woman_1.G AS G
FROM _xmt_sort_woman AS _xmt_sort_woman_1
=== W1 ======================================
-- Join(0)
SELECT _xmt_sort_woman_2.G AS W1,
_xmt_sort_woman_2.G AS G
FROM _xmt_sort_woman AS _xmt_sort_woman_2
=== (manPrefers M W W1) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_man.G AS M,
_xmt_sort_woman_1.G AS W,
_xmt_sort_woman_2.G AS W1,
apply("manPrefers", _xmt_sort_man.G, _xmt_sort_woman_1.G, _xmt_sort_woman_2.G) AS G
FROM _xmt_sort_man
JOIN _xmt_sort_woman AS _xmt_sort_woman_1
JOIN _xmt_sort_woman AS _xmt_sort_woman_2
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_man.G AS M,
_xmt_sort_woman_1.G AS W,
_xmt_sort_woman_2.G AS W1,
apply("manPrefers", _xmt_sort_man.G, _xmt_sort_woman_1.G, _xmt_sort_woman_2.G) AS G
FROM _xmt_sort_man
JOIN _xmt_sort_woman AS _xmt_sort_woman_1
JOIN _xmt_sort_woman AS _xmt_sort_woman_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_man.G AS M,
_xmt_sort_woman_1.G AS W,
_xmt_sort_woman_2.G AS W1,
apply("manPrefers", _xmt_sort_man.G, _xmt_sort_woman_1.G, _xmt_sort_woman_2.G) AS G
FROM _xmt_sort_man
JOIN _xmt_sort_woman AS _xmt_sort_woman_1
JOIN _xmt_sort_woman AS _xmt_sort_woman_2
=== (manAssignsScore M W) ======================================
-- Join(0)
SELECT _xmt_interp_manassignsscore_G_4.a_1 AS M,
_xmt_interp_manassignsscore_G_4.a_2 AS W,
_xmt_interp_manassignsscore_G_4.G AS G
FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_4
=== (manAssignsScore M W1) ======================================
-- Join(0)
SELECT _xmt_interp_manassignsscore_G_5.a_1 AS M,
_xmt_interp_manassignsscore_G_5.a_2 AS W1,
_xmt_interp_manassignsscore_G_5.G AS G
FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_5
=== (> (manAssignsScore M W) (manAssignsScore M W1)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_manassignsscore_G_4.a_1 AS M,
_xmt_interp_manassignsscore_G_4.a_2 AS W,
_xmt_interp_manassignsscore_G_5.a_2 AS W1,
compare_(">", _xmt_interp_manassignsscore_G_4.G, _xmt_interp_manassignsscore_G_5.G) AS G
FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_4
JOIN _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_5
ON _xmt_interp_manassignsscore_G_4.a_1 = _xmt_interp_manassignsscore_G_5.a_1
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_manassignsscore_G_4.a_1 AS M,
_xmt_interp_manassignsscore_G_4.a_2 AS W,
_xmt_interp_manassignsscore_G_5.a_2 AS W1,
compare_(">", _xmt_interp_manassignsscore_G_4.G, _xmt_interp_manassignsscore_G_5.G) AS G
FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_4
JOIN _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_5
ON _xmt_interp_manassignsscore_G_4.a_1 = _xmt_interp_manassignsscore_G_5.a_1
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_manassignsscore_G_4.a_1 AS M,
_xmt_interp_manassignsscore_G_4.a_2 AS W,
_xmt_interp_manassignsscore_G_5.a_2 AS W1,
compare_(">", _xmt_interp_manassignsscore_G_4.G, _xmt_interp_manassignsscore_G_5.G) AS G
FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_4
JOIN _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_5
ON _xmt_interp_manassignsscore_G_4.a_1 = _xmt_interp_manassignsscore_G_5.a_1
=== (= (manPrefers M W W1) (> (manAssignsScore M W) (manAssignsScore M W1))) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_manassignsscore_G_4.a_1 AS M,
_xmt_interp_manassignsscore_G_4.a_2 AS W,
_xmt_interp_manassignsscore_G_5.a_2 AS W1,
apply("=", apply("manPrefers", _xmt_interp_manassignsscore_G_4.a_1, _xmt_interp_manassignsscore_G_4.a_2, _xmt_interp_manassignsscore_G_5.a_2), compare_(">", _xmt_interp_manassignsscore_G_4.G, _xmt_interp_manassignsscore_G_5.G)) AS G
FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_4
JOIN _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_5
ON _xmt_interp_manassignsscore_G_4.a_1 = _xmt_interp_manassignsscore_G_5.a_1
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_manassignsscore_G_4.a_1 AS M,
_xmt_interp_manassignsscore_G_4.a_2 AS W,
_xmt_interp_manassignsscore_G_5.a_2 AS W1,
apply("=", apply("manPrefers", _xmt_interp_manassignsscore_G_4.a_1, _xmt_interp_manassignsscore_G_4.a_2, _xmt_interp_manassignsscore_G_5.a_2), compare_(">", _xmt_interp_manassignsscore_G_4.G, _xmt_interp_manassignsscore_G_5.G)) AS G
FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_4
JOIN _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_5
ON _xmt_interp_manassignsscore_G_4.a_1 = _xmt_interp_manassignsscore_G_5.a_1
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_manassignsscore_G_4.a_1 AS M,
_xmt_interp_manassignsscore_G_4.a_2 AS W,
_xmt_interp_manassignsscore_G_5.a_2 AS W1,
apply("=", apply("manPrefers", _xmt_interp_manassignsscore_G_4.a_1, _xmt_interp_manassignsscore_G_4.a_2, _xmt_interp_manassignsscore_G_5.a_2), compare_(">", _xmt_interp_manassignsscore_G_4.G, _xmt_interp_manassignsscore_G_5.G)) AS G
FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_4
JOIN _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_5
ON _xmt_interp_manassignsscore_G_4.a_1 = _xmt_interp_manassignsscore_G_5.a_1
=== (top) (forall ((M man) (W woman) (W1 woman)) (= (manPrefers M W W1) (> (manAssignsScore M W) (manAssignsScore M W1)))) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS M, NULL AS W, NULL AS W1, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_manassignsscore_G_4.a_1 AS M,
_xmt_interp_manassignsscore_G_4.a_2 AS W,
_xmt_interp_manassignsscore_G_5.a_2 AS W1,
apply("=", apply("manPrefers", _xmt_interp_manassignsscore_G_4.a_1, _xmt_interp_manassignsscore_G_4.a_2, _xmt_interp_manassignsscore_G_5.a_2), compare_(">", _xmt_interp_manassignsscore_G_4.G, _xmt_interp_manassignsscore_G_5.G)) AS G
FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_4
JOIN _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_5
ON _xmt_interp_manassignsscore_G_4.a_1 = _xmt_interp_manassignsscore_G_5.a_1)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT _xmt_interp_manassignsscore_G_4.a_1 AS M,
_xmt_interp_manassignsscore_G_4.a_2 AS W,
_xmt_interp_manassignsscore_G_5.a_2 AS W1,
apply("=", apply("manPrefers", _xmt_interp_manassignsscore_G_4.a_1, _xmt_interp_manassignsscore_G_4.a_2, _xmt_interp_manassignsscore_G_5.a_2), compare_(">", _xmt_interp_manassignsscore_G_4.G, _xmt_interp_manassignsscore_G_5.G)) AS G
FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_4
JOIN _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_5
ON _xmt_interp_manassignsscore_G_4.a_1 = _xmt_interp_manassignsscore_G_5.a_1)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS M, NULL AS W, NULL AS W1, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_manassignsscore_G_4.a_1 AS M,
_xmt_interp_manassignsscore_G_4.a_2 AS W,
_xmt_interp_manassignsscore_G_5.a_2 AS W1,
apply("=", apply("manPrefers", _xmt_interp_manassignsscore_G_4.a_1, _xmt_interp_manassignsscore_G_4.a_2, _xmt_interp_manassignsscore_G_5.a_2), compare_(">", _xmt_interp_manassignsscore_G_4.G, _xmt_interp_manassignsscore_G_5.G)) AS G
FROM _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_4
JOIN _xmt_interp_manassignsscore_G AS _xmt_interp_manassignsscore_G_5
ON _xmt_interp_manassignsscore_G_4.a_1 = _xmt_interp_manassignsscore_G_5.a_1)
===========================================