Working with constraints

[simonefulvio-rollini]

Hello, I am trying to figure out how to perform verification of assertions in presence of linear constraints.
Consider the following simple piece of code:

:- module(test5, [p1/2], [assertions,nativeprops]).
:- use_module(domain(polyhedra)).
:- use_module(library(ppl)).

:- entry p1(X,Y) : (int(X), constraint([X>=5, X=<10])).
:- check success p1(X,Y) => (int(Y), constraint([Y>=8, Y=<13])).
p1(X,Y) :- p2(X,Y). 

:- trust pred p2(X,Y) : (int(X)) => (Y is X + 3).
p2(1,4).

There are two assumptions: (1) when p1 is called, X is in [5,10], and, (2) when p2 is called and returns, Y = X+3. The first assumption uses an 'entry' assertion, while the second assumption uses a 'trust' status.
I would expect this information sufficient to prove that, when p1 returns, Y is in [8,13].

However, the output puzzles me.
First, towards the beginning, the output reports:

NOTE (p_unit): (lns 7-9) arithmetic:is/2 used in an assertion for test5:p2/2 in test5 has not been loaded (this is a bug)
}
{loaded in 246.799 msec.}
}
{WARNING (auto_interface): Domain polyhedra is unavailable in this build (please use full CiaoPP version)}

I have installed the latest full CiaoPP version, and even the Parma Polyhedra library, so I do not understand the reason for the warning. Note that the warning message appears also when analyzing the above code in the Ciao Playground.

Second, the outcome of the analysis is:

{WARNING (ctchecks_pred_messages): (lns 6-6) Could not verify assertion:
:- check success p1(X,Y)
   => ( int(Y), constraint([Y>=8,Y=<13]) ).
because
    constraint([Y>=8,Y=<13])
could not be derived from inferred success:
[eterms] rt0(X),rt1(Y) 
with:
:- regtype rt1/1.
rt1(4).

:- regtype rt0/1.
rt0(1).


[shfr]   ground([X,Y]) }
{WARNING (ctchecks_pred_messages): (lns 6-6) Could not verify assertion:
:- check success p1(X,Y)
   => ( int(Y), constraint([Y>=8,Y=<13]) ).
because
    constraint([Y>=8,Y=<13])
could not be derived from inferred success:
[eterms] rt0(X),rt1(Y) 
with:
:- regtype rt1/1.
rt1(4).

:- regtype rt0/1.
rt0(1).


[shfr]   ground([X,Y]) }
{NOTE (ctchecks_pred_messages): (lns 7-9) Verified assertion:
:- check calls p2(X,Y)
   : int(X).
}
}
{assertions checked in 6.891 msec.}
}
{NOTE (analysis_stats): Assertion checking summary:
[Predicate-level] Checked: 1 (33.33%) False: 0 (0.00%) Check: 2 (66.67%) Total: 3
[Call site-level] Checked: 0 (--) False: 0 (--) Check: 0 (--) Total: 0
}

The tool is not able to prove the 'check calls' assertion; nothing changes if the two 'use_module' predicates are commented away.

Can you please help me understand what I am getting wrong and how to make this example work?
Thanks,
Simone

[djurjo]

Hi Simone,

it looks like the assertion of p2/2 is not well-formed. We do not
support the usage of is/2 in assertions (basically is/2 is not a
property). To do so you need to write it as a constraint. I've tried
the following program on my machine:

:- entry p1(X,Y) : (int(X), constraint([X>=5, X=<10])).
:- check success p1(X,Y) => (int(Y), constraint([Y>=8, Y=<13])).
p1(X,Y) :- p2(X,Y). 

:- trust pred p2(X,Y) : (int(X)) => (constraint([Y = X + 3])).
p2(1,4).

and compile-time checking works as expected:

{NOTE (ctchecks_pred_messages): (lns 7-7) Verified assertion:
:- check success p1(X,Y)
   => ( int(Y), constraint([Y>=8,Y=<13]) ).
}
{NOTE (ctchecks_pred_messages): (lns 8-10) Verified assertion:
:- check calls p2(X,Y)
   : int(X).
}
}
{assertions checked in 1.015 msec.}
}
{NOTE (analysis_stats): Assertion checking summary:
[Predicate-level] Checked: 2 (100.00%) False: 0 (0.00%) Check: 0
(0.00%) Total: 2
[Call site-level] Checked: 0 (--) False: 0 (--) Check: 0 (--) Total: 0
}

However, I see from your message that it seems that the polyhedra
domain may not be installed well. How did you install it? Did you use
the option given by the Ciao installer or did you install it from its
own repository? If its the latter maybe the following helps:

cd /path/to/ciao/ciao-devel
./ciao-boot.sh build ciao_ppl
./ciao-boot.sh build ciaopp

If that does not work, please let us know what system you're working on
and what error messages you are getting and we will figure out what's
happening. The integration with PPL is quite complex and because of it,
and its dependencies, it may break sometimes because of updates/changes
in the architecture.

Best,

[simonefulvio-rollini]

My installation might be missing something:

There is no 'ciao-devel' folder.
The two components are there:

The two commands both return an error:

./ciao-boot.sh build ciao_ppl
{ERROR (ciao_builder): 'ciao_ppl' does not look like a valid builder target.

It does not correspond to a known bundle name, a path to a bundle, or a path
to a workspace containing bundles.

Some possible reasons:
 - target unreachable from CIAOROOT or CIAOPATH
 - (only for bundles in catalogues) the ACTIVATE mark is missing
 - Manifest.pl file is invalid
 - the bundle has not been configured or built
}

./ciao-boot.sh build ciaopp
=> ciaopp: preparing build [bin]
=> ciaopp: building [bin]
   compiled src/ (86 modules)
   compiled domains/ (66 modules)
   compiled lib/ (7 modules)
   compiled spec/ (43 modules)
   compiled batch/ (7 modules)
   compiling ciaopp-dump (command)
   compiling ciaopp-batch (command)
   compiling ciaopp_master (command)
   compiling ciaopp_batch_report (command)
=> ciaopp.cmds: building [bin]
   compiling ciaopp (command)
=> ciaopp.ciaopp_client: building [bin]
=> ciaopp: building [docs]
   generating ciaopp (manual)
   generating ciaopp_tutorials (manual)
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:exfilter(exfilter_lpdoc) does not exist}
ERROR: {Program ended with failure}
{ERROR: No handle found for thrown exception error(return_code(2,pcall(<mypath>/.ciaoroot/v1.25.0-m1/build/bin/lpdoc,[--output_dir=<mypath>/.ciaoroot/v1.25.0-m1/build/doc,-t,all,<mypath>/.ciaoroot/v1.25.0-m1/ciaopp/doc/tutorials/SETTINGS.pl],[env([CIAOALIASPATH=,CIAOROOT=<mypath>/.ciaoroot/v1.25.0-m1,CIAOHDIR=<mypath>/.ciaoroot/v1.25.0-m1/build/eng/ciaoengine/include,CIAOENGINE=<mypath>/.ciaoroot/v1.25.0-m1/build/eng/ciaoengine/objs/LINUXx86_64/ciaoengine])])),process_join/1)}

Should I try reinstalling CiaoPP in another manner?

[djurjo]

Hi again Simone,

Sorry, I meant your installation folder (in my case it was ciao-devel).
It looks like something is breaking when generating the tutorials. We are looking at it and working on a fix.
In the meantime, please try running:

ciao build --bin ciao_ppl
ciao build --bin ciaopp

This should build both ciao_ppl and ciaopp without generating the tutorials.

[simonefulvio-rollini]

I am still running into errors: executing the first command, while in the installation folder, yields:

~/.ciaoroot/v1.25.0-m1$ ciao build --bin ciao_ppl
=> core.engine: building [bin]
   compiling ciaoengine.LINUXx86_64 (engine)
=> core.exec_header: building [bin]
=> core.ciaoc: building [bin]
   compiling ciaoc (command) [using bootstrap compiler]
=> core.shell: building [bin]
   compiling ciaosh (command)
   compiling ciao-shell (command)
=> core: building [bin]
   compiled engine/ (23 modules)
   compiled lib/ (119 modules)
   compiled library/ (257 modules)
   compiled library/clpq/ (9 modules)
   compiled library/clpr/ (10 modules)
=> core.ciao_env: building [bin]
=> core.core_cmds: building [bin]
   compiling ciaodump (command)
   compiling pldiff (command)
   compiling ciaoc_sdyn (command)
   compiling ciao-serve (command)
   compiling rundaemon (libexec)
=> core.ciaocl: building [bin]
=> core.ciao_sysconf: building [bin]
=> builder: building [bin]
   compiled src/ (47 modules)
   compiled sh_src/ (0 modules)
   compiling ciao_builder (command)
   compiling ciao_publish (command)
=> typeslib: building [bin]
   compiled src/ (5 modules)
=> ciao_emacs: building [bin]
   compiling ciao-emacs (command)
=> ciao_emacs.emacs_mode: building [bin]
Loading /etc/emacs/site-start.d/00debian.el (source)...
Loading /etc/emacs/site-start.d/50autoconf.el (source)...
Loading /etc/emacs/site-start.d/50dictionaries-common.el (source)...
Loading debian-ispell...
Loading /var/cache/dictionaries-common/emacsen-ispell-default.el (source)...
Loading /var/cache/dictionaries-common/emacsen-ispell-dicts.el (source)...
Loading /etc/emacs/site-start.d/50git-core.el (source)...
git removed but not purged, skipping setup
  INFO     Scraping files for ciao-site-file.el... 
  INFO     Scraping files for ciao-site-file.el...done
Loading /etc/emacs/site-start.d/00debian.el (source)...
Loading /etc/emacs/site-start.d/50autoconf.el (source)...
Loading /etc/emacs/site-start.d/50dictionaries-common.el (source)...
Loading debian-ispell...
Loading /var/cache/dictionaries-common/emacsen-ispell-default.el (source)...
Loading /var/cache/dictionaries-common/emacsen-ispell-dicts.el (source)...
Loading /etc/emacs/site-start.d/50git-core.el (source)...
git removed but not purged, skipping setup
Source file ‘<mypath>/.ciaoroot/v1.25.0-m1/ciao_emacs/elisp/ciao-config.el’ newer than byte-compiled file; using older file

In end of data:
ciao-builder.el:252:1:Warning: the function ‘ciao-inferior-mode’ is not known
    to be defined.
=> lpdoc: preparing build [bin]
=> lpdoc: building [bin]
   compiled src/ (27 modules)
   compiled lib/ (4 modules)
   compiling lpdoc (command)
=> ciaofmt: building [bin]
   compiling ciaofmt (command)
=> ciao_ppl: preparing build [bin]
   auto-installing GMP (third party)
   gmp auto-installation: activate (already_done)
   auto-installing PPL (third party)
   ppl auto-installation: activate (already_done)
   configuring PPL interface
=> ciao_ppl: building [bin]
   compiled lib/ (1 modules)
=> ciaopp: preparing build [bin]
=> ciaopp: building [bin]
   compiled src/ (86 modules)
   compiled domains/ (66 modules)
   compiled lib/ (7 modules)
   compiled spec/ (43 modules)
   compiled batch/ (7 modules)
   compiling ciaopp-dump (command)
{Compiling <mypath>/.ciaoroot/v1.25.0-m1/ciaopp/spec/abs_exec_cond.pl
ERROR: (lns 185-191) Bad module qualification of input_user_interface/5, predicate not imported from module polyhedra
ERROR: (lns 185-191) Bad module qualification of less_or_equal/2, predicate not imported from module polyhedra
ERROR: Aborted module compilation
{ERROR: No handle found for thrown exception error(return_code(1,pcall(<mypath>/.ciaoroot/v1.25.0-m1/build/bin/ciaoc,[-x,-o,<mypath>/.ciaoroot/v1.25.0-m1/build/bin/ciaopp-dump,ciaopp-dump.pl],[env([CIAOALIASPATH=,CIAOROOT=<mypath>/.ciaoroot/v1.25.0-m1,CIAOHDIR=<mypath>/.ciaoroot/v1.25.0-m1/build/eng/ciaoengine/include,CIAOENGINE=<mypath>/.ciaoroot/v1.25.0-m1/build/eng/ciaoengine/objs/LINUXx86_64/ciaoengine]),cwd(<mypath>/.ciaoroot/v1.25.0-m1/ciaopp/cmds)])),process_join/1)}

The second one terminates successfully:
~/.ciaoroot/v1.25.0-m1$ ciao build --bin ciaopp

=> ciaopp: preparing build [bin]
=> ciaopp: building [bin]
   compiled src/ (86 modules)
   compiled domains/ (66 modules)
   compiled lib/ (7 modules)
   compiled spec/ (43 modules)
   compiled batch/ (7 modules)
   compiling ciaopp-dump (command)
   compiling ciaopp-batch (command)
   compiling ciaopp_master (command)
   compiling ciaopp_batch_report (command)
=> ciaopp.cmds: building [bin]
   compiling ciaopp (command)
=> ciaopp.ciaopp_client: building [bin]

[djurjo]

Hi Simone
Currently, when ciao_ppl is installed, some code is automatically
enabled in ciaopp but it still requires recompilation. It is
probably that incremental compilation is not fully detecting the
changes. Could you try ciao clean --bin ciaopp before and try
again?

[simonefulvio-rollini]

I tried that, unfortunately it did not help.
Based on the installation instructions, I also tried manually compiling from the sources, fetching ciao_ppl before the actual build, with this sequence of commands:

git clone https://github.com/ciao-lang/ciao
cd ciao
./ciao-boot.sh configure
./ciao-boot.sh fetch devenv
./ciao-boot.sh fetch ciao_ppl
./ciao-boot.sh build
./ciao-boot.sh install

Is this sequence correct?
I ran into the error we have already seen, during the build step, but I could conclude the process and generate the binaries:

   generating ciaopp_tutorials (manual)
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:exfilter(exfilter_lpdoc) does not exist}
ERROR: {Program ended with failure}
{ERROR: No handle found for thrown exception  
...

Now, going back to the example we discussed:

:- module(test5_v2, [p1/2], [assertions,nativeprops]).
%:- use_module(domain(polyhedra)).
%:- use_module(library(ppl)).

:- entry p1(X,Y) : (int(X), constraint([X>=5, X=<10])).
:- check success p1(X,Y) => (int(Y), constraint([Y>=8, Y=<13])).
p1(X,Y) :- p2(X,Y). 

:- trust pred p2(X,Y) : (int(X)) => (constraint([Y=X+3])).
p2(1,4).

Analyzing it, I got the following error:
{ERROR: ppl:ppl_initialize/0 - existence error: procedure:ppl:ppl_initialize/0 does not exist}

Then I deleted everything, started again from scratch, and tried to add the ciao_ppl bundle after the build:

git clone https://github.com/ciao-lang/ciao
cd ciao
./ciao-boot.sh configure
./ciao-boot.sh fetch devenv
./ciao-boot.sh build
./ciao-boot.sh fetch ciao_ppl
./ciao-boot.sh build ciao_ppl

This led to the warning we have already encountered: '{WARNING (auto_interface): Domain polyhedra is unavailable in this build (please use full CiaoPP version)}'.

After this, I went back to your advice and tried:

./ciao-boot.sh build --bin ciao_ppl
./ciao-boot.sh build --bin ciaopp

with the second command giving the error we saw about bad module qualification and predicate not imported from module polyhedra.

Then, I ran:

./ciao-boot.sh clean --bin ciaopp
./ciao-boot.sh build --bin ciaopp

No error was raised. I then started ciao-emacs and analyzed the Prolog example. Here is the output:

{ERROR: dynlink(<myhome>/.ciao/build/cache/ciao_ppl.lib.ppl.ppl_LINUXx86_64.so, ppl): could not load library
 libppl.so.15: cannot open shared object file: No such file or directory)}
Ciao 1.25.0 (2025-06-21 10:37:14 +0200) [LINUXx86_64]
ciaopp ?- auto_check_assert('<myhome>/Documents/logicprogramming/Examples/test5_v2.pl').
{NOTE (frontend_driver): uncached library sources (enable with 'ciaopp --gen-lib-cache')}
{Loading current module from <myhome>/Documents/logicprogramming/Examples/test5_v2.pl
{loaded in 83.517 msec.}
}
{Analyzing (eterms): [<myhome>/Documents/logicprogramming/Examples/test5_v2.pl]
{init for the plai fixpoint in 0.079 msec.}
{preprocessed for the plai fixpoint in 0.129 msec.}
{fixpoint reached by plai using eterms with local-control off in 0.636 msec.}
{analyzed by plai in 1.119 msec.}
}
{Analyzing (polyhedra): [<myhome>/Documents/logicprogramming/Examples/test5_v2.pl]
{init for the plai fixpoint in 0.042 msec.}
{preprocessed for the plai fixpoint in 0.098 msec.}
{ERROR: ppl:ppl_initialize/0 - existence error: procedure:ppl:ppl_initialize/0 does not exist}

aborted

Enabling 'use_module(library(ppl))' made the situation worse:

{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:<myhome>/.ciaoroot/v1.25.0-m1/core/engine/arithmetic does not exist}
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:<myhome>/.ciaoroot/v1.25.0-m1/core/engine/atomic_basic does not exist}
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:<myhome>/.ciaoroot/v1.25.0-m1/core/engine/basiccontrol does not exist}
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:<myhome>/.ciaoroot/v1.25.0-m1/core/engine/exceptions does not exist}
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:<myhome>/.ciaoroot/v1.25.0-m1/core/engine/term_basic does not exist}
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:<myhome>/.ciaoroot/v1.25.0-m1/core/engine/term_compare does not exist}
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:<myhome>/.ciaoroot/v1.25.0-m1/core/engine/term_typing does not exist}
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:<myhome>/.ciaoroot/v1.25.0-m1/core/engine/basic_props does not exist}
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:<myhome>/.ciaoroot/v1.25.0-m1/core/engine/hiord_rt does not exist}
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:<myhome>/.ciaoroot/v1.25.0-m1/core/lib/foreign_interface/foreign_interface_properties does not exist}
{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:<myhome>/.ciaoroot/v1.25.0-m1/core/engine/debugger_support does not exist}

The impression I get is that somehow the files are searched in the default folder of the network-based installation, that is '.ciaoroot'.

Could you please suggest a sequence of commands, starting from cloning the repository, that works for you and allows to analyze examples with occurrences of the 'constraint' predicate, and examples making use of predicates from the PPL Prolog interface?