sine_axiom_selection.rb revision 01f82915d3add64f685ccd7d9386a424e54a3587
bcb4e51a409d94ae670de96afb8483a4f7855294Stephan Boschclass SineAxiomSelection < ActiveRecord::Base
5e0ce63bb65db34d7f48b34bbb5545fa791781c4Timo Sirainen acts_as :axiom_selection
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen
a857fb61f1cc77a81d18adee6a95ae04c27a5ffbTimo Sirainen attr_accessible :commonness_threshold, :depth_limit, :tolerance
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen validates_numericality_of :commonness_threshold,
1904e2fc786dbc037039d284b371730777277fc5Aki Tuomi greater_than_or_equal_to: 0,
1904e2fc786dbc037039d284b371730777277fc5Aki Tuomi only_integer: true
1904e2fc786dbc037039d284b371730777277fc5Aki Tuomi # Special case: The depth limit of -1 is considered to be infinite.
a95a4743552a44f95f72e9bd3ad41cc44609632dTimo Sirainen validates_numericality_of :depth_limit,
1904e2fc786dbc037039d284b371730777277fc5Aki Tuomi greater_than_or_equal_to: -1,
fb09842fd58e4f8c30de9dd0836434c712c62198Timo Sirainen only_integer: true
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen validates_numericality_of :tolerance, greater_than_or_equal_to: 1
5a35caefcf8cf38c347f8406b26701487c8cda57Timo Sirainen
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen delegate :lock_key, :mark_as_finished!, to: :axiom_selection
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen def call
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen Semaphore.exclusively(lock_key) do
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen unless finished
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen preprocess
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen select_axioms
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen mark_as_finished!
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen end
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen end
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen end
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen protected
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen def ontology
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen @ontology ||= goal.ontology
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen end
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen def goal
35283613d4c04ce18836e9fc431582c87b3710a0Timo Sirainen @goal ||= proof_attempt_configurations.first.proof_attempt.theorem
35283613d4c04ce18836e9fc431582c87b3710a0Timo Sirainen end
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen def preprocess
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen calculate_commonness_table
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen calculate_symbol_axiom_trigger_table
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen end
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen def calculate_commonness_table
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen ontology.symbols.each { |symbol| calculate_commonness(symbol) }
a07b1d77c546256eebda95b7c403e92e1bbcbe94Timo Sirainen end
a07b1d77c546256eebda95b7c403e92e1bbcbe94Timo Sirainen
a07b1d77c546256eebda95b7c403e92e1bbcbe94Timo Sirainen # Number of axioms in which the symbol occurs
a07b1d77c546256eebda95b7c403e92e1bbcbe94Timo Sirainen def calculate_commonness(symbol)
a07b1d77c546256eebda95b7c403e92e1bbcbe94Timo Sirainen ssc = SineSymbolCommonness.
a07b1d77c546256eebda95b7c403e92e1bbcbe94Timo Sirainen where(symbol_id: symbol.id,
a07b1d77c546256eebda95b7c403e92e1bbcbe94Timo Sirainen axiom_selection_id: axiom_selection.id).first_or_initialize
a07b1d77c546256eebda95b7c403e92e1bbcbe94Timo Sirainen unless ssc.commonness
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen ssc.commonness = query_commonness(symbol)
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen ssc.save!
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen end
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen end
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen def query_commonness(symbol)
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen ontology.all_axioms.joins(:symbols).where(:'symbols.id' => symbol.id).count
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen end
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen def calculate_symbol_axiom_trigger_table
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen ontology.all_axioms.each do |axiom|
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen axiom.symbols.each do |symbol|
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen calculate_symbol_axiom_trigger(symbol, axiom)
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen end
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen end
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen end
a3fe8c0c54d87822f4b4f8f0d10caac611861b2bTimo Sirainen
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen def calculate_symbol_axiom_trigger(symbol, axiom)
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen ssat = SineSymbolAxiomTrigger.
a3fe8c0c54d87822f4b4f8f0d10caac611861b2bTimo Sirainen where(symbol_id: symbol.id,
a3fe8c0c54d87822f4b4f8f0d10caac611861b2bTimo Sirainen axiom_id: axiom.id,
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen axiom_selection_id: axiom_selection.id).first_or_initialize
a3fe8c0c54d87822f4b4f8f0d10caac611861b2bTimo Sirainen unless ssat.tolerance
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen ssat.tolerance = needed_tolerance(symbol, axiom)
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen ssat.save!
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen end
a3fe8c0c54d87822f4b4f8f0d10caac611861b2bTimo Sirainen end
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen def needed_tolerance(symbol, axiom)
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen lcs_commonness = commonness_of_least_common_symbol(axiom)
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen sym_commonness = symbol.sine_symbol_commonness.commonness
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen sym_commonness.to_f / lcs_commonness.to_f
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen end
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen def least_common_symbol(axiom)
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen axiom.symbols.includes(:sine_symbol_commonness).
a3fe8c0c54d87822f4b4f8f0d10caac611861b2bTimo Sirainen order('sine_symbol_commonnesses.commonness ASC').first
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen end
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen def commonness_of_least_common_symbol(axiom)
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen least_common_symbol(axiom).sine_symbol_commonness.commonness
a3fe8c0c54d87822f4b4f8f0d10caac611861b2bTimo Sirainen end
94d0d29f23083c4e79a3fc6b76e9ed761b0e3511Timo Sirainen
a3fe8c0c54d87822f4b4f8f0d10caac611861b2bTimo Sirainen def select_axioms
a3fe8c0c54d87822f4b4f8f0d10caac611861b2bTimo Sirainen @selected_axioms = []
a3fe8c0c54d87822f4b4f8f0d10caac611861b2bTimo Sirainen select_new_axioms(goal, 0)
a3fe8c0c54d87822f4b4f8f0d10caac611861b2bTimo Sirainen self.axioms = @selected_axioms
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen end
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen def select_new_axioms(sentence, current_depth)
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen return if depth_limit_reached?(current_depth)
eb627e89fba85791ec894e57f96752b1bd64d001Timo Sirainen new_axioms = select_axioms_by_sentence(sentence) - @selected_axioms
eb627e89fba85791ec894e57f96752b1bd64d001Timo Sirainen @selected_axioms += new_axioms
eb627e89fba85791ec894e57f96752b1bd64d001Timo Sirainen new_axioms.each { |axiom| select_new_axioms(axiom, current_depth + 1) }
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen end
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen def select_axioms_by_sentence(sentence)
eb627e89fba85791ec894e57f96752b1bd64d001Timo Sirainen sentence.symbols.map { |symbol| triggered_axioms(symbol) }.flatten
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen end
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen def triggered_axioms(symbol)
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen Axiom.unscoped.joins(:sine_symbol_axiom_triggers).
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen where('sine_symbol_axiom_triggers.symbol_id = ?', symbol.id).
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen where('sine_symbol_axiom_triggers.tolerance <= ?', tolerance)
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen end
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen def depth_limit_reached?(current_depth)
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen depth_limited? && current_depth >= depth_limit
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen end
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen
30be8c9beaa6944c13d80130fa7a1778b2f8a470Timo Sirainen def depth_limited?
53d794b1cb99c0cc437ec9449d19abf504058390Timo Sirainen depth_limit != -1
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen end
a857fb61f1cc77a81d18adee6a95ae04c27a5ffbTimo Sirainenend
cd2ed64888b42b481cde6bb9548c8520516fa3e9Timo Sirainen