| 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-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 |
| 2015-06-13 |
Tim King | Restricting TheoryArith to computeRelevantTerms. |
commit | commitdiff | tree |
| 2015-06-13 |
ajreynol | Disable sort inference for SMT COMP |
commit | commitdiff | tree |
| 2015-06-13 |
Clark Barrett | Fixed bug in iteSimp |
commit | commitdiff | tree |
| 2015-06-13 |
Clark Barrett | Fix for assertion failure: |
commit | commitdiff | tree |
| 2015-06-13 |
ajreynol | Fix for sort inference involving mixed Int/Real equalities. |
commit | commitdiff | tree |
| 2015-06-13 |
Tim King | A return value for an ApproxGLPK::loadVB() failure... |
commit | commitdiff | tree |
| 2015-06-13 |
ajreynol | Avoid instantiating with array constants. |
commit | commitdiff | tree |
| 2015-06-13 |
ajreynol | Ensure mkRep instantiation strategies do not violate... |
commit | commitdiff | tree |
| 2015-06-12 |
Kshitij Bansal | sync options of default-assertions run script with... |
commit | commitdiff | tree |
| 2015-06-12 |
ajreynol | Fix crash in non-linear cbqi. |
commit | commitdiff | tree |
| 2015-06-12 |
Tim King | In TheoryArithPrivate::vectorToIntHoleConflict, adding... |
commit | commitdiff | tree |
| 2015-06-12 |
ajreynol | Make sygus an output language. Parse declare-fun in... |
commit | commitdiff | tree |
| 2015-06-12 |
ajreynol | Accelerate sygus solution reconstruction for constants... |
commit | commitdiff | tree |
| 2015-06-11 |
Kshitij Bansal | remove runscripts from master meant for experimental... |
commit | commitdiff | tree |
| 2015-06-11 |
ajreynol | Avoid naming conflicts in sygus, refactor. Add missing... |
commit | commitdiff | tree |
| 2015-06-11 |
ajreynol | Handle duplicate operators in sygus grammars. Parse... |
commit | commitdiff | tree |
| 2015-06-11 |
ajreynol | Update experimental scripts. Support top-level non... |
commit | commitdiff | tree |
| 2015-06-10 |
ajreynol | Bug fix parsing constant constructor sygus. |
commit | commitdiff | tree |
| 2015-06-10 |
ajreynol | Support for printing solutions involving LetGTerm sygus... |
commit | commitdiff | tree |
| 2015-06-10 |
ajreynol | Parse support for sygus LetGTerm. |
commit | commitdiff | tree |
| 2015-06-09 |
Kshitij Bansal | bump thread stack size to 1 GB |
commit | commitdiff | tree |
| 2015-06-09 |
ajreynol | Bug fix instantiations for fmf-bound-int. Disable... |
commit | commitdiff | tree |
| 2015-06-09 |
Kshitij Bansal | make comment precise |
commit | commitdiff | tree |
| 2015-06-09 |
Kshitij Bansal | move delete beyond ifdef CVC4_COMPETITION_MODE |
commit | commitdiff | tree |
| 2015-06-05 |
Kshitij Bansal | pcvc4 with assertions |
commit | commitdiff | tree |
| 2015-06-05 |
Kshitij Bansal | update run script for assertions/scrambled run |
commit | commitdiff | tree |
| 2015-06-05 |
Kshitij Bansal | assertions runscript (for testing) derived from current... |
commit | commitdiff | tree |
| 2015-06-05 |
Kshitij Bansal | for experimental, use incremental instead of teardown... |
commit | commitdiff | tree |
| 2015-06-05 |
Kshitij Bansal | move decision to use teardown or not to logics |
commit | commitdiff | tree |
| 2015-06-04 |
ajreynol | Fix for last commit. |
commit | commitdiff | tree |
| 2015-06-04 |
Kshitij Bansal | rpl -- "--cbqi" "--cbqi --no-cbqi-sat" run-script-smtco... |
commit | commitdiff | tree |
| 2015-06-04 |
Kshitij Bansal | sync exerimental scripts with regular ones |
commit | commitdiff | tree |
| 2015-06-04 |
ajreynol | Minor changes to smt comp script for quantified arith... |
commit | commitdiff | tree |
| 2015-06-03 |
Kshitij Bansal | experimental run scripts |
commit | commitdiff | tree |
| 2015-06-03 |
Kshitij Bansal | runscript thread stack 256 |
commit | commitdiff | tree |
| 2015-06-03 |
ajreynol | Refactoring of sygus parsing, properly parse Constant... |
commit | commitdiff | tree |
| 2015-06-02 |
Kshitij Bansal | application smtcomp |
commit | commitdiff | tree |
| 2015-06-02 |
ajreynol | Flatten sygus grammars during parsing. Remove duplicate... |
commit | commitdiff | tree |
| 2015-06-02 |
ajreynol | Add casc 25 tfn script. Change tff script to output... |
commit | commitdiff | tree |
| 2015-06-01 |
ajreynol | When proof enabled, disable uf sym break. Add regression. |
commit | commitdiff | tree |
| 2015-05-29 |
ajreynol | Do not enforce dt fairness when single invocation sygus. |
commit | commitdiff | tree |
| 2015-05-29 |
lianah | changed resource step options to unsigned |
commit | commitdiff | tree |
| 2015-05-28 |
Liana Hadarean | added options for controlling resource step-count for... |
commit | commitdiff | tree |
| 2015-05-27 |
lianah | Merge pull request #75 from Dunedune/master |
commit | commitdiff | tree |
| 2015-05-25 |
ajreynol | Add missing regression |
commit | commitdiff | tree |
| 2015-05-25 |
ajreynol | Bug fix for CNF proofs (and/or case 1), thanks to Alain... |
commit | commitdiff | tree |
| 2015-05-22 |
Jordy Ruiz | Added throw LogicException to method lemma. |
commit | commitdiff | tree |
| 2015-05-15 |
ajreynol | Fixes related to cbqi + E-matching. |
commit | commitdiff | tree |
| 2015-05-15 |
ajreynol | Avoid ensureLiteral on unpreprocessed formulas in cbqi. |
commit | commitdiff | tree |
| 2015-05-13 |
ajreynol | Refactor interface for incompleteness in quantifiers... |
commit | commitdiff | tree |
| 2015-05-12 |
Clark Barrett | Added Finn Haedicke as a contributor. |
commit | commitdiff | tree |
| 2015-05-12 |
barrettcw | Merge pull request #74 from finnhaedicke/namespace_minisat |
commit | commitdiff | tree |
| 2015-05-11 |
ajreynol | Allow sygus with no syntactic restrictions for LIA... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog