cvc5.git
2 years agoFix bug in strict symbolic length strip (#8973)
Andrew Reynolds [Tue, 19 Jul 2022 15:21:54 +0000 (10:21 -0500)]
Fix bug in strict symbolic length strip (#8973)

Leads to incorrect rewrites. Fixes #8970.

2 years agoGlobal negate requires quantifiers (#8957)
Andrew Reynolds [Tue, 19 Jul 2022 13:54:47 +0000 (08:54 -0500)]
Global negate requires quantifiers (#8957)

Fixes cvc5/cvc5-projects#521.

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
2 years agoFix global-declarations with abduction (#8961)
Andrew Reynolds [Mon, 18 Jul 2022 18:09:43 +0000 (13:09 -0500)]
Fix global-declarations with abduction (#8961)

FYI @arjunvish

The same issue would lead to issues when using global-declarations with interpolation or block-models.

2 years agoFix issue 8959 (#8962)
mudathirmahgoub [Mon, 18 Jul 2022 13:46:39 +0000 (08:46 -0500)]
Fix issue 8959 (#8962)

This PR fixes issue #8959 which happens because group terms that are not representatives are not registered in the solver state.

2 years agofix incorrect 64-bit detection -- powerpc64le doesn't end in 64 but is 64-bit (#8955) main
Jacob Lifshay [Wed, 13 Jul 2022 17:11:30 +0000 (10:11 -0700)]
fix incorrect 64-bit detection -- powerpc64le doesn't end in 64 but is 64-bit (#8955)

Signed-off-by: Jacob Lifshay <programmerjake@gmail.com>
2 years agoMove bv arith conversions to arith (#8945)
Andrew Reynolds [Mon, 11 Jul 2022 20:02:59 +0000 (15:02 -0500)]
Move bv arith conversions to arith (#8945)

This is in preparation for lazier handling of bv2nat and int2bv. Our infrastructure in arithmetic is better equipped for doing this.

There are no behavior changes in this PR.

2 years ago[IntToBV] Add check for unsupported operators (#8949)
Andres Noetzli [Mon, 11 Jul 2022 17:57:22 +0000 (10:57 -0700)]
[IntToBV] Add check for unsupported operators (#8949)

Fixes #8935. This adds a check for unsupported operators in the IntToBV
preprocessing pass and improves error messages. Previously, operators
such as str.to_int, which return an integer but do not take an integer
as an argument were not detected as unsupported.

2 years agoRemove `--strings-unified-vspt` option (#8947)
Andres Noetzli [Sat, 9 Jul 2022 05:27:40 +0000 (22:27 -0700)]
Remove `--strings-unified-vspt` option (#8947)

This option was enabled by default and this commit enables it
permanently. Overall, the results (300s timeout) seem to indicate that
the option does not have a significant impact on performance (and is a
bit worse overall):

```
                                status  total  solved    sat  unsat   best  timeout  memout  error  uniq  disagr  time_cpu   memory
config
2022-07-07-strings-main-no-vspt     ok  69984   69513  42755  26758  65940      468       0      1    12       0  175814.9 456860.9
2022-07-07-strings-main-vspt        ok  69984   69509  42750  26759  65097      472       0      1     8       0  174975.7 456793.6
```

2 years agoEliminate static options accesses in sygus (#8943)
Andrew Reynolds [Sat, 9 Jul 2022 04:49:19 +0000 (23:49 -0500)]
Eliminate static options accesses in sygus (#8943)

Towards eliminating option scopes.

Also simplifies and corrects an issue in default Boolean grammar construction where included/excluded constructors were ignored.

2 years agoAdd scripts for casc j11 (#8941)
Andrew Reynolds [Sat, 9 Jul 2022 04:26:38 +0000 (23:26 -0500)]
Add scripts for casc j11 (#8941)

2 years agoEliminate static options access in proof utilities (#8927)
Andrew Reynolds [Sat, 9 Jul 2022 03:42:48 +0000 (22:42 -0500)]
Eliminate static options access in proof utilities (#8927)

This requires changing many of the proof interfaces to pass Env instead of ProofNodeManager. This is also work towards simplifying the initialization of our proof infrastructure.

2 years agoFix issues with mixed types in relevant domain (#8901)
Andrew Reynolds [Sat, 9 Jul 2022 03:07:27 +0000 (22:07 -0500)]
Fix issues with mixed types in relevant domain (#8901)

Fixes #8881.

Indentation changed, leading to the large diff. The code change is only to ensure the type of the term to add to the relevant domain matches the type of the variable.

2 years agoDo not use sygus-inst for internal bounded quantifiers for string reductions (#8946)
Andrew Reynolds [Fri, 8 Jul 2022 20:07:52 +0000 (15:07 -0500)]
Do not use sygus-inst for internal bounded quantifiers for string reductions (#8946)

Fixes #8944.

2 years agoFix casting for arith msum (#8940)
Andrew Reynolds [Thu, 7 Jul 2022 20:30:30 +0000 (15:30 -0500)]
Fix casting for arith msum (#8940)

Fixes #8872.

2 years agoFix mod elimination in learned rewrite preprocessing pass (#8938)
Andrew Reynolds [Thu, 7 Jul 2022 20:09:36 +0000 (15:09 -0500)]
Fix mod elimination in learned rewrite preprocessing pass (#8938)

Fixes #8934.

Also makes this rewrite cover more cases.

2 years agoDo not eagerly preprocess seq.nth (#8937)
Andrew Reynolds [Thu, 7 Jul 2022 19:15:07 +0000 (14:15 -0500)]
Do not eagerly preprocess seq.nth (#8937)

Fixes #8936.

2 years agoRevert usage of seq.nth in reductions (#8939)
Andrew Reynolds [Thu, 7 Jul 2022 18:54:05 +0000 (13:54 -0500)]
Revert usage of seq.nth in reductions (#8939)

Fixes #8932. Fixes #8926.

2 years agoFix pto handling for heaps that are not a subset of the base heap (#8942)
Andrew Reynolds [Thu, 7 Jul 2022 16:26:00 +0000 (11:26 -0500)]
Fix pto handling for heaps that are not a subset of the base heap (#8942)

These require a downwards rule to be compatible with our propagation rules for pto.

Fixes #8863.

2 years agoAdd rel.project operator to sets (#8929)
mudathirmahgoub [Wed, 6 Jul 2022 21:02:23 +0000 (16:02 -0500)]
Add rel.project operator to sets (#8929)

2 years agoUpdate SMT-COMP scripts (#8930)
Andres Noetzli [Wed, 6 Jul 2022 20:12:33 +0000 (13:12 -0700)]
Update SMT-COMP scripts (#8930)

2 years agoRemove `Theory::postsolve()` (#8924)
Andres Noetzli [Thu, 30 Jun 2022 23:18:06 +0000 (16:18 -0700)]
Remove `Theory::postsolve()` (#8924)

The feature was not used. This commit also uses the removal to simplify
`SolverEngine` a bit.

2 years agoRemove spurious pto singleton inference (#8925)
Andrew Reynolds [Thu, 30 Jun 2022 18:29:52 +0000 (13:29 -0500)]
Remove spurious pto singleton inference (#8925)

This removes a spurious lemma schema that is already covered by SEP_POS_REDUCTION.

2 years ago[SMT-COMP] Update use of `--decision` option (#8922)
Andres Noetzli [Thu, 30 Jun 2022 13:45:21 +0000 (06:45 -0700)]
[SMT-COMP] Update use of `--decision` option (#8922)

The name of the mode changed from justification-stoponly to just
stoponly.

2 years agoFix injectivity inferences for seq.nth applied to strings (#8920)
Andrew Reynolds [Thu, 30 Jun 2022 09:39:42 +0000 (04:39 -0500)]
Fix injectivity inferences for seq.nth applied to strings (#8920)

Fixes #8916.

2 years agoFix type issue in substitutions from covering solver (#8921)
Andrew Reynolds [Thu, 30 Jun 2022 04:54:56 +0000 (23:54 -0500)]
Fix type issue in substitutions from covering solver (#8921)

Fixes #8895. The benchmark in that issue now times out.

2 years agoAdd set.aggr operator to sets (#8878)
mudathirmahgoub [Thu, 30 Jun 2022 02:03:36 +0000 (21:03 -0500)]
Add  set.aggr operator to sets (#8878)

This PR depends on #8876

2 years agoFix reduction for seq.nth for strings (#8919)
Andrew Reynolds [Wed, 29 Jun 2022 21:02:54 +0000 (16:02 -0500)]
Fix reduction for seq.nth for strings (#8919)

Fixes #8918.

2 years agoFix model construction for str.unit (#8917)
Andrew Reynolds [Wed, 29 Jun 2022 20:19:41 +0000 (15:19 -0500)]
Fix model construction for str.unit (#8917)

Fixes #8915.

2 years agoAdd rel.group operator to sets (#8876)
mudathirmahgoub [Tue, 28 Jun 2022 17:50:41 +0000 (12:50 -0500)]
Add rel.group operator to sets (#8876)

This PR is dependent on #8819 and #8867.

2 years agoMove `SymbolManager` and `SymbolTable` to parser (#8910)
Andres Noetzli [Mon, 27 Jun 2022 22:28:27 +0000 (15:28 -0700)]
Move `SymbolManager` and `SymbolTable` to parser (#8910)

This moves `SymbolManager` and `SymbolTable` to the parser. To do so, it
modifies headers in the `context` package to be public to the parser
(changes `cvc5_private.h` to `cvc5parser_public.h`), because they are
shared between the parser and the main library.

2 years ago[Docs] Update `EnumDocumenter` for newer Sphinx (#8914)
Andres Noetzli [Mon, 27 Jun 2022 21:57:05 +0000 (14:57 -0700)]
[Docs] Update `EnumDocumenter` for newer Sphinx (#8914)

The `no_docstring` argument of
`sphinx.ext.autodoc.Documenter.add_content()` has been
[deprecated](https://www.sphinx-doc.org/en/master/changes.html) since
Sphinx 3.4.0 (released in December 2020). It seems that newer Sphinx
versions have removed that argument, which breaks our `EnumDocumenter`
(e.g., see the following
[example](https://github.com/cvc5/cvc5/runs/7081097179?check_suite_focus=true)).
This commit updates our use of
`sphinx.ext.autodoc.Documenter.add_content()`.

2 years agoRevert change in lemma order in prop engine (#8911)
Andrew Reynolds [Mon, 27 Jun 2022 20:46:04 +0000 (15:46 -0500)]
Revert change in lemma order in prop engine (#8911)

This reverts the change in lemma order from #8301.

2 years agoAdd inference rules for table.group (#8819)
mudathirmahgoub [Thu, 23 Jun 2022 21:21:56 +0000 (16:21 -0500)]
Add inference rules for table.group (#8819)

2 years agoRemove `CommandSequence` command (#8904)
Andres Noetzli [Thu, 23 Jun 2022 20:51:05 +0000 (13:51 -0700)]
Remove `CommandSequence` command (#8904)

The CommandSequence command was not widely used and was essentially
just replicating the functionality of a vector of commands. This is work
towards a streamlined parser API.

2 years agoMove non-stream options out of `printer_options.toml` (#8909)
Andres Noetzli [Thu, 23 Jun 2022 19:25:29 +0000 (12:25 -0700)]
Move non-stream options out of `printer_options.toml` (#8909)

After #8827, we automatically generate code for the options listed in printer_options.toml, which allows those options to be set on input/output streams. Some of the options that are currently in printer_options.toml are not a good fit for that and this commit moves them out of the file. This is in preparation of making that stream options public (or at public in the parser), because some commands require setting stream options.

2 years agoFix explanation for strings unit oob inference (#8908)
Andrew Reynolds [Thu, 23 Jun 2022 15:42:07 +0000 (10:42 -0500)]
Fix explanation for strings unit oob inference (#8908)

Fixes #8906.

2 years agoAdd set.fold operator (#8867)
mudathirmahgoub [Thu, 23 Jun 2022 14:18:41 +0000 (09:18 -0500)]
Add set.fold operator (#8867)

2 years agoFix rewrite for `(to_int real.pi)` (#8907)
Andres Noetzli [Thu, 23 Jun 2022 13:44:41 +0000 (06:44 -0700)]
Fix rewrite for `(to_int real.pi)` (#8907)

Fixes #8905. (to_int real.pi) was returning a real constant instead of
an integer, making the type of the rewritten term wrong.

2 years agoFix handling of injectivity for str.unit (#8899)
Andrew Reynolds [Thu, 23 Jun 2022 00:45:52 +0000 (19:45 -0500)]
Fix handling of injectivity for str.unit (#8899)

Fixes #8890.

2 years agoprint run_process command (#8859)
mudathirmahgoub [Wed, 22 Jun 2022 22:51:15 +0000 (17:51 -0500)]
print run_process command (#8859)

2 years agoRemove `Command::clone()` (#8903)
Andres Noetzli [Wed, 22 Jun 2022 22:26:23 +0000 (15:26 -0700)]
Remove `Command::clone()` (#8903)

This code was unused. This is work towards a streamlined parser API.

2 years agoSimplify printing of command results (#8902)
Andres Noetzli [Wed, 22 Jun 2022 21:55:52 +0000 (14:55 -0700)]
Simplify printing of command results (#8902)

This moves redundant code from `Command::printResult()` overrides to the
base method. This is a step towards simplifying printing options, which
is needed to fix #8893 (which itself is a step towards a parser API).

2 years agoAvoid quoting symbols already surrounded with vertical bars (#8896)
mudathirmahgoub [Wed, 22 Jun 2022 21:30:14 +0000 (16:30 -0500)]
Avoid quoting symbols already surrounded with vertical bars (#8896)

This PR fixes the issue of replacing bars with underscores in already quoted symbols.
For example previously this line would print |_a _|

std::cout << d_solver.declareFun("|a |", {}, d_solver.getRealSort());
Now it prints |a |.

2 years agoFix sort inference for equality over finite types (#8897)
Andrew Reynolds [Wed, 22 Jun 2022 18:16:00 +0000 (13:16 -0500)]
Fix sort inference for equality over finite types (#8897)

Sort inference for equality was not considering equality over some finite types, leading to potential solution soundness.

Fixes #8883.

2 years agoAdd type to uninterpreted constant values (#8891)
mudathirmahgoub [Wed, 22 Jun 2022 01:56:01 +0000 (20:56 -0500)]
Add type to uninterpreted constant values (#8891)

Before
```smt2
(define-fun x () UInt (as @a_0 UInt))
(define-fun y () Atom (as @a_0 Atom))
```
After

```smt2
(define-fun x () UInt (as @UInt_0 UInt))
(define-fun y () Atom (as @Atom_0 Atom))
```

2 years ago[Parser] Rename generated `.c` to `.cpp` files (#8894)
Andres Noetzli [Wed, 22 Jun 2022 01:36:22 +0000 (18:36 -0700)]
[Parser] Rename generated `.c` to `.cpp` files (#8894)

Using Clang on my machine, I am seeing the following warning:

```
clang-13: warning: treating 'c' input as 'c++' when in C++ mode, this behavior is deprecated [-Wdeprecated]
```

This is because we are treating the generated `.c` files as C++
files. To make our build system more robust, this commit
changes our command for generating files to rename the
generated files to use the `.cpp` extension.

2 years agoRemove unused `DeclarationSequence` command (#8892)
Andres Noetzli [Tue, 21 Jun 2022 20:23:54 +0000 (13:23 -0700)]
Remove unused `DeclarationSequence` command (#8892)

2 years agoRemove redundant projection operators (#8889)
mudathirmahgoub [Sat, 18 Jun 2022 17:31:08 +0000 (12:31 -0500)]
Remove redundant projection operators (#8889)

This removes all projection operators for tuples and tables except a generic one `ProjectOp`.
It also updates the number of indices and other issues in cvc5.cpp

2 years agoAdd support for operators with same payload (#8886)
Andres Noetzli [Fri, 17 Jun 2022 19:57:24 +0000 (12:57 -0700)]
Add support for operators with same payload (#8886)

This fixes an issue with supporting operators with the same payload. It
changes the API to use the `mkConst()` overload that passes an explicit
kind, which is required when the same payload is shared by multiple
kinds.

2 years ago[CMake] Remove redundant code (#8885)
Andres Noetzli [Thu, 16 Jun 2022 18:33:56 +0000 (11:33 -0700)]
[CMake] Remove redundant code (#8885)

2 years agoDisable parser regression for competition builds (#8884)
Andres Noetzli [Wed, 15 Jun 2022 20:53:41 +0000 (13:53 -0700)]
Disable parser regression for competition builds (#8884)

Competition builds do not print parser errors. This leads to a Buildbot
failure on one of our regressions for the competition build. Thus, this
commit changes the failing regression to be skipped for competition
builds.

2 years ago[Regressions] Disable ASan on slow regression (#8882)
Andres Noetzli [Wed, 15 Jun 2022 19:45:46 +0000 (12:45 -0700)]
[Regressions] Disable ASan on slow regression (#8882)

This should fix one of our Buildbot failures.

2 years ago[CMake] Fix `install()` commands (#8879)
Andres Noetzli [Tue, 14 Jun 2022 16:15:25 +0000 (09:15 -0700)]
[CMake] Fix `install()` commands (#8879)

This fixes two issues related to `install()` commands:

- It removes the installation of object files from the parser. Before,
  `make install` would add unnecessary object files to the library
  directory.
- It ensures that all artifacts related to the `cvc5` target are
  installed in the library directory. DLL files [count as `RUNTIME`
  artifacts](https://cmake.org/cmake/help/latest/command/install.html),
  so `libcvc5.dll` was not installed in the `lib/` directory with `make
  install`.

2 years agobv sat solvers: Update CaDiCaL and Kissat to most recent release versions. (#8877)
Aina Niemetz [Mon, 13 Jun 2022 12:36:18 +0000 (05:36 -0700)]
bv sat solvers: Update CaDiCaL and Kissat to most recent release versions. (#8877)

2 years agoInfrastructure for portfolio solving (#8709)
Gereon Kremer [Mon, 13 Jun 2022 09:56:54 +0000 (02:56 -0700)]
Infrastructure for portfolio solving (#8709)

We want to replace the set of competition scripts by an internal portfolio mechanism. It seems that this portfolio mechanism is best implemented from scratch in the driver instead of using, e.g., --tlimit or --tlimit-per.

This PR introduces the infrastructure for that, implementing the following approach:
first parse the input until a logic has been specified; if more than one configuration is to be used, parse the remaining commands into a vector; for every configuration, we fork the main process, and in the child process configure the solver and replay the vectors.

2 years ago[Win64] Use `CC_FOR_BUILD` when compiling GMP (#8874)
Andres Noetzli [Fri, 10 Jun 2022 23:17:21 +0000 (16:17 -0700)]
[Win64] Use `CC_FOR_BUILD` when compiling GMP (#8874)

This restores the use of the `CC_FOR_BUILD` environment variable. It was
(accidentally) removed in 4337cdb8e2a071ded73dbc9236c8bb2f4d42e6e5 after
it was added in b0500dd28ec42d6a1bada80d34b74ce8aea896cc. Without
`CC_FOR_BUILD`, cross-compilation of GMP fails on Arch Linux.

2 years ago[Java API] Do not link JNI libraries (#8870)
Andres Noetzli [Thu, 9 Jun 2022 02:30:40 +0000 (19:30 -0700)]
[Java API] Do not link JNI libraries (#8870)

Fixes #8869. We are not using `libjawt.so` or `libjvm.so` (we are not
using the Java Invocation API), so we don't need to link `libcvc5jni`
against `JNI_LIBRARIES`. This change allows us to use cvc5 from Java
without linking against the JNI libraries (see changes in the `examples`
folder).

2 years agoMove slow regression (#8866)
Haniel Barbosa [Tue, 7 Jun 2022 21:46:43 +0000 (18:46 -0300)]
Move slow regression (#8866)

To address a buildbot failure.

2 years agoAllow mixed int/real equalities in non-strict parsing mode (#8865)
Andrew Reynolds [Tue, 7 Jun 2022 21:25:10 +0000 (16:25 -0500)]
Allow mixed int/real equalities in non-strict parsing mode (#8865)

2 years agoAdd set.filter operator and its inference rules (#8856)
mudathirmahgoub [Tue, 7 Jun 2022 18:37:07 +0000 (13:37 -0500)]
Add set.filter operator and its inference rules (#8856)

2 years agoRemove redundant options headers from TPTP parser. (#8864)
Mathias Preiner [Tue, 7 Jun 2022 18:06:37 +0000 (11:06 -0700)]
Remove redundant options headers from TPTP parser. (#8864)

Fixes #8861.

2 years agoAdd str.unit to LFSC signature (#8862)
Andrew Reynolds [Tue, 7 Jun 2022 15:20:14 +0000 (10:20 -0500)]
Add str.unit to LFSC signature (#8862)

Fixes buildbot failure.

2 years agoAdd set.map signature to lfsc (#8860)
mudathirmahgoub [Tue, 7 Jun 2022 03:37:32 +0000 (22:37 -0500)]
Add set.map signature to lfsc (#8860)

Fix buildbot failure

2 years agoUse STRING_NTH in strings reductions and eliminate STRING_TO_CODE (#8851)
Andrew Reynolds [Tue, 7 Jun 2022 00:49:15 +0000 (19:49 -0500)]
Use STRING_NTH in strings reductions and eliminate STRING_TO_CODE (#8851)

This updates our string reductions for `to_lower`, `to_upper`, `from_int`, `to_int` to use STRING_NTH instead of STRING_TO_CODE applied to STRING_SUBSTR.

It optionally replaces STRING_TO_CODE with STRING_NTH during preprocessing (true by default).

This is work towards efficient support for `to_lower`/`to_upper`.

2 years ago[CMake] Improve FindGMP (#8846)
Andres Noetzli [Mon, 6 Jun 2022 22:16:15 +0000 (15:16 -0700)]
[CMake] Improve FindGMP (#8846)

Fixes #8792. This commit fixes issues with/improves our current
implementation of FindGMP:

- Version check that does not rely on regex matches in `gmp.h`. Instead,
  this commit uses a test program that checks at compile-time whether
  the GMP version is recent enough. This is more robust, because on some
  systems (such as Fedora), `gmp.h` includes another file that has that
  version information.
- It now also checks for the `gmpxx.h` header and the `gmpxx` library.
- The commit changes the compile test to use the include directories and
  libraries that were found using `find_path` and `find_library`.

2 years agoDisable `lfsc` tester if `proof` tester is disabled. (#8857)
Abdalrhman Mohamed [Mon, 6 Jun 2022 21:26:56 +0000 (00:26 +0300)]
Disable `lfsc` tester if `proof` tester is disabled. (#8857)

This automatically disables the `lfsc` tester for regressions where `proof` tester is disabled.

2 years agoAdd MBQI to SMT comp script (#8858)
Andrew Reynolds [Mon, 6 Jun 2022 19:19:16 +0000 (14:19 -0500)]
Add MBQI to SMT comp script (#8858)

Also fixes 2 existing issues in the script (that @nafur pointed out).

2 years agoAdd declareOracleFun to the Java API (#8815)
mudathirmahgoub [Mon, 6 Jun 2022 18:58:22 +0000 (13:58 -0500)]
Add declareOracleFun to the Java API (#8815)

2 years agoDisable LFSC for regression with learned rewrite (#8855)
Andrew Reynolds [Sun, 5 Jun 2022 00:09:53 +0000 (19:09 -0500)]
Disable LFSC for regression with learned rewrite (#8855)

Fixes buildbot issues.

2 years agoFix corner case of interpolants from conjectures with no free variables (#8853)
Andrew Reynolds [Sat, 4 Jun 2022 23:27:22 +0000 (18:27 -0500)]
Fix corner case of interpolants from conjectures with no free variables (#8853)

Fixes #8852.

2 years agoAdd inference rules for set.map operator (#8849)
mudathirmahgoub [Fri, 3 Jun 2022 22:24:39 +0000 (17:24 -0500)]
Add inference rules for set.map operator (#8849)

2 years agoFix check for whether a term contains an uninterpreted constant (#8845)
Andrew Reynolds [Fri, 3 Jun 2022 20:02:16 +0000 (15:02 -0500)]
Fix check for whether a term contains an uninterpreted constant (#8845)

Fixes #8842.

We now say "unknown" for the benchmark on that issue.

2 years agoDisable arithmetic static learning when unsat cores are enabled (#8830)
Andrew Reynolds [Fri, 3 Jun 2022 14:51:37 +0000 (09:51 -0500)]
Disable arithmetic static learning when unsat cores are enabled (#8830)

The arithmetic static learner uses non-local reasoning and does not have proof support. Thus it may rewrite A ^ B to A ^ B' where ( A ^ B ) => B', but the preprocessor by default assumes that the replacement is such that B => B'.

This disables the arithmetic static learner when unsat cores are enabled. Other static learning appears to be local and is still enabled.

This further corrects an issue in set_defaults that checked incompatibility with unsat cores based on whether proofs are enabled. We now check compatibility independent of whether proofs are enabled. This also corrects several restrictions on things that previously were treated as being incompatible with unsat cores (but not proof unsat cores) that were spurious.

Fixes #8822.

2 years agoEliminate static options access from pattern term selector (#8825)
Andrew Reynolds [Fri, 3 Jun 2022 13:59:59 +0000 (08:59 -0500)]
Eliminate static options access from pattern term selector (#8825)

Towards eliminating options scopes.

2 years agoPreparation for SEQ_NTH applied to strings (#8779)
Andrew Reynolds [Thu, 2 Jun 2022 20:02:55 +0000 (15:02 -0500)]
Preparation for SEQ_NTH applied to strings (#8779)

No behavior changes in this commit for current main.

2 years ago[proofs] [sat] [cores] Fix unsat cores based on the SAT proof (#8850)
Haniel Barbosa [Thu, 2 Jun 2022 18:49:41 +0000 (15:49 -0300)]
[proofs] [sat] [cores] Fix unsat cores based on the SAT proof (#8850)

The justifications for the theory lemmas (i.e., THEORY_LEMMA steps) sometimes was not being properly connected with the actual clause inserted into the SAT solver, leading to open proofs. The issue was triggered by a regression being added in ##8819, so we don't need to add one here.

2 years agoFix missing conclusion for sep pto neg prop (#8844)
Andrew Reynolds [Thu, 2 Jun 2022 16:37:53 +0000 (11:37 -0500)]
Fix missing conclusion for sep pto neg prop (#8844)

Was introduced in the refactoring in #8768.

Fixes #8841.

2 years agoRestricting the bit-width in int-to-bv (#8814)
yoni206 [Thu, 2 Jun 2022 03:26:45 +0000 (06:26 +0300)]
Restricting the bit-width in int-to-bv (#8814)

`cvc5` only supports bit-widths of `unsigned` size for BitVector sorts (see, e.g., [here](https://github.com/cvc5/cvc5/blob/4338d9d49a41022d34cd4cbabf17a66fdf39efae/src/expr/node_manager_template.cpp#L178)).

This checks that the provided bit-width for the `int-to-bv` option is in the right range.

Fixes https://github.com/cvc5/cvc5-projects/issues/425 and includes a regression that is based on the test from the issue.

2 years agoDisable arrays in eager bit-blasting (#8785)
yoni206 [Thu, 2 Jun 2022 03:08:43 +0000 (06:08 +0300)]
Disable arrays in eager bit-blasting (#8785)

Fixes cvc5/cvc5-projects#461 . This does not allow arrays in eager bit-blasting, that is, only QF_BV and QF_UFBV are allowed. The reason is that Ackermannization (which is turned on in eager bit-blasting) eliminates array operators but does not eliminate array variables, that later cause a logic exception.

2 years agoMake interpolation robust to conjectures with no shared variables (#8840)
Andrew Reynolds [Wed, 1 Jun 2022 12:03:04 +0000 (07:03 -0500)]
Make interpolation robust to conjectures with no shared variables (#8840)

Fixes #8833.

2 years agoRefactor how options are passed to the printer (#8827)
Gereon Kremer [Wed, 1 Jun 2022 03:57:52 +0000 (20:57 -0700)]
Refactor how options are passed to the printer (#8827)

Right now, the printers expect some options to be passed explicitly and read other options statically from the options object.
This refactors this, using the `ioutils` utility which we already use to store option values in the private storage associated with output streams. In detail, does a couple of things:
- the `mkoptions.py` script now generates the `options/io_utils.*` files to handle all options defined in the `printer` options module
- reading the necessary options from the ostreams is pushed into the printers themselves
- explicit options are removed from (almost) all `toStream()` functions
- a few options are moved to the `printer` options module (making the `printSuccess` utility obsolete)

2 years agoMake subs minimize utility robust to non-constant evaluation (#8839)
Andrew Reynolds [Tue, 31 May 2022 21:03:31 +0000 (16:03 -0500)]
Make subs minimize utility robust to non-constant evaluation (#8839)

Fixes #8834.

2 years agoFix issues with to_real around coverings solver (#8837)
Gereon Kremer [Tue, 31 May 2022 19:28:52 +0000 (12:28 -0700)]
Fix issues with to_real around coverings solver (#8837)

This PR fixes two issues with the (missing) handling of to_real.
The first is that equality substitution was not aware of to_real yet, possible introducing models for both x and (to_real x).
The second is that the conversion to libpoly polynomials would also not properly unpack to_real expressions.
Fixes #8835.

2 years agoFix FindCaDiCaL script (#8838)
Gereon Kremer [Tue, 31 May 2022 18:23:33 +0000 (11:23 -0700)]
Fix FindCaDiCaL script (#8838)

This fixes issues with finding a system-installed cadical.
Fixes #8836.

2 years agoUpdate to GoogleTest 1.11.0 (#8813)
yoni206 [Tue, 31 May 2022 15:47:36 +0000 (18:47 +0300)]
Update to GoogleTest 1.11.0 (#8813)

Using GoogleTest 1.10.0, when trying to build unit tests on m1 mac an error about deprecated methods fails the compilation of gtest.

2 years agoEliminate more static options accesses (#8832)
Andrew Reynolds [Fri, 27 May 2022 23:26:50 +0000 (18:26 -0500)]
Eliminate more static options accesses (#8832)

2 years agoEliminate static options access for central ee (#8823)
Andrew Reynolds [Fri, 27 May 2022 20:56:15 +0000 (15:56 -0500)]
Eliminate static options access for central ee (#8823)

Also refactors TheoryEngine to not maintain its own reference to logic info and an accessor to it.

Towards eliminating option scopes.

2 years agoEliminate static options access in skolemize (#8831)
Andrew Reynolds [Fri, 27 May 2022 20:11:34 +0000 (15:11 -0500)]
Eliminate static options access in skolemize (#8831)

2 years agoFix mixed arithmetic issue in relevant domain (#8826)
Andrew Reynolds [Fri, 27 May 2022 18:33:30 +0000 (13:33 -0500)]
Fix mixed arithmetic issue in relevant domain (#8826)

Fixes #8821.

2 years agoEliminate static options access in BV inverter (#8829)
Andrew Reynolds [Fri, 27 May 2022 17:58:30 +0000 (12:58 -0500)]
Eliminate static options access in BV inverter (#8829)

2 years agoMake Rewriter::rewrite non-static (#8828)
Andrew Reynolds [Fri, 27 May 2022 15:53:07 +0000 (10:53 -0500)]
Make Rewriter::rewrite non-static (#8828)

This furthermore eliminates smt::currentSolverEngine.

2 years agoUse function array constants in HO solver (#8818)
Andrew Reynolds [Thu, 26 May 2022 20:16:15 +0000 (15:16 -0500)]
Use function array constants in HO solver (#8818)

This makes lambdas rewrite to function array constants when possible. This extends our HO solver and utilities to be robust to check whether a node represents a lambda (uf::FunctionConst::toLambda).

This furthermore removes the isConst rule for LAMBDA; lambdas are never constant.

The PR also improves our check-model so that warnings are not thrown if rewriting can show that the model value of a term is equivalent modulo rewriting to its representative in the model equality engine.

This eliminates the last remaining static calls to rewrite. This is work towards eliminating SmtEngineScope.

2 years agoMake sure phase-shift lemma is properly typed (#8824)
Gereon Kremer [Thu, 26 May 2022 16:45:13 +0000 (09:45 -0700)]
Make sure phase-shift lemma is properly typed (#8824)

This PR addresses #8773 by making sure that the phase shift lemmas generated by the sine solver are properly typed.

2 years agoEliminate some static options access (#8795)
Andrew Reynolds [Wed, 25 May 2022 22:51:38 +0000 (17:51 -0500)]
Eliminate some static options access (#8795)

In preparation for eliminating options scopes.

2 years ago[proofs] [alethe] Remove static call to options from post-processor (#8817)
Haniel Barbosa [Wed, 25 May 2022 21:27:47 +0000 (18:27 -0300)]
[proofs] [alethe] Remove static call to options from post-processor (#8817)

2 years agoAdd model-based quantifier instantiation (#8729)
Andrew Reynolds [Wed, 25 May 2022 20:52:08 +0000 (15:52 -0500)]
Add model-based quantifier instantiation (#8729)

This is a straightforward reimplementation of Ge/deMoura from CAV 2009.

2 years agoEliminate static access to dtSharedSelectors (#8804)
Andrew Reynolds [Wed, 25 May 2022 20:16:40 +0000 (15:16 -0500)]
Eliminate static access to dtSharedSelectors (#8804)

Towards eliminating option scopes.

2 years agoEliminate more static options accesses (#8802)
Andrew Reynolds [Wed, 25 May 2022 19:43:04 +0000 (14:43 -0500)]
Eliminate more static options accesses (#8802)

A block of code changed indentation in the induction solver, this is cleaned to conform to guidelines.

2 years agoIntroduce function array constant (#8793)
Andrew Reynolds [Tue, 24 May 2022 20:01:19 +0000 (15:01 -0500)]
Introduce function array constant (#8793)

This introduces the FUNCTION_ARRAY_CONST kind and its payload FunctionArrayConst.

This is in preparation for refactoring isConst for functions in higher-order.

In particular, the plan is to never consider LAMBDA to denote a value of function sort. Instead, lambdas may be written to function array constants, whose uniqueness is trivial to justify.

This refactoring when completed will furthermore eliminate the last remaining static calls to the rewriter, to be done in a followup PR.

2 years agoFix subtype issues in proofs for nonlinear solver (#8782)
Andrew Reynolds [Tue, 24 May 2022 19:13:29 +0000 (14:13 -0500)]
Fix subtype issues in proofs for nonlinear solver (#8782)

Causes a debug proof failure on proof-new.