-1

その値 val1 >= val2 をアサートする必要があります。つまり、モデルのチェックに関して、証人 (反例) は val1 >= val2 であると断言する必要があります。

C（cbmc）で次のように簡単に実行できます。

C1 = True;

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

Pythonでそれを行う方法はありますか?

アップデート：

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

引き起こす

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

でももしそうなら

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

結果は、私が望むものの逆です (val2 >= val1 が必要です)。 編集：

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)

選択した z と r の値に応じて、これは中断するか通過して x 、 y を出力します。したがって、これは __CPROVER_assert のようには機能せず、有効な/満足している証人/解釈を見つけます!

たとえば、同じコードを 3 回実行した結果は次のようになりました。

>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

Python で制約の充足可能性を確認する方法はありますか。

4

2 に答える 2

0

これがあなたが望むものかどうかはまだわかりませんが、必要なのが2つの乱数x、yでx> = yの場合、このようにその条件を強制する場合に必要なことはすべてです

from random import randint

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

必要な数値は 2 つだけなので、組み込み関数を使用してmaxそれらminの数値の順序を選択できます。

使用例:

>>> 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

これは、代わりにリストを返すことで任意のサイズに拡張できます。そのリストも順序付けしたい場合は、組み込みsorted関数を使用できます

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

ここでは、ジェネレーター式を使用して、要求された数だけ生成し、それをに渡してsortedその仕事をさせ、descendingそれが降順かどうかを制御します

例

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

順序が関係ない場合は、単純なリスト内包表記で十分です

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

例

>>> myRandomList(1,10,5)
[6, 7, 5, 8, 1]
>>>
于 2016-04-15T23:33:29.453 に答える
0

(元の投稿を考えると) 次の Python コードでは、 If val1 >= val2is True, C1beFalseになり、 no はありませんAssertionError:

C1 = True
C1 = C1 ^ (val1 >= val2)
assert not C1
于 2016-04-15T16:55:49.823 に答える