mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix #2131

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-10 10:07:24 -08:00
parent 24dfdfe9bc
commit c5df6ce96e
3 changed files with 5 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/api/python/README.txt
View file

@ -1,8 +1,4 @@
You can learn more about Z3Py at: On Windows, to build Z3, you should executed the following command
http://rise4fun.com/Z3Py/tutorial/guide
On Windows, you must build Z3 before using Z3Py.
To build Z3, you should executed the following command
in the Z3 root directory at the Visual Studio Command Prompt in the Z3 root directory at the Visual Studio Command Prompt
msbuild /p:configuration=external msbuild /p:configuration=external
@ -12,8 +8,8 @@ If you are using a 64-bit Python interpreter, you should use
msbuild /p:configuration=external /p:platform=x64 msbuild /p:configuration=external /p:platform=x64
On Linux and macOS, you must install Z3Py, before trying example.py. On Linux and macOS, you must install python bindings, before trying example.py.
To install Z3Py on Linux and macOS, you should execute the following To install python on Linux and macOS, you should execute the following
command in the Z3 root directory command in the Z3 root directory
sudo make install-z3py sudo make install-z3py

2
src/api/python/setup.py
View file

@ -178,7 +178,7 @@ setup(
name='z3-solver', name='z3-solver',
version=_z3_version(), version=_z3_version(),
description='an efficient SMT solver library', description='an efficient SMT solver library',
long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compiliation, or installation, please submit issues to https://github.com/angr/angr-z3', long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compilation, or installation, please submit issues to https://github.com/angr/angr-z3',
author="The Z3 Theorem Prover Project", author="The Z3 Theorem Prover Project",
maintainer="Audrey Dutcher", maintainer="Audrey Dutcher",
maintainer_email="audrey@rhelmot.io", maintainer_email="audrey@rhelmot.io",

2
src/ast/recfun_decl_plugin.h
View file

@ -56,7 +56,7 @@ namespace recfun {
friend class def; friend class def;
func_decl_ref m_pred; //<! predicate used for this case func_decl_ref m_pred; //<! predicate used for this case
expr_ref_vector m_guards; //<! conjunction that is equivalent to this case expr_ref_vector m_guards; //<! conjunction that is equivalent to this case
expr_ref m_rhs; //<! if guard is true, `f(t1…tn) = rhs` holds expr_ref m_rhs; //<! if guard is true, `f(t1...tn) = rhs` holds
def * m_def; //<! definition this is a part of def * m_def; //<! definition this is a part of
bool m_immediate; //<! does `rhs` contain no defined_fun/case_pred? bool m_immediate; //<! does `rhs` contain no defined_fun/case_pred?