cvc5.git
2 years agoThrow logic exception for set.map (#8403)
Andrew Reynolds [Sat, 26 Mar 2022 02:51:29 +0000 (21:51 -0500)]
Throw logic exception for set.map (#8403)

Support parsing/rewriting, but not solving currently.

2 years agoMore minor cleaning of options (#8401)
Andrew Reynolds [Sat, 26 Mar 2022 01:53:51 +0000 (20:53 -0500)]
More minor cleaning of options (#8401)

Removes a few more unnecessary options and moves the location of one.

2 years agoFixes for API kind documentation (#8397)
Andrew Reynolds [Sat, 26 Mar 2022 01:07:05 +0000 (20:07 -0500)]
Fixes for API kind documentation (#8397)

Also renames str.tolower -> str.to_lower, str.toupper -> str.to_upper.

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
2 years agoAdd API unit tests for options (#8339)
Gereon Kremer [Sat, 26 Mar 2022 00:42:26 +0000 (01:42 +0100)]
Add API unit tests for options (#8339)

This PR adds some unit tests that cover some remaining cases of getOptionInfo() and getDriverOptions().
It also adds some fixes to the java bindings of these methods.

2 years agoapi: Unify mkOp variants. (#8369)
Mathias Preiner [Fri, 25 Mar 2022 23:57:10 +0000 (16:57 -0700)]
api: Unify mkOp variants. (#8369)

Co-authored-by: Gereon Kremer <nafur42@gmail.com>
2 years agoapi: More comprehensive documentation of INTERNAL_KIND. (#8400)
Aina Niemetz [Fri, 25 Mar 2022 23:33:17 +0000 (16:33 -0700)]
api: More comprehensive documentation of INTERNAL_KIND. (#8400)

2 years ago[Parser] Fix resolution of indexed symbols (#8383)
Andres Noetzli [Fri, 25 Mar 2022 23:09:13 +0000 (16:09 -0700)]
[Parser] Fix resolution of indexed symbols (#8383)

Fixes #8377. Commit 3a97480ffab492f8272ad9c7c192d04b43eeea60 changed how
we handle indexed symbols. In particular, it added the option to resolve
them later when the arguments are known. However, the condition for when
to do this resolution was incorrect: It was applied to _all_ known
indexed symbols and not only the ones that can't immediately be resolved
to a kind. This commit fixes the condition.

2 years agoapi: Remove Sort::isParametricDatatype(). (#8405)
Aina Niemetz [Fri, 25 Mar 2022 22:43:35 +0000 (15:43 -0700)]
api: Remove Sort::isParametricDatatype(). (#8405)

Previously, Sort::isParametricDatatype() returned true for both
instantiated and non-instantiated parametric datatypes.

This deletes the method, instead one can check getDatatype().isParametric(). Parametric datatypes will be distinguished from instantiated parametric datatypes via a forthcoming method Sort::isInstantiated.

Co-authored-by: ajreynol <andrew.j.reynolds@gmail.com>
2 years ago[proofs] [sat] Have SAT solver communicate whether it has optimized the assertion...
Haniel Barbosa [Fri, 25 Mar 2022 21:25:04 +0000 (18:25 -0300)]
[proofs] [sat] Have SAT solver communicate whether it has optimized the assertion level of a clause (#8399)

This way both the SAT proof manager and the Proof Cnf Stream can properly track
proofs for clauses added at assertion levels below their original user level.

This commit, besides some minor tweaks, adds the hooks in the places where
a clause can be created with an optimized level and we need to track:

when the explanation of a propagation is requested
when a clause/lemma is added
when a lemma is added (from the backlog of lemmas added when Minisat was busy)
For clauses derived via resolution, this information is computed directly in the SAT proof manager.

This commit also reverts a change from #7790 where whether to optimize clauses was computed only once for the SAT solver. This cannot be the case because between different check-sat calls the state can change.

Finally, this commit enables proofs for several regressions that were previously incompatible with proofs. Since now proofs are compatible with optimizing the level of clauses during incremental solving, this commit should lead to performance improvements.

Fixes cvc5/cvc5-projects#314

2 years agoapi: Rename kind NULL_EXPR to NULL_TERM. (#8402)
Aina Niemetz [Fri, 25 Mar 2022 20:50:34 +0000 (13:50 -0700)]
api: Rename kind NULL_EXPR to NULL_TERM. (#8402)

2 years agoGenerate `enum` bindings for Python and Java (#8393)
Andres Noetzli [Fri, 25 Mar 2022 20:28:12 +0000 (13:28 -0700)]
Generate `enum` bindings for Python and Java (#8393)

This commit generalizes the generation of bindings for enums to include
enums in cvc5_types.h. The commit only generates the bindings, but
does not use them yet (e.g., do add an argument to
Solver::blockModels()). The generated Java bindings already respect
the C++ namespace whereas the Python bindings require a minor
restructuring to make the namespaces work (i.e., instead of cvc5kinds,
we should have cvc5.api.kinds).

2 years agoUpdate checkSynth and checkSynthNext to return SynthResult (#8382)
Andrew Reynolds [Fri, 25 Mar 2022 20:00:14 +0000 (15:00 -0500)]
Update checkSynth and checkSynthNext to return SynthResult (#8382)

Also extends to non-trivial unit test of SynthResult.

Note this also changes the expected output when using --sygus-out=status from unsat/sat/unknown to feasible/infeasible/fail (the option is used mostly just for our regressions). The output mode status-or-def is now equivalent to standard and is hence deleted.

2 years agoChange output of abduction/interpolation for failed inputs (#8396)
Andrew Reynolds [Fri, 25 Mar 2022 19:19:35 +0000 (14:19 -0500)]
Change output of abduction/interpolation for failed inputs (#8396)

Changes from "none" to "fail" to be consistent with SyGuS standard. Note that this means that we don't know if an abduct/interpolant exists.

2 years ago[proofs] Alethe: Bug Fix in Cong Rule (#8391)
Lachnitt [Fri, 25 Mar 2022 18:59:26 +0000 (11:59 -0700)]
[proofs] Alethe: Bug Fix in Cong Rule (#8391)

cvc5 suffered a segfault in the CONG rule because the refl step, e.g. (= v0 v0), was added without the cl connector, e.g. (cl (= v0 v0))

2 years agoapi: Remove blocks in kinds header. (#8398)
Aina Niemetz [Fri, 25 Mar 2022 18:00:27 +0000 (11:00 -0700)]
api: Remove  blocks in kinds header. (#8398)

2 years ago[proofs] [cnf] Utilities to notify and track proofs of optimized SAT clauses in the...
Haniel Barbosa [Fri, 25 Mar 2022 17:41:56 +0000 (14:41 -0300)]
[proofs] [cnf] Utilities to notify and track proofs of optimized SAT clauses in the ProofCnfStream (#8388)

Adds functionality for the TheoryProxy and ProofCnfStream modules to be notified of clauses that were asserted in lower levels than the current one. These clauses have their proofs tracked in the ProofCnfStream via an OptimizedClausesManager object.

Since the SAT solver may optimize the assertion level of propagation
explanations and of added clauses, we need to be able to maintain proofs across
context-popping. Not doing this can lead to open proofs. To do this the Proof
cnf stream uses an OptClausesManager to re-add proofs of facts inserted at
optimized levels.

Future PRs will change the SAT solver to use these notifications.

2 years agoFixes related to set defaults for sygus/proofs (#8395)
Andrew Reynolds [Fri, 25 Mar 2022 17:02:23 +0000 (12:02 -0500)]
Fixes related to set defaults for sygus/proofs (#8395)

This ensures we always report that SyGuS is incompatible with proofs. As a result, we require disabling sygus in 2 contexts where it should have been disabled before.

2 years agoFix Python API tests (#8392)
Andres Noetzli [Fri, 25 Mar 2022 13:08:01 +0000 (06:08 -0700)]
Fix Python API tests (#8392)

Note that we are currently not running API tests on the CI due to the
changes in 23dd064.

2 years agoapi: Refactor kinds documentation. (#8384)
Aina Niemetz [Fri, 25 Mar 2022 03:13:06 +0000 (20:13 -0700)]
api: Refactor kinds documentation. (#8384)

2 years agoProperly guard commands in the SyGuS API (#8390)
Andrew Reynolds [Fri, 25 Mar 2022 02:21:44 +0000 (21:21 -0500)]
Properly guard commands in the SyGuS API (#8390)

This commit ensures we don't segfault in the SyGuS API (for non-text inputs) if the option sygus is not set to true. It also renames mkSygusVar to declareSygusVar for consistency with the sygus input format.

For SyGuS API inputs, we now use the option sygus to true instead of setting the language to sygus2.

This furthermore changes a few details in set-defaults regarding the relationship between the language, the sygus option, and when to apply default options for sygus.

It also adds a unit test for checkSynth.

2 years agoRecategorize options (#8386)
Andrew Reynolds [Fri, 25 Mar 2022 01:56:48 +0000 (20:56 -0500)]
Recategorize options (#8386)

2 years agoFixes for theory reference for datatypes (#8380)
Andrew Reynolds [Fri, 25 Mar 2022 01:11:25 +0000 (20:11 -0500)]
Fixes for theory reference for datatypes (#8380)

2 years agoDocument proof rules for coverings solver (#8376)
Gereon Kremer [Thu, 24 Mar 2022 23:28:07 +0000 (00:28 +0100)]
Document proof rules for coverings solver (#8376)

This PR converts the documentation for the proof rules for the coverings solver.

2 years agoMinor updates for quantifiers options (#8385)
Andrew Reynolds [Thu, 24 Mar 2022 21:02:48 +0000 (16:02 -0500)]
Minor updates for quantifiers options (#8385)

2 years ago[proofs] [sat] Handle resolution proofs for optimized clauses in incremental (#8389)
Haniel Barbosa [Thu, 24 Mar 2022 20:14:12 +0000 (17:14 -0300)]
[proofs] [sat] Handle resolution proofs for optimized clauses in incremental (#8389)

The SAT solver may associate, to the result of a resolution, a lower assertion
level than the current one. To be able to produce proofs to such clauses, we
extend the SAT proof manager to track which resolution results were
optimized. Then, when the SAT solver pops, the manager is notified and stores
the proofs for these optimized clauses, so that they can be reinserted when the
user context is popped. The latter is handled by the SAT proof manager's
OptClauseManager attribute.

2 years agoDocument arithmetic proof rules (#8373)
Gereon Kremer [Thu, 24 Mar 2022 19:14:40 +0000 (20:14 +0100)]
Document arithmetic proof rules (#8373)

This PR converts the documentation for the arithmetic proof rules, excluding those for transcendentals and coverings.

2 years agoStandardize more instances of skolems (#8351)
Andrew Reynolds [Thu, 24 Mar 2022 18:14:59 +0000 (13:14 -0500)]
Standardize more instances of skolems (#8351)

This is work towards limiting our usage of witness terms for skolems.

It standardizes witnessing of disequalities for sets, bags, and arrays in the appropriate way that uses mkSkolemFunction(...) instead of mkSkolem(...).

2 years ago[sat] Add option to disable Minisat simplifications (#7992)
Haniel Barbosa [Thu, 24 Mar 2022 17:34:59 +0000 (14:34 -0300)]
[sat] Add option to disable Minisat simplifications (#7992)

Useful to better control behavior, specially in terms of how the solver performs
when these simplifications (mainly variable and clause elimination) are
disabled, e.g. with incremental and/or proofs.

Also renames the previously confusing "--minisat--elimination" option, which
only refers to variable elimination, a subset of the Minisat simplifications.

Moreover deletes an old comment which no longer applies.

2 years agoFix a couple of parse error messages for sygus (#8381)
Andrew Reynolds [Thu, 24 Mar 2022 16:57:53 +0000 (11:57 -0500)]
Fix a couple of parse error messages for sygus (#8381)

2 years ago[unsat-cores] [sat-proof] Fix open proofs due to theory lemmas (#8371)
Haniel Barbosa [Thu, 24 Mar 2022 15:32:42 +0000 (12:32 -0300)]
[unsat-cores] [sat-proof] Fix open proofs due to theory lemmas (#8371)

Previously when producing sat proofs for unsat cores (no theory proofs) theory lemmas were becoming open leafs in the final proof, breaking the invariant that only inputs should be so. This commit guards against this by justifying these lemmas with a THEORY_LEMMA step.

Fixes cvc5/cvc5-projects#468

2 years agoClean options (#8309)
Andrew Reynolds [Wed, 23 Mar 2022 23:53:14 +0000 (18:53 -0500)]
Clean options (#8309)

Deletes many unnecessary options, cleans some documentation, consolidates several options.

2 years agoAdd API unit tests for statistics (#8341)
Gereon Kremer [Wed, 23 Mar 2022 22:59:23 +0000 (23:59 +0100)]
Add API unit tests for statistics (#8341)

This PR adds some unit tests that cover getStatistics() and the api::Stat class.

2 years agoAdd SynthResult to the API (#8370)
Andrew Reynolds [Wed, 23 Mar 2022 21:56:33 +0000 (16:56 -0500)]
Add SynthResult to the API (#8370)

Does not modify the code to return a SynthResult yet, just adds the class.

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
2 years agoAdd `getOptionInfo()` and `getOptionNames()` to python API (#8342)
Gereon Kremer [Wed, 23 Mar 2022 19:53:18 +0000 (20:53 +0100)]
Add `getOptionInfo()` and `getOptionNames()` to python API (#8342)

These extended options operations were still missing from the python API and are added with this PR. To simplify the integration (and also provide a reasonably pythonic interface) we return a dictionary from getOptionInfo() instead of exposing a std::variant-like interface.
The PR also includes the corresponding unit tests.

2 years agoDocument proof rules for transcendentals (#8375)
Gereon Kremer [Wed, 23 Mar 2022 19:17:29 +0000 (20:17 +0100)]
Document proof rules for transcendentals (#8375)

This PR converts the documentation for the proof rules for the transcendental reasoning in the arithmetic solver.

2 years agoMake IDOF_MAX rewrite only apply when all children are constant (#8363)
Andrew Reynolds [Wed, 23 Mar 2022 18:48:28 +0000 (13:48 -0500)]
Make IDOF_MAX rewrite only apply when all children are constant (#8363)

Fixes #8346.

2 years agoOnly update latest tag if commit changed. (#8379)
Mathias Preiner [Wed, 23 Mar 2022 18:26:15 +0000 (11:26 -0700)]
Only update latest tag if commit changed. (#8379)

Previously the latest tag was always updated when a new binary was added to a release (i.e. 3 updates per commit). This commit ensures that we only update the tag if the commit sha changed.

2 years agoAdd internal synth result class (#8352)
Andrew Reynolds [Wed, 23 Mar 2022 14:13:47 +0000 (09:13 -0500)]
Add internal synth result class (#8352)

This is in preparation for refactoring the return values of several API methods.

2 years agoRun gen-versioninfo unconditionally (#8368)
Gereon Kremer [Wed, 23 Mar 2022 08:27:33 +0000 (09:27 +0100)]
Run gen-versioninfo unconditionally (#8368)

This fixes an issue where the output of `--show-config` would not be updated properly in certain cases (e.g., when files were modified but cmake is not run). We now run the `gen-versioninfo` target unconditionally, always updating the `versioninfo.cpp` where the version data for `--show-config` is stored.

2 years agoStore latest builds in a special release (#8337)
Gereon Kremer [Wed, 23 Mar 2022 04:11:04 +0000 (05:11 +0100)]
Store latest builds in a special release (#8337)

This PR refactors our current github ci action that takes care of storing binaries for releases. It now stores binaries both in the current release (if we are in a release build) or attaches them to a special latest tag. For any regular build on the master branch, it moves the latest tag to the current commit, weeds out the current assets attached to that latest release and adds the current binary. This makes sure we always have the equivalent of our current nightly builds in one place.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
2 years agoRemove dependency on build (#8367)
Gereon Kremer [Wed, 23 Mar 2022 03:47:33 +0000 (04:47 +0100)]
Remove dependency on build (#8367)

We automatically update PRs that can be merged automatically in the CI on master. This PR makes it so that this update is done immediately, not only after the CI has run successfully for master.
As we only merge to master if CI works, CI failures on master should only be glitches or issues with the CI itself.
This allows to merge stuff to master twice as fast when using the auto-merge feature.

2 years agoupdate SET_COMPREHENSION documentation (#8372)
mudathirmahgoub [Wed, 23 Mar 2022 02:53:38 +0000 (21:53 -0500)]
update SET_COMPREHENSION documentation (#8372)

2 years agoInitial documentation on LFSC (#8365)
Andrew Reynolds [Wed, 23 Mar 2022 02:12:34 +0000 (21:12 -0500)]
Initial documentation on LFSC (#8365)

2 years agoFix cvc5-projects issue 497 (#8331)
mudathirmahgoub [Wed, 23 Mar 2022 01:11:06 +0000 (20:11 -0500)]
Fix cvc5-projects issue 497 (#8331)

Fixes cvc5/cvc5-projects#497

2 years agoFix non-termination issue in sygus enumerator (#8340)
Andrew Reynolds [Wed, 23 Mar 2022 00:05:38 +0000 (19:05 -0500)]
Fix non-termination issue in sygus enumerator (#8340)

This ensures that the sygus enumerator does not get stuck in rare cases.

In particular this is important when doing PBE and one of the enumerators (among return/condition enumeration) is out of values. This ensures we break when we fail to increment an enumerator for a type that is required to validate a child enumerator.

2 years agoChange null terminator for regular expression intersection (#8362)
Andrew Reynolds [Tue, 22 Mar 2022 23:36:37 +0000 (18:36 -0500)]
Change null terminator for regular expression intersection (#8362)

2 years agoRefactor proof rule documentation (#8303)
Gereon Kremer [Tue, 22 Mar 2022 22:26:56 +0000 (23:26 +0100)]
Refactor proof rule documentation (#8303)

This PR starts to refactor the proof rule comments so that they generate proper sphinx documentation.
It sets up doxygen to include the proof_rule.h, includes some useful configuration for mathjax and provides proper documentation for all core rules and Boolean rules.

2 years agoUpdates for the theory reference for separation logic (#8366)
Andrew Reynolds [Tue, 22 Mar 2022 21:24:52 +0000 (16:24 -0500)]
Updates for the theory reference for separation logic (#8366)

2 years agoMake uncovered-api-functions.py exit with 1 if something is not covered (#8360)
Gereon Kremer [Tue, 22 Mar 2022 20:33:11 +0000 (21:33 +0100)]
Make uncovered-api-functions.py exit with 1 if something is not covered (#8360)

This simplifies the integration of this script in CI or buildbot jobs. The idea is to automatically check that the whole API is covered by unit tests, and that the language bindings do the same.

2 years ago[proofs] Alethe: fixing formatting and adding missing comment (#7779)
Haniel Barbosa [Tue, 22 Mar 2022 19:53:42 +0000 (16:53 -0300)]
[proofs] Alethe: fixing formatting and adding missing comment (#7779)

2 years agoupdate sets-and-relations.rst (#8364)
mudathirmahgoub [Tue, 22 Mar 2022 19:14:59 +0000 (14:14 -0500)]
update sets-and-relations.rst (#8364)

2 years agoAdd a timeout option for verification of synthesized terms. (#8359)
Abdalrhman Mohamed [Tue, 22 Mar 2022 17:01:13 +0000 (12:01 -0500)]
Add a timeout option for verification of synthesized terms. (#8359)

This PR adds an option to timeout on the verification check for the terms enumerated by the Sygus solver.

2 years ago[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334)
Andres Noetzli [Tue, 22 Mar 2022 08:36:54 +0000 (01:36 -0700)]
[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind  (#8334)

This commit removes the `FLOATINGPOINT_TO_FP_GENERIC` kind, which was
only used in the parser and immediately rewritten by the floating-point
arithmetic solver. It extends the `ParseOp` class to handle indexed
operators of which we do not know the kind (`to_fp` in this case) by
storing the name and the indices. The name is then resolved later when
we have parsed the arguments.

2 years agoFixes for witness terms appearing in CEGQI instantiations (#8350)
Andrew Reynolds [Tue, 22 Mar 2022 07:43:30 +0000 (02:43 -0500)]
Fixes for witness terms appearing in CEGQI instantiations (#8350)

Fixes #8344.

We now have cases where witness terms e.g. `(witness x : String. len(x) = N)` appear in model values.  These terms require special care in CEGQI.

There are 2 fixes in this PR:
(1) we update our policy on what a legal term is,
(2) we erase annotations from witness terms appearing in instantiations, which is required for ensuring that proofs are consistent.  Otherwise, the skolemization lemma for a witness term does not introduce the same skolem.

2 years agoRefactor result class (#8313)
Andrew Reynolds [Tue, 22 Mar 2022 01:27:20 +0000 (20:27 -0500)]
Refactor result class (#8313)

This significantly refactors the internal result class. Entailments and "which" field are deleted, "Sat" is renamed to "Status". Moreover "TYPE_NONE" is made into a status.

Simplifies the usage of this class throughout the code.

It also changes the API Result method isSatUnknown to isUnknown.

2 years agoapi: Unify mkTerm variants. (#8357)
Mathias Preiner [Tue, 22 Mar 2022 00:22:41 +0000 (17:22 -0700)]
api: Unify mkTerm variants. (#8357)

2 years ago[API] Support `Op::operator[]` in Java and Python (#8356)
Andres Noetzli [Tue, 22 Mar 2022 00:00:58 +0000 (17:00 -0700)]
[API] Support `Op::operator[]` in Java and Python (#8356)

This commit adds support for `Op::operator[]` in Java and Python and
updates all unit tests to be consistent.

2 years agoRemove `Op::getIndices()` (#8355)
Andres Noetzli [Mon, 21 Mar 2022 23:27:40 +0000 (16:27 -0700)]
Remove `Op::getIndices()` (#8355)

This commit removes `Op::getIndices()`. As discussed offline, the
semantics of that method were confusing and the use cases are covered by
`Op::getNumIndices()` and `Op::operator[]()` (which mirror
`Term::getNumChildren()` and `Term::operator[]()`).

Future changes are going to update the Python and Java bindings to
support `Op::operator[]()`.

2 years agoFix return value for candidate rewrite database (#8354)
Andrew Reynolds [Mon, 21 Mar 2022 22:35:12 +0000 (17:35 -0500)]
Fix return value for candidate rewrite database (#8354)

Currently causes sygus reconstruction to return spurious solutions, due to being justified by candidate rewrites.

2 years agoRefactor documentation (#8288)
Gereon Kremer [Mon, 21 Mar 2022 21:19:11 +0000 (22:19 +0100)]
Refactor documentation (#8288)

This PR moves some stuff around in our documentation. Most notably, it moves some sections out of the "Binary documentation" to become their own top-level sections. While doing so, it refactors a few things in options and statistics to be more agnostic to the way cvc5 is used. To allow for command-output being used in regular (not auto-generated) documentation, we add a new extension that takes care of injecting the build folder into a new wrapper run-command.

2 years agoFix LFSC conversion for seq unit (#8353)
Andrew Reynolds [Mon, 21 Mar 2022 20:27:36 +0000 (15:27 -0500)]
Fix LFSC conversion for seq unit (#8353)

2 years agoFix names of unit tests (#8338)
Gereon Kremer [Mon, 21 Mar 2022 18:49:16 +0000 (19:49 +0100)]
Fix names of unit tests (#8338)

We are generally converging to tests names that are identical to their file name relative to the test directory, making running a particular subset of tests via ctest -R reasonably easy. This PR makes sure that the tests in unit/api/cpp also adhere to this schema.

2 years agoFix learned literals for top-level AND (#8336)
Andrew Reynolds [Mon, 21 Mar 2022 14:41:54 +0000 (09:41 -0500)]
Fix learned literals for top-level AND (#8336)

This is important for a deep restart strategy where substitutions may be consolidated by the preprocessor to a single AND.

2 years agoAdd `getStatistics()` to python API (#8343)
Gereon Kremer [Sun, 20 Mar 2022 16:39:41 +0000 (17:39 +0100)]
Add `getStatistics()` to python API (#8343)

This PR adds Solver.getStatistics() to the python API. To make the usage a bit more pythonic, we do not expose the iterator interface of api::Statistics but instead offer .get() which returns the whole range as a dictionary. The ::get() method to obtain a single statistic value is instead implemented via __getitem__().
The PR also includes the corresponding unit tests.

2 years ago[Parser] Simplify `Smt2::addIndexedOperator()` (#8333)
Andres Noetzli [Thu, 17 Mar 2022 21:36:48 +0000 (14:36 -0700)]
[Parser] Simplify `Smt2::addIndexedOperator()` (#8333)

It seems that Smt2::addIndexedOperator() has not been updated after we
fully switched the parser over to using API kinds. This commit
simplifies Smt2::addIndexedOperator() accordingly.

2 years agoctest: Fix labels for python unit tests. (#8328)
Aina Niemetz [Thu, 17 Mar 2022 19:59:43 +0000 (12:59 -0700)]
ctest: Fix labels for python unit tests. (#8328)

Previously, Python unit tests were labeled with one single label "unit
python". This fixes their labeling to two separate labels, "unit" and
"python".

2 years agoUpdate care graph computations to use standard node trie algorithm (#8298)
Andrew Reynolds [Thu, 17 Mar 2022 18:56:15 +0000 (13:56 -0500)]
Update care graph computations to use standard node trie algorithm (#8298)

Standardizes a few new methods in theory to support this.

This should not change the behavior, only refactors.

This is in preparation for adding efficient care graph computation for bags, and towards possible fixes for arrays.

2 years agoReplace `Debug` by `Trace` (#7793)
Gereon Kremer [Thu, 17 Mar 2022 18:00:56 +0000 (19:00 +0100)]
Replace `Debug` by `Trace` (#7793)

This PR replaces all usages of Debug() by Trace(), the same for similar methods like Debug.isOn().
Given that Debug is no longer used then, it is removed.

2 years agoRemove unused options handler (#8335)
Andres Noetzli [Thu, 17 Mar 2022 17:14:57 +0000 (10:14 -0700)]
Remove unused options handler (#8335)

The option --bitblast-aig was removed in #7455, but the corresponding
options handler was not. This commit removes the options handler.

2 years ago[CI] Use ccache for Windows builds (#8332)
Andres Noetzli [Thu, 17 Mar 2022 16:55:23 +0000 (09:55 -0700)]
[CI] Use ccache for Windows builds (#8332)

On Ubuntu, there are ccache symlinks for `x86_64-w64-mingw32-gcc` and `x86_64-w64-mingw32-g++` but not the POSIX-specific variants. Furthermore, not all Linux distributions add the `-posix` suffix for that variant. Thus, this commit changes our Toolchain file to use the more generic `x86_64-w64-mingw32-gcc` and `x86_64-w64-mingw32-g++` compiler names and changes our CI to use the POSIX variant by default.

2 years agoapi: Fix documentation for *TO_FP* kinds. (#8329)
Aina Niemetz [Thu, 17 Mar 2022 05:53:35 +0000 (22:53 -0700)]
api: Fix documentation for *TO_FP* kinds. (#8329)

2 years agoapi: Fix documentation for UNINTERPRETED_SORT_VALUE kind. (#8330)
Aina Niemetz [Thu, 17 Mar 2022 04:51:37 +0000 (21:51 -0700)]
api: Fix documentation for UNINTERPRETED_SORT_VALUE kind. (#8330)

2 years agodon't build gtest in CI (#8323)
Gereon Kremer [Thu, 17 Mar 2022 00:37:00 +0000 (01:37 +0100)]
don't build gtest in CI (#8323)

We currently build gtest in /usr/bin/... with every CI job on ubuntu. This PR removes this and uses our own external project instead. This way, we only build gtest if necessary and then cache these builds with ccache (saving some CI time).

2 years ago[CI] Strip stored binaries (#8327)
Andres Noetzli [Thu, 17 Mar 2022 00:12:09 +0000 (17:12 -0700)]
[CI] Strip stored binaries  (#8327)

This commit ensures that published binaries are stripped to make them
smaller. The stripping of the binaries is done before running the
regressions to make sure that the stripped binaries work as intended.
Stripping binaries decreases the executable size from about 28 MB to 24
MB.

2 years agoAdd unit test and assertion to test and catch cvc5-projects/issues/#337. (#7578)
Aina Niemetz [Wed, 16 Mar 2022 23:21:10 +0000 (16:21 -0700)]
Add unit test and assertion to test and catch cvc5-projects/issues/#337. (#7578)

2 years agoRemove unused files in `regress0` (#8325)
Andres Noetzli [Wed, 16 Mar 2022 22:56:23 +0000 (15:56 -0700)]
Remove unused files in `regress0` (#8325)

2 years ago[CI] Build and release Win64 binaries (#8321)
Andres Noetzli [Wed, 16 Mar 2022 21:29:27 +0000 (14:29 -0700)]
[CI] Build and release Win64 binaries (#8321)

This commit adds a check that cross-compiles a Windows binary, fixes
some minor issues to make the Windows build work, and adds support for
publishing a Windows binary to a (micro-)release.

Note: Regressions are currently not run for Windows builds.

2 years agoUse native cancellation mechanism (#8311)
Gereon Kremer [Wed, 16 Mar 2022 20:54:12 +0000 (21:54 +0100)]
Use native cancellation mechanism (#8311)

Github actions have a native mechanism to cancel previous runs of the same workflow now, much like the cancel workflow we have.

2 years agounit: Add test for api::Kind. (#8322)
Mathias Preiner [Wed, 16 Mar 2022 20:26:09 +0000 (13:26 -0700)]
unit: Add test for api::Kind. (#8322)

2 years agoFirst step towards refactoring regression tests. (#8324)
Aina Niemetz [Wed, 16 Mar 2022 19:44:33 +0000 (12:44 -0700)]
First step towards refactoring regression tests. (#8324)

This moves the current regression test infrastructure to
test/regress/cli. This is in preparation for introducing a new category
of regression api tests.

2 years agoAdd regression for cvc5-projects issue 490 (#8317)
mudathirmahgoub [Wed, 16 Mar 2022 04:49:36 +0000 (23:49 -0500)]
Add regression for cvc5-projects issue 490 (#8317)

Fixes cvc5/cvc5-projects#490.

2 years agoapi: Print the correct string for external kinds. (#8320)
Mathias Preiner [Wed, 16 Mar 2022 03:48:34 +0000 (20:48 -0700)]
api: Print the correct string for external kinds. (#8320)

We currently print the string representation of the internal kind.

2 years agorun_regression: Make sure to strip trailing whitespaces from error output. (#8319)
Mathias Preiner [Wed, 16 Mar 2022 03:07:25 +0000 (20:07 -0700)]
run_regression: Make sure to strip trailing whitespaces from error output. (#8319)

Should finally fix arm64 (qemu) nightly failures.

2 years agoapi: Make mkDatatypeDecl argument const&. (#8315)
Mathias Preiner [Wed, 16 Mar 2022 02:22:21 +0000 (19:22 -0700)]
api: Make mkDatatypeDecl argument const&. (#8315)

2 years agoFix shared library Windows builds with LibPoly (#8306)
Andres Noetzli [Wed, 16 Mar 2022 01:44:42 +0000 (18:44 -0700)]
Fix shared library Windows builds with LibPoly (#8306)

This commit fixes two issues that prevented us from compiling a shared
build of cvc5 for Windows:

    The search path of LibPoly is fixed to /usr/x86_64-w64-mingw32 when
    cross-compiling for Windows
    (https://github.com/SRI-CSL/libpoly/blob/06d4e3c1a1c18a5253398889c296ef787a3ce1cd/cmake/x86_64-w64-mingw32.cmake#L10).
    As a result, LibPoly was not able to find the cross-compiled version
    of GMP in our deps folder. Instead of passing search paths to
    LibPoly, this commit changes the CMAKE_ARGS passed to LibPoly to
    directly contain GMP_INCLUDE_DIR and GMP_LIBRARY.
    LibPoly installs the generated .dll files into bin instead of
    lib
    (https://github.com/SRI-CSL/libpoly/blob/06d4e3c1a1c18a5253398889c296ef787a3ce1cd/src/CMakeLists.txt#L91).
    The commit changes the by-products and
    Poly_LIBRARIES/PolyXX_LIBRARIES to account for this.

2 years agoFix getModelValue for arithmetic (#8316)
Andrew Reynolds [Wed, 16 Mar 2022 01:11:55 +0000 (20:11 -0500)]
Fix getModelValue for arithmetic (#8316)

Fixes #8276.

Theory::getModelValue is used as an optimization for computing the care graph of arrays. This method was wrong for (non-linear) arithmetic when the NL extension repaired values in the model.

2 years agoEnsure trusted steps are given for skolem lemmas when proofs are enabled (#8302)
Andrew Reynolds [Wed, 16 Mar 2022 00:41:06 +0000 (19:41 -0500)]
Ensure trusted steps are given for skolem lemmas when proofs are enabled (#8302)

Fixes cvc5/cvc5-projects#492.

2 years agoIgnore `CMAKE_SYSROOT` when cross-compiling (#8318)
Andres Noetzli [Wed, 16 Mar 2022 00:10:23 +0000 (17:10 -0700)]
Ignore `CMAKE_SYSROOT` when cross-compiling (#8318)

This commit changes our build system to ignore CMAKE_SYSROOT for
find_file(), find_path(), and find_library() when cross-compiling.
Previously, it could happen that, e.g., when we were cross-compiling a
static build for Windows, CMake would pick up /usr/lib/libgmp.a
instead of cross-compiling GMP. The comments in the Toolchain-*.cmake
files suggest that the new behavior was the intended behavior all along.

2 years agoMake learned literal computation more robust (#8308)
Andrew Reynolds [Tue, 15 Mar 2022 23:32:45 +0000 (18:32 -0500)]
Make learned literal computation more robust (#8308)

Simplifies our computation so that preprocessed learned literals are those exactly appearing as top-level assertions only.

2 years agoapi: Remove Sort::isFirstClass(). (#8312)
Aina Niemetz [Tue, 15 Mar 2022 22:51:42 +0000 (15:51 -0700)]
api: Remove Sort::isFirstClass(). (#8312)

2 years ago[BV] Fix strategy for rewriting `bvnot` (#8297)
Andres Noetzli [Tue, 15 Mar 2022 22:20:09 +0000 (15:20 -0700)]
[BV] Fix strategy for rewriting `bvnot` (#8297)

Fixes #8240. The currenty strategy was returning REWRITE_DONE
incorrectly, e.g., when we had a term like (bvnot (bvnot (bvnot #b0)))
because EvalNot was applied before NotIdemp, so we did not evaluate
the innermost bvnot after removing the double bvnot. The commit
fixes the strategy s.t. we are allowed to return REWRITE_DONE.

2 years agoAdd unit test involving seq concat term (#8257)
Andrew Reynolds [Tue, 15 Mar 2022 21:42:39 +0000 (16:42 -0500)]
Add unit test involving seq concat term (#8257)

On closer inspection, the initial version of the unit test has a type error, where an incorrect concatentation term is constructed.

Adds the updated test. Fixes cvc5/cvc5-projects#423.

2 years agoFix issues involving multiple sources of model substitutions in NL (#8300)
Andrew Reynolds [Tue, 15 Mar 2022 21:12:55 +0000 (16:12 -0500)]
Fix issues involving multiple sources of model substitutions in NL (#8300)

Fixes #8294.

The first benchmark times out, the second is added as a regression.

The issues center around 2 sources of substitutions (coverings and sine solvers) for model substitutions.

Also does minor cleanup to nl model.

2 years agoAdd skolem lemmas for bags card terms (#7995)
mudathirmahgoub [Tue, 15 Mar 2022 19:28:41 +0000 (14:28 -0500)]
Add skolem lemmas for bags card terms (#7995)

This PR refactors the way skolem lemmas are generated for bags, count terms, and card terms.
As a side effect, this refactoring fixed cvc5/cvc5-projects#481

2 years agoProperly guard sort instantiate (#8247)
Andrew Reynolds [Tue, 15 Mar 2022 18:47:36 +0000 (13:47 -0500)]
Properly guard sort instantiate (#8247)

Fixes cvc5/cvc5-projects#387.

Adds a prefix of that unit test before the first exception.

2 years agoEnable nl-cov-var-elim by default, but disable with proofs (#8310)
Gereon Kremer [Tue, 15 Mar 2022 18:25:21 +0000 (19:25 +0100)]
Enable nl-cov-var-elim by default, but disable with proofs (#8310)

This changes our policy for --nl-cov-var-elim. It is now enabled by default (it is only used when the coverings solver is used, though), but then disabled when proofs are enabled. Before, it was forced to be enabled when coverings were enabled in set_defaults.

Fixes cvc5/cvc5-projects#489

2 years agoRemove unecessary separation logic options (#8269)
Andrew Reynolds [Tue, 15 Mar 2022 17:07:14 +0000 (12:07 -0500)]
Remove unecessary separation logic options (#8269)

Code changed indentation and was cleaned slightly.

2 years agoSimplify `Scope` (#8307)
Andres Noetzli [Tue, 15 Mar 2022 16:07:44 +0000 (09:07 -0700)]
Simplify `Scope` (#8307)

Previously, we were using an std::unique_ptr<std::vector<ContextObj*>>
to store the list of ContextObjs to be garbage collected before the
destruction of the Scope. Lazily allocating that vector is a
micro-optimization that is not worth the trouble.

2 years agoFix to consider leafs of theory sets to be variables (#8305)
Andrew Reynolds [Tue, 15 Mar 2022 03:16:41 +0000 (22:16 -0500)]
Fix to consider leafs of theory sets to be variables (#8305)

Fixes cvc5/cvc5-projects#494.

With this fix, we now properly consider terms that belong to other theories that are of set type, e.g. (select x (as set.universe (Set RoundingMode)) in this example to be "variables" according to the theory of sets procedure.

The benchmark is unsat because there are 5 rounding modes and we are selecting an index in a sequence storing "false" at the first 6 indices.

2 years agoSimplify reductions for set and bag choose (#8304)
Andrew Reynolds [Tue, 15 Mar 2022 01:11:12 +0000 (20:11 -0500)]
Simplify reductions for set and bag choose (#8304)

Ensures that the reductions are deterministic, thus fixes cvc5/cvc5-projects#493.

The reductions can be further simplified to not introduce UF. This will be addressed in a later PR.