summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
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-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-11Update experimental scripts. Support top-level non-terminals in sygus gramma...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-09Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization f...ajreynol
2015-06-04Minor changes to smt comp script for quantified arith. Add option --cbqi-sat...ajreynol
2015-06-03Refactoring of sygus parsing, properly parse Constant/Variable constructors.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-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-11Allow sygus with no syntactic restrictions for LIA. Add regressions.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-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-27Disambiguate namespaces in options, fix permissionsClark Barrett
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-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-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-18Farkas proof coefficients.Tim King
2015-04-17Patch for Kshitij's fix on requriePhaseTianyi Liang
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-13Making CVC4::theory::quantifiers::PrenexQuantMode public for now.Tim King
2015-04-09Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, an...ajreynol
2015-04-09Fix performance issue with variable triggers + instantiation restrictions.ajreynol
2015-04-09Bug fix negative contains cache.ajreynol
2015-04-08Make fun-def quantifiers carry the function app they define, make fun-def uti...ajreynol
2015-04-07Removing the reference to THEORY_BOOL from the equality engine. This theoryDejan Jovanovic
2015-04-07Minor fixes for cegqi.ajreynol
2015-04-02Merge pull request #71 from kbansal/const-are-triggersKshitij Bansal
2015-04-01Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun...ajreynol
2015-03-31fix no return value warningKshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback