diff options
56 files changed, 322 insertions, 120 deletions
diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml index 67b5f6b4a..f56a0f595 100644 --- a/.github/workflows/docs_cleanup.yml +++ b/.github/workflows/docs_cleanup.yml @@ -4,8 +4,9 @@ on: - cron: '0 1 * * SUN' jobs: - build: + docs-cleanup: runs-on: ubuntu-latest + if: github.repository == 'cvc5/cvc5' steps: - name: Install Packages run: | @@ -58,6 +59,11 @@ jobs: python3 genindex.py git add README.md - git commit -m "Update README.md" + if git diff --cached --exit-code + then + echo "Nothing changed" + else + git commit -m "Update README.md" + fi git push -f diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml index 356337de6..7346371e3 100644 --- a/.github/workflows/docs_upload.yml +++ b/.github/workflows/docs_upload.yml @@ -75,15 +75,21 @@ jobs: if [ -n "$NAME" ]; then mv docs-new target/docs-$NAME-$HASH cd target/ - rm -f docs-$NAME - ln -s docs-$NAME-$HASH docs-$NAME - git add docs-$NAME docs-$NAME-$HASH - python3 genindex.py - git add README.md - git commit -m "Update docs for $NAME" + if diff -r target/docs-master/ target/docs-$NAME-$HASH + then + echo "Ignored run, documentation is the same as for current master" + else + rm -f docs-$NAME + ln -s docs-$NAME-$HASH docs-$NAME + git add docs-$NAME docs-$NAME-$HASH - git push + python3 genindex.py + git add README.md + git commit -m "Update docs for $NAME" + + git push + fi else echo "Ignored run" fi diff --git a/CMakeLists.txt b/CMakeLists.txt index 1c6ad1604..d7512e874 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -503,7 +503,6 @@ endif() # Add subdirectories add_subdirectory(src) -add_subdirectory(test) if(BUILD_BINDINGS_PYTHON) set(BUILD_BINDINGS_PYTHON_VERSION ${PYTHON_VERSION_MAJOR}) @@ -519,6 +518,8 @@ if(BUILD_DOCS) add_subdirectory(docs) endif() +add_subdirectory(test) + #-----------------------------------------------------------------------------# # Package configuration # diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt index 99c4f3ab3..11c4b8dfd 100644 --- a/docs/CMakeLists.txt +++ b/docs/CMakeLists.txt @@ -25,34 +25,38 @@ set(SPHINX_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/sphinx) configure_file(conf.py.in ${CMAKE_CURRENT_BINARY_DIR}/conf.py) -add_custom_target(docs ALL - DEPENDS docs-cpp docs-python gen-options - COMMAND - ${SPHINX_EXECUTABLE} -b html - -c ${CMAKE_CURRENT_BINARY_DIR} - # Tell Breathe where to find the Doxygen output - -Dbreathe_projects.cvc5=${CPP_DOXYGEN_XML_FOLDER} - -Dbreathe_projects.std=${CPP_DOXYGEN_XML_FOLDER} - ${SPHINX_INPUT_DIR} ${SPHINX_OUTPUT_DIR} - WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR} - COMMENT "Generating Sphinx Api docs") +add_custom_target( + docs ALL + DEPENDS docs-cpp docs-python gen-options + COMMAND + ${SPHINX_EXECUTABLE} -b html -c ${CMAKE_CURRENT_BINARY_DIR} + # Tell Breathe where to find the Doxygen output + -Dbreathe_projects.cvc5=${CPP_DOXYGEN_XML_FOLDER} + -Dbreathe_projects.std=${CPP_DOXYGEN_XML_FOLDER} ${SPHINX_INPUT_DIR} + ${SPHINX_OUTPUT_DIR} + WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR} + COMMENT "Generating Sphinx Api docs" +) set(SPHINX_GH_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/sphinx-gh) -add_custom_target(docs-gh ALL - DEPENDS docs - COMMAND ${CMAKE_COMMAND} -E remove_directory - ${SPHINX_GH_OUTPUT_DIR} - COMMAND ${CMAKE_COMMAND} -E copy_directory - ${SPHINX_OUTPUT_DIR} ${SPHINX_GH_OUTPUT_DIR} - COMMAND ${CMAKE_COMMAND} -E remove_directory - ${SPHINX_GH_OUTPUT_DIR}/_sources - COMMAND ${CMAKE_COMMAND} -E remove - ${SPHINX_GH_OUTPUT_DIR}/objects.inv - COMMAND ${CMAKE_COMMAND} -E rename - ${SPHINX_GH_OUTPUT_DIR}/_static - ${SPHINX_GH_OUTPUT_DIR}/static - COMMAND find ${SPHINX_GH_OUTPUT_DIR} -type f | - xargs sed -i'orig' 's/_static/static/' - COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete - COMMENT "Generating GitHub Api docs") - +add_custom_target( + docs-gh ALL + DEPENDS docs + # remove existing sphinx-gh/ directory + COMMAND ${CMAKE_COMMAND} -E remove_directory ${SPHINX_GH_OUTPUT_DIR} + # copy sphinx/ to sphinx-gh/ + COMMAND ${CMAKE_COMMAND} -E copy_directory ${SPHINX_OUTPUT_DIR} + ${SPHINX_GH_OUTPUT_DIR} + # remove leftovers from the build + COMMAND ${CMAKE_COMMAND} -E remove_directory ${SPHINX_GH_OUTPUT_DIR}/.doctrees + ${SPHINX_GH_OUTPUT_DIR}/_sources ${SPHINX_GH_OUTPUT_DIR}/_static/fonts + COMMAND ${CMAKE_COMMAND} -E remove ${SPHINX_GH_OUTPUT_DIR}/objects.inv + # rename _static/ to static/ (as jekyll ignores _*/ dirs) + COMMAND ${CMAKE_COMMAND} -E rename ${SPHINX_GH_OUTPUT_DIR}/_static + ${SPHINX_GH_OUTPUT_DIR}/static + COMMAND find ${SPHINX_GH_OUTPUT_DIR} -type f | xargs sed -i'orig' + 's/_static/static/' + COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete + # done + COMMENT "Generating GitHub Api docs" +) diff --git a/docs/_static/custom.css b/docs/_static/custom.css index 81ecdc936..032efba56 100644 --- a/docs/_static/custom.css +++ b/docs/_static/custom.css @@ -32,7 +32,19 @@ a:hover, a:focus { } .wy-side-nav-search > a { - color: #fcfffa; + color: #ace600; +} + +.wy-side-nav-search > a:hover, > a:focus, > a:visited { + color: #ace600; +} + +.wy-breadcrumbs a { + color: #739900; +} + +.wy-breadcrumbs a:hover, a:focus { + color: #0099e6; } .wy-side-nav-search input[type="text"] { @@ -56,10 +68,10 @@ a:hover, a:focus { } .wy-nav-top { - color: #fcfffa; + color: #ace600; background-color: #0099e6; } .wy-nav-top a { - color: #fcfffa; + color: #ace600; } diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst new file mode 100644 index 000000000..d28beab14 --- /dev/null +++ b/docs/binary/binary.rst @@ -0,0 +1,7 @@ +Binary Documentation +==================== + +.. toctree:: + :maxdepth: 2 + + options diff --git a/docs/options.rst b/docs/binary/options.rst index 6f9c613e7..6f9c613e7 100644 --- a/docs/options.rst +++ b/docs/binary/options.rst diff --git a/docs/conf.py.in b/docs/conf.py.in index 9dc5255bd..6a23ff759 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -70,6 +70,7 @@ html_css_files = ['custom.css'] # -- Breathe configuration --------------------------------------------------- breathe_default_project = "cvc5" breathe_domain_by_extension = {"h" : "cpp"} +cpp_index_common_prefix = ["cvc5::api::"] # where to look for include-build-file ibf_folders = ['${CMAKE_CURRENT_BINARY_DIR}'] diff --git a/docs/cpp/cpp.rst b/docs/cpp/cpp.rst index a2e928927..8d302d60c 100644 --- a/docs/cpp/cpp.rst +++ b/docs/cpp/cpp.rst @@ -1,3 +1,5 @@ +.. _cpp-api: + C++ API Documentation ===================== diff --git a/docs/examples/bitvectors.rst b/docs/examples/bitvectors.rst new file mode 100644 index 000000000..354c86751 --- /dev/null +++ b/docs/examples/bitvectors.rst @@ -0,0 +1,8 @@ +Theory of Bit-Vectors +===================== + + +.. api-examples:: + ../../examples/api/cpp/bitvectors.cpp + ../../examples/api/java/BitVectors.java + ../../examples/api/python/bitvectors.py diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst new file mode 100644 index 000000000..9d63f36bd --- /dev/null +++ b/docs/examples/bitvectors_and_arrays.rst @@ -0,0 +1,8 @@ +Theory of Bit-Vectors and Arrays +================================ + + +.. api-examples:: + ../../examples/api/cpp/bitvectors_and_arrays.cpp + ../../examples/api/java/BitVectorsAndArrays.java + ../../examples/api/python/bitvectors_and_arrays.py diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst new file mode 100644 index 000000000..5f301a14f --- /dev/null +++ b/docs/examples/combination.rst @@ -0,0 +1,8 @@ +Theory Combination +================== + + +.. api-examples:: + ../../examples/api/cpp/combination.cpp + ../../examples/api/java/Combination.java + ../../examples/api/python/combination.py diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst index 8200ebb14..abbb16964 100644 --- a/docs/examples/datatypes.rst +++ b/docs/examples/datatypes.rst @@ -1,8 +1,8 @@ -Datatypes -=========== +Theory of Datatypes +=================== .. api-examples:: - ../../examples/api/datatypes.cpp + ../../examples/api/cpp/datatypes.cpp ../../examples/api/java/Datatypes.java ../../examples/api/python/datatypes.py diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst index ff3651857..528566a3e 100644 --- a/docs/examples/examples.rst +++ b/docs/examples/examples.rst @@ -1,9 +1,25 @@ Examples =========== +The following examples show how the APIs (:ref:`cpp-api`, :ref:`python-api`) and input languages can be used. +For every example, the same problem is constructed and solved using different input mechanisms. + + .. toctree:: :maxdepth: 2 helloworld + exceptions + bitvectors + bitvectors_and_arrays + extract datatypes - lineararith
\ No newline at end of file + floatingpoint + lineararith + sequences + sets + strings + combination + sygus-fun + sygus-grammar + sygus-inv
\ No newline at end of file diff --git a/docs/examples/exceptions.rst b/docs/examples/exceptions.rst new file mode 100644 index 000000000..6598e8fb0 --- /dev/null +++ b/docs/examples/exceptions.rst @@ -0,0 +1,7 @@ +Exception Handling +====================================== + + +.. api-examples:: + ../../examples/api/java/Exceptions.java + ../../examples/api/python/exceptions.py diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst new file mode 100644 index 000000000..0108de948 --- /dev/null +++ b/docs/examples/extract.rst @@ -0,0 +1,7 @@ +Theory of Bit-Vectors: :code:`extract` +====================================== + + +.. api-examples:: + ../../examples/api/cpp/extract.cpp + ../../examples/api/python/extract.py diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst new file mode 100644 index 000000000..1b09102b2 --- /dev/null +++ b/docs/examples/floatingpoint.rst @@ -0,0 +1,7 @@ +Theory of Floating-Points +====================================== + + +.. api-examples:: + ../../examples/api/java/FloatingPointArith.java + ../../examples/api/python/floating_point.py diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst index 202952bb6..cdc424dfa 100644 --- a/docs/examples/helloworld.rst +++ b/docs/examples/helloworld.rst @@ -5,6 +5,7 @@ This example shows the very basic usage of the API. We create a solver, declare a Boolean variable and check whether it is entailed (by ``true``, as nothing has been asserted to the solver). .. api-examples:: - ../../examples/api/helloworld.cpp + ../../examples/api/cpp/helloworld.cpp ../../examples/api/java/HelloWorld.java ../../examples/api/python/helloworld.py + ../../examples/api/smtlib/helloworld.smt2 diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst index d772edbb3..29d84cae5 100644 --- a/docs/examples/lineararith.rst +++ b/docs/examples/lineararith.rst @@ -1,8 +1,13 @@ -Linear Arithmetic -================= +Theory of Linear Arithmetic +=========================== +This example asserts three constraints over an integer variable :code:`x` and a real variable :code:`y`. +Firstly, it checks that these constraints entail an upper bound on the difference :code:`y - x <= 2/3`. +Secondly, it checks that this bound is tight by asserting :code:`y - x = 2/3` and checking for satisfiability. +The two checks are separated by using :code:`push` and :code:`pop`. .. api-examples:: - ../../examples/api/linear_arith.cpp + ../../examples/api/cpp/linear_arith.cpp ../../examples/api/java/LinearArith.java ../../examples/api/python/linear_arith.py + ../../examples/api/smtlib/linear_arith.smt2 diff --git a/docs/examples/sequences.rst b/docs/examples/sequences.rst new file mode 100644 index 000000000..a6f9e2238 --- /dev/null +++ b/docs/examples/sequences.rst @@ -0,0 +1,7 @@ +Theory of Sequences +=================== + + +.. api-examples:: + ../../examples/api/cpp/sequences.cpp + ../../examples/api/python/sequences.py diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst new file mode 100644 index 000000000..71a6843c3 --- /dev/null +++ b/docs/examples/sets.rst @@ -0,0 +1,7 @@ +Theory of Sets +================= + + +.. api-examples:: + ../../examples/api/cpp/sets.cpp + ../../examples/api/python/sets.py diff --git a/docs/examples/strings.rst b/docs/examples/strings.rst new file mode 100644 index 000000000..87f566363 --- /dev/null +++ b/docs/examples/strings.rst @@ -0,0 +1,8 @@ +Theory of Strings +================= + + +.. api-examples:: + ../../examples/api/cpp/strings.cpp + ../../examples/api/java/Strings.java + ../../examples/api/python/strings.py diff --git a/docs/examples/sygus-fun.rst b/docs/examples/sygus-fun.rst new file mode 100644 index 000000000..3d5bddff1 --- /dev/null +++ b/docs/examples/sygus-fun.rst @@ -0,0 +1,7 @@ +SyGuS: Functions +=================== + + +.. api-examples:: + ../../examples/api/cpp/sygus-fun.cpp + ../../examples/api/python/sygus-fun.py diff --git a/docs/examples/sygus-grammar.rst b/docs/examples/sygus-grammar.rst new file mode 100644 index 000000000..3733fe2c3 --- /dev/null +++ b/docs/examples/sygus-grammar.rst @@ -0,0 +1,7 @@ +SyGuS: Grammars +=================== + + +.. api-examples:: + ../../examples/api/cpp/sygus-grammar.cpp + ../../examples/api/python/sygus-grammar.py diff --git a/docs/examples/sygus-inv.rst b/docs/examples/sygus-inv.rst new file mode 100644 index 000000000..f9698a720 --- /dev/null +++ b/docs/examples/sygus-inv.rst @@ -0,0 +1,7 @@ +SyGuS: Invariants +=================== + + +.. api-examples:: + ../../examples/api/cpp/sygus-inv.cpp + ../../examples/api/python/sygus-inv.py diff --git a/docs/ext/examples.py b/docs/ext/examples.py index befb6c175..003726de4 100644 --- a/docs/ext/examples.py +++ b/docs/ext/examples.py @@ -22,6 +22,7 @@ class APIExamples(Directive): '.cpp': {'title': 'C++', 'lang': 'c++'}, '.java': {'title': 'Java', 'lang': 'java'}, '.py': {'title': 'Python', 'lang': 'python'}, + '.smt2': {'title': 'SMT-LIBv2', 'lang': 'lisp'}, } # The "arguments" are actually the content of the directive diff --git a/docs/genindex.rst b/docs/genindex.rst new file mode 100644 index 000000000..9e530fa2f --- /dev/null +++ b/docs/genindex.rst @@ -0,0 +1,2 @@ +Index +===== diff --git a/docs/index.rst b/docs/index.rst index 8d77790fb..fc82111e2 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -6,17 +6,13 @@ cvc5 API Documentation ====================== - -* :ref:`genindex` - - ---------------- - .. toctree:: :maxdepth: 1 + installation/installation + binary/binary cpp/cpp python/python - references examples/examples - options + references + genindex diff --git a/docs/installation/installation.rst b/docs/installation/installation.rst new file mode 100644 index 000000000..e50cd8d4b --- /dev/null +++ b/docs/installation/installation.rst @@ -0,0 +1,2 @@ +Installation +============
\ No newline at end of file diff --git a/docs/python/python.rst b/docs/python/python.rst index 50d9077df..c3e425a7f 100644 --- a/docs/python/python.rst +++ b/docs/python/python.rst @@ -1,3 +1,5 @@ +.. _python-api: + Python API Documentation ======================== diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index a7ca31a7a..076715f2e 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -78,7 +78,7 @@ cvc5_add_example(simple_vc_quant_cxx "" "") # # argument to binary (for testing) # ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2) -add_subdirectory(api) +add_subdirectory(api/cpp) # TODO(project issue $206): Port example to new API # add_subdirectory(nra-translate) # add_subdirectory(sets-translate) diff --git a/examples/api/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt index bff7caa4d..bff7caa4d 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/cpp/CMakeLists.txt diff --git a/examples/api/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp index 8768bd996..8768bd996 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/cpp/bitvectors.cpp diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/cpp/bitvectors_and_arrays.cpp index 547b294a0..547b294a0 100644 --- a/examples/api/bitvectors_and_arrays.cpp +++ b/examples/api/cpp/bitvectors_and_arrays.cpp diff --git a/examples/api/combination.cpp b/examples/api/cpp/combination.cpp index d47897a7c..d47897a7c 100644 --- a/examples/api/combination.cpp +++ b/examples/api/cpp/combination.cpp diff --git a/examples/api/datatypes.cpp b/examples/api/cpp/datatypes.cpp index 76c6da0f0..76c6da0f0 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/cpp/datatypes.cpp diff --git a/examples/api/extract.cpp b/examples/api/cpp/extract.cpp index d21c59d59..d21c59d59 100644 --- a/examples/api/extract.cpp +++ b/examples/api/cpp/extract.cpp diff --git a/examples/api/helloworld.cpp b/examples/api/cpp/helloworld.cpp index 21eb8e8fc..21eb8e8fc 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/cpp/helloworld.cpp diff --git a/examples/api/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp index 02ddd956c..02ddd956c 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/cpp/linear_arith.cpp diff --git a/examples/api/sequences.cpp b/examples/api/cpp/sequences.cpp index 5ee66048f..5ee66048f 100644 --- a/examples/api/sequences.cpp +++ b/examples/api/cpp/sequences.cpp diff --git a/examples/api/sets.cpp b/examples/api/cpp/sets.cpp index 5c9652707..5c9652707 100644 --- a/examples/api/sets.cpp +++ b/examples/api/cpp/sets.cpp diff --git a/examples/api/strings.cpp b/examples/api/cpp/strings.cpp index a952b31d1..a952b31d1 100644 --- a/examples/api/strings.cpp +++ b/examples/api/cpp/strings.cpp diff --git a/examples/api/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp index 0f96e72a7..0f96e72a7 100644 --- a/examples/api/sygus-fun.cpp +++ b/examples/api/cpp/sygus-fun.cpp diff --git a/examples/api/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp index ce5a1bc8b..ce5a1bc8b 100644 --- a/examples/api/sygus-grammar.cpp +++ b/examples/api/cpp/sygus-grammar.cpp diff --git a/examples/api/sygus-inv.cpp b/examples/api/cpp/sygus-inv.cpp index f658fa33a..f658fa33a 100644 --- a/examples/api/sygus-inv.cpp +++ b/examples/api/cpp/sygus-inv.cpp diff --git a/examples/api/utils.cpp b/examples/api/cpp/utils.cpp index 69676819a..69676819a 100644 --- a/examples/api/utils.cpp +++ b/examples/api/cpp/utils.cpp diff --git a/examples/api/utils.h b/examples/api/cpp/utils.h index 69cddee26..69cddee26 100644 --- a/examples/api/utils.h +++ b/examples/api/cpp/utils.h diff --git a/examples/api/smtlib/helloworld.smt2 b/examples/api/smtlib/helloworld.smt2 new file mode 100644 index 000000000..b33689bb7 --- /dev/null +++ b/examples/api/smtlib/helloworld.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_UF) +(declare-const |Hello World!| Bool) +(assert (not |Hello World!|)) +(check-sat) diff --git a/examples/api/smtlib/linear_arith.smt2 b/examples/api/smtlib/linear_arith.smt2 new file mode 100644 index 000000000..ede655b0e --- /dev/null +++ b/examples/api/smtlib/linear_arith.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_LIRA) +(declare-const x Int) +(declare-const y Real) +(assert + (and + (>= x (* 3 y)) + (<= x y) + (< (- 2) x) + ) +) +(push 1) +(echo "Checking entailement by asserting the negation") +(echo "Unsat == ENTAILED") +(assert (not (<= (- y x) (/ 2 3)))) +(check-sat) +(pop 1) +(push 1) +(echo "Checking that the assertions are consistent") +(assert (= (- y x) (/ 2 3))) +(check-sat) +(pop 1) diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index d56f594ce..53ea46f46 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -112,5 +112,3 @@ add_jar(cvc5jar ) add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5) - -get_target_property(CVC5_JAR_PATH cvc5jar JAR_FILE)
\ No newline at end of file diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 281901c1c..007acc64d 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -95,23 +95,23 @@ private: */ Allocator d_allocator; -protected: + protected: /** * Private copy constructor used only by save(). d_list and * d_sizeAlloc are not copied: only the base class information and * d_size are needed in restore. */ - CDList(const CDList& l) : - ContextObj(l), - d_list(NULL), - d_size(l.d_size), - d_callDestructor(false), - d_sizeAlloc(0), - d_cleanUp(l.d_cleanUp), - d_allocator(l.d_allocator) { - Debug("cdlist") << "copy ctor: " << this - << " from " << &l - << " size " << d_size << std::endl; + CDList(const CDList& l) + : ContextObj(l), + d_list(nullptr), + d_size(l.d_size), + d_callDestructor(false), + d_sizeAlloc(0), + d_cleanUp(l.d_cleanUp), + d_allocator(l.d_allocator) + { + Debug("cdlist") << "copy ctor: " << this << " from " << &l << " size " + << d_size << std::endl; } CDList& operator=(const CDList& l) = delete; @@ -132,38 +132,50 @@ protected: Debug("cdlist") << "grow " << this << " " << getContext()->getLevel() << ": grow!" << std::endl; - if(d_list == NULL) { + const size_t maxSize = + std::allocator_traits<AllocatorT>::max_size(d_allocator); + if (d_list == nullptr) + { // Allocate an initial list if one does not yet exist d_sizeAlloc = INITIAL_SIZE; Debug("cdlist") << "initial grow of cdlist " << this << " level " << getContext()->getLevel() << " to " << d_sizeAlloc << std::endl; - if(d_sizeAlloc > d_allocator.max_size()) { - d_sizeAlloc = d_allocator.max_size(); + if (d_sizeAlloc > maxSize) + { + d_sizeAlloc = maxSize; } - d_list = d_allocator.allocate(d_sizeAlloc); - if(d_list == NULL) { + d_list = + std::allocator_traits<AllocatorT>::allocate(d_allocator, d_sizeAlloc); + if (d_list == nullptr) + { throw std::bad_alloc(); } - } else { + } + else + { // Allocate a new array with double the size size_t newSize = GROWTH_FACTOR * d_sizeAlloc; - if(newSize > d_allocator.max_size()) { - newSize = d_allocator.max_size(); + if (newSize > maxSize) + { + newSize = maxSize; Assert(newSize > d_sizeAlloc) << "cannot request larger list due to allocator limits"; } - T* newList = d_allocator.allocate(newSize); + T* newList = + std::allocator_traits<AllocatorT>::allocate(d_allocator, newSize); Debug("cdlist") << "2x grow of cdlist " << this << " level " << getContext()->getLevel() << " to " << newSize << " (from " << d_list << " to " << newList << ")" << std::endl; - if(newList == NULL) { + if (newList == nullptr) + { throw std::bad_alloc(); } std::memcpy(newList, d_list, sizeof(T) * d_sizeAlloc); - d_allocator.deallocate(d_list, d_sizeAlloc); + std::allocator_traits<AllocatorT>::deallocate( + d_allocator, d_list, d_sizeAlloc); d_list = newList; d_sizeAlloc = newSize; } @@ -222,7 +234,8 @@ protected: while(d_size != size) { --d_size; d_cleanUp(&d_list[d_size]); - d_allocator.destroy(&d_list[d_size]); + std::allocator_traits<AllocatorT>::destroy(d_allocator, + &d_list[d_size]); } } else { d_size = size; @@ -231,19 +244,20 @@ protected: public: /** - * Main constructor: d_list starts as NULL, size is 0 + * Main constructor: d_list starts as nullptr, size is 0 */ CDList(Context* context, bool callDestructor = true, const CleanUp& cleanup = CleanUp(), - const Allocator& alloc = Allocator()) : - ContextObj(context), - d_list(NULL), - d_size(0), - d_callDestructor(callDestructor), - d_sizeAlloc(0), - d_cleanUp(cleanup), - d_allocator(alloc) { + const Allocator& alloc = Allocator()) + : ContextObj(context), + d_list(nullptr), + d_size(0), + d_callDestructor(callDestructor), + d_sizeAlloc(0), + d_cleanUp(cleanup), + d_allocator(alloc) + { } /** @@ -256,7 +270,8 @@ protected: truncateList(0); } - this->d_allocator.deallocate(this->d_list, this->d_sizeAlloc); + std::allocator_traits<AllocatorT>::deallocate( + d_allocator, this->d_list, this->d_sizeAlloc); } /** @@ -295,7 +310,8 @@ protected: << ": construct! at " << d_list << "[" << d_size << "] == " << &d_list[d_size] << std::endl; - d_allocator.construct(&d_list[d_size], data); + std::allocator_traits<AllocatorT>::construct( + d_allocator, &d_list[d_size], data); Debug("cdlist") << "push_back " << this << " " << getContext()->getLevel() << ": done..." << std::endl; @@ -355,7 +371,7 @@ protected: * wrapper around a pointer. Note that for efficiency, we implement * only prefix increment and decrement. Also note that it's OK to * create an iterator from an empty, uninitialized list, as begin() - * and end() will have the same value (NULL). + * and end() will have the same value (nullptr). */ class const_iterator { T const* d_it; @@ -374,7 +390,7 @@ protected: typedef const T* pointer; typedef const T& reference; - const_iterator() : d_it(NULL) {} + const_iterator() : d_it(nullptr) {} inline bool operator==(const const_iterator& i) const { return d_it == i.d_it; diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index b17f19acd..ac0e487f9 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -92,7 +92,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) // into fixed length regular expressions are easy to handle. // the index of _* in re unsigned pivotIndex = 0; - size_t numPivotIndex = 0; + bool hasPivotIndex = false; + bool hasFixedLength = true; std::vector<Node> childLengths; std::vector<Node> childLengthsPostPivot; for (unsigned i = 0, size = children.size(); i < size; i++) @@ -101,34 +102,34 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node fl = RegExpEntail::getFixedLengthForRegexp(c); if (fl.isNull()) { - if (numPivotIndex == 0 && c.getKind() == REGEXP_STAR + if (!hasPivotIndex && c.getKind() == REGEXP_STAR && c[0].getKind() == REGEXP_SIGMA) { - numPivotIndex = 1; + hasPivotIndex = true; pivotIndex = i; // zero is used in sum below and is used for concat-fixed-len fl = zero; } else { - numPivotIndex++; + hasFixedLength = false; } } if (!fl.isNull()) { childLengths.push_back(fl); - if (numPivotIndex > 0) + if (hasPivotIndex) { childLengthsPostPivot.push_back(fl); } } } - Node lenSum = childLengths.size() > 1 ? nm->mkNode(PLUS, childLengths) - : childLengths[0]; - // if we have at most one pivot index - if (numPivotIndex <= 1) + Node lenSum = childLengths.size() > 1 + ? nm->mkNode(PLUS, childLengths) + : (childLengths.empty() ? zero : childLengths[0]); + // if we have a fixed length + if (hasFixedLength) { - bool hasPivotIndex = (numPivotIndex == 1); Assert(re.getNumChildren() == children.size()); std::vector<Node> conc; conc.push_back(nm->mkNode(hasPivotIndex ? GEQ : EQUAL, lenx, lenSum)); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3d8016379..01deeaede 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2089,6 +2089,7 @@ set(regress_1_tests regress1/strings/issue6271-rnf.smt2 regress1/strings/issue6271-2-rnf.smt2 regress1/strings/issue6567-empty-re-range.smt2 + regress1/strings/issue6604-2.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue6604-2.smt2 b/test/regress/regress1/strings/issue6604-2.smt2 new file mode 100644 index 000000000..e28f5dcb5 --- /dev/null +++ b/test/regress/regress1/strings/issue6604-2.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp --re-elim +; EXPECT: unsat +(set-logic ALL) +(declare-const a String) +(assert (str.in_re a (re.++ (str.to_re "A") re.allchar (str.to_re "A")))) +(assert (not (str.in_re a (re.++ (str.to_re "A") (re.* (re.++ (str.to_re "A") re.allchar)) re.allchar (str.to_re "A"))))) +(check-sat) diff --git a/test/unit/api/java/CMakeLists.txt b/test/unit/api/java/CMakeLists.txt index 0ef649b87..fe497ef3b 100644 --- a/test/unit/api/java/CMakeLists.txt +++ b/test/unit/api/java/CMakeLists.txt @@ -17,6 +17,8 @@ find_package(Java REQUIRED) include(UseJava) find_package(JUnit REQUIRED) +get_target_property(CVC5_JAR_PATH cvc5jar JAR_FILE) + # specify source files for junit tests set(java_test_src_files ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/SolverTest.java diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index d7f9a4dc3..617f032ab 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -785,30 +785,30 @@ TEST_F(TestApiBlackTerm, getReal) ASSERT_TRUE(real8.isRealValue()); ASSERT_TRUE(real9.isRealValue()); - ASSERT_EQ(std::make_pair(0, 1u), real1.getReal32Value()); - ASSERT_EQ(std::make_pair(0l, 1ul), real1.getReal64Value()); + ASSERT_EQ((std::pair<int32_t, uint32_t>(0, 1)), real1.getReal32Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(0, 1)), real1.getReal64Value()); ASSERT_EQ("0", real1.getRealValue()); - ASSERT_EQ(std::make_pair(0, 1u), real2.getReal32Value()); - ASSERT_EQ(std::make_pair(0l, 1ul), real2.getReal64Value()); + ASSERT_EQ((std::pair<int32_t, uint32_t>(0, 1)), real2.getReal32Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(0, 1)), real2.getReal64Value()); ASSERT_EQ("0", real2.getRealValue()); - ASSERT_EQ(std::make_pair(-17, 1u), real3.getReal32Value()); - ASSERT_EQ(std::make_pair(-17l, 1ul), real3.getReal64Value()); + ASSERT_EQ((std::pair<int32_t, uint32_t>(-17, 1)), real3.getReal32Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(-17, 1)), real3.getReal64Value()); ASSERT_EQ("-17", real3.getRealValue()); - ASSERT_EQ(std::make_pair(-3, 5u), real4.getReal32Value()); - ASSERT_EQ(std::make_pair(-3l, 5ul), real4.getReal64Value()); + ASSERT_EQ((std::pair<int32_t, uint32_t>(-3, 5)), real4.getReal32Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(-3, 5)), real4.getReal64Value()); ASSERT_EQ("-3/5", real4.getRealValue()); - ASSERT_EQ(std::make_pair(127, 10u), real5.getReal32Value()); - ASSERT_EQ(std::make_pair(127l, 10ul), real5.getReal64Value()); + ASSERT_EQ((std::pair<int32_t, uint32_t>(127, 10)), real5.getReal32Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(127, 10)), real5.getReal64Value()); ASSERT_EQ("127/10", real5.getRealValue()); - ASSERT_EQ(std::make_pair(1l, 4294967297ul), real6.getReal64Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)), real6.getReal64Value()); ASSERT_EQ("1/4294967297", real6.getRealValue()); - ASSERT_EQ(std::make_pair(4294967297l, 1ul), real7.getReal64Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)), real7.getReal64Value()); ASSERT_EQ("4294967297", real7.getRealValue()); ASSERT_EQ("1/18446744073709551617", real8.getRealValue()); |