109 lines
2.8 KiB
Text
109 lines
2.8 KiB
Text
(set-logic NIA)
|
|
|
|
(set-option :produce-models true)
|
|
(set-option :incremental true)
|
|
|
|
; Deklarace promennych pro vstupy
|
|
; ===============================
|
|
|
|
; Parametry
|
|
(declare-fun A () Int)
|
|
(declare-fun B () Int)
|
|
(declare-fun C () Int)
|
|
(declare-fun D () Int)
|
|
(declare-fun E () Int)
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
;;;;;;;; START OF SOLUTION ;;;;;;;;;;
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
; Declare the variables
|
|
(declare-fun x () Int)
|
|
(declare-fun y () Int)
|
|
(declare-fun z () Int)
|
|
|
|
|
|
; Constraints for D and E
|
|
(assert (and (> D 0) (> E 0)))
|
|
|
|
; Compute the variables
|
|
(assert (= x (* A B 2)))
|
|
(assert (ite (< x E) (= y (+ x (* 5 B))) (= y (- x C))))
|
|
(assert (ite (< (+ y 2) D) (= z (- (* x A) (* y B))) (= z (+ (* x B) (* y A)))))
|
|
|
|
; Function f returns true
|
|
(assert (< z (+ E D)))
|
|
|
|
; D + E is the smallest possible
|
|
(assert (forall ((d Int) (e Int) (X Int) (Y Int) (Z Int))
|
|
(=> (and (> d 0) (> e 0)
|
|
(= X (* A B 2))
|
|
(ite (< X e) (= Y (+ X (* 5 B))) (= Y (- X C)))
|
|
(ite (< (+ Y 2) d) (= Z (- (* X A) (* Y B))) (= Z (+ (* X B) (* Y A))))
|
|
(< Z (+ e d)))
|
|
(<= (+ D E) (+ d e))
|
|
)))
|
|
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
;;;;;;;;; END OF SOLUTION ;;;;;;;;;;;
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
; Testovaci vstupy
|
|
; ================
|
|
|
|
(echo "Test 1 - vstup A=1, B=1, C=3")
|
|
(echo "a) Ocekavany vystup je sat a D+E se rovna 2")
|
|
(check-sat-assuming (
|
|
(= A 1) (= B 1) (= C 3)
|
|
))
|
|
(get-value (D E (+ D E)))
|
|
(echo "b) Neexistuje jine reseni nez 2, ocekavany vystup je unsat")
|
|
(check-sat-assuming (
|
|
(= A 1) (= B 1) (= C 3) (distinct (+ D E) 2)
|
|
))
|
|
|
|
|
|
(echo "Test 2 - vstup A=5, B=2, C=5")
|
|
(echo "a) Ocekavany vystup je sat a D+E se rovna 54")
|
|
(check-sat-assuming (
|
|
(= A 5) (= B 2) (= C 5)
|
|
))
|
|
(get-value (D E (+ D E)))
|
|
(echo "b) Neexistuje jine reseni nez 54, ocekavany vystup je unsat")
|
|
(check-sat-assuming (
|
|
(= A 5) (= B 2) (= C 5) (distinct (+ D E) 54)
|
|
))
|
|
|
|
(echo "Test 3 - vstup A=100, B=15, C=1")
|
|
(echo "a) Ocekavany vystup je sat a D+E se rovna 253876")
|
|
(check-sat-assuming (
|
|
(= A 100) (= B 15) (= C 1)
|
|
))
|
|
(get-value (D E (+ D E)))
|
|
(echo "b) Neexistuje jine reseni nez 253876, ocekavany vystup je unsat")
|
|
(check-sat-assuming (
|
|
(= A 100) (= B 15) (= C 1) (distinct (+ D E) 253876)
|
|
))
|
|
|
|
(echo "Test 4 - vstup A=5, B=5, C=3")
|
|
(echo "a) Ocekavany vystup je sat a D+E se rovna 51")
|
|
(check-sat-assuming (
|
|
(= A 5) (= B 5) (= C 3)
|
|
))
|
|
(get-value (D E (+ D E)))
|
|
(echo "b) Neexistuje jine reseni nez 51, ocekavany vystup je unsat")
|
|
(check-sat-assuming (
|
|
(= A 5) (= B 5) (= C 3) (distinct (+ D E) 51)
|
|
))
|
|
|
|
(echo "Test 5 - vstup A=2, B=1, C=2")
|
|
(echo "a) Ocekavany vystup je sat a D+E se rovna 7")
|
|
(check-sat-assuming (
|
|
(= A 2) (= B 1) (= C 2)
|
|
))
|
|
(get-value (D E (+ D E)))
|
|
(echo "b) Neexistuje jine reseni nez 7, ocekavany vystup je unsat")
|
|
(check-sat-assuming (
|
|
(= A 2) (= B 1) (= C 2) (distinct (+ D E) 7)
|
|
))
|