summaryrefslogtreecommitdiff
path: root/src/proof
AgeCommit message (Expand)Author
2018-12-17New C++ API: Add tests for term object. (#2755)Aina Niemetz
2018-12-14 [LRA Proof] Storage for LRA proofs (#2747)Alex Ozdemir
2018-12-06Enable BV proofs when using an eager bitblaster (#2733)Alex Ozdemir
2018-12-06Fix use-after-free due to destruction order (#2739)Andres Noetzli
2018-12-03Bit vector proof superclass (#2599)Alex Ozdemir
2018-11-19Change lemma proof step storage & iterators (#2712)Alex Ozdemir
2018-09-25carefully printing trusted assertions in proofs (#2505)yoni206
2018-09-22cmake: Remove unused CMakeLists.txtMathias Preiner
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-27Resolution proof: separate printing from proof (#1964)Andres Noetzli
2018-08-17Remove support for flipDecision (#2319)Andrew Reynolds
2018-07-13Properly clean up assertion stack in CnfProof (#2147)Andres Noetzli
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-23Remove ProofProxy (#1965)Andres Noetzli
2018-05-03Fix warnings in proof code (#1850)Andres Noetzli
2018-04-25Refactor array-proofs and uf-proofs (#1655)yoni206
2018-04-02Reorganize bitblaster code. (#1695)Mathias Preiner
2018-03-06Make statistics output consistent. (#1647)Mathias Preiner
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
2018-02-09Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589)Aina Niemetz
2018-02-09Replacing an incorrect reference to an injected class name when the type was ...Tim King
2017-11-15Initializes BitVectorProof::d_isAssumptionConflict. Resolves CID 1362898. (#1...Tim King
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-10-25Removing throw specifiers from OutputChannel and subclasses. (#1209)Tim King
2017-10-25Switching EqProof to use shared_ptr everywhere. (#1217)Tim King
2017-10-11Cleaning up ProofArray class. (#1208)Tim King
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
2017-09-19Fix issue #1074, improve non-fatal error handling (#1075)Andres Noetzli
2017-08-21Change Bugzilla urls to Github issues.Mathias Preiner
2017-08-09Fix compiler warning in sat_proof_implementationAndres Noetzli
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-07Update copyright headers.Mathias Preiner
2017-06-30Fix use-after-free with unsat cores/proofs (#174)Andres Nötzli
2017-06-16Fix segfault by making unit conflict CDMaybeAndres Nötzli
2017-05-31A more informative error message when a theory is not yet supported by the pr...guykatzz
2017-05-26Fix use-after-free with ResChainsAndres Noetzli
2017-05-04skolemization manager may be called also when just unsatCores are on (related...guykatzz
2017-03-23support incremental unsat coresguykatzz
2017-03-17better support for proof production when encountering bool terms: handle the ...guykatzz
2017-03-14fix uninitialized variableAndres Notzli
2017-03-09bug fixguykatzz
2017-03-09better proof support for bools and formulasguykatzz
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2016-11-18Removing some throw specifiers from OutputChannel. Fixes bug 716.Tim King
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
2016-10-05Added an option that allow empty dependencies when attempting to minimize pre...guykatzz
2016-09-27Removing an unused iterator.Tim King
2016-09-16Let arith_proof print its own termsGuy
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback