summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-05-26Add more examples to the documentation (#6569)Gereon Kremer
This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details: - for consistency, all cpp examples are moved from examples/api to examples/api/cpp - add capabilities for SMT-LIB examples, and two simple smt2 examples - more docs/examples/*.rst files - two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)
2021-05-26Ensure proper types in unit tests (#6598)Gereon Kremer
This PR fixes a type mixup (the usual long vs long long mixup on macos systems) in the unit tests for the new api::Term getters. Fixes #6594.
2021-05-26Reduce size of sphinx-gh output (#6601)Gereon Kremer
This PR reduces the disk size of the docs generated by make sphinx-gh. Apart from reformatting the cmake source, we now not only remove the _sources folder, but also .doctrees (essentially the sphinx cache) and _static/fonts/ (the fonts that are actually used live in _static/css/fonts). In combination, this now reduces the disk size from about 20MB (sphinx) to less than 6MB (sphinx-gh). Furthermore this PR only uploads the generated documentation if it differs from whatever we currently have for master. This is relevant to make the docs-ci repository smaller (which already has more than 5GB...)
2021-05-25api docs: Fix and tweak style for home and top links. (#6618)Aina Niemetz
2021-05-25Replace deprecated calls to `std::allocator` (#6606)Andres Noetzli
Fixes #6453. This commit replaces all calls to std::allocator with calls to std::allocator_traits. Strictly speaking, allocate() and deallocate() are not deprecated but the commit replaces them for uniformity.
2021-05-25[Unit tests] Fix path of Java bindings (#6616)Andres Noetzli
Currently, when configuring cvc5 with Java bindings, CMake complains about `get_filename_component(CVC5_JNI_PATH ${CVC5_JAR_PATH} DIRECTORY)` not using the correct number of arguments in the Java unit tests. The issue is that `${CVC5_JAR_PATH}` is empty. The value of `${CVC5_JAR_PATH}` was computed in the Java API bindings but then not shared with the rest of the build system. Because `${CVC5_JAR_PATH}` is not used anywhere else, this commit moves the computation of `${CVC5_JAR_PATH}` to the unit tests. The commit also ensures that the API subdirectories are processed before the test subdirectories.
2021-05-24Fix non-fixed length case in re-elim (#6612)Andrew Reynolds
Fixes followup issues from #6604.
2021-05-24Implementation of the new justification heuristic (#6465)Andrew Reynolds
This adds the new implementation of the justification heuristic. It does not enable this strategy yet. A followup PR will activate this strategy within DecisionEngine.
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/. It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").
2021-05-24Fix re-elim length requirement for symbolic RE memberships (#6609)Andrew Reynolds
Fixes #6604. Previously, re-elim was solution unsound for cases where the LHS and a component of the RHS were both empty. This ensures a length requirement is given for the LHS to ensure proper containment.
2021-05-24Fix instance of no rewrite in extended rewriter (#6610)Andrew Reynolds
Fixes #6545. An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.
2021-05-24Better formalization of regular expression unfolding skolems (#6602)Andrew Reynolds
This replaces our previous formalization of RE unfolding skolems with a more explicit one that is amenable to external proof conversion. It adds a few associated utility methods to SkolemManager required for LFSC proof conversion for RE_UNFOLD_POS. It also changes the order of equalities in the RE_UNFOLD_POS rule, which simplifies LFSC proof checking.
2021-05-21Fix tests of unsat cores (#6593)Andrew Reynolds
This updates all regressions that pass check-unsat-cores to enable check-unsat-cores. This includes any incremental benchmark, which was disabled in run_regression.py previously. It adds --no-check-unsat-cores to a few corner benchmarks that were previously disabled based on --incremental. It also reverts a change to when proofs are disabled: options like sygus-inference should not permit proofs (or unsat cores).
2021-05-21Fix and refactor relevant domain (#6528)Andrew Reynolds
In a handcrafted case, one can make the body of quantified formula another quantified formula when special attributes are used. The relevant domain utility was not robust to this case, leading to instantiations with free variables. This fixes the issue and also updates its style to use a term context stack, which also avoids a tree traversal of the bodies of quantified formulas in this utility. Fixes #6476. The benchmark from that issue now times out.
2021-05-21Formalize shared selectors as skolem functions (#6591)Andrew Reynolds
This is work towards properly printing shared selectors in external proofs.
2021-05-21Minor simplification to boolean proof checker (#6590)Andrew Reynolds
2021-05-21(proof-new) Minor documentation sync (#6592)Andrew Reynolds
2021-05-21Add utility to get all types occurring in a term (#6588)Andrew Reynolds
Required for external proof conversions.
2021-05-21Update to sygus standard output for check-synth responses (#6521)Andrew Reynolds
This PR does two things: (1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model. (2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model. It also removes the unused command GetSynthSolutionCommand.
2021-05-21Support braced-init-lists with `mkNode()` (#6580)Andres Noetzli
This commit adds support for braced-init-lists in calls to `mkNode()`, e.g., `mkNode(REGEXP_EMPTY, {})`. Previously, such a call would result in a node of kind `REGEXP_EMPTY` with a single null node as a child because the compiler chose the `mkNode(Kind kind, TNode child1)` variant and converted `{}` to a node using the default constructor. This commit adds an overload of `mkNode()` that takes an `initializer_list<TNode>` to allow this use case. It also adds a `mkNode()` overload with zero children for convenience and removes the 4- and 5-children variants because they saw little use. Finally, it makes the default constructor of `NodeTemplate` explicit to avoid accidental conversions.
2021-05-21api docs: Tweak and fix style. (#6582)Aina Niemetz
This fixes the style for narrow layouts. It further fixes and improves the style for the menu.
2021-05-21api docs: Update copyright. (#6596)Aina Niemetz
2021-05-21Use scikit-build CMake files for pycvc5 (#6543)makaimann
This PR removes copied CMake files for the pycvc5 Cython target, and instead adds a dependency on scikit-build (where those CMake files originated anyway). This keeps us up to date with fixes. Furthermore, the PR switches from distutils to the more modern setuptools. This does add another dependency but it's a fairly reasonable one. setuptools is not part of the base Python distribution, but my understanding is that it is now the de facto standard, and most package managers install it automatically with Python. The main motivation for switching is in preparation for building wheels. This PR is a piece of this old one (#5657) which I am closing and splitting up.
2021-05-21Move option names out of struct (#6554)Gereon Kremer
This PR moves the option names out of the option struct (which will be removed) to free constexpr string constants.
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-20Update version of CaDiCaL. (#6583)Mathias Preiner
2021-05-20Disable unit testing for clang builds. (#6595)Aina Niemetz
We currently have issues with clang 11 failing for white unit tests. This disables unit tests for clang builds.
2021-05-20Properly initialize. (#6586)Gereon Kremer
This PR fixes a missing initialization that lead to a valgrind warning.
2021-05-20Remove old unsat cores (#6581)Haniel Barbosa
This commit removes the remaining old proof code and the code to produce unsat cores based on it.
2021-05-20Use most recent version of libpoly (#6587)Gereon Kremer
This PR updates to the most recent version of libpoly which fixes some memory leaks.
2021-05-20Avoid using printSynthSolution in the python API and examples (#6564)yoni206
The function printSynthSolution declared here is going to be removed in #6521. This PR removes it from the python API. Following #6530, this PR also replaces its usages in the examples by a utility function. For this, we also add support for getSynthSolutions in the python API.
2021-05-20Minor improvements to the API (#6585)Gereon Kremer
This PR does some minor improvements to the API: - remove getConstSequenceElements(), use getSequenceValue() instead - improve documentation for Term
2021-05-20Fix echo printing. (#6573)Aina Niemetz
Previously, echo surpressed leading, trailing and escape quotes of the string to print. However, the SMT-LIB standard states that the string is to be printed as is, including those quote characters.
2021-05-20Add more getters for api::Term (#6496)Gereon Kremer
This PR adds more getter functions for api::Term to retrieve values from constant terms (and terms that the average API use might consider constant). It also introduces std::wstring as regular representation for string constants instead of std::vector<uint32> for the SMT-LIB parser and the String class.
2021-05-20Expand arith's farkas lemma rule as a macro (#6577)Alex Ozdemir
reflects that it is a macro, which we will eliminate
2021-05-19Remove unused methods from `NodeManager` (#6578)Andres Noetzli
2021-05-19Correctly handle negated assertions for assumption-based unsat cores. (#6579)Mathias Preiner
2021-05-19Pass empty vector when constructing re empty, fixes rewrite (#6576)Andrew Reynolds
Fixes #6567.
2021-05-19Adding python API test part 4 (#6553)Ying Sheng
This commit (follow #6552) adds more unit tests for python API. Subsequent commits will include additional missing functions and unit tests.
2021-05-19Make output list of `mkoptions.py` more accurate (#6572)Andres Noetzli
After commit 6dc5b74, cvc5 was always being almost completely rebuilt, even if there hadn't been any changes if cvc5 was configured not to produce documentation (the default). This was because mkoptions.py only produces the options_generated.rst file when documentation is enabled. However, it was unconditionally declared to be an output of the script in CMakeLists.txt. As a result, the options (and thus most of the code base) were rebuilt every time because the file was missing in builds without documentation. This commit modifies the output list depending on the configuration.
2021-05-19Make strings emp inference an unhandled inference for proofs (#6575)Andrew Reynolds
The strings inference id STRINGS_INFER_EMP is a rare inference that currently leads to a segfault when proof reconstruction is tried for it. This PR makes it unhandled. This was caught by a new regression on the soon-to-be-merged jh-new branch.
2021-05-19Adding regressions that failed on old unsat cores (#6574)Haniel Barbosa
We can thus close #3455, #3651, #4925, #5079, #5238, #5902, #5908, and #5604.
2021-05-19Change the default unsat cores (#6571)Haniel Barbosa
This commit changes the default unsat cores to those based on solving-under-assumptions in the SAT solver and the (new) preprocessing proofs. The evaluation below on all the non-fp non-incremental SMT-LIB benchmarks, 120s timeout, shows the differences of the unsat cores based on the old proofs, the new ones based on SAT assumptions + preprocessing proofs, and the new ones based on SAT and preprocessing proofs. Note that the union of the last two is on par with the first. ``` status total solved sat unsat best timeout memout error uniq disagr time_cpu memory benchmark config AUFDTLIRA newUnsatCoresAssumps-safe/ ee 35 4 0 4 4 7 0 23 2 0 954.0 1267.5 newUnsatCoresProofs ok 35 31 0 31 25 4 0 0 0 0 894.1 1692.9 oldUnsatCores ok 35 32 0 32 30 3 0 0 1 0 799.2 1428.5 AUFLIA newUnsatCoresAssumps-safe/ ok 11 7 0 7 7 4 0 0 7 0 532.2 7604.4 newUnsatCoresProofs ok 11 4 0 4 1 6 0 0 0 0 829.0 12459.8 oldUnsatCores ok 11 4 0 4 3 6 0 0 0 0 818.2 7764.4 AUFLIRA newUnsatCoresAssumps-safe/ to 2 0 0 0 0 2 0 0 0 0 241.6 125.6 newUnsatCoresProofs ok 2 2 0 2 1 0 0 0 0 0 54.2 45.5 oldUnsatCores ok 2 2 0 2 2 0 0 0 0 0 49.4 79.7 AUFNIRA newUnsatCoresAssumps-safe/ ok 10 5 0 5 5 5 0 0 2 0 748.4 1630.0 newUnsatCoresProofs ok 10 4 0 4 0 6 0 0 0 0 850.7 2978.8 oldUnsatCores ok 10 8 0 8 5 2 0 0 1 0 502.7 2048.5 BV newUnsatCoresAssumps-safe/ ok 7 1 1 0 1 6 0 0 1 0 734.2 2065.0 newUnsatCoresProofs ok 7 6 3 3 4 1 0 0 0 0 246.7 1023.9 oldUnsatCores ok 7 6 3 3 3 1 0 0 0 0 248.6 992.0 LIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.9 47.7 newUnsatCoresProofs ok 1 1 0 1 1 0 0 0 0 0 0.3 6.5 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 0.3 5.3 LRA newUnsatCoresAssumps-safe/ ok 5 3 0 3 3 2 0 0 3 0 450.7 260.4 newUnsatCoresProofs ok 5 2 0 2 0 3 0 0 0 0 537.8 424.5 oldUnsatCores ok 5 2 0 2 2 3 0 0 0 0 533.8 298.5 NIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.8 22.0 newUnsatCoresProofs ok 1 1 0 1 0 0 0 0 0 0 46.3 48.0 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 43.3 40.3 QF_ABV newUnsatCoresAssumps-safe/ ok 105 70 59 11 70 35 0 0 63 0 8195.5 19363.3 newUnsatCoresProofs ok 105 34 24 10 17 71 0 0 5 0 11099.5 35756.7 oldUnsatCores ok 105 37 23 14 18 69 0 0 1 0 11198.0 26878.1 QF_ANIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1631.8 newUnsatCoresProofs ok 4 4 3 1 2 0 0 0 0 0 175.1 1513.6 oldUnsatCores ok 4 4 3 1 3 0 0 0 0 0 173.8 1495.1 QF_AUFLIA newUnsatCoresAssumps-safe/ ok 35 6 1 5 6 29 0 0 3 0 3718.4 524.1 newUnsatCoresProofs ok 35 24 4 20 1 11 0 0 0 0 2357.2 36556.0 oldUnsatCores ok 35 32 5 27 29 3 0 0 5 0 1857.6 10067.7 QF_AUFNIA newUnsatCoresAssumps-safe/ ok 3 1 0 1 1 2 0 0 0 0 324.7 543.6 newUnsatCoresProofs ok 3 2 2 0 1 1 0 0 1 0 223.1 509.0 oldUnsatCores ok 3 2 1 1 1 1 0 0 0 0 268.5 484.3 QF_AX newUnsatCoresAssumps-safe/ ok 12 1 0 1 1 11 0 0 0 0 1379.2 391.3 newUnsatCoresProofs ok 12 10 0 10 0 2 0 0 0 0 528.7 7433.9 oldUnsatCores ok 12 12 0 12 11 0 0 0 1 0 343.0 2855.2 QF_BV newUnsatCoresAssumps-safe/ ok 96 56 30 26 49 39 2 0 35 0 9248.2 98058.7 newUnsatCoresProofs ok 96 37 26 11 23 52 7 0 7 0 9781.9 135924.7 oldUnsatCores ok 96 50 29 21 24 43 3 0 7 0 9155.6 107216.0 QF_IDL newUnsatCoresAssumps-safe/ ok 109 51 39 12 43 58 0 0 33 0 10427.2 50846.5 newUnsatCoresProofs ok 109 33 32 1 2 76 0 0 0 0 11692.8 108963.1 oldUnsatCores ok 109 75 55 20 64 34 0 0 26 0 10088.1 53105.6 QF_LIA newUnsatCoresAssumps-safe/ ok 306 155 111 44 138 151 0 0 119 0 25346.4 50556.0 newUnsatCoresProofs ok 306 117 95 22 49 189 0 0 0 0 27092.6 122894.9 oldUnsatCores ok 306 187 110 77 152 119 0 0 34 0 24521.0 61261.1 QF_LRA newUnsatCoresAssumps-safe/ ok 72 39 20 19 38 33 0 0 31 0 7475.3 16892.2 newUnsatCoresProofs ok 72 31 16 15 2 41 0 0 0 0 7569.3 35658.7 oldUnsatCores ok 72 41 18 23 32 31 0 0 2 0 7243.2 20593.9 QF_NIA newUnsatCoresAssumps-safe/ ok 4389 2009 1862 147 2002 903 0 0 1931 0 163975.7 280779.3 newUnsatCoresProofs ok 4389 2326 2156 170 752 792 0 0 37 0 151051.9 387779.8 oldUnsatCores ok 4389 2394 2199 195 2174 730 0 0 81 0 146419.3 259669.8 QF_NRA newUnsatCoresAssumps-safe/ ok 135 65 57 8 57 70 0 0 45 0 10195.7 24701.4 newUnsatCoresProofs ok 135 71 49 22 35 64 0 0 5 0 10825.3 32982.8 oldUnsatCores ok 135 75 54 21 51 61 0 0 9 0 10865.3 27260.9 QF_RDL newUnsatCoresAssumps-safe/ ok 7 5 1 4 5 2 0 0 1 0 564.7 958.4 newUnsatCoresProofs ok 7 1 1 0 0 6 0 0 0 0 842.0 11029.6 oldUnsatCores ok 7 6 1 5 2 1 0 0 1 0 665.8 1982.6 QF_S newUnsatCoresAssumps-safe/ ok 5 1 1 0 0 4 0 0 0 0 603.3 191.4 newUnsatCoresProofs ok 5 5 5 0 2 0 0 0 0 0 161.9 285.8 oldUnsatCores ok 5 4 4 0 3 1 0 0 0 0 225.9 219.3 QF_SLIA newUnsatCoresAssumps-safe/ ok 258 74 67 7 70 184 0 0 64 0 27245.9 20290.4 newUnsatCoresProofs ok 258 179 163 16 47 79 0 0 6 0 18996.0 33722.6 oldUnsatCores ok 258 184 162 22 149 74 0 0 9 0 18395.8 23004.3 QF_UF newUnsatCoresAssumps-safe/ ok 29 25 0 25 6 4 0 0 2 0 2362.4 7504.3 newUnsatCoresProofs ok 29 0 0 0 0 28 1 0 0 0 3508.0 124190.7 oldUnsatCores ok 29 27 0 27 23 2 0 0 4 0 1866.3 13635.1 QF_UFBV newUnsatCoresAssumps-safe/ ok 2 2 0 2 1 0 0 0 1 0 189.5 1599.3 newUnsatCoresProofs to 2 0 0 0 0 2 0 0 0 0 241.8 1818.8 oldUnsatCores ok 2 1 0 1 1 1 0 0 0 0 193.7 1500.9 QF_UFIDL newUnsatCoresAssumps-safe/ ok 9 9 0 9 7 0 0 0 4 0 697.0 1133.0 newUnsatCoresProofs to 9 0 0 0 0 9 0 0 0 0 1088.0 14652.6 oldUnsatCores ok 9 5 0 5 2 4 0 0 0 0 848.5 2079.6 QF_UFLIA newUnsatCoresAssumps-safe/ ok 1 1 0 1 0 0 0 0 0 0 117.1 76.4 newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.9 208.5 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 110.6 127.7 QF_UFLRA newUnsatCoresAssumps-safe/ ok 7 4 1 3 0 0 3 0 0 0 266.6 55098.3 newUnsatCoresProofs mo 7 0 0 0 0 0 7 0 0 0 261.7 56000.0 oldUnsatCores ok 7 7 4 3 7 0 0 0 3 0 408.4 20933.4 QF_UFNIA newUnsatCoresAssumps-safe/ ok 48 21 19 2 21 4 0 0 20 0 592.3 880.6 newUnsatCoresProofs ok 48 27 22 5 18 4 0 0 1 0 641.4 1548.8 oldUnsatCores ok 48 26 21 5 26 7 0 0 1 0 887.5 1044.6 QF_UFNRA newUnsatCoresAssumps-safe/ ok 1 1 1 0 1 0 0 0 1 0 108.3 17.9 newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.8 19.0 oldUnsatCores to 1 0 0 0 0 1 0 0 0 0 120.8 14.7 UF newUnsatCoresAssumps-safe/ ok 21 5 0 5 5 16 0 0 5 0 2123.8 3168.7 newUnsatCoresProofs ok 21 13 0 13 6 8 0 0 0 0 1496.3 6617.8 oldUnsatCores ok 21 16 0 16 11 5 0 0 3 0 1443.3 3919.2 UFDT newUnsatCoresAssumps-safe/ ok 35 6 0 6 6 29 0 0 5 0 3777.0 4485.5 newUnsatCoresProofs ok 35 28 0 28 15 7 0 0 0 0 1416.9 4293.6 oldUnsatCores ok 35 30 0 30 26 5 0 0 1 0 1406.9 3188.5 UFDTLIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1640.5 newUnsatCoresProofs ok 4 4 0 4 1 0 0 0 0 0 139.3 942.3 oldUnsatCores ok 4 4 0 4 3 0 0 0 0 0 156.4 851.8 UFDTLIRA newUnsatCoresAssumps-safe/ ok 1 1 0 1 1 0 0 0 1 0 0.0 3.1 newUnsatCoresProofs ok 1 0 0 0 0 0 0 0 0 0 0.0 3.2 oldUnsatCores ok 1 0 0 0 0 0 0 0 0 0 0.0 2.7 UFDTNIRA newUnsatCoresAssumps-safe/ ok 10 3 0 3 3 6 0 0 3 0 754.8 1386.9 newUnsatCoresProofs ok 10 7 0 7 5 3 0 0 0 0 377.0 848.8 oldUnsatCores ok 10 7 0 7 7 3 0 0 0 0 376.5 563.4 UFLIA newUnsatCoresAssumps-safe/ ok 24 8 0 8 8 16 0 0 8 0 2231.6 3179.2 newUnsatCoresProofs ok 24 14 0 14 3 10 0 0 1 0 1915.5 5131.1 oldUnsatCores ok 24 15 0 15 14 9 0 0 2 0 1857.5 3479.7 UFNIA newUnsatCoresAssumps-safe/ ok 354 183 28 155 116 133 0 0 113 0 25941.4 839089.7 newUnsatCoresProofs ok 354 107 17 90 28 107 92 0 2 0 23496.9 1020258.1 oldUnsatCores ok 354 237 19 218 233 72 0 0 66 0 19906.9 914273.0 ```
2021-05-19Adding python API test part 3 (#6552)Ying Sheng
This commit (follow #6551) adds more unit tests for python API. Subsequent commits will include additional missing functions and unit tests.
2021-05-19Fix strings rewriter for non-standard re range (#6570)Andrew Reynolds
Fixes #6561. Previously we missed a case where a rewrite fired for (re.range x x) where x is not a character.
2021-05-19Add more missing inference ids (#6313)Andrew Reynolds
This also makes the relations solver use the inference manager in the standard way.
2021-05-19bv: Add support for --bitblast=eager. (#6516)Mathias Preiner
This PR adds support for handling --bitblast=eager in the new bitblast solver.
2021-05-19Fix positive contains indexof rewrites for empty string second argument (#6566)Andrew Reynolds
Fixes #6560.
2021-05-19Remove accidental print (#6568)Gereon Kremer
2021-05-19Generate command line options for sphinx docs (#6555)Gereon Kremer
This PR adds documentation about the command line options to the sphinx documentation. It is mostly a reformatted version of what --help would print.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback