From 4d0519fe3c999a427184fc58af0cf9a55cb36887 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Thu, 20 Feb 2020 13:51:51 +0100 Subject: [PATCH] Initial NPN3 finder with MUX and MAJ finder. --- src/sat/CMakeLists.txt | 1 + src/sat/sat_npn3_finder.cpp | Bin 0 -> 20510 bytes src/sat/sat_npn3_finder.h | Bin 0 -> 6314 bytes src/sat/sat_solver.h | 1 + 4 files changed, 2 insertions(+) create mode 100644 src/sat/sat_npn3_finder.cpp create mode 100644 src/sat/sat_npn3_finder.h diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt index 6f04bb7c6..a3f46e54c 100644 --- a/src/sat/CMakeLists.txt +++ b/src/sat/CMakeLists.txt @@ -26,6 +26,7 @@ z3_add_component(sat sat_lut_finder.cpp sat_model_converter.cpp sat_mus.cpp + sat_npn3_finder.cpp sat_parallel.cpp sat_prob.cpp sat_probing.cpp diff --git a/src/sat/sat_npn3_finder.cpp b/src/sat/sat_npn3_finder.cpp new file mode 100644 index 0000000000000000000000000000000000000000..dece7eeb3a62a809c779f044b9633ec9a3e50b17 GIT binary patch literal 20510 zcmeHP+in}l5$)#y`3Kqo4B3hAYd?6M1bfL1$a;efHZP7rP!wfpBg>2^tt~mLPfv1A zAC|hhr{_Y7wv2^ANHd)2uCA)CI#pdg!~gyFZnzbGjn6N`FTx0)ufppv52xWM?1z_O zFC63AR+xsHI6esX;@>EIgS%6-c^ww`+l{T*^9X(Ue}XIfI6I7VjrKRVvJ+0iL70Ks zGqiezvnN@b5h$|v7=7pXdx*1L&^koV87SYuxO03+)98Kyn#bUkBbU_3E9vcl#ssuS z;qPcS3;)93p_A!$lWC{(O zM0rNx`cmGzy>joNEol#-!C5&7KQ1+9J=yzksr3bPIDsxX6Vmu7yu09&mcY+ld`4kA zay@}|PcL-NyY(4*0!{fI<@YUcwjXs$J2?QIad;bkgJbjhX}o>{4rge^`wR3Og7r^|0;@2zD&No$hYaUXL@i+>ACGpi$Y+W+tHciOnlJLGBy zazDY@8%Q;e6ett9_&n3vPuaJ1b;wao@wi)bT$k8yq!HNBPD&j?mZB%zLPV4UN~Pr63C9iit8 zcTRAmSHFUPkMVy$TE;QvtT~^Y9o}iqDDOOs^EN7^-UcW1tW~6)g@3Op=_FdS_oY%7 z+ZA2V%gvhYm}_Se^)U*+#fRQa?TnyXYM1v;aZLA4tM=hcoD%Rzi!V4_Jh}DoioX4ZWH+E%Z9W z?B=M}hF(Hm%9*2AIa1TFJ~U3|7E`k!VI^nPaBW?r}0?^9yO z`Z#JMGb(x%tzDfaF=8xF~^KZ^KeaUhG&&!XXyx)@t)MLFz z=5fqfr-%adBXa2PirYHICZ2_G%rMEl?DGi7KLhV|EVJyL8N*4;7|K!m`%S_R7_Ylu za|Vax6Z_z5j_9=y2{=n-gp)0oSBF}!MGUV$h!ocFZ#k zW{=c-oBlY<%(fYsIp?LHzQGk)=N(uhGrTeKYs$)Okp0Xey)7Cqb~G8^#OSwJTDN5? z<80QH=_?o7#^}m}*we<(H7%d$8r`^9MKgJ>U8k@M=?|cXQoBtn8{(UD%*1PGf;L7C z<(8aVcAuBhQtAjq-1hnG_#!rNO*g?k)&_V^-%l-N``vVNH1DSD+lqE>)pd;7ji{u0 zNSRH}mzJ9AjcCbw#ciw|xng<+8IR)HM46~CRo+pvq2w3L+Bnxo(Fc-dl&g=zb7<^E z1s&=uYh`!2C6AERQo~+?lquIWVwRcnvkg8puEr@dp*k8EEt8pJvpS(Q3gxHnG+V;> zqz`&HD@Lr<(0cZwre>(-a4p$}`!=HC!z|8|`S}jUqfOGo?_l;gTB<=9GL*7e6~$<` z9ZPztrqLXSt1_7T4#8Sf4O2VdSZE`qT3IDjw|-sq|^@k;;jbh1KYr z9?Yhvm|fOs&LD+in<5(P8$)f?^H%e}Em$Ct$s#JF#dFkCUo7$DdARS+A1u#rpjEpL zO%6M@a(a^v!&JCfqTWJ5B4t(%GOxp(E?+cTXqoA&)u zMpb43m(3UwLZuq5pSgF{^@Hb)_{Z$t=MX~OGTPRC%&^bXG~BYa9x;pA4r6CO5>A(S z2pUUd0v-=rwlf9I&rl5^JPM&UpBjDYX?8u9!>cl~WhXSfFP8F=41$hElH z6^~g$+G$*UmBW1r?oTqe=UQ2Np7hw#_v$S0l;*Jzfh)^su?g8EtQs=}F`eS6Kh)^UpP zb!}Q-o9$-idM&O6x!*3-V+-!KvRbBNTdj+m>^YQ|=wSu-NkuFAU0 zwpJlZHR7};dRJZj*ld=RPI@AWwub^>(apavMOfl zjwxy(Lsk_gx6j`AG+ljX!&=+1Ue~a@$wnBtS(CPvlW-_s$&`L&RP31aljuqd@?Y(b zZbyx4m#nWAVwB&9>?x;99%(xix1ftV%X}%-v)g^z__X86(wpZ?pFq)M;b|ACu0q0qj)~%&ZsNXziD0Ol9OsDyb#_&w1CaHPa zHTXfAVUE&|C|=)nD{9JXGnpb#cb=2l2?^`t`244vo^RPj@hYkq@_g0;7QlMGS3rAW zlwd86>v?9Jqqs9XfpymAGsQ}?MB>{I=*2x~?y$>BQ}$ZsYeJIp>c^BNj_~xW;Tg{? zMRL)_DQ?8BLW;oA^KDKqDJ^kIRVp^@r-}$ufn4U0OZ{IOr)!6ejvMJfu zYI`$gb>{PR`rdLkOJ9_IEZ!`AX~t)3?}NUVVzczU<|V~y^xG>CpZ4Bp`%V1}*?Vi& zAw9~K@Au>tD#kum5~+XfDWyFoW}$rJ-`<{jTI^xvlxolABwAfq>)#>choM#i|E#z3eR0tcg<5^6zHV9+TKD=%@4Mu0)KL4X&MjKBL9RI0 zeC}U!s(14E{FApAN^F#_^DZU-LD-!UO> z@i#y8dne>f?~@QEnE?}%x{${-^*w&gSbu=BKJDm_~%pF==kSWy4yVLi0yv~ ze*~WV1HStmeE3`Z;uH6OwbRju5zH)@TU?LX0JUKI#mqZ)V`RLJ`)b8~C2LO-n> literal 0 HcmV?d00001 diff --git a/src/sat/sat_npn3_finder.h b/src/sat/sat_npn3_finder.h new file mode 100644 index 0000000000000000000000000000000000000000..7ff3070a7add82eb854acb720ffd83bd6b544e15 GIT binary patch literal 6314 zcmdT|*-jKe6ur+T{zC^6GN1^;8={H&3^DNoIz7V-jIudB5Rl-ftLIdCskJwS2Q!(e z>FT?lyVUaQ=ay{93w)l-Gb!--C>L@mx3ZAA9LtF;F*lNltYh4fZSyVU0B&| z*hG0M^SzA0u{1g-7-MM#xNf}nH8f9PK?OT%yyNrC*jzx@rqOhXcl7%M<}Zx374(zt z3L~{x-|EN`a-A4isTBvts}pcmM(1bHP30@Tl&r{Z8iY5^v+w00sF%jtRPv#G0+zeR zK8KUyvk9LzWb47wRiMiF90U6bJdDu@&F=)&&vjyJDaG${kMqRQoVW`G2 z>^$~7B+loshM8X*Jc+($eIa)bkzh6QV{NWMO)BOiv0KQSR?2+!sC<>Jqc3;O=&{oE zy^hu!ed-?15NXSkTC3cOEbDt_bT5%9d-%llwhzxQfaei9(kVt(1atXRUV?A<%(}b- zA1i=8Camoe((@QJ(-(+p`A6Ov|x z#CFEgP*X}X7TvYIpOr=}#46TQxA<$j{FUh%g~=+`(E@eZl+}tC7)!hE@Hh>mi_ zwh@Jm3_AHNQ7O!RwKLAz0ti@JVhc-HM;n`MSnset)Z0ZJVtWEyYjpQ6T-8TbP7Obg zF|y0Err0a(K7bv5g#E)PiWyf0@-2lOXK8jAZmu2G`ws6zf2Q)Sw=ZK@#UA@NK2#=V zKJx6|zL(=i@lw6lHD2SuG4$MaNX@^lc*a?%b;3;i-hp`7M~I%?LAJ*+v~PHQ#1@yZ zlh(%8aQ`~Yk}moX=clTe5T7`k{+F6*_rg|9JI&MAO}q=yh;qj{Mn9Nh_4F&7S>``; zzoI<3ckDr2^?aW4frD#{>SbhlPuHQ-s1J6-N$ z%b-4MbG~#ZvhZxcwZX6EI_a^^mXX)tJvZ7@MB4d%6s&}%&fr!Kn+J>|*Ff#Qqv*L= zZ(8S0j`Je!efgb)-ABZC)J6q9hL(>KmTGSiRInyH8oU&`t;<0H6+HIf}F zL}G#-#gjU3Di)2aXf96n1T-v4O||9ZU!zabvm=bGuM+=fnXJoK!z6q+4mHq7C0Wys~K>j!lYw9;H^ z^Cr}u=7Q7Bym@>-*oFO0%v(zCOn47wZw38x0RQLjfJW$H?iPvNt{JNzjWW1S+{t}l zk?MEV${SYRAJ~4X9igp_ZjmK3A)@XXW4VPBzCg1$McPH^VG_OK)=ud5hT@ xP7=jn&uuk6zUNJ=YtCbyg3_wV`%8O=_?tiR`}GvokKJv!nn`m|Pq{Y7eglZY#qt0E literal 0 HcmV?d00001 diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 3c76e858f..bb0b1cde3 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -220,6 +220,7 @@ namespace sat { friend class xor_finder; friend class aig_finder; friend class lut_finder; + friend class npn3_finder; public: solver(params_ref const & p, reslimit& l); ~solver() override;