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)
Aina Niemetz [Tue, 4 May 2021 01:00:03 +0000 (18:00 -0700)]
FP: Move type check from expandDefinitions. (#6479)
Aina Niemetz [Mon, 3 May 2021 20:27:02 +0000 (13:27 -0700)]
FP: Rewrite to_fp conversion from signed bit-vector. (#6472)
SymFPU does not allow to_fp conversion from signed bv of size 1. This
adds rewrites for this case.
Rewrites for the constant and the non-constant cases were tested in
isolation.
Gereon Kremer [Mon, 3 May 2021 20:15:36 +0000 (22:15 +0200)]
Add missing --auto-download in CI (#6478)
This PR adds --auto-download for the CI job that builds the documentation. Also makes sure that the documentation workflow never fails.
Gereon Kremer [Mon, 3 May 2021 19:21:19 +0000 (21:21 +0200)]
Add CI jobs to build docs (#6413)
This PR adds CI jobs to automatically build documentation for branches on the main repository and for pull request.
The first job builds the documentation for every push and pr and stores the generated documentation in cvc5.github.io/docs-ci. All versions are stored and for every branch and PR a symbolic link to the most recent version is maintained.
Note that the PR jobs are run by the pull_request_target trigger that allows access to repository secrets, but runs in the context of the target branch and we thus need to (carefully!) pull in the relevant changes manually.
The second job runs once a week and prunes the docs-ci repository: all directories that have not been touched for a month are removed, and all commits older than a month are squashed into a single commit. This retains the full history for the last month, but effectively removes everything older than that.
Aina Niemetz [Mon, 3 May 2021 17:48:06 +0000 (10:48 -0700)]
SymFPU: Automatically apply patch from 2020-11-14. (#6471)
This automatically applies @martin-cs's working patch from 2020-11-14.
It fixes several issues, all covered open issues are added as
regression tests.
Fixes #3582.
Fixes #5511.
Fixes #6164.
yoni206 [Mon, 3 May 2021 06:35:47 +0000 (23:35 -0700)]
Python API tests for terms -- Part 1 (#6468)
This PR removes the old python api tests for terms from test/api/python/test_term.py and replaces it with a new test file test/python/unit/api/test_term.py. The new test file is obtained by translating test/unit/api/term_black.cpp.
In this PR I only include the tests that pass without requiring any change to the python API. The next PR will add functions to the python API that are currently not supported, along with corresponding tests.
Comment: This was originally done in #6460 on the wrong fork. Now it is re-opened, and addresses all comments given there.
Mathias Preiner [Fri, 30 Apr 2021 22:15:44 +0000 (15:15 -0700)]
bv: Refactor ppAssert and move to TheoryBV. (#6470)
This PR refactors ppAssert from the lazy BV solver and moves it to TheoryBV.
Aina Niemetz [Fri, 30 Apr 2021 22:06:30 +0000 (15:06 -0700)]
Add parameter name for argument `isPreRewrite` for FP rewrites. (#6469)
Ouyancheng [Fri, 30 Apr 2021 21:40:49 +0000 (14:40 -0700)]
Refactor optimization result and objective classes + add preliminary support for multiple objectives (#6459)
This PR is one part of multiple.
Preliminary support means currently only supports single objective.
It supports queue-ing up objectives and it always optimizes the first.
Multiple-obj optimization algorithm will be up next.
* Refactor optimization result and objective classes
* Add preliminary support for multiple objectives
* The unit tests are now comparing node values instead of node addresses
Andrew Reynolds [Fri, 30 Apr 2021 19:12:56 +0000 (14:12 -0500)]
Use substitutions for implementing defined functions (#6437)
This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions.
In other words, the effect of:
(define-fun f X t)
is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when
(= f (lambda X t)) was an equality solved by non-clausal simplification
The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula.
In this PR:
define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline.
Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit.
The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions.
The proof manager does not require a special case of using the define-function maps.
Define-function maps are eliminated from SmtEngine.
Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR.
Andrew Reynolds [Thu, 29 Apr 2021 16:48:29 +0000 (11:48 -0500)]
Add assertion list utility for justification heuristic (#6414)
Gereon Kremer [Thu, 29 Apr 2021 16:20:36 +0000 (18:20 +0200)]
Simplify generated code for getOption() and setOption() (#6462)
This PR simplifies the generated code for Options::getOption() and Options::setOption(). It now uses less string streams, less temporary vectors and the new options[...] syntax (instead of options::...().
Gereon Kremer [Thu, 29 Apr 2021 13:49:20 +0000 (15:49 +0200)]
Add missing include. (#6463)
This PR fixes an issue with one of our nightlies.
Gereon Kremer [Thu, 29 Apr 2021 12:38:19 +0000 (14:38 +0200)]
Avoid exponential explosion of small constant in CEGQI (#6461)
This PR fixes an issue that can lead to an exponential explosion of a rational constant for repeated calls to the cegqi instantiation strategy. The d_small_const variable was squared regularly, we now simply multiply it with its original value.
Ouyancheng [Wed, 28 Apr 2021 23:10:51 +0000 (16:10 -0700)]
Fix BV Optimization Boundary Condition when lower bound = upper bound + 1 (#6452)
If lb = ub + 1 then (lb+ub)/2 =pivot == lb since it's rounding to -infinity.
and lb <= x < pivot will always be UNSAT.
We need to handle this differently.
And this only happens in minimization.
Gereon Kremer [Wed, 28 Apr 2021 19:50:23 +0000 (21:50 +0200)]
Refactor resource manager options (#6446)
This PR refactors how the resource manager options are used. It moves options relevant for the resource manager into its own file (making the number of smt options a bit smaller) and uses the Options object directly instead of using the old static accessors.
Gereon Kremer [Wed, 28 Apr 2021 18:32:42 +0000 (20:32 +0200)]
Remove exception headers from options.h (#6456)
This PR removes two headers for exceptions from options.h, and instead pushes the includes to a couple of source files.
Gereon Kremer [Wed, 28 Apr 2021 18:01:15 +0000 (20:01 +0200)]
Make sure reference stats are reset properly (#6457)
This PR adds a reset() method to the ReferenceStat class. It then uses it to properly reset such statistics in the minisat solvers where lifetime is an issue.
Gereon Kremer [Wed, 28 Apr 2021 17:31:41 +0000 (19:31 +0200)]
Clean up options holder class (#6458)
This PR does some cleanup on the options class: it puts the option defaults into the member declaration and removes the explicit constructor; it puts the holder into a unique_ptr; it uses the regular struct copy operation instead of reconstructing the holder object; it moves some macros required for option defaults into the option holder header.
Also, this PR removes some obsolete code related to suggestions for typos.
Gereon Kremer [Wed, 28 Apr 2021 14:42:17 +0000 (16:42 +0200)]
Cleanup DidYouMean (#6454)
This PR does a bit of cleanup on our didyoumean code.
Andrew Reynolds [Tue, 27 Apr 2021 22:32:40 +0000 (17:32 -0500)]
Add internal support for datatype update (#6450)
Andrew Reynolds [Tue, 27 Apr 2021 21:58:25 +0000 (16:58 -0500)]
Move slow regression to regress3 (#6451)
Benchmark is taking 40 seconds on production, due to the configuration that tests --check-unsat-cores.
Andrew Reynolds [Tue, 27 Apr 2021 21:25:11 +0000 (16:25 -0500)]
Fix refutational soundness bug in quantifier prenexing (#6448)
This bug can be triggered by define-fun, quantifier macros or inferred substitutions whose RHS contain quantified formulas.
This corrects the issue by ensuring that bound variables introduced for prenexing are fresh for distinct quantified formula subterms that may share quantified variables.
This was reported by Geoff Sutcliffe via a TPTP run.
Andrew Reynolds [Tue, 27 Apr 2021 20:53:37 +0000 (15:53 -0500)]
Simplify making function types (#6447)
Previously, we were conditionally checking whether a function was "flat" e.g. did not have a function type as the range type.
The original motivation for this was to catch cases where the user made a declare-fun that had function return type, which is not permitted. All these checks are already done at the API level https://github.com/CVC4/CVC4/blob/master/src/api/cpp/cvc5_checks.h#L441.
However, internally we should have no such restriction. This is required for simplifying the LFSC term processor.
Gereon Kremer [Tue, 27 Apr 2021 13:29:19 +0000 (15:29 +0200)]
Initial setup for docs of python API (#6445)
This PR adds the basic setup for including the python API in our sphinx documentation and shows how it works using the Datatype class as an example. In detail
- it enables sphinx.ext.autodoc and makes sure the generated pycvc5 is in the search path
- adds a index page for the python API
- adds a page for the Datatype class
- adds docstrings for the Datatype class
- does some finetuning (remove source locations, but adds signature information)
Gereon Kremer [Tue, 27 Apr 2021 05:31:58 +0000 (07:31 +0200)]
Use std::hash for API types (#6432)
This PR replaces all api::*HashFunction objects by specializations of std::hash. std::hash is meant to be extended in this way, and it allows for a much cleaner usage of std::unordered_set and std::unordered_map with these types.
Aina Niemetz [Tue, 27 Apr 2021 03:33:03 +0000 (20:33 -0700)]
Bool: Move implementation of type rules to cpp. (#6420)
Gereon Kremer [Mon, 26 Apr 2021 20:48:40 +0000 (22:48 +0200)]
Generate docs conf.py by cmake (#6441)
This PR makes cmake generate the sphinx configuration file. This will simplify dynamically modifying this file in the future, for example to add custom paths within the build directory (for the python API).
Gereon Kremer [Mon, 26 Apr 2021 20:16:27 +0000 (22:16 +0200)]
Protect int stats methods (#6442)
This PR protects two methods of the IntStat class in case statistics are disabled.
Gereon Kremer [Mon, 26 Apr 2021 19:43:15 +0000 (21:43 +0200)]
First part of options refactoring (#6428)
This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular
- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()
The removed methods are only used in few places with are changed to using Options::current().X() instead.
In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.
Andrew Reynolds [Mon, 26 Apr 2021 18:58:53 +0000 (13:58 -0500)]
Fix theoryOf for Boolean equalities (#6444)
Required for fixing a bug in CNF stream's ensureLiteral, which was crashing when combined with unsat-cores-mode=assumptions.
With this PR, we assign a formula like (= (= x y) (= z w)) to have theoryOf THEORY_BOOL. Previously, it mistaken was assigned THEORY_UF if e.g. x,y z, w were terms whose type was an uninterpreted sort.
We should retest unsat-cores-mode=assumptions after this PR is merged.
projects / cvc5.git / log