proof_attempt.rb revision 5a102b3c56d4ac75632c7e9244ee0ce5bdbbf13a
bcb4e51a409d94ae670de96afb8483a4f7855294Stephan Boschclass ProofAttempt < LocIdBaseModel
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen include Numbering
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen include StateUpdater
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen numbering_parent_column 'sentence_id'
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen belongs_to :theorem, foreign_key: 'sentence_id'
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen belongs_to :proof_status
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen belongs_to :prover
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen belongs_to :proof_attempt_configuration, dependent: :destroy
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen has_one :axiom_selection, through: :proof_attempt_configuration
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen has_one :prover_output, dependent: :destroy
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen has_one :tactic_script, dependent: :destroy
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen has_many :generated_axioms, dependent: :destroy
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen has_and_belongs_to_many :used_axioms,
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen class_name: 'Axiom',
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen association_foreign_key: 'sentence_id',
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen join_table: 'used_axioms_proof_attempts'
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen has_and_belongs_to_many :used_theorems,
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen class_name: 'Theorem',
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen association_foreign_key: 'sentence_id',
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen join_table: 'used_axioms_proof_attempts'
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen attr_accessible :time_taken,
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen :number,
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen :state,
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen :state_updated_at,
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen :last_error
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen validates :state, inclusion: {in: State::STATES}
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen validates :theorem, presence: true
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen before_save :set_default_proof_status
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen after_save :update_theorem_status
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
53a00f21e1af586498f94220038aa21fb3861b37Timo Sirainen scope :latest, order('number DESC')
53a00f21e1af586498f94220038aa21fb3861b37Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen has_one :ontology, through: :theorem
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen def set_default_proof_status
53a00f21e1af586498f94220038aa21fb3861b37Timo Sirainen self.proof_status ||= ProofStatus.find(ProofStatus::DEFAULT_OPEN_STATUS)
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen end
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
28e3b41961f0e4004688d68002d005551fac3adfTimo Sirainen def generate_locid_string
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen sep = '//'
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen klass = self.class.to_s.underscore.dasherize
53a00f21e1af586498f94220038aa21fb3861b37Timo Sirainen "#{theorem.locid}#{sep}#{klass}-#{number}"
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen end
53a00f21e1af586498f94220038aa21fb3861b37Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen def update_theorem_status
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen theorem.update_proof_status!
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen end
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen def associate_prover_with_ontology_version
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen ontology_version = theorem.ontology.current_version
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen unless ontology_version.provers.include?(prover)
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen ontology_version.provers << prover
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen ontology_version.save!
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen end
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen end
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen def retry_failed
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen ProofExecutionWorker.perform_async(id)
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen end
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen def proper_subset_of_axioms_selected?
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen selected = proof_attempt_configuration.axiom_selection.axioms
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen available = theorem.ontology.axioms
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen selected.any? && selected.count < available.count
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen end
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainenend
3dd0679b6f24be0287cc42d7a60bbf59cdf8b637Timo Sirainen