cvc5.git
3 years agoImplementation of the new justification heuristic (#6465)
Andrew Reynolds [Mon, 24 May 2021 19:32:48 +0000 (14:32 -0500)]
Implementation of the new justification heuristic (#6465)

This adds the new implementation of the justification heuristic. It does not enable this strategy yet.

A followup PR will activate this strategy within DecisionEngine.

3 years agoMove proof utilities to src/proof/ (#6611)
Andrew Reynolds [Mon, 24 May 2021 18:51:09 +0000 (13:51 -0500)]
Move proof utilities to src/proof/ (#6611)

This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.

It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").

3 years agoFix re-elim length requirement for symbolic RE memberships (#6609)
Andrew Reynolds [Mon, 24 May 2021 16:15:12 +0000 (11:15 -0500)]
Fix re-elim length requirement for symbolic RE memberships (#6609)

Fixes #6604.

Previously, re-elim was solution unsound for cases where the LHS and a component of the RHS were both empty. This ensures a length requirement is given for the LHS to ensure proper containment.

3 years agoFix instance of no rewrite in extended rewriter (#6610)
Andrew Reynolds [Mon, 24 May 2021 15:55:17 +0000 (10:55 -0500)]
Fix instance of no rewrite in extended rewriter (#6610)

Fixes #6545.

An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.

3 years agoBetter formalization of regular expression unfolding skolems (#6602)
Andrew Reynolds [Mon, 24 May 2021 14:39:56 +0000 (09:39 -0500)]
Better formalization of regular expression unfolding skolems (#6602)

This replaces our previous formalization of RE unfolding skolems with a more explicit one that is amenable to external proof conversion. It adds a few associated utility methods to SkolemManager required for LFSC proof conversion for RE_UNFOLD_POS.

It also changes the order of equalities in the RE_UNFOLD_POS rule, which simplifies LFSC proof checking.

3 years agoFix tests of unsat cores (#6593)
Andrew Reynolds [Fri, 21 May 2021 21:46:48 +0000 (16:46 -0500)]
Fix tests of unsat cores (#6593)

This updates all regressions that pass check-unsat-cores to enable check-unsat-cores. This includes any incremental benchmark, which was disabled in run_regression.py previously.

It adds --no-check-unsat-cores to a few corner benchmarks that were previously disabled based on --incremental.

It also reverts a change to when proofs are disabled: options like sygus-inference should not permit proofs (or unsat cores).

3 years agoFix and refactor relevant domain (#6528)
Andrew Reynolds [Fri, 21 May 2021 21:27:19 +0000 (16:27 -0500)]
Fix and refactor relevant domain (#6528)

In a handcrafted case, one can make the body of quantified formula another quantified formula when special attributes are used. The relevant domain utility was not robust to this case, leading to instantiations with free variables.

This fixes the issue and also updates its style to use a term context stack, which also avoids a tree traversal of the bodies of quantified formulas in this utility.

Fixes #6476. The benchmark from that issue now times out.

3 years agoFormalize shared selectors as skolem functions (#6591)
Andrew Reynolds [Fri, 21 May 2021 21:07:50 +0000 (16:07 -0500)]
Formalize shared selectors as skolem functions (#6591)

This is work towards properly printing shared selectors in external proofs.

3 years agoMinor simplification to boolean proof checker (#6590)
Andrew Reynolds [Fri, 21 May 2021 20:48:39 +0000 (15:48 -0500)]
Minor simplification to boolean proof checker (#6590)

3 years ago(proof-new) Minor documentation sync (#6592)
Andrew Reynolds [Fri, 21 May 2021 20:16:20 +0000 (15:16 -0500)]
(proof-new) Minor documentation sync (#6592)

3 years agoAdd utility to get all types occurring in a term (#6588)
Andrew Reynolds [Fri, 21 May 2021 18:04:49 +0000 (13:04 -0500)]
Add utility to get all types occurring in a term (#6588)

Required for external proof conversions.

3 years agoUpdate to sygus standard output for check-synth responses (#6521)
Andrew Reynolds [Fri, 21 May 2021 17:15:28 +0000 (12:15 -0500)]
Update to sygus standard output for check-synth responses (#6521)

This PR does two things:
(1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model.
(2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model.

It also removes the unused command GetSynthSolutionCommand.

3 years agoSupport braced-init-lists with `mkNode()` (#6580)
Andres Noetzli [Fri, 21 May 2021 16:05:45 +0000 (09:05 -0700)]
Support braced-init-lists with `mkNode()` (#6580)

This commit adds support for braced-init-lists in calls to `mkNode()`,
e.g., `mkNode(REGEXP_EMPTY, {})`. Previously, such a call would result
in a node of kind `REGEXP_EMPTY` with a single null node as a child
because the compiler chose the `mkNode(Kind kind, TNode child1)` variant
and converted `{}` to a node using the default constructor. This commit
adds an overload of `mkNode()` that takes an `initializer_list<TNode>`
to allow this use case. It also adds a `mkNode()` overload with zero children
for convenience and removes the 4- and 5-children variants because they
saw little use. Finally, it makes the default constructor of `NodeTemplate`
explicit to avoid accidental conversions.

3 years agoapi docs: Tweak and fix style. (#6582)
Aina Niemetz [Fri, 21 May 2021 10:19:10 +0000 (03:19 -0700)]
api docs: Tweak and fix style. (#6582)

This fixes the style for narrow layouts. It further fixes and improves
the style for the menu.

3 years agoapi docs: Update copyright. (#6596)
Aina Niemetz [Fri, 21 May 2021 08:02:57 +0000 (01:02 -0700)]
api docs: Update copyright. (#6596)

3 years agoUse scikit-build CMake files for pycvc5 (#6543)
makaimann [Fri, 21 May 2021 04:20:30 +0000 (00:20 -0400)]
Use scikit-build CMake files for pycvc5 (#6543)

This PR removes copied CMake files for the pycvc5 Cython target, and instead adds a dependency on scikit-build (where those CMake files originated anyway). This keeps us up to date with fixes. Furthermore, the PR switches from distutils to the more modern setuptools. This does add another dependency but it's a fairly reasonable one. setuptools is not part of the base Python distribution, but my understanding is that it is now the de facto standard, and most package managers install it automatically with Python. The main motivation for switching is in preparation for building wheels.

This PR is a piece of this old one (#5657) which I am closing and splitting up.

3 years agoMove option names out of struct (#6554)
Gereon Kremer [Fri, 21 May 2021 03:22:40 +0000 (05:22 +0200)]
Move option names out of struct (#6554)

This PR moves the option names out of the option struct (which will be removed) to free constexpr string constants.

3 years agoBV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
Aina Niemetz [Fri, 21 May 2021 00:41:50 +0000 (17:41 -0700)]
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)

3 years agoUpdate version of CaDiCaL. (#6583)
Mathias Preiner [Thu, 20 May 2021 22:53:02 +0000 (15:53 -0700)]
Update version of CaDiCaL. (#6583)

3 years agoDisable unit testing for clang builds. (#6595)
Aina Niemetz [Thu, 20 May 2021 22:26:49 +0000 (15:26 -0700)]
Disable unit testing for clang builds. (#6595)

We currently have issues with clang 11 failing for white unit tests.
This disables unit tests for clang builds.

3 years agoProperly initialize. (#6586)
Gereon Kremer [Thu, 20 May 2021 18:50:50 +0000 (20:50 +0200)]
Properly initialize. (#6586)

This PR fixes a missing initialization that lead to a valgrind warning.

3 years agoRemove old unsat cores (#6581)
Haniel Barbosa [Thu, 20 May 2021 18:29:32 +0000 (15:29 -0300)]
Remove old unsat cores (#6581)

This commit removes the remaining old proof code and the code to produce unsat cores based on it.

3 years agoUse most recent version of libpoly (#6587)
Gereon Kremer [Thu, 20 May 2021 17:55:35 +0000 (19:55 +0200)]
Use most recent version of libpoly (#6587)

This PR updates to the most recent version of libpoly which fixes some memory leaks.

3 years agoAvoid using printSynthSolution in the python API and examples (#6564)
yoni206 [Thu, 20 May 2021 15:29:27 +0000 (08:29 -0700)]
Avoid using printSynthSolution in the python API and examples (#6564)

The function printSynthSolution declared here is going to be removed in #6521.

This PR removes it from the python API.
Following #6530, this PR also replaces its usages in the examples by a utility function.
For this, we also add support for getSynthSolutions in the python API.

3 years agoMinor improvements to the API (#6585)
Gereon Kremer [Thu, 20 May 2021 14:29:17 +0000 (16:29 +0200)]
Minor improvements to the API (#6585)

This PR does some minor improvements to the API:
- remove getConstSequenceElements(), use getSequenceValue() instead
- improve documentation for Term

3 years agoFix echo printing. (#6573)
Aina Niemetz [Thu, 20 May 2021 02:54:52 +0000 (19:54 -0700)]
Fix echo printing. (#6573)

Previously, echo surpressed leading, trailing and escape quotes of the
string to print. However, the SMT-LIB standard states that the string is
to be printed as is, including those quote characters.

3 years agoAdd more getters for api::Term (#6496)
Gereon Kremer [Thu, 20 May 2021 02:08:56 +0000 (04:08 +0200)]
Add more getters for api::Term (#6496)

This PR adds more getter functions for api::Term to retrieve values from constant terms (and terms that the average API use might consider constant).
It also introduces std::wstring as regular representation for string constants instead of std::vector<uint32> for the SMT-LIB parser and the String class.

3 years agoExpand arith's farkas lemma rule as a macro (#6577)
Alex Ozdemir [Thu, 20 May 2021 01:16:12 +0000 (18:16 -0700)]
Expand arith's farkas lemma rule as a macro (#6577)

reflects that it is a macro, which we will eliminate

3 years agoRemove unused methods from `NodeManager` (#6578)
Andres Noetzli [Wed, 19 May 2021 23:40:59 +0000 (16:40 -0700)]
Remove unused methods from `NodeManager` (#6578)

3 years agoCorrectly handle negated assertions for assumption-based unsat cores. (#6579)
Mathias Preiner [Wed, 19 May 2021 23:32:25 +0000 (16:32 -0700)]
Correctly handle negated assertions for assumption-based unsat cores. (#6579)

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)