|
| 1 | +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
| 2 | +<html xmlns="http://www.w3.org/1999/xhtml"> |
| 3 | + <!-- #include virtual="head.shtml" --> |
| 4 | + <head> |
| 5 | + <title>SMT-LIB The Satisfiability Modulo Theories Library</title> |
| 6 | + <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> |
| 7 | + <link href="style.css" rel="stylesheet" type="text/css" /> |
| 8 | + <!-- CuFon: Enables smooth pretty custom font rendering. 100% SEO friendly. To disable, remove this section --> |
| 9 | + <script type="text/javascript" src="js/cufon-yui.js"></script> |
| 10 | + <script type="text/javascript" src="js/arial.js"></script> |
| 11 | + <script type="text/javascript" src="js/cuf_run.js"></script> |
| 12 | + <!-- CuFon ends --> |
| 13 | + <link href="code-prettify/prettify.css" type="text/css" rel="stylesheet" /> |
| 14 | + <script src="code-prettify/run_prettify.js?lang=smtlib&skin=desert"></script> |
| 15 | + </head> |
| 16 | + |
| 17 | + <body> |
| 18 | + <div class="main"> |
| 19 | + <div class="header"> |
| 20 | + <div class="header_resize"> |
| 21 | + <div class="menu_nav"> |
| 22 | + <ul> |
| 23 | + <li class="active"><a href="index.shtml">Home</a></li> |
| 24 | + <li><a href="about.shtml">About</a></li> |
| 25 | + <li><a href="news.shtml">News</a></li> |
| 26 | + <li><a href="standard.shtml">Standard</a></li> |
| 27 | + <li><a href="benchmarks.shtml">Benchmarks</a></li> |
| 28 | + <li><a href="software.shtml">Software</a></li> |
| 29 | + <li><a href="credits.shtml">Credits</a></li> |
| 30 | + </ul> |
| 31 | + </div> |
| 32 | + <!-- #include virtual="logo.shtml" --> |
| 33 | +<div class="clr"></div> |
| 34 | +<div class="logo"> |
| 35 | + <h1><a href="index.shtml">SMT-LIB <br/> |
| 36 | + <small>The Satisfiability Modulo Theories Library</small></a> |
| 37 | + </h1> |
| 38 | +</div> |
| 39 | + |
| 40 | + </div> |
| 41 | + </div> |
| 42 | + <div class="content"> |
| 43 | + <div class="content_resize"> |
| 44 | + <div class="mainbar"> |
| 45 | + <div class="article"> |
| 46 | + <p> SMT-LIB is an international initiative aimed at facilitating research and development in |
| 47 | + <a href="http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories">Satisfiability Modulo Theories</a> (SMT). Since its inception in 2003, the initiative has pursued these aims by focusing on the following concrete goals. |
| 48 | + <ul> |
| 49 | + <li>Provide standard rigorous descriptions of background theories used in SMT systems. |
| 50 | + </li> |
| 51 | + <li>Develop and promote common input and output languages for |
| 52 | + <a href="http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories#SMT_solvers">SMT solvers</a>. |
| 53 | + </li> |
| 54 | + <li>Connect developers, researchers and users of SMT, and develop a community around it. |
| 55 | + </li> |
| 56 | + <li>Establish and make available to the research community a large library of benchmarks for SMT solvers. |
| 57 | + </li> |
| 58 | + <li>Collect and promote software tools useful to the SMT community. |
| 59 | + </li> |
| 60 | + </ul> |
| 61 | + This website provides access to the following main artifacts of the initiative. |
| 62 | + <ul> |
| 63 | + <li>Documents describing the SMT-LIB input/output language for SMT solvers and its semantics; |
| 64 | + </li> |
| 65 | + <li>Specifications of background theories and <em>logics</em>; |
| 66 | + </li> |
| 67 | + <li>A large library of input problems, or benchmarks, written in the SMT-LIB language. |
| 68 | + </li> |
| 69 | + <li>Links to SMT solvers and related tools and utilities. |
| 70 | + </li> |
| 71 | + </ul> |
| 72 | + </p> |
| 73 | + </div> |
| 74 | + </div> |
| 75 | + <!-- #include virtual="sidebar.shtml" --> |
| 76 | + <div class="sidebar"> |
| 77 | + <div class="gadget"> |
| 78 | + <ul class="sb_menu"> |
| 79 | + <li><a href="index.shtml">Home</a></li> |
| 80 | + <li><a href="about.shtml">About</a></li> |
| 81 | + <li><a href="news.shtml">News</a></li> |
| 82 | + <li>Standard |
| 83 | + <ul class="ex_menu"> |
| 84 | + <li><a href="language.shtml">Language</a> |
| 85 | + <li><a href="theories.shtml">Theories</a> |
| 86 | + <li><a href="logics.shtml">Logics</a> |
| 87 | + <li><a href="examples.shtml">Examples</a> |
| 88 | + </ul> |
| 89 | + </li> |
| 90 | + <li><a href="benchmarks.shtml">Benchmarks</a></li> |
| 91 | + <li>Software |
| 92 | + <ul class="ex_menu"> |
| 93 | + <li><a href="solvers.shtml">Solvers</a></li> |
| 94 | + <li><a href="utilities.shtml">Utilities</a></li> |
| 95 | + </ul> |
| 96 | + </li> |
| 97 | + <li><a href="contact.shtml">Contact</a></li> |
| 98 | + <li><a href="related.shtml">Related</a></li> |
| 99 | + <li><a href="credits.shtml">Credits</a></li> |
| 100 | + </ul> |
| 101 | + </div> |
| 102 | + </div> |
| 103 | + |
| 104 | + </div> |
| 105 | + </div> |
| 106 | + |
| 107 | + <!-- #include virtual="bottom.shtml" --> |
| 108 | + <div class="clr"></div> |
| 109 | +<div class="fbg"> |
| 110 | + <div class="fbg_resize"> |
| 111 | + <div class="col c1"> |
| 112 | + <h3>Latest News</h3> |
| 113 | + <small>May 12, 2021</small> |
| 114 | + <p> |
| 115 | + A new release of the the SMT-LIB 2.6 reference document |
| 116 | + is now available. This is a minor release addressing a |
| 117 | + minor error in the 2021-04-02 release. |
| 118 | + </p> |
| 119 | + </div> |
| 120 | + <div class="col c2"> |
| 121 | + <h3>Previous News</h3> |
| 122 | + <small>April 2, 2021</small> |
| 123 | + <p> |
| 124 | + A new release of the SMT-LIB 2.6 reference document |
| 125 | + is now available. This is a minor release addressing a few |
| 126 | + errors in the 2017-07-18 release. |
| 127 | + </p> |
| 128 | + </div> |
| 129 | + <div class="col c3"> |
| 130 | + <h3>Older News</h3> |
| 131 | + <small>Feb 11, 2020</small> |
| 132 | + <p> |
| 133 | + A theory of Unicode character strings and regular expressions has been added |
| 134 | + to the set of <a href="theories.shtml">SMT-LIB theories</a>. |
| 135 | + </p> |
| 136 | + <a href="news.shtml#2020-01-11">[More]</a> |
| 137 | + </p> |
| 138 | + </div> |
| 139 | + </div> |
| 140 | +</div> |
| 141 | + |
| 142 | + <div class="clr"></div> |
| 143 | + <div class="footer"> |
| 144 | + <div class="footer_resize"> |
| 145 | + <!-- #include virtual="copyright.shtml" --> |
| 146 | + <p class="lf"> |
| 147 | + © Copyright The SMT-LIB Initiative <br> |
| 148 | + Based on a design by |
| 149 | + Blue <a href="http://www.bluewebtemplates.com">Web Templates</a> |
| 150 | + </p> |
| 151 | + |
| 152 | + <ul class="fmenu"> |
| 153 | + <li class="active"><a href="index.shtml">Home</a></li> |
| 154 | + <li><a href="about.shtml">About</a></li> |
| 155 | + <li><a href="news.shtml">News</a></li> |
| 156 | + <li><a href="standard.shtml">Standard</a></li> |
| 157 | + <li><a href="benchmarks.shtml">Benchmarks</a></li> |
| 158 | + <li><a href="software.shtml">Software</a></li> |
| 159 | + <li><a href="credits.shtml">Credits</a></li> |
| 160 | + </ul> |
| 161 | + <div class="clr"></div> |
| 162 | + </div> |
| 163 | + </div> |
| 164 | + </div> |
| 165 | + </body> |
| 166 | +</html> |
0 commit comments