Logtk.Congruence.FO · logtk 1.6

logtk

Core types and algorithms for logic

Version

Overview Documentation

IN THIS PACKAGE

library logtk
- module Logtk
  - module AllocCache
    
    module Arr
  - module Binder
    
    module TPTP
    
    module ZF
  - module Builtin
    
    module Arith
    
    module ArithOp
    
    module Map
    
    module Set
    
    module TPTP
    
    module Tag
    
    module Tbl
    
    module ZF
  - module Cnf
  - module Comparison
    
    module type PARTIAL_ORD
  - module Compute_prec
  - module Congruence
    
    module FO
    
    module Make
    
    argument 1-T
    
    module type TERM
  - module Congruence_intf
    
    module type S
  - module DBEnv
  - module Defined_pos
    
    module Arr
  - module Dtree
    
    module Default
    
    module Make
    
    argument 1-E
  - module FV_tree
    
    module Make
    
    argument 1-C
    
    module Feature_fun
  - module FeatureVector
    
    module Make
    
    argument 1-C
    
    module Feature
  - module Fingerprint
    
    module Make
    
    argument 1-X
    
    module Leaf
  - module FixpointUnif
  - module Flex_state
  - module HO_unif
  - module HVar
  - module Hash
  - module Hashcons
    
    module type HashedType
    
    module Make
    
    argument 1-X
    
    module MakeNonWeak
    
    argument 1-X
    
    module type S
  - module IArray
  - module ID
    
    module Map
    
    module Set
    
    module Tbl
  - module Ind_ty
  - module Index
    
    module BasicEquation
    
    module MakeLeaf
    
    argument 1-X
  - module Index_intf
    
    module type CLAUSE
    
    module type EQUATION
    
    module type LEAF
    
    module type SUBSUMPTION_IDX
    
    module C
    
    module type TERM_IDX
    
    module Leaf
    
    module type UNIT_IDX
    
    module E
  - module InnerTerm
    
    module DB
    
    module Map
    
    module Pos
    
    module Seq
    
    module Set
    
    module Tbl
    
    module VarMap
    
    module VarSet
    
    module VarTbl
  - module Input_format
  - module Int_lit
    
    module Focus
    
    module Seq
    
    module Util
  - module Interfaces
    
    module type EQ
    
    module type GROUP
    
    module type HASH
    
    module type ITER
    
    module type MONOID
    
    module type ORD
    
    module type PRINT
    
    module type PRINT1
    
    module type PRINT2
    
    module type PRINT3
    
    module type PRINT_DE_BRUIJN
    
    module type PRINT_OVERLOAD
  - module JPFull
    
    module Make
    
    argument 1-S
  - module JP_unif
    
    module S
  - module Lambda
    
    module Inner
  - module LazyList
  - module Literal
    
    module Comp
    
    module Conv
    
    module Pos
    
    module Seq
    
    module Set
    
    module View
  - module Literals
    
    module Conv
    
    module Pos
    
    module Seq
    
    module View
  - module Monome
    
    module Focus
    
    module Int
    
    module Modulo
    
    module Solve
    
    module Rat
    
    module Seq
  - module Multiset
    
    module Make
    
    argument 1-X
    
    module Seq
  - module Multiset_intf
    
    module type S
    
    module Seq
  - module Multisets
    
    module MMT
    
    module Seq
    
    module MT
    
    module Seq
  - module NPDtree
    
    module Make
    
    argument 1-E
    
    module MakeTerm
    
    argument 1-X
    
    module Leaf
  - module Options
  - module Ordering
  - module Ordinal
  - module Output_format
  - module PUnif
    
    module IntSet
    
    module Make
    
    argument 1-S
  - module ParseLocation
    
    module Infix
  - module PatternUnif
    
    module S
  - module Position
    
    module Build
    
    module Map
    
    module With
    
    module Infix
  - module PragUnifParams
  - module Precedence
    
    module Constr
    
    module Seq
    
    module Weight
    
    module Infix
  - module Proof
    
    module Kind
    
    module Parent
    
    module Result
    
    module Rule
    
    module S
    
    module Tbl
    
    module Src
    
    module Step
  - module Rat_lit
    
    module Focus
    
    module Seq
  - module Rewrite
    
    module Defined_cst
    
    module Lit
    
    module Rule
    
    module Rule
    
    module Rule_set
    
    module Term
    
    module Rule
    
    module Rule_inst_set
    
    module Set
  - module SLiteral
    
    module TPTP
    
    module ZF
  - module STerm
    
    module Map
    
    module Seq
    
    module Set
    
    module StrMap
    
    module StringSet
    
    module TPTP
    
    module TPTP_THF
    
    module Tbl
    
    module ZF
  - module Scoped
  - module Signal
  - module Signature
    
    module Seq
  - module Skolem
  - module SolidSubsumption
    
    module Make
    
    argument 1-S
  - module SolidUnif
    
    module Make
    
    argument 1-S
  - module Statement
    
    module Seq
    
    module TPTP
    
    module ZF
  - module Subst
    
    module FO
    
    module Projection
    
    module Renaming
    
    module type SPECIALIZED
    
    module Ty
  - module Term
    
    module AC
    
    argument 1-A
    
    module type AC_SPEC
    
    module Arith
    
    module Classic
    
    module Conv
    
    module DB
    
    module Form
    
    module IntMap
    
    module Map
    
    module Pos
    
    module Seq
    
    module Set
    
    module TPTP
    
    module Tbl
    
    module VarMap
    
    module VarSet
    
    module VarTbl
    
    module ZF
  - module Test_prop
  - module Type
    
    module Conv
    
    module Map
    
    module Seq
    
    module Set
    
    module TPTP
    
    module Tbl
    
    module VarMap
    
    module VarSet
    
    module VarTbl
    
    module ZF
  - module TypeInference
    
    module Ctx
    
    module TyBuiltin
  - module TypedSTerm
    
    module Form
    
    module Map
    
    module Seq
    
    module Set
    
    module Subst
    
    module TPTP
    
    module TPTP_THF
    
    module Tbl
    
    module Ty
    
    module UStack
    
    module Var_tbl
    
    module ZF
  - module Unif
    
    module FO
    
    module Inner
    
    module Ty
  - module UnifFramework
    
    module Make
    
    argument 1-X
    
    module type PARAMETERS
  - module Unif_constr
    
    module FO
  - module Unif_intf
    
    module type S
  - module Unif_subst
    
    module FO
  - module UnionFind
    
    module Make
    
    argument 1-P
    
    module type PAIR
  - module UntypedAST
    
    module A
  - module Util
    
    module Exn
    
    module Flag
    
    module Int_map
    
    module Int_set
    
    module Section
  - module Var
    
    module Set
    
    module Subst
library logtk.parsers
- module Logtk_parsers
  - module Ast_dk
    
    module Map
    
    module Seq
    
    module Set
    
    module StrMap
    
    module StringSet
    
    module TPTP
    
    module TPTP_THF
    
    module Tbl
    
    module ZF
  - module Ast_tptp
  - module CallProver
    
    module Eprover
    
    module Prover
  - module Lex_dk
  - module Lex_tptp
  - module Lex_zf
  - module Parse_dk
  - module Parse_tptp
  - module Parse_zf
  - module Parsing_utils
  - module Tip_ast
  - module Tip_lexer
  - module Tip_parser
  - module Trace_tstp
    
    module StepTbl
  - module Util_dk
  - module Util_tip
  - module Util_tptp
  - module Util_zf
library logtk.proofs
- module Logtk_proofs
  - module LLProof
    
    module Dot
    
    module Tbl
  - module LLProof_check
  - module LLProof_conv
  - module LLProver
  - module LLTerm
    
    module Conv
    
    module Form
    
    module Int_op
    
    module type LINEXP
    
    module Linexp_int
    
    module Linexp_rat
    
    module Rat_op
    
    module Set
library logtk.solving
- module Logtk_solving
  - module Lpo
    
    module Constraint
    
    module Seq
    
    module FO
    
    module Solution
    
    module TypedSTerm

Module Logtk . Congruence . FO

type term = Term.t

type t

Represents a congruence

val create : ?size:int -> unit -> t

New congruence.

parameter size
a hint for the initial size of the hashtable.

val iter : t -> ( mem:term -> repr:term -> unit ) -> unit

Iterate on terms that are explicitly present in the congruence. The callback is given mem, the term itself, and repr, the current representative of the term mem.

Invariant: when calling iter cc f, if f ~mem ~repr is called, then find cc mem == repr holds.

val iter_roots : t -> ( term -> unit ) -> unit

Iterate on the congruence classes' representative elements. Exactly one term per congruence class will be passed to the function.

val add : t -> term -> t

Add the term to the congruence closure

val mk_eq : t -> term -> term -> t

mk_eq congruence t1 t2 asserts that t1 = t2 belongs to the congruence

val is_eq : t -> term -> term -> bool

Returns true if the two terms are equal in the congruence. This updates the congruence, because the two terms need to be added.

val pp_debug : t CCFormat.printer