next up previous
Next: 5.1 Current limitations Up: The Omega Calculator Previous: 4 Code Generation

5 Presburger Arithmetic with Uninterpreted Function Symbols

The Omega Calculator allows certain restricted uses of uninterpreted function symbols in a Presburger formula. Functions may be declared in the symbolic statement as

symbolic Function ( Arity)
where Function is the function name and Arity is its number of arguments. Functions of arity 0 are symbolic constants.

Functions may only be applied to a prefix of the input or output tuple of a relation, or a prefix of the tuple of a set. The function application may list the names of the argument variables explicitly ( not yet supported), or use the abbreviations Function( In), Function( Out), and Function( Set), to describe the application of a function to the appropriate length prefix of the desired tuple.

Our system relies on the following observation: Consider a formula F that contains references and , where i and j are free in F. Let be F with and substituted for and . F if satisfiable iff is satisfiable. For more details, see [Sho79].

Presburger Arithmetic with uninterpreted function symbols is in general undecidable, so in some circumstances we will have to produce approximate results (as we do with the transitive closure operation) [KPRS95].

The following examples show some legal uses of uninterpreted function symbols in the Omega Calculator:

# symbolic p(2), n, m;
# 
# R  := { [ir,jr] : 1 <= ir <= n && 1 <= jr <= m };
# 
# W1 := { [iw,jw] : 1 <= iw <= n && 1 <= jw <= m && p(Set) >= 0 };
# 
# W2 := { [iw,jw] : 1 <= iw <= n && 1 <= jw <= m && p(Set) <  0 };
# 
# Exposed := R intersection complement ( W1 union W2 );
# 
# Exposed;

{[In_1,In_2]  : FALSE }

# 
# 
# symbolic f(1);
# 
# R1 := { [i] -> [j] : 1 <= i = j <= 100 && f(In) <= f(Out)};
# 
# R2 := { [i] -> [j] : 1 <= i <= j <= 100 && f(In) = f(Out)};
# 
# 
# R1 intersection R2;

{[i] -> [i] : 1 <= i <= 100}

# 
# R1 union R2;

{[i] -> [j] : f(j) = f(i) && 1 <= i < j <= 100} union
 {[i] -> [i] : 1 <= i <= 100}

# 
# R1 intersection complement R2;

{[i] -> [j]  : FALSE }

# 
# R1;

{[i] -> [i] : 1 <= i <= 100}





omega@cs.umd.edu