summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-04-29Fix for --force-logic to extend its reach to the parser.Morgan Deters
2014-04-29fixed couple of more warningsKshitij Bansal
2014-04-29fix was compiler warning in antlr_input, crashing test case with the old fixKshitij Bansal
2014-04-29Revert a compiler warning fix from ea6a5a6.Morgan Deters
2014-04-29fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlrTianyi Liang
2014-04-29add leading zeros support for str.to.intTianyi Liang
2014-04-29Significantly improve performance for producing datatypes models.ajreynol
2014-04-28Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-28Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-04-28add strings-opt2 for regular splittingTianyi Liang
2014-04-28cleanupKshitij Bansal
2014-04-28minor change with kshitij's changeTianyi Liang
2014-04-28nodemanager robust skolem numberingKshitij Bansal
2014-04-28add strings-opt2 for regular splittingTianyi Liang
2014-04-28Merge pull request #25 from kbansal/setsKshitij Bansal
2014-04-28Preparation for models for co-inductive datatypes. Minor cleanup.Andrew Reynolds
2014-04-28Optimizations for datatypes: check for clashes modulo equality. Avoid buildi...ajreynol
2014-04-28minor fixKshitij Bansal
2014-04-28Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-28travis, please!Kshitij Bansal
2014-04-27attempt to improve CVC4's "parse error" messageKshitij Bansal
2014-04-27rm undocument/non-working* "feature"Kshitij Bansal
2014-04-24minor change: add a heuristic for preventing constant splitting.Tianyi Liang
2014-04-24optimizationKshitij Bansal
2014-04-24Avoid assigning constructor terms to 1-constructor datatype eqcs, when possib...ajreynol
2014-04-24Compute care graph for datatypes. Preliminary results show 20x speed up on l...Andrew Reynolds
2014-04-24Add --inst-max-level=N option for Kshitij. Support define-const command in S...Andrew Reynolds
2014-04-22Minor fix to avoid rewriting datatype equalities into non-equalitiers, as req...Andrew Reynolds
2014-04-19Eh, what?Kshitij Bansal
2014-04-19fix warnings in strings/Kshitij Bansal
2014-04-17Allow fmf-bound-int to be set with set-option and via API.Morgan Deters
2014-04-17simplify mkSkolem naming system: don't use $$Kshitij Bansal
2014-04-17use internal skolem numberingKshitij Bansal
2014-04-17Minor refactoring and optimizing.Andrew Reynolds
2014-04-14Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ...Andrew Reynolds
2014-04-14Add initial support for co-datatypes.Andrew Reynolds
2014-04-11Better support for building with mingw64; thanks to Nicolas Roche @ Altran fo...Morgan Deters
2014-04-10setType -> setOfType, resolves bug 556Morgan Deters
2014-04-10Fix the build; --check-proof works for UF but not for the new UFC logic.Morgan Deters
2014-04-10Expand definitions in theory datatypes, now has the expected semantics for in...Andrew Reynolds
2014-04-10Boolean terms conversion fix for datatypes, fixes a problem Andy discovered o...Morgan Deters
2014-04-10Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-04-10minor fix for stringsTianyi Liang
2014-04-10minor fix for stringsTianyi Liang
2014-04-10Add support for cardinality constraints logic UFC. Add regressions in fmf/. ...Andrew Reynolds
2014-04-10refactor .travis.ymlKshitij Bansal
2014-04-09Merge pull request #24 from kbansal/sets-modelKshitij Bansal
2014-04-09Minor change to better support parameterized partial/total kinds (for upcomin...Morgan Deters
2014-04-09Revert E-matching datatypes fix.Andrew Reynolds
2014-04-09Handle fmf.card as input from user, add support in SMT2 parser, as requested ...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback