squares.smt

(set-option :pp.bv-literals false)
(define-sort I () (_ BitVec 300))

(declare-const a I)
(declare-const b I)
(declare-const c I)
(declare-const d I)
(declare-const e I)
(declare-const f I)
(declare-const g I)
(declare-const h I) (declare-const i I)

; a through i are square numbers.
(declare-const aRoot I)
(declare-const bRoot I)
(declare-const cRoot I)
(declare-const dRoot I)
(declare-const eRoot I)
(declare-const fRoot I)
(declare-const gRoot I)
(declare-const hRoot I)
(declare-const iRoot I)

(assert (bvult aRoot (_ bv713623846352979940529142984724747568191373312 300)))
(assert (bvult bRoot (_ bv713623846352979940529142984724747568191373312 300)))
(assert (bvult cRoot (_ bv713623846352979940529142984724747568191373312 300)))
(assert (bvult dRoot (_ bv713623846352979940529142984724747568191373312 300)))
(assert (bvult eRoot (_ bv713623846352979940529142984724747568191373312 300)))
(assert (bvult fRoot (_ bv713623846352979940529142984724747568191373312 300)))
(assert (bvult gRoot (_ bv713623846352979940529142984724747568191373312 300)))
(assert (bvult hRoot (_ bv713623846352979940529142984724747568191373312 300)))
(assert (bvult iRoot (_ bv713623846352979940529142984724747568191373312 300)))

(assert (= a (bvmul aRoot aRoot)))
(assert (= b (bvmul bRoot bRoot)))
(assert (= c (bvmul cRoot cRoot)))
(assert (= d (bvmul dRoot dRoot)))
(assert (= e (bvmul eRoot eRoot)))
(assert (= f (bvmul fRoot fRoot)))
(assert (= g (bvmul gRoot gRoot)))
(assert (= h (bvmul hRoot hRoot)))
(assert (= i (bvmul iRoot iRoot)))

(assert (bvumul_noovfl aRoot aRoot))
(assert (bvumul_noovfl bRoot bRoot))
(assert (bvumul_noovfl cRoot cRoot))
(assert (bvumul_noovfl dRoot dRoot))
(assert (bvumul_noovfl eRoot eRoot))
(assert (bvumul_noovfl fRoot fRoot))
(assert (bvumul_noovfl gRoot gRoot))
(assert (bvumul_noovfl hRoot hRoot))
(assert (bvumul_noovfl iRoot iRoot))

(declare-const target I)

; The rows sum to the target.
(assert (= target (bvadd a b c)))
(assert (= target (bvadd d e f)))
(assert (= target (bvadd g h i)))

; The columns sum to the target.
(assert (= target (bvadd a d g)))
(assert (= target (bvadd b e h)))
(assert (= target (bvadd c f i)))

; The diagonals sum to the target.
(assert (= target (bvadd a e i)))
(assert (= target (bvadd c e g)))

; All the numbers are different.
(assert (distinct a b c d e f g h i))

; Add the strictest modulo invariant from this page:
; http://www.multimagie.com/English/SquaresOfSquaresSearch.htm
(declare-const x I)
(declare-const y I)
(declare-const z I)
(assert (= a (bvadd x y)))
(assert (= b (bvsub (bvsub x y) z)))
(assert (= c (bvadd x z)))
(assert (= d (bvadd (bvsub x y) z)))
(assert (= e x))
(assert (= f (bvsub (bvadd x y) z)))
(assert (= g (bvsub x z)))
(assert (= h (bvadd x y z)))
(assert (= i (bvsub x y)))
(assert (= (_ bv0 300)
           (bvurem (bvmul x y z (bvadd y z) (bvsub y z))
					        	(_ bv1546645545467664981281303961600 300))))

(check-sat)
(get-value (a))
(get-value (b))
(get-value (c))
(get-value (d))
(get-value (e))
(get-value (f))
(get-value (g))
(get-value (h))
(get-value (i))
(get-value (target))
(get-value (aRoot))
(get-value (bRoot))
(get-value (cRoot))
(get-value (dRoot))
(get-value (eRoot))
(get-value (fRoot))
(get-value (gRoot))
(get-value (hRoot))
(get-value (iRoot))