summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2016-07-25Bug fixGuy
2016-07-25Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-07-24cleanupGuy
2016-07-24Use letification for the aliasing declarations as well (consequently, print t...Guy
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-19Bug fixGuy
2016-07-19Allow a caller to query whether an unsat core is available or notGuy
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-15Moved the assertion to a better spotGuy
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-07-01When proving a lemma, ignore literals that don't belong to the theory in ques...Guy
2016-07-01Handle bitvector lemmas where a literal gets rewritten into false, and conseq...Guy
2016-06-30Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-30Support for the letification of chained AND and OR operations in LFSC proofsGuy
2016-06-23Add theory/sep/kinds to EXTRA_DIST to fix distcheck failures.Clark Barrett
2016-06-23Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,Clark Barrett
2016-06-20Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-20Addressed a bug that occurs when proof production is triggered via text flags...Guy
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
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-08Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-08LFSC letification is true by defaultGuy
2016-06-08Support for printing a global let map in LFSC proofs.Guy
2016-06-06Merge pull request #85 from CVC4/master_for_proof_mergeguykatzz
2016-06-03Remove NodeListMap from datatypes and equality inference. Add option --dt-bla...ajreynol
2016-06-03Better infrastructure for proving constant disequality.Guy
2016-06-03A better mechanism for handling BV terms with aliases: inject the alias at th...Guy
2016-06-03Remove NodeListMap from strings, fixes memory leaks. Fix for regexp intersect...ajreynol
2016-06-03Simple memory fixes, minor cleanup in quantifiers.ajreynol
2016-06-03Reduce number of passes in quantifiers rewriter.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback