Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-02-21 | add 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-21 | fix a -Wunused | Kshitij Bansal | |
2014-02-20 | fix makefile | Tianyi Liang | |
2014-02-20 | add more tests, and define int.to.str(NEGATIVE)="" | Tianyi Liang | |
2014-02-20 | add two cases to the regression test | Tianyi Liang | |
2014-02-20 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
Conflicts: src/theory/strings/theory_strings_preprocess.cpp | |||
2014-02-20 | hot fix for str2int/int2str | Tianyi Liang | |
2014-02-20 | add negative int2str | Tianyi Liang | |
2014-02-20 | String parsing example in CVC parser | Morgan Deters | |
2014-02-20 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
Conflicts: src/theory/strings/theory_strings_preprocess.cpp | |||
2014-02-20 | hot fix for str2int/int2str | Tianyi Liang | |
2014-02-20 | add negative int2str | Tianyi Liang | |
2014-02-20 | String parsing example in CVC parser | Morgan Deters | |
2014-02-20 | Fix 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-20 | portfolio: add stat to track time spent waiting for interrupted threads to stop | Kshitij Bansal | |
2014-02-19 | Merge branch 'master' of github.com:CVC4/CVC4 | Tim King | |
2014-02-19 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-02-19 | Merge branch '1.3.x' | Tim King | |
2014-02-19 | Stopping non-linear terms from entering the dio solver. Fixes bug 547. | Tim King | |
2014-02-19 | add negative int2str | Tianyi Liang | |
2014-02-18 | String parsing example in CVC parser | Morgan Deters | |
2014-02-18 | missed files for the latter commit | Tianyi Liang | |
2014-02-18 | str.to.int(INVALID) = -1 | Tianyi Liang | |
2014-02-18 | switch to total function str.to.int: maps invalid and non-digit strings to 0 | Tianyi Liang | |
2014-02-17 | bring back the commits which is lost accidentally. | Tianyi Liang | |
2014-02-17 | add str2int | Tianyi Liang | |
2014-02-17 | Fix for strings-exp: enable quantifiers | Morgan Deters | |
2014-02-17 | Fix strings preprocessing for justification heuristic | Morgan Deters | |
2014-02-17 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-02-17 | type conversion | Tianyi Liang | |
2014-02-17 | type conversion | Tianyi Liang | |
2014-02-14 | Make 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-14 | partial function charat | Tianyi Liang | |
2014-02-13 | fix expanding def | Tianyi Liang | |
2014-02-12 | bug fix for reverse check | Tianyi Liang | |
2014-02-11 | lexer fix: disable smt-lib conversion for string literals | Tianyi Liang | |
2014-02-11 | minor fix for recognizing the tail backslash, still have smt-lib compliance ↵ | Tianyi Liang | |
issue. | |||
2014-02-11 | resolve merge conflicts | Tianyi Liang | |
2014-02-11 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
Conflicts: src/theory/strings/theory_strings.cpp | |||
2014-02-11 | escaped characters, having an issue with smt-lib defintion, further repair ↵ | Tianyi Liang | |
is needed. | |||
2014-02-11 | minor fix for merge | Tianyi Liang | |
2014-02-11 | minor cleanup for merge | Tianyi Liang | |
2014-02-11 | minor fix for merge | Tianyi Liang | |
2014-02-11 | escaped characters, having an issue with smt-lib defintion, further repair ↵ | Tianyi Liang | |
is needed. | |||
2014-02-10 | Fix build (some nonexistent files listed in Makefile) | Morgan Deters | |
2014-02-09 | More 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-06 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-02-06 | minor cleanup for merge | Tianyi Liang | |
2014-02-06 | minor fix for merge | Tianyi Liang | |
2014-02-06 | minor cleanup for merge | Tianyi Liang | |