summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2015-06-04Minor changes to smt comp script for quantified arith. Add option --cbqi-sat...ajreynol
2015-06-03experimental run scriptsKshitij Bansal
2015-06-03runscript thread stack 256Kshitij Bansal
2015-06-03Refactoring of sygus parsing, properly parse Constant/Variable constructors.ajreynol
2015-06-02application smtcompKshitij Bansal
2015-06-02Flatten sygus grammars during parsing. Remove duplicate operators from grammars.ajreynol
2015-06-02Add casc 25 tfn script. Change tff script to output instantiations. Work tow...ajreynol
2015-06-01When proof enabled, disable uf sym break. Add regression.ajreynol
2015-05-29Do not enforce dt fairness when single invocation sygus.ajreynol
2015-05-29changed resource step options to unsignedlianah
2015-05-28added options for controlling resource step-count for various solving stagesLiana Hadarean
2015-05-27Merge pull request #75 from Dunedune/masterlianah
2015-05-25Add missing regressionajreynol
2015-05-25Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report.ajreynol
2015-05-22Added throw LogicException to method lemma.Jordy Ruiz
2015-05-15Fixes related to cbqi + E-matching.ajreynol
2015-05-15Avoid ensureLiteral on unpreprocessed formulas in cbqi.ajreynol
2015-05-13Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ...ajreynol
2015-05-12Added Finn Haedicke as a contributor.Clark Barrett
2015-05-12Merge pull request #74 from finnhaedicke/namespace_minisatbarrettcw
2015-05-11Allow sygus with no syntactic restrictions for LIA. Add regressions.ajreynol
2015-05-11Add missing regression.ajreynol
2015-05-11Support for arbitrary constants/variables in Sygus grammars.ajreynol
2015-05-10Minor improvements to infrastructure. Minor changes to default options. Add t...ajreynol
2015-05-08Add casc25 fnt script.ajreynol
2015-05-02Minor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add co...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback