moving my common z3 stuff to z3util.py … note the vset() call essentially returns a list with no duplicate elements, it's like set but allows the user to add in a function to compute the representation of the list elements.

src/api/python/z3util.py

@@ -1,5 +1,46 @@
+"""
+Usage:  
+import common_z3 as CM_Z3
+"""
+
+import common as CM
 from z3 import *
 
+def get_z3_version(as_str=False):
+    major = ctypes.c_uint(0)
+    minor = ctypes.c_uint(0)
+    build = ctypes.c_uint(0)
+    rev   = ctypes.c_uint(0)
+    Z3_get_version(major,minor,build,rev)
+    rs = map(int,(major.value,minor.value,build.value,rev.value))
+    if as_str:
+        return "{}.{}.{}.{}".format(*rs)
+    else:
+        return rs
+        
+    
+
+
+
+def ehash(v):
+    """
+    Returns a 'stronger' hash value than the default hash() method.
+    The result from hash() is not enough to distinguish between 2 
+    z3 expressions in some cases.
+    
+    >>> x1 = Bool('x'); x2 = Bool('x'); x3 = Int('x')
+    >>> print x1.hash(),x2.hash(),x3.hash() #BAD: all same hash values
+    783810685 783810685 783810685
+    >>> print ehash(x1), ehash(x2), ehash(x3)
+    x_783810685_1 x_783810685_1 x_783810685_2
+    
+    """
+    if __debug__:
+        assert is_expr(v)
+
+    return "{}_{}_{}".format(str(v),v.hash(),v.sort_kind())
+
+
 """
 In Z3, variables are caleld *uninterpreted* consts and 
 variables are *interpreted* consts.
@@ -56,3 +97,372 @@ def is_expr_val(v):
     """        
     return is_const(v) and v.decl().kind()!=Z3_OP_UNINTERPRETED
 
+
+
+
+def get_vars(f,rs=[]):
+    """
+    >>> x,y = Ints('x y')
+    >>> a,b = Bools('a b')
+    >>> get_vars(Implies(And(x+y==0,x*2==10),Or(a,Implies(a,b==False))))
+    [x, y, a, b]
+
+    """
+    if __debug__:
+        assert is_expr(f)
+
+    if is_const(f):
+        if is_expr_val(f):
+            return rs
+        else:  #variable
+            return CM.vset(rs + [f],str)
+
+    else:
+        for f_ in f.children():
+            rs = get_vars(f_,rs)
+
+        return CM.vset(rs,str)
+
+
+
+def mk_var(name,vsort):
+    if vsort.kind() == Z3_INT_SORT:
+        v = Int(name)
+    elif vsort.kind() == Z3_REAL_SORT:
+        v = Real(name)
+    elif vsort.kind() == Z3_BOOL_SORT:
+        v = Bool(name)
+    elif vsort.kind() == Z3_DATATYPE_SORT:
+        v = Const(name,vsort)
+
+    else:
+        assert False, 'Cannot handle this sort (s: %sid: %d)'\
+            %(vsort,vsort.kind())
+
+    return v
+
+
+
+def prove(claim,assume=None,verbose=0):
+    """
+    >>> r,m = prove(BoolVal(True),verbose=0); r,model_str(m,as_str=False)
+    (True, None)
+
+    #infinite counter example when proving contradiction
+    >>> r,m = prove(BoolVal(False)); r,model_str(m,as_str=False)
+    (False, [])
+
+    >>> x,y,z=Bools('x y z')
+    >>> r,m = prove(And(x,Not(x))); r,model_str(m,as_str=True)
+    (False, '[]')
+
+    >>> r,m = prove(True,assume=And(x,Not(x)),verbose=0)
+    Traceback (most recent call last):
+    ...
+    AssertionError: Assumption is alway False!
+
+    >>> r,m = prove(Implies(x,x),assume=y,verbose=2); r,model_str(m,as_str=False)
+    assume: 
+    y
+    claim: 
+    Implies(x, x)
+    to_prove: 
+    Implies(y, Implies(x, x))
+    (True, None)
+
+    >>> r,m = prove(And(x,True),assume=y,verbose=0); r,model_str(m,as_str=False)
+    (False, [(x, False), (y, True)])
+
+    >>> r,m = prove(And(x,y),assume=y,verbose=0)
+    >>> print r
+    False
+    >>> print model_str(m,as_str=True)
+    x = False
+    y = True
+
+    >>> a,b = Ints('a b')
+    >>> r,m = prove(a**b == b**a,assume=None,verbose=0)
+    E: cannot solve !
+    >>> r is None and m is None
+    True
+
+    """
+
+    if __debug__:
+        assert not assume or is_expr(assume)
+
+
+    to_prove = claim
+    if assume:
+        if __debug__:
+            is_proved,_ = prove(Not(assume))
+
+            def _f():
+                emsg = "Assumption is alway False!"
+                if verbose >= 2:
+                    emsg = "{}\n{}".format(assume,emsg)
+                return emsg
+
+            assert is_proved==False, _f()
+
+        to_prove = Implies(assume,to_prove)
+
+
+
+    if verbose >= 2:
+        print 'assume: '
+        print assume
+        print 'claim: '
+        print claim
+        print 'to_prove: '
+        print to_prove
+
+    f = Not(to_prove)
+
+    models = get_models(f,k=1)
+    if models is None: #unknown
+        print 'E: cannot solve !'
+        return None, None
+    elif models == False: #unsat
+        return True,None   
+    else: #sat
+        if __debug__:
+            assert isinstance(models,list)
+
+        if models:
+            return False, models[0] #the first counterexample
+        else:
+            return False, []  #infinite counterexample,models
+        
+
+def get_models(f,k):
+    """
+    Returns the first k models satisfiying f.
+    If f is not satisfiable, returns False.
+    If f cannot be solved, returns None
+    If f is satisfiable, returns the first k models
+    Note that if f is a tautology, e.g.\ True, then the result is []
+    
+    Based on http://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation
+
+    EXAMPLES:
+    >>> x, y = Ints('x y')
+    >>> len(get_models(And(0<=x,x <= 4),k=11))
+    5
+    >>> get_models(And(0<=x**y,x <= 1),k=2) is None
+    True
+    >>> get_models(And(0<=x,x <= -1),k=2)
+    False
+    >>> len(get_models(x+y==7,5))
+    5
+    >>> len(get_models(And(x<=5,x>=1),7))
+    5
+    >>> get_models(And(x<=0,x>=5),7)
+    False
+
+    >>> x = Bool('x')
+    >>> get_models(And(x,Not(x)),k=1)
+    False
+    >>> get_models(Implies(x,x),k=1)
+    []
+    >>> get_models(BoolVal(True),k=1)
+    []
+
+
+
+    """
+
+    if __debug__:
+        assert is_expr(f)
+        assert k>=1
+    
+
+
+    s = Solver()
+    s.add(f)
+
+    models = []
+    i = 0
+    while s.check() == sat and i < k:
+        i = i + 1
+
+        m = s.model()
+
+        if not m: #if m == []
+            break
+
+        models.append(m)
+
+
+        #create new constraint to block the current model
+        block = Not(And([v() == m[v] for v in m]))
+        s.add(block)
+
+    
+    if s.check() == unknown:
+        return None
+    elif s.check() == unsat and i==0:
+        return False
+    else:
+        return models
+
+def is_tautology(claim,verbose=0):
+    """
+    >>> is_tautology(Implies(Bool('x'),Bool('x')))
+    True
+
+    >>> is_tautology(Implies(Bool('x'),Bool('y')))
+    False
+
+    >>> is_tautology(BoolVal(True))
+    True
+
+    >>> is_tautology(BoolVal(False))
+    False
+
+    """
+    return prove(claim=claim,assume=None,verbose=verbose)[0]
+
+
+def is_contradiction(claim,verbose=0):
+    """
+    >>> x,y=Bools('x y')
+    >>> is_contradiction(BoolVal(False))
+    True
+    
+    >>> is_contradiction(BoolVal(True))
+    False
+    
+    >>> is_contradiction(x)
+    False
+    
+    >>> is_contradiction(Implies(x,y))
+    False
+    
+    >>> is_contradiction(Implies(x,x))
+    False
+    
+    >>> is_contradiction(And(x,Not(x)))
+    True
+    """
+
+    return prove(claim=Not(claim),assume=None,verbose=verbose)[0]
+
+
+def exact_one_model(f):
+    """
+    return True if f has exactly 1 model, False otherwise.
+    
+    EXAMPLES:
+
+    >>> x, y = Ints('x y')
+    >>> exact_one_model(And(0<=x**y,x <= 0))
+    False
+
+    >>> exact_one_model(And(0<=x,x <= 0))
+    True
+
+    >>> exact_one_model(And(0<=x,x <= 1))
+    False
+
+    >>> exact_one_model(And(0<=x,x <= -1))
+    False
+    """
+
+    models = get_models(f,k=2)
+    if isinstance(models,list):
+        return len(models)==1
+    else:
+        return False
+        
+    
+
+def myBinOp(op,*L):
+    """
+    >>> myAnd(*[Bool('x'),Bool('y')])
+    And(x, y)
+    
+    >>> myAnd(*[Bool('x'),None])
+    x
+    
+    >>> myAnd(*[Bool('x')])
+    x
+    
+    >>> myAnd(*[])
+    
+    >>> myAnd(Bool('x'),Bool('y'))
+    And(x, y)
+    
+    >>> myAnd(*[Bool('x'),Bool('y')])
+    And(x, y)
+
+    >>> myAnd([Bool('x'),Bool('y')])
+    And(x, y)
+
+    >>> myAnd((Bool('x'),Bool('y')))
+    And(x, y)
+    
+    >>> myAnd(*[Bool('x'),Bool('y'),True])
+    Traceback (most recent call last):
+    ...
+    AssertionError
+    """
+
+    if __debug__:
+        assert op == Z3_OP_OR or op == Z3_OP_AND or op == Z3_OP_IMPLIES
+    
+    if len(L)==1 and (isinstance(L[0],list) or isinstance(L[0],tuple)):
+        L = L[0]
+
+    if __debug__:
+        assert all(not isinstance(l,bool) for l in L)
+
+    L = [l for l in L if is_expr(l)]
+    if L:
+        if len(L)==1:
+            return L[0]
+        else:
+            if op ==  Z3_OP_OR:
+                return Or(L)
+            elif op == Z3_OP_AND:
+                return And(L)
+            else:   #IMPLIES
+                return Implies(L[0],L[1])
+    else:
+        return None
+
+
+def myAnd(*L): return myBinOp(Z3_OP_AND,*L)
+def myOr(*L): return myBinOp(Z3_OP_OR,*L)
+def myImplies(a,b):return myBinOp(Z3_OP_IMPLIES,[a,b])
+    
+
+
+Iff = lambda f,g: And(Implies(f,g),Implies(g,f))
+
+
+
+def model_str(m,as_str=True):
+    """
+    Returned a 'sorted' model (so that it's easier to see)
+    The model is sorted by its key, 
+    e.g. if the model is y = 3 , x = 10, then the result is 
+    x = 10, y = 3
+
+    EXAMPLES:
+    see doctest exampels from function prove() 
+
+    """
+    if __debug__:
+        assert m is None or m == [] or isinstance(m,ModelRef)
+
+    if m :
+        vs = [(v,m[v]) for v in m]
+        vs = sorted(vs,key=lambda (a,_): str(a)) 
+        if as_str:
+            return '\n'.join(['{} = {}'.format(k,v) for (k,v) in vs])
+        else:
+            return vs
+    else:
+        return str(m) if as_str else m
+