Age | Commit message (Expand) | Author |
2014-03-16 | Fix for ite of >=64bit wide bitvectors with unconstrained condition. | Peter Collingbourne |
2014-03-14 | Add ability to provide theory-specific proof rules to EqualityEngine, extends... | Andrew Reynolds |
2014-03-12 | Work on array pf signature, add working example. Add quantifiers proof signa... | Andrew Reynolds |
2014-03-12 | Minor fixes post-merge of RR. | Andrew Reynolds |
2014-03-11 | Fix for rewriterules build breakage. | Morgan Deters |
2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
2014-03-10 | adds intro vars length cache | Tianyi Liang |
2014-03-10 | minor change for strings-fmf | Tianyi Liang |
2014-03-08 | Re-fix bug 551 by adding a check to the arith ITE simplifier to ignore non-gr... | Morgan Deters |
2014-03-08 | Fixing name changes that cam in from the merge. | Tim King |
2014-03-08 | Merge remote-tracking branch 'CVC4root/master' | Tim King |
2014-03-07 | Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodi... | Morgan Deters |
2014-03-07 | Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into m... | Tim King |
2014-03-07 | remove unrolling depth | Tianyi Liang |
2014-03-07 | bring back D-Norm | Tianyi Liang |
2014-03-06 | adds incremental for strings; clean-up codes | Tianyi Liang |
2014-03-05 | Improving support for POW in arithmetic. Resolves bug 549. | Tim King |
2014-03-04 | Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r... | Morgan Deters |
2014-02-28 | add re.nostr for the empty regular expression; add re.allchar for the regular... | Tianyi Liang |
2014-02-28 | minor clean-up, bring back derivatives | Tianyi Liang |
2014-02-28 | a new regular expression engine for solving both positive and negative member... | Tianyi Liang |
2014-02-28 | theory/sets: cleanup | Kshitij Bansal |
2014-02-28 | rename kind::IN to kind::MEMBER (fixes some windows build conflicts) | Kshitij Bansal |
2014-02-27 | Bug fix for QCF algorithm, was missing instantiations. Make prop-eq the defa... | Andrew Reynolds |
2014-02-26 | bug fix (caused by merge), move cardinality option to expert option | Tianyi Liang |
2014-02-26 | for merging | Tianyi Liang |
2014-02-25 | Add options --full-saturate-quant and --mbqi=trust. Other minor changes. | Andrew Reynolds |
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 | reorganize substr, fix some potential bugs, adds cache for preprocessing | Tianyi Liang |
2014-02-21 | disable test cvc3_main, attempt to fix dist_check | Kshitij Bansal |
2014-02-21 | add new theory (sets) | Kshitij Bansal |
2014-02-21 | fix a -Wunused | Kshitij Bansal |
2014-02-20 | add more tests, and define int.to.str(NEGATIVE)="" | Tianyi Liang |
2014-02-20 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang |
2014-02-20 | hot fix for str2int/int2str | Tianyi Liang |
2014-02-20 | add negative int2str | Tianyi Liang |
2014-02-20 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang |
2014-02-20 | hot fix for str2int/int2str | Tianyi Liang |
2014-02-20 | add negative int2str | Tianyi Liang |
2014-02-20 | Fix ite and iff handling in QCF. Add option for heuristic instantiation in Q... | Andrew Reynolds |
2014-02-19 | Merge branch 'master' of github.com:CVC4/CVC4 | Tim King |
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 | 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 |