summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2016-08-31Cleaning up the dead FORIT macros.Tim King
2016-08-31Removing the usage of typeof from theory_sets_private.Tim King
2016-08-31Beautifying theory_model.h.Tim King
2016-08-31Removing BOOST_FOREACH from theory/sets/scrutinize.h.Tim King
2016-08-31Removing typeof from sets normal form and beautifying the file.Tim King
2016-08-26Basic support for EPR+CBQI. Minor cleanup.ajreynol
2016-08-25Minor cleanup preprocessing, add ppNotifyAssertions.ajreynol
2016-08-25Options for counterexample guided instantiation.ajreynol
2016-08-16Initial infrastructure for ExtTheory, generalize extended term handling in Th...ajreynol
2016-08-15Enable bounded set membership with --fmf-bound. Map to term models for bounde...ajreynol
2016-08-12Minor fixes to model construction to take singleton equivalence classes into ...ajreynol
2016-08-11Minor change to strings, introduce proxy vars only when necessary.ajreynol
2016-08-10Improvements to strings: work on propagations for reverse normal form process...ajreynol
2016-08-09Fixes for sep star rewrite.ajreynol
2016-07-30Prioritize inferences when processing normal forms in strings.ajreynol
2016-07-28Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-07-28Bug fix involving negated lemmasGuy
2016-07-28Fix bug 749.ajreynol
2016-07-28Add the negative conjunction caseGuy
2016-07-27Proper instrumentation of the preprocessing phaseGuy
2016-07-27proper handling of ITEsGuy
2016-07-27Proper handling of IFF lemmas in the unsat core.Guy
2016-07-26Add option to minimize sygus solutions based on using weakest implicants of i...ajreynol
2016-07-26Minor improvements to strings related to constant splitting, including a few ...ajreynol
2016-07-25Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-07-24cleanupGuy
2016-07-24Proper handling for lemmas that are conjuncts:Guy
2016-07-22Minor, error handling for polymorphism + sep logic.ajreynol
2016-07-21Fixes for strings, explanations for constant split propagations, substr under...ajreynol
2016-07-20Infrastructure for storing and printing heap models for separation logic. Ens...ajreynol
2016-07-20Print only instantiations that are in the unsat core when --proof is enabled....ajreynol
2016-07-20Infer conflicts in strings based on abstracting equality as contains. Minor c...ajreynol
2016-07-19Add infrastructure for tracking instantiation lemmas (for proofs, and minimiz...ajreynol
2016-07-16Refactor strings extf evaluation info. Ensure strings eager preprocess elimin...ajreynol
2016-07-15The ProofManager now allows theory solvers to get their lemmas that participa...Guy
2016-07-15Minor simplification to normal form explanations.ajreynol
2016-07-08Minor fix to last commit.ajreynol
2016-07-07Simplifications for strings normal forms, fix case for concat reps in normal ...ajreynol
2016-07-07Ensure heap disjointness in sep refinements.ajreynol
2016-07-07Refactoring of strings preprocess module. When enabled, apply eager preproces...ajreynol
2016-07-06A few proof bugs fixedGuy
2016-07-06Minor cleanup in strings, mostly related to negated str.contains.ajreynol
2016-07-06Add comment field for model, resolves hack for printing sep logic models.ajreynol
2016-07-05Refactor last call for theories, only create one model when quantifiers are e...ajreynol
2016-07-05Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ...ajreynol
2016-06-20Minor change to sep/kindsajreynol
2016-06-20Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-20Fixed a bug where the proofManager's init() call was not getting called, resu...Guy
2016-06-18Fix unit test.ajreynol
2016-06-17Cleanup from last commit, treat sep.nil as variable kind.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback