The SC2 project arose out of the recognition that the Symbolic Computation and Satis ability Checking communities mutually bene t from the sharing of results and techniques. An SMT solver can pro t from the inclusion of computer algebra techniques in its theory solver, while a computer algebra system can pro t from dispatching SAT or SMT queries which arise as sub-problems during computation to a dedicated external solver; many existing implementations of both of these may be found. Here we describe on-going work in the second category: an API in Maple for dispatching computations to, and processing results from, an SMT solver supporting the SMT-LIB 2 format.
1.1
SC2, Maple, and SMT-LIB
The SC2 project [
The opposite task of incorporating SAT or SMT solving techniques into a
computer algebra system also has signi cant prior art. One such example from
the computer algebra system Redlog is the integration of learning strategies from
CDCL-based SMT solving into real quanti er elimination [
We describe here a interface between Maple[
The SMT-LIB 2.0 standard de nes a language for writing terms and formulas in a sorted version of rst-order logic, specifying background theories and logics, and interacting with SMT solvers in order to impose and retract assertions and inquire about their satis ability. 1.2
SMT-like Queries in Maple
Consistent with Maple's roots as a computer algebra system, its solvers (such as
solve, dsolve, int) generally seek to provide the user with 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, and its core routines make regular use of satis ability queries in the course of symbolic simpli cation.
The existing general-purpose commands in Maple for querying universal and
existential properties about a given expression are named is and coulditbe
respectively. [
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: it may be a symbol with no numeric value, an expression of arbitrary size containing such a symbol, or simply 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 is limited to those corresponding to real numbers.
An illustrative example can be found with the Maple command 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.)
This is an example of what is essentially an SMT instance appearing as a subproblem in the course of symbolic computation. Many examples of such queries may be found in the Maple library; a common pattern is to pose an is query (that is, verify that a speci ed condition holds universally) as a precondition to applying a certain transformation.
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 26 July 2017. This includes both instances in which the test case explicitly calls is/coulditbe and instances in which is/coulditbe are invoked by other library functions such as product, as shown previously.
In total, 24085 distinct is and 5771 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.
It is probable that a signi cant subset of these queries are expressible in the SMT-LIB 2 format. Explicitly dispatching such queries from Maple to an external SMT solver could o er performance improvements and permit a broader class of queries to be decided (i.e. return answers other than FAIL) than is possible with analogous existing tools in Maple. More generally, the scope of these queries serves to provide evidence that posing existential questions about the satis ability of problems over the integers and real numbers in the style of SMT is, in fact, a natural activity when doing computer algebra. 2
The Maple language is loosely-typed and permits identi ers which have not been previously de ned to be freely used in algebraic expressions, with the understanding that such identi ers represent symbolic indeterminates. Maple therefore places no requirements on the user to provide an advance declaration of the mathematical domain associated with or theory underlying the input expression. Maple does possess a facility with which additional properties about symbols may be speci ed using the commands assume or assuming. In general however the e ective interpretation of symbols is imposed by the particular command being invoked: for example, coeffs(x2^+3,x) interprets x as a transcendental element while evalc((x+I)2^) interprets x as a real number.
This overall exibility presents a signi cant obstacle to translating an arbitrary algebraic expression from Maple to SMT-LIB: we must either oblige a user to specify the SMT-LIB logic underlying the expression and the type of each symbol explicitly, or attempt to detect them. 3
We present a work-in-progress Maple package, SMTLIB, designed to facilitate interaction with an SMT solver supporting the SMT-LIB standard. This package o ers three commands: ToString, Satisfiable, and Satisfy.
The rst of these, ToString, accepts a Maple expression and returns a string output containing an SMT-LIB 2.0 script. By default, this simply asserts the truth of the expression corresponding to the Maple input and requests a satis ability check (i.e. (check-sat)). It does not explicitly invoke an SMT solver, but merely returns the input which would be sent to one if Satisfiable or Satisfy were invoked.
The SMT-LIB logic may be explicitly speci ed or inferred. In the following example, we ask about the sati ability of x2+1 = 0 while instructing ToString to use the SMT-LIB logic QF LRA (quanti er-free linear real arithmetic), implicitly forcing the variable x to be real. (Note that the input line is preceded by > and output lines follow afterwards.) > SMTLIB:-ToString( x^2+1=0, logic="QF_LRA" ); "(set-logic QF_LRA) (declare-fun x () Real) (assert (= (+ (* x x) 1) 0)) (check-sat) (exit)"
In the event that the logic is not speci ed, ToString will attempt to choose
the \smallest" SMT-LIB logic in which the input can be represented, according
to the partial order on SMT-LIB logics described in [
If we repeat the previous command while leaving the logic unspeci ed, ToString defaults to using the logic QF NIA (quanti er-free nonlinear integer arithmetic) because that is the minimal logic in which both the integer addition and the square term can be represented. > SMTLIB:-ToString( x^2+1=0 ); "(set-logic QF_NIA) (declare-fun x () Int) (assert (= (+ (* x x) 1) 0)) (check-sat) (exit)"
The Satisfiable and Satisfy commands simply generate SMT-LIB scripts
(which request a satis ability check and a satisfying witness, respectively) and
dispatch the query to an SMT solver. By specifying the path to the executable for
the SMT solver, an arbitrary SMT-LIB compliant solver may be used, though the
default implementation uses Z3 [
The following examples rst con rm that a satisfying assignment exists and then returns a satisfying assignment for the equation w3 +x3 = y3 +z3 in positive integers where w 6= y; w 6= z: The SMTLIB Maple package presents a concrete example of a computer algebra system e ectively harnessing the power of an SMT solver. The fact that its interface is su ciently generic to be uncoupled from any particular SMT solver stands as testimony to the bene t of the widespread adoption of the SMT-LIB standard by implementors of SMT solvers.
This implementation nevertheless currently leaves a considerable portion of the functionality de ned in the SMT-LIB 2 standard unexploited, including definition of new theories and use of the command language for interacting with assertions via stack push/pop operations. 5
The inclusion of the SMTLIB package in Maple provides a facility for users explicitly interested in interacting with an SMT solver. In future, we aim to examine the utility of using as a general-purpose tool for solving SMT instances which arise during evaluation of symbolic expressions.
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.
We also hope to nd ways of meaningfully incorporating other parts of the SMT-LIB 2 speci cation into the Maple interface. At present, in the case of unsatis ability users of the interface must accept a mere false or NULL; they would bene t from access to concrete evidence of unsatis ability (e.g. an unsatis able core).
The interface would also bene t from the addition of support for other existing SMT-LIB types, including { Uninterpreted functions (QF UF and logics which extend it) { Arrays { Bit vectors { Floating-point arithmetic