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.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.
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)
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)
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'
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.
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 <> xnFor 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
pred _AllAscending(x1::T, x2::T, x3::T, ..., xn::T) iff x1 < x2 & x1 < x3 & ... x1 < xnFor 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
pred _Ascending(x1::T, x2::T, x3::T, ..., xn::T) iff x1 <= x2 & x1 <= x3 & ... x1 <= xnFor 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
pred _AllDescending(x1::T, x2::T, x3::T, ..., xn::T) iff x1 > x2 & x1 > x3 & ... x1 > xnFor 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
pred _Descending(x1::T, x2::T, x3::T, ..., xn::T) iff x1 >= x2 & x1 >= x3 & ... x1 >= xnFor 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
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.
Convert an integer number to a decimal string.
Syntax:
RtlLtoS(x:<L, s:>S)
Note: Conversion implicitly assumes a decimal number.
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.
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.
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
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]
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’.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’.Convenience API. Convert an ASCII string to upper case.
Syntax:
RtlToUpperString(sin:<S, out:>S)
Convenience API. Convert an ASCII string to lower case.
Syntax:
RtlToLowerString(sin:<S, out:>S)
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]
Retrieve the command line string.
Syntax:
RtlGetCommandLineString(cmdline:>S)
Note: Routine typically used by standalone executables.
Routine parses the command line string and returns an array of strings.
Syntax:
RtlGetCommandArguments(cmdars:>[0..]->S)
Note: Routine typically used by standalone executables.
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.
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:00The 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.
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.
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
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.
Check if any user key input present.
Syntax:
proc TTYKeyHit()
Note: Succeeds if the keyboard buffer is not empty, fails otherwise.
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”.
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.
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.
Show the console window.
Syntax:
proc TTYShow()
Note: The call allows to display the console previously hidden.
Hide the console window.
Syntax:
proc TTYHide()
Note: The call allows to hide the console at runtime.
Store a record at the current position.
Syntax:
proc DbPut(f:.file T, x:<T)
Current record is accessed and the file is advanced by one record.
Syntax:
proc DbGet(f:.file T, rec:>T)
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
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.
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.
Position the file at the beginning, always succeeds.
Syntax:
proc DbRewind(f:.file T)
Test for end of file. Call succeeds if there are no more records left after the current position.
Syntax:
proc DbEof(f:.file T)
Positions the file at the end, always succeeds.
Syntax:
proc DbEofSet(f:.file T)
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.
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)
Position the DB file pointer to the record containing the key value.
Syntax:
proc DbSeek(f:.IndexFile,keyvalue:<T)
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.
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.
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.
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.
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.
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.
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)
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)