STP의 C / C ++ 인터페이스에서 Boolean 및 BitVector 변수가있는 제약 조건을 해결하는 방법
문제
다음과 같은 제약 조건이 있다고 가정합니다.
(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 ++ 인터페이스에 해당 코드를 작성하는 방법은 무엇입니까? 내 응용 프로그램은 이와 비슷한 제약 조건을 해결해야합니다. 어떤 도움이 감사합니다.
해결책
C API TestCases 를 참조하십시오.STP의 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 인터페이스 헤더 다른 운영자를 구성하는 방법
제휴하지 않습니다 StackOverflow