 Connectivity - Maple Help

 Connectivity SMTLIB

The SMTLIB package provides support for converting Maple expressions to input in the SMT-LIB language format.

SMT-LIB is an interface language frequently used by programs designed to solve SMT (Satisfiability Modulo Theories) problems.

The SMTLIB[ToString] command converts a Maple expression into SMT-LIB input which can then be fed as input into an SMT solver program. By default, the generated SMT-LIB script performs a simple satisfiability query.

Example 1: Generate an SMT-LIB script testing whether a logical formula has a satisfying assignment (that is, an assignment of values making the formula true).

 ${\mathrm{expr}}{≔}\left({\mathrm{V1}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathrm{V3}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathrm{V2}}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({\mathrm{V2}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathrm{V3}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathrm{V1}}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({\mathrm{V3}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathrm{V1}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathrm{V2}}\right)$ (1.1)

$\mathrm{with}\left(\mathrm{SMTLIB}\right)$

 $\left[{\mathrm{ToString}}\right]$ (1.2)

 ${"\left(set-logic QF_UF\right) \left(declare-fun V1 \left(\right) Bool\right) \left(declare-fun V2 \left(\right) Bool\right) \left(declare-fun V3 \left(\right) Bool\right) \left(assert \left(and \left(or V1 V3 \left(not V2\right)\right) \left(or V2 V3 \left(not V1\right)\right) \left(or V3 \left(not V1\right) \left(not V2\right)\right)\right)\right) \left(check-sat\right) \left(exit\right)"}$ (1.3)

If an explicit satisfying assignment is desired, we can optionally generate a script requesting the SMT solver to produce one (here, a set of values for $\mathrm{V1}$, $\mathrm{V2}$, $\mathrm{V3}$ for which the formula is true).

 ${"\left(set-option :produce-models true\right) \left(set-logic QF_UF\right) \left(declare-fun V1 \left(\right) Bool\right) \left(declare-fun V2 \left(\right) Bool\right) \left(declare-fun V3 \left(\right) Bool\right) \left(assert \left(and \left(or V1 V3 \left(not V2\right)\right) \left(or V2 V3 \left(not V1\right)\right) \left(or V3 \left(not V1\right) \left(not V2\right)\right)\right)\right) \left(check-sat\right) \left(get-value \left(V1 V2 V3\right)\right) \left(exit\right)"}$ (1.4)

In addition to Boolean-valued variables, SMT-LIB variables may also be numeric. The generated SMT-LIB requests a nontrivial solution in positive integers to the equation ${w}^{3}+{x}^{3}={y}^{3}+{z}^{3}$. (When such a solution exists, the integer ${w}^{3}+{x}^{3}$ is known as a taxicab number, the smallest of which is 1729.)

 ${"\left(set-option :produce-models true\right) \left(set-logic QF_NIA\right) \left(declare-fun w \left(\right) Int\right) \left(declare-fun x \left(\right) Int\right) \left(declare-fun y \left(\right) Int\right) \left(declare-fun z \left(\right) Int\right) \left(assert \left(and \left(= \left(+ \left(* w w w\right) \left(* x x x\right)\right) \left(+ \left(* y y y\right) \left(* z z z\right)\right)\right) \left(distinct w y\right) \left(distinct w z\right) \left(< 0 w\right) \left(< 0 x\right) \left(< 0 y\right) \left(< 0 z\right)\right)\right) \left(check-sat\right) \left(get-value \left(w x y z\right)\right) \left(exit\right)"}$ (1.5) URL

The existing URL package has been extended with three new commands: URL[Delete], URL[Head], and URL[Put]. These correspond directly to the HTTP (Hypertext Transfer Protocol) commands DELETE, HEAD, and PUT, respectively.

The inclusion of Delete, Head, and Put in the URL package, along with the existing URL[Get] and URL[Post], enables Maple code to make use of REST (REpresentational State Transfer) web interfaces. These interfaces offer access and manipulation of online resources by use of a uniform set of stateless operations based on HTTP.

Example: The Head command issues an HTTP HEAD request. This requests a response from the server identical to that of a GET request, but without the body of the response. Among many other uses, this command may be used to confirm that a remote server is online and accepting requests.

$\mathrm{with}\left(\mathrm{URL}\right)$

 $\left[{\mathrm{Construct}}{,}{\mathrm{Delete}}{,}{\mathrm{Escape}}{,}{\mathrm{Get}}{,}{\mathrm{Head}}{,}{\mathrm{Parse}}{,}{\mathrm{Post}}{,}{\mathrm{Put}}{,}{\mathrm{Unescape}}\right]$ (2.1)

 ${table}{}\left(\left[{"Date"}{=}{"Mon, 23 Jan 2017 22:17:11 GMT"}{,}{"X-Powered-By"}{=}{"ASP.NET"}{,}{"X-AspNet-Version"}{=}{"2.0.50727"}{,}{"Cache-Control"}{=}{"private"}{,}{"Content-Length"}{=}{"53676"}{,}{"Content-Type"}{=}{"text/html; charset=utf-8"}{,}{"Set-Cookie"}{=}{"ASP.NET_SessionId=b0eexnvcsrscup45x14dftid; path=/; HttpOnly"}{,}{"Server"}{=}{"Microsoft-IIS/8.5"}\right]\right){,}{""}{,}{200}$ (2.2) YAML

The new YAML package allows import and export of files and strings in the YAML format, a lightweight file format for exchanging structured data.
The commands YAML[ParseFile] and YAML[ParseString] parse YAML files and strings, respectively, to Maple expressions. The inverse operation, conversion of Maple structures to YAML, is provided by YAML[ToString].

The general-purpose commands Import and Export have also been extended to support YAML.

 ${T}{≔}{table}{}\left(\left[{"address"}{=}{table}{}\left(\left[{"city"}{=}{"Waterloo"}{,}{"country"}{=}{"Canada"}{,}{"province"}{=}{"ON"}{,}{"streetAddress"}{=}{"615 Kumpf Drive"}{,}{"postalCode"}{=}{"N2V 1K8"}\right]\right){,}{"companyName"}{=}{"Maplesoft"}{,}{"phoneNumbers"}{=}\left[{table}{}\left(\left[{"type"}{=}{"local"}{,}{"number"}{=}{"+1 \left(519\right) 747-2373"}\right]\right){,}{table}{}\left(\left[{"type"}{=}{"toll-free"}{,}{"number"}{=}{"+1 \left(800\right) 267-6583"}\right]\right){,}{table}{}\left(\left[{"type"}{=}{"fax"}{,}{"number"}{=}{"+1 \left(519\right) 747-5284"}\right]\right)\right]{,}{"founded"}{=}{1988}\right]\right)$ (3.1)
$T\left["companyName"\right]$
 ${"Maplesoft"}$ (3.2)
 ${"Waterloo"}{,}{"Canada"}$ (3.3)