proof_attempt.rb revision 7ea1ddbe5d4686c823b01ed40fd9df5462bee5e5
1281N/Aclass ProofAttempt < ActiveRecord::Base
0N/A include Numbering
0N/A include StateUpdater
0N/A
1281N/A numbering_parent_column 'sentence_id'
0N/A
0N/A belongs_to :theorem, foreign_key: 'sentence_id'
0N/A belongs_to :proof_status
0N/A belongs_to :prover
0N/A belongs_to :proof_attempt_configuration
0N/A has_one :prover_output
0N/A has_one :tactic_script
0N/A has_many :generated_axioms, dependent: :destroy
0N/A has_and_belongs_to_many :used_axioms,
0N/A class_name: 'Axiom',
0N/A association_foreign_key: 'sentence_id',
0N/A join_table: 'used_axioms_proof_attempts'
0N/A has_and_belongs_to_many :used_theorems,
1105N/A class_name: 'Theorem',
1186N/A association_foreign_key: 'sentence_id',
0N/A join_table: 'used_axioms_proof_attempts'
1186N/A
1186N/A attr_accessible :locid
1186N/A attr_accessible :time_taken,
1186N/A :number,
1140N/A :state,
1186N/A :state_updated_at,
1186N/A :last_error
1186N/A
1281N/A validates :state, inclusion: {in: State::STATES}
1281N/A validates :theorem, presence: true
1186N/A
1281N/A before_create :generate_locid
1281N/A before_save :set_default_proof_status
1281N/A after_save :update_theorem_status
1281N/A
1281N/A scope :latest, order('number DESC')
1281N/A
1281N/A delegate :ontology, to: :theorem
1281N/A
1281N/A def self.find_with_locid(locid, _iri = nil)
1281N/A where(locid: locid).first
1186N/A end
1281N/A
1186N/A def used_sentences
1186N/A @used_sentences ||= used_axioms + used_theorems
1364N/A end
0N/A
1281N/A def set_default_proof_status
1281N/A self.proof_status ||= ProofStatus.find(ProofStatus::DEFAULT_OPEN_STATUS)
1186N/A end
1281N/A
1186N/A def generate_locid
1186N/A self.locid =
1186N/A "#{theorem.locid}//#{self.class.to_s.underscore.dasherize}-#{number}"
1281N/A end
1281N/A
1281N/A def update_theorem_status
1186N/A theorem.update_proof_status(proof_status)
1186N/A end
1186N/A
1281N/A def associate_prover_with_ontology_version
1281N/A ontology_version = theorem.ontology.current_version
1281N/A unless ontology_version.provers.include?(prover)
1281N/A ontology_version.provers << prover
1281N/A ontology_version.save!
0N/A end
1281N/A end
1281N/A
1281N/A def retry_failed
1281N/A ProofExecutionWorker.perform_async(id)
1281N/A end
1281N/A
1281N/A def proper_subset_of_axioms_selected?
1281N/A selected = proof_attempt_configuration.axiom_selection.axioms
1281N/A available = theorem.ontology.axioms
1281N/A selected.any? && selected.count < available.count
1281N/A end
1186N/A
1186N/A protected
1186N/A
1186N/A def prove_options_from_configuration
1186N/A pac = proof_attempt_configuration
1186N/A Hets::ProveOptions.new({prover: pac.prover,
1186N/A timeout: pac.timeout})
end
end