Calculemus

Propexamples Module

Namespace: Calculemus
Assembly: Calculemus.dll

Some propositional formulas to test, and functions to generate classes.

This module, while showing some applications of propositional logic, is used above all to generate interesting classes of problems in order to have a stock of non-trivial formulas on which to test the efficiency of propositional logic algorithms.

Table of contents

Ramsey numbers

Functions and values

Function or value Description

ramsey s t n

Full Usage: ramsey s t n

Parameters:
    s : int - The number of connected vertices.
    t : int - The number of disconnected vertices.
    n : int - The number supposed to be greater or equal to the Ramsey number.

Returns: formula<prop> A propositional formula that is a tautology if if n is greater or equal than the Ramsey number R(s,t).

Generates an assertion equivalent to R(s,t) <= n for the Ramsey number R(s,t).

In terms of graph theory, the ramsey number R(s,t) is the minimum number x such that all graphs of x vertices have a completely connected subgraph of size s or a completely disconnected subgraph of size t. The Ramsey's theorem proves that for every pair of \(s,t \in \mathbb{N}\) such a number exists.

s : int

The number of connected vertices.

t : int

The number of disconnected vertices.

n : int

The number supposed to be greater or equal to the Ramsey number.

Returns: formula<prop>

A propositional formula that is a tautology if if n is greater or equal than the Ramsey number R(s,t).

Example 

 ramsey 3 3 4
Evaluates to (p_1_2 /\ p_1_3 /\ p_2_3 \/ p_1_2 /\ p_1_4 /\ p_2_4 \/ p_1_3 /\ p_1_4 /\ p_3_4 \/ p_2_3 /\ p_2_4 /\ p_3_4) \/ ~p_1_2 /\ ~p_1_3 /\ ~p_2_3 \/ ~p_1_2 /\ ~p_1_4 /\ ~p_2_4 \/ ~p_1_3 /\ ~p_1_4 /\ ~p_3_4 \/ ~p_2_3 /\ ~p_2_4 /\ ~p_3_4.

Example 

 tautology(ramsey 3 3 5)
Evaluates to false.

Example 

 tautology(ramsey 3 3 6)
Evaluates to true.

Half adder

Functions and values

Function or value Description

ha x y s c

Full Usage: ha x y s c

Parameters:
    x : formula<'a> - The first one-bit-number to be added.
    y : formula<'a> - The second one-bit-number to be added.
    s : formula<'a> - The supposed sum.
    c : formula<'a> - The supposed carry.

Returns: formula<'a> The propositional formula that is true in those valuations in which s and c are, respectively, the sum and carry calculated by an half-adder for the sum of x and y.

Half adder function.
(s <=> x <=> ~y) /\ (c <=> x /\ y).

An half adder calculates the sum and carry for only two one-bit-numbers.

ha generates a propositional formula that is true in those valuations in which s and c are, respectively, the sum and carry calculated by an half-adder for the sum of x and y.

x : formula<'a>

The first one-bit-number to be added.

y : formula<'a>

The second one-bit-number to be added.

s : formula<'a>

The supposed sum.

c : formula<'a>

The supposed carry.

Returns: formula<'a>

The propositional formula that is true in those valuations in which s and c are, respectively, the sum and carry calculated by an half-adder for the sum of x and y.

Example 

 ha (True:prop formula) True False True
Evaluates to `(false <=> true <=> ~true) /\ (true <=> true /\ true)`.

Example

All the valuations satisfying the formula represent the correct relation between input and output of an half adder. 

 let fm = ha (!>"x") (!>"y") (!>"s") (!>"c")
 // `(s <=> x <=> ~y) /\ (c <=> x /\ y)`
 
 printfn "-----------------"
 printfn "| x | y | c | s |"
 printfn "-----------------"
 
 (allsatvaluations (eval fm) (fun _ -> false) (atoms fm))
 |> List.iter (fun v -> 
     printfn "| %A | %A | %A | %A |" 
         (v (P "x") |> System.Convert.ToInt32)
         (v (P "y") |> System.Convert.ToInt32)
         (v (P "c") |> System.Convert.ToInt32)
         (v (P "s") |> System.Convert.ToInt32)
 )
 printfn "-----------------"
val fm: obj
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val iter: action: ('T -> unit) -> list: 'T list -> unit
val v: (obj -> obj)
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
After evaluation the following is printed to the stdout: 
 -----------------
 | x | y | c | s |
 -----------------
 | 0 | 0 | 0 | 0 |
 | 0 | 1 | 0 | 1 |
 | 1 | 0 | 0 | 1 |
 | 1 | 1 | 1 | 0 |
 -----------------

halfcarry x y

Full Usage: halfcarry x y

Parameters:
    x : formula<'a> - The first one-bit-number to be added.
    y : formula<'a> - The second one-bit-number to be added.

Returns: formula<'a> The prop formula that represents the half adder's carry of x + y.

Carry of an half adder.
x /\ y.

The truth-value of the generated propositional formula corresponds to the carry of an half adder of two one-bit-numbers x and y also represented as prop formulas. In this context the truth-values false and true should be read as the two digits of the binary system: 0 and 1.

x : formula<'a>

The first one-bit-number to be added.

y : formula<'a>

The second one-bit-number to be added.

Returns: formula<'a>

The prop formula that represents the half adder's carry of x + y.

Example 

 halfcarry (True:prop formula) False
Evaluates to `true /\ false``.

Example

The truth-table of the output formula, with truth-values converted in integers, shows how it calculates the half-adder carry: 

 let fm = halfcarry (!>"x") (!>"y")
 // evaluates to `x /\ y`
 
 printfn "-------------"
 printfn "| x | y | c |"
 printfn "-------------"
 
 // for each valuation:
 allvaluations fm
 |> List.iter (fun v -> 
     // for each atom:
     atoms fm
     |> List.iter (fun atm -> 
         // print the truth-value of the atom in the valuation;
         printf "| %A " (v atm |> System.Convert.ToInt32)
     )
     // and print the truth-value of the formula in the valuation.
     printfn "| %A |" 
         (eval fm v |> System.Convert.ToInt32)
 )
 printfn "-------------"
val fm: obj
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val iter: action: ('T -> unit) -> list: 'T list -> unit
val v: (obj -> obj)
val atm: obj
val printf: format: Printf.TextWriterFormat<'T> -> 'T
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
After evaluation the following is printed to the stdout: 
 -------------
 | x | y | c |
 -------------
 | 0 | 0 | 0 |
 | 0 | 1 | 0 |
 | 1 | 0 | 0 |
 | 1 | 1 | 1 |
 -------------

halfsum x y

Full Usage: halfsum x y

Parameters:
    x : formula<'a> - The first one-bit-number to be added.
    y : formula<'a> - The second one-bit-number to be added.

Returns: formula<'a> The prop formula that represents the half adder's sum of x + y.

Sum of an half adder.
x <=> ~ y.

The truth-value of the generated propositional formula corresponds to the sum of an half adder of two one-bit-numbers x and y also represented as prop formulas. In this context the truth-values false and true should be read as the two digits of the binary system: 0 and 1.

x : formula<'a>

The first one-bit-number to be added.

y : formula<'a>

The second one-bit-number to be added.

Returns: formula<'a>

The prop formula that represents the half adder's sum of x + y.

Example 

 halfsum (True:prop formula) False
Evaluates to `true <=> ~false`.

Example

The truth-table of the output formula, with truth-values converted in integers, shows how it calculates the half-adder sum: 

 let fm = halfsum (!>"x") (!>"y")
 // evaluates to `x <=> ~y`
 
 printfn "-------------"
 printfn "| x | y | s |"
 printfn "-------------"
 
 // for each valuation:
 allvaluations fm
 |> List.iter (fun v -> 
     // for each atom:
     atoms fm
     |> List.iter (fun atm -> 
         // print the truth-value of the atom in the valuation;
         printf "| %A " (v atm |> System.Convert.ToInt32)
     )
     // and print the truth-value of the formula in the valuation.
     printfn "| %A |" 
         (eval fm v |> System.Convert.ToInt32)
 )
 printfn "-------------"
val fm: obj
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val iter: action: ('T -> unit) -> list: 'T list -> unit
val v: (obj -> obj)
val atm: obj
val printf: format: Printf.TextWriterFormat<'T> -> 'T
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
After evaluation the following is printed to the stdout: 
 -------------
 | x | y | s |
 -------------
 | 0 | 0 | 0 |
 | 0 | 1 | 1 |
 | 1 | 0 | 1 |
 | 1 | 1 | 0 |
 -------------

Full adder

Functions and values

Function or value Description

carry x y z

Full Usage: carry x y z

Parameters:
    x : formula<'a> - The first one-bit-number to be added.
    y : formula<'a> - The second one-bit-number to be added.
    z : formula<'a> - The possible carry of a previous sum.

Returns: formula<'a> The full adder's carry of x + y + z

Carry of a full adder.
(x /\ y) \/ ((x \/ y) /\ z).

The truth-value of the generated propositional formula corresponds to the carry of a full adder of two one-bit-numbers x and y plus a carry z from a previous sum also represented as prop formulas. In this context the truth-values false and true should be read as the two digits of the binary system: 0 and 1.

x : formula<'a>

The first one-bit-number to be added.

y : formula<'a>

The second one-bit-number to be added.

z : formula<'a>

The possible carry of a previous sum.

Returns: formula<'a>

The full adder's carry of x + y + z

Example 

 carry (True:prop formula) False True
Evaluates to `true /\ false \/ (true \/ false) /\ true`.

Example

The truth-table of the output formula, with truth-values converted in integers, shows how it calculates the half-adder carry: 

 let fm = carry (!>"x") (!>"y") (!>"z")
 // evaluates to `x /\ y \/ (x \/ y) /\ z`
 
 printfn "-----------------"
 printfn "| x | y | z | c |"
 printfn "-----------------"
 
 // for each valuation:
 allvaluations fm
 |> List.iter (fun v -> 
     // for each atom:
     atoms fm
     |> List.iter (fun atm -> 
         // print the truth-value of the atom in the valuation;
         printf "| %A " (v atm |> System.Convert.ToInt32)
     )
     // and print the truth-value of the formula in the valuation.
     printfn "| %A |" 
         (eval fm v |> System.Convert.ToInt32)
 )
 printfn "-----------------"
val fm: obj
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val iter: action: ('T -> unit) -> list: 'T list -> unit
val v: (obj -> obj)
val atm: obj
val printf: format: Printf.TextWriterFormat<'T> -> 'T
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
After evaluation the following is printed to the stdout: 
 -----------------
 | x | y | z | c |
 -----------------
 | 0 | 0 | 0 | 0 |
 | 0 | 0 | 1 | 0 |
 | 0 | 1 | 0 | 0 |
 | 0 | 1 | 1 | 1 |
 | 1 | 0 | 0 | 0 |
 | 1 | 0 | 1 | 1 |
 | 1 | 1 | 0 | 1 |
 | 1 | 1 | 1 | 1 |
 -----------------

fa x y z s c

Full Usage: fa x y z s c

Parameters:
    x : formula<'a> - The first one-bit-number to be added.
    y : formula<'a> - The second one-bit-number to be added.
    z : formula<'a> - The carry from a previous sum.
    s : formula<'a> - The supposed sum.
    c : formula<'a> - The supposed carry.

Returns: formula<'a> The propositional formula that is true in those valuations in which s and c are, respectively, the sum and carry calculated by a full-adder for the sum of x and y plus the carry z for a previous sum.

Full adder function.
(s <=> (x <=> ~y) <=> ~z) /\ (c <=> x /\ y \/ (x \/ y) /\ z)

A full adder is a one-bit adder that adds three one-bit-numbers: two operands x and y plus z that represent the carry from a previous sum.

fa generates a propositional formula that is true in those valuations in which s and c are, respectively, the sum and carry calculated by a full-adder for the sum of x and y plus the carry z for a previous sum.

x : formula<'a>

The first one-bit-number to be added.

y : formula<'a>

The second one-bit-number to be added.

z : formula<'a>

The carry from a previous sum.

s : formula<'a>

The supposed sum.

c : formula<'a>

The supposed carry.

Returns: formula<'a>

The propositional formula that is true in those valuations in which s and c are, respectively, the sum and carry calculated by a full-adder for the sum of x and y plus the carry z for a previous sum.

Example

All the valuations satisfying the formula represent the correct relation between input and output of an half adder. 

 printfn "---------------------"
 printfn "| x | y | z | c | s |"
 printfn "---------------------"
 
 (allsatvaluations (eval fm) (fun _ -> false) (atoms fm))
 |> List.iter (fun v -> 
     printfn "| %A | %A | %A | %A | %A |" 
         (v (P "x") |> System.Convert.ToInt32)
         (v (P "y") |> System.Convert.ToInt32)
         (v (P "z") |> System.Convert.ToInt32)
         (v (P "c") |> System.Convert.ToInt32)
         (v (P "s") |> System.Convert.ToInt32)
 )
 printfn "---------------------"
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val iter: action: ('T -> unit) -> list: 'T list -> unit
val v: (obj -> obj)
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
After evaluation the following is printed to the stdout: 
 ---------------------
 | x | y | z | c | s |
 ---------------------
 | 0 | 0 | 0 | 0 | 0 |
 | 0 | 0 | 1 | 0 | 1 |
 | 0 | 1 | 0 | 0 | 1 |
 | 1 | 0 | 0 | 0 | 1 |
 | 0 | 1 | 1 | 1 | 0 |
 | 1 | 0 | 1 | 1 | 0 |
 | 1 | 1 | 0 | 1 | 0 |
 | 1 | 1 | 1 | 1 | 1 |
 ---------------------

sum x y z

Full Usage: sum x y z

Parameters:
    x : formula<'a> - The first one-bit-number to be added.
    y : formula<'a> - The second one-bit-number to be added.
    z : formula<'a> - The possibile carry of a previous sum.

Returns: formula<'a> The full adder's sum of x + y + z.

Sum of a full adder.
(x <=> ~ y) <=> ~ z.

The truth-value of the generated propositional formula corresponds to the sum of a full adder of two one-bit-numbers x and y plus a carry z from a previous sum also represented as prop formulas. In this context the truth-values false and true should be read as the two digits of the binary system: 0 and 1.

x : formula<'a>

The first one-bit-number to be added.

y : formula<'a>

The second one-bit-number to be added.

z : formula<'a>

The possibile carry of a previous sum.

Returns: formula<'a>

The full adder's sum of x + y + z.

Example 

 sum (True:prop formula) False True
Evaluates to `(true <=> ~false) <=> ~true`.

Example

The truth-table of the output formula, with truth-values converted in integers, shows how it calculates the half-adder carry: 

 let fm = sum (!>"x") (!>"y") (!>"z")
 // evaluates to `(x <=> ~y) <=> ~z`
 
 printfn "-----------------"
 printfn "| x | y | z | c |"
 printfn "-----------------"
 
 // for each valuation:
 allvaluations fm
 |> List.iter (fun v -> 
     // for each atom:
     atoms fm
     |> List.iter (fun atm -> 
         // print the truth-value of the atom in the valuation;
         printf "| %A " (v atm |> System.Convert.ToInt32)
     )
     // and print the truth-value of the formula in the valuation.
     printfn "| %A |" 
         (eval fm v |> System.Convert.ToInt32)
 )
 printfn "-----------------"
val fm: obj
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val iter: action: ('T -> unit) -> list: 'T list -> unit
val v: (obj -> obj)
val atm: obj
val printf: format: Printf.TextWriterFormat<'T> -> 'T
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
After evaluation the following is printed to the stdout: 
 -----------------
 | x | y | z | c |
 -----------------
 | 0 | 0 | 0 | 0 |
 | 0 | 0 | 1 | 1 |
 | 0 | 1 | 0 | 1 |
 | 0 | 1 | 1 | 0 |
 | 1 | 0 | 0 | 1 |
 | 1 | 0 | 1 | 0 |
 | 1 | 1 | 0 | 0 |
 | 1 | 1 | 1 | 1 |
 -----------------

Ripple carry adder

Functions and values

Function or value Description

conjoin f l

Full Usage: conjoin f l

Parameters:
    f : 'a -> formula<'b> - A function from indexes to formulas.
    l : 'a list - A list of indexes.

Returns: formula<'b> The conjunctions of the formulas obtained by applying f to the elements of l.

Constructs a conjunction of the formulas obtained by applying a function (from indexes to formulas) to the elements of a list of indexes.

Its intended use, in our context, is to put multiple 1-bit adders together into an n-bit adder. Indexes in this case point to the n-bit positions of the two n-bit numbers to be added. For example, Propexamples.ripplecarry use this function to 'conjoin' n Propexamples.fa's in order to obtain an n-bit adder.

f : 'a -> formula<'b>

A function from indexes to formulas.

l : 'a list

A list of indexes.

Returns: formula<'b>

The conjunctions of the formulas obtained by applying f to the elements of l.

Example 

 conjoin Atom [1;2;3]
Evaluates to And (Atom 1, And (Atom 2, Atom 3)).

mk_index x i

Full Usage: mk_index x i

Parameters:
    x : string - The variable name.
    i : int - The variable index.

Returns: formula<prop> The indexed prop variable Atom (P x_i)

Returns indexed propositional variables.

Given a string "x" and an integer i, generates a propositional variable Atom (P x_i).

Its intended use is to generate input for the ripplecarry functions: partially applying mk_index, just to the first string argument, generates the type of functions (from integers to propositional variables) expected by ripplecarry functions.

x : string

The variable name.

i : int

The variable index.

Returns: formula<prop>

The indexed prop variable Atom (P x_i)

Example 

 mk_index "x" 0
Evaluates to Atom (P "x_0").

mk_index2 x i j

Full Usage: mk_index2 x i j

Parameters:
    x : string - The variable name.
    i : int - The first variable index.
    j : int - The second variable index.

Returns: formula<prop> The double indexed prop variable Atom (P x_i_j).

Returns double indexed propositional variables.

Similar to Propexamples.mk_index

Given a string "x" and indexes i and j, it generates a propositional variable Atom (P x_i_j).

x : string

The variable name.

i : int

The first variable index.

j : int

The second variable index.

Returns: formula<prop>

The double indexed prop variable Atom (P x_i_j).

Example 

 mk_index2 "x" 0 1
Evaluates to Atom (P "x_0_1").

ripplecarry x y c out n

Full Usage: ripplecarry x y c out n

Parameters:
    x : int -> formula<'a> - The function that produces the indexed variables to encode the bits of the first addend.
    y : int -> formula<'a> - The function that produces the indexed variables to encode the bits of the second addend.
    c : int -> formula<'a> - The function that produces the indexed variables to encode the carry at each bit.
    out : int -> formula<'a> - The function that produces the indexed variables to encode the sum at each bit.
    n : int - The number of bits handled by the adder.

Returns: formula<'a> The conjunction of the formulas that represent full adders for each bit position.

Ripple carry adder with carry c(0) propagated in and c(n) out.
(s_0 <=> (x_0 <=> ~y_0) <=> ~c_0) /\ (c_1 <=> x_0 /\ y_0 \/ (x_0 \/ y_0) /\ c_0) /\ ... /\ (s_n <=> (x_n <=> ~y_n) <=> ~c_n) /\ (c_(n+1) <=> x_n /\ y_n \/ (x_n \/ y_n) /\ c_n).

Conjoins (see Propexamples.conjoin) n one-bit full adders to obtain an n-bit adder.

The generated propositional formula represents the correct relations between the input and output of a ripple carry adder, just as Propexamples.ha and Propexamples.fa, respectively, represent the correct relations between input and output for an half-adder and a full-adder.

It expects the user to supply functions x, y, out and c that, when given an index, generates an appropriate new variable. Propexamples.mk_index is supplied to generate such functions.

x : int -> formula<'a>

The function that produces the indexed variables to encode the bits of the first addend.

y : int -> formula<'a>

The function that produces the indexed variables to encode the bits of the second addend.

c : int -> formula<'a>

The function that produces the indexed variables to encode the carry at each bit.

out : int -> formula<'a>

The function that produces the indexed variables to encode the sum at each bit.

n : int

The number of bits handled by the adder.

Returns: formula<'a>

The conjunction of the formulas that represent full adders for each bit position.

Example

Ripple carry adder of two 2-bit numbers: printing all the valuations satisfying the formula shows all the possible correct relations between input. 

 let x, y, s, c = 
     mk_index "x",
     mk_index "y",
     mk_index "s",
     mk_index "c"
 
 let fm = ripplecarry x y c s 2
 // ((s_0 <=> (x_0 <=> ~y_0) <=> ~c_0) /\ (c_1 <=> x_0 /\ y_0 \/ 
 // (x_0 \/ y_0) /\ c_0)) /\ 
 // (s_1 <=> (x_1 <=> ~y_1) <=> ~c_1) /\ (c_2 <=> x_1 /\ y_1 \/ 
 // (x_1 \/ y_1) /\ c_1)
 
 // eval the atom at the input valuations and convert to int
 let toInt (v: prop -> bool) x =
     v (P x) |> System.Convert.ToInt32
 
 allsatvaluations (eval fm) (fun _ -> false) (atoms fm)
 |> List.iteri (fun i v -> 
     printfn "carry |   %A %A |" (toInt v "c_1") (toInt v "c_0")
     printfn "---------------"
     printfn "x     |   %A %A |" (toInt v "x_1") (toInt v "x_0")
     printfn "y     |   %A %A |" (toInt v "y_1") (toInt v "y_0")
     printfn "==============="
     printfn "sum   | %A %A %A |" 
         (toInt v "c_2")
         (toInt v "s_1")
         (toInt v "s_0")
     printfn ""
 )
val x: obj
val y: obj
val s: obj
val c: obj
val fm: obj
val toInt: v: ('a -> bool) -> x: 'b -> int
val v: ('a -> bool)
type bool = System.Boolean
val x: 'b
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val iteri: action: (int -> 'T -> unit) -> list: 'T list -> unit
val i: int
val v: (obj -> bool)
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
Some output omitted for brevity: 
 carry |   0 0 |
 ---------------
 x     |   0 0 |
 y     |   0 0 |
 ===============
 sum   | 0 0 0 |
 ...
 carry |   0 0 |
 ---------------
 x     |   1 0 |
 y     |   1 1 |
 ===============
 sum   | 1 0 1 |
 ...
 carry |   1 1 |
 ---------------
 x     |   1 1 |
 y     |   1 1 |
 ===============
 sum   | 1 1 1 |
Note how this version admit a carry c(0) different from 0 propagated in at the first bit.

ripplecarry0 x y c out n

Full Usage: ripplecarry0 x y c out n

Parameters:
    x : int -> formula<'a> - The function that produces the indexed variables to encode the bits of the first addend.
    y : int -> formula<'a> - The function that produces the indexed variables to encode the bits of the second addend.
    c : int -> formula<'a> - The function that produces the indexed variables to encode the carry at each bit.
    out : int -> formula<'a> - The function that produces the indexed variables to encode the sum at each bit.
    n : int - The number of bits handled by the adder.

Returns: formula<'a> The conjunction of the formulas that represent full adders for each bit position, except for the first position that is represented by an half adder.

Ripple carry adder with carry c(0) forced to 0.
((s_0 <=> x_0 <=> ~y_0) /\ (c_1 <=> x_0 /\ y_0)) /\ ... /\ (s_n <=> (x_n <=> ~y_n) <=> ~c_n) /\ (c_(n+1) <=> x_n /\ y_n \/ (x_n \/ y_n) /\ c_n)

It can be used when we are not interested in a carry in at the low end.

x : int -> formula<'a>

The function that produces the indexed variables to encode the bits of the first addend.

y : int -> formula<'a>

The function that produces the indexed variables to encode the bits of the second addend.

c : int -> formula<'a>

The function that produces the indexed variables to encode the carry at each bit.

out : int -> formula<'a>

The function that produces the indexed variables to encode the sum at each bit.

n : int

The number of bits handled by the adder.

Returns: formula<'a>

The conjunction of the formulas that represent full adders for each bit position, except for the first position that is represented by an half adder.

Example

Filtering the satisfying valuations with x_1=0,x_0=0,y_1=1,y_0=1 gives the ripplecarry0 for the sum of 01+11: 

 let x, y, s, c = 
   mk_index "x",
   mk_index "y",
   mk_index "s",
   mk_index "c"
 
 let rc0 = ripplecarry0 x y c s 2
 // ((s_0 <=> x_0 <=> ~y_0) /\ 
 //      (c_1 <=> x_0 /\ y_0)) /\ 
 // (s_1 <=> (x_1 <=> ~y_1) <=> ~c_1) /\ 
 //      (c_2 <=> x_1 /\ y_1 \/ (x_1 \/ y_1) /\ c_1)
 
 // eval the atom at the input valuations and convert to int
 let toInt (v: prop -> bool) x =
     v (P x) |> System.Convert.ToInt32
 
 allsatvaluations (eval rc0) (fun _ -> false) (atoms rc0)
 |> List.filter (fun v -> 
     (toInt v "x_1") = 0 && (toInt v "x_0") = 1      // x = 01
     && (toInt v "y_1") = 1 && (toInt v "y_0") = 1   // y = 11
 )
 |> List.iteri (fun i v -> 
     printfn "carry |   %A %A |" (toInt v "c_1") (toInt v "c_0")
     printfn "---------------"
     printfn "x     |   %A %A |" (toInt v "x_1") (toInt v "x_0")
     printfn "y     |   %A %A |" (toInt v "y_1") (toInt v "y_0")
     printfn "==============="
     printfn "sum   | %A %A %A |" 
         (toInt v "c_2")
         (toInt v "s_1")
         (toInt v "s_0")
     printfn ""
 )
val x: obj
val y: obj
val s: obj
val c: obj
val rc0: obj
val toInt: v: ('a -> bool) -> x: 'b -> int
val v: ('a -> bool)
type bool = System.Boolean
val x: 'b
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val filter: predicate: ('T -> bool) -> list: 'T list -> 'T list
val v: (obj -> bool)
val iteri: action: (int -> 'T -> unit) -> list: 'T list -> unit
val i: int
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
After evaluation the following is printed to the stdout: 
 carry |   1 0 |
 ---------------
 x     |   0 1 |
 y     |   1 1 |
 ===============
 sum   | 1 0 0 |

ripplecarry1 x y c out n

Full Usage: ripplecarry1 x y c out n

Parameters:
    x : int -> formula<'a> - The function that produces the indexed variables to encode the bits of the first addend.
    y : int -> formula<'a> - The function that produces the indexed variables to encode the bits of the second addend.
    c : int -> formula<'a> - The function that produces the indexed variables to encode the carry at each bit.
    out : int -> formula<'a> - The function that produces the indexed variables to encode the sum at each bit.
    n : int - The number of bits handled by the adder.

Returns: formula<'a> The conjunction of the formulas that represent full adders for each bit position, except for the first position in which a carry-in of 1 is forced.

Ripple carry adder with carry c(0) forced to 1.
((s_0 <=> ~(x_0 <=> ~y_0)) /\ (c_1 <=> x_0 /\ y_0 \/ x_0 \/ y_0)) /\ ... /\(s_n <=> (x_n <=> ~y_n) <=> ~c_n) /\ (c_(n+1) <=> x_n /\ y_n \/ (x_n \/ y_n) /\ c_n)

Together with Propexamples.ripplecarry0 is used to define Propexamples.carryselect.

x : int -> formula<'a>

The function that produces the indexed variables to encode the bits of the first addend.

y : int -> formula<'a>

The function that produces the indexed variables to encode the bits of the second addend.

c : int -> formula<'a>

The function that produces the indexed variables to encode the carry at each bit.

out : int -> formula<'a>

The function that produces the indexed variables to encode the sum at each bit.

n : int

The number of bits handled by the adder.

Returns: formula<'a>

The conjunction of the formulas that represent full adders for each bit position, except for the first position in which a carry-in of 1 is forced.

Example

Filtering the satisfying valuations with x_1=0,x_0=0,y_1=1,y_0=1 gives the ripplecarry1 for the sum of 01+11: 

 let x, y, s, c = 
   mk_index "x",
   mk_index "y",
   mk_index "s",
   mk_index "c"
 
 let rc1 = ripplecarry1 x y c s 2
 // ((s_0 <=> ~(x_0 <=> ~y_0)) /\ 
 //    (c_1 <=> x_0 /\ y_0 \/ x_0 \/ y_0)) /\ 
 // (s_1 <=> (x_1 <=> ~y_1) <=> ~c_1) /\ 
 //    (c_2 <=> x_1 /\ y_1 \/ (x_1 \/ y_1) /\ c_1)
 
 // eval the atom at the input valuations and convert to int
 let toInt (v: prop -> bool) x =
     v (P x) |> System.Convert.ToInt32
 
 allsatvaluations (eval rc1) (fun _ -> false) (atoms rc1)
 |> List.filter (fun v -> 
     (toInt v "x_1") = 0 && (toInt v "x_0") = 1      // x = 01
     && (toInt v "y_1") = 1 && (toInt v "y_0") = 1   // y = 11
 )
 |> List.iteri (fun i v -> 
     printfn "carry |   %A %A |" (toInt v "c_1") (toInt v "c_0")
     printfn "---------------"
     printfn "x     |   %A %A |" (toInt v "x_1") (toInt v "x_0")
     printfn "y     |   %A %A |" (toInt v "y_1") (toInt v "y_0")
     printfn "==============="
     printfn "sum   | %A %A %A |" 
         (toInt v "c_2")
         (toInt v "s_1")
         (toInt v "s_0")
     printfn ""
 )
val x: obj
val y: obj
val s: obj
val c: obj
val rc1: obj
val toInt: v: ('a -> bool) -> x: 'b -> int
val v: ('a -> bool)
type bool = System.Boolean
val x: 'b
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val filter: predicate: ('T -> bool) -> list: 'T list -> 'T list
val v: (obj -> bool)
val iteri: action: (int -> 'T -> unit) -> list: 'T list -> unit
val i: int
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
After evaluation the following is printed to the stdout: 
 carry |   1 0 |
 ---------------
 x     |   0 1 |
 y     |   1 1 |
 ===============
 sum   | 1 0 1 |
Note that while there is no c_0 in the formula the sum is calculated as if c_0 were equal to 1.

Carry select adder

Functions and values

Function or value Description

carryselect x y c0 c1 s0 s1 c s n k

Full Usage: carryselect x y c0 c1 s0 s1 c s n k

Parameters:
    x : int -> formula<'a> - The function that produces the indexed variables to encode the bits of the first addend.
    y : int -> formula<'a> - The function that produces the indexed variables to encode the bits of the second addend.
    c0 : int -> formula<'a> - The function that produces the indexed variables to encode the carries of the Propexamples.ripplecarry0 step.
    c1 : int -> formula<'a> - The function that produces the indexed variables to encode the carries of the Propexamples.ripplecarry1 step.
    s0 : int -> formula<'a> - The function that produces the indexed variables to encode the sums of the Propexamples.ripplecarry0 step.
    s1 : int -> formula<'a> - The function that produces the indexed variables to encode the sums of the Propexamples.ripplecarry1 step.
    c : int -> formula<'a> - The function that produces the indexed variables to encode the carry at each bit.
    s : int -> formula<'a> - The function that produces the indexed variables to encode the sum at each bit.
    n : int - The number of bits handled by the adder.
    k : int - The number of blocks in which the input are splitted.

Returns: formula<'a> The propositional formula that is true in the valuations that represent the correct relations between input and output of a carry select adder.

Carry select adder

The carry select adder is a more efficient adder than the ripplecarry, in which the n-bit inputs are split into several blocks of k, and corresponding k-bit blocks are added twice, once assuming a carry-in of 0 and once assuming a carry-in of 1.

Here it is used as a comparison term for use in Propexamples.mk_adder_test which demonstrates how it is possible to verify that the efficiency optimization introduced has not made any logical change to the function computed (one of the key problems in the design and verification of computer systems).

x : int -> formula<'a>

The function that produces the indexed variables to encode the bits of the first addend.

y : int -> formula<'a>

The function that produces the indexed variables to encode the bits of the second addend.

c0 : int -> formula<'a>

The function that produces the indexed variables to encode the carries of the Propexamples.ripplecarry0 step.

c1 : int -> formula<'a>

The function that produces the indexed variables to encode the carries of the Propexamples.ripplecarry1 step.

s0 : int -> formula<'a>

The function that produces the indexed variables to encode the sums of the Propexamples.ripplecarry0 step.

s1 : int -> formula<'a>

The function that produces the indexed variables to encode the sums of the Propexamples.ripplecarry1 step.

c : int -> formula<'a>

The function that produces the indexed variables to encode the carry at each bit.

s : int -> formula<'a>

The function that produces the indexed variables to encode the sum at each bit.

n : int

The number of bits handled by the adder.

k : int

The number of blocks in which the input are splitted.

Returns: formula<'a>

The propositional formula that is true in the valuations that represent the correct relations between input and output of a carry select adder.

Example 

 let x, y, c0, c1, s0, s1, s, c = 
      mk_index "x",
      mk_index "y",
      mk_index "c0",
      mk_index "c1",
      mk_index "s0",
      mk_index "s1",
      mk_index "s",
      mk_index "c"
 
 let cs = carryselect x y c0 c1 s0 s1 c s 2 2
 
  // eval the atom at the input valuations and convert to int
 let toInt (v: prop -> bool) x =
     v (P x) |> System.Convert.ToInt32
 
 allsatvaluations (eval cs) (fun _ -> false) (atoms cs)
 |> List.filter (fun v -> 
     (toInt v "x_1") = 0 && (toInt v "x_0") = 1      // x = 01
     && (toInt v "y_1") = 1 && (toInt v "y_0") = 1   // y = 11
 )
 |> List.iteri (fun i v -> 
     printfn "carry |   %A %A |" (toInt v "c_1") (toInt v "c_0")
     printfn "---------------"
     printfn "x     |   %A %A |" (toInt v "x_1") (toInt v "x_0")
     printfn "y     |   %A %A |" (toInt v "y_1") (toInt v "y_0")
     printfn "==============="
     printfn "sum   | %A %A %A |" 
         (toInt v "c_2")
         (toInt v "s_1")
         (toInt v "s_0")
     printfn ""
 )
val x: obj
val y: obj
val c0: obj
val c1: obj
val s0: obj
val s1: obj
val s: obj
val c: obj
val cs: obj
val toInt: v: ('a -> bool) -> x: 'b -> int
val v: ('a -> bool)
type bool = System.Boolean
val x: 'b
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val filter: predicate: ('T -> bool) -> list: 'T list -> 'T list
val v: (obj -> bool)
val iteri: action: (int -> 'T -> unit) -> list: 'T list -> unit
val i: int
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
After evaluation the following is printed to the stdout: 
 carry |   0 0 |
 ---------------
 x     |   0 1 |
 y     |   1 1 |
 ===============
 sum   | 1 0 0 |
 
 carry |   0 1 |
 ---------------
 x     |   0 1 |
 y     |   1 1 |
 ===============
 sum   | 1 0 1 |

mk_adder_test n k

Full Usage: mk_adder_test n k

Parameters:
    n : int - The number of bit to be added.
    k : int - The number of blocks in the carryselect.

Returns: formula<prop> A propositional formula that is a tautology, if Propexamples.ripplecarry0 and Propexamples.carryselect are equivalent.

Tests equivalence of ripple carry and carry select.

Generates propositions that state the equivalence of various ripplecarry and carryselect circuits based on the input n (number of bit to be added) and k (number of blocks in the carryselect circuit).

If the proposition generated is a tautology, the equivalence between the two circuit is proved.

n : int

The number of bit to be added.

k : int

The number of blocks in the carryselect.

Returns: formula<prop>

A propositional formula that is a tautology, if Propexamples.ripplecarry0 and Propexamples.carryselect are equivalent.

Example 

 mk_adder_test 2 1
 |> tautology
Evaluates to true.

mux sel in0 in1

Full Usage: mux sel in0 in1

Parameters:
    sel : formula<'a> - The formula that drives selection.
    in0 : formula<'a> - The first option.
    in1 : formula<'a> - The second option.

Returns: formula<'a> The formula that when sel is true, corresponds to in1 and otherwise to in0.

Multiplexer.
~sel /\ in0 \/ sel /\ in1

Selects between two alternatives: if sel selects in1, otherwise selects in0.

It is used in the the carry-select adder's implementation to select between carry-in of 0 or 1 when we do carry propagation.

sel : formula<'a>

The formula that drives selection.

in0 : formula<'a>

The first option.

in1 : formula<'a>

The second option.

Returns: formula<'a>

The formula that when sel is true, corresponds to in1 and otherwise to in0.

Example

If sel=true, the formula corresponds to in1. 

 mux !>"true" !>"in0" !>"in1"
 |> print_truthtable
After evaluation the following is printed to the stdout. 
 in0   in1   |   formula
 ---------------------
 false false | false 
 false true  | true  
 true  false | false 
 true  true  | true  
 ---------------------

Example

If sel=false, the formula corresponds to in0. 

 mux !>"false" !>"in0" !>"in1"
 |> print_truthtable
After evaluation the following is printed to the stdout. 
 in0   in1   |   formula
 ---------------------
 false false | false 
 false true  | false 
 true  false | true  
 true  true  | true  
 ---------------------

offset n x i

Full Usage: offset n x i

Parameters:
    n : int - The variable's index to offset.
    x : int -> 'a - A function that returns variables at given indexes.
    i : int - The number of position by which to offset the variable's index.

Returns: 'a The offset propositional variable.

Offsets the indices in an array of bits.

It is used to define the carry-select adder.

n : int

The variable's index to offset.

x : int -> 'a

A function that returns variables at given indexes.

i : int

The number of position by which to offset the variable's index.

Returns: 'a

The offset propositional variable.

Example 

 offset 1 (mk_index "x") 2
Evaluates to Atom (P "x_3").

Multiplier circuit

Functions and values

Function or value Description

multiplier x u v out n

Full Usage: multiplier x u v out n

Parameters:
    x : int -> int -> formula<'a> - The function from each bit positions of both operands to their products (represented as simple conjunctions of their variables).
    u : int -> int -> formula<'a> - An n-by-n 'array' to hold the intermediate sums.
    v : int -> int -> formula<'a> - An n-by-n 'array' to hold the intermediate carries.
    out : int -> formula<'a> - An n-by-n 'array' to hold the result.
    n : int - The number of bits handled by the multiplier.

Returns: formula<'a> The propositional formula that represents the relations between the input and output of the multiplier.

Naive multiplier based on repeated ripple carry.

x : int -> int -> formula<'a>

The function from each bit positions of both operands to their products (represented as simple conjunctions of their variables).

u : int -> int -> formula<'a>

An n-by-n 'array' to hold the intermediate sums.

v : int -> int -> formula<'a>

An n-by-n 'array' to hold the intermediate carries.

out : int -> formula<'a>

An n-by-n 'array' to hold the result.

n : int

The number of bits handled by the multiplier.

Returns: formula<'a>

The propositional formula that represents the relations between the input and output of the multiplier.

Example 

 // eval the atom at the input valuations and convert to int
 let toInt (v: prop -> bool) x =
     v (P x) |> System.Convert.ToInt32
 
 let x,y,out = 
     mk_index "x",
     mk_index "y",
     mk_index "out"
 
 let m i j = And(x i,y j)
 
 let u,v = 
     mk_index2 "u",
     mk_index2 "v"
 
 let ml = multiplier m u v out 3
 
 // Checks if the variable x in the valuation v represent the binary 
 // number n.
 let isIn v n x =  
     let max = (n |> String.length) - 1
     [0..max]
     |> List.forall (fun i -> 
         let bit = n |> seq |> Seq.item(max-i) |> string
         toInt v (sprintf "%s_%i" x i) = System.Int32.Parse(bit)
     )
 
 let printIn v n x = 
     [0..n-1]
     |> List.sortDescending
     |> List.iter (fun i -> 
         try printf "%s" ((toInt v (sprintf "%s_%i" x i)) |> string)
         with _ -> printf " "
     )
     printfn ""
 
 allsatvaluations (eval ml) (fun _ -> false) (atoms ml)
 |> List.filter (fun v -> 
     "x" |> isIn v "110"
     && "y" |> isIn v "111"
 )
 |> List.iteri (fun i v -> 
     "x" |> printIn v 6
     "y" |> printIn v 6
     printfn "======"
     "out" |> printIn v 6
 )
val toInt: v: ('a -> bool) -> x: 'b -> int
val v: ('a -> bool)
type bool = System.Boolean
val x: 'b
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
val x: obj
val y: obj
val out: obj
val m: i: 'a -> j: 'b -> 'c
val i: 'a
val j: 'b
val u: obj
val v: obj
val ml: obj
val isIn: v: ('a -> bool) -> n: string -> x: string -> bool
val n: string
val x: string
val max: int
module String from Microsoft.FSharp.Core
val length: str: string -> int
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val forall: predicate: ('T -> bool) -> list: 'T list -> bool
val i: int
val bit: string
Multiple items
val seq: sequence: seq<'T> -> seq<'T>

--------------------
type seq<'T> = System.Collections.Generic.IEnumerable<'T>
module Seq from Microsoft.FSharp.Collections
val item: index: int -> source: seq<'T> -> 'T
Multiple items
val string: value: 'T -> string

--------------------
type string = System.String
val sprintf: format: Printf.StringFormat<'T> -> 'T
[<Struct>] type Int32 = member CompareTo: value: int -> int + 1 overload member Equals: obj: int -> bool + 1 overload member GetHashCode: unit -> int member GetTypeCode: unit -> TypeCode member ToString: unit -> string + 3 overloads member TryFormat: destination: Span<char> * charsWritten: byref<int> * ?format: ReadOnlySpan<char> * ?provider: IFormatProvider -> bool static member Abs: value: int -> int static member Clamp: value: int * min: int * max: int -> int static member CopySign: value: int * sign: int -> int static member CreateChecked<'TOther (requires 'TOther :> INumberBase<'TOther>)> : value: 'TOther -> int ...
<summary>Represents a 32-bit signed integer.</summary>
System.Int32.Parse(s: string) : int
System.Int32.Parse(s: string, provider: System.IFormatProvider) : int
System.Int32.Parse(s: string, style: System.Globalization.NumberStyles) : int
System.Int32.Parse(s: System.ReadOnlySpan<char>, provider: System.IFormatProvider) : int
System.Int32.Parse(s: string, style: System.Globalization.NumberStyles, provider: System.IFormatProvider) : int
System.Int32.Parse(s: System.ReadOnlySpan<char>, ?style: System.Globalization.NumberStyles, ?provider: System.IFormatProvider) : int
val printIn: v: ('a -> bool) -> n: int -> x: string -> unit
val n: int
val sortDescending: list: 'T list -> 'T list (requires comparison)
val iter: action: ('T -> unit) -> list: 'T list -> unit
val printf: format: Printf.TextWriterFormat<'T> -> 'T
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
val filter: predicate: ('T -> bool) -> list: 'T list -> 'T list
val v: (obj -> bool)
val iteri: action: (int -> 'T -> unit) -> list: 'T list -> unit
After evaluation the following is printed to the stdout. 
 000110
 000111
 ======
 101010

rippleshift u v c z w n

Full Usage: rippleshift u v c z w n

Parameters:
    u : int -> formula<'a> - A function that, given an index, returns a variable that represent the bit of the first addend at that bit.
    v : int -> formula<'a> - A function that, given an index, returns a variable that represent the bit of the second addend at that bit.
    c : int -> formula<'a> - A function that, given an index, returns a variable for the value of the carry (in and out) at that bit (index).
    z : formula<'a> - The variable that represent the less significant bit of the resulting sum.
    w : int -> formula<'a> - A function that, given an index, returns a variable that represent the bit of the sum addend at index+1.
    n : int - The number of bits of the operands added by the ripplecarry adder.

Returns: formula<'a> A Propexamples.ripplecarry0 with z as the less significant bit of the sum and w as the other bits

ripplecarry0 that, in the result, separates the less significant bit z from the other bits w.
((z <=> u_0 <=> ~v_0) /\ (c_2 <=> u_0 /\ v_0)) /\ (w_0 <=> (u_1 <=> ~v_1) <=> ~c_2) /\ (w_1 <=> u_1 /\ v_1 \/ (u_1 \/ v_1) /\ c_2)

u : int -> formula<'a>

A function that, given an index, returns a variable that represent the bit of the first addend at that bit.

v : int -> formula<'a>

A function that, given an index, returns a variable that represent the bit of the second addend at that bit.

c : int -> formula<'a>

A function that, given an index, returns a variable for the value of the carry (in and out) at that bit (index).

z : formula<'a>

The variable that represent the less significant bit of the resulting sum.

w : int -> formula<'a>

A function that, given an index, returns a variable that represent the bit of the sum addend at index+1.

n : int

The number of bits of the operands added by the ripplecarry adder.

Returns: formula<'a>

A Propexamples.ripplecarry0 with z as the less significant bit of the sum and w as the other bits

Example 

 // eval the atom at the input valuations and convert to int
 let toInt (v: prop -> bool) x =
     v (P x) |> System.Convert.ToInt32
 
 // rippleshift
 
 let u,v,c,w = 
     mk_index "u",
     mk_index "v",
     mk_index "c",
     mk_index "w"
 
 let rs = rippleshift u v c !>"z" w 2
 
 allsatvaluations (eval rs) (fun _ -> false) (atoms rs)
 |> List.iteri (fun i v -> 
     printfn "u     |   %A %A |" (toInt v "u_1") (toInt v "u_0")
     printfn "v     |   %A %A |" (toInt v "v_1") (toInt v "v_0")
     printfn "==============="
     printfn "w     | %A %A   |" 
         (toInt v "w_1")
         (toInt v "w_0")
     printfn "z     |     %A |" 
         (toInt v "z")
     printfn ""
 )
val toInt: v: ('a -> bool) -> x: 'b -> int
val v: ('a -> bool)
type bool = System.Boolean
val x: 'b
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
val u: obj
val v: obj
val c: obj
val w: obj
val rs: obj
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val iteri: action: (int -> 'T -> unit) -> list: 'T list -> unit
val i: int
val v: (obj -> bool)
val printfn: format: Printf.TextWriterFormat<'T> -> 'T
After evaluation the following is printed to the stdout. (Some result omitted for brevity.) 
 u     |   0 0 |
 v     |   0 0 |
 ===============
 w     | 0 0   |
 z     |     0 |
 
 u     |   0 0 |
 v     |   1 0 |
 ===============
 w     | 0 1   |
 z     |     0 |
 
 ...
 u     |   0 0 |
 v     |   1 1 |
 ===============
 w     | 0 1   |
 z     |     1 |
 ...
 
 u     |   1 1 |
 v     |   1 1 |
 ===============
 w     | 1 1   |
 z     |     0 |

Prime numbers

Functions and values

Function or value Description

bit n x

Full Usage: bit n x

Parameters:
    n : int - The index of the bit to extract.
    x : int - The decimal number to represent in binary notation.

Returns: bool The value of the bit at the given index.

Extract the nth bit (as a boolean value) of a nonnegative integer x.

n : int

The index of the bit to extract.

x : int

The decimal number to represent in binary notation.

Returns: bool

The value of the bit at the given index.

Example 

 bit 2 5
Evaluates to true.

bitlength x

Full Usage: bitlength x

Parameters:
    x : int - The decimal number to represent in binary notation.

Returns: int The number of bit needed to represent x in binary notation.

Returns the number of bit needed to represent x in binary notation.

x : int

The decimal number to represent in binary notation.

Returns: int

The number of bit needed to represent x in binary notation.

Example 

 bitlength 10
Evaluates to 4.

congruent_to x m n

Full Usage: congruent_to x m n

Parameters:
    x : int -> formula<'a> - The integer-to-string function that produces the indexed variables to encode the bits.
    m : int - The value to be encoded.
    n : int - The number of bits to use.

Returns: formula<'a> The propositional formula that is true in those valuations that assign to the variables the correct values to encode m in binary using n number of bits.

Produces a propositional formula asserting that the atoms x(i) encode the bits of a value m, at least modulo 2^n.

x : int -> formula<'a>

The integer-to-string function that produces the indexed variables to encode the bits.

m : int

The value to be encoded.

n : int

The number of bits to use.

Returns: formula<'a>

The propositional formula that is true in those valuations that assign to the variables the correct values to encode m in binary using n number of bits.

Example 

 congruent_to (mk_index "x") 10 4
Evaluates to `~x_0 /\ x_1 /\ ~x_2 /\ x_3`. A formula true just in the valuation \(x_0 \mapsto false, x_1 \mapsto true, x_2 \mapsto false, x_3 \mapsto true\) that (reverting and converting booleans to int) can be read as 1010.

Example 

 [0..10]
 |> List.map (fun i -> 
     let fm = congruent_to (mk_index "x") i (bitlength i)
     i,
     (allsatvaluations (eval fm) (fun _ -> false) (atoms fm))
     |> List.map (fun v -> 
         atoms fm
         |> Seq.map (v >> System.Convert.ToInt32 >> string)
         |> Seq.rev
         |> System.String.Concat
     )
     |> System.String.Concat
 )
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val map: mapping: ('T -> 'U) -> list: 'T list -> 'U list
val i: int
val fm: obj
val v: (obj -> obj)
module Seq from Microsoft.FSharp.Collections
val map: mapping: ('T -> 'U) -> source: seq<'T> -> seq<'U>
namespace System
type Convert = static member ChangeType: value: obj * conversionType: Type -> obj + 3 overloads static member FromBase64CharArray: inArray: char array * offset: int * length: int -> byte array static member FromBase64String: s: string -> byte array static member FromHexString: chars: ReadOnlySpan<char> -> byte array + 1 overload static member GetTypeCode: value: obj -> TypeCode static member IsDBNull: value: obj -> bool static member ToBase64CharArray: inArray: byte array * offsetIn: int * length: int * outArray: char array * offsetOut: int -> int + 1 overload static member ToBase64String: inArray: byte array -> string + 4 overloads static member ToBoolean: value: bool -> bool + 17 overloads static member ToByte: value: bool -> byte + 18 overloads ...
<summary>Converts a base data type to another base data type.</summary>
System.Convert.ToInt32(value: uint64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: uint16) : int
   (+0 other overloads)
System.Convert.ToInt32(value: string) : int
   (+0 other overloads)
System.Convert.ToInt32(value: float32) : int
   (+0 other overloads)
System.Convert.ToInt32(value: sbyte) : int
   (+0 other overloads)
System.Convert.ToInt32(value: obj) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int64) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int) : int
   (+0 other overloads)
System.Convert.ToInt32(value: int16) : int
   (+0 other overloads)
Multiple items
val string: value: 'T -> string

--------------------
type string = System.String
val rev: source: seq<'T> -> seq<'T>
Multiple items
type String = interface IEnumerable<char> interface IEnumerable interface ICloneable interface IComparable interface IComparable<string> interface IConvertible interface IEquatable<string> new: value: nativeptr<char> -> unit + 8 overloads member Clone: unit -> obj member CompareTo: value: obj -> int + 1 overload ...
<summary>Represents text as a sequence of UTF-16 code units.</summary>

--------------------
System.String(value: nativeptr<char>) : System.String
System.String(value: char array) : System.String
System.String(value: System.ReadOnlySpan<char>) : System.String
System.String(value: nativeptr<sbyte>) : System.String
System.String(c: char, count: int) : System.String
System.String(value: nativeptr<char>, startIndex: int, length: int) : System.String
System.String(value: char array, startIndex: int, length: int) : System.String
System.String(value: nativeptr<sbyte>, startIndex: int, length: int) : System.String
System.String(value: nativeptr<sbyte>, startIndex: int, length: int, enc: System.Text.Encoding) : System.String
System.String.Concat<'T>(values: System.Collections.Generic.IEnumerable<'T>) : string
   (+0 other overloads)
System.String.Concat([<System.ParamArray>] values: string array) : string
   (+0 other overloads)
System.String.Concat([<System.ParamArray>] args: obj array) : string
   (+0 other overloads)
System.String.Concat(arg0: obj) : string
   (+0 other overloads)
System.String.Concat(values: System.Collections.Generic.IEnumerable<string>) : string
   (+0 other overloads)
System.String.Concat(str0: string, str1: string) : string
   (+0 other overloads)
System.String.Concat(str0: System.ReadOnlySpan<char>, str1: System.ReadOnlySpan<char>) : string
   (+0 other overloads)
System.String.Concat(arg0: obj, arg1: obj) : string
   (+0 other overloads)
System.String.Concat(str0: string, str1: string, str2: string) : string
   (+0 other overloads)
System.String.Concat(str0: System.ReadOnlySpan<char>, str1: System.ReadOnlySpan<char>, str2: System.ReadOnlySpan<char>) : string
   (+0 other overloads)
Evaluates to [(0, ""); (1, "1"); (2, "10"); (3, "11"); (4, "100"); (5, "101"); (6, "110"); (7, "111"); (8, "1000"); (9, "1001"); (10, "1010")].

prime p

Full Usage: prime p

Parameters:
    p : int - The input number.

Returns: formula<prop> A propositional formula that is a tautology if p is prime.

Applied to a positive integer p generates a propositional formula that is a tautology precisely if p is prime.

p : int

The input number.

Returns: formula<prop>

A propositional formula that is a tautology if p is prime.

Example 

 prime 2
 // `~(((out_0 <=> x_0 /\ y_0) /\ ~out_1) /\ ~out_0 /\ out_1)`
 |> tautology
Evaluates to true.