prove_evaluator.rb revision 2fd88efc10e9ebf955b6fa407d0216faf4a51dfb
effcbdb12c7ef892f1fd92a745cb33a08ca4ba30Stephen Gallagher register :set_object_value, :start, to: :set_object_value
effcbdb12c7ef892f1fd92a745cb33a08ca4ba30Stephen Gallagher register :add_array_value, :start, to: :add_array_value
effcbdb12c7ef892f1fd92a745cb33a08ca4ba30Stephen Gallagher register :tactic_script, :start, to: :tactic_script_start
effcbdb12c7ef892f1fd92a745cb33a08ca4ba30Stephen Gallagher register :tactic_script, :end, to: :tactic_script_end
effcbdb12c7ef892f1fd92a745cb33a08ca4ba30Stephen Gallagher register :tactic_script_extra_options, :start,
effcbdb12c7ef892f1fd92a745cb33a08ca4ba30Stephen Gallagher register :tactic_script_extra_options, :end,
74e95cfd9d3939dfe9417d79d2f6fc79b361405fJakub Hrozek register :used_time, :start, to: :used_time_start
effcbdb12c7ef892f1fd92a745cb33a08ca4ba30Stephen Gallagher register :used_time, :end, to: :used_time_end
55d80b1301fe969fb4ba2b9481027887b9462dbbJakub Hrozek register :used_time_components, :start, to: :used_time_components_start
55d80b1301fe969fb4ba2b9481027887b9462dbbJakub Hrozek register :used_time_components, :end, to: :used_time_components_end
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek register :used_axioms, :start, to: :used_axioms_start
44ba573582072823d8760d0f18e5b3195cecc182Jakub Hrozek register :used_axioms, :end, to: :used_axioms_end
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek proof_attempt.theorem = find_theorem_with_hash(proof_info, ontology)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek proof_attempt.proof_status = find_proof_status_with_hash(proof_info)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek proof_attempt.prover = proof_info[:used_prover]
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek proof_attempt.prover_output = proof_info[:prover_output]
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek proof_attempt.time_taken = proof_info[:time_taken]
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek proof_attempt.tactic_script = tactic_script_from_hash(proof_info)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek used_axioms_from_hash(proof_info, proof_attempt)
90afedb00608547ae1f32aa7aafd552c4b306909Jakub Hrozek proof_attempt.generated_axioms = generated_axioms
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def find_theorem_with_hash(proof_info, ontology)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek ontology.theorems.find_by_name(proof_info[:theorem_name])
35d420c5d4609b6e999920e38a9b2ec40a0e1ac4Jakub Hrozek time_limit: proof_info[:tactic_script_time_limit],
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek extra_options: proof_info[:tactic_script_extra_options],
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def used_axioms_from_hash(proof_info, proof_attempt)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek if proof_info[:used_axioms] && proof_attempt.theorem
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek [[], [], []]
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def process_used_axioms(proof_info, proof_attempt)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek axiom = find_sentence_or_generate_axiom(axiom_name, proof_attempt)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek used_theorems << axiom if axiom.is_a?(Theorem)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek generated_axioms << axiom if axiom.is_a?(GeneratedAxiom)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek [used_axioms, used_theorems, generated_axioms]
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek # Logic translations applied before proving can introduce new axioms that
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek # are not stored as sentences in our database. They need to be
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek # distinguished from sentences.
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def find_sentence_or_generate_axiom(axiom_name, proof_attempt)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek sentence = Sentence.
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek where(ontology_id: proof_attempt.theorem.ontology.id,
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek name: axiom_name).first
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek sentence || generate_axiom(axiom_name, proof_attempt)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def generate_axiom(axiom_name, proof_attempt)
933314e53fac878d1a9b126af216454172cb945aJakub Hrozek generated_axiom = GeneratedAxiom.new
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek generated_axiom.name = axiom_name
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek generated_axiom.proof_attempt = proof_attempt
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek generated_axiom.save
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek generated_axiom
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def all_start
90afedb00608547ae1f32aa7aafd552c4b306909Jakub Hrozek self.hierarchy = []
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def set_object_value(value, key)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek info = proof_attempt_info(key, value)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek object_hash[info.keys.first] = info.values.first if info
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov def add_array_value(value)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek info = proof_attempt_info
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek object_hash[info.keys.first] ||= []
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek object_hash[info.keys.first] << value
933314e53fac878d1a9b126af216454172cb945aJakub Hrozek def node_start
933314e53fac878d1a9b126af216454172cb945aJakub Hrozek hierarchy << :node
933314e53fac878d1a9b126af216454172cb945aJakub Hrozek self.object_hash = {}
933314e53fac878d1a9b126af216454172cb945aJakub Hrozek def node_end
933314e53fac878d1a9b126af216454172cb945aJakub Hrozek hierarchy.pop
933314e53fac878d1a9b126af216454172cb945aJakub Hrozek def goal_start
933314e53fac878d1a9b126af216454172cb945aJakub Hrozek hierarchy << :goal
933314e53fac878d1a9b126af216454172cb945aJakub Hrozek ontology_name = object_hash[:ontology_name]
933314e53fac878d1a9b126af216454172cb945aJakub Hrozek self.object_hash = {ontology_name: ontology_name}
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek hierarchy.pop
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek create_proof_attempt_from_hash(object_hash)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek %i(tactic_script
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek tactic_script_extra_options
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek used_time_components
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek used_axioms).each do |hook|
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek define_method("#{hook}_start") do
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek hierarchy << hook
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek define_method("#{hook}_end") do
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek hierarchy.pop
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def proof_attempt_info(key = nil, value = nil)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek case hierarchy.last
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek {ontology_name: value} if key == 'node'
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek goal_info(key, value)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek when :tactic_script
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek {:"tactic_script_#{key.underscore}" => value}
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek when :tactic_script_extra_options
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek {:tactic_script_extra_options => nil}
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek when :used_time
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek {:time_taken => value} if key == 'seconds'
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek when :used_time_components
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek # don't use them
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek when :used_axioms
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek {:used_axioms => nil}
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek {key.underscore.to_sym => value}
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def goal_info(key, value)
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek if key == 'name'
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek {:theorem_name => value}
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek {key.underscore.to_sym => value}
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def initiate_concurrency_handling
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek # overwrite this method - concurrency is not an issue here
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def finish_concurrency_handling
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek # overwrite this method - concurrency is not an issue here
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek def cancel_concurrency_handling_on_error
ebc6ab564dc2a0a2b08c42d727fc403dde4a2dc9Jakub Hrozek # overwrite this method - concurrency is not an issue here