🚀 go-pugleaf

Hello,
  I am hoping someone can assist me with a problem I am having in calling
the Leantap theorem prover from a C program, using Sicstus Prolog.

  As a test case, I'm using the formula :

	p(a),-p(f(f(a))),all(X,(-p(X);p(f(X))))

  This works fine under Sicstus Prolog like so :



% sicstus 
SICStus 3  #3: Thu Jul 11 00:38:52 EST 1996
| ?- consult(leantap).
{consulting /home/dave/test/leantap.pl...}
{loading /usr/local/lib/sicstus/library/lists.ql...}
{loaded /usr/local/lib/sicstus/library/lists.ql in module lists, 40 msec 30864 bytes}
{loading /home/dave/test/unify.ql...}
{loaded /home/dave/test/unify.ql in module unify, 10 msec 11216 bytes}
{consulted /home/dave/test/leantap.pl in module leantap, 120 msec 62784 bytes}

yes
| ?- prove((p(a),-p(f(f(a))),all(X,(-p(X);p(f(X))))),2). 

true ? 

yes
| ?- 



  Now, I have compiled leantap.pl, nnf.pl and unify.pl using the Sicstus
fcompile predicate, and generated .ql files.
  I then wrote the following C program :



#include <stdio.h>
#include "/usr/local/include/sicstus/sicstus.h"

main ()
{
        SP_pred_ref     pred;
        SP_term_ref     formula, varlimit;
        int             result;
        extern int      SP_errno;

        if (SP_initialize (0, NULL, NULL) != SP_SUCCESS)
                printf ("Init:%s\n", SP_error_message (SP_errno));

        if (SP_load ("leantap.ql") != SP_SUCCESS)
                printf ("Load:%s\n", SP_error_message (SP_errno));

        pred = SP_predicate ("prove", 2, "leantap");
        formula = SP_new_term_ref ();
        varlimit = SP_new_term_ref ();

        SP_put_string (formula, "p(a),-p(f(f(a))),all(X,(-p(X);p(f(X))))");
        SP_put_integer (varlimit, 2);

        result = SP_query (pred, formula, varlimit);

        if (result == SP_SUCCESS)
                printf ("true indeed\n");
        else if (result == SP_FAILURE)
                printf ("no good\n");
        else
                printf ("Error: %s\n", SP_error_message (SP_errno));
}




  I compile my program like so, including the Sicstus run-time library :

% SP_PATH=/usr/local/lib/sicstus
% export SB_PATH
% gcc -o testit testit.c /usr/local/lib/sicstus/bin/flinkage.c \
       /usr/local/lib/sicstus/bin/runtime.o -lm -rdynamic -ldl

  but when I run my program I always get the message "no good" - no
matter what sort of arguments I try to give (e.g. -(pv-p) etc.).

  Has any fine person out there tried to call Leantap from a C program?
Have you got it working?  Could you kindly tell me what I am doing wrong?
Many thanks !

-- 
   .////.   .//    David M. Williams            d.williams@qcc.hl.com.au
 o:::::::::///     Computer Scientist                Phone: (049) 612201
>::::::::::\\\     Quality Coal Consulting             Fax: (049) 611231
   '\\\\\'   \\    Newcastle, NSW, Australia        Mobile:  0412 215440