Open
Conversation
…rewriter (cvc5#11556) Behavior (mostly) does not change in this PR, apart from eliminating a few direct calls to the rewriter. We no longer pass the rewriter directly to the strings rewriter. The next step will be to not pass the rewriter to the arith/string entailment utilities in the main rewriter. Will performance test this change.
Adds 24 string rewrites addressing some of the low hanging rewrite proof holes in SMT-LIB and our regressions.
It also applies a workaround for the Twine issue [cvc5#1216](pypa/twine#1216).
It also uses Twine to check the generated wheels and the `--skip-existing` option in Twine to continue uploading files if they already exist.
Signed-off-by: Robert Bradshaw <[email protected]>
These rewrites have not shown to be important in practice and moreover are cumbersome to represent in proofs. The behavior of the extended rewriter still is able to accomplish these rewrites. The extended rewriter is modified slightly in this PR to be more robust in general with further changes.
These are 8 tests for the conjecture generator. I have removed any irrelevant commands that I could identify, including assertions. cvc5 takes <1 second to report 'unsat' for each test so long as the unsat core tester is disabled. Based on my observations cvc5 cannot solve them with induction switched on and conjecture generation switched off, making conjecture generation essential to get a quick 'unsat' response from the solver. These tests will help ensure that I do not worsen the performance of the conjecture generator as I clean it up. They might also help us identify which changes to other components of cvc5 can impact the conjecture generator. Fixes cvc5#11520
This operation will be at the heart of ~5 forthcoming proof rules. This PR deletes the primative `Word::noOverlapWith` (which wasn't directional and had a more complicated meaning) in favor of this new utility. A rewrite that relies on this utility is demoted to the extended rewriter. Unit tests are added for this utility.
This adds the default implementation of a proof logger (for cpc proofs). It also adds some logic to ensure proof logging is used only in valid configurations.
This adds the Eunoia definition of the evaluation methods for the SMT-LIB standard operators `str.replace_re` and `str.replace_re_all`, and the cvc5-specific extension `str.indexof_re`. It also updates the strings rewrite to call the reference implementations of these rules, which was missed in a previous PR. Note these evaluators call `$str_eval_str_in_re` as a submethod, which would benefit automatically from future optimizations to this method.
Towards filling remaining proof holes. Furthermore adds this case to the Eunoia signature for `evaluate`.
Requires 4 new RARE rewrites for ITE lifting, and 4 for reasoning about min/max terms.
A separate step is necessary to partition the expert RARE rewrites / non-expert ones, after which I will ensure the includes are fully disjoint.
…1543) The `cong` rule of `Uf.eo` uses `$nary_reverse` in its conclusion. Import `programs/Nary.eo` to resolve this issue. In `Nary.eo`, the type `Int` from `theories/Arith.eo` is used in `$nary_prefix` and `$nary_subsequence`. Import `theories/Arith.eo` to resolve this issue. Because `theories/Arith.eo` imports `theories/Builtin.eo`, which imports `programs/Utils.eo`, the import of `programs/Utils.eo` in `programs/Nary.eo` is no longer needed. Remove this include. Signed-off-by: ciaran <[email protected]>
This splits the definitions of arith/bv conversion functions to their own theory file and adds the 2 existing theory rewrites for eliminating these two operators via reductions to the CPC+Eunoia signature.
…5#11582) I think the implementation of `ConjectureGenerator::check()` will read better if it is split across a few helper functions.
Also makes minor modifications to the reduction utility to make it consistent with the style of the other reductions.
…verlap reasoning (cvc5#11580) This adds a four new ad-hoc theory rewrites for strings, including their internal and Eunoia definitions. 3 of these rules are exercized extensively in SMT-LIB, and all 4 will be covered in regressions once they are enabled. They are each based around the notion of computing "overlaps". This will be used to elaborate proofs for 4 macro theory rewrites, to be added in followup PRs. Note: in their current form, these rules *cannot* be applied to sequences, as it is non-trivial in general to *prove* the distinctness of sequence characters. Furthermore note that the existing definition of `ProofRule::CONCAT_CPROP` will be later simplified to use the `$str_has_overlap` utility (it currently computes the *size* of a maximal overlap using `$str_overlap`, which can be simplified by an internal elaboration step). The signature definition of this rule at the moment is theoretically unsound for sequences, since we do not prove the distinctness of sequence characters (although cvc5 internally will do so).
CI currently builds cvc5 on Ubuntu 20.04 to ensure compatibility with this older OS version for dynamically linked binaries. However, the Ubuntu 20.04 Actions runner image will begin deprecation on 2025-02-01 and will be fully unsupported by 2025-04-01 (see [notice](actions/runner-images#11101) here). Therefore, this PR updates the runners to Ubuntu 22.04. Additionally, this PR removes a workaround previously required for old versions of ccache.
This change has a similar motivation to cvc5#11501. In particular, it is unintuitive to store an internal kind as an argument to a proof rule which is exported. Instead, we store the conclusion of the rule, analogous to ARITH_POLY_NORM. The Eunoia definition can be made more elegant.
This adds proof elaboration for the recently itnroduced rule `MACRO_ARRAYS_NORMALIZE_OP` in terms of small step rewrites that RARE can handle. Notice that `MACRO_ARRAYS_NORMALIZE_OP` is now attempted *prior* to RARE, meaning this rule now is used to preprocess >99% of array rewrites into single steps for RARE.
…vc5#11590) This is work towards simplifying CPC and its formalism in Eunoia for the sake of further verification efforts.
Makes the following changes: - `produceUnsatCores`, `checkUnsatCores` are promoted to "common" as they are part of our core infrastructure. - `fullSaturateQuant`/`enumInst` (which are an alias of one another) are promoted to "common". The justification is that this option is recommended to be used in addition to any other combination of options for quantifiers for those that prefer more effort + timeouts to unknowns. - Similarly, `decisionMode` is promoted to "common", as it is intended to be used in combination with all other options, e.g. in portfolios. - `unconstrainedSimp` and `sortInference` are demoted to "expert" since they do not meet the requirements of producing *models* (as well as proofs). - A new expert option `varEntEqElimQuant` now guards a (seldom used) rewrite for quantifiers+strings that is hard to justify.
The fix involves the use of unused variables to ensure we can miniscope OR when reversing elaboration of prenex. Both were leading to proof holes which this PR fixes. The second ensures we add unique variables for shared subformulas. For example: forall x. (forall y. P(y) or forall y. P(y)) we previously would prenex to: forall x z z. (P(z) or P(z)) now we prenex to forall x z w. (P(z) or P(w)) While it is technically legal to prenex to the same variable when their polarity is the same, it is harder to justify and leads to unexpected shadowing. --------- Co-authored-by: Abdalrhman Mohamed <[email protected]>
This fixes a bug in how RARE proof reconstruction works for macro elaboration. In particular, our subgoal tracking was incorrect if a macro was elaboarted to a single TRUST step as a subgoal, since the updater updates the current proof node in-place. The PR cvc5#11441 introduces a case in our regressions for this. To fix this, I've refactored the post-processor to a more elegant version which runs the proof node updater recursively. It tracks the depth of how many trust steps we've expanded in the current context using a `d_traversing` vector. This makes explicit tracking of subgoals unecessary, the RARE proof reconstruction method is cleaned up as a result.
This is necessary to build against libc++ in newer LLVM versions.
Includes one regression where cvc5 fails to generate a proof, due to non-determinism in the rewriter. I've opened cvc5/cvc5-projects#760 to track this.
…vc5#11441) Adds 2 new RARE rules that suffice to prove these rules. FYI @Lachnitt This fills all the remaining known holes for (linear) arithmetic rewriting.
Introduces a new utility method in the style of others in node_algorithm.h and updates a non-standard use of checking for bound variables.
- Add .toml files for the existing kinds - Add python script to generate type_checker.cpp --------- Co-authored-by: Mathias Preiner <[email protected]>
Co-authored-by: Daniel Larraz <[email protected]>
This fixes issues in C++ `deadPool` test and resolves nightly memory leak failure.
This adds a simple utilty for attempting to reconstruction proofs for unhandled arithmetic theory lemmas. In particular, lemmas marked `ARITH_DIO_LEMMA` typically can be reconstructed using substitution+rewriting, leveraging the rewrite rules from cvc5#11441. This fills in the last remaining holes for arithmetic theory lemmas in the regressions and SMT-LIB. --------- Co-authored-by: Abdalrhman Mohamed <[email protected]>
…vc5#11808) This makes the essential changes to support the new defaults of declare-parameterized-const. It also fixes some misplaced attributes which will be caught by ethos when it is updated.
It is redundant to apply `$singleton_elim` to heads of RARE rules, as we know heads are always matched syntactically. This makes the Eunoia definitions clearer and should help performance slightly.
The evaluator is primarily used for sygus symmetry breaking and for RARE proof reconstruction. Moreover repeat is eliminated during rewriting, so this bug had a very minimal impact. I discovered it due to a proof hole that appeared in my dev branch related to RARE reconstruction.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
15 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.