| Age | Commit message (Collapse) | Author |
|---|
|
Also deletes unused code encountered in TheoryArrays while investigating cyclic proofs.
|
|
This is a coarse grained proof rule for showing that two terms are equivalent up to polynomial normalization. It will be used as a hard coded case in proof reconstruction with DSL granularity.
|
|
Includes miscellaneous improvements and fixes to the LFSC proof conversion from proof-new in preparation for CI on master.
|
|
Essentially moves the code for this check from the Alethe post-processor. A further PR will include a new use of this method.
|
|
This avoids cyclic proofs in a rare case where theory explanations involve an equality and its symmetric form.
This PR disables auto-symmetry on lazy proofs used for theory explanations, which is slightly less convenient but avoids potentials for cyclic proofs. Note this complication would not arise if the theory engine did not allow non-rewritten equalities to be propagated between theories.
Fixes cvc5/cvc5-projects#311.
|
|
Implementation of the translation of a number of rules that follow the clause pattern into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of AND_ELIM rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of CONTRA rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of NOT_NOT_ELIM rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of MODUS_PONENS rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of SPLIT rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
This PR resolves a subtle issue with CDCAC proofs.
The CDCAC proof is maintained as a tree where (mostly) every node corresponds to an (infeasible) interval generated within the CDCAC method. We prune these intervals regularly to get rid of redundant intervals, which also sorts intervals. The pruning however relied on a stable ordering of both intervals and child nodes within the proof tree, as there was no easy way to map nodes back to intervals.
This PR adds an objectId field to the proof tree nodes and assigns ids to the CDCAC intervals. This allows for a robust mapping between the two, even if the interval list is reordered.
Fixes cvc5/cvc5-projects#313.
|
|
Implementation of the translation of FACTORING rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of RESOLUTION and CHAIN_RESOLUTION rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
|
|
Provides background on the translation into the Alethe calculus that is common to all rules.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
|
|
This adds the remaining implementation of the LFSC printer.
It also corrects a bug introduced during merging the last PR.
The printer will be connected to the proof manager in a follow up PR. It will also be extended with support for DSL proof rule printing when the infrastructure is added.
|
|
This adds the LFSC printer for proof nodes. This PR has been split to not include support for DSL rewrite rules yet, or its main print method which will be added in a followup PR.
Further PRs will connect this printer as a possible output format for cvc5.
|
|
Changes the order of the arguments of addAletheStepFromOr to be consistent with addAletheStep.
|
|
Implementation of the translation of THEORY_REWRITE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Adds Alethe proof rule and option. Adds alethe_post_processor and alethe_proof_rule files to list of files to be compiled.
During incorporating these changes errors occurred in the SCOPE rule that are also fixed in this PR.
|
|
Implementation of the translation of SCOPE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
This is a modified version of #6137 which accounts for extended rewriting between quantified formulas that are considered alpha equivalent.
It also generalizes the proof rule ALPHA_EQUIV. Notice that if we were to make this rule more pedantic, we would check for variable shadowing during substitution, although this is not currently done.
|
|
Implementation of the translation of ASSUME rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of addAletheStep and addAletheStepFromOr. Added stub for AletheProofPostprocessCallback update function that will be populated by subsequent PRs.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Currently the only transformation it applies is removing attributes from quantifiers. Others may be added later.
|
|
Includes the necessary conversions to LFSC for the core rules of the internal calculus.
|
|
Added proof postprocessor class to alethe_proof_processor header file.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Added final callback class to alethe_proof_processor header file.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Added alethe_proof_processor header file and introduced callback class.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation file for Alethe proof rules.
|
|
Adds header for Alethe proof rules
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
These are utilities used for two-pass printing of LFSC proofs.
|
|
This also heavily refactors the preskolemization method (now in QuantifiersPreprocess), in preparation for it being enabled by default. This method previously was doing a tree traversal, it now maintains a visited cache.
It makes minor cleanup to the dependencies of this method.
|
|
Required for automatic generation of side conditions from DSL rewrite rules.
|
|
|
|
This utility converts from terms used in the internal calculus to terms that capture how they should be printed in LFSC.
|
|
This implements several variants of lazy proof checking in the core proof checker.
Note this extends the ProofNode class with an additional Boolean d_provenChecked indicating whether the d_proven field was checked by the underlying proof checker.
This PR updates the default proof checking mode to lazy. The previous default can now be enabled by --proof-check=eager-simple.
|
|
Our way of constructing proofs from the equality engine in very rare cases may cause cyclic proofs due to constructing double applications of SYMM, which are not recognized as assumptions in CDProof. This is due to an interplay between LazyProofChain using an underlying CDProof as its default proof generator, where the proof chain would use the proofs from the CDProof to form a cyclic proof.
This was encountered in 9 SMT-LIB benchmarks in QF_SLIA.
This makes us safer in several places related to double SYMM steps.
|
|
This makes it so that we call the strings::InferProofCons::convert lazily, instead deferring to a temporary, trusted STRING_INFERENCE rule.
This decreases our average proof overhead on commonly solved instances from 64% to 58% on QF_S + QF_SLIA. It also reduces timeouts significantly, from 2010 to 1460. (Note these numbers were with a slightly extended version of this branch that includes other pending PRs for proofs).
Also fixes one subtle issue where proof reconstruction was misusing sequential substitutions (leading to warnings during proof post-processing).
|
|
There was an inconsistency between when the equality engine would explain a literal and when we would provide a proof for it. This led to rare cases where we over zealously provided a proof for a fact that should have been an assumption in the theory lemma proof.
This corrects the issue by ensuring that no-explain premises are explicitly marked via a new helper proof generator "AssumptionProofGenerator" which always supplies (ASSUME f) as the proof for f.
This corrects some proof checking errors on string benchmarks.
|
|
Makes it so that all theory-specific proof rules for this purpose are replaced by the generic THEORY_INFERENCE.
|
|
|
|
|
|
This makes it so that we replace subproof A with subproof B if A and B prove the same thing, and B contains no assumptions. This is independent of the scope that A and B are in.
The previous policy replaced subproof A with subproof B if A and B prove the same thing and were in the same scope. This is not safe if A occurs in multiple scopes, where free assumptions can escape.
The new policy is more effective and safer than the previous one.
|
|
This PR fixes the escaped characters in the dot printer. The output is now a valid DOT.
Signed-off-by: Diego Della Rocca de Camargos diegodellarocc@gmail.com
|
|
Work towards making our policy for subproof merging safer.
|
