-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 那样工作，它找到了一个有效/满意的见证/解释！

例如，我对相同代码的三个不同运行结果为：

>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，C1will be False，并且将没有AssertionError：

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