active questions tagged z3 - Stack Overflow News Feed 
Thursday, November 20, 2014  |  From active questions tagged z3 - Stack Overflow




In Non-linear arithmetic and uninterpreted functions, Leonardo de Moura states that the qfnra-nlsat tactic hasn't been fully integrated with the rest of Z3 yet. I thought that the situation has changed in two years, but apparently the integration is still not very complete.



In the example below, I use datatypes purely for "software engineering" purposes: to organize my data into records. Even though there are no uninterpreted functions, Z3 still fails to give me a solution:



(declare-datatypes () (
    (Point (point (point-x Real) (point-y Real)))
    (Line (line (line-a Real) (line-b Real) (line-c Real)))))

(define-fun point-line-subst ((p Point) (l Line)) Real
    (+ (* (line-a l) (point-x p)) (* (line-b l) (point-y p)) (line-c l)))

(declare-const p Point)
(declare-const l Line)

(assert (> (point-y p) 20.0))
(assert (= 0.0 (point-line-subst p l)))

(check-sat-using qfnra-nlsat)
(get-model)





> unknown
(model 
)


However, if I manually inline all the functions, Z3 finds a model instantly:



(declare-const x Real)
(declare-const y Real)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)

(assert (> y 20.0))
(assert (= 0.0 (+ (* a x) (* b y) c)))

(check-sat-using qfnra-nlsat)
(get-model)





> sat
(model 
  (define-fun y () Real
    21.0)
  (define-fun a () Real
    0.0)
  (define-fun x () Real
    0.0)
  (define-fun b () Real
    0.0)
  (define-fun c () Real
    0.0)
)


My question is, is there a way to perform such an inlining automatically? I'm fine with either one of these workflows:



  1. Launch Z3 with a tactic that says "Inline first, then apply qfnra-nlsat. I haven't found a way to do so, but maybe I wasn't looking well enough.
  2. Launch Z3 using some version of simplify to do the inlining. Launch Z3 the second time on the result of the first invocation (the inlined version).

In other words, how to make qfnra-nlsat work with tuples?



Thank you!



Thursday, November 20, 2014  |  From active questions tagged z3 - Stack Overflow




I noticed some strange behavior with Z3 4.3.1 when working with .smt2 files.



If I do (assert (= 0 0.5)) it will be satisfiable. However, if I switch the order and do (assert (= 0.5 0)) it's not satisfiable.



My guess as to what is happening is that if the first parameter is an integer, it casts both of them to integers (rounding 0.5 down to 0), then does the comparison. If I change "0" to "0.0" it works as expected. This is in contrast to most programming languages I've worked with where if either of the parameters is a floating-point number, they are both cast to floating-point numbers and compared. Is this really the expected behavior in Z3?



Wednesday, November 19, 2014  |  From active questions tagged z3 - Stack Overflow




I have a model which aiming to represent the following representation:



enter image description here



The model below shows2 events and 2 objects. I want to write a constraints to say that each event must associate to only one object. I've tried the following code but it seems the constraint not working when I tried to test it at the end. It should give me unsat when I assign 2 events to the same object But it give sat.
My z3 code logically seem ok but when I test it it doesn't give me a correct solution.



(declare-sort Object )
(declare-sort Associations)
(declare-sort Event)

(declare-fun O1 () Object)
(declare-fun O2 () Object)
(assert( not( = O1 O2)
(declare-const e1  Event)
(declare-const e2  Event)

(declare-const connect Associations)

(declare-fun event-Object (Event Object) Associations)
 (assert 
   (forall ((ev1 Event)(n Object) (m Object) (a Associations)) 
  (=> 
   (and
   (= (event-Object ev1 n) a)
   (= (event-Object ev1 m) a)
   (not (= n m))
    (= a connect)
   )
   (or
   (= (event-Object ev1 n) a)
   (= (event-Object ev1 m) a))
  )
 )
)

(assert (= (event-Object e1 O1)connect))
(assert (= (event-Object e1 O1)connect))

(check-sat)
(get-model)


This should give me unsat because $e1$ is in relation with $O1$ and $O2$ in the same time which it shouldn't according to the function above but it always gives sat :(. Any one can help?



Wednesday, November 19, 2014  |  From active questions tagged z3 - Stack Overflow




i'm trying to unlock bootloader of my xperia z3 following sony's site instructions.



After connecting the phone to the pc in fastboot mode (blue light on) i open the command window in the platform-tools folder as instructed. Then i type fastboot devices but nothing happens, and if i try to enter my unlock code i get "waiting for device" forever.



I tried to point windows to the right driver, through device manager, but when it tries to install the driver i get "hash for the file is not available in the specified catalogue. File is probably damaged"



Of course i downloaded the file from sony's site and replaced with the original one in usb_driver folder.



Anyone can help me?



Tuesday, November 18, 2014  |  From active questions tagged z3 - Stack Overflow




In Non-linear arithmetic and uninterpreted functions, Leonardo de Moura states that the qfnra-nlsat tactic hasn't been fully integrated with the rest of Z3 yet. I thought that the situation has changed in two years, but apparently the integration is still not very complete.



In the example below, I use datatypes purely for "software engineering" purposes: to organize my data into records. Even though there are no uninterpreted functions, Z3 still fails to give me a solution:



(declare-datatypes () (
    (Point (point (point-x Real) (point-y Real)))
    (Line (line (line-a Real) (line-b Real) (line-c Real)))))

(define-fun point-line-subst ((p Point) (l Line)) Real
    (+ (* (line-a l) (point-x p)) (* (line-b l) (point-y p)) (line-c l)))

(declare-const p Point)
(declare-const l Line)

(assert (> (point-y p) 20.0))
(assert (= 0.0 (point-line-subst p l)))

(check-sat-using qfnra-nlsat)
(get-model)





> unknown
(model 
)


However, if I manually inline all the functions, Z3 finds a model instantly:



(declare-datatypes () (
    (Point (point (point-x Real) (point-y Real)))
    (Line (line (line-a Real) (line-b Real) (line-c Real)))))

(define-fun point-line-subst ((p Point) (l Line)) Real
    (+ (* (line-a l) (point-x p)) (* (line-b l) (point-y p)) (line-c l)))

(declare-const x Real)
(declare-const y Real)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)

(assert (> y 20.0))
(assert (= 0.0 (+ (* a x) (* b y) c)))

(check-sat-using qfnra-nlsat)
(get-model)





> sat
(model 
  (define-fun y () Real
    21.0)
  (define-fun a () Real
    0.0)
  (define-fun x () Real
    0.0)
  (define-fun b () Real
    0.0)
  (define-fun c () Real
    0.0)
)


My question is, is there a way to perform such an inlining automatically? I'm fine with either one of these workflows:



  1. Launch Z3 with a tactic that says "Inline first, then apply qfnra-nlsat. I haven't found a way to do so, but maybe I wasn't looking well enough.
  2. Launch Z3 using some version of simplify to do the inlining. Launch Z3 the second time on the result of the first invocation (the inlined version).

In other words, how to make qfnra-nlsat work with tuples?



Thank you!



Tuesday, November 18, 2014  |  From active questions tagged z3 - Stack Overflow




In Non-linear arithmetic and uninterpreted functions, Leonardo de Moura states that the qfnra-nlsat tactic hasn't been fully integrated with the rest of Z3 yet. I thought that the situation has changed in two years, but apparently the integration is still not very complete.



In the example below, I use datatypes purely for "software engineering" purposes: to organize my data into records. Even though there are no uninterpreted functions, Z3 still fails to give me a solution:



(declare-datatypes () (
    (Point (point (point-x Real) (point-y Real)))
    (Line (line (line-a Real) (line-b Real) (line-c Real)))))

(define-fun point-line-subst ((p Point) (l Line)) Real
    (+ (* (line-a l) (point-x p)) (* (line-b l) (point-y p)) (line-c l)))

(declare-const p Point)
(declare-const l Line)

(assert (> (point-y p) 20.0))
(assert (= 0.0 (point-line-subst p l)))

(check-sat-using qfnra-nlsat)
(get-model)





> unknown
(model 
)


However, if I manually inline all the functions, Z3 finds a model instantly:



(declare-datatypes () (
    (Point (point (point-x Real) (point-y Real)))
    (Line (line (line-a Real) (line-b Real) (line-c Real)))))

(define-fun point-line-subst ((p Point) (l Line)) Real
    (+ (* (line-a l) (point-x p)) (* (line-b l) (point-y p)) (line-c l)))

(declare-const x Real)
(declare-const y Real)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)

(assert (> y 20.0))
(assert (= 0.0 (+ (* a x) (* b y) c)))

(check-sat-using qfnra-nlsat)
(get-model)





> sat
(model 
  (define-fun y () Real
    21.0)
  (define-fun a () Real
    0.0)
  (define-fun x () Real
    0.0)
  (define-fun b () Real
    0.0)
  (define-fun c () Real
    0.0)
)


My question is, is there a way to perform such an inlining automatically? I'm fine with either one of these workflows:



  1. Launch Z3 with a tactic that says "Inline first, then apply qfnra-nlsat. I haven't found a way to do so, but maybe I wasn't looking well enough.
  2. Launch Z3 using some version of simplify to do the inlining. Launch Z3 the second time on the result of the first invocation (the inlined version).

Thank you!



Tuesday, November 18, 2014  |  From active questions tagged z3 - Stack Overflow




I'm trying to pose queries to Z3 that involve uninterpreted functions (always with domain int), reals, and quantifiers. I know that adding quantifiers will often lead to unknown results, but I was surprised at how quickly this happened:



(declare-fun $in1 (Int) Real)
(declare-fun $in2 (Int) Real)
(assert (< ($in1 0) ($in2 0)))
(assert (forall (($$out Real))
  (not (and (< ($in1 0) $$out) (< $$out ($in2 0))))))
(check-sat)


This query should result in unsat but instead times out with unknown. Is there a flag or option I could set which might lead Z3 to solve this query? I'd hate to have to go through and flatten all my uninterpreted functions into scalars, but that is something I could do.



Tuesday, November 18, 2014  |  From active questions tagged z3 - Stack Overflow




The arithmetic solver of Z3 is developed based on DPLL(T) and Simplex (described in this paper). And I do not understand how Z3 perform the backtrack when a conflict explanation is generated. I give an example:



The linear arithmetic formula is:



(2x1+x2≤200 OR 3x1+x2≤250) AND (2x1+x2+x3≤200 OR 4x1+2x2+x3≤400)
AND x1≥50 AND x2≥50 AND x3≥60



after asserting 2x1+x2≤200, 2x1+x2+x3≤200, x1≥50, x2≥50 and x3≥60 successively, it yields a conflict explanation set {2x1+x2+x3≤200, x1≥50, x2≥50, x3≥60}.



My question is, how then the backtrack is performed when this conflict set is generated?



Monday, November 17, 2014  |  From active questions tagged z3 - Stack Overflow




I have narrowed down my problem in the following code. I am trying to convert a string into equivalent z3 expression. The problem is that when the variable name is big, the 'eval' puts extra \n in between the expression but if I use a smaller variable name the extra \n is not there. I need to have a bigger variable name because that is not under my control. Please suggest how can I make the code working correctly with bigger variable names



EXTRA \n PRODUCING CODE



from z3 import BitVec, Solver #@UnresolvedImport

z3sig_dict = {}
z3sig_dict['v__DOT__process_1_reg3'] = {"z3name":BitVec('v__DOT__process_1_reg3', 32), "bits":32}
z3sig_dict['v__DOT__process_1_reg3_1'] = {"z3name":BitVec('v__DOT__process_1_reg3_1', 32), "bits":32}
string = "(z3sig_dict['v__DOT__process_1_reg3']['z3name'] == (8 + (z3sig_dict['v__DOT__process_1_reg3_1']['z3name'] % 0x20000000)))"
s = Solver()
print(string)
clause = eval(string)
print(str(clause))
s.add(clause)


The output of this code is



(z3sig_dict['v__DOT__process_1_reg3']['z3name'] == (8 + (z3sig_dict['v__DOT__process_1_reg3_1']['z3name'] % 0x20000000)))
v__DOT__process_1_reg3 ==
8 + v__DOT__process_1_reg3_1%536870912


CORRECTLY WORKING CODE



from z3 import BitVec, Solver #@UnresolvedImport

z3sig_dict = {}
z3sig_dict['reg3'] = {"z3name":BitVec('reg3', 32), "bits":32}
z3sig_dict['reg3_1'] = {"z3name":BitVec('reg3_1', 32), "bits":32}
string = "(z3sig_dict['reg3']['z3name'] == (8 + (z3sig_dict['reg3_1']['z3name'] % 0x20000000)))"
s = Solver()
print(string)
clause = eval(string)
print(str(clause))
s.add(clause)


The output of this code is



(z3sig_dict['reg3']['z3name'] == (8 + (z3sig_dict['reg3_1']['z3name'] % 0x20000000)))
reg3 == 8 + reg3_1%536870912


SOME OBSERVATIONS



If I reduce the % 0x20000000 to % 0x2000, then also the code works correctly, but incorrectly if I add one more zero i.e 0x20000



Monday, November 17, 2014  |  From active questions tagged z3 - Stack Overflow




Z3 has a prove() method, that can prove the equivalence of two formulas.



However, I cannot find technical documentation of this prove() method. What is the definition of "equivalence" that prove() is using behind the scene ? Is that the "partial equivalence" (proposed in the "Regression Verification" paper), or something more powerful ?



A reminder, the "partial equivalence" guarantees that two formulas are equivalent if given the same input, they produce the same output.



Monday, November 17, 2014  |  From active questions tagged z3 - Stack Overflow




I'm trying out some of the examples of a Z3 tutorial that involve recursive functions. I've tried out the following example.



  1. Fibonacci (Section 8.3)
  2. IsNat (Section 8.3)
  3. Inductive (Section 10.5)

Z3 times out on all of the above examples. But, the tutorial seems to imply that only Inductive is non-terminating.



Can Z3 check the satisfiability of formulas that contain recursive functions or it cannot handle any inductive facts?



Sunday, November 16, 2014  |  From active questions tagged z3 - Stack Overflow




I want to the solution got back from z3 without simplification using let statements.



For example if I give the following:



(declare-const x Int)
  (elim-quantifiers (exists ((x.1 Int)) 
    (and (or (and (= (- x.1 2) 0) (<= (- x.1 9) 0)) 
             (and (or (= (- x.1 2) 0) (and (<= (- x.1 4) 0) 
                                      (and (<= (- 4 x.1) 0) 
                                           (<= (- x.1 11) 0)))) (<= (- x.1 9) 0))) (= (- (+ x.1 2) x) 0))))


I get back the solution as:



(let ((a!1 (and (or (and (<= x 4) (>= x 4)) (and (<= x 6) (>= x 6) (<= x 13)))
                (<= x 11))))
    (or (and (<= x 4) (>= x 4) (<= x 11)) a!1))


Is there a way to tell Z3 not to extract some complex expressions into a let statement ? It will be easier for me to parse the result if I get the answer flat without let statement.



Saturday, November 15, 2014  |  From active questions tagged z3 - Stack Overflow




I am wondering if z3 supports associative arrays (aka maps)? If not is there a simple way to model such data structures using the current version of z3?



Thursday, November 13, 2014  |  From active questions tagged z3 - Stack Overflow




I'm trying to find the minimal value of the Parabola y=(x+2)**2-3, apparently, the answer should be y==-3, when x ==-2.
But z3 gives the answer [x = 0, y = 1], which doesn't meet the ForAll assertion.



Am I assuming wrongly with something?



Here is the python code:



from z3 import *

x, y, z = Reals('x y z')

print(Tactic('qe').apply(And(y == (x + 2) ** 2 - 3,
                             ForAll([z], y <= (z + 2) ** 2 - 3))))

solve(y == x * x + 4 * x +1,
      ForAll([z], y <= z * z + 4 * z +1))


And the result:



[[y == (x + 2)**2 - 3, True]]
[x = 0, y = 1]


The result shows that 'qe' tactic eliminated that ForAll assertion into True, although it's NOT always true.
Is that the reason that solver gives a wrong answer?
What should I code to find the minimal (or maximal) value of such an expression?



BTW, the Z3 version is 4.3.2 for Mac.



Thursday, November 13, 2014  |  From active questions tagged z3 - Stack Overflow




I'm trying to find the minimal value of the Parabola y=(x+2)**2-3, apparently, the answer should be y==-3, when x ==-2.
But z3 gives the answer [x = 0, y = 1], which doesn't meet the ForAll assertion.



Am I assuming wrongly with something?



Here is the python code:



from z3 import *

x, y, z = Reals('x y z')

print(Tactic('qe').apply(And(y == (x + 2) ** 2 - 3,
                             ForAll([z], y <= (z + 2) ** 2 - 3))))

solve(y == x * x + 4 * x +1,
      ForAll([z], y <= z * z + 4 * z +1))


And the result:



[[y == (x + 2)**2 - 3, True]]
[x = 0, y = 1]


The result shows that 'qe' tactic eliminated that ForAll assertion into True, although it's NOT always true.
Is that the reason that solver gives a wrong answer?
What should I code to find the minimal (or maximal) value of such an expression?



BTW, the Z3 version is 4.3.2 for Mac.



Thursday, November 13, 2014  |  From active questions tagged z3 - Stack Overflow




I am trying to obtain a non-trivial model of an idempotent quasigroup using Z3 with the following code



(set-logic AUFNIRA)
(set-option :macro-finder true)
(set-option :mbqi true)
(set-option :pull-nested-quantifiers true)

(declare-sort S 0)
(declare-fun prod (S S) S)
(declare-fun left (S S) S)
(declare-fun right (S S) S)

(assert (forall ((x S) (y S))
                (= (prod (left x y) y) x)))

(assert (forall ((x S) (y S))
                (= (prod x (right x y) ) y)))

(assert (forall ((x S) (y S))
                (= (left (prod x y) y ) x)))

(assert (forall ((x S) (y S))
                (= (right x (prod x y)) y)))
(assert (forall ((x S)) (= (prod x x) x)   ))

(check-sat)
(get-model)


but I am obtaining only a trivial model:



sat
(model
  ;; universe for S:
  ;;   S!val!0
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun S!val!0 () S)
  ;; cardinality constraint:
  (forall ((x S)) (= x S!val!0))
  ;; -----------
  (define-fun elem!3 () S
    S!val!0)
  (define-fun elem!2 () S
    S!val!0)
  (define-fun elem!0 () S
    S!val!0)
  (define-fun elem!1 () S
    S!val!0)
  (define-fun left ((x!1 S) (x!2 S)) S
    S!val!0)
  (define-fun right ((x!1 S) (x!2 S)) S
    S!val!0)
  (define-fun prod ((x!1 S) (x!2 S)) S
    x!1)
)


Run this example online here



Please let me know how we can obtain a non-trivial model. Many thanks.



Thursday, November 13, 2014  |  From active questions tagged z3 - Stack Overflow




I thought I read somewhere that Z3 has some option for returning the model with the "least" value eg given something like



x >= 2


Z3 would return 2. I could swear that I saw some reference to this recently, but I am unable to find it now. Can anyone confirm this?



Thursday, November 13, 2014  |  From active questions tagged z3 - Stack Overflow




I've just start learning z3 solver. I've seen some puzzles solved by z3 i.e sudoku and Eight Queens. I'm just wondering if any one solved River crossing problem in z3. z3 seems very good in problem solving.



Regards



Thursday, November 13, 2014  |  From active questions tagged z3 - Stack Overflow




Dynamic load of a dll statically linked to libz3.dll fails, GetlastError after failed LoadLibrary returns "Invalid access to memory location" error. Is it possible to dynamically load libz3.dll?



Wednesday, November 12, 2014  |  From active questions tagged z3 - Stack Overflow




I want to create SMT model that connect three elements together as the following figure shows:



enter image description here



i've wrote the below code but I couldn't write a general assert to say that there is no relation $next$ between the object and event and there is no relation $first$ or $second$ between events. the following asserts is just for specific case but I need something for all cases.



(assert (= (event-object1 e1 o1)first))
(assert (not(= (event-object1 e1 o1)next)))
(assert (not(= (event-object1 e1 o1)second)))


also I'd like to write an assert to say that the relation between object and events either first or second but I'm not sure it the following assert is correct.



(assert (forall ((e Event)(O Object1)(a Associations)) (=> (= e O a) (or (= (event-object1 e O)      first) (= (event-object1 e O) second)))))    


here is the code:



(declare-sort Object1 )
(declare-sort Associations)
(declare-sort Event)

(declare-const first Associations)
(declare-const second Associations)
(declare-const next Associations)

(declare-fun event-object1 (Event Object1) Associations)
(assert (forall ((e Event)(O Object1)(a Associations)) (=> (= e O a) (or (= (event-object1 e O)     first) (= (event-object1 e O) second)))))


(declare-fun event-event (Event Event) Associations)
(assert (forall ((e1 Event)(e2 Event)(a Associations)) (=> (= e1 e2 a) (= (event-event e1 e2) next))))

(declare-const o1 Object1)
(declare-const e1  Event)
(declare-const e2  Event)

(assert (= (event-object1 e1 o1)first))
(assert (not(= (event-object1 e1 o1)next)))
(assert (not(= (event-object1 e1 o1)second)))

(assert (= (event-object1 e2 o1)second))
(assert (not(= (event-object1 e2 o1)next)))
(assert (not(= (event-object1 e2 o1)first)))

(assert (= (event-event e1 e2)next))
(assert (not(= (event-event e1 e2)first)))
(assert (not(= (event-event e1 e2)second)))

(check-sat)
(get-model)


 active questions tagged z3 - Stack Overflow News Feed 

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

Comments

No comments yet.