blob: 664536a0b70b237ca5180434b4cf6e28ec0fe56d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
#include "api/cpp/cvc5.h"
using namespace cvc5::api;
int main(void)
{
Solver slv;
slv.setOption("check-proofs", "true");
slv.setOption("proof-check", "eager");
Sort s1 = slv.getBooleanSort();
Sort s3 = slv.getStringSort();
Term t1 = slv.mkConst(s3, "_x0");
Term t3 = slv.mkConst(s1, "_x2");
Term t11 = slv.mkString("");
Term t14 = slv.mkConst(s3, "_x11");
Term t42 = slv.mkTerm(Kind::ITE, t3, t14, t1);
Term t58 = slv.mkTerm(Kind::STRING_LEQ, t14, t11);
Term t95 = slv.mkTerm(Kind::EQUAL, t14, t42);
slv.assertFormula(t95);
slv.checkSatAssuming({t58});
}
|