Age | Commit message (Expand) | Author |
2016-08-31 | Removing BOOST_FOREACH from theory/sets/scrutinize.h. | Tim King |
2016-08-31 | Removing typeof from sets normal form and beautifying the file. | Tim King |
2016-08-26 | Basic support for EPR+CBQI. Minor cleanup. | ajreynol |
2016-08-25 | Minor cleanup preprocessing, add ppNotifyAssertions. | ajreynol |
2016-08-25 | Options for counterexample guided instantiation. | ajreynol |
2016-08-16 | Initial infrastructure for ExtTheory, generalize extended term handling in Th... | ajreynol |
2016-08-15 | Enable bounded set membership with --fmf-bound. Map to term models for bounde... | ajreynol |
2016-08-12 | Minor fixes to model construction to take singleton equivalence classes into ... | ajreynol |
2016-08-11 | Minor change to strings, introduce proxy vars only when necessary. | ajreynol |
2016-08-10 | Improvements to strings: work on propagations for reverse normal form process... | ajreynol |
2016-08-09 | Fixes for sep star rewrite. | ajreynol |
2016-07-30 | Prioritize inferences when processing normal forms in strings. | ajreynol |
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-26 | Add option to minimize sygus solutions based on using weakest implicants of i... | ajreynol |
2016-07-26 | Minor improvements to strings related to constant splitting, including a few ... | ajreynol |
2016-07-25 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-07-24 | cleanup | 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 | 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 | 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-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-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 |