From 96dcf80d249ecbf12f1e3a0cd473deade007a1c3 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 13 Jul 2018 03:04:49 -0700 Subject: New C++ API: Minor reorder. (#2163) --- src/api/cvc4cpp.cpp | 311 ++++++++++++++++++++++++++-------------------------- 1 file changed, 155 insertions(+), 156 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 958438751..488590deb 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1491,7 +1491,158 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const /* Solver */ /* -------------------------------------------------------------------------- */ -/* Create constants --------------------------------------------------------- */ +Solver::Solver(Options* opts) + : d_opts(new Options()) +{ + if (opts) d_opts->copyValues(*opts); + d_exprMgr = std::unique_ptr(new ExprManager(*d_opts)); + d_smtEngine = std::unique_ptr(new SmtEngine(d_exprMgr.get())); + d_rng = std::unique_ptr(new Random((*d_opts)[options::seed])); +} + +Solver::~Solver() {} + +/* Sorts Handling */ +/* -------------------------------------------------------------------------- */ + +Sort Solver::getBooleanSort(void) const { return d_exprMgr->booleanType(); } + +Sort Solver::getIntegerSort(void) const { return d_exprMgr->integerType(); } + +Sort Solver::getRealSort(void) const { return d_exprMgr->realType(); } + +Sort Solver::getRegExpSort(void) const { return d_exprMgr->regExpType(); } + +Sort Solver::getStringSort(void) const { return d_exprMgr->stringType(); } + +Sort Solver::getRoundingmodeSort(void) const +{ + return d_exprMgr->roundingModeType(); +} + +/* Create sorts ------------------------------------------------------- */ + +Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const +{ + // CHECK: indexSort exists + // CHECK: elemSort exists + return d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type); +} + +Sort Solver::mkBitVectorSort(uint32_t size) const +{ + // CHECK: size > 0 + return d_exprMgr->mkBitVectorType(size); +} + +Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const +{ + // CHECK: num constructors > 0 + return d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype); +} + +Sort Solver::mkFunctionSort(Sort domain, Sort range) const +{ + // CHECK: domain exists + // CHECK: range exists + // CHECK: + // domain.isFirstClass() + // else "can not create function type for domain type that is not + // first class" + // CHECK: + // range.isFirstClass() + // else "can not create function type for range type that is not + // first class" + // CHECK: + // !range.isFunction() + // else "must flatten function types" + return d_exprMgr->mkFunctionType(*domain.d_type, *range.d_type); +} + +Sort Solver::mkFunctionSort(const std::vector& argSorts, Sort range) const +{ + // CHECK: for all s in argSorts, s exists + // CHECK: range exists + // CHECK: argSorts.size() >= 1 + // CHECK: + // for (unsigned i = 0; i < argSorts.size(); ++ i) + // argSorts[i].isFirstClass() + // else "can not create function type for argument type that is not + // first class" + // CHECK: + // range.isFirstClass() + // else "can not create function type for range type that is not + // first class" + // CHECK: + // !range.isFunction() + // else "must flatten function types" + std::vector argTypes = sortVectorToTypes(argSorts); + return d_exprMgr->mkFunctionType(argTypes, *range.d_type); +} + +Sort Solver::mkParamSort(const std::string& symbol) const +{ + return d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER); +} + +Sort Solver::mkPredicateSort(const std::vector& sorts) const +{ + // CHECK: for all s in sorts, s exists + // CHECK: sorts.size() >= 1 + // CHECK: + // for (unsigned i = 0; i < sorts.size(); ++ i) + // sorts[i].isFirstClass() + // else "can not create predicate type for argument type that is not + // first class" + std::vector types = sortVectorToTypes(sorts); + return d_exprMgr->mkPredicateType(types); +} + +Sort Solver::mkRecordSort( + const std::vector>& fields) const +{ + std::vector> f; + for (const auto& p : fields) + { + f.emplace_back(p.first, *p.second.d_type); + } + return d_exprMgr->mkRecordType(Record(f)); +} + +Sort Solver::mkSetSort(Sort elemSort) const +{ + return d_exprMgr->mkSetType(*elemSort.d_type); +} + +Sort Solver::mkUninterpretedSort(const std::string& symbol) const +{ + return d_exprMgr->mkSort(symbol); +} + +Sort Solver::mkTupleSort(const std::vector& sorts) const +{ + // CHECK: for all s in sorts, s exists + // CHECK: + // for (unsigned i = 0; i < sorts.size(); ++ i) + // !sorts[i].isFunctionLike() + // else "function-like types in tuples not allowed" + std::vector types = sortVectorToTypes(sorts); + return d_exprMgr->mkTupleType(types); +} + +std::vector Solver::sortVectorToTypes( + const std::vector& sorts) const +{ + std::vector res; + for (const Sort& s : sorts) + { + res.push_back(*s.d_type); + } + return res; +} + +/* Create consts */ +/* -------------------------------------------------------------------------- */ Term Solver::mkTrue(void) const { return d_exprMgr->mkConst(true); } @@ -1810,7 +1961,8 @@ Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst())); } -/* Create variables --------------------------------------------------- */ +/* Create variables */ +/* -------------------------------------------------------------------------- */ Term Solver::mkVar(const std::string& symbol, Sort sort) const { @@ -1836,161 +1988,8 @@ Term Solver::mkBoundVar(Sort sort) const return d_exprMgr->mkBoundVar(*sort.d_type); } +/* Create terms */ /* -------------------------------------------------------------------------- */ -/* Solver */ -/* -------------------------------------------------------------------------- */ - -Solver::Solver(Options* opts) - : d_opts(new Options()) -{ - if (opts) d_opts->copyValues(*opts); - d_exprMgr = std::unique_ptr(new ExprManager(*d_opts)); - d_smtEngine = std::unique_ptr(new SmtEngine(d_exprMgr.get())); - d_rng = std::unique_ptr(new Random((*d_opts)[options::seed])); -} - -Solver::~Solver() {} - -/* Sorts Handling */ -/* -------------------------------------------------------------------------- */ - -Sort Solver::getBooleanSort(void) const { return d_exprMgr->booleanType(); } - -Sort Solver::getIntegerSort(void) const { return d_exprMgr->integerType(); } - -Sort Solver::getRealSort(void) const { return d_exprMgr->realType(); } - -Sort Solver::getRegExpSort(void) const { return d_exprMgr->regExpType(); } - -Sort Solver::getStringSort(void) const { return d_exprMgr->stringType(); } - -Sort Solver::getRoundingmodeSort(void) const -{ - return d_exprMgr->roundingModeType(); -} - -/* Create sorts ------------------------------------------------------- */ - -Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const -{ - // CHECK: indexSort exists - // CHECK: elemSort exists - return d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type); -} - -Sort Solver::mkBitVectorSort(uint32_t size) const -{ - // CHECK: size > 0 - return d_exprMgr->mkBitVectorType(size); -} - -Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const -{ - // CHECK: num constructors > 0 - return d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype); -} - -Sort Solver::mkFunctionSort(Sort domain, Sort range) const -{ - // CHECK: domain exists - // CHECK: range exists - // CHECK: - // domain.isFirstClass() - // else "can not create function type for domain type that is not - // first class" - // CHECK: - // range.isFirstClass() - // else "can not create function type for range type that is not - // first class" - // CHECK: - // !range.isFunction() - // else "must flatten function types" - return d_exprMgr->mkFunctionType(*domain.d_type, *range.d_type); -} - -Sort Solver::mkFunctionSort(const std::vector& argSorts, Sort range) const -{ - // CHECK: for all s in argSorts, s exists - // CHECK: range exists - // CHECK: argSorts.size() >= 1 - // CHECK: - // for (unsigned i = 0; i < argSorts.size(); ++ i) - // argSorts[i].isFirstClass() - // else "can not create function type for argument type that is not - // first class" - // CHECK: - // range.isFirstClass() - // else "can not create function type for range type that is not - // first class" - // CHECK: - // !range.isFunction() - // else "must flatten function types" - std::vector argTypes = sortVectorToTypes(argSorts); - return d_exprMgr->mkFunctionType(argTypes, *range.d_type); -} - -Sort Solver::mkParamSort(const std::string& symbol) const -{ - return d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER); -} - -Sort Solver::mkPredicateSort(const std::vector& sorts) const -{ - // CHECK: for all s in sorts, s exists - // CHECK: sorts.size() >= 1 - // CHECK: - // for (unsigned i = 0; i < sorts.size(); ++ i) - // sorts[i].isFirstClass() - // else "can not create predicate type for argument type that is not - // first class" - std::vector types = sortVectorToTypes(sorts); - return d_exprMgr->mkPredicateType(types); -} - -Sort Solver::mkRecordSort( - const std::vector>& fields) const -{ - std::vector> f; - for (const auto& p : fields) - { - f.emplace_back(p.first, *p.second.d_type); - } - return d_exprMgr->mkRecordType(Record(f)); -} - -Sort Solver::mkSetSort(Sort elemSort) const -{ - return d_exprMgr->mkSetType(*elemSort.d_type); -} - -Sort Solver::mkUninterpretedSort(const std::string& symbol) const -{ - return d_exprMgr->mkSort(symbol); -} - -Sort Solver::mkTupleSort(const std::vector& sorts) const -{ - // CHECK: for all s in sorts, s exists - // CHECK: - // for (unsigned i = 0; i < sorts.size(); ++ i) - // !sorts[i].isFunctionLike() - // else "function-like types in tuples not allowed" - std::vector types = sortVectorToTypes(sorts); - return d_exprMgr->mkTupleType(types); -} - -std::vector Solver::sortVectorToTypes( - const std::vector& sorts) const -{ - std::vector res; - for (const Sort& s : sorts) - { - res.push_back(*s.d_type); - } - return res; -} - -/* Create terms ------------------------------------------------------- */ Term Solver::mkTerm(Kind kind) const { -- cgit v1.2.3