b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnikmodule Hets
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik class ProveOptions < HetsOptions
0f04241fc90f134af0272eb0999e75fb6749b595Pavel Březina # Hets has problems finding the conjecture of TPTP if we pass the
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik # theorems-array in the prove-request.
0f04241fc90f134af0272eb0999e75fb6749b595Pavel Březina SINGLE_THEOREM_INPUT_TYPES = %w(tptp)
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik def initialize(opts = {})
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik @need_to_normalize_timeout = opts.has_key?(:timeout)
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik super(opts)
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik end
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik def add(**opts)
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik @need_to_normalize_timeout = opts.has_key?(:timeout)
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik super(**opts)
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik end
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik def single_theorem_input_type?
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik SINGLE_THEOREM_INPUT_TYPES.include?(options[:'input-type'])
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik end
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik
4ddd5591c50e27dffa55f03fbce0dcc85cd50a8bPavel Březina protected
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik def prepare
4ddd5591c50e27dffa55f03fbce0dcc85cd50a8bPavel Březina super
a2057618f30a3c64bdffb35a2ef3c2ba148c8a03Pavel Březina prepare_node
b24e4bec819b29f1ec8e77083d4e7610c5dd9c77Lukas Slebodnik prepare_prover
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina prepare_timeout
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina prepare_axioms
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina prepare_theorems
4ddd5591c50e27dffa55f03fbce0dcc85cd50a8bPavel Březina end
4ddd5591c50e27dffa55f03fbce0dcc85cd50a8bPavel Březina
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina def prepare_node
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina @ontology = @options[:ontology]
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina if @ontology.is_a?(Ontology)
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina @options[:node] = @ontology.name if @ontology.in_distributed?
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina @options.delete(:ontology)
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina def prepare_prover
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina if @options[:prover].is_a?(Prover)
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina @options[:prover] = @options[:prover].name
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina def prepare_timeout
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina normalize_timeout
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina if @options[:timeout].is_a?(Fixnum)
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina @options[:timeout] = @options[:timeout].to_s
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina def prepare_axioms
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina prepare_sentences(:axioms)
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina def prepare_theorems
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina prepare_sentences(:theorems)
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina options.delete(:theorems) if single_theorem_input_type?
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina def prepare_sentences(field)
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina if @options[field].respond_to?(:map)
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina @options[field].map! do |sentence_or_name|
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina if sentence_or_name.is_a?(Sentence)
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina sentence_or_name.name
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina else
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina # This is already a prepared string (sentence name).
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina sentence_or_name
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina # Hets considers the given timeout as "timeout per goal"
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina # Ontohub considers the selected timeout as "overall timeout"
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina # This should be normalized once after setting the timeout.
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina def normalize_timeout
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina if @need_to_normalize_timeout
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina if @options[:timeout]
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina # Hets can only handle integers as the timeout.
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina @options[:timeout] = [1, @options[:timeout].to_i / goals_count].max
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina @need_to_normalize_timeout = false
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina def goals_count
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina if @options[:theorems]
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina @options[:theorems].size
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina elsif @ontology && @ontology.in_distributed?
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina @ontology.theorems.original.count
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina else
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina 1
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina end
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březinaend
dea636af4d1902a081ee891f1b19ee2f8729d759Pavel Březina