summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-09-27Removing an unused iterator.Tim King
2016-09-27Reverting part of the previous changes to unconstrained simplifier.Tim King
2016-09-26Simplifying control flow to avoid goto's in unconstrained_simplifier.cpp.Tim King
2016-09-25Adding missing break statements.Tim King
2016-09-25Closing an open file descriptor in MemoryMapFile.Tim King
2016-09-25Freeing memory in error handling code for bounded_token_buffer.Tim King
2016-09-25Deleting the eager bitblasting solver if present in TheoryBV.Tim King
2016-09-25Adding a destructor to QuantAntiSkolem.Tim King
2016-09-25Adding a destructor to TermDb.Tim King
2016-09-25Adding a destructor to CegqiOutputSingleInv.Tim King
2016-09-25Deleting optional members of StrongSolverTheoryUF.Tim King
2016-09-25Disambiguating a vector insert warning coming from coverity scan.Tim King
2016-09-25Deleting a temporary in theory sets enumerator.Tim King
2016-09-25Deleting the intermediate command singleton.Tim King
2016-09-25Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here.Tim King
2016-09-25Adding virtual destructors to several classes in expr.h .Tim King
2016-09-25Removing an unused iterator.Tim King
2016-09-25Fixing a potential use after free coming from a pop_back() call invalidating ...Tim King
2016-09-25Integrating a working coverity_scan travis rule back into master.Tim King
2016-09-23fixed a few bugsPaul Meng
2016-09-21Remove duplicate code from my last commitajreynol
2016-09-21Fixing an error in the previous travis commit.Tim King
2016-09-20Updating the travis file for coverity scan.Tim King
2016-09-20Refactor, separate theory-specific counterexample-guided instantiation.ajreynol
2016-09-20More refactoring of cbqi. Add a few regressions. Add option for qcf.ajreynol
2016-09-18Merge pull request #92 from timothy-king/travis-cpp11Tim King
2016-09-18Adding a clang format file for the project.Tim King
2016-09-18Adding a gnu++11 rule to travis.Tim King
2016-09-18Minor fix for stringsajreynol
2016-09-16In a ROW guard proof, if the transitivity proof does not have a disequality, ...guykatzz
2016-09-16Merge branch 'master' of https://github.com/CVC4/CVC4guykatzz
2016-09-16Use matching heuristics for EPR instantiation.ajreynol
2016-09-16Handling a corner case where a ROW's guard is a constant disequality.Guy
2016-09-16Let arith_proof print its own termsGuy
2016-09-16More refactoring of cbqi, start developing new interface.ajreynol
2016-09-15Further refactor cbqi.ajreynol
2016-09-15Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by defaul...ajreynol
2016-09-15Make sep pto a trigger kind, track in equality engines and term database.ajreynol
2016-09-15Refactor setIncomplete in quantifiers.ajreynol
2016-09-14Support for unique variable generation in node manager.ajreynol
2016-09-14Lemma cache in theory sep. Minor optimization for sets. Minor improvements to...ajreynol
2016-09-13fixed type checking and computing for PRODUCT and JOINPaul Meng
2016-09-13Minor changes to sep logic, epr, quantifier splitting.ajreynol
2016-09-13refactored the code, added more benchmarks and minor fixesPaul Meng
2016-09-12fixed capitalized "kind"Paul Meng
2016-09-12Refactor prenex modes.ajreynol
2016-09-12Remove old implementation of cbqiajreynol
2016-09-12Prefer non-cardinality constants in term models for sep logic.ajreynol
2016-09-12Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry b...ajreynol
2016-09-09Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback