mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
00e19fdbe2
We now track difficulty on lemmas themselves, which can potentially used as a heuristic for measuring the usefulness of lemmas. This also makes it so that all literals in lemmas are used for incrementing difficulty.
3647 lines
133 KiB
C++
3647 lines
133 KiB
C++
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Aina Niemetz, Andrew Reynolds, Mathias Preiner
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
|
|
* in the top-level source directory and their institutional affiliations.
|
|
* All rights reserved. See the file COPYING in the top-level source
|
|
* directory for licensing information.
|
|
* ****************************************************************************
|
|
*
|
|
* Black box testing of the Solver class of the C++ API.
|
|
*/
|
|
|
|
#include <algorithm>
|
|
#include <cmath>
|
|
|
|
#include "base/output.h"
|
|
#include "test_api.h"
|
|
|
|
namespace cvc5::internal {
|
|
|
|
namespace test {
|
|
|
|
class TestApiBlackSolver : public TestApi
|
|
{
|
|
};
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue416)
|
|
{
|
|
Solver slv;
|
|
slv.setOption("solve-bv-as-int", "sum");
|
|
slv.setOption("strings-exp", "true");
|
|
Sort s1 = slv.getStringSort();
|
|
Term t27 = slv.mkConst(s1, "_x50");
|
|
Term t333 = slv.mkRegexpAll();
|
|
Term t1243 = slv.mkTerm(Kind::STRING_REPLACE_RE_ALL, {t27, t333, t27});
|
|
Term t1291 = slv.mkTerm(Kind::EQUAL, {t1243, t27});
|
|
slv.assertFormula(t1291);
|
|
slv.checkSat();
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue435)
|
|
{
|
|
Solver slv;
|
|
slv.setOption("strings-exp", "true");
|
|
Sort s1 = slv.mkUninterpretedSort("_u0");
|
|
Sort s3 = slv.getBooleanSort();
|
|
Sort _p7 = slv.mkParamSort("_p7");
|
|
DatatypeDecl _dt5 = slv.mkDatatypeDecl("_dt5", {_p7});
|
|
DatatypeConstructorDecl _cons33 = slv.mkDatatypeConstructorDecl("_cons33");
|
|
_cons33.addSelector("_sel31", s1);
|
|
_cons33.addSelector("_sel32", _p7);
|
|
_dt5.addConstructor(_cons33);
|
|
std::vector<Sort> _s6 = slv.mkDatatypeSorts({_dt5});
|
|
Sort s6 = _s6[0];
|
|
Sort s21 = s6.instantiate({s3});
|
|
Sort s42 = slv.mkSequenceSort(s21);
|
|
Term t40 = slv.mkConst(s42, "_x64");
|
|
Term t75 = slv.mkTerm(Kind::SEQ_REV, {t40});
|
|
Term t91 = slv.mkTerm(Kind::SEQ_PREFIX, {t75, t40});
|
|
slv.checkSatAssuming({t91});
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, pow2Large1)
|
|
{
|
|
// Based on https://github.com/cvc5/cvc5-projects/issues/371
|
|
Sort s1 = d_solver.getStringSort();
|
|
Sort s2 = d_solver.getIntegerSort();
|
|
Sort s4 = d_solver.mkArraySort(s1, s2);
|
|
Sort s7 = d_solver.mkArraySort(s2, s1);
|
|
Term t10 = d_solver.mkInteger("68038927088685865242724985643");
|
|
Term t74 = d_solver.mkInteger("8416288636405");
|
|
std::vector<DatatypeConstructorDecl> ctors;
|
|
ctors.push_back(d_solver.mkDatatypeConstructorDecl("_x109"));
|
|
ctors.back().addSelector("_x108", s7);
|
|
ctors.push_back(d_solver.mkDatatypeConstructorDecl("_x113"));
|
|
ctors.back().addSelector("_x110", s4);
|
|
ctors.back().addSelector("_x111", s2);
|
|
ctors.back().addSelector("_x112", s7);
|
|
Sort s11 = d_solver.declareDatatype("_x107", ctors);
|
|
Term t82 = d_solver.mkConst(s11, "_x114");
|
|
Term t180 = d_solver.mkTerm(POW2, {t10});
|
|
Term t258 = d_solver.mkTerm(GEQ, {t74, t180});
|
|
d_solver.assertFormula(t258);
|
|
ASSERT_THROW(d_solver.simplify(t82), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, pow2Large2)
|
|
{
|
|
// Based on https://github.com/cvc5/cvc5-projects/issues/333
|
|
Term t1 = d_solver.mkBitVector(63, ~(((uint64_t)1) << 62));
|
|
Term t2 = d_solver.mkTerm(Kind::BITVECTOR_TO_NAT, {t1});
|
|
Term t3 = d_solver.mkTerm(Kind::POW2, {t2});
|
|
Term t4 = d_solver.mkTerm(Kind::DISTINCT, {t3, t2});
|
|
ASSERT_THROW(d_solver.checkSatAssuming({t4}), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, pow2Large3)
|
|
{
|
|
// Based on https://github.com/cvc5/cvc5-projects/issues/339
|
|
Sort s4 = d_solver.getIntegerSort();
|
|
Term t203 = d_solver.mkInteger("6135470354240554220207");
|
|
Term t262 = d_solver.mkTerm(POW2, {t203});
|
|
Term t536 = d_solver.mkTerm(d_solver.mkOp(INT_TO_BITVECTOR, {49}), {t262});
|
|
ASSERT_THROW(d_solver.simplify(t536), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, recoverableException)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
|
|
d_solver.assertFormula(x.eqTerm(x).notTerm());
|
|
ASSERT_THROW(d_solver.getValue(x), CVC5ApiRecoverableException);
|
|
|
|
try {
|
|
d_solver.getValue(x);
|
|
}
|
|
catch (const CVC5ApiRecoverableException& e)
|
|
{
|
|
ASSERT_NO_THROW(e.what());
|
|
ASSERT_NO_THROW(e.getMessage());
|
|
}
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, supportsFloatingPoint)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getBooleanSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.getBooleanSort());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getIntegerSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.getIntegerSort());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getRealSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.getRealSort());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getRegExpSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.getRegExpSort());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getStringSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.getStringSort());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getRoundingModeSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.getRoundingModeSort());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkArraySort)
|
|
{
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort realSort = d_solver.getRealSort();
|
|
Sort bvSort = d_solver.mkBitVectorSort(32);
|
|
ASSERT_NO_THROW(d_solver.mkArraySort(boolSort, boolSort));
|
|
ASSERT_NO_THROW(d_solver.mkArraySort(intSort, intSort));
|
|
ASSERT_NO_THROW(d_solver.mkArraySort(realSort, realSort));
|
|
ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, bvSort));
|
|
ASSERT_NO_THROW(d_solver.mkArraySort(boolSort, intSort));
|
|
ASSERT_NO_THROW(d_solver.mkArraySort(realSort, bvSort));
|
|
|
|
Sort fpSort = d_solver.mkFloatingPointSort(3, 5);
|
|
ASSERT_NO_THROW(d_solver.mkArraySort(fpSort, fpSort));
|
|
ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, fpSort));
|
|
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkArraySort(boolSort, boolSort));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkBitVectorSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkBitVectorSort(32));
|
|
ASSERT_THROW(d_solver.mkBitVectorSort(0), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkFiniteFieldSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkFiniteFieldSort("31"));
|
|
ASSERT_THROW(d_solver.mkFiniteFieldSort("6"), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkFloatingPointSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8));
|
|
ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkFloatingPointSort(1, 8), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkFloatingPointSort(4, 1), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkDatatypeSort)
|
|
{
|
|
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
|
|
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
|
|
cons.addSelector("head", d_solver.getIntegerSort());
|
|
dtypeSpec.addConstructor(cons);
|
|
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
|
|
dtypeSpec.addConstructor(nil);
|
|
ASSERT_NO_THROW(d_solver.mkDatatypeSort(dtypeSpec));
|
|
|
|
ASSERT_THROW(d_solver.mkDatatypeSort(dtypeSpec), CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_THROW(slv.mkDatatypeSort(dtypeSpec), CVC5ApiException);
|
|
|
|
DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
|
|
ASSERT_THROW(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkDatatypeSorts)
|
|
{
|
|
Solver slv;
|
|
|
|
DatatypeDecl dtypeSpec1 = d_solver.mkDatatypeDecl("list1");
|
|
DatatypeConstructorDecl cons1 = d_solver.mkDatatypeConstructorDecl("cons1");
|
|
cons1.addSelector("head1", d_solver.getIntegerSort());
|
|
dtypeSpec1.addConstructor(cons1);
|
|
DatatypeConstructorDecl nil1 = d_solver.mkDatatypeConstructorDecl("nil1");
|
|
dtypeSpec1.addConstructor(nil1);
|
|
DatatypeDecl dtypeSpec2 = d_solver.mkDatatypeDecl("list2");
|
|
DatatypeConstructorDecl cons2 = d_solver.mkDatatypeConstructorDecl("cons2");
|
|
cons2.addSelector("head2", d_solver.getIntegerSort());
|
|
dtypeSpec2.addConstructor(cons2);
|
|
DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2");
|
|
dtypeSpec2.addConstructor(nil2);
|
|
std::vector<DatatypeDecl> decls = {dtypeSpec1, dtypeSpec2};
|
|
ASSERT_NO_THROW(d_solver.mkDatatypeSorts(decls));
|
|
|
|
ASSERT_THROW(d_solver.mkDatatypeSorts(decls), CVC5ApiException);
|
|
ASSERT_THROW(slv.mkDatatypeSorts(decls), CVC5ApiException);
|
|
|
|
DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
|
|
std::vector<DatatypeDecl> throwsDecls = {throwsDtypeSpec};
|
|
ASSERT_THROW(d_solver.mkDatatypeSorts(throwsDecls), CVC5ApiException);
|
|
|
|
/* with unresolved sorts */
|
|
Sort unresList = d_solver.mkUnresolvedDatatypeSort("ulist");
|
|
DatatypeDecl ulist = d_solver.mkDatatypeDecl("ulist");
|
|
DatatypeConstructorDecl ucons = d_solver.mkDatatypeConstructorDecl("ucons");
|
|
ucons.addSelector("car", unresList);
|
|
ucons.addSelector("cdr", unresList);
|
|
ulist.addConstructor(ucons);
|
|
DatatypeConstructorDecl unil = d_solver.mkDatatypeConstructorDecl("unil");
|
|
ulist.addConstructor(unil);
|
|
std::vector<DatatypeDecl> udecls = {ulist};
|
|
ASSERT_NO_THROW(d_solver.mkDatatypeSorts(udecls));
|
|
|
|
ASSERT_THROW(d_solver.mkDatatypeSorts(udecls), CVC5ApiException);
|
|
ASSERT_THROW(slv.mkDatatypeSorts(udecls), CVC5ApiException);
|
|
|
|
/* mutually recursive with unresolved parameterized sorts */
|
|
Sort p0 = d_solver.mkParamSort("p0");
|
|
Sort p1 = d_solver.mkParamSort("p1");
|
|
Sort u0 = d_solver.mkUnresolvedDatatypeSort("dt0", 1);
|
|
Sort u1 = d_solver.mkUnresolvedDatatypeSort("dt1", 1);
|
|
DatatypeDecl dtdecl0 = d_solver.mkDatatypeDecl("dt0", {p0});
|
|
DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("dt1", {p1});
|
|
DatatypeConstructorDecl ctordecl0 = d_solver.mkDatatypeConstructorDecl("c0");
|
|
ctordecl0.addSelector("s0", u1.instantiate({p0}));
|
|
DatatypeConstructorDecl ctordecl1 = d_solver.mkDatatypeConstructorDecl("c1");
|
|
ctordecl1.addSelector("s1", u0.instantiate({p1}));
|
|
dtdecl0.addConstructor(ctordecl0);
|
|
dtdecl1.addConstructor(ctordecl1);
|
|
dtdecl1.addConstructor(d_solver.mkDatatypeConstructorDecl("nil"));
|
|
std::vector<Sort> dt_sorts = d_solver.mkDatatypeSorts({dtdecl0, dtdecl1});
|
|
Sort isort1 = dt_sorts[1].instantiate({d_solver.getBooleanSort()});
|
|
Term t1 = d_solver.mkConst(isort1, "t");
|
|
Term t0 = d_solver.mkTerm(
|
|
APPLY_SELECTOR,
|
|
{t1.getSort().getDatatype().getSelector("s1").getTerm(), t1});
|
|
ASSERT_EQ(dt_sorts[0].instantiate({d_solver.getBooleanSort()}), t0.getSort());
|
|
|
|
/* Note: More tests are in datatype_api_black. */
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkFunctionSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
|
|
d_solver.getIntegerSort()));
|
|
Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
|
|
d_solver.getIntegerSort());
|
|
// function arguments are allowed
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkFunctionSort({funSort}, d_solver.getIntegerSort()));
|
|
// non-first-class arguments are not allowed
|
|
Sort reSort = d_solver.getRegExpSort();
|
|
ASSERT_THROW(d_solver.mkFunctionSort({reSort}, d_solver.getIntegerSort()),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkFunctionSort({d_solver.getIntegerSort()}, funSort),
|
|
CVC5ApiException);
|
|
ASSERT_NO_THROW(d_solver.mkFunctionSort(
|
|
{d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()},
|
|
d_solver.getIntegerSort()));
|
|
Sort funSort2 = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
|
|
d_solver.getIntegerSort());
|
|
// function arguments are allowed
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")},
|
|
d_solver.getIntegerSort()));
|
|
ASSERT_THROW(d_solver.mkFunctionSort({d_solver.getIntegerSort(),
|
|
d_solver.mkUninterpretedSort("u")},
|
|
funSort2),
|
|
CVC5ApiException);
|
|
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
|
|
d_solver.getIntegerSort()));
|
|
ASSERT_NO_THROW(slv.mkFunctionSort({slv.mkUninterpretedSort("u")},
|
|
d_solver.getIntegerSort()));
|
|
std::vector<Sort> sorts1 = {d_solver.getBooleanSort(),
|
|
slv.getIntegerSort(),
|
|
d_solver.getIntegerSort()};
|
|
std::vector<Sort> sorts2 = {slv.getBooleanSort(), slv.getIntegerSort()};
|
|
ASSERT_NO_THROW(slv.mkFunctionSort(sorts2, slv.getIntegerSort()));
|
|
ASSERT_NO_THROW(slv.mkFunctionSort(sorts1, slv.getIntegerSort()));
|
|
ASSERT_NO_THROW(slv.mkFunctionSort(sorts2, d_solver.getIntegerSort()));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkParamSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkParamSort("T"));
|
|
ASSERT_NO_THROW(d_solver.mkParamSort(""));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkPredicateSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
|
|
ASSERT_THROW(d_solver.mkPredicateSort({}), CVC5ApiException);
|
|
Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
|
|
d_solver.getIntegerSort());
|
|
// functions as arguments are allowed
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}));
|
|
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkPredicateSort({d_solver.getIntegerSort()}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkRecordSort)
|
|
{
|
|
std::vector<std::pair<std::string, Sort>> fields = {
|
|
std::make_pair("b", d_solver.getBooleanSort()),
|
|
std::make_pair("bv", d_solver.mkBitVectorSort(8)),
|
|
std::make_pair("i", d_solver.getIntegerSort())};
|
|
std::vector<std::pair<std::string, Sort>> empty;
|
|
ASSERT_NO_THROW(d_solver.mkRecordSort(fields));
|
|
ASSERT_NO_THROW(d_solver.mkRecordSort(empty));
|
|
Sort recSort = d_solver.mkRecordSort(fields);
|
|
ASSERT_NO_THROW(recSort.getDatatype());
|
|
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkRecordSort(fields));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkSetSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getBooleanSort()));
|
|
ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getIntegerSort()));
|
|
ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.mkBitVectorSort(4)));
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkSetSort(d_solver.mkBitVectorSort(4)));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkBagSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getBooleanSort()));
|
|
ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getIntegerSort()));
|
|
ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.mkBitVectorSort(4)));
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkBagSort(d_solver.mkBitVectorSort(4)));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkSequenceSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkSequenceSort(d_solver.getBooleanSort()));
|
|
ASSERT_NO_THROW(d_solver.mkSequenceSort(
|
|
d_solver.mkSequenceSort(d_solver.getIntegerSort())));
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkSequenceSort(d_solver.getIntegerSort()));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkAbstractSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkAbstractSort(ARRAY_SORT));
|
|
ASSERT_NO_THROW(d_solver.mkAbstractSort(BITVECTOR_SORT));
|
|
ASSERT_NO_THROW(d_solver.mkAbstractSort(TUPLE_SORT));
|
|
ASSERT_NO_THROW(d_solver.mkAbstractSort(SET_SORT));
|
|
ASSERT_THROW(d_solver.mkAbstractSort(BOOLEAN_SORT), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkUninterpretedSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkUninterpretedSort("u"));
|
|
ASSERT_NO_THROW(d_solver.mkUninterpretedSort(""));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkUnresolvedDatatypeSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort("u"));
|
|
ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort("u", 1));
|
|
ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort(""));
|
|
ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort("", 1));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkUninterpretedSortConstructorSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkUninterpretedSortConstructorSort(2, "s"));
|
|
ASSERT_NO_THROW(d_solver.mkUninterpretedSortConstructorSort(2, ""));
|
|
ASSERT_THROW(d_solver.mkUninterpretedSortConstructorSort(0),
|
|
CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkTupleSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
|
|
Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
|
|
d_solver.getIntegerSort());
|
|
ASSERT_NO_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}));
|
|
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkTupleSort({d_solver.getIntegerSort()}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkBitVector)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkBitVector(8, 2));
|
|
ASSERT_NO_THROW(d_solver.mkBitVector(32, 2));
|
|
ASSERT_NO_THROW(d_solver.mkBitVector(8, "-1111111", 2));
|
|
ASSERT_NO_THROW(d_solver.mkBitVector(8, "0101", 2));
|
|
ASSERT_NO_THROW(d_solver.mkBitVector(8, "00000101", 2));
|
|
ASSERT_NO_THROW(d_solver.mkBitVector(8, "-127", 10));
|
|
ASSERT_NO_THROW(d_solver.mkBitVector(8, "255", 10));
|
|
ASSERT_NO_THROW(d_solver.mkBitVector(8, "-7f", 16));
|
|
ASSERT_NO_THROW(d_solver.mkBitVector(8, "a0", 16));
|
|
|
|
ASSERT_THROW(d_solver.mkBitVector(0, 2), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(0, "-127", 10), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(0, "a0", 16), CVC5ApiException);
|
|
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "", 2), CVC5ApiException);
|
|
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "101", 5), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "128", 11), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "a0", 21), CVC5ApiException);
|
|
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "-11111111", 2), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "101010101", 2), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "-256", 10), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "257", 10), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "-a0", 16), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "fffff", 16), CVC5ApiException);
|
|
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "10201010", 2), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "-25x", 10), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "2x7", 10), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkBitVector(8, "fzff", 16), CVC5ApiException);
|
|
|
|
ASSERT_EQ(d_solver.mkBitVector(8, "0101", 2),
|
|
d_solver.mkBitVector(8, "00000101", 2));
|
|
ASSERT_EQ(d_solver.mkBitVector(4, "-1", 2),
|
|
d_solver.mkBitVector(4, "1111", 2));
|
|
ASSERT_EQ(d_solver.mkBitVector(4, "-1", 16),
|
|
d_solver.mkBitVector(4, "1111", 2));
|
|
ASSERT_EQ(d_solver.mkBitVector(4, "-1", 10),
|
|
d_solver.mkBitVector(4, "1111", 2));
|
|
ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101");
|
|
ASSERT_EQ(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111");
|
|
ASSERT_EQ(d_solver.mkBitVector(8, "-1", 10),
|
|
d_solver.mkBitVector(8, "FF", 16));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkFiniteFieldElem)
|
|
{
|
|
Sort f = d_solver.mkFiniteFieldSort("7");
|
|
Sort bv = d_solver.mkBitVectorSort(4);
|
|
|
|
ASSERT_NO_THROW(d_solver.mkFiniteFieldElem("0", f));
|
|
ASSERT_NO_THROW(d_solver.mkFiniteFieldElem("1", f));
|
|
ASSERT_NO_THROW(d_solver.mkFiniteFieldElem("6", f));
|
|
ASSERT_NO_THROW(d_solver.mkFiniteFieldElem("8", f));
|
|
ASSERT_NO_THROW(d_solver.mkFiniteFieldElem("-1", f));
|
|
|
|
ASSERT_THROW(d_solver.mkFiniteFieldElem("-1", bv), CVC5ApiException);
|
|
|
|
ASSERT_EQ(d_solver.mkFiniteFieldElem("-1", f),
|
|
d_solver.mkFiniteFieldElem("6", f));
|
|
ASSERT_EQ(d_solver.mkFiniteFieldElem("1", f),
|
|
d_solver.mkFiniteFieldElem("8", f));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkVar)
|
|
{
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort funSort = d_solver.mkFunctionSort({intSort}, boolSort);
|
|
ASSERT_NO_THROW(d_solver.mkVar(boolSort));
|
|
ASSERT_NO_THROW(d_solver.mkVar(funSort));
|
|
ASSERT_NO_THROW(d_solver.mkVar(boolSort, std::string("b")));
|
|
ASSERT_NO_THROW(d_solver.mkVar(funSort, ""));
|
|
ASSERT_THROW(d_solver.mkVar(Sort()), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkVar(Sort(), "a"), CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkVar(boolSort, "x"));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkBoolean)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkBoolean(true));
|
|
ASSERT_NO_THROW(d_solver.mkBoolean(false));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkRoundingMode)
|
|
{
|
|
ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN)
|
|
.toString(),
|
|
"roundNearestTiesToEven");
|
|
ASSERT_EQ(
|
|
d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE).toString(),
|
|
"roundTowardPositive");
|
|
ASSERT_EQ(
|
|
d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_NEGATIVE).toString(),
|
|
"roundTowardNegative");
|
|
ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO).toString(),
|
|
"roundTowardZero");
|
|
ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY)
|
|
.toString(),
|
|
"roundNearestTiesToAway");
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkFloatingPoint)
|
|
{
|
|
Term t1 = d_solver.mkBitVector(8);
|
|
Term t2 = d_solver.mkBitVector(4);
|
|
Term t3 = d_solver.mkInteger(2);
|
|
ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1));
|
|
ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, Term()), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, t1), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkFloatingPoint(3, 0, t1), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException);
|
|
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkFloatingPoint(3, 5, t1));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkCardinalityConstraint)
|
|
{
|
|
Sort su = d_solver.mkUninterpretedSort("u");
|
|
Sort si = d_solver.getIntegerSort();
|
|
ASSERT_NO_THROW(d_solver.mkCardinalityConstraint(su, 3));
|
|
ASSERT_THROW(d_solver.mkCardinalityConstraint(si, 3), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkCardinalityConstraint(su, 0), CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkCardinalityConstraint(su, 3));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkEmptySet)
|
|
{
|
|
Sort s = d_solver.mkSetSort(d_solver.getBooleanSort());
|
|
ASSERT_THROW(d_solver.mkEmptySet(Sort()), CVC5ApiException);
|
|
ASSERT_NO_THROW(d_solver.mkEmptySet(s));
|
|
ASSERT_THROW(d_solver.mkEmptySet(d_solver.getBooleanSort()),
|
|
CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkEmptySet(s));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkEmptyBag)
|
|
{
|
|
Sort s = d_solver.mkBagSort(d_solver.getBooleanSort());
|
|
ASSERT_THROW(d_solver.mkEmptyBag(Sort()), CVC5ApiException);
|
|
ASSERT_NO_THROW(d_solver.mkEmptyBag(s));
|
|
ASSERT_THROW(d_solver.mkEmptyBag(d_solver.getBooleanSort()),
|
|
CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkEmptyBag(s));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkEmptySequence)
|
|
{
|
|
Sort s = d_solver.mkSequenceSort(d_solver.getBooleanSort());
|
|
ASSERT_NO_THROW(d_solver.mkEmptySequence(s));
|
|
ASSERT_NO_THROW(d_solver.mkEmptySequence(d_solver.getBooleanSort()));
|
|
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkEmptySequence(s));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkFalse)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkFalse());
|
|
ASSERT_NO_THROW(d_solver.mkFalse());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkFloatingPointNaN)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkFloatingPointNaN(3, 5));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkFloatingPointNegZero)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkFloatingPointNegZero(3, 5));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkFloatingPointNegInf)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkFloatingPointNegInf(3, 5));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkFloatingPointPosInf)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkFloatingPointPosInf(3, 5));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkFloatingPointPosZero)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkFloatingPointPosZero(3, 5));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkOp)
|
|
{
|
|
// mkOp(Kind kind, const std::string& arg)
|
|
ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, "2147483648"));
|
|
ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"), CVC5ApiException);
|
|
|
|
// mkOp(Kind kind, std::vector<uint32_t> args)
|
|
ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, {1}));
|
|
ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_LEFT, {1}));
|
|
ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, {1}));
|
|
ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, {1}), CVC5ApiException);
|
|
|
|
ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, {1, 1}));
|
|
ASSERT_THROW(d_solver.mkOp(DIVISIBLE, {1, 2}), CVC5ApiException);
|
|
|
|
ASSERT_NO_THROW(d_solver.mkOp(TUPLE_PROJECT, {1, 2, 2}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); }
|
|
|
|
TEST_F(TestApiBlackSolver, mkInteger)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkInteger("123"));
|
|
ASSERT_THROW(d_solver.mkInteger("1.23"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger("1/23"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger("12/3"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(".2"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger("2."), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(""), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger("asdf"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger("1.2/3"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger("."), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger("/"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger("2/"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger("/2"), CVC5ApiException);
|
|
|
|
ASSERT_NO_THROW(d_solver.mkReal(std::string("123")));
|
|
ASSERT_THROW(d_solver.mkInteger(std::string("1.23")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(std::string("1/23")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(std::string("12/3")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(std::string(".2")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(std::string("2.")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(std::string("")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(std::string("asdf")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(std::string("1.2/3")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(std::string(".")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(std::string("/")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(std::string("2/")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkInteger(std::string("/2")), CVC5ApiException);
|
|
|
|
int32_t val1 = 1;
|
|
int64_t val2 = -1;
|
|
uint32_t val3 = 1;
|
|
uint64_t val4 = -1;
|
|
ASSERT_NO_THROW(d_solver.mkInteger(val1));
|
|
ASSERT_NO_THROW(d_solver.mkInteger(val2));
|
|
ASSERT_NO_THROW(d_solver.mkInteger(val3));
|
|
ASSERT_NO_THROW(d_solver.mkInteger(val4));
|
|
ASSERT_NO_THROW(d_solver.mkInteger(val4));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkReal)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkReal("123"));
|
|
ASSERT_NO_THROW(d_solver.mkReal("1.23"));
|
|
ASSERT_NO_THROW(d_solver.mkReal("1/23"));
|
|
ASSERT_NO_THROW(d_solver.mkReal("12/3"));
|
|
ASSERT_NO_THROW(d_solver.mkReal(".2"));
|
|
ASSERT_NO_THROW(d_solver.mkReal("2."));
|
|
ASSERT_THROW(d_solver.mkReal(""), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal("asdf"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal("1.2/3"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal("."), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal("/"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal("2/"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal("/2"), CVC5ApiException);
|
|
|
|
ASSERT_NO_THROW(d_solver.mkReal(std::string("123")));
|
|
ASSERT_NO_THROW(d_solver.mkReal(std::string("1.23")));
|
|
ASSERT_NO_THROW(d_solver.mkReal(std::string("1/23")));
|
|
ASSERT_NO_THROW(d_solver.mkReal(std::string("12/3")));
|
|
ASSERT_NO_THROW(d_solver.mkReal(std::string(".2")));
|
|
ASSERT_NO_THROW(d_solver.mkReal(std::string("2.")));
|
|
ASSERT_THROW(d_solver.mkReal(std::string("")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal(std::string("asdf")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal(std::string("1.2/3")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal(std::string(".")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal(std::string("/")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal(std::string("2/")), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkReal(std::string("/2")), CVC5ApiException);
|
|
|
|
int32_t val1 = 1;
|
|
int64_t val2 = -1;
|
|
uint32_t val3 = 1;
|
|
uint64_t val4 = -1;
|
|
ASSERT_NO_THROW(d_solver.mkReal(val1));
|
|
ASSERT_NO_THROW(d_solver.mkReal(val2));
|
|
ASSERT_NO_THROW(d_solver.mkReal(val3));
|
|
ASSERT_NO_THROW(d_solver.mkReal(val4));
|
|
ASSERT_NO_THROW(d_solver.mkReal(val4));
|
|
ASSERT_NO_THROW(d_solver.mkReal(val1, val1));
|
|
ASSERT_NO_THROW(d_solver.mkReal(val2, val2));
|
|
ASSERT_NO_THROW(d_solver.mkReal(val3, val3));
|
|
ASSERT_NO_THROW(d_solver.mkReal(val4, val4));
|
|
ASSERT_NO_THROW(d_solver.mkReal("-1/-1"));
|
|
ASSERT_NO_THROW(d_solver.mkReal("1/-1"));
|
|
ASSERT_NO_THROW(d_solver.mkReal("-1/1"));
|
|
ASSERT_NO_THROW(d_solver.mkReal("1/1"));
|
|
ASSERT_THROW(d_solver.mkReal("/-5"), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkRegexpAll)
|
|
{
|
|
Sort strSort = d_solver.getStringSort();
|
|
Term s = d_solver.mkConst(strSort, "s");
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(STRING_IN_REGEXP, {s, d_solver.mkRegexpAll()}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkRegexpAllchar)
|
|
{
|
|
Sort strSort = d_solver.getStringSort();
|
|
Term s = d_solver.mkConst(strSort, "s");
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(STRING_IN_REGEXP, {s, d_solver.mkRegexpAllchar()}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkRegexpNone)
|
|
{
|
|
Sort strSort = d_solver.getStringSort();
|
|
Term s = d_solver.mkConst(strSort, "s");
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(STRING_IN_REGEXP, {s, d_solver.mkRegexpNone()}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); }
|
|
|
|
TEST_F(TestApiBlackSolver, mkSepNil)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort()));
|
|
ASSERT_THROW(d_solver.mkSepNil(Sort()), CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkSepNil(d_solver.getIntegerSort()));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkString)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkString(""));
|
|
ASSERT_NO_THROW(d_solver.mkString("asdfasdf"));
|
|
ASSERT_EQ(d_solver.mkString("asdf\\nasdf").toString(),
|
|
"\"asdf\\u{5c}nasdf\"");
|
|
ASSERT_EQ(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(),
|
|
"\"asdf\\u{5c}nasdf\"");
|
|
std::wstring s;
|
|
ASSERT_EQ(d_solver.mkString(s).getStringValue(), s);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkTerm)
|
|
{
|
|
Sort bv32 = d_solver.mkBitVectorSort(32);
|
|
Term a = d_solver.mkConst(bv32, "a");
|
|
Term b = d_solver.mkConst(bv32, "b");
|
|
std::vector<Term> v1 = {a, b};
|
|
std::vector<Term> v2 = {a, Term()};
|
|
std::vector<Term> v3 = {a, d_solver.mkTrue()};
|
|
std::vector<Term> v4 = {d_solver.mkInteger(1), d_solver.mkInteger(2)};
|
|
std::vector<Term> v5 = {d_solver.mkInteger(1), Term()};
|
|
std::vector<Term> v6 = {};
|
|
Solver slv;
|
|
|
|
// mkTerm(Kind kind) const
|
|
ASSERT_NO_THROW(d_solver.mkTerm(PI));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(PI, {v6}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(PI)));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(PI), {v6}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_NONE));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_NONE, {v6}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_NONE)));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_NONE), {v6}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_ALLCHAR));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_ALLCHAR, {v6}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_ALLCHAR)));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_ALLCHAR), {v6}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(SEP_EMP));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(SEP_EMP, {v6}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(SEP_EMP)));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(SEP_EMP), {v6}));
|
|
ASSERT_THROW(d_solver.mkTerm(CONST_BITVECTOR), CVC5ApiException);
|
|
|
|
// mkTerm(Kind kind, Term child) const
|
|
ASSERT_NO_THROW(d_solver.mkTerm(NOT, {d_solver.mkTrue()}));
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(BAG_MAKE, {d_solver.mkTrue(), d_solver.mkInteger(1)}));
|
|
ASSERT_THROW(d_solver.mkTerm(NOT, {Term()}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(NOT, {a}), CVC5ApiException);
|
|
ASSERT_NO_THROW(slv.mkTerm(NOT, {d_solver.mkTrue()}));
|
|
|
|
// mkTerm(Kind kind, Term child1, Term child2) const
|
|
ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, {a, b}));
|
|
ASSERT_THROW(d_solver.mkTerm(EQUAL, {Term(), b}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(EQUAL, {a, Term()}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(EQUAL, {a, d_solver.mkTrue()}),
|
|
CVC5ApiException);
|
|
ASSERT_NO_THROW(slv.mkTerm(EQUAL, {a, b}));
|
|
|
|
// mkTerm(Kind kind, Term child1, Term child2, Term child3) const
|
|
ASSERT_NO_THROW(d_solver.mkTerm(
|
|
ITE, {d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()}));
|
|
ASSERT_THROW(
|
|
d_solver.mkTerm(ITE, {Term(), d_solver.mkTrue(), d_solver.mkTrue()}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(
|
|
d_solver.mkTerm(ITE, {d_solver.mkTrue(), Term(), d_solver.mkTrue()}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(
|
|
d_solver.mkTerm(ITE, {d_solver.mkTrue(), d_solver.mkTrue(), Term()}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(ITE, {d_solver.mkTrue(), d_solver.mkTrue(), b}),
|
|
CVC5ApiException);
|
|
ASSERT_NO_THROW(slv.mkTerm(
|
|
ITE, {d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()}));
|
|
|
|
// mkTerm(Kind kind, const std::vector<Term>& children) const
|
|
ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, {v1}));
|
|
ASSERT_THROW(d_solver.mkTerm(EQUAL, {v2}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(EQUAL, {v3}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(DISTINCT, {v6}), CVC5ApiException);
|
|
|
|
// Test cases that are nary via the API but have arity = 2 internally
|
|
Sort s_bool = d_solver.getBooleanSort();
|
|
Term t_bool = d_solver.mkConst(s_bool, "t_bool");
|
|
ASSERT_NO_THROW(d_solver.mkTerm(IMPLIES, {t_bool, t_bool, t_bool}));
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(d_solver.mkOp(IMPLIES), {t_bool, t_bool, t_bool}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(XOR, {t_bool, t_bool, t_bool}));
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(d_solver.mkOp(XOR), {t_bool, t_bool, t_bool}));
|
|
Term t_int = d_solver.mkConst(d_solver.getIntegerSort(), "t_int");
|
|
ASSERT_NO_THROW(d_solver.mkTerm(DIVISION, {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(d_solver.mkOp(DIVISION), {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(INTS_DIVISION, {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(d_solver.mkOp(INTS_DIVISION), {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(SUB, {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(SUB), {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(EQUAL), {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(LT, {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(LT), {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(GT, {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(GT), {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(LEQ, {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(LEQ), {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(GEQ, {t_int, t_int, t_int}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(GEQ), {t_int, t_int, t_int}));
|
|
Term t_reg = d_solver.mkConst(d_solver.getRegExpSort(), "t_reg");
|
|
ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_DIFF, {t_reg, t_reg, t_reg}));
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(d_solver.mkOp(REGEXP_DIFF), {t_reg, t_reg, t_reg}));
|
|
Term t_fun = d_solver.mkConst(
|
|
d_solver.mkFunctionSort({s_bool, s_bool, s_bool}, s_bool));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(HO_APPLY, {t_fun, t_bool, t_bool, t_bool}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(HO_APPLY),
|
|
{t_fun, t_bool, t_bool, t_bool}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkTermFromOp)
|
|
{
|
|
Sort bv32 = d_solver.mkBitVectorSort(32);
|
|
Term a = d_solver.mkConst(bv32, "a");
|
|
Term b = d_solver.mkConst(bv32, "b");
|
|
std::vector<Term> v1 = {d_solver.mkInteger(1), d_solver.mkInteger(2)};
|
|
std::vector<Term> v2 = {d_solver.mkInteger(1), Term()};
|
|
std::vector<Term> v3 = {};
|
|
std::vector<Term> v4 = {d_solver.mkInteger(5)};
|
|
Solver slv;
|
|
|
|
// simple operator terms
|
|
Op opterm1 = d_solver.mkOp(BITVECTOR_EXTRACT, {2, 1});
|
|
Op opterm2 = d_solver.mkOp(DIVISIBLE, {1});
|
|
|
|
// list datatype
|
|
Sort sort = d_solver.mkParamSort("T");
|
|
DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", {sort});
|
|
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
|
|
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
|
|
cons.addSelector("head", sort);
|
|
cons.addSelectorSelf("tail");
|
|
listDecl.addConstructor(cons);
|
|
listDecl.addConstructor(nil);
|
|
Sort listSort = d_solver.mkDatatypeSort(listDecl);
|
|
Sort intListSort =
|
|
listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
|
|
Term c = d_solver.mkConst(intListSort, "c");
|
|
Datatype list = listSort.getDatatype();
|
|
|
|
// list datatype constructor and selector operator terms
|
|
Term consTerm = list.getConstructor("cons").getTerm();
|
|
Term nilTerm = list.getConstructor("nil").getTerm();
|
|
Term headTerm = list["cons"].getSelector("head").getTerm();
|
|
Term tailTerm = list["cons"]["tail"].getTerm();
|
|
|
|
// mkTerm(Op op, Term term) const
|
|
ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}));
|
|
ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {nilTerm}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {consTerm}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {headTerm}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException);
|
|
ASSERT_NO_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}));
|
|
|
|
// mkTerm(Op op, Term child) const
|
|
ASSERT_NO_THROW(d_solver.mkTerm(opterm1, {a}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(opterm2, {d_solver.mkInteger(1)}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {headTerm, c}));
|
|
ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {tailTerm, c}));
|
|
ASSERT_THROW(d_solver.mkTerm(opterm2, {a}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(opterm1, {Term()}), CVC5ApiException);
|
|
ASSERT_THROW(
|
|
d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm, d_solver.mkInteger(0)}),
|
|
CVC5ApiException);
|
|
ASSERT_NO_THROW(slv.mkTerm(opterm1, {a}));
|
|
|
|
// mkTerm(Op op, Term child1, Term child2) const
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(APPLY_CONSTRUCTOR,
|
|
{consTerm,
|
|
d_solver.mkInteger(0),
|
|
d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm})}));
|
|
ASSERT_THROW(
|
|
d_solver.mkTerm(opterm2, {d_solver.mkInteger(1), d_solver.mkInteger(2)}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(opterm1, {a, b}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(opterm2, {d_solver.mkInteger(1), Term()}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(opterm2, {Term(), d_solver.mkInteger(1)}),
|
|
CVC5ApiException);
|
|
ASSERT_NO_THROW(slv.mkTerm(APPLY_CONSTRUCTOR,
|
|
{consTerm,
|
|
d_solver.mkInteger(0),
|
|
d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm})}));
|
|
|
|
// mkTerm(Op op, Term child1, Term child2, Term child3) const
|
|
ASSERT_THROW(d_solver.mkTerm(opterm1, {a, b, a}), CVC5ApiException);
|
|
ASSERT_THROW(
|
|
d_solver.mkTerm(opterm2,
|
|
{d_solver.mkInteger(1), d_solver.mkInteger(1), Term()}),
|
|
CVC5ApiException);
|
|
|
|
// mkTerm(Op op, const std::vector<Term>& children) const
|
|
ASSERT_NO_THROW(d_solver.mkTerm(opterm2, {v4}));
|
|
ASSERT_THROW(d_solver.mkTerm(opterm2, {v1}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(opterm2, {v2}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(opterm2, {v3}), CVC5ApiException);
|
|
ASSERT_NO_THROW(slv.mkTerm(opterm2, {v4}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkTrue)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkTrue());
|
|
ASSERT_NO_THROW(d_solver.mkTrue());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkTuple)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(3)},
|
|
{d_solver.mkBitVector(3, "101", 2)}));
|
|
ASSERT_THROW(
|
|
d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkInteger("5")}),
|
|
CVC5ApiException);
|
|
|
|
ASSERT_THROW(d_solver.mkTuple({}, {d_solver.mkBitVector(3, "101", 2)}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(4)},
|
|
{d_solver.mkBitVector(3, "101", 2)}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(
|
|
d_solver.mkTuple({d_solver.getIntegerSort()}, {d_solver.mkReal("5.3")}),
|
|
CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkTuple({d_solver.mkBitVectorSort(3)},
|
|
{slv.mkBitVector(3, "101", 2)}));
|
|
ASSERT_NO_THROW(slv.mkTuple({slv.mkBitVectorSort(3)},
|
|
{d_solver.mkBitVector(3, "101", 2)}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkUniverseSet)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.mkUniverseSet(d_solver.getBooleanSort()));
|
|
ASSERT_THROW(d_solver.mkUniverseSet(Sort()), CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkUniverseSet(d_solver.getBooleanSort()));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkConst)
|
|
{
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort funSort = d_solver.mkFunctionSort({intSort}, boolSort);
|
|
ASSERT_NO_THROW(d_solver.mkConst(boolSort));
|
|
ASSERT_NO_THROW(d_solver.mkConst(funSort));
|
|
ASSERT_NO_THROW(d_solver.mkConst(boolSort, std::string("b")));
|
|
ASSERT_NO_THROW(d_solver.mkConst(intSort, std::string("i")));
|
|
ASSERT_NO_THROW(d_solver.mkConst(funSort, "f"));
|
|
ASSERT_NO_THROW(d_solver.mkConst(funSort, ""));
|
|
ASSERT_THROW(d_solver.mkConst(Sort()), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkConst(Sort(), "a"), CVC5ApiException);
|
|
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.mkConst(boolSort));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkConstArray)
|
|
{
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort arrSort = d_solver.mkArraySort(intSort, intSort);
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term constArr = d_solver.mkConstArray(arrSort, zero);
|
|
|
|
ASSERT_NO_THROW(d_solver.mkConstArray(arrSort, zero));
|
|
ASSERT_THROW(d_solver.mkConstArray(Sort(), zero), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkConstArray(arrSort, Term()), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkConstArray(arrSort, d_solver.mkBitVector(1, 1)),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkConstArray(intSort, zero), CVC5ApiException);
|
|
Solver slv;
|
|
Term zero2 = slv.mkInteger(0);
|
|
Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
|
|
ASSERT_NO_THROW(slv.mkConstArray(arrSort2, zero));
|
|
ASSERT_NO_THROW(slv.mkConstArray(arrSort, zero2));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, declareDatatype)
|
|
{
|
|
DatatypeConstructorDecl lin = d_solver.mkDatatypeConstructorDecl("lin");
|
|
std::vector<DatatypeConstructorDecl> ctors0 = {lin};
|
|
ASSERT_NO_THROW(d_solver.declareDatatype(std::string(""), ctors0));
|
|
|
|
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
|
|
std::vector<DatatypeConstructorDecl> ctors1 = {nil};
|
|
ASSERT_NO_THROW(d_solver.declareDatatype(std::string("a"), ctors1));
|
|
|
|
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
|
|
DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil");
|
|
std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2};
|
|
ASSERT_NO_THROW(d_solver.declareDatatype(std::string("b"), ctors2));
|
|
|
|
DatatypeConstructorDecl cons2 = d_solver.mkDatatypeConstructorDecl("cons");
|
|
DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil");
|
|
std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3};
|
|
ASSERT_NO_THROW(d_solver.declareDatatype(std::string(""), ctors3));
|
|
|
|
// must have at least one constructor
|
|
std::vector<DatatypeConstructorDecl> ctors4;
|
|
ASSERT_THROW(d_solver.declareDatatype(std::string("c"), ctors4),
|
|
CVC5ApiException);
|
|
// constructors may not be reused
|
|
DatatypeConstructorDecl ctor1 = d_solver.mkDatatypeConstructorDecl("_x21");
|
|
DatatypeConstructorDecl ctor2 = d_solver.mkDatatypeConstructorDecl("_x31");
|
|
Sort s3 = d_solver.declareDatatype(std::string("_x17"), {ctor1, ctor2});
|
|
ASSERT_THROW(d_solver.declareDatatype(std::string("_x86"), {ctor1, ctor2}),
|
|
CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_THROW(slv.declareDatatype(std::string("a"), ctors1), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, declareFun)
|
|
{
|
|
Sort bvSort = d_solver.mkBitVectorSort(32);
|
|
Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
|
|
d_solver.getIntegerSort());
|
|
ASSERT_NO_THROW(d_solver.declareFun("f1", {}, bvSort));
|
|
ASSERT_NO_THROW(
|
|
d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort));
|
|
ASSERT_THROW(d_solver.declareFun("f2", {}, funSort), CVC5ApiException);
|
|
// functions as arguments is allowed
|
|
ASSERT_NO_THROW(d_solver.declareFun("f4", {bvSort, funSort}, bvSort));
|
|
ASSERT_THROW(d_solver.declareFun("f5", {bvSort, bvSort}, funSort),
|
|
CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.declareFun("f1", {}, bvSort));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, declareSort)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.declareSort("s", 0));
|
|
ASSERT_NO_THROW(d_solver.declareSort("s", 2));
|
|
ASSERT_NO_THROW(d_solver.declareSort("", 2));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, defineSort)
|
|
{
|
|
Sort sortVar0 = d_solver.mkParamSort("T0");
|
|
Sort sortVar1 = d_solver.mkParamSort("T1");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort realSort = d_solver.getRealSort();
|
|
Sort arraySort0 = d_solver.mkArraySort(sortVar0, sortVar0);
|
|
Sort arraySort1 = d_solver.mkArraySort(sortVar0, sortVar1);
|
|
// Now create instantiations of the defined sorts
|
|
ASSERT_NO_THROW(arraySort0.substitute(sortVar0, intSort));
|
|
ASSERT_NO_THROW(
|
|
arraySort1.substitute({sortVar0, sortVar1}, {intSort, realSort}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, defineFun)
|
|
{
|
|
Sort bvSort = d_solver.mkBitVectorSort(32);
|
|
Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
|
|
d_solver.getIntegerSort());
|
|
Term b1 = d_solver.mkVar(bvSort, "b1");
|
|
Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
|
|
Term b3 = d_solver.mkVar(funSort, "b3");
|
|
Term v1 = d_solver.mkConst(bvSort, "v1");
|
|
Term v2 = d_solver.mkConst(funSort, "v2");
|
|
ASSERT_NO_THROW(d_solver.defineFun("f", {}, bvSort, v1));
|
|
ASSERT_NO_THROW(d_solver.defineFun("ff", {b1, b2}, bvSort, v1));
|
|
ASSERT_THROW(d_solver.defineFun("ff", {v1, b2}, bvSort, v1),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFun("fff", {b1}, bvSort, v2), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFun("ffff", {b1}, funSort, v2), CVC5ApiException);
|
|
// b3 has function sort, which is allowed as an argument
|
|
ASSERT_NO_THROW(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1));
|
|
|
|
Solver slv;
|
|
Sort bvSort2 = slv.mkBitVectorSort(32);
|
|
Term v12 = slv.mkConst(bvSort2, "v1");
|
|
Term b12 = slv.mkVar(bvSort2, "b1");
|
|
Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
|
|
ASSERT_NO_THROW(slv.defineFun("f", {}, bvSort, v12));
|
|
ASSERT_NO_THROW(slv.defineFun("f", {}, bvSort2, v1));
|
|
ASSERT_NO_THROW(slv.defineFun("ff", {b1, b22}, bvSort2, v12));
|
|
ASSERT_NO_THROW(slv.defineFun("ff", {b12, b2}, bvSort2, v12));
|
|
ASSERT_NO_THROW(slv.defineFun("ff", {b12, b22}, bvSort, v12));
|
|
ASSERT_NO_THROW(slv.defineFun("ff", {b12, b22}, bvSort2, v1));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, defineFunGlobal)
|
|
{
|
|
Sort bSort = d_solver.getBooleanSort();
|
|
|
|
Term bTrue = d_solver.mkBoolean(true);
|
|
// (define-fun f () Bool true)
|
|
Term f = d_solver.defineFun("f", {}, bSort, bTrue, true);
|
|
Term b = d_solver.mkVar(bSort, "b");
|
|
// (define-fun g (b Bool) Bool b)
|
|
Term g = d_solver.defineFun("g", {b}, bSort, b, true);
|
|
|
|
// (assert (or (not f) (not (g true))))
|
|
d_solver.assertFormula(d_solver.mkTerm(
|
|
OR, {f.notTerm(), d_solver.mkTerm(APPLY_UF, {g, bTrue}).notTerm()}));
|
|
ASSERT_TRUE(d_solver.checkSat().isUnsat());
|
|
d_solver.resetAssertions();
|
|
// (assert (or (not f) (not (g true))))
|
|
d_solver.assertFormula(d_solver.mkTerm(
|
|
OR, {f.notTerm(), d_solver.mkTerm(APPLY_UF, {g, bTrue}).notTerm()}));
|
|
ASSERT_TRUE(d_solver.checkSat().isUnsat());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, defineFunRec)
|
|
{
|
|
Sort bvSort = d_solver.mkBitVectorSort(32);
|
|
Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
|
|
Sort funSort2 = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
|
|
d_solver.getIntegerSort());
|
|
Term b1 = d_solver.mkVar(bvSort, "b1");
|
|
Term b11 = d_solver.mkVar(bvSort, "b1");
|
|
Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
|
|
Term b3 = d_solver.mkVar(funSort2, "b3");
|
|
Term v1 = d_solver.mkConst(bvSort, "v1");
|
|
Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
|
|
Term v3 = d_solver.mkConst(funSort2, "v3");
|
|
Term f1 = d_solver.mkConst(funSort1, "f1");
|
|
Term f2 = d_solver.mkConst(funSort2, "f2");
|
|
Term f3 = d_solver.mkConst(bvSort, "f3");
|
|
ASSERT_NO_THROW(d_solver.defineFunRec("f", {}, bvSort, v1));
|
|
ASSERT_NO_THROW(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1));
|
|
ASSERT_NO_THROW(d_solver.defineFunRec(f1, {b1, b11}, v1));
|
|
ASSERT_THROW(d_solver.defineFunRec("fff", {b1}, bvSort, v3),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFunRec("ff", {b1, v2}, bvSort, v1),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFunRec("ffff", {b1}, funSort2, v3),
|
|
CVC5ApiException);
|
|
// b3 has function sort, which is allowed as an argument
|
|
ASSERT_NO_THROW(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1));
|
|
ASSERT_THROW(d_solver.defineFunRec(f1, {b1}, v1), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFunRec(f2, {b1}, v2), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFunRec(f3, {b1}, v1), CVC5ApiException);
|
|
|
|
Solver slv;
|
|
Sort bvSort2 = slv.mkBitVectorSort(32);
|
|
Term v12 = slv.mkConst(bvSort2, "v1");
|
|
Term b12 = slv.mkVar(bvSort2, "b1");
|
|
Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
|
|
ASSERT_NO_THROW(slv.defineFunRec("f", {}, bvSort2, v12));
|
|
ASSERT_NO_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v12));
|
|
ASSERT_NO_THROW(slv.defineFunRec("f", {}, bvSort, v12));
|
|
ASSERT_NO_THROW(slv.defineFunRec("f", {}, bvSort2, v1));
|
|
ASSERT_NO_THROW(slv.defineFunRec("ff", {b1, b22}, bvSort2, v12));
|
|
ASSERT_NO_THROW(slv.defineFunRec("ff", {b12, b2}, bvSort2, v12));
|
|
ASSERT_NO_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort, v12));
|
|
ASSERT_NO_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v1));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, defineFunRecWrongLogic)
|
|
{
|
|
d_solver.setLogic("QF_BV");
|
|
Sort bvSort = d_solver.mkBitVectorSort(32);
|
|
Sort funSort = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
|
|
Term b = d_solver.mkVar(bvSort, "b");
|
|
Term v = d_solver.mkConst(bvSort, "v");
|
|
Term f = d_solver.mkConst(funSort, "f");
|
|
ASSERT_THROW(d_solver.defineFunRec("f", {}, bvSort, v), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFunRec(f, {b, b}, v), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, defineFunRecGlobal)
|
|
{
|
|
Sort bSort = d_solver.getBooleanSort();
|
|
Sort fSort = d_solver.mkFunctionSort({bSort}, bSort);
|
|
|
|
d_solver.push();
|
|
Term bTrue = d_solver.mkBoolean(true);
|
|
// (define-fun f () Bool true)
|
|
Term f = d_solver.defineFunRec("f", {}, bSort, bTrue, true);
|
|
Term b = d_solver.mkVar(bSort, "b");
|
|
Term gSym = d_solver.mkConst(fSort, "g");
|
|
// (define-fun g (b Bool) Bool b)
|
|
Term g = d_solver.defineFunRec(gSym, {b}, b, true);
|
|
|
|
// (assert (or (not f) (not (g true))))
|
|
d_solver.assertFormula(d_solver.mkTerm(
|
|
OR, {f.notTerm(), d_solver.mkTerm(APPLY_UF, {g, bTrue}).notTerm()}));
|
|
ASSERT_TRUE(d_solver.checkSat().isUnsat());
|
|
d_solver.pop();
|
|
// (assert (or (not f) (not (g true))))
|
|
d_solver.assertFormula(d_solver.mkTerm(
|
|
OR, {f.notTerm(), d_solver.mkTerm(APPLY_UF, {g, bTrue}).notTerm()}));
|
|
ASSERT_TRUE(d_solver.checkSat().isUnsat());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, defineFunsRec)
|
|
{
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Sort bvSort = d_solver.mkBitVectorSort(32);
|
|
Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
|
|
Sort funSort2 = d_solver.mkFunctionSort({uSort}, d_solver.getIntegerSort());
|
|
Term b1 = d_solver.mkVar(bvSort, "b1");
|
|
Term b11 = d_solver.mkVar(bvSort, "b1");
|
|
Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
|
|
Term b3 = d_solver.mkVar(funSort2, "b3");
|
|
Term b4 = d_solver.mkVar(uSort, "b4");
|
|
Term v1 = d_solver.mkConst(bvSort, "v1");
|
|
Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
|
|
Term v3 = d_solver.mkConst(funSort2, "v3");
|
|
Term v4 = d_solver.mkConst(uSort, "v4");
|
|
Term f1 = d_solver.mkConst(funSort1, "f1");
|
|
Term f2 = d_solver.mkConst(funSort2, "f2");
|
|
Term f3 = d_solver.mkConst(bvSort, "f3");
|
|
ASSERT_NO_THROW(
|
|
d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
|
|
ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{v1, b11}, {b4}}, {v1, v2}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
|
|
CVC5ApiException);
|
|
|
|
Solver slv;
|
|
Sort uSort2 = slv.mkUninterpretedSort("u");
|
|
Sort bvSort2 = slv.mkBitVectorSort(32);
|
|
Sort funSort12 = slv.mkFunctionSort({bvSort2, bvSort2}, bvSort2);
|
|
Sort funSort22 = slv.mkFunctionSort({uSort2}, slv.getIntegerSort());
|
|
Term b12 = slv.mkVar(bvSort2, "b1");
|
|
Term b112 = slv.mkVar(bvSort2, "b1");
|
|
Term b42 = slv.mkVar(uSort2, "b4");
|
|
Term v12 = slv.mkConst(bvSort2, "v1");
|
|
Term v22 = slv.mkConst(slv.getIntegerSort(), "v2");
|
|
Term f12 = slv.mkConst(funSort12, "f1");
|
|
Term f22 = slv.mkConst(funSort22, "f2");
|
|
ASSERT_NO_THROW(
|
|
slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v22}));
|
|
ASSERT_NO_THROW(
|
|
slv.defineFunsRec({f1, f22}, {{b12, b112}, {b42}}, {v12, v22}));
|
|
ASSERT_THROW(slv.defineFunsRec({f12, f2}, {{b12, b112}, {b42}}, {v12, v22}),
|
|
CVC5ApiException);
|
|
ASSERT_NO_THROW(
|
|
slv.defineFunsRec({f12, f22}, {{b1, b112}, {b42}}, {v12, v22}));
|
|
ASSERT_NO_THROW(
|
|
slv.defineFunsRec({f12, f22}, {{b12, b11}, {b42}}, {v12, v22}));
|
|
ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b4}}, {v12, v22}),
|
|
CVC5ApiException);
|
|
ASSERT_NO_THROW(
|
|
slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v1, v22}));
|
|
ASSERT_NO_THROW(
|
|
slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v2}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic)
|
|
{
|
|
d_solver.setLogic("QF_BV");
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Sort bvSort = d_solver.mkBitVectorSort(32);
|
|
Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
|
|
Sort funSort2 = d_solver.mkFunctionSort({uSort}, d_solver.getIntegerSort());
|
|
Term b = d_solver.mkVar(bvSort, "b");
|
|
Term u = d_solver.mkVar(uSort, "u");
|
|
Term v1 = d_solver.mkConst(bvSort, "v1");
|
|
Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
|
|
Term f1 = d_solver.mkConst(funSort1, "f1");
|
|
Term f2 = d_solver.mkConst(funSort2, "f2");
|
|
ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b, b}, {u}}, {v1, v2}),
|
|
CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, defineFunsRecGlobal)
|
|
{
|
|
Sort bSort = d_solver.getBooleanSort();
|
|
Sort fSort = d_solver.mkFunctionSort({bSort}, bSort);
|
|
|
|
d_solver.push();
|
|
Term bTrue = d_solver.mkBoolean(true);
|
|
Term b = d_solver.mkVar(bSort, "b");
|
|
Term gSym = d_solver.mkConst(fSort, "g");
|
|
// (define-funs-rec ((g ((b Bool)) Bool)) (b))
|
|
d_solver.defineFunsRec({gSym}, {{b}}, {b}, true);
|
|
|
|
// (assert (not (g true)))
|
|
d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, {gSym, bTrue}).notTerm());
|
|
ASSERT_TRUE(d_solver.checkSat().isUnsat());
|
|
d_solver.pop();
|
|
// (assert (not (g true)))
|
|
d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, {gSym, bTrue}).notTerm());
|
|
ASSERT_TRUE(d_solver.checkSat().isUnsat());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, uFIteration)
|
|
{
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort funSort = d_solver.mkFunctionSort({intSort, intSort}, intSort);
|
|
Term x = d_solver.mkConst(intSort, "x");
|
|
Term y = d_solver.mkConst(intSort, "y");
|
|
Term f = d_solver.mkConst(funSort, "f");
|
|
Term fxy = d_solver.mkTerm(APPLY_UF, {f, x, y});
|
|
|
|
// Expecting the uninterpreted function to be one of the children
|
|
Term expected_children[3] = {f, x, y};
|
|
uint32_t idx = 0;
|
|
for (auto c : fxy)
|
|
{
|
|
ASSERT_LT(idx, 3);
|
|
ASSERT_EQ(c, expected_children[idx]);
|
|
idx++;
|
|
}
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getAssertions)
|
|
{
|
|
Term a = d_solver.mkConst(d_solver.getBooleanSort(), "a");
|
|
Term b = d_solver.mkConst(d_solver.getBooleanSort(), "b");
|
|
d_solver.assertFormula(a);
|
|
d_solver.assertFormula(b);
|
|
std::vector<Term> asserts{a, b};
|
|
ASSERT_EQ(d_solver.getAssertions(), asserts);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getInfo)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.getInfo("name"));
|
|
ASSERT_THROW(d_solver.getInfo("asdf"), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getAbduct)
|
|
{
|
|
d_solver.setLogic("QF_LIA");
|
|
d_solver.setOption("produce-abducts", "true");
|
|
d_solver.setOption("incremental", "false");
|
|
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term x = d_solver.mkConst(intSort, "x");
|
|
Term y = d_solver.mkConst(intSort, "y");
|
|
|
|
// Assumptions for abduction: x > 0
|
|
d_solver.assertFormula(d_solver.mkTerm(GT, {x, zero}));
|
|
// Conjecture for abduction: y > 0
|
|
Term conj = d_solver.mkTerm(GT, {y, zero});
|
|
// Call the abduction api, while the resulting abduct is the output
|
|
Term output = d_solver.getAbduct(conj);
|
|
// We expect the resulting output to be a boolean formula
|
|
ASSERT_TRUE(!output.isNull() && output.getSort().isBoolean());
|
|
|
|
// try with a grammar, a simple grammar admitting true
|
|
Sort boolean = d_solver.getBooleanSort();
|
|
Term truen = d_solver.mkBoolean(true);
|
|
Term start = d_solver.mkVar(boolean);
|
|
Term output2;
|
|
Grammar g = d_solver.mkGrammar({}, {start});
|
|
Term conj2 = d_solver.mkTerm(GT, {x, zero});
|
|
ASSERT_NO_THROW(g.addRule(start, truen));
|
|
// Call the abduction api, while the resulting abduct is the output
|
|
output2 = d_solver.getAbduct(conj2, g);
|
|
// abduct must be true
|
|
ASSERT_EQ(output2, truen);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getAbduct2)
|
|
{
|
|
d_solver.setLogic("QF_LIA");
|
|
d_solver.setOption("incremental", "false");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term x = d_solver.mkConst(intSort, "x");
|
|
Term y = d_solver.mkConst(intSort, "y");
|
|
// Assumptions for abduction: x > 0
|
|
d_solver.assertFormula(d_solver.mkTerm(GT, {x, zero}));
|
|
// Conjecture for abduction: y > 0
|
|
Term conj = d_solver.mkTerm(GT, {y, zero});
|
|
// Fails due to option not set
|
|
ASSERT_THROW(d_solver.getAbduct(conj), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getAbductNext)
|
|
{
|
|
d_solver.setLogic("QF_LIA");
|
|
d_solver.setOption("produce-abducts", "true");
|
|
d_solver.setOption("incremental", "true");
|
|
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term x = d_solver.mkConst(intSort, "x");
|
|
Term y = d_solver.mkConst(intSort, "y");
|
|
|
|
// Assumptions for abduction: x > 0
|
|
d_solver.assertFormula(d_solver.mkTerm(GT, {x, zero}));
|
|
// Conjecture for abduction: y > 0
|
|
Term conj = d_solver.mkTerm(GT, {y, zero});
|
|
// Call the abduction api, while the resulting abduct is the output
|
|
Term output = d_solver.getAbduct(conj);
|
|
Term output2 = d_solver.getAbductNext();
|
|
// should produce a different output
|
|
ASSERT_TRUE(output != output2);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getInterpolant)
|
|
{
|
|
d_solver.setLogic("QF_LIA");
|
|
d_solver.setOption("produce-interpolants", "true");
|
|
d_solver.setOption("incremental", "false");
|
|
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term x = d_solver.mkConst(intSort, "x");
|
|
Term y = d_solver.mkConst(intSort, "y");
|
|
Term z = d_solver.mkConst(intSort, "z");
|
|
|
|
// Assumptions for interpolation: x + y > 0 /\ x < 0
|
|
d_solver.assertFormula(
|
|
d_solver.mkTerm(GT, {d_solver.mkTerm(ADD, {x, y}), zero}));
|
|
d_solver.assertFormula(d_solver.mkTerm(LT, {x, zero}));
|
|
// Conjecture for interpolation: y + z > 0 \/ z < 0
|
|
Term conj = d_solver.mkTerm(
|
|
OR,
|
|
{d_solver.mkTerm(GT, {d_solver.mkTerm(ADD, {y, z}), zero}),
|
|
d_solver.mkTerm(LT, {z, zero})});
|
|
// Call the interpolation api, while the resulting interpolant is the output
|
|
Term output = d_solver.getInterpolant(conj);
|
|
// We expect the resulting output to be a boolean formula
|
|
ASSERT_TRUE(output.getSort().isBoolean());
|
|
|
|
// try with a grammar, a simple grammar admitting true
|
|
Sort boolean = d_solver.getBooleanSort();
|
|
Term truen = d_solver.mkBoolean(true);
|
|
Term start = d_solver.mkVar(boolean);
|
|
Grammar g = d_solver.mkGrammar({}, {start});
|
|
Term conj2 = d_solver.mkTerm(EQUAL, {zero, zero});
|
|
ASSERT_NO_THROW(g.addRule(start, truen));
|
|
// Call the interpolation api, while the resulting interpolant is the output
|
|
Term output2 = d_solver.getInterpolant(conj2, g);
|
|
// interpolant must be true
|
|
ASSERT_EQ(output2, truen);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getInterpolantNext)
|
|
{
|
|
d_solver.setLogic("QF_LIA");
|
|
d_solver.setOption("produce-interpolants", "true");
|
|
d_solver.setOption("incremental", "true");
|
|
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term x = d_solver.mkConst(intSort, "x");
|
|
Term y = d_solver.mkConst(intSort, "y");
|
|
Term z = d_solver.mkConst(intSort, "z");
|
|
// Assumptions for interpolation: x + y > 0 /\ x < 0
|
|
d_solver.assertFormula(
|
|
d_solver.mkTerm(GT, {d_solver.mkTerm(ADD, {x, y}), zero}));
|
|
d_solver.assertFormula(d_solver.mkTerm(LT, {x, zero}));
|
|
// Conjecture for interpolation: y + z > 0 \/ z < 0
|
|
Term conj = d_solver.mkTerm(
|
|
OR,
|
|
{d_solver.mkTerm(GT, {d_solver.mkTerm(ADD, {y, z}), zero}),
|
|
d_solver.mkTerm(LT, {z, zero})});
|
|
Term output = d_solver.getInterpolant(conj);
|
|
Term output2 = d_solver.getInterpolantNext();
|
|
|
|
// We expect the next output to be distinct
|
|
ASSERT_TRUE(output != output2);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, declarePool)
|
|
{
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort setSort = d_solver.mkSetSort(intSort);
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term x = d_solver.mkConst(intSort, "x");
|
|
Term y = d_solver.mkConst(intSort, "y");
|
|
// declare a pool with initial value { 0, x, y }
|
|
Term p = d_solver.declarePool("p", intSort, {zero, x, y});
|
|
// pool should have the same sort
|
|
ASSERT_TRUE(p.getSort() == setSort);
|
|
// cannot pass null sort
|
|
Sort nullSort;
|
|
ASSERT_THROW(d_solver.declarePool("i", nullSort, {}), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getOp)
|
|
{
|
|
Sort bv32 = d_solver.mkBitVectorSort(32);
|
|
Term a = d_solver.mkConst(bv32, "a");
|
|
Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, {2, 1});
|
|
Term exta = d_solver.mkTerm(ext, {a});
|
|
|
|
ASSERT_FALSE(a.hasOp());
|
|
ASSERT_THROW(a.getOp(), CVC5ApiException);
|
|
ASSERT_TRUE(exta.hasOp());
|
|
ASSERT_EQ(exta.getOp(), ext);
|
|
|
|
// Test Datatypes -- more complicated
|
|
DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
|
|
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
|
|
cons.addSelector("head", d_solver.getIntegerSort());
|
|
cons.addSelectorSelf("tail");
|
|
consListSpec.addConstructor(cons);
|
|
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
|
|
consListSpec.addConstructor(nil);
|
|
Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
|
|
Datatype consList = consListSort.getDatatype();
|
|
|
|
Term consTerm = consList.getConstructor("cons").getTerm();
|
|
Term nilTerm = consList.getConstructor("nil").getTerm();
|
|
Term headTerm = consList["cons"].getSelector("head").getTerm();
|
|
|
|
Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm});
|
|
Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR,
|
|
{consTerm, d_solver.mkInteger(1), listnil});
|
|
Term listhead = d_solver.mkTerm(APPLY_SELECTOR, {headTerm, listcons1});
|
|
|
|
ASSERT_TRUE(listnil.hasOp());
|
|
ASSERT_TRUE(listcons1.hasOp());
|
|
ASSERT_TRUE(listhead.hasOp());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getOption)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.getOption("incremental"));
|
|
ASSERT_THROW(d_solver.getOption("asdf"), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getOptionNames)
|
|
{
|
|
std::vector<std::string> names = d_solver.getOptionNames();
|
|
ASSERT_TRUE(names.size() > 100);
|
|
ASSERT_NE(std::find(names.begin(), names.end(), "verbose"), names.end());
|
|
ASSERT_EQ(std::find(names.begin(), names.end(), "foobar"), names.end());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getOptionInfo)
|
|
{
|
|
{
|
|
ASSERT_THROW(d_solver.getOptionInfo("asdf-invalid"), CVC5ApiException);
|
|
}
|
|
{
|
|
cvc5::OptionInfo info = d_solver.getOptionInfo("verbose");
|
|
ASSERT_EQ("verbose", info.name);
|
|
ASSERT_EQ(std::vector<std::string>{}, info.aliases);
|
|
ASSERT_TRUE(std::holds_alternative<OptionInfo::VoidInfo>(info.valueInfo));
|
|
std::stringstream ss;
|
|
ss << info;
|
|
ASSERT_EQ(ss.str(), "OptionInfo{ verbose | void }");
|
|
}
|
|
{
|
|
// bool type with default
|
|
cvc5::OptionInfo info = d_solver.getOptionInfo("print-success");
|
|
ASSERT_EQ("print-success", info.name);
|
|
ASSERT_EQ(std::vector<std::string>{}, info.aliases);
|
|
ASSERT_TRUE(
|
|
std::holds_alternative<OptionInfo::ValueInfo<bool>>(info.valueInfo));
|
|
auto valInfo = std::get<OptionInfo::ValueInfo<bool>>(info.valueInfo);
|
|
ASSERT_EQ(false, valInfo.defaultValue);
|
|
ASSERT_EQ(false, valInfo.currentValue);
|
|
ASSERT_EQ(info.boolValue(), false);
|
|
std::stringstream ss;
|
|
ss << info;
|
|
ASSERT_EQ(ss.str(),
|
|
"OptionInfo{ print-success | bool | false | default false }");
|
|
}
|
|
{
|
|
// int64 type with default
|
|
cvc5::OptionInfo info = d_solver.getOptionInfo("verbosity");
|
|
ASSERT_EQ("verbosity", info.name);
|
|
ASSERT_EQ(std::vector<std::string>{}, info.aliases);
|
|
ASSERT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(
|
|
info.valueInfo));
|
|
auto numInfo = std::get<OptionInfo::NumberInfo<int64_t>>(info.valueInfo);
|
|
ASSERT_EQ(0, numInfo.defaultValue);
|
|
ASSERT_EQ(0, numInfo.currentValue);
|
|
ASSERT_FALSE(numInfo.minimum || numInfo.maximum);
|
|
ASSERT_EQ(info.intValue(), 0);
|
|
std::stringstream ss;
|
|
ss << info;
|
|
ASSERT_EQ(ss.str(), "OptionInfo{ verbosity | int64_t | 0 | default 0 }");
|
|
}
|
|
{
|
|
// uint64 type with default
|
|
cvc5::OptionInfo info = d_solver.getOptionInfo("rlimit");
|
|
ASSERT_EQ("rlimit", info.name);
|
|
ASSERT_EQ(std::vector<std::string>{}, info.aliases);
|
|
ASSERT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(
|
|
info.valueInfo));
|
|
auto numInfo = std::get<OptionInfo::NumberInfo<uint64_t>>(info.valueInfo);
|
|
ASSERT_EQ(0, numInfo.defaultValue);
|
|
ASSERT_EQ(0, numInfo.currentValue);
|
|
ASSERT_FALSE(numInfo.minimum || numInfo.maximum);
|
|
ASSERT_EQ(info.uintValue(), 0);
|
|
std::stringstream ss;
|
|
ss << info;
|
|
ASSERT_EQ(ss.str(), "OptionInfo{ rlimit | uint64_t | 0 | default 0 }");
|
|
}
|
|
{
|
|
auto info = d_solver.getOptionInfo("random-freq");
|
|
ASSERT_EQ(info.name, "random-freq");
|
|
ASSERT_EQ(info.aliases, std::vector<std::string>{"random-frequency"});
|
|
ASSERT_TRUE(std::holds_alternative<cvc5::OptionInfo::NumberInfo<double>>(
|
|
info.valueInfo));
|
|
auto ni = std::get<cvc5::OptionInfo::NumberInfo<double>>(info.valueInfo);
|
|
ASSERT_EQ(ni.currentValue, 0.0);
|
|
ASSERT_EQ(ni.defaultValue, 0.0);
|
|
ASSERT_TRUE(ni.minimum && ni.maximum);
|
|
ASSERT_EQ(*ni.minimum, 0.0);
|
|
ASSERT_EQ(*ni.maximum, 1.0);
|
|
ASSERT_EQ(info.doubleValue(), 0.0);
|
|
std::stringstream ss;
|
|
ss << info;
|
|
ASSERT_EQ(ss.str(),
|
|
"OptionInfo{ random-freq, random-frequency | double | 0 | "
|
|
"default 0 | 0 <= x <= 1 }");
|
|
}
|
|
{
|
|
// string type with default
|
|
cvc5::OptionInfo info = d_solver.getOptionInfo("force-logic");
|
|
ASSERT_EQ("force-logic", info.name);
|
|
ASSERT_EQ(std::vector<std::string>{}, info.aliases);
|
|
ASSERT_TRUE(std::holds_alternative<OptionInfo::ValueInfo<std::string>>(
|
|
info.valueInfo));
|
|
auto valInfo = std::get<OptionInfo::ValueInfo<std::string>>(info.valueInfo);
|
|
ASSERT_EQ("", valInfo.defaultValue);
|
|
ASSERT_EQ("", valInfo.currentValue);
|
|
ASSERT_EQ(info.stringValue(), "");
|
|
std::stringstream ss;
|
|
ss << info;
|
|
ASSERT_EQ(ss.str(),
|
|
"OptionInfo{ force-logic | string | \"\" | default \"\" }");
|
|
}
|
|
{
|
|
// mode option
|
|
cvc5::OptionInfo info = d_solver.getOptionInfo("simplification");
|
|
ASSERT_EQ("simplification", info.name);
|
|
ASSERT_EQ(std::vector<std::string>{"simplification-mode"}, info.aliases);
|
|
ASSERT_TRUE(std::holds_alternative<OptionInfo::ModeInfo>(info.valueInfo));
|
|
auto modeInfo = std::get<OptionInfo::ModeInfo>(info.valueInfo);
|
|
ASSERT_EQ("batch", modeInfo.defaultValue);
|
|
ASSERT_EQ("batch", modeInfo.currentValue);
|
|
ASSERT_EQ(2, modeInfo.modes.size());
|
|
ASSERT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "batch")
|
|
!= modeInfo.modes.end());
|
|
ASSERT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "none")
|
|
!= modeInfo.modes.end());
|
|
std::stringstream ss;
|
|
ss << info;
|
|
ASSERT_EQ(ss.str(),
|
|
"OptionInfo{ simplification, simplification-mode | mode | batch "
|
|
"| default batch | modes: batch, none }");
|
|
}
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getDriverOptions)
|
|
{
|
|
auto dopts = d_solver.getDriverOptions();
|
|
ASSERT_EQ(dopts.err().rdbuf(), std::cerr.rdbuf());
|
|
ASSERT_EQ(dopts.in().rdbuf(), std::cin.rdbuf());
|
|
ASSERT_EQ(dopts.out().rdbuf(), std::cout.rdbuf());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getStatistics)
|
|
{
|
|
ASSERT_NO_THROW(cvc5::Stat());
|
|
// do some array reasoning to make sure we have a double statistics
|
|
{
|
|
Sort s1 = d_solver.getIntegerSort();
|
|
Sort s2 = d_solver.mkArraySort(s1, s1);
|
|
Term t1 = d_solver.mkConst(s1, "i");
|
|
Term t2 = d_solver.mkVar(s2, "a");
|
|
Term t3 = d_solver.mkTerm(Kind::SELECT, {t2, t1});
|
|
d_solver.checkSat();
|
|
}
|
|
cvc5::Statistics stats = d_solver.getStatistics();
|
|
{
|
|
std::stringstream ss;
|
|
ss << stats;
|
|
}
|
|
{
|
|
auto s = stats.get("global::totalTime");
|
|
ASSERT_FALSE(s.isInternal());
|
|
ASSERT_FALSE(s.isDefault());
|
|
ASSERT_TRUE(s.isString());
|
|
std::string time = s.getString();
|
|
ASSERT_TRUE(time.rfind("ms") == time.size() - 2); // ends with "ms"
|
|
ASSERT_FALSE(s.isDouble());
|
|
s = stats.get("resource::resourceUnitsUsed");
|
|
ASSERT_TRUE(s.isInternal());
|
|
ASSERT_FALSE(s.isDefault());
|
|
ASSERT_TRUE(s.isInt());
|
|
ASSERT_TRUE(s.getInt() >= 0);
|
|
}
|
|
for (const auto& s: stats)
|
|
{
|
|
ASSERT_FALSE(s.first.empty());
|
|
}
|
|
for (auto it = stats.begin(true, true); it != stats.end(); ++it)
|
|
{
|
|
{
|
|
auto tmp1 = it, tmp2 = it;
|
|
++tmp1;
|
|
tmp2++;
|
|
ASSERT_EQ(tmp1, tmp2);
|
|
--tmp1;
|
|
tmp2--;
|
|
ASSERT_EQ(tmp1, tmp2);
|
|
ASSERT_EQ(tmp1, it);
|
|
ASSERT_EQ(it, tmp2);
|
|
}
|
|
const auto& s = *it;
|
|
// check some basic utility methods
|
|
ASSERT_TRUE(!(it == stats.end()));
|
|
ASSERT_EQ(s.first, it->first);
|
|
if (s.first == "cvc5::CONSTANT")
|
|
{
|
|
ASSERT_FALSE(s.second.isInternal());
|
|
ASSERT_FALSE(s.second.isDefault());
|
|
ASSERT_TRUE(s.second.isHistogram());
|
|
auto hist = s.second.getHistogram();
|
|
ASSERT_FALSE(hist.empty());
|
|
std::stringstream ss;
|
|
ss << s.second;
|
|
ASSERT_EQ(ss.str(), "{ integer type: 1 }");
|
|
}
|
|
else if (s.first == "theory::arrays::avgIndexListLength")
|
|
{
|
|
ASSERT_TRUE(s.second.isInternal());
|
|
ASSERT_TRUE(s.second.isDouble());
|
|
ASSERT_TRUE(std::isnan(s.second.getDouble()));
|
|
}
|
|
}
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, printStatisticsSafe)
|
|
{
|
|
testing::internal::CaptureStdout();
|
|
d_solver.printStatisticsSafe(STDOUT_FILENO);
|
|
testing::internal::GetCapturedStdout();
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
|
|
{
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.checkSatAssuming(d_solver.mkFalse());
|
|
ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getUnsatAssumptions2)
|
|
{
|
|
d_solver.setOption("incremental", "true");
|
|
d_solver.setOption("produce-unsat-assumptions", "false");
|
|
d_solver.checkSatAssuming(d_solver.mkFalse());
|
|
ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getUnsatAssumptions3)
|
|
{
|
|
d_solver.setOption("incremental", "true");
|
|
d_solver.setOption("produce-unsat-assumptions", "true");
|
|
d_solver.checkSatAssuming(d_solver.mkFalse());
|
|
ASSERT_NO_THROW(d_solver.getUnsatAssumptions());
|
|
d_solver.checkSatAssuming(d_solver.mkTrue());
|
|
ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getUnsatCore1)
|
|
{
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.assertFormula(d_solver.mkFalse());
|
|
d_solver.checkSat();
|
|
ASSERT_THROW(d_solver.getUnsatCore(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getUnsatCore2)
|
|
{
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-unsat-cores", "false");
|
|
d_solver.assertFormula(d_solver.mkFalse());
|
|
d_solver.checkSat();
|
|
ASSERT_THROW(d_solver.getUnsatCore(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getUnsatCoreAndProof)
|
|
{
|
|
d_solver.setOption("incremental", "true");
|
|
d_solver.setOption("produce-unsat-cores", "true");
|
|
d_solver.setOption("produce-proofs", "true");
|
|
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Sort uToIntSort = d_solver.mkFunctionSort({uSort}, intSort);
|
|
Sort intPredSort = d_solver.mkFunctionSort({intSort}, boolSort);
|
|
std::vector<Term> uc;
|
|
|
|
Term x = d_solver.mkConst(uSort, "x");
|
|
Term y = d_solver.mkConst(uSort, "y");
|
|
Term f = d_solver.mkConst(uToIntSort, "f");
|
|
Term p = d_solver.mkConst(intPredSort, "p");
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term one = d_solver.mkInteger(1);
|
|
Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
|
|
Term f_y = d_solver.mkTerm(APPLY_UF, {f, y});
|
|
Term sum = d_solver.mkTerm(ADD, {f_x, f_y});
|
|
Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
|
|
Term p_f_y = d_solver.mkTerm(APPLY_UF, {p, f_y});
|
|
d_solver.assertFormula(d_solver.mkTerm(GT, {zero, f_x}));
|
|
d_solver.assertFormula(d_solver.mkTerm(GT, {zero, f_y}));
|
|
d_solver.assertFormula(d_solver.mkTerm(GT, {sum, one}));
|
|
d_solver.assertFormula(p_0);
|
|
d_solver.assertFormula(p_f_y.notTerm());
|
|
ASSERT_TRUE(d_solver.checkSat().isUnsat());
|
|
|
|
ASSERT_NO_THROW(uc = d_solver.getUnsatCore());
|
|
ASSERT_FALSE(uc.empty());
|
|
|
|
ASSERT_NO_THROW(d_solver.getProof());
|
|
ASSERT_NO_THROW(d_solver.getProof(modes::PROOF_COMPONENT_SAT));
|
|
|
|
d_solver.resetAssertions();
|
|
for (const auto& t : uc)
|
|
{
|
|
d_solver.assertFormula(t);
|
|
}
|
|
cvc5::Result res = d_solver.checkSat();
|
|
ASSERT_TRUE(res.isUnsat());
|
|
ASSERT_NO_THROW(d_solver.getProof());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getDifficulty)
|
|
{
|
|
d_solver.setOption("produce-difficulty", "true");
|
|
// cannot ask before a check sat
|
|
ASSERT_THROW(d_solver.getDifficulty(), CVC5ApiException);
|
|
d_solver.checkSat();
|
|
ASSERT_NO_THROW(d_solver.getDifficulty());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getDifficulty2)
|
|
{
|
|
d_solver.checkSat();
|
|
// option is not set
|
|
ASSERT_THROW(d_solver.getDifficulty(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getDifficulty3)
|
|
{
|
|
d_solver.setOption("produce-difficulty", "true");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Term x = d_solver.mkConst(intSort, "x");
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term ten = d_solver.mkInteger(10);
|
|
Term f0 = d_solver.mkTerm(GEQ, {x, ten});
|
|
Term f1 = d_solver.mkTerm(GEQ, {zero, x});
|
|
d_solver.assertFormula(f0);
|
|
d_solver.assertFormula(f1);
|
|
d_solver.checkSat();
|
|
std::map<Term, Term> dmap;
|
|
ASSERT_NO_THROW(dmap = d_solver.getDifficulty());
|
|
// difficulty should map assertions to integer values
|
|
for (const std::pair<const Term, Term>& t : dmap)
|
|
{
|
|
ASSERT_TRUE(t.first == f0 || t.first == f1);
|
|
ASSERT_TRUE(t.second.getKind() == CONST_INTEGER);
|
|
}
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getLearnedLiterals)
|
|
{
|
|
d_solver.setOption("produce-learned-literals", "true");
|
|
// cannot ask before a check sat
|
|
ASSERT_THROW(d_solver.getLearnedLiterals(), CVC5ApiException);
|
|
d_solver.checkSat();
|
|
ASSERT_NO_THROW(d_solver.getLearnedLiterals());
|
|
ASSERT_NO_THROW(d_solver.getLearnedLiterals(modes::LEARNED_LIT_PREPROCESS));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getLearnedLiterals2)
|
|
{
|
|
d_solver.setOption("produce-learned-literals", "true");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Term x = d_solver.mkConst(intSort, "x");
|
|
Term y = d_solver.mkConst(intSort, "y");
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term ten = d_solver.mkInteger(10);
|
|
Term f0 = d_solver.mkTerm(GEQ, {x, ten});
|
|
Term f1 = d_solver.mkTerm(
|
|
OR, {d_solver.mkTerm(GEQ, {zero, x}), d_solver.mkTerm(GEQ, {y, zero})});
|
|
d_solver.assertFormula(f0);
|
|
d_solver.assertFormula(f1);
|
|
d_solver.checkSat();
|
|
ASSERT_NO_THROW(d_solver.getLearnedLiterals());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValue1)
|
|
{
|
|
d_solver.setOption("produce-models", "false");
|
|
Term t = d_solver.mkTrue();
|
|
d_solver.assertFormula(t);
|
|
d_solver.checkSat();
|
|
ASSERT_THROW(d_solver.getValue(t), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValue2)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Term t = d_solver.mkFalse();
|
|
d_solver.assertFormula(t);
|
|
d_solver.checkSat();
|
|
ASSERT_THROW(d_solver.getValue(t), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValue3)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Sort uToIntSort = d_solver.mkFunctionSort({uSort}, intSort);
|
|
Sort intPredSort = d_solver.mkFunctionSort({intSort}, boolSort);
|
|
std::vector<Term> unsat_core;
|
|
|
|
Term x = d_solver.mkConst(uSort, "x");
|
|
Term y = d_solver.mkConst(uSort, "y");
|
|
Term z = d_solver.mkConst(uSort, "z");
|
|
Term f = d_solver.mkConst(uToIntSort, "f");
|
|
Term p = d_solver.mkConst(intPredSort, "p");
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term one = d_solver.mkInteger(1);
|
|
Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
|
|
Term f_y = d_solver.mkTerm(APPLY_UF, {f, y});
|
|
Term sum = d_solver.mkTerm(ADD, {f_x, f_y});
|
|
Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
|
|
Term p_f_y = d_solver.mkTerm(APPLY_UF, {p, f_y});
|
|
|
|
d_solver.assertFormula(d_solver.mkTerm(LEQ, {zero, f_x}));
|
|
d_solver.assertFormula(d_solver.mkTerm(LEQ, {zero, f_y}));
|
|
d_solver.assertFormula(d_solver.mkTerm(LEQ, {sum, one}));
|
|
d_solver.assertFormula(p_0.notTerm());
|
|
d_solver.assertFormula(p_f_y);
|
|
ASSERT_TRUE(d_solver.checkSat().isSat());
|
|
ASSERT_NO_THROW(d_solver.getValue(x));
|
|
ASSERT_NO_THROW(d_solver.getValue(y));
|
|
ASSERT_NO_THROW(d_solver.getValue(z));
|
|
ASSERT_NO_THROW(d_solver.getValue(sum));
|
|
ASSERT_NO_THROW(d_solver.getValue(p_f_y));
|
|
|
|
std::vector<Term> a;
|
|
ASSERT_NO_THROW(a.emplace_back(d_solver.getValue(x)));
|
|
ASSERT_NO_THROW(a.emplace_back(d_solver.getValue(y)));
|
|
ASSERT_NO_THROW(a.emplace_back(d_solver.getValue(z)));
|
|
std::vector<Term> b;
|
|
ASSERT_NO_THROW(b = d_solver.getValue({x,y,z}));
|
|
ASSERT_EQ(a,b);
|
|
|
|
Solver slv;
|
|
ASSERT_THROW(slv.getValue(x), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getModelDomainElements)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Term x = d_solver.mkConst(uSort, "x");
|
|
Term y = d_solver.mkConst(uSort, "y");
|
|
Term z = d_solver.mkConst(uSort, "z");
|
|
Term f = d_solver.mkTerm(DISTINCT, {x, y, z});
|
|
d_solver.assertFormula(f);
|
|
d_solver.checkSat();
|
|
ASSERT_NO_THROW(d_solver.getModelDomainElements(uSort));
|
|
ASSERT_TRUE(d_solver.getModelDomainElements(uSort).size() >= 3);
|
|
ASSERT_THROW(d_solver.getModelDomainElements(intSort), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getModelDomainElements2)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
d_solver.setOption("finite-model-find", "true");
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Term x = d_solver.mkVar(uSort, "x");
|
|
Term y = d_solver.mkVar(uSort, "y");
|
|
Term eq = d_solver.mkTerm(EQUAL, {x, y});
|
|
Term bvl = d_solver.mkTerm(VARIABLE_LIST, {x, y});
|
|
Term f = d_solver.mkTerm(FORALL, {bvl, eq});
|
|
d_solver.assertFormula(f);
|
|
d_solver.checkSat();
|
|
ASSERT_NO_THROW(d_solver.getModelDomainElements(uSort));
|
|
// a model for the above must interpret u as size 1
|
|
ASSERT_TRUE(d_solver.getModelDomainElements(uSort).size() == 1);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, isModelCoreSymbol)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
d_solver.setOption("model-cores", "simple");
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Term x = d_solver.mkConst(uSort, "x");
|
|
Term y = d_solver.mkConst(uSort, "y");
|
|
Term z = d_solver.mkConst(uSort, "z");
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term f = d_solver.mkTerm(NOT, {d_solver.mkTerm(EQUAL, {x, y})});
|
|
d_solver.assertFormula(f);
|
|
d_solver.checkSat();
|
|
ASSERT_TRUE(d_solver.isModelCoreSymbol(x));
|
|
ASSERT_TRUE(d_solver.isModelCoreSymbol(y));
|
|
ASSERT_FALSE(d_solver.isModelCoreSymbol(z));
|
|
ASSERT_THROW(d_solver.isModelCoreSymbol(zero), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getModel)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Term x = d_solver.mkConst(uSort, "x");
|
|
Term y = d_solver.mkConst(uSort, "y");
|
|
Term z = d_solver.mkConst(uSort, "z");
|
|
Term f = d_solver.mkTerm(NOT, {d_solver.mkTerm(EQUAL, {x, y})});
|
|
d_solver.assertFormula(f);
|
|
d_solver.checkSat();
|
|
std::vector<Sort> sorts;
|
|
sorts.push_back(uSort);
|
|
std::vector<Term> terms;
|
|
terms.push_back(x);
|
|
terms.push_back(y);
|
|
ASSERT_NO_THROW(d_solver.getModel(sorts, terms));
|
|
Term null;
|
|
terms.push_back(null);
|
|
ASSERT_THROW(d_solver.getModel(sorts, terms), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getModel2)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
std::vector<Sort> sorts;
|
|
std::vector<Term> terms;
|
|
ASSERT_THROW(d_solver.getModel(sorts, terms), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getModel3)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
std::vector<Sort> sorts;
|
|
std::vector<Term> terms;
|
|
d_solver.checkSat();
|
|
ASSERT_NO_THROW(d_solver.getModel(sorts, terms));
|
|
Sort integer = d_solver.getIntegerSort();
|
|
sorts.push_back(integer);
|
|
ASSERT_THROW(d_solver.getModel(sorts, terms), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getQuantifierElimination)
|
|
{
|
|
Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
|
|
Term forall =
|
|
d_solver.mkTerm(FORALL,
|
|
{d_solver.mkTerm(VARIABLE_LIST, {x}),
|
|
d_solver.mkTerm(OR, {x, d_solver.mkTerm(NOT, {x})})});
|
|
ASSERT_THROW(d_solver.getQuantifierElimination(Term()), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.getQuantifierElimination(Solver().mkBoolean(false)),
|
|
CVC5ApiException);
|
|
ASSERT_NO_THROW(d_solver.getQuantifierElimination(forall));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct)
|
|
{
|
|
Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
|
|
Term forall =
|
|
d_solver.mkTerm(FORALL,
|
|
{d_solver.mkTerm(VARIABLE_LIST, {x}),
|
|
d_solver.mkTerm(OR, {x, d_solver.mkTerm(NOT, {x})})});
|
|
ASSERT_THROW(d_solver.getQuantifierEliminationDisjunct(Term()),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(
|
|
d_solver.getQuantifierEliminationDisjunct(Solver().mkBoolean(false)),
|
|
CVC5ApiException);
|
|
ASSERT_NO_THROW(d_solver.getQuantifierEliminationDisjunct(forall));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, declareSepHeap)
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
Sort integer = d_solver.getIntegerSort();
|
|
ASSERT_NO_THROW(d_solver.declareSepHeap(integer, integer));
|
|
// cannot declare separation logic heap more than once
|
|
ASSERT_THROW(d_solver.declareSepHeap(integer, integer), CVC5ApiException);
|
|
}
|
|
|
|
namespace {
|
|
/**
|
|
* Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks
|
|
* some simple separation logic constraints.
|
|
*/
|
|
void checkSimpleSeparationConstraints(Solver* solver)
|
|
{
|
|
Sort integer = solver->getIntegerSort();
|
|
// declare the separation heap
|
|
solver->declareSepHeap(integer, integer);
|
|
Term x = solver->mkConst(integer, "x");
|
|
Term p = solver->mkConst(integer, "p");
|
|
Term heap = solver->mkTerm(cvc5::Kind::SEP_PTO, {p, x});
|
|
solver->assertFormula(heap);
|
|
Term nil = solver->mkSepNil(integer);
|
|
solver->assertFormula(nil.eqTerm(solver->mkInteger(5)));
|
|
solver->checkSat();
|
|
}
|
|
} // namespace
|
|
|
|
TEST_F(TestApiBlackSolver, getValueSepHeap1)
|
|
{
|
|
d_solver.setLogic("QF_BV");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "true");
|
|
Term t = d_solver.mkTrue();
|
|
d_solver.assertFormula(t);
|
|
ASSERT_THROW(d_solver.getValueSepHeap(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValueSepHeap2)
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "false");
|
|
checkSimpleSeparationConstraints(&d_solver);
|
|
ASSERT_THROW(d_solver.getValueSepHeap(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValueSepHeap3)
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "true");
|
|
Term t = d_solver.mkFalse();
|
|
d_solver.assertFormula(t);
|
|
d_solver.checkSat();
|
|
ASSERT_THROW(d_solver.getValueSepHeap(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValueSepHeap4)
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "true");
|
|
Term t = d_solver.mkTrue();
|
|
d_solver.assertFormula(t);
|
|
d_solver.checkSat();
|
|
ASSERT_THROW(d_solver.getValueSepHeap(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValueSepHeap5)
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "true");
|
|
checkSimpleSeparationConstraints(&d_solver);
|
|
ASSERT_NO_THROW(d_solver.getValueSepHeap());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValueSepNil1)
|
|
{
|
|
d_solver.setLogic("QF_BV");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "true");
|
|
Term t = d_solver.mkTrue();
|
|
d_solver.assertFormula(t);
|
|
ASSERT_THROW(d_solver.getValueSepNil(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValueSepNil2)
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "false");
|
|
checkSimpleSeparationConstraints(&d_solver);
|
|
ASSERT_THROW(d_solver.getValueSepNil(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValueSepNil3)
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "true");
|
|
Term t = d_solver.mkFalse();
|
|
d_solver.assertFormula(t);
|
|
d_solver.checkSat();
|
|
ASSERT_THROW(d_solver.getValueSepNil(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValueSepNil4)
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "true");
|
|
Term t = d_solver.mkTrue();
|
|
d_solver.assertFormula(t);
|
|
d_solver.checkSat();
|
|
ASSERT_THROW(d_solver.getValueSepNil(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getValueSepNil5)
|
|
{
|
|
d_solver.setLogic("ALL");
|
|
d_solver.setOption("incremental", "false");
|
|
d_solver.setOption("produce-models", "true");
|
|
checkSimpleSeparationConstraints(&d_solver);
|
|
ASSERT_NO_THROW(d_solver.getValueSepNil());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, push1)
|
|
{
|
|
d_solver.setOption("incremental", "true");
|
|
ASSERT_NO_THROW(d_solver.push(1));
|
|
ASSERT_THROW(d_solver.setOption("incremental", "false"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.setOption("incremental", "true"), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, push2)
|
|
{
|
|
d_solver.setOption("incremental", "false");
|
|
ASSERT_THROW(d_solver.push(1), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, pop1)
|
|
{
|
|
d_solver.setOption("incremental", "false");
|
|
ASSERT_THROW(d_solver.pop(1), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, pop2)
|
|
{
|
|
d_solver.setOption("incremental", "true");
|
|
ASSERT_THROW(d_solver.pop(1), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, pop3)
|
|
{
|
|
d_solver.setOption("incremental", "true");
|
|
ASSERT_NO_THROW(d_solver.push(1));
|
|
ASSERT_NO_THROW(d_solver.pop(1));
|
|
ASSERT_THROW(d_solver.pop(1), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, blockModel1)
|
|
{
|
|
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
|
|
d_solver.assertFormula(x.eqTerm(x));
|
|
d_solver.checkSat();
|
|
ASSERT_THROW(d_solver.blockModel(modes::BlockModelsMode::LITERALS),
|
|
CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, blockModel2)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
|
|
d_solver.assertFormula(x.eqTerm(x));
|
|
ASSERT_THROW(d_solver.blockModel(modes::BlockModelsMode::LITERALS),
|
|
CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, blockModel3)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
|
|
d_solver.assertFormula(x.eqTerm(x));
|
|
d_solver.checkSat();
|
|
ASSERT_NO_THROW(d_solver.blockModel(modes::BlockModelsMode::LITERALS));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, blockModelValues1)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
|
|
d_solver.assertFormula(x.eqTerm(x));
|
|
d_solver.checkSat();
|
|
ASSERT_THROW(d_solver.blockModelValues({}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.blockModelValues({Term()}), CVC5ApiException);
|
|
ASSERT_NO_THROW(d_solver.blockModelValues({Solver().mkBoolean(false)}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, blockModelValues2)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
|
|
d_solver.assertFormula(x.eqTerm(x));
|
|
d_solver.checkSat();
|
|
ASSERT_NO_THROW(d_solver.blockModelValues({x}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, blockModelValues3)
|
|
{
|
|
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
|
|
d_solver.assertFormula(x.eqTerm(x));
|
|
d_solver.checkSat();
|
|
ASSERT_THROW(d_solver.blockModelValues({x}), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, blockModelValues4)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
|
|
d_solver.assertFormula(x.eqTerm(x));
|
|
ASSERT_THROW(d_solver.blockModelValues({x}), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, blockModelValues5)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
|
|
d_solver.assertFormula(x.eqTerm(x));
|
|
d_solver.checkSat();
|
|
ASSERT_NO_THROW(d_solver.blockModelValues({x}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getInstantiations)
|
|
{
|
|
Sort iSort = d_solver.getIntegerSort();
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Term p = d_solver.declareFun("p", {iSort}, boolSort);
|
|
Term x = d_solver.mkVar(iSort, "x");
|
|
Term bvl = d_solver.mkTerm(VARIABLE_LIST, {x});
|
|
Term app = d_solver.mkTerm(APPLY_UF, {p, x});
|
|
Term q = d_solver.mkTerm(FORALL, {bvl, app});
|
|
d_solver.assertFormula(q);
|
|
Term five = d_solver.mkInteger(5);
|
|
Term app2 = d_solver.mkTerm(NOT, {d_solver.mkTerm(APPLY_UF, {p, five})});
|
|
d_solver.assertFormula(app2);
|
|
ASSERT_THROW(d_solver.getInstantiations(), CVC5ApiException);
|
|
d_solver.checkSat();
|
|
ASSERT_NO_THROW(d_solver.getInstantiations());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, setInfo)
|
|
{
|
|
ASSERT_THROW(d_solver.setInfo("cvc5-lagic", "QF_BV"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.setInfo("cvc2-logic", "QF_BV"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.setInfo("cvc5-logic", "asdf"), CVC5ApiException);
|
|
|
|
ASSERT_NO_THROW(d_solver.setInfo("source", "asdf"));
|
|
ASSERT_NO_THROW(d_solver.setInfo("category", "asdf"));
|
|
ASSERT_NO_THROW(d_solver.setInfo("difficulty", "asdf"));
|
|
ASSERT_NO_THROW(d_solver.setInfo("filename", "asdf"));
|
|
ASSERT_NO_THROW(d_solver.setInfo("license", "asdf"));
|
|
ASSERT_NO_THROW(d_solver.setInfo("name", "asdf"));
|
|
ASSERT_NO_THROW(d_solver.setInfo("notes", "asdf"));
|
|
|
|
ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2"));
|
|
ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.0"));
|
|
ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.5"));
|
|
ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.6"));
|
|
ASSERT_THROW(d_solver.setInfo("smt-lib-version", ".0"), CVC5ApiException);
|
|
|
|
ASSERT_NO_THROW(d_solver.setInfo("status", "sat"));
|
|
ASSERT_NO_THROW(d_solver.setInfo("status", "unsat"));
|
|
ASSERT_NO_THROW(d_solver.setInfo("status", "unknown"));
|
|
ASSERT_THROW(d_solver.setInfo("status", "asdf"), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, simplify)
|
|
{
|
|
ASSERT_THROW(d_solver.simplify(Term()), CVC5ApiException);
|
|
|
|
Sort bvSort = d_solver.mkBitVectorSort(32);
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
|
|
Sort funSort2 = d_solver.mkFunctionSort({uSort}, d_solver.getIntegerSort());
|
|
DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
|
|
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
|
|
cons.addSelector("head", d_solver.getIntegerSort());
|
|
cons.addSelectorSelf("tail");
|
|
consListSpec.addConstructor(cons);
|
|
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
|
|
consListSpec.addConstructor(nil);
|
|
Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
|
|
|
|
Term x = d_solver.mkConst(bvSort, "x");
|
|
ASSERT_NO_THROW(d_solver.simplify(x));
|
|
Term a = d_solver.mkConst(bvSort, "a");
|
|
ASSERT_NO_THROW(d_solver.simplify(a));
|
|
Term b = d_solver.mkConst(bvSort, "b");
|
|
ASSERT_NO_THROW(d_solver.simplify(b));
|
|
Term x_eq_x = d_solver.mkTerm(EQUAL, {x, x});
|
|
ASSERT_NO_THROW(d_solver.simplify(x_eq_x));
|
|
ASSERT_NE(d_solver.mkTrue(), x_eq_x);
|
|
ASSERT_EQ(d_solver.mkTrue(), d_solver.simplify(x_eq_x));
|
|
Term x_eq_b = d_solver.mkTerm(EQUAL, {x, b});
|
|
ASSERT_NO_THROW(d_solver.simplify(x_eq_b));
|
|
ASSERT_NE(d_solver.mkTrue(), x_eq_b);
|
|
ASSERT_NE(d_solver.mkTrue(), d_solver.simplify(x_eq_b));
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.simplify(x));
|
|
|
|
Term i1 = d_solver.mkConst(d_solver.getIntegerSort(), "i1");
|
|
ASSERT_NO_THROW(d_solver.simplify(i1));
|
|
Term i2 = d_solver.mkTerm(MULT, {i1, d_solver.mkInteger("23")});
|
|
ASSERT_NO_THROW(d_solver.simplify(i2));
|
|
ASSERT_NE(i1, i2);
|
|
ASSERT_NE(i1, d_solver.simplify(i2));
|
|
Term i3 = d_solver.mkTerm(ADD, {i1, d_solver.mkInteger(0)});
|
|
ASSERT_NO_THROW(d_solver.simplify(i3));
|
|
ASSERT_NE(i1, i3);
|
|
ASSERT_EQ(i1, d_solver.simplify(i3));
|
|
|
|
Datatype consList = consListSort.getDatatype();
|
|
Term dt1 = d_solver.mkTerm(
|
|
APPLY_CONSTRUCTOR,
|
|
{consList.getConstructor("cons").getTerm(),
|
|
d_solver.mkInteger(0),
|
|
d_solver.mkTerm(APPLY_CONSTRUCTOR,
|
|
{consList.getConstructor("nil").getTerm()})});
|
|
ASSERT_NO_THROW(d_solver.simplify(dt1));
|
|
Term dt2 = d_solver.mkTerm(
|
|
APPLY_SELECTOR, {consList["cons"].getSelector("head").getTerm(), dt1});
|
|
ASSERT_NO_THROW(d_solver.simplify(dt2));
|
|
|
|
Term b1 = d_solver.mkVar(bvSort, "b1");
|
|
ASSERT_NO_THROW(d_solver.simplify(b1));
|
|
Term b2 = d_solver.mkVar(bvSort, "b1");
|
|
ASSERT_NO_THROW(d_solver.simplify(b2));
|
|
Term b3 = d_solver.mkVar(uSort, "b3");
|
|
ASSERT_NO_THROW(d_solver.simplify(b3));
|
|
Term v1 = d_solver.mkConst(bvSort, "v1");
|
|
ASSERT_NO_THROW(d_solver.simplify(v1));
|
|
Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
|
|
ASSERT_NO_THROW(d_solver.simplify(v2));
|
|
Term f1 = d_solver.mkConst(funSort1, "f1");
|
|
ASSERT_NO_THROW(d_solver.simplify(f1));
|
|
Term f2 = d_solver.mkConst(funSort2, "f2");
|
|
ASSERT_NO_THROW(d_solver.simplify(f2));
|
|
d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b3}}, {v1, v2});
|
|
ASSERT_NO_THROW(d_solver.simplify(f1));
|
|
ASSERT_NO_THROW(d_solver.simplify(f2));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, assertFormula)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.assertFormula(d_solver.mkTrue()));
|
|
ASSERT_THROW(d_solver.assertFormula(Term()), CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.assertFormula(d_solver.mkTrue()));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, checkSat)
|
|
{
|
|
d_solver.setOption("incremental", "false");
|
|
ASSERT_NO_THROW(d_solver.checkSat());
|
|
ASSERT_THROW(d_solver.checkSat(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, checkSatAssuming)
|
|
{
|
|
d_solver.setOption("incremental", "false");
|
|
ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
|
|
ASSERT_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()), CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.checkSatAssuming(d_solver.mkTrue()));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, checkSatAssuming1)
|
|
{
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Term x = d_solver.mkConst(boolSort, "x");
|
|
Term y = d_solver.mkConst(boolSort, "y");
|
|
Term z = d_solver.mkTerm(AND, {x, y});
|
|
d_solver.setOption("incremental", "true");
|
|
ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
|
|
ASSERT_THROW(d_solver.checkSatAssuming(Term()), CVC5ApiException);
|
|
ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
|
|
ASSERT_NO_THROW(d_solver.checkSatAssuming(z));
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.checkSatAssuming(d_solver.mkTrue()));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, checkSatAssuming2)
|
|
{
|
|
d_solver.setOption("incremental", "true");
|
|
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Sort uToIntSort = d_solver.mkFunctionSort({uSort}, intSort);
|
|
Sort intPredSort = d_solver.mkFunctionSort({intSort}, boolSort);
|
|
|
|
Term n = Term();
|
|
// Constants
|
|
Term x = d_solver.mkConst(uSort, "x");
|
|
Term y = d_solver.mkConst(uSort, "y");
|
|
// Functions
|
|
Term f = d_solver.mkConst(uToIntSort, "f");
|
|
Term p = d_solver.mkConst(intPredSort, "p");
|
|
// Values
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term one = d_solver.mkInteger(1);
|
|
// Terms
|
|
Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
|
|
Term f_y = d_solver.mkTerm(APPLY_UF, {f, y});
|
|
Term sum = d_solver.mkTerm(ADD, {f_x, f_y});
|
|
Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
|
|
Term p_f_y = d_solver.mkTerm(APPLY_UF, {p, f_y});
|
|
// Assertions
|
|
Term assertions =
|
|
d_solver.mkTerm(AND,
|
|
{
|
|
d_solver.mkTerm(LEQ, {zero, f_x}), // 0 <= f(x)
|
|
d_solver.mkTerm(LEQ, {zero, f_y}), // 0 <= f(y)
|
|
d_solver.mkTerm(LEQ, {sum, one}), // f(x) + f(y) <= 1
|
|
p_0.notTerm(), // not p(0)
|
|
p_f_y // p(f(y))
|
|
});
|
|
|
|
ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
|
|
d_solver.assertFormula(assertions);
|
|
ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTerm(DISTINCT, {x, y})));
|
|
ASSERT_NO_THROW(d_solver.checkSatAssuming(
|
|
{d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, {x, y})}));
|
|
ASSERT_THROW(d_solver.checkSatAssuming(n), CVC5ApiException);
|
|
ASSERT_THROW(
|
|
d_solver.checkSatAssuming({n, d_solver.mkTerm(DISTINCT, {x, y})}),
|
|
CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_NO_THROW(slv.checkSatAssuming(d_solver.mkTrue()));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, setLogic)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.setLogic("AUFLIRA"));
|
|
ASSERT_THROW(d_solver.setLogic("AF_BV"), CVC5ApiException);
|
|
d_solver.assertFormula(d_solver.mkTrue());
|
|
ASSERT_THROW(d_solver.setLogic("AUFLIRA"), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, setOption)
|
|
{
|
|
ASSERT_NO_THROW(d_solver.setOption("bv-sat-solver", "minisat"));
|
|
ASSERT_THROW(d_solver.setOption("bv-sat-solver", "1"), CVC5ApiException);
|
|
d_solver.assertFormula(d_solver.mkTrue());
|
|
ASSERT_THROW(d_solver.setOption("bv-sat-solver", "minisat"),
|
|
CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, resetAssertions)
|
|
{
|
|
d_solver.setOption("incremental", "true");
|
|
|
|
Sort bvSort = d_solver.mkBitVectorSort(4);
|
|
Term one = d_solver.mkBitVector(4, 1);
|
|
Term x = d_solver.mkConst(bvSort, "x");
|
|
Term ule = d_solver.mkTerm(BITVECTOR_ULE, {x, one});
|
|
Term srem = d_solver.mkTerm(BITVECTOR_SREM, {one, x});
|
|
d_solver.push(4);
|
|
Term slt = d_solver.mkTerm(BITVECTOR_SLT, {srem, one});
|
|
d_solver.resetAssertions();
|
|
d_solver.checkSatAssuming({slt, ule});
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, declareSygusVar)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort funSort = d_solver.mkFunctionSort({intSort}, boolSort);
|
|
|
|
ASSERT_NO_THROW(d_solver.declareSygusVar("", boolSort));
|
|
ASSERT_NO_THROW(d_solver.declareSygusVar("", funSort));
|
|
ASSERT_NO_THROW(d_solver.declareSygusVar(std::string("b"), boolSort));
|
|
ASSERT_THROW(d_solver.declareSygusVar("", Sort()), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.declareSygusVar("a", Sort()), CVC5ApiException);
|
|
Solver slv;
|
|
ASSERT_THROW(slv.declareSygusVar("", boolSort), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, mkGrammar)
|
|
{
|
|
Term nullTerm;
|
|
Term boolTerm = d_solver.mkBoolean(true);
|
|
Term boolVar = d_solver.mkVar(d_solver.getBooleanSort());
|
|
Term intVar = d_solver.mkVar(d_solver.getIntegerSort());
|
|
|
|
ASSERT_NO_THROW(d_solver.mkGrammar({}, {intVar}));
|
|
ASSERT_NO_THROW(d_solver.mkGrammar({boolVar}, {intVar}));
|
|
ASSERT_THROW(d_solver.mkGrammar({}, {}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkGrammar({}, {nullTerm}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkGrammar({}, {boolTerm}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkGrammar({boolTerm}, {intVar}), CVC5ApiException);
|
|
Solver slv;
|
|
Term boolVar2 = slv.mkVar(slv.getBooleanSort());
|
|
Term intVar2 = slv.mkVar(slv.getIntegerSort());
|
|
ASSERT_NO_THROW(slv.mkGrammar({boolVar2}, {intVar2}));
|
|
ASSERT_NO_THROW(slv.mkGrammar({boolVar}, {intVar2}));
|
|
ASSERT_NO_THROW(slv.mkGrammar({boolVar2}, {intVar}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, synthFun)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Sort null;
|
|
Sort boolean = d_solver.getBooleanSort();
|
|
Sort integer = d_solver.getIntegerSort();
|
|
|
|
Term nullTerm;
|
|
Term x = d_solver.mkVar(boolean);
|
|
|
|
Term start1 = d_solver.mkVar(boolean);
|
|
Term start2 = d_solver.mkVar(integer);
|
|
|
|
Grammar g1 = d_solver.mkGrammar({x}, {start1});
|
|
g1.addRule(start1, d_solver.mkBoolean(false));
|
|
|
|
Grammar g2 = d_solver.mkGrammar({x}, {start2});
|
|
g2.addRule(start2, d_solver.mkInteger(0));
|
|
|
|
ASSERT_NO_THROW(d_solver.synthFun("", {}, boolean));
|
|
ASSERT_NO_THROW(d_solver.synthFun("f1", {x}, boolean));
|
|
ASSERT_NO_THROW(d_solver.synthFun("f2", {x}, boolean, g1));
|
|
|
|
ASSERT_THROW(d_solver.synthFun("f3", {nullTerm}, boolean), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.synthFun("f4", {}, null), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.synthFun("f6", {x}, boolean, g2), CVC5ApiException);
|
|
Solver slv;
|
|
slv.setOption("sygus", "true");
|
|
Term x2 = slv.mkVar(slv.getBooleanSort());
|
|
ASSERT_NO_THROW(slv.synthFun("f1", {x2}, slv.getBooleanSort()));
|
|
ASSERT_NO_THROW(slv.synthFun("", {}, d_solver.getBooleanSort()));
|
|
ASSERT_NO_THROW(slv.synthFun("f1", {x}, d_solver.getBooleanSort()));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, synthInv)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Sort boolean = d_solver.getBooleanSort();
|
|
Sort integer = d_solver.getIntegerSort();
|
|
|
|
Term nullTerm;
|
|
Term x = d_solver.mkVar(boolean);
|
|
|
|
Term start1 = d_solver.mkVar(boolean);
|
|
Term start2 = d_solver.mkVar(integer);
|
|
|
|
Grammar g1 = d_solver.mkGrammar({x}, {start1});
|
|
g1.addRule(start1, d_solver.mkBoolean(false));
|
|
|
|
Grammar g2 = d_solver.mkGrammar({x}, {start2});
|
|
g2.addRule(start2, d_solver.mkInteger(0));
|
|
|
|
ASSERT_NO_THROW(d_solver.synthInv("", {}));
|
|
ASSERT_NO_THROW(d_solver.synthInv("i1", {x}));
|
|
ASSERT_NO_THROW(d_solver.synthInv("i2", {x}, g1));
|
|
|
|
ASSERT_THROW(d_solver.synthInv("i3", {nullTerm}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.synthInv("i4", {x}, g2), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, addSygusConstraint)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Term nullTerm;
|
|
Term boolTerm = d_solver.mkBoolean(true);
|
|
Term intTerm = d_solver.mkInteger(1);
|
|
|
|
ASSERT_NO_THROW(d_solver.addSygusConstraint(boolTerm));
|
|
ASSERT_THROW(d_solver.addSygusConstraint(nullTerm), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.addSygusConstraint(intTerm), CVC5ApiException);
|
|
|
|
Solver slv;
|
|
slv.setOption("sygus", "true");
|
|
ASSERT_NO_THROW(slv.addSygusConstraint(boolTerm));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getSygusConstraints)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Term trueTerm = d_solver.mkBoolean(true);
|
|
Term falseTerm = d_solver.mkBoolean(false);
|
|
d_solver.addSygusConstraint(trueTerm);
|
|
d_solver.addSygusConstraint(falseTerm);
|
|
std::vector<Term> constraints{trueTerm, falseTerm};
|
|
ASSERT_EQ(d_solver.getSygusConstraints(), constraints);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, addSygusAssume)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Term nullTerm;
|
|
Term boolTerm = d_solver.mkBoolean(false);
|
|
Term intTerm = d_solver.mkInteger(1);
|
|
|
|
ASSERT_NO_THROW(d_solver.addSygusAssume(boolTerm));
|
|
ASSERT_THROW(d_solver.addSygusAssume(nullTerm), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.addSygusAssume(intTerm), CVC5ApiException);
|
|
|
|
Solver slv;
|
|
slv.setOption("sygus", "true");
|
|
ASSERT_NO_THROW(slv.addSygusAssume(boolTerm));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getSygusAssumptions)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Term trueTerm = d_solver.mkBoolean(true);
|
|
Term falseTerm = d_solver.mkBoolean(false);
|
|
d_solver.addSygusAssume(trueTerm);
|
|
d_solver.addSygusAssume(falseTerm);
|
|
std::vector<Term> assumptions{trueTerm, falseTerm};
|
|
ASSERT_EQ(d_solver.getSygusAssumptions(), assumptions);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, addSygusInvConstraint)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
Sort boolean = d_solver.getBooleanSort();
|
|
Sort real = d_solver.getRealSort();
|
|
|
|
Term nullTerm;
|
|
Term intTerm = d_solver.mkInteger(1);
|
|
|
|
Term inv = d_solver.declareFun("inv", {real}, boolean);
|
|
Term pre = d_solver.declareFun("pre", {real}, boolean);
|
|
Term trans = d_solver.declareFun("trans", {real, real}, boolean);
|
|
Term post = d_solver.declareFun("post", {real}, boolean);
|
|
|
|
Term inv1 = d_solver.declareFun("inv1", {real}, real);
|
|
|
|
Term trans1 = d_solver.declareFun("trans1", {boolean, real}, boolean);
|
|
Term trans2 = d_solver.declareFun("trans2", {real, boolean}, boolean);
|
|
Term trans3 = d_solver.declareFun("trans3", {real, real}, real);
|
|
|
|
ASSERT_NO_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, post));
|
|
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(nullTerm, pre, trans, post),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(inv, nullTerm, trans, post),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, nullTerm, post),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, nullTerm),
|
|
CVC5ApiException);
|
|
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(intTerm, pre, trans, post),
|
|
CVC5ApiException);
|
|
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(inv1, pre, trans, post),
|
|
CVC5ApiException);
|
|
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(inv, trans, trans, post),
|
|
CVC5ApiException);
|
|
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, intTerm, post),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, pre, post),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans1, post),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans2, post),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans3, post),
|
|
CVC5ApiException);
|
|
|
|
ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, trans),
|
|
CVC5ApiException);
|
|
Solver slv;
|
|
slv.setOption("sygus", "true");
|
|
Sort boolean2 = slv.getBooleanSort();
|
|
Sort real2 = slv.getRealSort();
|
|
Term inv22 = slv.declareFun("inv", {real2}, boolean2);
|
|
Term pre22 = slv.declareFun("pre", {real2}, boolean2);
|
|
Term trans22 = slv.declareFun("trans", {real2, real2}, boolean2);
|
|
Term post22 = slv.declareFun("post", {real2}, boolean2);
|
|
ASSERT_NO_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post22));
|
|
ASSERT_NO_THROW(slv.addSygusInvConstraint(inv, pre22, trans22, post22));
|
|
ASSERT_NO_THROW(slv.addSygusInvConstraint(inv22, pre, trans22, post22));
|
|
ASSERT_NO_THROW(slv.addSygusInvConstraint(inv22, pre22, trans, post22));
|
|
ASSERT_NO_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, checkSynth)
|
|
{
|
|
// requires option to be set
|
|
ASSERT_THROW(d_solver.checkSynth(), CVC5ApiException);
|
|
d_solver.setOption("sygus", "true");
|
|
ASSERT_NO_THROW(d_solver.checkSynth());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getSynthSolution)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
d_solver.setOption("incremental", "false");
|
|
|
|
Term nullTerm;
|
|
Term x = d_solver.mkBoolean(false);
|
|
Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
|
|
|
|
ASSERT_THROW(d_solver.getSynthSolution(f), CVC5ApiException);
|
|
|
|
cvc5::SynthResult sr = d_solver.checkSynth();
|
|
ASSERT_EQ(sr.hasSolution(), true);
|
|
|
|
ASSERT_NO_THROW(d_solver.getSynthSolution(f));
|
|
ASSERT_NO_THROW(d_solver.getSynthSolution(f));
|
|
|
|
ASSERT_THROW(d_solver.getSynthSolution(nullTerm), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.getSynthSolution(x), CVC5ApiException);
|
|
|
|
Solver slv;
|
|
ASSERT_THROW(slv.getSynthSolution(f), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getSynthSolutions)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
d_solver.setOption("incremental", "false");
|
|
|
|
Term nullTerm;
|
|
Term x = d_solver.mkBoolean(false);
|
|
Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
|
|
|
|
ASSERT_THROW(d_solver.getSynthSolutions({}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.getSynthSolutions({f}), CVC5ApiException);
|
|
|
|
d_solver.checkSynth();
|
|
|
|
ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
|
|
ASSERT_NO_THROW(d_solver.getSynthSolutions({f, f}));
|
|
|
|
ASSERT_THROW(d_solver.getSynthSolutions({}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.getSynthSolutions({nullTerm}), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.getSynthSolutions({x}), CVC5ApiException);
|
|
|
|
Solver slv;
|
|
ASSERT_THROW(slv.getSynthSolutions({x}), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, checkSynthNext)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
d_solver.setOption("incremental", "true");
|
|
Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
|
|
|
|
cvc5::SynthResult sr = d_solver.checkSynth();
|
|
ASSERT_EQ(sr.hasSolution(), true);
|
|
ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
|
|
sr = d_solver.checkSynthNext();
|
|
ASSERT_EQ(sr.hasSolution(), true);
|
|
ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, checkSynthNext2)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
d_solver.setOption("incremental", "false");
|
|
Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
|
|
|
|
d_solver.checkSynth();
|
|
ASSERT_THROW(d_solver.checkSynthNext(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, checkSynthNext3)
|
|
{
|
|
d_solver.setOption("sygus", "true");
|
|
d_solver.setOption("incremental", "true");
|
|
Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
|
|
|
|
ASSERT_THROW(d_solver.checkSynthNext(), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, tupleProject)
|
|
{
|
|
std::vector<Sort> sorts = {d_solver.getBooleanSort(),
|
|
d_solver.getIntegerSort(),
|
|
d_solver.getStringSort(),
|
|
d_solver.mkSetSort(d_solver.getStringSort())};
|
|
std::vector<Term> elements = {
|
|
d_solver.mkBoolean(true),
|
|
d_solver.mkInteger(3),
|
|
d_solver.mkString("C"),
|
|
d_solver.mkTerm(SET_SINGLETON, {d_solver.mkString("Z")})};
|
|
|
|
Term tuple = d_solver.mkTuple(sorts, elements);
|
|
|
|
std::vector<uint32_t> indices1 = {};
|
|
std::vector<uint32_t> indices2 = {0};
|
|
std::vector<uint32_t> indices3 = {0, 1};
|
|
std::vector<uint32_t> indices4 = {0, 0, 2, 2, 3, 3, 0};
|
|
std::vector<uint32_t> indices5 = {4};
|
|
std::vector<uint32_t> indices6 = {0, 4};
|
|
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices1), {tuple}));
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices2), {tuple}));
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices3), {tuple}));
|
|
ASSERT_NO_THROW(
|
|
d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices4), {tuple}));
|
|
|
|
ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices5), {tuple}),
|
|
CVC5ApiException);
|
|
ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices6), {tuple}),
|
|
CVC5ApiException);
|
|
|
|
std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
|
|
|
|
Op op = d_solver.mkOp(TUPLE_PROJECT, indices);
|
|
Term projection = d_solver.mkTerm(op, {tuple});
|
|
|
|
Datatype datatype = tuple.getSort().getDatatype();
|
|
DatatypeConstructor constructor = datatype[0];
|
|
|
|
for (size_t i = 0; i < indices.size(); i++)
|
|
{
|
|
Term selectorTerm = constructor[indices[i]].getTerm();
|
|
Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, {selectorTerm, tuple});
|
|
Term simplifiedTerm = d_solver.simplify(selectedTerm);
|
|
ASSERT_EQ(elements[indices[i]], simplifiedTerm);
|
|
}
|
|
|
|
ASSERT_EQ(
|
|
"((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton "
|
|
"\"Z\")))",
|
|
projection.toString());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, Output)
|
|
{
|
|
ASSERT_THROW(d_solver.isOutputOn("foo-invalid"), CVC5ApiException);
|
|
ASSERT_THROW(d_solver.getOutput("foo-invalid"), CVC5ApiException);
|
|
ASSERT_FALSE(d_solver.isOutputOn("inst"));
|
|
ASSERT_EQ(null_os.rdbuf(), d_solver.getOutput("inst").rdbuf());
|
|
d_solver.setOption("output", "inst");
|
|
ASSERT_TRUE(d_solver.isOutputOn("inst"));
|
|
ASSERT_NE(null_os.rdbuf(), d_solver.getOutput("inst").rdbuf());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, issue7000)
|
|
{
|
|
Sort s1 = d_solver.getIntegerSort();
|
|
Sort s2 = d_solver.mkFunctionSort({s1}, s1);
|
|
Sort s3 = d_solver.getRealSort();
|
|
Term t4 = d_solver.mkPi();
|
|
Term t7 = d_solver.mkConst(s3, "_x5");
|
|
Term t37 = d_solver.mkConst(s2, "_x32");
|
|
Term t59 = d_solver.mkConst(s2, "_x51");
|
|
Term t72 = d_solver.mkTerm(EQUAL, {t37, t59});
|
|
Term t74 = d_solver.mkTerm(GT, {t4, t7});
|
|
Term query = d_solver.mkTerm(AND, {t72, t74, t72, t72});
|
|
// throws logic exception since logic is not higher order by default
|
|
ASSERT_THROW(d_solver.checkSatAssuming(query.notTerm()), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, issue5893)
|
|
{
|
|
Solver slv;
|
|
Sort bvsort4 = d_solver.mkBitVectorSort(4);
|
|
Sort bvsort8 = d_solver.mkBitVectorSort(8);
|
|
Sort arrsort = d_solver.mkArraySort(bvsort4, bvsort8);
|
|
Term arr = d_solver.mkConst(arrsort, "arr");
|
|
Term idx = d_solver.mkConst(bvsort4, "idx");
|
|
Term ten = d_solver.mkBitVector(8, "10", 10);
|
|
Term sel = d_solver.mkTerm(SELECT, {arr, idx});
|
|
Term distinct = d_solver.mkTerm(DISTINCT, {sel, ten});
|
|
ASSERT_NO_FATAL_FAILURE(distinct.getOp());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue308)
|
|
{
|
|
Solver slv;
|
|
slv.setOption("check-proofs", "true");
|
|
Sort s1 = slv.getBooleanSort();
|
|
Term t1 = slv.mkConst(s1, "_x0");
|
|
Term t2 = slv.mkTerm(Kind::XOR, {t1, t1});
|
|
slv.checkSatAssuming({t2});
|
|
auto unsat_core = slv.getUnsatCore();
|
|
ASSERT_FALSE(unsat_core.empty());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue373)
|
|
{
|
|
Sort s1 = d_solver.getRealSort();
|
|
|
|
DatatypeConstructorDecl ctor13 = d_solver.mkDatatypeConstructorDecl("_x115");
|
|
ctor13.addSelector("_x109", s1);
|
|
Sort s4 = d_solver.declareDatatype("_x86", {ctor13});
|
|
|
|
Term t452 = d_solver.mkVar(s1, "_x281");
|
|
Term bvl = d_solver.mkTerm(d_solver.mkOp(VARIABLE_LIST), {t452});
|
|
Term acons = d_solver.mkTerm(
|
|
d_solver.mkOp(APPLY_CONSTRUCTOR),
|
|
{s4.getDatatype().getConstructor("_x115").getTerm(), t452});
|
|
// type exception
|
|
ASSERT_THROW(
|
|
d_solver.mkTerm(d_solver.mkOp(APPLY_CONSTRUCTOR), {bvl, acons, t452}),
|
|
CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue378)
|
|
{
|
|
DatatypeDecl dtdecl;
|
|
DatatypeConstructorDecl cdecl;
|
|
|
|
Sort s1 = d_solver.getBooleanSort();
|
|
|
|
dtdecl = d_solver.mkDatatypeDecl("_x0");
|
|
cdecl = d_solver.mkDatatypeConstructorDecl("_x6");
|
|
cdecl.addSelector("_x1", s1);
|
|
dtdecl.addConstructor(cdecl);
|
|
Sort s2 = d_solver.mkDatatypeSort(dtdecl);
|
|
|
|
dtdecl = d_solver.mkDatatypeDecl("_x36");
|
|
cdecl = d_solver.mkDatatypeConstructorDecl("_x42");
|
|
cdecl.addSelector("_x37", s1);
|
|
dtdecl.addConstructor(cdecl);
|
|
Sort s4 = d_solver.mkDatatypeSort(dtdecl);
|
|
|
|
Term t1 = d_solver.mkConst(s1, "_x53");
|
|
Term t4 = d_solver.mkConst(s4, "_x56");
|
|
Term t7 = d_solver.mkConst(s2, "_x58");
|
|
|
|
Sort sp = d_solver.mkParamSort("_x178");
|
|
dtdecl = d_solver.mkDatatypeDecl("_x176", {sp});
|
|
cdecl = d_solver.mkDatatypeConstructorDecl("_x184");
|
|
cdecl.addSelector("_x180", s2);
|
|
dtdecl.addConstructor(cdecl);
|
|
cdecl = d_solver.mkDatatypeConstructorDecl("_x186");
|
|
cdecl.addSelector("_x185", sp);
|
|
dtdecl.addConstructor(cdecl);
|
|
Sort s7 = d_solver.mkDatatypeSort(dtdecl);
|
|
Sort s9 = s7.instantiate({s2});
|
|
Term t1507 =
|
|
d_solver.mkTerm(APPLY_CONSTRUCTOR,
|
|
{s9.getDatatype().getConstructor("_x184").getTerm(), t7});
|
|
ASSERT_NO_THROW(d_solver.mkTerm(
|
|
APPLY_UPDATER,
|
|
{s9.getDatatype().getConstructor("_x186").getSelector("_x185").getTerm(),
|
|
t1507,
|
|
t7}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue379)
|
|
{
|
|
Sort bsort = d_solver.getBooleanSort();
|
|
Sort psort = d_solver.mkParamSort("_x1");
|
|
DatatypeConstructorDecl cdecl;
|
|
DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("x_0", {psort});
|
|
cdecl = d_solver.mkDatatypeConstructorDecl("_x8");
|
|
cdecl.addSelector("_x7", bsort);
|
|
dtdecl.addConstructor(cdecl);
|
|
cdecl = d_solver.mkDatatypeConstructorDecl("_x6");
|
|
cdecl.addSelector("_x2", psort);
|
|
cdecl.addSelectorSelf("_x3");
|
|
cdecl.addSelector("_x4", psort);
|
|
cdecl.addSelector("_x5", bsort);
|
|
Sort s2 = d_solver.mkDatatypeSort(dtdecl);
|
|
Sort s6 = s2.instantiate({bsort});
|
|
Term t317 = d_solver.mkConst(bsort, "_x345");
|
|
Term t843 = d_solver.mkConst(s6, "_x346");
|
|
Term t879 = d_solver.mkTerm(APPLY_UPDATER,
|
|
{t843.getSort()
|
|
.getDatatype()
|
|
.getConstructor("_x8")
|
|
.getSelector("_x7")
|
|
.getUpdaterTerm(),
|
|
t843,
|
|
t317});
|
|
ASSERT_EQ(t879.getSort(), s6);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getDatatypeArity)
|
|
{
|
|
DatatypeConstructorDecl ctor1 = d_solver.mkDatatypeConstructorDecl("_x21");
|
|
DatatypeConstructorDecl ctor2 = d_solver.mkDatatypeConstructorDecl("_x31");
|
|
Sort s3 = d_solver.declareDatatype(std::string("_x17"), {ctor1, ctor2});
|
|
ASSERT_EQ(s3.getDatatypeArity(), 0);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue381)
|
|
{
|
|
Sort s1 = d_solver.getBooleanSort();
|
|
|
|
Sort psort = d_solver.mkParamSort("_x9");
|
|
DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x8", {psort});
|
|
DatatypeConstructorDecl ctor = d_solver.mkDatatypeConstructorDecl("_x22");
|
|
ctor.addSelector("_x19", s1);
|
|
dtdecl.addConstructor(ctor);
|
|
Sort s3 = d_solver.mkDatatypeSort(dtdecl);
|
|
Sort s6 = s3.instantiate({s1});
|
|
Term t26 = d_solver.mkConst(s6, "_x63");
|
|
Term t5 = d_solver.mkTrue();
|
|
Term t187 = d_solver.mkTerm(APPLY_UPDATER,
|
|
{t26.getSort()
|
|
.getDatatype()
|
|
.getConstructor("_x22")
|
|
.getSelector("_x19")
|
|
.getUpdaterTerm(),
|
|
t26,
|
|
t5});
|
|
ASSERT_NO_THROW(d_solver.simplify(t187));
|
|
}
|
|
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue382)
|
|
{
|
|
Sort s1 = d_solver.getBooleanSort();
|
|
Sort psort = d_solver.mkParamSort("_x1");
|
|
DatatypeConstructorDecl ctor = d_solver.mkDatatypeConstructorDecl("_x20");
|
|
ctor.addSelector("_x19", psort);
|
|
DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x0", {psort});
|
|
dtdecl.addConstructor(ctor);
|
|
Sort s2 = d_solver.mkDatatypeSort(dtdecl);
|
|
Sort s6 = s2.instantiate({s1});
|
|
Term t13 = d_solver.mkVar(s6, "_x58");
|
|
Term t18 = d_solver.mkConst(s6, "_x63");
|
|
Term t52 = d_solver.mkVar(s6, "_x70");
|
|
Term t53 = d_solver.mkTerm(MATCH_BIND_CASE,
|
|
{d_solver.mkTerm(VARIABLE_LIST, {t52}), t52, t18});
|
|
Term t73 = d_solver.mkVar(s1, "_x78");
|
|
Term t81 = d_solver.mkTerm(
|
|
MATCH_BIND_CASE,
|
|
{d_solver.mkTerm(VARIABLE_LIST, {t73}),
|
|
d_solver.mkTerm(
|
|
APPLY_CONSTRUCTOR,
|
|
{s6.getDatatype().getConstructor("_x20").getInstantiatedTerm(s6),
|
|
t73}),
|
|
t18});
|
|
Term t82 = d_solver.mkTerm(MATCH, {t13, t53, t53, t53, t81});
|
|
Term t325 = d_solver.mkTerm(
|
|
APPLY_SELECTOR,
|
|
{t82.getSort().getDatatype().getSelector("_x19").getTerm(), t82});
|
|
ASSERT_NO_THROW(d_solver.simplify(t325));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue383)
|
|
{
|
|
d_solver.setOption("produce-models", "true");
|
|
|
|
Sort s1 = d_solver.getBooleanSort();
|
|
|
|
DatatypeConstructorDecl ctordecl = d_solver.mkDatatypeConstructorDecl("_x5");
|
|
DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x0");
|
|
dtdecl.addConstructor(ctordecl);
|
|
Sort s2 = d_solver.mkDatatypeSort(dtdecl);
|
|
|
|
ctordecl = d_solver.mkDatatypeConstructorDecl("_x23");
|
|
ctordecl.addSelectorSelf("_x21");
|
|
dtdecl = d_solver.mkDatatypeDecl("_x12");
|
|
dtdecl.addConstructor(ctordecl);
|
|
ASSERT_THROW(d_solver.mkDatatypeSort(dtdecl), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue386)
|
|
{
|
|
Sort s1 = d_solver.getBooleanSort();
|
|
Sort p1 = d_solver.mkParamSort("_p1");
|
|
Sort p2 = d_solver.mkParamSort("_p2");
|
|
DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x0", {p1, p2});
|
|
DatatypeConstructorDecl ctordecl = d_solver.mkDatatypeConstructorDecl("_x1");
|
|
ctordecl.addSelector("_x2", p1);
|
|
dtdecl.addConstructor(ctordecl);
|
|
Sort s2 = d_solver.mkDatatypeSort(dtdecl);
|
|
ASSERT_THROW(s2.instantiate({s1}), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue414)
|
|
{
|
|
Solver slv;
|
|
Sort s2 = slv.getRealSort();
|
|
Term t1 = slv.mkConst(s2, "_x0");
|
|
Term t16 = slv.mkTerm(Kind::PI);
|
|
Term t53 = slv.mkTerm(Kind::SUB, {t1, t16});
|
|
Term t54 = slv.mkTerm(Kind::SECANT, {t53});
|
|
ASSERT_NO_THROW(slv.simplify(t54));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue420)
|
|
{
|
|
Solver slv;
|
|
slv.setOption("strings-exp", "true");
|
|
slv.setOption("produce-models", "true");
|
|
slv.setOption("produce-unsat-cores", "true");
|
|
Sort s2 = slv.getRealSort();
|
|
Sort s3 = slv.mkUninterpretedSort("_u0");
|
|
DatatypeDecl _dt1 = slv.mkDatatypeDecl("_dt1", {});
|
|
DatatypeConstructorDecl _cons16 = slv.mkDatatypeConstructorDecl("_cons16");
|
|
_cons16.addSelector("_sel13", s3);
|
|
_dt1.addConstructor(_cons16);
|
|
std::vector<Sort> _s4 = slv.mkDatatypeSorts({_dt1});
|
|
Sort s4 = _s4[0];
|
|
Sort s5 = slv.mkSequenceSort(s2);
|
|
Term t3 = slv.mkConst(s5, "_x18");
|
|
Term t7 = slv.mkConst(s4, "_x22");
|
|
// was initially a dt size application
|
|
Term t13 = slv.mkConst(slv.getIntegerSort(), "t13");
|
|
Term t53 = slv.mkTerm(Kind::SEQ_NTH, {t3, t13});
|
|
ASSERT_NO_THROW(slv.checkSat());
|
|
ASSERT_NO_THROW(slv.blockModelValues({t53, t7}));
|
|
ASSERT_NO_THROW(slv.checkSat());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue440)
|
|
{
|
|
Solver slv;
|
|
slv.setLogic("QF_ALL");
|
|
slv.setOption("global-negate", "true");
|
|
slv.setOption("produce-unsat-cores", "true");
|
|
Sort s1 = slv.getBooleanSort();
|
|
Term t9 = slv.mkBoolean(true);
|
|
Term t109 = slv.mkTerm(Kind::NOT, {t9});
|
|
// should throw an option exception
|
|
ASSERT_THROW(slv.checkSatAssuming({t109}), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue434)
|
|
{
|
|
Solver slv;
|
|
slv.setOption("dump-difficulty", "true");
|
|
slv.setOption("debug-check-models", "true");
|
|
Sort s1 = slv.mkUninterpretedSort("_u0");
|
|
Sort s2 = slv.mkUninterpretedSort("_u1");
|
|
Sort s3 = slv.mkUninterpretedSort("_u2");
|
|
Sort s4 = slv.getBooleanSort();
|
|
Term t1 = slv.mkConst(s1, "_x3");
|
|
Term t3 = slv.mkConst(s3, "_x5");
|
|
Term t15 = slv.mkConst(s1, "_x17");
|
|
Term t26 = slv.mkBoolean(false);
|
|
Term t60 = slv.mkVar(s4, "_f29_1");
|
|
Term t73 = slv.defineFun("_f29", {t60}, t60.getSort(), t60);
|
|
Term t123 = slv.mkVar(s4, "_f31_0");
|
|
Term t135 = slv.defineFun("_f31", {t123}, t123.getSort(), t123);
|
|
Term t506 = slv.mkVar(s1, "_f37_0");
|
|
Term t507 = slv.mkVar(s4, "_f37_1");
|
|
Term t510 = slv.mkTerm(Kind::APPLY_UF, {t73, t507});
|
|
Term t530 = slv.defineFun("_f37", {t507}, t510.getSort(), t510);
|
|
Term t559 = slv.mkTerm(Kind::DISTINCT, {t15, t1});
|
|
Term t631 = slv.mkTerm(Kind::XOR, {t559, t26});
|
|
Term t632 = slv.mkTerm(Kind::APPLY_UF, {t135, t631});
|
|
Term t715 = slv.mkVar(s4, "_f40_0");
|
|
Term t721 = slv.mkTerm(Kind::APPLY_UF, {t530, t715});
|
|
Term t722 = slv.mkTerm(Kind::APPLY_UF, {t530, t721});
|
|
Term t731 = slv.defineFun("_f40", {t715}, t722.getSort(), t722);
|
|
Term t1014 = slv.mkVar(s4, "_f45_0");
|
|
Term t1034 = slv.mkTerm(Kind::DISTINCT, {t510, t510});
|
|
Term t1035 = slv.mkTerm(Kind::XOR, {t1034, t632});
|
|
Term t1037 = slv.mkTerm(Kind::APPLY_UF, {t135, t1035});
|
|
Term t1039 = slv.mkTerm(Kind::APPLY_UF, {t731, t1037});
|
|
Term t1040 = slv.defineFun("_f45", {t1014}, t1039.getSort(), t1039);
|
|
Term t1072 = slv.mkTerm(Kind::APPLY_UF, {t1040, t510});
|
|
Term t1073 = slv.mkTerm(Kind::APPLY_UF, {t73, t1072});
|
|
// the query has free variables, and should throw an exception
|
|
ASSERT_THROW(slv.checkSatAssuming({t1073, t510}), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue436)
|
|
{
|
|
Solver slv;
|
|
slv.setOption("produce-abducts", "true");
|
|
slv.setOption("solve-bv-as-int", "sum");
|
|
Sort s8 = slv.mkBitVectorSort(68);
|
|
Term t17 = slv.mkConst(s8, "_x6");
|
|
Term t23;
|
|
{
|
|
uint32_t bw = s8.getBitVectorSize();
|
|
t23 = slv.mkBitVector(bw, 1);
|
|
}
|
|
Term t33 = slv.mkTerm(Kind::BITVECTOR_ULT, {t17, t23});
|
|
// solve-bv-as-int is incompatible with get-abduct
|
|
ASSERT_THROW(slv.getAbduct(t33), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue431)
|
|
{
|
|
Solver slv;
|
|
slv.setOption("produce-models", "true");
|
|
slv.setOption("produce-unsat-assumptions", "true");
|
|
slv.setOption("produce-assertions", "true");
|
|
Sort s1 = slv.getStringSort();
|
|
Sort s3 = slv.getIntegerSort();
|
|
Sort s7 = slv.mkArraySort(s1, s3);
|
|
Term t3 = slv.mkConst(s1, "_x2");
|
|
Term t57 = slv.mkVar(s7, "_x38");
|
|
Term t103 = slv.mkTerm(Kind::SELECT, {t57, t3});
|
|
slv.checkSat();
|
|
ASSERT_THROW(slv.blockModelValues({t103}), CVC5ApiException);
|
|
}
|
|
TEST_F(TestApiBlackSolver, proj_issue426)
|
|
{
|
|
Solver slv;
|
|
slv.setLogic("ALL");
|
|
slv.setOption("strings-exp", "true");
|
|
slv.setOption("produce-models", "true");
|
|
slv.setOption("produce-assertions", "true");
|
|
Sort s1 = slv.getRealSort();
|
|
Sort s2 = slv.getRoundingModeSort();
|
|
Sort s4 = slv.mkSequenceSort(s1);
|
|
Sort s5 = slv.mkArraySort(s4, s4);
|
|
Term t4 = slv.mkConst(s1, "_x3");
|
|
Term t5 = slv.mkReal("9192/832927743");
|
|
Term t19 = slv.mkConst(s2, "_x42");
|
|
Term t24 = slv.mkConst(s5, "_x44");
|
|
Term t37 = slv.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE);
|
|
slv.checkSat();
|
|
slv.blockModelValues({t24, t19, t4, t37});
|
|
slv.checkSat();
|
|
ASSERT_NO_THROW(slv.getValue({t5}));
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue429)
|
|
{
|
|
Solver slv;
|
|
Sort s1 = slv.getRealSort();
|
|
Term t6 = slv.mkConst(s1, "_x5");
|
|
Term t16 =
|
|
slv.mkReal(std::stoll("1696223.9473797265702297792792306581323741"));
|
|
Term t111 = slv.mkTerm(Kind::SEQ_UNIT, {t16});
|
|
Term t119 = slv.mkTerm(slv.mkOp(Kind::SEQ_UNIT), {t6});
|
|
Term t126 = slv.mkTerm(Kind::SEQ_PREFIX, {t111, t119});
|
|
slv.checkSatAssuming({t126.notTerm()});
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue422)
|
|
{
|
|
Solver slv;
|
|
slv.setOption("sygus-rr-synth-input", "true");
|
|
slv.setOption("strings-exp", "true");
|
|
slv.setOption("sygus-abort-size", "1");
|
|
Sort s1 = slv.mkBitVectorSort(36);
|
|
Sort s2 = slv.getStringSort();
|
|
Term t1 = slv.mkConst(s2, "_x0");
|
|
Term t2 = slv.mkConst(s1, "_x1");
|
|
Term t11;
|
|
{
|
|
uint32_t bw = s1.getBitVectorSize();
|
|
std::string val(bw, '1');
|
|
val[0] = '0';
|
|
t11 = slv.mkBitVector(bw, val, 2);
|
|
}
|
|
Term t60 = slv.mkTerm(Kind::SET_SINGLETON, {t1});
|
|
Term t66 = slv.mkTerm(Kind::BITVECTOR_COMP, {t2, t11});
|
|
Term t92 = slv.mkRegexpAll();
|
|
Term t96 = slv.mkTerm(slv.mkOp(Kind::BITVECTOR_ZERO_EXTEND, {51}), {t66});
|
|
Term t105 = slv.mkTerm(Kind::BITVECTOR_ADD, {t96, t96});
|
|
Term t113 = slv.mkTerm(Kind::BITVECTOR_SUB, {t105, t105});
|
|
Term t137 = slv.mkTerm(Kind::BITVECTOR_XOR, {t113, t105});
|
|
Term t211 = slv.mkTerm(Kind::BITVECTOR_SLTBV, {t137, t137});
|
|
Term t212 = slv.mkTerm(Kind::SET_MINUS, {t60, t60});
|
|
Term t234 = slv.mkTerm(Kind::SET_CHOOSE, {t212});
|
|
Term t250 = slv.mkTerm(Kind::STRING_REPLACE_RE_ALL, {t1, t92, t1});
|
|
Term t259 = slv.mkTerm(Kind::STRING_REPLACE_ALL, {t234, t234, t250});
|
|
Term t263 = slv.mkTerm(Kind::STRING_TO_LOWER, {t259});
|
|
Term t272 = slv.mkTerm(Kind::BITVECTOR_SDIV, {t211, t66});
|
|
Term t276 = slv.mkTerm(slv.mkOp(Kind::BITVECTOR_ZERO_EXTEND, {71}), {t272});
|
|
Term t288 = slv.mkTerm(Kind::EQUAL, {t263, t1});
|
|
Term t300 = slv.mkTerm(Kind::BITVECTOR_SLT, {t276, t276});
|
|
Term t301 = slv.mkTerm(Kind::EQUAL, {t288, t300});
|
|
slv.assertFormula({t301});
|
|
// should terminate with an exception indicating we are done enumerating
|
|
// rewrite rules.
|
|
ASSERT_THROW(slv.push(4), CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, proj_issue423)
|
|
{
|
|
Solver slv;
|
|
slv.setOption("produce-models", "true");
|
|
slv.setOption("produce-difficulty", "true");
|
|
Sort s2 = slv.getRealSort();
|
|
Sort s3 = slv.mkSequenceSort(s2);
|
|
Term t2;
|
|
{
|
|
t2 = slv.mkEmptySequence(s3.getSequenceElementSort());
|
|
}
|
|
Term t22 = slv.mkReal("119605652059157009");
|
|
Term t32 = slv.mkTerm(Kind::SEQ_UNIT, {t22});
|
|
Term t43 = slv.mkTerm(Kind::SEQ_CONCAT, {t2, t32});
|
|
Term t51 = slv.mkTerm(Kind::DISTINCT, {t32, t32});
|
|
slv.checkSat();
|
|
slv.blockModelValues({t51, t43});
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, projIssue431)
|
|
{
|
|
Solver slv;
|
|
slv.setOption("produce-abducts", "true");
|
|
Sort s2 = slv.mkBitVectorSort(22);
|
|
Sort s4 = slv.mkSetSort(s2);
|
|
Sort s5 = slv.getBooleanSort();
|
|
Sort s6 = slv.getRealSort();
|
|
Sort s7 = slv.mkFunctionSort({s6}, s5);
|
|
DatatypeDecl _dt46 = slv.mkDatatypeDecl("_dt46", {});
|
|
DatatypeConstructorDecl _cons64 = slv.mkDatatypeConstructorDecl("_cons64");
|
|
_cons64.addSelector("_sel62", s6);
|
|
_cons64.addSelector("_sel63", s4);
|
|
_dt46.addConstructor(_cons64);
|
|
Sort s14 = slv.mkDatatypeSorts({_dt46})[0];
|
|
Term t31 = slv.mkConst(s7, "_x100");
|
|
Term t47 = slv.mkConst(s14, "_x112");
|
|
Term sel = t47.getSort()
|
|
.getDatatype()
|
|
.getConstructor("_cons64")
|
|
.getSelector("_sel62")
|
|
.getTerm();
|
|
Term t274 = slv.mkTerm(APPLY_SELECTOR, {sel, t47});
|
|
Term t488 = slv.mkTerm(Kind::APPLY_UF, {t31, t274});
|
|
slv.assertFormula({t488});
|
|
Term abduct;
|
|
abduct = slv.getAbduct(t488);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, projIssue337)
|
|
{
|
|
Term t =
|
|
d_solver.mkTerm(SEQ_UNIT, {d_solver.mkReal("3416574625719121610379268")});
|
|
Term tt = d_solver.simplify(t);
|
|
ASSERT_EQ(t.getSort(), tt.getSort());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, declareOracleFunError)
|
|
{
|
|
Sort iSort = d_solver.getIntegerSort();
|
|
// cannot declare without option
|
|
ASSERT_THROW(d_solver.declareOracleFun(
|
|
"f",
|
|
{iSort},
|
|
iSort,
|
|
[&](const std::vector<Term>& input) { return d_solver.mkInteger(0); });
|
|
, CVC5ApiException);
|
|
d_solver.setOption("oracles", "true");
|
|
Sort nullSort;
|
|
// bad sort
|
|
ASSERT_THROW(d_solver.declareOracleFun(
|
|
"f",
|
|
{nullSort},
|
|
iSort,
|
|
[&](const std::vector<Term>& input) { return d_solver.mkInteger(0); });
|
|
, CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, declareOracleFunUnsat)
|
|
{
|
|
d_solver.setOption("oracles", "true");
|
|
Sort iSort = d_solver.getIntegerSort();
|
|
// f is the function implementing (lambda ((x Int)) (+ x 1))
|
|
Term f = d_solver.declareOracleFun(
|
|
"f", {iSort}, iSort, [&](const std::vector<Term>& input) {
|
|
if (input[0].isUInt32Value())
|
|
{
|
|
return d_solver.mkInteger(input[0].getUInt32Value() + 1);
|
|
}
|
|
return d_solver.mkInteger(0);
|
|
});
|
|
Term three = d_solver.mkInteger(3);
|
|
Term five = d_solver.mkInteger(5);
|
|
Term eq =
|
|
d_solver.mkTerm(EQUAL, {d_solver.mkTerm(APPLY_UF, {f, three}), five});
|
|
d_solver.assertFormula(eq);
|
|
// (f 3) = 5
|
|
ASSERT_TRUE(d_solver.checkSat().isUnsat());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, declareOracleFunSat)
|
|
{
|
|
d_solver.setOption("oracles", "true");
|
|
d_solver.setOption("produce-models", "true");
|
|
Sort iSort = d_solver.getIntegerSort();
|
|
// f is the function implementing (lambda ((x Int)) (% x 10))
|
|
Term f = d_solver.declareOracleFun(
|
|
"f", {iSort}, iSort, [&](const std::vector<Term>& input) {
|
|
if (input[0].isUInt32Value())
|
|
{
|
|
return d_solver.mkInteger(input[0].getUInt32Value() % 10);
|
|
}
|
|
return d_solver.mkInteger(0);
|
|
});
|
|
Term seven = d_solver.mkInteger(7);
|
|
Term x = d_solver.mkConst(iSort, "x");
|
|
Term lb = d_solver.mkTerm(GEQ, {x, d_solver.mkInteger(0)});
|
|
d_solver.assertFormula(lb);
|
|
Term ub = d_solver.mkTerm(LEQ, {x, d_solver.mkInteger(100)});
|
|
d_solver.assertFormula(ub);
|
|
Term eq = d_solver.mkTerm(EQUAL, {d_solver.mkTerm(APPLY_UF, {f, x}), seven});
|
|
d_solver.assertFormula(eq);
|
|
// x >= 0 ^ x <= 100 ^ (f x) = 7
|
|
ASSERT_TRUE(d_solver.checkSat().isSat());
|
|
Term xval = d_solver.getValue(x);
|
|
ASSERT_TRUE(xval.isUInt32Value());
|
|
ASSERT_TRUE(xval.getUInt32Value() % 10 == 7);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, declareOracleFunSat2)
|
|
{
|
|
d_solver.setOption("oracles", "true");
|
|
d_solver.setOption("produce-models", "true");
|
|
Sort iSort = d_solver.getIntegerSort();
|
|
Sort bSort = d_solver.getBooleanSort();
|
|
// f is the function implementing (lambda ((x Int) (y Int)) (= x y))
|
|
Term eq = d_solver.declareOracleFun(
|
|
"eq", {iSort, iSort}, bSort, [&](const std::vector<Term>& input) {
|
|
return d_solver.mkBoolean(input[0] == input[1]);
|
|
});
|
|
Term x = d_solver.mkConst(iSort, "x");
|
|
Term y = d_solver.mkConst(iSort, "y");
|
|
Term neq = d_solver.mkTerm(NOT, {d_solver.mkTerm(APPLY_UF, {eq, x, y})});
|
|
d_solver.assertFormula(neq);
|
|
// (not (eq x y))
|
|
ASSERT_TRUE(d_solver.checkSat().isSat());
|
|
Term xval = d_solver.getValue(x);
|
|
Term yval = d_solver.getValue(y);
|
|
ASSERT_TRUE(xval != yval);
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, verticalBars)
|
|
{
|
|
Term a = d_solver.declareFun("|a |", {}, d_solver.getRealSort());
|
|
ASSERT_EQ("|a |", a.toString());
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, getVersion)
|
|
{
|
|
std::cout << d_solver.getVersion() << std::endl;
|
|
}
|
|
|
|
TEST_F(TestApiBlackSolver, multipleSolvers)
|
|
{
|
|
Term function1, function2, value1, value2, definedFunction;
|
|
Sort integerSort;
|
|
Term zero;
|
|
{
|
|
Solver s1;
|
|
s1.setLogic("ALL");
|
|
s1.setOption("produce-models", "true");
|
|
integerSort = s1.getIntegerSort();
|
|
function1 = s1.declareFun("f1", {}, s1.getIntegerSort());
|
|
Term x = s1.mkVar(integerSort, "x");
|
|
zero = s1.mkInteger(0);
|
|
definedFunction = s1.defineFun("f", {x}, integerSort, zero);
|
|
s1.assertFormula(function1.eqTerm(zero));
|
|
s1.checkSat();
|
|
value1 = s1.getValue(function1);
|
|
}
|
|
ASSERT_EQ(zero, value1);
|
|
{
|
|
Solver s2;
|
|
s2.setLogic("ALL");
|
|
s2.setOption("produce-models", "true");
|
|
function2 = s2.declareFun("function2", {}, integerSort);
|
|
s2.assertFormula(function2.eqTerm(value1));
|
|
s2.checkSat();
|
|
value2 = s2.getValue(function2);
|
|
}
|
|
ASSERT_EQ(value1, value2);
|
|
{
|
|
Solver s3;
|
|
s3.setLogic("ALL");
|
|
s3.setOption("produce-models", "true");
|
|
function2 = s3.declareFun("function3", {}, integerSort);
|
|
Term apply = s3.mkTerm(APPLY_UF, {definedFunction, zero});
|
|
s3.assertFormula(function2.eqTerm(apply));
|
|
s3.checkSat();
|
|
Term value3 = s3.getValue(function2);
|
|
ASSERT_EQ(value1, value3);
|
|
}
|
|
}
|
|
|
|
} // namespace test
|
|
} // namespace cvc5::internal
|