SHARE
TWEET

Untitled

a guest Apr 19th, 2019 135 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. #include <iostream>
  2. #include <string>
  3. #include <algorithm>
  4. #include <set>
  5. #include <map>
  6. #include <unordered_set>
  7. #include <unordered_map>
  8. #include <vector>
  9. #include <queue>
  10. #include <sstream>
  11.  
  12. class god {
  13. private :
  14.  
  15.     class operation {
  16.     public:
  17.         std::string operator_sign;
  18.  
  19.         virtual std::string print() = 0;
  20.  
  21.         virtual size_t hash() const = 0;
  22.  
  23.         virtual bool operator==(  operation *oper) const = 0;
  24.  
  25.         virtual bool operator!=(  operation *oper) const {
  26.             return !(this->operator==(oper));
  27.         }
  28.  
  29.  
  30.     };
  31.  
  32.     class abstract_operaiton : public operation {
  33.     public :
  34.         operation *left;
  35.         operation *right;
  36.  
  37.  
  38.         abstract_operaiton(operation *left, operation *right) : left(left), right(right) {};
  39.  
  40.         std::string print() override {
  41.             return "(" + left->print() + " " + operator_sign + " " + right->print() + ")";
  42.         }
  43.  
  44.         size_t hash() const override {
  45.             return left->hash() * 31 + right->hash() * 17 + (std::hash<std::string>{}(operator_sign));
  46.         }
  47.  
  48.         bool operator==(operation *oper) const override {
  49.             if (dynamic_cast<abstract_operaiton *> (oper) != nullptr) {
  50.                 auto *box = dynamic_cast<abstract_operaiton *> (oper);
  51.                 return operator_sign == box->operator_sign && left->operator==(box->left) &&
  52.                        right->operator==(box->right);
  53.             }
  54.             return false;
  55.         }
  56.  
  57.  
  58.     };
  59.  
  60.     using AO = abstract_operaiton;
  61.     using first = operation;
  62.  
  63.     class AND : public AO {
  64.     public :
  65.         AND(first *left, first *right) : abstract_operaiton(left, right) {
  66.             this->operator_sign = "&";
  67.         };
  68.     };
  69.  
  70.     class OR : public AO {
  71.     public :
  72.         OR(first *left, first *right) : AO(left, right) {
  73.             this->operator_sign = "|";
  74.         };
  75.     };
  76.  
  77.     class SO : public AO {
  78.     public :
  79.         SO(first *left, first *right) : AO(left, right) {
  80.             this->operator_sign = "->";
  81.         };
  82.     };
  83.  
  84.     class DEC : public operation {
  85.     public :
  86.         first *mid;
  87.  
  88.         explicit DEC(first *mid) : mid(mid) { this->operator_sign = "!"; };
  89.  
  90.         std::string print() override {
  91.             return "!" + mid->print();
  92.         }
  93.  
  94.         size_t hash() const override {
  95.             return mid->hash() * 71 ;
  96.         }
  97.  
  98.         bool operator==( operation *oper) const override {
  99.             if (dynamic_cast<DEC * > (oper) != nullptr) {
  100.                 auto *box = dynamic_cast<DEC *> (oper);
  101.                 return mid->operator==(box->mid);
  102.             }
  103.             return false;
  104.         }
  105.  
  106.  
  107.     };
  108.  
  109.  
  110.     class VAR : public operation {
  111.     public :
  112.         std::string var;
  113.  
  114.         explicit VAR(std::string &var) : var(var) { this->operator_sign = "var"; };
  115.  
  116.         std::string print() override {
  117.             return var;
  118.         }
  119.  
  120.         size_t hash() const override {
  121.             return (std::hash<std::string>{}(var));
  122.         }
  123.  
  124.         bool operator==(operation *oper) const override {
  125.             if (dynamic_cast<VAR *> (oper) != nullptr) {
  126.                 auto *box = dynamic_cast<VAR *> (oper);
  127.                 return var == box->var;
  128.             }
  129.             return false;
  130.         }
  131.  
  132.     };
  133.  
  134.     using PAIR = std::pair<operation *, int>;
  135.  
  136.     class parser {
  137.     public :
  138.  
  139.         int current = 0;
  140.         std::string str = "";
  141.  
  142.         parser() = default;
  143.  
  144.         std::string delete_spaces(std::string &exp) {
  145.             std::string answer;
  146.             for (auto &i : exp) if (i != ' ') answer.push_back(i);
  147.             return answer;
  148.         }
  149.  
  150.         operation *parse(std::string &exp) {
  151.             str = delete_spaces(exp);
  152.             current = 0;
  153.             return parseSO();
  154.         }
  155.  
  156.  
  157.         operation *parseSO() {
  158.             operation *answer = parseOR();
  159.             while (current < str.size() && str[current] == '-') {
  160.                 current += 2;
  161.                 operation *answer2 = parseSO();
  162.                 answer = new SO(answer, answer2);
  163.             }
  164.             return answer;
  165.         }
  166.  
  167.         operation *parseOR() {
  168.             operation *answer = parseAND();
  169.             while (current < str.size() && str[current] == '|') {
  170.                 ++current;
  171.                 operation *answer2 = parseAND();
  172.                 answer = new OR(answer, answer2);
  173.             }
  174.             return answer;
  175.         }
  176.  
  177.         operation *parseAND() {
  178.             operation *answer = parseB();
  179.             for (;;) {
  180.                 if (current == str.size() || str[current] != '&') return answer;
  181.                 current++;
  182.                 operation *answer2 = parseB();
  183.                 answer = new AND(answer, answer2);
  184.             }
  185.         }
  186.  
  187.         operation *parseB() {
  188.             if (str[current] == '!') {
  189.                 current++;
  190.                 operation *answer = parseB();
  191.                 return new DEC(answer);
  192.             } else {
  193.                 if (str[current] == '(') {
  194.                     ++current;
  195.                     operation *answer = parseSO();
  196.                     if (str[current] == ')') {
  197.                         current++;
  198.                     }
  199.                     return answer;
  200.                 }
  201.             }
  202.             return parseVar();
  203.         }
  204.  
  205.         operation *parseVar() {
  206.             std::string var;
  207.             while (current < str.size() && !is_operation(str[current])) {
  208.                 var.push_back(str[current]);
  209.                 current++;
  210.             }
  211.             operation *operation1 = new VAR(var);
  212.             return operation1;
  213.         }
  214.  
  215.         bool is_operation(char t) {
  216.             return t == '-' || t == '&' || t == '!' || t == '|' || t == '(' || t == ')';
  217.         }
  218.  
  219.     };
  220.  
  221.     struct operation_hash {
  222.         std::size_t operator()(const operation *k) const {
  223.             return k->hash();
  224.         }
  225.     };
  226.  
  227.     struct operation_equality {
  228.         bool operator()(operation *k, operation *s) const {
  229.             return k->operator==(s);
  230.         }
  231.     };
  232.  
  233.  
  234.     class axiom {
  235.     private:
  236.         operation *kernel;
  237.         std::unordered_map<std::string, operation *> flow_variable_map;
  238.     public:
  239.         axiom() = default;
  240.  
  241.         axiom(operation *ker) : kernel(ker) {};
  242.  
  243.         bool is_scheme(operation *kern, operation *expr) {
  244.             if (dynamic_cast<abstract_operaiton *>(expr) != nullptr) {
  245.                 if (kern->operator_sign == expr->operator_sign) {
  246.                     auto *box1 = dynamic_cast<abstract_operaiton *> (kern);
  247.                     auto *box2 = dynamic_cast<abstract_operaiton *> (expr);
  248.                     return is_scheme(box1->left, box2->left) && is_scheme(box1->right, box2->right);
  249.                 } else return false;
  250.             }
  251.             if (dynamic_cast<DEC *>(expr) != nullptr) {
  252.                 if (kern->operator_sign == expr->operator_sign) {
  253.                     auto *box1 = dynamic_cast<DEC *> (kern);
  254.                     auto *box2 = dynamic_cast<DEC *> (expr);
  255.                     return is_scheme(box1->mid, box2->mid);
  256.                 } else return false;
  257.             }
  258.             if (dynamic_cast<VAR *>(expr) != nullptr) {
  259.                 std::string tree_string = expr->print();
  260.                 if (flow_variable_map.count(tree_string) == 0) {
  261.                     flow_variable_map[tree_string] = kern;
  262.                 } else return flow_variable_map[tree_string]->operator==(kern);
  263.             }
  264.             return true;
  265.         }
  266.  
  267.         bool is_scheme(operation *expr) {
  268.             flow_variable_map.clear();
  269.             return is_scheme(expr, kernel);
  270.         }
  271.     };
  272.  
  273.     struct META {
  274.         int way = -1;
  275.         int id = -1;
  276.     };
  277.  
  278.     struct MP {
  279.         std::unordered_set<operation *, operation_hash, operation_equality> possible_M = {};
  280.     };
  281.  
  282.     struct MP_total {
  283.         operation *L = nullptr;
  284.     };
  285.  
  286.  
  287.     class proof {
  288.     private :
  289.  
  290.         std::string A;
  291.  
  292.         operation *A_op;
  293.  
  294.         std::string first_shit;
  295.  
  296.         std::vector<axiom> axioms;
  297.  
  298.         std::unordered_map<operation *, int, operation_hash, operation_equality> hypothesis;
  299.  
  300.         std::unordered_map<operation *, META, operation_hash, operation_equality> printed;
  301.  
  302.         std::vector<operation *> proofment;
  303.  
  304.         std::unordered_map<operation *, MP, operation_hash, operation_equality> MP_check;
  305.  
  306.         std::unordered_map<operation *, MP_total, operation_hash, operation_equality> MP_correct;
  307.  
  308.         std::unordered_map<operation *, int, operation_hash, operation_equality> index;
  309.  
  310.         std::unordered_map<operation *, int, operation_hash, operation_equality> old_index;
  311.  
  312.         std::unordered_map<operation *, bool, operation_hash, operation_equality> used;
  313.  
  314.  
  315.         std::vector<std::pair<int, operation *>> min;
  316.  
  317.         parser parser1;
  318.  
  319.     public :
  320.         explicit proof() {
  321.             std::vector<std::string> axiomss(10);
  322.             axioms.resize(10);
  323.             axiomss[0] = "A->(B->A)";
  324.             axiomss[1] = "(A->B)->((A->B->C)->(A->C))";
  325.             axiomss[2] = "(A->(B->(A&B)))";
  326.             axiomss[3] = "A&B->A";
  327.             axiomss[4] = "A&B->B";
  328.             axiomss[5] = "A ->A|B";
  329.             axiomss[6] = "B->A|B";
  330.             axiomss[7] = "(A->C)->((B->C)->((A|B)->C)";
  331.             axiomss[8] = "(A->B)->((A->!B)->!A)";
  332.             axiomss[9] = "!!A->A";
  333.             for (int i = 0; i < 10; ++i) axioms[i] = {parser1.parse(axiomss[i])};
  334.             take_context();
  335.             if (!get_proof() || check_priveledge()) {
  336.                 std::cout << "Proof is incorrect";
  337.                 return;
  338.             }
  339.             minimize();
  340.             print_answer();
  341.         }
  342.  
  343.         bool check_priveledge() {
  344.             if (proofment.empty()) return true;
  345.             return proofment.back()->operator!=(A_op);
  346.         }
  347.  
  348.  
  349.         void take_context() {
  350.             std::getline(std::cin, first_shit);
  351.             int stop_position = find_hamma_symbol();
  352.             fill_hypothesis(stop_position);
  353.             get_A(stop_position);
  354.  
  355.         }
  356.  
  357.         int find_hamma_symbol() {
  358.             for (int i = 1; i < first_shit.size(); ++i)
  359.                 if (first_shit[i] == '-' && first_shit[i - 1] == '|') return i - 1;
  360.             return 0;
  361.         }
  362.  
  363.         void fill_hypothesis(int stp_pstn) {
  364.             std::string str;
  365.             int count = 1;
  366.             for (int i = 0; i < stp_pstn; ++i) {
  367.                 if (first_shit[i] == ',') {
  368.                     hypothesis[parser1.parse(str)] = count;
  369.                     ++count;
  370.                     str.clear();
  371.                 } else str.push_back(first_shit[i]);
  372.             }
  373.             if (!str.empty()) hypothesis[parser1.parse(str)] = count;
  374.         }
  375.  
  376.         void get_A(int stp_pstn) {
  377.             for (int i = stp_pstn + 2; i < first_shit.size(); ++i) A.push_back(first_shit[i]);
  378.             A_op = parser1.parse(A);
  379.         }
  380.  
  381.         bool is_printed(operation *oper) {
  382.             return printed.find(oper) != printed.end();
  383.         }
  384.  
  385.         bool get_proof() {
  386.             std::string box;
  387.             while (std::getline(std::cin, box)) {
  388.                 if (box.empty()) return true;
  389.                 operation *oper = parser1.parse(box);
  390.                 if (!is_printed(oper)) {
  391.                     if (is_hypothesis(oper) || is_scheme(oper) || is_modus_ponens(oper)) {
  392.                         proofment.push_back(oper);
  393.                         used[oper] = false;
  394.                         it_can_be_modens_ponens(oper);
  395.                     } else {
  396.                         return false;
  397.                     }
  398.                 }
  399.                 if (oper->operator==(A_op)) return true ;
  400.             }
  401.             return true;
  402.         }
  403.  
  404.         bool is_hypothesis(operation *oper) {
  405.             if (hypothesis.find(oper) != hypothesis.end()) {
  406.                 printed[oper] = {0, hypothesis[oper]};
  407.                 return true;
  408.             }
  409.             return false;
  410.         }
  411.  
  412.         bool is_scheme(operation *oper) {
  413.             for (int i = 0; i < 10; ++i) {
  414.                 if (axioms[i].is_scheme(oper)) {
  415.                     printed[oper] = {1, i + 1};
  416.                     return true;
  417.                 }
  418.             }
  419.             return false;
  420.         }
  421.  
  422.         bool is_modus_ponens(operation *oper) {
  423.             if (MP_correct.find(oper) != MP_correct.end()) return true;
  424.             if (!MP_check[oper].possible_M.empty()) {
  425.                 for (auto j : MP_check[oper].possible_M) {
  426.                     if (printed.find(dynamic_cast<abstract_operaiton *>(j)->left) != printed.end()) {
  427.                         printed[oper] = {2, 0};
  428.                         MP_correct[oper].L = j;
  429.                         return true;
  430.                     }
  431.                 }
  432.             }
  433.             return false;
  434.         }
  435.  
  436.         bool it_can_be_modens_ponens(operation *oper) {
  437.             if (oper->operator_sign == "->") {
  438.                 auto *box = dynamic_cast<abstract_operaiton * > (oper);
  439.                 MP_check[box->right].possible_M.insert(box);
  440.                 return true;
  441.             }
  442.             return false;
  443.         }
  444.  
  445.         static bool comp(const std::pair<int, operation *> &first, const std::pair<int, operation *> &second) {
  446.             return first.first >= second.first;
  447.         }
  448.  
  449.         void minimize() {
  450.             for (int i = 0; i < proofment.size(); ++i) old_index[proofment[i]] = i;
  451.             minimize(A_op);
  452.             std::sort(min.begin(), min.end(), comp);
  453.             for (int i = 0; i < min.size(); ++i) index[min[i].second] = i;
  454.         }
  455.  
  456.         void minimize(operation *oper) {
  457.             if (used[oper]) return;
  458.             used[oper] = true;
  459.             min.emplace_back(old_index[oper], oper);
  460.             if (printed[oper].way == 0 || printed[oper].way == 1) return;
  461.             if (printed[oper].way == 2) {
  462.                 minimize(MP_correct[oper].L);
  463.                 minimize(dynamic_cast<abstract_operaiton *>(MP_correct[oper].L)->left);
  464.             }
  465.         }
  466.  
  467.         void print_answer() {
  468.             std::cout << first_shit << std::endl;
  469.             for (int i = static_cast<int>(min.size() - 1); i >= 0; --i) {
  470.                 operation *cur = min[i].second;
  471.                 if (printed[cur].way == 0) {
  472.                     std::cout << "[" << min.size() - i << ". Hypothesis " << printed[cur].id << "]" << " "
  473.                               << cur->print() << std::endl;
  474.                 }
  475.                 if (printed[cur].way == 1) {
  476.                     std::cout << "[" << min.size() - i << ". Ax. sch. " << printed[cur].id << "]" << " " << cur->print()
  477.                               << std::endl;
  478.                 }
  479.                 if (printed[cur].way == 2) {
  480.                     std::cout << "[" << min.size() - i << ". M.P. " << min.size() - index[MP_correct[cur].L] << ", "
  481.                               << min.size() - index[dynamic_cast<abstract_operaiton *>(MP_correct[cur].L)->left] << "] "
  482.                               << cur->print() << std::endl;
  483.                 }
  484.             }
  485.         }
  486.  
  487.     };
  488.  
  489.     proof proof1;
  490. public :
  491.  
  492.  
  493. };
  494.  
  495.  
  496. int main() {
  497.     god god1;
  498.     return 0;
  499. }
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top