summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-02-26bug fix (caused by merge), move cardinality option to expert optionTianyi Liang
2014-02-26Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-02-26add a new fileTianyi Liang
2014-02-26for mergingTianyi Liang
2014-02-26smt-lib syntax change: str.contain -> str.contains; add some prefix syntax ↵Tianyi Liang
for cvc format
2014-02-26for mergingTianyi Liang
2014-02-25Minor code clean up in parser.Morgan Deters
2014-02-25New translation work, support Z3-str-style string constraints.Morgan Deters
2014-02-25Fix quotes in string constants.Morgan Deters
2014-02-25Add options --full-saturate-quant and --mbqi=trust. Other minor changes.Andrew Reynolds
2014-02-24smt-lib syntax change: str.contain -> str.contains; add some prefix syntax ↵Tianyi Liang
for cvc format
2014-02-24bug fix: strings preprocess for the orignal term, causing unknown in some casesTianyi Liang
2014-02-21Merge branch '1.3.x'Morgan Deters
2014-02-21No diamond-breaking under quantifiers (resolves bug #550).Morgan Deters
2014-02-21Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-02-21reorganize substr, fix some potential bugs, adds cache for preprocessingTianyi Liang
2014-02-21reorganize substr, fix some potential bugs, adds cache for preprocessingTianyi Liang
2014-02-21Merge branch '1.3.x'Morgan Deters
2014-02-21Fix 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-21portfolio: fix export of emptysetKshitij Bansal
2014-02-21Fix makefile dependence for system tests.Morgan Deters
2014-02-21disable test cvc3_main, attempt to fix dist_checkKshitij Bansal
2014-02-21Merge pull request #10 from kbansal/sets-for-mergeKshitij Bansal
Sets for merge
2014-02-21option to print stats after every satisfiability or validity queryKshitij Bansal
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback