Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-02-26 | bug fix (caused by merge), move cardinality option to expert option | Tianyi Liang | |
2014-02-26 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-02-26 | add a new file | Tianyi Liang | |
2014-02-26 | for merging | Tianyi Liang | |
2014-02-26 | smt-lib syntax change: str.contain -> str.contains; add some prefix syntax ↵ | Tianyi Liang | |
for cvc format | |||
2014-02-26 | for merging | Tianyi Liang | |
2014-02-25 | Minor code clean up in parser. | Morgan Deters | |
2014-02-25 | New translation work, support Z3-str-style string constraints. | Morgan Deters | |
2014-02-25 | Fix quotes in string constants. | Morgan Deters | |
2014-02-25 | Add options --full-saturate-quant and --mbqi=trust. Other minor changes. | Andrew Reynolds | |
2014-02-24 | smt-lib syntax change: str.contain -> str.contains; add some prefix syntax ↵ | Tianyi Liang | |
for cvc format | |||
2014-02-24 | bug fix: strings preprocess for the orignal term, causing unknown in some cases | Tianyi Liang | |
2014-02-21 | Merge branch '1.3.x' | Morgan Deters | |
2014-02-21 | No diamond-breaking under quantifiers (resolves bug #550). | Morgan Deters | |
2014-02-21 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-02-21 | reorganize substr, fix some potential bugs, adds cache for preprocessing | Tianyi Liang | |
2014-02-21 | reorganize substr, fix some potential bugs, adds cache for preprocessing | Tianyi Liang | |
2014-02-21 | Merge branch '1.3.x' | Morgan Deters | |
2014-02-21 | Fix two variants of Node::substitute(). | Morgan Deters | |
Node::substitute() is overloaded. One version was properly substituting operators (e.g. the "f" in f(x) could be substituted). The others were ignoring anything in function position. Fixed. Thanks to Wei Wang for pointing this out. | |||
2014-02-21 | portfolio: fix export of emptyset | Kshitij Bansal | |
2014-02-21 | Fix makefile dependence for system tests. | Morgan Deters | |
2014-02-21 | disable test cvc3_main, attempt to fix dist_check | Kshitij Bansal | |
2014-02-21 | Merge pull request #10 from kbansal/sets-for-merge | Kshitij Bansal | |
Sets for merge | |||
2014-02-21 | option to print stats after every satisfiability or validity query | Kshitij Bansal | |
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 | |