active questions tagged z3 - Stack Overflow News Feed 
Monday, July 28, 2014  |  From active questions tagged z3 - Stack Overflow




I declared an exclusive datatype in z3 as well as a constant and a little assertion:



(declare-datatypes () ((IntOrBool (bpart (b Bool)) (ipart (i Int)))))
(declare-fun iob () (IntOrBool))    
(assert (= true (b iob)))


I get the expected result (bpart true), but with



(assert (= 1 (i iob)))


z3 reports (bpart false).
Does z3 ignore the assertion I gave? If he treats the datatype as a non-exclusive one, how can I force z3 to return an ipart as result?



Sunday, July 27, 2014  |  From active questions tagged z3 - Stack Overflow




I declared an exclusive datatype in z3 as well as a constant and a little assertion:



(declare-datatypes () ((IntOrBool (bpart (b Bool)) (ipart (i Int)))))
(declare-fun iob () (IntOrBool))    
(assert (= true (b iob)))


I get the expected result (bpart true), but with



(assert (= 1 (i iob)))


z3 reports (bpart false).
Does z3 ignore the assertion I gave? If he treats the datatype as a non-exclusive one, how can I force z3 to return an ipart as result?



Thursday, July 24, 2014  |  From active questions tagged z3 - Stack Overflow




I'm using latest z3 master code from Codeplex, tagged as v4.3.1.



I want a function like prove that has a useful return value and does not print. So, I wrote what seemed obvious:



def prove2(claim):
    s = Solver()
    s.add(Not(claim))
    if s.check() == unsat:
        return True, []
    return False, s.model()


However, this code runs dramatically slower than the default prove function.



The code for prove (slimmed) in src/api/python/z3.py is:



def prove(claim, **keywords):
    s = Solver()
    s.set(**keywords)
    s.add(Not(claim))
    if keywords.get('show', False):
        print s
    r = s.check()
    if r == unsat:
        print "proved"
    elif r == unknown:
        print "failed to prove"
        print s.model()
    else:
        print "counterexample"
        print s.model()


When I add s.set() to my code, it is fast and finds the same counterexample.



What is going on here?



  • Does that empty call to s.set() somehow clear some option that is bad in general?
  • .. bad for my particular test?
  • Something else?

I tried to find out what the default solver options were, but str(s) repr(s), s.__dict__, and google didn't really help.



Any advice is appreciated!



Thursday, July 24, 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.



Thursday, July 24, 2014  |  From active questions tagged z3 - Stack Overflow




I am new to Z3. I am confused about what the following declaration of a one dimensional array in Z3 means



(declare-const a1 (Array t1 t2))


Is this a 1-D array of sort (type) t1 or of sort (type) t2?



Is one of t1 or t2 the type of the indexing in array a1?



Could you suggest a reference to understand Z3? I have been following the tutorial on http://z3.codeplex.com/.



Wednesday, July 23, 2014  |  From active questions tagged z3 - Stack Overflow




I am new to Z3. I am confused about what the following declaration of a one dimensional array in Z3 means



(declare-const a1 (Array t1 t2))


Is this a 1-D array of sort (type) t1 or of sort (type) t2?



Is one of t1 or t2 the type of the indexing in array a1?



Could you suggest a reference to understand Z3? I have been following the tutorial on http://z3.codeplex.com/.



Tuesday, July 22, 2014  |  From active questions tagged z3 - Stack Overflow




I'm writing some code to generate constraints for Z3 and then solve for results. I can print out the result by the command Z3_model_to_string(ctx,m) and the result shows x1-> 1 x2->100 where x1 and x2 are both int. My question is how I can save these integer values into C++ variables for future analysis?



Here is the part of code I wrote for Z3



Z3_model m;
context ctx;
Z3_ast fs;
string str = "(declare-const x1 Int) (assert (> x1 0)) (declare-const x2 Int) (assert (not (< x2 100)))" //Generated by some other function
fs  = Z3_parse_smtlib2_string(Z3_context(ctx), str, 0, 0, 0, 0, 0, 0);
Z3_assert_cnstr(Z3_context(ctx), fs);
Z3_lbool result = Z3_check_and_get_model(Z3_context(ctx), &m);
switch (result) {
case Z3_L_FALSE:
    printf("unsat\n");
    break;
case Z3_L_UNDEF:
    printf("unknown\n");
    printf("potential model:\n%s\n", Z3_model_to_string(Z3_context(ctx), m));
    break;
case Z3_L_TRUE:
    printf("sat\n%s\n", Z3_model_to_string(Z3_context(ctx), m));
    break;
}
int num_constants = Z3_get_model_num_constants(Z3_context(ctx), m);
model aaa(ctx,m);
for (i = 0; i< num_constants; i++) {
    z3::expr r = aaa.get_const_interp(aaa.get_func_decl(i));
}


Tuesday, July 22, 2014  |  From active questions tagged z3 - Stack Overflow




The top line of my code 'module Title' is giving me a dual warning "The search directory 'C:\z3-4.3.0-x64\bin\' could not be found". One for my .fs (f#) file and one for some FSC file. I believe FSC is or has something to do with the main project file.



Although I suppose I could try placing a z3 library folder in that specific location, I really don't want to. I have to localize this project for portability. I'm not sure if that file path string is hardcoded or if it was generated from asking my system where things like that are supposed to be installed.



When I search for things like "The search directory" + "could not be found" + visual + studio, I don't get any interesting results.



Tuesday, July 22, 2014  |  From active questions tagged z3 - Stack Overflow




I'm writing some codes by calling Z3 to calculate division but I found the model result is not correct. Basically what I want to do is to the get value of a and b satisfying a/b == 1. So I manually wrote an input file like following to check whether it's my code's problem or Z3's.



(declare-const a Int)
(declare-const b Int)
(assert (= (div a b) 1))
(assert (not (= b 0)))
(check-sat)
(get-model)


Result from this in my machine is a =77 b = 39 instead of some equalized value of a and b. Is this a bug or did I do something wrong?



Tuesday, July 22, 2014  |  From active questions tagged z3 - Stack Overflow




The top line of my code 'module Title' is giving me a dual warning "The search directory 'C:\z3-4.3.0-x64\bin\' could not be found". One for my .fs (f#) file and one for some FSC file. I believe FSC is or has something to do with the main project file.



Although I suppose I could try placing a z3 library folder in that specific location, I really don't want to. I have to localize this project for portability. I'm not sure if that file path string is hardcoded or if it was generated from asking my system where things like that are supposed to be installed.



When I search for things like "The search directory" + "could not be found" + visual + studio, I don't get any interesting results.



Tuesday, July 22, 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.



Saturday, July 19, 2014  |  From active questions tagged z3 - Stack Overflow




I have a rather specific question about using the optimization features of the Z3 opt-branch.



Namely, I can add assertions to the "opt" context using z3_optimize_assert, and those constraints do work.
However, all constraints added to the original z3_context, which was used to create the optimization context are ignored.
Is it a bug or a feature? What is the purpose of having two contexts?



Saturday, July 19, 2014  |  From active questions tagged z3 - Stack Overflow




I have a rather specific question about using the optimization features of the Z3 opt-branch.



Namely, I can add assertions to the "opt" context using z3_optimize_assert, and those constraints do work.
However, all constraints added to the original z3_context, which was used to create the optimization context are ignored.
Is it a bug or a feature? What is the purpose of having two contexts?



Saturday, July 19, 2014  |  From active questions tagged z3 - Stack Overflow




I'm trying to:



  • Test the equivalence of two little pieces of C code
  • Check if a little piece of C code always returns same value.

I'm wondering what existing tools would provide the most support for a project like this. I honestly want as little to do with the nitty gritty SMT/SE/SAT as possible. Pointers to tools, papers, etc would be really helpful—getting a sense of where to start from more experienced people would be amazing.



I don't want to write my own program to bit-blast a bunch of code and then SAT it myself. :(



Thanks for all the help you can offer. Happy to clarify anything.



Saturday, July 19, 2014  |  From active questions tagged z3 - Stack Overflow




We prove the following theorem in Frobenius Algebras



enter image description here



The proof is performed using the following code



;; Frobenius algebra object (A,mu,eta,delta, epsilon)
(declare-sort A)
(declare-sort AA)
(declare-sort A_AA)
(declare-sort AA_A)
(declare-sort I)
(declare-sort I_A)
(declare-sort A_I)
(declare-fun alpha (AA_A) A_AA)
(declare-fun inv_alpha (A_AA) AA_A)
(declare-fun mu (AA) A)
(declare-fun eta (I) A)
(declare-fun mu_id (AA_A) AA)
(declare-fun id_mu (A_AA) AA)
(declare-fun eta_id (I_A) AA)
(declare-fun id_eta (A_I) AA)
(declare-fun lambda (I_A) A)
(declare-fun rho (A_I) A)
(declare-fun delta (A) AA)
(declare-fun delta_id (AA) AA_A)
(declare-fun id_delta (AA) A_AA)
(declare-fun epsilon (A) I)
(declare-fun inv_lambda (A) I_A)
(declare-fun inv_rho (A) A_I)
(declare-fun epsilon_id (AA) I_A)
(declare-fun id_epsilon (AA) A_I)
(declare-fun Id (A) A)
(declare-fun beta1 (A) A_I)
(declare-fun beta2 (A) I_A)
(declare-fun inv_beta1 (A_I) A)
(declare-fun inv_beta2 (I_A) A)
(define-fun gamma ((x I))  AA
            (delta (eta x)))

;; Algebra Object
(assert (forall ((x I_A)) (= (lambda x) (mu (eta_id x)))    ))
(assert (forall ((x A_I) ) (= (rho x) (mu (id_eta x)))    ))
(assert (forall ((x AA_A) ) (= (mu (id_mu (alpha x)) ) (mu (mu_id x))    )   ) )

;; Coalgebra Object
(assert (forall ((x A)) (= (id_delta (delta x)) (alpha (delta_id (delta x)))  )  )   )

(assert (forall ((x A)) (= (epsilon_id (delta x))  (inv_lambda x)  )    ) )  

(assert (forall ((x A)) (= (id_epsilon (delta x))  (inv_rho x)  )    ) )  

;; Frobenius Relation

(assert (forall ((x AA)) (= (mu_id (inv_alpha (id_delta x))) (delta (mu x)))    ) )

(assert (forall ((x AA)) (= (id_mu (alpha (delta_id x))) (delta (mu x)))    ) )

(assert (forall ((x A)) (= (mu (id_eta (beta1 x))) (Id x))   ))

(assert (forall ((x A)) (= (mu (eta_id (beta2 x))) (Id x))   ))

(assert (forall ((x A)) (= (inv_beta1 (id_epsilon (delta x))) (Id x) )   ))

(assert (forall ((x A)) (= (inv_beta2 (epsilon_id (delta x))) (Id x))   ))

(assert (forall ((x A)) (= (Id (Id x)) (Id x))   ) )

(check-sat)
;;(get-model)


;; First Identity

(push)
(assert (forall ((x I_A)) (distinct (id_epsilon (id_mu (alpha (delta_id (eta_id x)) )  ) ) 
                                    (id_epsilon (delta (mu (eta_id x))))     )  ) )
(check-sat)
(pop)


(push)
(assert (forall ((x A )) (distinct (inv_beta1 (id_epsilon (delta (mu (eta_id (beta2 x)))))) 
                                    (Id x)     )  ) )
(check-sat)
(pop)


;; Second Identity
(push)
(assert (forall ((x A_I)) (distinct (epsilon_id (mu_id (inv_alpha (id_delta (id_eta x)) )  ) ) 
                                    (epsilon_id (delta (mu (id_eta x))))     )  ) )
(check-sat)
(pop)


(push)
(assert (forall ((x A)) (distinct (inv_beta2 (epsilon_id (delta (mu (id_eta (beta1 x))))) ) 
                                  (Id x)     )  ) )
(check-sat)
(pop)


And the corresponding output is



sat
unsat
unsat

unsat
unsat


Please run this proof online here



My claim is that this example is the first application of Z3 in Frobenius algebra. Do you agree?



Friday, July 18, 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 satisfied. However, if I switch the order and do (assert (= 0.5 0)) it's not satisfied.



My guess as to what is happening is that if the first parameter is an integer, it casts both of them to as 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?



Friday, July 18, 2014  |  From active questions tagged z3 - Stack Overflow




I found an example of how sets can be encoded withing z3 using the extended array theory (http://rise4fun.com/Z3/DWYC). I would like to use z3 through the python API (Z3py) but I didn't manage to find the right python calls to implement the same example. For instance, how do you define sorts in the python API?
Can anyone provide me with a z3py translation of the given Set definition example?



Thanks!



Thursday, July 17, 2014  |  From active questions tagged z3 - Stack Overflow




We prove the following theorem in Frobenius Algebras



enter image description here



The proof is performed using the following code



;; Frobenius algebra object (A,mu,eta,delta, epsilon)
(declare-sort A)
(declare-sort AA)
(declare-sort A_AA)
(declare-sort AA_A)
(declare-sort I)
(declare-sort I_A)
(declare-sort A_I)
(declare-fun alpha (AA_A) A_AA)
(declare-fun inv_alpha (A_AA) AA_A)
(declare-fun mu (AA) A)
(declare-fun eta (I) A)
(declare-fun mu_id (AA_A) AA)
(declare-fun id_mu (A_AA) AA)
(declare-fun eta_id (I_A) AA)
(declare-fun id_eta (A_I) AA)
(declare-fun lambda (I_A) A)
(declare-fun rho (A_I) A)
(declare-fun delta (A) AA)
(declare-fun delta_id (AA) AA_A)
(declare-fun id_delta (AA) A_AA)
(declare-fun epsilon (A) I)
(declare-fun inv_lambda (A) I_A)
(declare-fun inv_rho (A) A_I)
(declare-fun epsilon_id (AA) I_A)
(declare-fun id_epsilon (AA) A_I)
(define-fun gamma ((x I))  AA
            (delta (eta x)))
;; Algebra Object
(assert (forall ((x I_A)) (= (lambda x) (mu (eta_id x)))    ))
(assert (forall ((x A_I) ) (= (rho x) (mu (id_eta x)))    ))
(assert (forall ((x AA_A) ) (= (mu (id_mu (alpha x)) ) (mu (mu_id x))    )   ) )

;; Coalgebra Object
(assert (forall ((x A)) (= (id_delta (delta x)) (alpha (delta_id (delta x)))  )  )   )

(assert (forall ((x A)) (= (epsilon_id (delta x))  (inv_lambda x)  )    ) )  

(assert (forall ((x A)) (= (id_epsilon (delta x))  (inv_rho x)  )    ) )  

;; Frobenius Relation

(assert (forall ((x AA)) (= (mu_id (inv_alpha (id_delta x))) (delta (mu x)))    ) )

(assert (forall ((x AA)) (= (id_mu (alpha (delta_id x))) (delta (mu x)))    ) )

(check-sat)
;;(get-model)

(push)
(assert (forall ((x AA)) (distinct (mu_id (inv_alpha (id_delta x))) (id_mu (alpha (delta_id x)))) ) )
(check-sat)
(pop)

(push)
(assert (forall ((x I_A)) (distinct (id_epsilon (id_mu (alpha (delta_id (eta_id x)) )  ) ) 
                                    (id_epsilon (delta (mu (eta_id x))))     )  ) )
(check-sat)
(pop)



(push)
(assert (forall ((x A_I)) (distinct (epsilon_id (mu_id (inv_alpha (id_delta (id_eta x)) )  ) ) 
                                    (epsilon_id (delta (mu (id_eta x))))     )  ) )
(check-sat)
(pop)


And the corresponding output is



sat
unsat
unsat
unsat


My claim is that this example is the first application of Z3 in Frobenius algebra. Do you agree?



Thursday, July 17, 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 satisfied. However, if I switch the order and do (assert (= 0.5 0)) it's not satisfied.



My guess as to what is happening is that if the first parameter is an integer, it casts both of them to as 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?



Thursday, July 17, 2014  |  From active questions tagged z3 - Stack Overflow




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



If I do (assert (= 0 0.5)) it will be satisfiable. 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 an integer (rounding 0.5 down to 0) and 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 are a floating-point number, they are both cast to floating-point numbers and compared. Is this really the expected behavior in Z3?



 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.