Class: Udb::LogicNode::MemoizedState

Inherits:
T::Struct
  • Object
show all
Defined in:
lib/udb/logic.rb

Overview

object to hold results of expensive calculations LogicNode type and children are frozen at construction so we can safely remember and return these values

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(is_cnf: nil, cnf_form: nil, is_nested_cnf: nil, is_reduced: nil, terms: nil, literals: nil, is_satisfiable: nil, equisat_cnf: nil, equiv_cnf: nil)

Parameters:

  • is_cnf (Boolean, nil) (defaults to: nil) —

    when true, the formula is known to be in CNF form when false, the formula is known to not be in CNF form

  • cnf_form (LogicNode, nil) (defaults to: nil) —

    when not nil, an equisatisfiable representation of self in CNF form

  • is_nested_cnf (Boolean, nil) (defaults to: nil) —

    when true, a flattened version of the formula would be CNF when false, a flattened version of the formula would not be CNF

  • is_reduced (Boolean, nil) (defaults to: nil) —

    when true, the formula would be unaltered by calling reduce when false, the formula would be reduced further by calling reduce

  • terms (Array<TermType>, nil) (defaults to: nil) —

    list of terms in the formula

  • literals (Array<TermType>, nil) (defaults to: nil) —

    list of literals in the formula

  • is_satisfiable (Boolean, nil) (defaults to: nil) —

    when true, formula is known to be satisfiable when false, formula is known to be unsatisfiable

  • equisat_cnf (LogicNode, nil) (defaults to: nil) —

    result of #equisat_cnf

  • equiv_cnf (LogicNode, nil) (defaults to: nil) —

    result of #equisat_cnf




# File ''

prop :is_cnf, T.nilable(T::Boolean)
prop :cnf_form, T.nilable(LogicNode)
prop :is_nested_cnf, T.nilable(T::Boolean)
prop :is_reduced, T.nilable(T::Boolean)
prop :terms, T.nilable(T::Array[TermType])
prop :literals, T.nilable(T::Array[TermType])
prop :is_satisfiable, T.nilable(T::Boolean)
prop :equisat_cnf, T.nilable(LogicNode)
prop :equiv_cnf, T.nilable(LogicNode)

Instance Attribute Details

#cnf_form ⇒ LogicNode?

when not nil, an equisatisfiable representation of self in CNF form

Returns:




# File ''

prop :cnf_form, T.nilable(LogicNode)

#equisat_cnf ⇒ LogicNode?

result of #equisat_cnf

Returns:




# File ''

prop :equisat_cnf, T.nilable(LogicNode)

#equiv_cnf ⇒ LogicNode?

result of #equisat_cnf

Returns:




# File ''

prop :equiv_cnf, T.nilable(LogicNode)

#is_cnf ⇒ Boolean?

when true, the formula is known to be in CNF form when false, the formula is known to not be in CNF form

Returns:

  • (Boolean, nil) 



# File ''

prop :is_cnf, T.nilable(T::Boolean)

#is_nested_cnf ⇒ Boolean?

when true, a flattened version of the formula would be CNF when false, a flattened version of the formula would not be CNF

Returns:

  • (Boolean, nil) 



# File ''

prop :is_nested_cnf, T.nilable(T::Boolean)

#is_reduced ⇒ Boolean?

when true, the formula would be unaltered by calling reduce when false, the formula would be reduced further by calling reduce

Returns:

  • (Boolean, nil) 



# File ''

prop :is_reduced, T.nilable(T::Boolean)

#is_satisfiable ⇒ Boolean?

when true, formula is known to be satisfiable when false, formula is known to be unsatisfiable

Returns:

  • (Boolean, nil) 



# File ''

prop :is_satisfiable, T.nilable(T::Boolean)

#literals ⇒ Array<TermType>?

list of literals in the formula

Returns:




# File ''

prop :literals, T.nilable(T::Array[TermType])

#terms ⇒ Array<TermType>?

list of terms in the formula

Returns:




# File ''

prop :terms, T.nilable(T::Array[TermType])