问题描述
我是python的新手，还是z3的新手。我正在尝试通过z3py解决一些SMT问题。 现在我需要设置一个限制：array1（1,8）至少有5个零。但是我遇到了一些错误。
/// <summary>
/// Extension methods to quickly convert byte array to string and back.
/// </summary>
public static class HexConverter
{
/// <summary>
/// Map values to hex digits
/// </summary>
private static readonly char[] HexDigits =
{
'0','1','2','3','4','5','6','7','8','9','A','B','C','D','E','F'
};
/// <summary>
/// Map 56 characters between ['0','F'] to their hex equivalents,and set invalid characters
/// such that they will overflow byte to fail conversion.
/// </summary>
private static readonly ushort[] HexValues =
{
0x0000,0x0001,0x0002,0x0003,0x0004,0x0005,0x0006,0x0007,0x0008,0x0009,0x0100,0x000A,0x000B,0x000C,0x000D,0x000E,0x000F,0x000F
};
/// <summary>
/// Empty byte array
/// </summary>
private static readonly byte[] Empty = new byte[0];
/// <summary>
/// Convert a byte array to a hexadecimal string.
/// </summary>
/// <param name="bytes">
/// The input byte array.
/// </param>
/// <returns>
/// A string of hexadecimal digits.
/// </returns>
public static string ToHexString(this byte[] bytes)
{
var c = new char[bytes.Length * 2];
for (int i = 0,j = 0; i < bytes.Length; i++)
{
c[j++] = HexDigits[bytes[i] >> 4];
c[j++] = HexDigits[bytes[i] & 0x0F];
}
return new string(c);
}
/// <summary>
/// Parse a string of hexadecimal digits into a byte array.
/// </summary>
/// <param name="hexadecimalString">
/// The hexadecimal string.
/// </param>
/// <returns>
/// The parsed <see cref="byte[]"/> array.
/// </returns>
/// <exception cref="ArgumentException">
/// The input string either contained invalid characters,or was of an odd length.
/// </exception>
public static byte[] ToByteArray(string hexadecimalString)
{
if (!TryParse(hexadecimalString,out var value))
{
throw new ArgumentException("Invalid hexadecimal string",nameof(hexadecimalString));
}
return value;
}
/// <summary>
/// Parse a hexadecimal string to bytes
/// </summary>
/// <param name="hexadecimalString">
/// The hexadecimal string,which must be an even number of characters.
/// </param>
/// <param name="value">
/// The parsed value if successful.
/// </param>
/// <returns>
/// True if successful.
/// </returns>
public static bool TryParse(string hexadecimalString,out byte[] value)
{
if (hexadecimalString.Length == 0)
{
value = Empty;
return true;
}
if (hexadecimalString.Length % 2 != 0)
{
value = Empty;
return false;
}
try
{
value = new byte[hexadecimalString.Length / 2];
for (int i = 0,j = 0; j < hexadecimalString.Length; i++)
{
value[i] = (byte)((HexValues[hexadecimalString[j++] - '0'] << 4)
| HexValues[hexadecimalString[j++] - '0']);
}
return true;
}
catch (OverflowException)
{
value = Empty;
return false;
}
}
}
这是我声明的内容，当我想使用al1,al2,al3,al4,al5,al6,al7,al8=Ints('al1 al2 al3 al4 al5 al6 al7 al8')时，会出现错误消息，提示al1=If(be1*wi1,1,0)
或Z3Exception: Value cannot be converted into a Z3 Boolean value
我想知道如何计算这些元素中有多少个零？，我不确定是否可以更改此声明...我只是从示例中复制了这一部分。 >
解决方法
始终最好张贴完整的代码，以便人们可以看到并评论您的尝试。
在任何一种情况下，要表达这种最少/最多种类的约束，都应使用所谓的“伪布尔”约束。例如，要说这些元素中至少有5个是0，您可以说：
from z3 import *
al1,al2,al3,al4,al5,al6,al7,al8 = Ints('al1 al2 al3 al4 al5 al6 al7 al8')
s = Solver()
s.add(AtLeast(al1 == 0,al2 == 0,al3 == 0,al4 == 0,al5 == 0,al6 == 0,al7 == 0,al8 == 0,5))
print(s.check())
print(s.model())
运行此命令时，我得到：
sat
[al8 = 1,al7 = 1,al6 = 1,al5 = 0,al4 = 0,al3 = 0,al2 = 0,al1 = 0]
您看到5个变量为0。（显然，这不是唯一的模型，但z3为您找到了一个模型。您显然可以添加其他约束。）
有关伪布尔约束的详细信息，请参见：https://z3prover.github.io/api/html/namespacez3py.html#a8575bdeb9d1b8feac119aa162b5acfa6
您要研究的功能称为：AtMost，AtLeast，PbLe，PbGe和PbEq。