cvc5.git
2014-03-27 Tianyi Liangderiv symbolic regexp
2014-03-27 Tianyi Liangadds intersection
2014-03-26 Morgan DetersMerge branch '1.3.x'
2014-03-26 Morgan DetersWin32 build script fixes (to allow portfolio builds).
2014-03-26 Morgan DetersFix an off-the-end string pointer bug (showed up only...
2014-03-26 Tim KingMerging in a fix from 1.3.x.
2014-03-26 Tim KingFixes an idempotency issue for non-linear multiplicatio...
2014-03-21 Kshitij BansalMerge pull request #22 from kbansal/sets-model
2014-03-20 Kshitij Bansalcleanup
2014-03-20 Kshitij Bansalfix for sets/mar2014/..317minimized..
2014-03-20 Kshitij BansalFix for registration issues of term appearing in a...
2014-03-20 Kshitij Bansalrewriter fix, weaken an assertion
2014-03-20 Kshitij Bansalconstant normal form and rewrite
2014-03-20 Kshitij Bansalfix a sharing issues with sets
2014-03-20 Kshitij Bansalpush subtyping for sets to the element type
2014-03-20 Kshitij Bansalenable check-models for sets/ regressions
2014-03-20 Kshitij Bansalwork on set model
2014-03-20 Kshitij Bansaltestlemma regressions
2014-03-20 Andrew ReynoldsMinor fix for CBQI, ignore inst constant nodes.
2014-03-19 Morgan DetersFix documentation for Theory::preRegisterTerm().
2014-03-19 Martin BrainRefactor the theory specific parts of definition expans...
2014-03-19 Morgan DetersSet dumping options from (set-option..) and API more...
2014-03-19 Morgan DetersFix for bug 555; SMT-LIBv2 symbols now output with...
2014-03-19 Morgan DetersMove the translator binary from src/main to examples...
2014-03-19 Morgan DetersAppease compilers from latest XCode release (v5.1).
2014-03-19 Morgan DetersMinor usability fixes related to SMT-LIB compliance.
2014-03-19 Morgan DetersFix proof signatures makefile
2014-03-19 Morgan DetersMinor documentation fixups.
2014-03-19 Andrew ReynoldsFix a memory leak in LFSC proof checker. Largest QF_UF...
2014-03-17 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-03-17 Tianyi Lianghot fix for pre-reg term caching in strings
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
next