=Paper= {{Paper |id=Vol-1974/EAd |storemode=property |title=Integration of SMT-LIB Support into Maple |pdfUrl=https://ceur-ws.org/Vol-1974/EAd.pdf |volume=Vol-1974 |authors=Stephen Forrest |dblpUrl=https://dblp.org/rec/conf/issac/Forrest17 }} ==Integration of SMT-LIB Support into Maple== https://ceur-ws.org/Vol-1974/EAd.pdf

Integration of SMT-LIB Support into Maple

Stephen A. Forrest

Maplesoft Europe Ltd., Cambridge, UK
sforrest@maplesoft.com

Abstract. The SC2 project arose out of the recognition that the Sym-
bolic Computation and Satisfiability Checking communities mutually
benefit from the sharing of results and techniques. An SMT solver can
profit from the inclusion of computer algebra techniques in its theory
solver, while a computer algebra system can profit 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 cate-
gory: an API in Maple for dispatching computations to, and processing
results from, an SMT solver supporting the SMT-LIB 2 format.

1 Introduction
1.1 SC2 , Maple, and SMT-LIB
The SC2 project [1] was established with a mandate to promote the establish-
ment of bridges between the Symbolic Computation and Satisfiability Checking
communities in the form of common platforms and roadmaps. Applying this prin-
ciple to the software tools themselves, it is well understood that SMT solvers
can benefit substantially from incorporating computer algebra techniques such
as symbolic simplification or quantifier elimination in their theory solvers. [2]
This approach is realized in the implementation of several SMT solvers, such as
veriT [3] and SMT-RAT [4].
The opposite task of incorporating SAT or SMT solving techniques into a
computer algebra system also has significant prior art. One such example from
the computer algebra system Redlog is the integration of learning strategies from
CDCL-based SMT solving into real quantifier elimination [5].
We describe here a interface between Maple[6] and an arbitrary SMT solver
implementing the SMT-LIB 2.0 [7] format. Maple is a computer algebra system
originally developed by members of the Symbolic Computation Group in the
Faculty of Mathematics at the University of Waterloo. Since 1988, it has been
developed and commercially distributed by Maplesoft (formally Waterloo Maple
Inc.), a company based in Waterloo, Ontario, Canada, with ongoing contribu-
tions from affiliated research centres. The core Maple language is implemented
in a kernel written in C++ and much of the computational library is written
in the Maple language, though the system does employ external libraries such
as LAPACK and the GNU Multiprecision Library (GMP) for special-purpose
computations.
The SMT-LIB 2.0 standard defines a language for writing terms and formulas
in a sorted version of first-order logic, specifying background theories and logics,
and interacting with SMT solvers in order to impose and retract assertions and
inquire about their satisfiability.

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 simplification of such solutions using simplifiers based on heuristic methods
[8] is often necessary.
Nevertheless the approach of posing queries as questions about satisfiability
or requests for a satisfying witness is not unknown in Maple, and its core routines
make regular use of satisfiability queries in the course of symbolic simplification.
The existing general-purpose commands in Maple for querying universal and
existential properties about a given expression are named is and coulditbe
respectively. [9] 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 accepts identical syntax 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 analo-
gous 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 −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
Qb
to compute a symbolic formula for the product n=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 infinite, 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 infinite.)
This is an example of what is essentially an SMT instance appearing as a sub-
problem 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 specified condition holds universally) as a precondition to
applying a certain transformation.
Description is coulditbe
Queries with result true 2335 3582
Queries with result false 19020 1519
Queries with result FAIL 2730 670
Queries including addition 9849 2022
Queries including multiplication 17097 3106
Queries including equations (=), inequations (6=), and inequalities (<, ≤) 11333 4439
Queries including integer exponents ≥ 2 7965 875
Queries including complex arithmetic 6215 389
Queries with Boolean structure (¬, ∧, ∨) 564 168
Total distinct queries 24085 5771

Table 1. Distinct is and coulditbe queries encountered in a full library test run

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 approxi-
mately 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 significant subset of these queries are expressible in
the SMT-LIB 2 format. Explicitly dispatching such queries from Maple to an
external SMT solver could offer 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 satisfiability of problems over the integers and real numbers in the style of
SMT is, in fact, a natural activity when doing computer algebra.

2 Challenges
The Maple language is loosely-typed and permits identifiers which have not been
previously defined to be freely used in algebraic expressions, with the under-
standing that such identifiers represent symbolic indeterminates. Maple there-
fore 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 specified using the commands assume or assuming. In general however
the effective interpretation of symbols is imposed by the particular command
being invoked: for example, coeffs(x^ 2+3,x) interprets x as a transcendental
element while evalc((x+I)^ 2) interprets x as a real number.
This overall flexibility presents a significant obstacle to translating an arbi-
trary 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 Results
We present a work-in-progress Maple package, SMTLIB, designed to facilitate
interaction with an SMT solver supporting the SMT-LIB standard. This package
offers three commands: ToString, Satisfiable, and Satisfy.
The first 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 satisfia-
bility 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 specified or inferred. In the following
example, we ask about the satifiability of x2 +1 = 0 while instructing ToString to
use the SMT-LIB logic QF LRA (quantifier-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 specified, 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 [10]. That is it will choose
a logic which is sufficient to represent the input expression, and which will be a
sub-logic of any logic in which the input can be represented.
If we repeat the previous command while leaving the logic unspecified, ToString
defaults to using the logic QF NIA (quantifier-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 satisfiability 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 [11]. The output of the SMT solver is parsed and
returned as a corresponding Maple object: a Boolean result (for Satisfiable)
or either a satisfying assignment or the value NULL.
The following examples first confirm that a satisfying assignment exists and
then returns a satisfying assignment for the equation w3 +x3 = y 3 +z 3 in positive
integers where w 6= y, w 6= z:
> SMTLIB:-Satisfiable( {w^3+x^3=y^3+z^3, w>0,x>0,y>0,z>0,w<>y,w<>z},
logic="QF_NIA");
true

> SMTLIB:-Satisfy( {w^3+x^3=y^3+z^3, w>0,x>0,y>0,z>0,w<>y,w<>z},
logic="QF_NIA");
{w = 10, x = 9, y = 12, z = 1}

4 Conclusion
The SMTLIB Maple package presents a concrete example of a computer algebra
system effectively harnessing the power of an SMT solver. The fact that its
interface is sufficiently generic to be uncoupled from any particular SMT solver
stands as testimony to the benefit 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 defined in the SMT-LIB 2 standard unexploited, including def-
inition of new theories and use of the command language for interacting with
assertions via stack push/pop operations.

5 Future Work
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
offers better performance and meaningful answers (not FAIL) for a larger class
of such queries than existing tools in Maple.
We also hope to find ways of meaningfully incorporating other parts of the
SMT-LIB 2 specification into the Maple interface. At present, in the case of un-
satisfiability users of the interface must accept a mere false or NULL; they would
benefit from access to concrete evidence of unsatisfiability (e.g. an unsatisfiable
core).
The interface would also benefit from the addition of support for other ex-
isting SMT-LIB types, including

– Uninterpreted functions (QF UF and logics which extend it)
– Arrays
– Bit vectors
– Floating-point arithmetic

References
1. E. Ábrahám, J. Abbott, B. Becker, A.M. Bigatti, M. Brain, B. Buchberger, A.
Cimatti, J.H. Davenport M. England, P. Fontaine, S. Forrest, A. Griggio, D. Kroen-
ing, W.M. Seiler, and T. Sturm. SC2 : Satisfiability Checking Meets Symbolic Com-
putation. In: M. Kohlhase, M. Johansson, B. Miller, L. de Moura, F. Tompa, eds.,
Intelligent Computer Mathematics (Proceedings of CICM 2016), pp. 28-43, (Lec-
ture Notes in Computer Science, 9791). Springer International Publishing, 2016.
http://www.sc-square.org/Papers/CICM16.pdf.
2. Erika Ábrahám. 2015. Building Bridges between Symbolic Computation and Satis-
fiability Checking. In Proceedings of the 2015 ACM on International Symposium on
Symbolic and Algebraic Computation (ISSAC 2015). ACM, New York, NY, USA,
1-6. doi:10.1145/2755996.2756636.
3. Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal
Fontaine. (2009). veriT: An Open, Trustable and Efficient SMT-Solver. 151-156.
doi:10.1007/978-3-642-02959-2 12.
4. Florian Corzilius, Ulrich Loup, Sebastian Junges, and Erika Ábrahám. 2012. SMT-
RAT: an SMT-compliant nonlinear real arithmetic toolbox. In Proceedings of the
15th international conference on Theory and Applications of Satisfiability Test-
ing (SAT’12), Alessandro Cimatti and Roberto Sebastiani (Eds.). Springer-Verlag,
Berlin, Heidelberg, 442-448. doi:10.1007/978-3-642-31612-8 35.
5. Konstantin Korovin, Marek Kosta, Thomas Sturm. Towards Conflict-Driven Learn-
ing for Virtual Substitution. Vladimir P. Gerdt, Wolfram Koepf, Werner M. Seiler,
Evgenii V. Vorozhtsov. Computer Algebra in Scientific Computing - 16th Interna-
tional Workshop, CASC 2014, 2014, Warsaw, Poland. Springer, 8660, pp.256-270,
2014, Lecture Notes in Computer Science. doi:10.1007/978-3-319-10515-4 19.
6. Maple Programming Guide, Toronto: Maplesoft, a division of Waterloo Maple Inc.,
2005-2016.
7. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo The-
ories Library (SMT-LIB), http://www.smt-lib.org, 2016.
8. Jacques Carette. 2004. Understanding Expression Simplification. In Proceed-
ings of the 2004 International Symposium on Symbolic and Algebraic Compu-
tation, Santander, Spain (ISSAC 2004), ACM, New York, NY, USA, 72-79.
doi:10.1145/1005285.1005298.
9. The Assume Facility in Maple, Maple Online Help : The Assume Facility.
10. Logics in SMT-LIB, http://smtlib.org/logics.shtml.
11. de Moura, L. M., and Bjørner, N. Z3: an efficient SMT solver. In TACAS
(2008), vol. 4963 of Lecture Notes in Computer Science, Springer, pp. 337340.
https://github.com/Z3Prover/z3.