STP Examples

Python usage

import stp
s = stp.Solver()
a = s.bitvec('a', 32)
b = s.bitvec('b', 32)
c = s.bitvec('c', 32)
s.add(a == 5)
s.add(b == 6)
s.add(a + b == c)
s.check()
-> True
s.model()
-> {'a': 5L, 'b': 6L, 'c': 11L}

For more examples, see the python test suite.

C library usage

#include "stp/c_interface.h"
#include <assert.h>

int main(int argc, char **argv) {
  VC vc = vc_createValidityChecker();

  // 32-bit variable 'c'
  Expr c = vc_varExpr(vc, "c", vc_bvType(vc, 32));

  // 32 bit constant value 5
  Expr a = vc_bvConstExprFromInt(vc, 32, 5);

  // 32 bit constant value 6
  Expr b = vc_bvConstExprFromInt(vc, 32, 6);

  // a+b!=c
  Expr xp1 = vc_bvPlusExpr(vc, 32, a, b);
  Expr eq = vc_eqExpr(vc, xp1, c);
  Expr eq2 = vc_notExpr(vc, eq);

  //Is a+b!=c always correct?
  int ret = vc_query(vc, eq2);

  //No, c=a+b is a counterexample
  assert(ret == false);

  //print c = 11 counterexample
  vc_printCounterExample(vc);

  //Delete validity checker
  vc_Destroy(vc);

  return 0;
}

For more examples, check out the tests we have.

SMT-LIBv2 Usage

Signed division of -1/-2 =  0, should be satisfiable.

(set-logic QF_BV)
(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
(check-sat)
(exit)

For more examples, see the SMT-Libv2 tutorial by GrammaTech.
Comments