| 2015-06-11 |
ajreynol | Avoid naming conflicts in sygus, refactor. Add missing... |
commit | commitdiff | tree |
| 2015-06-11 |
ajreynol | Handle duplicate operators in sygus grammars. Parse... |
commit | commitdiff | tree |
| 2015-06-11 |
ajreynol | Update experimental scripts. Support top-level non... |
commit | commitdiff | tree |
| 2015-06-10 |
ajreynol | Bug fix parsing constant constructor sygus. |
commit | commitdiff | tree |
| 2015-06-10 |
ajreynol | Support for printing solutions involving LetGTerm sygus... |
commit | commitdiff | tree |
| 2015-06-10 |
ajreynol | Parse support for sygus LetGTerm. |
commit | commitdiff | tree |
| 2015-06-09 |
Kshitij Bansal | bump thread stack size to 1 GB |
commit | commitdiff | tree |
| 2015-06-09 |
ajreynol | Bug fix instantiations for fmf-bound-int. Disable... |
commit | commitdiff | tree |
| 2015-06-09 |
Kshitij Bansal | make comment precise |
commit | commitdiff | tree |
| 2015-06-09 |
Kshitij Bansal | move delete beyond ifdef CVC4_COMPETITION_MODE |
commit | commitdiff | tree |
| 2015-06-05 |
Kshitij Bansal | pcvc4 with assertions |
commit | commitdiff | tree |
| 2015-06-05 |
Kshitij Bansal | update run script for assertions/scrambled run |
commit | commitdiff | tree |
| 2015-06-05 |
Kshitij Bansal | assertions runscript (for testing) derived from current... |
commit | commitdiff | tree |
| 2015-06-05 |
Kshitij Bansal | for experimental, use incremental instead of teardown... |
commit | commitdiff | tree |
| 2015-06-05 |
Kshitij Bansal | move decision to use teardown or not to logics |
commit | commitdiff | tree |
| 2015-06-04 |
ajreynol | Fix for last commit. |
commit | commitdiff | tree |
| 2015-06-04 |
Kshitij Bansal | rpl -- "--cbqi" "--cbqi --no-cbqi-sat" run-script-smtco... |
commit | commitdiff | tree |
| 2015-06-04 |
Kshitij Bansal | sync exerimental scripts with regular ones |
commit | commitdiff | tree |
| 2015-06-04 |
ajreynol | Minor changes to smt comp script for quantified arith... |
commit | commitdiff | tree |
| 2015-06-03 |
Kshitij Bansal | experimental run scripts |
commit | commitdiff | tree |
| 2015-06-03 |
Kshitij Bansal | runscript thread stack 256 |
commit | commitdiff | tree |
| 2015-06-03 |
ajreynol | Refactoring of sygus parsing, properly parse Constant... |
commit | commitdiff | tree |
| 2015-06-02 |
Kshitij Bansal | application smtcomp |
commit | commitdiff | tree |
| 2015-06-02 |
ajreynol | Flatten sygus grammars during parsing. Remove duplicate... |
commit | commitdiff | tree |
| 2015-06-02 |
ajreynol | Add casc 25 tfn script. Change tff script to output... |
commit | commitdiff | tree |
| 2015-06-01 |
ajreynol | When proof enabled, disable uf sym break. Add regression. |
commit | commitdiff | tree |
| 2015-05-29 |
ajreynol | Do not enforce dt fairness when single invocation sygus. |
commit | commitdiff | tree |
| 2015-05-29 |
lianah | changed resource step options to unsigned |
commit | commitdiff | tree |
| 2015-05-28 |
Liana Hadarean | added options for controlling resource step-count for... |
commit | commitdiff | tree |
| 2015-05-27 |
lianah | Merge pull request #75 from Dunedune/master |
commit | commitdiff | tree |
| 2015-05-25 |
ajreynol | Add missing regression |
commit | commitdiff | tree |
| 2015-05-25 |
ajreynol | Bug fix for CNF proofs (and/or case 1), thanks to Alain... |
commit | commitdiff | tree |
| 2015-05-22 |
Jordy Ruiz | Added throw LogicException to method lemma. |
commit | commitdiff | tree |
| 2015-05-15 |
ajreynol | Fixes related to cbqi + E-matching. |
commit | commitdiff | tree |
| 2015-05-15 |
ajreynol | Avoid ensureLiteral on unpreprocessed formulas in cbqi. |
commit | commitdiff | tree |
| 2015-05-13 |
ajreynol | Refactor interface for incompleteness in quantifiers... |
commit | commitdiff | tree |
| 2015-05-12 |
Clark Barrett | Added Finn Haedicke as a contributor. |
commit | commitdiff | tree |
| 2015-05-12 |
barrettcw | Merge pull request #74 from finnhaedicke/namespace_minisat |
commit | commitdiff | tree |
| 2015-05-11 |
ajreynol | Allow sygus with no syntactic restrictions for LIA... |
commit | commitdiff | tree |
| 2015-05-11 |
ajreynol | Add missing regression. |
commit | commitdiff | tree |
| 2015-05-11 |
ajreynol | Support for arbitrary constants/variables in Sygus... |
commit | commitdiff | tree |
| 2015-05-10 |
ajreynol | Minor improvements to infrastructure. Minor changes... |
commit | commitdiff | tree |
| 2015-05-08 |
ajreynol | Add casc25 fnt script. |
commit | commitdiff | tree |
| 2015-05-02 |
ajreynol | Minor fix for corner cases of fmf-fun, fix for --dt... |
commit | commitdiff | tree |
| 2015-04-28 |
ajreynol | Fix smt2 printing of fun-def. Simplification of mbqi... |
commit | commitdiff | tree |
| 2015-04-28 |
Clark Barrett | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2015-04-28 |
Clark Barrett | Fixed problem with private/public header clash |
commit | commitdiff | tree |
| 2015-04-28 |
Clark Barrett | Disambiguate namespaces in options, fix permissions |
commit | commitdiff | tree |
| 2015-04-27 |
Tim King | Updating failing unit tests. |
commit | commitdiff | tree |
| 2015-04-26 |
ajreynol | Bug fixes and improvements for mbqi with theory symbols... |
commit | commitdiff | tree |
| 2015-04-24 |
ajreynol | More parser related bug fixes (define-funs-rec, declare... |
commit | commitdiff | tree |
| 2015-04-24 |
ajreynol | Fix sygus parser for non-tokenized operators, reenable... |
commit | commitdiff | tree |
| 2015-04-24 |
Clark Barrett | Fix compiler errors due to unbalanced throw specifiers. |
commit | commitdiff | tree |
| 2015-04-23 |
Clark Barrett | Merge branch 'master' into google |
commit | commitdiff | tree |
| 2015-04-23 |
Clark Barrett | Whitespace difference |
commit | commitdiff | tree |
| 2015-04-23 |
Clark Barrett | A few more minor updates to match google repository... |
commit | commitdiff | tree |
| 2015-04-23 |
Liana Hadarean | Added option for --check-unsat-cores and various core... |
commit | commitdiff | tree |
| 2015-04-22 |
Kshitij Bansal | Merge pull request #73 from kbansal/parser-dont-tokenize |
commit | commitdiff | tree |
| 2015-04-21 |
Clark Barrett | Changes needed to compile at Google, plus some bug... |
commit | commitdiff | tree |
| 2015-04-21 |
Clark Barrett | Fix file permissions |
commit | commitdiff | tree |
| 2015-04-21 |
ajreynol | Fix bug in fmf mbqi=fmc with arrays. Add two datatypes... |
commit | commitdiff | tree |
| 2015-04-21 |
Tim King | Adding an example of a tester in SMT2. |
commit | commitdiff | tree |
| 2015-04-18 |
Tim King | Farkas proof coefficients. |
commit | commitdiff | tree |
| 2015-04-17 |
Tianyi Liang | Patch for Kshitij's fix on requriePhase |
commit | commitdiff | tree |
| 2015-04-17 |
Kshitij Bansal | Merge pull request #72 from kbansal/decision-requirephase |
commit | commitdiff | tree |
| 2015-04-17 |
Finn Haedicke | moved Minisat namespace into CVC4 |
commit | commitdiff | tree |
| 2015-04-16 |
ajreynol | Fix option --quant-fun-wd. Add mk_starexec script... |
commit | commitdiff | tree |
| 2015-04-16 |
ajreynol | Handle (degenerate) case of synthesis conjectures for... |
commit | commitdiff | tree |
| 2015-04-16 |
Kshitij Bansal | disable failing sygus tests |
commit | commitdiff | tree |
| 2015-04-16 |
Kshitij Bansal | update comment |
commit | commitdiff | tree |
| 2015-04-16 |
Kshitij Bansal | string parser builtinop changes |
commit | commitdiff | tree |
| 2015-04-16 |
Kshitij Bansal | bv parserchanges cleanup |
commit | commitdiff | tree |
| 2015-04-16 |
Kshitij Bansal | fp builtinop parser changes |
commit | commitdiff | tree |
| 2015-04-16 |
Kshitij Bansal | fp reorder tokens to match other occurences |
commit | commitdiff | tree |
| 2015-04-16 |
Kshitij Bansal | THEORY_INTS parser changes |
commit | commitdiff | tree |
| 2015-04-16 |
Kshitij Bansal | THEORY_REAL_INTS parser changes |
commit | commitdiff | tree |
| 2015-04-16 |
Kshitij Bansal | array theory builtinop |
commit | commitdiff | tree |
| 2015-04-16 |
Kshitij Bansal | cleanup |
commit | commitdiff | tree |
| 2015-04-16 |
Kshitij Bansal | dont tokenize bv operators (normal ones) |
commit | commitdiff | tree |
| 2015-04-15 |
Tim King | Enabling the regression test: test/regress/regress0... |
commit | commitdiff | tree |
| 2015-04-15 |
Clark Barrett | Fix for unconstrained bug. |
commit | commitdiff | tree |
| 2015-04-15 |
Tim King | Adding an example that violates an assertion during... |
commit | commitdiff | tree |
| 2015-04-13 |
Tim King | Making CVC4::theory::quantifiers::PrenexQuantMode publi... |
commit | commitdiff | tree |
| 2015-04-09 |
Kshitij Bansal | disable string reqressions timing out after change |
commit | commitdiff | tree |
| 2015-04-09 |
Kshitij Bansal | DE requests respect requirePhase |
commit | commitdiff | tree |
| 2015-04-09 |
ajreynol | Fix unsat-core issues related to rewrite rules, quantif... |
commit | commitdiff | tree |
| 2015-04-09 |
ajreynol | Fix performance issue with variable triggers + instanti... |
commit | commitdiff | tree |
| 2015-04-09 |
ajreynol | Bug fix negative contains cache. |
commit | commitdiff | tree |
| 2015-04-08 |
ajreynol | Make fun-def quantifiers carry the function app they... |
commit | commitdiff | tree |
| 2015-04-08 |
Dejan Jovanovic | Removing the reference to THEORY_BOOL from the equality... |
commit | commitdiff | tree |
| 2015-04-07 |
ajreynol | Minor fixes for cegqi. |
commit | commitdiff | tree |
| 2015-04-02 |
Kshitij Bansal | Merge pull request #71 from kbansal/const-are-triggers |
commit | commitdiff | tree |
| 2015-04-01 |
ajreynol | Improvements and bug fixes related to cbqi/cegqi. ... |
commit | commitdiff | tree |
| 2015-03-31 |
Kshitij Bansal | fix no return value warning |
commit | commitdiff | tree |
| 2015-03-31 |
Kshitij Bansal | fix echo command in --tear-down-incremental |
commit | commitdiff | tree |
| 2015-03-28 |
Tianyi Liang | printer change for string smtlib2 |
commit | commitdiff | tree |
| 2015-03-25 |
Kshitij Bansal | change const are triggers from false to true in equalit... |
commit | commitdiff | tree |
| 2015-03-23 |
ajreynol | Parsing support for define-fun-rec/define-funs-rec. |
commit | commitdiff | tree |
| 2015-03-23 |
ajreynol | Decouple counter-example guided quantifier instantiatio... |
commit | commitdiff | tree |
| 2015-03-16 |
Tianyi Liang | Add requirePhase len(x) = 0. |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog