The recognition that Symbolic Computation tools could bene t from techniques from the world of Satis ability Checking was a primary motive for the founding of the SC2 community. These bene ts would be further demonstrated by the existence of \SMT-like" queries in legacy computer algebra systems; that is, computations which seek to decide satis ability or identify a satisfying witness. The Maple CAS has been under continuous development since the 1980s and its core symbolic routines incorporate many heuristics. We describe ongoing work to compose an inventory of such \SMT-like\ queries extracted from the built-in Maple library, most of which were added long before the inclusion in Maple of explicit software links to SAT/SMT tools. Some of these queries are expressible in the SMT-LIB format using an existing logic, and it is hoped that those that are not could help inform future development of the SMT-LIB standard.
1.1
Maple
Consistent with Maple's roots as a computer algebra system, its core symbolic
solvers (such as solve, dsolve, and int) generally aim to provide a general
solution to a posed problem which is both compact and useful. Further
transformation or simpli cation of such solutions using simpli ers based on heuristic
methods [
Nevertheless the approach of posing queries as questions about satis ability
or requests for a satisfying witness is not unknown in Maple. The most obvious
example is in the commands is and coulditbe. These are the standard
generalpurpose commands in Maple for querying universal and existential properties,
respectively, about a given expression. [
The is command accepts an expression p and asks if p evaluates to the value true for every possible assignment of values to the symbols in p. The coulditbe command operates similarly but asks if there is any assignment of values to the symbols in p which could cause p to evaluate to true.
Both is and coulditbe return results in ternary logic: true, false, or FAIL. Both also make use of the \assume facility", which is a system for associating Boolean properties with symbolic variables. This provides limits on the range of possible assignments considered by is and coulditbe and is roughly analogous to a type declaration. For example, the expression is(x^2>=0) evaluates to false because there are many possible values of x which do not evaluate to nonnegative real numbers, in particular the imaginary unit p 1. By contrast, the expression is(x^2>=0) assuming x::real returns true because the range of possible values of x has been constrained to real numbers.
An illustrative example is found in the function product. In the evaluation of the expression product(f(n),n=a..b), the system seeks to compute a symbolic formula for the product Qbn=a f (n). As one can verify by inspecting the source code with showstat(product), the implementation of product computes a set of roots of f (n) and, if neither a nor b is in nite, checks whether there exists a root r such that r is an integer and a r b. If so, it returns zero as the result of the product. (Similar logic is applied if either of a or b is in nite.)
As evidence of the ubiquity of such queries, Table 1 summarizes the distinct
invocations of is and coulditbe encountered during a complete run through
Maplesoft's internal test suite for the Maple library performed on 24 April 2018.
(An investigation into an earlier version of this dataset was published in [
Note that in the above table, whenever logic L2 is an extension of logic L1, the listed results for logic L2 refer only to those queries which are expressible in L2 but not in L1. For example, the 2888 is queries expressible in QF LIA are not included among the 1449 queries expressible in QF LIRA, even though all of them are expressible in the more general logic.
In total, 24006 distinct is and 5701 distinct coulditbe queries were issued during the course of the test run. The inputs vary considerably in size and in the complexity of the underlying theory, and for both is and coulditbe approximately 11% of queries cannot be decided (i.e. return FAIL rather than true or false). A complete list of queries encountered may be viewed at https://doi.org/10.5281/zenodo.943349.
Description is Total expressible in SMT-LIB 15572
Expressible with QF LIA 2888 Expressible with QF NIA 2129 Expressible with QF LRA 1542 Expressible with QF NRA 284 Expressible with AUFLIRA 1449
Expressible with AUFNIRA 7230
Total not expressible in SMT-LIB 8434
Expressible with complex arithmetic 4134
Linear arithmetic with Gaussian integers (\QF LICA") 258 Nonlinear arithmetic with Gaussian integers (\QF NICA") 259
Linear arithmetic with complex numbers (\AUFLIRCA") 165 Nonlinear arithmetic with complex numbers (\AURNIRCA") 2728
All \special" functions 3248 Exponential functions and logarithms 461
RootOf expressions 232 RootOf with exponential and trigometric functions 231
Remaining queries with Boolean structure 599
Total distinct queries 24006 coulditbe 4690 1686 744 505 41 687 1027 1011 565 171 88 32 207 441 76 40 24 5 5701
Of the total, 15572 of the is queries and 4690 of the coulditbe queries can be assigned to one of the SMT-LIB2 prede ned logics. Of the queries which cannot be so assigned, the reasons include the use of special functions unsupported by SMT-LIB, as well as complex arithmetic. 3
Recent versions of Maple have seen the addition of explicit links to SAT and
SMT solvers: Maple 2018 is distributed with both the SAT solver MapleSAT [
An important factor in this assessment will be whether this implementation o ers better performance and meaningful answers (not FAIL) for a larger class of such queries than existing tools in Maple.