summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2016-11-08Minor fixes related to ExtTheory + incremental, fixes bug760.ajreynol
2016-11-08Add a few options to separation logic and sets. Minor changes to separation l...ajreynol
2016-11-07Fixing a memory leak in the eager bitblaster.Tim King
2016-11-04Fix a few more minor memory leaks.ajreynol
2016-11-03Make data points accurate in sep logic models.ajreynol
2016-11-03Add priorities to getNextDecision. Properly handle case for finite types + un...ajreynol
2016-11-02Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ...ajreynol
2016-11-02Fix a few obvious memory leaks in sygus and quantifiers. Minor fix cvc3_compat.ajreynol
2016-11-01Fix memory leak in TheorySetsRels. Minor cleanup.ajreynol
2016-11-01Working memory leak free version, changes interface to pointers.ajreynol
2016-10-31Minor refactoring in preparation for datatypes node cycle breaking.ajreynol
2016-10-28Add get instantiations utilities to API.ajreynol
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver as...ajreynol
2016-10-19Fix minor bug and typo in boolean rewriterfix_rewriteAndres Notzli
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.ajreynol
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
2016-10-11- fixed a memory leak issue with context dependent data structurePaul Meng
2016-10-08Adding initializers for structs internal to ite_utilities.Tim King
2016-10-02Removing the throw specifiers from theory_uf_type_rules.h.Tim King
2016-10-02Removing the throw specifiers from theory_fp_type_rules.h.Tim King
2016-10-02Removing the throw specifiers from theory_datatypes_type_rules.h.Tim King
2016-10-02Removing an unused member from TreeLog.Tim King
2016-10-02Removing the throw specifiers from theory_bv_type_rules.h.Tim King
2016-10-01Incorporate non-bv parts of ajr/bvExt branchajreynol
2016-09-29Address some coverity warnings, add another stat.ajreynol
2016-09-29Minor cleanup and additions to quantifiers statistics.ajreynol
2016-09-28Fix the merge of kbansal/card branch (2039eab).Kshitij Bansal
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-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-25Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here.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-23fixed a few bugsPaul Meng
2016-09-21Remove duplicate code from my last commitajreynol
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-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-16More refactoring of cbqi, start developing new interface.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback