| 2015-04-22 |
Kshitij Bansal | Merge pull request #73 from kbansal/parser-dont-tokenize |
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-16 |
Kshitij Bansal | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2015-02-14 |
ajreynol | Fix unit tests. |
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-04 |
Martin Brain | Floating point infrastructure. |
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-17 |
Liana Hadarean | Resource-limiting work. |
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 |
| 2014-10-22 |
Morgan Deters | Fix bug590 regression distcheck failure from last night. |
tree | commitdiff |
| 2014-10-21 |
Clark Barrett | Fixed bug 590, added regression test |
tree | commitdiff |
| 2014-10-17 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-17 |
Morgan Deters | Remove a bad (unstable, timing-dependent) test. |
tree | commitdiff |
| 2014-10-16 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-14 |
Morgan Deters | Merge pull request #58 from mdeters/smt-attributes |
tree | commitdiff |
| 2014-10-14 |
Morgan Deters | Context-dependent expr attributes are now attached... |
tree | commitdiff |
| 2014-10-11 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-10 |
Kshitij Bansal | Merge remote-tracking branch 'origin/1.4.x' |
tree | commitdiff |
| 2014-10-10 |
Kshitij Bansal | Fix issue with shared but non-preregistered term setup... |
tree | commitdiff |
| 2014-10-09 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-07 |
Morgan Deters | Fix unit test that was broken with last commit. |
tree | commitdiff |
| 2014-10-07 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-07 |
Morgan Deters | Fix a bug in tuple-record handling. Thanks to Saumya... |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-06 |
Kshitij Bansal | fix for bug586 |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Extended parsing testcase, with constant arrays and... |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Fix native language parsing of chained-store expression... |
tree | commitdiff |
| 2014-10-04 |
Morgan Deters | Enable some old bug testcases that (maybe?) never got... |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Add some (so far trivial) regressions for constant... |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Fix unit test for ArrayStoreAll. |
tree | commitdiff |
| 2014-10-02 |
Morgan Deters | Merge branch '1.4.x'. |
tree | commitdiff |
| 2014-09-30 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-09-27 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-09-26 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-09-25 |
Morgan Deters | fix unit test for new fair datatype enumeration |
tree | commitdiff |
| 2014-09-24 |
ajreynol | Fix infinite loop in datatypes enumerator. Minor work... |
tree | commitdiff |
| 2014-09-17 |
Kshitij Bansal | Merge branch '1.4.x' while ignoring commit 8d5eb49. |
tree | commitdiff |
| 2014-09-17 |
Kshitij Bansal | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-09-17 |
ajreynol | Fix soundness bug for quantifier macros involving Int... |
tree | commitdiff |
| 2014-09-03 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' |
tree | commitdiff |
| 2014-09-03 |
ajreynol | Implement and enable --dt-var-exp-quant, cleanup trace... |
tree | commitdiff |
| 2014-08-28 |
lianah | fixing bug580 caused by bad bv inequality explanation |
tree | commitdiff |
| 2014-08-28 |
lianah | fixing bug580 caused by bad bv inequality explanation |
tree | commitdiff |
| 2014-08-23 |
Morgan Deters | Unit test fix. |
tree | commitdiff |
| next |
projects / cvc5.git / history