Top Constraints
French French German German ItalianItalian SpanishSpanish PortuguesePortuguese JapaneseJapanese KoreanKorean ChineseChinese

Runtime Library


Polymorphic Predicates



The runtime library (F1RTL.DLL) contains routines used directly by the FormulaOne compiler, but also several user accessible APIs. Available APIs can be viewed by expanding the F1RTL.DLL tree in the "Modules" tab.

Standard polymorphic predicates are described here as well. For each polymorfic predicate several different predicate declarations are given, each of which corresponds to a particular behaviour of the predicate. These declarations are really pseudo-code, only to indicate approximately how FormulaOne treats the predicates.
Note: You need FormulaOne compiler release 41C or later for _AllDifferent, _AllAscending, _AllDescending, _Ascending, _Descendig.
You need FormulaOne compiler release 42A or later for RtlIsPowerOf2 and RtlSquareRoot.

Print

Print acts as a procedure with any number of input parameters, of any types Tl to Tn:
proc Print(x1 :< Tl, ..., xn :< Tn)
The type information is used by Print to determine how it should print the arguments - as strings, arrays, tuples, etc.


Len

Len acts as each of the following predicates and procedures, for any type T:
proc Len(a :< [0..n]->T, len :> I) 
pred Len(a :: [0..n]->T, len :> I)
proc Len(a :< [0..]->T, len :> I) 
pred Len(a :: [0..]->T, len :> I)
proc Len(s :< S, len :> I)
proc Len(l :< list T, len :> I)
pred Len(l :: list T, len :: I)
With arrays, Len returns the number of elements in the array (recall that flexible arrays ave a known number of elements at run time, and that while the elements of symbolic arrays may be unknown, the number of elements is always known). With strings, Len returns the length of the string. With lists, Len returns the number of elements in the list, not counting Nil. The symbolic list predicate form of Len behaves exactly as the following predicate, for every T:
pred Len(l :: list T, len :: I) iff
    len = 0 & l =  Nil |
    len > 0 &
    l = (_,t) & Lent(t, len-1)


Append

Append acts as each of the following procedures and predicates, for every T:
proc Append(s1 :< S, s2 :< S, s_out :> S)
proc Append(l1 :< list T, l2 :< list T, l_out :> list T)
pred Append(l1 :: list T, l2 :: list T, l_out :: list T)
Append returns the string or list consisting of the concatenation of the first two parameters in its call. The last version of Append behaves exactly as the following predicate, for every T:
pred Append (l1 :: list T, l2 :: list T, l_out :: list T) iff
    l1 = Nil & l_out = l2 | l1 = (h, t) &
    l_out = (h, l_aux)
    & Append(t, l2, l aux)

in

The in operator is not exactly a predicate, but it behaves in a polymorphic way which is similar to that of the polymorphic predicate. If we think of every formula of the form xl in x2 as being a call to a predicate In(xl, x2), then this predicate In acts as each of the following predicates, for every T:
proc In(x :< T,	l :< list T)
pred In(x :> T,	l :< list T)
pred In(x :: T,	l :: list T)
proc In(pat :< S, s :< S)
The first list predicate form has the effect of testing the membership of x in l. The second form assigns to x each of the members of l on backtracking. The third form behaves exactly as the following predicate, for every T:
pred In(x :: T, l :: list T) iff
    l = (h, t) & ( h = x | In(x, t))
The form with string-typed arguments is a pattern matching form, which matches the wild-card character "*" to any sequence of text (possibly empty), and any other characters to themselves. For instance, all the following formulas should be true: '*a*a' in 'lava' '*a*a' in 'ada' '*a*a' in 'llama' \ '*ula*' in 'FormulaOne' '*log*' in 'Prolog'

Dupl

Dupl acts as a procedure of the following form, for every type T:
proc Dupl(n :< I, x :< T, array :> [0..]->T)
It has the effect of putting into array, an array constructed of n copies of the value x.

_AllDifferent

_AllDifferent acts as a predicate with any number of logical parameters, for every type T:
pred _AllDifferent(x1::T, x2::T, x3::T, ..., xn::T)
The _AllDifferent predicate places n(n-1)/2 binary constraints on n variables, ensuring no two variables can have the same value.
pred _AllDifferent(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 <> x2 & x1 <> x3 & ... x1 <> xn &
               x2 <> x3 & ... x2 <> xn &
                              x3 <> xn      
For example, the following query
    all x::[1..2] & y::[1..4] & z ::I[1..2] & _AllDifferent(x,y,z)
will generate the following solutions:
x = 2
y = 3
z = 1
___ Solution: 1 __________________________________

x = 2
y = 4
z = 1
___ Solution: 2 __________________________________

x = 1
y = 3
z = 2
___ Solution: 3 __________________________________

x = 1
y = 4
z = 2
___ Solution: 4 __________________________________
    
Number of solutions: 4   Number of backtracks: 0
Elapsed time: 00:00:00     


_AllAscending

_AllAscending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater than". These types currently include I, L, R and S. The _AllAscending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.
pred _AllAscending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 < x2 & x1 < x3 & ... x1 < xn 
                 
For example, the following query
   all x::[1..2] & y::[1..4] & z ::I[1..4] & _AllAscending(x,y,z)
will generate the following solutions:
x = 1
y = 2
z = 3
___ Solution: 1 __________________________________

x = 1
y = 2
z = 4
___ Solution: 2 __________________________________

x = 1
y = 3
z = 4
___ Solution: 3 __________________________________

x = 2
y = 3
z = 4
___ Solution: 4 __________________________________

Number of solutions: 4   Number of backtracks: 0
Elapsed time: 00:00:00  

_Ascending

_Ascending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater or equal than". These types currently include I, L, R and S. The _Ascending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.
pred _Ascending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 <= x2 & x1 <= x3 & ... x1 <= xn 
                 
For example, the following query
   all x::[1..2] & y::[1..4] & z ::I[1..2] & _Ascending(x,y,z)
will generate the following solutions:

x = 1
y = 1
z = 1
___ Solution: 1 __________________________________

x = 1
y = 1
z = 2
___ Solution: 2 __________________________________

x = 1
y = 2
z = 2
___ Solution: 3 __________________________________

x = 2
y = 2
z = 2
___ Solution: 4 __________________________________

Number of solutions: 4   Number of backtracks: 0
Elapsed time: 00:00:00 


_AllDescending

_AllDescending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater than". These types currently include I, L, R and S. The _AllDescending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.
pred _AllDescending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 > x2 & x1 > x3 & ... x1 > xn 
                 
For example, the following query
all x::[1..3] & y::[1..3] & z ::I[1..3] & _AllDescending(x,y,z)
will generate the following solutions:
x = 3
y = 2
z = 1
___ Solution: 1 __________________________________

Number of solutions: 1   Number of backtracks: 0
Elapsed time: 00:00:00   


_Descending

_Descending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater or equal than". These types currently include I, L, R and S. The _Descending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.
pred _Descending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 >= x2 & x1 >= x3 & ... x1 >= xn 
                 
For example, the following query
all x::[1..2] & y::[1..2] & z ::I[1..2] & _Descending(x,y,z)
  
will generate the following solutions:
x = 1
y = 1
z = 1
___ Solution: 1 __________________________________

x = 2
y = 1
z = 1
___ Solution: 2 __________________________________

x = 2
y = 2
z = 1
___ Solution: 3 __________________________________

x = 2
y = 2
z = 2
___ Solution: 4 __________________________________

Number of solutions: 4   Number of backtracks: 0
Elapsed time: 00:00:00    


RtlSystem

Execute a system call.

Syntax:

    RtlSystem(cmd:<S)

Example:

    RtlSystem(‘dir c:’)

Note: use with caution. The system output is redirected to the TTY. Do not use for system calls requiring user input.

RtlLtoS

Convert an integer number to a decimal string.

Syntax:

    RtlLtoS(x:<L, s:>S)

Note: Conversion implicitly assumes a decimal number.

RtlLtoSx

Convert an integer number to a string with specified base.

Syntax:

    RtlLtoSx(x:<L,base:<I[2..36], s:>S)

Note: Binary numbers use base 2, decimal numbers use base 10, hexadecimal numbers base 16 etc.

RtlStoL

Convert a string in decimal base to a number.

Syntax:

    RtlStoL(s:<S, x:>L)

Note: The string must contain only digits 0..9. There is no limit on the string length.

RtlStoLx

Convert a string representing a number in arbitrary base [2..36] to a number.

Syntax:

    RtlStoL(s:<S, base:<I[2..36], x:>L)

Note: The string must contain only alphanumerical characters valid for the required base

RtlReverse

Convenience polymorfic API. Reverse a string, array or a list.

Syntax:

    RtlReverse(in:<S, out:>S)
    RtlReverse(in:<list X, out:>list X)
    RtlReverse(in:<[0..]->X, out:>[..]->X)

Note: X can be of any type.

Examples:

Reversed string ‘abcd’ becomes ‘dcba’.
Reversed list el, e2, e3, e4, Nil becomes e4, e3, e2, e1, Nil.
Reversed array [a1,a2,a3,a4,a5] becomes [a5,a4,a3,a2,a1]

RtlSortAscending

Convenience polymorfic API. Sort a string, array or a list in ascending order.

Syntax:

    RtlSortAscending(in:<S, out:>S)
    RtlSortAscending(in:<list X, out:>list X)
    RtlSortAscending(in:<[0..]->X, out:>[..]->X)

Note: X can be of any type.

Examples:

Sorted string ‘bozo’ becomes ‘booz’.
Sorted list 3,1,5,4,7,9,3,2, Nil becomes 1,2,3,3,4,5,7,9,Nil.
Sorted array [2,1,5,6,0] becomes [0,1,2,5,6]

RtlSortDescending

Convenience polymorfic API. Sort a string, array or a list in descending order.

Syntax:

    RtlSortDescending(in:<S, out:>S)
    RtlSortDescending(in:<list X, out:>list X)
    RtlSortDescending(in:<[0..]->X, out:>[..]->X)

Note: X can be of any type.

Examples:

Sorted string ‘bozo’ becomes ‘zoob’.
Sorted list 3,1,5,4,7,9,3,2, Nil becomes 9,7,5,4,3,3,2,1,Nil.
Sorted array [2,1,5,6,0] becomes [6,5,2,1,0]

RtlToUpperString

Convenience API. Convert an ASCII string to upper case.

Syntax:

    RtlToUpperString(sin:<S, out:>S)

RtlToLowerString

Convenience API. Convert an ASCII string to lower case.

Syntax:

    RtlToLowerString(sin:<S, out:>S)

RtlParseString

Parse a string into individual tokens. The token separators are passed as a string.

Syntax:

    RtlParseString(sin:<S, separators:<S, output:>[0..]->S)

Example:

    y = RtlParseString('OK,parse this string 1,  2, 3   ,4,      5\n6\t7\t8\n', ' ,\n\t') 
Returs:
    y = [OK,parse,this,string,1,2,3,4,5,6,7,8] 

RtlGetCommandLine

Retrieve the command line string.

Syntax:

    RtlGetCommandLineString(cmdline:>S)

Note: Routine typically used by standalone executables.

RtlGetCommandArguments

Routine parses the command line string and returns an array of strings.

Syntax:

    RtlGetCommandArguments(cmdars:>[0..]->S)

Note: Routine typically used by standalone executables.


RtlGetCutPoint
RtlSetCutPoint

By using these routines we are able to prematurely terminate any predicate, explicitly cutting off the predicate backtracking branches.

Syntax:

    RtlGetCutPoint(cp:>I)
    RtlSetCutPoint(cp:<I)
The following code snippet illustrates typical usage of these routines: Terminate collecting of all results of the predicate MyPredicate if the proc WantNextSolution fails.
    all x in l 
        RtlGetCutPoint(cp) &
        MyPredicate(x) & 
        if ~WantNextSolution() then
            RtlSetCutPoint(cp)
        end
    end  

Note: Use caution when using these routines, as there is no proper argument validation. Incorrect usage will lead to bizarre program behaviour.


RtlTrimSolutions

Limit the number of solutions as collected by the "all" formula. For use in situations when more than one but less than all solutions are required.
If the number of solutions is less then specified by RtlTrimSolutions argument, the number of solutions is not affected.

Syntax:

    proc RtlTrimSolution(number:<I[1..])
For example, the query
    all x:<[0..100] & RtlTrimSolutions(4)
will generate the following solutions:
x = 0
___ Solution: 1 __________________________________

x = 1
___ Solution: 2 __________________________________

x = 2
___ Solution: 3 __________________________________

x = 3
___ Solution: 4 __________________________________

Number of solutions: 4   Number of backtracks: 0
Elapsed time: 00:00:00

The following code snippet illustrates typical usage of this routine: Terminate collecting of all results of the predicate MyPredicate if the number of solutions reaches a predetermined value of 1000.
    all x in l 
        RtlGetCutPoint(cp) &
        MyPredicate(x) & 
        RtlTrimSolutions(1000)
        end
    end  

Note: Use caution when using RtlTrimSolutions. This routine was more-less necessitated by real world programs. Clearly there is a logical contradiction between asking for "all" solutions and actually obtaining a reduced number of solutions.


RtlIsPowerOf2

Test if number is a perfect square.

Syntax:

    proc RtlIsPowerOf2(number:<L)
The routine succseeds if the number is a perfect square, fails otherwise. For example, the query
    all x:>[0..100] & RtlIsPowerOf2(x)
will generate the following solutions:
x = 0
___ Solution: 1 __________________________________

x = 1
___ Solution: 2 __________________________________

x = 4
___ Solution: 3 __________________________________

x = 9
___ Solution: 4 __________________________________

x = 16
___ Solution: 5 __________________________________

x = 25
___ Solution: 6 __________________________________

x = 36
___ Solution: 7 __________________________________

x = 49
___ Solution: 8 __________________________________

x = 64
___ Solution: 9 __________________________________

x = 81
___ Solution: 10 __________________________________

x = 100
___ Solution: 11 __________________________________

Number of solutions: 11   Number of backtracks: 90
Elapsed time: 00:00:00     

Note: Both 0 and 1 are considered to be perfect squares.


RtlSquareRoot

Calculate square root of an integer.

Syntax:

    proc RtlSquareRoot(number:<L, root:>L)
The routine will fail if number is not a perfect square. For example, the query
    all x:>[0..50] & RtlSquareRoot(x,y)
will generate the following solutions:
x = 0
y = 0
___ Solution: 1 __________________________________

x = 1
y = 1
___ Solution: 2 __________________________________

x = 4
y = 2
___ Solution: 3 __________________________________

x = 9
y = 3
___ Solution: 4 __________________________________

x = 16
y = 4
___ Solution: 5 __________________________________

x = 25
y = 5
___ Solution: 6 __________________________________

x = 36
y = 6
___ Solution: 7 __________________________________

x = 49
y = 7
___ Solution: 8 __________________________________

Number of solutions: 8   Number of backtracks: 43
Elapsed time: 00:00:00


TTYSetTitleBarText

Specify the title of the TTY window.

Syntax:

    proc TTYSetTitleBarText(title:<S)

Note: Typically meant for standalone applications. Replaces the default TTY title as it appears in the TTY window title bar.

TTYKeyHit

Check if any user key input present.

Syntax:

    proc TTYKeyHit()

Note: Succeeds if the keyboard buffer is not empty, fails otherwise.

TTYKeyWait

Wait for the user the press a key. The call always succeeds.

Syntax:

    proc TTYKeyWait()

Note: This is a blocking call. The procedure will not return until the user presses a key. Since the actual key value is not retrieved, TTYKeyWait is declared as “proc”.

TTYKeyGet

Wait for the user the press a key.The call always succeeds.

Syntax:

    subr TTYKeyGet(key:>I)

Note:  This is a blocking call. The procedure will not return until the user presses a key. The key value is retrieved.

TTYGetString

Wait for the user the enter a string. The call always succeeds.

Syntax:

    subr TTYGetString(string:>S)

Note:  This is a blocking call. The procedure will not return until the user presses the ENTER key.

TTYShow

Show the console window.

Syntax:

    proc TTYShow()

Note:  The call allows to display the console previously hidden.

TTYHide

Hide the console window.

Syntax:

    proc TTYHide()

Note:  The call allows to hide the console at runtime.


DbPut

Store a record at the current position.

Syntax:

    proc DbPut(f:.file T, x:<T) 

DbInsert

DbInsert is an alternative to DbPut. DbInsert uses the same arguments as DbPut. Using DbInsert creates a database file in sorted order. Unlike using DbPut, DbInsert places the records within the database file based on the actual records content. The records are inserted in standard order for sorting. Standard order of sorting basically specifies a method to determine which record is "smaller". If a record of the same value already exists, the record in not inserted again, otherwise the record is inserted after the first record of a "smaller" value. To keep the whole database file in sorted order, do not mix DbPut and DbInsert.

DbGet

Current record is accessed and the file is advanced by one record.

Syntax:

    proc DbGet(f:.file T, rec:>T)

DbAccess

Retrieve the current record.

Syntax:

    proc DbAccess(f:.file T, rec:>T)

Note: fails at EOF, otherwise succeeds returning the current record, does not change the file position

DbDelete

Delete the current record.

Syntax:

    proc DbDelete(f:.file T) 

Note: Fails at EOF, otherwise succeeds removing the current record.  Aborts when used with Bin or Ascii files.

DbSkip

Syntax:

    DbSkip(f:.file T, n:<I)

Fails if n negative, succeeds otherwise advancing the current position by n records or to the end of file if there are not n records left in the file.

DbRewind

Position the file at the beginning, always succeeds.

Syntax:

    proc DbRewind(f:.file T) 

DbEof

Test for end of file. Call succeeds if there are no more records left after the current position.

Syntax:

    proc DbEof(f:.file T)

DbEofSet

Positions the file at the end, always succeeds.

Syntax:

    proc DbEofSet(f:.file T)

DbTruncate

Truncate the file at the current position.

Syntax:

    proc DbTruncate(f:.file T)

Note: for database files, calling this function after DbRewind will delete all database records and indeces, otherwise this call will fail if index files exist.

DbFlush

Flush all modified blocks from the cache-buffers. This procedure is to be used from time to time as a safeguard against a hardware or software malfunction.

Syntax:

    proc DbFlush(f:.file T)

DbSeek

Position the DB file pointer to the record containing the key value.

Syntax:

    proc DbSeek(f:.IndexFile,keyvalue:<T)

DbSeekNext

Position the DB file pointer to the record with a greater or equal key value then the current record.

Syntax:

    proc DbSeekNext(f:.IndexFile)

Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.

DbSeekNextEq

Position the DB file pointer to the next record containing the same key value as the current record.

Syntax:

    proc DbSeekNextEq(f:.IndexFile)

Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.

DbSeekGt

Position the DB file pointer to the record with a greater key value then the current record.

Syntax:

    proc DbSeekGt(f:.IndexFile)

Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.

DbSeekPrev

Position the DB file pointer to the record with a lesser or equal key value then the current record.

Syntax:

    proc DbSeekPrev(f:.IndexFile)

Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.

DbSeekPrevEq

Position the DB file pointer to the previous record containing the same key value as the current record.

Syntax:

    proc DbSeekPrevEq(f:.IndexFile)

Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.

DbSeekLt

Position the DB file pointer to the record with a lesser key value then the current record.

Syntax:

    proc DbSeekLt(f:.IndexFile)

Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.

DbSeekFirst

Position the DB file pointer to the first record (leftmost node) as sorted by the index file. DB file pointer position is set to the record containing the smallest value of the index file key.

Syntax:

    proc DbSeekFirst(f:.IndexFile)

DbSeekLast

Position the DB file pointer to the last record (rightmost node) as sorted by the index file. DB file pointer position is set to the record containing the largest value of the index file key.

Syntax:

    proc DbSeekLast(f:.IndexFile)




Top Constraints