axiom_selection_proof_status_spec.rb revision 1f41235c9549cfe332cc93df708e2c7199a17c65
4136N/Arequire 'spec_helper'
4136N/A
4136N/Adescribe 'Axiom Selection: Proof Status', :http_interaction do
4136N/A setup_hets
4136N/A stub_fqdn_and_port_for_pipeline_generator
4136N/A let(:generator) do
4136N/A FixturesGeneration::PipelineGenerator.new
4136N/A end
4136N/A
4136N/A let(:user) { create :user }
4136N/A let(:repository) { create :repository }
4136N/A
4136N/A let(:ontology_fixture_file) { %w(prove/Simple_Implications casl) }
4136N/A let(:ontology_filepath) { ontology_fixture_file.join('.') }
4136N/A
4136N/A before { stub_hets_for(ontology_filepath) }
4136N/A
4136N/A let(:parent_ontology_version) do
4136N/A version = version_for_file(repository,
4136N/A ontology_file(*ontology_fixture_file))
5481N/A version.parse
4136N/A version
4136N/A end
4136N/A
4136N/A let(:parent_ontology) { parent_ontology_version.ontology }
4136N/A
4136N/A let(:ontology) do
4136N/A parent_ontology.children.find_by_name('Group')
4136N/A end
4136N/A let(:theorem) { ontology.theorems.original.find_by_name('rightunit') }
4136N/A let(:axioms) { ontology.axioms }
4136N/A
4136N/A let(:prover) { create :prover }
4136N/A let(:status_disproven) { create :proof_status_disproven }
4136N/A let(:status_disproven_on_subset) { create :proof_status_csas }
4136N/A let(:status_proven) { create :proof_status_proven }
4136N/A
4136N/A context 'all axioms' do
4561N/A let(:axiom_selection) { create :manual_axiom_selection, axioms: axioms }
4561N/A let(:proof_attempt) do
4561N/A create :proof_attempt, theorem: theorem, prover: prover
4561N/A end
4561N/A let!(:proof_attempt_configuration) do
4561N/A pac = proof_attempt.proof_attempt_configuration
4561N/A pac.axiom_selection = axiom_selection.axiom_selection
4561N/A pac.prover = prover
4136N/A pac
4136N/A end
4136N/A
5481N/A before do
5481N/A generator.with_cassette(generate_cassette_name, :hets_prove_uri) do
5481N/A ProofExecution.new(proof_attempt).call
5481N/A end
5481N/A end
5481N/A
5481N/A it 'proven' do |example|
5481N/A expect(proof_attempt.reload.proof_status).to eq(status_proven)
5481N/A end
5481N/A end
5481N/A
5481N/A context 'no axioms (meaning all are used)' do
5481N/A let(:axiom_selection) { create :manual_axiom_selection, axioms: [] }
4175N/A let(:proof_attempt) do
4175N/A create :proof_attempt, theorem: theorem, prover: prover
4175N/A end
4175N/A let!(:proof_attempt_configuration) do
4175N/A pac = proof_attempt.proof_attempt_configuration
4175N/A pac.axiom_selection = axiom_selection.axiom_selection
4175N/A pac.prover = prover
4175N/A pac
4175N/A end
4175N/A
4175N/A before do
4175N/A generator.with_cassette(generate_cassette_name, :hets_prove_uri) do
4136N/A ProofExecution.new(proof_attempt).call
4136N/A end
4136N/A end
4136N/A
4136N/A it 'proven' do |example|
4136N/A expect(proof_attempt.reload.proof_status).to eq(status_proven)
4136N/A end
4136N/A end
4136N/A
4136N/A context 'not sufficient axioms' do
4136N/A let(:axiom_selection) do
4136N/A create :manual_axiom_selection, axioms: [axioms.first]
4136N/A end
4136N/A let(:proof_attempt) do
4136N/A create :proof_attempt, theorem: theorem, prover: prover
4136N/A end
4136N/A let!(:proof_attempt_configuration) do
4136N/A pac = proof_attempt.proof_attempt_configuration
4136N/A pac.axiom_selection = axiom_selection.axiom_selection
4136N/A pac.prover = prover
4136N/A pac
4136N/A end
4136N/A
4136N/A before do
4136N/A generator.with_cassette(generate_cassette_name, :hets_prove_uri) do
4136N/A ProofExecution.new(proof_attempt).call
4136N/A end
4136N/A end
4136N/A
4136N/A it 'disproven on subset' do |example|
4136N/A expect(proof_attempt.reload.proof_status).to eq(status_disproven_on_subset)
4136N/A end
4136N/A end
4136N/Aend
4136N/A