sine_axiom_selection.rb revision 8d41e86f44b1fab6f02e776d7d4851a614a61916
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engenclass SineAxiomSelection < ActiveRecord::Base
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen acts_as :axiom_selection
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen attr_accessible :commonness_threshold, :depth_limit, :tolerance
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen validates_numericality_of :commonness_threshold,
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen greater_than_or_equal_to: 0,
391260dcb2ae8060134b635bc268ccdecf59003dDwight Engen only_integer: true
391260dcb2ae8060134b635bc268ccdecf59003dDwight Engen # Special case: The depth limit of -1 is considered to be infinite.
391260dcb2ae8060134b635bc268ccdecf59003dDwight Engen validates_numericality_of :depth_limit,
391260dcb2ae8060134b635bc268ccdecf59003dDwight Engen greater_than_or_equal_to: -1,
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen only_integer: true
391260dcb2ae8060134b635bc268ccdecf59003dDwight Engen validates_numericality_of :tolerance, greater_than_or_equal_to: 1
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen
391260dcb2ae8060134b635bc268ccdecf59003dDwight Engen delegate :mark_as_finished!, to: :axiom_selection
391260dcb2ae8060134b635bc268ccdecf59003dDwight Engen
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen def call
391260dcb2ae8060134b635bc268ccdecf59003dDwight Engen preprocess
391260dcb2ae8060134b635bc268ccdecf59003dDwight Engen select_axioms
391260dcb2ae8060134b635bc268ccdecf59003dDwight Engen end
391260dcb2ae8060134b635bc268ccdecf59003dDwight Engen
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen protected
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen def ontology
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen @ontology ||= goal.ontology
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen end
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen def goal
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen @goal ||= axiom_selection.proof_attempt_configuration.proof_attempt.theorem
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen end
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen def preprocess
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen calculate_commonness_table
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen calculate_symbol_axiom_trigger_table
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen end
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen def calculate_commonness_table
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen ontology.symbols.each { |symbol| calculate_commonness(symbol) }
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen end
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen # Number of axioms in which the symbol occurs
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen def calculate_commonness(symbol)
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen ssc = SineSymbolCommonness.
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen where(symbol_id: symbol.id,
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen axiom_selection_id: axiom_selection.id).first_or_initialize
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen unless ssc.commonness
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen ssc.commonness = query_commonness(symbol)
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen ssc.save!
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen end
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen end
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen def query_commonness(symbol)
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen ontology.all_axioms.joins(:symbols).where(:'symbols.id' => symbol.id).count
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen end
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen def calculate_symbol_axiom_trigger_table
7ceebfd12a0503bee5eaab8d4c062a4389939a61Dwight Engen ontology.all_axioms.each do |axiom|
axiom.symbols.each do |symbol|
calculate_symbol_axiom_trigger(symbol, axiom)
end
end
end
def calculate_symbol_axiom_trigger(symbol, axiom)
ssat = SineSymbolAxiomTrigger.
where(symbol_id: symbol.id,
axiom_id: axiom.id,
axiom_selection_id: axiom_selection.id).first_or_initialize
unless ssat.tolerance
ssat.tolerance = needed_tolerance(symbol, axiom)
ssat.save!
end
end
def needed_tolerance(symbol, axiom)
lcs_commonness = commonness_of_least_common_symbol(axiom)
sym_commonness = symbol.sine_symbol_commonness.commonness
sym_commonness.to_f / lcs_commonness.to_f
end
def least_common_symbol(axiom)
axiom.symbols.includes(:sine_symbol_commonness).
order('sine_symbol_commonnesses.commonness ASC').first
end
def commonness_of_least_common_symbol(axiom)
least_common_symbol(axiom).sine_symbol_commonness.commonness
end
def select_axioms
@selected_axioms = []
select_new_axioms(goal)
self.axioms = @selected_axioms
end
def select_new_axioms(sentence)
new_axioms = select_axioms_by_sentence(sentence) - @selected_axioms
@selected_axioms += new_axioms
new_axioms.each { |axiom| select_new_axioms(axiom) }
end
def select_axioms_by_sentence(sentence)
sentence.symbols.map { |symbol| triggered_axioms(symbol) }.flatten
end
def triggered_axioms(symbol)
Axiom.unscoped.joins(:sine_symbol_axiom_triggers).
where('sine_symbol_axiom_triggers.symbol_id = ?', symbol.id).
where('sine_symbol_axiom_triggers.tolerance <= ?', tolerance)
end
end