Age | Commit message (Expand) | Author |
2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol |
2015-07-12 | Add option --full-saturate-quant-rd. Fix option --register-quant-body-terms. | ajreynol |
2015-07-08 | fix bug 650 | Kshitij Bansal |
2015-07-05 | Add options --partial-triggers, --elim-taut-quant, improve robustness of --pu... | ajreynol |
2015-07-02 | On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force n... | ajreynol |
2015-07-01 | Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-qu... | ajreynol |
2015-06-30 | fix smt2 parameterized sort printing | Kshitij Bansal |
2015-06-29 | Module to infer alpha equivalence of quantified formulas. Minor clean up of ... | ajreynol |
2015-06-27 | Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de... | ajreynol |
2015-06-25 | Do not assert fail for fmf empty domains. Fixes bug 644. | ajreynol |
2015-06-22 | Add --user-pat=interleave. Remove unused lte inst strategy. | ajreynol |
2015-06-16 | Avoid completion for large finite types. Fix bug for --fmf-fun. | ajreynol |
2015-06-15 | Make array basis term a skolem (avoids crashing in fmf).smtcomp2015-stable | ajreynol |
2015-06-15 | Fixing an assertion Constraint::assertionFringe(...) to allow hasTrichotomyPr... | Tim King |
2015-06-14 | Handing the case in replay where a cut is directly in conflict with an existi... | Tim King |
2015-06-14 | Fixes for shared term normalization in replay for constraint construction. | Tim King |
2015-06-14 | Turning off aggressive arith ite simplifications during incremental solving. | Tim King |
2015-06-13 | Robust check to avoid store all instantiations. Fix prior commit for sort inf... | ajreynol |
2015-06-13 | Restricting TheoryArith to computeRelevantTerms. | Tim King |
2015-06-13 | Fixed bug in iteSimp | Clark Barrett |
2015-06-13 | Fix for assertion failure: | Clark Barrett |
2015-06-13 | Fix for sort inference involving mixed Int/Real equalities. | ajreynol |
2015-06-13 | A return value for an ApproxGLPK::loadVB() failure case was incorrect. | Tim King |
2015-06-13 | Avoid instantiating with array constants. | ajreynol |
2015-06-13 | Ensure mkRep instantiation strategies do not violate types. | ajreynol |
2015-06-12 | Fix crash in non-linear cbqi. | ajreynol |
2015-06-12 | In TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or n... | Tim King |
2015-06-12 | Make sygus an output language. Parse declare-fun in sygus. Minor improvemen... | ajreynol |
2015-06-12 | Accelerate sygus solution reconstruction for constants and id functions. Min... | ajreynol |
2015-06-11 | Avoid naming conflicts in sygus, refactor. Add missing regression. Detect St... | ajreynol |
2015-06-11 | Handle duplicate operators in sygus grammars. Parse sygus quoted literals. A... | ajreynol |
2015-06-11 | Update experimental scripts. Support top-level non-terminals in sygus gramma... | ajreynol |
2015-06-10 | Bug fix parsing constant constructor sygus. | ajreynol |
2015-06-10 | Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w... | ajreynol |
2015-06-10 | Parse support for sygus LetGTerm. | ajreynol |
2015-06-09 | Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization f... | ajreynol |
2015-06-08 | make comment precise | Kshitij Bansal |
2015-06-08 | move delete beyond ifdef CVC4_COMPETITION_MODE | Kshitij Bansal |
2015-06-04 | Minor changes to smt comp script for quantified arith. Add option --cbqi-sat... | ajreynol |
2015-06-03 | Refactoring of sygus parsing, properly parse Constant/Variable constructors. | ajreynol |
2015-06-02 | Flatten sygus grammars during parsing. Remove duplicate operators from grammars. | ajreynol |
2015-06-02 | Add casc 25 tfn script. Change tff script to output instantiations. Work tow... | ajreynol |
2015-06-01 | When proof enabled, disable uf sym break. Add regression. | ajreynol |
2015-05-29 | Do not enforce dt fairness when single invocation sygus. | ajreynol |
2015-05-29 | changed resource step options to unsigned | lianah |
2015-05-28 | added options for controlling resource step-count for various solving stages | Liana Hadarean |
2015-05-27 | Merge pull request #75 from Dunedune/master | lianah |
2015-05-25 | Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report. | ajreynol |
2015-05-22 | Added throw LogicException to method lemma. | Jordy Ruiz |
2015-05-15 | Fixes related to cbqi + E-matching. | ajreynol |