summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-02-21add new theory (sets)Kshitij Bansal
Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment
2014-02-21fix a -WunusedKshitij Bansal
2014-02-20fix makefileTianyi Liang
2014-02-20add more tests, and define int.to.str(NEGATIVE)=""Tianyi Liang
2014-02-20add two cases to the regression testTianyi Liang
2014-02-20Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
Conflicts: src/theory/strings/theory_strings_preprocess.cpp
2014-02-20hot fix for str2int/int2strTianyi Liang
2014-02-20add negative int2strTianyi Liang
2014-02-20String parsing example in CVC parserMorgan Deters
2014-02-20Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
Conflicts: src/theory/strings/theory_strings_preprocess.cpp
2014-02-20hot fix for str2int/int2strTianyi Liang
2014-02-20add negative int2strTianyi Liang
2014-02-20String parsing example in CVC parserMorgan Deters
2014-02-20Fix ite and iff handling in QCF. Add option for heuristic instantiation in ↵Andrew Reynolds
QCF (not working yet). Improve automatic option setting for quantifiers.
2014-02-20portfolio: add stat to track time spent waiting for interrupted threads to stopKshitij Bansal
2014-02-19Merge branch 'master' of github.com:CVC4/CVC4Tim King
2014-02-19Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-02-19Merge branch '1.3.x'Tim King
2014-02-19Stopping non-linear terms from entering the dio solver. Fixes bug 547.Tim King
2014-02-19add negative int2strTianyi Liang
2014-02-18String parsing example in CVC parserMorgan Deters
2014-02-18missed files for the latter commitTianyi Liang
2014-02-18str.to.int(INVALID) = -1Tianyi Liang
2014-02-18switch to total function str.to.int: maps invalid and non-digit strings to 0Tianyi Liang
2014-02-17bring back the commits which is lost accidentally.Tianyi Liang
2014-02-17add str2intTianyi Liang
2014-02-17Fix for strings-exp: enable quantifiersMorgan Deters
2014-02-17Fix strings preprocessing for justification heuristicMorgan Deters
2014-02-17Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-02-17type conversionTianyi Liang
2014-02-17type conversionTianyi Liang
2014-02-14Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add ↵Andrew Reynolds
support for ITE terms. Add full-delay inst-when mode. Make strings come before quantifiers in check. Minor cleanup.
2014-02-14partial function charatTianyi Liang
2014-02-13fix expanding defTianyi Liang
2014-02-12bug fix for reverse checkTianyi Liang
2014-02-11lexer fix: disable smt-lib conversion for string literalsTianyi Liang
2014-02-11minor fix for recognizing the tail backslash, still have smt-lib compliance ↵Tianyi Liang
issue.
2014-02-11resolve merge conflictsTianyi Liang
2014-02-11Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
Conflicts: src/theory/strings/theory_strings.cpp
2014-02-11escaped characters, having an issue with smt-lib defintion, further repair ↵Tianyi Liang
is needed.
2014-02-11minor fix for mergeTianyi Liang
2014-02-11minor cleanup for mergeTianyi Liang
2014-02-11minor fix for mergeTianyi Liang
2014-02-11escaped characters, having an issue with smt-lib defintion, further repair ↵Tianyi Liang
is needed.
2014-02-10Fix build (some nonexistent files listed in Makefile)Morgan Deters
2014-02-09More complete guess instantiation strategy, cvc4 now typically times out ↵Andrew Reynolds
instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
2014-02-06Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-02-06minor cleanup for mergeTianyi Liang
2014-02-06minor fix for mergeTianyi Liang
2014-02-06minor cleanup for mergeTianyi Liang
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback