From d00e64db0c05b42bf23a399b0f16ed987dc27c87 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Wed, 24 Feb 2016 19:39:20 +0000 Subject: [PATCH 01/30] README edited online with Bitbucket --- README | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/README b/README index 01394e1..c23782c 100644 --- a/README +++ b/README @@ -8,3 +8,12 @@ proceed normally. To compile this version of DSHARP simply run make +Please cite using the following: + +@inproceedings{Muise2012, + author = {Muise, Christian and McIlraith, Sheila A. and Beck, J. Christopher and Hsu, Eric}, + booktitle = {Canadian Conference on Artificial Intelligence}, + title = {{DSHARP: Fast d-DNNF Compilation with sharpSAT}}, + keywords = {sat, knowledge compilation}, + year = {2012} +} \ No newline at end of file From 65ab26cbd60e277e71fa68ebf4482e7f677d2d59 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Sat, 4 Apr 2020 11:30:07 -0400 Subject: [PATCH 02/30] Adding logo. --- logo.png | Bin 0 -> 6476 bytes 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 logo.png diff --git a/logo.png b/logo.png new file mode 100644 index 0000000000000000000000000000000000000000..bdce51035a3101f3b84a11832e23e3defe128cae GIT binary patch literal 6476 zcmdsb`#+QaANQPQ7=~g)naN=!8*(Ue%&Ews6CKQi|N{$nW zoO70#QcgMLnA7fSbpHq6$Nj^-$78#$Yu9zXUeEXI_)c zBr?AcF!0-O%ApkmLI{}}>YeweI&L!j3WzhkHK&hb>$?7hHwBEz?G;uNJ{+w zr_<~!tQ!o5PQ%ou&3BM?1JgplnzJ4$n$XAUf}xDv9WisLD;=;2luRZ=+uGWgN8eJB zy$6A}an8=pdlKH=8iS8k-)mU>yX;c2AxCtE^6~M3xwyE%o}QjyJRV;;$g}s-?_ND# z5C%e{fv+wabAJ{H0jtKvy{8}Ntyx(CRh{wsk8=K?Ja?TANQFcZ5UAKf5ILEkvI(pk zTkA><%afgmW7jL1y_UY81`7*U4(O7Ew>MWG=~-Nl(YtmnP4D8xEcnbUHorio66jF*-UrBt9g5{D-m0Mi&zrQ%QijSJ_geMAyl{|N94m zJTmp{t&0P`M+=5Pz~QdW95rGe_wQEsmGBZVP>$|~kaHC7?B6=qy$*4U!&w_yFKJH) zaU!`)C#dM$IBQ4pQe}XT&?Wl3A$$47w%<0;AdQ{h?psX-v4^!o%#8?-?@{7cW<@3T zKvef&`A8U;VYfuTjETloT6paDP~VA;Jk+F@-U&XO1J4taviL{tIx6j7>saHAFilT+$IujE$I~n>b25t7Wv} zgz`S0ho$5N92!~h+*I^KgZkutx1&%Rlb6$Z9K)&0Xi)h@%Qzj%Tn$TRIlky*kLq}h zvEfwJZpx0!74&Izc%mTIhzuXjyCH7;>rjJ1FG%vd*&dkjYP zWh`F<5~d<9fs;3r2>BxUv#6c_iM_Au5wMY(uuN}pNpU8h)%hDYt0r>9I{#D5cu>LN z)ils_1{QT{Yu5ed*N3@O6{=5hKdLF}XL)9M#FAR}Nk2@JE`b*<9p&oB;H^qzUC{nD zNrtgno8^}~R-Uuu58wUbRKaH{%OTm=;khfVIvHrrNi_cySg8}lTV)Dej;^YB-b=&gG1r*-Lm025jwA1M|AtbyRo+X@;5quj%4vq_3$5W zWGBf5sMGo7g8H~?m#99Mc4fQpfd3N(zd9KhPSuni<>}Bg3|rPhTU%bxhxji9E3d!y zTLD6u!RSrR0_*|e;O{3&yVmCK;MhIQy=Em|4XWv7!j7ogcvv65_Fz8x%&7L;#zgBV zte`$}lAI`5xLWvPebf|fMY!S5OYVs(Ut1U~Jf7Scx}LsTg$mO}-&yK8vh`M_&Lt)Y zN3PdguXwt}wx^F$!c9X$4V5++5;FSI8W&t;o|6$$uFvnjvB~P%itt;A*!p(ptl`wC z)%wHg8~HQ0jeb$p4-`CvOBu4y@8;X0KET-ukLM&JBavan?rR+3ln{!QSqSC9>&17P zd-m+LmE@ygVA&~KjGq3h{UTTUqJ`4*FM7DWaqjs@B(aNsh2m;VOh2@B)zpoaUMV_? zYCfBaP+sndJTg2)pRc=-Y@JyEAJEm7M}2RpzsSbGAfuty6lXu$?J3DvU)76p~GR96HYMRe0h*MSOqItX#Y%QvO z@GWK4H#QcMEJBHX760pu#vUe7WiHU6;$mHJ@UD=iOlxCfBkl8t&$Py~v{o{#G}@!P zVOaF&(W8d4P4(=+3rw9US%OTR0&e$Hq!U_q89FJw79L4rqV+bkTY_WiG&tLl@$vlG z9kYuE^DLZY+J1K{ppel~gEN2TBMMNRVG^~R%aV%wvQn{pL?n#;d1&ZW7D@0aP%|Ur z6UP}6c6de$SD+}f^^}E%xZ7`cvoJ@o@X~KyAB*z`1+vN`)`PsSVVf+?B!QrcM@QzZ%+AcbJn%w>(<8ad6F%PF*!=tgjH~NS%;F-w zGZ$DJRK7qS`o!)DbbEU{jzuA-MLsd)RWJj7`SN9W&W#)dnfw@T7jlI& zQnL8iBtZreIIl>K==UwlQLPC-29^Rjxj9%9D7;n9XWjOD^6Cc>Q{l3iD1a}Ckqnv=t#O>mHF;n1y< zm#P;>gYSIbek97jr?~n_4KE1;=ZH0VeHH1KSEhgHCX9C|n6zI>-KjJsHd@GeDPJ)7q+O`1yzK&96j^LZTYs z(_86pj+(w(xwajWEoY+Hop!Ro=3`(QW!ta=K~QXh&s5@Vg{eNVvE!fIGf0*_s&csy zNlc8?Y-M(Np2wB4{^ABN#O|LUV|4g>y2n>o{6M&7=*fQ;!tw#Nfvu*8!FU{v6*36T zhJ~@)y!`Uwrt~%_VEx-&h175>GZq2K$?Yq{8fd$PLw)jXP$!@j=^BdUUZE0G-m7r< zMHU=0wjwY2touY#1Y$q}dW5arFfOL=vjfEFof$fdns*2D#ic>X{x~j{{@4DDUF|?2 zZs}D8_uE|e3f6j_pMy%A3e3D|#rsucak5jQ;8h$-7(mDj&f+26n;eJ#oY0-1LY!=d zD?+Ck>kAUq0vgo2YRm`&I?Qkh7YGYA=$3H2AQQQ6-;;~IdPhB^h4rR%W0gW^zrIWx z)K3;=^zFJIqv7@mF{H{1`3|4B_L9OP*0&xowVLnT>t5Zw z!M4e#_=O-+92Ji2M_v4CUjD6P_d4i;bQm!ThxcF5j7hPelX!}6opcgK=XUXHe`(QX z)JED{5u|eg@2E&MZA2q}Q=hqs{c^+Gikx44X9J=AGYl)8K7qrzxVX^A#~m=rYL4{p z06}0w4@rUhHaGhS5v`YwsRaJr46kqQiV8`IO&MQb7=xZAADEEKVfUI{Q;aw#p@W^8 zn!?D*$yvI%X-GL+O#zlfq}Tadtn;euo3GkVj~j%9Dmy5wGuAIgUiMY`!;)^uv2zTR zfRk*47Aj(?x1Nf5hOfo_=*zgh-aY;cpgU1fvP%i`iTxQjmPPi9adxm2tn&Vv4x3|C zlIY=GCf8&H$JJ{5X%sllCWM!HC1Ao+I?cPUQ&ic9D>77iT`tZ7%Lz( z0wB`Q!uV_UMO0J&m13)1hHQMOQXDSlS#?+|;<()+$A?q6mveWOdpNu73@!)=Z2$7^ zSgK}&R}?W;%P$_Qf&@&h#cv^`o^5ARIRqq|OiukFeo4P$Yl?Qj=g*v%S={5vKuq(} zFc6OJ4AtK{&}_UIxA6fiM}qW-AqDiezrt^Xy~7WM!r^hhE|!(_hgLl+K%(Z5jo;!a zmVL>skif{5N^Cj{YO}lL1=A5gk~}Hl1p=XAn|(X@O3Go&7iUgjBuh~8fkcVox&hs! zI77oYO5yy2Kdh;?FSi=MeNDUYF_q1<^S^0cfK>x|*d^tdPx%rr<_d*ERc-D0Pd)+( z>-Ang@Od#K1V73DoypUguDHjlo1q?AxE*rnHOR(*7xZpYXJSeNY&2secpvpFkFt2f zn+%nE8RuG~!R(O?M%f6{mQao^9o3vlhx?*~6KmXu4L-2IXC`!2V~#WiN9@kk?cN8C zy=C)QMWKp@mqtlZnU_j8o|P8cDXe)!7NB0SM3|=>o;N28%rU(WD>E_SQzTcI~o|f>1V&GwQ@$@!iK#wm? zcHvC3LYW{rEIhZlw>-7~h3og6di4s%?wNVdiaH2AEfp>`8qnn32siMXPR)zXmg};6 zmZ)!L`rs9s|EKUot+rZjS1&Rwv!HSuuYkdJK8h1WP$df&Kjaz#JSLPtp$WZ&RzO^}G$p0|xf67C5;c zHC@my8J|jINe!{lLF=OgS1i%i^B&ct4F2Su0SHWh>f=6ZM2;UlX*b*RGxxyl4q3Y- z>&pbh^R3$3xB3>P9U&n<-_vVkbA2gg<^B0DP)ZKL3*xJ|pfBD_&G}FZ1l#J)Sc9No@!+LqckU2aF&_$YO}x_ooEPU3RTzF~1^%kSn1LKm?v zn4zrYzepVKm^-<_pA_~>N?2Gp;#|flELH1H!ua%m&%NAk;`sof%*-1)&^u6Mk4QiD z;Pc|oWs&L~{6y{QfRa68ezfMynjR17(DvW0$nkEHF|_DKNO2n4q8|Mn#=8Vr2;Iy7t_0QwsLC zLiq08yI@5R#R$NbDuLUJ@#E8_&!JETj4&3*k8^f(bnNQuyW!>Q6_zn!dV9jj%A$`w zOzpEt!4PJZdX)+VCN9vTv1+_VF$2^93}-B3D;Tk<@*={*c#OKb3kHM1(SQ6PJw4s- ziQHE^ZHdv5&>@wVA7|s_1Dl(hg9%~;usN@J z^9KvCvQ`U3Q!g=^5*5Gd3cCM3jajzUNu-lBA@hgQSWI4K_A5kBca#A%OCp#w5KULwnlC${|UC zZ6dyq!Qge%uhr$wwv2>9q(cui-t~MD?A25Mt-i|OB~Fsv?8SQflPb+uR3B(_F3gvZltqUy zpS^pif~T#JNrnV-zqyL3#~y*s3Y&X7@Uk>uX9-lCo_bSDs#eUSn$oAAmO#VYn{{*6 z+;j4yNCRXXt@W-V_ppvee3WG;uoKpYn4tB{xFj1N*<~bsXlvGVBC|NP37VWI@Y>D( z_5O8FVy=c1Z56|sdtiHhoJuNRvk@v%t_KJakeAmE(r8f$-)(Je5%Bj2Nf$Z>tFpbj z^K`s5MQKs`dv9tziMLQ0_-F;JksX)2Sln-c+#Mf@g6@uW7mdX=ywcFnfcyLV(?xLI zqJT{Snbm1nKA@Yk)-xCtigz$-GBJ;Xh*=J3%@00De*3U>cD zb$cd0|Gdm8UodCm$HhCV>yZZp?);Z=ei7)v06;fZTIx@If=NACJ^%Ov#sWhpB0~q+ z&@3)44ke%MRe2f`!cv?um{6~aW~bd8Xc zq2i2p^mYgJzcN{%d$v0jKA5Y9>BrgR^>1$7`Mpn?39L9EW9XA4@dIeIbPEg)Z>H7P z>y?*!>r^vni>s}dn85V;9!~tqn|WWQaOt&k#hqDUQe-422`DOkZ2%R-57s_7*)ZMn z9I>&nF?HYa$R7CY04@+=#jDr{1L5Yj?ki<54CWX9uFi^(GBc6&TOlSKRBD_LgoB+O z9u^jse^X6FM8p}&Hh0+2?q9w)J_X#Z3;8e@?2Nh1|5ylKbVYYq$)Wjb+7~;=8)Dh? zqu&2bY=n#Dl%5Jt_atP0K6NC>M1mh6Y|&0?1M9%^h-pH+`3ezRaU zX~0FI+LF#;{}lair`K`px^o;E%>*uh$TGm^9BFlovZ|h2$e8H;^c9UGp<(c}mqnu9El=q*gnH+&> pbVU{;=G=#Q`aj*p{67`O2J#gTK`mcCyu@6J>1hkY*ZR27{{#Q9Wm*6L literal 0 HcmV?d00001 From 5e4aa282c4d5b5ebc9f3799e7eadf2930d3dd82e Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Sat, 4 Apr 2020 11:31:43 -0400 Subject: [PATCH 03/30] Update README --- README | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/README b/README index c23782c..dddbc01 100644 --- a/README +++ b/README @@ -1,14 +1,19 @@ -DSHARP version 1.0 +# DSHARP + +![dsharp logo](logo.png) + +DSHARP is an open source CNF -> d-DNNF compiler based on sharpSAT. Similar to the c2d software, DSHARP takes a boolean theory in conjunctive normal form as input, and compiles it into deterministic decomposable negation normal form. + +## Usage If you would like the solver to use infinite precision numbers for the counting, you must have the GMP library (libgmp-dev) installed. To use the version with GMP, copy the Makefile_gmp to Makefile. Otherwise, copy Makefile_nogmp to Makefile and proceed normally. -To compile this version of DSHARP simply run -make +To compile this version of DSHARP simply run `make` -Please cite using the following: +## Citing @inproceedings{Muise2012, author = {Muise, Christian and McIlraith, Sheila A. and Beck, J. Christopher and Hsu, Eric}, @@ -16,4 +21,4 @@ Please cite using the following: title = {{DSHARP: Fast d-DNNF Compilation with sharpSAT}}, keywords = {sat, knowledge compilation}, year = {2012} -} \ No newline at end of file +} From 37ad32189969e7e741a53584b7d374fd648f5ce9 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Sat, 4 Apr 2020 11:32:41 -0400 Subject: [PATCH 04/30] Renaming readme. --- README => README.md | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename README => README.md (100%) diff --git a/README b/README.md similarity index 100% rename from README rename to README.md From b8b25260632df82ed9b202e66fd156a68299207c Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Sat, 4 Apr 2020 11:33:09 -0400 Subject: [PATCH 05/30] Update README.md --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index dddbc01..da8b31d 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ proceed normally. To compile this version of DSHARP simply run `make` ## Citing - +``` @inproceedings{Muise2012, author = {Muise, Christian and McIlraith, Sheila A. and Beck, J. Christopher and Hsu, Eric}, booktitle = {Canadian Conference on Artificial Intelligence}, @@ -22,3 +22,4 @@ To compile this version of DSHARP simply run `make` keywords = {sat, knowledge compilation}, year = {2012} } +``` From 970a7ec5dad8e76888b5373d7360813f4d996f7f Mon Sep 17 00:00:00 2001 From: Guillaume Girol Date: Wed, 17 Mar 2021 17:35:26 +0100 Subject: [PATCH 06/30] fix OR node choice variables * choice variables are variables (unsigned) not literals (signed) * remove conditional in NNF code that becomes redundant based on the above * fix that literals are translated but not choice variables, which could lead to wrong OR node labeling --- src/src_sharpSAT/MainSolver/DecisionTree.cpp | 6 +-- src/src_sharpSAT/MainSolver/DecisionTree.h | 2 +- src/src_sharpSAT/MainSolver/MainSolver.cpp | 2 +- src/src_sharpSAT/MainSolver/MainSolver.h | 56 +++++++++++++++++--- 4 files changed, 51 insertions(+), 15 deletions(-) diff --git a/src/src_sharpSAT/MainSolver/DecisionTree.cpp b/src/src_sharpSAT/MainSolver/DecisionTree.cpp index a9a3f11..a13a465 100644 --- a/src/src_sharpSAT/MainSolver/DecisionTree.cpp +++ b/src/src_sharpSAT/MainSolver/DecisionTree.cpp @@ -723,11 +723,7 @@ void DTNode::genNNF(ostream & out) } else if (DT_OR == type) { - //Dimitar Sht. Shterionov: ignoring negative values on OR nodes - if (choiceVar > 0) - out << "O " << choiceVar << " " << children.size(); - else - out << "O 0 " << children.size(); + out << "O " << choiceVar << " " << children.size(); if (2 != children.size()) toSTDOUT("Error: Or node with " << children.size() << " children."); diff --git a/src/src_sharpSAT/MainSolver/DecisionTree.h b/src/src_sharpSAT/MainSolver/DecisionTree.h index 66d1b7b..678f7b8 100644 --- a/src/src_sharpSAT/MainSolver/DecisionTree.h +++ b/src/src_sharpSAT/MainSolver/DecisionTree.h @@ -50,7 +50,7 @@ class DTNode public: - int choiceVar; + unsigned choiceVar; int nnfID; bool checked; diff --git a/src/src_sharpSAT/MainSolver/MainSolver.cpp b/src/src_sharpSAT/MainSolver/MainSolver.cpp index 2cf533a..41704ac 100755 --- a/src/src_sharpSAT/MainSolver/MainSolver.cpp +++ b/src/src_sharpSAT/MainSolver/MainSolver.cpp @@ -356,7 +356,7 @@ bool CMainSolver::decide() DTNode * leftLit = get_lit_node(theLit.toSignedInt()); DTNode * rightLit = get_lit_node(-1 * theLit.toSignedInt()); - newNode->choiceVar = theLit.toSignedInt(); + newNode->choiceVar = theLit.toVarIdx(); // Set the parents left->addParent(newNode, true); diff --git a/src/src_sharpSAT/MainSolver/MainSolver.h b/src/src_sharpSAT/MainSolver/MainSolver.h index 1eb440c..eb3f4d7 100644 --- a/src/src_sharpSAT/MainSolver/MainSolver.h +++ b/src/src_sharpSAT/MainSolver/MainSolver.h @@ -333,7 +333,7 @@ class CMainSolver: public CInstanceGraph out << "AND"; break; case DT_OR: - out << "OR"; + out << "OR " << node->choiceVar; break; case DT_BOTTOM: out << "F"; @@ -442,14 +442,54 @@ class CMainSolver: public CInstanceGraph } void translateLiterals(const vector varTranslation) { - for (int i = 0; i < litNodes.size(); i++) { - if (litNodes[i]->getVal() < 0) - { - litNodes[i]->setVal(-1 * varTranslation[-1 * litNodes[i]->getVal()]); - } - else + set nodesSeen; + queue openList; + openList.push(decStack.top().getDTNode()); + + int rootID = openList.front()->getID(); + + DTNode *node; + while (!openList.empty()) + { + node = openList.front(); + openList.pop(); + + int node_id = node->getID(); + + if (nodesSeen.find(node_id) == nodesSeen.end()) { - litNodes[i]->setVal(varTranslation[litNodes[i]->getVal()]); + // Make sure we don't add this twice + nodesSeen.insert(node_id); + + // Add the children to the open list + set::iterator it; + for (it = node->getChildrenBegin(); it + != node->getChildrenEnd(); it++) + { + openList.push(*it); + } + + // process the node + if (DT_LIT == node->getType()) + { + if (node->getVal() < 0) + { + node->setVal(-1 * varTranslation[-1 * node->getVal()]); + } + else + { + node->setVal(varTranslation[node->getVal()]); + } + } + + if (DT_OR == node->getType()) + { + if (node->choiceVar) { + node->choiceVar = varTranslation[node->choiceVar]; + } + } + + } } } From 8f8dbff2666c0e312d87e2e23450d755117874fc Mon Sep 17 00:00:00 2001 From: Guillaume Girol Date: Tue, 23 Mar 2021 17:59:37 +0100 Subject: [PATCH 07/30] fixup! fix OR node choice variables --- .../MainSolver/InstanceGraph/InstanceGraph.cpp | 4 ++-- .../MainSolver/InstanceGraph/InstanceGraph.h | 12 ++++++------ src/src_sharpSAT/MainSolver/MainSolver.h | 4 ++-- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp index d51c128..14e506f 100644 --- a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp +++ b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp @@ -944,8 +944,8 @@ bool CInstanceGraph::createfromFile(const char* lpstrFileName) //--- and add the default values for all variables for (unsigned int i = 0; i <= countAllVars(); i++) { - varTranslation[(int) i] = (int) i; - varUntranslation[(int) i] = (int) i; + varTranslation[(int) i] = i; + varUntranslation[(int) i] = i; } return true; diff --git a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h index 1c3da31..9c142e5 100644 --- a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h +++ b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h @@ -47,9 +47,9 @@ class CInstanceGraph unsigned int numBinClauses; unsigned int numBinCCls; - vector varTranslation; - vector varUntranslation; - vector origTranslation; + vector varTranslation; + vector varUntranslation; + vector origTranslation; protected: @@ -172,17 +172,17 @@ class CInstanceGraph CInstanceGraph(); ~CInstanceGraph(); - const vector & getVarTranslation() const + const vector & getVarTranslation() const { return varTranslation; } - const vector & getVarUnTranslation() const + const vector & getVarUnTranslation() const { return varUntranslation; } - const vector & getOrigTranslation() const + const vector & getOrigTranslation() const { return origTranslation; } diff --git a/src/src_sharpSAT/MainSolver/MainSolver.h b/src/src_sharpSAT/MainSolver/MainSolver.h index eb3f4d7..c770b25 100644 --- a/src/src_sharpSAT/MainSolver/MainSolver.h +++ b/src/src_sharpSAT/MainSolver/MainSolver.h @@ -432,7 +432,7 @@ class CMainSolver: public CInstanceGraph } } - void print_translation(const vector trans) + void print_translation(const vector trans) { toSTDOUT("Translation:" << endl); for (int i = 0; i < trans.size(); ++i) @@ -441,7 +441,7 @@ class CMainSolver: public CInstanceGraph } } - void translateLiterals(const vector varTranslation) { + void translateLiterals(const vector varTranslation) { set nodesSeen; queue openList; openList.push(decStack.top().getDTNode()); From 9eac83bdbbac9bdb0688958d1948cc558d6cb670 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Wed, 24 Mar 2021 17:10:48 +0000 Subject: [PATCH 08/30] Adding .gitignore file. --- .gitignore | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 .gitignore diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..e93fa3a --- /dev/null +++ b/.gitignore @@ -0,0 +1,7 @@ +.venv +Makefile +dsharp + +*.dot +*.nnf +*.png From e76dbc1d0e748f092546815bf8e584064f76972a Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Wed, 24 Mar 2021 17:11:25 +0000 Subject: [PATCH 09/30] Setting the choiceVar everywhere that needs it. --- src/src_sharpSAT/MainSolver/DecisionTree.cpp | 1 + src/src_sharpSAT/MainSolver/MainSolver.cpp | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/src_sharpSAT/MainSolver/DecisionTree.cpp b/src/src_sharpSAT/MainSolver/DecisionTree.cpp index a13a465..389c109 100644 --- a/src/src_sharpSAT/MainSolver/DecisionTree.cpp +++ b/src/src_sharpSAT/MainSolver/DecisionTree.cpp @@ -820,6 +820,7 @@ void DTNode::smooth(int &num_nodes, CMainSolver &solver, set &literals) newAnd->addChild(newOr, true); newOr->addChild(solver.get_lit_node_full(var), true); newOr->addChild(solver.get_lit_node_full(-1 * var), true); + newOr->choiceVar = (unsigned) var; } } // Record the new values diff --git a/src/src_sharpSAT/MainSolver/MainSolver.cpp b/src/src_sharpSAT/MainSolver/MainSolver.cpp index 41704ac..bca80f2 100755 --- a/src/src_sharpSAT/MainSolver/MainSolver.cpp +++ b/src/src_sharpSAT/MainSolver/MainSolver.cpp @@ -179,6 +179,7 @@ void CMainSolver::solve(const char *lpstrFileName) // Add an arbitrary choice between the two DTNode* newOr = new DTNode(DT_OR, num_Nodes++); + newOr->choiceVar = (unsigned) i; decStack.top().getDTNode()->addChild(newOr, true); newOr->addChild(new DTNode(i, true, num_Nodes++), true); newOr->addChild(new DTNode((-1 * i), true, num_Nodes++), true); @@ -192,6 +193,7 @@ void CMainSolver::solve(const char *lpstrFileName) newOr->addChild(get_lit_node_full(-1 * i), true); newOr->addChild(newAnd, true); + newOr->choiceVar = (unsigned) i; newAnd->addChild(new DTNode(i, true, num_Nodes++), true); newAnd->addChild(botNode, true); @@ -205,6 +207,7 @@ void CMainSolver::solve(const char *lpstrFileName) newOr->addChild(get_lit_node_full(i), true); newOr->addChild(newAnd, true); + newOr->choiceVar = (unsigned) i; newAnd->addChild(new DTNode((-1 * i), true, num_Nodes++), true); newAnd->addChild(botNode, true); From 07292dd5b2a89833dcbe3e4f728157d2a2c81fe3 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Tue, 22 Jun 2021 02:17:55 +0000 Subject: [PATCH 10/30] Update on what to ignore. --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index e93fa3a..d0f7711 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,4 @@ dsharp *.dot *.nnf *.png +*.o From 11fe18650578b9807d1896ea26cc04f0baeaa3d3 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Tue, 22 Jun 2021 02:19:03 +0000 Subject: [PATCH 11/30] Fixing bug with trivial UNSAT theories reporting SAT. --- src/src_sharpSAT/MainSolver/MainSolver.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/src_sharpSAT/MainSolver/MainSolver.cpp b/src/src_sharpSAT/MainSolver/MainSolver.cpp index bca80f2..d087259 100755 --- a/src/src_sharpSAT/MainSolver/MainSolver.cpp +++ b/src/src_sharpSAT/MainSolver/MainSolver.cpp @@ -1466,7 +1466,11 @@ bool CMainSolver::prepBCP(LiteralIdT firstLit) CVariableVertex *pV; for (unsigned int i = 0; i < impls.size(); i++) - if (getVar(impls[i]).setVal(impls[i].polarity(), 0)) + + if (getVar(impls[i]).getVal() == impls[i].oppositeLit().polarityTriVal()) + return false; + + else if (getVar(impls[i]).setVal(impls[i].polarity(), 0)) { unLit = impls[i].oppositeLit(); satLit = impls[i]; From 8345b5cb4370ac3c44a45994c474f78fdd6e3318 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Tue, 22 Jun 2021 02:19:25 +0000 Subject: [PATCH 12/30] Output an empty OR when things are UNSAT. --- src/src_sharpSAT/MainSolver/MainSolver.h | 17 +++++++++++++++-- src/src_sharpSAT/main.cpp | 9 +++++---- 2 files changed, 20 insertions(+), 6 deletions(-) diff --git a/src/src_sharpSAT/MainSolver/MainSolver.h b/src/src_sharpSAT/MainSolver/MainSolver.h index c770b25..0fdda13 100644 --- a/src/src_sharpSAT/MainSolver/MainSolver.h +++ b/src/src_sharpSAT/MainSolver/MainSolver.h @@ -273,7 +273,7 @@ class CMainSolver: public CInstanceGraph stopWatch.setTimeBound(i); } - void writeBDG(const char *fileName) + void writeBDG(const char *fileName, bool falsify=false) { set nodesSeen; set litsSeen; @@ -283,6 +283,12 @@ class CMainSolver: public CInstanceGraph out << "digraph backdoorgraph {" << endl; + if (falsify) { + out << " root [label=\"OR\"];" << endl; + out << "}" << endl; + return; + } + // First add the root if (1 == decStack.top().getDTNode()->numChildren()) openList.push(decStack.top().getDTNode()->onlyChild()); @@ -409,9 +415,16 @@ class CMainSolver: public CInstanceGraph } - void writeNNF(const char *fileName) + void writeNNF(const char *fileName, bool falsify=false) { ofstream out(fileName); + + if (falsify) { + out << "nnf 1 0 0" << endl; + out << "O 0 0" << endl; + return; + } + vector *nodeList = new vector (); DTNode* root; diff --git a/src/src_sharpSAT/main.cpp b/src/src_sharpSAT/main.cpp index e2ccf40..1bc678b 100644 --- a/src/src_sharpSAT/main.cpp +++ b/src/src_sharpSAT/main.cpp @@ -247,16 +247,17 @@ int main(int argc, char *argv[]) if (fileout) theRunAn.getData().writeToFile(dataFile); + bool falsify = false; if (0 == theRunAn.getData().getNumSatAssignments()) { - cout << "\nTheory is unsat. Skipping file output.\n" << endl; - return 0; + cout << "\nTheory is unsat. Resetting d-DNNF to empty Or.\n" << endl; + falsify = true; } if (graphFileout) - theSolver.writeBDG(graphFile); + theSolver.writeBDG(graphFile, falsify); if (nnfFileout) - theSolver.writeNNF(nnfFile); + theSolver.writeNNF(nnfFile, falsify); return 0; } From c4b24121b07d67004d06fd2e7b24c232b28e435d Mon Sep 17 00:00:00 2001 From: Guillaume Girol Date: Tue, 29 Jun 2021 12:00:00 +0000 Subject: [PATCH 13/30] report the correct number of variables in unsat nnf --- src/src_sharpSAT/MainSolver/MainSolver.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/src_sharpSAT/MainSolver/MainSolver.h b/src/src_sharpSAT/MainSolver/MainSolver.h index 0fdda13..a3eaf15 100644 --- a/src/src_sharpSAT/MainSolver/MainSolver.h +++ b/src/src_sharpSAT/MainSolver/MainSolver.h @@ -420,7 +420,7 @@ class CMainSolver: public CInstanceGraph ofstream out(fileName); if (falsify) { - out << "nnf 1 0 0" << endl; + out << "nnf 1 0 " << bdg_var_count << endl; out << "O 0 0" << endl; return; } From 2d7e621b4ce6293cc4215940af80117a1324418a Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Wed, 2 Mar 2022 22:36:41 -0500 Subject: [PATCH 14/30] Delete LICENSE --- LICENSE | 339 -------------------------------------------------------- 1 file changed, 339 deletions(-) delete mode 100644 LICENSE diff --git a/LICENSE b/LICENSE deleted file mode 100644 index d159169..0000000 --- a/LICENSE +++ /dev/null @@ -1,339 +0,0 @@ - GNU GENERAL PUBLIC LICENSE - Version 2, June 1991 - - Copyright (C) 1989, 1991 Free Software Foundation, Inc., - 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - - Preamble - - The licenses for most software are designed to take away your -freedom to share and change it. By contrast, the GNU General Public -License is intended to guarantee your freedom to share and change free -software--to make sure the software is free for all its users. This -General Public License applies to most of the Free Software -Foundation's software and to any other program whose authors commit to -using it. (Some other Free Software Foundation software is covered by -the GNU Lesser General Public License instead.) You can apply it to -your programs, too. - - When we speak of free software, we are referring to freedom, not -price. Our General Public Licenses are designed to make sure that you -have the freedom to distribute copies of free software (and charge for -this service if you wish), that you receive source code or can get it -if you want it, that you can change the software or use pieces of it -in new free programs; and that you know you can do these things. - - To protect your rights, we need to make restrictions that forbid -anyone to deny you these rights or to ask you to surrender the rights. -These restrictions translate to certain responsibilities for you if you -distribute copies of the software, or if you modify it. - - For example, if you distribute copies of such a program, whether -gratis or for a fee, you must give the recipients all the rights that -you have. You must make sure that they, too, receive or can get the -source code. And you must show them these terms so they know their -rights. - - We protect your rights with two steps: (1) copyright the software, and -(2) offer you this license which gives you legal permission to copy, -distribute and/or modify the software. - - Also, for each author's protection and ours, we want to make certain -that everyone understands that there is no warranty for this free -software. If the software is modified by someone else and passed on, we -want its recipients to know that what they have is not the original, so -that any problems introduced by others will not reflect on the original -authors' reputations. - - Finally, any free program is threatened constantly by software -patents. We wish to avoid the danger that redistributors of a free -program will individually obtain patent licenses, in effect making the -program proprietary. To prevent this, we have made it clear that any -patent must be licensed for everyone's free use or not licensed at all. - - The precise terms and conditions for copying, distribution and -modification follow. - - GNU GENERAL PUBLIC LICENSE - TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION - - 0. This License applies to any program or other work which contains -a notice placed by the copyright holder saying it may be distributed -under the terms of this General Public License. The "Program", below, -refers to any such program or work, and a "work based on the Program" -means either the Program or any derivative work under copyright law: -that is to say, a work containing the Program or a portion of it, -either verbatim or with modifications and/or translated into another -language. (Hereinafter, translation is included without limitation in -the term "modification".) Each licensee is addressed as "you". - -Activities other than copying, distribution and modification are not -covered by this License; they are outside its scope. The act of -running the Program is not restricted, and the output from the Program -is covered only if its contents constitute a work based on the -Program (independent of having been made by running the Program). -Whether that is true depends on what the Program does. - - 1. You may copy and distribute verbatim copies of the Program's -source code as you receive it, in any medium, provided that you -conspicuously and appropriately publish on each copy an appropriate -copyright notice and disclaimer of warranty; keep intact all the -notices that refer to this License and to the absence of any warranty; -and give any other recipients of the Program a copy of this License -along with the Program. - -You may charge a fee for the physical act of transferring a copy, and -you may at your option offer warranty protection in exchange for a fee. - - 2. You may modify your copy or copies of the Program or any portion -of it, thus forming a work based on the Program, and copy and -distribute such modifications or work under the terms of Section 1 -above, provided that you also meet all of these conditions: - - a) You must cause the modified files to carry prominent notices - stating that you changed the files and the date of any change. - - b) You must cause any work that you distribute or publish, that in - whole or in part contains or is derived from the Program or any - part thereof, to be licensed as a whole at no charge to all third - parties under the terms of this License. - - c) If the modified program normally reads commands interactively - when run, you must cause it, when started running for such - interactive use in the most ordinary way, to print or display an - announcement including an appropriate copyright notice and a - notice that there is no warranty (or else, saying that you provide - a warranty) and that users may redistribute the program under - these conditions, and telling the user how to view a copy of this - License. (Exception: if the Program itself is interactive but - does not normally print such an announcement, your work based on - the Program is not required to print an announcement.) - -These requirements apply to the modified work as a whole. If -identifiable sections of that work are not derived from the Program, -and can be reasonably considered independent and separate works in -themselves, then this License, and its terms, do not apply to those -sections when you distribute them as separate works. But when you -distribute the same sections as part of a whole which is a work based -on the Program, the distribution of the whole must be on the terms of -this License, whose permissions for other licensees extend to the -entire whole, and thus to each and every part regardless of who wrote it. - -Thus, it is not the intent of this section to claim rights or contest -your rights to work written entirely by you; rather, the intent is to -exercise the right to control the distribution of derivative or -collective works based on the Program. - -In addition, mere aggregation of another work not based on the Program -with the Program (or with a work based on the Program) on a volume of -a storage or distribution medium does not bring the other work under -the scope of this License. - - 3. You may copy and distribute the Program (or a work based on it, -under Section 2) in object code or executable form under the terms of -Sections 1 and 2 above provided that you also do one of the following: - - a) Accompany it with the complete corresponding machine-readable - source code, which must be distributed under the terms of Sections - 1 and 2 above on a medium customarily used for software interchange; or, - - b) Accompany it with a written offer, valid for at least three - years, to give any third party, for a charge no more than your - cost of physically performing source distribution, a complete - machine-readable copy of the corresponding source code, to be - distributed under the terms of Sections 1 and 2 above on a medium - customarily used for software interchange; or, - - c) Accompany it with the information you received as to the offer - to distribute corresponding source code. (This alternative is - allowed only for noncommercial distribution and only if you - received the program in object code or executable form with such - an offer, in accord with Subsection b above.) - -The source code for a work means the preferred form of the work for -making modifications to it. For an executable work, complete source -code means all the source code for all modules it contains, plus any -associated interface definition files, plus the scripts used to -control compilation and installation of the executable. However, as a -special exception, the source code distributed need not include -anything that is normally distributed (in either source or binary -form) with the major components (compiler, kernel, and so on) of the -operating system on which the executable runs, unless that component -itself accompanies the executable. - -If distribution of executable or object code is made by offering -access to copy from a designated place, then offering equivalent -access to copy the source code from the same place counts as -distribution of the source code, even though third parties are not -compelled to copy the source along with the object code. - - 4. You may not copy, modify, sublicense, or distribute the Program -except as expressly provided under this License. Any attempt -otherwise to copy, modify, sublicense or distribute the Program is -void, and will automatically terminate your rights under this License. -However, parties who have received copies, or rights, from you under -this License will not have their licenses terminated so long as such -parties remain in full compliance. - - 5. You are not required to accept this License, since you have not -signed it. However, nothing else grants you permission to modify or -distribute the Program or its derivative works. These actions are -prohibited by law if you do not accept this License. Therefore, by -modifying or distributing the Program (or any work based on the -Program), you indicate your acceptance of this License to do so, and -all its terms and conditions for copying, distributing or modifying -the Program or works based on it. - - 6. Each time you redistribute the Program (or any work based on the -Program), the recipient automatically receives a license from the -original licensor to copy, distribute or modify the Program subject to -these terms and conditions. You may not impose any further -restrictions on the recipients' exercise of the rights granted herein. -You are not responsible for enforcing compliance by third parties to -this License. - - 7. If, as a consequence of a court judgment or allegation of patent -infringement or for any other reason (not limited to patent issues), -conditions are imposed on you (whether by court order, agreement or -otherwise) that contradict the conditions of this License, they do not -excuse you from the conditions of this License. If you cannot -distribute so as to satisfy simultaneously your obligations under this -License and any other pertinent obligations, then as a consequence you -may not distribute the Program at all. For example, if a patent -license would not permit royalty-free redistribution of the Program by -all those who receive copies directly or indirectly through you, then -the only way you could satisfy both it and this License would be to -refrain entirely from distribution of the Program. - -If any portion of this section is held invalid or unenforceable under -any particular circumstance, the balance of the section is intended to -apply and the section as a whole is intended to apply in other -circumstances. - -It is not the purpose of this section to induce you to infringe any -patents or other property right claims or to contest validity of any -such claims; this section has the sole purpose of protecting the -integrity of the free software distribution system, which is -implemented by public license practices. Many people have made -generous contributions to the wide range of software distributed -through that system in reliance on consistent application of that -system; it is up to the author/donor to decide if he or she is willing -to distribute software through any other system and a licensee cannot -impose that choice. - -This section is intended to make thoroughly clear what is believed to -be a consequence of the rest of this License. - - 8. If the distribution and/or use of the Program is restricted in -certain countries either by patents or by copyrighted interfaces, the -original copyright holder who places the Program under this License -may add an explicit geographical distribution limitation excluding -those countries, so that distribution is permitted only in or among -countries not thus excluded. In such case, this License incorporates -the limitation as if written in the body of this License. - - 9. The Free Software Foundation may publish revised and/or new versions -of the General Public License from time to time. Such new versions will -be similar in spirit to the present version, but may differ in detail to -address new problems or concerns. - -Each version is given a distinguishing version number. If the Program -specifies a version number of this License which applies to it and "any -later version", you have the option of following the terms and conditions -either of that version or of any later version published by the Free -Software Foundation. If the Program does not specify a version number of -this License, you may choose any version ever published by the Free Software -Foundation. - - 10. If you wish to incorporate parts of the Program into other free -programs whose distribution conditions are different, write to the author -to ask for permission. For software which is copyrighted by the Free -Software Foundation, write to the Free Software Foundation; we sometimes -make exceptions for this. Our decision will be guided by the two goals -of preserving the free status of all derivatives of our free software and -of promoting the sharing and reuse of software generally. - - NO WARRANTY - - 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY -FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN -OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES -PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED -OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF -MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS -TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE -PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, -REPAIR OR CORRECTION. - - 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING -WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR -REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, -INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING -OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED -TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY -YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER -PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE -POSSIBILITY OF SUCH DAMAGES. - - END OF TERMS AND CONDITIONS - - How to Apply These Terms to Your New Programs - - If you develop a new program, and you want it to be of the greatest -possible use to the public, the best way to achieve this is to make it -free software which everyone can redistribute and change under these terms. - - To do so, attach the following notices to the program. It is safest -to attach them to the start of each source file to most effectively -convey the exclusion of warranty; and each file should have at least -the "copyright" line and a pointer to where the full notice is found. - - - Copyright (C) - - This program is free software; you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation; either version 2 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License along - with this program; if not, write to the Free Software Foundation, Inc., - 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. - -Also add information on how to contact you by electronic and paper mail. - -If the program is interactive, make it output a short notice like this -when it starts in an interactive mode: - - Gnomovision version 69, Copyright (C) year name of author - Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'. - This is free software, and you are welcome to redistribute it - under certain conditions; type `show c' for details. - -The hypothetical commands `show w' and `show c' should show the appropriate -parts of the General Public License. Of course, the commands you use may -be called something other than `show w' and `show c'; they could even be -mouse-clicks or menu items--whatever suits your program. - -You should also get your employer (if you work as a programmer) or your -school, if any, to sign a "copyright disclaimer" for the program, if -necessary. Here is a sample; alter the names: - - Yoyodyne, Inc., hereby disclaims all copyright interest in the program - `Gnomovision' (which makes passes at compilers) written by James Hacker. - - , 1 April 1989 - Ty Coon, President of Vice - -This General Public License does not permit incorporating your program into -proprietary programs. If your program is a subroutine library, you may -consider it more useful to permit linking proprietary applications with the -library. If this is what you want to do, use the GNU Lesser General -Public License instead of this License. From fd880bd416ff0b3d3af99b2b580e61fde9c1f225 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Wed, 2 Mar 2022 22:38:01 -0500 Subject: [PATCH 15/30] Create LICENSE --- LICENSE | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 LICENSE diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..3d9b202 --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2022 Christian Muise + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. From 8136bc219b02a44c2a3592e43e0f04cbc1c09d9f Mon Sep 17 00:00:00 2001 From: VincentDerk Date: Wed, 16 Mar 2022 00:28:36 +0100 Subject: [PATCH 16/30] Changed DIMAC cnf file parsing --- .../InstanceGraph/InstanceGraph.cpp | 130 ++++++++---------- 1 file changed, 56 insertions(+), 74 deletions(-) diff --git a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp index 14e506f..859525e 100644 --- a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp +++ b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp @@ -2,6 +2,8 @@ #include #include #include +#include +#include CRunAnalyzer theRunAn; @@ -615,13 +617,7 @@ bool CInstanceGraph::prep_CleanUpPool() bool CInstanceGraph::createfromFile(const char* lpstrFileName) { - - const int BUF_SZ = 65536; - const int TOK_SZ = 255; - - char buf[BUF_SZ]; - char token[TOK_SZ]; - unsigned int line = 0; + unsigned int nLine = 0; unsigned int nVars, nCls; int lit; vector litVec; @@ -646,73 +642,59 @@ bool CInstanceGraph::createfromFile(const char* lpstrFileName) fclose(filedesc); ifstream inFile(lpstrFileName, ios::in); - - // read the preamble of the cnf file - while (inFile.getline(buf, BUF_SZ)) - { - line++; - if (buf[0] == 'c') - continue; - if (buf[0] == 'p') - { - if (sscanf(buf, "p cnf %d %d", &nVars, &nCls) < 2) - { - toERROUT("line "< '9')) - i++; - if (buf[i] == 0x0) continue; - while (buf[i] == '-' || buf[i] >= '0' && buf[i] <= '9') - { - token[j] = buf[i]; - i++; - j++; - } - token[j] = 0x0; - lit = atoi(token); - j = 0; - if (lit == 0) // end of clause - { - if (clauseLen > 0) - litVec.push_back(0); - clauseLen = 0; - } - else - { - clauseLen++; - litVec.push_back(lit); - } - } - } - - if (!inFile.eof()) - { - toERROUT(" CNF input: line too long"); - } - inFile.close(); - /// END FILE input + string line; + string nextWord; + + // read the preamble of the cnf file + while(std::getline(inFile, line)) + { + nLine++; + if (line.compare(0, 5, "p cnf") == 0) + { + std::stringstream linestream(line); + linestream >> nextWord; // eat 'p' + linestream >> nextWord; // eat 'cnf' + if(!(linestream >> nVars) || !(linestream >> nCls)) + { + toERROUT("line "<> firstChar) + { + if(isdigit(firstChar) || firstChar == '-') + { + inFile.unget(); + // parse clause (begins with (negative) digit) + while((inFile >> lit) && lit != 0) + { + clauseLen++; + litVec.push_back(lit); + } + if (clauseLen > 0) + litVec.push_back(0); + clauseLen = 0; + inFile.ignore(numeric_limits::max(), '\n'); // skip till next line + nLine++; + } + else if (!isspace(firstChar)) // if whitespace, we eat it instead + { + // no digit (or whitespace) so we skip the line + inFile.ignore(numeric_limits::max(),'\n'); + nLine++; + } + } + + inFile.close(); + /// END FILE input vector::iterator it, jt, itEndCl; From da2c87f8036ff69dfaa3b6e227f7e8b11c3403dd Mon Sep 17 00:00:00 2001 From: VincentDerk Date: Sun, 17 Apr 2022 00:32:30 +0200 Subject: [PATCH 17/30] Added getAvailableMemory() for more platforms --- src/src_sharpSAT/MainSolver/FormulaCache.cpp | 38 +++++++++++++------- src/src_sharpSAT/MainSolver/FormulaCache.h | 19 ++++++++-- 2 files changed, 43 insertions(+), 14 deletions(-) diff --git a/src/src_sharpSAT/MainSolver/FormulaCache.cpp b/src/src_sharpSAT/MainSolver/FormulaCache.cpp index fcbcc77..d564dde 100755 --- a/src/src_sharpSAT/MainSolver/FormulaCache.cpp +++ b/src/src_sharpSAT/MainSolver/FormulaCache.cpp @@ -1,6 +1,30 @@ -#include #include "FormulaCache.h" +unsigned long availableMem() { + //Implementation is platform depended +#ifdef __linux__ + int pgs = getpagesize(); + long int pages = get_avphys_pages(); + return (pages * pgs) / 2; +#elif __APPLE__ && __MACH__ + long pgs = sysconf(_SC_PAGE_SIZE); + long int pages = sysconf(_SC_AVPHYS_PAGES); + return page_size * pages / 2; +#elif _WIN32 + // relevant documentation: + // https://docs.microsoft.com/en-us/windows/win32/api/sysinfoapi/nf-sysinfoapi-globalmemorystatusex + MEMORYSTATUSEX statex; + statex.dwLength = sizeof(statex); + GlobalMemoryStatusEx(&statex); + return statex.ullAvailPhys; +#elif SUN_OS + // This value was the previously used value for SUN_OS + return 100*1024*1024; +#else + // Did not implement any availableMem() function for this OS ... +#endif +} + unsigned int CFormulaCache::oldestEntryAllowed = (unsigned int) -1; @@ -12,18 +36,8 @@ CFormulaCache::CFormulaCache() theEntryBase.reserve(iBuckets*10); scoresDivTime = 50000; lastDivTime = 0; -#ifdef SUN_OS - if (CSolverConf::maxCacheSize == 0) - CSolverConf::maxCacheSize = 100*1024*1024; -#endif -#ifndef SUN_OS if (CSolverConf::maxCacheSize == 0) - { - int pgs = getpagesize(); - long int pages = get_avphys_pages(); - CSolverConf::maxCacheSize = (pgs*pages)/2; - } -#endif + CSolverConf::maxCacheSize = availableMem(); } diff --git a/src/src_sharpSAT/MainSolver/FormulaCache.h b/src/src_sharpSAT/MainSolver/FormulaCache.h index 7a14f83..8d74f95 100755 --- a/src/src_sharpSAT/MainSolver/FormulaCache.h +++ b/src/src_sharpSAT/MainSolver/FormulaCache.h @@ -6,7 +6,6 @@ #include #endif -#include #include #include @@ -20,7 +19,23 @@ #include "InstanceGraph/ComponentTypes.h" #include "DecisionStack.h" #include "DecisionTree.h" -using namespace std; + + + +// Different requirements for different availableMem +// implementations - platform depended. +#ifdef __linux__ +#include +#include +#elif __APPLE__ && __MACH__ +#include +#elif _WIN32 +#include +#endif +/** + * @return Available memory in bytes + */ +unsigned long availableMem(); typedef unsigned int CacheEntryId; From 29432fa7d09eb07c98c52345e152c620e365df14 Mon Sep 17 00:00:00 2001 From: VincentDerk Date: Sun, 17 Apr 2022 00:32:53 +0200 Subject: [PATCH 18/30] Changed uint to unsigned int --- src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h b/src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h index 93a1476..3b6e655 100755 --- a/src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h +++ b/src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h @@ -324,8 +324,8 @@ template bool CPackedCompId<_T,_bitsPerBlock>::equals(const CComponentId &rComp) const { - if ( (theVars.capacity() != (uint) rComp.countVars()*bpeVars/_bitsPerBlock +1) - || theClauses.capacity() != (uint) rComp.countCls()*bpeCls/_bitsPerBlock +1) return false; + if ( (theVars.capacity() != (unsigned int) rComp.countVars()*bpeVars/_bitsPerBlock +1) + || theClauses.capacity() != (unsigned int) rComp.countCls()*bpeCls/_bitsPerBlock +1) return false; unsigned int bitpos = 0; unsigned int h = 0; From b572e300b779b1421751a3b7444af316dee6ebfd Mon Sep 17 00:00:00 2001 From: VincentDerk Date: Tue, 19 Apr 2022 18:45:36 +0200 Subject: [PATCH 19/30] Replaced/removed 'using namespace std'. It is not advised to use 'using namespace std' on header files. For example, it causes issues for #include "windows.h" (https://developercommunity.visualstudio.com/t/error-c2872-byte-ambiguous-symbol/93889) --- src/shared/Interface/AnalyzerData.h | 5 +- src/shared/RealNumberTypes.h | 53 +++-- src/shared/SomeTime.h | 203 +++++++++--------- src/src_sharpSAT/Basics.h | 180 ++++++++-------- src/src_sharpSAT/MainSolver/DecisionStack.h | 1 - src/src_sharpSAT/MainSolver/DecisionTree.h | 3 +- .../MainSolver/InstanceGraph/AtomsAndNodes.h | 2 +- .../MainSolver/InstanceGraph/ComponentTypes.h | 1 - .../InstanceGraph/InstanceGraph.cpp | 7 +- .../MainSolver/InstanceGraph/InstanceGraph.h | 1 - src/src_sharpSAT/MainSolver/MainSolver.cpp | 4 +- src/src_sharpSAT/MainSolver/MainSolver.h | 4 + 12 files changed, 235 insertions(+), 229 deletions(-) diff --git a/src/shared/Interface/AnalyzerData.h b/src/shared/Interface/AnalyzerData.h index edaad3a..780214d 100755 --- a/src/shared/Interface/AnalyzerData.h +++ b/src/shared/Interface/AnalyzerData.h @@ -16,7 +16,10 @@ #include -using namespace std; +using std::vector; +using std::ifstream; +using std::ofstream; +using std::endl; enum DATA_IDX { diff --git a/src/shared/RealNumberTypes.h b/src/shared/RealNumberTypes.h index 3a41b5c..6055b4d 100755 --- a/src/shared/RealNumberTypes.h +++ b/src/shared/RealNumberTypes.h @@ -1,27 +1,26 @@ -#ifndef REALNUMBERTYPES_H -#define REALNUMBERTYPES_H - - - -using namespace std; - -#ifdef GMP_BIGNUM -#include -typedef mpf_class CRealNum; -extern bool pow(mpf_class &res, const mpf_class &base, unsigned long int iExp); -extern bool pow2(mpf_class &res, unsigned long int iExp); -extern bool to_div_2exp(mpf_class &res, const mpf_class &op1, unsigned long int iExp); -extern double to_doubleT(const mpf_class &num); - - - -#else -typedef long double CRealNum; - -extern bool pow(CRealNum &res, CRealNum base, unsigned long int iExp); -extern bool pow2(CRealNum &res, unsigned long int iExp); -extern bool to_div_2exp(CRealNum &res, const CRealNum &op1, unsigned long int iExp); -extern long double to_doubleT(const CRealNum &num); -#endif - -#endif +#ifndef REALNUMBERTYPES_H +#define REALNUMBERTYPES_H + + + + +#ifdef GMP_BIGNUM +#include +typedef mpf_class CRealNum; +extern bool pow(mpf_class &res, const mpf_class &base, unsigned long int iExp); +extern bool pow2(mpf_class &res, unsigned long int iExp); +extern bool to_div_2exp(mpf_class &res, const mpf_class &op1, unsigned long int iExp); +extern double to_doubleT(const mpf_class &num); + + + +#else +typedef long double CRealNum; + +extern bool pow(CRealNum &res, CRealNum base, unsigned long int iExp); +extern bool pow2(CRealNum &res, unsigned long int iExp); +extern bool to_div_2exp(CRealNum &res, const CRealNum &op1, unsigned long int iExp); +extern long double to_doubleT(const CRealNum &num); +#endif + +#endif diff --git a/src/shared/SomeTime.h b/src/shared/SomeTime.h index a5e13c0..8971c51 100755 --- a/src/shared/SomeTime.h +++ b/src/shared/SomeTime.h @@ -1,102 +1,101 @@ -#ifndef SOMETIME_H -#define SOMETIME_H - -#include -#include // To seed random generator - -using namespace std; - -extern bool diffTimes(timeval& ret, const timeval &tLater, const timeval &tEarlier); - -class CStepTime -{ - static int timeVal; - -public: - - static void makeStart() - { - timeVal = 0; - } - - static int getTime() - { - return timeVal; - } - - static void stepTime() - { - timeVal++; - } -}; - - - -class CStopWatch -{ - timeval timeStart; - timeval timeStop; - - long int timeBound; - -public: - - CStopWatch() {} - ~CStopWatch() {} - - bool timeBoundBroken() - { - timeval actTime; - gettimeofday(&actTime,NULL); - - return actTime.tv_sec - timeStart.tv_sec > timeBound; - } - - bool markStartTime() - { - return gettimeofday(&timeStart,NULL) == 0; - } - - bool markStopTime() - { - return gettimeofday(&timeStop,NULL) == 0; - } - - - void setTimeBound(long int seconds) - { - timeBound = seconds; - } - - long int getTimeBound() - { - return timeBound; - } - - double getElapsedTime() - { - timeval r; - double retT; - diffTimes(r,timeStop, timeStart); - - retT = r.tv_usec; - retT /= 1000000.0; - retT += (double)r.tv_sec; - return retT; - } - - unsigned int getElapsedusecs() - { - unsigned int retT; - timeval r; - - diffTimes(r,timeStop, timeStart); - - retT = r.tv_usec; - - retT += r.tv_sec * 1000000; - return retT; - } -}; - -#endif +#ifndef SOMETIME_H +#define SOMETIME_H + +#include +#include // To seed random generator + + +extern bool diffTimes(timeval& ret, const timeval &tLater, const timeval &tEarlier); + +class CStepTime +{ + static int timeVal; + +public: + + static void makeStart() + { + timeVal = 0; + } + + static int getTime() + { + return timeVal; + } + + static void stepTime() + { + timeVal++; + } +}; + + + +class CStopWatch +{ + timeval timeStart; + timeval timeStop; + + long int timeBound; + +public: + + CStopWatch() {} + ~CStopWatch() {} + + bool timeBoundBroken() + { + timeval actTime; + gettimeofday(&actTime,NULL); + + return actTime.tv_sec - timeStart.tv_sec > timeBound; + } + + bool markStartTime() + { + return gettimeofday(&timeStart,NULL) == 0; + } + + bool markStopTime() + { + return gettimeofday(&timeStop,NULL) == 0; + } + + + void setTimeBound(long int seconds) + { + timeBound = seconds; + } + + long int getTimeBound() + { + return timeBound; + } + + double getElapsedTime() + { + timeval r; + double retT; + diffTimes(r,timeStop, timeStart); + + retT = r.tv_usec; + retT /= 1000000.0; + retT += (double)r.tv_sec; + return retT; + } + + unsigned int getElapsedusecs() + { + unsigned int retT; + timeval r; + + diffTimes(r,timeStop, timeStart); + + retT = r.tv_usec; + + retT += r.tv_sec * 1000000; + return retT; + } +}; + +#endif diff --git a/src/src_sharpSAT/Basics.h b/src/src_sharpSAT/Basics.h index e63cff5..2becd18 100755 --- a/src/src_sharpSAT/Basics.h +++ b/src/src_sharpSAT/Basics.h @@ -1,90 +1,90 @@ -#ifndef _BASICS_H -#define _BASICS_H - -#include -#include -#include - -using namespace std; - - -#define FULL_DDNNF - -class CSolverConf -{ -public: - static bool analyzeConflicts; - static bool doNonChronBackTracking; - - static bool quietMode; - - static bool allowComponentCaching; - static bool allowImplicitBCP; - - static bool allowPreProcessing; - - static unsigned int secsTimeBound; - - static unsigned int maxCacheSize; // maximum Cache Size in bytes - - static int nodeCount; // Nodes currently in use - - static bool smoothNNF; - static bool ensureAllLits; - - static bool disableDynamicDecomp; - - CSolverConf(); - - ~CSolverConf(); - -}; - -#ifdef COMPILE_FOR_GUI -#define toSTDOUT(X) -#else -#define toSTDOUT(X) if(!CSolverConf::quietMode) cout << X; -#endif - - -#ifdef COMPILE_FOR_GUI -#define toERROUT(X) -#else -#define toERROUT(X) if(!CSolverConf::quietMode) cout << X; -#endif - -#ifdef DEBUG -#define toDEBUGOUT(X) if(!CSolverConf::quietMode) cout << X; -#else -#define toDEBUGOUT(X) -#endif - - -enum SOLVER_StateT -{ - - SUCCESS, - TIMEOUT, - ABORTED -}; - -enum TriValue -{ - - F = 0, - W = 1, - X = 2 -}; - -enum DT_NodeType -{ - DT_AND, - DT_OR, - DT_LIT, - DT_TOP, - DT_BOTTOM -}; - - -extern char TriValuetoChar(TriValue v); -#endif +#ifndef _BASICS_H +#define _BASICS_H + +#include +#include +#include + + + + +#define FULL_DDNNF + +class CSolverConf +{ +public: + static bool analyzeConflicts; + static bool doNonChronBackTracking; + + static bool quietMode; + + static bool allowComponentCaching; + static bool allowImplicitBCP; + + static bool allowPreProcessing; + + static unsigned int secsTimeBound; + + static unsigned int maxCacheSize; // maximum Cache Size in bytes + + static int nodeCount; // Nodes currently in use + + static bool smoothNNF; + static bool ensureAllLits; + + static bool disableDynamicDecomp; + + CSolverConf(); + + ~CSolverConf(); + +}; + +#ifdef COMPILE_FOR_GUI +#define toSTDOUT(X) +#else +#define toSTDOUT(X) if(!CSolverConf::quietMode) std::cout << X; +#endif + + +#ifdef COMPILE_FOR_GUI +#define toERROUT(X) +#else +#define toERROUT(X) if(!CSolverConf::quietMode) std::cout << X; +#endif + +#ifdef DEBUG +#define toDEBUGOUT(X) if(!CSolverConf::quietMode) cout << X; +#else +#define toDEBUGOUT(X) +#endif + + +enum SOLVER_StateT +{ + + SUCCESS, + TIMEOUT, + ABORTED +}; + +enum TriValue +{ + + F = 0, + W = 1, + X = 2 +}; + +enum DT_NodeType +{ + DT_AND, + DT_OR, + DT_LIT, + DT_TOP, + DT_BOTTOM +}; + + +extern char TriValuetoChar(TriValue v); +#endif diff --git a/src/src_sharpSAT/MainSolver/DecisionStack.h b/src/src_sharpSAT/MainSolver/DecisionStack.h index fac7221..d02b0dd 100755 --- a/src/src_sharpSAT/MainSolver/DecisionStack.h +++ b/src/src_sharpSAT/MainSolver/DecisionStack.h @@ -17,7 +17,6 @@ #include "DecisionTree.h" -using namespace std; /** \addtogroup Interna*/ /*@{*/ diff --git a/src/src_sharpSAT/MainSolver/DecisionTree.h b/src/src_sharpSAT/MainSolver/DecisionTree.h index 678f7b8..58c0446 100644 --- a/src/src_sharpSAT/MainSolver/DecisionTree.h +++ b/src/src_sharpSAT/MainSolver/DecisionTree.h @@ -33,7 +33,8 @@ #include "../Basics.h" -using namespace std; +using std::set; +using std::ostream; class CMainSolver; diff --git a/src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h b/src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h index 31a3876..416141a 100755 --- a/src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h +++ b/src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h @@ -10,7 +10,7 @@ #include "../../Basics.h" #include -using namespace std; +using std::vector; #define INVALID_DL -1 diff --git a/src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h b/src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h index 3b6e655..464b8ee 100755 --- a/src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h +++ b/src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h @@ -13,7 +13,6 @@ #include "AtomsAndNodes.h" -using namespace std; // // the identifier of the components diff --git a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp index 859525e..ebf09e1 100644 --- a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp +++ b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp @@ -5,6 +5,9 @@ #include #include +using std::ios; +using std::string; + CRunAnalyzer theRunAn; // class constructor @@ -682,13 +685,13 @@ bool CInstanceGraph::createfromFile(const char* lpstrFileName) if (clauseLen > 0) litVec.push_back(0); clauseLen = 0; - inFile.ignore(numeric_limits::max(), '\n'); // skip till next line + inFile.ignore(std::numeric_limits::max(), '\n'); // skip till next line nLine++; } else if (!isspace(firstChar)) // if whitespace, we eat it instead { // no digit (or whitespace) so we skip the line - inFile.ignore(numeric_limits::max(),'\n'); + inFile.ignore(std::numeric_limits::max(),'\n'); nLine++; } } diff --git a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h index 9c142e5..159aeab 100644 --- a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h +++ b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h @@ -8,7 +8,6 @@ #include #endif -using namespace std; #include diff --git a/src/src_sharpSAT/MainSolver/MainSolver.cpp b/src/src_sharpSAT/MainSolver/MainSolver.cpp index d087259..7103029 100755 --- a/src/src_sharpSAT/MainSolver/MainSolver.cpp +++ b/src/src_sharpSAT/MainSolver/MainSolver.cpp @@ -136,14 +136,14 @@ void CMainSolver::solve(const char *lpstrFileName) // We compress the tree now that the search is finished decStack.top().getDTNode()->uncheck(2); - cout << "Uncompressed Edges: " << decStack.top().getDTNode()->count(true) << endl; + std::cout << "Uncompressed Edges: " << decStack.top().getDTNode()->count(true) << endl; decStack.top().getDTNode()->uncheck(3); decStack.top().getDTNode()->compressNode(); decStack.top().getDTNode()->uncheck(4); bdg_edge_count = decStack.top().getDTNode()->count(true); - cout << "Compressed Edges: " << bdg_edge_count << endl; + std::cout << "Compressed Edges: " << bdg_edge_count << endl; // There may have been some translation done during the file parsing // phase, so we translate the bdg literals back. diff --git a/src/src_sharpSAT/MainSolver/MainSolver.h b/src/src_sharpSAT/MainSolver/MainSolver.h index a3eaf15..4c94549 100644 --- a/src/src_sharpSAT/MainSolver/MainSolver.h +++ b/src/src_sharpSAT/MainSolver/MainSolver.h @@ -19,6 +19,10 @@ * sollten. */ +using std::pair; +using std::vector; +using std::queue; + /*@{*/ typedef unsigned char viewStateT; From b028b6105a7e83b613cbad8d005c385752adca58 Mon Sep 17 00:00:00 2001 From: VincentDerk Date: Sat, 23 Apr 2022 14:21:40 +0200 Subject: [PATCH 20/30] Turned DT_NodeType enum into enum class + renamed enum values The enum values used full caps which caused collisions with macros from windows.h. Followed the style advice of https://google.github.io/styleguide/cppguide.html#Enumerator_Names to use 'k' followed by camel casing. --- src/src_sharpSAT/Basics.h | 15 ++- src/src_sharpSAT/MainSolver/DecisionStack.cpp | 6 +- src/src_sharpSAT/MainSolver/DecisionTree.cpp | 112 +++++++++--------- src/src_sharpSAT/MainSolver/DecisionTree.h | 4 +- src/src_sharpSAT/MainSolver/MainSolver.cpp | 24 ++-- src/src_sharpSAT/MainSolver/MainSolver.h | 20 ++-- 6 files changed, 92 insertions(+), 89 deletions(-) diff --git a/src/src_sharpSAT/Basics.h b/src/src_sharpSAT/Basics.h index 2becd18..5cf1b47 100755 --- a/src/src_sharpSAT/Basics.h +++ b/src/src_sharpSAT/Basics.h @@ -76,13 +76,16 @@ enum TriValue X = 2 }; -enum DT_NodeType +// Note: do not use full capital for enum values +// otherwise DT_BOTTOM/DT_TOP/.. collide with windows.h macros. +// https://google.github.io/styleguide/cppguide.html#Enumerator_Names +enum class DT_NodeType { - DT_AND, - DT_OR, - DT_LIT, - DT_TOP, - DT_BOTTOM + kDTAnd, + kDTOr, + kDTLit, + kDTTop, + kDTBottom }; diff --git a/src/src_sharpSAT/MainSolver/DecisionStack.cpp b/src/src_sharpSAT/MainSolver/DecisionStack.cpp index 2c45ff7..4418399 100755 --- a/src/src_sharpSAT/MainSolver/DecisionStack.cpp +++ b/src/src_sharpSAT/MainSolver/DecisionStack.cpp @@ -86,9 +86,9 @@ void CDecisionStack::init(unsigned int resSize) allComponentsStack.push_back(new CComponentId()); // initialize the stack to contain at least level zero - DTNode * dummyLeft = new DTNode(DT_AND, 2); - DTNode * dummyRight = new DTNode(DT_AND, 1); - dtMain = new DTNode(DT_AND, 0); + DTNode * dummyLeft = new DTNode(DT_NodeType::kDTAnd, 2); + DTNode * dummyRight = new DTNode(DT_NodeType::kDTAnd, 1); + dtMain = new DTNode(DT_NodeType::kDTAnd, 0); dummyLeft->addParent(dtMain, true); dummyRight->addParent(dtMain, true); diff --git a/src/src_sharpSAT/MainSolver/DecisionTree.cpp b/src/src_sharpSAT/MainSolver/DecisionTree.cpp index 389c109..29ab81a 100644 --- a/src/src_sharpSAT/MainSolver/DecisionTree.cpp +++ b/src/src_sharpSAT/MainSolver/DecisionTree.cpp @@ -92,34 +92,34 @@ int DTNode::getVal() bool DTNode::isBottom() { - return type == DT_BOTTOM; + return type == DT_NodeType::kDTBottom; } bool DTNode::isTop() { - return type == DT_TOP; + return type == DT_NodeType::kDTTop; } bool DTNode::isValid() { - return ((type == DT_TOP) || (type == DT_BOTTOM) || (type == DT_LIT) - || (type == DT_AND) || (type == DT_OR)); + return ((type == DT_NodeType::kDTTop) || (type == DT_NodeType::kDTBottom) || (type == DT_NodeType::kDTLit) + || (type == DT_NodeType::kDTAnd) || (type == DT_NodeType::kDTOr)); } void DTNode::topIfy() { - if (DT_LIT == type) - toSTDOUT("Warning: Converting DT_LIT to DT_TOP!!" << endl); + if (DT_NodeType::kDTLit == type) + toSTDOUT("Warning: Converting kDTLit to kDTTop!!" << endl); - type = DT_TOP; + type = DT_NodeType::kDTTop; } void DTNode::botIfy() { - if (DT_LIT == type) - toSTDOUT("Warning: Converting DT_LIT to DT_BOTTOM!!" << endl); + if (DT_NodeType::kDTLit == type) + toSTDOUT("Warning: Converting kDTLit to kDTBottom!!" << endl); - type = DT_BOTTOM; + type = DT_NodeType::kDTBottom; } // Add parent @@ -201,7 +201,7 @@ void DTNode::compressNode() switch (type) { - case DT_AND: + case DT_NodeType::kDTAnd: // First we recurse for (it = children.begin(); it != children.end(); it++) { @@ -222,12 +222,12 @@ void DTNode::compressNode() { (*it)->parentDeleted(this); - if ((0 == (*it)->numParents()) && ((*it)->getType() != DT_LIT)) + if ((0 == (*it)->numParents()) && ((*it)->getType() != DT_NodeType::kDTLit)) delete *it; } children.clear(); - type = DT_TOP; + type = DT_NodeType::kDTTop; return; } @@ -252,7 +252,7 @@ void DTNode::compressNode() // Get rid of the oldNode if this was the only parent if ((0 == oldNode->numParents()) && (oldNode->getType() - != DT_LIT)) + != DT_NodeType::kDTLit)) { delete oldNode; } @@ -263,7 +263,7 @@ void DTNode::compressNode() // Now we check if a False child exists (which falsifies this node) for (it = children.begin(); it != children.end(); it++) { - if (DT_BOTTOM == (*it)->getType()) + if (DT_NodeType::kDTBottom == (*it)->getType()) { // Remove the children for (it2 = children.begin(); it2 != children.end(); it2++) @@ -271,12 +271,12 @@ void DTNode::compressNode() (*it2)->parentDeleted(this); if ((0 == (*it2)->numParents()) && ((*it2)->getType() - != DT_LIT)) + != DT_NodeType::kDTLit)) delete *it2; } children.clear(); - type = DT_BOTTOM; + type = DT_NodeType::kDTBottom; return; } } @@ -290,8 +290,8 @@ void DTNode::compressNode() { if (0 == (*it)->numChildren()) { - if ((DT_AND == (*it)->getType()) || (DT_OR - == (*it)->getType())) + if ((DT_NodeType::kDTAnd == (*it)->getType()) || (DT_NodeType::kDTOr + == (*it)->getType())) { found = true; @@ -299,7 +299,7 @@ void DTNode::compressNode() childDeleted(*it); if ((0 == (*it)->numParents()) && ((*it)->getType() - != DT_LIT)) + != DT_NodeType::kDTLit)) delete *it; } } @@ -313,7 +313,7 @@ void DTNode::compressNode() found = false; for (it = children.begin(); it != children.end() && !found; it++) { - if (DT_TOP == (*it)->getType()) + if (DT_NodeType::kDTTop == (*it)->getType()) { found = true; @@ -321,7 +321,7 @@ void DTNode::compressNode() childDeleted(*it); if ((0 == (*it)->numParents()) && ((*it)->getType() - != DT_LIT)) + != DT_NodeType::kDTLit)) delete *it; } } @@ -334,7 +334,7 @@ void DTNode::compressNode() found = false; for (it = children.begin(); it != children.end() && !found; it++) { - if (DT_AND == (*it)->getType()) + if (DT_NodeType::kDTAnd == (*it)->getType()) { DTNode * oldNode = (*it); @@ -355,7 +355,7 @@ void DTNode::compressNode() // Remove oldNode if it no longer has a parent if ((0 == oldNode->numParents()) && (oldNode->getType() - != DT_LIT)) + != DT_NodeType::kDTLit)) delete oldNode; // Mark as found @@ -364,7 +364,7 @@ void DTNode::compressNode() } } break; - case DT_OR: + case DT_NodeType::kDTOr: // First we recurse for (it = children.begin(); it != children.end(); it++) @@ -385,11 +385,11 @@ void DTNode::compressNode() for (it = children.begin(); it != children.end(); it++) { (*it)->parentDeleted(this); - if ((0 == (*it)->numParents()) && ((*it)->getType() != DT_LIT)) + if ((0 == (*it)->numParents()) && ((*it)->getType() != DT_NodeType::kDTLit)) delete *it; } children.clear(); - type = DT_BOTTOM; + type = DT_NodeType::kDTBottom; return; } @@ -415,7 +415,7 @@ void DTNode::compressNode() // Get rid of the oldNode if this was the only parent if ((0 == oldNode->numParents()) && (oldNode->getType() - != DT_LIT)) + != DT_NodeType::kDTLit)) { delete oldNode; } @@ -426,18 +426,18 @@ void DTNode::compressNode() // Now we check if a True child exists (which trivializes this node) for (it = children.begin(); it != children.end(); it++) { - if (DT_TOP == (*it)->getType()) + if (DT_NodeType::kDTTop == (*it)->getType()) { // Remove the children for (it2 = children.begin(); it2 != children.end(); it2++) { (*it2)->parentDeleted(this); if ((0 == (*it2)->numParents()) && ((*it2)->getType() - != DT_LIT)) + != DT_NodeType::kDTLit)) delete *it2; } children.clear(); - type = DT_TOP; + type = DT_NodeType::kDTTop; return; } } @@ -451,8 +451,8 @@ void DTNode::compressNode() { if (0 == (*it)->numChildren()) { - if ((DT_AND == (*it)->getType()) || (DT_OR - == (*it)->getType())) + if ((DT_NodeType::kDTAnd == (*it)->getType()) || (DT_NodeType::kDTOr + == (*it)->getType())) { found = true; @@ -460,7 +460,7 @@ void DTNode::compressNode() childDeleted(*it); if ((0 == (*it)->numParents()) && ((*it)->getType() - != DT_LIT)) + != DT_NodeType::kDTLit)) delete *it; } } @@ -474,7 +474,7 @@ void DTNode::compressNode() found = false; for (it = children.begin(); it != children.end() && !found; it++) { - if (DT_BOTTOM == (*it)->getType()) + if (DT_NodeType::kDTBottom == (*it)->getType()) { found = true; @@ -482,7 +482,7 @@ void DTNode::compressNode() childDeleted(*it); if ((0 == (*it)->numParents()) && ((*it)->getType() - != DT_LIT)) + != DT_NodeType::kDTLit)) delete *it; } } @@ -495,7 +495,7 @@ void DTNode::compressNode() found = false; for (it = children.begin(); it != children.end() && !found; it++) { - if (DT_OR == (*it)->getType()) + if (DT_NodeType::kDTOr == (*it)->getType()) { DTNode * oldNode = (*it); oldNode->parentDeleted(this); @@ -515,7 +515,7 @@ void DTNode::compressNode() // Remove oldNode if it no longer has a parent if ((0 == oldNode->numParents()) && (oldNode->getType() - != DT_LIT)) + != DT_NodeType::kDTLit)) delete oldNode; // Mark as found @@ -529,7 +529,7 @@ void DTNode::compressNode() set litChildren; found = false; for (it = children.begin(); it != children.end(); it++) { - if (DT_LIT == (*it)->getType()) { + if (DT_NodeType::kDTLit == (*it)->getType()) { if (litChildren.find(-1 * (*it)->getVal()) != litChildren.end()) found = true; litChildren.insert((*it)->getVal()); @@ -541,9 +541,9 @@ void DTNode::compressNode() } break; /* Leaf node */ - case DT_BOTTOM: - case DT_TOP: - case DT_LIT: + case DT_NodeType::kDTBottom: + case DT_NodeType::kDTTop: + case DT_NodeType::kDTLit: default: return; } @@ -563,7 +563,7 @@ int DTNode::count(bool isRoot) // First we recurse for (it = children.begin(); it != children.end(); it++) { - if (DT_LIT == (*it)->getType()) + if (DT_NodeType::kDTLit == (*it)->getType()) { int lit_num = (*it)->getVal(); if (litsSeen.find(lit_num) == litsSeen.end()) @@ -658,8 +658,8 @@ void DTNode::reset() // Printout void DTNode::print(int depth) { - toSTDOUT("(" << id << "-" << type << ":"); - if (DT_LIT == type) + toSTDOUT("(" << id << "-" << (int) type << ":"); + if (DT_NodeType::kDTLit == type) { toSTDOUT(val); } @@ -681,13 +681,13 @@ void DTNode::prepNNF(vector * nodeList) if (nnfID != -1) return; - if (((DT_TOP == type) || (DT_BOTTOM == type)) && !(CSolverConf::smoothNNF)) + if (((DT_NodeType::kDTTop == type) || (DT_NodeType::kDTBottom == type)) && !(CSolverConf::smoothNNF)) { toSTDOUT("Error: type of DTNode is either top or bottom." << endl); return; } - if (DT_LIT != type) + if (DT_NodeType::kDTLit != type) { set::iterator it; for (it = children.begin(); it != children.end(); it++) @@ -705,13 +705,13 @@ void DTNode::prepNNF(vector * nodeList) // Output the nnf format void DTNode::genNNF(ostream & out) { - if (DT_LIT == type) + if (DT_NodeType::kDTLit == type) out << "L " << val << endl; - else if (DT_TOP == type) + else if (DT_NodeType::kDTTop == type) out << "A 0" << endl; - else if (DT_BOTTOM == type) + else if (DT_NodeType::kDTBottom == type) out << "O 0 0" << endl; - else if (DT_AND == type) + else if (DT_NodeType::kDTAnd == type) { out << "A " << children.size(); @@ -721,7 +721,7 @@ void DTNode::genNNF(ostream & out) out << endl; } - else if (DT_OR == type) + else if (DT_NodeType::kDTOr == type) { out << "O " << choiceVar << " " << children.size(); @@ -772,7 +772,7 @@ void DTNode::smooth(int &num_nodes, CMainSolver &solver, set &literals) variables.clear(); // If this is a literal, we just add the variable - if (DT_LIT == type) { + if (DT_NodeType::kDTLit == type) { int var = (val < 0) ? -1 * val : val; variables.insert(var); literals.insert(val); @@ -788,7 +788,7 @@ void DTNode::smooth(int &num_nodes, CMainSolver &solver, set &literals) } // If this is an AND node, there's nothing to do - if (DT_AND == type) + if (DT_NodeType::kDTAnd == type) return; set toAdd; @@ -800,7 +800,7 @@ void DTNode::smooth(int &num_nodes, CMainSolver &solver, set &literals) // If the counts are the same, then it is already smooth if (variables.size() != (*it)->numVariables()) { // Create the new AND child - DTNode* newAnd = new DTNode(DT_AND, num_nodes++); + DTNode* newAnd = new DTNode(DT_NodeType::kDTAnd, num_nodes++); (*it)->parentDeleted(this); @@ -816,7 +816,7 @@ void DTNode::smooth(int &num_nodes, CMainSolver &solver, set &literals) int var = *var_it; if (!((*it)->hasVariable(var))) { - DTNode* newOr = new DTNode(DT_OR, num_nodes++); + DTNode* newOr = new DTNode(DT_NodeType::kDTOr, num_nodes++); newAnd->addChild(newOr, true); newOr->addChild(solver.get_lit_node_full(var), true); newOr->addChild(solver.get_lit_node_full(-1 * var), true); diff --git a/src/src_sharpSAT/MainSolver/DecisionTree.h b/src/src_sharpSAT/MainSolver/DecisionTree.h index 58c0446..9e226d3 100644 --- a/src/src_sharpSAT/MainSolver/DecisionTree.h +++ b/src/src_sharpSAT/MainSolver/DecisionTree.h @@ -61,7 +61,7 @@ class DTNode // Constructor mainly for leaf nodes DTNode(int literal, bool lit_constructor, int CURRENT_ID) : - type(DT_LIT), val(literal), firstNode(NULL), secondNode(NULL) + type(DT_NodeType::kDTLit), val(literal), firstNode(NULL), secondNode(NULL) { id = CURRENT_ID; nnfID = -1; @@ -103,7 +103,7 @@ class DTNode if (0 == (*it)->numParents()) { // Protect against deleting a literal - if (DT_LIT != (*it)->getType()) + if (DT_NodeType::kDTLit != (*it)->getType()) delete (*it); } } diff --git a/src/src_sharpSAT/MainSolver/MainSolver.cpp b/src/src_sharpSAT/MainSolver/MainSolver.cpp index 7103029..dc76df3 100755 --- a/src/src_sharpSAT/MainSolver/MainSolver.cpp +++ b/src/src_sharpSAT/MainSolver/MainSolver.cpp @@ -165,11 +165,11 @@ void CMainSolver::solve(const char *lpstrFileName) return; // TODO: Fix an AND node to the top - if (DT_AND != decStack.top().getDTNode()->getType()) + if (DT_NodeType::kDTAnd != decStack.top().getDTNode()->getType()) toSTDOUT("Error: The top node wasn't an AND node."); // Make sure that every literal appears some place - DTNode* botNode = new DTNode(DT_AND, num_Nodes++); + DTNode* botNode = new DTNode(DT_NodeType::kDTAnd, num_Nodes++); botNode->botIfy(); for (int i = 1; i <= originalVarCount; ++i) { @@ -178,7 +178,7 @@ void CMainSolver::solve(const char *lpstrFileName) (literals.find(-1 * i) == literals.end())) { // Add an arbitrary choice between the two - DTNode* newOr = new DTNode(DT_OR, num_Nodes++); + DTNode* newOr = new DTNode(DT_NodeType::kDTOr, num_Nodes++); newOr->choiceVar = (unsigned) i; decStack.top().getDTNode()->addChild(newOr, true); newOr->addChild(new DTNode(i, true, num_Nodes++), true); @@ -186,8 +186,8 @@ void CMainSolver::solve(const char *lpstrFileName) } else if ((literals.find(i) == literals.end()) && CSolverConf::ensureAllLits) { - DTNode* newOr = new DTNode(DT_OR, num_Nodes++); - DTNode* newAnd = new DTNode(DT_AND, num_Nodes++); + DTNode* newOr = new DTNode(DT_NodeType::kDTOr, num_Nodes++); + DTNode* newAnd = new DTNode(DT_NodeType::kDTAnd, num_Nodes++); get_lit_node_full(-1 * i)->sub_parents(newOr); @@ -200,8 +200,8 @@ void CMainSolver::solve(const char *lpstrFileName) } else if ((literals.find(-1 * i) == literals.end()) && CSolverConf::ensureAllLits) { - DTNode* newOr = new DTNode(DT_OR, num_Nodes++); - DTNode* newAnd = new DTNode(DT_AND, num_Nodes++); + DTNode* newOr = new DTNode(DT_NodeType::kDTOr, num_Nodes++); + DTNode* newAnd = new DTNode(DT_NodeType::kDTAnd, num_Nodes++); get_lit_node_full(i)->sub_parents(newOr); @@ -353,9 +353,9 @@ bool CMainSolver::decide() ///////////////////////////// // Create the nodes - DTNode * newNode = new DTNode(DT_OR, num_Nodes++); - DTNode * left = new DTNode(DT_AND, num_Nodes++); - DTNode * right = new DTNode(DT_AND, num_Nodes++); + DTNode * newNode = new DTNode(DT_NodeType::kDTOr, num_Nodes++); + DTNode * left = new DTNode(DT_NodeType::kDTAnd, num_Nodes++); + DTNode * right = new DTNode(DT_NodeType::kDTAnd, num_Nodes++); DTNode * leftLit = get_lit_node(theLit.toSignedInt()); DTNode * rightLit = get_lit_node(-1 * theLit.toSignedInt()); @@ -514,7 +514,7 @@ retStateT CMainSolver::resolveConflict() int backtrackDecLev; // Since we have a conflict, we should add a bottom to the current DTNode - DTNode * newBot = new DTNode(DT_BOTTOM, num_Nodes++); + DTNode * newBot = new DTNode(DT_NodeType::kDTBottom, num_Nodes++); newBot->addParent(decStack.top().getCurrentDTNode(), true); for (vector::iterator it = theUnitClauses.begin(); it @@ -552,7 +552,7 @@ retStateT CMainSolver::resolveConflict() removeAllCachePollutions(); decStack.pop(); - newBot = new DTNode(DT_BOTTOM, num_Nodes++); + newBot = new DTNode(DT_NodeType::kDTBottom, num_Nodes++); newBot->addParent(decStack.top().getCurrentDTNode(), true); } diff --git a/src/src_sharpSAT/MainSolver/MainSolver.h b/src/src_sharpSAT/MainSolver/MainSolver.h index 4c94549..e62fc2e 100644 --- a/src/src_sharpSAT/MainSolver/MainSolver.h +++ b/src/src_sharpSAT/MainSolver/MainSolver.h @@ -93,7 +93,7 @@ class CMainSolver: public CInstanceGraph decStack.top().includeSol(rnCodedSols); theRunAn.addValue(SOLUTION, decStack.getDL()); - DTNode * newTop = new DTNode(DT_TOP, num_Nodes++); + DTNode * newTop = new DTNode(DT_NodeType::kDTTop, num_Nodes++); newTop->addParent(decStack.top().getCurrentDTNode()); } @@ -309,7 +309,7 @@ class CMainSolver: public CInstanceGraph int node_id = node->getID(); - if (DT_LIT == node->getType()) + if (DT_NodeType::kDTLit == node->getType()) { node_id = get_lit_node(node->getVal())->getID(); } @@ -339,19 +339,19 @@ class CMainSolver: public CInstanceGraph out << " [label=\""; switch (node->getType()) { - case DT_AND: + case DT_NodeType::kDTAnd: out << "AND"; break; - case DT_OR: + case DT_NodeType::kDTOr: out << "OR " << node->choiceVar; break; - case DT_BOTTOM: + case DT_NodeType::kDTBottom: out << "F"; break; - case DT_TOP: + case DT_NodeType::kDTTop: out << "T"; break; - case DT_LIT: + case DT_NodeType::kDTLit: out << node->getVal(); break; default: @@ -389,7 +389,7 @@ class CMainSolver: public CInstanceGraph { int node_id = (*it)->getID(); - if (DT_LIT == (*it)->getType()) + if (DT_NodeType::kDTLit == (*it)->getType()) { node_id = get_lit_node((*it)->getVal())->getID(); } @@ -487,7 +487,7 @@ class CMainSolver: public CInstanceGraph } // process the node - if (DT_LIT == node->getType()) + if (DT_NodeType::kDTLit == node->getType()) { if (node->getVal() < 0) { @@ -499,7 +499,7 @@ class CMainSolver: public CInstanceGraph } } - if (DT_OR == node->getType()) + if (DT_NodeType::kDTOr == node->getType()) { if (node->choiceVar) { node->choiceVar = varTranslation[node->choiceVar]; From 913e6052a032d2f50a8d4e0d7257f3b0726196af Mon Sep 17 00:00:00 2001 From: VincentDerk Date: Mon, 25 Apr 2022 13:36:30 +0200 Subject: [PATCH 21/30] changed enum class back to enum because enum class support is (only) since c++11 --- src/src_sharpSAT/Basics.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/src_sharpSAT/Basics.h b/src/src_sharpSAT/Basics.h index 5cf1b47..1f8c11a 100755 --- a/src/src_sharpSAT/Basics.h +++ b/src/src_sharpSAT/Basics.h @@ -79,7 +79,7 @@ enum TriValue // Note: do not use full capital for enum values // otherwise DT_BOTTOM/DT_TOP/.. collide with windows.h macros. // https://google.github.io/styleguide/cppguide.html#Enumerator_Names -enum class DT_NodeType +enum DT_NodeType { kDTAnd, kDTOr, From 94696db62aa10dfeeeda8801df5244cf34d7d0e1 Mon Sep 17 00:00:00 2001 From: VincentDerk Date: Tue, 26 Apr 2022 23:05:27 +0200 Subject: [PATCH 22/30] Changed datatype of memory tracking to size_t --- src/src_sharpSAT/Basics.cpp | 78 ++++++++++---------- src/src_sharpSAT/Basics.h | 2 +- src/src_sharpSAT/MainSolver/FormulaCache.cpp | 38 ++++++---- src/src_sharpSAT/MainSolver/FormulaCache.h | 9 ++- 4 files changed, 69 insertions(+), 58 deletions(-) diff --git a/src/src_sharpSAT/Basics.cpp b/src/src_sharpSAT/Basics.cpp index 3a908f6..7cbb50e 100755 --- a/src/src_sharpSAT/Basics.cpp +++ b/src/src_sharpSAT/Basics.cpp @@ -1,39 +1,39 @@ -#include "Basics.h" - - -bool CSolverConf::analyzeConflicts = true; -bool CSolverConf::doNonChronBackTracking = true; - -bool CSolverConf::allowComponentCaching = true; -bool CSolverConf::allowImplicitBCP = true; - -bool CSolverConf::allowPreProcessing = true; - -bool CSolverConf::quietMode = false; - -bool CSolverConf::smoothNNF = false; - -bool CSolverConf::ensureAllLits = true; - -bool CSolverConf::disableDynamicDecomp = false; - -unsigned int CSolverConf::secsTimeBound = 100000; - -unsigned int CSolverConf::maxCacheSize = 0; - -int CSolverConf::nodeCount = 0; - - -char TriValuetoChar(TriValue v) -{ - switch (v) - { - case W: - return '1'; - case F: - return '0'; - case X: - return '.'; - }; - return '.'; -} +#include "Basics.h" + + +bool CSolverConf::analyzeConflicts = true; +bool CSolverConf::doNonChronBackTracking = true; + +bool CSolverConf::allowComponentCaching = true; +bool CSolverConf::allowImplicitBCP = true; + +bool CSolverConf::allowPreProcessing = true; + +bool CSolverConf::quietMode = false; + +bool CSolverConf::smoothNNF = false; + +bool CSolverConf::ensureAllLits = true; + +bool CSolverConf::disableDynamicDecomp = false; + +unsigned int CSolverConf::secsTimeBound = 100000; + +size_t CSolverConf::maxCacheSize = 0; + +int CSolverConf::nodeCount = 0; + + +char TriValuetoChar(TriValue v) +{ + switch (v) + { + case W: + return '1'; + case F: + return '0'; + case X: + return '.'; + }; + return '.'; +} diff --git a/src/src_sharpSAT/Basics.h b/src/src_sharpSAT/Basics.h index 1f8c11a..baffe26 100755 --- a/src/src_sharpSAT/Basics.h +++ b/src/src_sharpSAT/Basics.h @@ -25,7 +25,7 @@ class CSolverConf static unsigned int secsTimeBound; - static unsigned int maxCacheSize; // maximum Cache Size in bytes + static size_t maxCacheSize; // maximum Cache Size in bytes static int nodeCount; // Nodes currently in use diff --git a/src/src_sharpSAT/MainSolver/FormulaCache.cpp b/src/src_sharpSAT/MainSolver/FormulaCache.cpp index d564dde..73359d4 100755 --- a/src/src_sharpSAT/MainSolver/FormulaCache.cpp +++ b/src/src_sharpSAT/MainSolver/FormulaCache.cpp @@ -1,15 +1,19 @@ #include "FormulaCache.h" -unsigned long availableMem() { +size_t availableMem() { //Implementation is platform depended #ifdef __linux__ - int pgs = getpagesize(); - long int pages = get_avphys_pages(); - return (pages * pgs) / 2; + auto pgs = getpagesize(); + auto pages = get_avphys_pages(); + return (pages * pgs); #elif __APPLE__ && __MACH__ - long pgs = sysconf(_SC_PAGE_SIZE); - long int pages = sysconf(_SC_AVPHYS_PAGES); - return page_size * pages / 2; + int mib[2]; + int64_t physical_memory; //TODO: size_t instead of int64_t? + mib[0] = CTL_HW; + mib[1] = HW_MEMSIZE; //TODO: != available memory + size_t length = sizeof(int64_t); + sysctl(mib, 2, &physical_memory, &length, NULL, 0); + return physical_memory; #elif _WIN32 // relevant documentation: // https://docs.microsoft.com/en-us/windows/win32/api/sysinfoapi/nf-sysinfoapi-globalmemorystatusex @@ -17,6 +21,10 @@ unsigned long availableMem() { statex.dwLength = sizeof(statex); GlobalMemoryStatusEx(&statex); return statex.ullAvailPhys; +#elif defined _SC_AVPHYS_PAGES && defined _SC_PAGESIZE + auto pages = sysconf (_SC_AVPHYS_PAGES); + auto pgs = sysconf (_SC_PAGESIZE); + return pages * pgs; #elif SUN_OS // This value was the previously used value for SUN_OS return 100*1024*1024; @@ -37,7 +45,7 @@ CFormulaCache::CFormulaCache() scoresDivTime = 50000; lastDivTime = 0; if (CSolverConf::maxCacheSize == 0) - CSolverConf::maxCacheSize = availableMem(); + CSolverConf::maxCacheSize = availableMem() / 2; } @@ -78,7 +86,7 @@ bool CFormulaCache::include(CComponentId &rComp, const CRealNum &val, DTNode * d //BEGIN satistics - unsigned int memU = memUsage/(10*1024*1024); + auto memU = memUsage/(10*1024*1024); memUsage += rEntry.memSize(); @@ -171,7 +179,7 @@ bool CFormulaCache::deleteEntries(CDecisionStack & rDecStack) vector::iterator it,itWrite; CCacheBucket::iterator bt; - if (memUsage < (unsigned int) ((double) 0.85* (double)CSolverConf::maxCacheSize)) return false; + if (memUsage < (size_t) (0.85 * (double) CSolverConf::maxCacheSize)) return false; // first : go through the EntryBase and mark the entries to be deleted as deleted (i.e. EMPTY for (it = beginEntries(); it != endEntries(); it++) @@ -196,7 +204,7 @@ bool CFormulaCache::deleteEntries(CDecisionStack & rDecStack) revalidateCacheLinksIn(rDecStack.getAllCompStack()); // finally: truly erase the empty entries, but keep the descendants tree consistent - long int newSZ = 0; + size_t newSZ = 0; long int SumNumOfVars= 0; CacheEntryId idOld,idNew; @@ -231,13 +239,13 @@ bool CFormulaCache::deleteEntries(CDecisionStack & rDecStack) toSTDOUT("Cache cleaned: "<>10)<< " KB remain"<> 1; // = 0.5 * maxCacheSize + if (memUsage < dbound) { minScoreBound/= 2; - if (memUsage < 0.5*dbound) scoresDivTime *= 2; + if (memUsage < (dbound >> 1)) scoresDivTime *= 2; } - else if (memUsage > (unsigned int) dbound) + else if (memUsage > dbound) { minScoreBound <<= 1; minScoreBound++; diff --git a/src/src_sharpSAT/MainSolver/FormulaCache.h b/src/src_sharpSAT/MainSolver/FormulaCache.h index 8d74f95..7c79e9c 100755 --- a/src/src_sharpSAT/MainSolver/FormulaCache.h +++ b/src/src_sharpSAT/MainSolver/FormulaCache.h @@ -28,14 +28,17 @@ #include #include #elif __APPLE__ && __MACH__ -#include +#include +#include #elif _WIN32 #include +#elif HAVE_UNISTD_H && defined _SC_AVPHYS_PAGES && defined _SC_PAGESIZE +#include #endif /** * @return Available memory in bytes */ -unsigned long availableMem(); +size_t availableMem(); typedef unsigned int CacheEntryId; @@ -210,7 +213,7 @@ class CFormulaCache unsigned int lastDivTime; /*end statistics */ - unsigned int memUsage; + size_t memUsage; //unsigned int maxMemUsage; double avgCachedSize() From 47439208c3c14b89a74641b8880b85b8c59f4758 Mon Sep 17 00:00:00 2001 From: VincentDerk Date: Wed, 18 May 2022 21:41:20 +0200 Subject: [PATCH 23/30] Finished(/fixed) availableMem implementation for mac --- src/src_sharpSAT/MainSolver/FormulaCache.cpp | 29 ++++++++++++++------ src/src_sharpSAT/MainSolver/FormulaCache.h | 3 +- 2 files changed, 21 insertions(+), 11 deletions(-) diff --git a/src/src_sharpSAT/MainSolver/FormulaCache.cpp b/src/src_sharpSAT/MainSolver/FormulaCache.cpp index 73359d4..e338d3a 100755 --- a/src/src_sharpSAT/MainSolver/FormulaCache.cpp +++ b/src/src_sharpSAT/MainSolver/FormulaCache.cpp @@ -1,5 +1,8 @@ #include "FormulaCache.h" +/** + * Available memory in bytes. + */ size_t availableMem() { //Implementation is platform depended #ifdef __linux__ @@ -7,13 +10,20 @@ size_t availableMem() { auto pages = get_avphys_pages(); return (pages * pgs); #elif __APPLE__ && __MACH__ - int mib[2]; - int64_t physical_memory; //TODO: size_t instead of int64_t? - mib[0] = CTL_HW; - mib[1] = HW_MEMSIZE; //TODO: != available memory - size_t length = sizeof(int64_t); - sysctl(mib, 2, &physical_memory, &length, NULL, 0); - return physical_memory; + // Get page size (in bytes) + vm_size_t pgs; + auto pgsStatus = host_page_size(mach_host_self(), &pgs); + // Get free memory (in pages) from host_statistics + vm_statistics_data_t vmstats; + mach_msg_type_number_t rSize = HOST_VM_INFO_COUNT; + auto vmstatsStatus = host_statistics(mach_host_self(), HOST_VM_INFO, (host_info_t) &vmstats, &rSize); + if (pgsStatus == KERN_SUCCESS && vmstatsStatus == KERN_SUCCESS) + { + return vmstats.free_count * pgs; + } else { + std::cout << "Failed to read free memory and page size, returning 100MB instead." << std::endl; + return 100*1024*1024; + } #elif _WIN32 // relevant documentation: // https://docs.microsoft.com/en-us/windows/win32/api/sysinfoapi/nf-sysinfoapi-globalmemorystatusex @@ -26,10 +36,11 @@ size_t availableMem() { auto pgs = sysconf (_SC_PAGESIZE); return pages * pgs; #elif SUN_OS - // This value was the previously used value for SUN_OS + // This value was the previously used value for SUN_OS. + // While rewriting this code, I kept it the same... return 100*1024*1024; #else - // Did not implement any availableMem() function for this OS ... + // availableMem() is yet to be implemented for this platform... #endif } diff --git a/src/src_sharpSAT/MainSolver/FormulaCache.h b/src/src_sharpSAT/MainSolver/FormulaCache.h index 7c79e9c..c6eecf4 100755 --- a/src/src_sharpSAT/MainSolver/FormulaCache.h +++ b/src/src_sharpSAT/MainSolver/FormulaCache.h @@ -28,8 +28,7 @@ #include #include #elif __APPLE__ && __MACH__ -#include -#include +#include #elif _WIN32 #include #elif HAVE_UNISTD_H && defined _SC_AVPHYS_PAGES && defined _SC_PAGESIZE From 05b0a47ca21c4377a08420297b06b106ee41eeff Mon Sep 17 00:00:00 2001 From: VincentDerk Date: Wed, 18 May 2022 21:56:03 +0200 Subject: [PATCH 24/30] Fixed bug in compressNode, causing SIGSEGV errors on mac OS 12.3 --- src/src_sharpSAT/MainSolver/DecisionTree.cpp | 35 +++++++++----------- 1 file changed, 15 insertions(+), 20 deletions(-) diff --git a/src/src_sharpSAT/MainSolver/DecisionTree.cpp b/src/src_sharpSAT/MainSolver/DecisionTree.cpp index 29ab81a..cb643d5 100644 --- a/src/src_sharpSAT/MainSolver/DecisionTree.cpp +++ b/src/src_sharpSAT/MainSolver/DecisionTree.cpp @@ -240,9 +240,6 @@ void DTNode::compressNode() { if (1 == (*it)->numChildren()) { - // Mark as found - found = true; - DTNode * oldNode = (*it); childDeleted(oldNode); @@ -253,9 +250,9 @@ void DTNode::compressNode() // Get rid of the oldNode if this was the only parent if ((0 == oldNode->numParents()) && (oldNode->getType() != DT_NodeType::kDTLit)) - { delete oldNode; - } + found = true; + break; // Note: required to prevent segfault (mac OS) } } } @@ -293,14 +290,14 @@ void DTNode::compressNode() if ((DT_NodeType::kDTAnd == (*it)->getType()) || (DT_NodeType::kDTOr == (*it)->getType())) { - found = true; - (*it)->parentDeleted(this); childDeleted(*it); if ((0 == (*it)->numParents()) && ((*it)->getType() != DT_NodeType::kDTLit)) delete *it; + found = true; + break; // Note: required to prevent segfault (mac OS) } } } @@ -315,14 +312,14 @@ void DTNode::compressNode() { if (DT_NodeType::kDTTop == (*it)->getType()) { - found = true; - (*it)->parentDeleted(this); childDeleted(*it); if ((0 == (*it)->numParents()) && ((*it)->getType() != DT_NodeType::kDTLit)) delete *it; + found = true; + break; // Note: required to prevent segfault (mac OS) } } } @@ -360,6 +357,7 @@ void DTNode::compressNode() // Mark as found found = true; + break; // Note: required to prevent segfault (mac OS) } } } @@ -402,10 +400,6 @@ void DTNode::compressNode() { if (1 == (*it)->numChildren()) { - - // Mark as found - found = true; - DTNode * oldNode = (*it); childDeleted(oldNode); @@ -416,9 +410,9 @@ void DTNode::compressNode() // Get rid of the oldNode if this was the only parent if ((0 == oldNode->numParents()) && (oldNode->getType() != DT_NodeType::kDTLit)) - { - delete oldNode; - } + delete oldNode; + found = true; + break; // Note: required to prevent segfault (mac OS) } } } @@ -454,14 +448,14 @@ void DTNode::compressNode() if ((DT_NodeType::kDTAnd == (*it)->getType()) || (DT_NodeType::kDTOr == (*it)->getType())) { - found = true; - (*it)->parentDeleted(this); childDeleted(*it); if ((0 == (*it)->numParents()) && ((*it)->getType() != DT_NodeType::kDTLit)) delete *it; + found = true; + break; // Note: required to prevent segfault (mac OS) } } } @@ -476,14 +470,14 @@ void DTNode::compressNode() { if (DT_NodeType::kDTBottom == (*it)->getType()) { - found = true; - (*it)->parentDeleted(this); childDeleted(*it); if ((0 == (*it)->numParents()) && ((*it)->getType() != DT_NodeType::kDTLit)) delete *it; + found = true; + break; // Note: required to prevent segfault (mac OS) } } } @@ -520,6 +514,7 @@ void DTNode::compressNode() // Mark as found found = true; + break; // Note: required to prevent segfault (mac OS) } } } From 38498fec2b42bac1ed3c2cac1a631a3081f1cd38 Mon Sep 17 00:00:00 2001 From: VincentDerk Date: Wed, 18 May 2022 23:01:54 +0200 Subject: [PATCH 25/30] Added missing std:: --- src/src_sharpSAT/Basics.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/src_sharpSAT/Basics.h b/src/src_sharpSAT/Basics.h index baffe26..ed88f9d 100755 --- a/src/src_sharpSAT/Basics.h +++ b/src/src_sharpSAT/Basics.h @@ -54,7 +54,7 @@ class CSolverConf #endif #ifdef DEBUG -#define toDEBUGOUT(X) if(!CSolverConf::quietMode) cout << X; +#define toDEBUGOUT(X) if(!CSolverConf::quietMode) std::cout << X; #else #define toDEBUGOUT(X) #endif From 12d8a10ce4b3e10b27a2b2f2ef3039803b8a8a0c Mon Sep 17 00:00:00 2001 From: VincentDerk Date: Fri, 20 May 2022 11:27:20 +0200 Subject: [PATCH 26/30] Bugfix: -cs overflow E.g. -cs 6000 overflowed. It is processed as integer arithmetics 6000 * 1024 * 1024, and only then assigned to size_t; but by then it already overflowed. --- src/src_sharpSAT/main.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/src_sharpSAT/main.cpp b/src/src_sharpSAT/main.cpp index 1bc678b..5f9cc3f 100644 --- a/src/src_sharpSAT/main.cpp +++ b/src/src_sharpSAT/main.cpp @@ -225,7 +225,7 @@ int main(int argc, char *argv[]) toSTDOUT("wrong parameters"< Date: Tue, 21 Jun 2022 01:53:10 +0800 Subject: [PATCH 27/30] static compilation --- Makefile_gmp | 3 +++ Makefile_nogmp | 3 +++ 2 files changed, 6 insertions(+) diff --git a/Makefile_gmp b/Makefile_gmp index 653dc4d..158a75f 100644 --- a/Makefile_gmp +++ b/Makefile_gmp @@ -96,6 +96,9 @@ first: all all: Makefile $(TARGET) +static: + make all CXXFLAGS="-pipe -O3 -w -DGMP_BIGNUM -static" LFLAGS="-static" + $(TARGET): $(OBJECTS) $(LINK) $(LFLAGS) -o $(TARGET) $(OBJECTS) $(LIBS) diff --git a/Makefile_nogmp b/Makefile_nogmp index 0ab2d8c..568206b 100644 --- a/Makefile_nogmp +++ b/Makefile_nogmp @@ -96,6 +96,9 @@ first: all all: Makefile $(TARGET) +static: + make all CXXFLAGS="-pipe -O3 -w -DGMP_BIGNUM -static" LFLAGS="-static" + $(TARGET): $(OBJECTS) $(LINK) $(LFLAGS) -o $(TARGET) $(OBJECTS) $(LIBS) From 2c77b375001275c75a513c510c46cb1edac814e9 Mon Sep 17 00:00:00 2001 From: mahi045 Date: Tue, 21 Jun 2022 02:02:11 +0800 Subject: [PATCH 28/30] oops, wrong param --- Makefile_nogmp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile_nogmp b/Makefile_nogmp index 568206b..bc4b986 100644 --- a/Makefile_nogmp +++ b/Makefile_nogmp @@ -97,7 +97,7 @@ first: all all: Makefile $(TARGET) static: - make all CXXFLAGS="-pipe -O3 -w -DGMP_BIGNUM -static" LFLAGS="-static" + make all CXXFLAGS="-pipe -O3 -w -static" LFLAGS="-static" $(TARGET): $(OBJECTS) $(LINK) $(LFLAGS) -o $(TARGET) $(OBJECTS) $(LIBS) From bd50207cb8fed8e453a867930a65481a06a15309 Mon Sep 17 00:00:00 2001 From: mahi045 Date: Tue, 21 Jun 2022 02:05:23 +0800 Subject: [PATCH 29/30] static build instruction added --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index da8b31d..9686732 100644 --- a/README.md +++ b/README.md @@ -12,6 +12,7 @@ copy the Makefile_gmp to Makefile. Otherwise, copy Makefile_nogmp to Makefile an proceed normally. To compile this version of DSHARP simply run `make` +To compile `DSHARP` statically, run `make static` ## Citing ``` From a48bbf9386b05d409a72b98de9d3f5e263c60336 Mon Sep 17 00:00:00 2001 From: mahi045 Date: Tue, 21 Jun 2022 02:06:36 +0800 Subject: [PATCH 30/30] new line --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 9686732..a9a4e2e 100644 --- a/README.md +++ b/README.md @@ -11,7 +11,8 @@ you must have the GMP library (libgmp-dev) installed. To use the version with GM copy the Makefile_gmp to Makefile. Otherwise, copy Makefile_nogmp to Makefile and proceed normally. -To compile this version of DSHARP simply run `make` +To compile this version of DSHARP simply run `make`. + To compile `DSHARP` statically, run `make static` ## Citing