| 2015-10-12 |
Kshitij Bansal | Merge pull request #76 from CVC4/proofs |
commit | commitdiff | tree |
| 2015-10-11 |
Kshitij Bansal | fix regression tests, support fallback mode for proofs |
commit | commitdiff | tree |
| 2015-10-11 |
Liana Hadarean | Default builds are now proof enabled. |
commit | commitdiff | tree |
| 2015-10-11 |
ajreynol | Fix strings preprocessing + incremental, fixes bug... |
commit | commitdiff | tree |
| 2015-10-09 |
Liana Hadarean | Temporary reverting commit 477e72b (proofs as default... |
commit | commitdiff | tree |
| 2015-10-08 |
ajreynol | Minor improvements to strings. Refactor rewriter. Enabl... |
commit | commitdiff | tree |
| 2015-10-07 |
Liana Hadarean | Default builds are now proof enabled. |
commit | commitdiff | tree |
| 2015-10-07 |
Liana Hadarean | Disabled donePPSimpITE when unsat-cores are enabled... |
commit | commitdiff | tree |
| 2015-10-07 |
ajreynol | Minor improvements, add endpoint eq inference to strings. |
commit | commitdiff | tree |
| 2015-10-06 |
ajreynol | More improvements to strings rewriter for regexps,... |
commit | commitdiff | tree |
| 2015-10-02 |
ajreynol | Fixes related to explanations for cycles, sym inference... |
commit | commitdiff | tree |
| 2015-10-02 |
ajreynol | Improvements to rewriter for regexp, contains, indexof... |
commit | commitdiff | tree |
| 2015-10-01 |
ajreynol | Evaluate extended operators on partially concrete argum... |
commit | commitdiff | tree |
| 2015-10-01 |
ajreynol | More improvements to strings. More aggressive inference... |
commit | commitdiff | tree |
| 2015-09-30 |
ajreynol | Refactor strings, bug fix inferences vs lemmas. |
commit | commitdiff | tree |
| 2015-09-29 |
ajreynol | Fix for fmf+incremental. Restrict cbqi to literals... |
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Improve quantifiers engine wrt incremental presolve... |
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Minor fix |
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Minor fixes to strings, add regressions. |
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Add missing regression |
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Fix bug for trivial extf inferences in strings. Improve... |
commit | commitdiff | tree |
| 2015-09-27 |
ajreynol | Improved handling of extended operators. Do preprocess... |
commit | commitdiff | tree |
| 2015-09-26 |
ajreynol | Lazy preprocessing of extended operators in strings... |
commit | commitdiff | tree |
| 2015-09-26 |
ajreynol | Better organization of quantifiers modules, promote... |
commit | commitdiff | tree |
| 2015-09-25 |
ajreynol | Clear term caches for quantifiers + incremental, fixes... |
commit | commitdiff | tree |
| 2015-09-24 |
ajreynol | Counterexample-guided instantiation for datatypes.... |
commit | commitdiff | tree |
| 2015-09-22 |
ajreynol | Improve ITE redundant branch elimination in quantifiers. |
commit | commitdiff | tree |
| 2015-09-21 |
Kshitij Bansal | Fix for sets segfault (reported by Ravi Kandhadai) |
commit | commitdiff | tree |
| 2015-09-18 |
ajreynol | Fix bug in quantifiers engine where model construction... |
commit | commitdiff | tree |
| 2015-09-18 |
ajreynol | More work mixing UF and sygus. |
commit | commitdiff | tree |
| 2015-09-17 |
ajreynol | Allow most smt2 commands as sygus commands. Fix bug... |
commit | commitdiff | tree |
| 2015-09-16 |
ajreynol | Add option --fmf-fun-rlv, remove deprecated option... |
commit | commitdiff | tree |
| 2015-09-15 |
ajreynol | Fix bug related to quantifiers + incremental, thanks... |
commit | commitdiff | tree |
| 2015-09-11 |
ajreynol | Minor cleanup related to codatatypes. |
commit | commitdiff | tree |
| 2015-09-10 |
ajreynol | Models for codatatypes. Fixes bug 662. |
commit | commitdiff | tree |
| 2015-09-10 |
ajreynol | Normalization of codatatype constants, codatatype now... |
commit | commitdiff | tree |
| 2015-09-10 |
ajreynol | Fix bug 670. Minor. |
commit | commitdiff | tree |
| 2015-09-09 |
ajreynol | Fix bug in strings rewriter regarding lengths of substr... |
commit | commitdiff | tree |
| 2015-09-09 |
ajreynol | Working towards a fair enumerator for codatatypes. |
commit | commitdiff | tree |
| 2015-09-06 |
ajreynol | Improve quantifiers rewriter, minor refactoring. |
commit | commitdiff | tree |
| 2015-09-05 |
ajreynol | Working fix for bugs 610 and 643 regarding check-model... |
commit | commitdiff | tree |
| 2015-09-05 |
ajreynol | Fix bugs related to fmf with incremental. Reinitialize... |
commit | commitdiff | tree |
| 2015-09-04 |
ajreynol | Fix bugs 605 and 667. |
commit | commitdiff | tree |
| 2015-09-02 |
Kshitij Bansal | fix regressions |
commit | commitdiff | tree |
| 2015-09-02 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' |
commit | commitdiff | tree |
| 2015-09-01 |
Clark Barrett | Fixed but with getAssertions |
commit | commitdiff | tree |
| 2015-08-30 |
ajreynol | Minor improvement to sygus sol reconstruction. |
commit | commitdiff | tree |
| 2015-08-28 |
ajreynol | Improvements to sygus, register equivalent terms based... |
commit | commitdiff | tree |
| 2015-08-27 |
ajreynol | Do ITE term bookkeeping when solving Sygus inputs.... |
commit | commitdiff | tree |
| 2015-08-27 |
ajreynol | Modify slow regressions. |
commit | commitdiff | tree |
| 2015-08-26 |
ajreynol | Minor improvements to cbqi, fix bug in solving with... |
commit | commitdiff | tree |
| 2015-08-25 |
ajreynol | Use zero in cbqi when not using infinities. |
commit | commitdiff | tree |
| 2015-08-24 |
Liana Hadarean | Added threshold for core bv cardinality lemmas |
commit | commitdiff | tree |
| 2015-08-24 |
Liana Hadarean | Fix for bv core cardinality lemma generation |
commit | commitdiff | tree |
| 2015-08-24 |
Liana Hadarean | eager bit-blasting gives models for boolean variables... |
commit | commitdiff | tree |
| 2015-08-24 |
ajreynol | Improvements to vts in cbqi, bug fix vts for non-atomic... |
commit | commitdiff | tree |
| 2015-08-21 |
ajreynol | Minor changes related to codatatypes for 1.5 release. |
commit | commitdiff | tree |
| 2015-08-21 |
ajreynol | Fix disequality bounds in cbqi, record literals for... |
commit | commitdiff | tree |
| 2015-08-21 |
Kshitij Bansal | better handling for conflicting options with nonlinear... |
commit | commitdiff | tree |
| 2015-08-21 |
Kshitij Bansal | Fix bug 649 (errors to regular output channel) |
commit | commitdiff | tree |
| 2015-08-20 |
Liana Hadarean | fix to bug659 due to algebraic solver model building |
commit | commitdiff | tree |
| 2015-08-20 |
Liana Hadarean | fix for bug660 and bug658 due to incorrect bit-blasting... |
commit | commitdiff | tree |
| 2015-08-19 |
ajreynol | Make cbqi robust to term ITE removal. Separate vts... |
commit | commitdiff | tree |
| 2015-08-19 |
Kshitij Bansal | fix bug 605 |
commit | commitdiff | tree |
| 2015-08-19 |
ajreynol | Implementation of model-based projection in cbqi, clean... |
commit | commitdiff | tree |
| 2015-08-18 |
Tianyi Liang | fix for bug663 |
commit | commitdiff | tree |
| 2015-08-16 |
ajreynol | More optimizations to --macros-quant, add --macros... |
commit | commitdiff | tree |
| 2015-08-12 |
ajreynol | Improvements to --macros-quant. Enable --clause-split... |
commit | commitdiff | tree |
| 2015-08-01 |
ajreynol | Simplification/improvement to solving deltas in LRA... |
commit | commitdiff | tree |
| 2015-08-01 |
ajreynol | Support for default grammar for datatypes in sygus... |
commit | commitdiff | tree |
| 2015-07-31 |
ajreynol | Make --fmf-fun and --macros-quant work in incremental... |
commit | commitdiff | tree |
| 2015-07-31 |
ajreynol | Sygus support for inductive datatypes. |
commit | commitdiff | tree |
| 2015-07-30 |
ajreynol | Implement virtual term substitution for non-nested... |
commit | commitdiff | tree |
| 2015-07-28 |
Tianyi Liang | Disable bug590.smt2 |
commit | commitdiff | tree |
| 2015-07-28 |
Tianyi Liang | minor change to the last fix |
commit | commitdiff | tree |
| 2015-07-28 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2015-07-28 |
Tianyi Liang | Hotfix for substr function. |
commit | commitdiff | tree |
| 2015-07-25 |
ajreynol | Add option --sygus-inv-templ for synthesizing strengthe... |
commit | commitdiff | tree |
| 2015-07-20 |
Tim King | Fix for BOOST_SED_CPP for gcc-5. |
commit | commitdiff | tree |
| 2015-07-20 |
ajreynol | Squashed merge of SygusComp 2015 branch. |
commit | commitdiff | tree |
| 2015-07-12 |
ajreynol | Add option --full-saturate-quant-rd. Fix option -... |
commit | commitdiff | tree |
| 2015-07-08 |
Kshitij Bansal | fix bug 650 |
commit | commitdiff | tree |
| 2015-07-05 |
ajreynol | Add options --partial-triggers, --elim-taut-quant,... |
commit | commitdiff | tree |
| 2015-07-02 |
ajreynol | On-demand upper bound lemmas for deltas in quantified... |
commit | commitdiff | tree |
| 2015-07-01 |
ajreynol | Add options --qcf-all-conflict, --ite-dtt-split-quant... |
commit | commitdiff | tree |
| 2015-06-30 |
Kshitij Bansal | fix sets-translate |
commit | commitdiff | tree |
| 2015-06-30 |
Kshitij Bansal | fix smt2 parameterized sort printing |
commit | commitdiff | tree |
| 2015-06-29 |
ajreynol | Module to infer alpha equivalence of quantified formula... |
commit | commitdiff | tree |
| 2015-06-27 |
ajreynol | Refactor various corner cases of fmf, quantifiers modul... |
commit | commitdiff | tree |
| 2015-06-25 |
ajreynol | Do not assert fail for fmf empty domains. Fixes bug... |
commit | commitdiff | tree |
| 2015-06-22 |
ajreynol | Add --user-pat=interleave. Remove unused lte inst strategy. |
commit | commitdiff | tree |
| 2015-06-16 |
ajreynol | Avoid completion for large finite types. Fix bug for... |
commit | commitdiff | tree |
| 2015-06-15 |
ajreynol | Make array basis term a skolem (avoids crashing in... |
commit | commitdiff | tree |
| 2015-06-15 |
Clark Barrett | Changing options for QF_AUFNIA to avoid bug |
commit | commitdiff | tree |
| 2015-06-14 |
Tim King | Fixing an assertion Constraint::assertionFringe(..... |
commit | commitdiff | tree |
| 2015-06-14 |
Tim King | Handing the case in replay where a cut is directly... |
commit | commitdiff | tree |
| 2015-06-14 |
Tim King | Fixes for shared term normalization in replay for const... |
commit | commitdiff | tree |
| 2015-06-13 |
Tim King | Turning off aggressive arith ite simplifications during... |
commit | commitdiff | tree |
| 2015-06-13 |
ajreynol | Robust check to avoid store all instantiations. Fix... |
commit | commitdiff | tree |
| 2015-06-13 |
Tim King | Changing the run script for master for the application... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog