Age | Commit message (Expand) | Author |
2014-03-31 | add str to u16/u32, and u16/u32 to str | Tianyi Liang |
2014-03-28 | add construles, type_rules rm redundant, kinds cleanup | Kshitij Bansal |
2014-03-27 | adds new feature: re.loop | Tianyi Liang |
2014-03-20 | Merge pull request #22 from kbansal/sets-model | Kshitij Bansal |
2014-03-20 | cleanup | Kshitij Bansal |
2014-03-20 | fix for sets/mar2014/..317minimized.. | Kshitij Bansal |
2014-03-20 | Fix for registration issues of term appearing in a shared lemma | Kshitij Bansal |
2014-03-20 | fix a sharing issues with sets | Kshitij Bansal |
2014-03-20 | enable check-models for sets/ regressions | Kshitij Bansal |
2014-03-20 | testlemma regressions | Kshitij Bansal |
2014-03-19 | Minor usability fixes related to SMT-LIB compliance. | Morgan Deters |
2014-03-12 | Work on array pf signature, add working example. Add quantifiers proof signa... | Andrew Reynolds |
2014-03-12 | Fix LogicInfo unit test. | Morgan Deters |
2014-03-12 | Some standardization of regression Makefiles that got out of sync. Fixes cas... | Morgan Deters |
2014-03-11 | Minor cleanup. | Morgan Deters |
2014-03-11 | Fix for (get-assignment), resolves bug 553. | Morgan Deters |
2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
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 | Fix run_regression on Mac. | Morgan Deters |
2014-03-07 | Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into m... | Tim King |
2014-03-05 | Array smtlib compliance tests | Kshitij Bansal |
2014-03-05 | Revert "fix naming conflicts in benchmarks" | Kshitij Bansal |
2014-03-05 | Don't tokenize SET_THEORY operators in smt2 parser | Kshitij Bansal |
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 | a new regular expression engine for solving both positive and negative member... | Tianyi Liang |
2014-02-26 | sorry for the missing file | Tianyi Liang |
2014-02-26 | bug fix (caused by merge), move cardinality option to expert option | Tianyi Liang |
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 | add new theory (sets) | 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-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-10 | Fix build (some nonexistent files listed in Makefile) | Morgan Deters |
2014-02-09 | More complete guess instantiation strategy, cvc4 now typically times out inst... | Andrew Reynolds |
2014-01-28 | merge internal and user of charat & substr into one | Tianyi Liang |
2014-01-26 | More optimization of QCF. Fixed InstMatchTrie for caching instantiations. U... | Andrew Reynolds |
2014-01-22 | Delay QuantifiersEngine and UF strong solver initialization until after final... | Morgan Deters |
2014-01-18 | strings with new ideas | Tianyi Liang |
2014-01-16 | adds partial functions | Tianyi Liang |
2013-12-26 | new functions in strings | Tianyi Liang |
2013-12-24 | Merge branch '1.3.x' | Morgan Deters |
2013-12-24 | Better automatic handling of output language setting. | Morgan Deters |
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof g... | Morgan Deters |
2013-12-18 | Add missing regression-results directory. | Morgan Deters |
2013-12-16 | Fix for bug 544. | Morgan Deters |