cvc5.git
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
2014-02-20 Tianyi Liangadd negative int2str
2014-02-20 Morgan DetersString parsing example in CVC parser
2014-02-20 Andrew ReynoldsFix ite and iff handling in QCF. Add option for heuris...
2014-02-20 Kshitij Bansalportfolio: add stat to track time spent waiting for...
2014-02-19 Tim KingMerge branch 'master' of github.com:CVC4/CVC4
2014-02-19 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-02-19 Tim KingMerge branch '1.3.x'
2014-02-19 Tim KingStopping non-linear terms from entering the dio solver...
2014-02-19 Tianyi Liangadd negative int2str
2014-02-19 Morgan DetersString parsing example in CVC parser
2014-02-18 Tianyi Liangmissed files for the latter commit
2014-02-18 Tianyi Liangstr.to.int(INVALID) = -1
2014-02-18 Tianyi Liangswitch to total function str.to.int: maps invalid and...
2014-02-18 Tianyi Liangbring back the commits which is lost accidentally.
2014-02-18 Tianyi Liangadd str2int
2014-02-17 Morgan DetersFix for strings-exp: enable quantifiers
2014-02-17 Morgan DetersFix strings preprocessing for justification heuristic
2014-02-17 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-02-17 Tianyi Liangtype conversion
2014-02-17 Tianyi Liangtype conversion
2014-02-14 Andrew ReynoldsMake QCF more incremental. Fix bug in QCF handling...
2014-02-14 Tianyi Liangpartial function charat
2014-02-14 Tianyi Liangfix expanding def
2014-02-12 Tianyi Liangbug fix for reverse check
2014-02-12 Tianyi Lianglexer fix: disable smt-lib conversion for string literals
2014-02-12 Tianyi Liangminor fix for recognizing the tail backslash, still...
2014-02-11 Tianyi Liangresolve merge conflicts
2014-02-11 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-02-11 Tianyi Liangescaped characters, having an issue with smt-lib defint...
2014-02-11 Tianyi Liangminor fix for merge
2014-02-11 Tianyi Liangminor cleanup for merge
2014-02-11 Tianyi Liangminor fix for merge
2014-02-11 Tianyi Liangescaped characters, having an issue with smt-lib defint...
2014-02-11 Morgan DetersFix build (some nonexistent files listed in Makefile)
2014-02-09 Andrew ReynoldsMore complete guess instantiation strategy, cvc4 now...
2014-02-06 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-02-06 Tianyi Liangminor cleanup for merge
2014-02-06 Tianyi Liangminor fix for merge
2014-02-06 Tianyi Liangminor cleanup for merge
2014-02-06 Morgan DetersMinor fix for previous commit
2014-02-06 Morgan DetersOops.. premature push on lexer fix (remove debugging...
2014-02-06 Morgan DetersFixes for escape-handling for string literals in SMT...
2014-02-05 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-02-05 Tianyi Liangminor fix for merge
2014-02-05 Tianyi Liangminor fix for merge
2014-02-05 Andrew ReynoldsBug fix for theory strings related to old cycle detecti...
2014-02-04 Andrew ReynoldsDo not use transitive closure module for cycle detectio...
2014-02-04 Andrew ReynoldsAdd variable ordering for QCF to accelerate matching...
2014-02-03 Andrew ReynoldsHandle nested (universal) quantifiers in QCF algorithm...
2014-01-31 Tianyi LiangSubstr fix: (= (str.substr "" 0 3) "xxx") should be...
2014-01-30 Andrew ReynoldsRefactor QCF slightly. Bug fix for relevant domain...
2014-01-30 Tianyi Liangstats for eq/diseq splits
2014-01-30 Tianyi Lianganother name change
2014-01-30 Tianyi Liangchange string stats text names
2014-01-30 Tianyi Liangadds stats
2014-01-29 Tianyi Liangroll back to uf implementation for substr and charat
2014-01-29 Tianyi Liangadd prefixof, suffixof
2014-01-28 Tianyi Liangmerge internal and user of charat & substr into one
2014-01-28 Andrew ReynoldsMore optimizations of quantifier instantiation data...
2014-01-27 Morgan DetersMerge branch '1.3.x'
2014-01-27 Morgan DetersURL update
2014-01-27 Andrew ReynoldsMore optimization of QCF and instantiation caching...
2014-01-26 Andrew ReynoldsMore optimization of QCF. Fixed InstMatchTrie for...
2014-01-25 Tianyi Liangreplace charat uf with internal one
2014-01-25 Tianyi Liangminor fix, indexof rewriter opt
2014-01-24 Tianyi Liangfix: indexof, replace rewriting
2014-01-24 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-01-24 Tianyi Liangrev diseq
2014-01-24 Tianyi Liangrev const split
2014-01-24 Tianyi Liangoptimize for the reverse direction
2014-01-24 Tianyi Liangrev diseq
2014-01-24 Tianyi Liangrev const split
2014-01-24 Andrew ReynoldsSimplify the QCF algorithm by more aggressive flattenin...
2014-01-24 Tianyi Liangoptimize for the reverse direction
2014-01-23 Tianyi Liangfix: constants are inferred to be the same
2014-01-23 Tianyi Liangminor fix
2014-01-22 Tianyi LiangMerge branch 'master' of https://github.com/CVC4/CVC4
2014-01-22 Morgan DetersSome minor fixes to SmtEngine strings settings.
2014-01-22 Tianyi Liangcommented out all_supported in strings for now, it...
2014-01-22 Tianyi Liangsolve string exp issue for regexp
2014-01-22 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-01-22 Tianyi Liangadd warning for using strings in ALL_SUPPORTED
2014-01-22 Tianyi LiangSmarter options, but still have a bug
2014-01-22 Morgan DetersDelay QuantifiersEngine and UF strong solver initializa...
next