Cong (Calculemus)

Cong Module

Namespace: Calculemus
Assembly: Calculemus.dll

Congruence closure.

Functions and values

Function or value Description


                
                  
                    
                      ccsatisfiable fms

Full Usage: ccsatisfiable fms

Parameters:

fms : formula<fol> list - The input list of equations/inequations.

Returns: bool true, if the input list of equations/inequations is satisfiable; otherwise, false.

Tests if a list of ground equations and inequations is satisfiable.

fms : formula<fol> list: The input list of equations/inequations.

Returns: bool: true, if the input list of equations/inequations is satisfiable; otherwise, false.

Exception Thrown with message dest_eq: not an equation when one of the input formulas is not an equation/inequation.

Example

 !!>["m(0,1)=1";"~(m(0,1)=0)"]
 |> ccsatisfiable

Evaluates to true.

Example

 !!>["m(0,1)=1";"~(m(0,1)=1)"]
 |> ccsatisfiable

Evaluates to false.

Example

 !!>["P(0)"]
 |> ccsatisfiable

Throws System.Exception: dest_eq: not an equation.

Full Usage: ccvalid fm

Parameters:

fm : formula<fol> - The input equation/inequation.

Returns: bool true, if the input equation/inequation is valid; otherwise, false.

Tests if an equation/inequation is valid

fm : formula<fol>: The input equation/inequation.

Returns: bool: true, if the input equation/inequation is valid; otherwise, false.

Exception Thrown with message dest_eq: not an equation when the input formulas is not an equation or inequation.

Example

 !! @"f(f(f(f(f(c))))) = c /\ f(f(f(c))) = c
 ==> f(c) = c \/ f(g(c)) = g(f(c))"
 |> ccvalid

Evaluates to true.

Example

 !! @"f(f(f(f(c)))) = c /\ f(f(c)) = c ==> f(c) = c"
 ==> f(c) = c 
 |> ccvalid

Evaluates to true.

Example

 !!"P(0)"
 |> ccvalid

Throws System.Exception: dest_eq: not an equation.


                
                  
                    
                      congruent eqv (s, t)

Full Usage: congruent eqv (s, t)

Parameters:

eqv : partition<term> - The input congruence.

s : term - The first input term.

t : term - The second input term.

Returns: bool true, if all the the input terms immediate subterms are already equivalent; otherwise, false.

Checks if s and t should be equated by a 1-step congruence.

eqv : partition<term>: The input congruence.
s : term: The first input term.
t : term: The second input term.

Returns: bool: true, if all the the input terms immediate subterms are already equivalent; otherwise, false.

Example

 congruent 
     (equate (!!!"2",!!!"4")unequal) 
     (!!!"f(4)", !!!"f(2)")

Evaluates to true.

Example

 congruent 
     (equate (!!!"2",!!!"4")unequal) 
     (!!!"f(4)", !!!"f(3)")

Evaluates to false.


                
                  
                    
                      emerge (s, t) (eqv, pfn)

Full Usage: emerge (s, t) (eqv, pfn)

Parameters:

s : term - The first input term.

t : term - The second input term.

eqv : partition<term> - The input congruence.

pfn : func<term, term list> - The input `predecessor function'.

Returns: partition<term> * func<term, term list> The extended congruence relation together with the updated predecessor function.

Extends the terms congruence relation eqv with the new equivalence s ~ t.

The algorithm maintains a `predecessor function' pfn mapping each canonical representative \(s\) of an equivalence class \(C\) to the set of terms of which some \(s' \in C\) is an immediate subterm.

s : term: The first input term.
t : term: The second input term.
eqv : partition<term>: The input congruence.
pfn : func<term, term list>: The input `predecessor function'.

Returns: partition<term> * func<term, term list>: The extended congruence relation together with the updated predecessor function.

Example

 (unequal,undefined)
 |> emerge (!!!"0",!!!"1") 
 |> fun (Partition f,pfn) -> graph f, graph pfn

val f: obj

val pfn: obj

Evaluates to ([(``0``, Nonterminal ``1``); (``1``, Terminal (``1``, 2))], [(``1``, [])]).


                
                  
                    
                      predecessors t pfn

Full Usage: predecessors t pfn

Parameters:

t : term - The input term.

pfn : func<term, term list> - The input `predecessor function'.

Returns: func<term, term list> The `predecessor function' updated with a new mapping for each immediate subterm of the term.

Updates a predecessor function with a new mapping for each immediate subterm of a term.

t : term: The input term.
pfn : func<term, term list>: The input `predecessor function'.

Returns: func<term, term list>: The `predecessor function' updated with a new mapping for each immediate subterm of the term.

Example

 predecessors !!!"f(0,g(1,0))" undefined
 |> graph

Evaluates to [(``0``, [``f(0,g(1,0))``]); (``g(1,0)``, [``f(0,g(1,0))``])].


                
                  
                    
                      subterms tm

Full Usage: subterms tm

Parameters:

tm : term - The input term.

Returns: term list The list of subterms of the input term.

Returns all subterms of a term.

tm : term: The input term.

Returns: term list: The list of subterms of the input term.

Example

 subterms !!!"f(g(x),y)"

Evaluates to [``x``; ``y``; ``f(g(x),y)``; ``g(x)``].