在Z3多值逻辑公式评价 [英] Evaluation of a logical formula at many values in Z3
问题描述
我需要评估过的Z3使用各种变量值的表达式的值。
我知道Z3是satisfiabilty检查，但model.Eval（参数）会导致一个表达式的评估在由模型生成的变量的值。
因此，它是可能的。p和q在p和q（p，q是布尔）的所有可能值
例>
因此，在一定意义上使用一些递归或迭代创建真值表出来。
是可以任何方式Z3这样做呢？
帮助与C＃的API会更好。
感谢
您可以考虑的方法替换在C＃API。它可以用来替代常量，如 P 和①按值。它还简化/评估应用替换后的公式。
下面是一个小的C＃示例（从我们的回归测试套件）使用替换：
使用Microsoft.Z3;
使用系统;
使用System.Collections.Generic;
类测试
{
公共无效的run（）
{
&字典LT;字符串，字符串> CFG =新词典<字符串，字符串>（）{
{AUTO_CONFIG，真}};
使用（上下文CTX =新的上下文（CFG））
{
IntExpr X = ctx.MkIntConst（X）;
IntExpr Y = ctx.MkIntConst（Y）;
FuncDecl F = ctx.MkFuncDecl（F，新的排序[] {ctx.IntSort，ctx.IntSort}，ctx.IntSort）;
FuncDecl G = ctx.MkFuncDecl（G，新的排序[] {} ctx.IntSort，ctx.IntSort）;
Expr的N = F [F [政[X]，G [G [X]]]，G [G [Y]]];
Console.WriteLine（N）;
Expr的NN = n.Substitute（新Expr的[] {绿[G [X]，G [Y]}，
新Expr的[] {Y，ctx.MkAdd（X ，ctx.MkInt（1））}）;
Console.WriteLine（NN）;
Console.WriteLine（n.Substitute（G [G [X]，Y））;
}
}
}
当然，你将有写一个循环遍历所有可能的值。
在Python中，你可以使用列表理解： http://rise4fun.com/Z3Py/56
另一种选择是使用方法简化。此方法可用于评估不包含未解释的符号，如点公式和①。
这里是用Python另外一个例子： http://rise4fun.com/Z3Py/PC $我使用Python，因为我们没有在浏览器中运行的C＃示例技术支援b $ b。
注意的是，在C＃Z3的API包含的Python之一的全部功能。
最后，另一个可能性是枚举的模型。
通过这样做，你基本上是生产的所有值 P 和①满足公式（即，它是真的）。这个想法是添加阻断当前模型新的限制，并再次解决。这是在Python小脚本这样做：
http://rise4fun.com/Z3Py/PDJ
约束块用于阻止当前模型。如果我们取消注释打印块，我们也可以将其打印由Z3制作每个模型。当然，如果有，在本实施例中满足式像无限模型这种方法没有终止：
HTTP ：//rise4fun.com/Z3Py/X0l
这些例子可以在C＃进行编码。这里是一个C＃示例演示了如何遍历模型中的常数（和功能），并获得他们的解释：
使用Microsoft.Z3;
使用系统;
类测试
{
$ B使用$ B公共无效的run（）
{
（上下文CTX =新的上下文（））
{
排序U = ctx.MkUninterpretedSort（U）;
FuncDecl F = ctx.MkFuncDecl（F，U，U）;
Expr的一个= ctx.MkConst（一，U）;
Expr的B = ctx.MkConst（B，U）;
Expr的C = ctx.MkConst（C，U）;
求解S = ctx.MkSolver（）;
s.Assert（ctx.MkEq（F [F [A]，B），
ctx.MkNot（ctx.MkEq（F [B]，C）），
CTX。 MkEq（F [C]，C））;
Console.WriteLine（s.Check（））;
型M = s.Model;
的foreach（在m.Decls FuncDecl D）
如果（d.DomainSize == 0）
Console.WriteLine（d.Name + - >中+ m.ConstInterp（D） ）;
，否则
Console.WriteLine（d.Name + - >中+ m.FuncInterp（D））;
Console.WriteLine（m.NumSorts）;
Console.WriteLine（m.Sorts [0]）;
的foreach（在m.Sorts排序SRT）
Console.WriteLine（SRT）;
的foreach（在m.SortUniverse（U Expr的V））
Console.WriteLine（V）;
}
}
}
I needed to evaluate the value of an expression over various values of variables using Z3. I know Z3 is a satisfiabilty checker but model.Eval(Args) causes evaluations of an expression at values of variables generated by model.
So is it possible for us to iterate over various values to evaluate an expression.
Example : p and q at all possible values of p and q (p,q being Boolean )
So in some sense creating a truth table out of it using some recursion or iteration. Is it possible any way for Z3 to do so?
Help with the C# API will be even better.
Thanks
You may consider the method Substitute in the C# API. It can be used to substitute constants such as p and q by values. It also simplifies/evaluates the formula after applying the substitution.
Here is a small C# example (from our regression suite) using Substitute:
using Microsoft.Z3;
using System;
using System.Collections.Generic;
class Test
{
public void Run()
{
Dictionary<string, string> cfg = new Dictionary<string, string>() {
{ "AUTO_CONFIG", "true" } };
using (Context ctx = new Context(cfg))
{
IntExpr x = ctx.MkIntConst("x");
IntExpr y = ctx.MkIntConst("y");
FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { ctx.IntSort, ctx.IntSort }, ctx.IntSort);
FuncDecl g = ctx.MkFuncDecl("g", new Sort[] { ctx.IntSort }, ctx.IntSort);
Expr n = f[f[g[x], g[g[x]]], g[g[y]]];
Console.WriteLine(n);
Expr nn = n.Substitute(new Expr[] { g[g[x]], g[y] },
new Expr[] { y, ctx.MkAdd(x, ctx.MkInt(1)) } );
Console.WriteLine(nn);
Console.WriteLine(n.Substitute(g[g[x]], y));
}
}
}
Of course, you will have to write a loop to iterate over all possible values.
In Python, you can use list comprehensions: http://rise4fun.com/Z3Py/56
Another option is to use the method Simplify. This method can be used to evaluate formulas that do not contains uninterpreted symbols such as p and q.
Here is another example in Python: http://rise4fun.com/Z3Py/PC
I'm using Python because we don't have support for running C# examples in the browser.
Note that, the Z3 API in C# contains all the functionality of the Python one.
Finally, another possibility is to enumerate models.
By doing it, you are essentially producing all values of p and q that satisfy the formula (i.e., make it true). The idea is to add new constraints that block the current model, and solve again. Here is a small script in Python for doing it:
http://rise4fun.com/Z3Py/PDJ
The constraint block is used to block the current model. If we uncomment print block, we can also print it for each model produced by Z3. Of course, this approach does not terminate if there are infinite models that satisfy the formula like in this example:
http://rise4fun.com/Z3Py/X0l
These examples can be encoded in C#. Here is a C# example demonstrating how to iterate over the constants (and functions) in a model, and obtaining their interpretation:
using Microsoft.Z3;
using System;
class Test
{
public void Run()
{
using (Context ctx = new Context())
{
Sort U = ctx.MkUninterpretedSort("U");
FuncDecl f = ctx.MkFuncDecl("f", U, U);
Expr a = ctx.MkConst("a", U);
Expr b = ctx.MkConst("b", U);
Expr c = ctx.MkConst("c", U);
Solver s = ctx.MkSolver();
s.Assert(ctx.MkEq(f[f[a]], b),
ctx.MkNot(ctx.MkEq(f[b], c)),
ctx.MkEq(f[c], c));
Console.WriteLine(s.Check());
Model m = s.Model;
foreach (FuncDecl d in m.Decls)
if (d.DomainSize == 0)
Console.WriteLine(d.Name + " -> " + m.ConstInterp(d));
else
Console.WriteLine(d.Name + " -> " + m.FuncInterp(d));
Console.WriteLine(m.NumSorts);
Console.WriteLine(m.Sorts[0]);
foreach(Sort srt in m.Sorts)
Console.WriteLine(srt);
foreach (Expr v in m.SortUniverse(U))
Console.WriteLine(v);
}
}
}
这篇关于在Z3多值逻辑公式评价的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
