app/models/proof_attempt.rb

	proof_attempt.rb revision 54a1f4b81d3db8dae3af04f4200ed7e14bf2543b
883N/Aclass ProofAttempt < ActiveRecord::Base
883N/A  include Numbering
883N/A
883N/A  numbering_parent_column 'sentence_id'
883N/A
883N/A  belongs_to :theorem, foreign_key: 'sentence_id'
883N/A  belongs_to :proof_status
883N/A  belongs_to :prover
883N/A  has_many :generated_axioms, dependent: :destroy
883N/A  has_and_belongs_to_many :used_axioms,
883N/A                          class_name: 'Axiom',
883N/A                          association_foreign_key: 'sentence_id',
883N/A                          join_table: 'used_axioms_proof_attempts'
883N/A  has_and_belongs_to_many :used_theorems,
883N/A                          class_name: 'Theorem',
883N/A                          association_foreign_key: 'sentence_id',
883N/A                          join_table: 'used_axioms_proof_attempts'
883N/A
883N/A  attr_accessible :prover_output,
883N/A                  :tactic_script,
883N/A                  :time_taken,
883N/A                  :number
883N/A
883N/A  validates :theorem, presence: true
883N/A
883N/A  after_save :update_theorem_status
883N/A
883N/A  scope :latest, order('number DESC')
883N/A
883N/A  def to_param
1273N/A    number
883N/A  end
883N/A
883N/A  def used_sentences
883N/A    @used_sentences ||= used_axioms + used_theorems
883N/A  end
883N/A
883N/A  def update_theorem_status
883N/A    theorem.update_proof_status(proof_status)
883N/A  end
883N/A
883N/A  def associate_prover_with_ontology_version
883N/A    ontology_version = theorem.ontology.current_version
883N/A    unless ontology_version.provers.include?(prover)
883N/A      ontology_version.provers << prover
883N/A      ontology_version.save!
883N/A    end
883N/A  end
883N/Aend
883N/A