cvc5.git
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.

2 years agobv: Disable rule ExtractArith. (#8816)
Aina Niemetz [Tue, 24 May 2022 18:05:40 +0000 (11:05 -0700)]
bv: Disable rule ExtractArith. (#8816)

2 years agoAdd table.group operator (#8731)
mudathirmahgoub [Tue, 24 May 2022 14:51:49 +0000 (09:51 -0500)]
Add table.group operator (#8731)

2 years agoAdd declareOracleFun to API (#8794)
Andrew Reynolds [Tue, 24 May 2022 14:07:42 +0000 (09:07 -0500)]
Add declareOracleFun to API (#8794)

Java and Python will be added in followup PRs.

2 years agoRemove spurious assertion in isLegalElimination (#8812)
Andrew Reynolds [Mon, 23 May 2022 21:11:07 +0000 (16:11 -0500)]
Remove spurious assertion in isLegalElimination (#8812)

Fixes #8805.

The isLegalElimination method correctly catches Int -> Real as an illegal elimination.

2 years agoMake model core robust to when we cannot show the model satisfies input (#8811)
Andrew Reynolds [Mon, 23 May 2022 20:46:51 +0000 (15:46 -0500)]
Make model core robust to when we cannot show the model satisfies input (#8811)

Fixes #8807.

2 years agobv: Add resource limits support for CaDiCaL. (#8788)
Mathias Preiner [Sun, 22 May 2022 16:04:55 +0000 (09:04 -0700)]
bv: Add resource limits support for CaDiCaL. (#8788)

Fixes #8776.

2 years agoSimplification of smt2 printer for type ascriptions (#8801)
Andrew Reynolds [Sun, 22 May 2022 00:02:54 +0000 (19:02 -0500)]
Simplification of smt2 printer for type ascriptions (#8801)

Previously had code for dealing with subtypes

2 years agoMove smt_util to preprocessing/util (#8799)
Andrew Reynolds [Sat, 21 May 2022 23:43:30 +0000 (18:43 -0500)]
Move smt_util to preprocessing/util (#8799)

src/smt_util contains a single file that is only used by the miplib trick preprocessing pass. This moves it to preprocessing/util.

2 years agoReenable assertion in skolem definition manager (#8797)
Andrew Reynolds [Sat, 21 May 2022 23:23:56 +0000 (18:23 -0500)]
Reenable assertion in skolem definition manager (#8797)

This reenables a variant of an assertion that was deleted in #8749, a weaker version of that assertion should now hold.

2 years agoAdd option to send all instantiations in a bounded range (#8796)
Andrew Reynolds [Sat, 21 May 2022 22:58:11 +0000 (17:58 -0500)]
Add option to send all instantiations in a bounded range (#8796)

There is a block of code in FMF instantiation that is questionable whether it is helpful, in particular for dealing with string reductions for long strings.

2 years agoAdd cross-compilation for arm64 on macOS (#8758)
Gereon Kremer [Sat, 21 May 2022 22:14:45 +0000 (15:14 -0700)]
Add cross-compilation for arm64 on macOS (#8758)

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
2 years agoMore removing of unused code (#8806)
Andrew Reynolds [Fri, 20 May 2022 17:49:57 +0000 (12:49 -0500)]
More removing of unused code (#8806)

2 years agoTrying to break cycles when printing a .dot DAG (#8698)
vinciusb [Fri, 20 May 2022 13:55:02 +0000 (10:55 -0300)]
Trying to break cycles when printing a .dot DAG (#8698)

Change the way cvc5 traverse and print the proof when --proof-dot-dag option is used. The main change is related to the way the printer deals with cycles between proof nodes that are in a ancestor/descendant relationship. The new conditions are:

- If any proof node under a first proof node has the hash equal to the first one, this would introduces a cycle. To avoid it, then no sharing between nodes happens in this case.

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com
2 years agoNew way to identify THEORY_LEMMA clusters when printing in the .dot format (#8745)
vinciusb [Fri, 20 May 2022 13:36:04 +0000 (10:36 -0300)]
New way to identify THEORY_LEMMA clusters when printing in the .dot format (#8745)

Change the way cvc5 identifies THEORY_LEMMA clusters when --print-dot-clusters option is used. Previously, only proof nodes with SCOPE rule after a CNF cluster could identify a THEORY_LEMMA cluster. Now, any of the following rules, after a CNF cluster, can identify it:

1. SCOPE
2. THEORY_LEMMA
3. Any rule R in the following range: CNF_ITE_NEG3 < R < LFSC_RULE

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com
2 years agoMinor deleting of unused code (#8800)
Andrew Reynolds [Thu, 19 May 2022 17:30:05 +0000 (12:30 -0500)]
Minor deleting of unused code (#8800)

Towards improving coverage.

2 years agoAdd options and regressions to increase coverage (#8803)
Andrew Reynolds [Thu, 19 May 2022 17:09:09 +0000 (12:09 -0500)]
Add options and regressions to increase coverage (#8803)

Also corrects an issue with the text interface. When get-model is used with model cores, we do not currently filter the output. This ensures that we do.

2 years agoBasic cleanup of sep theory (#8790)
Andrew Reynolds [Wed, 18 May 2022 15:35:51 +0000 (10:35 -0500)]
Basic cleanup of sep theory (#8790)

Most of the simplifications are due to the fact that we only handle a single heap type. (The solver was initially designed to potentially handle more than one heap type).

2 years agoMake skolem definition manager robust to definitions for already asserted skolems...
Andrew Reynolds [Wed, 18 May 2022 13:42:48 +0000 (08:42 -0500)]
Make skolem definition manager robust to definitions for already asserted skolems (#8749)

It makes the skolem definition manager more robust so that skolem definitions can be added for skolems that have already appeared in asserted literals. This was the initial motivation for the change in ordering. As a result, fixes #8347 and fixes cvc5/cvc5-projects#512. It also optimizes this class in a few ways.

It also comments more on the change to PropEngine introduced here: #8301 which led to performance degradation on a set of string benchmarks of interest.

2 years agoEliminate subtypes (#8783)
Andrew Reynolds [Wed, 18 May 2022 06:01:20 +0000 (01:01 -0500)]
Eliminate subtypes (#8783)

2 years agoRefactor declare oracle command (#8742)
Andrew Reynolds [Tue, 17 May 2022 22:26:53 +0000 (17:26 -0500)]
Refactor declare oracle command (#8742)

In preparation for adding oracle functions to API.

2 years agoMinor cleanup of datatypes theory (#8791)
Andrew Reynolds [Tue, 17 May 2022 21:08:02 +0000 (16:08 -0500)]
Minor cleanup of datatypes theory (#8791)

2 years agoFix LFSC proof construction for concat clash of sequences (#8739)
Andrew Reynolds [Tue, 17 May 2022 19:16:56 +0000 (14:16 -0500)]
Fix LFSC proof construction for concat clash of sequences (#8739)

Changes the internal proof calculus to require an explicit disequality between character constants for clashing sequences.

Makes it so that the disequality is expanded prior to proof post-processing, so that character clashing is properly expanded as it may require rewriting.

2 years agodocs: Remove references to checkEntailed(). (#8789)
Mathias Preiner [Tue, 17 May 2022 18:43:52 +0000 (11:43 -0700)]
docs: Remove references to checkEntailed(). (#8789)

2 years agoGeneralize pto constraint tracking for multiple heaps in sep theory (#8768)
Andrew Reynolds [Tue, 17 May 2022 14:05:49 +0000 (09:05 -0500)]
Generalize pto constraint tracking for multiple heaps in sep theory (#8768)

Fixes #8659.

2 years agoAdd getInterpolant with a grammar in the unit test for all language bindings (#8775)
Ying Sheng [Tue, 17 May 2022 13:40:32 +0000 (06:40 -0700)]
Add getInterpolant with a grammar in the unit test for all language bindings (#8775)

Add getInterpolant with a grammar in the unit test for all language bindings

2 years agonew test for resolved issue (#8784)
yoni206 [Tue, 17 May 2022 13:18:31 +0000 (16:18 +0300)]
new test for resolved issue (#8784)

#8412 is now fixed on main. This PR adds a regression from that issue.
closes #8412 .

2 years agoLast remaining fixes for eliminating subtyping (#8772)
Andrew Reynolds [Mon, 16 May 2022 22:46:41 +0000 (17:46 -0500)]
Last remaining fixes for eliminating subtyping (#8772)

Also fixes a debug failure for the nightlies.

This also changes mkTuple to not rely on subtyping (this method should regardless be deleted from our API, as it is not the recommended way of constructing tuples).

2 years ago[proofs] Generalize handling of constants merged in equality engine (#8781)
Haniel Barbosa [Mon, 16 May 2022 22:05:10 +0000 (19:05 -0300)]
[proofs] Generalize handling of constants merged in equality engine (#8781)

Previously the reconstruction of EUF proofs was not considering a corner case from the equality engine where it infers that two constants are disequal from other equalities, but these other equalities all become of the form x = x at the time we are explaining this disquality. In this case the constant disequality is justified with MERGED_THROUGH_CONSTANTS rather than MERGED_THROUGH_TRANS as other disequalities.

2 years agoRename equality engine trace to print E-graph (#8780)
Haniel Barbosa [Mon, 16 May 2022 21:07:59 +0000 (18:07 -0300)]
Rename equality engine trace to print E-graph (#8780)

The current trace depends on `-t equality::internal`, which is pointless and
leads to confusion when one inevitably forgets this when checking which trace to
use to print the E-graph and the output does not contain it.

2 years agoEliminate the use of CAST_TO_REAL (#8759)
Andrew Reynolds [Sun, 15 May 2022 17:11:42 +0000 (12:11 -0500)]
Eliminate the use of CAST_TO_REAL (#8759)

This simplifies the implementation of the API by not relying on CAST_TO_REAL. This was used as a way of manually marking integral reals as having real type.

2 years agoEliminate ops for parameterized type constructors (#8761)
Andrew Reynolds [Sun, 15 May 2022 16:30:26 +0000 (11:30 -0500)]
Eliminate ops for parameterized type constructors (#8761)

We now preserve types when rewriting. This means that we no longer need to use operators that store the type of terms to construct in the cases of bags, sets, and sequences.