获取不稳定的核心示例我想在C#实现中使用Z3坐标解算器。此代码非常接近Microsoft本身在“http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs”中给出的示例。我的代码是:使用Z3和c#
using (Context ctx = new Context(new Dictionary<string, string>() { { "proof", "true" } }))
{
...
Expr x = ctx.MkConst("x", ctx.MkIntSort());
Expr y = ctx.MkConst("y", ctx.MkIntSort());
Expr zero = ctx.MkNumeral(0, ctx.MkIntSort());
Expr one = ctx.MkNumeral(1, ctx.MkIntSort());
Expr five = ctx.MkNumeral(5, ctx.MkIntSort());
Solver s = ctx.MkSolver();
s.Assert(ctx.MkGt((ArithExpr)x, (ArithExpr)zero)); // x > 0
s.Assert(ctx.MkLt((ArithExpr)y, (ArithExpr)five)); // y < 5
s.Assert(ctx.MkLt((ArithExpr)x, (ArithExpr)zero)); // x < 0
s.Assert(ctx.MkEq((ArithExpr)y, ctx.MkAdd((ArithExpr)x, (ArithExpr)one))); // y = x + 1
Status result = s.Check();
if (result == Status.UNSATISFIABLE)
{
Console.WriteLine("unsat");
Console.WriteLine("proof: {0}", s.Proof);
Console.WriteLine("core: ");
foreach (Expr c in s.UnsatCore)
{
Console.WriteLine("{0}", c);
}
}
但仍然当我到达这个模型的“s.UnsatCore”它是空的。
我自己也尝试在这样的断言进入:
BoolExpr constraint1 = ctx.MkBoolConst("Constraint1");
s.AssertAndTrack(ctx.MkGt((ArithExpr)x, (ArithExpr)zero), constraint1);
BoolExpr constraint2 = ctx.MkBoolConst("Constraint2");
s.AssertAndTrack(ctx.MkLt((ArithExpr)y, (ArithExpr)five), constraint2);
BoolExpr constraint3 = ctx.MkBoolConst("Constraint3");
s.AssertAndTrack(ctx.MkLt((ArithExpr)x, (ArithExpr)zero), constraint3);
BoolExpr constraint4 = ctx.MkBoolConst("Constraint4");
s.AssertAndTrack(ctx.MkEq((ArithExpr)y, ctx.MkAdd((ArithExpr)x, (ArithExpr)one)), constraint4);
我想的UnsatCore返回“constraint1,constrint3”。任何人都可以帮助我做我做错了什么?
请添加输出结果和输出结果 – 2015-02-11 16:20:58
我希望返回第一个和最后一个约束。我也是这样写的: – 2015-02-11 16:30:18
BoolExpr constraint1 = ctx.MkBoolConst(“Constraint1”); s.AssertAndTrack(ctx.MkGt((ArithExpr)x,(ArithExpr)zero),constraint1); BoolExpr constraint2 = ctx。 MkBoolConst(“Constraint2”); s.AssertAndTrack(ctx.MkLt((ArithExpr)y,(ArithExpr)five),constraint2); BoolExpr constraint3 = ctx.MkBoolConst(“Constraint3”); s.AssertAndTrack(ctx。 MkLt((ArithExpr)x,(ArithExpr)zero),constraint3); – 2015-02-11 16:32:28