cvc5.git
2015-10-26 Tim KingThis commit moves the scripts for building the Debug_ta...
2015-10-26 Tim KingThis fixes a one definition rule violation for reduceDB...
2015-10-26 ajreynolPromote InstStrategyCbqi to quantifier module. Cleanup...
2015-10-26 ajreynolExtend counterexample-guided instantiation to extended...
2015-10-25 Kshitij BansalRevert "Default builds are now proof enabled."
2015-10-24 ajreynolFixes related to string contains.
2015-10-24 Tim KingThis removes a bug for reading data that has been poppe...
2015-10-24 Tim KingSpecify that the default initialization must always...
2015-10-24 Tim KingSwitching Options::current() to return a pointer. This...
2015-10-24 Tim KingChanges configure.ac so that the single recurisve invoc...
2015-10-24 Tim KingThis patch slightly generalizes how the std::isfinite...
2015-10-22 ajreynolEnable counterexample-guided quantifier instantiation...
2015-10-21 ajreynolMinor refactoring in strings related to length.
2015-10-20 ajreynolRefactor strings, remove old cycle checks in normalize...
2015-10-19 ajreynolClean up explanations involving string length. Add...
2015-10-19 ajreynolImprove stratification of strings extended function...
2015-10-19 ajreynolImprove regexp rewriter, simplify regexp preprocess...
2015-10-18 ajreynolFix for no condense func values.
2015-10-16 ajreynolAdd option to interleave enumerative instantiation...
2015-10-16 ajreynolThrow error for recursively defined types involving...
2015-10-16 ajreynolFix for codatatype constant rewrite, add regression.
2015-10-15 ajreynolFix congruence check in strings, fixes bug 686.
2015-10-15 ajreynolChange semantics of str.substr to allow endpoint out...
2015-10-15 ajreynolDecompose string contains, minor refactoring.
2015-10-14 Kshitij BansalMerge pull request #77 from kbansal/macsegfault
2015-10-13 Kshitij Bansalremove options infrastructure code which depended on...
2015-10-12 Kshitij BansalMerge pull request #76 from CVC4/proofs
2015-10-11 Kshitij Bansalfix regression tests, support fallback mode for proofs
2015-10-11 Liana HadareanDefault builds are now proof enabled.
2015-10-11 ajreynolFix strings preprocessing + incremental, fixes bug...
2015-10-09 Liana HadareanTemporary reverting commit 477e72b (proofs as default...
2015-10-08 ajreynolMinor improvements to strings. Refactor rewriter. Enabl...
2015-10-07 Liana HadareanDefault builds are now proof enabled.
2015-10-07 Liana HadareanDisabled donePPSimpITE when unsat-cores are enabled...
2015-10-07 ajreynolMinor improvements, add endpoint eq inference to strings.
2015-10-06 ajreynolMore improvements to strings rewriter for regexps,...
2015-10-02 ajreynolFixes related to explanations for cycles, sym inference...
2015-10-02 ajreynolImprovements to rewriter for regexp, contains, indexof...
2015-10-01 ajreynolEvaluate extended operators on partially concrete argum...
2015-10-01 ajreynolMore improvements to strings. More aggressive inference...
2015-09-30 ajreynolRefactor strings, bug fix inferences vs lemmas.
2015-09-29 ajreynolFix for fmf+incremental. Restrict cbqi to literals...
2015-09-28 ajreynolImprove quantifiers engine wrt incremental presolve...
2015-09-28 ajreynolMinor fix
2015-09-28 ajreynolMinor fixes to strings, add regressions.
2015-09-28 ajreynolAdd missing regression
2015-09-28 ajreynolFix bug for trivial extf inferences in strings. Improve...
2015-09-27 ajreynolImproved handling of extended operators. Do preprocess...
2015-09-26 ajreynolLazy preprocessing of extended operators in strings...
2015-09-26 ajreynolBetter organization of quantifiers modules, promote...
2015-09-25 ajreynolClear term caches for quantifiers + incremental, fixes...
2015-09-24 ajreynolCounterexample-guided instantiation for datatypes....
2015-09-22 ajreynolImprove ITE redundant branch elimination in quantifiers.
2015-09-21 Kshitij BansalFix for sets segfault (reported by Ravi Kandhadai)
2015-09-18 ajreynolFix bug in quantifiers engine where model construction...
2015-09-18 ajreynolMore work mixing UF and sygus.
2015-09-17 ajreynolAllow most smt2 commands as sygus commands. Fix bug...
2015-09-16 ajreynolAdd option --fmf-fun-rlv, remove deprecated option...
2015-09-15 ajreynolFix bug related to quantifiers + incremental, thanks...
2015-09-11 ajreynolMinor cleanup related to codatatypes.
2015-09-10 ajreynolModels for codatatypes. Fixes bug 662.
2015-09-10 ajreynolNormalization of codatatype constants, codatatype now...
2015-09-10 ajreynolFix bug 670. Minor.
2015-09-09 ajreynolFix bug in strings rewriter regarding lengths of substr...
2015-09-09 ajreynolWorking towards a fair enumerator for codatatypes.
2015-09-06 ajreynolImprove quantifiers rewriter, minor refactoring.
2015-09-05 ajreynolWorking fix for bugs 610 and 643 regarding check-model...
2015-09-05 ajreynolFix bugs related to fmf with incremental. Reinitialize...
2015-09-04 ajreynolFix bugs 605 and 667.
2015-09-02 Kshitij Bansalfix regressions
2015-09-02 Kshitij BansalMerge remote-tracking branch 'origin/master'
2015-09-01 Clark BarrettFixed but with getAssertions
2015-08-30 ajreynolMinor improvement to sygus sol reconstruction.
2015-08-28 ajreynolImprovements to sygus, register equivalent terms based...
2015-08-27 ajreynolDo ITE term bookkeeping when solving Sygus inputs....
2015-08-27 ajreynolModify slow regressions.
2015-08-26 ajreynolMinor improvements to cbqi, fix bug in solving with...
2015-08-25 ajreynolUse zero in cbqi when not using infinities.
2015-08-24 Liana HadareanAdded threshold for core bv cardinality lemmas
2015-08-24 Liana HadareanFix for bv core cardinality lemma generation
2015-08-24 Liana Hadareaneager bit-blasting gives models for boolean variables...
2015-08-24 ajreynolImprovements to vts in cbqi, bug fix vts for non-atomic...
2015-08-21 ajreynolMinor changes related to codatatypes for 1.5 release.
2015-08-21 ajreynolFix disequality bounds in cbqi, record literals for...
2015-08-21 Kshitij Bansalbetter handling for conflicting options with nonlinear...
2015-08-21 Kshitij BansalFix bug 649 (errors to regular output channel)
2015-08-20 Liana Hadareanfix to bug659 due to algebraic solver model building
2015-08-20 Liana Hadareanfix for bug660 and bug658 due to incorrect bit-blasting...
2015-08-19 ajreynolMake cbqi robust to term ITE removal. Separate vts...
2015-08-19 Kshitij Bansalfix bug 605
2015-08-19 ajreynolImplementation of model-based projection in cbqi, clean...
2015-08-18 Tianyi Liangfix for bug663
2015-08-16 ajreynolMore optimizations to --macros-quant, add --macros...
2015-08-12 ajreynolImprovements to --macros-quant. Enable --clause-split...
2015-08-01 ajreynolSimplification/improvement to solving deltas in LRA...
2015-08-01 ajreynolSupport for default grammar for datatypes in sygus...
2015-07-31 ajreynolMake --fmf-fun and --macros-quant work in incremental...
2015-07-31 ajreynolSygus support for inductive datatypes.
2015-07-30 ajreynolImplement virtual term substitution for non-nested...
2015-07-28 Tianyi LiangDisable bug590.smt2
next