From: Aina Niemetz Date: Mon, 23 Jul 2018 21:38:37 +0000 (-0700) Subject: New C++ API: Implementation of Solver class: OpTerm handling. (#2164) X-Git-Tag: cvc5-1.0.0~4875 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=03925b816a0f9aeb079e2c0037a426b5946e2eae;p=cvc5.git New C++ API: Implementation of Solver class: OpTerm handling. (#2164) --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 938dc127d..53b87f2fa 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -100,7 +100,6 @@ std::ostream& operator<<(std::ostream& out, const Result& r) return out; } - /* -------------------------------------------------------------------------- */ /* Kind */ /* -------------------------------------------------------------------------- */ @@ -605,20 +604,26 @@ const static std::unordered_map }; namespace { - Kind intToExtKind(CVC4::Kind k) +Kind intToExtKind(CVC4::Kind k) +{ + auto it = s_kinds_internal.find(k); + if (it == s_kinds_internal.end()) { - auto it = s_kinds_internal.find(k); - if (it == s_kinds_internal.end()) { return INTERNAL_KIND; } - return it->second; + return INTERNAL_KIND; } + return it->second; +} - CVC4::Kind extToIntKind(Kind k) +CVC4::Kind extToIntKind(Kind k) +{ + auto it = s_kinds.find(k); + if (it == s_kinds.end()) { - auto it = s_kinds.find(k); - if (it == s_kinds.end()) { return CVC4::Kind::UNDEFINED_KIND; } - return it->second; + return CVC4::Kind::UNDEFINED_KIND; } + return it->second; } +} // namespace std::ostream& operator<<(std::ostream& out, Kind k) { @@ -632,18 +637,13 @@ std::ostream& operator<<(std::ostream& out, Kind k) size_t KindHashFunction::operator()(Kind k) const { return k; } - /* -------------------------------------------------------------------------- */ /* Sort */ /* -------------------------------------------------------------------------- */ -Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) -{ -} +Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) {} -Sort::~Sort() -{ -} +Sort::~Sort() {} Sort& Sort::operator=(const Sort& s) { @@ -780,14 +780,17 @@ Sort Sort::instantiate(const std::vector& params) const { // CHECK: Is this a datatype/sort constructor sort? std::vector tparams; - for (const Sort& s : params) { tparams.push_back(*s.d_type.get()); } + for (const Sort& s : params) + { + tparams.push_back(*s.d_type.get()); + } if (d_type->isDatatype()) { // CHECK: is parametric? DatatypeType* type = static_cast(d_type.get()); return type->instantiate(tparams); } - Assert (d_type->isSortConstructor()); + Assert(d_type->isSortConstructor()); return static_cast(d_type.get())->instantiate(tparams); } @@ -797,32 +800,26 @@ std::string Sort::toString() const return d_type->toString(); } -std::ostream& operator<< (std::ostream& out, const Sort& s) +std::ostream& operator<<(std::ostream& out, const Sort& s) { out << s.toString(); return out; } -size_t SortHashFunction::operator()(const Sort& s) const { +size_t SortHashFunction::operator()(const Sort& s) const +{ return TypeHashFunction()(*s.d_type); } - /* -------------------------------------------------------------------------- */ /* Term */ /* -------------------------------------------------------------------------- */ -Term::Term() : d_expr(new CVC4::Expr()) -{ -} +Term::Term() : d_expr(new CVC4::Expr()) {} -Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) -{ -} +Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {} -Term::~Term() -{ -} +Term::~Term() {} Term& Term::operator=(const Term& t) { @@ -846,68 +843,34 @@ bool Term::operator!=(const Term& t) const return *d_expr != *t.d_expr; } -Kind Term::getKind() const -{ - return intToExtKind(d_expr->getKind()); -} +Kind Term::getKind() const { return intToExtKind(d_expr->getKind()); } -Sort Term::getSort() const -{ - return Sort(d_expr->getType()); -} +Sort Term::getSort() const { return Sort(d_expr->getType()); } -bool Term::isNull() const -{ - return d_expr->isNull(); -} +bool Term::isNull() const { return d_expr->isNull(); } -Term Term::notTerm() const -{ - return d_expr->notExpr(); -} +Term Term::notTerm() const { return d_expr->notExpr(); } -Term Term::andTerm(const Term& t) const -{ - return d_expr->andExpr(*t.d_expr); -} +Term Term::andTerm(const Term& t) const { return d_expr->andExpr(*t.d_expr); } -Term Term::orTerm(const Term& t) const -{ - return d_expr->orExpr(*t.d_expr); -} +Term Term::orTerm(const Term& t) const { return d_expr->orExpr(*t.d_expr); } -Term Term::xorTerm(const Term& t) const -{ - return d_expr->xorExpr(*t.d_expr); -} +Term Term::xorTerm(const Term& t) const { return d_expr->xorExpr(*t.d_expr); } -Term Term::iffTerm(const Term& t) const -{ - return d_expr->iffExpr(*t.d_expr); -} +Term Term::iffTerm(const Term& t) const { return d_expr->iffExpr(*t.d_expr); } -Term Term::impTerm(const Term& t) const -{ - return d_expr->impExpr(*t.d_expr); -} +Term Term::impTerm(const Term& t) const { return d_expr->impExpr(*t.d_expr); } Term Term::iteTerm(const Term& then_t, const Term& else_t) const { return d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr); } -std::string Term::toString() const -{ - return d_expr->toString(); -} +std::string Term::toString() const { return d_expr->toString(); } -Term::const_iterator::const_iterator() : d_iterator(nullptr) -{ -} +Term::const_iterator::const_iterator() : d_iterator(nullptr) {} -Term::const_iterator::const_iterator(void* it) : d_iterator(it) -{ -} +Term::const_iterator::const_iterator(void* it) : d_iterator(it) {} Term::const_iterator::const_iterator(const const_iterator& it) : d_iterator(nullptr) @@ -978,7 +941,7 @@ Term::const_iterator Term::end() const return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->end())); } -std::ostream& operator<< (std::ostream& out, const Term& t) +std::ostream& operator<<(std::ostream& out, const Term& t) { out << t.toString(); return out; @@ -1029,17 +992,11 @@ size_t TermHashFunction::operator()(const Term& t) const /* OpTerm */ /* -------------------------------------------------------------------------- */ -OpTerm::OpTerm() : d_expr(new CVC4::Expr()) -{ -} +OpTerm::OpTerm() : d_expr(new CVC4::Expr()) {} -OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) -{ -} +OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {} -OpTerm::~OpTerm() -{ -} +OpTerm::~OpTerm() {} OpTerm& OpTerm::operator=(const OpTerm& t) { @@ -1063,27 +1020,15 @@ bool OpTerm::operator!=(const OpTerm& t) const return *d_expr != *t.d_expr; } -Kind OpTerm::getKind() const -{ - return intToExtKind(d_expr->getKind()); -} +Kind OpTerm::getKind() const { return intToExtKind(d_expr->getKind()); } -Sort OpTerm::getSort() const -{ - return Sort(d_expr->getType()); -} +Sort OpTerm::getSort() const { return Sort(d_expr->getType()); } -bool OpTerm::isNull() const -{ - return d_expr->isNull(); -} +bool OpTerm::isNull() const { return d_expr->isNull(); } -std::string OpTerm::toString() const -{ - return d_expr->toString(); -} +std::string OpTerm::toString() const { return d_expr->toString(); } -std::ostream& operator<< (std::ostream& out, const OpTerm& t) +std::ostream& operator<<(std::ostream& out, const OpTerm& t) { out << t.toString(); return out; @@ -1209,19 +1154,14 @@ std::ostream& operator<<(std::ostream& out, /* DatatypeSelector --------------------------------------------------------- */ -DatatypeSelector::DatatypeSelector() -{ - d_stor = nullptr; -} +DatatypeSelector::DatatypeSelector() { d_stor = nullptr; } DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor) : d_stor(new CVC4::DatatypeConstructorArg(stor)) { } -DatatypeSelector::~DatatypeSelector() -{ -} +DatatypeSelector::~DatatypeSelector() {} std::string DatatypeSelector::toString() const { @@ -1238,19 +1178,14 @@ std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor) /* DatatypeConstructor ------------------------------------------------------ */ -DatatypeConstructor::DatatypeConstructor() -{ - d_ctor = nullptr; -} +DatatypeConstructor::DatatypeConstructor() { d_ctor = nullptr; } DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor) -: d_ctor(new CVC4::DatatypeConstructor(ctor)) + : d_ctor(new CVC4::DatatypeConstructor(ctor)) { } -DatatypeConstructor::~DatatypeConstructor() -{ -} +DatatypeConstructor::~DatatypeConstructor() {} DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const { @@ -1360,13 +1295,11 @@ std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor) /* Datatype ----------------------------------------------------------------- */ Datatype::Datatype(const CVC4::Datatype& dtype) -: d_dtype(new CVC4::Datatype(dtype)) + : d_dtype(new CVC4::Datatype(dtype)) { } -Datatype::~Datatype() -{ -} +Datatype::~Datatype() {} DatatypeConstructor Datatype::operator[](const std::string& name) const { @@ -1399,11 +1332,12 @@ Datatype::const_iterator Datatype::end() const return Datatype::const_iterator(*d_dtype, false); } -Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype, bool begin) +Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype, + bool begin) { d_int_ctors = dtype.getConstructors(); const std::vector* cons = - static_cast*>(d_int_ctors); + static_cast*>(d_int_ctors); for (const auto& c : *cons) { /* Can not use emplace_back here since constructor is private. */ @@ -1460,27 +1394,30 @@ bool Datatype::const_iterator::operator!=( /* Rounding Mode for Floating Points */ /* -------------------------------------------------------------------------- */ -const static std::unordered_map s_rmodes -{ - { ROUND_NEAREST_TIES_TO_EVEN, CVC4::RoundingMode::roundNearestTiesToEven }, - { ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::roundTowardPositive }, - { ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::roundTowardNegative }, - { ROUND_TOWARD_ZERO, CVC4::RoundingMode::roundTowardZero }, - { ROUND_NEAREST_TIES_TO_AWAY, CVC4::RoundingMode::roundNearestTiesToAway }, -}; +const static std:: + unordered_map + s_rmodes{ + {ROUND_NEAREST_TIES_TO_EVEN, + CVC4::RoundingMode::roundNearestTiesToEven}, + {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::roundTowardPositive}, + {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::roundTowardNegative}, + {ROUND_TOWARD_ZERO, CVC4::RoundingMode::roundTowardZero}, + {ROUND_NEAREST_TIES_TO_AWAY, + CVC4::RoundingMode::roundNearestTiesToAway}, + }; const static std::unordered_map s_rmodes_internal -{ - { CVC4::RoundingMode::roundNearestTiesToEven, ROUND_NEAREST_TIES_TO_EVEN }, - { CVC4::RoundingMode::roundTowardPositive, ROUND_TOWARD_POSITIVE }, - { CVC4::RoundingMode::roundTowardNegative, ROUND_TOWARD_NEGATIVE }, - { CVC4::RoundingMode::roundTowardZero, ROUND_TOWARD_ZERO }, - { CVC4::RoundingMode::roundNearestTiesToAway, ROUND_NEAREST_TIES_TO_AWAY }, -}; + RoundingMode, + CVC4::RoundingModeHashFunction> + s_rmodes_internal{ + {CVC4::RoundingMode::roundNearestTiesToEven, + ROUND_NEAREST_TIES_TO_EVEN}, + {CVC4::RoundingMode::roundTowardPositive, ROUND_TOWARD_POSITIVE}, + {CVC4::RoundingMode::roundTowardNegative, ROUND_TOWARD_NEGATIVE}, + {CVC4::RoundingMode::roundTowardZero, ROUND_TOWARD_ZERO}, + {CVC4::RoundingMode::roundNearestTiesToAway, + ROUND_NEAREST_TIES_TO_AWAY}, + }; size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const { @@ -1491,8 +1428,7 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const /* Solver */ /* -------------------------------------------------------------------------- */ -Solver::Solver(Options* opts) - : d_opts(new Options()) +Solver::Solver(Options* opts) : d_opts(new Options()) { if (opts) d_opts->copyValues(*opts); d_exprMgr = std::unique_ptr(new ExprManager(*d_opts)); @@ -2213,6 +2149,105 @@ std::vector Solver::termVectorToExprs( return res; } +/* Create operator terms */ +/* -------------------------------------------------------------------------- */ + +OpTerm Solver::mkOpTerm(Kind kind, Kind k) +{ + // CHECK: kind == CHAIN_OP + return d_exprMgr->mkConst(CVC4::Chain(extToIntKind(k))); +} + +OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) +{ + // CHECK: + // kind == RECORD_UPDATE_OP + return d_exprMgr->mkConst(CVC4::RecordUpdate(arg)); +} + +OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) +{ + OpTerm res; + switch (kind) + { + case DIVISIBLE_OP: res = d_exprMgr->mkConst(CVC4::Divisible(arg)); break; + case BITVECTOR_REPEAT_OP: + res = d_exprMgr->mkConst(CVC4::BitVectorRepeat(arg)); + break; + case BITVECTOR_ZERO_EXTEND_OP: + res = d_exprMgr->mkConst(CVC4::BitVectorZeroExtend(arg)); + break; + case BITVECTOR_SIGN_EXTEND_OP: + res = d_exprMgr->mkConst(CVC4::BitVectorSignExtend(arg)); + break; + case BITVECTOR_ROTATE_LEFT_OP: + res = d_exprMgr->mkConst(CVC4::BitVectorRotateLeft(arg)); + break; + case BITVECTOR_ROTATE_RIGHT_OP: + res = d_exprMgr->mkConst(CVC4::BitVectorRotateRight(arg)); + break; + case INT_TO_BITVECTOR_OP: + res = d_exprMgr->mkConst(CVC4::IntToBitVector(arg)); + break; + case FLOATINGPOINT_TO_UBV_OP: + res = d_exprMgr->mkConst(CVC4::FloatingPointToUBV(arg)); + break; + case FLOATINGPOINT_TO_UBV_TOTAL_OP: + res = d_exprMgr->mkConst(CVC4::FloatingPointToUBVTotal(arg)); + break; + case FLOATINGPOINT_TO_SBV_OP: + res = d_exprMgr->mkConst(CVC4::FloatingPointToSBV(arg)); + break; + case FLOATINGPOINT_TO_SBV_TOTAL_OP: + res = d_exprMgr->mkConst(CVC4::FloatingPointToSBVTotal(arg)); + break; + case TUPLE_UPDATE_OP: + res = d_exprMgr->mkConst(CVC4::TupleUpdate(arg)); + break; + default: + // CHECK: kind valid? + Assert(!res.isNull()); + } + return res; +} + +OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) +{ + OpTerm res; + switch (kind) + { + case BITVECTOR_EXTRACT_OP: + res = d_exprMgr->mkConst(CVC4::BitVectorExtract(arg1, arg2)); + break; + case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: + res = + d_exprMgr->mkConst(CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)); + break; + case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: + res = + d_exprMgr->mkConst(CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)); + break; + case FLOATINGPOINT_TO_FP_REAL_OP: + res = d_exprMgr->mkConst(CVC4::FloatingPointToFPReal(arg1, arg2)); + break; + case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: + res = d_exprMgr->mkConst( + CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)); + break; + case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: + res = d_exprMgr->mkConst( + CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)); + break; + case FLOATINGPOINT_TO_FP_GENERIC_OP: + res = d_exprMgr->mkConst(CVC4::FloatingPointToFPGeneric(arg1, arg2)); + break; + default: + // CHECK: kind valid? + Assert(!res.isNull()); + } + return res; +} + /** * ( declare-datatype ) */