| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
Adds proof support for the eqrange operator.
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
This adds optional arguments to INSTANTIATE steps in proofs to track fine-grained reasons for relevant instantiations.
Also simplifies an old argument modEq which was unused.
FYI @MikolasJanota
|
|
Adds basic utilities in preparation for the LFSC proof conversion.
Depends on #6881, review that first.
|
|
This will be used in the LFSC printer. It may be of general use to other proof printers.
|
|
Towards support for external proof conversions.
|
|
This enables default support for equality proofs in the theory of sets.
This is in preparation for proofs in the central equality engine, which requires that all active theories that use the central equality engine at least support the default interaction with the equality engine.
|
|
|
|
|
|
Introduces BV_BITBLAST_STEP rule, which replaces BV_BITBLAST_X rules.
|
|
The let map is printed as JSON-like dictionary via a comment of the dot output.
|
|
This changes an annotation of a step of rewriting from "post" to "pre" in the theory preprocessor.
Fixes #6754.
|
|
In preparation for further changes in the printer.
|
|
|
|
|
|
This PR fixes a missing connection in trust substitution proofs, which was the cause of open proofs when solved equalities from ppAssert were not justified by proofs.
Also distinguishes TRUST_SUBS_EQ from TRUST_SUBS_MAP for clarity.
|
|
|
|
This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.
|
|
We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).
The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.
|
|
This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.
It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").
|
|
This commit removes the remaining old proof code and the code to produce unsat cores based on it.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
propositional) (#6423)
Conclusion and rule are placed on the same node (records nodes in the dot format).
Nodes are colored based on the view they will belong to.
Signed-off-by: Diego Della Rocca de Camargos diegodellarocc@gmail.com
|
|
This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:
the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.
|
|
This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This PR uses IntegralHistogramStat instead of HistogramStat when appropriate, that is everywhere.
|
|
Adds a dot printer for proof nodes. Also adds an option to choose the proof format (as a mode).
Signed-off-by: Diego Della Rocca de Camargos <diegodellarocc@gmail.com>
|
|
This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.
Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.
|
|
|
|
|
