summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-11-07Adds the header file into makefile, solving building error; adds cache for ↵Tianyi Liang
derivative; disables loop detection when finite model finding is enabled.
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-05fixed proof regression script and added a new uf test caselianah
2013-11-04Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-10-28Turn off model-based arrays (causing crashes in portfolio)Clark Barrett
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-09cleaned up proof codelianah
2013-10-09fixed uf proof bug: now storing deleted theory lemmaslianah
2013-10-09More improvements to datatypes, eager selector collapsing, improved collect ↵Andrew Reynolds
model info. Also fix bug in model post-processor.
2013-10-08added currying for uf proofs; still needs debugginglianah
2013-10-08fixed uf proof with holes bugslianah
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-07first draft implementation of uf proofs with holesLiana 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-10-01Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback