summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2017-03-22Minor fix for bounded integers.ajreynol
2017-03-22Work on new approach for sygus involving conditional solutions. Refactoring o...ajreynol
2017-03-10Minor fix for cbqi-all.ajreynol
2017-03-07More fixes for printing/parsing sets, fix kind name.ajreynol
2017-03-06Support for set compliment and universe set. Simplify approach for sep.nil no...ajreynol
2017-03-02Fixes related to sets.ajreynol
2017-03-02Minor cleanup and reorganization related to last commit.ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2017-02-16Minor fixes for relations, quantifiers dsplit.ajreynol
2017-02-15Minimization modes for fmf bound.ajreynol
2017-02-07Generalize finite bound inference to unifiable variables in set membership li...ajreynol
2017-01-11Fix for when variables are (partially) bound in multiple ways, add regression...ajreynol
2016-12-07Add sets regression, fixes bug 754. Minor fix to regexp in strings.ajreynol
2016-12-07Refactoring, generalization of bounded inference module. Simplification of re...ajreynol
2016-12-06Improve bounds for global heap in sep, refactor preprocessing. Minor improvem...ajreynol
2016-12-02Bug fixes and refactoring of parametric datatypes, add some regressions.ajreynol
2016-12-02Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --...ajreynol
2016-12-01Fix quantifiers dynamic splitting module for incremental mode, fixes bug 765 ...ajreynol
2016-12-01Improvement and bug fix for str.indexof reduction, add regression. Other mino...ajreynol
2016-11-11Add simple inferences for extended bitvector functions, add a few related opt...ajreynol
2016-11-08Add a few options to separation logic and sets. Minor changes to separation l...ajreynol
2016-11-04Fix a few more minor memory leaks.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-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-09-29Address some coverity warnings, add another stat.ajreynol
2016-09-29Minor cleanup and additions to quantifiers statistics.ajreynol
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-25Disambiguating a vector insert warning coming from coverity scan.Tim King
2016-09-25Removing an unused iterator.Tim King
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-16Use matching heuristics for EPR instantiation.ajreynol
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-14Lemma cache in theory sep. Minor optimization for sets. Minor improvements to...ajreynol
2016-09-13Minor changes to sep logic, epr, quantifier splitting.ajreynol
2016-09-12Refactor prenex modes.ajreynol
2016-09-12Remove old implementation of cbqiajreynol
2016-09-03Miniscope top level conjunctions for prenex normal form, allow one level mini...ajreynol
2016-09-03Option for prenex normal formajreynol
2016-09-01Fix boolean term issue in invariants from sygus. Minor default options change...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback