問題タブ [optimathsat]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
python - Z3 最適化、厳密な不等式
以前に言及された問題があり、解決策がまったく得られません (代替と単純化の組み合わせ)。私のエンコーディングでは、厳密な不等式があり、イプシロンを 0 または非常に小さな値に設定する必要があります。たとえば、次の単純化された Python コードがあります。
p に最大値 1 を割り当てるにはどうすればよいですか? (現在は 1/2 が割り当てられています。) ありがとうございます。
z3 - モデル戻り値の z3 コントロール設定
質問: z3 でモデルの戻り値の設定を制御することはできますか?
例:次の命題論理式を考えると、2 つの可能なモデルがあります。
a: True, b: True, c: False(優先)a: True, b: False, c: True(引き続き有効、「第 2 選択」のみ)
aブール式/アサーション自体を介して、モデル whereおよびbare がモデル whereおよびareTrueよりも優先されるように制御したいと思います。ただし、追加の制約が追加されたためにそうできなかった場合は、 withおよびbeingを返す必要があります。acTruebTrueacTrue
SMT2 フォーミュラ: これは、rise4fun でテストできる SMT2 のフォーミュラの例です。
観察:節内の節の順序を実際に切り替えることによって、返されるモデルに含まれているかどうかを制御することが実際に可能であるように思われることに気付きbました。これは何らかの形で信頼できるものですか、それともこの些細な例で偶然に起こっているだけですか?cTrueandor
macos - コマンド gtime からのみ実行時間を取得する
コマンドを実行し、その実行時間を取得する必要があります。私は gtime を使用していますが、出力は私が望むものとは少し異なります。
gtime は実行結果と実行時間を返します。コマンドの出力（時間のみにする必要があります）を変数に保存し、後で使用する必要があります。コマンドを変更して実行時間のみを取得する方法はありますか?
したがって、以下のコマンドを書くと：
次に、これは私が得る出力の例です: