cvc5.git
2014-03-17 Tianyi Lianghot fix for pre-reg term caching in strings
2014-03-14 Morgan DetersSMT-LIB compliance: allow bin/hex set-info, e.g. (set...
2014-03-14 Morgan Detersdos2unix on the proof signatures, and fix the makefile.
2014-03-14 Andrew ReynoldsAdd ability to provide theory-specific proof rules...
2014-03-13 Andrew ReynoldsAdd working example of LFSC proof with quantifiers...
2014-03-12 Andrew ReynoldsWork on array pf signature, add working example. Add...
2014-03-12 Andrew ReynoldsMinor fixes post-merge of RR.
2014-03-12 Morgan DetersFix LogicInfo unit test.
2014-03-12 Morgan DetersSome standardization of regression Makefiles that got...
2014-03-12 Morgan DetersDraft contrib/get-abc script for bitvectors libabc...
2014-03-11 Morgan DetersMerge branch '1.3.x'
2014-03-11 Morgan DetersFix for rewriterules build breakage.
2014-03-11 Morgan DetersFix for random-seed option.
2014-03-11 Morgan DetersFix for portfolio.
2014-03-11 Morgan DetersMinor cleanup.
2014-03-11 Morgan DetersFix for (get-assignment), resolves bug 553.
2014-03-11 Morgan DetersMerge branch '1.3.x'
2014-03-11 Morgan DetersFix some Win32 and SMT-LIB compliance bugs discovered...
2014-03-11 Andrew ReynoldsInitial refactor of rewrite rules, make theory_rewriter...
2014-03-10 Tianyi Liangadds intro vars length cache
2014-03-10 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-03-10 Tianyi Liangminor change for strings-fmf
2014-03-10 Tianyi Liangminor change for strings-fmf
2014-03-08 Morgan DetersRe-fix bug 551 by adding a check to the arith ITE simpl...
2014-03-08 Tim KingMerge pull request #18 from timothy-king/master
2014-03-08 Tim KingFixing name changes that cam in from the merge.
2014-03-08 Tim KingMerge remote-tracking branch 'CVC4root/master'
2014-03-08 Morgan DetersRemove --ite-remove-quant; support pulling ground ITEs...
2014-03-08 Morgan DetersFix run_regression on Mac.
2014-03-08 Morgan DetersFix bug 554 (nominally).
2014-03-08 Tim KingFixing a SWIG problem for RationalFromDoubleException.
2014-03-07 Tim KingMerging a squash of the branch timothy-king/CVC4/glpkne...
2014-03-07 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-03-07 Tianyi Liangremove unrolling depth
2014-03-07 Tianyi Liangbring back D-Norm
2014-03-07 Morgan DetersFix strings-exp setting.
2014-03-07 Tianyi Liangremove unrolling depth
2014-03-07 Tianyi Liangbring back D-Norm
2014-03-07 Morgan DetersFix strings-exp setting.
2014-03-07 Thomas HungerAdd swig renames for new Z3STR language.
2014-03-07 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-03-07 Tianyi Liangadds incremental for strings; clean-up codes
2014-03-07 Tianyi Liangadds incremental for strings; clean-up codes
2014-03-05 Kshitij BansalMerge pull request #14 from kbansal/sets-parserchanges
2014-03-05 Kshitij BansalArray smtlib compliance tests
2014-03-05 Kshitij BansalRevert "fix naming conflicts in benchmarks"
2014-03-05 Kshitij BansalDon't tokenize SET_THEORY operators in smt2 parser
2014-03-05 Tim KingImproving support for POW in arithmetic. Resolves bug...
2014-03-04 Thomas HungerGuard java-specific swig code with SWIGJAVA.
2014-03-04 Morgan DetersDon't theory-preprocess under quantifiers; but DO theor...
2014-03-04 Morgan DetersMore useful error message when someone tries mkExpr...
2014-03-01 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-03-01 Tianyi Liangadd re.nostr for the empty regular expression; add...
2014-03-01 Tianyi Liangminor clean-up, bring back derivatives
2014-03-01 Tianyi Lianga new regular expression engine for solving both positi...
2014-03-01 Tianyi Liangadd re.nostr for the empty regular expression; add...
2014-02-28 Tianyi Liangminor clean-up, bring back derivatives
2014-02-28 Tianyi Lianga new regular expression engine for solving both positi...
2014-02-28 Kshitij BansalMerge pull request #12 from kbansal/in-to-member
2014-02-28 Kshitij Bansaltheory/sets: cleanup
2014-02-28 Kshitij Bansalrename kind::IN to kind::MEMBER (fixes some windows...
2014-02-28 Kshitij BansalMerge pull request #11 from kbansal/improve-stats-every...
2014-02-27 Kshitij Bansal--stats-every-query option: print increment in addition...
2014-02-27 Andrew ReynoldsBug fix for QCF algorithm, was missing instantiations...
2014-02-26 Tianyi Liangsorry for the missing file
2014-02-26 Tianyi Liangbug fix (caused by merge), move cardinality option...
2014-02-26 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-02-26 Tianyi Liangadd a new file
2014-02-26 Tianyi Liangfor merging
2014-02-26 Tianyi Liangsmt-lib syntax change: str.contain -> str.contains...
2014-02-26 Tianyi Liangfor merging
2014-02-25 Morgan DetersMinor code clean up in parser.
2014-02-25 Morgan DetersNew translation work, support Z3-str-style string const...
2014-02-25 Morgan DetersFix quotes in string constants.
2014-02-25 Andrew ReynoldsAdd options --full-saturate-quant and --mbqi=trust...
2014-02-24 Tianyi Liangsmt-lib syntax change: str.contain -> str.contains...
2014-02-24 Tianyi Liangbug fix: strings preprocess for the orignal term, causi...
2014-02-21 Morgan DetersMerge branch '1.3.x'
2014-02-21 Morgan DetersNo diamond-breaking under quantifiers (resolves bug...
2014-02-21 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-02-21 Tianyi Liangreorganize substr, fix some potential bugs, adds cache...
2014-02-21 Tianyi Liangreorganize substr, fix some potential bugs, adds cache...
2014-02-21 Morgan DetersMerge branch '1.3.x'
2014-02-21 Morgan DetersFix two variants of Node::substitute().
2014-02-21 Kshitij Bansalportfolio: fix export of emptyset
2014-02-21 Morgan DetersFix makefile dependence for system tests.
2014-02-21 Kshitij Bansaldisable test cvc3_main, attempt to fix dist_check
2014-02-21 Kshitij BansalMerge pull request #10 from kbansal/sets-for-merge
2014-02-21 Kshitij Bansaloption to print stats after every satisfiability or...
2014-02-21 Kshitij Bansaladd new theory (sets)
2014-02-21 Kshitij Bansalfix a -Wunused
2014-02-21 Tianyi Liangfix makefile
2014-02-21 Tianyi Liangadd more tests, and define int.to.str(NEGATIVE)=""
2014-02-20 Tianyi Liangadd two cases to the regression test
2014-02-20 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-02-20 Tianyi Lianghot fix for str2int/int2str
2014-02-20 Tianyi Liangadd negative int2str
2014-02-20 Morgan DetersString parsing example in CVC parser
2014-02-20 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-02-20 Tianyi Lianghot fix for str2int/int2str
next