Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Data Structures | Public Member Functions | Properties
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.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines