summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2017-06-30Minor change to trigger selection, fixes related to subtypes (in macros, cbqi...ajreynol
2017-06-15Fix for issue related to cbqi + E-matching.ajreynol
2017-06-15Fix relevant domain for datatypes, fixes bug 824.ajreynol
2017-06-15Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cb...ajreynol
2017-06-01Minor optimizations related to cbqi.ajreynol
2017-05-20Fix bug 812.ajreynol
2017-05-15Fix bug 806. Minor fixes to remove term formula pass.ajreynol
2017-05-15Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.ajreynol
2017-05-15Make conflict-based instantiation abort if a ground conflict is found in the ...ajreynol
2017-04-28Do not eliminate non-standard arithmetic operators in recursive function defi...ajreynol
2017-04-24Fixes and simplifications for fmf mbqi.ajreynol
2017-04-21Handle subtypes in sets. Bug fixes for tuples with subtypes.ajreynol
2017-04-11Bug fix in conjecture generation for --quant-ind.ajreynol
2017-04-05Caching for fun def process, add regression.ajreynol
2017-04-04Enable multi-trigger-linear by default, add option.ajreynol
2017-04-04Simplify Theory::collectModelInfo interface to not take deprecated fullModel ...ajreynol
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge com...Tim King
2017-03-31Add option multi-trigger-linear, minor optimization to E-matching.ajreynol
2017-03-30Minor fixes for trigger selection max.ajreynol
2017-03-29Add quantifiers options related to model and master equality engine.ajreynol
2017-03-28Minor refactoring sygus.ajreynol
2017-03-28More work on sygus. Add regress4 to Makefile.ajreynol
2017-03-27Making ppNotifyAssertions take a const vector.Tim King
2017-03-24Add some regressions. Minor.ajreynol
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ...ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback