diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bea9bec6de0..e825ab3d197 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -49,10 +49,11 @@ jobs: - name: ubuntu:production-dbg os: ubuntu-18.04 - config: production --auto-download --assertions --tracing --unit-testing --java-bindings --editline + config: production --auto-download --assertions --tracing --unit-testing --all-bindings --editline cache-key: dbg exclude_regress: 3-4 run_regression_args: --tester base --tester model --tester synth --tester abduct --tester proof --tester dump + python-bindings: true - name: ubuntu:production-dbg-clang os: ubuntu-latest diff --git a/docs/theories/bags.rst b/docs/theories/bags.rst new file mode 100644 index 00000000000..a458b44b2f1 --- /dev/null +++ b/docs/theories/bags.rst @@ -0,0 +1,86 @@ +Theory Reference: Bags +==================================== + +Finite Bags +----------- + +cvc5 supports the theory of finite bags using the following sorts, constants, +functions and predicates. + +For the C++ API examples in the table below, we assume that we have created +a `cvc5::api::Solver solver` object. + ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| | SMTLIB language | C++ API | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Logic String | ``(set-logic ALL)`` | ``solver.setLogic("ALL");`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Sort | ``(Bag )`` | ``solver.mkBagSort(cvc5::api::Sort elementSort);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Constants | ``(declare-const X (Bag String)`` | ``Sort s = solver.mkBagSort(solver.getStringSort());`` | +| | | | +| | | ``Term X = solver.mkConst(s, "X");`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Union disjoint | ``(bag.union_disjoint X Y)`` | ``Term Y = solver.mkConst(s, "Y");`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::BAG_UNION_DISJOINT, X, Y);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Union max | ``(bag.union_max X Y)`` | ``Term Y = solver.mkConst(s, "Y");`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::BAG_UNION_MAX, X, Y);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Intersection min | ``(bag.inter_min X Y)`` | ``Term t = solver.mkTerm(Kind::BAG_INTER_MIN, X, Y);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Difference subtract | ``(bag.difference_subtract X Y)`` | ``Term t = solver.mkTerm(Kind::BAG_DIFFERENCE_SUBTRACT, X, Y);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Duplicate elimination| ``(bag.duplicate_removal X)`` | ``Term t = solver.mkTerm(Kind::BAG_DUPLICATE_REMOVAL, X);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Membership | ``(bag.member x X)`` | ``Term x = solver.mkConst(solver.getStringSort(), "x");`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::BAG_MEMBER, x, X);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Subbag | ``(bag.subbag X Y)`` | ``Term t = solver.mkTerm(Kind::BAG_SUBBAG, X, Y);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Emptybag | ``(as bag.empty (Bag Int)`` | ``Term t = solver.mkEmptyBag(s);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Make bag | ``(bag "a" 3)`` | ``Term t = solver.mkTerm(Kind::BAG_MAKE,`` | +| | | ``solver.mkString("a"), solver.mkInteger(1));`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ + + +Semantics +^^^^^^^^^ + +A bag (or a multiset) :math:`m` can be defined as a function from the domain of its elements +to the set of natural numbers (i.e., :math:`m : D \rightarrow \mathbb{N}`), +where :math:`m(e)` represents the multiplicity of element :math:`e` in the bag :math:`m`. + +The semantics of supported bag operators is given in the table below. + ++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ +| Bag operator | cvc5 operator | Semantics | ++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ +| union disjoint :math:`m_1 \uplus m_2` | bag.union_disjoint | :math:`\forall e. \; (m_1 \uplus m_2)(e) = m_1(e) + m_2 (e)` | ++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ +| union max :math:`m_1 \cup m_2` | bag.union_max | :math:`\forall e. \; (m_1 \cup m_2)(e) = max(m_1(e), m_2 (e))` | ++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ +| intersection :math:`m_1 \cap m_2` | bag.inter_min | :math:`\forall e. \; (m_1 \cap m_2)(e) = min(m_1(e), m_2 (e))` | ++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ +| difference subtract :math:`m_1 \setminus m_2` | bag.difference_subtract | :math:`\forall e. \; (m_1 \setminus m_2)(e) = max(m_1(e) - m_2 (e), 0)` | ++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ +| difference remove :math:`m_1 \setminus\setminus m_2`| bag.difference_remove | :math:`\forall e. \; (m_1 \setminus\setminus m_2)(e) = ite(m_2(e) = 0, m_1(e), 0)` | ++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ +| duplicate elimination :math:`\delta(m)` | bag.duplicate_removal | :math:`\forall e. \; (\delta(m))(e) = ite(1 \leq m(e), 1, 0)` | ++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ +| subbag :math:`m_1 \subseteq m_2` | bag.subbag | :math:`\forall e. \; m_1(e) \leq m_2(e)` | ++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ +| equality :math:`m_1 = m_2` | = | :math:`\forall e. \; m_1(e) = m_2(e)` | ++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ +| membership :math:`e \in m` | bag.member | :math:`m(e) \geq 1` | ++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ + +Below is a more extensive example on how to use finite bags: + +.. api-examples:: + /api/smtlib/bags.smt2 + diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index 493561a6890..768c88ba3cb 100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -17,7 +17,7 @@ ## import cvc5 -from cvc5 import Kind +from cvc5 import Kind, RoundingMode if __name__ == "__main__": slv = cvc5.Solver() @@ -29,7 +29,7 @@ fp32 = slv.mkFloatingPointSort(8, 24) # the standard rounding mode - rm = slv.mkRoundingMode(cvc5.RoundNearestTiesToEven) + rm = slv.mkRoundingMode(RoundingMode.RoundNearestTiesToEven) # create a few single-precision variables x = slv.mkConst(fp32, 'x') diff --git a/examples/api/smtlib/bags.smt2 b/examples/api/smtlib/bags.smt2 new file mode 100644 index 00000000000..785a8d379d6 --- /dev/null +++ b/examples/api/smtlib/bags.smt2 @@ -0,0 +1,47 @@ +(set-logic ALL) + +(set-option :produce-models true) +(set-option :incremental true) + +(declare-const A (Bag String)) +(declare-const B (Bag String)) +(declare-const C (Bag String)) +(declare-const x String) + +; union disjoint does not distribute over intersection +; sat +(check-sat-assuming + ((distinct + (bag.inter_min (bag.union_disjoint A B) C) + (bag.union_disjoint (bag.inter_min A C) (bag.inter_min B C))))) + + +(get-value (A)) +(get-value (B)) +(get-value (C)) +(get-value ((bag.inter_min (bag.union_disjoint A B) C))) +(get-value ((bag.union_disjoint (bag.inter_min A C) (bag.inter_min B C)))) + +; union max distributes over intersection +; unsat +(check-sat-assuming + ((distinct + (bag.inter_min (bag.union_max A B) C) + (bag.union_max (bag.inter_min A C) (bag.inter_min B C))))) + +; Verify emptbag is a subbag of any bag +; unsat +(check-sat-assuming + ((not (bag.subbag (as bag.empty (Bag String)) A)))) + +; find an element with multiplicity 4 in the disjoint union of +; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|} +(check-sat-assuming + ((= 4 + (bag.count x + (bag.union_disjoint + (bag.union_disjoint (bag "a" 2) (bag "b" 3)) + (bag.union_disjoint (bag "b" 1) (bag "c" 2))))))) + +; x is "b" +(get-value (x)) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 5b36f4d388d..d0f0957d2e8 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -719,6 +719,31 @@ const static std::unordered_set s_indexed_kinds( FLOATINGPOINT_TO_FP_FROM_SBV, FLOATINGPOINT_TO_FP_FROM_UBV}); +/* -------------------------------------------------------------------------- */ +/* Rounding Mode for Floating Points */ +/* -------------------------------------------------------------------------- */ + +const static std::unordered_map s_rmodes{ + {ROUND_NEAREST_TIES_TO_EVEN, + cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN}, + {ROUND_TOWARD_POSITIVE, cvc5::RoundingMode::ROUND_TOWARD_POSITIVE}, + {ROUND_TOWARD_NEGATIVE, cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE}, + {ROUND_TOWARD_ZERO, cvc5::RoundingMode::ROUND_TOWARD_ZERO}, + {ROUND_NEAREST_TIES_TO_AWAY, + cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY}, +}; + +const static std::unordered_map + s_rmodes_internal{ + {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN, + ROUND_NEAREST_TIES_TO_EVEN}, + {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_POSITIVE}, + {cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_NEGATIVE}, + {cvc5::RoundingMode::ROUND_TOWARD_ZERO, ROUND_TOWARD_ZERO}, + {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY, + ROUND_NEAREST_TIES_TO_AWAY}, + }; + namespace { /** Convert a cvc5::Kind (internal) to a cvc5::api::Kind (external). */ @@ -1378,13 +1403,23 @@ Datatype Sort::getDatatype() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isDatatype()) << "Expected datatype sort."; + CVC5_API_CHECK(d_type->isDatatype()) << "Expected datatype sort."; //////// all checks before this line return Datatype(d_solver, d_type->getDType()); //////// CVC5_API_TRY_CATCH_END; } +bool Sort::isInstantiated() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_type->isInstantiated(); + //////// + CVC5_API_TRY_CATCH_END; +} + Sort Sort::instantiate(const std::vector& params) const { CVC5_API_TRY_CATCH_BEGIN; @@ -1639,20 +1674,6 @@ Sort Sort::getSequenceElementSort() const /* Uninterpreted sort -------------------------------------------------- */ -bool Sort::isUninterpretedSortParameterized() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; - //////// all checks before this line - - /* This method is not implemented in the NodeManager, since whether a - * uninterpreted sort is parameterized is irrelevant for solving. */ - return d_type->getNumChildren() > 0; - //////// - CVC5_API_TRY_CATCH_END; -} - std::vector Sort::getUninterpretedSortParamSorts() const { CVC5_API_TRY_CATCH_BEGIN; @@ -1731,7 +1752,7 @@ std::vector Sort::getDatatypeParamSorts() const CVC5_API_CHECK(d_type->isParametricDatatype()) << "Not a parametric datatype sort."; //////// all checks before this line - return typeNodeVectorToSorts(d_solver, d_type->getParamTypes()); + return typeNodeVectorToSorts(d_solver, d_type->getDType().getParameters()); //////// CVC5_API_TRY_CATCH_END; } @@ -3013,6 +3034,29 @@ std::vector Term::getTupleValue() const CVC5_API_TRY_CATCH_END; } +bool Term::isRoundingModeValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getKind() == cvc5::Kind::CONST_ROUNDINGMODE; + //////// + CVC5_API_TRY_CATCH_END; +} +RoundingMode Term::getRoundingModeValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED( + d_node->getKind() == cvc5::Kind::CONST_ROUNDINGMODE, *d_node) + << "Term to be a floating-point rounding mode value when calling " + "getRoundingModeValue()"; + //////// all checks before this line + return s_rmodes_internal.at(d_node->getConst()); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Term::isFloatingPointPosZero() const { CVC5_API_TRY_CATCH_BEGIN; @@ -3184,6 +3228,40 @@ std::vector Term::getSequenceValue() const CVC5_API_TRY_CATCH_END; } +bool Term::isCardinalityConstraint() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getKind() == cvc5::Kind::CARDINALITY_CONSTRAINT; + //////// + CVC5_API_TRY_CATCH_END; +} + +std::pair Term::getCardinalityConstraint() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED( + d_node->getKind() == cvc5::Kind::CARDINALITY_CONSTRAINT, *d_node) + << "Term to be a cardinality constraint when calling " + "getCardinalityConstraint()"; + // this should never happen since we restrict what the user can create + CVC5_API_ARG_CHECK_EXPECTED(detail::checkIntegerBounds( + d_node->getOperator() + .getConst() + .getUpperBound()), + *d_node) + << "Upper bound for cardinality constraint does not fit uint32_t"; + //////// all checks before this line + const CardinalityConstraint& cc = + d_node->getOperator().getConst(); + return std::make_pair(Sort(d_solver, cc.getType()), + cc.getUpperBound().getUnsignedInt()); + //////// + CVC5_API_TRY_CATCH_END; +} + std::ostream& operator<<(std::ostream& out, const Term& t) { out << t.toString(); @@ -4547,33 +4625,6 @@ std::ostream& operator<<(std::ostream& out, const Grammar& grammar) return out << grammar.toString(); } -/* -------------------------------------------------------------------------- */ -/* Rounding Mode for Floating Points */ -/* -------------------------------------------------------------------------- */ - -const static std::unordered_map s_rmodes{ - {ROUND_NEAREST_TIES_TO_EVEN, - cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN}, - {ROUND_TOWARD_POSITIVE, cvc5::RoundingMode::ROUND_TOWARD_POSITIVE}, - {ROUND_TOWARD_NEGATIVE, cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE}, - {ROUND_TOWARD_ZERO, cvc5::RoundingMode::ROUND_TOWARD_ZERO}, - {ROUND_NEAREST_TIES_TO_AWAY, - cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY}, -}; - -const static std::unordered_map - s_rmodes_internal{ - {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN, - ROUND_NEAREST_TIES_TO_EVEN}, - {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_POSITIVE}, - {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_NEGATIVE}, - {cvc5::RoundingMode::ROUND_TOWARD_ZERO, ROUND_TOWARD_ZERO}, - {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY, - ROUND_NEAREST_TIES_TO_AWAY}, - }; - /* -------------------------------------------------------------------------- */ /* Options */ /* -------------------------------------------------------------------------- */ @@ -7143,9 +7194,9 @@ Term Solver::getInterpolant(const Term& conj) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); - CVC5_API_CHECK(d_slv->getOptions().smt.interpols) + CVC5_API_CHECK(d_slv->getOptions().smt.interpolants) << "Cannot get interpolant unless interpolants are enabled (try " - "--produce-interpols)"; + "--produce-interpolants)"; //////// all checks before this line TypeNode nullType; Node result = d_slv->getInterpolant(*conj.d_node, nullType); @@ -7158,9 +7209,9 @@ Term Solver::getInterpolant(const Term& conj, Grammar& grammar) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); - CVC5_API_CHECK(d_slv->getOptions().smt.interpols) + CVC5_API_CHECK(d_slv->getOptions().smt.interpolants) << "Cannot get interpolant unless interpolants are enabled (try " - "--produce-interpols)"; + "--produce-interpolants)"; //////// all checks before this line Node result = d_slv->getInterpolant(*conj.d_node, *grammar.resolve().d_type); return Term(this, result); @@ -7171,9 +7222,9 @@ Term Solver::getInterpolant(const Term& conj, Grammar& grammar) const Term Solver::getInterpolantNext() const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_slv->getOptions().smt.interpols) + CVC5_API_CHECK(d_slv->getOptions().smt.interpolants) << "Cannot get interpolant unless interpolants are enabled (try " - "--produce-interpols)"; + "--produce-interpolants)"; CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving) << "Cannot get next interpolant when not solving incrementally (try " "--incremental)"; @@ -7668,12 +7719,6 @@ size_t hash::operator()(const cvc5::api::Op& t) const } } -size_t std::hash::operator()( - cvc5::api::RoundingMode rm) const -{ - return static_cast(rm); -} - size_t std::hash::operator()(const cvc5::api::Sort& s) const { return std::hash()(*s.d_type); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index eb997636196..3576f1f00d7 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -549,6 +549,7 @@ class CVC5_EXPORT Sort /** * Is this a record sort? + * @warning This method is experimental and may change in future versions. * @return true if the sort is a record sort */ bool isRecord() const; @@ -593,6 +594,18 @@ class CVC5_EXPORT Sort */ bool isUninterpretedSortConstructor() const; + /** + * Is this an instantiated (parametric datatype or uninterpreted sort + * constructor) sort? + * + * An instantiated sort is a sort that has been constructed from + * instantiating a sort with sort arguments + * (see Sort::instantiate(const std::vector&) const)). + * + * @return true if this is an instantiated sort + */ + bool isInstantiated() const; + /** * @return the underlying datatype of a datatype sort */ @@ -604,14 +617,14 @@ class CVC5_EXPORT Sort * * Create sorts parameter with Solver::mkParamSort(). * + * @warning This method is experimental and may change in future versions. + * * @param params the list of sort parameters to instantiate with */ Sort instantiate(const std::vector& params) const; /** * Substitution of Sorts. - * @param sort the subsort to be substituted within this sort. - * @param replacement the sort replacing the substituted subsort. * * Note that this replacement is applied during a pre-order traversal and * only once to the sort. It is not run until fix point. @@ -619,18 +632,26 @@ class CVC5_EXPORT Sort * For example, * (Array A B).substitute({A, C}, {(Array C D), (Array A B)}) will * return (Array (Array C D) B). + * + * @warning This method is experimental and may change in future versions. + * + * @param sort the subsort to be substituted within this sort. + * @param replacement the sort replacing the substituted subsort. */ Sort substitute(const Sort& sort, const Sort& replacement) const; /** * Simultaneous substitution of Sorts. - * @param sorts the subsorts to be substituted within this sort. - * @param replacements the sort replacing the substituted subsorts. * * Note that this replacement is applied during a pre-order traversal and * only once to the sort. It is not run until fix point. In the case that * sorts contains duplicates, the replacement earliest in the vector takes * priority. + * + * @warning This method is experimental and may change in future versions. + * + * @param sorts the subsorts to be substituted within this sort. + * @param replacements the sort replacing the substituted subsorts. */ Sort substitute(const std::vector& sorts, const std::vector& replacements) const; @@ -1505,6 +1526,16 @@ class CVC5_EXPORT Term */ std::vector getTupleValue() const; + /** + * @return true if the term is a floating-point rounding mode value. + */ + bool isRoundingModeValue() const; + /** + * Asserts isRoundingModeValue(). + * @return the floating-point rounding mode value held by the term. + */ + RoundingMode getRoundingModeValue() const; + /** * @return true if the term is the floating-point value for positive zero. */ @@ -1576,6 +1607,16 @@ class CVC5_EXPORT Term */ std::vector getSequenceValue() const; + /** + * @return true if the term is a cardinality constraint + */ + bool isCardinalityConstraint() const; + /** + * Asserts isCardinalityConstraint(). + * @return the sort the cardinality constraint is for and its upper bound. + */ + std::pair getCardinalityConstraint() const; + protected: /** * The associated solver object. @@ -2036,6 +2077,8 @@ class CVC5_EXPORT DatatypeConstructor * `Solver::mkTerm(APPLY_CONSTRUCTOR, {t})` is used to construct the * above (nullary) application of nil. * + * @warning This method is experimental and may change in future versions. + * * @param retSort the desired return sort of the constructor * @return the constructor term */ @@ -2293,12 +2336,17 @@ class CVC5_EXPORT Datatype size_t getNumConstructors() const; /** + * @warning This method is experimental and may change in future versions. + * * @return the parameters of this datatype, if it is parametric. An exception * is thrown if this datatype is not parametric. */ std::vector getParameters() const; - /** @return true if this datatype is parametric */ + /** + * @warning This method is experimental and may change in future versions. + * @return true if this datatype is parametric + */ bool isParametric() const; /** @return true if this datatype corresponds to a co-datatype */ @@ -2307,7 +2355,10 @@ class CVC5_EXPORT Datatype /** @return true if this datatype corresponds to a tuple */ bool isTuple() const; - /** @return true if this datatype corresponds to a record */ + /** + * @warning This method is experimental and may change in future versions. + * @return true if this datatype corresponds to a record + */ bool isRecord() const; /** @return true if this datatype is finite */ @@ -2697,75 +2748,6 @@ class CVC5_EXPORT Grammar */ std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC5_EXPORT; -/* -------------------------------------------------------------------------- */ -/* Rounding Mode for Floating-Points */ -/* -------------------------------------------------------------------------- */ - -/** - * Rounding modes for floating-point numbers. - * - * For many floating-point operations, infinitely precise results may not be - * representable with the number of available bits. Thus, the results are - * rounded in a certain way to one of the representable floating-point numbers. - * - * \verbatim embed:rst:leading-asterisk - * These rounding modes directly follow the SMT-LIB theory for floating-point - * arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`. - * The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE - * Standard 754. - * \endverbatim - */ -enum RoundingMode -{ - /** - * Round to the nearest even number. - * If the two nearest floating-point numbers bracketing an unrepresentable - * infinitely precise result are equally near, the one with an even least - * significant digit will be delivered. - */ - ROUND_NEAREST_TIES_TO_EVEN, - /** - * Round towards positive infinity (+oo). - * The result shall be the format's floating-point number (possibly +oo) - * closest to and no less than the infinitely precise result. - */ - ROUND_TOWARD_POSITIVE, - /** - * Round towards negative infinity (-oo). - * The result shall be the format's floating-point number (possibly -oo) - * closest to and no less than the infinitely precise result. - */ - ROUND_TOWARD_NEGATIVE, - /** - * Round towards zero. - * The result shall be the format's floating-point number closest to and no - * greater in magnitude than the infinitely precise result. - */ - ROUND_TOWARD_ZERO, - /** - * Round to the nearest number away from zero. - * If the two nearest floating-point numbers bracketing an unrepresentable - * infinitely precise result are equally near, the one with larger magnitude - * will be selected. - */ - ROUND_NEAREST_TIES_TO_AWAY, -}; - -} // namespace cvc5::api - -namespace std { - -/** - * Hash function for RoundingModes. - */ -template <> -struct CVC5_EXPORT hash -{ - size_t operator()(cvc5::api::RoundingMode rm) const; -}; -} // namespace std -namespace cvc5::api { - /* -------------------------------------------------------------------------- */ /* Options */ /* -------------------------------------------------------------------------- */ @@ -3223,6 +3205,9 @@ class CVC5_EXPORT Solver /** * Create a sort parameter. + * + * @warning This method is experimental and may change in future versions. + * * @param symbol the name of the sort * @return the sort parameter */ @@ -3237,6 +3222,9 @@ class CVC5_EXPORT Solver /** * Create a record sort + * + * @warning This method is experimental and may change in future versions. + * * @param fields the list of fields of the record * @return the record sort */ @@ -3480,12 +3468,18 @@ class CVC5_EXPORT Solver /** * Create a separation logic empty term. + * + * @warning This method is experimental and may change in future versions. + * * @return the separation logic empty term */ Term mkSepEmp() const; /** * Create a separation logic nil term. + * + * @warning This method is experimental and may change in future versions. + * * @param sort the sort of the nil term * @return the separation logic nil term */ @@ -3613,6 +3607,9 @@ class CVC5_EXPORT Solver /** * Create a cardinality constraint for an uninterpreted sort. + * + * @warning This method is experimental and may change in future versions. + * * @param sort the sort the cardinality constraint is for * @param upperBound the upper bound on the cardinality of the sort * @return the cardinality constraint @@ -3662,6 +3659,11 @@ class CVC5_EXPORT Solver /* Create datatype constructor declarations */ /* .................................................................... */ + /** + * Create a datatype constructor declaration. + * @param name the name of the datatype constructor + * @return the DatatypeConstructorDecl + */ DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name); /* .................................................................... */ @@ -3710,6 +3712,9 @@ class CVC5_EXPORT Solver * the SAT Engine in the simplification, but uses the current * definitions, assertions, and the current partial model, if one * has been constructed. It also involves theory normalization. + * + * @warning This method is experimental and may change in future versions. + * * @param t the formula to simplify * @return the simplified formula */ @@ -4052,6 +4057,8 @@ class CVC5_EXPORT Solver * Get a difficulty estimate for an asserted formula. This method is * intended to be called immediately after any response to a checkSat. * + * @warning This method is experimental and may change in future versions. + * * @return a map from (a subset of) the input assertions to a real value that * is an estimate of how difficult each assertion was to solve. * Unmentioned assertions can be assumed to have zero difficulty. @@ -4072,16 +4079,20 @@ class CVC5_EXPORT Solver * :ref:`produce-proofs `. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @return a string representing the proof, according to the value of * proof-format-mode. */ std::string getProof() const; /** - * Get learned literals + * Get a list of learned literals that are entailed by the current set of + * assertions. * - * @return a list of literals that were learned at top-level. In other words, - * these are literals that are entailed by the current set of assertions. + * @warning This method is experimental and may change in future versions. + * + * @return a list of literals that were learned at top-level. */ std::vector getLearnedLiterals() const; @@ -4135,6 +4146,8 @@ class CVC5_EXPORT Solver * \verbatim embed:rst:inline :ref:`model-cores ` * \endverbatim has been set. * + * @warning This method is experimental and may change in future versions. + * * @param v The term in question * @return true if v is a model core symbol */ @@ -4154,6 +4167,8 @@ class CVC5_EXPORT Solver * :ref:`produce-models `. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @param sorts The list of uninterpreted sorts that should be printed in the * model. * @param vars The list of free constants that should be printed in the @@ -4174,10 +4189,10 @@ class CVC5_EXPORT Solver * (get-qe ) * \endverbatim * - * Requires a logic that supports quantifier elimination. Currently, the only - * logics supported by quantifier elimination is LRA and LIA. + * @note Quantifier Elimination is is only complete for logics such as LRA, + * LIA and BV. * - * @note Quantifier Elimination is is only complete for LRA and LIA. + * @warning This method is experimental and may change in future versions. * * @param q a quantified formula of the form * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$ @@ -4205,8 +4220,11 @@ class CVC5_EXPORT Solver * (get-qe-disjunct ) * \endverbatim * - * Requires a logic that supports quantifier elimination. Currently, the only - * logics supported by quantifier elimination is LRA and LIA. + * @note Quantifier Elimination is is only complete for logics such as LRA, + * LIA and BV. + * + * @warning This method is experimental and may change in future versions. + * * @param q a quantified formula of the form * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$ * where @@ -4242,6 +4260,9 @@ class CVC5_EXPORT Solver * When using separation logic, this sets the location sort and the * datatype sort to the given ones. This method should be invoked exactly * once, before any separation logic constraints are provided. + * + * @warning This method is experimental and may change in future versions. + * * @param locSort The location sort of the heap * @param dataSort The data sort of the heap */ @@ -4249,12 +4270,18 @@ class CVC5_EXPORT Solver /** * When using separation logic, obtain the term for the heap. + * + * @warning This method is experimental and may change in future versions. + * * @return The term for the heap */ Term getValueSepHeap() const; /** * When using separation logic, obtain the term for nil. + * + * @warning This method is experimental and may change in future versions. + * * @return The term for nil */ Term getValueSepNil() const; @@ -4273,6 +4300,8 @@ class CVC5_EXPORT Solver * (declare-pool ( * )) * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @param symbol The name of the pool * @param sort The sort of the elements of the pool. * @param initValue The initial value of the pool @@ -4304,12 +4333,13 @@ class CVC5_EXPORT Solver * \verbatim embed:rst:leading-asterisk * .. code:: smtlib * - * (get-interpol ) + * (get-interpolant ) * * Requires option - * :ref:`produce-interpols ` to be set to a - * mode different from `none`. - * \endverbatim + * :ref:`produce-interpolants ` to be set to + * a mode different from `none`. \endverbatim + * + * @warning This method is experimental and may change in future versions. * * @param conj the conjecture term * @return a Term I such that A->I and I->B are valid, where A is the @@ -4326,12 +4356,13 @@ class CVC5_EXPORT Solver * \verbatim embed:rst:leading-asterisk * .. code:: smtlib * - * (get-interpol ) + * (get-interpolant ) * * Requires option - * :ref:`produce-interpols ` to be set to a - * mode different from `none`. - * \endverbatim + * :ref:`produce-interpolants ` to be set to + * a mode different from `none`. \endverbatim + * + * @warning This method is experimental and may change in future versions. * * @param conj the conjecture term * @param grammar the grammar for the interpolant I @@ -4343,7 +4374,7 @@ class CVC5_EXPORT Solver /** * Get the next interpolant. Can only be called immediately after a successful - * call to get-interpol or get-interpol-next. Is guaranteed to produce a + * call to get-interpolant or get-interpolant-next. Is guaranteed to produce a * syntactically different interpolant wrt the last returned interpolant if * successful. * @@ -4352,12 +4383,13 @@ class CVC5_EXPORT Solver * \verbatim embed:rst:leading-asterisk * .. code:: smtlib * - * (get-interpol-next) + * (get-interpolant-next) * * Requires to enable incremental mode, and option - * :ref:`produce-interpols ` to be set to a - * mode different from `none`. - * \endverbatim + * :ref:`produce-interpolants ` to be set to + * a mode different from `none`. \endverbatim + * + * @warning This method is experimental and may change in future versions. * * @return a Term I such that A->I and I->B are valid, where A is the * current set of assertions and B is given in the input by conj @@ -4379,6 +4411,8 @@ class CVC5_EXPORT Solver * :ref:`produce-abducts `. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @param conj the conjecture term * @return a term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable, * and @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @@ -4402,6 +4436,9 @@ class CVC5_EXPORT Solver * :ref:`produce-abducts `. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * + * * @param conj the conjecture term * @param grammar the grammar for the abduct @f$C@f$ * @return a term C such that @f$(A \wedge C)@f$ is satisfiable, and @@ -4427,6 +4464,8 @@ class CVC5_EXPORT Solver * :ref:`produce-abducts `. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @return a term C such that @f$(A \wedge C)@f$ is satisfiable, and * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is * the current set of assertions and @f$B@f$ is given in the input by @@ -4452,6 +4491,8 @@ class CVC5_EXPORT Solver * :ref:`block-models `. * to a mode other than ``none``. * \endverbatim + * + * @warning This method is experimental and may change in future versions. */ void blockModel() const; @@ -4470,10 +4511,14 @@ class CVC5_EXPORT Solver * :ref:`produce-models `. * 'produce-models'. * \endverbatim + * + * @warning This method is experimental and may change in future versions. */ void blockModelValues(const std::vector& terms) const; /** + * @warning This method is experimental and may change in future versions. + * * @return a string that contains information about all instantiations made by * the quantifiers module. */ @@ -4555,17 +4600,6 @@ class CVC5_EXPORT Solver */ void setOption(const std::string& option, const std::string& value) const; - /** - * If needed, convert this term to a given sort. - * - * @note The sort of the term must be convertible into the target sort. - * Currently only Int to Real conversions are supported. - * @param t the term - * @param s the target sort - * @return the term wrapped into a sort conversion if needed - */ - Term ensureTermSort(const Term& t, const Sort& s) const; - /** * Append \p symbol to the current list of universal variables. * @@ -4913,6 +4947,18 @@ class CVC5_EXPORT Solver /** Check whether string s is a valid decimal integer. */ bool isValidInteger(const std::string& s) const; + /** + * If needed, convert this term to a given sort. + * + * The sort of the term must be convertible into the target sort. + * Currently only Int to Real conversions are supported. + * + * @param t the term + * @param s the target sort + * @return the term wrapped into a sort conversion if needed + */ + Term ensureTermSort(const Term& t, const Sort& s) const; + /** * Check that the given term is a valid closed term, which can be used as an * argument to, e.g., assert, get-value, block-model-values, etc. diff --git a/src/api/cpp/cvc5_types.h b/src/api/cpp/cvc5_types.h index 3ce20688b9c..a5cda3d6b92 100644 --- a/src/api/cpp/cvc5_types.h +++ b/src/api/cpp/cvc5_types.h @@ -18,6 +18,60 @@ #ifndef CVC5__API__CVC5_TYPES_H #define CVC5__API__CVC5_TYPES_H +namespace cvc5::api { + +/** + * Rounding modes for floating-point numbers. + * + * For many floating-point operations, infinitely precise results may not be + * representable with the number of available bits. Thus, the results are + * rounded in a certain way to one of the representable floating-point numbers. + * + * \verbatim embed:rst:leading-asterisk + * These rounding modes directly follow the SMT-LIB theory for floating-point + * arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`. + * The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE + * Standard 754. + * \endverbatim + */ +enum RoundingMode +{ + /** + * Round to the nearest even number. + * If the two nearest floating-point numbers bracketing an unrepresentable + * infinitely precise result are equally near, the one with an even least + * significant digit will be delivered. + */ + ROUND_NEAREST_TIES_TO_EVEN, + /** + * Round towards positive infinity (+oo). + * The result shall be the format's floating-point number (possibly +oo) + * closest to and no less than the infinitely precise result. + */ + ROUND_TOWARD_POSITIVE, + /** + * Round towards negative infinity (-oo). + * The result shall be the format's floating-point number (possibly -oo) + * closest to and no less than the infinitely precise result. + */ + ROUND_TOWARD_NEGATIVE, + /** + * Round towards zero. + * The result shall be the format's floating-point number closest to and no + * greater in magnitude than the infinitely precise result. + */ + ROUND_TOWARD_ZERO, + /** + * Round to the nearest number away from zero. + * If the two nearest floating-point numbers bracketing an unrepresentable + * infinitely precise result are equally near, the one with larger magnitude + * will be selected. + */ + ROUND_NEAREST_TIES_TO_AWAY, +}; + +} // namespace cvc5::api + namespace cvc5::modes { enum BlockModelsMode diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index da4fa60c4c5..bafda832350 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -41,6 +41,7 @@ add_custom_target(generate-java-kinds DEPENDS ${JAVA_KIND_FILE}) set(JAVA_TYPES_FILES "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/BlockModelsMode.java" + "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/RoundingMode.java" ) add_custom_command( OUTPUT @@ -78,7 +79,6 @@ set(JAVA_FILES ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/OptionInfo.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Pair.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Result.java - ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/RoundingMode.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Solver.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Sort.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Stat.java diff --git a/src/api/java/genenums.py.in b/src/api/java/genenums.py.in index 5ecd5bd401f..3b7260f4dbe 100644 --- a/src/api/java/genenums.py.in +++ b/src/api/java/genenums.py.in @@ -46,37 +46,50 @@ public enum {name} ENUM_JAVA_BOTTOM = \ r"""; - /* the int value of the kind */ + /* the int value of the {name} */ private int value; - private static Map kindMap = new HashMap<>(); - private Kind(int value) - { + private static int minValue = 0; + private static int maxValue = 0; + private static Map enumMap = new HashMap<>(); + + private {name}(int value) + {{ this.value = value; - } + }} static - { - for (Kind kind : Kind.values()) - { - kindMap.put(kind.getValue(), kind); - } - } - - public static Kind fromInt(int value) throws CVC5ApiException - { - if (value < INTERNAL_KIND.value || value > LAST_KIND.value) - { - throw new CVC5ApiException("Kind value " + value + " is outside the valid range [" - + INTERNAL_KIND.value + "," + LAST_KIND.value + "]"); - } - return kindMap.get(value); - } + {{ + boolean firstValue = true; + for ({name} enumerator : {name}.values()) + {{ + int value = enumerator.getValue(); + if (firstValue) + {{ + minValue = value; + maxValue = value; + firstValue = false; + }} + minValue = Math.min(minValue, value); + maxValue = Math.max(maxValue, value); + enumMap.put(value, enumerator); + }} + }} + + public static {name} fromInt(int value) throws CVC5ApiException + {{ + if (value < minValue || value > maxValue) + {{ + throw new CVC5ApiException("{name} value " + value + " is outside the valid range [" + + minValue + "," + maxValue + "]"); + }} + return enumMap.get(value); + }} public int getValue() - { + {{ return value; - } -} + }} +}} """ # mapping from c++ patterns to java @@ -129,7 +142,7 @@ def gen_java(parser: EnumParser, path): comment = format_comment(comment) code += "{comment}\n {name}({enum_value}),\n".format( comment=comment, name=name, enum_value=value) - code += ENUM_JAVA_BOTTOM + code += ENUM_JAVA_BOTTOM.format(name=enum.name) f.write(code) diff --git a/src/api/java/io/github/cvc5/api/Datatype.java b/src/api/java/io/github/cvc5/api/Datatype.java index f2e260eae56..f4b73e1f4fc 100644 --- a/src/api/java/io/github/cvc5/api/Datatype.java +++ b/src/api/java/io/github/cvc5/api/Datatype.java @@ -111,6 +111,8 @@ public int getNumConstructors() private native int getNumConstructors(long pointer); /** + * @apiNote This method is experimental and may change in future versions. + * * @return the parameters of this datatype, if it is parametric. An exception * is thrown if this datatype is not parametric. */ @@ -122,7 +124,11 @@ public Sort[] getParameters() { private native long[] getParameters(long pointer); - /** @return true if this datatype is parametric */ + /** + * @apiNote This method is experimental and may change in future versions. + * + * @return true if this datatype is parametric + */ public boolean isParametric() { return isParametric(pointer); @@ -146,7 +152,11 @@ public boolean isTuple() private native boolean isTuple(long pointer); - /** @return true if this datatype corresponds to a record */ + /** + * @apiNote This method is experimental and may change in future versions. + * + * @return true if this datatype corresponds to a record + */ public boolean isRecord() { return isRecord(pointer); diff --git a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java index f824ac121f2..da30b3d4a17 100644 --- a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java +++ b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java @@ -75,6 +75,8 @@ public Term getConstructorTerm() * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above * (nullary) application of nil. * + * @apiNote This method is experimental and may change in future versions. + * * @param retSort the desired return sort of the constructor * @return the constructor term */ diff --git a/src/api/java/io/github/cvc5/api/RoundingMode.java b/src/api/java/io/github/cvc5/api/RoundingMode.java deleted file mode 100644 index 6a3c274a14b..00000000000 --- a/src/api/java/io/github/cvc5/api/RoundingMode.java +++ /dev/null @@ -1,63 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package io.github.cvc5.api; - -public enum RoundingMode { - /** - * Round to the nearest even number. - * If the two nearest floating-point numbers bracketing an unrepresentable - * infinitely precise result are equally near, the one with an even least - * significant digit will be delivered. - */ - ROUND_NEAREST_TIES_TO_EVEN(0), - /** - * Round towards positive infinity (+oo). - * The result shall be the format's floating-point number (possibly +oo) - * closest to and no less than the infinitely precise result. - */ - ROUND_TOWARD_POSITIVE(1), - /** - * Round towards negative infinity (-oo). - * The result shall be the format's floating-point number (possibly -oo) - * closest to and no less than the infinitely precise result. - */ - ROUND_TOWARD_NEGATIVE(2), - /** - * Round towards zero. - * The result shall be the format's floating-point number closest to and no - * greater in magnitude than the infinitely precise result. - */ - ROUND_TOWARD_ZERO(3), - /** - * Round to the nearest number away from zero. - * If the two nearest floating-point numbers bracketing an unrepresentable - * infinitely precise result are equally near, the one with larger magnitude - * will be selected. - */ - ROUND_NEAREST_TIES_TO_AWAY(4); - - private int value; - - private RoundingMode(int value) - { - this.value = value; - } - - public int getValue() - { - return value; - } -} diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 5b462bc2f18..4b4c2ccc8b4 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -339,6 +339,9 @@ public Sort mkFunctionSort(Sort[] sorts, Sort codomain) /** * Create a sort parameter. + * + * @apiNote This method is experimental and may change in future versions. + * * @param symbol the name of the sort * @return the sort parameter */ @@ -365,6 +368,9 @@ public Sort mkPredicateSort(Sort[] sorts) /** * Create a record sort + * + * @apiNote This method is experimental and may change in future versions. + * * @param fields the list of fields of the record * @return the record sort */ @@ -689,8 +695,10 @@ public Term mkTuple(Sort[] sorts, Term[] terms) * Create an operator for a builtin Kind * The Kind may not be the Kind for an indexed operator * (e.g. BITVECTOR_EXTRACT). + * * @apiNote In this case, the Op simply wraps the Kind. The Kind can be used * in mkTerm directly without creating an op first. + * * @param kind the kind to wrap */ public Op mkOp(Kind kind) @@ -965,6 +973,9 @@ public Term mkEmptyBag(Sort sort) /** * Create a separation logic empty term. + * + * @apiNote This method is experimental and may change in future versions. + * * @return the separation logic empty term */ public Term mkSepEmp() @@ -977,6 +988,9 @@ public Term mkSepEmp() /** * Create a separation logic nil term. + * + * @apiNote This method is experimental and may change in future versions. + * * @param sort the sort of the nil term * @return the separation logic nil term */ @@ -1238,6 +1252,9 @@ public Term mkFloatingPoint(int exp, int sig, Term val) throws CVC5ApiException /** * Create a cardinality constraint for an uninterpreted sort. + * + * @apiNote This method is experimental and may change in future versions. + * * @param sort the sort the cardinality constraint is for * @param upperBound the upper bound on the cardinality of the sort * @return the cardinality constraint @@ -1321,6 +1338,11 @@ public Term mkVar(Sort sort, String symbol) /* Create datatype constructor declarations */ /* .................................................................... */ + /** + * Create a datatype constructor declaration. + * @param name the name of the datatype constructor + * @return the DatatypeConstructorDecl + */ public DatatypeConstructorDecl mkDatatypeConstructorDecl(String name) { long declPointer = mkDatatypeConstructorDecl(pointer, name); @@ -1437,6 +1459,9 @@ private native long mkDatatypeDecl( * the SAT Engine in the simplification, but uses the current * definitions, assertions, and the current partial model, if one * has been constructed. It also involves theory normalization. + * + * @apiNote This method is experimental and may change in future versions. + * * @param t the formula to simplify * @return the simplified formula */ @@ -1559,8 +1584,10 @@ private native long declareFun( * {@code * ( declare-sort ) * } + * * @apiNote This corresponds to mkUninterpretedSort() const if arity = 0, and * to mkUninterpretedSortConstructorSort() const if arity > 0. + * * @param symbol the name of the sort * @param arity the arity of the sort * @return the sort @@ -1752,23 +1779,15 @@ private native void defineFunsRec(long pointer, long[] termPointers, boolean global); - /** - * Echo a given string to the given output stream. - * SMT-LIB: - * {@code - * ( echo ) - * } - * @param out the output stream - * @param str the string to echo - */ - // TODO: void echo(std::ostream& out, String str) - /** * Get a list of literals that are entailed by the current set of assertions * SMT-LIB: * {@code * ( get-learned-literals ) * } + * + * @apiNote This method is experimental and may change in future versions. + * * @return the list of learned literals */ public Term[] getLearnedLiterals() { @@ -1871,11 +1890,13 @@ public Term[] getUnsatAssumptions() * (get-unsat-core) * } * Requires to enable option 'produce-unsat-cores'. + * * @apiNote In contrast to SMT-LIB, the API does not distinguish between * named and unnamed assertions when producing an unsatisfiable * core. Additionally, the API allows this option to be called after * a check with assumptions. A subset of those assumptions may be * included in the unsatisfiable core returned by this method. + * * @return a set of terms representing the unsatisfiable core */ public Term[] getUnsatCore() @@ -1890,6 +1911,8 @@ public Term[] getUnsatCore() * Get a difficulty estimate for an asserted formula. This method is * intended to be called immediately after any response to a checkSat. * + * @apiNote This method is experimental and may change in future versions. + * * @return a map from (a subset of) the input assertions to a real value that * is an estimate of how difficult each assertion was to solve. Unmentioned * assertions can be assumed to have zero difficulty. @@ -1916,6 +1939,9 @@ public Map getDifficulty() * ( get-proof ) * } * Requires to enable option 'produce-proofs'. + * + * @apiNote This method is experimental and may change in future versions. + * * @return a string representing the proof, according to the value of * proof-format-mode. */ @@ -1983,6 +2009,8 @@ public Term[] getModelDomainElements(Sort s) * current model. This method will only return false (for any v) if * the model-cores option has been set. * + * @apiNote This method is experimental and may change in future versions. + * * @param v The term in question * @return true if v is a model core symbol */ @@ -2000,6 +2028,9 @@ public boolean isModelCoreSymbol(Term v) * ( get-model ) * } * Requires to enable option 'produce-models'. + * + * @apiNote This method is experimental and may change in future versions. + * * @param sorts The list of uninterpreted sorts that should be printed in the * model. * @param vars The list of free constants that should be printed in the @@ -2021,8 +2052,11 @@ public String getModel(Sort[] sorts, Term[] vars) * {@code * ( get-qe ) * } - * Requires a logic that supports quantifier elimination. Currently, the only - * logics supported by quantifier elimination is LRA and LIA. + * Quantifier Elimination is is only complete for logics such as LRA, + * LIA and BV. + * + * @apiNote This method is experimental and may change in future versions. + * * @param q a quantified formula of the form: * Q x1...xn. P( x1...xn, y1...yn ) * where P( x1...xn, y1...yn ) is a quantifier-free formula @@ -2047,8 +2081,11 @@ public Term getQuantifierElimination(Term q) * {@code * ( get-qe-disjunct ) * } - * Requires a logic that supports quantifier elimination. Currently, the only - * logics supported by quantifier elimination is LRA and LIA. + * Quantifier Elimination is is only complete for logics such as LRA, + * LIA and BV. + * + * @apiNote This method is experimental and may change in future versions. + * * @param q a quantified formula of the form: * Q x1...xn. P( x1...xn, y1...yn ) * where P( x1...xn, y1...yn ) is a quantifier-free formula @@ -2079,6 +2116,9 @@ public Term getQuantifierEliminationDisjunct(Term q) * When using separation logic, this sets the location sort and the * datatype sort to the given ones. This method should be invoked exactly * once, before any separation logic constraints are provided. + * + * @apiNote This method is experimental and may change in future versions. + * * @param locSort The location sort of the heap * @param dataSort The data sort of the heap */ @@ -2091,6 +2131,9 @@ public void declareSepHeap(Sort locSort, Sort dataSort) /** * When using separation logic, obtain the term for the heap. + * + * @apiNote This method is experimental and may change in future versions. + * * @return The term for the heap */ public Term getValueSepHeap() @@ -2103,6 +2146,9 @@ public Term getValueSepHeap() /** * When using separation logic, obtain the term for nil. + * + * @apiNote This method is experimental and may change in future versions. + * * @return The term for nil */ public Term getValueSepNil() @@ -2119,6 +2165,9 @@ public Term getValueSepNil() * {@code * ( declare-pool ( * ) ) * } + * + * @apiNote This method is experimental and may change in future versions. + * * @param symbol The name of the pool * @param sort The sort of the elements of the pool. * @param initValue The initial value of the pool @@ -2167,9 +2216,12 @@ public void pop(int nscopes) throws CVC5ApiException * Get an interpolant * SMT-LIB: * {@code - * ( get-interpol ) + * ( get-interpolant ) * } - * Requires 'produce-interpols' to be set to a mode different from 'none'. + * Requires 'produce-interpolants' to be set to a mode different from 'none'. + * + * @apiNote This method is experimental and may change in future versions. + * * @param conj the conjecture term * @return a Term I such that {@code A->I} and {@code I->B} are valid, where * A is the current set of assertions and B is given in the input by @@ -2187,9 +2239,12 @@ public Term getInterpolant(Term conj) * Get an interpolant * SMT-LIB: * {@code - * ( get-interpol ) + * ( get-interpolant ) * } - * Requires 'produce-interpols' to be set to a mode different from 'none'. + * Requires 'produce-interpolants' to be set to a mode different from 'none'. + * + * @apiNote This method is experimental and may change in future versions. + * * @param conj the conjecture term * @param grammar the grammar for the interpolant I * @return a Term I such that {@code A->I} and {@code I->B} are valid, where @@ -2206,7 +2261,7 @@ public Term getInterpolant(Term conj, Grammar grammar) /** * Get the next interpolant. Can only be called immediately after a successful - * call to get-interpol or get-interpol-next. Is guaranteed to produce a + * call to get-interpolant or get-interpolant-next. Is guaranteed to produce a * syntactically different interpolant wrt the last returned interpolant if * successful. * @@ -2215,12 +2270,14 @@ public Term getInterpolant(Term conj, Grammar grammar) * \verbatim embed:rst:leading-asterisk * .. code:: smtlib * - * (get-interpol-next) + * (get-interpolant-next) * - * Requires to enable incremental mode, and option 'produce-interpols' to be + * Requires to enable incremental mode, and option 'produce-interpolants' to be * set to a mode different from 'none'. * \endverbatim * + * @apiNote This method is experimental and may change in future versions. + * * @return a Term I such that {@code A->I} and {@code I->B} are valid, * where A is the current set of assertions and B is given in the input * by conj on the last call to getInterpolant, or the null term if such @@ -2241,6 +2298,9 @@ public Term getInterpolantNext() * ( get-abduct ) * } * Requires enabling option 'produce-abducts' + * + * @apiNote This method is experimental and may change in future versions. + * * @param conj the conjecture term * @return a term C such that A^C is satisfiable, and A^~B^C is * unsatisfiable, where A is the current set of assertions and B is @@ -2261,6 +2321,9 @@ public Term getAbduct(Term conj) * ( get-abduct ) * } * Requires enabling option 'produce-abducts' + * + * @apiNote This method is experimental and may change in future versions. + * * @param conj the conjecture term * @param grammar the grammar for the abduct C * @return a term C such that A^C is satisfiable, and A^~B^C is @@ -2285,6 +2348,9 @@ public Term getAbduct(Term conj, Grammar grammar) * ( get-abduct-next ) * } * Requires enabling incremental mode and option 'produce-abducts' + * + * @apiNote This method is experimental and may change in future versions. + * * @return a term C such that A^C is satisfiable, and A^~B^C is * unsatisfiable, where A is the current set of assertions and B is * given in the input by conj in the last call to getAbduct, or the @@ -2307,6 +2373,8 @@ public Term getAbductNext() * } * Requires enabling 'produce-models' option and setting 'block-models' option * to a mode other than "none". + * + * @apiNote This method is experimental and may change in future versions. */ public void blockModel() { @@ -2323,6 +2391,8 @@ public void blockModel() * ( block-model-values ( + ) ) * } * Requires enabling 'produce-models' option. + * + * @apiNote This method is experimental and may change in future versions. */ public void blockModelValues(Term[] terms) { @@ -2335,6 +2405,8 @@ public void blockModelValues(Term[] terms) /** * Return a string that contains information about all instantiations made by * the quantifiers module. + * + * @apiNote This method is experimental and may change in future versions. */ public String getInstantiations() { @@ -2436,23 +2508,6 @@ public void setOption(String option, String value) private native void setOption(long pointer, String option, String value); - /** - * If needed, convert this term to a given sort. - * - * @apiNote The sort of the term must be convertible into the target sort. - * Currently only Int to Real conversions are supported. - * @param t the term - * @param s the target sort - * @return the term wrapped into a sort conversion if needed - */ - public Term ensureTermSort(Term t, Sort s) - { - long termPointer = ensureTermSort(pointer, t.getPointer(), s.getPointer()); - return new Term(this, termPointer); - } - - private native long ensureTermSort(long pointer, long termPointer, long sortPointer); - /** * Append \p symbol to the current list of universal variables. * @param sort the sort of the universal variable diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index bf85107f661..fac9c4679c2 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -280,6 +280,9 @@ public boolean isTuple() /** * Is this a record sort? + * + * @apiNote This method is experimental and may change in future versions. + * * @return true if the sort is a record sort */ public boolean isRecord() @@ -359,6 +362,23 @@ public boolean isUninterpretedSortConstructor() private native boolean isUninterpretedSortConstructor(long pointer); + /** + * Is this an instantiated (parametric datatype or uninterpreted sort + * constructor) sort? + * + * An instantiated sort is a sort that has been constructed from + * instantiating a sort with sort arguments + * (see Sort.instantiate()). + * + * @return true if this is an instantiated sort + */ + public boolean isInstantiated() + { + return isInstantiated(pointer); + } + + private native boolean isInstantiated(long pointer); + /** * @return the underlying datatype of a datatype sort */ @@ -373,7 +393,11 @@ public Datatype getDatatype() /** * Instantiate a parameterized datatype sort or uninterpreted sort * constructor sort. + * * Create sorts parameter with Solver.mkParamSort(). + * + * @apiNote This method is experimental and may change in future versions. + * * @param params the list of sort parameters to instantiate with */ public Sort instantiate(List params) @@ -382,8 +406,13 @@ public Sort instantiate(List params) } /** - * Instantiate a parameterized datatype/sort sort. + * Instantiate a parameterized datatype sort or uninterpreted sort + * constructor sort. + * * Create sorts parameter with Solver.mkParamSort(). + * + * @apiNote This method is experimental and may change in future versions. + * * @param params the list of sort parameters to instantiate with */ public Sort instantiate(Sort[] params) @@ -397,11 +426,14 @@ public Sort instantiate(Sort[] params) /** * Substitution of Sorts. - * @param sort the subsort to be substituted within this sort. - * @param replacement the sort replacing the substituted subsort. * * Note that this replacement is applied during a pre-order traversal and * only once to the sort. It is not run until fix point. + * + * @apiNote This method is experimental and may change in future versions. + * + * @param sort the subsort to be substituted within this sort. + * @param replacement the sort replacing the substituted subsort. */ public Sort substitute(Sort sort, Sort replacement) { @@ -413,8 +445,6 @@ public Sort substitute(Sort sort, Sort replacement) /** * Simultaneous substitution of Sorts. - * @param sorts the subsorts to be substituted within this sort. - * @param replacements the sort replacing the substituted subsorts. * * Note that this replacement is applied during a pre-order traversal and * only once to the sort. It is not run until fix point. In the case that @@ -424,6 +454,11 @@ public Sort substitute(Sort sort, Sort replacement) * For example, * (Array A B).substitute({A, C}, {(Array C D), (Array A B)}) will * return (Array (Array C D) B). + * + * @apiNote This method is experimental and may change in future versions. + * + * @param sorts the subsorts to be substituted within this sort. + * @param replacements the sort replacing the substituted subsorts. */ public Sort substitute(Sort[] sorts, Sort[] replacements) { @@ -628,16 +663,6 @@ public Sort getSequenceElementSort() /* Uninterpreted sort -------------------------------------------------- */ - /** - * @return true if an uninterpreted sort is parameterezied - */ - public boolean isUninterpretedSortParameterized() - { - return isUninterpretedSortParameterized(pointer); - } - - private native boolean isUninterpretedSortParameterized(long pointer); - /** * @return the parameter sorts of an uninterpreted sort */ diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java index 7fddc49be15..02fb42cf4f4 100644 --- a/src/api/java/io/github/cvc5/api/Term.java +++ b/src/api/java/io/github/cvc5/api/Term.java @@ -522,6 +522,28 @@ public String getUninterpretedSortValue() private native String getUninterpretedSortValue(long pointer); + /** + * @return true if the term is a floating-point rounding mode value. + */ + public boolean isRoundingModeValue() + { + return isRoundingModeValue(pointer); + } + + private native boolean isRoundingModeValue(long pointer); + + /** + * Asserts isRoundingModeValue(). + * @return the floating-point rounding mode value held by the term. + */ + public RoundingMode getRoundingModeValue() throws CVC5ApiException + { + int value = getRoundingModeValue(pointer); + return RoundingMode.fromInt(value); + } + + private native int getRoundingModeValue(long pointer); + /** * @return true if the term is a tuple value. */ @@ -660,6 +682,29 @@ public Term[] getSequenceValue() private native long[] getSequenceValue(long pointer); + /** + * @return true if the term is a cardinality constraint + */ + public boolean isCardinalityConstraint() + { + return isCardinalityConstraint(pointer); + } + + private native boolean isCardinalityConstraint(long pointer); + + /** + * Asserts isCardinalityConstraint(). + * @return the sort the cardinality constraint is for and its upper bound. + */ + public Pair getCardinalityConstraint() + { + Pair pair = getCardinalityConstraint(pointer); + Sort sort = new Sort(solver, pair.first); + return new Pair(sort, pair.second); + } + + private native Pair getCardinalityConstraint(long pointer); + public class ConstIterator implements Iterator { private int currentIndex; diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 7eccbf2606f..bb7d816fe5e 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -2385,23 +2385,6 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_setOption( CVC5_JAVA_API_TRY_CATCH_END(env); } -/* - * Class: io_github_cvc5_api_Solver - * Method: ensureTermSort - * Signature: (JJJ)J - */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_ensureTermSort( - JNIEnv* env, jobject, jlong pointer, jlong termPointer, jlong sortPointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Solver* solver = reinterpret_cast(pointer); - Term* term = reinterpret_cast(termPointer); - Sort* sort = reinterpret_cast(sortPointer); - Term* retPointer = new Term(solver->ensureTermSort(*term, *sort)); - return reinterpret_cast(retPointer); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} - /* * Class: io_github_cvc5_api_Solver * Method: declareSygusVar diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp index a3d1f135f7b..4d5b6986c72 100644 --- a/src/api/java/jni/sort.cpp +++ b/src/api/java/jni/sort.cpp @@ -454,6 +454,20 @@ Java_io_github_cvc5_api_Sort_isUninterpretedSortConstructor(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } +/* + * Class: io_github_cvc5_api_Sort + * Method: isInstantiated + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isInstantiated(JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Sort* current = reinterpret_cast(pointer); + return static_cast(current->isInstantiated()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + /* * Class: io_github_cvc5_api_Sort * Method: getDatatype @@ -826,22 +840,6 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getSequenceElementSort( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } -/* - * Class: io_github_cvc5_api_Sort - * Method: isUninterpretedSortParameterized - * Signature: (J)Z - */ -JNIEXPORT jboolean JNICALL -Java_io_github_cvc5_api_Sort_isUninterpretedSortParameterized(JNIEnv* env, - jobject, - jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Sort* current = reinterpret_cast(pointer); - return static_cast(current->isUninterpretedSortParameterized()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); -} - /* * Class: io_github_cvc5_api_Sort * Method: getUninterpretedSortParamSorts diff --git a/src/api/java/jni/term.cpp b/src/api/java/jni/term.cpp index c45bb4d6a4f..e5bb02b2289 100644 --- a/src/api/java/jni/term.cpp +++ b/src/api/java/jni/term.cpp @@ -663,6 +663,34 @@ Java_io_github_cvc5_api_Term_getUninterpretedSortValue(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } +/* + * Class: io_github_cvc5_api_Term + * Method: isRoundingModeValue + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isRoundingModeValue( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isRoundingModeValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: io_github_cvc5_api_Term + * Method: getRoundingModeValue + * Signature: (J)I + */ +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Term_getRoundingModeValue( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->getRoundingModeValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_api_Term * Method: isTupleValue @@ -877,6 +905,49 @@ JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Term_getSequenceValue( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } +/* + * Class: io_github_cvc5_api_Term + * Method: isCardinalityConstraint + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isCardinalityConstraint( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isCardinalityConstraint()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: io_github_cvc5_api_Term + * Method: getCardinalityConstraint + * Signature: (J)Lio/github/cvc5/api/Pair; + */ +JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Term_getCardinalityConstraint( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + auto [sort, upperBound] = current->getCardinalityConstraint(); + Sort* sortPointer = new Sort(sort); + jobject u = getBigIntegerObject(env, upperBound); + + // Long s = new Long(sortPointer); + jclass longClass = env->FindClass("Ljava/lang/Long;"); + jmethodID longConstructor = env->GetMethodID(longClass, "", "(J)V"); + jobject s = env->NewObject(longClass, longConstructor, sortPointer); + + // Pair pair = new Pair(s, u); + jclass pairClass = env->FindClass("Lio/github/cvc5/api/Pair;"); + jmethodID pairConstructor = env->GetMethodID( + pairClass, "", "(Ljava/lang/Object;Ljava/lang/Object;)V"); + jobject pair = env->NewObject(pairClass, pairConstructor, s, u); + + return pair; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + /* * Class: io_github_cvc5_api_Term * Method: iterator diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index b5cbdf7cc5e..ce5dd100c80 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -8,6 +8,7 @@ from libcpp.string cimport string from libcpp.vector cimport vector from libcpp.pair cimport pair from cvc5kinds cimport Kind +from cvc5types cimport RoundingMode cdef extern from "" namespace "std": @@ -201,9 +202,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isUnknown() except + string toString() except + - cdef cppclass RoundingMode: - pass - cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::Result": cdef cppclass UnknownExplanation: pass @@ -399,6 +397,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isSequence() except + bint isUninterpretedSort() except + bint isUninterpretedSortConstructor() except + + bint isInstantiated() except + Datatype getDatatype() except + Sort instantiate(const vector[Sort]& params) except + Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except + @@ -417,7 +416,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort getSetElementSort() except + Sort getBagElementSort() except + Sort getSequenceElementSort() except + - bint isUninterpretedSortParameterized() except + vector[Sort] getUninterpretedSortParamSorts() except + size_t getUninterpretedSortConstructorArity() except + uint32_t getBitVectorSize() except + @@ -507,6 +505,11 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": string getBitVectorValue(uint32_t base) except + bint isUninterpretedSortValue() except + string getUninterpretedSortValue() except + + bint isTupleValue() except + + vector[Term] getTupleValue() except + + bint isRoundingModeValue() except + + RoundingMode getRoundingModeValue() except + + bint isFloatingPointPosZero() except + bint isFloatingPointNegZero() except + bint isFloatingPointPosInf() except + @@ -519,8 +522,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": set[Term] getSetValue() except + bint isSequenceValue() except + vector[Term] getSequenceValue() except + - bint isTupleValue() except + - vector[Term] getTupleValue() except + cdef cppclass TermHashFunction: @@ -528,14 +529,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": size_t operator()(const Term & t) except + -cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::RoundingMode": - cdef RoundingMode ROUND_NEAREST_TIES_TO_EVEN, - cdef RoundingMode ROUND_TOWARD_POSITIVE, - cdef RoundingMode ROUND_TOWARD_NEGATIVE, - cdef RoundingMode ROUND_TOWARD_ZERO, - cdef RoundingMode ROUND_NEAREST_TIES_TO_AWAY - - cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::Result::UnknownExplanation": cdef UnknownExplanation REQUIRES_FULL_CHECK cdef UnknownExplanation INCOMPLETE diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 09749b3d532..a378434ab3d 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -22,7 +22,6 @@ from cvc5 cimport DatatypeDecl as c_DatatypeDecl from cvc5 cimport DatatypeSelector as c_DatatypeSelector from cvc5 cimport Result as c_Result from cvc5 cimport SynthResult as c_SynthResult -from cvc5 cimport RoundingMode as c_RoundingMode from cvc5 cimport UnknownExplanation as c_UnknownExplanation from cvc5 cimport Op as c_Op from cvc5 cimport OptionInfo as c_OptionInfo @@ -33,9 +32,6 @@ from cvc5 cimport Statistics as c_Statistics from cvc5 cimport Stat as c_Stat from cvc5 cimport Grammar as c_Grammar from cvc5 cimport Sort as c_Sort -from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE -from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO -from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON @@ -46,6 +42,7 @@ from cvc5 cimport wstring as c_wstring from cvc5 cimport tuple as c_tuple from cvc5 cimport get0, get1, get2 from cvc5kinds cimport Kind as c_Kind +from cvc5types cimport RoundingMode as c_RoundingMode cdef extern from "Python.h": wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *) @@ -174,7 +171,11 @@ cdef class Datatype: return param_sorts def isParametric(self): - """:return: True if this datatype is parametric.""" + """ + .. warning:: This method is experimental and may change in future + versions. + :return: True if this datatype is parametric. + """ return self.cd.isParametric() def isCodatatype(self): @@ -186,7 +187,11 @@ cdef class Datatype: return self.cd.isTuple() def isRecord(self): - """:return: True if this datatype corresponds to a record.""" + """ + .. warning:: This method is experimental and may change in future + versions. + :return: True if this datatype corresponds to a record. + """ return self.cd.isRecord() def isFinite(self): @@ -255,6 +260,9 @@ cdef class DatatypeConstructor: :cpp:func:`DatatypeConstructor::getInstantiatedConstructorTerm() `). + .. warning:: This method is experimental and may change in future + versions. + :param retSort: the desired return sort of the constructor :return: the constructor operator as a term. """ @@ -661,44 +669,6 @@ cdef class SynthResult: def __repr__(self): return self.cr.toString().decode() -cdef class RoundingMode: - """ - Rounding modes for floating-point numbers. - - For many floating-point operations, infinitely precise results may not be - representable with the number of available bits. Thus, the results are - rounded in a certain way to one of the representable floating-point numbers. - - These rounding modes directly follow the SMT-LIB theory for floating-point - arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`. - The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE - Standard 754. - - Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`. - """ - cdef c_RoundingMode crm - cdef str name - def __cinit__(self, int rm): - # crm always assigned externally - self.crm = rm - self.name = __rounding_modes[rm] - - def __eq__(self, RoundingMode other): - return ( self.crm) == ( other.crm) - - def __ne__(self, RoundingMode other): - return not self.__eq__(other) - - def __hash__(self): - return hash(( self.crm, self.name)) - - def __str__(self): - return self.name - - def __repr__(self): - return self.name - - cdef class UnknownExplanation: """ Wrapper class for :cpp:enum:`cvc5::api::Result::UnknownExplanation`. @@ -894,6 +864,9 @@ cdef class Solver: def mkParamSort(self, symbolname): """ Create a sort parameter. + .. warning:: This method is experimental and may change in future + versions. + :param symbol: the name of the sort :return: the sort parameter """ @@ -919,6 +892,9 @@ cdef class Solver: def mkRecordSort(self, *fields): """Create a record sort + .. warning:: This method is experimental and may change in future + versions. + :param fields: the list of fields of the record, as a list or as distinct arguments :return: the record sort """ @@ -1218,6 +1194,9 @@ cdef class Solver: def mkSepEmp(self): """Create a separation logic empty term. + .. warning:: This method is experimental and may change in future + versions. + :return: the separation logic empty term """ cdef Term term = Term(self) @@ -1227,6 +1206,9 @@ cdef class Solver: def mkSepNil(self, Sort sort): """Create a separation logic nil term. + .. warning:: This method is experimental and may change in future + versions. + :param sort: the sort of the nil term :return: the separation logic nil term """ @@ -1392,13 +1374,13 @@ cdef class Solver: term.cterm = self.csolver.mkFloatingPointNegZero(exp, sig) return term - def mkRoundingMode(self, RoundingMode rm): + def mkRoundingMode(self, rm): """Create a roundingmode constant. :param rm: the floating point rounding mode this constant represents """ cdef Term term = Term(self) - term.cterm = self.csolver.mkRoundingMode( rm.crm) + term.cterm = self.csolver.mkRoundingMode( rm.value) return term def mkFloatingPoint(self, int exp, int sig, Term val): @@ -1415,6 +1397,9 @@ cdef class Solver: def mkCardinalityConstraint(self, Sort sort, int index): """Create cardinality constraint. + .. warning:: This method is experimental and may change in future + versions. + :param sort: Sort of the constraint :param index: The upper bound for the cardinality of the sort """ @@ -1464,8 +1449,8 @@ cdef class Solver: def mkDatatypeConstructorDecl(self, str name): """ - :return: a datatype constructor declaration :param name: the constructor's name + :return: the DatatypeConstructorDecl """ cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self) ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode()) @@ -1528,6 +1513,9 @@ cdef class Solver: assertions, and the current partial model, if one has been constructed. It also involves theory normalization. + .. warning:: This method is experimental and may change in future + versions. + :param t: the formula to simplify :return: the simplified formula """ @@ -1963,6 +1951,9 @@ cdef class Solver: Requires to enable option :ref:`produce-proofs `. + .. warning:: This method is experimental and may change in future + versions. + :return: a string representing the proof, according to the value of proof-format-mode. """ @@ -1977,6 +1968,9 @@ cdef class Solver: ( get-learned-literals ) + .. warning:: This method is experimental and may change in future + versions. + :return: the list of literals """ lits = [] @@ -2198,6 +2192,9 @@ cdef class Solver: using the current model. This method will only return false (for any v) if the model-cores option has been set. + .. warning:: This method is experimental and may change in future + versions. + :param v: The term in question :return: true if v is a model core symbol """ @@ -2214,6 +2211,9 @@ cdef class Solver: Requires to enable option :ref:`produce-models `. + + .. warning:: This method is experimental and may change in future + versions. :param sorts: The list of uninterpreted sorts that should be printed in the model. @@ -2236,6 +2236,9 @@ cdef class Solver: def getValueSepHeap(self): """When using separation logic, obtain the term for the heap. + .. warning:: This method is experimental and may change in future + versions. + :return: The term for the heap """ cdef Term term = Term(self) @@ -2245,6 +2248,9 @@ cdef class Solver: def getValueSepNil(self): """When using separation logic, obtain the term for nil. + .. warning:: This method is experimental and may change in future + versions. + :return: The term for nil """ cdef Term term = Term(self) @@ -2257,6 +2263,9 @@ cdef class Solver: datatype sort to the given ones. This method should be invoked exactly once, before any separation logic constraints are provided. + .. warning:: This method is experimental and may change in future + versions. + :param locSort: The location sort of the heap :param dataSort: The data sort of the heap """ @@ -2271,6 +2280,9 @@ cdef class Solver: ( declare-pool ( * ) ) + .. warning:: This method is experimental and may change in future + versions. + :param symbol: The name of the pool :param sort: The sort of the elements of the pool. :param initValue: The initial value of the pool @@ -2370,15 +2382,18 @@ cdef class Solver: .. code-block:: smtlib - ( get-interpol ) - ( get-interpol ) + ( get-interpolant ) + ( get-interpolant ) - Requires option :ref:`produce-interpols ` to be set to a mode different from `none`. + Requires option :ref:`produce-interpolants ` to be set to a mode different from `none`. Supports the following variants: - ``Term getInteprolant(Term conj)`` - ``Term getInteprolant(Term conj, Grammar grammar)`` + + .. warning:: This method is experimental and may change in future + versions. :param conj: the conjecture term :param output: the term where the result will be stored @@ -2398,7 +2413,7 @@ cdef class Solver: def getInterpolantNext(self): """ Get the next interpolant. Can only be called immediately after - a succesful call to get-interpol or get-interpol-next. + a succesful call to get-interpolant or get-interpolant-next. Is guaranteed to produce a syntactically different interpolant wrt the last returned interpolant if successful. @@ -2406,10 +2421,13 @@ cdef class Solver: .. code-block:: smtlib - ( get-interpol-next ) + ( get-interpolant-next ) Requires to enable incremental mode, and - option :ref:`produce-interpols ` to be set to a mode different from `none`. + option :ref:`produce-interpolants ` to be set to a mode different from `none`. + + .. warning:: This method is experimental and may change in future + versions. :param output: the term where the result will be stored :return: True iff an interpolant was found @@ -2434,6 +2452,9 @@ cdef class Solver: - ``Term getAbduct(Term conj)`` - ``Term getAbduct(Term conj, Grammar grammar)`` + + .. warning:: This method is experimental and may change in future + versions. :param conj: the conjecture term :param output: the term where the result will be stored @@ -2464,6 +2485,10 @@ cdef class Solver: Requires to enable incremental mode, and option :ref:`produce-abducts `. + + .. warning:: This method is experimental and may change in future + versions. + :param output: the term where the result will be stored :return: True iff an abduct was found """ @@ -2487,6 +2512,9 @@ cdef class Solver: and setting option :ref:`block-models ` to a mode other than ``none``. + + .. warning:: This method is experimental and may change in future + versions. """ self.csolver.blockModel() @@ -2503,6 +2531,9 @@ cdef class Solver: Requires enabling option :ref:`produce-models `. + + .. warning:: This method is experimental and may change in future + versions. """ cdef vector[c_Term] nts for t in terms: @@ -2513,6 +2544,9 @@ cdef class Solver: """ Return a string that contains information about all instantiations made by the quantifiers module. + + .. warning:: This method is experimental and may change in future + versions. """ return self.csolver.getInstantiations() @@ -2714,6 +2748,9 @@ cdef class Sort: """ Is this a record sort? + .. warning:: This method is experimental and may change in future + versions. + :return: True if the sort is a record sort. """ return self.csort.isRecord() @@ -2769,6 +2806,19 @@ cdef class Sort: """ return self.csort.isUninterpretedSortConstructor() + def isInstantiated(self): + """ + Is this an instantiated (parametric datatype or uninterpreted sort + constructor) sort? + + An instantiated sort is a sort that has been constructed from + instantiating a sort parameters with sort arguments + (see Sort::instantiate()). + + :return: True if this is an instantiated sort. + """ + return self.csort.isInstantiated() + def getDatatype(self): """ :return: the underlying datatype of a datatype sort @@ -2783,6 +2833,9 @@ cdef class Sort: constructor sort. Create sorts parameter with :py:meth:`Solver.mkParamSort()` + .. warning:: This method is experimental and may change in future + versions. + :param params: the list of sort parameters to instantiate with """ cdef Sort sort = Sort(self.solver) @@ -2796,9 +2849,6 @@ cdef class Sort: """ Substitution of Sorts. - :param sort_or_list_1: the subsort or subsorts to be substituted within this sort. - :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort. - Note that this replacement is applied during a pre-order traversal and only once to the sort. It is not run until fix point. In the case that sort_or_list_1 contains duplicates, the replacement earliest in the list @@ -2807,6 +2857,12 @@ cdef class Sort: For example, ``(Array A B) .substitute([A, C], [(Array C D), (Array A B)])`` will return ``(Array (Array C D) B)``. + + .. warning:: This method is experimental and may change in future + versions. + + :param sort_or_list_1: the subsort or subsorts to be substituted within this sort. + :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort. """ # The resulting sort after substitution @@ -2961,12 +3017,6 @@ cdef class Sort: sort.csort = self.csort.getSequenceElementSort() return sort - def isUninterpretedSortParameterized(self): - """ - :return: True if an uninterpreted sort is parameterized - """ - return self.csort.isUninterpretedSortParameterized() - def getUninterpretedSortParamSorts(self): """ :return: the parameter sorts of an uninterpreted sort @@ -3481,6 +3531,17 @@ cdef class Term: """:return: True iff this term is a tuple value.""" return self.cterm.isTupleValue() + def isRoundingModeValue(self): + """:return: True if the term is a floating-point rounding mode value.""" + return self.cterm.isRoundingModeValue() + + def getRoundingModeValue(self): + """ + Asserts isRoundingModeValue(). + :return: the floating-point rounding mode value held by the term. + """ + return RoundingMode( self.cterm.getRoundingModeValue()) + def getTupleValue(self): """ Asserts :py:meth:`isTupleValue()`. @@ -3579,29 +3640,6 @@ cdef class Term: return res -# Generate rounding modes -cdef __rounding_modes = { - ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven", - ROUND_TOWARD_POSITIVE: "RoundTowardPositive", - ROUND_TOWARD_NEGATIVE: "RoundTowardNegative", - ROUND_TOWARD_ZERO: "RoundTowardZero", - ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway" -} - -mod_ref = sys.modules[__name__] -for rm_int, name in __rounding_modes.items(): - r = RoundingMode(rm_int) - - if name in dir(mod_ref): - raise RuntimeError("Redefinition of Python RoundingMode %s."%name) - - setattr(mod_ref, name, r) - -del r -del rm_int -del name - - # Generate unknown explanations cdef __unknown_explanations = { REQUIRES_FULL_CHECK: "RequiresFullCheck", @@ -3616,6 +3654,7 @@ cdef __unknown_explanations = { UNKNOWN_REASON: "UnknownReason" } +mod_ref = sys.modules[__name__] for ue_int, name in __unknown_explanations.items(): u = UnknownExplanation(ue_int) diff --git a/src/api/python/cvc5_python_base.pyx b/src/api/python/cvc5_python_base.pyx index f093002654c..a70433140ab 100644 --- a/src/api/python/cvc5_python_base.pyx +++ b/src/api/python/cvc5_python_base.pyx @@ -1,2 +1,3 @@ include "cvc5kinds.pxi" +include "cvc5types.pxi" include "cvc5.pxi" diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 269f3ebca3b..c9c70f77893 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -199,7 +199,7 @@ std::pair DTypeConstructor::computeCardinalityInfo( if (isParam) { paramTypes = t.getDType().getParameters(); - instTypes = t.getParamTypes(); + instTypes = t.getInstantiatedParamTypes(); } for (unsigned i = 0, nargs = getNumArgs(); i < nargs; i++) { @@ -328,7 +328,7 @@ Cardinality DTypeConstructor::computeCardinality( if (isParam) { paramTypes = t.getDType().getParameters(); - instTypes = t.getParamTypes(); + instTypes = t.getInstantiatedParamTypes(); } for (size_t i = 0, nargs = d_args.size(); i < nargs; i++) { @@ -390,7 +390,7 @@ Node DTypeConstructor::computeGroundTerm(TypeNode t, if (isParam) { paramTypes = t.getDType().getParameters(); - instTypes = TypeNode(t).getParamTypes(); + instTypes = TypeNode(t).getInstantiatedParamTypes(); } for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++) { diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp index cd244df148e..cc33494d8e6 100644 --- a/src/expr/type_matcher.cpp +++ b/src/expr/type_matcher.cpp @@ -15,6 +15,8 @@ #include "type_matcher.h" +#include "expr/dtype.h" + namespace cvc5 { TypeMatcher::TypeMatcher(TypeNode dt) @@ -25,7 +27,15 @@ TypeMatcher::TypeMatcher(TypeNode dt) void TypeMatcher::addTypesFromDatatype(TypeNode dt) { - std::vector argTypes = dt.getParamTypes(); + std::vector argTypes; + if (dt.isInstantiated()) + { + argTypes = dt.getInstantiatedParamTypes(); + } + else + { + argTypes = dt.getDType().getParameters(); + } addTypes(argTypes); Trace("typecheck-idt") << "instantiating matcher for " << dt << std::endl; for (unsigned i = 0, narg = argTypes.size(); i < narg; ++i) diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index de85dfb06b5..b784e8ce154 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -360,10 +360,12 @@ std::vector TypeNode::getArgTypes() const { return args; } -std::vector TypeNode::getParamTypes() const { +std::vector TypeNode::getInstantiatedParamTypes() const +{ + Assert(isInstantiated()); vector params; - Assert(isParametricDatatype()); - for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) { + for (uint32_t i = 1, i_end = getNumChildren(); i < i_end; ++i) + { params.push_back((*this)[i]); } return params; @@ -417,6 +419,12 @@ bool TypeNode::isInstantiatedDatatype() const { return true; } +bool TypeNode::isInstantiated() const +{ + return isInstantiatedDatatype() + || (isSort() && getNumChildren() > 0); +} + TypeNode TypeNode::instantiateParametricDatatype( const std::vector& params) const { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 9882c7fc53b..60b24d57e61 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -529,10 +529,16 @@ class TypeNode { std::vector getArgTypes() const; /** - * Get the paramater types of a parameterized datatype. Fails an - * assertion if this type is not a parametric datatype. + * Get the types used to instantiate the type parameters of a parametric + * type (parametric datatype or uninterpreted sort constructor type, + * see TypeNode::instantiate(const std::vector& const). + * + * Asserts that this type is an instantiated type. + * + * @return the types used to instantiate the type parameters of a + * parametric type */ - std::vector getParamTypes() const; + std::vector getInstantiatedParamTypes() const; /** * Get the range type (i.e., the type of the result) of a function, @@ -597,6 +603,12 @@ class TypeNode { /** Is this a fully instantiated datatype type */ bool isInstantiatedDatatype() const; + /** + * Return true if this is an instantiated parametric datatype or + * uninterpreted sort constructor type. + */ + bool isInstantiated() const; + /** Is this a sygus datatype type */ bool isSygusDatatype() const; diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 28b72a168fa..9aebabde618 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -425,20 +425,20 @@ name = "SMT Layer" help = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)" [[option]] - name = "interpols" + name = "interpolants" category = "regular" - long = "produce-interpols" + long = "produce-interpolants" type = "bool" default = "false" help = "turn on interpolation generation." [[option]] - name = "interpolsMode" + name = "interpolantsMode" category = "regular" - long = "interpols-mode=MODE" - type = "InterpolsMode" + long = "interpolants-mode=MODE" + type = "InterpolantsMode" default = "DEFAULT" - help = "choose interpolants production mode, see --interpols-mode=help" + help = "choose interpolants production mode, see --interpolants-mode=help" help_mode = "Interpolants grammar mode" [[option.mode.DEFAULT]] name = "default" @@ -465,12 +465,12 @@ name = "SMT Layer" help = "support the get-abduct command" [[option]] - name = "checkInterpols" + name = "checkInterpolants" category = "regular" - long = "check-interpols" + long = "check-interpolants" type = "bool" default = "false" - help = "checks whether produced solutions to get-interpol are correct" + help = "checks whether produced solutions to get-interpolant are correct" [[option]] name = "checkAbducts" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e0caa77e7dd..57abe495ff1 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1023,11 +1023,11 @@ extendedCommand[std::unique_ptr* cmd] sygusGrammar[g, terms, name] )? { - cmd->reset(new GetInterpolCommand(name, e, g)); + cmd->reset(new GetInterpolantCommand(name, e, g)); } | GET_INTERPOL_NEXT_TOK { PARSER_STATE->checkThatLogicIsSet(); - cmd->reset(new GetInterpolNextCommand); + cmd->reset(new GetInterpolantNextCommand); } | DECLARE_HEAP LPAREN_TOK sortSymbol[t, CHECK_DECLARED] @@ -1706,8 +1706,7 @@ termAtomic[cvc5::api::Term& atomTerm] | DECIMAL_LITERAL { std::string realStr = AntlrInput::tokenText($DECIMAL_LITERAL); - atomTerm = SOLVER->ensureTermSort(SOLVER->mkReal(realStr), - SOLVER->getRealSort()); + atomTerm = SOLVER->mkReal(realStr); } // Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity @@ -2251,8 +2250,8 @@ GET_QE_TOK : 'get-qe'; GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; GET_ABDUCT_TOK : 'get-abduct'; GET_ABDUCT_NEXT_TOK : 'get-abduct-next'; -GET_INTERPOL_TOK : 'get-interpol'; -GET_INTERPOL_NEXT_TOK : 'get-interpol-next'; +GET_INTERPOL_TOK : 'get-interpolant'; +GET_INTERPOL_NEXT_TOK : 'get-interpolant-next'; DECLARE_HEAP : 'declare-heap'; DECLARE_POOL : 'declare-pool'; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index f3909ae3f68..f543f1be723 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -402,12 +402,12 @@ void Printer::toStreamCmdGetInterpol(std::ostream& out, Node conj, TypeNode sygusType) const { - printUnknownCommand(out, "get-interpol"); + printUnknownCommand(out, "get-interpolant"); } void Printer::toStreamCmdGetInterpolNext(std::ostream& out) const { - printUnknownCommand(out, "get-interpol-next"); + printUnknownCommand(out, "get-interpolant-next"); } void Printer::toStreamCmdGetAbduct(std::ostream& out, diff --git a/src/printer/printer.h b/src/printer/printer.h index 33824d42deb..c5dd5ddc260 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -194,13 +194,13 @@ class Printer /** Print get-instantiations command */ void toStreamCmdGetInstantiations(std::ostream& out) const; - /** Print get-interpol command */ + /** Print get-interpolant command */ virtual void toStreamCmdGetInterpol(std::ostream& out, const std::string& name, Node conj, TypeNode sygusType) const; - /** Print get-interpol-next command */ + /** Print get-interpolant-next command */ virtual void toStreamCmdGetInterpolNext(std::ostream& out) const; /** Print get-abduct command */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 616c51bab1e..7145471dd82 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -2003,7 +2003,7 @@ void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out, Node conj, TypeNode sygusType) const { - out << "(get-interpol " << cvc5::quoteSymbol(name) << ' ' << conj; + out << "(get-interpolant " << cvc5::quoteSymbol(name) << ' ' << conj; if (!sygusType.isNull()) { out << ' ' << sygusGrammarString(sygusType); @@ -2013,7 +2013,7 @@ void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out, void Smt2Printer::toStreamCmdGetInterpolNext(std::ostream& out) const { - out << "(get-interpol-next)" << std::endl; + out << "(get-interpolant-next)" << std::endl; } void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out, diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 6f78f96689c..ec403fe001b 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -168,13 +168,13 @@ class Smt2Printer : public cvc5::Printer /** Print get-proof command */ void toStreamCmdGetProof(std::ostream& out) const override; - /** Print get-interpol command */ + /** Print get-interpolant command */ void toStreamCmdGetInterpol(std::ostream& out, const std::string& name, Node conj, TypeNode sygusType) const override; - /** Print get-interpol-next command */ + /** Print get-interpolant-next command */ void toStreamCmdGetInterpolNext(std::ostream& out) const override; /** Print get-abduct command */ diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index 7bea8f3f2f1..36944cdd1de 100644 --- a/src/proof/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -128,19 +128,6 @@ std::shared_ptr ProofNodeManager::mkScope( acu.insert(a); continue; } - // trivial assumption - if (a == d_true) - { - Trace("pnm-scope") << "- justify trivial True assumption\n"; - for (std::shared_ptr pfs : fa.second) - { - Assert(pfs->getResult() == a); - updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a}); - } - Trace("pnm-scope") << "...finished" << std::endl; - acu.insert(a); - continue; - } Trace("pnm-scope") << "- try matching free assumption " << a << "\n"; // otherwise it may be due to symmetry? Node aeqSym = CDProof::getSymmFact(a); @@ -155,6 +142,20 @@ std::shared_ptr ProofNodeManager::mkScope( } else { + // trivial assumption (by rewriting) + Node ar = d_rewriter->rewrite(a); + if (ar == d_true) + { + Trace("pnm-scope") << "- justify trivial True assumption\n"; + for (std::shared_ptr pfs : fa.second) + { + Assert(pfs->getResult() == a); + updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a}); + } + Trace("pnm-scope") << "...finished" << std::endl; + acu.insert(a); + continue; + } // Otherwise, may be derivable by rewriting. Note this is used in // ensuring that proofs from the proof equality engine that involve // equality with Boolean constants are closed. @@ -164,13 +165,10 @@ std::shared_ptr ProofNodeManager::mkScope( for (const Node& acc : ac) { Node accr = d_rewriter->rewrite(acc); - if (accr != acc) - { - acr[accr] = acc; - } + acr[accr] = acc; } } - Node ar = d_rewriter->rewrite(a); + Trace("pnm-scope") << "- rewritten: " << ar << std::endl; std::unordered_map::iterator itr = acr.find(ar); if (itr != acr.end()) { diff --git a/src/smt/command.cpp b/src/smt/command.cpp index f7772dab635..b8f7fac8d4f 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1897,32 +1897,33 @@ void GetInstantiationsCommand::toStream(std::ostream& out, /* class GetInterpolCommand */ /* -------------------------------------------------------------------------- */ -GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj) +GetInterpolantCommand::GetInterpolantCommand(const std::string& name, + api::Term conj) : d_name(name), d_conj(conj), d_sygus_grammar(nullptr) { } -GetInterpolCommand::GetInterpolCommand(const std::string& name, - api::Term conj, - api::Grammar* g) +GetInterpolantCommand::GetInterpolantCommand(const std::string& name, + api::Term conj, + api::Grammar* g) : d_name(name), d_conj(conj), d_sygus_grammar(g) { } -api::Term GetInterpolCommand::getConjecture() const { return d_conj; } +api::Term GetInterpolantCommand::getConjecture() const { return d_conj; } -const api::Grammar* GetInterpolCommand::getGrammar() const +const api::Grammar* GetInterpolantCommand::getGrammar() const { return d_sygus_grammar; } -api::Term GetInterpolCommand::getResult() const { return d_result; } +api::Term GetInterpolantCommand::getResult() const { return d_result; } -void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm) +void GetInterpolantCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - // we must remember the name of the interpolant, in case get-interpol-next - // is called later. + // we must remember the name of the interpolant, in case + // get-interpolant-next is called later. sm->setLastSynthName(d_name); if (d_sygus_grammar == nullptr) { @@ -1940,7 +1941,7 @@ void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -void GetInterpolCommand::printResult(std::ostream& out) const +void GetInterpolantCommand::printResult(std::ostream& out) const { if (!ok()) { @@ -1962,23 +1963,23 @@ void GetInterpolCommand::printResult(std::ostream& out) const } } -Command* GetInterpolCommand::clone() const +Command* GetInterpolantCommand::clone() const { - GetInterpolCommand* c = - new GetInterpolCommand(d_name, d_conj, d_sygus_grammar); + GetInterpolantCommand* c = + new GetInterpolantCommand(d_name, d_conj, d_sygus_grammar); c->d_result = d_result; return c; } -std::string GetInterpolCommand::getCommandName() const +std::string GetInterpolantCommand::getCommandName() const { - return "get-interpol"; + return "get-interpolant"; } -void GetInterpolCommand::toStream(std::ostream& out, - int toDepth, - size_t dag, - Language language) const +void GetInterpolantCommand::toStream(std::ostream& out, + int toDepth, + size_t dag, + Language language) const { Printer::getPrinter(language)->toStreamCmdGetInterpol( out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar)); @@ -1988,11 +1989,11 @@ void GetInterpolCommand::toStream(std::ostream& out, /* class GetInterpolNextCommand */ /* -------------------------------------------------------------------------- */ -GetInterpolNextCommand::GetInterpolNextCommand() {} +GetInterpolantNextCommand::GetInterpolantNextCommand() {} -api::Term GetInterpolNextCommand::getResult() const { return d_result; } +api::Term GetInterpolantNextCommand::getResult() const { return d_result; } -void GetInterpolNextCommand::invoke(api::Solver* solver, SymbolManager* sm) +void GetInterpolantNextCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2007,7 +2008,7 @@ void GetInterpolNextCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -void GetInterpolNextCommand::printResult(std::ostream& out) const +void GetInterpolantNextCommand::printResult(std::ostream& out) const { if (!ok()) { @@ -2029,22 +2030,22 @@ void GetInterpolNextCommand::printResult(std::ostream& out) const } } -Command* GetInterpolNextCommand::clone() const +Command* GetInterpolantNextCommand::clone() const { - GetInterpolNextCommand* c = new GetInterpolNextCommand; + GetInterpolantNextCommand* c = new GetInterpolantNextCommand; c->d_result = d_result; return c; } -std::string GetInterpolNextCommand::getCommandName() const +std::string GetInterpolantNextCommand::getCommandName() const { - return "get-interpol-next"; + return "get-interpolant-next"; } -void GetInterpolNextCommand::toStream(std::ostream& out, - int toDepth, - size_t dag, - Language language) const +void GetInterpolantNextCommand::toStream(std::ostream& out, + int toDepth, + size_t dag, + Language language) const { Printer::getPrinter(language)->toStreamCmdGetInterpolNext(out); } diff --git a/src/smt/command.h b/src/smt/command.h index 3e4997878e0..66877f42535 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1012,7 +1012,7 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command api::Solver* d_solver; }; /* class GetInstantiationsCommand */ -/** The command (get-interpol s B (G)?) +/** The command (get-interpolant s B (G)?) * * This command asks for an interpolant from the current set of assertions and * conjecture (goal) B. @@ -1021,12 +1021,14 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command * find a predicate P, then the output response of this command is: (define-fun * s () Bool P) */ -class CVC5_EXPORT GetInterpolCommand : public Command +class CVC5_EXPORT GetInterpolantCommand : public Command { public: - GetInterpolCommand(const std::string& name, api::Term conj); + GetInterpolantCommand(const std::string& name, api::Term conj); /** The argument g is the grammar of the interpolation query */ - GetInterpolCommand(const std::string& name, api::Term conj, api::Grammar* g); + GetInterpolantCommand(const std::string& name, + api::Term conj, + api::Grammar* g); /** Get the conjecture of the interpolation query */ api::Term getConjecture() const; @@ -1056,11 +1058,11 @@ class CVC5_EXPORT GetInterpolCommand : public Command api::Term d_result; }; /* class GetInterpolCommand */ -/** The command (get-interpol-next) */ -class CVC5_EXPORT GetInterpolNextCommand : public Command +/** The command (get-interpolant-next) */ +class CVC5_EXPORT GetInterpolantNextCommand : public Command { public: - GetInterpolNextCommand(); + GetInterpolantNextCommand(); /** * Get the result of the query, which is the solution to the interpolation * query. diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 549d4f28b70..e7589ff8984 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -41,10 +41,10 @@ bool InterpolationSolver::getInterpolant(const std::vector& axioms, const TypeNode& grammarType, Node& interpol) { - if (!options().smt.interpols) + if (!options().smt.interpolants) { const char* msg = - "Cannot get interpolation when produce-interpols options is off."; + "Cannot get interpolation when produce-interpolants options is off."; throw ModalException(msg); } Trace("sygus-interpol") << "SolverEngine::getInterpol: conjecture " << conj @@ -58,7 +58,7 @@ bool InterpolationSolver::getInterpolant(const std::vector& axioms, if (d_subsolver->solveInterpolation( name, axioms, conjn, grammarType, interpol)) { - if (options().smt.checkInterpols) + if (options().smt.checkInterpolants) { checkInterpol(interpol, axioms, conj); } @@ -70,7 +70,7 @@ bool InterpolationSolver::getInterpolant(const std::vector& axioms, bool InterpolationSolver::getInterpolantNext(Node& interpol) { // should already have initialized a subsolver, since we are immediately - // preceeded by a successful call to get-interpol(-next). + // preceeded by a successful call to get-interpolant(-next). Assert(d_subsolver != nullptr); return d_subsolver->solveInterpolationNext(interpol); } diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index d1f1c7fd885..f41cea180d9 100644 --- a/src/smt/interpolation_solver.h +++ b/src/smt/interpolation_solver.h @@ -35,8 +35,8 @@ namespace smt { /** * A solver for interpolation queries. * - * This class is responsible for responding to get-interpol commands. It spawns - * a subsolver SolverEngine for a sygus conjecture that captures the + * This class is responsible for responding to get-interpolant commands. It + * spawns a subsolver SolverEngine for a sygus conjecture that captures the * interpolation query, and implements supporting utility methods such as * checkInterpol. */ diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 4b7e70b4a3d..9f5e7cbe28b 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -856,7 +856,7 @@ bool SetDefaults::isSygus(const Options& opts) const } if (!d_isInternalSubsolver) { - if (opts.smt.produceAbducts || opts.smt.interpols + if (opts.smt.produceAbducts || opts.smt.interpolants || opts.quantifiers.sygusInference || opts.quantifiers.sygusRewSynthInput) { diff --git a/src/smt/smt_mode.h b/src/smt/smt_mode.h index 098bf1cb754..8937c798ce1 100644 --- a/src/smt/smt_mode.h +++ b/src/smt/smt_mode.h @@ -41,7 +41,7 @@ enum class SmtMode UNSAT, // immediately after a successful call to get-abduct ABDUCT, - // immediately after a successful call to get-interpol + // immediately after a successful call to get-interpolant INTERPOL, // immediately after a successful call to check-synth or check-synth-next SYNTH diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 5a27454b7c7..f1f98c7413e 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -220,7 +220,7 @@ void SolverEngine::finishInit() { d_abductSolver.reset(new AbductionSolver(*d_env.get())); } - if (d_env->getOptions().smt.interpols) + if (d_env->getOptions().smt.interpolants) { d_interpolSolver.reset(new InterpolationSolver(*d_env)); } @@ -1643,7 +1643,7 @@ Node SolverEngine::getInterpolant(const Node& conj, const TypeNode& grammarType) Node interpol; bool success = d_interpolSolver->getInterpolant(axioms, conj, grammarType, interpol); - // notify the state of whether the get-interpol call was successfuly, which + // notify the state of whether the get-interpolant call was successfuly, which // impacts the SMT mode. d_state->notifyGetInterpol(success); Assert(success == !interpol.isNull()); @@ -1657,12 +1657,13 @@ Node SolverEngine::getInterpolantNext() if (d_state->getMode() != SmtMode::INTERPOL) { throw RecoverableModalException( - "Cannot get-interpol-next unless immediately preceded by a successful " - "call to get-interpol(-next)."); + "Cannot get-interpolant-next unless immediately preceded by a " + "successful " + "call to get-interpolant(-next)."); } Node interpol; bool success = d_interpolSolver->getInterpolantNext(interpol); - // notify the state of whether the get-interpolant-next call was successful + // notify the state of whether the get-interpolantant-next call was successful d_state->notifyGetInterpol(success); Assert(success == !interpol.isNull()); return interpol; diff --git a/src/smt/solver_engine_state.h b/src/smt/solver_engine_state.h index ac1a25e70e6..fe638181e41 100644 --- a/src/smt/solver_engine_state.h +++ b/src/smt/solver_engine_state.h @@ -108,7 +108,7 @@ class SolverEngineState : protected EnvObj /** * Notify that we finished an interpolation query, where success is whether * the command was successful. This is managed independently of the above - * calls for notifying check-sat. In other words, if a get-interpol command + * calls for notifying check-sat. In other words, if a get-interpolant command * is issued to an SolverEngine, it may use a satisfiability call (if desired) * to solve the interpolation query. This method is called *in addition* to * the above calls to notifyCheckSat / notifyCheckSatResult in this case. diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index b64f1d1da5e..72b05ec2d3e 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -795,6 +795,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) d_infoMap.setConstArr(node, node); Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node); d_defValues[node] = defaultValue; + setNonLinear(node); break; } default: diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index b1e9b32b736..3dae04861fe 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -117,7 +117,13 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node, NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - Node x = sm->mkPurifySkolem(node, "bagChoose"); + // the skolem will occur in a term context, thus we give it Boolean + // term variable kind immediately. + SkolemManager::SkolemFlags flags = node.getType().isBoolean() + ? SkolemManager::SKOLEM_BOOL_TERM_VAR + : SkolemManager::SKOLEM_DEFAULT; + Node x = sm->mkPurifySkolem( + node, "bagChoose", "a variable used to eliminate bag choose", flags); Node A = node[0]; TypeNode bagType = A.getType(); TypeNode ufType = nm->mkFunctionType(bagType, bagType.getBagElementType()); diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index 875896cd45a..a0596b3b680 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -255,6 +255,7 @@ Node IntBlaster::translateWithChildren( Assert(oldKind != kind::BITVECTOR_SREM); Assert(oldKind != kind::BITVECTOR_SMOD); Assert(oldKind != kind::BITVECTOR_XNOR); + Assert(oldKind != kind::BITVECTOR_NOR); Assert(oldKind != kind::BITVECTOR_NAND); Assert(oldKind != kind::BITVECTOR_SUB); Assert(oldKind != kind::BITVECTOR_REPEAT); @@ -1080,8 +1081,8 @@ Node IntBlaster::createBVNegNode(Node n, uint64_t bvsize) { // Based on Hacker's Delight section 2-2 equation a: // -x = ~x+1 - Node p2 = pow2(bvsize); - return d_nm->mkNode(kind::SUB, p2, n); + Node bvNotNode = createBVNotNode(n, bvsize); + return createBVAddNode(bvNotNode, d_one, bvsize); } Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize) diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index cfd49f97b9c..0d9aecf57d1 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -99,21 +99,22 @@ void SygusInterpol::getIncludeCons( std::map>& result) { NodeManager* nm = NodeManager::currentNM(); - Assert(options().smt.interpols); + Assert(options().smt.interpolants); // ASSUMPTIONS - if (options().smt.interpolsMode == options::InterpolsMode::ASSUMPTIONS) + if (options().smt.interpolantsMode == options::InterpolantsMode::ASSUMPTIONS) { Node tmpAssumptions = (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); expr::getOperatorsMap(tmpAssumptions, result); } // CONJECTURE - else if (options().smt.interpolsMode == options::InterpolsMode::CONJECTURE) + else if (options().smt.interpolantsMode + == options::InterpolantsMode::CONJECTURE) { expr::getOperatorsMap(conj, result); } // SHARED - else if (options().smt.interpolsMode == options::InterpolsMode::SHARED) + else if (options().smt.interpolantsMode == options::InterpolantsMode::SHARED) { // Get operators from axioms std::map> include_cons_axioms; @@ -153,7 +154,7 @@ void SygusInterpol::getIncludeCons( } } // ALL - else if (options().smt.interpolsMode == options::InterpolsMode::ALL) + else if (options().smt.interpolantsMode == options::InterpolantsMode::ALL) { Node tmpAssumptions = (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); @@ -274,7 +275,7 @@ bool SygusInterpol::findInterpol(SolverEngine* subSolver, Trace("sygus-interpol") << "SolverEngine::getInterpol: could not find solution!" << std::endl; throw RecoverableModalException( - "Could not find solution for get-interpol."); + "Could not find solution for get-interpolant."); return false; } Trace("sygus-interpol") << "SolverEngine::getInterpol: solution is " diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 604e7435fa3..78c7da61d4b 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -32,7 +32,7 @@ class SolverEngine; namespace theory { namespace quantifiers { /** - * This is an utility for the SMT-LIB command (get-interpol ). + * This is an utility for the SMT-LIB command (get-interpolant ). * The utility turns a set of quantifier-free assertions into a sygus * conjecture that encodes an interpolation problem, and then solve the * interpolation problem by synthesizing it. In detail, if our input formula is @@ -48,7 +48,7 @@ namespace quantifiers { * * This class uses a fresh copy of the SMT engine which is used for solving the * interpolation problem. In particular, consider the input: (assert A) - * (get-interpol s B) + * (get-interpolant s B) * In the copy of the SMT engine where these commands are issued, we maintain * A in the assertion stack. In solving the interpolation problem, we will * need to call a SMT engine solver with a different assertion stack, which is diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 8f23e9232f6..b01895a74d5 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -1030,7 +1030,12 @@ void CardinalityExtension::mkModelValueElementsFor( { TypeNode elementType = eqc.getType().getSetElementType(); bool elementTypeFinite = d_env.isFiniteType(elementType); - if (isModelValueBasic(eqc)) + bool isBasic = isModelValueBasic(eqc); + Trace("sets-model") << "mkModelValueElementsFor: " << eqc + << ", isBasic = " << isBasic + << ", isFinite = " << elementTypeFinite + << ", els = " << els << std::endl; + if (isBasic) { std::map::iterator it = d_eqc_to_card_term.find(eqc); if (it != d_eqc_to_card_term.end()) diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index e61881daa4d..6d5de217219 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -218,7 +218,7 @@ void TheorySets::processCarePairArgs(TNode a, TNode b) // equality or disequality between members affects the number of elements // in a set. Therefore we need to split on (= x y) for kind SET_MEMBER. // Example: - // Suppose (= (member x S) member(y S)) is true and there are + // Suppose (set.member x S) = (set.member y S) = true and there are // no other members in S. We would get S = {x} if (= x y) is true. // Otherwise we would get S = {x, y}. if (a.getKind() != SET_MEMBER && d_state.areEqual(a, b)) diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 099843e3c03..57835919e78 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -247,7 +247,14 @@ void TheorySetsPrivate::fullEffortCheck() Node n = (*eqc_i); if (n != eqc) { - Trace("sets-eqc") << n << " (" << n.isConst() << ") "; + if (TraceIsOn("sets-eqc")) + { + Trace("sets-eqc") << n; + if (n.isConst()) + { + Trace("sets-eqc") << " (const) "; + } + } } TypeNode tnn = n.getType(); if (isSet) @@ -1211,7 +1218,13 @@ TrustNode TheorySetsPrivate::expandChooseOperator( NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - Node x = sm->mkPurifySkolem(node, "setChoose"); + // the skolem will occur in a term context, thus we give it Boolean + // term variable kind immediately. + SkolemManager::SkolemFlags flags = node.getType().isBoolean() + ? SkolemManager::SKOLEM_BOOL_TERM_VAR + : SkolemManager::SKOLEM_DEFAULT; + Node x = sm->mkPurifySkolem( + node, "setChoose", "a variable used to eliminate set choose", flags); Node A = node[0]; TypeNode setType = A.getType(); ensureFirstClassSetType(setType); diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index f7a26e535a6..ac0ec5f052a 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -123,6 +123,8 @@ set(regress_0_tests regress0/arrays/issue5720.smt2 regress0/arrays/issue5836-2.smt2 regress0/arrays/issue5836.smt2 + regress0/arrays/issue5925.smt2 + regress0/arrays/issue5925-2.smt2 regress0/arrays/issue6276-2.smt2 regress0/arrays/issue6276.smt2 regress0/arrays/issue6700-inc-check-model.smt2 @@ -276,6 +278,8 @@ set(regress_0_tests regress0/bv/bv_to_int_bvuf_to_intuf.smt2 regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 regress0/bv/bv_to_int_elim_err.smt2 + regress0/bv/bv_to_int_issue_8413_1.smt2 + regress0/bv/bv_to_int_issue_8413_2.smt2 regress0/bv/bv_to_int_int1.smt2 regress0/bv/bv_to_int_zext.smt2 regress0/bv/bvcomp.cvc.smt2 @@ -1261,6 +1265,7 @@ set(regress_0_tests regress0/sets/proj-issue177.smt2 regress0/sets/proj-issue486-sets-split-eq.smt2 regress0/sets/proj-issue493-choose-det.smt2 + regress0/sets/proj-issue501-choose-bool-term-var.smt2 regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 regress0/sets/setel-eq.smt2 regress0/sets/sets-deq-dd.smt2 diff --git a/test/regress/cli/regress0/arrays/issue5925-2.smt2 b/test/regress/cli/regress0/arrays/issue5925-2.smt2 new file mode 100644 index 00000000000..6beb2e9ba30 --- /dev/null +++ b/test/regress/cli/regress0/arrays/issue5925-2.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_A) +(set-info :status unsat) +(declare-const a (Array Bool Bool)) +(assert (= (store a true false) (store (store ((as const (Array Bool Bool)) true) true false) false false))) +(assert (select a false)) +(check-sat) diff --git a/test/regress/cli/regress0/arrays/issue5925.smt2 b/test/regress/cli/regress0/arrays/issue5925.smt2 new file mode 100644 index 00000000000..de88c037ec3 --- /dev/null +++ b/test/regress/cli/regress0/arrays/issue5925.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_ABV) +(set-info :status unsat) +(declare-const a (Array Bool Bool)) +(declare-const b Bool) +(declare-const c Bool) +(declare-const d Bool) +(assert (= (store (store ((as const (Array Bool Bool)) true) true false) false false) (store a b c))) +(assert b) +(assert (= d (select a c))) +(assert d) +(check-sat) diff --git a/test/regress/cli/regress0/bv/bv_to_int_issue_8413_1.smt2 b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_1.smt2 new file mode 100644 index 00000000000..48073ac6722 --- /dev/null +++ b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_1.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --solve-bv-as-int=sum +; EXPECT: sat + +(set-logic QF_BV) + +(declare-fun zero () (_ BitVec 16)) +(declare-fun x () (_ BitVec 16)) + +(assert (= zero (_ bv0 16))) +(assert (= zero (bvneg x))) + +(check-sat) diff --git a/test/regress/cli/regress0/bv/bv_to_int_issue_8413_2.smt2 b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_2.smt2 new file mode 100644 index 00000000000..0dfa7a77aa2 --- /dev/null +++ b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_2.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --solve-bv-as-int=sum +; EXPECT: sat + +(set-logic QF_BV) +(declare-fun a () (_ BitVec 1)) +(assert (= (_ bv0 16) (bvsdiv ((_ zero_extend 8) ((_ zero_extend 7) a)) (bvnor (_ bv0 16) (_ bv0 16))))) +(check-sat) diff --git a/test/regress/cli/regress0/sets/proj-issue501-choose-bool-term-var.smt2 b/test/regress/cli/regress0/sets/proj-issue501-choose-bool-term-var.smt2 new file mode 100644 index 00000000000..0fcdbdd25ae --- /dev/null +++ b/test/regress/cli/regress0/sets/proj-issue501-choose-bool-term-var.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-option :sets-ext true) +(set-option :fmf-bound true) +(declare-const x (Bag (Set Bool))) +(declare-const x1 (Set Bool)) +(declare-const x3 (Set Bool)) +(declare-const x6 (Set Bool)) +(assert (set.choose (ite (set.is_singleton x3) x6 x1))) +(assert (<= (set.card x6) (bag.count x6 x))) +(check-sat) diff --git a/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2 b/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2 index 120683519c2..53a25ad12e5 100644 --- a/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2 +++ b/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols -i +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants -i ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic NIA) @@ -7,7 +7,7 @@ (declare-fun z ( ) Int) (push) (assert (= (* 2 x) y)) -(get-interpol A (distinct (+ (* 2 z) 1) y) +(get-interpolant A (distinct (+ (* 2 z) 1) y) ; the grammar for the interpol-to-synthesize ((Start Bool) (StartInt Int)) @@ -20,7 +20,7 @@ (pop) (assert (= (* 2 y) x)) -(get-interpol A (distinct (+ (* 2 z) 1) x) +(get-interpolant A (distinct (+ (* 2 z) 1) x) ; the grammar for the interpol-to-synthesize ((Start Bool) (StartInt Int)) ( diff --git a/test/regress/cli/regress1/sygus/interpol1.smt2 b/test/regress/cli/regress1/sygus/interpol1.smt2 index 4597a25921a..7e863c145d6 100644 --- a/test/regress/cli/regress1/sygus/interpol1.smt2 +++ b/test/regress/cli/regress1/sygus/interpol1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic NIA) @@ -6,7 +6,7 @@ (declare-fun y ( ) Int) (declare-fun z ( ) Int) (assert (= (* 2 x) y)) -(get-interpol A (distinct (+ (* 2 z) 1) y) +(get-interpolant A (distinct (+ (* 2 z) 1) y) ; the grammar for the interpol-to-synthesize ((Start Bool) (StartInt Int)) diff --git a/test/regress/cli/regress1/sygus/interpol3-next.smt2 b/test/regress/cli/regress1/sygus/interpol3-next.smt2 index 3108e08f801..7eab15652d9 100644 --- a/test/regress/cli/regress1/sygus/interpol3-next.smt2 +++ b/test/regress/cli/regress1/sygus/interpol3-next.smt2 @@ -1,8 +1,8 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --check-interpols -i +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --check-interpolants -i ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic LIA) (declare-fun a () Int) (assert (> a 1)) -(get-interpol A (> a 0)) -(get-interpol-next) +(get-interpolant A (> a 0)) +(get-interpolant-next) diff --git a/test/regress/cli/regress1/sygus/interpol3.smt2 b/test/regress/cli/regress1/sygus/interpol3.smt2 index 293ff545f15..6761129a498 100644 --- a/test/regress/cli/regress1/sygus/interpol3.smt2 +++ b/test/regress/cli/regress1/sygus/interpol3.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic LIA) (declare-fun a () Int) (assert (> a 1)) -(get-interpol A (> a 0)) +(get-interpolant A (> a 0)) diff --git a/test/regress/cli/regress1/sygus/interpol_arr1.smt2 b/test/regress/cli/regress1/sygus/interpol_arr1.smt2 index a15078bdbf5..27c0370f3a5 100644 --- a/test/regress/cli/regress1/sygus/interpol_arr1.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_arr1.smt2 @@ -1,8 +1,8 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) (declare-fun a () (Array (_ BitVec 4) (_ BitVec 4))) (declare-fun y () (_ BitVec 4)) (assert (= (select a y) (_ bv0 4))) -(get-interpol A (distinct (select a y) (_ bv1 4))) +(get-interpolant A (distinct (select a y) (_ bv1 4))) diff --git a/test/regress/cli/regress1/sygus/interpol_arr2.smt2 b/test/regress/cli/regress1/sygus/interpol_arr2.smt2 index 9bc7846ad4b..737b737223b 100644 --- a/test/regress/cli/regress1/sygus/interpol_arr2.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_arr2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -12,4 +12,4 @@ (assert (and A1 A2 A3 A4 A5)) ;The conjuecture is: 2 <= x+y -(get-interpol A (<= 2 (+ (select arr 2) (select arr 3)))) +(get-interpolant A (<= 2 (+ (select arr 2) (select arr 3)))) diff --git a/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2 b/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2 index 78a441384b7..400ead7e517 100644 --- a/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=conjecture --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=conjecture --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -24,4 +24,4 @@ (declare-fun op@2 () (_ BitVec 4)) (declare-fun witness_0@2 () Bool) (assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1))))) -(get-interpol I (not (and (and true (and (and (and (and true (= witness_0@2 (not (= (bvand (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@1 (_ bv0 4))) (bvadd a@1 b@1) (bvsub a@1 b@1)) (bvadd a@1 b@1)) input14@1))) (_ bv1 1))))) (= op@2 (ite (= cfg@1 (_ bv1 1)) (_ bv0 4) op@1))) (= counter@2 (bvadd counter@1 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@2 (_ bv0 1)))) (not witness_0@2)))) +(get-interpolant I (not (and (and true (and (and (and (and true (= witness_0@2 (not (= (bvand (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@1 (_ bv0 4))) (bvadd a@1 b@1) (bvsub a@1 b@1)) (bvadd a@1 b@1)) input14@1))) (_ bv1 1))))) (= op@2 (ite (= cfg@1 (_ bv1 1)) (_ bv0 4) op@1))) (= counter@2 (bvadd counter@1 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@2 (_ bv0 1)))) (not witness_0@2)))) diff --git a/test/regress/cli/regress1/sygus/interpol_dt.smt2 b/test/regress/cli/regress1/sygus/interpol_dt.smt2 index 50ab5749a91..1c7a9b702cf 100644 --- a/test/regress/cli/regress1/sygus/interpol_dt.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_dt.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -9,4 +9,4 @@ (assert ((_ is nil) (tail x))) (assert (= (head x) 0)) (assert (= x y)) -(get-interpol A (distinct y nil)) +(get-interpolant A (distinct y nil)) diff --git a/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2 b/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2 index 71c9e4a800d..eab51547168 100644 --- a/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -36,4 +36,4 @@ (declare-fun f1@0 () (_ BitVec 1)) (assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) -(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) +(get-interpolant I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) diff --git a/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2 b/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2 index 89c067a7314..a0ed63d57c1 100644 --- a/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -37,5 +37,5 @@ (assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) (assert (and (or (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (bvult v_c@0 (_ bv2 16))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) -(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) +(get-interpolant I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) diff --git a/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2 b/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2 index 37be96f10bc..bf9265621c5 100644 --- a/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -49,6 +49,6 @@ (declare-fun v_c@2 () (_ BitVec 16)) (assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) -(get-interpol I (not (and (and true (and (and (and (and (and (and (and (and (and (and true (= v_c@2 (bvxor (_ bv1 16) (ite (= f5@1 (_ bv1 1)) v_x2@1 (ite (= f2@1 (_ bv1 1)) v_x1@1 (bvxor (_ bv1 16) v_c@1)))))) (= v_x1@2 (ite (= f1@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x1@1)))) (= v_x2@2 (ite (= f4@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x2@1)))) (= a_Q_a1@2 (bvnot (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (= a_R_a1@2 (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)))) (= a_S_a1@2 (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)))) (= a_Q_a2@2 (bvnot (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))) (= a_R_a2@2 (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)))) (= a_S_a2@2 (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)))) (= dve_invalid@2 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@1) (bvand (bvnot a_Q_a1@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@1 (bvnot f1@1))) (bvor a_S_a1@1 (bvnot f2@1))) (bvor (bvnot f3@1) (bvand (bvnot a_Q_a2@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@1 (bvnot f4@1))) (bvor a_S_a2@1 (bvnot f5@1))) (bvor f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@1 f1@1) (bvand f2@1 (bvor f0@1 f1@1))) (bvand f3@1 (bvor f2@1 (bvor f0@1 f1@1)))) (bvand f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1))))) (bvand f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@1) a_R_a1@1) (bvand a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1)))) (bvor a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1))) (bvnot (bvor (bvand (bvnot a_Q_a2@1) a_R_a2@1) (bvand a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1))))) (bvor a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)) (bvand (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1))))) (bvor (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)) (bvand (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))))) (bvor (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1))))) (bvnot dve_invalid@1)))))) (not (not (= (bvand (bvnot dve_invalid@2) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@2) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) +(get-interpolant I (not (and (and true (and (and (and (and (and (and (and (and (and (and true (= v_c@2 (bvxor (_ bv1 16) (ite (= f5@1 (_ bv1 1)) v_x2@1 (ite (= f2@1 (_ bv1 1)) v_x1@1 (bvxor (_ bv1 16) v_c@1)))))) (= v_x1@2 (ite (= f1@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x1@1)))) (= v_x2@2 (ite (= f4@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x2@1)))) (= a_Q_a1@2 (bvnot (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (= a_R_a1@2 (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)))) (= a_S_a1@2 (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)))) (= a_Q_a2@2 (bvnot (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))) (= a_R_a2@2 (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)))) (= a_S_a2@2 (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)))) (= dve_invalid@2 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@1) (bvand (bvnot a_Q_a1@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@1 (bvnot f1@1))) (bvor a_S_a1@1 (bvnot f2@1))) (bvor (bvnot f3@1) (bvand (bvnot a_Q_a2@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@1 (bvnot f4@1))) (bvor a_S_a2@1 (bvnot f5@1))) (bvor f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@1 f1@1) (bvand f2@1 (bvor f0@1 f1@1))) (bvand f3@1 (bvor f2@1 (bvor f0@1 f1@1)))) (bvand f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1))))) (bvand f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@1) a_R_a1@1) (bvand a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1)))) (bvor a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1))) (bvnot (bvor (bvand (bvnot a_Q_a2@1) a_R_a2@1) (bvand a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1))))) (bvor a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)) (bvand (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1))))) (bvor (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)) (bvand (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))))) (bvor (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1))))) (bvnot dve_invalid@1)))))) (not (not (= (bvand (bvnot dve_invalid@2) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@2) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) diff --git a/test/regress/cli/regress3/interpol2.smt2 b/test/regress/cli/regress3/interpol2.smt2 index 7050fbd6347..67805b0169e 100644 --- a/test/regress/cli/regress3/interpol2.smt2 +++ b/test/regress/cli/regress3/interpol2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 @@ -28,4 +28,4 @@ (assert (and A1 A2 A3 A4 A5)) ;The conjuecture is: 2 <= x+y -(get-interpol A (<= 2 (+ x y))) +(get-interpolant A (<= 2 (+ x y))) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 1921cd645f9..d9a38ec08b5 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -452,7 +452,20 @@ TEST_F(TestApiBlackSolver, mkBoolean) TEST_F(TestApiBlackSolver, mkRoundingMode) { - ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); + 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) @@ -1402,7 +1415,7 @@ TEST_F(TestApiBlackSolver, getAbductNext) TEST_F(TestApiBlackSolver, getInterpolant) { d_solver.setLogic("QF_LIA"); - d_solver.setOption("produce-interpols", "true"); + d_solver.setOption("produce-interpolants", "true"); d_solver.setOption("incremental", "false"); Sort intSort = d_solver.getIntegerSort(); @@ -1430,7 +1443,7 @@ TEST_F(TestApiBlackSolver, getInterpolant) TEST_F(TestApiBlackSolver, getInterpolantNext) { d_solver.setLogic("QF_LIA"); - d_solver.setOption("produce-interpols", "true"); + d_solver.setOption("produce-interpolants", "true"); d_solver.setOption("incremental", "true"); Sort intSort = d_solver.getIntegerSort(); diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index 9a9368fbc9a..37beffa9083 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -321,6 +321,28 @@ TEST_F(TestApiBlackSort, instantiate) ASSERT_THROW( dtypeSort.instantiate(std::vector{d_solver.getIntegerSort()}), CVC5ApiException); + // instantiate uninterpreted sort constructor + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); + ASSERT_NO_THROW( + sortConsSort.instantiate(std::vector{d_solver.getIntegerSort()})); +} + +TEST_F(TestApiBlackSort, isInstantiated) +{ + Sort paramDtypeSort = create_param_datatype_sort(); + ASSERT_FALSE(paramDtypeSort.isInstantiated()); + Sort instParamDtypeSort = + paramDtypeSort.instantiate(std::vector{d_solver.getIntegerSort()}); + ASSERT_TRUE(instParamDtypeSort.isInstantiated()); + + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); + ASSERT_FALSE(sortConsSort.isInstantiated()); + Sort instSortConsSort = + sortConsSort.instantiate(std::vector{d_solver.getIntegerSort()}); + ASSERT_TRUE(instSortConsSort.isInstantiated()); + + ASSERT_FALSE(d_solver.getIntegerSort().isInstantiated()); + ASSERT_FALSE(d_solver.mkBitVectorSort(32).isInstantiated()); } TEST_F(TestApiBlackSort, getFunctionArity) @@ -406,17 +428,6 @@ TEST_F(TestApiBlackSort, getSymbol) ASSERT_THROW(bvSort.getSymbol(), CVC5ApiException); } -TEST_F(TestApiBlackSort, isUninterpretedSortParameterized) -{ - Sort uSort = d_solver.mkUninterpretedSort("u"); - ASSERT_FALSE(uSort.isUninterpretedSortParameterized()); - Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); - Sort siSort = sSort.instantiate({uSort}); - ASSERT_TRUE(siSort.isUninterpretedSortParameterized()); - Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.isUninterpretedSortParameterized(), CVC5ApiException); -} - TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts) { Sort uSort = d_solver.mkUninterpretedSort("u"); diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index 81dfd2e43ce..e5be408eb6e 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -920,6 +920,35 @@ TEST_F(TestApiBlackTerm, getUninterpretedSortValue) ASSERT_EQ(vx.getUninterpretedSortValue(), vy.getUninterpretedSortValue()); } +TEST_F(TestApiBlackTerm, isRoundingModeValue) +{ + ASSERT_FALSE(d_solver.mkInteger(15).isRoundingModeValue()); + ASSERT_TRUE(d_solver.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN) + .isRoundingModeValue()); + ASSERT_FALSE( + d_solver.mkConst(d_solver.getRoundingModeSort()).isRoundingModeValue()); +} + +TEST_F(TestApiBlackTerm, getRoundingModeValue) +{ + ASSERT_THROW(d_solver.mkInteger(15).getRoundingModeValue(), CVC5ApiException); + ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN) + .getRoundingModeValue(), + RoundingMode::ROUND_NEAREST_TIES_TO_EVEN); + ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE) + .getRoundingModeValue(), + RoundingMode::ROUND_TOWARD_POSITIVE); + ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_NEGATIVE) + .getRoundingModeValue(), + RoundingMode::ROUND_TOWARD_NEGATIVE); + ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO) + .getRoundingModeValue(), + RoundingMode::ROUND_TOWARD_ZERO); + ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY) + .getRoundingModeValue(), + RoundingMode::ROUND_NEAREST_TIES_TO_AWAY); +} + TEST_F(TestApiBlackTerm, getTuple) { Sort s1 = d_solver.getIntegerSort(); @@ -1108,6 +1137,21 @@ TEST_F(TestApiBlackTerm, getSequenceValue) ASSERT_THROW(su.getSequenceValue(), CVC5ApiException); } +TEST_F(TestApiBlackTerm, getCardinalityConstraint) +{ + Sort su = d_solver.mkUninterpretedSort("u"); + Term t = d_solver.mkCardinalityConstraint(su, 3); + ASSERT_TRUE(t.isCardinalityConstraint()); + std::pair cc = t.getCardinalityConstraint(); + ASSERT_EQ(cc.first, su); + ASSERT_EQ(cc.second, 3); + Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); + ASSERT_FALSE(x.isCardinalityConstraint()); + ASSERT_THROW(x.getCardinalityConstraint(), CVC5ApiException); + Term nullt; + ASSERT_THROW(nullt.isCardinalityConstraint(), CVC5ApiException); +} + TEST_F(TestApiBlackTerm, termScopedToString) { Sort intsort = d_solver.getIntegerSort(); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index e4b981dfa64..eebc335d9bb 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -430,7 +430,16 @@ class SolverTest @Test void mkRoundingMode() throws CVC5ApiException { - assertDoesNotThrow(() -> d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO)); + assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).toString(), + "roundNearestTiesToEven"); + assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE).toString(), + "roundTowardPositive"); + assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE).toString(), + "roundTowardNegative"); + assertEquals( + d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO).toString(), "roundTowardZero"); + assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY).toString(), + "roundNearestTiesToAway"); } @Test void mkFloatingPoint() throws CVC5ApiException @@ -1394,7 +1403,7 @@ class SolverTest @Test void getInterpolant() throws CVC5ApiException { d_solver.setLogic("QF_LIA"); - d_solver.setOption("produce-interpols", "true"); + d_solver.setOption("produce-interpolants", "true"); d_solver.setOption("incremental", "false"); Sort intSort = d_solver.getIntegerSort(); @@ -1419,7 +1428,7 @@ class SolverTest @Test void getInterpolantNext() throws CVC5ApiException { d_solver.setLogic("QF_LIA"); - d_solver.setOption("produce-interpols", "true"); + d_solver.setOption("produce-interpolants", "true"); d_solver.setOption("incremental", "true"); Sort intSort = d_solver.getIntegerSort(); diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index 2115c027a96..426b67a56dd 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -311,6 +311,25 @@ Sort create_param_datatype_sort() throws CVC5ApiException Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); assertThrows(CVC5ApiException.class, () -> dtypeSort.instantiate(new Sort[] {d_solver.getIntegerSort()})); + // instantiate uninterpreted sort constructor + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); + assertDoesNotThrow(() -> sortConsSort.instantiate(new Sort[] {d_solver.getIntegerSort()})); + } + + @Test void isInstantiated() throws CVC5ApiException + { + Sort paramDtypeSort = create_param_datatype_sort(); + assertFalse(paramDtypeSort.isInstantiated()); + Sort instParamDtypeSort = paramDtypeSort.instantiate(new Sort[] {d_solver.getIntegerSort()}); + assertTrue(instParamDtypeSort.isInstantiated()); + + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); + assertFalse(sortConsSort.isInstantiated()); + Sort instSortConsSort = sortConsSort.instantiate(new Sort[] {d_solver.getIntegerSort()}); + assertTrue(instSortConsSort.isInstantiated()); + + assertFalse(d_solver.getIntegerSort().isInstantiated()); + assertFalse(d_solver.mkBitVectorSort(32).isInstantiated()); } @Test void getFunctionArity() throws CVC5ApiException @@ -396,17 +415,6 @@ Sort create_param_datatype_sort() throws CVC5ApiException assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol()); } - @Test void isUninterpretedSortParameterized() throws CVC5ApiException - { - Sort uSort = d_solver.mkUninterpretedSort("u"); - assertFalse(uSort.isUninterpretedSortParameterized()); - Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); - Sort siSort = sSort.instantiate(new Sort[] {uSort}); - assertTrue(siSort.isUninterpretedSortParameterized()); - Sort bvSort = d_solver.mkBitVectorSort(32); - assertThrows(CVC5ApiException.class, () -> bvSort.isUninterpretedSortParameterized()); - } - @Test void getUninterpretedSortParamSorts() throws CVC5ApiException { Sort uSort = d_solver.mkUninterpretedSort("u"); diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index 9baa290af74..ee5d1429da5 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -870,6 +870,31 @@ class TermTest assertDoesNotThrow(() -> vy.getUninterpretedSortValue()); } + @Test void isRoundingModeValue() throws CVC5ApiException + { + assertFalse(d_solver.mkInteger(15).isRoundingModeValue()); + assertTrue( + d_solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).isRoundingModeValue()); + assertFalse(d_solver.mkConst(d_solver.getRoundingModeSort()).isRoundingModeValue()); + } + + @Test void getRoundingModeValue() throws CVC5ApiException + { + assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(15).getRoundingModeValue()); + assertEquals( + d_solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).getRoundingModeValue(), + RoundingMode.ROUND_NEAREST_TIES_TO_EVEN); + assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE).getRoundingModeValue(), + RoundingMode.ROUND_TOWARD_POSITIVE); + assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE).getRoundingModeValue(), + RoundingMode.ROUND_TOWARD_NEGATIVE); + assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO).getRoundingModeValue(), + RoundingMode.ROUND_TOWARD_ZERO); + assertEquals( + d_solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY).getRoundingModeValue(), + RoundingMode.ROUND_NEAREST_TIES_TO_AWAY); + } + @Test void getTuple() { Sort s1 = d_solver.getIntegerSort(); @@ -972,6 +997,21 @@ private void assertSetsEquality(Term[] A, Set B) assertEquals(Arrays.asList(new Term[] {i1, i1, i2}), Arrays.asList(s5.getSequenceValue())); } + @Test void getCardinalityConstraint() throws CVC5ApiException + { + Sort su = d_solver.mkUninterpretedSort("u"); + Term t = d_solver.mkCardinalityConstraint(su, 3); + assertTrue(t.isCardinalityConstraint()); + Pair cc = t.getCardinalityConstraint(); + assertEquals(cc.first, su); + assertEquals(cc.second, new BigInteger("3")); + Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); + assertFalse(x.isCardinalityConstraint()); + assertThrows(CVC5ApiException.class, () -> x.getCardinalityConstraint()); + Term nullt = d_solver.getNullTerm(); + assertThrows(CVC5ApiException.class, () -> nullt.isCardinalityConstraint()); + } + @Test void substitute() { Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index baf52b89709..fdb71ed44dd 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -15,7 +15,7 @@ import cvc5 import sys -from cvc5 import Kind +from cvc5 import Kind, RoundingMode @pytest.fixture @@ -32,7 +32,7 @@ def test_recoverable_exception(solver): def test_supports_floating_point(solver): - solver.mkRoundingMode(cvc5.RoundNearestTiesToEven) + solver.mkRoundingMode(RoundingMode.RoundNearestTiesToEven) def test_get_boolean_sort(solver): @@ -407,7 +407,16 @@ def test_mk_boolean(solver): def test_mk_rounding_mode(solver): - solver.mkRoundingMode(cvc5.RoundTowardZero) + assert str(solver.mkRoundingMode( + RoundingMode.RoundNearestTiesToEven)) == "roundNearestTiesToEven" + assert str(solver.mkRoundingMode( + RoundingMode.RoundTowardPositive)) == "roundTowardPositive" + assert str(solver.mkRoundingMode( + RoundingMode.RoundTowardNegative)) == "roundTowardNegative" + assert str(solver.mkRoundingMode( + RoundingMode.RoundTowardZero)) == "roundTowardZero" + assert str(solver.mkRoundingMode( + RoundingMode.RoundNearestTiesToAway)) == "roundNearestTiesToAway" def test_mk_floating_point(solver): @@ -2147,7 +2156,7 @@ def test_get_abduct_next(solver): def test_get_interpolant(solver): solver.setLogic("QF_LIA") - solver.setOption("produce-interpols", "true") + solver.setOption("produce-interpolants", "true") solver.setOption("incremental", "false") intSort = solver.getIntegerSort() @@ -2168,7 +2177,7 @@ def test_get_interpolant(solver): def test_get_interpolant_next(solver): solver.setLogic("QF_LIA") - solver.setOption("produce-interpols", "true") + solver.setOption("produce-interpolants", "true") solver.setOption("incremental", "true") intSort = solver.getIntegerSort() diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index b530f2c37f9..a78884a9316 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -299,7 +299,23 @@ def test_instantiate(solver): dtypeSort = solver.mkDatatypeSort(dtypeSpec) with pytest.raises(RuntimeError): dtypeSort.instantiate([solver.getIntegerSort()]) + # instantiate uninterpreted sort constructor + sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 1) + sortConsSort.instantiate([solver.getIntegerSort()]) +def test_is_instantiated(solver): + paramDtypeSort = create_param_datatype_sort(solver) + assert not paramDtypeSort.isInstantiated() + instParamDtypeSort = paramDtypeSort.instantiate([solver.getIntegerSort()]); + assert instParamDtypeSort.isInstantiated() + + sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 1) + assert not sortConsSort.isInstantiated() + instSortConsSort = sortConsSort.instantiate([solver.getIntegerSort()]) + assert instSortConsSort.isInstantiated() + + assert not solver.getIntegerSort().isInstantiated() + assert not solver.mkBitVectorSort(32).isInstantiated() def test_get_function_arity(solver): funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), @@ -384,17 +400,6 @@ def test_get_uninterpreted_sort_name(solver): bvSort.getSymbol() -def test_is_uninterpreted_sort_parameterized(solver): - uSort = solver.mkUninterpretedSort("u") - assert not uSort.isUninterpretedSortParameterized() - sSort = solver.mkUninterpretedSortConstructorSort("s", 1) - siSort = sSort.instantiate([uSort]) - assert siSort.isUninterpretedSortParameterized() - bvSort = solver.mkBitVectorSort(32) - with pytest.raises(RuntimeError): - bvSort.isUninterpretedSortParameterized() - - def test_get_uninterpreted_sort_paramsorts(solver): uSort = solver.mkUninterpretedSort("u") uSort.getUninterpretedSortParamSorts() diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index 27d1d913e3c..16f3fa180af 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -13,7 +13,7 @@ import pytest import cvc5 -from cvc5 import Kind +from cvc5 import Kind, RoundingMode from cvc5 import Sort, Term from fractions import Fraction @@ -972,6 +972,34 @@ def test_get_uninterpreted_sort_value(solver): assert vx.getUninterpretedSortValue() == vy.getUninterpretedSortValue() +def test_is_rounding_mode_value(solver): + assert not solver.mkInteger(15).isRoundingModeValue() + assert solver.mkRoundingMode( + RoundingMode.RoundNearestTiesToEven).isRoundingModeValue() + assert not solver.mkConst( + solver.getRoundingModeSort()).isRoundingModeValue() + + +def test_get_rounding_mode_value(solver): + with pytest.raises(RuntimeError): + solver.mkInteger(15).getRoundingModeValue() + assert solver.mkRoundingMode( + RoundingMode.RoundNearestTiesToEven).getRoundingModeValue( + ) == RoundingMode.RoundNearestTiesToEven + assert solver.mkRoundingMode( + RoundingMode.RoundTowardPositive).getRoundingModeValue( + ) == RoundingMode.RoundTowardPositive + assert solver.mkRoundingMode( + RoundingMode.RoundTowardNegative).getRoundingModeValue( + ) == RoundingMode.RoundTowardNegative + assert solver.mkRoundingMode( + RoundingMode.RoundTowardZero).getRoundingModeValue( + ) == RoundingMode.RoundTowardZero + assert solver.mkRoundingMode( + RoundingMode.RoundNearestTiesToAway).getRoundingModeValue( + ) == RoundingMode.RoundNearestTiesToAway + + def test_get_tuple(solver): s1 = solver.getIntegerSort() s2 = solver.getRealSort()