1====================================================================== 2 3 The Yices SMT Solver. Copyright 2017 SRI International. 4 5 Yices is free software: you can redistribute it and/or modify 6 it under the terms of the GNU General Public License as published by 7 the Free Software Foundation, either version 3 of the License, or 8 (at your option) any later version. 9 10 Yices is distributed in the hope that it will be useful, 11 but WITHOUT ANY WARRANTY; without even the implied warranty of 12 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 13 GNU General Public License for more details. 14 15 You should have received a copy of the GNU General Public License 16 along with Yices. If not, see <http://www.gnu.org/licenses/>. 17 18====================================================================== 19 20 21CONTENT 22------- 23 24This distribution includes the source of Yices, documentation, 25tests, and examples. 26 27Yices 2 is developed by Bruno Dutertre and Dejan Jovanovic, at the 28Computer Science Laboratory, SRI International. To contact us, report 29a bug, or to get more information about Yices, please visit our 30website at http://yices.csl.sri.com. 31 32 33PREREQUISITES 34------------- 35 36To build Yices from the source, you need: 37 38- GCC version 4.0.x or newer (or clang 3.0 or newer) 39- gperf version 3.0 or newer 40- the GMP library version 4.1 or newer 41 42+ other standard tools: make (gnumake is required), sed, etc. 43 44 45To build the manual, you also need: 46 47- a latex installation 48- the latexmk tool 49 50 51QUICK INSTALLATION 52------------------ 53 54Do this: 55 56 ./configure 57 make 58 sudo make install 59 60This will install binaries and libraries in /usr/local/ 61You can change the installation location by giving option 62 --prefix=... to the ./configure script. 63 64For more explanations, please check doc/COMPILING. 65 66 67 68SUPPORT FOR NON-LINEAR ARITHMETIC 69--------------------------------- 70 71This release has experimental support for non-linear real arithmetic, 72but it is not enabled by default. If you want non-linear arithmetic, 73follow these instructions: 74 751) Install SRI's library for polynomial manipulation. It's available 76 on github (https://github.com/SRI-CSL/libpoly). 77 782) After you've installed libpoly, configure yices with the 79 flag '--enable-mcsat', then build Yices as usual: 80 81 ./configure --enable-mcsat 82 make 83 sudo make install 84 85 You may need to provide LDFLAGS/CPPFLAGS if ./configure fails to 86 find the libpoly library. Other options may be useful too. Try 87 ./configure --help to see what's there. 88 89 90 91WINDOWS BUILD 92------------- 93 94We recommend compiling using Cygwin. If you want a version that works 95natively on Windows (i.e., does not depend on the Cygwin DLLs), you 96can compile from Cygwin using the MinGW cross-compilers. This is 97explained in doc/COMPILING. 98 99 100DOCUMENTATION 101------------- 102 103To build the manual from the source, type 104 105 make doc 106 107This will build ./doc/manual/manual.pdf. 108 109Other documentation is in the ./doc directory: 110 111- doc/COMPILING explains the compilation process and options in detail. 112- doc/NOTES gives an overview of the source code. 113- doc/YICES-LANGUAGE explains the syntax of the Yices language, and 114 describes commands, functions, and heuristic parameters. 115 116