### Interactive Configuration and Stored Profiles

Source: https://github.com/ciao-lang/ciaopp/blob/master/cmds/README.md

Shows how to use the interactive menu (-Q) to define a configuration and subsequently apply that saved configuration (-U) to a Prolog file.

```bash
# Interactively configure
ciaopp -Q ~/PrologTemp/fact.pl

# Use a saved configuration named 'default'
ciaopp -U default ~/PrologTemp/fact.pl
```

--------------------------------

### Install and Configure CiaoPP

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

Commands to install the CiaoPP bundle using the Ciao package manager and generate the library cache for optimized performance.

```bash
ciao get ciaopp
ciaopp --gen-lib-cache
```

--------------------------------

### Analyze and Optimize Prolog files via CLI

Source: https://github.com/ciao-lang/ciaopp/blob/master/cmds/README.md

Standard command-line interface usage for performing analysis (-A) or optimization (-O) on a target Prolog file.

```bash
ciaopp -A ~/PrologTemp/fact.pl
ciaopp -O ~/PrologTemp/fact.pl
```

--------------------------------

### Configure Analysis Flags

Source: https://github.com/ciao-lang/ciaopp/blob/master/cmds/README.md

Demonstrates how to modify default analysis behavior using specific flags, such as setting mode domains or disabling specific analysis types.

```bash
ciaopp -A ~/PrologTemp/fact.pl -fmodes=pd
ciaopp -A ~/PrologTemp/fact.pl -ftypes=none
```

--------------------------------

### Configure Analysis Domains via CLI

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

Examples of overriding default analysis domains using the -f flag to specify custom types or modes. Multiple domains can be combined or disabled as needed.

```bash
# Custom type domain
ciaopp -A myfile.pl -ftypes=terms

# Custom mode domain
ciaopp -A myfile.pl -fmodes=pd

# Disable types
ciaopp -A myfile.pl -ftypes=none
```

--------------------------------

### Verify Arithmetic Assertion in CiaoPP

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/qsort_without_assertions--V--filter=warnings.txt

Example of a CiaoPP assertion check for arithmetic comparison operators. These assertions require non-variable inputs and valid arithmetic expressions to verify successfully.

```prolog
:- check calls B=<A
   : ( nonvar(B), nonvar(A), arithexpression(B), arithexpression(A) ).

:- check calls B>A
   : ( nonvar(B), nonvar(A), arithexpression(B), arithexpression(A) ).
```

--------------------------------

### Define Prolog Regular Type Assertions

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/power_without_assertions--V--filter=warnings.txt

Examples of regular type definitions used in CiaoPP to specify the structure of terms. These types are used by the analyzer to validate inputs for arithmetic operations.

```prolog
:- regtype rt188/1.
rt188(0).

:- regtype rt201/1.
rt201(A*B) :-
    term(A),
    term(B).
```

--------------------------------

### Define arithmetic assertion verification types in Ciao Prolog

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/power_without_assertions1--V--filter=warnings.txt

Example of a regular type definition used by CiaoPP to verify arithmetic expressions. This snippet illustrates how complex terms are validated during static analysis.

```prolog
:- regtype rt201/1.
rt201(A*B) :-
    term(A),
    term(B).
```

--------------------------------

### Declare arithmetic assertion checks in Ciao Prolog

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/power_without_assertions1--V--filter=warnings.txt

Examples of check assertions used in CiaoPP to enforce constraints on arithmetic operations. These assertions define the expected state of variables before arithmetic evaluation.

```prolog
:- check calls B=<A : ( nonvar(B), nonvar(A), arithexpression(B), arithexpression(A) ).
:- check calls B>A : ( nonvar(B), nonvar(A), arithexpression(B), arithexpression(A) ).
:- check calls A is B : ( ( var(A), nonvar(B), var(A), arithexpression(B) ); ( var(A), nonvar(B), var(A), intexpression(B) ) ).
:- check calls A=\=B : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
```

--------------------------------

### Type Checking Assertion Failure in Ciao/Ciaopp Compiler

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/remove_power_bug3--V--filter=warn_error.txt

This error from the Ciao/Ciaopp compiler's type checker (ctchecks_pp_messages) highlights a failed assertion related to variable types or properties. The provided example shows a failure in an assertion checking for inequality (A=\=B) when variables A and B are expected to be non-variable, arithmetic expressions, but one of them is of type rt2(B) where rt2 is defined as power1.

```ciao
ERROR (ctchecks_pp_messages): (lns 4-5) At literal 1 false assertion:
:- check calls A=\=B
   : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
because on call arithmetic:=\=(A,B) :

[eterms] basic_props:term(A),rt2(B) 
with:

:- regtype rt2/1.
rt2(power1).
```

--------------------------------

### Interactive Preprocessing with CiaoPP

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

The `customize_and_preprocess/1` predicate initiates an interactive menu for configuring and preprocessing a program. `customize/0` allows customizing settings without preprocessing. Menu configurations can be saved and restored using `save_menu_config/1` and `restore_menu_config/1`, respectively, and listed with `show_menu_configs/0`.

```prolog
% Interactive configuration and preprocessing
?- customize_and_preprocess('myfile.pl').

% Just customize settings without preprocessing
?- customize.

% Save/restore menu configurations
?- save_menu_config(my_settings).
?- restore_menu_config(my_settings).
?- show_menu_configs.
```

--------------------------------

### Execute CiaoPP Analysis Workflow

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

A step-by-step interactive workflow for loading a module, performing specific analyses (mode, type, non-failure), checking assertions, and exporting the results.

```prolog
?- module('myprogram.pl').
?- analyze(shfr).
?- analyze(eterms).
?- analyze(nf).
?- acheck.
?- output('myprogram_analyzed.pl').
?- dump('myprogram.dump').
```

--------------------------------

### Interactive Configuration and Shell

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

Methods for using the interactive menu to save configurations or launching the CiaoPP top-level shell for advanced, session-based operations.

```bash
# Interactive menu configuration
ciaopp -Q myfile.pl

# Use saved configuration
ciaopp -U my_config myfile.pl

# Start interactive shell
ciaopp -T
```

--------------------------------

### Generate Output Files with CiaoPP

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

The `output/0` and `output/1` predicates generate output files for the preprocessed program. `output/0` creates a file with an auto-generated name based on analysis history. `output/1` allows specifying a filename. `output/2` supports additional options for controlling the output.

```prolog
% Output with auto-generated filename based on analysis history
?- output.
% Creates: myfile_eterms_shfr_co.pl (based on analyses performed)

% Output to specific filename
?- output('result.pl').

% output/2 with options
?- output(File, [output_symlink, add_srcloc_prop]).
```

--------------------------------

### Perform CLI Analysis and Optimization

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

Standard command-line operations for analyzing Prolog files, verifying assertions, and applying program optimizations. These commands generate output files containing inferred properties or transformed code.

```bash
# Basic analysis
ciaopp -A myfile.pl

# Verify assertions
ciaopp -o myfile_checked.pl -V myfile.pl

# Optimize program
ciaopp -O myfile.pl
```

--------------------------------

### Programmatic Module Loading and Analysis

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

Prolog API functions for loading modules into the CiaoPP environment and performing abstract analysis using specific domains like sharing, types, or determinism.

```prolog
% Load modules
?- module('examples/qsort.pl').
?- module(['module1.pl', 'module2.pl']).

% Perform analysis
?- analyze(shfr).
?- analyze([shfr, eterms, nf, det]).
```

--------------------------------

### Define Predicate Assertions in Prolog

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

Demonstrates how to use the 'assertions' and 'nativeprops' libraries to define preconditions and postconditions for Prolog predicates. These assertions help CiaoPP verify properties like groundness, list structure, and computational success.

```prolog
:- module(qsort, [qsort/2], [assertions, nativeprops]).

:- pred qsort(X, Y)
   : (ground(X), list(X), var(Y))
   => (ground(Y), list(Y))
   + not_fails.

qsort([], []).
qsort([H|T], Sorted) :- 
    partition(T, H, Less, Greater),
    qsort(Less, SortedLess),
    qsort(Greater, SortedGreater),
    append(SortedLess, [H|SortedGreater], Sorted).
```

--------------------------------

### Verify Computational Properties

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

Illustrates how to assert determinism and non-failure properties for recursive predicates like factorial, ensuring the function behaves predictably.

```prolog
:- pred fact(N, F)
   : (integer(N), N >= 0, var(F))
   => integer(F)
   + (not_fails, is_det).

fact(0, 1) :- !.
fact(N, F) :- N > 0, N1 is N - 1, fact(N1, F1), F is N * F1.
```

--------------------------------

### Check partition Predicate Success Conditions and Determinism

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/bugqsort_assertions--V--output=on--filter=check_pred.txt

Defines the success conditions for the partition predicate, ensuring the third argument is a list of numbers and the fourth is ground. It also asserts that the predicate is deterministic.

```ciao-pp
:- checked success partition(A,B,C,D)
   => ( list(num,C), ground(D) ).

:- checked comp partition(_A,_B,_C,_D)
   + is_det.
```

--------------------------------

### Save and Load Analysis Results with CiaoPP

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

The `dump/1` and `restore/1` predicates allow persisting analysis results to disk for later reuse. `dump/1` saves the current analysis state, and `restore/1` loads it, avoiding the need for re-analysis. `show_dump/1` can be used to inspect the contents of a dump file.

```prolog
% Analyze and save results to disk
?- module('large_program.pl').
?- analyze(shfr).
?- analyze(eterms).
?- dump('analysis_cache.dump').

% Later, restore without re-analyzing
?- restore('analysis_cache.dump').
?- acheck.  % Uses restored analysis info

% Show contents of a dump file
?- show_dump('analysis_cache.dump').
```

--------------------------------

### CiaoPP Abstract Domains for Analysis

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

CiaoPP supports various abstract domains for program analysis. These include domains for mode and sharing analysis (e.g., `shfr`, `share`, `gr`), type analysis (e.g., `eterms`, `ptypes`), and numeric/other analyses (e.g., `nf`, `det`, `polyhedra`). The `analyze/1` predicate is used to invoke these domains.

```prolog
% Sharing + Freeness (default for modes)
?- analyze(shfr).

% Pure sharing analysis
?- analyze(share).

% Groundness analysis
?- analyze(gr).

% Definiteness analysis
?- analyze(def).

% Possible definiteness
?- analyze(pd).

% Sharing with AMGU (Abstract Most General Unifier)
?- analyze(share_amgu).

% Sharing with clique-based representation
?- analyze(share_clique).

% Combined sharefree with AMGU
?- analyze(sharefree_amgu).

% Sondergaard's domain
?- analyze(son).

% Extended types (default)
?- analyze(eterms).

% Parametric types
?- analyze(ptypes).

% Set-valued terms
?- analyze(svterms).

% Basic terms domain
?- analyze(terms).

% Defined types
?- analyze(deftypes).

% Non-failure analysis
?- analyze(nf).

% Non-failure with groundness
?- analyze(nfg).

% Determinism analysis
?- analyze(det).

% Polyhedra domain (numerical constraints)
?- analyze(polyhedra).

% Linear signs domain
?- analyze(lsign).

% Depth-k abstraction
?- analyze(depthk).
```

--------------------------------

### Apply Program Transformations in CiaoPP

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

The `transform/1` predicate applies various source-to-source transformations to the loaded program. Available transformations include specialization, simplification, code generation, slicing, argument filtering, and unfolding entry points. A list of all available transformations can be obtained by calling `transform(T)`.

```prolog
% Program specialization based on analysis info
?- transform(spec).

% Program simplification
?- transform(simp).

% Code generation after specialization
?- transform(codegen).

% Program slicing
?- transform(slicing).

% Argument filtering optimization
?- transform(arg_filtering).

% Unfold entry points (for non-Prolog frontends)
?- transform(unfold_entry).

% List available transformations
?- transform(T).
% Returns: normalize, spec, simp, vers, codegen, codegen_af,
%          slicing, arg_filtering, granul, rtc, codegen_min, unfold_entry
```

--------------------------------

### Check partition Predicate Compilation and Calls

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/bugqsort_assertions--V--output=on--filter=check_pred.txt

Specifies compilation checks and checked calls for the partition predicate. It ensures that partition is called with ground arguments and a numeric second argument, and that it does not fail.

```ciao-pp
:- checked comp partition(_A,_B,_C,_D)
   + not_fails.

:- checked calls partition(A,B,C,D)
   : ( ground(A), num(B) ).
```

--------------------------------

### Check qsort Calls and Success Conditions

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/bugqsort_assertions--V--output=on--filter=check_pred.txt

Defines the checked calls and success conditions for the qsort predicate. It specifies that qsort is called with list arguments and succeeds with a list of numbers.

```ciao-pp
:- checked calls qsort(A,B)
   : list_num(A).

:- checked success qsort(A,B)
   => list_num(B).
```

--------------------------------

### Automatic Analysis Pipeline in CiaoPP

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

The `auto_analyze/1` predicate performs a complete analysis pipeline automatically using configured domains. `auto_analyze/2` additionally returns detailed statistics about the analysis process.

```prolog
% Automatically analyze with configured domains
?- auto_analyze('myfile.pl').

% auto_analyze/2 returns detailed statistics
?- auto_analyze('myfile.pl', Info).
```

--------------------------------

### Automatic Optimization in CiaoPP

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

The `auto_optimize/1` predicate automates the process of loading, analyzing, and optimizing a program. This provides a streamlined way to apply optimizations based on program analysis.

```prolog
% Complete optimization pipeline
?- auto_optimize('myfile.pl').
```

--------------------------------

### Define Static Analysis Assertions for nrev

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/revf_n_ub_det_verified--V--output=on--filter=check_pred.txt

These assertions define the call, success, and computational complexity properties for the naive reverse predicate. They specify that the input must be a list of numbers and the output is a list, while providing an exponential upper bound on steps.

```Ciao Prolog
:- checked calls nrev(A,B)
   : ( list(num,A), var(B) ).

:- checked success nrev(A,B)
   : ( list(num,A), var(B) )
   => list(B).

:- checked comp nrev(A,B)
   : ( list(num,A), var(B) )
   + ( det, terminates, steps_ub(exp(length(A),2)) ).
```

--------------------------------

### Define qsort Predicate in Ciao PP

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/qsort2--A--ana_nf=nfdet--ana_cost=resources--name=qsort--assertion=[cost,lb]--filter=tpred_plus.txt

Defines the 'qsort' predicate, specifying that it operates on a list of numbers and produces a sorted list. It includes type constraints and a cost model.

```ciaopp
:- true pred qsort(A,B)
   : ( list(num,A), var(B) )
   => ( list(num,A), list(num,B),
        size(lb,length,B,1) )
   + cost(lb,steps,0).
```

--------------------------------

### Define Custom Types and Assertions

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

Shows the use of 'regtype' to define custom data structures like binary trees and applying these types within predicate assertions to ensure type safety.

```prolog
:- module(trees, [btree/1, insert/3], [assertions, regtypes]).

:- regtype btree/1.
btree(empty).
btree(node(L, _, R)) :- btree(L), btree(R).

:- pred insert(X, T1, T2)
   : (ground(X), btree(T1), var(T2))
   => btree(T2)
   + (not_fails, is_det).

insert(X, empty, node(empty, X, empty)).
insert(X, node(L, Y, R), node(NL, Y, R)) :- X @< Y, !, insert(X, L, NL).
insert(X, node(L, Y, R), node(L, Y, NR)) :- insert(X, R, NR).
```

--------------------------------

### Define CiaoPP assertions for naive reverse (nrev)

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/revf_n_o_det_verified--V--output=on--filter=check_pred.txt

Defines static analysis assertions for the nrev predicate. It specifies input types, success conditions, and computational complexity bounds including determinacy and termination.

```Ciao Prolog
:- checked calls nrev(A,B)
   : ( list(num,A), var(B) ).

:- checked success nrev(A,B)
   : ( list(num,A), var(B) )
   => list(B).

:- checked comp nrev(A,B)
   : ( list(num,A), var(B) )
   + ( det, terminates, steps_o(exp(length(A),2)) ).
```

--------------------------------

### Automatic Assertion Checking in CiaoPP

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

The `auto_check_assert/1` predicate automates the complete assertion checking pipeline, including loading, analysis, and checking. `auto_check_assert/2` provides detailed statistics of the process.

```prolog
% Complete assertion checking pipeline
?- auto_check_assert('myfile.pl').

% With statistics
?- auto_check_assert('myfile.pl', Info).
```

--------------------------------

### Checked Calls for nrev Predicate in Ciaopp

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/nrev3--V--output=on--asr_not_stat_eval=warning--ctchecks_intervals=off--filter=check_pred.txt

Defines the conditions under which the nrev predicate is considered 'checked'. This involves ensuring that the first argument (A) is ground and a list, and the second argument (B) is a variable. This is crucial for static analysis and optimization.

```prolog
:- checked calls nrev(A,B)
   : ( ground(A), list(A), var(B) ).
```

--------------------------------

### Define Checked Calls for app Predicate in Ciao PP

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/app--V--output=on--filter=check_pred.txt

This snippet defines the expected argument types for calls to the 'app(A, B, C)' predicate. It specifies that arguments A and B must be lists. This helps in static analysis and error checking.

```ciaopp
:- checked calls app(A,B,C)
   : ( list(A), list(B) ).
```

--------------------------------

### Define CiaoPP predicate assertions for qsort

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/qsort--A--ana_nf=nf--name=qsort--filter=tpred_plus.txt

This snippet defines the CiaoPP assertion for the quicksort predicate. It specifies that for a given list of numbers, the predicate will produce a sorted list, ensuring the process does not fail and is fully covered by the analysis.

```Ciao Prolog
:- true pred qsort(A,B)
   : ( mshare([[B]]),
       var(B), ground([A]), list(num,A), term(B) )
   => ( ground([A,B]), list(num,A), list(num,B) )
   + ( not_fails, covered ).
```

--------------------------------

### Define nrev predicate assertions in CiaoPP

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/revf_n_o_det_error--V--output=on--name=nrev--assertion=[steps_lb]--filter=tpred_plus.txt

This snippet defines a CiaoPP assertion for the 'nrev' (naive reverse) predicate. It specifies input/output types, size relationships between the input and output lists, and provides lower and upper bounds for computational steps based on list length.

```Ciao
:- true pred nrev(A,B)
   : ( list(num,A), var(B) )
   => ( list(num,A), list(num,B),
        size_lb(length,B,length(A)),
        size_ub(length,B,length(A)) )
   + ( steps_lb(0.5*exp(length(A),2)+1.5*length(A)+1), steps_ub(0.5*exp(length(A),2)+1.5*length(A)+1) ).
```

--------------------------------

### Ciaopp: False Success for app Predicate

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/app_assrt_false--V--output=on--filter=check_pred.txt

Defines the false success condition for the 'app' predicate in Ciaopp. This condition is met when the first two arguments are lists and the third argument 'C' is a variable. It indicates that the predicate will not succeed if 'C' is uninstantiated under these list conditions.

```ciaopp
:- false success app(A,B,C)
   : ( list(A), list(B) )
   => var(C).
```

--------------------------------

### Asserting Complexity Constraints in Ciao

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/nrev2--V--asr_not_stat_eval=warning--ctchecks_intervals=off--filter=errors.txt

This snippet demonstrates a Ciao assertion used to define complexity bounds for the nrev predicate. It specifies that the number of steps should be proportional to the length of the input list, which triggered a verification error due to a mismatch with inferred complexity metrics.

```Ciao
:- check comp nrev(A,B)
   + steps_o(length(A)).
```

--------------------------------

### Compilation Optimization for nrev Predicate in Ciaopp

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/nrev3--V--output=on--asr_not_stat_eval=warning--ctchecks_intervals=off--filter=check_pred.txt

Specifies compilation optimizations for the nrev predicate. It includes an optimization step that expands the length of the first argument (A) to 2. This is a form of partial evaluation or specialization aimed at improving performance.

```prolog
:- checked comp nrev(A,B)
   + steps_o(exp(length(A),2)).
```

--------------------------------

### Check Assertions with CiaoPP

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

The `acheck` predicate in CiaoPP checks program assertions against current analysis information. It can be used without arguments to check all available information, or with a specific domain like `shfr` or `eterms`. The `acheck_summary` predicate provides a summary of the results.

```prolog
% Load module and analyze
?- module('myfile.pl').
?- analyze(shfr).
?- analyze(eterms).

% Check assertions using all available analysis info
?- acheck.

% Check with specific domain
?- acheck(shfr).

% Get summary of assertion checking results
?- acheck_summary(Summary).
% Summary = ok | warning | error
```

--------------------------------

### Define 'app' Predicate Type Constraints (Ciao PP)

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/app_assrt_false--A--filter=tpred.txt

This definition sets the type constraints for the 'app' predicate. It asserts that the first two arguments (A and B) must be lists, and the third argument (C) must be a term. The output constraint ensures that C will also be a list, consistent with list concatenation operations.

```Ciao PP
:- true pred app(A,B,C)
   : ( list(A), list(B), term(C) )
   => ( list(A), list(B), list(C) ).
```

--------------------------------

### Define Checked Success for app Predicate in Ciao PP

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/app--V--output=on--filter=check_pred.txt

This snippet defines the expected return type for successful calls to the 'app(A, B, C)' predicate. It indicates that when the predicate succeeds, argument C must be a list, given that A and B are also lists. This is useful for verifying program correctness.

```ciaopp
:- checked success app(A,B,C)
   : ( list(A), list(B) )
   => list(C).
```

--------------------------------

### Define CiaoPP assertions for qsort

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/qsort_assrt_det--V--ana_det=nfdet--output=on--filter=check_pred.txt

Specifies the call, success, and computational properties for the qsort predicate. It ensures the input is a list of numbers and defines the determinacy as semidet.

```Ciao
:- checked calls qsort(_A,_B)
   : list(num,_A).

:- checked success qsort(_A,_B)
   : list(num,_A)
   => list(num,_B).

:- checked comp qsort(_A,_B)
   : list(num,_A)
   + semidet.
```

--------------------------------

### Manage CiaoPP Preprocessor Flags

Source: https://context7.com/ciao-lang/ciaopp/llms.txt

Preprocessor flags in CiaoPP control its behavior. You can query the current value of a flag using `current_pp_flag/2`, set a flag using `set_pp_flag/2`, or temporarily push a value using `push_pp_flag/2` and `pop_pp_flag/1`. `pp_flag/1` lists all valid flags, and `valid_flag_value/2` checks flag value validity.

```prolog
% Get current value of a flag
?- current_pp_flag(types, Value).
% Value = eterms

% Set a flag value
?- set_pp_flag(types, terms).

% Temporarily push a flag value (restore with pop_pp_flag)
?- push_pp_flag(pp_info, on).
?- pop_pp_flag(pp_info).

% List all valid flags
?- pp_flag(F).

% Check if value is valid for a flag
?- valid_flag_value(types, eterms).
```

--------------------------------

### Define CiaoPP Assertions for powers/3

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/powers--V--output=on--filter=check_pred.txt

These assertions define the expected behavior and properties of the powers/3 predicate. It includes success conditions for input types, computational guarantees like non-failure, and call pattern validation.

```Ciao Prolog
:- check success powers(A,B,C)
   : ( list_nnegint(A), nnegint(B), var(C) )
   => ( list_nnegint(C), sorted(C) ).

:- check comp powers(A,B,C)
   : ( list_nnegint(A), nnegint(B), var(C) )
   + not_fails.

:- checked calls powers(A,B,C)
   : ( list_nnegint(A), nnegint(B), var(C) ).
```

--------------------------------

### Analyze nrev Calls and Success Conditions (CiaoPP)

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/revf_n_o_det_error--V--output=on--filter=check_pred.txt

Defines analysis directives for the 'nrev' predicate. 'checked calls' specifies the expected call pattern and its types. 'checked success' defines the success pattern and output types. 'false comp' indicates that the predicate does not succeed under the given conditions and specifies computational properties.

```ciaopp
:- checked calls nrev(A,B)
   : ( list(num,A), var(B) ).

:- checked success nrev(A,B)
   : ( list(num,A), var(B) )
   => list(B).

:- false comp nrev(A,B)
   : ( list(num,A), var(B) )
   + ( det, terminates, steps_o(length(A)) ).
```

--------------------------------

### Define 'app' Predicate Sharing Properties (Ciao PP)

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/app_assrt_false--A--filter=tpred.txt

This definition specifies the sharing properties for the 'app' predicate, which is commonly used for list concatenation. It outlines how the sharing of variables in the input arguments (A, B, C) relates to the sharing in the output. This is crucial for program analysis and optimization.

```Ciao PP
:- true pred app(A,B,C)
   : mshare([[A],[A,B],[A,B,C],[A,C],[B],[B,C],[C]])
   => mshare([[A,B,C],[A,C],[B,C]]).
```

--------------------------------

### Define sorted_insert predicate assertions in CiaoPP

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/sorted_insert_multi--A--ana_det=nfdet--name=sorted_insert--filter=tpred_plus.txt

This snippet defines the pre-conditions and post-conditions for the sorted_insert predicate. It uses CiaoPP assertion syntax to specify that the third argument must be a variable initially and becomes a ground list after execution.

```prolog
:- true pred sorted_insert(A,B,C)
   : ( mshare([[C]]),
       var(C), ground([A,B]), list_pair(A), num_pair(B), term(C) )
   => ( ground([A,B,C]), list_pair(A), num_pair(B), list_pair1(C) )
   + ( multi, covered, possibly_not_mut_exclusive ).
```

--------------------------------

### Define CiaoPP Predicate Assertions

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/qsort--A--types=none--modes=shfr--filter=tpred.txt

These assertions define the expected behavior and sharing properties for logic predicates. They specify the input/output grounding requirements and variable sharing constraints for the CiaoPP static analyzer.

```Ciao Prolog
:- true pred qsort(A,B)
   : ( mshare([[B]]),
       var(B), ground([A]) )
   => ground([A,B]).

:- true pred partition(_A,_1,Y1,Y2)
   : ( mshare([[Y1],[Y2]]),
       var(Y1), var(Y2), ground([_A,_1]) )
   => ground([_A,_1,Y1,Y2]).

:- true pred append(_A,X,_B)
   : ( mshare([[_B]]),
       var(_B), ground([_A,X]) )
   => ground([_A,X,_B]).
```

--------------------------------

### Define CiaoPP assertions for partition

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/qsort_assrt_det--V--ana_det=nfdet--output=on--filter=check_pred.txt

Specifies the call, success, and computational properties for the partition predicate. It validates that the input is a list of numbers and a pivot number, resulting in two lists of numbers.

```Ciao
:- checked calls partition(_A,_B,_C,_D)
   : ( list(num,_A), num(_B) ).

:- checked success partition(_A,_B,_C,_D)
   : ( list(num,_A), num(_B) )
   => ( list(num,_C), list(num,_D) ).

:- checked comp partition(_A,_B,_C,_D)
   : ( list(num,_A), num(_B) )
   + det.
```

--------------------------------

### Define CiaoPP Assertions for sorted_insert

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/sorted_insert_multi--V--comments=on--output=on--filter=check_pred.txt

Defines check, calls, and success assertions for the sorted_insert predicate. These assertions specify input types (list_pair, num_pair) and output properties (list_pair1) to enable static analysis and verification.

```Ciao Prolog
%% %% :- check pred sorted_insert(A,B,C)
%% %%    : ( list_pair(A), num_pair(B), var(C) )
%% %%    => list_pair1(C).

:- checked calls sorted_insert(A,B,C)
   : ( list_pair(A), num_pair(B), var(C) ).

:- checked success sorted_insert(A,B,C)
   : ( list_pair(A), num_pair(B), var(C) )
   => list_pair1(C).
```

--------------------------------

### Define Predicate Assertions in CiaoPP

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/power_without_assertions3--V--output=on--comments=on--filter=check_pred.txt

Defines the static analysis assertions for the 'powers' predicate. It specifies the input types for arguments A, B, and C, and defines the expected success state where the output C is a list of numbers.

```prolog
%% :- check pred powers(A,B,C)
%%    : ( list_num(A), num(B), var(C) )
%%    => list_num(C).

:- checked calls powers(A,B,C)
   : ( list_num(A), num(B), var(C) ).

:- checked success powers(A,B,C)
   : ( list_num(A), num(B), var(C) )
   => list_num(C).
```

--------------------------------

### Verify Assertion: A > B in CiaoPP

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/incompatible_type_f_fixed--V--filter=warn_error.txt

This snippet addresses a verification failure for the arithmetic assertion `A > B` in CiaoPP. The compilation process could not verify the necessary preconditions for the arithmetic comparison, specifically `nonvar(A)`, `nonvar(B)`, and `arithexpression(A)`, `arithexpression(B)`, based on the inferred terms.

```Ciao
WARNING (ctchecks_pp_messages): (lns 22-22) At literal 1 could not verify assertion:
:- check calls A>B
   : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
because on call arithmetic:>(A,B) :

[eterms] basic_props:term(A),basic_props:term(B),basic_props:term(A) 

[shfr]   native_props:mshare([[A],[A,B],[A,B,A],[A,A],[B],[B,A],[A]]) 

```

--------------------------------

### Ciaopp 'powers' Predicate Test with Small Numbers

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/power_testing--V--output=on--testing=on--filter=test.txt

This test case for the Ciaopp 'powers' predicate uses a list with small integers and a small integer exponent. It verifies the predicate's ability to compute powers correctly for these inputs and ensures the test passes without errors.

```ciaopp
:- checked test powers(A,B,C)
   : ( (A=[2,4]), (B=6) )
   => (C=[2,4,8,16,32,64])
   + not_fails.
```

--------------------------------

### Check Arithmetic Assertion

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/remove_power_bug1--V--filter=warn_error.txt

A static analysis assertion used to verify arithmetic expressions. It requires that both arguments are non-variable and valid arithmetic expressions before the inequality check is performed.

```prolog
:- check calls A=\=B
   : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
```

--------------------------------

### Define 'append' Predicate in Ciao/Ciaopp

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/qsort2--A--ana_nf=nf--ana_cost=resources--name=append--assertion=[cost,ub]--filter=tpred_plus.txt

Defines the 'append' predicate, which concatenates two lists. It specifies type constraints for input lists and the output list, ensuring type compatibility and calculating the output list's size based on the input lists. It also includes a cost model based on the length of the first list.

```ciao
:- true pred append(_A,X,_B)
   : ( list(num,_A), list1(num,X), var(_B) )
   => ( list(num,_A), list1(num,X), list1(num,_B),
        size(ub,length,_B,length(X)+length(_A)) )
   + cost(ub,steps,length(_A)+1).
```

--------------------------------

### Define CiaoPP assertions for append

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/qsort_assrt_det--V--ana_det=nfdet--output=on--filter=check_pred.txt

Specifies the call, success, and computational properties for the append predicate. It defines the input as two lists of numbers and the output as a single concatenated list of numbers.

```Ciao
:- checked calls append(_A,_B,_C)
   : ( list(num,_A), list(num,_B) ).

:- checked success append(_A,_B,_C)
   : ( list(num,_A), list(num,_B) )
   => list(num,_C).

:- checked comp append(_A,_B,_C)
   : ( list(num,_A), list(num,_B) )
   + semidet.
```

--------------------------------

### Auto-Interface Error Handling (Ciaopp)

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/app_assrt_false--V--filter=warn_error.txt

This snippet indicates an error detected during the automatic interface generation phase in the Ciaopp project. The presence of errors prevents further preprocessing, suggesting a critical issue in the interface definition or related code.

```ciao
ERROR (auto_interface): Errors detected. Further preprocessing aborted.
```

--------------------------------

### Define CiaoPP Assertions for Sorting and List Operations

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/bugqsort_assertions--V--output=on--simplify_checks=on--filter=check_pred.txt

These assertions specify the input requirements and output guarantees for sorting and list manipulation predicates. They utilize CiaoPP's checked calls and success directives to enforce type constraints and termination properties.

```prolog
:- checked calls qsort(A,B)
   : ( list(num,A) ).

:- check success qsort(A,B)
   => sorted_num_list(B).

:- checked calls partition(A,B,C,D)
   : ( ground(A), ground(B) ).

:- checked success partition(A,B,C,D)
   => ( list(num,C), ground(D) ).

:- checked comp partition(_A,_B,_C,_D)
   + not_fails.

:- checked comp partition(_A,_B,_C,_D)
   + det.

:- checked comp partition(A,B,C,D)
   + terminates.

:- check calls append(A,B,C)
   : list(num,B).
```

--------------------------------

### Define append predicate assertion in CiaoPP

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/qsort2--A--ana_nf=nfdet--ana_cost=resources--name=append--assertion=[cost,lb]--filter=tpred_plus.txt

This assertion specifies the behavior of the append predicate, defining input types as lists of numbers and output constraints. It includes a cost analysis annotation to track the number of steps based on list lengths.

```prolog
:- true pred append(_A,X,_B)
   : ( list(num,_A), list1(num,X), var(_B) )
   => ( list(num,_A), list1(num,X), list1(num,_B),
        size(lb,length,_B,length(X)+length(_A)) )
   + cost(lb,steps,0).
```

--------------------------------

### Assertion Failure in Predicate Check (Ciaopp)

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/app_assrt_false--V--filter=warn_error.txt

This snippet illustrates a false assertion error during predicate checking in the Ciaopp project. It highlights an incompatibility between the expected 'success' field and the inferred properties, specifically concerning list types for variables A, B, and C.

```ciao
ERROR (ctchecks_pred_messages): (lns 3-3) False assertion:
:- check success app(A,B,C)
   : ( list(A), list(B) )
   => var(C).
because the success field is incompatible with inferred success:
[eterms] basic_props:list(A),basic_props:list(B),basic_props:list(C)
```

--------------------------------

### Transform terms using term_to_fr in Ciao Prolog

Source: https://github.com/ciao-lang/ciaopp/blob/master/lib/term_filtering/fr_tests.txt

The term_to_fr/3 predicate takes an input term and a template term to produce a filtered result. The template uses binary values (1 to keep, 0 to filter) to determine which parts of the original term are included in the output structure.

```Prolog
?- term_to_fr(f(1,2,g(a,[7,8,9])),f(0,1,g(1,0)),FR).
% Output: FR = (f(2,g(a)),[1,[[7,8,9]]])

?- term_to_fr(p(f(a,b,c),5),p(f(1,0,0),0),FR).
% Output: FR = (p(f(a)),[[b,c],5])

?- term_to_fr(f(1,2,g(a,b,c,d),g(r([5,6,7,8],t))),f(0,1,g(1,0,0,1),g(r(1,0))),FR).
% Output: FR = (f(2,g(a,d),g(r([5,6,7,8]))),[1,[b,c],[[t]]])
```

--------------------------------

### Assertion Verification Failure in Ciaopp

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/incompatible_type_f_error--V--filter=warn_error.txt

This snippet illustrates a common warning from the Ciaopp preprocessor where an assertion could not be verified. It highlights issues with checking arithmetic expressions and non-variable terms.

```ciaopp
WARNING (ctchecks_pp_messages): (lns 22-22) At literal 1 could not verify assertion:
:- check calls A>B
   : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
because on call arithmetic:>(A,B) :

[eterms] basic_props:term(A),basic_props:term(B),basic_props:term(A) 

[shfr]   native_props:mshare([[A],[A,B],[A,B,A],[A,A],[B],[B,A],[A]]) 
```

--------------------------------

### CiaoPP Assertions for conc Predicate

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/revf_n_ub_det_error--V--output=on--filter=check_pred.txt

Specifies CiaoPP assertions for the 'conc' predicate, focusing on its compilation properties. It indicates that 'conc' is a deterministic predicate that terminates and provides an upper bound on its computational steps related to the length of its first argument.

```prolog
:- checked calls conc(A,B,C).

:- false comp conc(A,B,C)
   + ( det, terminates, steps_ub(length(A)) ).
```

--------------------------------

### Define Static Analysis Assertions for conc

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/revf_n_ub_det_verified--V--output=on--filter=check_pred.txt

These assertions define the call and computational complexity properties for the list concatenation predicate. It specifies that the operation is deterministic and terminates with a linear step complexity relative to the first list.

```Ciao Prolog
:- checked calls conc(A,B,C).

:- checked comp conc(A,B,C)
   + ( det, terminates, steps_ub(length(A)+1) ).
```

--------------------------------

### Analyze conc Predicate Properties (CiaoPP)

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/revf_n_o_det_error--V--output=on--filter=check_pred.txt

Specifies analysis directives for the 'conc' predicate. 'checked calls' defines the expected call pattern. 'checked comp' asserts computational properties such as determinacy, termination, and step bounds.

```ciaopp
:- checked calls conc(A,B,C).

:- checked comp conc(A,B,C)
   + ( det, terminates, steps_o(length(A)) ).
```

--------------------------------

### Verify Assertion: sorted(X) in CiaoPP

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/incompatible_type_f_fixed--V--filter=warn_error.txt

This snippet details a type checking failure in CiaoPP where the assertion `sorted(X)` could not be verified. The system inferred `rt27(X)` but could not derive the necessary properties for `sorted(X)` from it. This indicates a potential issue with type definitions or inference rules.

```Ciao
:- check success p(X)
   => sorted(X).
because
    incompatible_type_f_fixed:sorted(X)
could not be derived from inferred success:
[eterms] rt27(X) 
with:

:- regtype rt27/1.
rt27([A,B,C]) :-
    term(A),
    term(B),
    term(C).

[shfr]   native_props:mshare([[X]]) 

```

--------------------------------

### Define Regular Type for Power Expressions

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/remove_power_bug1--V--filter=warn_error.txt

Defines a regular type 'rt2' for the CiaoPP static analyzer to validate power-related terms. This ensures that the analyzer correctly identifies 'power1' as a valid term during type checking.

```prolog
:- regtype rt2/1.
rt2(power1).
```

--------------------------------

### Ciaopp 'powers' Predicate Test with Mixed Numbers

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/power_testing--V--output=on--testing=on--filter=test.txt

This test case for the Ciaopp 'powers' predicate uses a list with mixed integer values and an integer exponent. It checks the predicate's output for this scenario and confirms that the test completes successfully.

```ciaopp
:- checked test powers(A,B,C)
   : ( (A=[3,4,5]), (B=17) )
   => (C=[3,4,5,9,16,25,27,64,81,125,243,256,625,729,1024,2187,3125])
   + not_fails.
```

--------------------------------

### Define sorted_insert predicate assertion in CiaoPP

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/power_without_assertions3--A--absdomain=types--name=sorted_insert--filter=tpred.txt

This assertion defines the contract for the 'sorted_insert' predicate. It enforces that the input list contains pairs of numbers, the element to insert is of type 'rt96', and the output is a list of number pairs.

```Ciao Prolog
:- true pred sorted_insert(_A,X,_B)
   : ( list(^(('basic_props:num','basic_props:num')),_A), rt96(X), term(_B) )
   => ( list(^(('basic_props:num','basic_props:num')),_A), rt96(X), list1(^((num,num)),_B) ).
```

--------------------------------

### Ciaopp 'powers' Predicate Test with Large Numbers

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/power_testing--V--output=on--testing=on--filter=test.txt

This test case for the Ciaopp 'powers' predicate uses a list with a large number and a small integer. It verifies that the predicate correctly computes powers for the given inputs and does not result in any failures.

```ciaopp
:- checked test powers(A,B,C)
   : ( (A=[2,9999999,9999998]), (B=20) )
   => (C=[2,4,8,16,32,64,128,256,512,1024,2048,4096,8192,16384,32768,65536,131072,262144,524288,1048576])
   + not_fails.
```

--------------------------------

### Incompatible Success Field Error in Ciaopp

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/incompatible_type_f_error--V--filter=warn_error.txt

This snippet shows an error message from the Ciaopp preprocessor indicating a false assertion due to an incompatible success field. It relates to a predicate's inferred success not matching its defined success.

```ciaopp
ERROR (ctchecks_pred_messages): (lns 3-8) False assertion:
:- check success p(X)
   => sorted(X).
because the success field is incompatible with inferred success:
[eterms] rt27(X) 
with:

:- regtype rt27/1.
rt27(red).

ERROR (auto_interface): Errors detected. Further preprocessing aborted.
```

--------------------------------

### Arithmetic Assertion Failure in Ciao/Ciaopp Preprocessor

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/remove_power_bug3--V--filter=warn_error.txt

This error from the Ciao/Ciaopp preprocessor signifies that an arithmetic assertion within the code is failing. This often occurs when the types or values of variables in an arithmetic comparison are not as expected, leading to the assertion not being met.

```ciao
WARNING (preproc_errors): (lns 4-5) goal arithmetic:=\=(Power,power1) at literal 1 does not succeed!
WARNING (preproc_errors): (lns 6-7) goal remove_power_bug3:remove_power(Power,RestPFsIn,PFsOut) at literal 1 does not succeed!
```

--------------------------------

### Predicate Redefinition Warning in Ciao/Ciaopp

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/remove_power_bug3--V--filter=warn_error.txt

This warning indicates that a predicate with the same name and arity is being defined more than once in the Ciao/Ciaopp code. It is important to resolve these redefinitions to avoid unexpected behavior or compilation errors.

```ciao
WARNING: (lns 4-5) predicate remove_power/3 is already defined with arity 2
```

--------------------------------

### Ciao PP Error: Arithmetic Assertion Check Failure

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/remove_power_bug4--V--filter=errors.txt

This snippet details an error from the Ciao PP compiler related to a failed assertion check for arithmetic equality (A == B). It highlights the conditions under which the check fails, specifically when both A and B are non-variable and arithmetic expressions.

```ciao
ERROR (ctchecks_pp_messages): (lns 4-5) At literal 1 false assertion:
:- check calls A=\=B
   : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
because on call arithmetic:=\=(A,B) :

[eterms] basic_props:term(A),rt9(B)
```

--------------------------------

### Ciao PP Type Registration: rt9/1

Source: https://github.com/ciao-lang/ciaopp/blob/master/doc/tutorials/results/remove_power_bug4--V--filter=errors.txt

This snippet shows the registration of a new type or predicate named 'rt9' with an arity of 1 in the Ciao PP. This is often done to define custom types or properties used within the Ciao programming language.

```ciao
:- regtype rt9/1.
rt9(power1).
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.