| 2015-09-04 |
ajreynol | Fix bugs 605 and 667. |
tree | commitdiff |
| 2015-09-02 |
Kshitij Bansal | fix regressions |
tree | commitdiff |
| 2015-09-02 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' |
tree | commitdiff |
| 2015-08-27 |
ajreynol | Modify slow regressions. |
tree | commitdiff |
| 2015-08-24 |
ajreynol | Improvements to vts in cbqi, bug fix vts for non-atomic... |
tree | commitdiff |
| 2015-08-21 |
ajreynol | Fix disequality bounds in cbqi, record literals for... |
tree | commitdiff |
| 2015-08-19 |
Kshitij Bansal | fix bug 605 |
tree | commitdiff |
| 2015-08-19 |
ajreynol | Implementation of model-based projection in cbqi, clean... |
tree | commitdiff |
| 2015-08-16 |
ajreynol | More optimizations to --macros-quant, add --macros... |
tree | commitdiff |
| 2015-08-12 |
ajreynol | Improvements to --macros-quant. Enable --clause-split... |
tree | commitdiff |
| 2015-08-01 |
ajreynol | Support for default grammar for datatypes in sygus... |
tree | commitdiff |
| 2015-07-31 |
ajreynol | Make --fmf-fun and --macros-quant work in incremental... |
tree | commitdiff |
| 2015-07-31 |
ajreynol | Sygus support for inductive datatypes. |
tree | commitdiff |
| 2015-07-30 |
ajreynol | Implement virtual term substitution for non-nested... |
tree | commitdiff |
| 2015-07-28 |
Tianyi Liang | Disable bug590.smt2 |
tree | commitdiff |
| 2015-07-28 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2015-07-25 |
ajreynol | Add option --sygus-inv-templ for synthesizing strengthe... |
tree | commitdiff |
| 2015-07-20 |
ajreynol | Squashed merge of SygusComp 2015 branch. |
tree | commitdiff |
| 2015-06-27 |
ajreynol | Refactor various corner cases of fmf, quantifiers modul... |
tree | commitdiff |
| 2015-06-11 |
ajreynol | Avoid naming conflicts in sygus, refactor. Add missing... |
tree | commitdiff |
| 2015-06-11 |
ajreynol | Handle duplicate operators in sygus grammars. Parse... |
tree | commitdiff |
| 2015-06-11 |
ajreynol | Update experimental scripts. Support top-level non... |
tree | commitdiff |
| 2015-06-10 |
ajreynol | Support for printing solutions involving LetGTerm sygus... |
tree | commitdiff |
| 2015-06-02 |
ajreynol | Flatten sygus grammars during parsing. Remove duplicate... |
tree | commitdiff |
| 2015-06-01 |
ajreynol | When proof enabled, disable uf sym break. Add regression. |
tree | commitdiff |
| 2015-05-27 |
lianah | Merge pull request #75 from Dunedune/master |
tree | commitdiff |
| 2015-05-25 |
ajreynol | Add missing regression |
tree | commitdiff |
| 2015-05-25 |
ajreynol | Bug fix for CNF proofs (and/or case 1), thanks to Alain... |
tree | commitdiff |
| 2015-05-12 |
barrettcw | Merge pull request #74 from finnhaedicke/namespace_minisat |
tree | commitdiff |
| 2015-05-11 |
ajreynol | Allow sygus with no syntactic restrictions for LIA... |
tree | commitdiff |
| 2015-05-11 |
ajreynol | Add missing regression. |
tree | commitdiff |
| 2015-05-11 |
ajreynol | Support for arbitrary constants/variables in Sygus... |
tree | commitdiff |
| 2015-05-10 |
ajreynol | Minor improvements to infrastructure. Minor changes... |
tree | commitdiff |
| 2015-04-28 |
Clark Barrett | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2015-04-28 |
Clark Barrett | Disambiguate namespaces in options, fix permissions |
tree | commitdiff |
| 2015-04-26 |
ajreynol | Bug fixes and improvements for mbqi with theory symbols... |
tree | commitdiff |
| 2015-04-24 |
ajreynol | More parser related bug fixes (define-funs-rec, declare... |
tree | commitdiff |
| 2015-04-24 |
ajreynol | Fix sygus parser for non-tokenized operators, reenable... |
tree | commitdiff |
| 2015-04-23 |
Clark Barrett | Merge branch 'master' into google |
tree | commitdiff |
| 2015-04-23 |
Clark Barrett | A few more minor updates to match google repository... |
tree | commitdiff |
| 2015-04-23 |
Liana Hadarean | Added option for --check-unsat-cores and various core... |
tree | commitdiff |
| 2015-04-22 |
Kshitij Bansal | Merge pull request #73 from kbansal/parser-dont-tokenize |
tree | commitdiff |
| 2015-04-21 |
Clark Barrett | Fix file permissions |
tree | commitdiff |
| 2015-04-21 |
ajreynol | Fix bug in fmf mbqi=fmc with arrays. Add two datatypes... |
tree | commitdiff |
| 2015-04-21 |
Tim King | Adding an example of a tester in SMT2. |
tree | commitdiff |
| 2015-04-17 |
Tianyi Liang | Patch for Kshitij's fix on requriePhase |
tree | commitdiff |
| 2015-04-17 |
Kshitij Bansal | Merge pull request #72 from kbansal/decision-requirephase |
tree | commitdiff |
| 2015-04-16 |
Kshitij Bansal | disable failing sygus tests |
tree | commitdiff |
| 2015-04-15 |
Tim King | Enabling the regression test: test/regress/regress0... |
tree | commitdiff |
| 2015-04-15 |
Tim King | Adding an example that violates an assertion during... |
tree | commitdiff |
| 2015-04-09 |
Kshitij Bansal | disable string reqressions timing out after change |
tree | commitdiff |
| 2015-04-02 |
Kshitij Bansal | Merge pull request #71 from kbansal/const-are-triggers |
tree | commitdiff |
| 2015-03-23 |
ajreynol | Parsing support for define-fun-rec/define-funs-rec. |
tree | commitdiff |
| 2015-03-10 |
ajreynol | CNF proofs. Infrastructure for preprocessing proofs... |
tree | commitdiff |
| 2015-02-26 |
ajreynol | Robust strategy for single invocation LIA synthesis... |
tree | commitdiff |
| 2015-02-13 |
ajreynol | Handle recursive singleton case for codatatypes, add... |
tree | commitdiff |
| 2015-02-06 |
Tianyi Liang | Minor clean up |
tree | commitdiff |
| 2015-02-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2015-02-06 |
Tianyi Liang | Improved string performance, thanks to Peter's benchmarks. |
tree | commitdiff |
| 2015-02-06 |
Tianyi Liang | Improved string performance, thanks to Peter's benchmarks. |
tree | commitdiff |
| 2015-01-20 |
ajreynol | Mark datatypes as sygus. Add option to normalize sygus... |
tree | commitdiff |
| 2015-01-19 |
Tim King | Adding tests for get-value output for arithmetic. |
tree | commitdiff |
| 2015-01-14 |
Morgan Deters | sygus input language and benchmark |
tree | commitdiff |
| 2015-01-11 |
Tianyi Liang | adjusted to both v2.0 and v2.5 string literals |
tree | commitdiff |
| 2015-01-09 |
Tianyi Liang | blocked unprintable characters in string literals; |
tree | commitdiff |
| 2015-01-07 |
Tianyi Liang | bug fix, thanks to Pierre's report |
tree | commitdiff |
| 2015-01-07 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-12-28 |
ajreynol | Disable prenex by default when using fmf bound int... |
tree | commitdiff |
| 2014-12-05 |
Tianyi Liang | Relaxed the constant requirement for regular expression... |
tree | commitdiff |
| 2014-12-03 |
Kshitij Bansal | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2014-11-27 |
Tianyi Liang | add intersection rewriting |
tree | commitdiff |
| 2014-11-27 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-11-21 |
ajreynol | Throw error when pattern is not list of terms. |
tree | commitdiff |
| 2014-11-21 |
ajreynol | Change default option to --inst-when=full-last-call... |
tree | commitdiff |
| 2014-11-20 |
ajreynol | Disable constants sharing in eq engine, disable hack... |
tree | commitdiff |
| 2014-11-18 |
ajreynol | Compute model basis only for fmf. Add another co-datat... |
tree | commitdiff |
| 2014-11-18 |
ajreynol | Add local theory extensions instantiation strategy... |
tree | commitdiff |
| 2014-11-11 |
Kshitij Bansal | Merge pull request #64 from mdeters/theorysets-hashset... |
tree | commitdiff |
| 2014-11-10 |
Tianyi Liang | Merge pull request #63 from mdeters/theorystrings-hashs... |
tree | commitdiff |
| 2014-11-10 |
Dejan Jovanović | Bug 593 fix: if the type is finite, it is now considere... |
tree | commitdiff |
| 2014-11-10 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-09 |
Morgan Deters | Increase stack size when running regressions (fixes... |
tree | commitdiff |
| 2014-11-09 |
ajreynol | Fix dt shared terms issue, reenable regression. |
tree | commitdiff |
| 2014-11-08 |
ajreynol | Fix bug with incremental+datatypes. Minor cleanup... |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Fix missing case in Boolean terms rewriting. (Resolves... |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Corrected fix for missing case in model postprocessor... |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Revert "Fix missing case in model postprocessor (resolv... |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Revert "Fix missing case in model postprocessor (resolv... |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Fix missing case in model postprocessor (resolves bug... |
tree | commitdiff |
| 2014-11-07 |
ajreynol | Properly distinguish which EQC to assign values in... |
tree | commitdiff |
| 2014-11-06 |
ajreynol | Reenable regression. Add (for now, disabled) changes... |
tree | commitdiff |
| 2014-11-05 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-05 |
ajreynol | More work on datatypes theory combination: fix bug... |
tree | commitdiff |
| 2014-11-01 |
ajreynol | Fix bug 592: introduce skolem for dt instantiate lemma... |
tree | commitdiff |
| 2014-11-01 |
ajreynol | Fix some mistakes in datatypes theory combination,... |
tree | commitdiff |
| 2014-10-31 |
ajreynol | Do not allow duplication of function definitions. ... |
tree | commitdiff |
| 2014-10-23 |
Morgan Deters | Parsing and infrastructure support for SMT-LIBv2.5... |
tree | commitdiff |
| next |
projects / cvc5.git / history