Skip to content

Commit 01f45c4

Browse files
author
jo1996jo
committed
1차 완성
1 parent cb919a2 commit 01f45c4

File tree

4 files changed

+220
-70
lines changed

4 files changed

+220
-70
lines changed

‎cnf.cpp

+74-40
Original file line numberDiff line numberDiff line change
@@ -83,13 +83,14 @@ TreeNode::~TreeNode() {
8383

8484
void reset(shared_ptr<TreeNode>& node) {
8585
// cout << node.use_count() << " " << node->value << endl;
86+
if (!node) return;
8687
if (node->left) {
8788
reset(node->left);
8889
}
8990
if (node->right) {
9091
reset(node->right);
9192
}
92-
node.reset();
93+
if (node.use_count() > 1) node.reset();
9394
}
9495

9596
// void TreeNode::Free() {
@@ -434,7 +435,9 @@ shared_ptr<TreeNode> CnfTree::CNF(shared_ptr<TreeNode> node) {
434435
node->right = CNF(node->right);
435436
} else if (node->value == "|") {
436437
shared_ptr<TreeNode> leftVar = CNF(node->left);
438+
// compact_tree(leftVar);
437439
shared_ptr<TreeNode> rightVar = CNF(node->right);
440+
// compact_tree(rightVar);
438441
shared_ptr<TreeNode> d = distr(leftVar, rightVar);
439442
node = d;
440443
compact_tree(node);
@@ -466,34 +469,39 @@ shared_ptr<TreeNode> CnfTree::distr(shared_ptr<TreeNode> node1, shared_ptr<TreeN
466469
return returnValue;
467470
}
468471

469-
void CnfTree::compact_tree(shared_ptr<TreeNode> node) {
470-
// if (node->is_compact) return node;
472+
void CnfTree::compact_tree(shared_ptr<TreeNode>& node) {
471473
if (node == NULL) {
472474
node = NULL;
475+
return;
473476
}
474-
string a, b;
475-
if ((node->valueType == 1 || node->valueType == 2)) {
477+
if (node->valueType) {
476478
compact_tree(node->left);
477-
cout << node->left->value << endl;
479+
// cout << node->left->value << endl;
480+
// cout << node->value << endl;
478481
}
479482
if (node->valueType == 2) {
480483
compact_tree(node->right);
481-
cout << node->right->value << endl;
484+
// cout << node->right->value << endl;
485+
// cout << node->value << endl;
482486
}
483487
if (node->valueType == 2) {
484488
if (node->left == NULL && node->right == NULL) {
485489
node = NULL;
490+
return;
486491
} else if (node->left == NULL) {
487492
node = node->right;
493+
return;
488494
} else if (node->right == NULL) {
489495
node = node->left;
496+
return;
490497
}
491498
} else if (node->valueType == 1) {
492499
if (node->left == NULL) {
493500
node = NULL;
501+
return;
494502
}
495503
}
496-
if (node->left && node->left->value == "true") {
504+
if (node->valueType && node->left->value == "true") {
497505
if (node->value == "|") {
498506
reset(node->left);
499507
reset(node->right);
@@ -514,7 +522,7 @@ void CnfTree::compact_tree(shared_ptr<TreeNode> node) {
514522
node->value = "false";
515523
node->valueType = 0;
516524
}
517-
} else if (node->right && node->right->value == "true") {
525+
} else if (node->valueType == 2 && node->right->value == "true") {
518526
if (node->value == "|") {
519527
reset(node->left);
520528
reset(node->right);
@@ -524,7 +532,7 @@ void CnfTree::compact_tree(shared_ptr<TreeNode> node) {
524532
reset(node->right);
525533
node = node->left;
526534
}
527-
} else if (node->left && node->left->value == "false") {
535+
} else if (node->valueType && node->left->value == "false") {
528536
if (node->value == "&") {
529537
reset(node->left);
530538
reset(node->right);
@@ -545,7 +553,7 @@ void CnfTree::compact_tree(shared_ptr<TreeNode> node) {
545553
node->value = "true";
546554
node->valueType = 0;
547555
}
548-
} else if (node->right && node->right->value == "false") {
556+
} else if (node->valueType == 2 && node->right->value == "false") {
549557
if (node->value == "&") {
550558
reset(node->left);
551559
reset(node->right);
@@ -593,7 +601,7 @@ void CnfTree::compact_tree(shared_ptr<TreeNode> node) {
593601
break;
594602
}
595603
}
596-
if (false && !to_break) {
604+
if (!to_break) {
597605
string negationLeft = ReplaceAll(left, "- ", "-");
598606
string negationRight = ReplaceAll(right, "- ", "-");
599607
vector<string> negationLeftString = split(negationLeft);
@@ -607,9 +615,8 @@ void CnfTree::compact_tree(shared_ptr<TreeNode> node) {
607615
auto it = negationLeftString.rbegin();
608616
if (*it != "|") break;
609617
negationLeftString.pop_back();
610-
negationLeftString.insert(negationLeftString.begin(), "|");
611618
}
612-
for (int i = 0; i < (int)negationLeftString.size() - 3; i++) {
619+
for (int i = 0; i < (int)negationLeftString.size() - 1; i++) {
613620
negationLeft += "| ";
614621
}
615622
for (auto str:negationLeftString) {
@@ -623,36 +630,44 @@ void CnfTree::compact_tree(shared_ptr<TreeNode> node) {
623630
auto it = negationRightString.rbegin();
624631
if (*it != "|") break;
625632
negationRightString.pop_back();
626-
negationRightString.insert(negationRightString.begin(), "|");
627633
}
628-
for (int i = 0; i < (int)negationRightString.size() - 3; i++) {
634+
for (int i = 0; i < (int)negationRightString.size() - 1; i++) {
629635
negationRight += "| ";
630636
}
631637
for (auto str:negationRightString) {
632638
negationRight += str + " ";
633639
}
634640
negationRight = negationRight.substr(0, negationRight.length() - 1);
635641
// cout << "negationRight " << negationRight << endl;
636-
if (negationLeftString == negationRightString) {
642+
// if (negationLeftString == negationRightString) {
643+
// reset(node);
644+
// node = make_sub_tree(ReplaceAll(negationLeft, "-", "- "));
645+
// while(!exp_stack.empty()) exp_stack.pop();
646+
int count = 0;
647+
for (auto a:negationLeftString) {
648+
for (auto b:negationRightString) {
649+
if (a == b) {
650+
count++;
651+
}
652+
}
653+
}
654+
if (count == negationLeftString.size()) {
655+
reset(node);
656+
node = make_sub_tree(ReplaceAll(negationRight, "-", "- "));
657+
while(!exp_stack.empty()) exp_stack.pop();
658+
} else if (count == negationRightString.size()) {
637659
reset(node);
638660
node = make_sub_tree(ReplaceAll(negationLeft, "-", "- "));
639661
while(!exp_stack.empty()) exp_stack.pop();
640-
if (node->valueType) {
641-
// cout << "node->value " << node->value << " " << "node->left->value " << node->left->value << endl;
642-
}
643662
} else {
663+
// cout << "node->left->value" << node->left->value << endl;
644664
reset(node->left);
665+
// cout << "node->right->value" << node->right->value << endl;
645666
reset(node->right);
646667
node->left = make_sub_tree(ReplaceAll(negationLeft, "-", "- "));
647668
while(!exp_stack.empty()) exp_stack.pop();
648-
if (node->left->valueType) {
649-
// cout << "node->left->value " << node->left->value << " " << "node->left->left->value " << node->left->left->value << endl;
650-
}
651669
node->right = make_sub_tree(ReplaceAll(negationRight, "-", "- "));
652670
while(!exp_stack.empty()) exp_stack.pop();
653-
if (node->right->valueType) {
654-
// cout << "node->right->value " << node->right->value << " " << "node->right->left->value " << node->right->left->value << endl;
655-
}
656671
}
657672
}
658673
}
@@ -692,7 +707,7 @@ void CnfTree::compact_tree(shared_ptr<TreeNode> node) {
692707
break;
693708
}
694709
}
695-
if (false && !to_break) {
710+
if (!to_break) {
696711
string negationLeft = ReplaceAll(left, "- ", "-");
697712
string negationRight = ReplaceAll(right, "- ", "-");
698713
vector<string> negationLeftString = split(negationLeft);
@@ -702,7 +717,12 @@ void CnfTree::compact_tree(shared_ptr<TreeNode> node) {
702717
sort(negationLeftString.begin(), negationLeftString.end());
703718
sort(negationRightString.begin(), negationRightString.end());
704719
negationLeft = "";
705-
for (int i = 0; i < (int)negationLeftString.size() - 3; i++) {
720+
while (true) {
721+
auto it = negationLeftString.begin();
722+
if (*it != "&") break;
723+
negationLeftString.erase(negationLeftString.begin());
724+
}
725+
for (int i = 0; i < (int)negationLeftString.size() - 1; i++) {
706726
negationLeft += "& ";
707727
}
708728
for (auto str:negationLeftString) {
@@ -712,40 +732,54 @@ void CnfTree::compact_tree(shared_ptr<TreeNode> node) {
712732
// cout << "negationLeft " << negationLeft << endl;
713733

714734
negationRight = "";
715-
for (int i = 0; i < (int)negationRightString.size() - 3; i++) {
735+
while (true) {
736+
auto it = negationRightString.begin();
737+
if (*it != "&") break;
738+
negationRightString.erase(negationRightString.begin());
739+
}
740+
for (int i = 0; i < (int)negationRightString.size() - 1; i++) {
716741
negationRight += "& ";
717742
}
718743
for (auto str:negationRightString) {
719744
negationRight += str + " ";
720745
}
721746
negationRight = negationRight.substr(0, negationRight.length() - 1);
722747
// cout << "negationRight " << negationRight << endl;
723-
if (negationLeftString == negationRightString) {
748+
// if (negationLeftString == negationRightString) {
749+
// reset(node);
750+
// node = make_sub_tree(ReplaceAll(negationLeft, "-", "- "));
751+
// while(!exp_stack.empty()) exp_stack.pop();
752+
int count = 0;
753+
for (auto a:negationLeftString) {
754+
for (auto b:negationRightString) {
755+
if (a == b) {
756+
count++;
757+
}
758+
}
759+
}
760+
if (count == negationLeftString.size()) {
761+
reset(node);
762+
node = make_sub_tree(ReplaceAll(negationRight, "-", "- "));
763+
while(!exp_stack.empty()) exp_stack.pop();
764+
} else if (count == negationRightString.size()) {
724765
reset(node);
725766
node = make_sub_tree(ReplaceAll(negationLeft, "-", "- "));
726767
while(!exp_stack.empty()) exp_stack.pop();
727-
if (node->valueType) {
728-
// cout << "node->value " << node->value << " " << "node->left->value " << node->left->value << endl;
729-
}
730768
} else {
769+
// cout << "node->left->value" << node->left->value << endl;
731770
reset(node->left);
771+
// cout << "node->right->value" << node->right->value << endl;
732772
reset(node->right);
733773
node->left = make_sub_tree(ReplaceAll(negationLeft, "-", "- "));
734774
while(!exp_stack.empty()) exp_stack.pop();
735-
if (node->left->valueType) {
736-
// cout << "node->left->value " << node->left->value << " " << "node->left->left->value " << node->left->left->value << endl;
737-
}
738775
node->right = make_sub_tree(ReplaceAll(negationRight, "-", "- "));
739776
while(!exp_stack.empty()) exp_stack.pop();
740-
if (node->right->valueType) {
741-
// cout << "node->right->value " << node->right->value << " " << "node->right->left->value " << node->right->left->value << endl;
742-
}
743777
}
744778
}
745779
}
746780
}
747781
node->is_compact = true;
748-
cout << node->value << endl;
782+
// cout << node->value << endl;
749783
}
750784

751785
int main(int argc, char** argv) {

‎cnf.hpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ class CnfTree {
4949
shared_ptr<TreeNode> NNF(shared_ptr<TreeNode> node);
5050
shared_ptr<TreeNode> CNF(shared_ptr<TreeNode> node);
5151
shared_ptr<TreeNode> distr(shared_ptr<TreeNode> node1, shared_ptr<TreeNode> node2);
52-
void compact_tree(shared_ptr<TreeNode> node);
52+
void compact_tree(shared_ptr<TreeNode>& node);
5353
shared_ptr<TreeNode> root;
5454
vector<string> literals;
5555
int CNF_clauses;

0 commit comments

Comments
 (0)