| Age | Commit message (Collapse) | Author |
|---|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
|
|
|
|
|
|
calculus (#6051)
This makes a simplification to the internal proof calculus. In particular, purification skolems are no longer are special case of witness skolems. They are now independent concepts. The concept of "witness form" is replaced in most places by "original form".
This is required for fixing two issues:
(1) variable shadowing issues in skolemization.
(2) bookkeeping issues for bound variables introduced to construct witness terms. This made the LFSC proof conversion extremely cumbersome for e.g. string reductions.
In this PR, the main changes:
The internals of SkolemManager are changed to use original form vs witness form when necessary. This eliminates the need to do variable renaming in SkolemManager::skolemize.
the rule WITNESS_INTRO is replaced by SKOLEM_INTRO
MACRO_SR_* rules use original form
Proof post processing is simplified
These changes imply that ppRewrite should not return WITNESS terms. Followup PRs will modify arithmetic preprocessing so that its ppRewrite method returns skolems instead.
|
|
|
|
generator (#5833)
This is work towards resolving two kinds of failures on proof-new:
(1) Functional issues with proofs from the rewriter, in particular when a term pre-rewrites and post-rewrites to different things,
(2) Conversion issues in theory-preprocessing, where all steps are assumed to be post-rewrites but some are in fact pre-rewrites. This leads to the term conversion proof generator proving something different than what is expected.
A followup PR will simplify and fix proofs for theory-preprocessing.
|
|
Ensuring closed proofs should not be enabled by default, it is actually not used very often as a whole. Moreover, the "trust id" argument is the most useful argument and hence should come as the 3rd argument. This updates all uses of addLazyStep for the change in interface, also changes term conversion generator which had a similar issue with default arguments.
Notice that some calls to addLazyStep were checking closed but without providing a debug string, these I've left alone (they no longer check closed).
|
|
This formalizes the proofs of existentials that justify purification variables, e.g. those with witness form witness x. x = t for the term t they purify.
This PR generalizes EXISTS_INTRO to do this, and makes some simplifications to SkolemManager.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
(#5072)
In some cases, e.g. witness form conversion, we require traversing to operators in term conversion proofs. This updates the term conversion generator to support (term-context-sensitive) rewrites involving operators using HO_CONG. This requires updating the term context utilities with support for operators.
|
|
This includes configurable naming and a caching policy for term conversion proof generator.
Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs.
|
|
This class is responsible for the connection between terms and their witness form in the final proof.
|
