Age | Commit message (Expand) | Author |
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 |
2015-05-15 | Avoid ensureLiteral on unpreprocessed formulas in cbqi. | ajreynol |
2015-05-13 | Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ... | ajreynol |
2015-05-12 | Merge pull request #74 from finnhaedicke/namespace_minisat | barrettcw |
2015-05-11 | Allow sygus with no syntactic restrictions for LIA. Add regressions. | ajreynol |
2015-05-11 | Support for arbitrary constants/variables in Sygus grammars. | ajreynol |
2015-05-10 | Minor improvements to infrastructure. Minor changes to default options. Add t... | ajreynol |
2015-05-02 | Minor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add co... | ajreynol |
2015-04-28 | Fix smt2 printing of fun-def. Simplification of mbqi interface. | ajreynol |
2015-04-27 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Clark Barrett |
2015-04-27 | Fixed problem with private/public header clash | Clark Barrett |
2015-04-27 | Disambiguate namespaces in options, fix permissions | Clark Barrett |
2015-04-26 | Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullMode... | ajreynol |
2015-04-24 | More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fm... | ajreynol |
2015-04-24 | Fix sygus parser for non-tokenized operators, reenable regression. Fix for --... | ajreynol |
2015-04-24 | Fix compiler errors due to unbalanced throw specifiers. | Clark Barrett |
2015-04-23 | Merge branch 'master' into google | Clark Barrett |
2015-04-23 | A few more minor updates to match google repository with CVC4 repository | Clark Barrett |
2015-04-23 | Added option for --check-unsat-cores and various core bug fixes (merge of Mor... | Liana Hadarean |
2015-04-22 | Merge pull request #73 from kbansal/parser-dont-tokenize | Kshitij Bansal |
2015-04-21 | Changes needed to compile at Google, plus some bug fixes from Google. | Clark Barrett |
2015-04-21 | Fix file permissions | Clark Barrett |
2015-04-21 | Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions. | ajreynol |