1

非線形の実数演算に Z3_solver を使用しています。また、ソルバーのタイムアウトを設定したいと考えています。次のコードを使用していますが、ソルバーが永久に実行されるため、タイムアウトが機能しないようです。誰でも問題を見つけるのを手伝ってもらえますか? 

  Z3_solver solver;
  cfg = Z3_mk_config();
  ctx = Z3_mk_context(cfg);

  Z3_symbol logic_symbol = Z3_mk_string_symbol(ctx, "QF_UFNRA");
  solver = Z3_mk_solver_for_logic((Z3_context)ctx, logic_symbol);
  Z3_solver_inc_ref(ctx, solver);

  Z3_params params = Z3_mk_params(ctx);  
  Z3_params_inc_ref(ctx, params);
  Z3_symbol r = Z3_mk_string_symbol(ctx, ":timeout");    
  Z3_params_set_uint(ctx, params, r, 10);
  Z3_solver_set_params(ctx, solver, params);  
  Z3_params_dec_ref(ctx, params);

  Z3_del_config(cfg);


  ....
  Z3_solver_assert(ctx,solver,pred);
  Z3_lbool b = Z3_solver_check(ctx, solver);
4

1 に答える 1

2

LinuxまたはFreeBSDでZ3を使用していますか？最近、これら2つのシステムに影響するタイマー設定の問題を修正しました（コミット：http：//z3.codeplex.com/SourceControl/changeset/9674f511b3c1）

この修正は、「進行中の作業」ブランチですでに利用可能です。を使用して取得できます

git clone https://git01.codeplex.com/z3 -b unstable

次のPythonスクリプトを使用してテストしました。ところで、「不安定な」ブランチで問題を見つけた場合は、それらを報告してください。

from z3 import *
a1, a2, t1, t2 = Reals('a1 a2 t1 t2'); 
s = SolverFor("QF_NRA")
s.add( a1 + a2 == 2,
       a1*t1 + a2*t2 == Q(2,3),
       a1*t1*t1 + a2*t2*t2 == Q(2,5),
       a1*t1*t1*t1 + a2*t2*t2*t2 == Q(2,7) )
# On my machine, I get unknown when I set the timeout to 1ms.
s.set(timeout=1) 
print s.check()

編集： Z3unstableブランチ（別名「working-in-progress」ブランチ）を構築する方法の説明は次のとおりです。

前提：Z3ソースコードをディレクトリ~/codeに配置し、システム全体のインストールは実行しないことを前提としています。

cd ~
mkdir -p code
cd code
git clone https://git01.codeplex.com/z3 -b unstable
cd z3 
python scripts/mk_make.py 
cd build 
make

ところで、マルチコアマシンを使用している場合は、次を使用してコンパイル手順を高速化できます。

make -j N

それ以外の

make

マシンのコアの数はどこNですか。

于 2012-12-19T01:25:53.460 に答える