Andrew Reynolds [Mon, 24 May 2021 23:59:28 +0000 (18:59 -0500)]
Fix non-fixed length case in re-elim (#6612)
Fixes followup issues from #6604.
Andrew Reynolds [Mon, 24 May 2021 19:32:48 +0000 (14:32 -0500)]
Implementation of the new justification heuristic (#6465)
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.
Andrew Reynolds [Mon, 24 May 2021 18:51:09 +0000 (13:51 -0500)]
Move proof utilities to src/proof/ (#6611)
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").
Andrew Reynolds [Mon, 24 May 2021 16:15:12 +0000 (11:15 -0500)]
Fix re-elim length requirement for symbolic RE memberships (#6609)
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.
Andrew Reynolds [Mon, 24 May 2021 15:55:17 +0000 (10:55 -0500)]
Fix instance of no rewrite in extended rewriter (#6610)
Fixes #6545.
An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.
Andrew Reynolds [Mon, 24 May 2021 14:39:56 +0000 (09:39 -0500)]
Better formalization of regular expression unfolding skolems (#6602)
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.
Andrew Reynolds [Fri, 21 May 2021 21:46:48 +0000 (16:46 -0500)]
Fix tests of unsat cores (#6593)
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).
Andrew Reynolds [Fri, 21 May 2021 21:27:19 +0000 (16:27 -0500)]
Fix and refactor relevant domain (#6528)
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.
Andrew Reynolds [Fri, 21 May 2021 21:07:50 +0000 (16:07 -0500)]
Formalize shared selectors as skolem functions (#6591)
This is work towards properly printing shared selectors in external proofs.
Andrew Reynolds [Fri, 21 May 2021 20:48:39 +0000 (15:48 -0500)]
Minor simplification to boolean proof checker (#6590)
Andrew Reynolds [Fri, 21 May 2021 20:16:20 +0000 (15:16 -0500)]
(proof-new) Minor documentation sync (#6592)
Andrew Reynolds [Fri, 21 May 2021 18:04:49 +0000 (13:04 -0500)]
Add utility to get all types occurring in a term (#6588)
Required for external proof conversions.
Andrew Reynolds [Fri, 21 May 2021 17:15:28 +0000 (12:15 -0500)]
Update to sygus standard output for check-synth responses (#6521)
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.
Andres Noetzli [Fri, 21 May 2021 16:05:45 +0000 (09:05 -0700)]
Support braced-init-lists with `mkNode()` (#6580)
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.
Aina Niemetz [Fri, 21 May 2021 10:19:10 +0000 (03:19 -0700)]
api docs: Tweak and fix style. (#6582)
This fixes the style for narrow layouts. It further fixes and improves
the style for the menu.
Aina Niemetz [Fri, 21 May 2021 08:02:57 +0000 (01:02 -0700)]
api docs: Update copyright. (#6596)
makaimann [Fri, 21 May 2021 04:20:30 +0000 (00:20 -0400)]
Use scikit-build CMake files for pycvc5 (#6543)
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.
Gereon Kremer [Fri, 21 May 2021 03:22:40 +0000 (05:22 +0200)]
Move option names out of struct (#6554)
This PR moves the option names out of the option struct (which will be removed) to free constexpr string constants.
Aina Niemetz [Fri, 21 May 2021 00:41:50 +0000 (17:41 -0700)]
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
Mathias Preiner [Thu, 20 May 2021 22:53:02 +0000 (15:53 -0700)]
Update version of CaDiCaL. (#6583)
Aina Niemetz [Thu, 20 May 2021 22:26:49 +0000 (15:26 -0700)]
Disable unit testing for clang builds. (#6595)
We currently have issues with clang 11 failing for white unit tests.
This disables unit tests for clang builds.
Gereon Kremer [Thu, 20 May 2021 18:50:50 +0000 (20:50 +0200)]
Properly initialize. (#6586)
This PR fixes a missing initialization that lead to a valgrind warning.
Haniel Barbosa [Thu, 20 May 2021 18:29:32 +0000 (15:29 -0300)]
Remove old unsat cores (#6581)
This commit removes the remaining old proof code and the code to produce unsat cores based on it.
Gereon Kremer [Thu, 20 May 2021 17:55:35 +0000 (19:55 +0200)]
Use most recent version of libpoly (#6587)
This PR updates to the most recent version of libpoly which fixes some memory leaks.
yoni206 [Thu, 20 May 2021 15:29:27 +0000 (08:29 -0700)]
Avoid using printSynthSolution in the python API and examples (#6564)
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.
Gereon Kremer [Thu, 20 May 2021 14:29:17 +0000 (16:29 +0200)]
Minor improvements to the API (#6585)
This PR does some minor improvements to the API:
- remove getConstSequenceElements(), use getSequenceValue() instead
- improve documentation for Term
Aina Niemetz [Thu, 20 May 2021 02:54:52 +0000 (19:54 -0700)]
Fix echo printing. (#6573)
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.
Gereon Kremer [Thu, 20 May 2021 02:08:56 +0000 (04:08 +0200)]
Add more getters for api::Term (#6496)
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.
Alex Ozdemir [Thu, 20 May 2021 01:16:12 +0000 (18:16 -0700)]
Expand arith's farkas lemma rule as a macro (#6577)
reflects that it is a macro, which we will eliminate
Andres Noetzli [Wed, 19 May 2021 23:40:59 +0000 (16:40 -0700)]
Remove unused methods from `NodeManager` (#6578)
Mathias Preiner [Wed, 19 May 2021 23:32:25 +0000 (16:32 -0700)]
Correctly handle negated assertions for assumption-based unsat cores. (#6579)
Andrew Reynolds [Wed, 19 May 2021 22:50:43 +0000 (17:50 -0500)]
Pass empty vector when constructing re empty, fixes rewrite (#6576)
Fixes #6567.
Ying Sheng [Wed, 19 May 2021 22:15:45 +0000 (15:15 -0700)]
Adding python API test part 4 (#6553)
This commit (follow #6552) adds more unit tests for python API.
Subsequent commits will include additional missing functions and unit tests.
Andres Noetzli [Wed, 19 May 2021 21:53:27 +0000 (14:53 -0700)]
Make output list of `mkoptions.py` more accurate (#6572)
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.
Andrew Reynolds [Wed, 19 May 2021 21:33:06 +0000 (16:33 -0500)]
Make strings emp inference an unhandled inference for proofs (#6575)
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.
Haniel Barbosa [Wed, 19 May 2021 21:05:07 +0000 (18:05 -0300)]
Adding regressions that failed on old unsat cores (#6574)
We can thus close #3455, #3651, #4925, #5079, #5238, #5902, #5908, and #5604.
Haniel Barbosa [Wed, 19 May 2021 20:25:18 +0000 (17:25 -0300)]
Change the default unsat cores (#6571)
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
```
Ying Sheng [Wed, 19 May 2021 20:08:54 +0000 (13:08 -0700)]
Adding python API test part 3 (#6552)
This commit (follow #6551) adds more unit tests for python API.
Subsequent commits will include additional missing functions and unit tests.
Andrew Reynolds [Wed, 19 May 2021 19:42:21 +0000 (14:42 -0500)]
Fix strings rewriter for non-standard re range (#6570)
Fixes #6561.
Previously we missed a case where a rewrite fired for (re.range x x) where x is not a character.
Andrew Reynolds [Wed, 19 May 2021 18:39:59 +0000 (13:39 -0500)]
Add more missing inference ids (#6313)
This also makes the relations solver use the inference manager in the standard way.
Mathias Preiner [Wed, 19 May 2021 17:21:42 +0000 (10:21 -0700)]
bv: Add support for --bitblast=eager. (#6516)
This PR adds support for handling --bitblast=eager in the new bitblast solver.
Andrew Reynolds [Wed, 19 May 2021 17:12:28 +0000 (12:12 -0500)]
Fix positive contains indexof rewrites for empty string second argument (#6566)
Fixes #6560.
Gereon Kremer [Wed, 19 May 2021 14:00:10 +0000 (16:00 +0200)]
Remove accidental print (#6568)
Gereon Kremer [Wed, 19 May 2021 05:55:53 +0000 (07:55 +0200)]
Generate command line options for sphinx docs (#6555)
This PR adds documentation about the command line options to the sphinx documentation. It is mostly a reformatted version of what --help would print.
Andres Noetzli [Wed, 19 May 2021 01:27:09 +0000 (18:27 -0700)]
Improve handling of `:named` attributes (#6549)
Currently, when a :named attribute is used in a binder, the parser
complains about an illegal argument. This is because an argument check
in the SymbolManager fails. This is not very user friendly. This
commit makes the error message clearer for the user:
Cannot name a term in a binder (e.g., quantifiers, definitions)
To do this, the commit changes the return type for
SymbolManager::setExpressionName to include more information that can
then be used by the parser to generate an appropriate error message.
The commit also changes define-fun to not push/pop the local scope
if it has zero arguments because it is semantically equivalent to a
define-const, which allows :named terms.
Andrew Reynolds [Wed, 19 May 2021 00:59:09 +0000 (19:59 -0500)]
Fix handling of non-standard re.range terms (#6563)
Fixes #6561. That benchmark now gives an error:
(error "expecting a single constant string term in regexp range").
This PR also makes isConstRegExp do a non-recursive dag traversal.
Abdalrhman Mohamed [Tue, 18 May 2021 22:32:21 +0000 (17:32 -0500)]
Loop over terms to reconstruct instead of obligations. (#6504)
This PR modifies the rcons algorithm to loop over terms to reconstruct instead of obligations. It also modifies the Obs data structure to reflect this change. The rest of the PR is mostly updating documentation and refactoring the affected code.
Andres Noetzli [Tue, 18 May 2021 21:32:51 +0000 (14:32 -0700)]
Fix `collectEmptyEqs()` in string utils (#6562)
Fixes #6483. The benchmark in the issue was performing the following
incorrect rewrite:
Rewrite (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") to (str.replace "B" a "B") by RPL_X_Y_X_SIMP.
The rewrite RPL_X_Y_X_SIMP rewrites terms of the form (str.replace x y x), where x is of length one and (= y "") rewrites to a
conjunction of equalities of the form (= y_i "") where y_i is some
term. The function responsible for collecting the terms y_i from this
conjunction, collectEmptyEqs(), returns a bool and a vector of
Nodes. The bool indicates whether all equalities in the conjunction
were of the form (= y_i ""). The rewrite RPL_X_Y_X_SIMP only applies
if this is true. However, collectEmptyEqs() had a bug where it would
not return false when all of the conjuncts were equalities but not all
of them were equalities with the empty string. This commit fixes
collectEmptyEqs() and adds tests.
Ying Sheng [Tue, 18 May 2021 17:11:16 +0000 (10:11 -0700)]
Adding python API test part 2 (#6551)
This commit (follow #6546) adds more unit tests for python API.
Subsequent commits will include additional missing functions and unit tests.
Andrew Reynolds [Tue, 18 May 2021 16:57:04 +0000 (11:57 -0500)]
(proof-new) Miscellaneous updates to strings from proof-new (#6557)
This includes:
(1) The type rule for `re.range` no longer insists on constant arguments, or a non-empty range. This is required for LFSC proof conversion, where re.range terms take arguments that are not (cvc5 internal) constants.
(2) Simplifications to reductions for indexof, which fixes proof checking errors in LFSC.
Andrew Reynolds [Tue, 18 May 2021 16:36:22 +0000 (11:36 -0500)]
Fix smt2 printing (#6558)
This fixes bugs related to the smt2 printer where we rely on stream operators for recursive printing calls for certain parts of terms.
Notice that a call to
`out << n;`
within `SmtPrinter::toStream(...)` is wrong since then recursively `n` is printed with the current output language. This means that if one were to ask to print a term in SMT2 format and the output language is not SMT2, then the above call would print `n` in a different format.
This is required to fix bugs in the LFSC proof converter, which explicitly changes the output format to SMT2.
mudathirmahgoub [Tue, 18 May 2021 06:18:23 +0000 (01:18 -0500)]
Add Solver.java to the Java API (#6196)
PR changes:
Add Solver.java and relation JNI c files
Update FindJUnit to download JUnit5
Add Java unit tests
Andres Noetzli [Mon, 17 May 2021 18:33:01 +0000 (11:33 -0700)]
Fix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites (#6550)
Fixes #6520. The `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites were
applied too aggressively. Those rewrites attempt to rewrite string
equalities between concatenations where the prefix on one side is
provably shorter than the prefix on the other side. The length of the
shorter prefix is then stripped from the longer prefix. However, cvc5
was not checking whether it was able to strip the length of the full
prefix. If cvc5 cannot strip the full length of the shorter prefix, then
the rewrite does not apply because parts of the shorter prefix would
have to be kept. This commit adds an additional condition that checks
whether the length of the full prefix was stripped.
Ying Sheng [Mon, 17 May 2021 18:20:31 +0000 (11:20 -0700)]
Adding python API test (#6546)
This commit adds unit tests for python API.
Subsequent commits will include additional missing functions and unit tests.
yoni206 [Mon, 17 May 2021 18:00:41 +0000 (11:00 -0700)]
Move and enhance python API grammar tests (#6538)
The existing test for python API grammar is moved to the right location, `yapf`ed, and changed according to the new style of python API tests. Additionally, minor changes are introduced in order to be an exact translation of https://github.com/cvc5/cvc5/blob/master/test/unit/api/grammar_black.cpp
Gereon Kremer [Mon, 17 May 2021 17:08:51 +0000 (19:08 +0200)]
Replace smt_name by aliases (#6541)
This PR replaces the confusing co-existence of long and smt_name for options by long and a list of alias.
Andres Noetzli [Mon, 17 May 2021 16:52:55 +0000 (09:52 -0700)]
Include cinttypes instead of inttypes.h (#6548)
This commit changes the includes used by MiniSat. This commit changes
the includes from stdint.h/inttypes.h/limits.h to
cstdint/cinttypes/climits. This ensures that the macros in
cinttypes/inttypes.h, e.g., `PRIi64`, are actually defined. The C99
standard suggested that those macros are only defined for C++ code when
`__STDC_FORMAT_MACROS` is defined. This was never adopted by a C++
standard (https://en.cppreference.com/w/cpp/types/integer). However,
certain versions of mingw-w64 seem to require it with inttypes.h but not
cinttypes.
This fixes the nightly Windows build (tested in the Docker container
used by the nightlies).
Gereon Kremer [Mon, 17 May 2021 15:18:57 +0000 (17:18 +0200)]
Improve integration of CAD with nl-Ext (#6542)
This PR improves the integration of the CAD solver with the nl-ext solver in a simple way: we simply use a few of the simple linearization lemmas in combination with CAD by default, significantly improving the performance on QF_NRA.
Andres Noetzli [Fri, 14 May 2021 23:17:54 +0000 (16:17 -0700)]
Decouple parser creation from input selection (#6533)
This commit decouples the creation of a `Parser` instance from creating
an `Input` and setting the `Input` on the parser. This is a first step
in refactoring the parser infrastructure. A future PR will split the
parser class into three classes: `Parser`, `ParserState`, and
`InputParser`. The `Parser` and `InputParser` classes will be the
public-facing classes. The new `Parser` class will have methods to
create `InputParser`s from files, streams, and strings. `InputParser`s
will have methods to get commands/exprs from a given input. The
`ParserState` class will keep track of the state of the parser and will
be the internal interface for the parsers. The current `Parser` class is
used both publicly and internally, which is messy.
Gereon Kremer [Fri, 14 May 2021 20:25:14 +0000 (22:25 +0200)]
Restrict additional CI jobs (#6539)
The new upload-docs CI job is currently run unconditionally after the CI job finishes. It can only work, though, if the CI job worked and stored an artifact. The PR update job is run for all commits on master, though it only has the necessary token when running on the main repository.
This PR restricts both jobs to cases where they work.
Abdalrhman Mohamed [Fri, 14 May 2021 16:24:54 +0000 (11:24 -0500)]
Stop using the solver for printing sygus synthesis solutions. (#6530)
This PR uses custom methods for printing the synthesis solutions instead of Solver::printSynthSolution, which is going to be removed by #6521.
Alex Ozdemir [Fri, 14 May 2021 11:34:38 +0000 (04:34 -0700)]
Add getId function to python API (#6523)
(Z3 exposes it to facilitate custom hashes)
mudathirmahgoub [Fri, 14 May 2021 01:15:21 +0000 (20:15 -0500)]
Add Result.java to the java API (#6385)
This PR adds Result.java ResultTest.java and cvc5_Result.cpp to the java api.
Mathias Preiner [Fri, 14 May 2021 00:29:52 +0000 (17:29 -0700)]
bv: Assert input facts on user-level 0. (#6515)
The bitblast solver currently uses solving under assumptions for all facts that are sent to the bit-vector solver. For input facts on user-level 0 we can however assert the fact to the SAT solver, which allows the SAT solver to do more preprocessing. This PR adds the option to assert user-level 0 input facts, which is disabled by default.
Aina Niemetz [Fri, 14 May 2021 00:05:18 +0000 (17:05 -0700)]
api docs: Tweak style to be consistent with website style. (#6537)
Andres Noetzli [Thu, 13 May 2021 16:49:33 +0000 (09:49 -0700)]
Always parse streams with line buffer (#6532)
When cvc5 was compiled in competition mode (but not for the application
track), then it had a special behavior when reading from stdin. When it
received input from stdin, it would read all of stdin and then parse the
input as a string because it assumed that the full input is directly
available on stdin. However, the non-application tracks of SMT-COMP do
not use stdin anymore. They pass a filename to the solver. This special
case is not used as a result. Usually, cvc5 parses from stdin using the
line buffer, so this commit makes it so that this is always the case,
which simplifies the code.
Mathias Preiner [Thu, 13 May 2021 06:33:00 +0000 (23:33 -0700)]
Add std::hash overloads for Node, TNode and TypeNode. (#6534)
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
Gereon Kremer [Thu, 13 May 2021 06:02:58 +0000 (08:02 +0200)]
Split options holder class (#6527)
This PR splits the OptionsHolder class into separate holder classes for every options module and makes them directly accessible via appropriate Options::<module>() methods. We forward declare these new holder classes and thereby retain that we only need to recompile when we change an option module that is explicitly included.
All (generated) methods that previously accessed the old holder object are changed to instead use the new holder objects.
This PR does the bare minimum to do this change, further PRs will eventually get rid of all template specializations that currently surround our options class.
yoni206 [Thu, 13 May 2021 05:32:55 +0000 (22:32 -0700)]
Adding functions to the python API and testing them -- part 2 (#6517)
This PR adds some functions that are missing in the python API, along with unit tests for them.
The unit tests are translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/term_black.cpp
Alex Ozdemir [Thu, 13 May 2021 03:47:13 +0000 (20:47 -0700)]
Fix error message in toPythonObj (#6524)
Gereon Kremer [Wed, 12 May 2021 17:13:06 +0000 (19:13 +0200)]
Move docs upload to a different workflow (#6512)
This PR (finally, I hope) uses a proper setup for uploading the documentation. One of the CI jobs generates the documentation and stores it in an artifact. Another workflow is triggered (via workflow_run) and then uploads this artifact. Only this setup seems to properly work for PR builds.
Andrew Reynolds [Wed, 12 May 2021 14:38:59 +0000 (09:38 -0500)]
Preliminary draft of changes for SMT comp 2021 (#6522)
Covers improvements to quantifiers.
Andrew Reynolds [Wed, 12 May 2021 13:30:42 +0000 (08:30 -0500)]
Ensure sequences of Booleans generate Boolean term variable skolems when applicable (#6529)
Fixes #6510.
This PR also eliminates a deprecated variant mkBooleanTermVariable from SkolemManager.
Gereon Kremer [Wed, 12 May 2021 06:22:52 +0000 (08:22 +0200)]
Use signal(sig, SIG_DFL); raise(sig); instead of abort() (#6518)
As discussed in #6484 (and https://www.gnu.org/software/libc/manual/html_node/Termination-in-Handler.html), simply calling std::abort at the end of a custom signal handler seems to be bad practice. As suggested, this PR changes these calls to instead first reset to the default signal handler for the given signal, and then calling it.
Fixes #6484.
Gereon Kremer [Mon, 10 May 2021 22:22:24 +0000 (00:22 +0200)]
Remove header for option modules (#6514)
This PR further simplifies the option declaration by removing the header attribute from module options.
Instead of specifying it manually, it is now automatically generated from the filename of the toml file. The header files and the toml files use matching names already, so this PR simply removes another mechanism that is not used anyway.
This PR also does a minor cleanup of the Options class in the mkoptions.py script.
Gereon Kremer [Mon, 10 May 2021 21:37:12 +0000 (23:37 +0200)]
Remove read_only from options. (#6513)
This PR removes the possibility of declaring options read_only.
It's only effect is making an attempts to disallow changing the respective option from within our internal code (by not providing a setter method). However, a "read-only" option can still be set via the setOption() methods that is also used by the API, and by SMT-LIB's set-option.
Andrew Reynolds [Mon, 10 May 2021 14:29:09 +0000 (09:29 -0500)]
Unify top-level substitutions and model substitutions (#6499)
This unifies top-level substitutions and theory model substitutions. Env is now passed to the TheoryModel, which has access to top-level substitutions.
The former was used for simplfying assertions in the preprocessor, the latter was used for evaluating terms in the model.
There is no reason to have these two things be separate.
mudathirmahgoub [Mon, 10 May 2021 12:18:32 +0000 (07:18 -0500)]
Add doc to Kind.java (#6498)
This PR adds documentation to java kinds.
yoni206 [Sat, 8 May 2021 01:01:17 +0000 (18:01 -0700)]
Adding functions to the python API and testing them (#6477)
This PR adds some functions that are missing in the python API, along with unit tests for them.
Subsequent PR will include additional missing functions.
Also includes a yapf run to reformat the test file.
Co-authored-by: Makai Mann makaim@stanford.edu
Andrew Reynolds [Sat, 8 May 2021 00:25:27 +0000 (19:25 -0500)]
Add support for datatype update (#6449)
This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.
Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.
Aina Niemetz [Fri, 7 May 2021 23:30:48 +0000 (16:30 -0700)]
Move slow regressions and update guidelines. (#6508)
This moves regression test that exceed the time limit of their
respective level to the appropriate level. It further updates the
guidelines in the README with information on how to properly categorize
regression tests into levels (with time limits).
Note: Test regress3/issue4717.smt2 was previously unsolved (unknown) and
is now sat (Z3 agrees).
Aina Niemetz [Fri, 7 May 2021 23:23:08 +0000 (16:23 -0700)]
Fix and add missing REQUIRE labels for FP regression tests. (#6506)
Gereon Kremer [Fri, 7 May 2021 23:14:13 +0000 (01:14 +0200)]
Integrate documentation build with the regular CI workflow (#6490)
The new documentation workflow requires building CVC5 again in a separate workflow, which takes quite some time.
This PR integrates building the documentation with the regular CI workflow.
Haniel Barbosa [Fri, 7 May 2021 20:28:44 +0000 (17:28 -0300)]
Properly printing INST_PATTERN_LIST by itself (#6507)
Previously the SMT2 printer would print pattern lists wrong when they were not printed as part of a binder containing it. This commit fixes this by removing an unused hardcoded restriction that led to issues when printing the ASTs of proof nodes containing patterns.
Andrew Reynolds [Fri, 7 May 2021 19:09:58 +0000 (14:09 -0500)]
Simplifications to expand definitions (#6487)
This removes the expandOnly flag from expandDefinitions.
The use of expandOnly = true is equivalent to applying top-level substitutions only, which should be done explicitly via Env::getTopLevelSubstitutions. It updates the trust substitutions utility to distinguish apply vs applyTrusted for convenience for this purpose.
This also breaks several dependencies in e.g. expand definitions module.
makaimann [Fri, 7 May 2021 18:01:16 +0000 (14:01 -0400)]
Fix for toPythonObj of integer value with real sort (#6505)
Haniel Barbosa [Thu, 6 May 2021 22:56:35 +0000 (19:56 -0300)]
[proof-new] Updating documentation for Subs/Rw ids (#6502)
Andrew Reynolds [Thu, 6 May 2021 21:57:37 +0000 (16:57 -0500)]
Discard duplicate terms in patterns (#6501)
Fixes #6495.
Mathias Preiner [Thu, 6 May 2021 19:55:51 +0000 (12:55 -0700)]
Update README.md and remove last CVC4 references. (#6497)
Andrew Reynolds [Thu, 6 May 2021 19:22:46 +0000 (14:22 -0500)]
Use constant folding for evaluating BV eager atom (#6494)
This is work towards unifying top-level substitutions with model substitutions.
Currently, for model evaluation, BV eager atom preprocessing pass adds mappings (BV_EAGER_ATOM X) -> X to say how (BV_EAGER_ATOM X) should be evaluated in the model. This is not necessary since a rewrite rule (BV_EAGER_ATOM c) -> c for constant c would suffice.
This eliminates the call to addModelSubstitution in that preprocessing pass.
It also makes it so that we don't make true/false themselves into eager atoms.
Andrew Reynolds [Wed, 5 May 2021 23:09:24 +0000 (18:09 -0500)]
Do not have quantifiers model inherit from theory model (#6493)
This is work towards making the initialization of theory engine, theory models, quantifiers engine more flexible.
This makes it so that the specialized quantifiers models classes (FirstOrderModel) do not inherit from TheoryModel. There is no longer any reason for this, since FirstOrderModel does not have any override methods.
As a result of this PR, there is only one kind of TheoryModel and it is constructed immediately when ModelManager is constructed.
This required refactoring the initialization of when FirstOrderModel is constructed in ModelBuilder classes in quantifiers.
This also avoids the need for casting TheoryModel to FirstOrderModel.
makaimann [Wed, 5 May 2021 07:15:39 +0000 (03:15 -0400)]
Save block comments associated with each kind when parsing kinds file (#6489)
This PR adds features to the KindsParser for saving and looking up the documentation comment associated with each Kind. This PR does not make use of it yet, but future PRs can query for the comment to automatically add it to language binding documentation (e.g., Python / Java bindings).
Ouyancheng [Wed, 5 May 2021 00:34:54 +0000 (17:34 -0700)]
Add helper functions for multi-objective optimization + refactoring (#6473)
add 3 helper functions
judge whether a node is optimizable
make strong improvement expression according to optimization objective
make weak improvement expression according to optimization objective
optChecker is now created by optimizationSolver instead of the minimize/maximize functions
Slightly refactors function signatures so that they are accepting OptimizationObjective instead of accepting target, type in separate parameters.
Andrew Reynolds [Wed, 5 May 2021 00:25:25 +0000 (19:25 -0500)]
Move current decision engine to decision engine old (#6466)
The decision engine is the class that contains strategies for doing e.g. justification heuristic.
The current implementation is hardcoded for the old implementation of justification heuristic.
Since both implementations will be maintained in the short term, this splits the parts of DecisionEngine that are specific to the old implementation to a class DecisionEngineOld.
It refactors the interface of DecisionEngine in a way that is compatible with both implementations.
Andrew Reynolds [Tue, 4 May 2021 23:22:49 +0000 (18:22 -0500)]
Move env into smt solver, theory engine, prop engine (#6486)
This is work towards eliminating singletons.
Also, TheoryModel should use the same substitution map as the preprocessor. This is work towards unifying these things, which will be done in a future PR.
Haniel Barbosa [Tue, 4 May 2021 18:36:41 +0000 (15:36 -0300)]
Do not use proof CNF stream with assumptions-based cores (#6488)
Previously using proof CNF stream together with assumptions-based unsat cores added unnecessary performance overhead.
Co-authored-by: Mathias Preiner mathias.preiner@gmail.com
Gereon Kremer [Tue, 4 May 2021 17:06:35 +0000 (19:06 +0200)]
Use proper commit hash for PRs (#6485)
For PRs, the automatically generated documentation is stored under the current master commit hash instead of the hash of the latest commit on the PR. This PR fixes this issue by exporting the commit hash (much like the name of the PR or branch).
Mathias Preiner [Tue, 4 May 2021 16:55:28 +0000 (09:55 -0700)]
cmake: Fix ninja build. (#6481)
Gereon Kremer [Tue, 4 May 2021 16:33:59 +0000 (18:33 +0200)]
Improve generation of python API documentation (#6482)
This PR makes generating the python part of our API documentation more reliable. If python bindings are enabled, it makes the docs target depend on pycvc5 and renders a warning into the documentation if python bindings are disabled.
To make the dependency on pycvc5 work properly, it changes the python bindings build so that the library is directly put in the right place and avoid the manual rename, so that the pycvc5 target actually points to the correct file.
Unfortunately, this means we need to build libcvc5 when building docs with python bindings enabled.
Aina Niemetz [Tue, 4 May 2021 02:07:52 +0000 (19:07 -0700)]
FP: Move removal of generic to_fp operations to rewriter. (#6480)