Skip to content

Commit

Permalink
Support forwarding get_assertion() to the temporary generator.
Browse files Browse the repository at this point in the history
  • Loading branch information
giomasce committed Apr 9, 2018
1 parent 527b8ab commit 3a7644a
Show file tree
Hide file tree
Showing 6 changed files with 27 additions and 2 deletions.
9 changes: 9 additions & 0 deletions mm/library.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,15 @@ const Assertion &LibraryImpl::get_assertion(LabTok label) const
return this->assertions.at(label.val());
}

const Assertion *LibraryImpl::get_assertion_ptr(LabTok label) const
{
if (label.val() < this->assertions.size()) {
return &this->assertions[label.val()];
} else {
return nullptr;
}
}

const std::vector<Sentence> &LibraryImpl::get_sentences() const
{
return this->sentences;
Expand Down
2 changes: 2 additions & 0 deletions mm/library.h
Original file line number Diff line number Diff line change
Expand Up @@ -297,6 +297,7 @@ class Library {
class ExtendedLibrary : public Library {
public:
virtual const Sentence *get_sentence_ptr(LabTok label) const = 0;
virtual const Assertion *get_assertion_ptr(LabTok label) const = 0;
virtual const std::unordered_map< SymTok, std::string > &get_symbols() const = 0;
virtual const std::unordered_map<LabTok, std::string> &get_labels() const = 0;
virtual const std::vector< Sentence > &get_sentences() const = 0;
Expand All @@ -322,6 +323,7 @@ class LibraryImpl final : public ExtendedLibrary
const Sentence *get_sentence_ptr(LabTok label) const override;
SentenceType get_sentence_type(LabTok label) const override;
const Assertion &get_assertion(LabTok label) const override;
const Assertion *get_assertion_ptr(LabTok label) const override;
const std::vector< Sentence > &get_sentences() const override;
const std::vector< SentenceType > &get_sentence_types() const override;
const std::vector< Assertion > &get_assertions() const override;
Expand Down
8 changes: 8 additions & 0 deletions mm/tempgen.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ void TempGenerator::create_temp_var(SymTok type_sym)
SymTok sym = this->temp_syms.create(sym_name);
LabTok lab = this->temp_labs.create(lab_name);
this->temp_types[lab] = { type_sym, sym };
this->temp_asses[lab] = {};

// Add the variables to a few structures
//this->derivations.at(type_sym).push_back(pair< LabTok, vector< SymTok > >(lab, { sym }));
Expand Down Expand Up @@ -142,6 +143,13 @@ const Sentence &TempGenerator::get_sentence(LabTok label)
return this->temp_types.at(label);
}

const Assertion &TempGenerator::get_assertion(LabTok label)
{
std::unique_lock< std::mutex > lock(this->global_mutex);

return this->temp_asses.at(label);
}

LabTok TempGenerator::get_var_sym_to_lab(SymTok sym)
{
std::unique_lock< std::mutex > lock(this->global_mutex);
Expand Down
2 changes: 2 additions & 0 deletions mm/tempgen.h
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ class TempGenerator {
size_t get_symbols_num();
size_t get_labels_num();
const Sentence &get_sentence(LabTok label);
const Assertion &get_assertion(LabTok label);

// LibraryToolbox-like interface
LabTok get_var_sym_to_lab(SymTok sym);
Expand All @@ -42,6 +43,7 @@ class TempGenerator {
const Library &lib;
std::map< SymTok, size_t > temp_idx;
std::unordered_map< LabTok, Sentence > temp_types;
std::unordered_map< LabTok, Assertion > temp_asses;
StringCache< SymTok > temp_syms;
StringCache< LabTok > temp_labs;
std::size_t syms_base;
Expand Down
6 changes: 5 additions & 1 deletion mm/toolbox.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -452,7 +452,11 @@ SentenceType LibraryToolbox::get_sentence_type(LabTok label) const

const Assertion &LibraryToolbox::get_assertion(LabTok label) const
{
return this->lib.get_assertion(label);
const Assertion *ass = this->lib.get_assertion_ptr(label);
if (ass != nullptr) {
return *ass;
}
return this->temp_generator->get_assertion(label);
}

/*std::function<const Assertion *()> LibraryToolbox::list_assertions() const
Expand Down
2 changes: 1 addition & 1 deletion mm/toolbox.h
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,7 @@ class LibraryToolbox : public Library
void type_proving_helper_unwind_tree(const ParsingTree< SymTok, LabTok > &tree, Engine &engine, const std::unordered_map<LabTok, const Prover< Engine >* > &var_provers) const {
// We need to sort children according to their order as floating hypotheses of this assertion
// If this is not an assertion, then there are no children
const Assertion &ass = this->lib.get_assertion(tree.label);
const Assertion &ass = this->get_assertion(tree.label);
auto it = var_provers.find(tree.label);
if (ass.is_valid()) {
assert(it == var_provers.end());
Expand Down

0 comments on commit 3a7644a

Please sign in to comment.