Age | Commit message (Expand) | Author |
2016-07-28 | The "aggressive" optimizer for lemma L now returns the conjunction of all lem... | Guy |
2016-07-28 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-07-28 | Bug fix involving negated lemmas | Guy |
2016-07-28 | Fix bug 749. | ajreynol |
2016-07-28 | Add the negative conjunction case | Guy |
2016-07-27 | Proper instrumentation of the preprocessing phase | Guy |
2016-07-27 | proper handling of ITEs | Guy |
2016-07-27 | Proper handling of IFF lemmas in the unsat core. | Guy |
2016-07-27 | Added an option for a more aggressive weakest implicant optimization | Guy |
2016-07-27 | If we can't find a weaker implicant, fail gracefully and return the original ... | Guy |
2016-07-26 | Fix warnings in src/proof | Andres Notzli |
2016-07-26 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-07-26 | Bug fix: | Guy |
2016-07-26 | Add option to minimize sygus solutions based on using weakest implicants of i... | ajreynol |
2016-07-26 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-07-26 | Letification of BV constants | Guy |
2016-07-26 | Minor improvements to strings related to constant splitting, including a few ... | ajreynol |
2016-07-26 | Added functionality to retrieve a lemma's "weakest implicant" in the unsat co... | Guy |
2016-07-25 | Bug fix | Guy |
2016-07-25 | Propagate the usage of proof let maps into constant disequality proofs | Guy |
2016-07-25 | Bug fix | Guy |
2016-07-25 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-07-24 | cleanup | Guy |
2016-07-24 | Use letification for the aliasing declarations as well (consequently, print t... | Guy |
2016-07-24 | Proper handling for lemmas that are conjuncts: | Guy |
2016-07-22 | Minor, error handling for polymorphism + sep logic. | ajreynol |
2016-07-21 | Fixes for strings, explanations for constant split propagations, substr under... | ajreynol |
2016-07-20 | Infrastructure for storing and printing heap models for separation logic. Ens... | ajreynol |
2016-07-20 | Print only instantiations that are in the unsat core when --proof is enabled.... | ajreynol |
2016-07-20 | Infer conflicts in strings based on abstracting equality as contains. Minor c... | ajreynol |
2016-07-19 | Bug fix | Guy |
2016-07-19 | Allow a caller to query whether an unsat core is available or not | Guy |
2016-07-19 | Add infrastructure for tracking instantiation lemmas (for proofs, and minimiz... | ajreynol |
2016-07-16 | Refactor strings extf evaluation info. Ensure strings eager preprocess elimin... | ajreynol |
2016-07-15 | Moved the assertion to a better spot | Guy |
2016-07-15 | The ProofManager now allows theory solvers to get their lemmas that participa... | Guy |
2016-07-15 | Minor simplification to normal form explanations. | ajreynol |
2016-07-08 | Minor fix to last commit. | ajreynol |
2016-07-07 | Simplifications for strings normal forms, fix case for concat reps in normal ... | ajreynol |
2016-07-07 | Ensure heap disjointness in sep refinements. | ajreynol |
2016-07-07 | Refactoring of strings preprocess module. When enabled, apply eager preproces... | ajreynol |
2016-07-06 | A few proof bugs fixed | Guy |
2016-07-06 | Minor cleanup in strings, mostly related to negated str.contains. | ajreynol |
2016-07-06 | Add comment field for model, resolves hack for printing sep logic models. | ajreynol |
2016-07-05 | Refactor last call for theories, only create one model when quantifiers are e... | ajreynol |
2016-07-05 | Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ... | ajreynol |
2016-07-01 | When proving a lemma, ignore literals that don't belong to the theory in ques... | Guy |
2016-07-01 | Handle bitvector lemmas where a literal gets rewritten into false, and conseq... | Guy |
2016-06-30 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-06-30 | Support for the letification of chained AND and OR operations in LFSC proofs | Guy |