私は Z3 を初めて使用しますが、考えられるさまざまな評価に基づいて条件付きの新しい割り当てを表現する方法をまだ見つけることができませんでした。https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c#L1846の If-then-else の例では 、true または false への割り当てを行う必要があります。別の変数の可能な評価に基づいて true または false にします。これどうやってするの？
評価の例では、計算された値を使用して、後でアサーションによってチェックされるまだ評価されていない値に影響を与えたいと考えています。それで、これが新しい（評価ベースの）条件で国連評価されたモデルをコンテキストに戻す方法である場合はどうすればよいですか？つまり、最終評価なしで複合条件を実行したいのです。それは可能ですか？