我们可以在教程中使用下面的代码来解决狗,猫,老鼠的难题。
dog, cat, mouse = Ints('dog cat mouse')
s = Solver();
s.add(dog>=1)
s.add(cat>=1)
s.add(mouse>=1)
s.add(dog+cat+mouse==100)
s.add(1500 * dog + 100 * cat + 25 * mouse == 10000)
print s.check()
print s.model()
好吧,我知道我可以使用
m=s.model
for d in m.decls():
print "%s = %s" % (d.name(), m[d])
以获取变量的名称和值。例如,cat = 41。我想知道我是否可以从名称和值创建一个新的断言,例如 cat != 41。我用了
s.add(d.name != m[d])
s.add("%s != %s" % (d.name(), m[d]))
但是,它们都行不通。有人知道如何通过读取模型的名称和值来添加新断言吗?非常感谢。
在for d in m.decls():
中,d
是一个func_decl,即只是一个声明,还不是一个变量(常量函数),所以我们需要将其应用于它的参数,这里为空。因此,我们可以做到:
m = s.model()
for d in m.decls():
v = d() # <-- Note parenthesis ()
print("%s != %s" % (v, m[d]))
s.add(v != m[d])
print(s)
print(s.check())
要得到
...
cat != 41
mouse != 56
dog != 3
[dog >= 1,
cat >= 1,
mouse >= 1,
dog + cat + mouse == 100,
1500*dog + 100*cat + 25*mouse == 10000,
41 != cat,
56 != mouse,
3 != dog]
unsat
要得到