I want to solve this in the z3 solver with bit vector 48:
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= *someNumber* (* x y)))
(assert (> x 1))
(assert (> y 1))
(check-sat)
(get-model)
(exit)
I'm trying to figure out how to use the arithmetic function however, it does not work out very well. The problems with that (for me) are the correct Syntax of the functions && how to set the values in there.
(set-option :produce-models true)
(set-logic QF_BV)
;; Declaring all the variables
(declare-const a (_ BitVec 48))
(declare-const b (_ BitVec 48))
(declare-const c (_ BitVec 48))
;; Soft constraints to limit reuse
(assert (= c #xnumberInHex))
(assert-soft (not (= a b)))
(check-sat-using (then simplify solve-eqs bit-blast sat))
(simplify (= c (bvmul a b))
(simplify (bvugt a #b000000000001))
(simplify (bvugt b #b000000000001))
(check-sat)
(get-model)
Any help is much appreciated. Syntax / how to write the correct bit vector there
Looks like you've got almost all the pieces in there, but perhaps not exactly getting the syntax right. Here's a complete encoding with c = 18:
(set-option :produce-models true)
(set-logic ALL)
;; Declaring all the variables
(declare-const a (_ BitVec 48))
(declare-const b (_ BitVec 48))
(declare-const c (_ BitVec 48))
(assert (= c #x000000000012)) ; 18 is 0x12 in hex
(assert (= c (bvmul a b)))
; don't allow overflow
(assert (bvumul_noovfl a b))
(assert (bvult #x000000000001 a))
(assert (bvult #x000000000001 b))
;; Soft constraints to limit reuse
(assert-soft (not (= a b)))
(check-sat)
(get-model)
Note the use of the ALL logic and the function bvumul_noovfl which detects unsigned bit-vector multiplication overflow. (This function is z3 specific, and is only available when you pick the logic to be ALL.) Since you're doing bit-vector arithmetic, it is subject to wrap-around, and I'm guessing this is something you'd like to avoid. By explicitly stating we do not want the multiplication of a and b to overflow, we're achieving that goal.
For this input, z3 says:
sat
(model
(define-fun b () (_ BitVec 48)
#x000000000009)
(define-fun a () (_ BitVec 48)
#x000000000002)
(define-fun c () (_ BitVec 48)
#x000000000012)
)
which correctly factors the number 18 (written here in hexadecimal as 12) into 2 and 9.
Note that multiplication is a hard problem. As you increase the bit-size (here you picked 48, but could be larger), or if the number c itself gets larger, the problem will become harder and harder for z3 to solve. This is, of course, not surprising: Factorization is a hard problem in general, and there's no magic here for z3 to correctly factor your input value without solving a huge set of internal equations, which increase exponentially in size as the bit-width increases.
But fear not: Bit-vector logic is complete: This means that z3 will always be able to factor, albeit slowly, assuming you do not run out of memory or patience first!