1

Visual Studio 2010 コンパイラを使用して、Windows 7 64 Professional 64 ビットで Z3 定理証明器を構築しようとしています。「ビルド」ディレクトリに移動してnmake. しばらくすると、次のようになります。

    cl /Fez3.exe /nologo /MD shell/datalog_frontend.obj shell/dimacs_frontend.obj shell/install_tactic.obj shell/main.obj shell/smtlib_frontend.ob
j shell/z3_log_frontend.obj api/api.lib parsers/smt/smtparser.lib tactic/portfolio/portfolio.lib tactic/ufbv/ufbv_tactic.lib tactic/smtlogics/smtlogic
_tactics.lib muz_qe/muz_qe.lib tactic/sls/sls_tactic.lib smt/tactic/smt_tactic.lib tactic/fpa/fpa.lib tactic/bv/bv_tactics.lib smt/user_plugin/user_pl
ugin.lib smt/smt.lib smt/proto_model/proto_model.lib ast/rewriter/bit_blaster/bit_blaster.lib ast/proof_checker/proof_checker.lib ast/macros/macros.li
b ast/pattern/pattern.lib parsers/smt2/smt2parser.lib cmd_context/extra_cmds/extra_cmds.lib cmd_context/cmd_context.lib solver/solver.lib tactic/aig/a
ig_tactic.lib math/subpaving/tactic/subpaving_tactic.lib nlsat/tactic/nlsat_tactic.lib tactic/arith/arith_tactics.lib sat/tactic/sat_tactic.lib tactic
/core/core_tactics.lib ast/normal_forms/normal_forms.lib ast/simplifier/simplifier.lib front_end_params/front_end_params.lib math/euclid/euclid.lib ma
th/grobner/grobner.lib parsers/util/parser_util.lib ast/substitution/substitution.lib tactic/tactic.lib model/model.lib ast/rewriter/rewriter.lib ast/
ast.lib math/subpaving/subpaving.lib math/interval/interval.lib nlsat/nlsat.lib sat/sat.lib math/polynomial/polynomial.lib util/util.lib /link /DEBUG
/MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT

shell/datalog_frontend.obj : fatal error LNK1112: Modul-Computertyp "x64" steht in Konflikt mit dem Zielcomputertyp "X86".
NMAKE : fatal error U1077: ""C:\Program Files (x86)\Microsoft Visual Studio 10.0\VC\BIN\amd64\cl.EXE"": Rückgabe-Code "0x2"
Stop.

残念ながら、エラーメッセージはドイツ語です（i18nを爆破してください、私は英語を十分に理解しており、このがらくた全体がバグハンティングを遅くするだけです）が、大まかに次のように述べています："module machine type 'x64' conflicts with target machine type 'X86'"

でコードを取得しましたgit clone https://git01.codeplex.com/z3。何をすべきかについてのヒントはありますか？

4

1 に答える 1

5

通常、このエラーは、x86 コマンド ライン環境から x64 バイナリをビルドしようとすると発生します。

次のいずれかを実行します。

  1. Z3 を 64 ビットでビルドするには: a) 64 ビットの Visual Studio コマンド ライン ウィンドウを開きます。VS ディストリビューションには、32 ビットまたは 64 ビットのいずれかのコマンドライン ウィンドウへの事前構成されたショートカットがいくつか付属しています。b) scripts\mk_make.py --x64 -b release_x64 の形式のコマンドを使用して、Z3 のビルド環境を構成します。これにより、Z3 の 64 ビット バージョンをビルドできるディレクトリ release_x64 が作成されます。c) cd release_x64 d) nmake

  2. Z3 を 32 ビットでビルドするには: a) 32 ビットの VS コマンド ライン ウィンドウを開きます。b) コマンド scripts\mk_make.py -b release_x86 を使用してビルド環境を構成します。c) cd release_x86 d) nmake

于 2013-06-22T16:16:16.173 に答える