Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
using_automata_to_decide_presburger_arithmetic [2009/04/29 10:53] vkuncak |
using_automata_to_decide_presburger_arithmetic [2009/04/29 10:55] vkuncak |
||
---|---|---|---|
Line 83: | Line 83: | ||
Therefore, to check if $F$ is satisfiable, we construct $A(F)$ automaton and check whether the graph of $A(F)$ has a reachable accepting state. | Therefore, to check if $F$ is satisfiable, we construct $A(F)$ automaton and check whether the graph of $A(F)$ has a reachable accepting state. | ||
+ | **Example:** Step-by-step construction of automaton for | ||
+ | \[ | ||
+ | \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) | ||
+ | \] | ||