cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2021-04-15	Rename occurrences of CVC4 to CVC5. (#6351)	Aina Niemetz
	This renames everything but GitHub links and build system related macros. Switching the build system to cvc5 will be the last step in the renaming process.
2021-04-14	Rename public and private headers in src/include. (#6352)	Aina Niemetz

2021-04-12	Refactor and update copyright headers. (#6316)	Aina Niemetz

2021-04-09	Rename CVC4__ header guards to CVC5__. (#6326)	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-01	Rename namespace CVC5 to cvc5. (#6258)	Aina Niemetz

2021-03-31	Rename namespace CVC4 to CVC5. (#6249)	Aina Niemetz

2021-03-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2021-01-19	Implement proofs for arith BRAB lemmas (#5784)	Alex Ozdemir
	All changes: Add a Pf type alias for std::shared_ptr to expr/proof_rule.h Add an eager proof generator to TheoryArith for preprocessing rewrites. Right now those are proven with INT_TRUST. Will eventually fix. Generate proved lemmas in TheoryArithPrivate::branchIntegerVariable. Same for TheoryArithPrivate::roundRobinBranch Add EagerProofGenerator::mkTrustedRewrite. Add some proofsEnabled methods.
2020-12-02	Update copyright headers.	Aina Niemetz

2020-09-28	[proof-new] Adds a proof node hash function (#5154)	Haniel Barbosa

2020-09-22	Update 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-07-30	(proof-new) Stream output for ProofNode (#4789)	Andrew Reynolds

2020-06-16	Update copyright headers.	Aina Niemetz

2020-06-15	(proof-new) Update proof node, add proof node algorithm utility file. (#4600)	Andrew Reynolds
	Moves get free assumptions to a proof_node_algorithm.h/cpp file, analogous to node_algorithm.h/cpp. Adds a more general form of it, getFreeAssumptionsMap, which is required for future method ProofNodeManager::mkScope.
2020-04-20	Add SCOPE proof rule (#4332)	Andrew Reynolds
	This rule is dual to ASSUME. It is a way of closing free assumptions to conclude an implication. It also changes getId -> getRule.
2020-04-16	Add 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.
2020-04-15	Add ProofNode data structure (#4311)	Andrew Reynolds
	This is the core data structure for proofs in the new proofs infrastructure. PfRule is a global enumeration of ids of proof nodes (analogous to Kind for Nodes).