1

我想在 ac 程序中使用Yices SMT 求解器来求解表达式x > 100并获得x. 这是我的代码：

#include<stdio.h>
#include"yices_c.h"

int main() {
  yices_context ctx = yices_mk_context();
  char int_ty_name[] = "int";
  yices_type int_ty = yices_mk_type(ctx, int_ty_name);
  char vname[] = "x";
  yices_expr e1 = yices_mk_num(ctx,100);
  yices_var_decl v = yices_mk_var_decl(ctx,vname,int_ty);
  yices_expr e2 = yices_mk_var_from_decl(ctx,v);
  yices_expr eq1 = yices_mk_lt(ctx, e1, e2);
  yices_assert(ctx, eq1);
  yices_dump_context(ctx);
  switch(yices_check(ctx)) {
  case l_true:
    printf("satisfiable\n");
    yices_model m = yices_get_model(ctx);
    long i;
    yices_get_int_value(m,v,&i);
    printf("e2 = %d\n", i);
    yices_display_model(m);
    break;  
  case l_false:
    printf("unsatisfiable\n");
    break;
  case l_undef:
    printf("unknown\n");
    break;
  }
  yices_del_context(ctx);
  return 0;
}

这个程序总是结果x =101。这101只是此表达式的可能结果之一。我希望求解器从所有可能的结果中选择一个随机结果（从 101 到 MAX_INT 的随机整数）。

我应该怎么办？

4

2 回答 2

0

尝试使用yices_find_weighted_model(ctx, 1)而不是yices_check(ctx).

如果您没有加权约束，yices_find_weighted_model(ctx, 0)则应在语义上等效于yices_check(ctx). 但是 的第二个参数yices_find_weighted_model称为random，如果您将其设置为非零值，则允许您使用随机搜索而不是默认决策过程。检查文档。

于 2013-09-01T11:26:54.673 回答
0

您将首先得到一个非随机结果。然后你可以添加一个随机约束 (X>nonRandomResult+delta或X<nonRandomResult-delta) 和一个随机增量。

只要无法解决，您就必须使用具有先前值一半的新增量来更改约束。一旦有了解决方案，该解决方案很可能与该增量一样随机。

于 2013-09-30T16:39:36.110 回答