active questions tagged z3 - Stack Overflow News Feed 
Wednesday, October 01, 2014  |  From active questions tagged z3 - Stack Overflow




I'm trying to use Z3 to solve equations involving unknown projection functions, to find a valid interpretation of the functions that satisfy the equation. So for example for the equation: snd . f = g . fst a valid interpretation would be f = \(x,y) -> (y,x) and g = id. I know that Z3 isn't higher order so I've been trying to encode the problem in first order form. So for example for f = g.fst I use:



(declare-datatypes (T) ((Tree (leaf (value T)) (node (children TreeList)))
                        (TreeList nil (cons (head Tree) (tail TreeList)))))
(define-fun fst ((x (Tree Int))) (Tree Int) (head (children x)))
(define-fun snd ((x (Tree Int))) (Tree Int) (head (tail (children x))))
(declare-fun f ((Tree Int)) (Tree Int))
(declare-fun g ((Tree Int)) (Tree Int))
(assert (forall ((x (Tree Int))) (= (f x) (g (fst x)))))
(check-sat)
(get-model)


Which sort of works returning:



(define-fun g ((x!1 (Tree Int))) (Tree Int)
  (leaf 0))
(define-fun f ((x!1 (Tree Int))) (Tree Int)
  (g (head (children x!1))))


However for snd . f = g . fst (I've simplified trees to pairs to try and help):



(declare-datatypes (T) ((Pair (leaf (value T)) (pair (fst Pair) (snd Pair)))))
(declare-fun f ((Pair Int)) (Pair Int))
(declare-fun g ((Pair Int)) (Pair Int))
(assert (forall ((x (Pair Int))) (= (snd (f x)) (g (fst x)))))


I get unknown.



I've also tried to encode a similar problem without the ADT just using booleans or ints as parameters, but then the model just assigns constant values to the functions. I've also tried to define a simple ADT for function constants, the identity function, and pairwise and sequential composition, and then define an "equals" function that can simplify expressions like f.id = f, but this either involves a recursive function like:



(declare-datatypes () (
  (Fun id 
       (fun (funnum Int))
       (seq (after Fun) (before Fun))
       (pair (fst Fun) (snd Fun)) )))
(define-fun eq ((x Fun) (y Fun)) Bool (or
    (= x y)
      (eq x (seq y id)) ; id neutral for seq
      (eq x (seq id y))
      (eq y (seq x id))
      (eq y (seq id x))))
(declare-const f Fun)
(declare-const g Fun)
(assert (eq f (seq id g)))
(check-sat)
(get-model)


Which is obviously invalid. Or if I use an uninterpretted function, it makes "eq" a constant function i.e.



(declare-fun eq (Fun Fun) Bool)
(assert (forall ((x Fun) (y Fun))  ; semantic equality
    (= (eq x y) (or
      (= x y) ; syntactic eq
      (eq x (seq y id)) ; id neutral for seq
      (eq x (seq id y))
      (eq y (seq x id))
      (eq y (seq id x))
    ))
))
=>
(define-fun eq ((x!1 Fun) (x!2 Fun)) Bool
    true)


And similarly with equations involving functions with type Int -> Int, this returns constant functions for f and g:



(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (forall ((x Int)) (= (+ (f x) 1) (+ (g x) 2)) ))


and adding these times out:



(assert (forall ((x Int) (y Int)) (=> 
  (not (= x y)) 
  (not (= (g x) (g y))))))
(assert (forall ((x Int) (y Int)) (=> 
  (not (= x y)) 
  (not (= (f x) (f y))))))


Any ideas how I can get this sort of thing to work?



Many thanks!



Monday, September 29, 2014  |  From active questions tagged z3 - Stack Overflow




The following code leads to a SIGSEV



Map<String, String> settings = new HashMap<String, String>();
settings.put("model", "true");
Context z3_ctx = new Context(settings);
BitVecExpr bv_left = z3_ctx.mkBV(10, 32);
IntExpr ret_val = z3_ctx.mkBV2Int(bv_left, true); 


If signed==false, then no problem happens.



I am running Z3 on a MAC OS X.



Any ideas?



Sunday, September 28, 2014  |  From active questions tagged z3 - Stack Overflow




Given the following SMT2 script:



(set-option :produce-proofs true)
(set-logic AUFLIRA)
(declare-sort Complex$ 0)
(declare-fun r$ () Real)
(declare-fun s$ () Complex$)
(declare-fun re$ (Complex$) Real)
(declare-fun norm$ (Complex$) Real)
(assert (! (not (=> (and (forall ((?v0 Complex$)) (<= (ite (< (re$ ?v0) 0.0) (- (re$ ?v0)) (re$ ?v0)) (norm$ ?v0))) (<= (norm$ s$) r$)) (<= (ite (< (re$ s$) 0.0) (- (re$ s$)) (re$ s$)) (+ r$ 1.0)))) :named a0))
(check-sat)
(get-proof)


Z3 (unstable version) produces a proof that contains a Skolem function "norm$0". This function is introduced in a rewrite step:



(ALL v0. (if 0 <= Re v0 then Re v0 else - 1 * Re v0) <= cmod v0) =
((ALL v0. cmod v0 = (if 0 <= Re v0 then Re v0 else - 1 * Re v0) + norm_0 v0) & (ALL v0. 0 <= norm_0 v0))


Can this behavior be suppressed by a command-line switch? That is, is there an option such that Z3 produces a proof without such a Skolem function? This should, in principle, be possible, as Z3 version 3.2 finds a proof that does not require a Skolem function.



Friday, September 26, 2014  |  From active questions tagged z3 - Stack Overflow




I'm currently playing with the maximization API for Z3 (opt branch), and I've stumbled upon a following bug:



Whenever I give it any unbounded problem, it simply returns me OPT and gives zero in the resulting model (e.g. maximize Real('x') with no constraints on the model).



Python example:



from z3 import *

context = main_ctx()
x = Real('x')
optimize_context = Z3_mk_optimize(context.ctx)
Z3_optimize_assert(context.ctx, optimize_context, (x >= 0).ast)

Z3_optimize_maximize(context.ctx, optimize_context, x.ast)
out = Z3_optimize_check(context.ctx, optimize_context)
print out


And I get the value of out to be 1 (OPT), while it seems like it should be -1.



Friday, September 26, 2014  |  From active questions tagged z3 - Stack Overflow




While adding constraints in my code, I found I have to add identical constraints into an expression vector for multiple times. Is there any API to detect whether two expressions are exactly the same so that I can remove redundant expressions?



Friday, September 26, 2014  |  From active questions tagged z3 - Stack Overflow




As previously asked Z3 can not provide a model for recursive functions. However, is it possible to tell Z3 (preferably via the Java API) that a model without a definition for recursive functions is sufficient (or indeed choose the functions I am interested in, essentially I do not need a model for non-constant functions)? Obviously, that might lead to queries that return sat although some functions do not have a model. Basically, the user then has to ensure that these functions do have some model.
However, I would assume this is not really realizable the way Z3 or SMT solvers work, i.e., I would assume Z3 needs a (partial) model of recursive functions to evalutate expressions.



Friday, September 26, 2014  |  From active questions tagged z3 - Stack Overflow




I'm using Z3 C++ API (Version 4.3.1) and I want to extract variables of a formula (An object of type expr). I've found a similar question but it is in Z3py. I am wonder if there is a method in Z3 C/C++ API to extract variables from expr object. Thanks!



For example (some details omitted):



    expr fs = implies(x + y == 0, z * x < 15);
    std::vector<expr> varlist = get_vars(fs);


Then varlist should contain x,y,z.



Friday, September 26, 2014  |  From active questions tagged z3 - Stack Overflow




I previously used Z3's API to define an enumerated type like so



let T = ctx.MkEnumSort("T", [| "a"; "b"; "c"|])


which enumerates the elements of a type T as being "a" "b" and "c" (and nothing else). However I am now trying to do something similar but via SMT-LIB rather than the API and I am running into a problem of Z3 complaining about quantifiers. The program I am using (Boogie) generates the following smt



...
(declare-sort T@T 0)
(declare-fun a() T@T)
(declare-fun b() T@T)
(declare-fun c() T@T)
(assert (forall ((x T@T) ) 
    (! (or
          (= x a)
          (= x b)
          (= x c)
       )
       :qid |gen.28:15|
       :skolemid |1|
     )))
...


The assertion is the type closure axiom that asserts that the type has no other members. But when I send this (along with other stuff) to Z3, after thinking about it a bit, returns



WARNING: relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5
unknown
(:reason-unknown (incomplete quantifiers))


Notes: 1. I have MBQI turned on. 2. Boogie has an option called "z3types" but it doesn't seem to make any difference



What is the SMT-LIB equivalent of the MkEnumSort API call?



thanks



P.S. I have tried with RELEVANCY set to both 1 and 2 and I still get the warning about relevancy (CASE_SPLIT is set to 3)



Friday, September 26, 2014  |  From active questions tagged z3 - Stack Overflow




I am using Z3 as SAT solver for a tough satisfiability problem encoded in CNF/DIMACS format.



Would it make sense to randomize the input in order to increase the chance to find a solution:



  • Shuffle the order of CNF clauses
  • Sort/shuffle the numbering of input
    variables

Measurements (100 test runs per solver and sorting mode) for a smaller problem with Z3, Cryptominisat and Clasp:



enter image description here



For Z3, sorting/randomization does not look promising for my example which is probably not representative.



I have not found a random seed commandline parameter which influences the SAT module of Z3.
Parameter "random_seed" only seems to control the SMT solver.



Friday, September 26, 2014  |  From active questions tagged z3 - Stack Overflow




I am using Z3py and trying to get the set of all the variables in any constraint in a Solver. I can call Solver.assertions() to get an ASTVector, then loop over this vector and get objects of type BoolRef, for example, but then I'm stuck. How can I recursively iterate over an assertion, a BoolRef instance for example, to get the individual variables?



Friday, September 26, 2014  |  From active questions tagged z3 - Stack Overflow




The problem in relational algebra REL052+1.p reads



File     : REL052+1 : TPTP v6.1.0. Released v4.0.0.
% Domain   : Relation Algebra
% Problem  : Non-discrete dense ordering


Using TPTP syntax with fof the corresponding code is



fof(f01,axiom,(
    ! [A] : o(A,A) )).

fof(f02,axiom,(
    ! [A,B] :
      ( ( A != B
        & o(A,B) )
     => ~ o(B,A) ) )).

fof(f03,axiom,(
    ! [A,B,C] :
      ( ( o(A,B)
        & o(B,C) )
     => o(A,C) ) )).

fof(f04,axiom,(
    ! [A,B] :
      ( ( A != B
        & o(A,B) )
     => ( o(A,f(A,B))
        & o(f(A,B),B) ) ) )).

fof(f05,axiom,(
    ! [A,B] :
      ( f(A,B) != A
      & f(A,B) != B ) )).

fof(f06,axiom,(
    ? [A,B] :
      ( o(A,B)
      & A != B ) )).


As you can see in TPTP all ATPs are not able to prove such problem.



This theorem was proved with Z3 using the following SMT-LIB



(declare-sort S)
(declare-fun o (S S) Bool)
(declare-fun f (S S) S)
(assert (forall ((A S)) (o A A) ))
(assert (forall ((A S) (B S)) (implies (and (distinct A B) (o A B)) 
                                       (not (o B A)))   ) )
(assert (forall ((A S) (B S) (C S)) (implies (and (o A B) (o B C)) 
                                             (o A C))   ) )
(assert (forall ((A S) (B S)) (implies (and (distinct A B) (o A B)) 
                                       (and (o A (f A B)) (o (f A B) B)))   ) )
(declare-fun B () S)
(assert (forall ((A S)) (and (distinct (f A B) A) 
                                   (distinct (f A B) B))    ) )
(assert (exists ((X S) (Y S)) (and (o X Y) (distinct X Y))) )

(check-sat)


and the corresponding output is



sat


My question is: The proof with Z3 is correct?



Friday, September 26, 2014  |  From active questions tagged z3 - Stack Overflow




I'm currently playing with the maximization API for Z3 (opt branch), and I've stumbled upon a following bug:



Whenever I give it any unbounded problem, it simply returns me OPT and gives zero in the resulting model (e.g. maximize Real('x') with no constraints on the model).



Python example:



from z3 import *

context = main_ctx()
x = Real('x')
optimize_context = Z3_mk_optimize(context.ctx)
Z3_optimize_assert(context.ctx, optimize_context, (x >= 0).ast)

Z3_optimize_maximize(context.ctx, optimize_context, x.ast)
out = Z3_optimize_check(context.ctx, optimize_context)
print out


And I get the value of out to be 1 (OPT), while it seems like it should be -1.



Thursday, September 25, 2014  |  From active questions tagged z3 - Stack Overflow




I am trying to devise ways to improve performance of z3 on my problems. I am aware of the the CAV'06 paper and the tech report . Do relevant parts of z3 v4.3.1 differ from what is described in these documents, and if so in what ways? Also, what is the strategy followed by default in z3 for deciding when to check for consistency in Linear Real Arithmetic, of the theory atoms corresponding to the decided (and propagated) propositional literals?



Wednesday, September 24, 2014  |  From active questions tagged z3 - Stack Overflow




I was trying to represent a real number with two integer numbers as using them as the numerator and the denominator of the real number. I wrote the following program:



(declare-const a Int)
(declare-const b Int)
(declare-const f Real)

(assert (= f (/ a b)))
(assert (= f 0.5))
(assert (> b 2))
(assert (> b a))

(check-sat)
(get-model)


The program returned SAT result as follows:



sat
(model 
  (define-fun f () Real
    (/ 1.0 2.0))
  (define-fun b () Int
    4)
  (define-fun a () Int
    2)
)


However, if I write '(assert (= f (div a b)))' instead of '(assert (= f (/ a b)))', then the result is UNSAT. Why does not div return the same result?



Moreover, and the main concern for me, I did not find a way to use operator '/' in z3 .Net API. I can see only function MkDiv, which actually for operator 'div'. Is there a way so that I can apply operator '/' in the case of z3 .Net API? Thank you in advance.



Wednesday, September 24, 2014  |  From active questions tagged z3 - Stack Overflow




I was trying to represent a real number with two integer numbers as using them as the numerator and the denominator of the real number. I wrote the following program:



(declare-const a Int)
(declare-const b Int)
(declare-const f Real)

(assert (= f (/ a b)))
(assert (= f 0.5))
(assert (> b 2))
(assert (> b a))

(check-sat)
(get-model)


The program returned SAT result as follows:



sat
(model 
  (define-fun f () Real
    (/ 1.0 2.0))
  (define-fun b () Int
    4)
  (define-fun a () Int
    2)
)


However, if I write '(assert (= f (div a b)))' instead of '(assert (= f (/ a b)))', then the result is UNSAT. Why does not div return the same result?



Moreover, and the main concern for me, I did not find a way to use operator '/' in z3 .Net API. I can see only function MkDiv, which actually for operator 'div'. Is there a way so that I can apply operator '/' in the case of z3 .Net API? Thank you in advance.



Wednesday, September 24, 2014  |  From active questions tagged z3 - Stack Overflow




My Python program uses Z3 Python API. It generates a number of assumptions to be checked by Z3 using the command:



check(P1, P2,....Pn)


Then I get the unsat core using the command:



unsat_core()


Is there a way I can use in my python program the command check(P1, P2,....Pn) without knowing the number of assertions in advance?
The number of assumptions is defined during the run of the code and changes every run.



Thanks in advance!



Tuesday, September 23, 2014  |  From active questions tagged z3 - Stack Overflow




I got some problems between OCaml interpreter and OCaml compiler. Can anyone help me? Thank you so much!



I have just compiled successfully the OCaml bindings for Z3 following by the instructions at https://github.com/polazarus/z3-installer. They use an old Z3 version: 4.1



First, I change the file Makefile.ocaml:



# Findlib package installation obtion, for instance -destdir /usr/lib/ocaml
OCAMLFIND_INSTALL_FLAGS = -destdir /home/maidinh/.opam/4.01.0/lib/


Then, I compile it:



sudo apt-get install camlidl
sudo make
sudo make install


I don't know why it fails when run 'make' without 'sudo' permission:



Finally, I test the OCaml bindings for Z3 by running the OCaml interpreter 4.01.0:



./ocaml
#use "topfind";;
#require "z3";;
open Z3;;
Z3.mk_context;;
- : (string * string) list -> Z3.context = <fun>


Successfully!






However, my program failed to run using OCaml compiler. This is my program:



let _ = print_endline "Start" in
let _ = Z3.mk_context [] in 
()


Then, I compile and run:



ocamlfind ocamlc -linkpkg -package z3 -c main.ml -o main.cmo
ocamlfind ocamlc -linkpkg -package z3 -o main  main.cmo
./main
Start
Error: internal error


Can anyone explain the error to me? Thank you so much!



Tuesday, September 23, 2014  |  From active questions tagged z3 - Stack Overflow




I wanted to create a SMT sequence, such that I have a total ordering which should be complete.



example 1:
a < b and b < c should be satisfiable



example 2:
a < b and c < d should be unsatisfiable.
By adding b < c we will get satisfiability.



Does anyone have any idea if this is even possible in general?
So far I tried the following:



 (declare-fun my_rel (Int Int) (Bool))
 (assert (forall ((i Int)(j Int)) (implies (my_rel i j) (> i j))))
 (declare-const a Int)
 (declare-const b Int)
 (declare-const c Int)
 (declare-const d Int)
 (assert (my_rel a b))
 (assert (my_rel c d))
 (check-sat)


This should return UNSAT. By adding (assert (my_rel b c)) it should satisfy.



Tuesday, September 23, 2014  |  From active questions tagged z3 - Stack Overflow




As previously asked Z3 can not provide a model for recursive functions. However, is it possible to tell Z3 (preferably via the Java API) that a model without a definition for recursive functions is sufficient (or indeed choose the functions I am interested in, essentially I do not need a model for non-constant functions)? Obviously, that might lead to queries that return sat although some functions do not have a model. Basically, the user then has to ensure that these functions do have some model.
However, I would assume this is not really realizable the way Z3 or SMT solvers work, i.e., I would assume Z3 needs a (partial) model of recursive functions to evalutate expressions.



Monday, September 22, 2014  |  From active questions tagged z3 - Stack Overflow




I wanted to create a SMT sequence, such that I have a total ordering which should be complete.



example 1:
a < b and b < c should be satisfiable



example 2:
a < b and c < d should be unsatisfiable.
By adding b < c we will get satisfiability.



Does anyone have any idea if this is even possible in general?
So far I tried the following:



 (declare-fun my_rel (Int Int) (Bool))
 (assert (forall ((i Int)(j Int)) (implies (my_rel i j) (> i j))))
 (declare-const a Int)
 (declare-const b Int)
 (declare-const c Int)
 (declare-const d Int)
 (assert (my_rel a b))
 (assert (my_rel c d))
 (check-sat)


This should return UNSAT. By adding (assert (my_rel b c)) it should satisfy.



 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.