cvc5.git
2014-11-28 ajreynolSynchronize conjecture generation with E-matching....
2014-11-27 Tianyi Liangadd intersection rewriting
2014-11-27 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-11-27 Tianyi Liangadd more regexp rewriting
2014-11-27 Tianyi Liangadd more functions for regular expressions
2014-11-27 Tianyi Liangadd more regexp rewriting
2014-11-27 Tianyi Liangadd more functions for regular expressions
2014-11-25 ajreynolFix bug in --term-db-mode=relevant with variable trigge...
2014-11-22 lianahadded number of resource units used as a stat
2014-11-21 ajreynolThrow error when pattern is not list of terms.
2014-11-21 ajreynolChange default option to --inst-when=full-last-call...
2014-11-20 ajreynolDisable constants sharing in eq engine, disable hack...
2014-11-20 Morgan DetersFix #lines in template.
2014-11-20 Dejan JovanovićMaking construction of trigger sets not use the global...
2014-11-19 Morgan DetersDistribute UnsafeInterruptException interface file...
2014-11-19 Kshitij BansalMerge pull request #70 from kbansal/sets-for-merge...
2014-11-19 Kshitij BansalSet Constant's normal form and other short fixes
2014-11-18 Liana Hadareanclear model cache in BVQuickCheck clearSolver() (fixes...
2014-11-18 lianahAll Minisat solve calls now return lbool (fixes bug...
2014-11-18 ajreynolCompute model basis only for fmf. Add another co-datat...
2014-11-18 ajreynolAdd local theory extensions instantiation strategy...
2014-11-17 lianahadded command line option for extractArith bv rewrite
2014-11-17 Morgan DetersShort-circuit in TheoryArithPrivate::check(), care...
2014-11-17 Morgan DetersNew, uniform checkTime statistic for all theories ...
2014-11-17 Liana HadareanResource-limiting work.
2014-11-16 ajreynolAdd term db mode. Minor changes to quantifiers rewrite...
2014-11-14 ajreynolBe lazier to consider EQC in UF+cardinality solver...
2014-11-13 Clark BarrettMinor changes to AUTHORS and COPYING
2014-11-13 Morgan DetersMinor adjustments to wording.
2014-11-13 Morgan DetersCopyright text fixes.
2014-11-13 Morgan DetersMerge pull request #69 from mdeters/bug594
2014-11-13 ajreynolRemove two obsolete versions of MBQI.
2014-11-13 ajreynolMore preparation for filtering relevant terms in TermDb.
2014-11-13 Morgan DetersPossible fix for bug594
2014-11-13 Morgan DetersMerge pull request #65 from mdeters/bv-ineq-cachefix
2014-11-13 Morgan DetersBV inequality graph TNode fix.
2014-11-13 Morgan DetersFix BV inequality solver caching.
2014-11-12 Morgan DetersFix tokenization of "reset" in SMT-LIB v2.0. It's...
2014-11-11 Morgan DetersMinor cleanup.
2014-11-11 Kshitij BansalMerge pull request #64 from mdeters/theorysets-hashset...
2014-11-11 ajreynolWork on synchronizing decision=justification and E...
2014-11-10 Tianyi LiangMerge pull request #63 from mdeters/theorystrings-hashs...
2014-11-10 Dejan JovanovićBug 593 fix: if the type is finite, it is now considere...
2014-11-10 ajreynolDo not eliminate variables only occurring in patterns...
2014-11-10 Morgan DetersMerge branch '1.4.x'
2014-11-10 Morgan DetersUpdate TheorySets to use CDHashSet<>::key_begin() ...
2014-11-09 Morgan DetersUpdate TheoryStrings to use CDHashSet<>::key_begin...
2014-11-09 Morgan DetersWork around an apparent bug in libc++ that was causing...
2014-11-09 Morgan DetersFix a deterministic assignment-ordering for get-assignm...
2014-11-09 Morgan DetersIncrease stack size when running regressions (fixes...
2014-11-09 ajreynolFix dt shared terms issue, reenable regression.
2014-11-08 ajreynolFix bug with incremental+datatypes. Minor cleanup...
2014-11-08 Morgan DetersMerge pull request #62 from mdeters/bv-cleanup
2014-11-08 Morgan DetersRemove some unused variables.
2014-11-08 Clark BarrettFixed bug in model builder with subtypes
2014-11-07 Morgan DetersRemove some dead code.
2014-11-07 Morgan DetersFix a memory leak in SatSolverRegistry (re: bug #594).
2014-11-07 Morgan DetersFix memory issues in bitvector theory, which is now...
2014-11-07 Morgan DetersMerge branch '1.4.x'
2014-11-07 Morgan DetersFix missing case in Boolean terms rewriting. (Resolves...
2014-11-07 Morgan DetersMerge branch '1.4.x'
2014-11-07 Morgan DetersCorrected fix for missing case in model postprocessor...
2014-11-07 ajreynolEnable --quant-cf by default. Fix bug in qcf for mixed...
2014-11-07 Morgan DetersRevert "Fix missing case in model postprocessor (resolv...
2014-11-07 Morgan DetersRevert "Fix missing case in model postprocessor (resolv...
2014-11-07 Morgan DetersUpdate competition build rules.
2014-11-07 Morgan DetersMerge branch '1.4.x'
2014-11-07 Morgan DetersFix missing case in model postprocessor (resolves bug...
2014-11-07 ajreynolProperly distinguish which EQC to assign values in...
2014-11-06 ajreynolMinor fix for getInstCons
2014-11-06 ajreynolReenable regression. Add (for now, disabled) changes...
2014-11-05 ajreynolFix model bug in --mbqi=fmc. Minor cleanup in datatypes.
2014-11-05 Morgan DetersMerge branch '1.4.x'
2014-11-05 Morgan DetersFix get-bug-attachments script.
2014-11-05 ajreynolMore work on datatypes theory combination: fix bug...
2014-11-02 Clark BarrettAdded cache to getModelValue
2014-11-01 ajreynolFix cegqi for synthesis without syntax.
2014-11-01 ajreynolSimplify which lemmas to communicate in dt.
2014-11-01 ajreynolFix bug 592: introduce skolem for dt instantiate lemma...
2014-11-01 ajreynolFix some mistakes in datatypes theory combination,...
2014-10-31 ajreynolDo not allow duplication of function definitions. ...
2014-10-30 Clark BarrettBe more lazy about generating array lemmas
2014-10-30 Clark BarrettAdded new, much faster, care graph computation for...
2014-10-28 ajreynolPreprocessing step for finding finite runs of well...
2014-10-28 ajreynolInitial infrastructure for function definition quantifi...
2014-10-28 ajreynolImprove stats in conjecture generator, minor cleanup.
2014-10-25 ajreynolMinor fix for --user-pat=resort
2014-10-24 Morgan DetersFix typo.
2014-10-24 Morgan DetersMinor parser performance fix.
2014-10-24 ajreynolAdd --user-pat=resort. Minor cleanup of options.
2014-10-23 Morgan DetersParsing and infrastructure support for SMT-LIBv2.5...
2014-10-23 lianahFixed inefficiency in bit-vector rewrite rule.
2014-10-22 Morgan DetersFix bug590 regression distcheck failure from last night.
2014-10-22 Tianyi LiangFixed bug 589
2014-10-21 Clark BarrettFixed bug 590, added regression test
2014-10-20 ajreynolMinor cleanup in datatypes.
2014-10-20 Kshitij BansalMerge pull request #59 from kbansal/sets3
2014-10-20 Kshitij BansalFinish sets type enumerator implementation.
2014-10-20 Kshitij Bansalfix statistic in decision engine
2014-10-18 ajreynolFix assertion.
next