Class: ADSL::FOL::ForAll

Inherits:
Object show all
Defined in:
lib/adsl/fol/first_order_logic.rb

Instance Method Summary collapse

Constructor Details

#initialize(*params) ⇒ ForAll

Returns a new instance of ForAll.

Raises:

  • (ArgumentError)


102
103
104
105
106
107
# File 'lib/adsl/fol/first_order_logic.rb', line 102

def initialize(*params)
  params = params.flatten
  raise ArgumentError, "At least a formula required" if params.length < 1
  @args = params.first(params.length - 1)
  @formula = params.last
end

Instance Method Details

#resolve_spassObject



109
110
111
112
113
114
115
116
# File 'lib/adsl/fol/first_order_logic.rb', line 109

def resolve_spass
  args = @args.map{ |obj| obj.resolve_spass }
  formula = @formula.resolve_spass
  return formula if args.empty?
  return 'true' if formula == 'true'
  return 'false' if formula == 'false'
  "forall( [#{args.join(', ')}], #{formula})" 
end