Age | Commit message (Expand) | Author |
2016-09-09 | Support for separation logic + EPR. Refactor preprocessing of sep.nil, only a... | ajreynol |
2016-09-08 | Refactor seplog preprocess. Handle case where sep data type cannot be inferred. | ajreynol |
2016-09-03 | Miniscope top level conjunctions for prenex normal form, allow one level mini... | ajreynol |
2016-09-03 | Option for prenex normal form | ajreynol |
2016-09-01 | Merge pull request #91 from timothy-king/no-throw | Tim King |
2016-09-01 | Fix boolean term issue in invariants from sygus. Minor default options change... | ajreynol |
2016-09-01 | Cleanup quantifier elimination in smt engine. | ajreynol |
2016-09-01 | Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifier... | ajreynol |
2016-09-01 | Relaxing the throw specifiers for the destructors for Node, TypeNode, the con... | Tim King |
2016-08-31 | Removing the forward declaration of QuantInfo from rewrite_engine.h. | Tim King |
2016-08-31 | Cleaning up the dead FORIT macros. | Tim King |
2016-08-31 | Removing the usage of typeof from theory_sets_private. | Tim King |
2016-08-31 | Beautifying theory_model.h. | Tim King |
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 |