无法在Windows 10上安装z3

Question

我安装了很多软件包，从来没有出过问题 可能的原因？？在

车轮问题 试图编译一些东西 它在Wondershare中想要的文件不在那里

C:\Users\XXXX
λ pip install z3-solver
Collecting z3-solver
  Using cached z3-solver-4.5.1.0.post2.tar.gz
Building wheels for collected packages: z3-solver
  Running setup.py bdist_wheel for z3-solver ... error
  Complete output from command "C:\Program Files\Anaconda3\python.exe" -u -c "import setuptools, tokenize;__file__='C:\\Users\\Public\\Documents\\Wondershare\\CreatorTemp\\pip-build-uehmymoh\\z3-solver\\setup.py';f=getattr(tokenize, 'open', open)(__file__);code=f.read().replace('\r\n', '\n');f.close();exec(compile(code, __file__, 'exec'))" bdist_wheel -d C:\Users\Public\Documents\Wondershare\CreatorTemp\tmp9uv6yw5apip-wheel- --python-tag cp36:
  running bdist_wheel
  running build
  Configuring Z3
  opt = -x, arg =
  New component: 'util'
  New component: 'lp'
  New component: 'polynomial'
  New component: 'sat'
  New component: 'nlsat'
  New component: 'hilbert'
  New component: 'simplex'
  New component: 'automata'
  New component: 'interval'
  New component: 'realclosure'
  New component: 'subpaving'
  New component: 'ast'
  New component: 'rewriter'
  New component: 'normal_forms'
  New component: 'model'
  New component: 'tactic'
  New component: 'substitution'
  New component: 'parser_util'
  New component: 'grobner'
  New component: 'euclid'
  New component: 'core_tactics'
  New component: 'sat_tactic'
  New component: 'arith_tactics'
  New component: 'nlsat_tactic'
  New component: 'subpaving_tactic'
  New component: 'aig_tactic'
  New component: 'solver'
  New component: 'ackermannization'
  New component: 'interp'
  New component: 'cmd_context'
  New component: 'extra_cmds'
  New component: 'smt2parser'
  New component: 'proof_checker'
  New component: 'simplifier'
  New component: 'fpa'
  New component: 'macros'
  New component: 'pattern'
  New component: 'bit_blaster'
  New component: 'smt_params'
  New component: 'proto_model'
  New component: 'smt'
  New component: 'bv_tactics'
  New component: 'fuzzing'
  New component: 'smt_tactic'
  New component: 'sls_tactic'
  New component: 'qe'
  New component: 'duality'
  New component: 'muz'
  New component: 'dataflow'
  New component: 'transforms'
  New component: 'rel'
  New component: 'pdr'
  New component: 'clp'
  New component: 'tab'
  New component: 'bmc'
  New component: 'ddnf'
  New component: 'duality_intf'
  New component: 'fp'
  New component: 'nlsat_smt_tactic'
  New component: 'ufbv_tactic'
  New component: 'sat_solver'
  New component: 'smtlogic_tactics'
  New component: 'fpa_tactics'
  New component: 'portfolio'
  New component: 'smtparser'
  New component: 'opt'
  New component: 'api'
  New component: 'shell'
  New component: 'test'
  New component: 'api_dll'
  New component: 'dotnet'
  New component: 'java'
  New component: 'ml'
  New component: 'cpp'
  Python bindings directory was detected.
  New component: 'python'
  New component: 'python_install'
  New component: 'cpp_example'
  New component: 'z3_tptp'
  New component: 'c_example'
  New component: 'maxsat'
  New component: 'dotnet_example'
  New component: 'java_example'
  New component: 'ml_example'
  New component: 'py_example'
  Generating src\util\version.h from src\util\version.h.in
  Generated 'src\util\version.h'
  Generating src\api\dotnet\Properties\AssemblyInfo.cs from src\api\dotnet\Properties\AssemblyInfo.cs.in
  Generated 'src\api\dll\api_dll.def'
  Generated 'src\ackermannization\ackermannization_params.hpp'
  Generated 'src\ackermannization\ackermannize_bv_tactic_params.hpp'
  Generated 'src\ast\pp_params.hpp'
  Generated 'src\ast\fpa\fpa2bv_rewriter_params.hpp'
  Generated 'src\ast\normal_forms\nnf_params.hpp'
  Generated 'src\ast\pattern\pattern_inference_params_helper.hpp'
  Generated 'src\ast\rewriter\arith_rewriter_params.hpp'
  Generated 'src\ast\rewriter\array_rewriter_params.hpp'
  Generated 'src\ast\rewriter\bool_rewriter_params.hpp'
  Generated 'src\ast\rewriter\bv_rewriter_params.hpp'
  Generated 'src\ast\rewriter\fpa_rewriter_params.hpp'
  Generated 'src\ast\rewriter\poly_rewriter_params.hpp'
  Generated 'src\ast\rewriter\rewriter_params.hpp'
  Generated 'src\ast\simplifier\arith_simplifier_params_helper.hpp'
  Generated 'src\ast\simplifier\array_simplifier_params_helper.hpp'
  Generated 'src\ast\simplifier\bv_simplifier_params_helper.hpp'
  Generated 'src\interp\interp_params.hpp'
  Generated 'src\math\polynomial\algebraic_params.hpp'
  Generated 'src\math\realclosure\rcf_params.hpp'
  Generated 'src\model\model_evaluator_params.hpp'
  Generated 'src\model\model_params.hpp'
  Generated 'src\muz\base\fixedpoint_params.hpp'
  Generated 'src\nlsat\nlsat_params.hpp'
  Generated 'src\opt\opt_params.hpp'
  Generated 'src\parsers\util\parser_params.hpp'
  Generated 'src\sat\sat_asymm_branch_params.hpp'
  Generated 'src\sat\sat_params.hpp'
  Generated 'src\sat\sat_scc_params.hpp'
  Generated 'src\sat\sat_simplifier_params.hpp'
  Generated 'src\smt\params\smt_params_helper.hpp'
  Generated 'src\solver\combined_solver_params.hpp'
  Generated 'src\tactic\sls\sls_params.hpp'
  Generated 'src\tactic\smtlogics\qfufbv_tactic_params.hpp'
  Generated 'src\util\lp\lp_params.hpp'
  Generated 'src\ast\pattern\database.h'
  Generated 'src\shell\install_tactic.cpp'
  Generated 'src\test\install_tactic.cpp'
  Generated 'src\api\dll\install_tactic.cpp'
  Generated 'src\shell\mem_initializer.cpp'
  Generated 'src\test\mem_initializer.cpp'
  Generated 'src\api\dll\mem_initializer.cpp'
  Generated 'src\shell\gparams_register_modules.cpp'
  Generated 'src\test\gparams_register_modules.cpp'
  Generated 'src\api\dll\gparams_register_modules.cpp'
  Generated 'src\api\python\z3\z3consts.py
  Generated 'src\api\api_log_macros.h'
  Generated 'src\api\api_log_macros.cpp'
  Generated 'src\api\api_commands.cpp'
  Generated 'src\api\python\z3\z3core.py'
  Listing 'src\\api\\python\\z3'...
  Compiling 'src\\api\\python\\z3\\z3consts.py'...
  Compiling 'src\\api\\python\\z3\\z3core.py'...
  Generated python bytecode
  Copied 'z3consts.py'
  Copied 'z3core.py'
  Copied 'z3consts.cpython-36.pyc'
  Copied 'z3core.cpython-36.pyc'
  Testing OpenMP...
  64-bit:         True
  OpenMP:         False
  Writing build\Makefile
  Copied Z3Py example 'all_interval_series.py' to 'build\python'
  Copied Z3Py example 'example.py' to 'build\python'
  Copied Z3Py example 'socrates.py' to 'build\python'
  Copied Z3Py example 'visitor.py' to 'build\python'
  Makefile was successfully generated.
    compilation mode: Release
    platform: x64

  To build Z3, open a [Visual Studio x64 Command Prompt], then
  type 'cd C:\Users\Public\Documents\Wondershare\CreatorTemp\pip-build-uehmymoh\z3-solver\core\build && nmake'

  Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"
  Building Z3
  error: [WinError 2] The system cannot find the file specified

  ----------------------------------------
  Failed building wheel for z3-solver
  Running setup.py clean for z3-solver
Failed to build z3-solver
Installing collected packages: z3-solver
  Running setup.py install for z3-solver ... error
    Complete output from command "C:\Program Files\Anaconda3\python.exe" -u -c "import setuptools, tokenize;__file__='C:\\Users\\Public\\Documents\\Wondershare\\CreatorTemp\\pip-build-uehmymoh\\z3-solver\\setup.py';f=getattr(tokenize, 'open', open)(__file__);code=f.read().replace('\r\n', '\n');f.close();exec(compile(code, __file__, 'exec'))" install --record C:\Users\Public\Documents\Wondershare\CreatorTemp\pip-cpcgkren-record\install-record.txt --single-version-externally-managed --compile:
    running install
    running build
    Configuring Z3
    Building Z3
    error: [WinError 2] The system cannot find the file specified

    ----------------------------------------
Command ""C:\Program Files\Anaconda3\python.exe" -u -c "import setuptools, tokenize;__file__='C:\\Users\\Public\\Documents\\Wondershare\\CreatorTemp\\pip-build-uehmymoh\\z3-solver\\setup.py';f=getattr(tokenize, 'open', open)(__file__);code=f.read().replace('\r\n', '\n');f.close();exec(compile(code, __file__, 'exec'))" install --record C:\Users\Public\Documents\Wondershare\CreatorTemp\pip-cpcgkren-record\install-record.txt --single-version-externally-managed --compile" failed with error code 1 in C:\Users\Public\Documents\Wondershare\CreatorTemp\pip-build-uehmymoh\z3-solver\

C:\Users\XXXX
λ