You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
70 lines
1.9 KiB
70 lines
1.9 KiB
(set-option :produce-proofs true)
|
|
(declare-datatypes () ((Box (mk-box (fst Real) (snd Real) (trd Real)))))
|
|
|
|
; Valid interval = (1/2, 1)
|
|
(define-fun valint ((x Real)) Bool
|
|
(and (< 0.5 x) (< x 1)))
|
|
; Valid box
|
|
(define-fun valbox ((x Box)) Bool
|
|
(and (valint (fst x))
|
|
(valint (snd x))
|
|
(valint (trd x))))
|
|
|
|
(define-fun fits1 ((x1 Real) (x2 Real) (x3 Real) (y1 Real) (y2 Real) (y3 Real)) Bool
|
|
(and (< x1 y1) (< x2 y2) (< x3 y3)))
|
|
(define-fun fits2 ((x1 Real) (x2 Real) (x3 Real) (y1 Real) (y2 Real) (y3 Real)) Bool
|
|
(or
|
|
(fits1 x1 x2 x3 y1 y2 y3)
|
|
(fits1 x1 x2 x3 y1 y3 y2)
|
|
(fits1 x1 x2 x3 y2 y1 y3)
|
|
(fits1 x1 x2 x3 y2 y3 y1)
|
|
(fits1 x1 x2 x3 y3 y1 y2)
|
|
(fits1 x1 x2 x3 y3 y2 y1)))
|
|
; Box x fits inside box y
|
|
(define-fun fits ((x Box) (y Box)) Bool
|
|
(fits2 (fst x) (snd x) (trd x) (fst y) (snd y) (trd y)))
|
|
; x and y do not fit in each other
|
|
(define-fun nfits ((x Box) (y Box)) Bool
|
|
(and (not (fits x y)) (not (fits y x))))
|
|
|
|
; nodes
|
|
(declare-datatypes () ((Dom A1 A2 A4 A7 A8 A11 A13 A14)))
|
|
; edges
|
|
(declare-fun rel (Dom Dom) Bool)
|
|
; transitive
|
|
(assert (forall ((x Dom) (y Dom) (z Dom)) (implies (and (rel x y) (rel y z)) (rel x z))))
|
|
; acyclic
|
|
(assert (forall ((x Dom) (y Dom)) (not (and (rel x y) (rel y x)))))
|
|
|
|
(assert (rel A1 A7))
|
|
(assert (rel A2 A7))
|
|
(assert (rel A4 A7))
|
|
(assert (not (rel A8 A7)))
|
|
(assert (rel A1 A11))
|
|
(assert (rel A2 A11))
|
|
(assert (not (rel A4 A11)))
|
|
(assert (rel A8 A11))
|
|
(assert (rel A1 A13))
|
|
(assert (not (rel A2 A13)))
|
|
(assert (rel A4 A13))
|
|
(assert (rel A8 A13))
|
|
(assert (not (rel A1 A14)))
|
|
(assert (rel A2 A14))
|
|
(assert (rel A4 A14))
|
|
(assert (rel A8 A14))
|
|
|
|
; check graph
|
|
(check-sat)
|
|
(push)
|
|
|
|
; strong homomorphism to boxes
|
|
(declare-fun boxes (Dom) Box)
|
|
(assert (forall ((x Dom)) (valbox (boxes x))))
|
|
(assert (forall ((x Dom) (y Dom)) (implies (rel x y) (fits (boxes x) (boxes y)))))
|
|
(assert (forall ((x Dom) (y Dom)) (implies (fits (boxes x) (boxes y)) (rel x y))))
|
|
|
|
; Compute boxes
|
|
(check-sat)
|
|
; (get-proof)
|
|
(pop)
|
|
(exit)
|
|
|