summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2014-04-09some debugging changesKshitij Bansal
2014-04-06Merge branch 'master' of https://github.com/CVC4/CVC4Kshitij Bansal
2014-04-06Merge pull request #21 from pcc/ite-fixTim King
2014-04-06fix for hiding prompt/header in shell, error-behavior options as in SMTLIBKshitij Bansal
2014-04-04For security, add --no-filesystem-access option, which disables SMT-LIB scrip...Morgan Deters
2014-04-04Allow turning off the interactive prompt while in interactive mode.Morgan Deters
2014-04-03Properly quote symbols in SMT-LIB printer.Morgan Deters
2014-04-03Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiann...Morgan Deters
2014-04-01Merge branch '1.3.x'Tim King
2014-04-01Fixing bug 552. There was a bug when integers are made using a string with a...1.3.xTim King
2014-04-01windows build fix for UINT32_MAXTianyi Liang
2014-03-31add str to u16/u32, and u16/u32 to strTianyi Liang
2014-03-28rm old unused codeKshitij Bansal
2014-03-28add construles, type_rules rm redundant, kinds cleanupKshitij Bansal
2014-03-28minor printer fix; intersection fixTianyi Liang
2014-03-27Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-03-27adds new feature: re.loopTianyi Liang
2014-03-27adds intersectionTianyi Liang
2014-03-27deriv symbolic regexpTianyi Liang
2014-03-27adds intersectionTianyi Liang
2014-03-27adds new feature: re.loopTianyi Liang
2014-03-26Merge branch '1.3.x'Morgan Deters
2014-03-26Win32 build script fixes (to allow portfolio builds).Morgan Deters
2014-03-26Fix an off-the-end string pointer bug (showed up only in some Win32 builds).Morgan Deters
2014-03-26deriv symbolic regexpTianyi Liang
2014-03-26adds intersectionTianyi Liang
2014-03-26Merging in a fix from 1.3.x.Tim King
2014-03-26Fixes an idempotency issue for non-linear multiplication with integer and rea...Tim King
2014-03-20Merge pull request #22 from kbansal/sets-modelKshitij Bansal
2014-03-20cleanupKshitij Bansal
2014-03-20fix for sets/mar2014/..317minimized..Kshitij Bansal
2014-03-20Fix for registration issues of term appearing in a shared lemmaKshitij Bansal
2014-03-20rewriter fix, weaken an assertionKshitij Bansal
2014-03-20constant normal form and rewriteKshitij Bansal
2014-03-20fix a sharing issues with setsKshitij Bansal
2014-03-20push subtyping for sets to the element typeKshitij Bansal
2014-03-20work on set modelKshitij Bansal
2014-03-20Minor fix for CBQI, ignore inst constant nodes.Andrew Reynolds
2014-03-19Fix documentation for Theory::preRegisterTerm().Morgan Deters
2014-03-19Refactor the theory specific parts of definition expansion into the theory so...Martin Brain
2014-03-19Set dumping options from (set-option..) and API more directly.Morgan Deters
2014-03-19Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting.Morgan Deters
2014-03-19Move the translator binary from src/main to examples, no longer built by defa...Morgan Deters
2014-03-19Appease compilers from latest XCode release (v5.1).Morgan Deters
2014-03-19Minor usability fixes related to SMT-LIB compliance.Morgan Deters
2014-03-17hot fix for pre-reg term caching in stringsTianyi Liang
2014-03-16Fix for ite of >=64bit wide bitvectors with unconstrained condition.Peter Collingbourne
2014-03-14SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff). Tha...Morgan Deters
2014-03-14Add ability to provide theory-specific proof rules to EqualityEngine, extends...Andrew Reynolds
2014-03-12Work on array pf signature, add working example. Add quantifiers proof signa...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback