summaryrefslogtreecommitdiff
path: root/src/proof
AgeCommit message (Expand)Author
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
2016-07-26Bug fix:Guy
2016-07-26Letification of BV constantsGuy
2016-07-26Added functionality to retrieve a lemma's "weakest implicant" in the unsat co...Guy
2016-07-25Bug fixGuy
2016-07-25Propagate the usage of proof let maps into constant disequality proofsGuy
2016-07-25Bug fixGuy
2016-07-24Use letification for the aliasing declarations as well (consequently, print t...Guy
2016-07-19Bug fixGuy
2016-07-19Allow a caller to query whether an unsat core is available or notGuy
2016-07-15Moved the assertion to a better spotGuy
2016-07-15The ProofManager now allows theory solvers to get their lemmas that participa...Guy
2016-07-06A few proof bugs fixedGuy
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-07-01When proving a lemma, ignore literals that don't belong to the theory in ques...Guy
2016-07-01Handle bitvector lemmas where a literal gets rewritten into false, and conseq...Guy
2016-06-30Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-30Support for the letification of chained AND and OR operations in LFSC proofsGuy
2016-06-23Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,Clark Barrett
2016-06-20Addressed a bug that occurs when proof production is triggered via text flags...Guy
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback