Getting an effect of __CPROVER_assert in Python?

Question

I have to assert that value val1 >= val2. That is in terms of Model checking, the witness(counterexample) has to assert that the val1 >= val2.

I can do it easily in C (cbmc) by:

C1 = True;

C1 = (C1 && (val1 >= val2));
__CPROVER_assert(!C1 ,"constraint sat");

Is there a way to do that in Python?

Update:

C1  = True
C1 = C1 && (val1 >= val2)
assert not C1

causing

 File "python_version.py", line 123, in main
    assert not  C1
AssertionError

But if I do

C1  = True
C1 = C1 && (val1 >= val2)
assert C1

The result is the reverse of what I want (I want val2 >= val1). Edit:

import math 
from random import randint

def main():

C1 = True
z = randint(1,10)
r = randint(1,10)
x  = z + 2
y  = r + 2

C1 = C1 and (x >= y)
assert  C1

print(x)
print(y)

Depending upon the value of z and r chosen, this will break or goes through and prints x , y. So this not working as __CPROVER_assert does, which finds a witness / interpretation that is valid / satisfied !

For example, my three different runs of same code resulted as:

>mokambo 11:16 PM ~/cost-allocation/Constraint_solving python checkPython.py 

Traceback (most recent call last):

  File "checkPython.py", line 23, in <module>
    main()

  File "checkPython.py", line 15, in main
    assert  C1
AssertionError

>mokambo 11:16 PM ~/cost-allocation/Constraint_solving python checkPython.py 

7
4

>mokambo 11:16 PM ~/cost-allocation/Constraint_solving python checkPython.py 

12
11

Is there any way to check satisfiability of a constraint in Python.

Could you use an [`assert`](https://docs.python.org/2/reference/simple_stmts.html#the-assert-statement) statement? e.g. `assert (C1 && (val1 >= val2))`. You can also follow this [stackoverflow post](http://stackoverflow.com/questions/5142418/what-is-the-use-of-assert-in-python) for more details. — AKS, Apr 15 '16 at 10:56
@AKS assert is causing only one way. val2 i.e if i'm doing !(C1 && (val1 >= val2))) its coming fine. but using this val1 >= val2 causing violation. — Pushpa, Apr 15 '16 at 16:43
Are you asking for an `assert` function that works in that it tries every combination of values and asserts that it'll always be True? So like `x` and `y` would be any possible numbers and you're looking for an assert where `special_assert(x>y)` would be true if x and y was any number ever? — TankorSmash, Apr 15 '16 at 17:34
yes sir, So that i could check validity directly and using !prop i can check satisfaibility. — Pushpa, Apr 15 '16 at 17:42
Consider the [combinations function](https://docs.python.org/2/library/itertools.html). For instance, `for combination in combinations(iterable, combinationLength): print combination`, where all possible combinations of the elements in a list or tuple are iterated (no duplicates with a different order) — ballade4op52, Apr 15 '16 at 18:00
so you want to get 2 randoms numbers x, y such that always x>=y ? or you are given 2 number x,y and want to do something if x>=y and trow a error otherwise? In the first case just build it like that, in the second that should be obvious — Copperfield, Apr 15 '16 at 18:03
No i want the first thing. I have make sure that the x and y be chosen such that x >= y. In case its not possible for example x = random_number() and y = x + 1; then it should say satisfiable i.e have no interpretation of x and y such that this assertion holds. — Pushpa, Apr 15 '16 at 19:09

ballade4op52 · Answer 1 · 2016-04-15T17:32:34.650

0

(Given the original post) With the following Python code, If val1 >= val2 is True, C1 will be False, and there will be no AssertionError:

C1 = True
C1 = C1 ^ (val1 >= val2)
assert not C1

edited Apr 15 '16 at 17:32

answered Apr 15 '16 at 16:55

ballade4op52

2,142
5
27
42

Phill i have to make sure that C1 is never Violated rather than C1 comes out to be False. That means i have make sure that val1 >= val2 is the case. – Pushpa Apr 15 '16 at 17:00
It appears your issue is not with how to use `assert`, but with why `val1` is less than `val2`, in which case more information is required. – ballade4op52 Apr 15 '16 at 17:14
Okay I understood Now. Its working not like __CPROVER_assert there is no search for all thing by default. So how to check satisfiability in Python ? that there exist an interpretation that satisfies that there exists a value for val1 , val2 such that val1 >= val2 . – Pushpa Apr 15 '16 at 17:21

score 0 · Answer 2 · answered Apr 15 '16 at 23:33

I still not sure if this is what you want, but if all you need is 2 random numbers x, y such that x>=y all you need to do if force that condition, like this

from random import randint

def myRandomTuple(ini,fin):
    x = randint(ini,fin)
    y = randint(ini,fin)
    return (max(x,y),min(x,y))

as we only want 2 numbers we can use the build-in function max and min to choose the order of those numbers

example of use:

>>> myRandomTuple(1,10)
(10, 2)
>>> myRandomTuple(1,10)
(9, 3)
>>> myRandomTuple(1,10)
(7, 1)
>>> myRandomTuple(1,10)
(4, 4)
>>> myRandomTuple(1,10)
(10, 3)
>>> myRandomTuple(1,10)
(8, 1)
>>> x,y = myRandomTuple(1,10)
>>> x
10
>>> y
6

this can be extended to any arbitrary size by returning a list instead, and if we want that that list be ordered as well we can use the build-in sorted function

def myRandomList(ini,fin,size,descending=True):
    return sorted( (randint(ini,fin) for _ in range(size)), reverse=descending)

here I use a generator expression, to well, generate as many number as asked for, pass that to sorted and let it do its job and with descending I control if it is descending order or not

example

>>> myRandomList(1,10,5)
[6, 6, 5, 4, 2]
>>>

if the order is irrelevant, then a simple list comprehension is enough

def myRandomList(ini,fin,size):
    return [ randint(ini,fin) for _ in range(size) ]

example

>>> myRandomList(1,10,5)
[6, 7, 5, 8, 1]
>>>

Getting an effect of __CPROVER_assert in Python?

2 Answers2