summaryrefslogtreecommitdiff
path: root/src/expr/proof_node_manager.cpp
AgeCommit message (Collapse)Author
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
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").
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-07(proof-new) Proper implementation of proof node cloning (#6285)Andrew Reynolds
Previously, we were traversing proof node as a tree, now we use a dag traversal. This also makes sure that proofs work when we have a external proof conversion and we are in incremental mode. In such cases, the final proof must be cloned to ensure that we do not overwrite proof nodes, which may be reused across multiple check-sat.
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-25Add missing includes. (#6207)Gereon Kremer
This PR adds includes that are missing from source files, but currently provided by other includes. This mostly concerns <sstream> which is currently included by the statistics, which will change in the future.
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
2021-02-22(proof-new) Change proof-new option to proof (#5955)Andrew Reynolds
Also moves several proof-specific options to proof_options.
2020-12-02Update copyright headers.Aina Niemetz
2020-11-12(proof-new) Fix true explanations of propagations in pf equality engine (#5338)Andrew Reynolds
This ensures we construct proper proofs for propagations whose conclusions are of the form (=> true lit). Literals may be propagated with "true" as an explanation in datatypes, e.g. discriminators for datatypes with 1 constructor.
2020-10-18(proof-new) Refactoring cyclic checks (#5291)Andrew Reynolds
This PR makes it so that cyclic checks are only performed eager when proofNewEagerChecking is true. It refactors the existing cyclic check in ProofNodeToSExpr to have a more consistent style, and adds a cyclic check to getFreeAssumptions.
2020-10-06(proof-new) Allow null proofs from generators in LazyCDProof (#5196)Andrew Reynolds
In some cases, a proof generator provided to a LazyCDProof may provide a null proof, which causes a segfault on proof-new currently. This PR makes LazyCDProof robust to this case; nullptr is interpreted as the fact is an assumption.
2020-09-30(proof-new) Add the term conversion sequence generator (#5097)Andrew Reynolds
This class will be used in the theory preprocessor and is planned to be used in other preprocessing passes that can be understood as sequences of rewrite systems.
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
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.
2020-09-17[proof-new] Have mkScope agnostic to True assumptions (#5086)Haniel Barbosa
2020-09-16[proof-new] Adds Lazy CDProof chain data-structure (#5060)Haniel Barbosa
A proof generator to facilitate connection of locally independent but globally dependent proofs. In particular this will be used to model the resolution chains done in Minisat.
2020-09-11(proof-new) Handle mismatched assumptions in proof equality engine during ↵Andrew Reynolds
mkScope (#5012) This modifies the fix for Boolean equalities with constants so that is addressed lazily during ProofNodeManager mkScope instead of when asserting assumptions to the proof equality engine. This ensures that the default method for asserting facts to the equality engine for external assertions does not have any special cases. A previously abandoned solution to this issue had made this a part of CDProof. Instead, this PR modifies the mkScope method only. The fix makes mkScope robust to any assumption mismatches in mkScope that can be fixed by rewriting, not just Boolean equality with constants. It is intended to be used infrequently as a last resort when mkScope has mismatched assumptions. The handling of mismatches due to symmetry remains in this method.
2020-09-02(proof-new) Improve debugging infrastructure for open proofs (#4984)Andrew Reynolds
This includes more versions of checking whether a proof node is closed and standardizing output.
2020-06-23(proof-new) Updates to proof node manager (#4617)Andrew Reynolds
Main feature added is the mkScope interface, which is agnostic to symmetry of (dis)equalities. It also adds a check for cyclic proofs when using the interface ProofNodeManager::updateNode. Note that an earlier version of this method was agnostics to predicates vs Boolean equality with constants. This is no longer required.
2020-06-16Update copyright headers.Aina Niemetz
2020-06-05(proof-new) Updates to CDProof (#4565)Andrew Reynolds
This updates CDProof with several new functionalities, including making it agnostic to symmetry of (dis)equalites.
2020-04-16Add ProofNodeManager and ProofChecker (#4317)Andrew Reynolds
Further work on adding core utilities for ProofNode objects, in support of the new proof infrastructure. ProofNodeManager is analogous to NodeManager. It is a trusted way of generating only "well-formed" ProofNode pointers (according to a checker). ProofChecker is analogous to TypeChecker. It is intended to be infrastructure for our internal proof checker. This PR (and 1 more) is required to get to a place where Haniel and I can collaborate on further development for proofs.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback