式 x'=x+1 が与えられた場合、x' を y に名前変更したいと考えています。z3の使い方は？
1 に答える
2
用語を変更し、古い用語を新しいサブ用語に置き換える API 関数が多数あります。これらは、修飾子 Z3_update_term、z3_substitute、および Z3_substitute_vars を含む Modifiers セクションで説明されています (2 つのコンテキスト間で用語を移植するための Z3_translate もあります)。リンクは次のとおりです。
http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa7497c70a827db2d61ba98889fe657b5
用語を直接トラバースし、ユーティリティを記述して用語を変更することもできます。display_ast の例は、用語を再帰的にトラバースする主なケースを示しています。
http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi__ex.html#ga807b5fe0e26acdec09e52a77318208d0
于 2012-09-02T22:31:07.263 に答える