diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-11-11 20:32:43 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-11-11 20:32:43 -0800 |
| commit | 3ce6b395e69d492d02cb41cce118d14ae45e8b01 (patch) | |
| tree | 208ca69503f7793fd511936243fca80ecfcfb337 | |
| parent | 4597b472f1c81551e6ca2d92b95c438bd3081b4c (diff) | |
| parent | 5cfbb67e228daf76835b7fd0a95d214859be030e (diff) | |
Merge branch 'master' into mapConstRational
150 files changed, 1387 insertions, 523 deletions
diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt index f505a7fb4..e37183f90 100644 --- a/docs/CMakeLists.txt +++ b/docs/CMakeLists.txt @@ -16,6 +16,7 @@ find_package(Sphinx REQUIRED) check_python_module(breathe) check_python_module(sphinxcontrib.bibtex sphinxcontrib-bibtex) check_python_module(sphinx_tabs.tabs sphinx-tabs) +check_python_module(sphinxcontrib.programoutput sphinxcontrib.programoutput) add_subdirectory(api) diff --git a/docs/api/api.rst b/docs/api/api.rst index a3acdda17..4a1fb7202 100644 --- a/docs/api/api.rst +++ b/docs/api/api.rst @@ -1,6 +1,11 @@ API Documentation ================= +In addition to using cvc5 :doc:`as a binary <../binary/binary>`, cvc5 features APIs +for several different programming languages. +While the :doc:`C++ API <cpp/cpp>` is considered the primary interface to cvc5, both the :doc:`Java API <java/index>` and the :doc:`Python API <python/python>` implement a thin wrapper around it. +Additionally, a more pythonic Python API is availble at https://github.com/cvc5/cvc5_z3py_compat. + .. toctree:: :maxdepth: 1 diff --git a/docs/api/cpp/class_hierarchy.rst b/docs/api/cpp/class_hierarchy.rst deleted file mode 100644 index b441106ff..000000000 --- a/docs/api/cpp/class_hierarchy.rst +++ /dev/null @@ -1,47 +0,0 @@ -C++ API Class Hierarchy -======================= - -``namespace cvc5::api {`` - - * class :cpp:class:`CVC5ApiException <cvc5::api::CVC5ApiException>` - * class :cpp:class:`CVC5ApiRecoverableException <cvc5::api::CVC5ApiRecoverableException>` - - * class :ref:`api/cpp/datatype:datatype` - - * class :cpp:class:`const_iterator <cvc5::api::Datatype::const_iterator>` - - * class :ref:`api/cpp/datatypeconstructor:datatypeconstructor` - - * class :cpp:class:`const_iterator <cvc5::api::DatatypeConstructor::const_iterator>` - - * class :ref:`api/cpp/datatypeconstructordecl:datatypeconstructordecl` - * class :ref:`api/cpp/datatypedecl:datatypedecl` - * class :ref:`api/cpp/datatypeselector:datatypeselector` - - * class :ref:`api/cpp/grammar:grammar` - - * class :ref:`api/cpp/kind:kind` - - * class :ref:`api/cpp/op:op` - - * class :ref:`api/cpp/optioninfo:optioninfo` - - * class :ref:`api/cpp/result:result` - - * enum :cpp:enum:`UnknownExplanation <cvc5::api::Result::UnknownExplanation>` - - * class :ref:`api/cpp/roundingmode:roundingmode` - - * class :ref:`api/cpp/solver:solver` - - * class :ref:`api/cpp/sort:sort` - - * class :cpp:class:`Stat <cvc5::api::Stat>` - - * class :cpp:class:`Statistics <cvc5::api::Statistics>` - - * class :ref:`api/cpp/term:term` - - * class :cpp:class:`const_iterator <cvc5::api::Term::const_iterator>` - -``}`` diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst index edcbbd87d..96177e7d8 100644 --- a/docs/api/cpp/cpp.rst +++ b/docs/api/cpp/cpp.rst @@ -1,25 +1,23 @@ -.. _cpp-api: - C++ API Documentation ===================== -.. toctree:: - :maxdepth: 1 +The C++ API is the primary interface for cvc5 and exposes the full functionality of cvc5. +The :doc:`quickstart guide <quickstart>` gives a short introduction, while the following class hierarchy of the ``cvc5::api`` namespace provides more details on the individual classes. +For most applications, the :cpp:class:`Solver <cvc5::api::Solver>` class is the main entry point to cvc5. - quickstart - class_hierarchy .. container:: hide-toctree .. toctree:: :maxdepth: 0 + quickstart + exceptions datatype datatypeconstructor datatypeconstructordecl datatypedecl datatypeselector - exceptions grammar kind op @@ -30,3 +28,41 @@ C++ API Documentation sort statistics term + + +Class hierarchy +^^^^^^^^^^^^^^^ + +``namespace cvc5::api {`` + + * class :cpp:class:`CVC5ApiException <cvc5::api::CVC5ApiException>` + * class :cpp:class:`CVC5ApiRecoverableException <cvc5::api::CVC5ApiRecoverableException>` + * class :ref:`api/cpp/datatype:datatype` + + * class :cpp:class:`const_iterator <cvc5::api::Datatype::const_iterator>` + + * class :ref:`api/cpp/datatypeconstructor:datatypeconstructor` + + * class :cpp:class:`const_iterator <cvc5::api::DatatypeConstructor::const_iterator>` + + * class :ref:`api/cpp/datatypeconstructordecl:datatypeconstructordecl` + * class :ref:`api/cpp/datatypedecl:datatypedecl` + * class :ref:`api/cpp/datatypeselector:datatypeselector` + * class :ref:`api/cpp/grammar:grammar` + * class :ref:`api/cpp/kind:kind` + * class :ref:`api/cpp/op:op` + * class :ref:`api/cpp/optioninfo:optioninfo` + * class :ref:`api/cpp/result:result` + + * enum :cpp:enum:`UnknownExplanation <cvc5::api::Result::UnknownExplanation>` + + * class :ref:`api/cpp/roundingmode:roundingmode` + * class :ref:`api/cpp/solver:solver` + * class :ref:`api/cpp/sort:sort` + * class :cpp:class:`Stat <cvc5::api::Stat>` + * class :cpp:class:`Statistics <cvc5::api::Statistics>` + * class :ref:`api/cpp/term:term` + + * class :cpp:class:`const_iterator <cvc5::api::Term::const_iterator>` + +``}``
\ No newline at end of file diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt index 7c897a354..8a728407f 100644 --- a/docs/api/java/CMakeLists.txt +++ b/docs/api/java/CMakeLists.txt @@ -23,19 +23,18 @@ if(BUILD_BINDINGS_JAVA) # used to trigger the rebuild set(JAVADOC_INDEX_FILE ${JAVADOC_OUTPUT_DIR}/index.html) - get_target_property(SOURCES cvc5jar SOURCES) - + get_target_property(CVC5_JAR_FILE cvc5jar JAR_FILE) add_custom_command( - OUTPUT "${JAVADOC_INDEX_FILE}" - COMMAND + OUTPUT ${JAVADOC_INDEX_FILE} + COMMAND ${Java_JAVADOC_EXECUTABLE} io.github.cvc5.api - -sourcepath ${CMAKE_SOURCE_DIR}/src/api/java/ + -sourcepath ${CMAKE_SOURCE_DIR}/src/api/java/:${CMAKE_BINARY_DIR}/src/api/java/ -d ${JAVADOC_OUTPUT_DIR} - -cp ${CMAKE_BINARY_DIR}/src/api/java/cvc5.jar + -cp ${CVC5_JAR_FILE} -notimestamp COMMAND find ${JAVADOC_OUTPUT_DIR} -type f -exec sed -i'orig' 's/<!-- Generated by javadoc [^>]* -->//' {} "\;" COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete - DEPENDS cvc5jar ${SOURCES} + DEPENDS cvc5jar ${CVC5_JAR_FILE} COMMENT "Generating javadocs" ) diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index f6258af2d..0cf78d0ce 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -1,5 +1,3 @@ -.. _python-api: - Python API Documentation ======================== diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst index 91e2493e7..44a177afb 100644 --- a/docs/binary/binary.rst +++ b/docs/binary/binary.rst @@ -1,11 +1,18 @@ Binary Documentation ==================== +The easiest way to use cvc5 is usually to invoke the cvc5 binary via the command line. +The :doc:`quickstart guide <quickstart>` gives a short introduction on how to use cvc5 via the SMT-LIBv2 +interface, but cvc5 also supports other :doc:`input languages <languages>`. +The behavior of cvc5 can be changed with a number of :doc:`options <options>`, and :doc:`output tags <output-tags>` allow to extract structured information about the solving process. + +Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different programming languages. .. toctree:: :maxdepth: 2 quickstart + languages options output-tags diff --git a/docs/languages.rst b/docs/binary/languages.rst index 34c536017..34c536017 100644 --- a/docs/languages.rst +++ b/docs/binary/languages.rst diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst index 67280ca45..f3c9c4ad8 100644 --- a/docs/binary/quickstart.rst +++ b/docs/binary/quickstart.rst @@ -119,7 +119,7 @@ Example | The source code for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_. .. api-examples:: + ../../examples/api/smtlib/quickstart.smt2 ../../examples/api/cpp/quickstart.cpp ../../examples/api/java/QuickStart.java ../../examples/api/python/quickstart.py - ../../examples/api/smtlib/quickstart.smt2 diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst index 0b2651851..accdd004f 100644 --- a/docs/examples/examples.rst +++ b/docs/examples/examples.rst @@ -1,7 +1,7 @@ Examples =========== -The following examples show how the APIs (:ref:`cpp-api`, :ref:`python-api`) +The following examples show how the APIs (:doc:`../api/cpp/cpp`, :doc:`../api/java/index`, :doc:`../api/python/python`) and input languages can be used. For every example, the same problem is constructed and solved using different input mechanisms. diff --git a/docs/index.rst b/docs/index.rst index 5f0ede34f..27b7b728d 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -18,7 +18,6 @@ Table of Contents binary/binary api/api examples/examples - languages theory references genindex diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst index 423a5d4b1..8bce6b72c 100644 --- a/docs/theories/sets-and-relations.rst +++ b/docs/theories/sets-and-relations.rst @@ -42,7 +42,9 @@ a `cvc5::api::Solver solver` object. | | | | | | | ``Term t = solver.mkTerm(Kind::SET_UNION, X, Y);`` | +----------------------+----------------------------------------------+-------------------------------------------------------------------------+ -| Intersection | ``(set.minus X Y)`` | ``Term t = solver.mkTerm(Kind::SET_MINUS, X, Y);`` | +| Intersection | ``(set.inter X Y)`` | ``Term t = solver.mkTerm(Kind::SET_INTER, X, Y);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Minus | ``(set.minus X Y)`` | ``Term t = solver.mkTerm(Kind::SET_MINUS, X, Y);`` | +----------------------+----------------------------------------------+-------------------------------------------------------------------------+ | Membership | ``(set.member x X)`` | ``Term x = solver.mkConst(solver.getIntegerSort(), "x");`` | | | | | @@ -76,7 +78,7 @@ Semantics ^^^^^^^^^ The semantics of most of the above operators (e.g., ``set.union``, -``set.intersection``, difference) are straightforward. +``set.inter``, difference) are straightforward. The semantics for the universe set and complement are more subtle and explained in the following. diff --git a/examples/api/cpp/sets.cpp b/examples/api/cpp/sets.cpp index a4bc12ec8..ff3546b6f 100644 --- a/examples/api/cpp/sets.cpp +++ b/examples/api/cpp/sets.cpp @@ -43,10 +43,10 @@ int main() Term C = slv.mkConst(set, "C"); Term unionAB = slv.mkTerm(SET_UNION, A, B); - Term lhs = slv.mkTerm(SET_INTERSECTION, unionAB, C); + Term lhs = slv.mkTerm(SET_INTER, unionAB, C); - Term intersectionAC = slv.mkTerm(SET_INTERSECTION, A, C); - Term intersectionBC = slv.mkTerm(SET_INTERSECTION, B, C); + Term intersectionAC = slv.mkTerm(SET_INTER, A, C); + Term intersectionBC = slv.mkTerm(SET_INTER, B, C); Term rhs = slv.mkTerm(SET_UNION, intersectionAC, intersectionBC); Term theorem = slv.mkTerm(EQUAL, lhs, rhs); @@ -77,7 +77,7 @@ int main() Term singleton_three = slv.mkTerm(SET_SINGLETON, three); Term one_two = slv.mkTerm(SET_UNION, singleton_one, singleton_two); Term two_three = slv.mkTerm(SET_UNION, singleton_two, singleton_three); - Term intersection = slv.mkTerm(SET_INTERSECTION, one_two, two_three); + Term intersection = slv.mkTerm(SET_INTER, one_two, two_three); Term x = slv.mkConst(integer, "x"); diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index bf487c617..31f20dfeb 100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -40,10 +40,10 @@ if __name__ == "__main__": C = slv.mkConst(set_, "C") unionAB = slv.mkTerm(kinds.SetUnion, A, B) - lhs = slv.mkTerm(kinds.SetIntersection, unionAB, C) + lhs = slv.mkTerm(kinds.SetInter, unionAB, C) - intersectionAC = slv.mkTerm(kinds.SetIntersection, A, C) - intersectionBC = slv.mkTerm(kinds.SetIntersection, B, C) + intersectionAC = slv.mkTerm(kinds.SetInter, A, C) + intersectionBC = slv.mkTerm(kinds.SetInter, B, C) rhs = slv.mkTerm(kinds.SetUnion, intersectionAC, intersectionBC) theorem = slv.mkTerm(kinds.Equal, lhs, rhs) @@ -72,7 +72,7 @@ if __name__ == "__main__": singleton_three = slv.mkTerm(kinds.SetSingleton, three) one_two = slv.mkTerm(kinds.SetUnion, singleton_one, singleton_two) two_three = slv.mkTerm(kinds.SetUnion, singleton_two, singleton_three) - intersection = slv.mkTerm(kinds.SetIntersection, one_two, two_three) + intersection = slv.mkTerm(kinds.SetInter, one_two, two_three) x = slv.mkConst(integer, "x") diff --git a/examples/api/smtlib/sets.smt2 b/examples/api/smtlib/sets.smt2 index f8b30ae47..59d3cdc4f 100644 --- a/examples/api/smtlib/sets.smt2 +++ b/examples/api/smtlib/sets.smt2 @@ -10,8 +10,8 @@ (check-sat-assuming ( (distinct - (set.intersection (set.union A B) C) - (set.union (set.intersection A C) (set.intersection B C))) + (set.inter (set.union A B) C) + (set.union (set.inter A C) (set.inter B C))) ) ) @@ -27,7 +27,7 @@ ( (set.member x - (set.intersection + (set.inter (set.union (set.singleton 1) (set.singleton 2)) (set.union (set.singleton 2) (set.singleton 3)))) ) diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index 69fc07837..0e1b93146 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -146,7 +146,7 @@ class Mapper { << " ( (s1 " << name << ") (s2 " << name << ") )" << " " << name << "" << " ((_ map and) s1 s2))" << endl; - setoperators[make_pair(t, kind::SET_INTERSECTION)] = + setoperators[make_pair(t, kind::SET_INTER)] = em->mkVar(std::string("intersection") + elementTypeAsString, em->mkFunctionType(t_t, t)); diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index db18a4bc8..4d90ae742 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1129,6 +1129,8 @@ libcvc5_add_sources( theory/uf/proof_equality_engine.h theory/uf/ho_extension.cpp theory/uf/ho_extension.h + theory/uf/lambda_lift.cpp + theory/uf/lambda_lift.h theory/uf/symmetry_breaker.cpp theory/uf/symmetry_breaker.h theory/uf/theory_uf.cpp diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index e62a3249d..39277b7e8 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -53,6 +53,7 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" #include "expr/node_manager.h" +#include "expr/node_manager_attributes.h" #include "expr/sequence.h" #include "expr/type_node.h" #include "expr/uninterpreted_constant.h" @@ -275,7 +276,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{ /* Sets ---------------------------------------------------------------- */ {SET_EMPTY, cvc5::Kind::SET_EMPTY}, {SET_UNION, cvc5::Kind::SET_UNION}, - {SET_INTERSECTION, cvc5::Kind::SET_INTERSECTION}, + {SET_INTER, cvc5::Kind::SET_INTER}, {SET_MINUS, cvc5::Kind::SET_MINUS}, {SET_SUBSET, cvc5::Kind::SET_SUBSET}, {SET_MEMBER, cvc5::Kind::SET_MEMBER}, @@ -585,7 +586,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> /* Sets ------------------------------------------------------------ */ {cvc5::Kind::SET_EMPTY, SET_EMPTY}, {cvc5::Kind::SET_UNION, SET_UNION}, - {cvc5::Kind::SET_INTERSECTION, SET_INTERSECTION}, + {cvc5::Kind::SET_INTER, SET_INTER}, {cvc5::Kind::SET_MINUS, SET_MINUS}, {cvc5::Kind::SET_SUBSET, SET_SUBSET}, {cvc5::Kind::SET_MEMBER, SET_MEMBER}, @@ -2528,6 +2529,29 @@ Op Term::getOp() const CVC5_API_TRY_CATCH_END; } +bool Term::hasSymbol() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->hasAttribute(expr::VarNameAttr()); + //////// + CVC5_API_TRY_CATCH_END; +} + +std::string Term::getSymbol() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(d_node->hasAttribute(expr::VarNameAttr())) + << "Invalid call to '" << __PRETTY_FUNCTION__ + << "', expected the term to have a symbol."; + //////// all checks before this line + return d_node->getAttribute(expr::VarNameAttr()); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Term::isNull() const { CVC5_API_TRY_CATCH_BEGIN; @@ -4687,6 +4711,7 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, bool Grammar::containsFreeVariables(const Term& rule) const { + // we allow the argument list and non-terminal symbols to be in scope std::unordered_set<TNode> scope; for (const Term& sygusVar : d_sygusVars) @@ -4699,8 +4724,7 @@ bool Grammar::containsFreeVariables(const Term& rule) const scope.emplace(*ntsymbol.d_node); } - std::unordered_set<Node> fvs; - return expr::getFreeVariablesScope(*rule.d_node, fvs, scope, false); + return expr::hasFreeVariablesScope(*rule.d_node, scope); } std::ostream& operator<<(std::ostream& out, const Grammar& grammar) @@ -5080,8 +5104,12 @@ Term Solver::mkBVFromStrHelper(uint32_t size, Term Solver::getValueHelper(const Term& term) const { // Note: Term is checked in the caller to avoid double checks - CVC5_API_RECOVERABLE_CHECK(!expr::hasFreeVar(term.getNode())) - << "Cannot get value of term containing free variables"; + bool wasShadow = false; + bool freeOrShadowedVar = + expr::hasFreeOrShadowedVar(term.getNode(), wasShadow); + CVC5_API_RECOVERABLE_CHECK(!freeOrShadowedVar) + << "Cannot get value of term containing " + << (wasShadow ? "shadowed" : "free") << " variables"; //////// all checks before this line Node value = d_slv->getValue(*term.d_node); Term res = Term(this, value); @@ -5798,6 +5826,19 @@ Term Solver::mkReal(int64_t num, int64_t den) const CVC5_API_TRY_CATCH_END; } +Term Solver::mkRegexpAll() const +{ + CVC5_API_TRY_CATCH_BEGIN; + //////// all checks before this line + Node res = d_nodeMgr->mkNode( + cvc5::kind::REGEXP_STAR, + d_nodeMgr->mkNode(cvc5::kind::REGEXP_ALLCHAR, std::vector<cvc5::Node>())); + (void)res.getType(true); /* kick off type checking */ + return Term(this, res); + //////// + CVC5_API_TRY_CATCH_END; +} + Term Solver::mkRegexpNone() const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 73e3c6942..ad6f4c7df 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1129,6 +1129,17 @@ class CVC5_EXPORT Term Op getOp() const; /** + * @return true if the term has a symbol. + */ + bool hasSymbol() const; + + /** + * Asserts hasSymbol(). + * @return the raw symbol of the term. + */ + std::string getSymbol() const; + + /** * @return true if this Term is a null term */ bool isNull() const; @@ -2649,19 +2660,19 @@ enum RoundingMode ROUND_NEAREST_TIES_TO_EVEN, /** * Round towards positive infinity (+oo). - * The result shall be the format’s floating-point number (possibly +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) + * 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 + * 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, @@ -3444,18 +3455,24 @@ class CVC5_EXPORT Solver Term mkReal(int64_t num, int64_t den) const; /** - * Create a regular expression none (re.none) term. - * @return the empty term + * Create a regular expression all (re.all) term. + * @return the all term */ - Term mkRegexpNone() const; + Term mkRegexpAll() const; /** * Create a regular expression allchar (re.allchar) term. - * @return the sigma term + * @return the allchar term */ Term mkRegexpAllchar() const; /** + * Create a regular expression none (re.none) term. + * @return the none term + */ + Term mkRegexpNone() const; + + /** * Create a constant representing an empty set of the given sort. * @param sort the sort of the set elements. * @return the empty set constant diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 162ec24e7..c0c269be2 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -331,10 +331,6 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ CARDINALITY_CONSTRAINT, -#if 0 - /* Partial uninterpreted function application. */ - PARTIAL_APPLY_UF, -#endif /** * Higher-order applicative encoding of function application, left * associative. @@ -2139,7 +2135,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - SET_INTERSECTION, + SET_INTER, /** * Set subtraction. * diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 58f9ee4b5..ecfec2109 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -140,6 +140,5 @@ add_jar(cvc5jar VERSION ${CVC5_VERSION} OUTPUT_NAME cvc5 ) -set_target_properties(cvc5jar PROPERTIES SOURCES "${JAVA_FILES}") add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5) diff --git a/src/api/java/genkinds.py.in b/src/api/java/genkinds.py.in index a15472a1a..d44ae3c0d 100644 --- a/src/api/java/genkinds.py.in +++ b/src/api/java/genkinds.py.in @@ -97,7 +97,12 @@ CPP_JAVA_MAPPING = \ r"std::vector<Term>": "Term[]", r"std::string": "String", r"&": "", - r"::": "." + r"::": ".", + r">": ">", + r"<": "<", + r"@f\[": "", + r"@f\]": "", + r"@note": "", } diff --git a/src/api/java/io/github/cvc5/api/RoundingMode.java b/src/api/java/io/github/cvc5/api/RoundingMode.java index ecc01c342..6a3c274a1 100644 --- a/src/api/java/io/github/cvc5/api/RoundingMode.java +++ b/src/api/java/io/github/cvc5/api/RoundingMode.java @@ -25,19 +25,19 @@ public enum RoundingMode { ROUND_NEAREST_TIES_TO_EVEN(0), /** * Round towards positive infinity (+oo). - * The result shall be the format’s floating-point number (possibly +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) + * 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 + * 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), diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 09ad66f5b..16220228c 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -851,8 +851,8 @@ public class Solver implements IPointer, AutoCloseable private native long mkReal(long pointer, long num, long den); /** - * Create a regular expression empty term. - * @return the empty term + * Create a regular expression none (re.none) term. + * @return the none term */ public Term mkRegexpNone() { @@ -863,8 +863,20 @@ public class Solver implements IPointer, AutoCloseable private native long mkRegexpNone(long pointer); /** - * Create a regular expression sigma term. - * @return the sigma term + * Create a regular expression all (re.all) term. + * @return the all term + */ + public Term mkRegexpAll() + { + long termPointer = mkRegexpAll(pointer); + return new Term(this, termPointer); + } + + private native long mkRegexpAll(long pointer); + + /** + * Create a regular expression allchar (re.allchar) term. + * @return the allchar term */ public Term mkRegexpAllchar() { diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java index bbed609f7..fc09767ed 100644 --- a/src/api/java/io/github/cvc5/api/Term.java +++ b/src/api/java/io/github/cvc5/api/Term.java @@ -201,6 +201,27 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable< private native long getOp(long pointer); /** + * @return true if the term has a symbol. + */ + public boolean hasSymbol() + { + return hasSymbol(pointer); + } + + private native boolean hasSymbol(long pointer); + + /** + * Asserts hasSymbol(). + * @return the raw symbol of the term. + */ + public String getSymbol() + { + return getSymbol(pointer); + } + + private native String getSymbol(long pointer); + + /** * @return true if this Term is a null term */ public boolean isNull() diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index a3ce49f4e..2e4404362 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -992,6 +992,21 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpNone( /* * Class: io_github_cvc5_api_Solver + * Method: mkRegexpAll + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkRegexpAll(JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkRegexpAll()); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: io_github_cvc5_api_Solver * Method: mkRegexpAllchar * Signature: (J)J */ diff --git a/src/api/java/jni/term.cpp b/src/api/java/jni/term.cpp index d54b0a2b5..702a5064d 100644 --- a/src/api/java/jni/term.cpp +++ b/src/api/java/jni/term.cpp @@ -247,6 +247,36 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getOp(JNIEnv* env, /* * Class: io_github_cvc5_api_Term + * Method: hasSymbol + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_hasSymbol(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast<Term*>(pointer); + return static_cast<jboolean>(current->hasSymbol()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false)); +} + +/* + * Class: io_github_cvc5_api_Term + * Method: getSymbol + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getSymbol(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast<Term*>(pointer); + return env->NewStringUTF(current->getSymbol().c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: io_github_cvc5_api_Term * Method: isNull * Signature: (J)Z */ diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index baee5899e..f5dc2aca2 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -215,8 +215,9 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkInteger(const uint64_t i) except + Term mkInteger(const string& s) except + Term mkReal(const string& s) except + - Term mkRegexpNone() except + + Term mkRegexpAll() except + Term mkRegexpAllchar() except + + Term mkRegexpNone() except + Term mkEmptySet(Sort s) except + Term mkEmptyBag(Sort s) except + Term mkSepEmp() except + @@ -390,6 +391,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term substitute(const vector[Term] & es, const vector[Term] & reps) except + bint hasOp() except + Op getOp() except + + bint hasSymbol() except + + string getSymbol() except + bint isNull() except + Term getConstArrayBase() except + Term notTerm() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 9e1aeaca1..3d24b5dbd 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1130,24 +1130,33 @@ cdef class Solver: term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode()) return term - def mkRegexpNone(self): - """Create a regular expression empty term. + def mkRegexpAll(self): + """Create a regular expression all (re.all) term. - :return: the empty term + :return: the all term """ cdef Term term = Term(self) - term.cterm = self.csolver.mkRegexpNone() + term.cterm = self.csolver.mkRegexpAll() return term def mkRegexpAllchar(self): - """Create a regular expression sigma term. + """Create a regular expression allchar (re.allchar) term. - :return: the sigma term + :return: the allchar term """ cdef Term term = Term(self) term.cterm = self.csolver.mkRegexpAllchar() return term + def mkRegexpNone(self): + """Create a regular expression none (re.none) term. + + :return: the none term + """ + cdef Term term = Term(self) + term.cterm = self.csolver.mkRegexpNone() + return term + def mkEmptySet(self, Sort s): """Create a constant representing an empty set of the given sort. @@ -2830,6 +2839,12 @@ cdef class Term: op.cop = self.cterm.getOp() return op + def hasSymbol(self): + return self.cterm.hasSymbol() + + def getSymbol(self): + return self.cterm.getSymbol().decode() + def isNull(self): return self.cterm.isNull() diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 13265db71..badf0b75a 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -281,64 +281,32 @@ bool hasBoundVar(TNode n) return n.getAttribute(HasBoundVarAttr()); } -bool hasFreeVar(TNode n) -{ - // optimization for variables and constants - if (n.getNumChildren() == 0) - { - return n.getKind() == kind::BOUND_VARIABLE; - } - std::unordered_set<Node> fvs; - return getFreeVariables(n, fvs, false); -} - -struct HasClosureTag -{ -}; -struct HasClosureComputedTag -{ -}; -/** Attribute true for expressions with closures in them */ -typedef expr::Attribute<HasClosureTag, bool> HasClosureAttr; -typedef expr::Attribute<HasClosureComputedTag, bool> HasClosureComputedAttr; - -bool hasClosure(Node n) -{ - if (!n.getAttribute(HasClosureComputedAttr())) - { - bool hasC = false; - if (n.isClosure()) - { - hasC = true; - } - else - { - for (auto i = n.begin(); i != n.end() && !hasC; ++i) - { - hasC = hasClosure(*i); - } - } - if (!hasC && n.hasOperator()) - { - hasC = hasClosure(n.getOperator()); - } - n.setAttribute(HasClosureAttr(), hasC); - n.setAttribute(HasClosureComputedAttr(), true); - return hasC; - } - return n.getAttribute(HasClosureAttr()); -} - -bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs, bool computeFv) -{ - std::unordered_set<TNode> scope; - return getFreeVariablesScope(n, fvs, scope, computeFv); -} - -bool getFreeVariablesScope(TNode n, - std::unordered_set<Node>& fvs, - std::unordered_set<TNode>& scope, - bool computeFv) +/** + * Check variables internal, which is used as a helper to implement many of the + * methods in this file. + * + * This computes the free variables in n, that is, the subterms of n of kind + * BOUND_VARIABLE that are not bound in n or occur in scope, adds these to fvs + * if computeFv is true. + * + * @param n The node under investigation + * @param fvs The set which free variables are added to + * @param scope The scope we are considering. + * @param wasShadow Flag set to true if variable shadowing was encountered. + * Only computed if checkShadow is true. + * @param computeFv If this flag is false, then we only return true/false and + * do not add to fvs. + * @param checkShadow If this flag is true, we immediately return true if a + * variable is shadowing. If this flag is false, we give an assertion failure + * when this occurs. + * @return true iff this node contains a free variable. + */ +bool checkVariablesInternal(TNode n, + std::unordered_set<Node>& fvs, + std::unordered_set<TNode>& scope, + bool& wasShadow, + bool computeFv = true, + bool checkShadow = false) { std::unordered_set<TNode> visited; std::vector<TNode> visit; @@ -376,13 +344,26 @@ bool getFreeVariablesScope(TNode n, // add to scope for (const TNode& cn : cur[0]) { - // should not shadow - Assert(scope.find(cn) == scope.end()) - << "Shadowed variable " << cn << " in " << cur << "\n"; + if (checkShadow) + { + if (scope.find(cn) != scope.end()) + { + wasShadow = true; + return true; + } + } + else + { + // should not shadow + Assert(scope.find(cn) == scope.end()) + << "Shadowed variable " << cn << " in " << cur << "\n"; + } scope.insert(cn); } // must make recursive call to use separate cache - if (getFreeVariablesScope(cur[1], fvs, scope, computeFv) && !computeFv) + if (checkVariablesInternal( + cur[1], fvs, scope, wasShadow, computeFv, checkShadow) + && !computeFv) { return true; } @@ -406,6 +387,95 @@ bool getFreeVariablesScope(TNode n, return !fvs.empty(); } +/** Same as above, without checking for shadowing */ +bool getVariablesInternal(TNode n, + std::unordered_set<Node>& fvs, + std::unordered_set<TNode>& scope, + bool computeFv = true) +{ + bool wasShadow = false; + return checkVariablesInternal(n, fvs, scope, wasShadow, computeFv, false); +} + +bool hasFreeVar(TNode n) +{ + // optimization for variables and constants + if (n.getNumChildren() == 0) + { + return n.getKind() == kind::BOUND_VARIABLE; + } + std::unordered_set<Node> fvs; + std::unordered_set<TNode> scope; + return getVariablesInternal(n, fvs, scope, false); +} + +bool hasFreeOrShadowedVar(TNode n, bool& wasShadow) +{ + // optimization for variables and constants + if (n.getNumChildren() == 0) + { + return n.getKind() == kind::BOUND_VARIABLE; + } + std::unordered_set<Node> fvs; + std::unordered_set<TNode> scope; + return checkVariablesInternal(n, fvs, scope, wasShadow, false, true); +} + +struct HasClosureTag +{ +}; +struct HasClosureComputedTag +{ +}; +/** Attribute true for expressions with closures in them */ +typedef expr::Attribute<HasClosureTag, bool> HasClosureAttr; +typedef expr::Attribute<HasClosureComputedTag, bool> HasClosureComputedAttr; + +bool hasClosure(Node n) +{ + if (!n.getAttribute(HasClosureComputedAttr())) + { + bool hasC = false; + if (n.isClosure()) + { + hasC = true; + } + else + { + for (auto i = n.begin(); i != n.end() && !hasC; ++i) + { + hasC = hasClosure(*i); + } + } + if (!hasC && n.hasOperator()) + { + hasC = hasClosure(n.getOperator()); + } + n.setAttribute(HasClosureAttr(), hasC); + n.setAttribute(HasClosureComputedAttr(), true); + return hasC; + } + return n.getAttribute(HasClosureAttr()); +} + +bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs) +{ + std::unordered_set<TNode> scope; + return getVariablesInternal(n, fvs, scope); +} + +bool getFreeVariablesScope(TNode n, + std::unordered_set<Node>& fvs, + std::unordered_set<TNode>& scope) +{ + return getVariablesInternal(n, fvs, scope); +} +bool hasFreeVariablesScope(TNode n, std::unordered_set<TNode>& scope) +{ + std::unordered_set<Node> fvs; + return getVariablesInternal(n, fvs, scope, false); +} + bool getVariables(TNode n, std::unordered_set<TNode>& vs) { std::unordered_set<TNode> visited; diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 72ea03176..c3ee4b604 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -85,6 +85,16 @@ bool hasBoundVar(TNode n); bool hasFreeVar(TNode n); /** + * Returns true iff the node n contains a free variable, that is, a node + * of kind BOUND_VARIABLE that is not bound in n, or a BOUND_VARIABLE that + * is shadowed (e.g. it is bound twice in the same context). + * @param n The node under investigation + * @param wasShadow Set to true if n had a shadowed variable. + * @return true iff this node contains a free or shadowed variable. + */ +bool hasFreeOrShadowedVar(TNode n, bool& wasShadow); + +/** * Returns true iff the node n contains a closure, that is, a node * whose kind is FORALL, EXISTS, WITNESS, LAMBDA, or any other closure currently * supported. @@ -98,27 +108,27 @@ bool hasClosure(Node n); * BOUND_VARIABLE that are not bound in n, adds these to fvs. * @param n The node under investigation * @param fvs The set which free variables are added to - * @param computeFv If this flag is false, then we only return true/false and - * do not add to fvs. * @return true iff this node contains a free variable. */ -bool getFreeVariables(TNode n, - std::unordered_set<Node>& fvs, - bool computeFv = true); +bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs); /** * Get the free variables in n, that is, the subterms of n of kind * BOUND_VARIABLE that are not bound in n or occur in scope, adds these to fvs. * @param n The node under investigation * @param fvs The set which free variables are added to * @param scope The scope we are considering. - * @param computeFv If this flag is false, then we only return true/false and - * do not add to fvs. * @return true iff this node contains a free variable. */ bool getFreeVariablesScope(TNode n, std::unordered_set<Node>& fvs, - std::unordered_set<TNode>& scope, - bool computeFv = true); + std::unordered_set<TNode>& scope); +/** + * Return true if n has any free variables in the given scope. + * @param n The node under investigation + * @param scope The scope we are considering. + * @return true iff this node contains a free variable. + */ +bool hasFreeVariablesScope(TNode n, std::unordered_set<TNode>& scope); /** * Get all variables in n. diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7add605c5..b4f39a315 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -145,9 +145,7 @@ void Smt2::addDatatypesOperators() } void Smt2::addStringOperators() { - defineVar( - "re.all", - getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpAllchar())); + defineVar("re.all", getSolver()->mkRegexpAll()); addOperator(api::STRING_CONCAT, "str.++"); addOperator(api::STRING_LENGTH, "str.len"); addOperator(api::STRING_SUBSTR, "str.substr"); @@ -594,7 +592,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) d_solver->mkUniverseSet(d_solver->getBooleanSort())); addOperator(api::SET_UNION, "set.union"); - addOperator(api::SET_INTERSECTION, "set.intersection"); + addOperator(api::SET_INTER, "set.inter"); addOperator(api::SET_MINUS, "set.minus"); addOperator(api::SET_SUBSET, "set.subset"); addOperator(api::SET_MEMBER, "set.member"); @@ -1011,13 +1009,32 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) // resulting rational here. This also is applied for integral real values // like 5.0 which are converted to (/ 5 1) to distinguish them from // integer constants. We must ensure numerator and denominator are - // constant and the denominator is non-zero. - if (constVal.getKind() == api::DIVISION) + // constant and the denominator is non-zero. A similar issue happens for + // negative integers and reals, with unary minus. + bool isNeg = false; + if (constVal.getKind() == api::UMINUS) + { + isNeg = true; + constVal = constVal[0]; + } + if (constVal.getKind() == api::DIVISION + && constVal[0].getKind() == api::CONST_RATIONAL + && constVal[1].getKind() == api::CONST_RATIONAL) { std::stringstream sdiv; - sdiv << constVal[0] << "/" << constVal[1]; + sdiv << (isNeg ? "-" : "") << constVal[0] << "/" << constVal[1]; constVal = d_solver->mkReal(sdiv.str()); } + else if (constVal.getKind() == api::CONST_RATIONAL && isNeg) + { + std::stringstream sneg; + sneg << "-" << constVal; + constVal = d_solver->mkInteger(sneg.str()); + } + else + { + constVal = args[0]; + } if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort())) { diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index b66ae5728..16b626e30 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -16,6 +16,7 @@ #include <string> +#include "expr/node_manager_attributes.h" #include "options/base_options.h" #include "options/language.h" #include "printer/ast/ast_printer.h" @@ -201,9 +202,8 @@ void Printer::toStreamCmdDeclareFunction(std::ostream& out, void Printer::toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const { - std::stringstream vs; - vs << v; - toStreamCmdDeclareFunction(out, vs.str(), v.getType()); + std::string vs = v.getAttribute(expr::VarNameAttr()); + toStreamCmdDeclareFunction(out, vs, v.getType()); } void Printer::toStreamCmdDeclarePool(std::ostream& out, diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5d4387658..8ed4929e5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1061,7 +1061,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) // set theory case kind::SET_UNION: return "set.union"; - case kind::SET_INTERSECTION: return "set.intersection"; + case kind::SET_INTER: return "set.inter"; case kind::SET_MINUS: return "set.minus"; case kind::SET_SUBSET: return "set.subset"; case kind::SET_MEMBER: return "set.member"; diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index b984119ae..5caf565c0 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -1365,6 +1365,117 @@ bool AletheProofPostprocessCallback::update(Node res, {}, *cdp); } + //================================================= Quantifiers rules + // ======== Instantiate + // See proof_rule.h for documentation on the INSTANTIATE rule. This + // comment uses variable names as introduced there. + // + // ----- FORALL_INST, (= x1 t1) ... (= xn tn) + // VP1 + // ----- OR + // VP2 P + // -------------------- RESOLUTION + // (cl F*sigma)^ + // + // VP1: (cl (or (not (forall ((x1 T1) ... (xn Tn)) F*sigma) + // VP2: (cl (not (forall ((x1 T1) ... (xn Tn)) F)) F*sigma) + // + // ^ the corresponding proof node is F*sigma + case PfRule::INSTANTIATE: + { + for (size_t i = 0, size = children[0][0].getNumChildren(); i < size; i++) + { + new_args.push_back(children[0][0][i].eqNode(args[i])); + } + Node vp1 = nm->mkNode( + kind::SEXPR, d_cl, nm->mkNode(kind::OR, children[0].notNode(), res)); + Node vp2 = nm->mkNode(kind::SEXPR, d_cl, children[0].notNode(), res); + return addAletheStep( + AletheRule::FORALL_INST, vp1, vp1, {}, new_args, *cdp) + && addAletheStep(AletheRule::OR, vp2, vp2, {vp1}, {}, *cdp) + && addAletheStep(AletheRule::RESOLUTION, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + {vp2, children[0]}, + {}, + *cdp); + } + //================================================= Arithmetic rules + // ======== Adding Inequalities + // + // ----- LIA_GENERIC + // VP1 P1 ... Pn + // ------------------------------- RESOLUTION + // (cl (>< t1 t2))* + // + // VP1: (cl (not l1) ... (not ln) (>< t1 t2)) + // + // * the corresponding proof node is (>< t1 t2) + case PfRule::MACRO_ARITH_SCALE_SUM_UB: + { + std::vector<Node> vp1s{d_cl}; + for (const Node& child : children) + { + vp1s.push_back(child.notNode()); + } + vp1s.push_back(res); + Node vp1 = nm->mkNode(kind::SEXPR, vp1s); + std::vector<Node> new_children = {vp1}; + new_children.insert(new_children.end(), children.begin(), children.end()); + return addAletheStep(AletheRule::LIA_GENERIC, vp1, vp1, {}, args, *cdp) + && addAletheStep(AletheRule::RESOLUTION, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + new_children, + {}, + *cdp); + } + // ======== Tightening Strict Integer Upper Bounds + // + // ----- LA_GENERIC, 1 + // VP1 P + // ------------------------------------- RESOLUTION + // (cl (<= i greatestIntLessThan(c)))* + // + // VP1: (cl (not (< i c)) (<= i greatestIntLessThan(c))) + // + // * the corresponding proof node is (<= i greatestIntLessThan(c)) + case PfRule::INT_TIGHT_UB: + { + Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res); + std::vector<Node> new_children = {vp1, children[0]}; + new_args.push_back(nm->mkConst<Rational>(1)); + return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp) + && addAletheStep(AletheRule::RESOLUTION, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + new_children, + {}, + *cdp); + } + // ======== Tightening Strict Integer Lower Bounds + // + // ----- LA_GENERIC, 1 + // VP1 P + // ------------------------------------- RESOLUTION + // (cl (>= i leastIntGreaterThan(c)))* + // + // VP1: (cl (not (> i c)) (>= i leastIntGreaterThan(c))) + // + // * the corresponding proof node is (>= i leastIntGreaterThan(c)) + case PfRule::INT_TIGHT_LB: + { + Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res); + std::vector<Node> new_children = {vp1, children[0]}; + new_args.push_back(nm->mkConst<Rational>(1)); + return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp) + && addAletheStep(AletheRule::RESOLUTION, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + new_children, + {}, + *cdp); + } default: { return addAletheStep(AletheRule::UNDEFINED, diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 9c24dd690..8d066c1ba 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -190,16 +190,19 @@ void Assertions::addFormula(TNode n, // Ensure that it does not contain free variables if (maybeHasFv) { - if (expr::hasFreeVar(n)) + bool wasShadow = false; + if (expr::hasFreeOrShadowedVar(n, wasShadow)) { + std::string varType(wasShadow ? "shadowed" : "free"); std::stringstream se; if (isFunDef) { - se << "Cannot process function definition with free variable."; + se << "Cannot process function definition with " << varType + << " variable."; } else { - se << "Cannot process assertion with free variable."; + se << "Cannot process assertion with " << varType << " variable."; if (language::isLangSygus(options().base.inputLanguage)) { // Common misuse of SyGuS is to use top-level assert instead of diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index edf4e2761..341893a70 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -342,48 +342,6 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node, } } } - else if (node.getKind() == kind::LAMBDA) - { - // if a lambda, do lambda-lifting - if (!expr::hasFreeVar(node)) - { - skolem = getSkolemForNode(node); - if (skolem.isNull()) - { - Trace("rtf-proof-debug") - << "RemoveTermFormulas::run: make LAMBDA skolem" << std::endl; - // Make the skolem to represent the lambda - SkolemManager* sm = nodeManager->getSkolemManager(); - skolem = sm->mkPurifySkolem( - node, - "lambdaF", - "a function introduced due to term-level lambda removal"); - d_skolem_cache.insert(node, skolem); - - // The new assertion - std::vector<Node> children; - // bound variable list - children.push_back(node[0]); - // body - std::vector<Node> skolem_app_c; - skolem_app_c.push_back(skolem); - skolem_app_c.insert(skolem_app_c.end(), node[0].begin(), node[0].end()); - Node skolem_app = nodeManager->mkNode(kind::APPLY_UF, skolem_app_c); - children.push_back(skolem_app.eqNode(node[1])); - // axiom defining skolem - newAssertion = nodeManager->mkNode(kind::FORALL, children); - - // Lambda lifting is trivial to justify, hence we don't set a proof - // generator here. In particular, replacing the skolem introduced - // here with its original lambda ensures the new assertion rewrites - // to true. - // For example, if (lambda y. t[y]) has skolem k, then this lemma is: - // forall x. k(x)=t[x] - // whose witness form rewrites - // forall x. (lambda y. t[y])(x)=t[x] --> forall x. t[x]=t[x] --> true - } - } - } else if (node.getKind() == kind::WITNESS) { // If a witness choice diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 9c067caf6..c65f5ccc2 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -58,41 +58,24 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e) Assert(n.getKind() == MK_BAG); Assert(e.getType() == n.getType().getBagElementType()); + /* + * (ite (and (= e x) (>= c 1)) + * (= (bag.count e skolem) c) + * (= (bag.count e skolem) 0)) + */ Node x = n[0]; Node c = n[1]; + InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG); + Node same = d_nm->mkNode(EQUAL, e, x); Node geq = d_nm->mkNode(GEQ, c, d_one); - if (d_state->areEqual(e, x)) - { - // (= (bag.count e skolem) (ite (>= c 1) c 0))) - InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG_SAME_ELEMENT); - Node skolem = getSkolem(n, inferInfo); - Node count = getMultiplicityTerm(e, skolem); - Node ite = d_nm->mkNode(ITE, geq, c, d_zero); - inferInfo.d_conclusion = count.eqNode(ite); - return inferInfo; - } - if (d_state->areDisequal(e, x)) - { - //(= (bag.count e skolem) 0)) - InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG_SAME_ELEMENT); - Node skolem = getSkolem(n, inferInfo); - Node count = getMultiplicityTerm(e, skolem); - inferInfo.d_conclusion = count.eqNode(d_zero); - return inferInfo; - } - else - { - // (= (bag.count e skolem) (ite (and (= e x) (>= c 1)) c 0))) - InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG); - Node skolem = getSkolem(n, inferInfo); - Node count = getMultiplicityTerm(e, skolem); - Node same = d_nm->mkNode(EQUAL, e, x); - Node andNode = same.andNode(geq); - Node ite = d_nm->mkNode(ITE, andNode, c, d_zero); - Node equal = count.eqNode(ite); - inferInfo.d_conclusion = equal; - return inferInfo; - } + Node andNode = same.andNode(geq); + Node skolem = getSkolem(n, inferInfo); + Node count = getMultiplicityTerm(e, skolem); + Node equalC = d_nm->mkNode(EQUAL, count, c); + Node equalZero = d_nm->mkNode(EQUAL, count, d_zero); + Node ite = d_nm->mkNode(ITE, andNode, equalC, equalZero); + inferInfo.d_conclusion = ite; + return inferInfo; } /** diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index 3f38d05b9..391a352bd 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -50,13 +50,10 @@ class InferenceGenerator /** * @param n is (bag x c) of type (Bag E) * @param e is a node of type E - * @return an inference that represents the following cases: - * 1- e, x are in the same equivalent class, then we infer: - * (= (bag.count e skolem) (ite (>= c 1) c 0))) - * 2- e, x are known to be disequal, then we infer: - * (= (bag.count e skolem) 0)) - * 3- if neither holds, we infer: - * (= (bag.count e skolem) (ite (and (= e x) (>= c 1)) c 0))) + * @return an inference that represents the following lemma: + * (ite (and (= e x) (>= c 1)) + * (= (bag.count e skolem) c) + * (= (bag.count e skolem) 0)) * where skolem = (bag x c) is a fresh variable */ InferInfo mkBag(Node n, Node e); diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 9b5f1a581..4747aeaf2 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -106,8 +106,6 @@ const char* toString(InferenceId i) case InferenceId::ARRAYS_EQ_TAUTOLOGY: return "ARRAYS_EQ_TAUTOLOGY"; case InferenceId::BAGS_NON_NEGATIVE_COUNT: return "BAGS_NON_NEGATIVE_COUNT"; - case InferenceId::BAGS_MK_BAG_DIFFERENT_ELEMENT: return "BAGS_MK_BAG_DIFFERENT_ELEMENT"; - case InferenceId::BAGS_MK_BAG_SAME_ELEMENT: return "BAGS_MK_BAG_SAME_ELEMENT"; case InferenceId::BAGS_MK_BAG: return "BAGS_MK_BAG"; case InferenceId::BAGS_EQUALITY: return "BAGS_EQUALITY"; case InferenceId::BAGS_DISEQUALITY: return "BAGS_DISEQUALITY"; @@ -455,6 +453,8 @@ const char* toString(InferenceId i) case InferenceId::UF_HO_MODEL_APP_ENCODE: return "UF_HO_MODEL_APP_ENCODE"; case InferenceId::UF_HO_MODEL_EXTENSIONALITY: return "UF_HO_MODEL_EXTENSIONALITY"; + case InferenceId::UF_HO_LAMBDA_UNIV_EQ: return "HO_LAMBDA_UNIV_EQ"; + case InferenceId::UF_HO_LAMBDA_APP_REDUCE: return "HO_LAMBDA_APP_REDUCE"; default: return "?"; } diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index cebf02c9d..a13bc4d1b 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -169,8 +169,6 @@ enum class InferenceId // ---------------------------------- bags theory BAGS_NON_NEGATIVE_COUNT, - BAGS_MK_BAG_DIFFERENT_ELEMENT, - BAGS_MK_BAG_SAME_ELEMENT, BAGS_MK_BAG, BAGS_EQUALITY, BAGS_DISEQUALITY, @@ -840,6 +838,15 @@ enum class InferenceId // different applications // (not (= (f sk1 .. skn) (g sk1 .. skn)) UF_HO_MODEL_EXTENSIONALITY, + // equivalence of lambda functions + // f = g => forall x. reduce(lambda(f)(x)) = reduce(lambda(g)(x)) + // This is applied when lamda functions f and g are in the same eq class. + UF_HO_LAMBDA_UNIV_EQ, + // equivalence of a lambda function and an ordinary function + // f = h => h(t) = reduce(lambda(f)(t)) + // This is applied when lamda function f and ordinary function h are in the + // same eq class. + UF_HO_LAMBDA_APP_REDUCE, //-------------------- end model-construction specific part //-------------------- end HO extension to UF //-------------------------------------- end uf theory diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp index 75a353dbe..24efc60c3 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.cpp +++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp @@ -54,7 +54,7 @@ bool TriggerTermInfo::isAtomicTriggerKind(Kind k) // where these two things require those kinds respectively. return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR || k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL - || k == APPLY_TESTER || k == SET_UNION || k == SET_INTERSECTION + || k == APPLY_TESTER || k == SET_UNION || k == SET_INTER || k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER || k == SET_SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT || k == INT_TO_BITVECTOR || k == HO_APPLY || k == STRING_LENGTH diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index b8981c13d..cca1d76e2 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -991,7 +991,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( sdts[i].addConstructor(lambda, "singleton", cargsSingleton); // add for union, difference, intersection - std::vector<Kind> bin_kinds = {SET_UNION, SET_INTERSECTION, SET_MINUS}; + std::vector<Kind> bin_kinds = {SET_UNION, SET_INTER, SET_MINUS}; std::vector<TypeNode> cargsBinary; cargsBinary.push_back(unres_t); cargsBinary.push_back(unres_t); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5c9e91d32..0408d27da 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -186,7 +186,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) Node TermDb::getMatchOperator( Node n ) { Kind k = n.getKind(); //datatype operators may be parametric, always assume they are - if (k == SELECT || k == STORE || k == SET_UNION || k == SET_INTERSECTION + if (k == SELECT || k == STORE || k == SET_UNION || k == SET_INTER || k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER || k == SET_SINGLETON || k == APPLY_SELECTOR_TOTAL || k == APPLY_SELECTOR || k == APPLY_TESTER || k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 8e76c0a3a..cb8bad174 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -283,7 +283,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry) { if (reqNAry) { - if (k == SET_UNION || k == SET_INTERSECTION) + if (k == SET_UNION || k == SET_INTER) { return false; } @@ -292,7 +292,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry) || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT - || k == SET_UNION || k == SET_INTERSECTION || k == RELATION_JOIN + || k == SET_UNION || k == SET_INTER || k == RELATION_JOIN || k == RELATION_PRODUCT || k == SEP_STAR; } @@ -300,7 +300,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry) { if (reqNAry) { - if (k == SET_UNION || k == SET_INTERSECTION) + if (k == SET_UNION || k == SET_INTER) { return false; } @@ -308,7 +308,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry) return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR - || k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTERSECTION + || k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTER || k == SEP_STAR; } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 218c09804..3ee4fa012 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -385,7 +385,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) { for (size_t j = (i + 1); j < lsize; j++) { - Node s = nm->mkNode(SET_INTERSECTION, labels[i], labels[j]); + Node s = nm->mkNode(SET_INTER, labels[i], labels[j]); Node ilem = s.eqNode(empSet); Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, disjoint : " << ilem @@ -401,7 +401,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, union : " << ulem << std::endl; c_lems.push_back(ulem); - Node s = nm->mkNode(SET_INTERSECTION, slbl, labels[0]); + Node s = nm->mkNode(SET_INTER, slbl, labels[0]); Node ilem = s.eqNode(empSet); Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, disjoint : " << ilem << std::endl; @@ -1427,10 +1427,9 @@ Node TheorySep::instantiateLabel(Node n, Node sub_lbl = itl->second; Node lbl_mval = d_label_model[sub_lbl].getValue( rtn ); for( unsigned j=0; j<vs.size(); j++ ){ - bchildren.push_back( - NodeManager::currentNM() - ->mkNode(kind::SET_INTERSECTION, lbl_mval, vs[j]) - .eqNode(empSet)); + bchildren.push_back(NodeManager::currentNM() + ->mkNode(kind::SET_INTER, lbl_mval, vs[j]) + .eqNode(empSet)); } vs.push_back( lbl_mval ); if( vsu.isNull() ){ @@ -1476,11 +1475,10 @@ Node TheorySep::instantiateLabel(Node n, //disjoint constraints Node sub_lbl_0 = d_label_map[n][lbl][0]; Node lbl_mval_0 = d_label_model[sub_lbl_0].getValue( rtn ); - wchildren.push_back( - NodeManager::currentNM() - ->mkNode(kind::SET_INTERSECTION, lbl_mval_0, lbl) - .eqNode(empSet) - .negate()); + wchildren.push_back(NodeManager::currentNM() + ->mkNode(kind::SET_INTER, lbl_mval_0, lbl) + .eqNode(empSet) + .negate()); //return the lemma wchildren.push_back( children[0].negate() ); diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 57b49570d..e2181b4c6 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -243,7 +243,7 @@ void CardinalityExtension::checkRegister() // if setminus, do for intersection instead if (n.getKind() == SET_MINUS) { - n = rewrite(nm->mkNode(SET_INTERSECTION, n[0], n[1])); + n = rewrite(nm->mkNode(SET_INTER, n[0], n[1])); } registerCardinalityTerm(n); } @@ -269,7 +269,7 @@ void CardinalityExtension::registerCardinalityTerm(Node n) NodeManager* nm = NodeManager::currentNM(); Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl; std::vector<Node> cterms; - if (n.getKind() == SET_INTERSECTION) + if (n.getKind() == SET_INTER) { for (unsigned e = 0; e < 2; e++) { @@ -382,7 +382,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, for (const Node& n : nvsets) { Kind nk = n.getKind(); - if (nk != SET_INTERSECTION && nk != SET_MINUS) + if (nk != SET_INTER && nk != SET_MINUS) { continue; } @@ -390,7 +390,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, << std::endl; std::vector<Node> sib; unsigned true_sib = 0; - if (n.getKind() == SET_INTERSECTION) + if (n.getKind() == SET_INTER) { d_localBase[n] = n; for (unsigned e = 0; e < 2; e++) @@ -402,7 +402,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, } else { - Node si = rewrite(nm->mkNode(SET_INTERSECTION, n[0], n[1])); + Node si = rewrite(nm->mkNode(SET_INTER, n[0], n[1])); sib.push_back(si); d_localBase[n] = si; Node osm = rewrite(nm->mkNode(SET_MINUS, n[1], n[0])); @@ -491,7 +491,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, << "Sibling " << sib[si] << " is already empty." << std::endl; } } - if (!is_union && nk == SET_INTERSECTION && !u.isNull()) + if (!is_union && nk == SET_INTER && !u.isNull()) { // union is equal to other parent if (!d_state.areEqual(u, n[1 - e])) @@ -579,7 +579,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, << " are equal, ids = " << card_parent_ids[l] << " " << card_parent_ids[k] << std::endl; dup = true; - if (n.getKind() != SET_INTERSECTION) + if (n.getKind() != SET_INTER) { continue; } @@ -818,7 +818,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, Node r1 = e == 0 ? o0 : o1; Node r2 = e == 0 ? o1 : o0; // check if their intersection exists modulo equality - Node r1r2i = d_state.getBinaryOpTerm(SET_INTERSECTION, r1, r2); + Node r1r2i = d_state.getBinaryOpTerm(SET_INTER, r1, r2); if (!r1r2i.isNull()) { Trace("sets-nf-debug") @@ -839,7 +839,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, Assert(o0 != o1); Node kca = d_treg.getProxy(o0); Node kcb = d_treg.getProxy(o1); - Node intro = rewrite(nm->mkNode(SET_INTERSECTION, kca, kcb)); + Node intro = rewrite(nm->mkNode(SET_INTER, kca, kcb)); Trace("sets-nf") << " Intro split : " << o0 << " against " << o1 << ", term is " << intro << std::endl; intro_sets.push_back(intro); diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index f5ed7cd87..71d5fce4a 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -37,7 +37,7 @@ enumerator SET_TYPE \ # operators operator SET_UNION 2 "set union" -operator SET_INTERSECTION 2 "set intersection" +operator SET_INTER 2 "set intersection" operator SET_MINUS 2 "set subtraction" operator SET_SUBSET 2 "subset predicate; first parameter a subset of second" operator SET_MEMBER 2 "set membership predicate; first parameter a member of second" @@ -88,7 +88,7 @@ operator RELATION_JOIN_IMAGE 2 "relation join image" operator RELATION_IDEN 1 "relation identity" typerule SET_UNION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule -typerule SET_INTERSECTION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule +typerule SET_INTER ::cvc5::theory::sets::SetsBinaryOperatorTypeRule typerule SET_MINUS ::cvc5::theory::sets::SetsBinaryOperatorTypeRule typerule SET_SUBSET ::cvc5::theory::sets::SubsetTypeRule typerule SET_MEMBER ::cvc5::theory::sets::MemberTypeRule diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 023a8a6af..3f619dcad 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -90,7 +90,7 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n) } } } - else if (nk == SET_SINGLETON || nk == SET_UNION || nk == SET_INTERSECTION + else if (nk == SET_SINGLETON || nk == SET_UNION || nk == SET_INTER || nk == SET_MINUS || nk == SET_EMPTY || nk == SET_UNIVERSE) { if (nk == SET_SINGLETON) diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp index 41fe0b4c8..d4b5aa824 100644 --- a/src/theory/sets/term_registry.cpp +++ b/src/theory/sets/term_registry.cpp @@ -44,7 +44,7 @@ TermRegistry::TermRegistry(Env& env, Node TermRegistry::getProxy(Node n) { Kind nk = n.getKind(); - if (nk != SET_EMPTY && nk != SET_SINGLETON && nk != SET_INTERSECTION + if (nk != SET_EMPTY && nk != SET_SINGLETON && nk != SET_INTER && nk != SET_MINUS && nk != SET_UNION && nk != SET_UNIVERSE) { return n; diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index b2eb80f75..c3d0b9bbe 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -76,7 +76,7 @@ void TheorySets::finishInit() // functions we are doing congruence over d_equalityEngine->addFunctionKind(SET_SINGLETON); d_equalityEngine->addFunctionKind(SET_UNION); - d_equalityEngine->addFunctionKind(SET_INTERSECTION); + d_equalityEngine->addFunctionKind(SET_INTER); d_equalityEngine->addFunctionKind(SET_MINUS); d_equalityEngine->addFunctionKind(SET_MEMBER); d_equalityEngine->addFunctionKind(SET_SUBSET); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 407352d94..f06580292 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -523,7 +523,7 @@ void TheorySetsPrivate::checkUpwardsClosure() // see if there are members in second argument const std::map<Node, Node>& r2mem = d_state.getMembers(r2); const std::map<Node, Node>& r2nmem = d_state.getNegativeMembers(r2); - if (!r2mem.empty() || k != kind::SET_INTERSECTION) + if (!r2mem.empty() || k != kind::SET_INTER) { Trace("sets-debug") << "Checking " << term << ", members = " << (!r1mem.empty()) @@ -546,7 +546,7 @@ void TheorySetsPrivate::checkUpwardsClosure() { valid = true; } - else if (k == kind::SET_INTERSECTION) + else if (k == kind::SET_INTER) { // conclude x is in term // if also existing in members of r2 diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 3ae937f3b..d63368f19 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -81,7 +81,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { nm->mkNode(kind::EQUAL, node[0], node[1][0])); } else if (node[1].getKind() == kind::SET_UNION - || node[1].getKind() == kind::SET_INTERSECTION + || node[1].getKind() == kind::SET_INTER || node[1].getKind() == kind::SET_MINUS) { std::vector<Node> children; @@ -157,7 +157,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { else if (node[1].getKind() == kind::SET_MINUS && node[1][0] == node[0]) { // (setminus A (setminus A B)) = (intersection A B) - Node intersection = nm->mkNode(SET_INTERSECTION, node[0], node[1][1]); + Node intersection = nm->mkNode(SET_INTER, node[0], node[1][1]); return RewriteResponse(REWRITE_AGAIN, intersection); } else if (node[1].getKind() == kind::SET_UNIVERSE) @@ -185,7 +185,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { break; } // kind::SET_MINUS - case kind::SET_INTERSECTION: + case kind::SET_INTER: { if(node[0] == node[1]) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; @@ -291,7 +291,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager::currentNM()->mkNode( kind::SET_CARD, NodeManager::currentNM()->mkNode( - kind::SET_INTERSECTION, node[0][0], node[0][1]))); + kind::SET_INTER, node[0][0], node[0][1]))); return RewriteResponse(REWRITE_DONE, ret ); } else if (node[0].getKind() == kind::SET_MINUS) @@ -302,7 +302,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager::currentNM()->mkNode( kind::SET_CARD, NodeManager::currentNM()->mkNode( - kind::SET_INTERSECTION, node[0][0], node[0][1]))); + kind::SET_INTER, node[0][0], node[0][1]))); return RewriteResponse(REWRITE_DONE, ret ); } break; diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp index 0793f011b..6602e7d03 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -30,7 +30,7 @@ TypeNode SetsBinaryOperatorTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::SET_UNION || n.getKind() == kind::SET_INTERSECTION + Assert(n.getKind() == kind::SET_UNION || n.getKind() == kind::SET_INTER || n.getKind() == kind::SET_MINUS); TypeNode setType = n[0].getType(check); if (check) @@ -57,7 +57,7 @@ bool SetsBinaryOperatorTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) { // only SET_UNION has a const rule in kinds. - // SET_INTERSECTION and SET_MINUS are not used in the canonical representation + // SET_INTER and SET_MINUS are not used in the canonical representation // of sets and therefore they do not have const rules in kinds Assert(n.getKind() == kind::SET_UNION); return NormalForm::checkNormalConstant(n); diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp index 1ff2e2da8..65ff4cde4 100644 --- a/src/theory/strings/array_solver.cpp +++ b/src/theory/strings/array_solver.cpp @@ -15,8 +15,10 @@ #include "theory/strings/array_solver.h" +#include "expr/sequence.h" #include "theory/strings/arith_entail.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/strings/word.h" #include "util/rational.h" using namespace cvc5::context; @@ -81,6 +83,7 @@ void ArraySolver::checkTerms(Kind k) Node r = d_state.getRepresentative(t[0]); NormalForm& nf = d_csolver.getNormalForm(r); Trace("seq-array-debug") << "...normal form " << nf.d_nf << std::endl; + std::vector<Node> nfChildren; if (nf.d_nf.empty()) { // updates should have been reduced (UPD_EMPTYSTR) @@ -92,8 +95,16 @@ void ArraySolver::checkTerms(Kind k) { Trace("seq-array-debug") << "...norm form size 1" << std::endl; // NOTE: could split on n=0 if needed, do not introduce ITE - if (nf.d_nf[0].getKind() == SEQ_UNIT) + Kind ck = nf.d_nf[0].getKind(); + // Note that (seq.unit c) is rewritten to CONST_SEQUENCE{c}, hence we + // check two cases here. It is important for completeness of this schema + // to handle this differently from STRINGS_ARRAY_UPDATE_CONCAT / + // STRINGS_ARRAY_NTH_CONCAT. Otherwise we would conclude a trivial + // equality when update/nth is applied to a constant of length one. + if (ck == SEQ_UNIT + || (ck == CONST_SEQUENCE && Word::getLength(nf.d_nf[0]) == 1)) { + Trace("seq-array-debug") << "...unit case" << std::endl; // do we know whether n = 0 ? // x = (seq.unit m) => (seq.update x n z) = ite(n=0, z, (seq.unit m)) // x = (seq.unit m) => (seq.nth x n) = ite(n=0, m, Uf(x, n)) @@ -109,7 +120,15 @@ void ArraySolver::checkTerms(Kind k) else { Assert(k == SEQ_NTH); - thenBranch = nf.d_nf[0][0]; + if (ck == CONST_SEQUENCE) + { + const Sequence& seq = nf.d_nf[0].getConst<Sequence>(); + thenBranch = seq.getVec()[0]; + } + else + { + thenBranch = nf.d_nf[0][0]; + } Node uf = SkolemCache::mkSkolemSeqNth(t[0].getType(), "Uf"); elseBranch = nm->mkNode(APPLY_UF, uf, t[0], t[1]); iid = InferenceId::STRINGS_ARRAY_NTH_UNIT; @@ -126,17 +145,33 @@ void ArraySolver::checkTerms(Kind k) d_eqProc.insert(eq); d_im.sendInference(exp, eq, iid); } + continue; } - // otherwise, the equivalence class is pure wrt concatenation - d_currTerms[k].push_back(t); - continue; + else if (ck != CONST_SEQUENCE) + { + // otherwise, if the normal form is not a constant sequence, the + // equivalence class is pure wrt concatenation. + d_currTerms[k].push_back(t); + continue; + } + // if the normal form is a constant sequence, it is treated as a + // concatenation. We split per character and case split on whether the + // nth/update falls on each character below, which must have a size + // greater than one. + std::vector<Node> chars = Word::getChars(nf.d_nf[0]); + Assert (chars.size()>1); + nfChildren.insert(nfChildren.end(), chars.begin(), chars.end()); + } + else + { + nfChildren.insert(nfChildren.end(), nf.d_nf.begin(), nf.d_nf.end()); } // otherwise, we are the concatenation of the components // NOTE: for nth, split on index vs component lengths, do not introduce ITE std::vector<Node> cond; std::vector<Node> cchildren; std::vector<Node> lacc; - for (const Node& c : nf.d_nf) + for (const Node& c : nfChildren) { Trace("seq-array-debug") << "...process " << c << std::endl; Node clen = nm->mkNode(STRING_LENGTH, c); @@ -146,26 +181,49 @@ void ArraySolver::checkTerms(Kind k) Node currSum = lacc.size() == 1 ? lacc[0] : nm->mkNode(PLUS, lacc); currIndex = nm->mkNode(MINUS, currIndex, currSum); } - if (k == STRING_UPDATE) + Node cc; + // If it is a constant of length one, then the update/nth is determined + // in this interval. Notice this is done here as + // an optimization to short cut introducing terms like + // (seq.nth (seq.unit c) i), which by construction is only relevant in + // the context where i = 0, hence we replace by c here. + if (c.getKind() == CONST_SEQUENCE) { - Node cc = nm->mkNode(STRING_UPDATE, c, currIndex, t[2]); - Trace("seq-array-debug") << "......component " << cc << std::endl; - cchildren.push_back(cc); + const Sequence& seq = c.getConst<Sequence>(); + if (seq.size() == 1) + { + if (k == STRING_UPDATE) + { + cc = nm->mkNode(ITE, t[1].eqNode(d_zero), t[2], c); + } + else + { + cc = seq.getVec()[0]; + } + } } - else + // if we did not process as a constant of length one + if (cc.isNull()) { - Assert(k == SEQ_NTH); - Node cc = nm->mkNode(SEQ_NTH, c, currIndex); - Trace("seq-array-debug") << "......component " << cc << std::endl; - cchildren.push_back(cc); + if (k == STRING_UPDATE) + { + cc = nm->mkNode(STRING_UPDATE, c, currIndex, t[2]); + } + else + { + Assert(k == SEQ_NTH); + cc = nm->mkNode(SEQ_NTH, c, currIndex); + } } + Trace("seq-array-debug") << "......component " << cc << std::endl; + cchildren.push_back(cc); lacc.push_back(clen); if (k == SEQ_NTH) { Node currSumPost = lacc.size() == 1 ? lacc[0] : nm->mkNode(PLUS, lacc); - Node cc = nm->mkNode(LT, t[1], currSumPost); - Trace("seq-array-debug") << "......condition " << cc << std::endl; - cond.push_back(cc); + Node cf = nm->mkNode(LT, t[1], currSumPost); + Trace("seq-array-debug") << "......condition " << cf << std::endl; + cond.push_back(cf); } } // z = (seq.++ x y) => diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 96029eab8..aec223d66 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -19,6 +19,7 @@ #include "expr/skolem_manager.h" #include "options/uf_options.h" #include "theory/theory_model.h" +#include "theory/uf/lambda_lift.h" #include "theory/uf/theory_uf_rewriter.h" using namespace std; @@ -30,31 +31,83 @@ namespace uf { HoExtension::HoExtension(Env& env, TheoryState& state, - TheoryInferenceManager& im) + TheoryInferenceManager& im, + LambdaLift& ll) : EnvObj(env), d_state(state), d_im(im), + d_ll(ll), d_extensionality(userContext()), + d_cachedLemmas(userContext()), d_uf_std_skolem(userContext()) { d_true = NodeManager::currentNM()->mkConst(true); } -Node HoExtension::ppRewrite(Node node) +TrustNode HoExtension::ppRewrite(Node node, std::vector<SkolemLemma>& lems) { - // convert HO_APPLY to APPLY_UF if fully applied - if (node.getKind() == HO_APPLY) + Kind k = node.getKind(); + if (k == HO_APPLY) { + // convert HO_APPLY to APPLY_UF if fully applied if (node[0].getType().getNumChildren() == 2) { Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; Node ret = getApplyUfForHoApply(node); Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret << std::endl; - return ret; + return TrustNode::mkTrustRewrite(node, ret); } + // partial beta reduction + // f ---> (lambda ((x Int) (y Int)) s[x, y]) then (@ f t) is preprocessed + // to (lambda ((y Int)) s[t, y]). + if (options().uf.ufHoLazyLambdaLift) + { + Node op = node[0]; + Node opl = d_ll.getLambdaFor(op); + if (!opl.isNull()) + { + NodeManager* nm = NodeManager::currentNM(); + Node app = nm->mkNode(HO_APPLY, opl, node[1]); + app = rewrite(app); + Trace("uf-lazy-ll") + << "Partial beta reduce: " << node << " -> " << app << std::endl; + return TrustNode::mkTrustRewrite(node, app, nullptr); + } + } + } + else if (k == APPLY_UF) + { + // Say (lambda ((x Int)) t[x]) occurs in the input. We replace this + // by k during ppRewrite. In the following, if we see (k s), we replace + // it by t[s]. This maintains the invariant that the *only* occurences + // of k are as arguments to other functions; k is not applied + // in any preprocessed constraints. + if (options().uf.ufHoLazyLambdaLift) + { + // if an application of the lambda lifted function, do beta reduction + // immediately + Node op = node.getOperator(); + Node opl = d_ll.getLambdaFor(op); + if (!opl.isNull()) + { + Assert(opl.getKind() == LAMBDA); + std::vector<Node> args(node.begin(), node.end()); + Node app = d_ll.betaReduce(opl, args); + Trace("uf-lazy-ll") + << "Beta reduce: " << node << " -> " << app << std::endl; + return TrustNode::mkTrustRewrite(node, app, nullptr); + } + } + } + else if (k == kind::LAMBDA) + { + Trace("uf-lazy-ll") << "Preprocess lambda: " << node << std::endl; + TrustNode skTrn = d_ll.ppRewrite(node, lems); + Trace("uf-lazy-ll") << "...return " << skTrn.getNode() << std::endl; + return skTrn; } - return node; + return TrustNode::null(); } Node HoExtension::getExtensionalityDeq(TNode deq, bool isCached) @@ -217,7 +270,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) { Node eqc = (*eqcs_i); TypeNode tn = eqc.getType(); - if (tn.isFunction()) + if (tn.isFunction() && d_lambdaEqc.find(eqc) == d_lambdaEqc.end()) { hasFunctions = true; // if during collect model, must have an infinite type @@ -413,6 +466,168 @@ unsigned HoExtension::checkAppCompletion() return 0; } +unsigned HoExtension::checkLazyLambda() +{ + if (!options().uf.ufHoLazyLambdaLift) + { + // no lambdas are lazily lifted + return 0; + } + Trace("uf-ho") << "HoExtension::checkLazyLambda..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); + unsigned numLemmas = 0; + d_lambdaEqc.clear(); + eq::EqualityEngine* ee = d_state.getEqualityEngine(); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); + // normal functions equated to lambda functions + std::unordered_set<Node> normalEqFuns; + // mapping from functions to terms + while (!eqcs_i.isFinished()) + { + Node eqc = (*eqcs_i); + ++eqcs_i; + if (!eqc.getType().isFunction()) + { + continue; + } + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); + Node lamRep; // the first lambda function we encounter in the equivalence + // class + Node lamRepLam; + std::unordered_set<Node> normalEqFunWait; + while (!eqc_i.isFinished()) + { + Node n = *eqc_i; + ++eqc_i; + Node lam = d_ll.getLambdaFor(n); + if (lam.isNull()) + { + if (!lamRep.isNull()) + { + // if we are equal to a lambda function, we must beta-reduce + // applications of this + normalEqFuns.insert(n); + } + else + { + // waiting to see if there is a lambda function in this equivalence + // class + normalEqFunWait.insert(n); + } + } + else if (lamRep.isNull()) + { + // there is a lambda function in this equivalence class + lamRep = n; + lamRepLam = lam; + // must consider all normal functions we've seen so far + normalEqFuns.insert(normalEqFunWait.begin(), normalEqFunWait.end()); + normalEqFunWait.clear(); + } + else + { + // two lambda functions are in same equivalence class + Node f = lamRep < n ? lamRep : n; + Node g = lamRep < n ? n : lamRep; + Trace("uf-ho-debug") << " found equivalent lambda functions " << f + << " and " << g << std::endl; + Node flam = lamRep < n ? lamRepLam : lam; + Assert(!flam.isNull() && flam.getKind() == LAMBDA); + Node lhs = flam[1]; + Node glam = lamRep < n ? lam : lamRepLam; + Trace("uf-ho-debug") + << " lambda are " << flam << " and " << glam << std::endl; + std::vector<Node> args(flam[0].begin(), flam[0].end()); + Node rhs = d_ll.betaReduce(glam, args); + Node univ = nm->mkNode(FORALL, flam[0], lhs.eqNode(rhs)); + // f = g => forall x. reduce(lambda(f)(x)) = reduce(lambda(g)(x)) + // + // For example, if f -> lambda z. z+1, g -> lambda y. y+3, this + // will infer: f = g => forall x. x+1 = x+3, which simplifies to + // f != g. + Node lem = nm->mkNode(IMPLIES, f.eqNode(g), univ); + if (cacheLemma(lem)) + { + d_im.lemma(lem, InferenceId::UF_HO_LAMBDA_UNIV_EQ); + numLemmas++; + } + } + } + if (!lamRep.isNull()) + { + d_lambdaEqc[eqc] = lamRep; + } + } + Trace("uf-ho-debug") + << " found " << normalEqFuns.size() + << " ordinary functions that are equal to lambda functions" << std::endl; + if (normalEqFuns.empty()) + { + return numLemmas; + } + // if we have normal functions that are equal to lambda functions, go back + // and ensure they are mapped properly + // mapping from functions to terms + eq::EqClassesIterator eqcs_i2 = eq::EqClassesIterator(ee); + while (!eqcs_i2.isFinished()) + { + Node eqc = (*eqcs_i2); + ++eqcs_i2; + Trace("uf-ho-debug") << "Check equivalence class " << eqc << std::endl; + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); + while (!eqc_i.isFinished()) + { + Node n = *eqc_i; + ++eqc_i; + Trace("uf-ho-debug") << "Check term " << n << std::endl; + Node op; + Kind k = n.getKind(); + std::vector<Node> args; + if (k == APPLY_UF) + { + op = n.getOperator(); + args.insert(args.end(), n.begin(), n.end()); + } + else if (k == HO_APPLY) + { + op = n[0]; + args.push_back(n[1]); + } + else + { + continue; + } + if (normalEqFuns.find(op) == normalEqFuns.end()) + { + continue; + } + Trace("uf-ho-debug") << " found relevant ordinary application " << n + << std::endl; + Assert(ee->hasTerm(op)); + Node r = ee->getRepresentative(op); + Assert(d_lambdaEqc.find(r) != d_lambdaEqc.end()); + Node lf = d_lambdaEqc[r]; + Node lam = d_ll.getLambdaFor(lf); + Assert(!lam.isNull() && lam.getKind() == LAMBDA); + // a normal function g equal to a lambda, say f --> lambda(f) + // need to infer f = g => g(t) = f(t) for all terms g(t) + // that occur in the equality engine. + Node premise = op.eqNode(lf); + args.insert(args.begin(), lam); + Node rhs = nm->mkNode(n.getKind(), args); + rhs = rewrite(rhs); + Node conc = n.eqNode(rhs); + Node lem = nm->mkNode(IMPLIES, premise, conc); + if (cacheLemma(lem)) + { + d_im.lemma(lem, InferenceId::UF_HO_LAMBDA_APP_REDUCE); + numLemmas++; + } + } + } + return numLemmas; +} + unsigned HoExtension::check() { Trace("uf-ho") << "HoExtension::checkHigherOrder..." << std::endl; @@ -429,14 +644,24 @@ unsigned HoExtension::check() } } while (num_facts > 0); - unsigned num_lemmas = 0; - - num_lemmas = checkExtensionality(); - if (num_lemmas > 0) + // Apply extensionality, lazy lambda schemas in order. We make lazy lambda + // handling come last as it may introduce quantifiers. + for (size_t i = 0; i < 2; i++) { - Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas." - << std::endl; - return num_lemmas; + unsigned num_lemmas = 0; + // apply the schema + switch (i) + { + case 0: num_lemmas = checkExtensionality(); break; + case 1: num_lemmas = checkLazyLambda(); break; + default: break; + } + // finish if we added lemmas + if (num_lemmas > 0) + { + Trace("uf-ho") << "...returned " << num_lemmas << " lemmas." << std::endl; + return num_lemmas; + } } Trace("uf-ho") << "...finished check higher order." << std::endl; @@ -464,6 +689,16 @@ bool HoExtension::collectModelInfoHo(TheoryModel* m, // non-standard alternative to using a type enumerator over function // values to assign unique values. int addedLemmas = checkExtensionality(m); + // for equivalence classes that we know to assign a lambda directly + for (const std::pair<const Node, Node>& p : d_lambdaEqc) + { + Node lam = d_ll.getLambdaFor(p.second); + Assert(!lam.isNull()); + m->assertEquality(p.second, lam, true); + m->assertSkeleton(lam); + // assign it as the function definition for all variables in this class + m->assignFunctionDefinition(p.second, lam); + } return addedLemmas == 0; } @@ -484,6 +719,17 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m) return true; } +bool HoExtension::cacheLemma(TNode lem) +{ + Node rewritten = rewrite(lem); + if (d_cachedLemmas.find(rewritten) != d_cachedLemmas.end()) + { + return false; + } + d_cachedLemmas.insert(rewritten); + return true; +} + } // namespace uf } // namespace theory } // namespace cvc5 diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h index a646b57be..13d381622 100644 --- a/src/theory/uf/ho_extension.h +++ b/src/theory/uf/ho_extension.h @@ -15,14 +15,15 @@ #include "cvc5_private.h" -#ifndef __CVC5__THEORY__UF__HO_EXTENSION_H -#define __CVC5__THEORY__UF__HO_EXTENSION_H +#ifndef CVC5__THEORY__UF__HO_EXTENSION_H +#define CVC5__THEORY__UF__HO_EXTENSION_H #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdo.h" #include "expr/node.h" #include "smt/env_obj.h" +#include "theory/skolem_lemma.h" #include "theory/theory_inference_manager.h" #include "theory/theory_model.h" #include "theory/theory_state.h" @@ -31,7 +32,7 @@ namespace cvc5 { namespace theory { namespace uf { -class TheoryUF; +class LambdaLift; /** The higher-order extension of the theory of uninterpreted functions * @@ -54,7 +55,10 @@ class HoExtension : protected EnvObj typedef context::CDHashMap<Node, Node> NodeNodeMap; public: - HoExtension(Env& env, TheoryState& state, TheoryInferenceManager& im); + HoExtension(Env& env, + TheoryState& state, + TheoryInferenceManager& im, + LambdaLift& ll); /** ppRewrite * @@ -65,7 +69,7 @@ class HoExtension : protected EnvObj * function variables for function heads that are not variables via the * getApplyUfForHoApply method below. */ - Node ppRewrite(Node node); + TrustNode ppRewrite(Node node, std::vector<SkolemLemma>& lems); /** check higher order * @@ -171,8 +175,20 @@ class HoExtension : protected EnvObj /** check whether app-completion should be applied for any * pair of terms in the equality engine. + * + * Returns the number of lemmas added on this call. */ unsigned checkAppCompletion(); + /** + * Check lazy lambda. + * + * This assumes that lambdas are not eagerly lifted to quantified formulas. + * It processes two lemma schemas, UF_HO_LAMBDA_UNIV_EQ and + * UF_HO_LAMBDA_APP_REDUCE. For details on these, see inference_id.h. + * + * Returns the number of lemmas added on this call. + */ + unsigned checkLazyLambda(); /** collect model info for higher-order term * * This adds required constraints to m for term n. In particular, if n is @@ -182,24 +198,43 @@ class HoExtension : protected EnvObj bool collectModelInfoHoTerm(Node n, TheoryModel* m); private: + /** Cache lemma lem, return true if it does not already exist */ + bool cacheLemma(TNode lem); /** common constants */ Node d_true; /** Reference to the state object */ TheoryState& d_state; /** Reference to the inference manager */ TheoryInferenceManager& d_im; + /** Lambda lifting utility */ + LambdaLift& d_ll; /** extensionality has been applied to these disequalities */ NodeSet d_extensionality; + /** + * The lemmas we have sent. This is required since the UF inference manager + * does not cache lemmas. + */ + NodeSet d_cachedLemmas; + /** + * In the following, we say that a "lambda function" is a variable k that was + * introduced by the lambda lifting utility, and has a corresponding lambda + * definition. + * + * This maps equivalence class representatives that have lambda functions in + * them to one such lambda function. This map is computed at each full effort + * and valid only during collectModelInfoHo. + */ + std::unordered_map<Node, Node> d_lambdaEqc; /** cache of getExtensionalityDeq below */ std::map<Node, Node> d_extensionality_deq; /** map from non-standard operators to their skolems */ NodeNodeMap d_uf_std_skolem; -}; /* class TheoryUF */ +}; } // namespace uf } // namespace theory } // namespace cvc5 -#endif /* __CVC5__THEORY__UF__HO_EXTENSION_H */ +#endif diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index a1db5120f..252020b88 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -33,8 +33,6 @@ typerule LAMBDA ::cvc5::theory::uf::LambdaTypeRule variable BOOLEAN_TERM_VARIABLE "Boolean term variable" -variable LAMBDA_VARIABLE "Lambda variable, used for lazy lambda lifting" - # lambda expressions that are isomorphic to array constants can be considered constants construle LAMBDA ::cvc5::theory::uf::LambdaTypeRule diff --git a/src/theory/uf/lambda_lift.cpp b/src/theory/uf/lambda_lift.cpp index 3d51e6858..605e346af 100644 --- a/src/theory/uf/lambda_lift.cpp +++ b/src/theory/uf/lambda_lift.cpp @@ -90,6 +90,11 @@ Node LambdaLift::getLambdaFor(TNode skolem) const return it->second; } +bool LambdaLift::isLambdaFunction(TNode n) const +{ + return !getLambdaFor(n).isNull(); +} + Node LambdaLift::getAssertionFor(TNode node) { TNode skolem = getSkolemFor(node); diff --git a/src/theory/uf/lambda_lift.h b/src/theory/uf/lambda_lift.h index f61007d1c..1e36dad31 100644 --- a/src/theory/uf/lambda_lift.h +++ b/src/theory/uf/lambda_lift.h @@ -60,6 +60,8 @@ class LambdaLift : protected EnvObj /** Get the lambda term for skolem, if skolem is a lambda function. */ Node getLambdaFor(TNode skolem) const; + /** Is skolem a lambda function? */ + bool isLambdaFunction(TNode n) const; /** * Beta-reduce node. If node is APPLY_UF and its operator is a lambda diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 5c9446507..b6d789773 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -21,6 +21,7 @@ #include <sstream> #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" @@ -31,6 +32,7 @@ #include "theory/type_enumerator.h" #include "theory/uf/cardinality_extension.h" #include "theory/uf/ho_extension.h" +#include "theory/uf/lambda_lift.h" #include "theory/uf/theory_uf_rewriter.h" using namespace std; @@ -46,6 +48,7 @@ TheoryUF::TheoryUF(Env& env, std::string instanceName) : Theory(THEORY_UF, env, out, valuation, instanceName), d_thss(nullptr), + d_lambdaLift(new LambdaLift(env)), d_ho(nullptr), d_functionsTerms(context()), d_symb(env, instanceName), @@ -100,7 +103,7 @@ void TheoryUF::finishInit() { if (isHo) { d_equalityEngine->addFunctionKind(kind::HO_APPLY); - d_ho.reset(new HoExtension(d_env, d_state, d_im)); + d_ho.reset(new HoExtension(d_env, d_state, d_im, *d_lambdaLift.get())); } } @@ -212,38 +215,41 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems) Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node << std::endl; Kind k = node.getKind(); + bool isHol = logicInfo().isHigherOrder(); if (k == kind::HO_APPLY || (node.isVar() && node.getType().isFunction())) { - if (!logicInfo().isHigherOrder()) + if (!isHol) { std::stringstream ss; ss << "Partial function applications are only supported with " "higher-order logic. Try adding the logic prefix HO_."; throw LogicException(ss.str()); } - Node ret = d_ho->ppRewrite(node); - if (ret != node) - { - Trace("uf-exp-def") << "TheoryUF::ppRewrite: higher-order: " << node - << " to " << ret << std::endl; - return TrustNode::mkTrustRewrite(node, ret, nullptr); - } } else if (k == kind::APPLY_UF) { - // check for higher-order - // logic exception if higher-order is not enabled - if (isHigherOrderType(node.getOperator().getType()) - && !logicInfo().isHigherOrder()) + if (!isHol && isHigherOrderType(node.getOperator().getType())) { + // check for higher-order + // logic exception if higher-order is not enabled std::stringstream ss; ss << "UF received an application whose operator has higher-order type " << node - << ", which is only supported with higher-order logic. Try adding the " - "logic prefix HO_."; + << ", which is only supported with higher-order logic. Try adding " + "the logic prefix HO_."; throw LogicException(ss.str()); } } + if (isHol) + { + TrustNode ret = d_ho->ppRewrite(node, lems); + if (!ret.isNull()) + { + Trace("uf-exp-def") << "TheoryUF::ppRewrite: higher-order: " << node + << " to " << ret.getNode() << std::endl; + return ret; + } + } return TrustNode::null(); } @@ -308,6 +314,18 @@ void TheoryUF::preRegisterTerm(TNode node) d_equalityEngine->addTerm(node); break; } + + if (logicInfo().isHigherOrder()) + { + // When using lazy lambda handling, if node is a lambda function, it must + // be marked as a shared term. This is to ensure we split on the equality + // of lambda functions with other functions when doing care graph + // based theory combination. + if (d_lambdaLift->isLambdaFunction(node)) + { + addSharedTerm(node); + } + } } void TheoryUF::explain(TNode literal, Node& exp) @@ -523,7 +541,20 @@ bool TheoryUF::areCareDisequal(TNode x, TNode y) TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF); EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); - if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){ + if (eqStatus == EQUALITY_FALSE || eqStatus == EQUALITY_FALSE_AND_PROPAGATED) + { + return true; + } + else if (eqStatus == EQUALITY_FALSE_IN_MODEL) + { + // if x or y is a lambda function, and they are neither entailed to + // be equal or disequal, then we return false. This ensures the pair + // (x,y) may be considered for the care graph. + if (d_lambdaLift->isLambdaFunction(x) + || d_lambdaLift->isLambdaFunction(y)) + { + return false; + } return true; } } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 6f04035ed..b72262164 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -35,6 +35,7 @@ namespace uf { class CardinalityExtension; class HoExtension; +class LambdaLift; class TheoryUF : public Theory { public: @@ -74,6 +75,8 @@ class TheoryUF : public Theory { private: /** The associated cardinality extension (or nullptr if it does not exist) */ std::unique_ptr<CardinalityExtension> d_thss; + /** the lambda lifting utility */ + std::unique_ptr<LambdaLift> d_lambdaLift; /** the higher-order solver extension (or nullptr if it does not exist) */ std::unique_ptr<HoExtension> d_ho; diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index d3ff709ca..5f96d2b9b 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -41,8 +41,3 @@ add_subdirectory(api EXCLUDE_FROM_ALL) if(ENABLE_UNIT_TESTING) add_subdirectory(unit EXCLUDE_FROM_ALL) endif() - -# add Python bindings tests if building with Python bindings -if (BUILD_BINDINGS_PYTHON) - add_subdirectory(python) -endif() diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt deleted file mode 100644 index 5b681ca36..000000000 --- a/test/python/CMakeLists.txt +++ /dev/null @@ -1,37 +0,0 @@ -############################################################################### -# Top contributors (to current version): -# Yoni Zohar, Aina Niemetz, Mathias Preiner -# -# 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 build system configuration. -## - -# Check if the pytest Python module is installed. -check_python_module("pytest") - -# Add Python bindings API tests. -macro(cvc5_add_python_api_test name filename) -# We create test target 'python/unit/api/myapitest' and run it with -# 'ctest -R "python/unit/api/myapitest"'. -add_test (NAME python/unit/api/${name} - COMMAND ${PYTHON_EXECUTABLE} -m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename} - # directory for importing the python bindings - WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python) -endmacro() - -# add specific test files -cvc5_add_python_api_test(pytest_solver unit/api/test_solver.py) -cvc5_add_python_api_test(pytest_sort unit/api/test_sort.py) -cvc5_add_python_api_test(pytest_term unit/api/test_term.py) -cvc5_add_python_api_test(pytest_datatype_api unit/api/test_datatype_api.py) -cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py) -cvc5_add_python_api_test(pytest_to_python_obj unit/api/test_to_python_obj.py) -cvc5_add_python_api_test(pytest_op unit/api/test_op.py) -cvc5_add_python_api_test(pytest_result unit/api/test_result.py) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b08b2f6f5..4937c8481 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -109,6 +109,7 @@ set(regress_0_tests regress0/arrays/issue3813-massign-assert.smt2 regress0/arrays/issue3814.smt2 regress0/arrays/issue4927-unsat-cores.smt2 + regress0/arrays/issue7596-define-array-uminus.smt2 regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2 regress0/arrays/x2.smtv1.smt2 regress0/arrays/x3.smtv1.smt2 @@ -659,11 +660,14 @@ set(regress_0_tests regress0/ho/issue6536.smt2 regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 + regress0/ho/lazy-lambda-model.smt2 regress0/ho/match-middle.smt2 regress0/ho/modulo-func-equality.smt2 regress0/ho/qgu-fuzz-ho-1-dd.smt2 regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2 regress0/ho/shadowing-defs.smt2 + regress0/ho/simple-conf-lazy-lambda-lift.smt2 + regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 regress0/ho/simple-matching-partial.smt2 regress0/ho/simple-matching.smt2 regress0/ho/trans.smt2 @@ -1599,9 +1603,11 @@ set(regress_1_tests regress1/bags/fuzzy3.smt2 regress1/bags/fuzzy4.smt2 regress1/bags/fuzzy5.smt2 + regress1/bags/fuzzy6.smt2 regress1/bags/intersection_min1.smt2 regress1/bags/intersection_min2.smt2 regress1/bags/issue5759.smt2 + regress1/bags/map-lazy-lam.smt2 regress1/bags/map1.smt2 regress1/bags/map2.smt2 regress1/bags/map3.smt2 @@ -1726,8 +1732,10 @@ set(regress_1_tests regress1/fmf/with-ind-104-core.smt2 regress1/gensys_brn001.smt2 regress1/ho/bug_freeVar_BDD_General_data_270.p + regress1/ho/bug_freevar_PHI004^4-delta.smt2 regress1/ho/bound_var_bug.p regress1/ho/fta0328.lfho.p + regress1/ho/ho-fun-sharing-dd.smt2 regress1/ho/issue3136-fconst-bool-bool.smt2 regress1/ho/issue4065-no-rep.smt2 regress1/ho/issue4092-sinf.smt2 @@ -2803,8 +2811,6 @@ set(regression_disabled_tests ### regress1/bug472.smt2 regress1/datatypes/non-simple-rec-set.smt2 - # disabled temporarily until lazy lambda handling is merged - regress1/ho/bug_freevar_PHI004^4-delta.smt2 # results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 # after disallowing solving for terms with quantifiers diff --git a/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 b/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 new file mode 100644 index 000000000..da21db28e --- /dev/null +++ b/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status sat) +(define-fun foo () (Array Int Int) ((as const (Array Int Int)) (- 1))) +(assert (= (select foo 0) (- 1))) +(check-sat) diff --git a/test/regress/regress0/ho/lazy-lambda-model.smt2 b/test/regress/regress0/ho/lazy-lambda-model.smt2 new file mode 100644 index 000000000..71df017e9 --- /dev/null +++ b/test/regress/regress0/ho/lazy-lambda-model.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --uf-lazy-ll +; EXPECT: sat +(set-logic HO_ALL) +(declare-fun g (Int) Int) +(declare-fun h (Int) Int) +(define-fun f ((x Int)) Int (ite (> x 0) (* 2 x) x)) + +(declare-fun a () Int) +(declare-fun b () Int) + + +(assert (or (= f g) (= f h))) + +(assert (and (= (h a) 26) (= (g b) 26))) + +(check-sat) diff --git a/test/regress/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 new file mode 100644 index 000000000..ab949c40c --- /dev/null +++ b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --uf-lazy-ll +; EXPECT: unsat +(set-logic HO_ALL) +(set-info :status unsat) +(define-fun f ((x Int)) Int (+ x 1)) +(declare-fun g (Int) Int) +(declare-fun h (Int) Int) + +(assert (or (= f g) (= f h))) + +(assert (= (g 4) 0)) +(assert (= (h 4) 8)) + +(check-sat) diff --git a/test/regress/regress0/ho/simple-conf-lazy-lambda-lift.smt2 b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift.smt2 new file mode 100644 index 000000000..d11a4418b --- /dev/null +++ b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --uf-lazy-ll +; EXPECT: unsat +(set-logic HO_ALL) +(set-info :status unsat) +(define-fun f ((x Int)) Int (+ x 1)) +(define-fun g ((x Int)) Int (+ x 2)) +(define-fun h ((x Int)) Int 6) + +(assert (or (= f g) (= f h))) + +(check-sat) diff --git a/test/regress/regress0/rels/addr_book_0.cvc.smt2 b/test/regress/regress0/rels/addr_book_0.cvc.smt2 index 70488b4eb..9bc85f268 100644 --- a/test/regress/regress0/rels/addr_book_0.cvc.smt2 +++ b/test/regress/regress0/rels/addr_book_0.cvc.smt2 @@ -33,7 +33,7 @@ (assert (set.member t_tup Target)) (assert (set.subset (rel.join (rel.join Book addr) Target) Name)) (assert (set.subset (rel.join Book names) Name)) -(assert (= (set.intersection Name Addr) (as set.empty (Set (Tuple Atom))))) +(assert (= (set.inter Name Addr) (as set.empty (Set (Tuple Atom))))) (assert (= (rel.join (set.singleton n_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Set (Tuple Atom))))) (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.union (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (set.singleton t_tup))))) (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b3_tup) addr)) (set.minus (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.singleton t_tup))))) diff --git a/test/regress/regress0/rels/iden_0.cvc.smt2 b/test/regress/regress0/rels/iden_0.cvc.smt2 index 1cdeffbff..75dc80d22 100644 --- a/test/regress/regress0/rels/iden_0.cvc.smt2 +++ b/test/regress/regress0/rels/iden_0.cvc.smt2 @@ -21,5 +21,5 @@ (assert (set.member v x)) (assert (set.member a x)) (assert (= id (rel.iden t))) -(assert (not (set.member (tuple 1 1) (set.intersection id x)))) +(assert (not (set.member (tuple 1 1) (set.inter id x)))) (check-sat) diff --git a/test/regress/regress0/sets/complement3.cvc.smt2 b/test/regress/regress0/sets/complement3.cvc.smt2 index 20cfb36f8..2046b2fc9 100644 --- a/test/regress/regress0/sets/complement3.cvc.smt2 +++ b/test/regress/regress0/sets/complement3.cvc.smt2 @@ -8,7 +8,7 @@ (declare-fun C4 () (Set (Tuple Atom))) (declare-fun ATOM_UNIV () (Set (Tuple Atom))) (declare-fun V1 () Atom) -(assert (= C32 (set.intersection (set.complement C2) (set.complement C4)))) +(assert (= C32 (set.inter (set.complement C2) (set.complement C4)))) (assert (set.member (tuple V1) (set.complement C32))) (assert (= ATOM_UNIV (as set.universe (Set (Tuple Atom))))) (assert (set.member (tuple V1) ATOM_UNIV)) diff --git a/test/regress/regress0/sets/cvc-sample.cvc.smt2 b/test/regress/regress0/sets/cvc-sample.cvc.smt2 index 9ee199b43..9c89df0c6 100644 --- a/test/regress/regress0/sets/cvc-sample.cvc.smt2 +++ b/test/regress/regress0/sets/cvc-sample.cvc.smt2 @@ -20,12 +20,12 @@ (declare-fun e () Int) (assert (= a (set.singleton 5))) (assert (= c (set.union a b))) -(assert (not (= c (set.intersection a b)))) +(assert (not (= c (set.inter a b)))) (assert (= c (set.minus a b))) (assert (set.subset a b)) (assert (set.member e c)) (assert (set.member e a)) -(assert (set.member e (set.intersection a b))) +(assert (set.member e (set.inter a b))) (push 1) (assert true) diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2 index 0ecd32bf8..c93b18857 100644 --- a/test/regress/regress0/sets/eqtest.smt2 +++ b/test/regress/regress0/sets/eqtest.smt2 @@ -10,9 +10,9 @@ (declare-fun H () (Set Int) ) (declare-fun I () (Set Int) ) (declare-fun x () Int) -(assert (set.member x (set.intersection (set.union A B) C))) +(assert (set.member x (set.inter (set.union A B) C))) (assert (not (set.member x G))) (assert (= (set.union A B) D)) -(assert (= C (set.intersection E F))) +(assert (= C (set.inter E F))) (assert (and (= F H) (= G H) (= H I))) (check-sat) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 index 7e2f627ae..76592a691 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 index f6fd4bd53..b0172db39 100644 --- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 index f70d59b16..1538a2e9f 100644 --- a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 +++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 @@ -66,7 +66,7 @@ (assert (! (= sk_?X_36$0 FP$0) :named precondition_of_rec_copy_loop_34_11_18)) -(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_38$0 sk_?X_37$0)) +(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_38$0 sk_?X_37$0)) :named precondition_of_rec_copy_loop_34_11_19)) (assert (! (= old_cp_2$0 cp$0) :named assign_41_4)) diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2 index 6857e5147..66f843c9d 100644 --- a/test/regress/regress0/sets/sets-inter.smt2 +++ b/test/regress/regress0/sets/sets-inter.smt2 @@ -5,7 +5,7 @@ (declare-fun b () (Set Int)) (declare-fun x () Int) ;(assert (not (set.member x a))) -(assert (set.member x (set.intersection a b))) +(assert (set.member x (set.inter a b))) (assert (not (set.member x b))) (check-sat) (exit) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index 4a49bef07..0020e5c55 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -8,7 +8,7 @@ (declare-fun x () Int) (assert (set.member x (set.union A B))) -(assert (not (set.member x (set.intersection A B)))) +(assert (not (set.member x (set.inter A B)))) (assert (not (set.member x (set.minus A B)))) ;(assert (not (set.member x (set.minus B A)))) ;(assert (set.member x B)) diff --git a/test/regress/regress0/sets/sets-poly-int-real.smt2 b/test/regress/regress0/sets/sets-poly-int-real.smt2 index 20832c573..00546eee2 100644 --- a/test/regress/regress0/sets/sets-poly-int-real.smt2 +++ b/test/regress/regress0/sets/sets-poly-int-real.smt2 @@ -11,7 +11,7 @@ (assert (= t1 (set.union s (set.singleton 2.5)))) (assert (= t2 (set.union s (set.singleton 2.0)))) (assert (= t3 (set.union r3 (set.singleton 2.5)))) -(assert (= (set.intersection r1 r2) (set.intersection s (set.singleton 0.0)))) +(assert (= (set.inter r1 r2) (set.inter s (set.singleton 0.0)))) (assert (not (= r1 (as set.empty (Set Real))))) (check-sat) diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 index 3dcafae08..4a11bcc78 100644 --- a/test/regress/regress0/sets/sets-sample.smt2 +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -15,12 +15,12 @@ (declare-fun e () Int) (assert (= a (set.singleton 5))) (assert (= c (set.union a b) )) -(assert (not (= c (set.intersection a b) ))) +(assert (not (= c (set.inter a b) ))) (assert (= c (set.minus a b) )) (assert (set.subset a b)) (assert (set.member e c)) (assert (set.member e a)) -(assert (set.member e (set.intersection a b))) +(assert (set.member e (set.inter a b))) (check-sat) (pop 1) diff --git a/test/regress/regress0/sets/sharing-simp.smt2 b/test/regress/regress0/sets/sharing-simp.smt2 index be746be1d..a591792cf 100644 --- a/test/regress/regress0/sets/sharing-simp.smt2 +++ b/test/regress/regress0/sets/sharing-simp.smt2 @@ -9,7 +9,7 @@ (assert (set.member x A)) (assert (set.member y B)) -(assert (or (= C (set.intersection A B)) (= D (set.intersection A B)))) +(assert (or (= C (set.inter A B)) (= D (set.inter A B)))) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy6.smt2 b/test/regress/regress1/bags/fuzzy6.smt2 new file mode 100644 index 000000000..2bcc024dd --- /dev/null +++ b/test/regress/regress1/bags/fuzzy6.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Bag (Tuple Int Int))) +(declare-fun c () Int) +(declare-fun d () (Tuple Int Int)) +(assert + (let ((double_c (+ c c))) + (let ((formula (= A (bag (tuple c double_c) c)))) + (and (not (= formula (= A (bag (tuple c c) c)))) + (not (= formula (= A (bag (tuple 0 c) double_c)))))))) + +(check-sat) diff --git a/test/regress/regress1/bags/map-lazy-lam.smt2 b/test/regress/regress1/bags/map-lazy-lam.smt2 new file mode 100644 index 000000000..c99bab7c9 --- /dev/null +++ b/test/regress/regress1/bags/map-lazy-lam.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --fmf-bound --uf-lazy-ll +; EXPECT: sat +(set-logic HO_ALL) +(define-fun f ((x String)) Int 1) +(define-fun cardinality ((A (Bag String))) Int + (bag.count 1 (bag.map f A))) +(declare-fun A () (Bag String)) +(assert (= (cardinality A) 20)) +(check-sat) diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 index 7c9de4c49..0155eecb2 100644 --- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 +++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find -q --decision=justification-old +; COMMAND-LINE: --finite-model-find --decision=justification-old --uf-lazy-ll -q ; EXPECT: sat (set-logic HO_ALL) diff --git a/test/regress/regress1/ho/ho-fun-sharing-dd.smt2 b/test/regress/regress1/ho/ho-fun-sharing-dd.smt2 new file mode 100644 index 000000000..300dc26de --- /dev/null +++ b/test/regress/regress1/ho/ho-fun-sharing-dd.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat +(set-logic HO_ALL) +(declare-sort n 0) +(declare-fun x () n) +(declare-fun s (n) n) +(declare-fun t ((-> n Bool)) Bool) +(assert (forall ((X n)) (t (lambda ((Xu n)) (= X (s Xu)))))) +(assert (not (t (lambda ((Xu n)) (= x (s Xu)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/set8.smt2 b/test/regress/regress1/quantifiers/set8.smt2 index 209b213c1..17eea7b0a 100644 --- a/test/regress/regress1/quantifiers/set8.smt2 +++ b/test/regress/regress1/quantifiers/set8.smt2 @@ -15,12 +15,12 @@ (assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (and (set.subset ?s1 ?s2) (set.subset ?s2 ?s1))))) (declare-fun union (Set Set) Set) (assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (union ?s1 ?s2)) (or (set.member ?x ?s1) (set.member ?x ?s2))))) -(declare-fun set.intersection (Set Set) Set) -(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (set.intersection ?s1 ?s2)) (and (set.member ?x ?s1) (set.member ?x ?s2))))) +(declare-fun set.inter (Set Set) Set) +(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (set.inter ?s1 ?s2)) (and (set.member ?x ?s1) (set.member ?x ?s2))))) (declare-fun difference (Set Set) Set) (assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (difference ?s1 ?s2)) (and (set.member ?x ?s1) (not (set.member ?x ?s2)))))) (declare-fun a () Set) (declare-fun b () Set) -(assert (not (seteq (set.intersection a b) (set.intersection b a)))) +(assert (not (seteq (set.inter a b) (set.inter b a)))) (check-sat) (exit) diff --git a/test/regress/regress1/rels/rel_complex_3.cvc.smt2 b/test/regress/regress1/rels/rel_complex_3.cvc.smt2 index 7e80fdd70..8269daf42 100644 --- a/test/regress/regress1/rels/rel_complex_3.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_3.cvc.smt2 @@ -20,12 +20,12 @@ (assert (= r (rel.join x y))) (declare-fun e () (Tuple Int Int)) (assert (not (set.member e r))) -(assert (not (= z (set.intersection x y)))) +(assert (not (= z (set.inter x y)))) (assert (= z (set.minus x y))) (assert (set.subset x y)) (assert (set.member e (rel.join r z))) (assert (set.member e x)) -(assert (set.member e (set.intersection x y))) +(assert (set.member e (set.inter x y))) (push 1) (assert true) diff --git a/test/regress/regress1/rels/rel_complex_4.cvc.smt2 b/test/regress/regress1/rels/rel_complex_4.cvc.smt2 index 9a35f336e..134a99c73 100644 --- a/test/regress/regress1/rels/rel_complex_4.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_4.cvc.smt2 @@ -24,12 +24,12 @@ (assert (= w (set.singleton e))) (assert (set.subset (rel.transpose w) y)) (assert (not (set.member e r))) -(assert (not (= z (set.intersection x y)))) +(assert (not (= z (set.inter x y)))) (assert (= z (set.minus x y))) (assert (set.subset x y)) (assert (set.member e (rel.join r z))) (assert (set.member e x)) -(assert (set.member e (set.intersection x y))) +(assert (set.member e (set.inter x y))) (push 1) (assert true) diff --git a/test/regress/regress1/rels/rel_complex_5.cvc.smt2 b/test/regress/regress1/rels/rel_complex_5.cvc.smt2 index fc2d73235..ed894518e 100644 --- a/test/regress/regress1/rels/rel_complex_5.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_5.cvc.smt2 @@ -26,12 +26,12 @@ (assert (let ((_let_1 (set.singleton a))) (= w (rel.product _let_1 _let_1)))) (assert (set.subset (rel.transpose w) y)) (assert (not (set.member e r))) -(assert (not (= z (set.intersection x y)))) +(assert (not (= z (set.inter x y)))) (assert (= z (set.minus x y))) (assert (set.subset x y)) (assert (set.member e (rel.join r z))) (assert (set.member e x)) -(assert (set.member e (set.intersection x y))) +(assert (set.member e (set.inter x y))) (push 1) (assert true) diff --git a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 index 144566fc5..e5b92a4fc 100644 --- a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 +++ b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 @@ -12,7 +12,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 index 9a2521520..206450142 100644 --- a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 +++ b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 @@ -7,7 +7,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 index b2732dbd2..fe7e7d7ac 100644 --- a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 +++ b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -7,7 +7,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 index ee24367c3..078b98eef 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 index b0cfe4888..756f0430c 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 index 9ac15e9a4..1e45c21e9 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) (declare-fun z3v66 () Int) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 index 68ed72a93..a3fd883b6 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/card-3.smt2 b/test/regress/regress1/sets/card-3.smt2 index 383395b0d..bbcf1c489 100644 --- a/test/regress/regress1/sets/card-3.smt2 +++ b/test/regress/regress1/sets/card-3.smt2 @@ -8,5 +8,5 @@ (assert (>= (set.card (set.union s u)) 8)) (assert (<= (set.card (set.union t u)) 5)) (assert (<= (set.card s) 5)) -(assert (= (as set.empty (Set E)) (set.intersection t u))) +(assert (= (as set.empty (Set E)) (set.inter t u))) (check-sat) diff --git a/test/regress/regress1/sets/card-4.smt2 b/test/regress/regress1/sets/card-4.smt2 index 019b16a09..9f0e96dc5 100644 --- a/test/regress/regress1/sets/card-4.smt2 +++ b/test/regress/regress1/sets/card-4.smt2 @@ -8,7 +8,7 @@ (assert (>= (set.card (set.union s u)) 8)) ;(assert (<= (set.card (set.union t u)) 5)) (assert (<= (set.card s) 5)) -(assert (= (as set.empty (Set E)) (set.intersection t u))) +(assert (= (as set.empty (Set E)) (set.inter t u))) (declare-fun x1 () E) (declare-fun x2 () E) (declare-fun x3 () E) diff --git a/test/regress/regress1/sets/card-5.smt2 b/test/regress/regress1/sets/card-5.smt2 index c24ca974a..51ad7971c 100644 --- a/test/regress/regress1/sets/card-5.smt2 +++ b/test/regress/regress1/sets/card-5.smt2 @@ -8,7 +8,7 @@ (assert (>= (set.card (set.union s u)) 8)) ;(assert (<= (set.card (set.union t u)) 5)) (assert (<= (set.card s) 5)) -(assert (= (as set.empty (Set E)) (set.intersection t u))) +(assert (= (as set.empty (Set E)) (set.inter t u))) (declare-fun x1 () E) (declare-fun x2 () E) (declare-fun x3 () E) diff --git a/test/regress/regress1/sets/card-6.smt2 b/test/regress/regress1/sets/card-6.smt2 index b0ef3a3b9..fc2d34acc 100644 --- a/test/regress/regress1/sets/card-6.smt2 +++ b/test/regress/regress1/sets/card-6.smt2 @@ -7,7 +7,7 @@ (assert (and (= (as set.empty (Set E)) - (set.intersection A B)) + (set.inter A B)) (set.subset C (set.union A B)) (>= (set.card C) 5) (<= (set.card A) 2) diff --git a/test/regress/regress1/sets/comp-intersect.smt2 b/test/regress/regress1/sets/comp-intersect.smt2 index 60d9046bd..5f6f7576b 100644 --- a/test/regress/regress1/sets/comp-intersect.smt2 +++ b/test/regress/regress1/sets/comp-intersect.smt2 @@ -9,6 +9,6 @@ (assert (= x (set.comprehension ((z Int)) (> z 4) (* 5 z)))) (assert (= y (set.comprehension ((z Int)) (< z 10) (+ (* 5 z) 1)))) -(assert (not (= (set.intersection x y) (as set.empty (Set Int))))) +(assert (not (= (set.inter x y) (as set.empty (Set Int))))) (check-sat) diff --git a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 index 7c5e09b5a..93d359b60 100644 --- a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 +++ b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -7,7 +7,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 index aa5b62d09..ec82ddb8b 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 @@ -7,6 +7,6 @@ (declare-fun universe () (Set Bool)) (assert (= (set.card A) 2)) (assert (= (set.card B) 2)) -(assert (= (set.intersection A B) (as set.empty (Set Bool)))) +(assert (= (set.inter A B) (as set.empty (Set Bool)))) (assert (= universe (as set.universe (Set Bool)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 index 91bf1905a..0003349b3 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 @@ -8,7 +8,7 @@ (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) (assert (not (= A B))) -(assert (= (set.card (set.intersection A B)) 2)) +(assert (= (set.card (set.inter A B)) 2)) (assert (= (set.card (set.minus A B)) 3)) (assert (= (set.card (set.minus B A)) 3)) (assert (= universe (as set.universe (Set (_ BitVec 3))))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 index adbe51507..5808c4ec7 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 @@ -9,7 +9,7 @@ (assert (= (set.card A) 3)) (assert (= (set.card B) 3)) (assert (not (= A B))) -(assert (= (set.card (set.intersection A B)) 1)) +(assert (= (set.card (set.inter A B)) 1)) (assert (= (set.card (set.minus A B)) 2)) (assert (= (set.card (set.minus B A)) 2)) (assert (not (set.member x A))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 index 2ccbc8a58..81c49e1e3 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 @@ -9,7 +9,7 @@ (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) (assert (not (= A B))) -(assert (= (set.card (set.intersection A B)) 2)) +(assert (= (set.card (set.inter A B)) 2)) (assert (= (set.card (set.minus A B)) 3)) (assert (= (set.card (set.minus B A)) 3)) (assert (= universe (as set.universe (Set (_ BitVec 3))))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 index 4c113c84b..62c0bc224 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 @@ -9,6 +9,6 @@ (declare-fun x () Rec) (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) -(assert (= (set.card (set.intersection A B)) 1)) +(assert (= (set.card (set.inter A B)) 1)) (assert (= universe (as set.universe (Set Rec)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 index 4c9bdadd5..70e3a88d8 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 @@ -8,6 +8,6 @@ (declare-fun universe () (Set Rec)) (assert (= (set.card A) 9)) (assert (= (set.card B) 9)) -(assert (= (set.card (set.intersection A B)) 1)) +(assert (= (set.card (set.inter A B)) 1)) (assert (= universe (as set.universe (Set Rec)))) (check-sat) diff --git a/test/regress/regress1/sets/fuzz14418.smt2 b/test/regress/regress1/sets/fuzz14418.smt2 index 2fb60cb72..b09cf1151 100644 --- a/test/regress/regress1/sets/fuzz14418.smt2 +++ b/test/regress/regress1/sets/fuzz14418.smt2 @@ -34,7 +34,7 @@ (let ((e14 (set.minus v2 v2))) (let ((e15 (f1 v1 v4 v1))) (let ((e16 (f1 e14 v1 v4))) -(let ((e17 (set.intersection e16 e15))) +(let ((e17 (set.inter e16 e15))) (let ((e18 (f1 v4 e15 v2))) (let ((e19 (ite (p1 e13) (set.singleton 1) (set.singleton 0)))) (let ((e20 (set.member v0 e17))) diff --git a/test/regress/regress1/sets/fuzz15201.smt2 b/test/regress/regress1/sets/fuzz15201.smt2 index 3094a8d84..bdcbe7d59 100644 --- a/test/regress/regress1/sets/fuzz15201.smt2 +++ b/test/regress/regress1/sets/fuzz15201.smt2 @@ -29,9 +29,9 @@ (let ((e16 (set.minus v2 v1))) (let ((e17 (set.minus v1 v2))) (let ((e18 (set.union e17 e17))) -(let ((e19 (set.intersection e17 v1))) -(let ((e20 (set.intersection e17 e18))) -(let ((e21 (set.intersection v1 e16))) +(let ((e19 (set.inter e17 v1))) +(let ((e20 (set.inter e17 e18))) +(let ((e21 (set.inter v1 e16))) (let ((e22 (set.minus e20 e16))) (let ((e23 (ite (p1 v2 e18 e21) (set.singleton 1) (set.singleton 0)))) (let ((e24 (set.minus e17 e23))) diff --git a/test/regress/regress1/sets/fuzz31811.smt2 b/test/regress/regress1/sets/fuzz31811.smt2 index e86901f9a..ca028488a 100644 --- a/test/regress/regress1/sets/fuzz31811.smt2 +++ b/test/regress/regress1/sets/fuzz31811.smt2 @@ -28,19 +28,19 @@ (let ((e10 (f0 v0 e8 e8))) (let ((e11 (ite (p1 v1) (set.singleton 1) (set.singleton 0)))) (let ((e12 (set.union v3 v3))) -(let ((e13 (set.intersection v3 v1))) +(let ((e13 (set.inter v3 v1))) (let ((e14 (ite (p1 v3) (set.singleton 1) (set.singleton 0)))) -(let ((e15 (set.intersection v2 e14))) +(let ((e15 (set.inter v2 e14))) (let ((e16 (ite (p1 e11) (set.singleton 1) (set.singleton 0)))) (let ((e17 (ite (p1 v4) (set.singleton 1) (set.singleton 0)))) (let ((e18 (set.union e15 v2))) (let ((e19 (ite (p1 e16) (set.singleton 1) (set.singleton 0)))) -(let ((e20 (set.intersection e18 v3))) +(let ((e20 (set.inter e18 v3))) (let ((e21 (set.minus v4 e12))) (let ((e22 (set.union v3 v2))) (let ((e23 (set.minus e12 v4))) (let ((e24 (set.minus v3 e16))) -(let ((e25 (set.intersection e19 e20))) +(let ((e25 (set.inter e19 e20))) (let ((e26 (ite (p1 e15) (set.singleton 1) (set.singleton 0)))) (let ((e27 (set.minus e17 e15))) (let ((e28 (f1 e23 e12))) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 index f6d032f11..57f4344c6 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 @@ -7,6 +7,6 @@ (assert (= (set.card universe) 3)) (assert (= (set.card A) 2)) (assert (= (set.card B) 2)) -(assert (= (set.intersection A B) (as set.empty (Set (Array Int Int))))) +(assert (= (set.inter A B) (as set.empty (Set (Array Int Int))))) (assert (= universe (as set.universe (Set (Array Int Int))))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 index d7e6a758c..76828576e 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 @@ -7,6 +7,6 @@ (assert (= (set.card universe) 3)) (assert (= (set.card A) 1)) (assert (= (set.card B) 2)) -(assert (= (set.intersection A B) (as set.empty (Set (Array Int Int))))) +(assert (= (set.inter A B) (as set.empty (Set (Array Int Int))))) (assert (= universe (as set.universe (Set (Array Int Int))))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 index c649c9be2..2cf5e566d 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 @@ -7,6 +7,6 @@ (declare-const B (Set Int)) (assert (= (set.card A) 6)) (assert (= (set.card B) 5)) -(assert (= (set.intersection A B) (as set.empty (Set Int)))) +(assert (= (set.inter A B) (as set.empty (Set Int)))) (assert (= universe (as set.universe (Set Int)))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 index b3958e79e..8668b9c27 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 @@ -7,6 +7,6 @@ (declare-const B (Set Int)) (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) -(assert (= (set.intersection A B) (as set.empty (Set Int)))) +(assert (= (set.inter A B) (as set.empty (Set Int)))) (assert (= universe (as set.universe (Set Int)))) (check-sat) diff --git a/test/regress/regress1/sets/insert_invariant_37_2.smt2 b/test/regress/regress1/sets/insert_invariant_37_2.smt2 index cac805531..a8f117062 100644 --- a/test/regress/regress1/sets/insert_invariant_37_2.smt2 +++ b/test/regress/regress1/sets/insert_invariant_37_2.smt2 @@ -723,7 +723,7 @@ (assert (! (not (set.member null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1)) (assert (! (or (= prev_2$0 curr_2$0) - (set.member sk_?e_1$0 (set.intersection sk_?X_4$0 sk_?X_3$0)) + (set.member sk_?e_1$0 (set.inter sk_?X_4$0 sk_?X_3$0)) (and (set.member sk_?e_1$0 sk_FP$0) (not (set.member sk_?e_1$0 FP$0))) (and (set.member sk_?e$0 (set.union c1_2$0 c2_2$0)) (not (set.member sk_?e$0 content$0))) (and (set.member sk_?e$0 c1_2$0) diff --git a/test/regress/regress1/sets/issue2904.smt2 b/test/regress/regress1/sets/issue2904.smt2 index c39ea09ba..d2ffdbd7c 100644 --- a/test/regress/regress1/sets/issue2904.smt2 +++ b/test/regress/regress1/sets/issue2904.smt2 @@ -21,6 +21,6 @@ (assert (> n (+ (* 2 f) m))) -(assert (>= (set.card (set.minus UNIVERALSET (set.intersection (set.minus UNIVERALSET b) (set.minus UNIVERALSET c)))) n)) +(assert (>= (set.card (set.minus UNIVERALSET (set.inter (set.minus UNIVERALSET b) (set.minus UNIVERALSET c)))) n)) (check-sat) diff --git a/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 b/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 index fd3bd62eb..f57837d05 100644 --- a/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 +++ b/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 @@ -2,6 +2,6 @@ (set-info :status unsat) (declare-fun st1 () (Set Int)) (declare-fun st7 () (Set Int)) -(assert (> 0 (set.card (set.intersection st1 (set.union st7 st1))))) +(assert (> 0 (set.card (set.inter st1 (set.union st7 st1))))) (assert (set.subset st1 st7)) (check-sat) diff --git a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 index bc2f103d2..55b4ac581 100644 --- a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 +++ b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 @@ -2,7 +2,7 @@ (set-info :status unsat) (declare-fun st3 () (Set String)) (declare-fun st9 () (Set String)) -(assert (set.is_singleton (set.intersection st3 st9))) -(assert (< 1 (set.card (set.intersection st3 st9)))) +(assert (set.is_singleton (set.inter st3 st9))) +(assert (< 1 (set.card (set.inter st3 st9)))) (assert (set.is_singleton st9)) (check-sat) diff --git a/test/regress/regress1/sets/issue4391-card-lasso.smt2 b/test/regress/regress1/sets/issue4391-card-lasso.smt2 index f7a720436..76e27f5b0 100644 --- a/test/regress/regress1/sets/issue4391-card-lasso.smt2 +++ b/test/regress/regress1/sets/issue4391-card-lasso.smt2 @@ -11,6 +11,6 @@ (assert (= (set.card b) d)) (assert (= (set.card c) 0)) (assert (= 0 (mod 0 d))) -(assert (> (set.card (set.minus e (set.intersection (set.intersection e b) (set.minus e c)))) 1)) +(assert (> (set.card (set.minus e (set.inter (set.inter e b) (set.minus e c)))) 1)) (check-sat) diff --git a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 index ae71a1edb..a5ee519f5 100644 --- a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 +++ b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 @@ -27,7 +27,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/remove_check_free_31_6.smt2 b/test/regress/regress1/sets/remove_check_free_31_6.smt2 index c2ff1da23..9c2bc9be7 100644 --- a/test/regress/regress1/sets/remove_check_free_31_6.smt2 +++ b/test/regress/regress1/sets/remove_check_free_31_6.smt2 @@ -230,7 +230,7 @@ (assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0)) :named invariant_18_4_69)) -(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_27$0 sk_?X_28$0)) +(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_27$0 sk_?X_28$0)) :named invariant_18_4_70)) (assert (! (= Alloc$0 (set.union FP_Caller$0 Alloc$0)) @@ -246,7 +246,7 @@ (assert (! (= FP_2$0 (set.union (set.minus FP$0 FP_1$0) - (set.union (set.intersection Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0)))) + (set.union (set.inter Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0)))) :named framecondition_of_remove_loop_18_4_17)) (assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0) @@ -311,7 +311,7 @@ (assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74)) -(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_32$0 sk_?X_31$0)) +(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_32$0 sk_?X_31$0)) :named invariant_18_4_75)) (assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76)) @@ -320,7 +320,7 @@ :named invariant_18_4_77)) (assert (! (= sk_?X_29$0 - (set.union (set.intersection Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0))) + (set.union (set.inter Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0))) :named invariant_18_4_78)) (assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) diff --git a/test/regress/regress1/sym/sym5.smt2 b/test/regress/regress1/sym/sym5.smt2 index cf9cbe092..16b44d115 100644 --- a/test/regress/regress1/sym/sym5.smt2 +++ b/test/regress/regress1/sym/sym5.smt2 @@ -13,6 +13,6 @@ (assert (set.subset A (set.insert g h i (set.singleton f)))) (assert (= C (set.minus A B) )) (assert (set.subset B A)) -(assert (= C (set.intersection A B))) +(assert (= C (set.inter A B))) (assert (set.member j C)) (check-sat) diff --git a/test/regress/regress1/trim.cvc.smt2 b/test/regress/regress1/trim.cvc.smt2 index f05e08572..d823e565d 100644 --- a/test/regress/regress1/trim.cvc.smt2 +++ b/test/regress/regress1/trim.cvc.smt2 @@ -18,9 +18,9 @@ (declare-fun ic0_c () (Set myType)) (assert (forall ((r myType)) (=> (set.member r ic0_i) (forall ((r2 myType)) (=> (set.member r2 (neg (select d r))) (set.member r2 ic0_c)))))) (assert (set.subset (set.singleton A) ic0_i)) -(assert (or (exists ((e0 myType)) (=> (set.member e0 ic0_i) (set.subset (select l A) (select l e0)))) (set.subset (set.intersection ic0_i ic0_c) emptymyTypeSet))) +(assert (or (exists ((e0 myType)) (=> (set.member e0 ic0_i) (set.subset (select l A) (select l e0)))) (set.subset (set.inter ic0_i ic0_c) emptymyTypeSet))) (declare-fun ic1_i () (Set myType)) (declare-fun ic1_c () (Set myType)) (assert (forall ((r myType)) (=> (set.member r (pos (select d B))) (set.member r ic1_i)))) -(assert (or (exists ((e1 myType)) (=> (set.member e1 ic1_i) (set.subset (select l B) (select l e1)))) (set.subset (set.intersection ic1_i ic1_c) emptymyTypeSet))) +(assert (or (exists ((e1 myType)) (=> (set.member e1 ic1_i) (set.subset (select l B) (select l e1)))) (set.subset (set.inter ic1_i ic1_c) emptymyTypeSet))) (check-sat) diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 11c2e8514..9be9dcefa 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -70,7 +70,11 @@ macro(cvc5_add_unit_test is_white name output_dir) if("${output_dir}" STREQUAL "") set(test_name unit/${name}) else() - set(test_name unit/${output_dir}/${name}) + if("${output_dir}" STREQUAL "api") + set(test_name unit/${output_dir}/cpp/${name}) + else() + set(test_name unit/${output_dir}/${name}) + endif() endif() add_test(${test_name} ${test_bin_dir}/${name}) set_tests_properties(${test_name} PROPERTIES LABELS "unit") diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index ae6db51ef..0701c3ca6 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -13,17 +13,10 @@ # The build system configuration. ## -# Add unit tests. -cvc5_add_unit_test_black(datatype_api_black api) -cvc5_add_unit_test_black(grammar_black api) -cvc5_add_unit_test_black(op_black api) -cvc5_add_unit_test_white(op_white api) -cvc5_add_unit_test_black(result_black api) -cvc5_add_unit_test_black(solver_black api) -cvc5_add_unit_test_white(solver_white api) -cvc5_add_unit_test_black(sort_black api) -cvc5_add_unit_test_black(term_black api) -cvc5_add_unit_test_white(term_white api) +add_subdirectory(cpp) +if (BUILD_BINDINGS_PYTHON) + add_subdirectory(python) +endif() if (BUILD_BINDINGS_JAVA) add_subdirectory(java) endif() diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt new file mode 100644 index 000000000..e99732ca4 --- /dev/null +++ b/test/unit/api/cpp/CMakeLists.txt @@ -0,0 +1,24 @@ +############################################################################### +# Top contributors (to current version): +# Aina Niemetz +# +# 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 build system configuration. +## +cvc5_add_unit_test_black(datatype_api_black api) +cvc5_add_unit_test_black(grammar_black api) +cvc5_add_unit_test_black(op_black api) +cvc5_add_unit_test_white(op_white api) +cvc5_add_unit_test_black(result_black api) +cvc5_add_unit_test_black(solver_black api) +cvc5_add_unit_test_white(solver_white api) +cvc5_add_unit_test_black(sort_black api) +cvc5_add_unit_test_black(term_black api) +cvc5_add_unit_test_white(term_white api) diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index 745abc17c..745abc17c 100644 --- a/test/unit/api/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/cpp/grammar_black.cpp index 7b7556539..7b7556539 100644 --- a/test/unit/api/grammar_black.cpp +++ b/test/unit/api/cpp/grammar_black.cpp diff --git a/test/unit/api/op_black.cpp b/test/unit/api/cpp/op_black.cpp index fd45b1c22..fd45b1c22 100644 --- a/test/unit/api/op_black.cpp +++ b/test/unit/api/cpp/op_black.cpp diff --git a/test/unit/api/op_white.cpp b/test/unit/api/cpp/op_white.cpp index 39952739b..39952739b 100644 --- a/test/unit/api/op_white.cpp +++ b/test/unit/api/cpp/op_white.cpp diff --git a/test/unit/api/result_black.cpp b/test/unit/api/cpp/result_black.cpp index 9bf6b8491..9bf6b8491 100644 --- a/test/unit/api/result_black.cpp +++ b/test/unit/api/cpp/result_black.cpp diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 79a4aa63e..51a0f38b5 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -15,8 +15,8 @@ #include <algorithm> -#include "test_api.h" #include "base/output.h" +#include "test_api.h" namespace cvc5 { @@ -341,9 +341,12 @@ TEST_F(TestApiBlackSolver, mkBitVector) ASSERT_EQ(d_solver.mkBitVector(8, "0101", 2), d_solver.mkBitVector(8, "00000101", 2)); - ASSERT_EQ(d_solver.mkBitVector(4, "-1", 2), d_solver.mkBitVector(4, "1111", 2)); - ASSERT_EQ(d_solver.mkBitVector(4, "-1", 16), d_solver.mkBitVector(4, "1111", 2)); - ASSERT_EQ(d_solver.mkBitVector(4, "-1", 10), d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 2), + d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 16), + d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 10), + d_solver.mkBitVector(4, "1111", 2)); ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101"); ASSERT_EQ(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111"); ASSERT_EQ(d_solver.mkBitVector(8, "-1", 10), @@ -592,12 +595,11 @@ TEST_F(TestApiBlackSolver, mkReal) ASSERT_NO_THROW(d_solver.mkReal(val4, val4)); } -TEST_F(TestApiBlackSolver, mkRegexpNone) +TEST_F(TestApiBlackSolver, mkRegexpAll) { Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); - ASSERT_NO_THROW( - d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); + ASSERT_NO_THROW(d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll())); } TEST_F(TestApiBlackSolver, mkRegexpAllchar) @@ -608,6 +610,14 @@ TEST_F(TestApiBlackSolver, mkRegexpAllchar) d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar())); } +TEST_F(TestApiBlackSolver, mkRegexpNone) +{ + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkConst(strSort, "s"); + ASSERT_NO_THROW( + d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); +} + TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); } TEST_F(TestApiBlackSolver, mkSepNil) @@ -1351,7 +1361,8 @@ TEST_F(TestApiBlackSolver, getOptionInfo) api::OptionInfo info = d_solver.getOptionInfo("verbosity"); EXPECT_EQ("verbosity", info.name); EXPECT_EQ(std::vector<std::string>{}, info.aliases); - EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(info.valueInfo)); + EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>( + info.valueInfo)); auto numInfo = std::get<OptionInfo::NumberInfo<int64_t>>(info.valueInfo); EXPECT_EQ(0, numInfo.defaultValue); EXPECT_EQ(0, numInfo.currentValue); @@ -1362,7 +1373,8 @@ TEST_F(TestApiBlackSolver, getOptionInfo) auto info = d_solver.getOptionInfo("random-freq"); ASSERT_EQ(info.name, "random-freq"); ASSERT_EQ(info.aliases, std::vector<std::string>{"random-frequency"}); - ASSERT_TRUE(std::holds_alternative<api::OptionInfo::NumberInfo<double>>(info.valueInfo)); + ASSERT_TRUE(std::holds_alternative<api::OptionInfo::NumberInfo<double>>( + info.valueInfo)); auto ni = std::get<api::OptionInfo::NumberInfo<double>>(info.valueInfo); ASSERT_EQ(ni.currentValue, 0.0); ASSERT_EQ(ni.defaultValue, 0.0); @@ -2540,7 +2552,6 @@ TEST_F(TestApiBlackSolver, Output) ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf()); } - TEST_F(TestApiBlackSolver, issue7000) { Sort s1 = d_solver.getIntegerSort(); diff --git a/test/unit/api/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp index 5d7b9eacf..5d7b9eacf 100644 --- a/test/unit/api/solver_white.cpp +++ b/test/unit/api/cpp/solver_white.cpp diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index d0c755cf7..d0c755cf7 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp diff --git a/test/unit/api/term_black.cpp b/test/unit/api/cpp/term_black.cpp index 9e52174b4..c76182e47 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -212,6 +212,21 @@ TEST_F(TestApiBlackTerm, getOp) ASSERT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children)); } +TEST_F(TestApiBlackTerm, hasGetSymbol) +{ + Term n; + Term t = d_solver.mkBoolean(true); + Term c = d_solver.mkConst(d_solver.getBooleanSort(), "|\\|"); + + ASSERT_THROW(n.hasSymbol(), CVC5ApiException); + ASSERT_FALSE(t.hasSymbol()); + ASSERT_TRUE(c.hasSymbol()); + + ASSERT_THROW(n.getSymbol(), CVC5ApiException); + ASSERT_THROW(t.getSymbol(), CVC5ApiException); + ASSERT_EQ(c.getSymbol(), "|\\|"); +} + TEST_F(TestApiBlackTerm, isNull) { Term x; @@ -807,10 +822,12 @@ TEST_F(TestApiBlackTerm, getReal) ASSERT_EQ((std::pair<int64_t, uint64_t>(127, 10)), real5.getReal64Value()); ASSERT_EQ("127/10", real5.getRealValue()); - ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)), real6.getReal64Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)), + real6.getReal64Value()); ASSERT_EQ("1/4294967297", real6.getRealValue()); - ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)), real7.getReal64Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)), + real7.getReal64Value()); ASSERT_EQ("4294967297/1", real7.getRealValue()); ASSERT_EQ("1/18446744073709551617", real8.getRealValue()); diff --git a/test/unit/api/term_white.cpp b/test/unit/api/cpp/term_white.cpp index ace5645dc..ace5645dc 100644 --- a/test/unit/api/term_white.cpp +++ b/test/unit/api/cpp/term_white.cpp diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 161854421..6a08d79c6 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -639,6 +639,13 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); } + @Test void mkRegexpAll() + { + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkConst(strSort, "s"); + assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll())); + } + @Test void mkRegexpAllchar() { Sort strSort = d_solver.getStringSort(); diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index bf0beb024..b7f111428 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -219,6 +219,21 @@ class TermTest Term nilOpTerm = list.getConstructorTerm("nil"); } + @Test void hasGetSymbol() throws CVC5ApiException + { + Term n = d_solver.getNullTerm(); + Term t = d_solver.mkBoolean(true); + Term c = d_solver.mkConst(d_solver.getBooleanSort(), "|\\|"); + + assertThrows(CVC5ApiException.class, () -> n.hasSymbol()); + assertFalse(t.hasSymbol()); + assertTrue(c.hasSymbol()); + + assertThrows(CVC5ApiException.class, () -> n.getSymbol()); + assertThrows(CVC5ApiException.class, () -> t.getSymbol()); + assertEquals(c.getSymbol(), "|\\|"); + } + @Test void isNull() throws CVC5ApiException { Term x = d_solver.getNullTerm(); diff --git a/test/unit/api/python/CMakeLists.txt b/test/unit/api/python/CMakeLists.txt new file mode 100644 index 000000000..cbf9629ce --- /dev/null +++ b/test/unit/api/python/CMakeLists.txt @@ -0,0 +1,40 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Aina Niemetz, Mathias Preiner +# +# 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 build system configuration. +## + +# Check if the pytest Python module is installed. +check_python_module("pytest") + +# Add Python bindings API tests. +macro(cvc5_add_python_api_unit_test name filename) +# We create test target 'python/unit/api/myapitest' and run it with +# 'ctest -R "python/unit/api/myapitest"'. + set(test_name unit/api/python/${name}) + add_test (NAME ${test_name} + COMMAND ${PYTHON_EXECUTABLE} + -m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename} + # directory for importing the python bindings + WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python) + set_tests_properties(${test_name} PROPERTIES LABELS "unit") +endmacro() + +# add specific test files +cvc5_add_python_api_unit_test(pytest_solver test_solver.py) +cvc5_add_python_api_unit_test(pytest_sort test_sort.py) +cvc5_add_python_api_unit_test(pytest_term test_term.py) +cvc5_add_python_api_unit_test(pytest_datatype_api test_datatype_api.py) +cvc5_add_python_api_unit_test(pytest_grammar test_grammar.py) +cvc5_add_python_api_unit_test(pytest_to_python_obj test_to_python_obj.py) +cvc5_add_python_api_unit_test(pytest_op test_op.py) +cvc5_add_python_api_unit_test(pytest_result test_result.py) diff --git a/test/python/unit/api/__init__.py b/test/unit/api/python/__init__.py index e69de29bb..e69de29bb 100644 --- a/test/python/unit/api/__init__.py +++ b/test/unit/api/python/__init__.py diff --git a/test/python/unit/api/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index d8a4c26f7..d8a4c26f7 100644 --- a/test/python/unit/api/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py diff --git a/test/python/unit/api/test_grammar.py b/test/unit/api/python/test_grammar.py index db567a6ba..db567a6ba 100644 --- a/test/python/unit/api/test_grammar.py +++ b/test/unit/api/python/test_grammar.py diff --git a/test/python/unit/api/test_op.py b/test/unit/api/python/test_op.py index 5126a481d..5126a481d 100644 --- a/test/python/unit/api/test_op.py +++ b/test/unit/api/python/test_op.py diff --git a/test/python/unit/api/test_result.py b/test/unit/api/python/test_result.py index bd97646f9..bd97646f9 100644 --- a/test/python/unit/api/test_result.py +++ b/test/unit/api/python/test_result.py diff --git a/test/python/unit/api/test_solver.py b/test/unit/api/python/test_solver.py index 71ab17465..89e99bd9e 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -643,13 +643,19 @@ def test_mk_real(solver): solver.mkReal(val4, val4) -def test_mk_regexp_empty(solver): +def test_mk_regexp_none(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpNone()) -def test_mk_regexp_sigma(solver): +def test_mk_regexp_all(solver): + strSort = solver.getStringSort() + s = solver.mkConst(strSort, "s") + solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAll()) + + +def test_mk_regexp_allchar(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAllchar()) diff --git a/test/python/unit/api/test_sort.py b/test/unit/api/python/test_sort.py index 98cf76d76..98cf76d76 100644 --- a/test/python/unit/api/test_sort.py +++ b/test/unit/api/python/test_sort.py diff --git a/test/python/unit/api/test_term.py b/test/unit/api/python/test_term.py index 34a79d597..49314638f 100644 --- a/test/python/unit/api/test_term.py +++ b/test/unit/api/python/test_term.py @@ -208,6 +208,23 @@ def test_get_op(solver): assert headTerm == solver.mkTerm(headTerm.getOp(), children) +def test_has_get_symbol(solver): + n = Term(solver) + t = solver.mkBoolean(True) + c = solver.mkConst(solver.getBooleanSort(), "|\\|") + + with pytest.raises(RuntimeError): + n.hasSymbol() + assert not t.hasSymbol() + assert c.hasSymbol() + + with pytest.raises(RuntimeError): + n.getSymbol() + with pytest.raises(RuntimeError): + t.getSymbol() + assert c.getSymbol() == "|\\|" + + def test_is_null(solver): x = Term(solver) assert x.isNull() diff --git a/test/python/unit/api/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py index bb30fae8f..bb30fae8f 100644 --- a/test/python/unit/api/test_to_python_obj.py +++ b/test/unit/api/python/test_to_python_obj.py |