1

Suppose I have the following constraints

(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)

How to write the corresponding code in c/c++ interface of stp? My application requires to solve a constraint set similar to this. Any help is appreciated.

Dingbao Xie
  • 716
  • 9
  • 21

1 Answers1

2

See the C API testcases. There are a number of small, easy to read examples for how to use STP's C interface. Here is 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);
}

This corresponds to the smt query:

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

Once you have gotten a couple of these working, you can take a look at the c interface header for how to construct different operators.

Tim
  • 1,008
  • 5
  • 13
  • 1
    Thanks for your reply, Tim. Could you tell me how to declare and manipulate boolean variables? – Dingbao Xie Jun 05 '14 at 02:06
  • 1
    Try combining vc_boolType and vc_boolType to get a boolean variable. For manipulating boolean variables, you probably are going to have to read the c_interface.h header. Unfortunately, I don't have a copy of stp built in order to test this. – Tim Jun 06 '14 at 16:06