IT/Description/HolBdd.tex

224 $\exists$ and the \HOL{} term parser plus \ml{termToBdd} provides a
227 \ml{HolBddLib}. However, in addition it allows FL-like BDD programming
273 \end{verbatim}\index{HolBddLib!ML bindings!{init}@\ml{init}}
313 \end{verbatim}\index{HolBddLib!ML bindings!{done}@\ml{done}}
324 \end{verbatim}\index{HolBddLib!ML bindings!{isRunning}@\ml{isRunning}}
344 \end{verbatim}\index{HolBddLib!ML bindings!{stats}@\ml{stats}}
372 \end{verbatim}\index{HolBddLib!ML bindings!{setMaxincrease}@\ml{setMaxincrease}}\index{HolBddLib!ML bindings!{setCacheratio}@\ml{setCacheratio}}
391 \end{verbatim}\index{HolBddLib!ML bindings!{fromBool}@\ml{fromBool}}\index{HolBddLib!ML bindings!{toBool}@\ml{toBool}}
398 \end{verbatim}\index{HolBddLib!ML bindings!{equal}@\ml{equal}}
415 \end{verbatim}\index{HolBddLib!ML bindings!{setVarnum}@\ml{setVarnum}}
425 \end{verbatim}\index{HolBddLib!ML bindings!{getVarnum}@\ml{getVarnum}}
434 \end{verbatim}\index{HolBddLib!ML bindings!{ithvar}@\ml{ithvar}}
441 \end{verbatim}\index{HolBddLib!ML bindings!{nithvar}@\ml{nithvar}}
463 \end{verbatim}\index{HolBddLib!ML bindings!{makese}@\ml{makese}}\index{HolBddLib!ML bindings!{scanset}@\ml{scanset}}\index{HolBddLib!ML bindings!{fromSet}@\ml{fromSet}}
474 \end{verbatim}\index{HolBddLib!ML bindings!{forall}@\ml{forall}}\index{HolBddLib!ML bindings!{exist}@\ml{exist}}
486 is a value of type \t{composeSet}\index{HolBddLib!ML bindings!{composeSet}@\ml{composeSet}}
493 \end{verbatim}\index{HolBddLib!ML bindings!{veccompose}@\ml{veccompose}}
499 \end{verbatim}\index{HolBddLib!ML bindings!{compose}@\ml{compose}}
505 an argument of type \t{pairSet}\index{HolBddLib!ML bindings!{pairSet}@\ml{pairSet}} representing sets of pairs of variables
511 \end{verbatim}\index{HolBddLib!ML bindings!{makepairSet}@\ml{makepairSet}}\index{HolBddLib!ML bindings!{replace}@\ml{replace}}
520 as argument a value of type \t{assignment}\index{HolBddLib!ML bindings!{assignment}@\ml{assignment}}
527 \end{verbatim}\index{HolBddLib!ML bindings!{restrict}@\ml{restrict}}\index{HolBddLib!ML bindings!{assignment}@\ml{assignment}}\index{HolBddLib!ML bindings!{getAssignment}@\ml{getAssignment}}
540 \end{verbatim}\index{HolBddLib!ML bindings!{makeset}@\ml{makeset}}\index{HolBddLib!ML bindings!{scanset}@\ml{scanset}}\index{HolBddLib!ML bindings!{fromSet}@\ml{fromSet}}
577 \end{verbatim}\index{HolBddLib!ML bindings!{apply}@\ml{apply}}
588 \end{verbatim}\index{HolBddLib!ML bindings!{appall}@\ml{appall}}\index{HolBddLib!ML bindings!{appex}@\ml{appex}}
601 \t{bddop}\index{HolBddLib!ML bindings!{bddop}@\ml{bddop}} & \t{bdd~*~bdd~->~bdd} & Result of applying to $(b_1,b_2)$\\ \hline\hline
602 \t{And}\index{HolBddLib!ML bindings!{And}@\ml{And}} & \t{AND} & $b_1\wedge b_2$ \\ \hline
603 \t{Nand}\index{HolBddLib!ML bindings!{Nand}@\ml{Nand}} & \t{NAND} & $\neg(b_1\wedge b_2)$ \\ \hline
604 \t{Or}\index{HolBddLib!ML bindings!{Or}@\ml{Or}}  & \t{OR} & $b_1\vee b_2$ \\ \hline
605 \t{Nor}\index{HolBddLib!ML bindings!{Nor}@\ml{Nor}} & \t{NOR} & $\neg(b_1\vee b_2)$ \\ \hline
606 \t{Biimp}\index{HolBddLib!ML bindings!{Biimp}@\ml{Biimp}} & \t{BIIMP} & $b_1= b_2$ \\ \hline
607 \t{Xor}\index{HolBddLib!ML bindings!{Xor}@\ml{Xor}} & \t{XOR} & $\neg(b_1=b_2)$ \\ \hline
608 \t{Imp}\index{HolBddLib!ML bindings!{Imp}@\ml{Imp}} & \t{IMP} & $b_1\imp b_2$ \\ \hline
609 \t{Invimp}\index{HolBddLib!ML bindings!{Invimp}@\ml{Invimp}} & \t{INVIMP} & $b_2\imp b_1$ \\ \hline
610 \t{Lessth}\index{HolBddLib!ML bindings!{Lessth}@\ml{Lessth}} & \t{LESSTH} & $\neg b_1\wedge b_2$ \\ \hline
611 \t{Diff}\index{HolBddLib!ML bindings!{Diff}@\ml{Diff}} & \t{DIFF} & $b_1\wedge \neg b_2$ \\ \hline
621 \end{verbatim}\index{HolBddLib!ML bindings!{NOT}@\ml{NOT}}\index{HolBddLib!ML bindings!{ITE}@\ml{ITE}}
639 \end{verbatim}\index{HolBddLib!ML bindings!{var}@\ml{var}}\index{HolBddLib!ML bindings!{high}@\ml{high}}\index{HolBddLib!ML bindings!{low}@\ml{low}}
653 \end{verbatim}\index{HolBddLib!ML bindings!{nodetable}@\ml{nodetable}}
669 \end{verbatim}\index{HolBddLib!ML bindings!{nodecount}@\ml{nodecount}}
688 \end{verbatim}\index{HolBddLib!ML bindings!{satcount}@\ml{satcount}}
698 \end{verbatim}\index{HolBddLib!ML bindings!{support}@\ml{support}}
708 \end{verbatim}\index{HolBddLib!ML bindings!{statecount}@\ml{statecount}}
737 \end{verbatim}\index{HolBddLib!ML bindings!{simplify}@\ml{simplify}}
761 \end{verbatim}\index{HolBddLib!ML bindings!{bddSave}@\ml{bddSave}}\index{HolBddLib!ML bindings!{bddLoad}@\ml{bddLoad}}
774 \end{verbatim}\index{HolBddLib!ML bindings!{hash}@\ml{hash}}
785 \end{verbatim}\index{HolBddLib!ML bindings!{printset}@\ml{printset}}\index{HolBddLib!ML bindings!{printdot}@\ml{printdot}}\index{HolBddLib!ML bindings!{fnprintset}@\ml{fnprintset}}\index{HolBddLib!ML bindings!{fnprintdot}@\ml{fnprintdot}}
972 \end{verbatim}\index{HolBddLib!ML bindings!{verbosegc}@\ml{verbosegc}}
1024 \subsection{The structure \ml{Varmap}}\label{Varmap}\index{HolBddLib!termbdd@\ml{term\_bdd}!varmaps}
1032 \end{verbatim}\index{HolBddLib!ML bindings!{varmap}@\ml{varmap}}
1052 \index{HolBddLib!ML bindings!{Varmap.empty}@\ml{Varmap.empty}}
1053 \index{HolBddLib!ML bindings!{Varmap.insert}@\ml{Varmap.insert}}
1054 \index{HolBddLib!ML bindings!{Varmap.remove}@\ml{Varmap.remove}}
1055 \index{HolBddLib!ML bindings!{Varmap.peek}@\ml{Varmap.peek}}
1056 \index{HolBddLib!ML bindings!{Varmap.dest}@\ml{Varmap.dest}}
1057 \index{HolBddLib!ML bindings!{Varmap.eq}@\ml{Varmap.eq}}
1058 \index{HolBddLib!ML bindings!{Varmap.size}@\ml{Varmap.size}}
1059 \index{HolBddLib!ML bindings!{Varmap.extends}@\ml{Varmap.extends}}
1060 \index{HolBddLib!ML bindings!{Varmap.unify}@\ml{Varmap.unify}}
1078 \subsection{The structure \ml{PrintBdd}}\label{PrintBdd}\index{HolBddLib!termbdd@\ml{term\_bdd}!printing}
1088 \index{HolBddLib!ML bindings!{dotBdd}@\ml{dotBdd}}
1089 \index{HolBddLib!ML bindings!{dotLabelledTermBdd}@\ml{dotLabelledTermBdd}}
1090 \index{HolBddLib!ML bindings!{dotTermBdd}@\ml{dotTermBdd}}
1116 \subsection{The structure \t{PrimitiveBddRules}}\label{PrimitiveBddRules}\index{HolBddLib!termbdd@\ml{term\_bdd}!primitive rules}
1118 The structure \ml{PrimitiveBddRules} defines the type \termbddty{} by
1125 \end{verbatim}\index{HolBddLib!ML bindings!termbdd@\ml{term\_bdd}}\index{HolBddLib!ML bindings!{assums}@\ml{assums}}
1160 from the representation judgement \termbdd{a}{\rho}{t}{\ml{TRUE}}
1224 \fbox{\usebox{\BddExtendVarmap}}\index{HolBddLib!ML bindings!{BddExtendVarmap}@\ml{BddExtendVarmap}}
1254 \fbox{\usebox{\BddFreevarsContractVarmap}}\index{HolBddLib!ML bindings!{BddFreevarsContractVarmap}@\ml{BddFreevarsContractVarmap}}
1286 \fbox{\usebox{\BddSupportContractVarmap}}\index{HolBddLib!ML bindings!{BddSupportContractVarmap}@\ml{BddSupportContractVarmap}}
1328 \fbox{\usebox{\BddVar}}\index{HolBddLib!ML bindings!{BddVar}@\ml{BddVar}}
1368 \fbox{\usebox{\BddCon}}\index{HolBddLib!ML bindings!{BddCon}@\ml{BddCon}}
1400 \fbox{\usebox{\BddNot}}\index{HolBddLib!ML bindings!{BddNot}@\ml{BddNot}}
1431 \fbox{\usebox{\BddIte}}\index{HolBddLib!ML bindings!{BddIte}@\ml{BddIte}}
1466 \fbox{\usebox{\BddOp}}\index{HolBddLib!ML bindings!{BddOp}@\ml{BddOp}}
1500 \fbox{\usebox{\BddForall}}\index{HolBddLib!ML bindings!{BddForall}@\ml{BddForall}}
1534 \fbox{\usebox{\BddExists}}\index{HolBddLib!ML bindings!{BddExists}@\ml{BddExists}}
1576 \fbox{\usebox{\BddAppall}}\index{HolBddLib!ML bindings!{BddAppall}@\ml{BddAppall}}
1619 \fbox{\usebox{\BddAppex}}\index{HolBddLib!ML bindings!{BddAppex}@\ml{BddAppex}}
1655 \fbox{\usebox{\BddCompose}}\index{HolBddLib!ML bindings!{BddCompose}@\ml{BddCompose}}
1697 \fbox{\usebox{\BddListCompose}}\index{HolBddLib!ML bindings!{BddListCompose}@\ml{BddListCompose}}
1744 \fbox{\usebox{\BddRestrict}}\index{HolBddLib!ML bindings!{BddRestrict}@\ml{BddRestrict}}
1788 \fbox{\usebox{\BddReplace}}\index{HolBddLib!ML bindings!{BddReplace}@\ml{BddReplace}}
1821 \fbox{\usebox{\BddSimplify}}\index{HolBddLib!ML bindings!{BddSimplify}@\ml{BddSimplify}}
1858 \fbox{\usebox{\BddFindModel}}\index{HolBddLib!ML bindings!{BddFindModel}@\ml{BddFindModel}}
1860 \subsection{Linking representation judgements to theorems}\label{oracle}\index{HolBddLib!termbdd@\ml{term\_bdd}!linking to theorems}
1875 \termbdd{a}{\rho}{t}{\ml{TRUE}}
1889 \fbox{\usebox{\BddThmOracle}}\index{HolBddLib!ML bindings!{BddThmOracle}@\ml{BddThmOracle}}
1922 \fbox{\usebox{\BddEqMp}}\index{HolBddLib!ML bindings!{BddEqMp}@\ml{BddEqMp}}
1957 \fbox{\usebox{\destructors}}\index{HolBddLib!termbdd@\ml{term\_bdd}!destructors}
1977 \fbox{\usebox{\inSupport}}\index{HolBddLib!ML bindings!{inSupport}@\ml{inSupport}}
2015 \fbox{\usebox{\termApply}}\index{HolBddLib!ML bindings!{termApply}@\ml{termApply}}
2017 \subsection{The structure \t{DerivedBddRules}}\label{DerivedBddRules}\index{HolBddLib!termbdd@\ml{term\_bdd}!derived rules}
2029 \fbox{\usebox{\extendVarmap}}\index{HolBddLib!ML bindings!{extendVarmap}@\ml{extendVarmap}}
2038 \fbox{\usebox{\globalvarmap}}\index{HolBddLib!ML bindings!{global\_varmap}@\ml{global\_varmap}}
2048 \fbox{\usebox{\BddEqualTest}}\index{HolBddLib!ML bindings!{BddEqualTest}@\ml{BddEqualTest}}
2056 \fbox{\usebox{\isTRUE}}\index{HolBddLib!ML bindings!{isTRUE}@\ml{isTRUE}}
2064 \fbox{\usebox{\isFALSE}}\index{HolBddLib!ML bindings!{isFALSE}@\ml{isFALSE}}
2074 \fbox{\usebox{\GenTermToTermBdd}}\index{HolBddLib!ML bindings!{GenTermToTermBdd}@\ml{GenTermToTermBdd}}
2082 \fbox{\usebox{\failfn}}\index{HolBddLib!ML bindings!{failfn}@\ml{failfn}}
2090 \fbox{\usebox{\bddToTerm}}\index{HolBddLib!ML bindings!{bddToTerm}@\ml{bddToTerm}}
2098 \fbox{\usebox{\termToTermBdd}}\index{HolBddLib!ML bindings!{termToTermBdd}@\ml{termToTermBdd}}
2105 \fbox{\usebox{\destBddOp}}\index{HolBddLib!ML bindings!{dest\_BddOp}@\ml{dest\_BddOp}}
2116 \fbox{\usebox{\TermBddToEqThm}}\index{HolBddLib!ML bindings!{TermBddToEqThm}@\ml{TermBddToEqThm}}
2125 \fbox{\usebox{\BddRhsOracle}}\index{HolBddLib!ML bindings!{BddRhsOracle}@\ml{BddRhsOracle}}
2138 \fbox{\usebox{\findModel}}\index{HolBddLib!ML bindings!{findModel}@\ml{findModel}}
2150 \fbox{\usebox{\BddApThm}}\index{HolBddLib!ML bindings!{BddApThm}@\ml{BddApThm}}
2160 \fbox{\usebox{\BddApReplace}}\index{HolBddLib!ML bindings!{BddApReplace}@\ml{BddApReplace}}
2170 \fbox{\usebox{\BddApRestrict}}\index{HolBddLib!ML bindings!{BddApRestrict}@\ml{BddApRestrict}}
2193 \fbox{\usebox{\BddSubst}}\index{HolBddLib!ML bindings!{BddSubst}@\ml{BddSubst}}
2203 \fbox{\usebox{\BddApSubst}}\index{HolBddLib!ML bindings!{BddApSubst}@\ml{BddApSubst}}
2213 \fbox{\usebox{\eqToTermBdd}}\index{HolBddLib!ML bindings!{eqToTermBdd}@\ml{eqToTermBdd}}
2222 \fbox{\usebox{\BddApConv}}\index{HolBddLib!ML bindings!{BddApConv}@\ml{BddApConv}}
2243 \fbox{\usebox{\BddSatone}}\index{HolBddLib!ML bindings!{BddSatone}@\ml{BddSatone}}
2262 \fbox{\usebox{\computeFixedpoint}}\index{HolBddLib!ML bindings!{computeFixedpoint}@\ml{computeFixedpoint}}
2273 \fbox{\usebox{\computeTrace}}\index{HolBddLib!ML bindings!{computeTrace}@\ml{computeTrace}}
2288 \fbox{\usebox{\findTrace}}\index{HolBddLib!ML bindings!{findTrace}@\ml{findTrace}}
2296 \fbox{\usebox{\MakeSimpRecThm}}\index{HolBddLib!ML bindings!{MakeSimpRecThm}@\ml{MakeSimpRecThm}}