cvc5.git
3 years agoPass empty vector when constructing re empty, fixes rewrite (#6576)
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.

3 years agoAdding python API test part 4 (#6553)
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.

3 years agoMake output list of `mkoptions.py` more accurate (#6572)
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.

3 years agoMake strings emp inference an unhandled inference for proofs (#6575)
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.

3 years agoAdding regressions that failed on old unsat cores (#6574)
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.

3 years agoChange the default unsat cores (#6571)
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
```

3 years agoAdding python API test part 3 (#6552)
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.

3 years agoFix strings rewriter for non-standard re range (#6570)
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.

3 years agoAdd more missing inference ids (#6313)
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.

3 years agobv: Add support for --bitblast=eager. (#6516)
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.

3 years agoFix positive contains indexof rewrites for empty string second argument (#6566)
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.

3 years agoRemove accidental print (#6568)
Gereon Kremer [Wed, 19 May 2021 14:00:10 +0000 (16:00 +0200)]
Remove accidental print (#6568)

3 years agoGenerate command line options for sphinx docs (#6555)
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.

3 years agoImprove handling of `:named` attributes (#6549)
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.

3 years agoFix handling of non-standard re.range terms (#6563)
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.

3 years agoLoop over terms to reconstruct instead of obligations. (#6504)
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.

3 years agoFix `collectEmptyEqs()` in string utils (#6562)
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.

3 years agoAdding python API test part 2 (#6551)
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.

3 years ago(proof-new) Miscellaneous updates to strings from proof-new (#6557)
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.

3 years agoFix smt2 printing (#6558)
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.

3 years agoAdd Solver.java to the Java API (#6196)
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

3 years agoFix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites (#6550)
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.

3 years agoAdding python API test (#6546)
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.

3 years agoMove and enhance python API grammar tests (#6538)
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

3 years agoReplace smt_name by aliases (#6541)
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.

3 years agoInclude cinttypes instead of inttypes.h (#6548)
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).

3 years agoImprove integration of CAD with nl-Ext (#6542)
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.

3 years agoDecouple parser creation from input selection (#6533)
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.

3 years agoRestrict additional CI jobs (#6539)
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.

3 years agoStop using the solver for printing sygus synthesis solutions. (#6530)
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.

3 years agoAdd getId function to python API (#6523)
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)

3 years agoAdd Result.java to the java API (#6385)
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.

3 years agobv: Assert input facts on user-level 0. (#6515)
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.

3 years agoapi docs: Tweak style to be consistent with website style. (#6537)
Aina Niemetz [Fri, 14 May 2021 00:05:18 +0000 (17:05 -0700)]
api docs: Tweak style to be consistent with website style. (#6537)

3 years agoAlways parse streams with line buffer (#6532)
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.

3 years agoAdd std::hash overloads for Node, TNode and TypeNode. (#6534)
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.

3 years agoSplit options holder class (#6527)
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.

3 years agoAdding functions to the python API and testing them -- part 2 (#6517)
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

3 years agoFix error message in toPythonObj (#6524)
Alex Ozdemir [Thu, 13 May 2021 03:47:13 +0000 (20:47 -0700)]
Fix error message in toPythonObj (#6524)

3 years agoMove docs upload to a different workflow (#6512)
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.

3 years agoPreliminary draft of changes for SMT comp 2021 (#6522)
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.

3 years agoEnsure sequences of Booleans generate Boolean term variable skolems when applicable...
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.

3 years agoUse signal(sig, SIG_DFL); raise(sig); instead of abort() (#6518)
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.

3 years agoRemove header for option modules (#6514)
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.

3 years agoRemove read_only from options. (#6513)
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.

3 years agoUnify top-level substitutions and model substitutions (#6499)
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.

3 years agoAdd doc to Kind.java (#6498)
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.

3 years agoAdding functions to the python API and testing them (#6477)
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
3 years agoAdd support for datatype update (#6449)
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.

3 years agoMove slow regressions and update guidelines. (#6508)
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).

3 years agoFix and add missing REQUIRE labels for FP regression tests. (#6506)
Aina Niemetz [Fri, 7 May 2021 23:23:08 +0000 (16:23 -0700)]
Fix and add missing REQUIRE labels for FP regression tests. (#6506)

3 years agoIntegrate documentation build with the regular CI workflow (#6490)
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.

3 years agoProperly printing INST_PATTERN_LIST by itself (#6507)
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.

3 years agoSimplifications to expand definitions (#6487)
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.

3 years agoFix for toPythonObj of integer value with real sort (#6505)
makaimann [Fri, 7 May 2021 18:01:16 +0000 (14:01 -0400)]
Fix for toPythonObj of integer value with real sort (#6505)

3 years ago[proof-new] Updating documentation for Subs/Rw ids (#6502)
Haniel Barbosa [Thu, 6 May 2021 22:56:35 +0000 (19:56 -0300)]
[proof-new] Updating documentation for Subs/Rw ids (#6502)

3 years agoDiscard duplicate terms in patterns (#6501)
Andrew Reynolds [Thu, 6 May 2021 21:57:37 +0000 (16:57 -0500)]
Discard duplicate terms in patterns (#6501)

Fixes #6495.

3 years agoUpdate README.md and remove last CVC4 references. (#6497)
Mathias Preiner [Thu, 6 May 2021 19:55:51 +0000 (12:55 -0700)]
Update README.md and remove last CVC4 references. (#6497)

3 years agoUse constant folding for evaluating BV eager atom (#6494)
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.

3 years agoDo not have quantifiers model inherit from theory model (#6493)
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.

3 years agoSave block comments associated with each kind when parsing kinds file (#6489)
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).

3 years agoAdd helper functions for multi-objective optimization + refactoring (#6473)
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.

3 years agoMove current decision engine to decision engine old (#6466)
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.

3 years agoMove env into smt solver, theory engine, prop engine (#6486)
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.

3 years agoDo not use proof CNF stream with assumptions-based cores (#6488)
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
3 years agoUse proper commit hash for PRs (#6485)
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).

3 years agocmake: Fix ninja build. (#6481)
Mathias Preiner [Tue, 4 May 2021 16:55:28 +0000 (09:55 -0700)]
cmake: Fix ninja build. (#6481)

3 years agoImprove generation of python API documentation (#6482)
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.

3 years agoFP: Move removal of generic to_fp operations to rewriter. (#6480)
Aina Niemetz [Tue, 4 May 2021 02:07:52 +0000 (19:07 -0700)]
FP: Move removal of generic to_fp operations to rewriter. (#6480)

3 years agoFP: Move type check from expandDefinitions. (#6479)
Aina Niemetz [Tue, 4 May 2021 01:00:03 +0000 (18:00 -0700)]
FP: Move type check from expandDefinitions. (#6479)

3 years agoFP: Rewrite to_fp conversion from signed bit-vector. (#6472)
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.

3 years agoAdd missing --auto-download in CI (#6478)
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.

3 years agoAdd CI jobs to build docs (#6413)
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.

3 years agoSymFPU: Automatically apply patch from 2020-11-14. (#6471)
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.

3 years agoPython API tests for terms -- Part 1 (#6468)
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.

3 years agobv: Refactor ppAssert and move to TheoryBV. (#6470)
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.

3 years agoAdd parameter name for argument `isPreRewrite` for FP rewrites. (#6469)
Aina Niemetz [Fri, 30 Apr 2021 22:06:30 +0000 (15:06 -0700)]
Add parameter name for argument `isPreRewrite` for FP rewrites. (#6469)

3 years agoRefactor optimization result and objective classes + add preliminary support for...
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

3 years agoUse substitutions for implementing defined functions (#6437)
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.

3 years agoAdd assertion list utility for justification heuristic (#6414)
Andrew Reynolds [Thu, 29 Apr 2021 16:48:29 +0000 (11:48 -0500)]
Add assertion list utility for justification heuristic (#6414)

3 years agoSimplify generated code for getOption() and setOption() (#6462)
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::...().

3 years agoAdd missing include. (#6463)
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.

3 years agoAvoid exponential explosion of small constant in CEGQI (#6461)
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.

3 years agoFix BV Optimization Boundary Condition when lower bound = upper bound + 1 (#6452)
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.

3 years agoRefactor resource manager options (#6446)
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.

3 years agoRemove exception headers from options.h (#6456)
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.

3 years agoMake sure reference stats are reset properly (#6457)
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.

3 years agoClean up options holder class (#6458)
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.

3 years agoCleanup DidYouMean (#6454)
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.

3 years agoAdd internal support for datatype update (#6450)
Andrew Reynolds [Tue, 27 Apr 2021 22:32:40 +0000 (17:32 -0500)]
Add internal support for datatype update (#6450)

3 years agoMove slow regression to regress3 (#6451)
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.

3 years agoFix refutational soundness bug in quantifier prenexing (#6448)
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.

3 years agoSimplify making function types (#6447)
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.

3 years agoInitial setup for docs of python API (#6445)
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)

3 years agoUse std::hash for API types (#6432)
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.

3 years agoBool: Move implementation of type rules to cpp. (#6420)
Aina Niemetz [Tue, 27 Apr 2021 03:33:03 +0000 (20:33 -0700)]
Bool: Move implementation of type rules to cpp. (#6420)

3 years agoGenerate docs conf.py by cmake (#6441)
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).

3 years agoProtect int stats methods (#6442)
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.

3 years agoFirst part of options refactoring (#6428)
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.

3 years agoFix theoryOf for Boolean equalities (#6444)
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.