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.
mudathirmahgoub [Wed, 23 Mar 2022 02:53:38 +0000 (21:53 -0500)]
update SET_COMPREHENSION documentation (#8372)
Andrew Reynolds [Wed, 23 Mar 2022 02:12:34 +0000 (21:12 -0500)]
Initial documentation on LFSC (#8365)
mudathirmahgoub [Wed, 23 Mar 2022 01:11:06 +0000 (20:11 -0500)]
Fix cvc5-projects issue 497 (#8331)
Fixes cvc5/cvc5-projects#497
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.
Andrew Reynolds [Tue, 22 Mar 2022 23:36:37 +0000 (18:36 -0500)]
Change null terminator for regular expression intersection (#8362)
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.
Andrew Reynolds [Tue, 22 Mar 2022 21:24:52 +0000 (16:24 -0500)]
Updates for the theory reference for separation logic (#8366)
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.
Haniel Barbosa [Tue, 22 Mar 2022 19:53:42 +0000 (16:53 -0300)]
[proofs] Alethe: fixing formatting and adding missing comment (#7779)
mudathirmahgoub [Tue, 22 Mar 2022 19:14:59 +0000 (14:14 -0500)]
update sets-and-relations.rst (#8364)
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.
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.
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.
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.
Mathias Preiner [Tue, 22 Mar 2022 00:22:41 +0000 (17:22 -0700)]
api: Unify mkTerm variants. (#8357)
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.
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[]()`.
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.
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.
Andrew Reynolds [Mon, 21 Mar 2022 20:27:36 +0000 (15:27 -0500)]
Fix LFSC conversion for seq unit (#8353)
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.
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.
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.
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.
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".
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.
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.
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.
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.
Aina Niemetz [Thu, 17 Mar 2022 05:53:35 +0000 (22:53 -0700)]
api: Fix documentation for *TO_FP* kinds. (#8329)
Aina Niemetz [Thu, 17 Mar 2022 04:51:37 +0000 (21:51 -0700)]
api: Fix documentation for UNINTERPRETED_SORT_VALUE kind. (#8330)
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).
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.
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)
Andres Noetzli [Wed, 16 Mar 2022 22:56:23 +0000 (15:56 -0700)]
Remove unused files in `regress0` (#8325)
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.
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.
Mathias Preiner [Wed, 16 Mar 2022 20:26:09 +0000 (13:26 -0700)]
unit: Add test for api::Kind. (#8322)
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.
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.
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.
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.
Mathias Preiner [Wed, 16 Mar 2022 02:22:21 +0000 (19:22 -0700)]
api: Make mkDatatypeDecl argument const&. (#8315)
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.
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.
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.
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.
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.
Aina Niemetz [Tue, 15 Mar 2022 22:51:42 +0000 (15:51 -0700)]
api: Remove Sort::isFirstClass(). (#8312)
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.
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.
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.
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
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.
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
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.
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.
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.
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.
Aina Niemetz [Tue, 15 Mar 2022 00:18:52 +0000 (17:18 -0700)]
Rename TO_FP operator kinds. (#8285)
FLOATINGPOINT_TO_FP_FP -> FLOATINGPOINT_TO_FP_FROM_FP
FLOATINGPOINT_TO_FP_IEEE_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_IEEE_BV
FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_SBV
FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_UBV
FLOATINGPOINT_TO_FP_REAL -> FLOATINGPOINT_TO_FP_FROM_REAL
Andrew Reynolds [Mon, 14 Mar 2022 21:02:40 +0000 (16:02 -0500)]
Fixes for skolem definition management (#8301)
Fixes two issues with how we manage skolem definitions (used for tracking which assertions are relevant for the decision engine).
First, the theory proxy must be notified of skolem definitions before we have assertions involving them, or else hasSkolems is wrong. This was previously done incorrectly for lemmas. This PR changes the order in PropEngine::assertLemmasInternal.
Second, skolem definitions are local to a solver instance and should not be managed by attributes, moreover they are user-context dependent. This changes it to a local user-context dependent map in Skolem.
Fixes #8296.
Andrew Reynolds [Mon, 14 Mar 2022 18:29:30 +0000 (13:29 -0500)]
Remove unecessary methods from the API (#8260)
Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.
Updates examples and unit tests.
Andrew Reynolds [Mon, 14 Mar 2022 18:02:09 +0000 (13:02 -0500)]
Add rewrite for allchar beneath union + star (#8299)
Addresses the issue on #8295.
The re elimination module was assuming that a trivial RE was rewritten when it was not.
Andrew Reynolds [Mon, 14 Mar 2022 16:56:52 +0000 (11:56 -0500)]
Run preprocess rewrite on equalities until fixed point (#8291)
Previously we were only running once, while strings assumed this was run on what it returned.
This should significantly improve our performance on the benchmarks from SMT-LIB that involving looping word equations.
Andrew Reynolds [Sun, 13 Mar 2022 01:31:56 +0000 (19:31 -0600)]
Minor sync from proof-new (#8293)
Andrew Reynolds [Sat, 12 Mar 2022 23:21:02 +0000 (17:21 -0600)]
Introduce new splitting inference in sets + cardinality (#8290)
Fixes cvc5/cvc5-projects#486.
This introduces a new strategy which splits on whether Venn regions are equal to each other before it splits them into sub-Venn regions.
The issue in the above was caused by a case where the sets solver decided to make 2 Venn regions of the same equivalence class disjoint. By splitting on their equality first, this should introduce the necessary information to discover this is a conflict (via disequality witnessing). It should also be more efficient since we introduce new set terms lazier.
Andrew Reynolds [Sat, 12 Mar 2022 04:18:12 +0000 (22:18 -0600)]
Add algorithm for finding pairs of paths in a node trie (#8286)
This is in preparation for cleaning our implementation of care graph computations.
Right now, UF, datatypes, sets, and strings all have copy/pasted versions of an algorithm that creates an index of operators and run the algorithm in the PR for computing care graphs.
Followup PRs will extend the theory interface and add an instance of this class for computing care graphs. Then, we will add optimized care graph computation for bags (which is missing right now), and then perhaps revisit arrays, which appears to have issues in its computeCareGraph method.
Mathias Preiner [Sat, 12 Mar 2022 03:54:49 +0000 (19:54 -0800)]
cmake: Do not require googletest if unit tests are disabled. (#8271)
Fixes #8088
Andrew Reynolds [Sat, 12 Mar 2022 03:29:23 +0000 (21:29 -0600)]
Improvements for sygus query generation (#8224)
Makes the two sygus query generators have a common base class, which makes it so that they both can dump queries.
Also fixes the expression miner to use user-level sygus terms, otherwise we can make queries using invalid internal terms, e.g. SEQ_NTH_OOB skolem.
The majority of the diff in this PR is moving query_generator to query_generator_sample_sat, and adding a basic version of query generation.
Andrew Reynolds [Sat, 12 Mar 2022 01:09:54 +0000 (19:09 -0600)]
Document type rules (#8248)
Fixes cvc5/cvc5-projects#272.
Fixes cvc5/cvc5-projects#270.
Fixes cvc5/cvc5-projects#269.
Fixes cvc5/cvc5-projects#268.
Also makes a few minor internal fixes to type rules.
Andrew Reynolds [Sat, 12 Mar 2022 00:26:37 +0000 (18:26 -0600)]
Always ensure literal when requiring phase via inference manager (#8292)
Also to be safe, ensures we clear pending in quantifiers engine.
Fixes cvc5/cvc5-projects#484.
Andres Noetzli [Fri, 11 Mar 2022 23:46:38 +0000 (15:46 -0800)]
[API/Python] Add support for `Solver::getModel()` (#8267)
This commit implements support for Solver::getModel() in the Python API,
which was missing before.
Aina Niemetz [Fri, 11 Mar 2022 23:08:31 +0000 (15:08 -0800)]
api: Make checks header private. (#8283)
Andrew Reynolds [Fri, 11 Mar 2022 22:11:07 +0000 (16:11 -0600)]
Remove old decision justification heurstic (#8275)
Fixes cvc5/cvc5-projects#374.
Andrew Reynolds [Fri, 11 Mar 2022 21:41:54 +0000 (15:41 -0600)]
Update abduction and interpolation API to not use pass/return by reference (#8263)
Andrew Reynolds [Fri, 11 Mar 2022 21:09:53 +0000 (15:09 -0600)]
Fix maximum value for pedantic proof level (#8246)
Fixes cvc5/cvc5-projects#357.
Now gives:
(error "Error in option parsing: proof-pedantic =
5773657586652532005 is not a legal setting, value should be at most 100.")
Andrew Reynolds [Fri, 11 Mar 2022 20:49:36 +0000 (14:49 -0600)]
Guard parametric datatypes instantiated by non-first-class sorts (#8277)
Fixes cvc5/cvc5-projects#471.
Gereon Kremer [Fri, 11 Mar 2022 20:09:45 +0000 (21:09 +0100)]
Add first step for proofs documentation (#8193)
This PR initializes some documentation for our proofs. It adds some almost empty files and makes sure that we can show documentation for the PfRule enum.
Andrew Reynolds [Fri, 11 Mar 2022 19:41:46 +0000 (13:41 -0600)]
Remove unecessary CEGQI options (#8281)
Code changed indenting, but did not change otherwise.
Andrew Reynolds [Fri, 11 Mar 2022 18:03:09 +0000 (12:03 -0600)]
Consider APPLY_CONSTRUCTOR applied to values to be a value (#8284)
Fixes cvc5/cvc5-projects#474.
Previously TheoryModel::isModelValue was incorrect for APPLY_CONSTRUCTOR.
Andrew Reynolds [Fri, 11 Mar 2022 17:40:16 +0000 (11:40 -0600)]
Fix reduction for arc trig functions (#8289)
We were not guarding the case where the argument was out of the bounds, e.g. arccos(x) requires -1 <= x <= 1.
Fixes cvc5/cvc5-projects#485.
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.
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.
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.
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.
Andrew Reynolds [Thu, 10 Mar 2022 19:20:35 +0000 (13:20 -0600)]
Eliminate unecessary datatype options (#8280)
mudathirmahgoub [Thu, 10 Mar 2022 18:49:31 +0000 (12:49 -0600)]
Fix cvc5-projects issue 475 (#8278)
Fixes cvc5/cvc5-projects#475.
Andrew Reynolds [Thu, 10 Mar 2022 18:28:54 +0000 (12:28 -0600)]
Add output -o pre-asserts (#8270)
Analogous to -o post-asserts.
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.
Mathias Preiner [Thu, 10 Mar 2022 00:28:44 +0000 (16:28 -0800)]
Fix regression errors for arm64 nightlies. (#8268)
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.
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
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.
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.
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.
Andrew Reynolds [Wed, 9 Mar 2022 01:42:37 +0000 (19:42 -0600)]
Add regression for fixed issue 6700 (#8265)
Fixes #6700.
Andrew Reynolds [Wed, 9 Mar 2022 00:21:34 +0000 (18:21 -0600)]
Eliminate the APPLY_SELECTOR_TOTAL kind (#8266)
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.
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.