summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2015-04-28Fix smt2 printing of fun-def. Simplification of mbqi interface.ajreynol
2015-04-27Merge branch 'master' of https://github.com/CVC4/CVC4Clark Barrett
2015-04-27Fixed problem with private/public header clashClark Barrett
2015-04-27Disambiguate namespaces in options, fix permissionsClark Barrett
2015-04-27Updating failing unit tests.Tim King
2015-04-26Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullMode...ajreynol
2015-04-24More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fm...ajreynol
2015-04-24Fix sygus parser for non-tokenized operators, reenable regression. Fix for --...ajreynol
2015-04-24Fix compiler errors due to unbalanced throw specifiers.Clark Barrett
2015-04-23Merge branch 'master' into googleClark Barrett
2015-04-23Whitespace differenceClark Barrett
2015-04-23A few more minor updates to match google repository with CVC4 repositoryClark Barrett
2015-04-23Added option for --check-unsat-cores and various core bug fixes (merge of Mor...Liana Hadarean
2015-04-22Merge pull request #73 from kbansal/parser-dont-tokenizeKshitij Bansal
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-04-21Fix file permissionsClark Barrett
2015-04-21Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.ajreynol
2015-04-21Adding an example of a tester in SMT2.Tim King
2015-04-18Farkas proof coefficients.Tim King
2015-04-17Patch for Kshitij's fix on requriePhaseTianyi Liang
2015-04-17Merge pull request #72 from kbansal/decision-requirephaseKshitij Bansal
2015-04-17moved Minisat namespace into CVC4Finn Haedicke
2015-04-16Fix option --quant-fun-wd. Add mk_starexec script to contrib.ajreynol
2015-04-16Handle (degenerate) case of synthesis conjectures for constants. Disable del...ajreynol
2015-04-16disable failing sygus testsKshitij Bansal
2015-04-16update commentKshitij Bansal
2015-04-15string parser builtinop changesKshitij Bansal
2015-04-15bv parserchanges cleanupKshitij Bansal
2015-04-15fp builtinop parser changesKshitij Bansal
2015-04-15fp reorder tokens to match other occurencesKshitij Bansal
2015-04-15THEORY_INTS parser changesKshitij Bansal
2015-04-15THEORY_REAL_INTS parser changesKshitij Bansal
2015-04-15array theory builtinopKshitij Bansal
2015-04-15cleanupKshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback