summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2013-11-06Bug fixes for bounded integer quantification. Current best strategy is to ↵Andrew Reynolds
turn off MBQI. Disable relevant triggers by default.
2013-11-06bug fixTianyi Liang
2013-11-06change optionsTianyi Liang
2013-11-06add seperate regular expression filesTianyi Liang
2013-11-04Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-10-24Fix for bug515Clark Barrett
2013-10-23add back eager approachTianyi Liang
2013-10-23bug fix for loop ruleTianyi Liang
2013-10-23bug fixTianyi Liang
2013-10-22bug fixes: some issues remain, need more discussion laterTianyi Liang
2013-10-21remove nested re or; opt loopTianyi Liang
2013-10-21string fixTianyi Liang
2013-10-21bug fix for string special caseTianyi Liang
2013-10-20adds regular expression rangeTianyi Liang
2013-10-16adds fmf for stringsTianyi Liang
2013-10-16renames for strings fmfTianyi Liang
2013-10-15bug fix in strings : change from assert to alwaysassertTianyi Liang
2013-10-15removes some junksTianyi Liang
2013-10-15performance optimizations for quantifier instantiationAndrew Reynolds
2013-10-15bug fix: string cache cleaningTianyi Liang
2013-10-14Adds Regular Expression support.Tianyi Liang
2013-10-11Adds regular expression support, it is actually CFL because of variables.Tianyi Liang
2013-10-11add constant membershipTianyi Liang
2013-10-11adds native regexp.Tianyi Liang
2013-10-10Minor bug fix to datatypes.Andrew Reynolds
2013-10-09fixed options::proof() segfaultlianah
2013-10-09More improvements to datatypes, eager selector collapsing, improved collect ↵Andrew Reynolds
model info. Also fix bug in model post-processor.
2013-10-08Optimizations for datatypes theory. There seems to be a bug in ↵Andrew Reynolds
trans_closure, currently implemented a work around.
2013-10-07fixed some bugsLiana Hadarean
2013-10-07merged goldenLiana Hadarean
2013-10-07Multiple fixes for datatypes theory solver: add support for parametric ↵Andrew Reynolds
datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.
2013-10-03Added support for converting unsorted problems to multi-sorted problems via ↵Andrew Reynolds
sort inference and monotonicity. Minor cleanup.
2013-10-03adds some fixes. it solves kaluza problemsTianyi Liang
2013-10-01adds partial function substr. the use of this function should be guarded, ↵Tianyi Liang
especially for disequalities
2013-09-30replace with a new method for disequality, move to QF_STianyi Liang
2013-09-30add x=yTianyi Liang
2013-09-30fixed a loop bugTianyi Liang
2013-09-30merged goldenLiana Hadarean
2013-09-30Bug fixes and improvements for symmetry breaking, it now supports multiple ↵Andrew Reynolds
sorts. Working on monotonicity inference.
2013-09-27Some fixes to recent strings commits.Morgan Deters
2013-09-27Merge branch 'master' of github.com:tiliang/CVC4Morgan Deters
2013-09-27adds communication with arith engineTianyi Liang
2013-09-27Add new symmetry breaking technique for finite model finding. Improvements ↵Andrew Reynolds
to bounded integer quantifier instantiation.
2013-09-27removes unsound cases, adds unrollingTianyi Liang
2013-09-27fix the infinite issueTianyi Liang
2013-09-27for morgan to see the regression problemsTianyi Liang
2013-09-27fix loop detection for multi-varsTianyi Liang
2013-09-27optimizing model generation for stringsTianyi Liang
2013-09-27adds model generation for strings, and a hacked way in arith engine for modelsTianyi Liang
2013-09-24Reduce compiler dependencies on substitutions.h,Clark Barrett
Some new functionality in substitutions.h/cpp
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback