summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-07-05Add options --partial-triggers, --elim-taut-quant, improve robustness of --pu...ajreynol
2015-07-02On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force n...ajreynol
2015-07-01Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-qu...ajreynol
2015-06-30fix sets-translateKshitij Bansal
2015-06-30fix smt2 parameterized sort printingKshitij Bansal
2015-06-29Module to infer alpha equivalence of quantified formulas. Minor clean up of ...ajreynol
2015-06-27Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de...ajreynol
2015-06-25Do not assert fail for fmf empty domains. Fixes bug 644.ajreynol
2015-06-22Add --user-pat=interleave. Remove unused lte inst strategy.ajreynol
2015-06-16Avoid completion for large finite types. Fix bug for --fmf-fun.ajreynol
2015-06-15Make array basis term a skolem (avoids crashing in fmf).smtcomp2015-stableajreynol
2015-06-14Changing options for QF_AUFNIA to avoid bugClark Barrett
2015-06-15Fixing an assertion Constraint::assertionFringe(...) to allow hasTrichotomyPr...Tim King
2015-06-14Handing the case in replay where a cut is directly in conflict with an existi...Tim King
2015-06-14Fixes for shared term normalization in replay for constraint construction.Tim King
2015-06-14Turning off aggressive arith ite simplifications during incremental solving.Tim King
2015-06-13Robust check to avoid store all instantiations. Fix prior commit for sort inf...ajreynol
2015-06-13Changing the run script for master for the application track.Tim King
2015-06-13Restricting TheoryArith to computeRelevantTerms.Tim King
2015-06-13Disable sort inference for SMT COMPajreynol
2015-06-13Fixed bug in iteSimpClark Barrett
2015-06-13Fix for assertion failure:Clark Barrett
2015-06-13Fix for sort inference involving mixed Int/Real equalities.ajreynol
2015-06-13A return value for an ApproxGLPK::loadVB() failure case was incorrect.Tim King
2015-06-13Avoid instantiating with array constants.ajreynol
2015-06-13Ensure mkRep instantiation strategies do not violate types.ajreynol
2015-06-12sync options of default-assertions run script with defaultKshitij Bansal
2015-06-12Fix crash in non-linear cbqi.ajreynol
2015-06-12In TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or n...Tim King
2015-06-12Make sygus an output language. Parse declare-fun in sygus. Minor improvemen...ajreynol
2015-06-12Accelerate sygus solution reconstruction for constants and id functions. Min...ajreynol
2015-06-11remove runscripts from master meant for experimental submissionKshitij Bansal
2015-06-11Avoid naming conflicts in sygus, refactor. Add missing regression. Detect St...ajreynol
2015-06-11Handle duplicate operators in sygus grammars. Parse sygus quoted literals. A...ajreynol
2015-06-11Update experimental scripts. Support top-level non-terminals in sygus gramma...ajreynol
2015-06-10Bug fix parsing constant constructor sygus.ajreynol
2015-06-10Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w...ajreynol
2015-06-10Parse support for sygus LetGTerm.ajreynol
2015-06-09bump thread stack size to 1 GBKshitij Bansal
2015-06-09Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization f...ajreynol
2015-06-08make comment preciseKshitij Bansal
2015-06-08move delete beyond ifdef CVC4_COMPETITION_MODEKshitij Bansal
2015-06-05pcvc4 with assertionsKshitij Bansal
2015-06-05update run script for assertions/scrambled runKshitij Bansal
2015-06-05assertions runscript (for testing) derived from current stable (default) scriptKshitij Bansal
2015-06-05for experimental, use incremental instead of teardown for all logics for test...Kshitij Bansal
2015-06-05move decision to use teardown or not to logicsKshitij Bansal
2015-06-04Fix for last commit.ajreynol
2015-06-04rpl -- "--cbqi" "--cbqi --no-cbqi-sat" run-script-smtcomp2015{,-application}Kshitij Bansal
2015-06-04sync exerimental scripts with regular onesKshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback