active questions tagged z3 - Stack Overflow News Feed 
Friday, July 03, 2015  |  From active questions tagged z3 - Stack Overflow




I have a declaration in Alloy



sig Card{}
sig ATM {card : disj set Card}



and i converted it into Z3 like that:



1- (declare-sort ATM)
2- (declare-fun isATM (ATM) Bool)
3- (declare-sort Card)
4- (declare-fun isCard (Card) Bool)
5- (declare-fun card (ATM Card) Bool)
6- (assert(forall ((c Card) (atm ATM)) (=> (card atm c) (and(isATM atm) (isCard c)))))
7- (declare-fun disjSetCard (ATM) Card)
8- (assert(forall ((atm ATM) (c Card)) (=> (card atm c)(= c(disjSetCard atm)))))
check sat



the question is, in line 7, how to make the function disjSetCard return (disj set) of Cards instead of one Card. is my code correct or there is different solution please?



thanks



Thursday, July 02, 2015  |  From active questions tagged z3 - Stack Overflow




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

(assert (exists ((a0 Int) (b0 Int) (c0 Int))
 (and (<= a 3)
      (>= a 0)
      (<= b 3)
      (>= b 0)
      (<= c 3)
      (>= c 0)
      (= 3 (+ a b c))
      (> a 1)
      (= a0 a)
      (= b0 b)
      (= c0 c)
      (= a0 2)
      (= b0 0)
      (= c0 1))))
(apply  (then qe ctx-solver-simplify propagate-ineqs))


I am trying to generate this code using the provided Java-API for the Z3 Solver. However, this ends up throwing the following Exception:



Z3 Managed Exception: propagate-ineqs does not support unsat core production



 Goal g = ctx.mkGoal(true, true, false);
 g.add((BoolExpr) exp);
 Tactic qe = ctx.mkTactic("qe");
 Tactic simpify = ctx.mkTactic("simplify");
 Tactic ctxSimpify = ctx.mkTactic("ctx-simplify");
 Tactic ctxSolverSimplify = ctx.mkTactic("ctx-solver-simplify");
 Tactic propagateIneqs = ctx.mkTactic("propagate-ineqs");
 Tactic then = ctx.then(qe, simpify, ctxSimpify, ctxSolverSimplify,
            propagateIneqs);
 ApplyResult ar = then.apply(g);
 BoolExpr result = ctx.mkAnd(ar.getSubgoals()[0].getFormulas());


Kindly let me know where am I going wrong and how can I use the tactic propagate-ineqs in Java-API. So that, I can get answers with trivial inequalities are simplified.



Thursday, July 02, 2015  |  From active questions tagged z3 - Stack Overflow




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

(assert (exists ((a0 Int) (b0 Int) (c0 Int))
 (and (<= a 3)
      (>= a 0)
      (<= b 3)
      (>= b 0)
      (<= c 3)
      (>= c 0)
      (= 3 (+ a b c))
      (> a 1)
      (= a0 a)
      (= b0 b)
      (= c0 c)
      (= a0 2)
      (= b0 0)
      (= c0 1))))
(apply  (then qe ctx-solver-simplify propagate-ineqs))


I am trying to generate this code using the provided Java-API for the Z3 Solver. However, this ends up throwing the following Exception:



Z3 Managed Exception: propagate-ineqs does not support unsat core production



 Goal g = ctx.mkGoal(true, true, false);
 g.add((BoolExpr) exp);
 Tactic qe = ctx.mkTactic("qe");
 Tactic simpify = ctx.mkTactic("simplify");
 Tactic ctxSimpify = ctx.mkTactic("ctx-simplify");
 Tactic ctxSolverSimplify = ctx.mkTactic("ctx-solver-simplify");
 Tactic propagateIneqs = ctx.mkTactic("propagate-ineqs");
 Tactic then = ctx.then(qe, simpify, ctxSimpify, ctxSolverSimplify,
            propagateIneqs);
 ApplyResult ar = then.apply(g);
 BoolExpr result = ctx.mkAnd(ar.getSubgoals()[0].getFormulas());


Kindly let me know where am I going wrong and how can I use the tactic propagate-ineqs in Java-API. So that, I can get answers with trivial inequalities are simplified.



Tuesday, June 30, 2015  |  From active questions tagged z3 - Stack Overflow




When checking the following problem using Z3, I receive different answers when wrapping or not wrapping it by a pair of push/pop



(declare-fun sz_53 () Int)
(declare-fun x () Int)
(declare-fun u () Int)
(declare-fun y () Int)
(assert (> u 0))
(assert (= (+ y (- 0 0)) 0))
(assert (or (= (- x u) 0) (> x 0)))
(assert (<= (* (- 0 1) sz_53) 0))
(assert (or (= (- x u) 0) (not (= (- x u) 0))))
(assert (not (and (and (and (and (exists ((sz_64 Int)) (and (= sz_64 0) (exists ((sz_62 Int)) (and (exists ((sz_55 Int)) (and (<= (* (- 0 1) sz_55) 0) (= (+ sz_53 (- sz_62 sz_55)) 0))) (= (+ sz_62 (- (- 0 1) sz_64)) 0))))) (>= y 0)) (or (= (+ x (* (- 0 1) y)) 0) (> x 0))) (not (= (+ u (* (- 0 1) y)) 0))) (not (= (+ u (* (- 0 1) y)) 0)))))
(assert (not false))
(check-sat)


Particularly, when checking it directly (not wrapping by push/pop), Z3 returns unsat
(Here is the online link: http://rise4fun.com/Z3/cDt3)



However, when wrapping it by push/pop, Z3 returns unknown
(http://rise4fun.com/Z3/epyh0)



Is there anybody who knows why Z3 behaves like this?



Thank you very much!



Tuesday, June 30, 2015  |  From active questions tagged z3 - Stack Overflow




I am inferring a function using z3py as follows



f = Function('f',IntSort(),IntSort(),IntSort())


After asserting a set of constraints like:



s.add(f(a1,b1)==c1)
s.add(f(a2,b2)==c2)
s.add(f(a3,b3)==c3)...


The function is inferred as



[(a1,b1) -> c1,
(a2,b2) -> c2,
(a3,b3) -> c3,
...,
else -> 2]


How could I constraint the "else" value to a fixed number? So that the output of inferred f will be



[(a1,b1) -> c1,
(a2,b2) -> c2,
(a3,b3) -> c3,
...,
else -> some number that I assert]


Edit:



from z3 import *

s = Solver()
k = Int('k')
f = Function('f',IntSort(),IntSort())

s.add(And(f(1)==1,f(2)==2))

list1 = []
list1.append(k!=1)
list1.append(k!=2)
s.add(ForAll(k,Implies(And(list1),f(k)==5)))

print s.check()
print s.model()


The output is



sat
[f = [1 -> 1, 2 -> 2, else -> 5]]


This seems to work fine for this simple case.



However, when the input for function 'f' in the constraints is undecided. The output can be weird. For example



from z3 import *

s = Solver()

f = Function('f',IntSort(),IntSort(),IntSort())

i = Int('i')
j = Int('j')
k = Int('k')
l = Int('l')


s.add(i>=0,i<5)
s.add(j>=0,j<5)

s.add(And(f(j,1)==i,f(i,2)==j))

list1 = []
list1.append(And(k==1,l==j))
list1.append(And(k==2,l==i))
s.add(ForAll([k,l],Implies(Not(Or(list1)),f(l,k)==5)))

print s.check()
print s.model()


The output is



[i = 0,
 k!6 = 0,
 j = 3,
 k!12 = 6,
 f = [else -> f!15(k!13(Var(0)), k!14(Var(1)))],
 f!15 = [(3, 1) -> 0, (0, 2) -> 3, else -> 5],
 k!13 = [0 -> 0, 3 -> 3, else -> 6],
 k!14 = [2 -> 2, 1 -> 1, else -> 0]]


Then it is hard to interpret the inferred f.



Tuesday, June 30, 2015  |  From active questions tagged z3 - Stack Overflow




I have an enumeration type BoolT that contains Bool and Bot



(declare-datatypes () ((BoolT Bool Bot)))


and I want to define an equality function eq that given two BoolT returns Bot if one of the arguments is Bot, otherwise the equality between the two Bool arguments. However, I am not able to define the actual comparison between the boolean values. Until now I get the function



(define-fun eq ((x1 BoolT) (x2 BoolT)) BoolT
    (ite (or (= x1 Bot) (= x2 Bot)) Bot Bool))


while I need something like



(define-fun eq ((x1 BoolT) (x2 BoolT)) BoolT
    (ite (or (= x1 Bot) (= x2 Bot)) Bot 
           (or (and (= x1 true)(= x2 true)) (and (= x1 false)(= x2 false)))
)


or at least a correct definition of the following predicate



(define-fun is-True ((x1 BoolT)) Bool 
     (ite (= x1 true) true false)
)


Is there a way to model the eq function or the previous predicate on BoolT?



Monday, June 29, 2015  |  From active questions tagged z3 - Stack Overflow




Recently, I am using Z3 C-API to solve problems of forall and datatypes.I want to set a timeout for context, but it looks like that the timeout does not work.Can anyone help me?



Z3_config  cfg;
Z3_context ctx;
cfg = Z3_mk_config();
Z3_set_param_value(cfg, "timeout", "2000");
ctx= Z3_mk_context(cfg);
Z3_del_config(cfg);


Monday, June 29, 2015  |  From active questions tagged z3 - Stack Overflow




I am inferring a function using z3py as follows



f = Function('f',IntSort(),IntSort(),IntSort())


After asserting a set of constraints like:



s.add(f(a1,b1)==c1)
s.add(f(a2,b2)==c2)
s.add(f(a3,b3)==c3)...


The function is inferred as



[(a1,b1) -> c1,
(a2,b2) -> c2,
(a3,b3) -> c3,
...,
else -> 2]


How could I constraint the "else" value to a fixed number? So that the output of inferred f will be



[(a1,b1) -> c1,
(a2,b2) -> c2,
(a3,b3) -> c3,
...,
else -> some number that I assert]


Monday, June 29, 2015  |  From active questions tagged z3 - Stack Overflow




In fact, does the SMT-LIB standard have a rational (not just real) sort? Going by its website, it does not.

If x is a rational and we have a constraint x^2 = 2, then we should get back ``unsatisfiable''. The closest I could get to encoding that constraint is the following:



;;(set-logic QF_NRA) ;; intentionally commented out

(declare-const x Real)

(assert (= (* x x) 2.0))

(check-sat)

(get-model)



for which z3 returns a solution, as there is a solution (irrational) in the reals. I do understand that z3 has its own rational library, which it uses, for instance, when solving QF_LRA constraints using an adaptation of the Simplex algorithm. On a related note, is there an SMT solver that supports rationals at the input level?



Monday, June 29, 2015  |  From active questions tagged z3 - Stack Overflow




I am trying to express the sum of the range of an unbounded Array in z3. For instance in Python:



IntArray = ArraySort(IntSort(), IntSort())

sum = Function('sum', IntArray, IntSort())

........


Is there any way to complete the definition of 'sum'? Otherwise, is there a more plausible alternative?



Thanks!



Thursday, June 25, 2015  |  From active questions tagged z3 - Stack Overflow




I am trying to use Z3 to solve string constraints using Z3 C# API.



So far, i have researched examples but Z3 seems to support only number based algebraic expressions such as :



x > 0
y = x + 1 
y < 3


which can be expressed using z3 c# API as:



using (Context ctx = new Context())
{
    Expr x = ctx.MkConst("x", ctx.MkIntSort());
    Expr y = ctx.MkConst("y", ctx.MkIntSort());
    Expr zero = ctx.MkNumeral(0, ctx.MkIntSort());
    Expr one = ctx.MkNumeral(1, ctx.MkIntSort());
    Expr three = ctx.MkNumeral(3, ctx.MkIntSort());

    Solver s = ctx.MkSolver();
    s.Assert(ctx.MkAnd(ctx.MkGt((ArithExpr)x, (ArithExpr)zero), ctx.MkEq((ArithExpr)y, 
        ctx.MkAdd((ArithExpr)x, (ArithExpr)one)), ctx.MkLt((ArithExpr)y, (ArithExpr)three)));
    Console.WriteLine(s.Check());

    Model m = s.Model;
    foreach (FuncDecl d in m.Decls)
            Console.WriteLine(d.Name + " -> " + m.ConstInterp(d));

    Console.ReadLine();
}


Is there any way to evaluate string based expressions such as:



string S1;
string S2:
string S3;
S3=S1+S2;


Any help with string based constraints will be appreciated.



Wednesday, June 24, 2015  |  From active questions tagged z3 - Stack Overflow




Environment: ubuntu12.04 + z3-v.4.3.2



Problem is same as : http://z3.codeplex.com/workitem/45



ASSERTION VIOLATION
File: ../src/ast/simplifier/poly_simplifier_plugin.cpp
Line: 58
i == 0 || !is_numeral(args[i])
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB


It was fixed before. However, it may be not fixed completely.



In following case , this problem will be triggered.In my project, all variables are represent as real_sort kind.



For following constraint,



if( a & 5)
{   
}


To represent “a& 5”, “a” and “5” should be represent bv_sort first, “&” require “a” and “5” be bv_sort kind. I write a function to realize converting from real to bv and bv to real due to lack of this API in z3 c++ API. Converted code is :



expr Z3_real2bv(expr rv, context &c)
{
    expr iv(c,Z3_mk_real2int(c,rv));
    expr bv(c,Z3_mk_int2bv(c,32,iv));
    return bv;
}

expr Z3_bv2real(expr bv, context &ctx)
{

    expr iv(ctx,Z3_mk_bv2int(ctx,bv,1));
    expr rv(ctx,Z3_mk_int2real(ctx,iv));
    return rv;
}


Then ,“a&5” may be wrote as followed:



context ctx;
expr a=ctx.real_const("a");
expr b=ctx.real_val("5");
expr av=Z3_real2bv(a,ctx);
expr bv=Z3_real2bv(b,ctx);
expr temp=av&bv;


all variables should be represented as real_sort, “temp” shall be converted back to real_sort,



expr r=Z3_bv2real(temp,ctx);


constraint “if(a&5)” is realized as followed:



solver s(ctx);
s.add(r!=0);


build and run, problem will be triggered.( a &b, b is a real_const will not triggered).



PS: to makes all variables are be represented as real_sort kind is project needed.



Wednesday, June 24, 2015  |  From active questions tagged z3 - Stack Overflow




This is a follow up question of this ticket How to loop over array in Z3Py



I am trying to assert a set of constraints for each element of an integer array in Z3.py. If I use "ForAll" to loop through the array, it takes a lot more time than writing a for loop using python code. Here is the sample code.



Loop using "ForAll":



from z3 import *
from timeit import default_timer as timer

s = Solver()

intArray = Array('intArray',IntSort(),IntSort())
i = Int('i')
check_start = timer()

s.add(ForAll(i,Implies(And(i>=0,i<200),intArray[i]==i)))

check_end = timer()
print "Modeling time: %.3f s" % (check_end - check_start)
check_start = timer()

print s.check()

check_end = timer()
print "Checking time: %.3f s" % (check_end - check_start)


Loop using python code



from z3 import *
from timeit import default_timer as timer

s = Solver()

intArray = Array('intArray',IntSort(),IntSort())
check_start = timer()

for i in range(0,1000):
    s.add(intArray[i]==i)

check_end = timer()
print "Modeling time: %.3f s" % (check_end - check_start)
check_start = timer()

print s.check()

check_end = timer()
print "Checking time: %.3f s" % (check_end - check_start)


But since, in my case, the size of the array is to be inferred, I cannot use the for loop in python. What is a faster way to assert constraints for each element of this kind of array?



I also found that when using for loop in python, the modeling time could be a lot more than the checking time when the number of iterations was large. Why is that? Is there any way to decrease the modeling time?



Wednesday, June 24, 2015  |  From active questions tagged z3 - Stack Overflow




I have a block of code that is ran via a loop for X iterations and each successive iteration relies on a value from a previous iteration.



For instance, the first iteration will take a value that is XOR'd with a seed and then use that as the first iteration. The result of that first computation with the seed is used for the 2nd iteration and so on and so forth.



I'm trying to figure out what a valid value would be for using that seed to get a specific end result for X iterations using the the Z3 SMT solver python API however I'm having trouble figuring out how one would even go about using previous SMT solutions for each successive iteration after?



Can somebody give me a hint or point me in the right direction?



Monday, June 22, 2015  |  From active questions tagged z3 - Stack Overflow




I have a very simple example Z3 program which is as follows:



(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)


This sample program can be executed in the Z3 online compiler and there are no problems. But when I want to execute the same program using command line prompt with the following command:



Z3 <script path>


I get the error saying:



ERROR: line 1 column 21: could not match expression to benchmark .


and this error is repeated for each line in the program.
Can anyone help me to see what I am doing wrong?



Monday, June 22, 2015  |  From active questions tagged z3 - Stack Overflow




I am experiencing some issues with the bitvector operations. In particular, given the following model. I was expecting var0 to be 11.



(declare-const var1 Int)
(declare-const var0 Int)
(assert (= var1 10))
(assert (= var0 ((_ bv2int 32) (bvor ((_ int2bv 32) var1) ((_ int2bv 32) 1)))))
(check-sat)
(get-model)
(exit)


However, the solution given by Z3 for fun was:



sat (model 
(define-fun var1 () Int 10) 
(define-fun var0 () Int (- 1)) 
)


This means, -1 instead of 10. Am I doing something wrong?



Monday, June 22, 2015  |  From active questions tagged z3 - Stack Overflow




As part of a reverse engineering exercise, I'm trying to write a Z3 solver to find a username and password that satisfy the program below. This is especially tough because the z3py tutorial that everyone refers to (rise4fun) is down.



#include <iostream>
#include <string>

using namespace std;

int main() {
    string name, pass;
    cout << "Name: ";
    cin >> name;

    cout << "Pass: ";
    cin >> pass;

    int sum = 0;
    for (size_t i = 0; i < name.size(); i++) {
        char c = name[i];
        if (c < 'A') {
            cout << "Lose: char is less than A" << endl;
            return 1;
        }
        if (c > 'Z') {
            sum += c - 32;
        } else {
            sum += c;
        }
    }
    int r1 = 0x5678 ^ sum;

    int r2 = 0;
    for (size_t i = 0; i < pass.size(); i++) {
        char c = pass[i];
        c -= 48;
        r2 *= 10;
        r2 += c;
    }
    r2 ^= 0x1234;

    cout << "r1: " << r1 << endl;
    cout << "r2: " << r2 << endl;
    if (r1 == r2) {
        cout << "Win" << endl;
    } else {
        cout << "Lose: r1 and r2 don't match" << endl;
    }
}


I got that code from the assembly of a binary, and while it may be wrong I want to focus on writing the solver. I'm starting with the first part, just calculating r1, and this is what I have:



from z3 import *

s = Solver()
sum = Int('sum')
name = Array('name', IntSort(), IntSort())
for c in name:
    s.add(c < 65)
    if c > 90:
        sum += c - 32
    else:
        sum += c
r1 = Xor(sum, 0x5678)
print s.check()
print s.model()


All I'm asserting is that there are no letters less than 'A' in the array, so I expect to get back an array of any size that has numbers greater than 65.



Obviously this is completely wrong, mainly because it infinite loops. Also, I'm not sure I'm calculating sum correctly, because I don't know if it's initialized to 0. Could someone help figure out how to get this first loop working?



EDIT: I was able to get a z3 script that is close to the C++ code shown above:



from z3 import *

s = Solver()
sum = 0
name = Array('name', BitVecSort(32), BitVecSort(32))
i = Int('i')

for i in xrange(0, 1):
    s.add(name[i] >= 65)
    s.add(name[i] < 127)
    if name[i] > 90:
        sum += name[i] - 32
    else:
        sum += name[i]
r1 = sum ^ 0x5678

passwd = Array('passwd', BitVecSort(32), BitVecSort(32))
r2 = 0
for i in xrange(0, 5):
    s.add(passwd[i] < 127)
    s.add(passwd[i] >= 48)
    c = passwd[i] - 48
    r2 *= 10
    r2 += c
r2 ^= 0x1234

s.add(r1 == r2)

print s.check()
print s.model()


This code was able to give me a correct username and password. However, I hardcoded the lengths of one for the username and five for the password. How would I change the script so I wouldn't have to hard code the lengths? And how would I generate a different solution each time I run the program?



Monday, June 22, 2015  |  From active questions tagged z3 - Stack Overflow




This is a simplified code using the similar implementation idea as the z3py code for another problem I am trying to solve which is more complex and takes about 1 minute to run.



The intuition of the following code is to translate the array of integers in the inputArray into the array of months defined as EnumSort, which is essentially to infer the model of monthArray.



from z3 import *
s = Solver()

Month,(Jan,Feb,Mar,Apr,May,Jun,Jul,Aug,Sep,Oct,Nov,Dec)=EnumSort('Month',['Jan','Feb','Mar','Apr','May','Jun','Jul','Aug','Sep','Oct','Nov','Dec'])
monthArray = Array('monthArray',IntSort(), Month)
inputArray = Array('inputArray',IntSort(),IntSort())
tempArray = Array('tempArray',IntSort(),IntSort())

intArray = [1,3,6,7,8,3,5,6,3,12,11,5,2,5,7,3,7,3,2,7,12,4,5,1,10,9]
for idx,num in enumerate(intArray):
    tempArray = Store(tempArray,idx,num)

s.add(inputArray==tempArray)

length = Int('length')
s.add(length == len(intArray))
i = Int('i')
s.add(ForAll(i,Implies(And(i>=0,i<length),And(
    Implies(inputArray[i]==1,monthArray[i]==Jan),
    Implies(inputArray[i]==2,monthArray[i]==Feb),
    Implies(inputArray[i]==3,monthArray[i]==Mar),
    Implies(inputArray[i]==4,monthArray[i]==Apr),
    Implies(inputArray[i]==5,monthArray[i]==May),
    Implies(inputArray[i]==6,monthArray[i]==Jun),
    Implies(inputArray[i]==7,monthArray[i]==Jul),
    Implies(inputArray[i]==8,monthArray[i]==Aug),
    Implies(inputArray[i]==9,monthArray[i]==Sep),
    Implies(inputArray[i]==10,monthArray[i]==Oct),
    Implies(inputArray[i]==11,monthArray[i]==Nov),
    Implies(inputArray[i]==12,monthArray[i]==Dec)
    ))))

print s.check()
print s.model()


Could anyone give me some suggestions about the ways to improve the time efficiency using this code as an example? Thanks.



Edit:
SMT language output by calling Solver.to_smt2()



(set-info :status unknown)
(declare-datatypes () ((Month (Jan ) (Feb ) (Mar ) (Apr ) (May ) (Jun ) (Jul ) (Aug ) (Sep ) (Oct ) (Nov ) (Dec ))))
(declare-fun inputArray () (Array Int Int))
(declare-fun length () Int)
(declare-fun monthArray () (Array Int Month))
(assert
(= (select inputArray 0) 1))
(assert
(= (select inputArray 1) 3))
(assert
(= (select inputArray 2) 6))
(assert
(= (select inputArray 3) 7))
(assert
(= (select inputArray 4) 8))
(assert
(= (select inputArray 5) 3))
(assert
(= (select inputArray 6) 5))
(assert
(= (select inputArray 7) 6))
(assert
(= (select inputArray 8) 3))
(assert
(= (select inputArray 9) 12))
(assert
(= (select inputArray 10) 11))
(assert
(= (select inputArray 11) 5))
(assert
(= (select inputArray 12) 2))
(assert
(= (select inputArray 13) 5))
(assert
(= (select inputArray 14) 7))
(assert
(= (select inputArray 15) 3))
(assert
(= (select inputArray 16) 7))
(assert
(= (select inputArray 17) 3))
(assert
(= (select inputArray 18) 2))
(assert
(= (select inputArray 19) 7))
(assert
(= (select inputArray 20) 12))
(assert
(= (select inputArray 21) 4))
(assert
(= (select inputArray 22) 5))
(assert
(= (select inputArray 23) 1))
(assert
(= (select inputArray 24) 10))
(assert
(= (select inputArray 25) 9))
(assert
(= length 26))
(assert
(forall ((i Int) )(let (($x172 (=> (= (select inputArray i) 12) (= (select monthArray i) Dec))))
(let (($x175 (=> (= (select inputArray i) 11) (= (select monthArray i) Nov))))
(let (($x178 (=> (= (select inputArray i) 10) (= (select monthArray i) Oct))))
(let (($x181 (=> (= (select inputArray i) 9) (= (select monthArray i) Sep))))
(let (($x184 (=> (= (select inputArray i) 8) (= (select monthArray i) Aug))))
(let (($x187 (=> (= (select inputArray i) 7) (= (select monthArray i) Jul))))
(let (($x190 (=> (= (select inputArray i) 6) (= (select monthArray i) Jun))))
(let (($x193 (=> (= (select inputArray i) 5) (= (select monthArray i) May))))
(let (($x196 (=> (= (select inputArray i) 4) (= (select monthArray i) Apr))))
(let (($x199 (=> (= (select inputArray i) 3) (= (select monthArray i) Mar))))
(let (($x202 (=> (= (select inputArray i) 2) (= (select monthArray i) Feb))))
(let (($x205 (=> (= (select inputArray i) 1) (= (select monthArray i) Jan))))
(=> (and (>= i 0) (< i length)) (and $x205 $x202 $x199 $x196 $x193 $x190 $x187 $x184 $x181 $x178 $x175 $x172)))))))))))))))
)
(check-sat)


Sunday, June 21, 2015  |  From active questions tagged z3 - Stack Overflow




I'd like to create an uninterpreted datatype in Z3 lets call it "A". According to z3 documentations, I can declare it by using "DeclareSort" as follows:



A = DeclareSort('A')
a, b = Consts('a b', A)
s = Solver()
s.add(a != b)
s.check()


However I've seen some people using the following:



A = Datatype('Event')
A.declare('A0')
A = A.create()

a, b = Consts('a b', A) 


My question is that what is the difference between those two and which one is correct to declare new uninterpreted datatype. Also I could not understand what does A.declare('A0') means in the second part.



Sunday, June 21, 2015  |  From active questions tagged z3 - Stack Overflow




I have a question about the using of ForAll in Z3.py. I want to create a local variable in ForAll declaration as follows:



A = DeclareSort('A')
a0,a1,a2,a3 = Consts('a0 a1 a2 a3', A)

s = Solver()
f = Function('f', A, A, BoolSort())
s.add(ForAll ([a0],(f(a0, a0))))

print (s.check())
print (s.model())


The result should be applied to all Consts except a0 as it is a local variable in the ForAll but the model shows the solution apply to all Consts including a0.



Creating local variable is possible in SMT but not in python.



Can anyone help?



 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.