Age | Commit message (Expand) | Author |
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 |
2016-06-23 | Add theory/sep/kinds to EXTRA_DIST to fix distcheck failures. | Clark Barrett |
2016-06-23 | Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black, | Clark Barrett |
2016-06-20 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-06-20 | Addressed a bug that occurs when proof production is triggered via text flags... | Guy |
2016-06-20 | Minor change to sep/kinds | ajreynol |
2016-06-20 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-06-20 | Fixed a bug where the proofManager's init() call was not getting called, resu... | Guy |
2016-06-18 | Fix unit test. | ajreynol |
2016-06-17 | Cleanup from last commit, treat sep.nil as variable kind. | ajreynol |
2016-06-17 | Support for separation logic. Enable cbqi by default for pure BV. | ajreynol |
2016-06-17 | Add syguscomp2016 scripts. | ajreynol |
2016-06-09 | Dummy commit. | Clark Barrett |
2016-06-08 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-06-08 | LFSC letification is true by default | Guy |
2016-06-08 | Support for printing a global let map in LFSC proofs. | Guy |
2016-06-06 | Merge pull request #85 from CVC4/master_for_proof_merge | guykatzz |
2016-06-03 | Remove NodeListMap from datatypes and equality inference. Add option --dt-bla... | ajreynol |
2016-06-03 | Better infrastructure for proving constant disequality. | Guy |
2016-06-03 | A better mechanism for handling BV terms with aliases: inject the alias at th... | Guy |
2016-06-03 | Remove NodeListMap from strings, fixes memory leaks. Fix for regexp intersect... | ajreynol |
2016-06-03 | Simple memory fixes, minor cleanup in quantifiers. | ajreynol |
2016-06-03 | Reduce number of passes in quantifiers rewriter. | ajreynol |
2016-06-02 | Fixed a magical bug that only appears when compiling with clang: | Guy |
2016-06-02 | Fix | Guy |
2016-06-01 | Merge from proof branch | Guy |