Skip to content

Instantly share code, notes, and snippets.

@moyix

moyix/synth.smt2

Created July 27, 2020 17:38
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save moyix/ac50dd264dc4cf2e72154b2e04280492 to your computer and use it in GitHub Desktop.
Save moyix/ac50dd264dc4cf2e72154b2e04280492 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
synth.smt2
; Synthesis example:
; specification: x * 9
; template: x << (hb1 ? x : hn1) + (hb2 ? x : hn2)
(declare-const hb1!1 (_ BitVec 64))
(declare-const hb2!3 (_ BitVec 64))
(declare-const hn1!2 (_ BitVec 64))
(declare-const hn2!4 (_ BitVec 64))
(assert
(forall ((x!0 (_ BitVec 64)))
(= (bvmul x!0 #x0000000000000009)
(bvadd (bvshl x!0
(bvadd (bvmul (ite (not (= hb1!1 #x0000000000000000))
#x0000000000000001
#x0000000000000000)
x!0)
(bvmul (ite (= hb1!1 #x0000000000000000)
#x0000000000000001
#x0000000000000000)
hn1!2)))
(bvmul (ite (not (= hb2!3 #x0000000000000000))
#x0000000000000001
#x0000000000000000)
x!0)
(bvmul (ite (= hb2!3 #x0000000000000000)
#x0000000000000001
#x0000000000000000)
hn2!4))))
)
(check-sat)
(get-model)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment