summaryrefslogtreecommitdiff
path: root/src/proof
AgeCommit message (Expand)Author
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
2016-08-11Add support for fewer preprocessing holesAndres Notzli
2016-08-09Fix missing/redundant spaces in proofsfix_proof_spacesAndres Notzli
2016-08-05Minor: add/fix comments, remove redundant includesAndres Notzli
2016-08-03Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.Guy
2016-07-28The "aggressive" optimizer for lemma L now returns the conjunction of all lem...Guy
2016-07-28Bug fix involving negated lemmasGuy
2016-07-27Proper handling of IFF lemmas in the unsat core.Guy
2016-07-27Added an option for a more aggressive weakest implicant optimizationGuy
2016-07-27If we can't find a weaker implicant, fail gracefully and return the original ...Guy
2016-07-26Fix warnings in src/proofAndres Notzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback