如何在 stp 的 c/c++ 接口中使用布尔变量和位向量变量解决约束答案

【问题标题】：How to solve constraints with boolean and bitvector variables in c/c++ interface of stp如何在 stp 的 c/c++ 接口中使用布尔变量和位向量变量解决约束
【发布时间】：2014-07-25 02:53:56
【问题描述】：

假设我有以下限制

(declare-fun x () Bool)
(declare-fun y () Bool)
(declare-fun t1 () (_ BitVec 8))
(declare-fun t2 () (_ BitVec 8))
(assert (or x y))
(assert (=> x (bvule t1 t2)))
(assert (=> y (bvule t2 t1)))
(check-sat)

如何在stp的c/c++接口中编写相应的代码？我的应用程序需要解决与此类似的约束集。任何帮助表示赞赏。

【问题讨论】：

标签： smt bitvector stp

【解决方案1】：

请参阅C API testcases。关于如何使用 STP 的 C 接口，有许多易于阅读的小示例。这是push-pop.c。

/* g++ -I$(HOME)/stp/c_interface push-pop.c -L$(HOME)/lib -lstp -o cc*/

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

int main() {
  VC vc = vc_createValidityChecker();
  vc_setFlags('n');
  vc_setFlags('d');
  vc_setFlags('p');
  //vc_setFlags('v');
  //vc_setFlags('s');

  Type bv8 = vc_bvType(vc, 8);

  Expr a = vc_varExpr(vc, "a", bv8);
  Expr ct_0 = vc_bvConstExprFromInt(vc, 8, 0);

  Expr a_eq_0 = vc_eqExpr(vc, a, ct_0);

  int query = vc_query(vc, a_eq_0);
  printf("query = %d\n", query);

  vc_push(vc);
  query = vc_query(vc, a_eq_0);
  vc_pop(vc);

  printf("query = %d\n", query);
}

这对应于smt查询：

(declare-fun a () (_ BitVec 8))
(push)
(assert (not (= a (_ bv0 8))))
(check-sat)
(pop)

一旦您完成了其中的一些工作，您可以查看c interface header，了解如何构造不同的运算符。

【讨论】：

感谢您的回复，蒂姆。你能告诉我如何声明和操作布尔变量吗？
尝试结合 vc_boolType 和 vc_boolType 来获得一个布尔变量。为了操作布尔变量，您可能必须阅读 c_interface.h 头文件。不幸的是，我没有为测试这个而构建的 stp 副本。