diff --git a/configure b/configure
index 4ab8a9ba7..eb5c7d141 100755
--- a/configure
+++ b/configure
@@ -8301,374 +8301,13 @@ if test ! "$yap_cv_cplint" = "no"
LDFLAGS=${LDFLAGS}" `echo $GLIBS | awk '{print $1}'` -L$prefix/lib/"
if test ! "$yap_cv_cplint" = "yes"
then
- LDFLAGS+=" -L${yap_cv_cplint}/lib"
- CPLINT_LDFLAGS+=" -L${yap_cv_cplint}/lib"
+ CPLINT_LDFLAGS+=" -L${yap_cv_cplint}/cudd -L${yap_cv_cplint}/mtr -L${yap_cv_cplint}/st -L${yap_cv_cplint}/util -L${yap_cv_cplint}/epd "
CPLINT_CFLAGS+=" -I${yap_cv_cplint}/include"
+ CPLINT_LIBS="-lcudd -lmtr -lst -lutil -lepd -lm "$CPLINT_LIBS
fi
- { $as_echo "$as_me:$LINENO: checking for library containing g_hash_table_new" >&5
-$as_echo_n "checking for library containing g_hash_table_new... " >&6; }
-if test "${ac_cv_search_g_hash_table_new+set}" = set; then
- $as_echo_n "(cached) " >&6
-else
- ac_func_search_save_LIBS=$LIBS
-cat >conftest.$ac_ext <<_ACEOF
-/* confdefs.h. */
-_ACEOF
-cat confdefs.h >>conftest.$ac_ext
-cat >>conftest.$ac_ext <<_ACEOF
-/* end confdefs.h. */
-
-/* Override any GCC internal prototype to avoid an error.
- Use char because int might match the return type of a GCC
- builtin and then its argument prototype would still apply. */
-#ifdef __cplusplus
-extern "C"
-#endif
-char g_hash_table_new ();
-int
-main ()
-{
-return g_hash_table_new ();
- ;
- return 0;
-}
-_ACEOF
-for ac_lib in '' glib-2.0; do
- if test -z "$ac_lib"; then
- ac_res="none required"
- else
- ac_res=-l$ac_lib
- LIBS="-l$ac_lib $ac_func_search_save_LIBS"
- fi
- rm -f conftest.$ac_objext conftest$ac_exeext
-if { (ac_try="$ac_link"
-case "(($ac_try" in
- *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
- *) ac_try_echo=$ac_try;;
-esac
-eval ac_try_echo="\"\$as_me:$LINENO: $ac_try_echo\""
-$as_echo "$ac_try_echo") >&5
- (eval "$ac_link") 2>conftest.er1
- ac_status=$?
- grep -v '^ *+' conftest.er1 >conftest.err
- rm -f conftest.er1
- cat conftest.err >&5
- $as_echo "$as_me:$LINENO: \$? = $ac_status" >&5
- (exit $ac_status); } && {
- test -z "$ac_c_werror_flag" ||
- test ! -s conftest.err
- } && test -s conftest$ac_exeext && {
- test "$cross_compiling" = yes ||
- $as_test_x conftest$ac_exeext
- }; then
- ac_cv_search_g_hash_table_new=$ac_res
-else
- $as_echo "$as_me: failed program was:" >&5
-sed 's/^/| /' conftest.$ac_ext >&5
-
-
-fi
-
-rm -rf conftest.dSYM
-rm -f core conftest.err conftest.$ac_objext conftest_ipa8_conftest.oo \
- conftest$ac_exeext
- if test "${ac_cv_search_g_hash_table_new+set}" = set; then
- break
-fi
-done
-if test "${ac_cv_search_g_hash_table_new+set}" = set; then
- :
-else
- ac_cv_search_g_hash_table_new=no
-fi
-rm conftest.$ac_ext
-LIBS=$ac_func_search_save_LIBS
-fi
-{ $as_echo "$as_me:$LINENO: result: $ac_cv_search_g_hash_table_new" >&5
-$as_echo "$ac_cv_search_g_hash_table_new" >&6; }
-ac_res=$ac_cv_search_g_hash_table_new
-if test "$ac_res" != no; then
- test "$ac_res" = "none required" || LIBS="$ac_res $LIBS"
- CPLINT_LIBS="-lglib-2.0 "
-else
- { { $as_echo "$as_me:$LINENO: error: This package needs glib >=2.0." >&5
-$as_echo "$as_me: error: This package needs glib >=2.0." >&2;}
- { (exit 1); exit 1; }; }
-fi
-
- { $as_echo "$as_me:$LINENO: checking for library containing array_do_alloc" >&5
-$as_echo_n "checking for library containing array_do_alloc... " >&6; }
-if test "${ac_cv_search_array_do_alloc+set}" = set; then
- $as_echo_n "(cached) " >&6
-else
- ac_func_search_save_LIBS=$LIBS
-cat >conftest.$ac_ext <<_ACEOF
-/* confdefs.h. */
-_ACEOF
-cat confdefs.h >>conftest.$ac_ext
-cat >>conftest.$ac_ext <<_ACEOF
-/* end confdefs.h. */
-
-/* Override any GCC internal prototype to avoid an error.
- Use char because int might match the return type of a GCC
- builtin and then its argument prototype would still apply. */
-#ifdef __cplusplus
-extern "C"
-#endif
-char array_do_alloc ();
-int
-main ()
-{
-return array_do_alloc ();
- ;
- return 0;
-}
-_ACEOF
-for ac_lib in '' glu; do
- if test -z "$ac_lib"; then
- ac_res="none required"
- else
- ac_res=-l$ac_lib
- LIBS="-l$ac_lib $ac_func_search_save_LIBS"
- fi
- rm -f conftest.$ac_objext conftest$ac_exeext
-if { (ac_try="$ac_link"
-case "(($ac_try" in
- *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
- *) ac_try_echo=$ac_try;;
-esac
-eval ac_try_echo="\"\$as_me:$LINENO: $ac_try_echo\""
-$as_echo "$ac_try_echo") >&5
- (eval "$ac_link") 2>conftest.er1
- ac_status=$?
- grep -v '^ *+' conftest.er1 >conftest.err
- rm -f conftest.er1
- cat conftest.err >&5
- $as_echo "$as_me:$LINENO: \$? = $ac_status" >&5
- (exit $ac_status); } && {
- test -z "$ac_c_werror_flag" ||
- test ! -s conftest.err
- } && test -s conftest$ac_exeext && {
- test "$cross_compiling" = yes ||
- $as_test_x conftest$ac_exeext
- }; then
- ac_cv_search_array_do_alloc=$ac_res
-else
- $as_echo "$as_me: failed program was:" >&5
-sed 's/^/| /' conftest.$ac_ext >&5
-
-
-fi
-
-rm -rf conftest.dSYM
-rm -f core conftest.err conftest.$ac_objext conftest_ipa8_conftest.oo \
- conftest$ac_exeext
- if test "${ac_cv_search_array_do_alloc+set}" = set; then
- break
-fi
-done
-if test "${ac_cv_search_array_do_alloc+set}" = set; then
- :
-else
- ac_cv_search_array_do_alloc=no
-fi
-rm conftest.$ac_ext
-LIBS=$ac_func_search_save_LIBS
-fi
-{ $as_echo "$as_me:$LINENO: result: $ac_cv_search_array_do_alloc" >&5
-$as_echo "$ac_cv_search_array_do_alloc" >&6; }
-ac_res=$ac_cv_search_array_do_alloc
-if test "$ac_res" != no; then
- test "$ac_res" = "none required" || LIBS="$ac_res $LIBS"
- CPLINT_LIBS="-lglu "$CPLINT_LIBS
-else
- { { $as_echo "$as_me:$LINENO: error: This package needs glu." >&5
-$as_echo "$as_me: error: This package needs glu." >&2;}
- { (exit 1); exit 1; }; }
-fi
-
- { $as_echo "$as_me:$LINENO: checking for library containing Cudd_Init" >&5
-$as_echo_n "checking for library containing Cudd_Init... " >&6; }
-if test "${ac_cv_search_Cudd_Init+set}" = set; then
- $as_echo_n "(cached) " >&6
-else
- ac_func_search_save_LIBS=$LIBS
-cat >conftest.$ac_ext <<_ACEOF
-/* confdefs.h. */
-_ACEOF
-cat confdefs.h >>conftest.$ac_ext
-cat >>conftest.$ac_ext <<_ACEOF
-/* end confdefs.h. */
-
-/* Override any GCC internal prototype to avoid an error.
- Use char because int might match the return type of a GCC
- builtin and then its argument prototype would still apply. */
-#ifdef __cplusplus
-extern "C"
-#endif
-char Cudd_Init ();
-int
-main ()
-{
-return Cudd_Init ();
- ;
- return 0;
-}
-_ACEOF
-for ac_lib in '' cu; do
- if test -z "$ac_lib"; then
- ac_res="none required"
- else
- ac_res=-l$ac_lib
- LIBS="-l$ac_lib -lglu -lm $ac_func_search_save_LIBS"
- fi
- rm -f conftest.$ac_objext conftest$ac_exeext
-if { (ac_try="$ac_link"
-case "(($ac_try" in
- *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
- *) ac_try_echo=$ac_try;;
-esac
-eval ac_try_echo="\"\$as_me:$LINENO: $ac_try_echo\""
-$as_echo "$ac_try_echo") >&5
- (eval "$ac_link") 2>conftest.er1
- ac_status=$?
- grep -v '^ *+' conftest.er1 >conftest.err
- rm -f conftest.er1
- cat conftest.err >&5
- $as_echo "$as_me:$LINENO: \$? = $ac_status" >&5
- (exit $ac_status); } && {
- test -z "$ac_c_werror_flag" ||
- test ! -s conftest.err
- } && test -s conftest$ac_exeext && {
- test "$cross_compiling" = yes ||
- $as_test_x conftest$ac_exeext
- }; then
- ac_cv_search_Cudd_Init=$ac_res
-else
- $as_echo "$as_me: failed program was:" >&5
-sed 's/^/| /' conftest.$ac_ext >&5
-
-
-fi
-
-rm -rf conftest.dSYM
-rm -f core conftest.err conftest.$ac_objext conftest_ipa8_conftest.oo \
- conftest$ac_exeext
- if test "${ac_cv_search_Cudd_Init+set}" = set; then
- break
-fi
-done
-if test "${ac_cv_search_Cudd_Init+set}" = set; then
- :
-else
- ac_cv_search_Cudd_Init=no
-fi
-rm conftest.$ac_ext
-LIBS=$ac_func_search_save_LIBS
-fi
-{ $as_echo "$as_me:$LINENO: result: $ac_cv_search_Cudd_Init" >&5
-$as_echo "$ac_cv_search_Cudd_Init" >&6; }
-ac_res=$ac_cv_search_Cudd_Init
-if test "$ac_res" != no; then
- test "$ac_res" = "none required" || LIBS="$ac_res $LIBS"
- CPLINT_LIBS="-lcu "$CPLINT_LIBS
-else
- { { $as_echo "$as_me:$LINENO: error: This package needs glu." >&5
-$as_echo "$as_me: error: This package needs glu." >&2;}
- { (exit 1); exit 1; }; }
-fi
-
- { $as_echo "$as_me:$LINENO: checking for library containing pow" >&5
-$as_echo_n "checking for library containing pow... " >&6; }
-if test "${ac_cv_search_pow+set}" = set; then
- $as_echo_n "(cached) " >&6
-else
- ac_func_search_save_LIBS=$LIBS
-cat >conftest.$ac_ext <<_ACEOF
-/* confdefs.h. */
-_ACEOF
-cat confdefs.h >>conftest.$ac_ext
-cat >>conftest.$ac_ext <<_ACEOF
-/* end confdefs.h. */
-
-/* Override any GCC internal prototype to avoid an error.
- Use char because int might match the return type of a GCC
- builtin and then its argument prototype would still apply. */
-#ifdef __cplusplus
-extern "C"
-#endif
-char pow ();
-int
-main ()
-{
-return pow ();
- ;
- return 0;
-}
-_ACEOF
-for ac_lib in '' m; do
- if test -z "$ac_lib"; then
- ac_res="none required"
- else
- ac_res=-l$ac_lib
- LIBS="-l$ac_lib -lglu -lm $ac_func_search_save_LIBS"
- fi
- rm -f conftest.$ac_objext conftest$ac_exeext
-if { (ac_try="$ac_link"
-case "(($ac_try" in
- *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
- *) ac_try_echo=$ac_try;;
-esac
-eval ac_try_echo="\"\$as_me:$LINENO: $ac_try_echo\""
-$as_echo "$ac_try_echo") >&5
- (eval "$ac_link") 2>conftest.er1
- ac_status=$?
- grep -v '^ *+' conftest.er1 >conftest.err
- rm -f conftest.er1
- cat conftest.err >&5
- $as_echo "$as_me:$LINENO: \$? = $ac_status" >&5
- (exit $ac_status); } && {
- test -z "$ac_c_werror_flag" ||
- test ! -s conftest.err
- } && test -s conftest$ac_exeext && {
- test "$cross_compiling" = yes ||
- $as_test_x conftest$ac_exeext
- }; then
- ac_cv_search_pow=$ac_res
-else
- $as_echo "$as_me: failed program was:" >&5
-sed 's/^/| /' conftest.$ac_ext >&5
-
-
-fi
-
-rm -rf conftest.dSYM
-rm -f core conftest.err conftest.$ac_objext conftest_ipa8_conftest.oo \
- conftest$ac_exeext
- if test "${ac_cv_search_pow+set}" = set; then
- break
-fi
-done
-if test "${ac_cv_search_pow+set}" = set; then
- :
-else
- ac_cv_search_pow=no
-fi
-rm conftest.$ac_ext
-LIBS=$ac_func_search_save_LIBS
-fi
-{ $as_echo "$as_me:$LINENO: result: $ac_cv_search_pow" >&5
-$as_echo "$ac_cv_search_pow" >&6; }
-ac_res=$ac_cv_search_pow
-if test "$ac_res" != no; then
- test "$ac_res" = "none required" || LIBS="$ac_res $LIBS"
- CPLINT_LIBS="-lm "$CPLINT_LIBS
-else
- { { $as_echo "$as_me:$LINENO: error: This package needs m." >&5
-$as_echo "$as_me: error: This package needs m." >&2;}
- { (exit 1); exit 1; }; }
-fi
-
+ #AC_SEARCH_LIBS([g_hash_table_new], [glib-2.0], [], [AC_MSG_ERROR([This package needs glib >=2.0.], [1])], [])
+ #AC_SEARCH_LIBS([Cudd_Init], [cudd], [], [AC_MSG_ERROR([This package needs CUDD.], [1])], [-lcudd -lmtr -lst -lutil -lepd -lm])
+ #AC_SEARCH_LIBS([pow], [m], [], [AC_MSG_ERROR([This package needs m.], [1])], [-lm])
ENABLE_CPLINT=""
if test "$target_os" = "cygwin" -o "$target_os" = "mingw32"
then
diff --git a/configure.in b/configure.in
index 9aef9e7a4..d156d872d 100755
--- a/configure.in
+++ b/configure.in
@@ -1239,14 +1239,13 @@ if test ! "$yap_cv_cplint" = "no"
LDFLAGS=${LDFLAGS}" `echo $GLIBS | awk '{print $1}'` -L$prefix/lib/"
if test ! "$yap_cv_cplint" = "yes"
then
- LDFLAGS+=" -L${yap_cv_cplint}/lib"
- CPLINT_LDFLAGS+=" -L${yap_cv_cplint}/lib"
+ CPLINT_LDFLAGS+=" -L${yap_cv_cplint}/cudd -L${yap_cv_cplint}/mtr -L${yap_cv_cplint}/st -L${yap_cv_cplint}/util -L${yap_cv_cplint}/epd "
CPLINT_CFLAGS+=" -I${yap_cv_cplint}/include"
+ CPLINT_LIBS="-lcudd -lmtr -lst -lutil -lepd -lm "$CPLINT_LIBS
fi
- AC_SEARCH_LIBS([g_hash_table_new], [glib-2.0], [CPLINT_LIBS="-lglib-2.0 "], [AC_MSG_ERROR([This package needs glib >=2.0.], [1])], [])
- AC_SEARCH_LIBS([array_do_alloc], [glu], [CPLINT_LIBS="-lglu "$CPLINT_LIBS], [AC_MSG_ERROR([This package needs glu.], [1])], [])
- AC_SEARCH_LIBS([Cudd_Init], [cu], [CPLINT_LIBS="-lcu "$CPLINT_LIBS], [AC_MSG_ERROR([This package needs glu.], [1])], [-lglu -lm])
- AC_SEARCH_LIBS([pow], [m], [CPLINT_LIBS="-lm "$CPLINT_LIBS], [AC_MSG_ERROR([This package needs m.], [1])], [-lglu -lm])
+ #AC_SEARCH_LIBS([g_hash_table_new], [glib-2.0], [], [AC_MSG_ERROR([This package needs glib >=2.0.], [1])], [])
+ #AC_SEARCH_LIBS([Cudd_Init], [cudd], [], [AC_MSG_ERROR([This package needs CUDD.], [1])], [-lcudd -lmtr -lst -lutil -lepd -lm])
+ #AC_SEARCH_LIBS([pow], [m], [], [AC_MSG_ERROR([This package needs m.], [1])], [-lm])
ENABLE_CPLINT=""
if test "$target_os" = "cygwin" -o "$target_os" = "mingw32"
then
diff --git a/packages/cplint/README b/packages/cplint/README
index e725d93aa..4c3ad442b 100644
--- a/packages/cplint/README
+++ b/packages/cplint/README
@@ -1,32 +1,26 @@
This directory contains the code of the LPAD anc CP-logic interpreter cplint
COMPILATION:
-This package requires GLU (a subpackage of VIS) and GLIB version 1.2.
-You can download GLU from http://vlsi.colorado.edu/~vis/getting_VIS_2.1.html
+This package requires CUDD and GLIB version 1.2.
+You can download CUDD from http://vlsi.colorado.edu/~fabio/CUDD/
You can download GLIB from http://www.gtk.org/. This is a standard Linux package
so it is easy to install using the package management software of your Linux
distribution
INSTALLATION:
-Install glu:
- 1) downlad glu-2.1.tar.gz
+Compile CUDD:
+ 1) downlad cudd-2.4.2.tar.gz
2) decompress it
- 3) cd glu-2.1
- 3) mkdir arch
- 4) cd arch
- 5) ../configure
- 6) make
- 7) su
- 8) make install
-This will install glu into /usr/local, if you want to install to a different DIR
-use ../configure --prefix DIR
+ 3) cd cudd-2.4.2
+ 4) check makefile options
+ 5) make
Installation of cplint:
When compiling Yap, use
- configure --enable-cplint
-Under Windows, you have to use cygwin (glu does not compile under MinGW), so
- configure --enable-cplint --enable-cygwin
-If you installed glu in DIR, use --enable-cplint=DIR
+ configure --enable-cplint=DIR
+Under Windows, you have to use cygwin (CUDD does not compile under MinGW), so
+ configure --enable-cplint --enable-cygwin=DIR
+where DIR is the directory where you compiled CUDD
FEEDBACK:
diff --git a/packages/cplint/cplint_yap.c b/packages/cplint/cplint_yap.c
index 5021f8019..04315f360 100644
--- a/packages/cplint/cplint_yap.c
+++ b/packages/cplint/cplint_yap.c
@@ -42,6 +42,7 @@ returns also the names of the variables to be used to save the ADD in dot format
b=0;
vars.nVar=0;
+ varIndex=0;
while(YAP_IsPairTerm(t))
{
diff --git a/packages/cplint/doc/manual.css b/packages/cplint/doc/manual.css
index ce87c709c..b108289a8 100644
--- a/packages/cplint/doc/manual.css
+++ b/packages/cplint/doc/manual.css
@@ -11,6 +11,7 @@
.cmtt-10{font-family: monospace;}
.cmti-10{ font-style: italic;}
p.noindent { text-indent: 0em }
+td p.noindent { text-indent: 0em; margin-top:0em; }
p.nopar { text-indent: 0em; }
p.indent{ text-indent: 1.5em }
@media print {div.crosslinks {visibility:hidden;}}
@@ -20,6 +21,9 @@ td center { margin-top:0em; margin-bottom:0em; }
.Canvas { position:relative; }
img.math{vertical-align:middle;}
li p.indent { text-indent: 0em }
+li p:first-child{ margin-top:0em; }
+li p:last-child, li div:last-child { margin-bottom:0.5em; }
+li p~ul:last-child, li p~ol:last-child{ margin-bottom:0.5em; }
.enumerate1 {list-style-type:decimal;}
.enumerate2 {list-style-type:lower-alpha;}
.enumerate3 {list-style-type:lower-roman;}
@@ -32,11 +36,11 @@ div.obeylines-v p { margin-top:0; margin-bottom:0; }
td.displaylines {text-align:center; white-space:nowrap;}
.centerline {text-align:center;}
.rightline {text-align:right;}
-div.verbatim {font-family: monospace; white-space: nowrap; }
-table.verbatim {width:100%;}
+div.verbatim {font-family: monospace; white-space: nowrap; text-align:left; clear:both; }
.fbox {padding-left:3.0pt; padding-right:3.0pt; text-indent:0pt; border:solid black 0.4pt; }
+div.fbox {display:table}
div.center div.fbox {text-align:center; clear:both; padding-left:3.0pt; padding-right:3.0pt; text-indent:0pt; border:solid black 0.4pt; }
-table.minipage{width:100%;}
+div.minipage{width:100%;}
div.center, div.center div.center {text-align: center; margin-left:1em; margin-right:1em;}
div.center div {text-align: left;}
div.flushright, div.flushright div.flushright {text-align: right;}
@@ -53,6 +57,8 @@ span.footnote-mark sup.textsuperscript, span.footnote-mark a sup.textsuperscript
div.tabular, div.center div.tabular {text-align: center; margin-top:0.5em; margin-bottom:0.5em; }
table.tabular td p{margin-top:0em;}
table.tabular {margin-left: auto; margin-right: auto;}
+td p:first-child{ margin-top:0em; }
+td p:last-child{ margin-bottom:0em; }
div.td00{ margin-left:0pt; margin-right:0pt; }
div.td01{ margin-left:0pt; margin-right:5pt; }
div.td10{ margin-left:5pt; margin-right:0pt; }
@@ -70,8 +76,9 @@ span.TEX span.E{ position:relative;top:0.5ex;left:-0.0417em;}
a span.TEX span.E {text-decoration: none; }
span.LATEX span.A{ position:relative; top:-0.5ex; left:-0.4em; font-size:85%;}
span.LATEX span.TEX{ position:relative; left: -0.4em; }
-div.float img, div.float .caption {text-align:center;}
-div.figure img, div.figure .caption {text-align:center;}
+div.float, div.figure {margin-left: auto; margin-right: auto;}
+div.float img {text-align:center;}
+div.figure img {text-align:center;}
.marginpar {width:20%; float:right; text-align:left; margin-left:auto; margin-top:0.5em; font-size:85%; text-decoration:underline;}
.marginpar p{margin-top:0.4em; margin-bottom:0.4em;}
table.equation {width:100%;}
@@ -88,10 +95,12 @@ table.pmatrix {width:100%;}
span.pmatrix img{vertical-align:middle;}
div.pmatrix {text-align:center;}
table.pmatrix {width:100%;}
+span.bar-css {text-decoration:overline;}
img.cdots{vertical-align:middle;}
.partToc a, .partToc, .likepartToc a, .likepartToc {line-height: 200%; font-weight:bold; font-size:110%;}
-.caption td.id{font-weight: bold; white-space: nowrap; }
-table.caption {text-align:center;}
+.index-item, .index-subitem, .index-subsubitem {display:block}
+div.caption {text-indent:-2em; margin-left:3em; margin-right:1em; text-align:left;}
+div.caption span.id{font-weight: bold; white-space: nowrap; }
h1.partHead{text-align: center}
p.bibitem { text-indent: -2em; margin-left: 2em; margin-top:0.6em; margin-bottom:0.6em; }
p.bibitem-p { text-indent: 0em; margin-left: 2em; margin-top:0.6em; margin-bottom:0.6em; }
@@ -107,7 +116,7 @@ div.thanks{text-align:left; margin-left:10%; font-size:85%; font-style:italic; }
div.author{white-space: nowrap;}
.quotation {margin-bottom:0.25em; margin-top:0.25em; margin-left:1em; }
.abstract p {margin-left:5%; margin-right:5%;}
-table.abstract {width:100%;}
+div.abstract {width:100%;}
.figure img.graphics {margin-left:10%;}
/* end css.sty */
diff --git a/packages/cplint/doc/manual.html b/packages/cplint/doc/manual.html
index 7404f09a4..16d034d2c 100644
--- a/packages/cplint/doc/manual.html
+++ b/packages/cplint/doc/manual.html
@@ -1,13 +1,13 @@
-cplint Version beta2.0 Manual
+cplint Version 2.0 Manual
-
+
@@ -15,28 +15,27 @@
-
cplint Version beta2.0 Manual
+
cplint Version 2.0 Manual
Fabrizio Riguzzi fabrizio.riguzzi@unife.it
-
+class="cmr-12">fabrizio.riguzzi@unife.it
June 19, 2008
+class="cmr-12">July 27, 2010
1 Introduction
-
cplint is a suite of programs for reasoning with LPADs [11, 12] and CP-logic
programs [10, 13].
-
It consists of three Prolog modules for answering queries using goal-oriented
+
It consists of three Prolog modules for answering queries using goal-oriented
procedures plus three Prolog modules for answering queries using the definition of the
semantics of LPADs and CP-logic.
-
The modules for answering queries using using goal-oriented procedures are
+
The modules for answering queries using using goal-oriented procedures are
lpadsld.pl, lpad.pl and 7] and [8]. It is based on SLDNF resolution and
is an adaptation of the interpreter for ProbLog [4].
-
It was proved correct [
It was proved correct [8] with respect to the semantics of LPADs for range
restricted acyclic programs [1] without function symbols.
-
It is also able to deal with extensions of LPADs and CP-logic: the clause
+
It is also able to deal with extensions of LPADs and CP-logic: the clause
bodies can contain setof and bagof, the probabilities in the head may
@@ -84,7 +83,7 @@ href="#XDBLP:journals/jacm/ChenW96">3
]. As a consequence, it works fo
class="cmtt-10">cpl.pl
: computes the probability of a query using a top-down procedure
based on SLG resolution and moreover checks that the CP-logic program
is valid, i.e., that it has at least an execution model.
-
The modules for answering queries using the definition of the semantics of LPADs
+
The modules for answering queries using the definition of the semantics of LPADs
and CP-logic are semlpadsld.pl, semlpad.pl and P, i.e.,
and temporal precedence. It uses the definition of the semantics given in
[13].
-
+
2 Installation
-
cplint is distributed in source code in the CVS version of Yap. It
+
cplint is distributed in source code in the git version of Yap. It
includes Prolog and C files. Download it by following the instruction in
-http://www.ncc.up.pt/~vsc/Yap/downloads.html .
-
cplint requires cudd and glib-2.0. You can download cudd from
+http://vlsi.colorado.edu/ fabio/CUDD/ . You can download glib-2.0 (version ≥ 2.0) from http://www.gtk.org/ . This is a standard GNU package
-so it is easy to install it using the package management software of your Linux or
-Cygwin distribution.
-
Install glu:
+class="cmmi-10">.
0)
+from http://www.gtk.org/ . This is a standard GNU package so it is easy to
+install it using the package management software of your Linux or Cygwin
+distribution.
+
Compile cudd:
-
downlad glu-2.1.tar.gz
+
downlad cudd-2.4.2.tar.gz
-
decompress it
+
decompress it
-
cd glu-2.1
+
cd cudd-2.4.2
-
mkdir arch
+
check makefile options
-
cd arch
-
-
../configure
-
-
make
-
-
su
-
-
make install
-
This will install glu into /usr/local, if you want to install to a different DIR use
-../configure --prefix DIR
-
Install Yap together with make
+
Install Yap together with cplint: when compiling Yap following the instuction of
the INSTALL file in the root of the Yap folder, use
-
-configure --enable-cplint
+
+configure --enable-cplint=DIR
-
-
Under Windows, you have to use Cygwin (glu does not compile under MinGW),
-so
-
+
Under Windows, you have to use Cygwin (glu does not compile under MinGW),
+so
-
-configure --enable-cplint --enable-cygwin
+
+configure --enable-cplint=DIR --enable-cygwin
-
-
If you installed glu in DIR, use --enable-cplint=DIR
-
After having performed
where DIR is the path to the directory cudd-2.4.2 (including cudd-2.4.2).
+
After having performed make install you can do make installcheck that will
execute a suite of tests of the various programs. If no error is reported you have a
working installation of cplint.
-
+
3 Syntax
-
Disjunction in the head is represented with a semicolon and atoms in the head are
+
Disjunction in the head is represented with a semicolon and atoms in the head are
separated from probabilities by a colon. For the rest, the usual syntax of Prolog is
used. For example, the CP-logic clause
@@ -220,49 +190,35 @@ used. For example, the CP-logic clause
src="manual0x.png" alt="h1 : p1 ∨...∨ hn : pn ← b1,...,bm,¬c1,...,¬cl " class="math-display" >
is
represented by
-
+
h1:p1 ; ... ; hn:pn :- b1,...,bm,\+ c1,....,\+ cl
-
-
No parentheses are necessary. The
No parentheses are necessary. The pi are numeric expressions. It is up to the user to
ensure that the numeric expressions are legal, i.e. that they sum up to less than
one.
-
If the clause has an empty body, it can be represented like this
+
If the clause has an empty body, it can be represented like this
-
+
h1:p1 ; ... ;hn:pn.
-
-
If the clause has a single head with probability 1, the annotation can be omitted and
+
If the clause has a single head with probability 1, the annotation can be omitted and
the clause takes the form of a normal prolog clause, i.e.
-
The first clause states that if we toss a coin that is not biased it has equal
+
The first clause states that if we toss a coin that is not biased it has equal
probability of landing heads and tails. The second states that if the coin is biased it
has a slightly higher probability of landing heads. The third states that the coin is
fair with probability 0.9 and biased with probability 0.1 and the last clause states
that we toss a coin with certainty.
-
+
4 Commands
-
All six modules accept the same commands for reading in files and answering queries.
+
All six modules accept the same commands for reading in files and answering queries.
The LPAD or CP-logic program must be stored in a text file with extension .cpl.
Suppose you have stored the example above in file lpad.pl) by issuing the command
-
+
use_module(library(lpad)).
-
-
at the command prompt. Then you must parse the source file
at the command prompt. Then you must parse the source file coin.cpl with the
command
-
+
p(coin).
-
-
if
if coin.cpl is in the current directory, or
-
+
p(’path_to_coin/coin’).
-
-
if
if coin.cpl is in a different directory. At this point you can pose query to the
program by using the predicate s/2 (for solve) that takes as its first argument a
@@ -325,13 +271,10 @@ as its second argument. For example, the probability of the conjunction
head(coin),biased(coin) can be asked with the query
-
+
s([head(coin),biased(coin)],P).
-
-
For computing the probability of a conjunction given another conjunction you can
+
For computing the probability of a conjunction given another conjunction you can
use the predicate sc/3 (for solve conditional) that take takes as input the query
conjunction as its first argument, the evidence conjunction as its second argument
@@ -341,25 +284,22 @@ class="cmtt-10">heads(coin)
given the evidence biased(coin) can be asked with the
query
-
+
sc([heads(coin)],[biased(coin)],P).
-
-
After having parsed a program, in order to read in a new program you must restart
+
After having parsed a program, in order to read in a new program you must restart
Yap when using semlpadsld.pl and semlpad.pl. With the other modules, you can
directly parse a new program.
-
When using
When using lpad.pl, the system can print the message “Uunsound program” in
the case in which an instance with a three valued well founded model is found.
Moreover, it can print the message “It requires the choice of a head atom from a non
ground head”: in this case, in order to answer the query, all the groundings of the
culprit clause must be generated, which may be impossible for programs with
function symbols.
-
When using
When using semcpl.pl, you can print the execution process by using the
command print. after context is a list of atoms that are true in the context.
semcpl.pl can print “Invalid program” in the case in which no execution process
exists.
-
When using
When using cpl.pl you can print a partial execution model including all the
clauses involved in the query issued with print. cpl.pl can print the messages
“Uunsound program”, “It requires the choice of a head atom from a non ground
head” and “Invalid program”.
-
The modules make use of a number of parameters in order to control their
+
The modules make use of a number of parameters in order to control their
behavior. They that can be set with the command
-
+
set(parameter,value).
-
-
from the Yap prompt after having loaded the module. The current value can be read
+
from the Yap prompt after having loaded the module. The current value can be read
with
-
+
setting(parameter,Value).
-
-
from the Yap prompt. The available parameters are:
+
from the Yap prompt. The available parameters are:
epsilon_parsing (valid for all six modules): if (1 - the sum of the
@@ -418,13 +352,10 @@ class="cmtt-10">m
is the number of the binary variable. The correspondenc
between variables and clauses can be evinced from the message printed on the
screen, such as
-
+
Variables: [(2,[X=2,X1=1]),(2,[X=1,X1=0]),(1,[])]
-
-
where the first element of each couple is the clause number of the input file
+
where the first element of each couple is the clause number of the input file
(starting from 1). In the example above variable X0 corresponds to clause 2
@@ -441,13 +372,10 @@ class="cmtt-10">graphviz
ground_body (valid for false, ground
constant. In the case where the body contains variables not in the
head, setting it to false means that the body represents an existential
event.
-
+
5 Semantic Modules
-
The three semantic modules need to produce a grounding of the program in order to
+
The three semantic modules need to produce a grounding of the program in order to
compute the semantics. They require an extra file with extension .uni (for universe)
in the same directory where the .cpl file is.
-
There are two ways to specify how to ground a program. The first consists in
+
There are two ways to specify how to ground a program. The first consists in
providing the list of constants to which each variable can be instantiated. For
example, in our case the current directory will contain a file coin.uni that is a
Prolog file containing facts of the form
-
+
universe(var_list,const_list).
-
-
where
where var_list is a list of variables names (each must be included in single quotes)
and const_list is a list of constants. The semantic modules generate the grounding
@@ -490,29 +415,23 @@ class="cmtt-10">var_list
with the constants of
class="cmtt-10">const_list
. Note that the variables are identified by name, so a variable with
the same name in two different clauses will be instantiated with the same
constants.
-
The other way to specify how to ground a program consists in using mode and
+
The other way to specify how to ground a program consists in using mode and
type information. For each predicate, the file .uni must contain a fact of the
form
-
+
mode(predicate(t1,...,tn)).
-
-
that specifies the number and types of each argument of the predicate. Then, the list
+
that specifies the number and types of each argument of the predicate. Then, the list
of constants that are in the domain of each type ti must be specified with a fact of
the form
-
+
type(ti,list_of_constants).
-
-
The file
The file .uni can contain both universe and mode declaration, the ones to be used
depend on the value of the parameter grounding: with value variables, the
universe declarations are used, with value modes the mode declarations are
used.
-
With
With semcpl.pl only mode declarations can be used.
-
+
6 Extensions
-
In this section we will present the extensions to the syntax of LPADs and CP-logic
+
In this section we will present the extensions to the syntax of LPADs and CP-logic
programs that cplint can handle.
-
The first is the use of some standard Prolog predicates. The bodies can contain
+
The first is the use of some standard Prolog predicates. The bodies can contain
the built-in predicates:
-
The bodies can also contain the following library predicates:
+
The bodies can also contain the following library predicates:
-
+
member/2
max_list/2
min_list/2
nth0/3
nth/3
-
-
plus the predicate
+
plus the predicate
-
+
average/2
-
-
that, given a list of numbers, computes its arithmetic mean.
-
When using
that, given a list of numbers, computes its arithmetic mean.
+
When using lpadsld.pl, the bodies can contain the predicates setof/3 and
bagof/3 with the same meaning as in Prolog. Existential quantifiers are allowed in
both, so for example the query
-
+
setof(Z, (term(X,Y))^foo(X,Y,Z), L).
-
-
returns all the instantiations of
returns all the instantiations of Z such that there exists an instantiation of X and Y
for which foo(X,Y,Z) is true.
-
An example of the use of
An example of the use of setof and bagof is in the file female.cpl:
-
The disjunctive rule expresses the probability of a person of unknown sex of being
+
The disjunctive rule expresses the probability of a person of unknown sex of being
male or female depending on the number of males and females that are known. This
is an example of the use of expressions in the probabilities in the head that depend
on variables in the body. The probabilities are well defined because they always sum
to 1 (unless P is 0).
-
Another use of
Another use of setof and bagof is to have an attribute depend on an
aggregate function of another attribute, similarly to what is done in PRM and
CLP(BN).
-
So, in the classical school example (available in
So, in the classical school example (available in student.cpl) you can find the
following clauses:
-
where registr_stu(R,S) expresses that registration R refers to student S and
@@ -656,7 +557,7 @@ class="cmtt-10">R
reports grade G which is a natural
number. The two clauses express a dependency of the rank of the student from the
average of her grades.
-
Another extension can be used with
Another extension can be used with lpadsld.pl in order to be able to represent
reference uncertainty of PRMs. Reference uncertainty means that the link structure
of a relational model is not fixed but is uncertain: this is represented by having the
@@ -668,31 +569,25 @@ selected uniformly from certain sets, the following clauses can be used (see fil
paper_ref_simple.cpl):
-
The first clauses states that the paper P cited in a citation C is selected
uniformly from the set of all papers with topic theory. The second clauses
expresses that the citing paper is selected uniformly from the papers with topic
ai.
-
These clauses make use of the predicate
+
These clauses make use of the predicate
-
+
uniform(Atom,Variable,List)
-
-
in the head, where
in the head, where Atom must contain Variable. The meaning is the following:
the set of all the atoms obtained by instantiating ∕N where N is the length of
List.
-
A more elaborate example is present in file
A more elaborate example is present in file paper_ref.cpl:
-
where the cited paper depends on the topic of the citing paper. In particular, if the
+
where the cited paper depends on the topic of the citing paper. In particular, if the
topic is theory, the cited paper is selected uniformly from the papers about theory
with probability 0.9 and from the papers about ai with probability 0.1. if
the topic is ai, the cited paper is selected uniformly from the papers about
theory with probability 0.01 and from the papers about ai with probability
0.99.
-
PRMs take into account as well existence uncertainty, where the existence of
+
PRMs take into account as well existence uncertainty, where the existence of
instances is also probabilistic. For example, in the paper domain, the total number of
citations may be unknown and a citation between any two paper may have a
probability of existing. For example, a citation between two paper may be more
probable if they are about the same topic:
-
This is an example where the probabilities in the head do not sum up to one so the
+
This is an example where the probabilities in the head do not sum up to one so the
null event is automatically added to the head. The first clause states that, if the topic
of a paper X is theory and of paper X to Y. The other clauses consider the remaining cases for the
topics.
-
+
7 Additional Files
-
In the directory where Yap keeps the library files (usually
In the directory where Yap keeps the library files (usually /usr/local/share/ Yap)
you can find the directory cplint that contains the files:
@@ -861,13 +750,13 @@ class="cmtt-10">student.cpl
: student example from Figure 1.
href="#XGetFri01-BC">5].
win.cpl, light.cpl, trigger.cpl, throws.cpl, hiv.cpl,
- win.cpl, light.cpl, trigger.cpl, throws.cpl, hiv.cpl, invalid.cpl: programs taken from [13]. invalid.cpl is an example
of a program that is invalid but sound.
-
The files
The files *.uni that are present for some of the examples are used by the
semantical modules. Some of the example files contain in an initial comment
some queries together with their result.
@@ -875,18 +764,18 @@ class="cmtt-10">*.uni
that are present for some of the examples are used
Subdirectory doc: contains this manual in latex, html and pdf.
-
+
8 License
-
cplint, as Yap, follows the Artistic License 2.0 that you can find in Yap CVS root
dir. The copyright is by Fabrizio Riguzzi.
-
Copyright (c) 1995-2004, Regents of the University of Colorado
-
All rights reserved.
-
Redistribution and use in source and binary forms, with or without modification,
+
Copyright (c) 1995-2004, Regents of the University of Colorado
+
All rights reserved.
+
Redistribution and use in source and binary forms, with or without modification,
are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this
@@ -899,8 +788,8 @@ are permitted provided that the following conditions are met:
Neither the name of the University of Colorado nor the names of its
contributors may be used to endorse or promote products derived from
this software without specific prior written permission.
-
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS
- AND CONTRIBUTORS ”AS IS” AND ANY EXPRESS OR IMPLIED
+
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ”AS IS” AND ANY EXPRESS OR IMPLIED
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
@@ -908,12 +797,12 @@ OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
-INTERRUPTION) HOWEVER CAU-SED
- AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+INTERRUPTION) HOWEVER CAU-SED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF
ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
lpad.pl, semlpad.pl and cpl.pl are based on the SLG system by
+
References
-
+
-
+
[1]K. R. Apt and M. Bezem. Acyclic programs. New GenerationComput., 9(3/4):335–364, 1991.
-
+
[2]H. Blockeel. Probabilistic logical models for mendel’s experiments: An
exercise. In Inductive Logic Programming (ILP 2004), Work in ProgressTrack, 2004.
-
+
[3]Weidong Chen and David Scott Warren. Tabled evaluation with
delaying for general logic programs. J. ACM, 43(1):20–74, 1996.
-
+
[4]L. De Raedt, A. Kimmig, and H. Toivonen. Problog: A probabilistic
prolog and its application in link discovery. In Proceedings of the 20th
class="cmti-10">International Joint Conference on Artificial Intelligence
, pages 2462–2467,
2007.
-
+
[5]L. Getoor, N. Friedman, D. Koller, and A. Pfeffer. Learning
probabilistic relational models. In Saso Dzeroski and Nada Lavrac, editors,
Relational Data Mining. Springer-Verlag, Berlin, 2001.
-
+
[6]L. Getoor, N. Friedman, D. Koller, and B. Taskar. Learning
probabilistic models of relational structure. Journal of Machine LearningResearch, 3:679–707, December 2002.
-
+
[7]Fabrizio Riguzzi. A top down interpreter for lpad and cp-logic. In
h
.
-
+
[8]Fabrizio Riguzzi. A top down interpreter for lpad and
cp-logic. In Algorithms for Solving Problems with Combinatorial Explosion
http://pst.istc.cnr.it/RCRA07/articoli/P19-riguzzi-RCRA07.pdf .
-
+
[9]V. Santos Costa, D. Page, M. Qazi, and J. Cussens. CLP(BN):
Constraint logic programming for probabilistic knowledge. In Uncertaintyin Artificial Intelligence (UAI 2003), 2003.
-
+
[10]J. Vennekens, M. Denecker, and M. Bruynooghe. Representing causal
information about a probabilistic process. In 10th European Conference on
class="cmti-10">Logics in Artificial Intelligence, JELIA 2006
, LNAI. Springer, September
2006.
-
+
[11]J. Vennekens and S. Verbaeten. Logic programs with annotated
disjunctions. Technical Report CW386, K. U. Leuven, 2003. ~
joost/techrep.ps .
-
+
[12]J. Vennekens, S. Verbaeten, and M. Bruynooghe. Logic programs with
annotated disjunctions. In ~joost/
.
-
+
[13]Joost Vennekens, Marc Denecker, and Maurice Bruynooge. Extending
the role of causality in
diff --git a/packages/cplint/doc/manual.pdf b/packages/cplint/doc/manual.pdf
index 878568114..a37549757 100644
Binary files a/packages/cplint/doc/manual.pdf and b/packages/cplint/doc/manual.pdf differ
diff --git a/packages/cplint/doc/manual.tex b/packages/cplint/doc/manual.tex
index 739f35451..ef9b79fd7 100644
--- a/packages/cplint/doc/manual.tex
+++ b/packages/cplint/doc/manual.tex
@@ -7,6 +7,7 @@
\documentclass{article}
\usepackage{graphicx}
\DeclareGraphicsExtensions{.png, .gif, .jpg}
+\newcommand{\url}[1]{\Link[#1]{}{} #1 \EndLink}
\newcommand{\href}[2]{\Link[#1]{}{} #2 \EndLink}
\newcommand{\hypertarget}[2]{\Link[]{}{#1} #2 \EndLink}
\newcommand{\hyperlink}[2]{\Link[]{#1}{} #2 \EndLink}
@@ -15,7 +16,7 @@
\begin{document}
-\title{\texttt{cplint} Version beta2.0 Manual}
+\title{\texttt{cplint} Version 2.0 Manual}
\author{Fabrizio Riguzzi\\
@@ -57,39 +58,33 @@ The modules for answering queries using the definition of the semantics of LPADs
%For program with function symbols, the semantics of LPADs and CP-logic are not defined. However, the interpreter accepts programs with function symbols and, if it does not go into a loop, it returns an answer. What is the meaning of this answer is subject of current study.
\section{Installation}
-\texttt{cplint} is distributed in source code in the CVS version of Yap. It includes Prolog and C files. Download it by following the instruction in \href{http://www.ncc.up.pt/~vsc/Yap/downloads.html}{http://www.ncc.up.pt/$\sim$vsc/Yap/downloads.html}.
+\texttt{cplint} is distributed in source code in the git version of Yap. It includes Prolog and C files. Download it by following the instruction in \url{http://www.ncc.up.pt/~vsc/Yap/downloads.html}.
-\texttt{cplint} requires glu (a subpackage of vis) and glib-2.0.
-You can download glu from \href{http://vlsi.colorado.edu/~vis/getting_VIS_2.1.html}{http://vlsi.colorado.edu/$\sim$vis/getting\_VIS\_2.1.html}
-You can download glib-2.0 (version $\geq 2.0$) from \href{http://www.gtk.org/}{http://www.gtk.org/}. This is a standard GNU package
+\texttt{cplint} requires cudd and glib-2.0.
+You can download cudd from \url{http://vlsi.colorado.edu/~fabio/CUDD/}.
+You can download glib-2.0 (version $\geq 2.0$) from \url{http://www.gtk.org/}. This is a standard GNU package
so it is easy to install it using the package management software of your Linux or Cygwin
distribution.
-Install glu:
+Compile cudd:
\begin{enumerate}
-\item downlad \texttt{glu-2.1.tar.gz}
+\item downlad \texttt{cudd-2.4.2.tar.gz}
\item decompress it
-\item \texttt{cd glu-2.1}
-\item \texttt{mkdir arch}
-\item \texttt{cd arch}
-\item \texttt{../configure}
+\item \texttt{cd cudd-2.4.2}
+\item check makefile options
\item \texttt{make}
- \item \texttt{su}
- \item \texttt{make install}
\end{enumerate}
-This will install glu into \texttt{/usr/local}, if you want to install to a different \texttt{DIR}
-use \texttt{../configure --prefix DIR}
Install Yap together with \texttt{cplint}:
when compiling Yap following the instuction of the \texttt{INSTALL} file in the root of the Yap folder, use
\begin{verbatim}
-configure --enable-cplint
+configure --enable-cplint=DIR
\end{verbatim}
Under Windows, you have to use Cygwin (glu does not compile under MinGW), so\\
\begin{verbatim}
-configure --enable-cplint --enable-cygwin
+configure --enable-cplint=DIR --enable-cygwin
\end{verbatim}
-If you installed glu in \texttt{DIR}, use \texttt{--enable-cplint=DIR}
+where \texttt{DIR} is the path to the directory \texttt{cudd-2.4.2} (including \texttt{cudd-2.4.2}).
After having performed \texttt{make install} you can do \texttt{make installcheck} that will execute a suite of tests of the various programs. If no error is reported you have a working installation of \texttt{cplint}.
@@ -201,7 +196,7 @@ Variables: [(2,[X=2,X1=1]),(2,[X=1,X1=0]),(1,[])]
In the example above variable \texttt{X0} corresponds to clause \texttt{2} with the substitutions \texttt{X=2,X1=1},
variable \texttt{X1} corresponds to clause \texttt{2} with the substitutions \texttt{X=1,X1=0} and
variable \texttt{X2} corresponds to clause \texttt{1} with the empty substitution.
- You can view the graph with \texttt{graphviz} (\href{www.graphviz.org}{www.graphviz.org}) using the
+ You can view the graph with \texttt{graphviz} (\url{www.graphviz.org}) using the
command
\begin{verbatim}
dotty cpl.dot &