FuncInterp Class Reference

A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments. More...

Inheritance diagram for FuncInterp:

Data Structures
class	DecRefQueue
class	Entry
	An Entry object represents an element in the finite map used to encode a function interpretation. More...
Public Member Functions
override string	ToString ()
	A string representation of the function interpretation.
Properties
uint	NumEntries [get]
	The number of entries in the function interpretation.
Entry[]	Entries [get]
	The entries in the function interpretation.
Expr	Else [get]
	The (symbolic) `else' value of the function interpretation.
uint	Arity [get]
	The arity of the function interpretation.

---

Detailed Description

A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.

Definition at line 30 of file FuncInterp.cs.

---

Member Function Documentation

override string ToString

(

)

[inline]

A string representation of the function interpretation.

Definition at line 169 of file FuncInterp.cs.

        {
            string res = "";
            res += "[";
            foreach (Entry e in Entries)
            {
                uint n = e.NumArgs;
                if (n > 1) res += "[";
                Expr[] args = e.Args;
                for (uint i = 0; i < n; i++)
                {
                    if (i != 0) res += ", ";
                    res += args[i];
                }
                if (n > 1) res += "]";
                res += " -> " + e.Value + ", ";
            }
            res += "else -> " + Else;
            res += "]";
            return res;
        }

---

Property Documentation

uint Arity [get]

The arity of the function interpretation.

Definition at line 162 of file FuncInterp.cs.

Expr Else [get]

The (symbolic) `else' value of the function interpretation.

Definition at line 149 of file FuncInterp.cs.

Entry [] Entries [get]

The entries in the function interpretation.

Definition at line 131 of file FuncInterp.cs.

uint NumEntries [get]

The number of entries in the function interpretation.

Definition at line 123 of file FuncInterp.cs.