cvc5.git
2 years ago[CI] Make building static/shared configurable (#8272)
Andres Noetzli [Fri, 11 Mar 2022 14:48:39 +0000 (06:48 -0800)]
[CI] Make building static/shared configurable (#8272)

This commit changes our CI workflow to actually pass through
build-shared and build-static to the configure-and-build action
and fixes how the condition is checked there. If we just pass through
the inputs, then the condition "${{ inputs.build-shared }}" != "true"
would be true (i.e., the step would be skipped) if
build-shared/build-static are not set explicitly in ci.yml because
of the default values for build-shared/build-static in ci.yml.

2 years agoRefactor kinds parser (#8287)
Andres Noetzli [Fri, 11 Mar 2022 01:54:33 +0000 (17:54 -0800)]
Refactor kinds parser (#8287)

This commit does a minor refactoring of the kinds parser. It moves the
Python name formatting out of parsekinds.py, adds parsekinds.py as a
dependency for the Java kinds generator, and reformats the scripts using
YAPF.

This is the first step towards generalizing the scripts for other enums.

2 years agoFix issue with subtyping from set membership in models (#8282)
Andrew Reynolds [Thu, 10 Mar 2022 22:30:10 +0000 (16:30 -0600)]
Fix issue with subtyping from set membership in models (#8282)

Fixes cvc5/cvc5-projects#480.

That benchmark now times out.

2 years agoFix theoryOf call in get equality status (#8279)
Andrew Reynolds [Thu, 10 Mar 2022 20:41:26 +0000 (14:41 -0600)]
Fix theoryOf call in get equality status (#8279)

Should depend on uninterpreted sort owner.

Fixes cvc5/cvc5-projects#476.

2 years agoEliminate unecessary datatype options (#8280)
Andrew Reynolds [Thu, 10 Mar 2022 19:20:35 +0000 (13:20 -0600)]
Eliminate unecessary datatype options (#8280)

2 years agoFix cvc5-projects issue 475 (#8278)
mudathirmahgoub [Thu, 10 Mar 2022 18:49:31 +0000 (12:49 -0600)]
Fix cvc5-projects issue 475 (#8278)

Fixes cvc5/cvc5-projects#475.

2 years agoAdd output -o pre-asserts (#8270)
Andrew Reynolds [Thu, 10 Mar 2022 18:28:54 +0000 (12:28 -0600)]
Add output -o pre-asserts (#8270)

Analogous to -o post-asserts.

2 years agoDisable timing out regressions (#8273)
Andrew Reynolds [Thu, 10 Mar 2022 17:02:14 +0000 (11:02 -0600)]
Disable timing out regressions (#8273)

Fixes several of the nightly failures.

Both benchmarks involve undecidable logics and are delicate.

Also should fix the errors involving (missing) SyGuS warnings in the nightlies, which requires competition build to be disabled.

2 years agoFix regression errors for arm64 nightlies. (#8268)
Mathias Preiner [Thu, 10 Mar 2022 00:28:44 +0000 (16:28 -0800)]
Fix regression errors for arm64 nightlies. (#8268)

2 years agoRename expert statistics to internal, add documentation (#8262)
Gereon Kremer [Wed, 9 Mar 2022 23:40:43 +0000 (00:40 +0100)]
Rename expert statistics to internal, add documentation (#8262)

We decided to rename statistics from "public / expert" to "public / internal". Also, this adds some reasonable documentation about statistics to our online docs.

2 years agoClear obsolete pending lemmas in arithmetic (#8236)
Gereon Kremer [Wed, 9 Mar 2022 16:37:13 +0000 (17:37 +0100)]
Clear obsolete pending lemmas in arithmetic (#8236)

Arithmetic generally generates nonlinear lemmas as full effort checks, but only sends them out in the subsequent last call effort check. If this one does not happen, the next full effort check still has pending lemmas that may not only be irrelevant now, but possibly carry proofs that are already out of scope.
This PR makes sure that such lemmas are always pruned.
Fixes cvc5/cvc5-projects#465

2 years agoChange interface for printing instantiations in the API (#8251)
Andrew Reynolds [Wed, 9 Mar 2022 14:58:27 +0000 (08:58 -0600)]
Change interface for printing instantiations in the API (#8251)

Furthermore note that this should take several modes, similar to the discussion with `blockModel` / `getLearnedLiterals`.  It is currently limited to a fixed print mode.

2 years agoUse expression mining independent of whether sygus stream is enabled (#8250)
Andrew Reynolds [Wed, 9 Mar 2022 11:42:01 +0000 (05:42 -0600)]
Use expression mining independent of whether sygus stream is enabled (#8250)

Since it is possible to use SyGuS in incremental mode, e.g. for `get-abduct-next`, our expression mining, e.g. for filtering weak solutions, should apply independent of whether sygusStream is enabled.  This refactors the SyGuS solver so that we do so.

2 years agoAdd REGEXP_ALL kind to API (#8264)
Andrew Reynolds [Wed, 9 Mar 2022 10:14:39 +0000 (04:14 -0600)]
Add REGEXP_ALL kind to API (#8264)

Previously was immediately converted to (re.* re.allchar) upon construction.

2 years agoAdd regression for fixed issue 6700 (#8265)
Andrew Reynolds [Wed, 9 Mar 2022 01:42:37 +0000 (19:42 -0600)]
Add regression for fixed issue 6700 (#8265)

Fixes #6700.

2 years agoEliminate the APPLY_SELECTOR_TOTAL kind (#8266)
Andrew Reynolds [Wed, 9 Mar 2022 00:21:34 +0000 (18:21 -0600)]
Eliminate the APPLY_SELECTOR_TOTAL kind (#8266)

2 years agoProduce intermediate json output for coverage (#8252)
Gereon Kremer [Tue, 8 Mar 2022 23:19:36 +0000 (00:19 +0100)]
Produce intermediate json output for coverage (#8252)

This splits the generation of coverage information into two steps, generating an intermediate json file. This allows further tooling to used this json information: we plan to check whether the APIs (and their tests) are complete by looking at their code coverage within the cpp api.

2 years agoDo not expand APPLY_SELECTOR (#8174)
Andrew Reynolds [Tue, 8 Mar 2022 22:38:20 +0000 (16:38 -0600)]
Do not expand APPLY_SELECTOR (#8174)

Currently we expand (sel_C_n x) to (ite (is-C x) (sel_C_n_total x) (uf x)) during ppRewrite. This introduces ITEs very eagerly and moreover is not necessary since we do congruence over selectors.

This makes it so that we don't do this expansion. The code changes to use APPLY_SELECTOR everywhere instead of APPLY_SELECTOR_TOTAL, which can be deleted in a followup PR. It makes some of the datatype utilities more robust and independent of options.

This required changing one detail of the sygus solver to not do evaluation unfolding in cases where a selector chain was wrongly applied, as this now will not rewrite to a constant.

2 years ago[API/Python] Add support for `Solver::getProof()` (#8259)
Andres Noetzli [Tue, 8 Mar 2022 22:02:50 +0000 (14:02 -0800)]
[API/Python] Add support for `Solver::getProof()` (#8259)

This commit implements support for Solver::getProof() in the Python
API, which was missing before.

2 years agoGuard another case of non-termination in quantifiers rewriting (#8255)
Andrew Reynolds [Tue, 8 Mar 2022 21:17:32 +0000 (15:17 -0600)]
Guard another case of non-termination in quantifiers rewriting (#8255)

Fixes cvc5/cvc5-projects#152.

2 years agoMake one CI job not use libpoly (#8261)
Gereon Kremer [Tue, 8 Mar 2022 20:34:48 +0000 (21:34 +0100)]
Make one CI job not use libpoly (#8261)

This PR fixes a regression that was missing the REQUIRES: poly annotation. To avoid these issues in the future, we add --no-poly to one of the CI jobs.

2 years agoFixes and additions to LFSC signature (#8205)
Andrew Reynolds [Tue, 8 Mar 2022 18:29:06 +0000 (12:29 -0600)]
Fixes and additions to LFSC signature (#8205)

Includes:

Proper printing of various FP terms and constants.
Distinguishing "variants" of overloaded symbols, in case a user declares 2 symbols with the same name.
Miscellaneous fixes for printing terms.

2 years agoEliminate shadowing in the quantifiers rewriter (#8244)
Andrew Reynolds [Tue, 8 Mar 2022 07:12:23 +0000 (01:12 -0600)]
Eliminate shadowing in the quantifiers rewriter (#8244)

Fixes #8227.

Recently, we allowed unevaluatable terms to be in the range of substitutions solved during preprocess.

In very rare cases, it may be the case that a quantified formula is substituted into itself, e.g.:
forall x. P(x, b) where b was solved to be forall x. P(x, c)
This leads to forall x. P(x, forall x. P(x, c)) where x is shadowed.

To resolve this issue, we eliminate shadowing in the quantifiers rewriter, e.g. we rewrite the above to forall x. P(x, forall y. P(y, c)).

An alternative solution would be to ensure we use capture avoiding substitutions, but this severely complicates our usage of substitutions throughout the preprocessor / proof system.

This PR also eliminates some dead code in the quantifiers rewriter.

2 years agoAdd unit for fixed project issue (#8253)
Andrew Reynolds [Tue, 8 Mar 2022 02:53:18 +0000 (20:53 -0600)]
Add unit for fixed project issue (#8253)

Fixes cvc5/cvc5-projects#377.

Was not able to reproduce this on master.

2 years agoScript to list not covered API functions (#8254)
Gereon Kremer [Tue, 8 Mar 2022 02:13:43 +0000 (03:13 +0100)]
Script to list not covered API functions (#8254)

Adds a script that lists all functions from the cpp API not covered by the current coverage information.

2 years agoRerun failed tests in CI (#8258)
Gereon Kremer [Tue, 8 Mar 2022 01:29:03 +0000 (02:29 +0100)]
Rerun failed tests in CI (#8258)

This commit makes our CI rerun failed tests to have the error output at the bottom of the log. This simplifies retrieving the errors from CI logs.

2 years agoDon't run the pypi packaging job on forks (#8256)
Gereon Kremer [Tue, 8 Mar 2022 00:49:15 +0000 (01:49 +0100)]
Don't run the pypi packaging job on forks (#8256)

Right now, the nightly pypi packaging job runs on all forks. This commit disabled this.

See https://github.community/t/do-not-run-cron-workflows-in-forks/17636

2 years agoUpdate documentation of `Solver::getUnsatCore()` (#8239)
Andres Noetzli [Mon, 7 Mar 2022 22:11:55 +0000 (14:11 -0800)]
Update documentation of `Solver::getUnsatCore()` (#8239)

Fixes https://github.com/cvc5/cvc5-projects/issues/308. This commit adds
documentation for the differences between `Solver::getUnsatCore()` and
SMT-LIB's `(get-unsat-core)`.

2 years agoFix docs warnings (#8019)
Gereon Kremer [Mon, 7 Mar 2022 21:22:44 +0000 (22:22 +0100)]
Fix docs warnings (#8019)

This fixes a bunch of warnings when generating our sphinx documentation.
They are mostly related to incorrect indentation/spacing, line breaks where
no line breaks should be, or missing code blocks.
Note that running clang-format causes some of these issues.

2 years agoProper error message for non-first-class sets (#8245)
Andrew Reynolds [Mon, 7 Mar 2022 20:33:52 +0000 (14:33 -0600)]
Proper error message for non-first-class sets (#8245)

Fixes cvc5/cvc5-projects#347.

2 years agoTry harder to show that a RAN is rational (#8230)
Gereon Kremer [Mon, 7 Mar 2022 15:31:07 +0000 (16:31 +0100)]
Try harder to show that a RAN is rational (#8230)

We try to rewrite real algebraic numbers to rationals. This is important to, e.g., allow the linear solver to see rational constants at all. Refining real algebraic numbers is done lazily, and (almost) any operation may trigger a refinement that makes libpoly realize it actually is rational. Thus, even the mere act of creating a node out of a real algebraic number may do this (it hashes it).
This PR thus introduces a fixed-point loop into the RAN node constructor that defends against this case.
Fixes #8226.

2 years agoDisallow models with `--arrays-weak-equiv` (#8217)
Andres Noetzli [Sun, 6 Mar 2022 16:02:26 +0000 (08:02 -0800)]
Disallow models with `--arrays-weak-equiv` (#8217)

Fixes #2007. We currently do not support generating models when
`--arrays-weak-equiv` is enabled. This commit adds a corresponding
user-facing error message.

2 years agoUnit tests for fixed projects issues (#8229)
Andrew Reynolds [Sat, 5 Mar 2022 20:50:25 +0000 (14:50 -0600)]
Unit tests for fixed projects issues (#8229)

Fixes cvc5/cvc5-projects#421.
Fixes cvc5/cvc5-projects#361.

2 years agoMake seq.unit robust wrt subtyping (#8209)
Andrew Reynolds [Sat, 5 Mar 2022 19:43:43 +0000 (13:43 -0600)]
Make seq.unit robust wrt subtyping (#8209)

Fixes cvc5/cvc5-projects#384.
Fixes cvc5/cvc5-projects#426.
Fixes cvc5/cvc5-projects#427.
Fixes cvc5/cvc5-projects#429.

Issue cvc5/cvc5-projects#423 still remains, to be addressed in a followup PR.

Also fixes issues with subtyping in how sequence constants are printed.

Note this solution is required since we are not ready to eliminate arithmetic subtyping in the short term. These changes will be unnecessary when this happens.

2 years ago[Docs] Add missing requirement (#8238)
Andres Noetzli [Sat, 5 Mar 2022 18:00:42 +0000 (10:00 -0800)]
[Docs] Add missing requirement (#8238)

Our docs do not build without the `sphinx-rtd-theme` package. This
commit adds the module as an explicit requirement such that if the
module is missing, building the docs fails when configuring and with a
useful error message.

2 years agoAdd regressions for fixed issue (#8237)
Gereon Kremer [Sat, 5 Mar 2022 01:46:57 +0000 (02:46 +0100)]
Add regressions for fixed issue (#8237)

Adds regressions for an issue that has been fixed in the meantime.
Fixes #4334

2 years agoEnable NL tangent planes by default (#8233)
Andrew Reynolds [Sat, 5 Mar 2022 00:47:13 +0000 (18:47 -0600)]
Enable NL tangent planes by default (#8233)

Fixes cvc5/cvc5-projects#215
Fixes cvc5/cvc5-projects#291
Fixes cvc5/cvc5-projects#292
Fixes cvc5/cvc5-projects#294
Fixes cvc5/cvc5-projects#297

Previously the concern was that this would interfere with e.g. quantifiers + non-linear. However, our strategy is now fair wrt other theories as we send lemmas at LAST_CALL effort, and is properly restricted by the nl-ext mode.

Moreover, this option increases our ability to solve problems (instead of saying "unknown") significantly, even for quantified logics like UFNIA.

2 years agoFix bag.map upwards inferences (#8232)
mudathirmahgoub [Fri, 4 Mar 2022 23:33:47 +0000 (17:33 -0600)]
Fix bag.map upwards inferences (#8232)

2 years agoAdd unit test for fixed issue (#8235)
Gereon Kremer [Fri, 4 Mar 2022 23:09:49 +0000 (00:09 +0100)]
Add unit test for fixed issue (#8235)

This unit test exercised a non-idempotent rewrite for RANs before the rewriter was fully refactored.
Fixed cvc5/cvc5-projects#455

2 years agoRemove spurious assertion in linear solver (#8231)
Gereon Kremer [Fri, 4 Mar 2022 22:31:10 +0000 (23:31 +0100)]
Remove spurious assertion in linear solver (#8231)

This PR removes a spurious assertion about how integer equality should look like. It actually requires that the coefficients of the leading terms on both sides of the equation are positive, which can't be true in general anyway. Note that the regression failed before we refactored the arithmetic rewriter.

Fixes cvc5/cvc5-projects#469

2 years agoGuard recursion into terms during substitution in arithmetic utility (#8234)
Gereon Kremer [Fri, 4 Mar 2022 21:50:32 +0000 (22:50 +0100)]
Guard recursion into terms during substitution in arithmetic utility (#8234)

This PR fixes an issue during variable elimination using equalities in the nonlinear arithmetic solver. We need to make sure that we don't apply the substitutions within terms that are not native arithmetic terms. While we already did that whenever we actually used the resulting term, we did not when we just checked for a possible loop.
Although we always invalidate the substitution cache, the apply method also poisons the actual substitution map. By protecting the calls to apply where we don't actually store the result as well, we avoid this type of "poisoning".
Fixes #8161.

2 years agoFix rewrite rule synthesis for 0-ary operators (#8221)
Andrew Reynolds [Fri, 4 Mar 2022 19:40:30 +0000 (13:40 -0600)]
Fix rewrite rule synthesis for 0-ary operators (#8221)

Fixes cvc5/cvc5-projects#422.

Also changes the default setting for rewrite rule synthesis to check correct of rewrite rules by default.

2 years agoLogic exception when using solution filtering for non-Boolean grammars (#8225)
Andrew Reynolds [Fri, 4 Mar 2022 19:12:52 +0000 (13:12 -0600)]
Logic exception when using solution filtering for non-Boolean grammars (#8225)

Fixes cvc5/cvc5-projects#464.

2 years agoOnly build wheels nightly and for releases (#8223)
Gereon Kremer [Fri, 4 Mar 2022 18:19:39 +0000 (19:19 +0100)]
Only build wheels nightly and for releases (#8223)

We accidentally enabled building the python wheels with every commit. This fixes it to only build them once at night and for releases.

2 years agoAdd regressions for fixed projects issues (#8228)
Andrew Reynolds [Fri, 4 Mar 2022 17:22:18 +0000 (11:22 -0600)]
Add regressions for fixed projects issues (#8228)

Fixes cvc5/cvc5-projects#119
Fixes cvc5/cvc5-projects#135
Fixes cvc5/cvc5-projects#139
Fixes cvc5/cvc5-projects#151
Fixes cvc5/cvc5-projects#155
Fixed cvc5/cvc5-projects#158
Fixes cvc5/cvc5-projects#161
Fixes cvc5/cvc5-projects#165
Fixes cvc5/cvc5-projects#177
Fixes cvc5/cvc5-projects#231
Fixes cvc5/cvc5-projects#232
Fixes cvc5/cvc5-projects#251
Fixes cvc5/cvc5-projects#253
Fixes cvc5/cvc5-projects#264
Fixes cvc5/cvc5-projects#280
Fixes cvc5/cvc5-projects#281
Fixes cvc5/cvc5-projects#282
Fixes cvc5/cvc5-projects#285
Fixes cvc5/cvc5-projects#286
Fixes cvc5/cvc5-projects#290
Fixes cvc5/cvc5-projects#295

2 years agoAdd support for get learned literals in the API (#8099)
Andrew Reynolds [Fri, 4 Mar 2022 14:37:54 +0000 (08:37 -0600)]
Add support for get learned literals in the API (#8099)

This command will eventually take a mode; for now it assumes a default implementation. I've opened cvc5/cvc5-wishues#104 to track this.

This is a feature requested by Certora.

2 years agoFix datatype declaration printing in LFSC printer (#8222)
Andrew Reynolds [Thu, 3 Mar 2022 22:54:27 +0000 (16:54 -0600)]
Fix datatype declaration printing in LFSC printer (#8222)

2 years agoBuild python wheels in our CI (#8087)
Gereon Kremer [Thu, 3 Mar 2022 18:39:16 +0000 (19:39 +0100)]
Build python wheels in our CI (#8087)

This PR integrates building and publishing cvc5 with its base and pythonic python APIs as a package to PyPi into our CI.
We build wheels for Linux and macOS for CPython 3.6 to 3.10 and PyPy 3.7 and 3.8.
The job is run nightly and for a release, and only published to PyPi for a release (as long as there is no reasonable way to automatically prune nightly builds from either PyPi or TestPyPi).

2 years agoGeneralize LFSC string signature to sequences (#8220)
Andrew Reynolds [Thu, 3 Mar 2022 15:59:04 +0000 (09:59 -0600)]
Generalize LFSC string signature to sequences (#8220)

2 years ago[proofs] Alethe: Removed Steps that are Double-Printed (#7754)
Lachnitt [Thu, 3 Mar 2022 12:57:14 +0000 (04:57 -0800)]
[proofs] Alethe: Removed Steps that are Double-Printed (#7754)

This PR fixes that some steps are printed more than once. To this end, it deletes that the reference maps in which the steps are stored are constant and optimizes where the steps are added to the maps. It also stores ProofNodes instead of Nodes in the maps.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2 years agoThrow logic exception if a transcendental function is encountered when nl-ext is...
Andrew Reynolds [Thu, 3 Mar 2022 05:00:32 +0000 (23:00 -0600)]
Throw logic exception if a transcendental function is encountered when nl-ext is not full (#8212)

Fixes cvc5/cvc5-projects#376.

2 years agoAdd regression for fixed issue (#8213)
Andrew Reynolds [Thu, 3 Mar 2022 04:26:54 +0000 (22:26 -0600)]
Add regression for fixed issue (#8213)

Fixes #5815.

This adds the regression, in theory I still think it is possible for the assertion to fail, but I don't think it is worth pursuing right now.

2 years agoImprove error for higher-order logic (#8207)
Andrew Reynolds [Thu, 3 Mar 2022 03:51:42 +0000 (21:51 -0600)]
Improve error for higher-order logic (#8207)

Makes the error more informative when a higher-order function variable is encountered.
Fixes cvc5/cvc5-projects#450.

2 years agocmake: Fix murxla setup. (#8215)
Mathias Preiner [Thu, 3 Mar 2022 02:57:09 +0000 (18:57 -0800)]
cmake: Fix murxla setup. (#8215)

2 years agoIntegrate pythonic api (#8131)
Gereon Kremer [Thu, 3 Mar 2022 02:16:09 +0000 (03:16 +0100)]
Integrate pythonic api (#8131)

We decided we want to ship the pythonic API together with our base python API.
This PR adds a new target cvc5_python_api that first builds the base python API and then copies the pythonic API over. Furthermore we now use the cvc5.pythonic module to generate the corresponding documentation.

2 years agoFix rewriting of mixed-integer atoms (#8214)
Gereon Kremer [Thu, 3 Mar 2022 00:37:05 +0000 (01:37 +0100)]
Fix rewriting of mixed-integer atoms (#8214)

The sixth input from #8159 revealed a subtle issue in our rewriting of arithmetic atoms. As real and integer atoms are rewritten differently, we check this and then call different functions. However, we check this on the original input, although this property can change during rewriting, e.g., when the only real variable vanishes.
This PR fixes this issue.

2 years agoFix issue with dropping non-reduced sine terms (#8211)
Andrew Reynolds [Wed, 2 Mar 2022 23:09:24 +0000 (17:09 -0600)]
Fix issue with dropping non-reduced sine terms (#8211)

Fixes #8208.

A spurious "break" was leftover from when this code was a loop, this meant when the first reduced term was encountered, it ignored the remainder.

2 years agoFix models involving cardinality of sets of finite type (#8206)
Andrew Reynolds [Wed, 2 Mar 2022 22:36:05 +0000 (16:36 -0600)]
Fix models involving cardinality of sets of finite type (#8206)

Was caused by a flag not being reset, thus making it so that subsequent models did not use exclusion sets.

Fixes #5402. (Fixes the last benchmark on that issue, the first two are fixed by #8201).

2 years agoAlways purify universe from set minus (#8201)
Andrew Reynolds [Wed, 2 Mar 2022 21:55:52 +0000 (15:55 -0600)]
Always purify universe from set minus (#8201)

This fixes a bug in our handling of set cardinality + set universe (also used for set complement).

The bug was caused by using the rewritten form of terms to compute siblings in the cardinality graph. This is problematic for
(set.minus set.universe t) whose sibling was computed to be rewrite( (set.inter set.universe t) ) = t.

To avoid the issue, we now purify the argument of set.minus to avoid this behavior.

Fixes #5400.
Fixes the first benchmark on #5402.

This also eliminates a spurious lemma schema for set universe that was leftover from handling set subtyping.

2 years agoEliminate CDHashMap::insertAtContextLevelZero (#8173)
Andrew Reynolds [Wed, 2 Mar 2022 21:11:05 +0000 (15:11 -0600)]
Eliminate CDHashMap::insertAtContextLevelZero (#8173)

This method unnecessarily complicates the usage of CDHashMap. It had one usage in the current code, for dealing with global declarations. However, this was an entirely artificial use case, as one should properly manage scopes when this option is true (i.e. global-declarations simply disables user-level scoping in the symbol table).

It also simplifies the symbol table so that it doesn't automatically push a global outermost scope. Instead, this scope is pushed when the logic is declared, so that background symbols are correctly added at level 0.

Fixes #4767.

2 years agoFix incorrect assertion in prop engine proofs (#8204)
Andrew Reynolds [Wed, 2 Mar 2022 20:36:36 +0000 (14:36 -0600)]
Fix incorrect assertion in prop engine proofs (#8204)

Leftover from when unsat cores mode was tied to proof mode.

Fixes cvc5/cvc5-projects#462.

2 years agoClean usage of options in regressions (#8190)
Andrew Reynolds [Wed, 2 Mar 2022 18:59:56 +0000 (12:59 -0600)]
Clean usage of options in regressions (#8190)

We now support tester annotations, thus it is best practice not to use check-unsat-cores or check-models explicitly in the regressions.

This changes regressions to not use these options, where these options are either:

removed entirely (the benchmark was fixed in the meantime)
changed to -q (the benchmark succeeds with a warning)
changed to produce- instead of check- if the option on the benchmark is required to ensure a configuration of models/unsat-cores is run. This is done for unsat-cores on sat benchmarks and models on unsat benchmarks.
replaced by DISABLE-TESTER: model.
one spurious regression is deleted, which was identical to another + check-models.
It also makes some fixes to enable more benchmarks succeed with check-models, and adds a warning when fmf-fun is combined with check-model.

2 years agoImprove error message when not using strings-exp (#8203)
Andrew Reynolds [Wed, 2 Mar 2022 18:16:20 +0000 (12:16 -0600)]
Improve error message when not using strings-exp (#8203)

Fixes #6005.

Also improves smt2 printing of sequences so that we print the compliant kinds, which is work towards cvc5/cvc5-wishues#106.

2 years agoMove libpoly <-> CoCoA conversion to new utility (#8199)
Gereon Kremer [Wed, 2 Mar 2022 17:21:32 +0000 (18:21 +0100)]
Move libpoly <-> CoCoA conversion to new utility (#8199)

This PR factors the conversion between libpoly and CoCoA out of the LazardEvaluation class into a new utility. The goal is to make it reusable for other applications of CoCoA within cvc5, for example to replace the (rather naive) equality substitution utility by a new simplification technique based on CoCoAs Gröbner bases. This PR merely moves code around and should not actually change anything.

2 years agoRefactor rewriting of arithmetic division (#8195)
Gereon Kremer [Wed, 2 Mar 2022 16:37:03 +0000 (17:37 +0100)]
Refactor rewriting of arithmetic division (#8195)

This PR does minor refactoring of how we rewrite division. Also, it moves some functions around to reconcile the order in header and source file.

2 years agoAdd utility to access how to print floating point (#8141)
Andrew Reynolds [Wed, 2 Mar 2022 15:48:54 +0000 (09:48 -0600)]
Add utility to access how to print floating point (#8141)

This makes the code for printing a floating point based on its BV components accessible as a utility.

This is required for proper printing of FP constants in LFSC.

2 years agoMake blockModelValues robust to non-closed enumerable types (#8055)
Andrew Reynolds [Wed, 2 Mar 2022 05:12:08 +0000 (23:12 -0600)]
Make blockModelValues robust to non-closed enumerable types (#8055)

Fixes cvc5/cvc5-projects#420.

Also fixes the trivial case where there is nothing to block, in which case we should add false (via mkOr) not true.

2 years agoAdd regressions for fixed issues (#8202)
Andrew Reynolds [Wed, 2 Mar 2022 02:38:21 +0000 (20:38 -0600)]
Add regressions for fixed issues (#8202)

Fixes #4463.
Fixes cvc5/cvc5-projects#403.

2 years agoPrune spurious roots in lazard evaluation of coverings solver (#8200)
Gereon Kremer [Wed, 2 Mar 2022 01:27:02 +0000 (02:27 +0100)]
Prune spurious roots in lazard evaluation of coverings solver (#8200)

This PR fixes a subtle issue in the Lazard evaluation used in the coverings solver if --nl-cov-lift=lazard is used.
When isolating real roots (over a partial assignment that contains real algebraic number), the core root solver may find roots that are spurious, i.e., they are not actually roots of the input polynomial. This is due to the way how the multivariate polynomial is "partially evaluated" before calling the univariate real root isolation.
When using the libpoly real root isolation, this is all done internally. For the Lazard evaluation, however, we explicitly call the libpoly real root isolation on a univariate polynomial that already has these spurious roots, hence we need to remove them ourselves.

While debugging this issue, another weird oversight was detected (and fixed): for some reason we expected the vanishing factor (after factoring the defining polynomial when constructing the next field extension) to only have two term. There is no reason for this restriction, and the code below works just fine.

2 years agoAdd standard theories to documentation (#8192)
Gereon Kremer [Wed, 2 Mar 2022 00:44:03 +0000 (01:44 +0100)]
Add standard theories to documentation (#8192)

This PR adds the standardized theories to our theories overview.

2 years agoFix issue involving dropped purification lemmas for transcendental functions (#8198)
Andrew Reynolds [Tue, 1 Mar 2022 21:14:16 +0000 (15:14 -0600)]
Fix issue involving dropped purification lemmas for transcendental functions (#8198)

Fixes #4693.
Fixes #8181 (which now times out).

The issue was caused by purification lemmas being dropped, often in incremental mode. This meant that we were replacing sin(t) by sin(k) when checking models, but not having any information about sin(k).

We now are more robust and send the purification lemmas for transcendental functions based on checking whether it is necessary to do so.

2 years agoDo not use sygus evaluation functions in sygus-inst (#8185)
Andrew Reynolds [Tue, 1 Mar 2022 20:46:56 +0000 (14:46 -0600)]
Do not use sygus evaluation functions in sygus-inst (#8185)

This simplification was realized while we were writing the paper.

This should avoid spurious check-model failures when using sygus-inst.

2 years agoDisable regression (#8191)
Andrew Reynolds [Tue, 1 Mar 2022 17:01:50 +0000 (11:01 -0600)]
Disable regression (#8191)

Benchmark is "unknown" on some builds. We don't have a strong reason why we will always say "sat" for this benchmark.

Fixes one of the issues in the nightlies.

2 years ago[BV] Fix rewriter policy for `bvneg` (#8196)
Andres Noetzli [Tue, 1 Mar 2022 09:07:56 +0000 (01:07 -0800)]
[BV] Fix rewriter policy for `bvneg` (#8196)

Our rewriter was returning `REWRITE_DONE` prematurely for `bvneg`. This
commit makes the status returned more conservative.

2 years agoFix lambda lifting + proofs (#8152)
Andrew Reynolds [Tue, 1 Mar 2022 06:02:51 +0000 (00:02 -0600)]
Fix lambda lifting + proofs (#8152)

Was leading to eager proof checking failures on proof-new.

2 years agoRemove unused data members from `TheoryArrays` (#8197)
Andres Noetzli [Tue, 1 Mar 2022 02:19:02 +0000 (18:19 -0800)]
Remove unused data members from `TheoryArrays` (#8197)

2 years agoRename cad to coverings (#8187)
Gereon Kremer [Tue, 1 Mar 2022 00:37:13 +0000 (01:37 +0100)]
Rename cad to coverings (#8187)

The nonlinear subsolver that implements cylindrical algebraic coverings is still called cad in many places, which really was a misnomer from the beginning. This PR renames it everywhere.

2 years ago[Seq/Model] Do not enumerate elements of constants (#8179)
Andres Noetzli [Mon, 28 Feb 2022 23:56:38 +0000 (15:56 -0800)]
[Seq/Model] Do not enumerate elements of constants (#8179)

Fixes #8133. In the input from the issue, the string solver was
assigning a skeleton `(seq.unit smvX)` to a constant of sort `(Seq (Seq
Int))`. This constant was asserted to be different from `(seq.unit (as
seq.empty (Seq Int)))`. However, the `TheoryModelBuilder` was assigning
`smvX` the value `(as seq.empty (Seq Int))`, because `(as seq.empty (Seq
Int))` was not being registered with the equality engine. This is
because elements of constant sequences are not considered children, but
are a data member of the `Sequence` class. The commit updates
`TheoryStrings::collectModelInfoType()` to also register elements of
sequence constants with the equality engine.

2 years agoRefactor rewriting of arithmetic atoms (#8175)
Gereon Kremer [Mon, 28 Feb 2022 23:15:27 +0000 (00:15 +0100)]
Refactor rewriting of arithmetic atoms (#8175)

This PR uses the new utilities for atom rewriting in the arithmetic rewriter.

2 years agoFix special casing for PI in model value (#8189)
Andrew Reynolds [Mon, 28 Feb 2022 22:37:08 +0000 (16:37 -0600)]
Fix special casing for PI in model value (#8189)

PI should be considered a model value but not a "base" model value. This avoid spurious debug assertion failures, which are now treated as warnings. This makes a difference when another theory e.g. UF says that PI is currently equal to a constant value c. Since our lemma schemas are model-based, we may require building a spurious model where PI is c, and refine afterwards.

This also fixes a bug in our extended function rewriting which would mistakenly think that PI was reduced, and hence skip a full effort check if PI was the only extended function in the current context. This was previously causing a final model to be one where PI = 0.0.

Fixes #8183.

2 years agoPreserve model values for exact sine points (#8188)
Andrew Reynolds [Mon, 28 Feb 2022 22:04:16 +0000 (16:04 -0600)]
Preserve model values for exact sine points (#8188)

Fixes #8182.

2 years agoTrack names for witness terms in model (#8184)
Andrew Reynolds [Mon, 28 Feb 2022 21:03:30 +0000 (15:03 -0600)]
Track names for witness terms in model (#8184)

This ensures that enough information is set to allow users to understand models with witness terms.

For example, for input:

(set-logic ALL)
(set-info :status sat)
(declare-fun x () String)
(declare-fun y () String)
(declare-fun z () String)
(assert (= (str.len x) 999999999999999999999999))
(assert (= (str.len y) 999999999999999999999999))
(assert (= z (str.++ x y)))
(check-sat)
we now get:

sat
(
(define-fun x () String (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w1) ))
(define-fun y () String (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w0) ))
(define-fun z () String (str.++ (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w1) ) (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w0) )))
)

2 years agoAdd two reduction schemas for sin terms (#8171)
Andrew Reynolds [Mon, 28 Feb 2022 20:01:30 +0000 (14:01 -0600)]
Add two reduction schemas for sin terms (#8171)

This restores our reasoning for symmetry of sine, now on-demand and without introducing sin terms eagerly.

It also ensures that sin terms whose arguments fall exactly on boundary points are removed from consideration from the transcendental solver. This allows us to answer sat for inputs involving sin(k) when k = pi/2.

It also cleans the relationship of sine solver and transcendental state, and makes a small fix to the monotonicity of sin schema.

2 years agoRemove broken/unused `--mmap` option (#8178)
Andres Noetzli [Mon, 28 Feb 2022 19:21:16 +0000 (11:21 -0800)]
Remove broken/unused `--mmap` option (#8178)

Fixes #2705. This commit removes the broken and unused --mmap option.
Given that we are planning to change to a different parser at some
point, it is not worth attempting to fix the option.

2 years agoAdd scripts to build python wheels (#8132)
Gereon Kremer [Mon, 28 Feb 2022 18:47:28 +0000 (19:47 +0100)]
Add scripts to build python wheels (#8132)

This adds a new set of scripts to build python wheels for cvc5. It includes

mk_wheel.py which builds the python wheel within an existing build folder
mk_build_dir.py which runs configure.sh and directs cmake to a custom python interpreter
mk_clean_wheel.sh which builds the python wheel in a clean environment (a python venv and a fresh build folder)
a dockerfile that slightly customizes manylinux2014 to our use case
a readme giving a highlevel overview of what we are doing

2 years agoRefactor rewriting of arithmetic leafs (#8177)
Gereon Kremer [Mon, 28 Feb 2022 15:45:56 +0000 (16:45 +0100)]
Refactor rewriting of arithmetic leafs (#8177)

Minor refactoring of how we rewrite arithmetic leaf nodes (constants, algebraic numbers and "variables").

2 years agoRefactor rewriting of arithmetic addition (#8180)
Gereon Kremer [Mon, 28 Feb 2022 15:22:48 +0000 (16:22 +0100)]
Refactor rewriting of arithmetic addition (#8180)

This PR uses the new addition utilities to refactor rewriting of arithmetic addition. This properly handles real algebraic numbers now, eliminating a few more edge cases where the previous solution might allow for non-idempotent rewrites.

2 years agoConsider PI to be a model value (#8176)
Andrew Reynolds [Fri, 25 Feb 2022 22:48:12 +0000 (16:48 -0600)]
Consider PI to be a model value (#8176)

Fixes cvc5/cvc5-projects#460.

The special case is necessary due to the node representation of nullary operators, which uses variables internally to represent operators. The other nullary operators are not model values.

2 years agoSyntax fixes for LFSC signature (#8172)
Andrew Reynolds [Fri, 25 Feb 2022 22:01:01 +0000 (16:01 -0600)]
Syntax fixes for LFSC signature (#8172)

2 years agoAdd utilities to rewrite atoms for the arithmetic rewriter (#8014)
Gereon Kremer [Fri, 25 Feb 2022 21:22:36 +0000 (22:22 +0100)]
Add utilities to rewrite atoms for the arithmetic rewriter (#8014)

This PR adds utilities to rewrite atoms in the arithmetic rewriter. They retain compatibility with the current normal_form utility, but make the process more transparent so that changing the normal form in the future should be simpler.

2 years agoRefactor rewriting of arithmetic negation and subtraction (#8170)
Gereon Kremer [Fri, 25 Feb 2022 20:56:21 +0000 (21:56 +0100)]
Refactor rewriting of arithmetic negation and subtraction (#8170)

Slightly refactor negation and subtraction, get rid of utility functions.

2 years agoSlightly refactor arithmetic rewriting for extended operators (#8169)
Gereon Kremer [Fri, 25 Feb 2022 20:17:34 +0000 (21:17 +0100)]
Slightly refactor arithmetic rewriting for extended operators (#8169)

This PR mostly reorders the implementation to match the order in the header, and does a few very minor refactorings for the rewriters for transcendental functions, and the pow2 and iand operators.

2 years agoFix non-termination in quantifiers rewriter (#8165)
Andrew Reynolds [Fri, 25 Feb 2022 19:59:27 +0000 (13:59 -0600)]
Fix non-termination in quantifiers rewriter (#8165)

Caused by 2 rewrite steps (conditional splitting and extended rewriting) being inverses of each other when miniscoping is disabled.

Fixes the third benchmark on #8159.

2 years agoSimplify and fix how purified terms are managed in the trancendental solver (#8167)
Andrew Reynolds [Fri, 25 Feb 2022 18:45:43 +0000 (12:45 -0600)]
Simplify and fix how purified terms are managed in the trancendental solver (#8167)

Simplification is leftover from the sine symmetry heuristic, now the mapping from terms to what purifies them is injective.
Also makes the mapping context-dependent.

It also ensures that we keep model values for purification arguments. Fixes #8160.

2 years agoFix dropped bounds on PI (#8164)
Andrew Reynolds [Fri, 25 Feb 2022 17:15:00 +0000 (11:15 -0600)]
Fix dropped bounds on PI (#8164)

Fixes #8162.

In this example, we were failing to send the initial PI bound lemma, likely due to a conflict while this lemma was buffered.

This makes the PI refinement utility more robust by explicitly checking based on the model whether we need to refine PI.

2 years agoRemove approximations infrastructure from model (#8166)
Andrew Reynolds [Fri, 25 Feb 2022 16:45:41 +0000 (10:45 -0600)]
Remove approximations infrastructure from model (#8166)

We now allow partial specifications. Recording approximations is arithmetic specific, and if necessary could be added as a post-processing analysis e.g. during check-model.

2 years agoRemove spurious assertion involving constants for arguments to UF from FMF (#8168)
Andrew Reynolds [Fri, 25 Feb 2022 16:27:16 +0000 (10:27 -0600)]
Remove spurious assertion involving constants for arguments to UF from FMF (#8168)

Fixes #8163.

2 years agoMake quantifiers terminate if it detects a (duplicate) quantifier-free conflict ...
Andrew Reynolds [Fri, 25 Feb 2022 07:13:43 +0000 (01:13 -0600)]
Make quantifiers terminate if it detects a (duplicate) quantifier-free conflict (#8157)

Fixes #6859.

The benchmark is now unknown.

2 years agoAdd regression for fixed transcendental regression (#8155)
Andrew Reynolds [Fri, 25 Feb 2022 06:27:29 +0000 (00:27 -0600)]
Add regression for fixed transcendental regression (#8155)

Fixes #7938.

2 years agoConsolidate extended rewrite preprocessing modes (#8156)
Andrew Reynolds [Fri, 25 Feb 2022 06:05:41 +0000 (00:05 -0600)]
Consolidate extended rewrite preprocessing modes (#8156)