SMT2 Description of the vietnamese problem

VietnameseSMT2

;Nous déclarons 10 nombres entiers nommés a,b,c,...,i :
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(declare-const g Int)
(declare-const h Int)
(declare-const i Int)</code>

;Ces nombres doivent etre distincts :
(assert (distinct a b c d e f g h i))

;Ces nombres doivent etre compris entre 0 et 10 exclus :
(assert (and (&gt; a 0) (&lt; a 10))) (assert (and (&gt; b 0) (&lt; b 10))) (assert (and (&gt; c 0) (&lt; c 10))) (assert (and (&gt; d 0) (&lt; d 10))) (assert (and (&gt; e 0) (&lt; e 10))) (assert (and (&gt; f 0) (&lt; f 10))) (assert (and (&gt; g 0) (&lt; g 10))) (assert (and (&gt; h 0) (&lt; h 10))) (assert (and (&gt; i 0) (&lt; i 10)))

;Ces nombres doivent vérifier l'equation donnee par le schema :
; a + 13 * b / c + d + 12 * e - f - 11 + g * h / i - 10 = 66
(assert (= (- (+(-(- (+ (+ (+ a (div (* 13 b) c)) d) (* 12 e)) f) 11) (div (* g h) i)) 10) 66))

;Enfin nous demandons au programme de trouver une solution et de l'afficher
(check-sat)
(get-model)