active questions tagged z3 - Stack Overflow News Feed 
Tuesday, March 31, 2015  |  From active questions tagged z3 - Stack Overflow




The link mentioned in the online tutorial doesn't contain any link to opt branch:



http://z3.codeplex.com/


and also there isn't any page under download section... Is it possible to get the binaries for windows/linux?



Thanks



Monday, March 30, 2015  |  From active questions tagged z3 - Stack Overflow




We look for a number of the form efghiihgfe which is the product of two numbers of the form 999ab and 99qcd.



We use the following code



 (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)
(declare-const p Int)
(declare-const q Int)


(assert (and (>= a 0) (<= a 9)))
(assert (and (>= b 0) (<= b 9)))
(assert (and (>= c 0) (<= c 9)))
(assert (and (>= d 0) (<= d 9)))
(assert (and (>= e 0) (<= e 9)))
(assert (and (>= f 0) (<= f 9)))
(assert (and (>= g 0) (<= g 9)))
(assert (and (>= h 0) (<= h 9)))
(assert (and (>= i 0) (<= i 9)))
(assert (and (>= p 0) (<= p 9)))
(assert (and (>= q 0) (<= q 9)))


(assert (= (* (+ 99900 (* 10 a) b  )  (+ 99000 (* 100 q) (* 10 c)  d  ))      
           (+ (* (^ 10 9) e) (* (^ 10 8)  f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5)   i)    
              (* (^ 10 4)  i)  (* 1000 h ) (* 100 g) (* 10 f) e)    ) )




(check-sat)
(get-model)

(eval (+ (* (^ 10 9) e) (* (^ 10 8)  f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5)   i)    
              (* (^ 10 4)  i)  (* 1000 h ) (* 100 g) (* 10 f) e))


and the output is



    (model
  (define-fun q () Int
    6)
  (define-fun p () Int
    0)
  (define-fun i () Int
    0)
  (define-fun h () Int
    6)
  (define-fun g () Int
    6)
  (define-fun f () Int
    9)
  (define-fun e () Int
    9)
  (define-fun d () Int
    1)
  (define-fun c () Int
    8)
  (define-fun b () Int
    9)
  (define-fun a () Int
    7)
)
9966006699


To verify that 9966006699 is the maxim we run the code



 (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)
(declare-const p Int)
(declare-const q Int)


(assert (and (>= a 0) (<= a 9)))
(assert (and (>= b 0) (<= b 9)))
(assert (and (>= c 0) (<= c 9)))
(assert (and (>= d 0) (<= d 9)))
(assert (and (>= e 0) (<= e 9)))
(assert (and (>= f 0) (<= f 9)))
(assert (and (>= g 0) (<= g 9)))
(assert (and (>= h 0) (<= h 9)))
(assert (and (>= i 0) (<= i 9)))
(assert (and (>= p 0) (<= p 9)))
(assert (and (>= q 0) (<= q 9)))


(assert (= (* (+ 99900 (* 10 a) b  )  (+ 99000 (* 100 q) (* 10 c)  d  ))      
           (+ (* (^ 10 9) e) (* (^ 10 8)  f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5)   i)    
              (* (^ 10 4)  i)  (* 1000 h ) (* 100 g) (* 10 f) e)    ) )


(assert  (> (+ (* (^ 10 9) e) (* (^ 10 8)  f) (* (^ 10 7) g) (* (^ 10 6) h) (* (^ 10 5)   i)    
              (* (^ 10 4)  i)  (* 1000 h ) (* 100 g) (* 10 f) e)   9966006699 ))

(check-sat)


and the output is



unsat


Please let me know if there is a more efficient program with Z3 to solve the problem.



Sunday, March 29, 2015  |  From active questions tagged z3 - Stack Overflow




Based on "Test-Only Development" with the Z3 Theorem Prover, I'm trying to encode Project Euler problem 4 in SMT-LIB and solve it using Z3.



The problem is to find the largest palindromic integer product of two three-digit numbers. The solution is 993 * 913 = 906609.



In the code below, I've only been able to encode that two three-digit numbers should be palindromic. This produces the correct, but not maximal, value of 604406.



How can I change my code so that the maximal value of 906609 is found?
I've tried using (maximize (* p q)), but that reports an error, saying Objective function '(* p q)' is not supported. I can tweak the range of a, but I'm looking for a way to have Z3 do that for me.



What I have so far is:



(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(declare-const p Int)
(declare-const q Int)

(declare-const pq Int)

(define-fun satisfy ((pq Int)) Bool
 (and
  (<= 1 a 9)
  (<= 0 b 9)
  (<= 0 c 9)

  (<= 100 p 999)
  (<= p q 999)

  (= pq
     (* p q)
     (+ (* 100001 a)
        (*  10010 b)
        (*   1100 c)))))

(assert (satisfy pq))

; Does not work:
;(maximize (* p q))

(check-sat)
(get-model)


Running this with z3 -smt2 e4.smt2 as-is produces:



sat
(model
  (define-fun q () Int
    913)
  (define-fun p () Int
    662)
  (define-fun c () Int
    4)
  (define-fun b () Int
    0)
  (define-fun a () Int
    6)
  (define-fun pq () Int
    604406)
)


Sunday, March 29, 2015  |  From active questions tagged z3 - Stack Overflow




Based on "Test-Only Development" with the Z3 Theorem Prover, I'm trying to encode Project Euler problem 4 in SMT-LIB and solve it using Z3.



The problem is to find the largest palindromic integer product of two three-digit numbers. The solution is 993 * 913 = 906609.



In the code below, I've only been able to encode that two three-digit numbers should be palindromic. This produces the correct, but not maximal, value of 604406.



How can I change my code so that the maximal value of 906609 is found?
I've tried using (maximize (* p q)), but that reports an error, saying Objective function '(* p q)' is not supported. I can tweak the range of a, but I'm looking for a way to have Z3 do that for me.



What I have so far is:



(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(declare-const p Int)
(declare-const q Int)

(declare-const pq Int)

(define-fun satisfy ((pq Int)) Bool
 (and
  (<= 1 a 9)
  (<= 0 b 9)
  (<= 0 c 9)

  (<= 100 p 999)
  (<= p q 999)

  (= pq
     (* p q)
     (+ (* 100001 a)
        (*  10010 b)
        (*   1100 c)))))

(assert (satisfy pq))

; Does not work:
;(maximize (* p q))

(check-sat)
(get-model)


Running this with z3 -smt2 e4.smt2 as-is produces:



sat
(model
  (define-fun q () Int
    913)
  (define-fun p () Int
    662)
  (define-fun c () Int
    4)
  (define-fun b () Int
    0)
  (define-fun a () Int
    6)
  (define-fun pq () Int
    604406)
)


Sunday, March 29, 2015  |  From active questions tagged z3 - Stack Overflow




This smt2 script gives UNSAT if I use
(check-sat-using (then simplify solve-eqs (repeat bit-blast) (! smt :bv.enable_int2bv true :arith.euclidean_solver true))), and gives SAT if I remove ":arith.euclidean_solver true". The expected result is SAT.
Z3 version 4.4.0



Thank you in advance.



Sunday, March 29, 2015  |  From active questions tagged z3 - Stack Overflow




Based on "Test-Only Development" with the Z3 Theorem Prover, I'm trying to encode Project Euler problem 4 in SMT-LIB and solve it using Z3.



The problem is to find the largest palindromic integer product of two three-digit numbers. The solution is 993 * 913 = 906609.



In the code below, I've only been able to encode that two three-digit numbers should be palindromic. This produces the correct, but not maximal, value of 604406.



How can I change my code so that the maximal value of 906609 is found?
I've tried using (maximize (* p q)), but that reports an error, saying Objective function '(* p q)' is not supported. I can tweak the range of a, but I'm looking for a way to have Z3 do that for me.



What I have so far is:



(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(declare-const p Int)
(declare-const q Int)

(declare-const pq Int)

(define-fun satisfy ((pq Int)) Bool
 (and
  (<= 1 a 9)
  (<= 0 b 9)
  (<= 0 c 9)

  (<= 100 p 999)
  (<= p q 999)

  (= pq
     (* p q)
     (+ (* 100001 a)
        (*  10010 b)
        (*   1100 c)))))

(assert (satisfy pq))

; Does not work:
;(maximize (* p q))

(check-sat)
(get-model)


Running this with z3 -smt2 e4.smt2 as-is produces:



sat
(model
  (define-fun q () Int
    913)
  (define-fun p () Int
    662)
  (define-fun c () Int
    4)
  (define-fun b () Int
    0)
  (define-fun a () Int
    6)
  (define-fun pq () Int
    604406)
)


Friday, March 27, 2015  |  From active questions tagged z3 - Stack Overflow




Based on "Test-Only Development" with the Z3 Theorem Prover, I'm trying to encode Project Euler problem 4 in SMT-LIB and solve it using Z3.



The problem is to find the largest palindromic integer product of two three-digit numbers. The solution is 993 * 913 = 906609.



In the code below, I've only been able to encode that two three-digit numbers should be palindromic. This produces the correct, but not maximal, value of 604406.



How can I change my code so that the maximal value of 906609 is found?
I've tried using (maximize (* p q)), but that reports an error, saying Objective function '(* p q)' is not supported. I can tweak the range of a, but I'm looking for a way to have Z3 do that for me.



What I have so far is:



(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(declare-const p Int)
(declare-const q Int)

(declare-const pq Int)

(define-fun satisfy ((pq Int)) Bool
 (and
  (<= 1 a 9)
  (<= 0 b 9)
  (<= 0 c 9)

  (<= 100 p 999)
  (<= p q 999)

  (= pq
     (* p q)
     (+ (* 100001 a)
        (*  10010 b)
        (*   1100 c)))))

(assert (satisfy pq))

; Does not work:
;(maximize (* p q))

(check-sat)
(get-model)


Running this with z3 -smt2 e4.smt2 as-is produces:



sat
(model
  (define-fun q () Int
    913)
  (define-fun p () Int
    662)
  (define-fun c () Int
    4)
  (define-fun b () Int
    0)
  (define-fun a () Int
    6)
  (define-fun pq () Int
    604406)
)


Wednesday, March 25, 2015  |  From active questions tagged z3 - Stack Overflow




A small example indicates that the nonlinear real arithmetic (NRA) solvers are hindered when NRA assertions are labeled by premises pi in connection with (sat p1 ... pn) checks.



The following SMT2 example returns SAT with the correct model:



(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)

(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)

(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))

(assert (and p1 p2 p3 p4))
(check-sat)
(get-model)


The following semantically equivalent example returns unknown:



(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)

(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)

(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))

(check-sat p1 p2 p3 p4)
(get-model)


Moreover, the model query returns a model, which is incorrect!



Working with the first style is not an option for me since I am particularly interested in getting unsat-cores from UNSAT problem instances, and I wish to dynamically combine "active" premises. However, by connecting the premise with "and", unsat core production is prevented.



It looks like the first example with (assert (and p1 p2 p3 p4)) is somehow simplified in a preprocessing step, so that the NRA solver looks at all four constraints together and is able to solve them. This seems not to be the case using the second example with (check-sat p1 p2 p3 p4).



Am I missing something? Thank you!



PS: I'm working with Z3 version 4.4.0 from the unstable branch (loaded 2015-03-26).



Wednesday, March 25, 2015  |  From active questions tagged z3 - Stack Overflow




A small example indicates that the nonlinear real arithmetic (NRA) solvers are hindered when NRA assertions are labeled by premises pi in connection with (sat p1 ... pn) checks.



The following SMT2 example returns SAT with the correct model:



(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)

(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)

(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))

(assert (and p1 p2 p3 p4))
(check-sat)
(get-model)


The following semantically equivalent example returns unknown:



(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)

(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)

(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))

(check-sat p1 p2 p3 p4)
(get-model)


Moreover, the model query returns a model, which is incorrect!



Working with the first style is not an option for me since I am particularly interested in getting unsat-cores from UNSAT problem instances, and I wish to dynamically combine "active" premises. However, by connecting the premise with "and", unsat core production is prevented.



It looks like the first example with (assert (and p1 p2 p3 p4)) is somehow simplified in a preprocessing step, so that the NRA solver looks at all four constraints together and is able to solve them. This seems not to be the case using the second example with (check-sat p1 p2 p3 p4).



Am I missing something? Thank you!



PS: I'm working with Z3 version 4.4.0 from the unstable branch (loaded 2015-03-26).



Wednesday, March 25, 2015  |  From active questions tagged z3 - Stack Overflow




While trying to solve large nonlinear real arithmetic problems, I track every assertion using answer literals and explicit implications, as recommended in other posts. It should be equivalent to using the (! (...) :named p1) syntax of the SMT2 format. It seems, though, that both methods are handled differently internally.



The following SMT2 code gives an UNKNOWN result, with explanation "(incomplete (theory arithmetic))":



(set-option :print-success false) 
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation

(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)
(declare-const p5 Bool)

(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)

(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))
(assert (=> p5 (< x3 0.0)))
(check-sat p1 p2 p3)
(get-info:reason-unknown)


On the other hand, the following SMT2 code gives the correct answer, UNSAT, and produces an informative unsat core (p4, p5):



(set-option :print-success false) 
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation

(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)

(assert (! (= x1 (/ 1.0 (* x2 x2))) :named p1))
(assert (! (not (= x2 0.0)) :named p2))
(assert (! (= x3 (* 2.0 x1)) :named p3))
(assert (! (= x3 5.0) :named p4))
(assert (! (< x3 0) :named p5))
(check-sat)
(get-unsat-core)
;(get-model)


My specific questions are:



  • How can this differing behavior be explained? What is recommended practice for tracking nonlinear real equations and inequalities?
  • What would be the equivalent OCaml API call for the (! (...) :named p1) syntax of SMT2? Is it assert_and_track?

I am using Z3 version 4.3.2 from the ml-ng branch under Linux.



Many thanks!



Saturday, March 21, 2015  |  From active questions tagged z3 - Stack Overflow




My problem is as followed,



Environment: 64 bit windows 7, vs 2010, z3-4.3.2



First, compiled Z3 from source(download from z3 homepage ), this step is ok and without any mistake (from the command window);



Second, tested the c++ example under the “src/example”, first, test function find_model_example1(), compile, link, this is no warning, and error. However, got stuck when run. Then, after I debug step by step, stuck at the second statement, “context c”;



1, std::cout << "find_model_example1\n";
2, context c;
3, expr x = c.int_const("x");


Keep going with F11 at this statement, it stuck at function “reinterpret_cast” , line 424 in api_context.cpp, keep going with F11, in the constructor of “context” :“context(config_params *, bool)”, function “m_replay_stack” will call function “copy_core”(vector.h), which triggered 0xC00000005 error.



Saturday, March 21, 2015  |  From active questions tagged z3 - Stack Overflow




I'm trying to build Z3 newest version (v4.3.2) on Mac OS X 10.10.2.



Downloading the latest source from http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?he ProjectName=z3&changeSetId=cee7dd39444c9060186df79c2a2c7f8845de415b to follow the command in http://z3.codeplex.com/SourceControl/latest#README.



CXX=clang++ CC=clang python scripts/mk_make.py
cd build
make
sudo make install


The build and installation seems to be OK, however, when I tried to run the example.py, I got this error.



Traceback (most recent call last):
  File "example.py", line 3, in <module>
    x = Real('x')
  File "/Library/Python/2.7/site-packages/z3.py", line 2774, in Real
    ctx = _get_ctx(ctx)
  File "/Library/Python/2.7/site-packages/z3.py", line 210, in _get_ctx
    return main_ctx()
  File "/Library/Python/2.7/site-packages/z3.py", line 205, in main_ctx
    _main_ctx = Context()
  File "/Library/Python/2.7/site-packages/z3.py", line 151, in __init__
    conf = Z3_mk_config()
  File "/Library/Python/2.7/site-packages/z3core.py", line 1036, in Z3_mk_config
    r = lib().Z3_mk_config()
  File "/Library/Python/2.7/site-packages/z3core.py", line 24, in lib
    raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
z3types.Z3Exception: init(Z3_LIBRARY_PATH) must be invoked before using Z3-python
Exception AttributeError: "Context instance has no attribute 'lib'" in <bound method Context.__del__ of <z3.Context instance at 0x227800>> ignored


I added export Z3_LIBRARY_PATH=/Library/Python/2.7/site-packages/ in the environment variables, and tried 64 bit python with arch -x86_64 python example.py to get the same results.



From Using Z3Py With Python 3.3, I tried to copy the libz3.a/dylib/java.dylib files into the /Library/Python/2.7/site-packages, but without success.



What might be wrong?



Saturday, March 21, 2015  |  From active questions tagged z3 - Stack Overflow




Given the following input



(set-option :auto_config false)
(set-option :smt.mbqi false)

(declare-fun len (Int) Int)
(declare-fun idx (Int Int) Int)
(declare-const x Int)

(define-fun FOO () Bool
  (forall ((i Int)) (!
    (implies
      (and (<= 0 i) (< i (len x)))
      (exists ((j Int)) (!
        (implies
          (and (<= 0 j) (< j (len x)))
          (> (idx x j) 0))))))))

(assert FOO)

; (push)
(assert (not FOO))
(check-sat)
; (pop)

; (push)
(assert (not FOO))
(check-sat)
; (pop)


Z3 4.3.2 x64 reports unsat for the first check-sat (as expected), but unknown for the second. If the commented push/pops are uncommented, both check-sats yield unknown.



My guess is that this is either a bug, or a consequence of Z3 switching to incremental mode when it reaches the second check-sat. The latter could also explain why both check-sats yield unknown if push/pop is used because Z3 will (as far as I understand) switch to incremental mode on first push.



Question: Is it a bug or an expected consequence?



Saturday, March 21, 2015  |  From active questions tagged z3 - Stack Overflow




The ctx-solver-simplify tactic only works for bool variables, so how would I deal with variables over finite domain (e.g., which tactics to use)? For example, if z can only take 3 values 0,1,2, then how to simplify Or(z==0,z==1,z==2) to true ?



Also, even for bool expressions, the tactic ctx-solver-simplify doesn't simplify completely. For example:



x,y,z = z3.Bools('x y z')
c1 = z3.And(x==True,y==True,z==True)
c2 = z3.And(x==True,y==True,z==False)
c3 = z3.And(x==True,y==False,z==True)
c4 = z3.And(x==True,y==True,z==False)
z3.Tactic('ctx-solver-simplify')(z3.Or([c1,c2,c3,c4]))
[[Or(And(x, z), And(x == True, y == True, z == False))]]


How do I get something like And(x, Or(z, y)) ?



Thanks !



Saturday, March 21, 2015  |  From active questions tagged z3 - Stack Overflow




Are the numbers returned by (get-info :all-statistics) accumulated across multiple calls to check-sat, and across multiple push-pop scopes? Or are they reset at each check-sat (or at push or pop)?



Phrased differently, if I get statistics at various points during a run of Z3, and if a certain statistics, e.g.quant-instantiations always has the same value, can I then conclude that no quantifier instantiation happened in between getting these statistics?



Friday, March 20, 2015  |  From active questions tagged z3 - Stack Overflow




Given the following input



(set-option :auto_config false)
(set-option :smt.mbqi false)

(declare-fun len (Int) Int)
(declare-fun idx (Int Int) Int)
(declare-const x Int)

(define-fun FOO () Bool
  (forall ((i Int)) (!
    (implies
      (and (<= 0 i) (< i (len x)))
      (exists ((j Int)) (!
        (implies
          (and (<= 0 j) (< j (len x)))
          (> (idx x j) 0))))))))

(assert FOO)

; (push)
(assert (not FOO))
(check-sat)
; (pop)

; (push)
(assert (not FOO))
(check-sat)
; (pop)


Z3 4.3.2 x64 reports unsat for the first check-sat (as expected), but unknown for the second. If the commented push/pops are uncommented, both check-sats yield unknown.



My guess is that this is either a bug, or a consequence of Z3 switching to incremental mode when it reaches the second check-sat. The latter could also explain why both check-sats yield unknown if push/pop is used because Z3 will (as far as I understand) switch to incremental mode on first push.



Question: Is it a bug or an expected consequence?



Friday, March 20, 2015  |  From active questions tagged z3 - Stack Overflow




In Z3, soft constraints can be implemented by placing the actual constraint P on the right-hand side of an implication whose left-hand side is a fresh boolean variable, e.g. assert (=> b1 P). Constraints can then be "switched on" per check-sat by listing bs which are to be considered true, e.g. (check-sat b1).



Question: What happens with such constraints P if their guard variable b is not included in a check-sat? I assume Z3 treats b's value as unknown, and then branches over the implication/over b's value - is that correct?



Background: The background of my question is that I use Z3 in incremental mode (push/pop blocks), and that I check assertions P by (push)(assert (not P))(check-sat)(pop); if the check-sat is unsat then P holds.
I thought about using soft constraints instead, i.e. to replace each such push/pop block by (declare-const b_i Int)(assert (=> b_i P))(check-sat b_i). Each b_i would only be used once. However, if Z3 may branch over all previous b_j, then it sounds as if that might potentially slow down Z3 quite a bit - hence my question.



(P.S.: I am aware of this answer by Leo, which says that soft constraints might also reduce performance because certain optimisations might not be applicable.)



Friday, March 20, 2015  |  From active questions tagged z3 - Stack Overflow




I am trying to evaluate resultant matrix by asserting constraint on matrix multiplication using z3py API. The following method works for matrix addition. Following is the code, which have 3 matrices: x, y, and sol.
sol is the addition of x and y (sol==x+y), I am interested to restrict the values of resultant matrix (sol) to zero, and check which unknown values in "x" and "y" yield resultant matrix to be zero. Following is the list comprehension approach for addition.



from z3 import*

x = [ [Real("x_%s_%s" %(i+1, j+1))  for j in range(2) ] for i in range(2)]
y = [ [Real("y_%s_%s" %(i+1, j+1))  for j in range(2) ] for i in range(2)]
sol = [ [Real("sol_%s_%s" %(i+1, j+1))  for j in range(2) ] for i in range(2)]
addition = [sol[i][j]==x[i][j]+y[i][j]   for i in range(2) for j in range(2) ]


s = Solver()

s.add(addition)
s.add(x[0][0]>=0)
s.add(x[0][1]>=0)
s.add(x[1][0]>=0)
s.add(x[1][1]>=1)

s.add(And(y[0][0]>=0, y[0][0]<=2))
s.add(And(y[0][1]>=0, y[0][0]<=2))
s.add(And(y[1][0]>=0, y[0][0]<=2))
s.add(And(y[1][1]>=0, y[0][0]<=2))

s.add(sol[0][0]==0)
s.add(sol[0][1]==0)
s.add(sol[1][0]==0)
s.add(sol[1][1]==0)


if s.check()==sat:
    m =s.model()
    print  SAT,'\n', m
    result=[[ m.evaluate(sol[i][j]) for i in range (2)] for j in range (2)]
    print result
if (s.check()==unsat):
    print "UNSAT, no model exists"


Now, is there any way in list comprehension through which I can assert matrix multiplication? (sol==x*y)...?



Friday, March 20, 2015  |  From active questions tagged z3 - Stack Overflow




I need to use Z3_parse_smtlib2_string to parse some SMTLIB strings into Z3 using the C++ API, and the use the Z3 C++ API to find the unsat core of this.



I know that there are other ways to find the unsat core as described here and here that are easier and less cumbersome, but I really want to be able to do this using only data structures parsed from strings to Z3. The reason is that I am trying to automate something using Z3.



It is obvious that if I passed this SMTLIB program into Z3, it is UNSAT.



(declare-const p0 Bool)
(assert(= p0 true)) (assert(= p0 false))
(assert (exists ((x Int)) (= 3 x)))


What I want to do, is to be able to get the unsat core programmatically using Z3. What I did was to read each of those lines separately into Z3 and give them a name using solver.add(expr, name), using the program below.



void my_test() {
    context c1;
    solver s(c1);

    std::string declare = "(declare-const p0 Bool)";
    std::string testing = "(assert(= p0 true)) (assert(= p0 false))";
    std::string obvious = "(assert (exists ((x Int)) (= 3 x)))";

    Z3_ast parsed1 = Z3_parse_smtlib2_string(c1, declare.c_str(), 0,0,0,0,0,0);
    expr e1(c1, parsed1);

    Z3_ast parsed2 = Z3_parse_smtlib2_string(c1, testing.c_str(), 0,0,0,0,0,0);
    expr e2(c1, parsed2);
    std::cout << "what: " << e2 << std::endl;

    Z3_ast parsed3 = Z3_parse_smtlib2_string(c1, obvious.c_str(), 0,0,0,0,0,0);
    expr e3(c1, parsed3);

    s.add(e1, "declare");
    s.add(e2, "testing");
    s.add(e3, "obvious");

    if (s.check() == z3::sat) {
        std::cout << "SAT!\n";
        model m = s.get_model();
        std::cout << m << std::endl;
    } else {
        std::cout << "UNSAT!\n";
        expr_vector core = s.unsat_core();
        std::cout << core << "\n";
        std::cout << "size: " << core.size() << "\n";
        for (unsigned i = 0; i < core.size(); i++) {
            std::cout << core[i] << "\n";
        }
    }
}


I expect to get the unsat core to be just declare, since that is clearly false, while the other expressions are clearly valid. However, Z3 gives me this response:



(error "line 1 column 11: unknown constant p0")
(error "line 1 column 31: unknown constant p0")
what: true
SAT!
(define-fun testing () Bool
  true)
(define-fun declare () Bool
  true)
(define-fun obvious () Bool
  true)


Which is clearly wrong, since declare, which references (assert(= p0 true)) (assert(= p0 false)), is SAT! Obviously this should be UNSAT. Also, I do in fact declare p0, but Z3 doesn't seem to know that I declared it already.



Any ideas what I'm doing wrong?



Thursday, March 19, 2015  |  From active questions tagged z3 - Stack Overflow




Given the following input



(set-option :auto_config false)
(set-option :smt.mbqi false)

(declare-fun len (Int) Int)
(declare-fun idx (Int Int) Int)
(declare-const x Int)

(define-fun FOO () Bool
  (forall ((i Int)) (!
    (implies
      (and (<= 0 i) (< i (len x)))
      (exists ((j Int)) (!
        (implies
          (and (<= 0 j) (< j (len x)))
          (> (idx x j) 0))))))))

(assert FOO)

; (push)
(assert (not FOO))
(check-sat)
; (pop)

; (push)
(assert (not FOO))
(check-sat)
; (pop)


Z3 4.3.2 x64 reports unsat for the first check-sat (as expected), but unknown for the second. If the commented push/pops are uncommented, both check-sats yield unknown.



My guess is that this is either a bug, or a consequence of Z3 switching to incremental mode when it reaches the second check-sat. The latter could also explain why both check-sats yield unknown if push/pop is used because Z3 will (as far as I understand) switch to incremental mode on first push.



Question: Is it a bug or an expected consequence?



 active questions tagged z3 - Stack Overflow News Feed 

Last edited Nov 23, 2012 at 4:52 AM by leodemoura, version 13

Comments

No comments yet.