## Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP ∗

## JOAQUÍN ARIAS and MANUEL CARRO

IMDEA Software Institute and Universidad Politécnica de Madrid joaquin.arias@{imdea.org,alumnos.upm.es}, manuel.carro@{imdea.org,upm.es}

submitted 1 January 2003; revised 1 January 2003; accepted 1 January 2003

## Abstract

CiaoPP is an analyzer and optimizer for logic programs, part of the Ciao Prolog system. It includes PLAI, a fixpoint algorithm for the abstract interpretation of logic programs which we adapt to use tabled constraint logic programming . In this adaptation, the tabling engine drives the fixpoint computation, while the constraint solver handles the LUB of the abstract substitutions of different clauses. That simplifies the code and improves performance, since termination, dependencies, and some crucial operations (e.g., branch switching and resumption) are directly handled by the tabling engine. Determining whether the fixpoint has been reached uses semantic equivalence , which can decide that two syntactically different abstract substitutions represent the same element in the abstract domain. Therefore, the tabling analyzer can reuse answers in more cases than an analyzer using syntactical equality. This helps achieve better performance, even taking into account the additional cost associated to these checks. Our implementation is based on the TCLP framework available in Ciao Prolog and is one-third the size of the initial fixpoint implementation in CiaoPP. Its performance has been evaluated by analyzing several programs using different abstract domains.

This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP).

KEYWORDS : Abstract Interpretation, Constraints, Tabling, Prolog, PLAI.

## 1 Introduction

Tabling (Tamaki and Sato 1986; Warren 1992) is an execution strategy for logic programs that suspends repeated calls which could cause infinite loops. Answers from non-looping branches are used to resume suspended calls which can, in turn, generate more answers and resume other suspended calls. Only new answers are saved, and evaluation finishes when no new answers can be generated. Tabled evaluation always terminates for calls/programs with the bounded term depth property (i.e., they can only generate terms with a fixed finite depth) and can improve efficiency for terminating programs which repeat computations, as it automatically implements a variant of dynamic programming. Tabling has been successfully applied in a variety of contexts, including deductive databases, program analysis, semantic Web reasoning, and model checking.

Constraint Logic Programming (CLP) (Jaffar and Maher 1994) extends Logic Programming (LP) with variables that can belong to arbitrary constraint domains and the ability to incrementally solve equations involving these variables. CLP brings additional expressive power

- ∗ Work partially supported by EIT Digital (https://eitdigital.eu), MINECO project TIN2015-67522-C3-1-R (TRACES), and Comunidad de Madrid project S2018/TCS-4339 BLOQUES-CM co-funded by EIE Funds of the European Union.

to LP, since constraints can very concisely capture complex relationships. Also, shifting from 'generate-and-test' to 'constraint-and-generate' patterns reduces the search tree and therefore brings additional performance, even if constraint solving is in general more expensive than unification.

The integration of tabling and constraint solvers makes it possible to exploit their synergy in several application fields: abstract interpretation (Swift and Warren 2010), reasoning on ontologies, and constraint-based verification (Gange et al. 2013). In this paper we use Mod TCLP (Arias and Carro 2019a) to adapt PLAI, the fixpoint algorithm implemented in the program analysis, optimization, and transformation tool CiaoPP (Hermenegildo et al. 2012; Hermenegildo et al. 2005). The re-implementation of PLAI uses tabling to reach the fixpoint (following ideas similar to (Kanamori and Kawamura 1993; Janssens and Sagonas 1998)), incremental aggregation techniques (Guo and Gupta 2008; Zhou et al. 2010; Swift and Warren 2010; Arias and Carro 2019b) to join the answers, by discarding the more particular ones, and call entailment checks (Chico de Guzmán et al. 2012; Arias and Carro 2019a) to detect repeated calls (in order to suspend execution to reuse answers from previous calls), thereby speeding up convergence. The resulting code space is reduced to one third and, consequently, increases the maintainability of the abstract interpreter.

## 2 Related Work

Abstract interpretation has always been seen as one of the most clear applications of tabled logic programming. It requires a fixpoint procedure, often implemented using memo tables and dependency tracking, which play a role very similar to the internal data structures that tabling engines need to detect repeated calls, store and reuse answers, and check for termination.

The relationship between abstract interpretation and tabling was recognized very early. Extension tables (Dietrich 1987) were proposed to record results from the execution of predicates and turn intensional definitions into extensional definitions. Their applications included 'improving the termination and completeness characteristics of depth-first evaluation strategies in the presence of recursion'. The idea of extension tables were applied as the embryo of SLG resolution and the XSB system. At the same time, abstract interpretation was then viewed as inefficient, and as part of the efforts to make it a practical technique to implement analyzers, tables, but also other ideas such as dependency tracking, were used (Warren et al. 1988), thus making it clear that a common underlying technology could be used in both types of systems.

The next step was to use these components, independently available in tabling systems, to explore how they could be used to build abstract interpreters. Earlier work (Kanamori and Kawamura 1993) explored the possibilities offered by OLDT (Tamaki and Sato 1986) to implement abstract interpretation. Using type inference as the guiding example, it suggests certain changes to OLDT and concludes that it is feasible to do abstract interpretation with OLDT. The paper neither describes an implementation nor reports performance, but it states that the abstract interpreter was implemented and was available. In (Warren 1999) an abstract interpreter written in XSB is presented as one of the applications of tabled Prolog.

However, surprisingly few examples of abstract interpreters implemented using tabling have been presented and evaluated w.r.t. implementations without tabling. One of them is a framework (Janssens and Sagonas 1998) based on abstract compilation that executes the abstract version of the program under analysis, together with domain-dependent abstract operations, which is evaluated using the tabling system XSB and compared with the AMAI and PLAI sys-

tems (Janssens et al. 1995; Muthukumar and Hermenegildo 1992). Both systems use abstract interpreters written in Prolog without tabling, but they rely on very different underlying technologies, and with different representations for the abstract domains. From that evaluation, the paper concludes that tabling is a viable infrastructure for abstract interpretation, but concedes that the PLAI fixpoint algorithm was the most efficient abstract interpreter for logic programming available at the moment. The very different underlying infrastructure makes it difficult to use these results to draw meaningful conclusions.

On the other hand, abstract interpretation has been used as a benchmark to compare different implementations and/or scheduling strategies of tabling (Demoen and Sagonas 1998; Freire et al. 2001). Advanced tabled systems and techniques have been proposed to implement more efficient abstract interpreters by using the least upper bound operator (Schrijvers et al. 2008) to combine answers, numeric constraint solvers (Chico de Guzmán et al. 2012) to implement the Octagon domain, and the partial order answer subsumption with abstraction (Swift and Warren 2010) for cases where, e.g., the program computed does not have a finite model. However, none of them reports performance evaluation against other frameworks.

In this paper we started with PLAI, the state-of-the-art abstract interpreter used by CiaoPP, and re-implemented its fixpoint procedure in Tabled CLP preserving the interface with the rest of the system. Therefore, we can compare some indicators of code complexity (e.g., comparing lines of code, with the assumption that the tabled version is essentially a subset of the original version) and performance on a completely equal footing. This is, to our best knowledge, the first comparison that has these characteristics.

## 3 Background

In this section we briefly describe Mod TCLP (Arias and Carro 2019a), a generic interface that facilitates the integration of constraint solvers with the tabling engine in Ciao, Aggregate-TCLP (Arias and Carro 2019b), a framework implemented on top of Mod TCLP to incrementally compute lattice-based aggregates, and PLAI, the fixpoint algorithm used by CiaoPP.

## 3.1 The Mod TCLP framework

Tabled Logic Programming with Constraints (TCLP) (Arias and Carro 2019a; Schrijvers et al. 2008; Cui and Warren 2000) improves program expressiveness and, in many cases, efficiency and termination properties. Let us consider a program to compute distances between nodes in a graph written using tabling (Fig. 1, left). The query ?- dist(a Y D) , , , D &lt; K. would loop under SLD due to the left-recursive rule, while it would terminate under tabling for acyclic graphs.

Tabling records the first occurrence of each call to a tabled predicate (the generator ) and its answers. In variant tabling (the most usual form of tabling), when a call is found to be equal, modulo variable renaming, to a previous generator, the execution of the call is suspended and it is flagged as a consumer of the generator. For example dist(a Y D) , , is a variant of dist(a Z D) , , if Y and Z are free variables. Upon suspension, execution switches to evaluating another untried branch. A branch which does not suspend can generate answers for the initial goal. When a generator finitely finishes exploring all the clauses and all answers are collected, the consumers that depend on it are resumed and fed with the answers of the generator. This may make generators produce new answers which can in turn resume more consumers. This process finishes when

1

![image](https://ac.marcodsn.me/arxiv-markdown-images/1908.00104v1-figure-04c4bad7-395c-4334-a112-e35ade32acc4.jpg)

:- table dist/3.

Fig. 1: Distance traversal in a graph. Note: The symbols #&gt; and #= are (in)equalities in CLP.

no new answers can be generated - i.e., a fixpoint has been reached. Tabling is sound and, for programs with a finite Herbrand model, complete (and, therefore, it always finishes in these cases).

However, in a cyclic graph, dist/3 has an infinite Herbrand model: every cycle can be traversed repeatedly and create paths of increasing length. Therefore, the previous query ?- dist(a Y D) , , , D &lt; K will not terminate under variant tabling, although the query as a whole has a finite model.

On the other hand, if the integration of tabling and CLP (Fig. 1, center) uses constraint entailment (Chico de Guzmán et al. 2012), calls to dist/3 will suspend if there are previous similar calls that are more general, and only the most general answers will be kept. The query ?- D #&lt; K , dist(a Y D) , , terminates under TCLP because by placing the constraint D#&lt;K before dist(a Y D) , , , the search is pruned when the values in D are larger than or equal to K .

This illustrates the main idea underlying the use of entailment ( glyph[subsetsqequal] ) in TCLP: more particular calls (consumers) can suspend and later reuse the answers collected by more general calls (generators). In order to make this entailment relationship explicit, we will represent a TCLP goal as 〈 g c , g 〉 where g is the call (a literal) and cg is the projection of the current constraint store onto the variables of the call. For example, 〈 dist a Y D ( , , ) , D &gt; 0 ∧ D &lt; 75 〉 entails the goal 〈 dist a Y D ( , , ) , D &lt; 150 〉 because ( D &gt; 0 ∧ D &lt; 75 ) glyph[subsetsqequal] D &lt; 150 . The latter is therefore more general (i.e., it is a generator) than the former (a consumer). All the solutions of a consumer are solutions for its generator, since the space of solutions of the consumer is a subset of that of the generator. However, not all answers from a generator are valid for its consumers. For example Y = b ∧ D &gt; 125 ∧ D &lt; 135 is a solution for our generator, but not for our consumer, since the consumer call was made under a constraint store more restrictive than the generator. Therefore, the tabling engine has to filter, via the constraint solver, the answers from the generator that are consistent w.r.t. the constraint store of the consumer.

Additionally, the Mod TCLP framework (Arias and Carro 2019a) has been used to implement in Ciao a framework, called Aggregate-TCLP (Arias and Carro 2019b), that incrementally computes aggregates for elements in a lattice. The Aggregate-TCLP framework uses the entailment and join relations in a lattice to define and compute aggregates, and to decide whether some atom is compatible with (i.e., entails) the aggregate. For example, the directive :- table dist(\_ \_ min) , , (Fig. 1, right), specifies the (aggregate) mode min for the third argument. The query ?- dist(a Y D) , , will in this case terminate because only the shortest distance between two nodes found at every moment is kept, and it will be returned in D as a result of the evaluation of the initial call. Other tabling engines implement answer subsumption (Swift and Warren

2010) or a restricted form of it via mode-directed tabling (Guo and Gupta 2008; Zhou et al. 2010; Wielemaker et al. 2012; Santos Costa et al. 2012), that can be used to compute aggregates. However, answer subsumption, as implemented in XSB, assumes answers to be safe (i.e., ground) and works on non-ground answers only in some cases, so it would in principle not be applicable when answers are constraints. Answer subsumption also performs subsumption only on answers, while Aggregate-TCLP can in addition check entailment for calls. In the case of the TCLP implementation of the abstract interpreter, this makes it possible to reuse answers obtained from calls semantically equivalent (i.e., calls whose associated abstract substitutions differ, but that still represent the same object in the lattice) and/or more general (i.e., that represent an element higher in the lattice hierarchy). Note that in our benchmarks we are using semantic equivalence, since using entailment to detect more general calls would cause a loss of precision as the domains we are using are non-relational. Last, answer subsumption does not provide the freedom to be used with aggregates that cannot be expressed in terms of a lattice, such as sum/3 , which (Arias and Carro 2019b) can work around.

## 3.2 The PLAI algorithm

We assume that the reader is familiar with the basic principles of abstract interpretation (Cousot and Cousot 1977; Bruynooghe 1991; Nielson et al. 2005). The PLAI algorithm used by the abstract interpreter of CiaoPP for static analysis extends the fixpoint algorithms proposed by (Bruynooghe 1991) with the optimizations described in (Muthukumar and Hermenegildo 1990). In logic programming, all possible concrete substitutions in the program (i.e., terms to which the variables in that program will be bound at run-time for a given query) can be infinite, which gives rise to an infinite execution tree. The core idea of PLAI is to represent this infinite execution tree by an abstract and-or tree using abstract substitutions to finitely represent the possibly infinite sets of substitutions in the concrete domain. The set of all possible abstract substitutions that a variable can be bound to is the abstract domain which is usually a complete lattice (or a complete partial order of finite height).

Domains in PLAI PLAI is domain-independent: new abstract domains can be easily implemented and integrated by using a common interface. The operations required by the domain interface are:

- · l ′ glyph[unionsq] l ′′ , which gives the LUB of the abstract substitutions l ′ and l ′′ . The LUB operation is defined in terms of the glyph[subsetsqequal] relation of the abstract domain.
- · call\_to\_entry(p( ) C glyph[vector] u , , l ) , where C is a clause and p( ) glyph[vector] u is a call. It gives an abstract substitution describing the effects on vars(C) of unifying p( ) glyph[vector] u with head(C) given an abstract substitution l for the variables in glyph[vector] u .
- · exit\_to\_success( l , p( ) glyph[vector] u , C , b ) which returns an abstract substitution describing the effect of execution p( ) glyph[vector] u against clause C . For this, the variables of the abstract substitution b are renamed taking into account the unification with the terms in head(C) and the variables in p( ) glyph[vector] u , and a new abstract substitution is returned updating l with the new information.
- · extend( l l , ′ ) which extends abstract substitution l to incorporate the information in l ' in a way that it is still consistent.
- · project\_in( glyph[vector] u , l ) which extends the abstract substitution l so that it refers to all the variables in glyph[vector] u .

| Algorithm 1: entry_to_exit : Compute exit substitution from entry substitution.                                                                                                                                                                                                                                                                                       |
|-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| Data: A clause C of the form h( glyph[vector] u ):- p 1 ( glyph[vector] u 1 ) , . . . , p m ( glyph[vector] u m ) ; an entry substitution b entry Result: An exit substitution b exit l 1 := project_in( vars ( C ) , b entry ) ; for i := 1 to m do l i + 1 := call_to_success(p i ( glyph[vector] u i ) , l i ) ; return project_out( glyph[vector] u , l m + 1 ) ; |

Algorithm 2: call\_to\_success : Compute success substitution from call substitution.

Data: A goal p( ) glyph[vector] u ; an abstract call substitution l call

Result: A success substitution l success

l proj := project\_out( glyph[vector] u , l call ) ;

l ′ := ⊥ ;

for each clause C which unifies with p( glyph[vector] u ) do

b exit := entry\_to\_exit(C call\_to\_entry(p( ) C , glyph[vector] u , , l proj )) ; ′ ′

l := l glyph[unionsq] exit\_to\_success( l proj , p( ) C glyph[vector] u , , b exit ) ;

return extend( l call , l ′ ) ;

- · project\_out( glyph[vector] u , l ) which restricts the abstract substitution l to refer only to the variables in glyph[vector] u .

For additional examples of abstract domains integrated in CiaoPP, we refer the reader to (Bueno et al. 2004; Muthukumar and Hermenegildo 1989; Vaucheret and Bueno 2002).

And-Or trees and substitutions In PLAI, the abstract and-or tree is constructed using a top-down driven strategy (instead of a bottom-up computation) so that the computation is restricted to what is required for the given query. In the resulting and-or tree, an and-node is a clause head h whose children are the literals in its body, p 1 , . . . , p n , and an or-node is a literal, p i , whose children are the heads h 1 , . . . , h m of the clauses that unify with p i . Its construction starts with the abstract call substitution for the query. Then, abstract substitutions at all points of the abstract and-or tree are computed and finally, the success substitution for the query is computed.

Inside a clause, abstract substitutions at every point are denoted depending on their position among its literals. Given a clause h:- p 1 , . . . , p n , let l i and l i + 1 be the abstract substitutions to the left and right of the subgoal pi , 1 ≤ i ≤ n . Then, l i and l i + 1 are, respectively, the abstract call substitution and the abstract success substitution for the subgoal pi . The projection of l 1 on vars ( h ) is the abstract entry substitution , b entry , of the given clause, and, similarly, the projection of l n + 1 on vars ( h ) is its abstract exit substitution , b exit . The abstract substitutions for a clause are computed as follows:

- · Exit substitution from the entry substitution (Algorithm 1): Given a clause h:- p 1 , . . . , p n and an entry substitution b entry for the clause head h , the call substitution l 1 for p 1 is computed by simply adding to b entry an abstraction for the variables in the clause that do not appear in the head. The success substitution for p 1 is l 2, and it is computed as explained below (essentially, by repeating this same process for the clauses which unify

with p 1). l 3 , . . . , l n + 1 are computed similarly. The exit substitution b exit for this clause is the projection of l n + 1 onto glyph[vector] u , the variables in h .

- · Success substitution from the call substitution (Algorithm 2): Given a call substitution l call for a subgoal p , let h 1 , . . . , hm be the heads of clauses that unify with p . Compute the entry substitutions b 1 entry , . . . , b mentry for these clauses. Compute their exit substitutions b 1 exit , . . . , b mexit as explained above. Compute the success substitutions l 1 success , . . . , l msuccess from the exit substitutions corresponding to these clauses. At this point, all different success substitutions can be considered for the rest of the analysis, or a single success substitution l success for subgoal p computed by means of an aggregation operation for l 1 success , . . . , l msuccess . This aggregate is the least upper bound (LUB), denoted by glyph[unionsq] , of the abstract domain.

Note that these two procedures are mutually recursive and would not finish in case of mutually recursive calls. They merely describe how abstract substitutions are generated for the case of literals in a body (by carrying success abstract substitutions to call abstract substitutions) and how entry and exit substitutions of several clauses are composed together. For the general case of recursive predicates, where repeated calls and termination have to be detected, PLAI implements a fixpoint algorithm that we sketch below.

PLAI's fix point algorithm The core idea of PLAI's fixpoint algorithm (Muthukumar and Hermenegildo 1990) is that the subtree corresponding to the abstract interpretation of a node with a recursive predicate p should be finite. If the abstract domain is finite, a predicate p can only have a finite number of distinct call substitutions and therefore the subtree can only have a finite number of occurrences of nodes that have a variant of p and which themselves have subtrees. In addition to that, all other nodes in the subtree with the same predicate name p and with the same call substitutions (modulo variable renaming) use the approximate value of the success substitution computed previously for the root node of the subtree labeled with p , and hence they do not have any descendent nodes.

Based on this idea, the fixpoint algorithm iteratively refines the approximate values of the success substitution of the recursive predicate p as follows:

- · First, it computes an approximate value of the projected success substitution using the LUB of the projected success substitutions corresponding to the non-recursive clauses of p . This provides an initial, hopefully non-empty, abstract substitution that is fast to compute (it does not need to check for repeated calls or termination) and accelerates the convergence of the fixpoint algorithm. In practice, it can be delegated to a specialized version of Algorithms 1 and 2 restricted to non-recursive calls / clauses. These can be determined beforehand by a reachability analysis based on strongly connected components.
- · Then, it traverses the (finite) subtree corresponding to p in a depth-first fashion. When an entry-exit combination is needed for a call to p having the same call substitution (modulo variable renaming), the existing approximation is used. For a call to p with a different call substitution, a new (nested) fixpoint computation is started. When the analysis returns to the root of the subtree, the success substitution for p is updated as the LUB of the previous value and the value just computed from the recursive clauses of p .
- · If there is a change in the success substitution for p , the depth-first traversal is restarted using the new success substitution, which is used for the subtree nodes corresponding to p that have a compatible call substitution. These depth-first traversal iterations can take place

- only a bounded number of times, since the LUB operation is monotonic and the abstract substitutions form a lattice of finite height. 1 Therefore, a fixpoint will be reached in a finite number of steps.
- · If there is no change in the success substitution for the root node of the subtree of p for a given call substitution, then the analysis of that subtree is complete (for that call substitution) and the fixpoint computation of the predicate p terminates.

For recursive predicates called from within recursive predicates, the dependencies between nested calls have to be recorded to restart the traversal of the subtrees containing predicate calls whose success substitution has been updated.

## 4 Implementations of the PLAI Algorithm: Prolog vs. Tabling

We will now describe more in depth how the PLAI algorithm is implemented in CiaoPP 2 and highlight the differences w.r.t. the version that uses Tabled CLP.

## 4.1 PLAI in CiaoPP

The implementation of call\_to\_success is the entry point, as it relates the entry and exit substitutions of a call (in particular, of the top-level call). During the analysis of a goal p( ) glyph[vector] u , and for each clause that unifies with p( ) glyph[vector] u , the predicate call\_to\_success invokes entry\_to\_exit which, for each subgoal in the body of the clause, invokes again call\_to\_success . The abstract interpreter is able to stop the evaluation of a part of the program and move to another part to evaluate calls to other predicates. The implementation of PLAI is optimized to accelerate the convergence of the fixpoint and reduce the computation by reusing previous results, among other techniques.

The PLAI algorithm is based on the construction of an and-or tree, described in Section 3.2, with the nodes representing the predicate calls visited during the analysis. To construct this tree, call\_to\_success identifies each goal with its corresponding and/or node and with the specialized version of its father (i.e., the version of the literal that originated the call) and carries around a list with the nodes on which the current goal depends. The analysis starts with a query (a goal) and a call substitution. With this information, call\_to\_success creates the root node of the tree and the list of clauses that unify with the goal. If the goal corresponds to a non-recursive predicate, it computes the success substitution which is asserted in a memo-table to reuse the result later on. Otherwise, the goal corresponds to a recursive predicate and it is dealt with by the fixpoint algorithm: first, it evaluates the non-recursive clauses obtaining an approximation of the success substitution and, after this, it starts the fixpoint computation.

During the fixpoint computation, for a goal with a given call substitution:

- · If complete information has been already inferred and saved, call\_to\_success reuses it, to avoid re-computations.

1 While it is true that abstract domains can be infinite, if convergence is not reached after some time, a widening operation changes the representation of the abstract substitutions to a coarser domain that has more chances to converge (or is sure to converge, if it is finite).

2 The code is available at www.ciao-lang.org . For the reader convenience, we sketch it in Appendix B.

- · If it is already inside a fixpoint computation (some parent started a fixpoint with the same call), call\_to\_success reuses the approximation stored for this call, to avoid entering loops.
- · If an analyzed call depends on other nodes whose fixpoint are not completed yet, two cases are treated:
- -If the information on which the predicate depends is updated, a local fixpoint computation is started.
- -Otherwise, nothing is done.

To decide whether updated information for a node is available, the information inferred for it has a version number:

- -When the information on a node is updated, its version number is increased by one.
- -When a node uses information from another node, it stores the version of that information in the list of nodes on which it depends.

Version numbers are used to detect updates of the information on which a node analysis depend. If the version number of the last information used from a node does not match its current version number, there has been an update that needs to be propagated.

When the fixpoint computation finishes and the list of dependent nodes is empty, the current information for this call is asserted. Otherwise, if this list is not empty, the information remains flagged as an approximation and the fixpoint restarts. As it can easily be seen, while the algorithm can be conceptually not too complex, its implementation is cumbersome and at points costly, since many interactions are done through the database using identifiers for program points.

## 4.2 The PLAI Algorithm in TCLP

The PLAI code using tabling is a simplification of the corresponding Prolog implementation. The main points that were changed are:

- · The handling of dependencies among nodes and the detection of termination in the fixpoint computation, that were explicit in the Prolog version, are now transferred to the underlying fixpoint of the tabling engine.
- · The calculation of the LUB of the abstract substitutions generated by different clauses unifying with a call is done via lattice-based constraint aggregation (which is in turn built upon tabling).

## 4.2.1 Internal Database and Dependencies

In the Prolog implementation, the information related to the abstract substitutions is kept in a dynamic database relating code, program points, entry/exit substitutions, and dependencies. This makes it globally accessible and allows it to survive across backtracking and calls, so that it does not need to be carried around the program and be rebuilt every time there is a change in the substitution at a program point.

However, making the abstract interpreter update that information, switch among calls, and re-analyze calls needs accessing and updating this database, which is costly and mixes declarative and imperative styles. On top of that, the CiaoPP implementation has been fine-tuned during many years to avoid unnecessary (re-)analyses and minimize the overhead of accessing the

```
                                                                                                                                                                                                        J. Arias and M. Carro                                                                                                                                                                                                       
                                                                                                                                                                                                        }
                                                                                                                                                                                                       }                                                                                                                                                                                                        |
                                                                                                                                                                                                       |                                                                                                                                                                                                        <!-- use_package(tclp_aggregate).
                                                                                                                                                                                                      
																																																													                                                                                                                                                                                                       		                                                                                                                                                                                                      |
																																																																																																																																																																																																								                                                                                                                                           |
																																																											                                                                                                                                             |
																																																									                                                                                                                                               |
																																																							                                                                                                                                                 |
																																																					                                                                                                                                                   |
																																																			                                                                                                                                                     |
																																																	                                                                                                                                                       |
```

Fig. 2: Implementation of call\_to\_success/7 under the TCLP framework

database. All of these optimizations cause the code to have to deal with specific cases for the sake of performance, hence adding to its complexity. But despite the involved implementation, this machinery mimics, at Prolog level, an infrastructure similar to a tabling engine, but specialized for a given program -the abstract interpreter- and with optimizations specific for the task at hand.

This bookkeeping becomes unnecessary when using a tabling-based implementation. An abstract interpreter written using tabling and equipped with the capability to detect when two syntactically different substitutions represent the same object, can automatically take care of termination, suspend analysis when repeated calls are detected, and resume them when new information is available - all of it as part of the normal execution of a tabled program, without having to explicitly update and check dependencies.

That makes the code much simpler (no dependencies, lists of pending goals, resuming, etc. need to be explicitly coded) and shorter (we have obtained a threefold reduction in code size). On the other hand, the tabling engine is generic and cannot decide which suspension and/or resumption policy is better for a particular application. We on purpose chose to (a) keep the TCLP code simple and not include any specific heuristic in the code, (b) not to reimplement an analyzer from scratch, but simplify existing code, and (c) keep exactly the same interfaces (both those offered to the rest of CiaoPP and those required by the fixpoint code) so that the TCLP-based abstract interpreter can interoperate with the rest of the CiaoPP machinery as a drop-in replacement with close to zero effort. For these and other reasons, our performance figures (Section 5) are a lower bound of what could be achieved.

As an example, the implementation of call\_to\_success/13 in Prolog checks several cases: if the call being analyzed is complete, under evaluation in a fixpoint, a call to a recursive predicate, a call to a non-recursive predicate, etc. to update information accordingly. It eventually invokes proj\_to\_prime\_nr/9 , which starts the fixpoint computation itself, and which recursively calls call\_to\_success/13 . call\_to\_success/13 has eight clauses and proj\_to\_prime\_nr/9 has six clauses (see Appendix B or the corresponding file at http: //www.cliplab.org/papers/tclp-plai-iclp2019 ).

In the tabling implementation, the underlying engine and the calls to the abstract domain operations through the constraint solver interface take care of these cases and dependencies. This makes the implementation of call\_to\_success have just one clause (Fig. 2). The counterpart

1

2

3

call\_entail(abst\_lub

,

st(Sv \_ ProjA AbsInt \_)

,

,

,

,

,

st(Sv \_ ProjB AbsInt \_) ) :- identical\_abstract(AbsInt ProjA ProjB).

,

,

answer\_entail(abst\_lub

,

st(Sv \_ \_ AbsInt PrimeA)

,

,

,

,

,

,

,

,

,

st(Sv \_ \_ AbsInt PrimeB) ) :-

,

,

,

,

4

less\_or\_equal(AbsInt PrimeA PrimeB).

,

,

- 5 answer\_join(abst\_lub st(Sv \_ \_ Abs , , , , , A) , st(Sv \_ \_ Abs , , , , B) , st(Sv \_ \_ Abs New) ) :-, , , , 6 compute\_lub(Abs [A B] New). , , ,
- 7 apply\_answer(abst\_lub , st(Sv \_ \_ AbsInt Prime) , , , , , st(Sv \_ \_ AbsInt Prime) ). , , , ,

Fig. 3: Code of the operator abst\_lub under the TCLP framework

to proj\_to\_prime\_nr/9 (which we renamed call\_to\_success\_fixpoint/3 for clarity) has just two clauses: one for user predicates and another one for library and builtin predicates.

Additionally, the use of tabling makes it unnecessary to save explicitly all the intermediate substitutions, database identifiers for calls and program points, dependencies among goals, etc. This reduces the number of arguments, and call\_to\_success went from thirteen used in Prolog:

call\_to\_success(RFlag SgKey Call Proj Sg Sv AbsInt ClId Succ List F N Id) , , , , , , , , , , , , to seven in the tabling-based implementation:

call\_to\_success(SgKey Call Proj Sg Sv AbsInt Succ) , , , , , ,

## 4.2.2 Deciding Termination and Computing the LUB

In the PLAI algorithm, the different exit substitutions obtained from the clauses that unify with a given call are combined using the LUB operator of the abstract domain (Algorithm 2): exit substitutions b i exit , for every clause Ci are joined to return the success substitution l success .

The CiaoPP implementation uses bagof/3 to collect all the clauses in a list and then traverses it and analyzes every clause to create another list of abstract substitutions that are joined with the LUB. This processing is conceptually simple, but its implementation obscures the code with low-level operations, does not match the idea of having an interpreter executing on an abstract domain, and requires database accesses to retrieve the substitution applicable at that point.

In our implementation, the use of lattice-based aggregates with the tabling engine (Arias and Carro 2019b) simplifies the code. The abst\_lub identifier in line 6 of Fig. 2 is the name of an interface that has several missions: determine suspension of calls, detect termination of the fixpoint, and perform aggregation of abstract substitutions. In the same line, the underscores state that the corresponding arguments are to be checked for equality (necessary to decide whether a fixpoint has been reached) using the variant policy, i.e., syntactical equality modulo variable renaming.

The implementation of the interface named abst\_lub in Fig. 3 tells the tabling engine how to treat the argument selected previously with this identifier. In particular, the tabling engine checks the corresponding arguments for equality by calling call\_entail/3 . In our case, two abstract substitutions are termed equal if the abstract domain implementation ( identical\_abstract/3 ) decides so. This makes it possible to detect that two different representations correspond to the same object in the lattice and, if so, suspend a call or retrieve saved answers for it.

The code in Fig. 3 also aggregates the results returned in the third argument (the abstract substitutions) by joining them with the LUB of the lattice. The tabling engine calls answer\_entail/3 to decide whether a new answer (a substitution) is or not more general than an existing an-

swer ( less\_or\_equal/3 ). If its not comparable, answer\_join/4 (which in turn invokes compute\_lub/3 ) is called to compute the LUB of a previous answer and the new one. With these definitions, lines 7 to 12 in Fig. 2 contain all the code necessary to return the exit substitution of a call w.r.t. all its matching clauses. The implementation of the LUB operation ( abs\_lub , Fig. 3) is based on the operations provided by the abstract domain implementation.

This code also performs an incremental computation of the LUB as follows: upon success, the first answer, corresponding to the exit substitution b 1 exit , is stored in the answer table of the tabled predicate. Let us call this stored answer b exit . For the subsequent exit substitutions b i exit , i &gt; 1, there are two possible cases: if the saved substitution is more general ( b i exit glyph[subsetsqequal] b exit ), then b i exit is discarded; otherwise we make b exit = b exit glyph[unionsq] b i exit .

## 4.2.3 Connecting Abstract Substitutions with Lattice-Based Aggregates

The TCLP system handles entailment, aggregation, etc. by delegating operations to an underlying constraint solver using a fixed interface (Arias and Carro 2019a). Since we purposely did not change the representation of the CiaoPP abstract domains (they are used in other parts of the system), we constructed a bridge between these domains and the interface that TCLP expects.

The original entry point of the fixpoint, proj\_to\_prime\_nr/9 (renamed as call\_to\_success\_fixpoint/3 in the TCLP implementation), now tabled, is automatically rewritten (by the package tclp\_aggregate ) to call an auxiliary predicate that, at run time, substitutes the arguments carrying abstract substitutions by attributed variables (Holzbaur 1992) that simulate having a constrained variable. Their attributes are tuples that contain (a) the identifier ( abst\_lub , in our example) that determines the interface to be used and (b) the abstract substitution and ancillary information necessary by the abstract interpreter.

When one operation of the tabling engine involves a call with attributed variables, the engine checks if it has an attribute with contents it recognizes. If so, it calls the corresponding predicate from the interface that, in our case, operates on the substitution stored in the attributes.

## 5 Evaluation

Besides simplifying code, the implementation of PLAI using TCLP gives performance advantages in many cases. These come mainly because part of the bookkeeping related to dependencies, saving the analysis state when restarting the analysis of a dependent call, checking for termination, etc. are handled at a lower level. On the other hand, the implementation currently in CiaoPP, as commented before, has been fine-tuned and specialized during many years to minimize the overhead of the fixpoint implementation, so that a large proportion of the analysis time is spent in domain-related operations. On top of that, the CiaoPP domain representation and domain operations are designed to work well with its current architecture and coding decisions (e.g. saving and retrieving from the dynamic databases) and are suboptimal for a tabling-based implementation: for example, redundant data is manipulated and/or stored. As commented earlier, we did not change any of these so the TCLP fixpoint can seamlessly interact with the rest of the CiaoPP tool, exposing and using exactly the same interfaces.

Even with these constraints, we observed speedups when analyzing most programs from a benchmark set. We used the Groundness and Sharing+Freeness (Muthukumar and Hermenegildo 1991) domains due to their relevance (e.g., for program optimization and correctness of parallelization). Groundness (see Table 1 for performance results) determines if some program vari-

Table 1: Performance comparison: CiaoPP fixpoint in Prolog and TCLP ( Groundness domain).

|             |   Speedup |   TCLP (ms) |   CiaoPP (ms) |
|-------------|-----------|-------------|---------------|
| fibf_alt    |      1.6  |        0.29 |          0.46 |
| aiakl       |      1.56 |        2.45 |          3.82 |
| boyer       |      1.5  |        7.31 |         10.97 |
| pv_queen    |      1.46 |        0.74 |          1.07 |
| subst       |      1.41 |        0.25 |          0.35 |
| pv_gabriel  |      1.37 |        3.65 |          4.99 |
| rdtok       |      1.32 |        7.03 |          9.25 |
| mmatf       |      1.24 |        0.31 |          0.39 |
| hanoi       |      1.22 |        0.53 |          0.65 |
| revf_lin    |      1.2  |        0.27 |          0.32 |
| append      |      1.2  |        0.17 |          0.2  |
| rev_lin     |      1.19 |        0.26 |          0.31 |
| prefix      |      1.16 |        0.27 |          0.31 |
| revf        |      1.15 |        0.32 |          0.37 |
| pv_plan     |      1.15 |        1.94 |          2.23 |
| sublist_app |      1.14 |        0.24 |          0.27 |
| reverse     |      1.14 |        0.38 |          0.43 |
| flatten     |      1.13 |        0.55 |          0.62 |
| palindro    |      1.12 |        0.34 |          0.38 |
| fact        |      1.08 |        0.25 |          0.27 |
| rotate      |      1.06 |        0.46 |          0.49 |
| maxtree     |      0.98 |        0.63 |          0.61 |
| zebra       |      0.92 |        1.38 |          1.26 |
| browse      |      0.89 |        1.76 |          1.57 |
| AVG         |      1.31 |       31.78 |         41.59 |

able will be bound to a ground term. This is useful to derive modes, optimize unification, and improve the precision of the Sharing+Freeness analysis, among others.

Sharing+Freeness (see Table 2) determines if two (or more) program variables may be bound to terms sharing a common variable. It is useful to determine, for example, whether running two goals in parallel may try to bind the same variable, thus causing races and compromising correctness. The benchmarks used are standard programs that have been previously used to evaluate CiaoPP.

All the experiments in this paper were performed on a Linux 5.0.0-13-generic machine with an Intel Core i7 at 1.80GHz with 16Gb of memory and using gcc 8.3.0 to compile the abstract machine of Ciao Prolog. In all cases, every program was analyzed 40 times and the 10 worst times were discarded, both when using the tabling and the Prolog implementation, to try to minimize the effect of spurious interruptions, O.S. scheduling, etc. that can introduce noise in the execution. The remaining times were averaged. All the code and the system under evaluation is available at http://www.cliplab.org/papers/tclp-plai-iclp2019 .

The average speedups in each table were calculated by adding up the (averaged) execution times for all the benchmarks and dividing the CiaoPP time by the TCLP time. This shows that, on average, the analysis with the Groundness domain speeds up a bit more than 30%, while the analysis with the Sharing+Freeness has experienced, on average, a slight slowdown (about 3%).

By looking at every benchmark in isolation, we can observe that the speedups differ greatly

J. Arias and M. Carro

|             |   Speedup |   TCLP (ms) |   CiaoPP (ms) |
|-------------|-----------|-------------|---------------|
| fact        |      1.3  |        0.26 |          0.33 |
| pv_queen    |      1.23 |        1.21 |          1.49 |
| mmatf       |      1.17 |        0.51 |          0.6  |
| mmatrix     |      1.15 |        0.53 |          0.61 |
| prefix      |      1.14 |        0.46 |          0.52 |
| revf        |      1.12 |        0.47 |          0.53 |
| revf_lin    |      1.1  |        0.39 |          0.43 |
| reverse     |      1.1  |        0.39 |          0.43 |
| rev_lin     |      1.1  |        0.38 |          0.42 |
| rotate      |      1.06 |        0.72 |          0.76 |
| pv_pg       |      1.01 |        2.67 |          2.7  |
| append      |      0.98 |        1.11 |          1.09 |
| sublist_app |      0.96 |        0.87 |          0.84 |
| zebra       |      0.91 |       16.34 |         14.8  |
| AVG         |      0.97 |       26.31 |         25.55 |

Table 2: Performance comparison: CiaoPP fixpoint in Prolog and TCLP ( Sh+Fr domain).

among them. We have sorted the benchmarks according to the speedup to appreciate better the differences. In both cases, only a small part of the benchmarks (three) experienced a slowdown, and even in these cases, the maximum slowdown was about 10%. In the case of Sharing+Freeness , the slowest analysis corresponded as well to the largest execution time (larger than the rest of the benchmarks combined). We want to note that this benchmark (zebra) is probably not a representative of a typical program, as it is a combinatorial problem with many free variables in a single clause, some of which are aliased with each other.

The source of the speed difference is not easy to determine. A profile of the number of fixpoint calls in CiaoPP vs. fixpoint calls, entailment checks, joins, etc. in the TCLP version does not seem to show a correlation with the observed speedups. We therefore conjecture that the shape and size of the abstract substitution, and the relative cost of checking entailment, has to be explored to have a better explanation of the differences observed.

## 6 Conclusions and Future Work

We have presented a re-implementation of PLAI, a fixpoint computation algorithm for abstract interpretation, using tabled constraint logic programming. The resulting code is considerably shorter than the current Prolog implementation of PLAI in CiaoPP (one-third of its size) and much simpler: all the bookkeeping necessary to keep track of dependencies between predicates, analysis restarting, etc. is in charge of the tabling engine, which increases the maintainability of the implementation of PLAI.

We have evaluated its performance using several benchmarks and abstract domains, and compared it with the original implementation in CiaoPP. In most cases, the TCLP implementation showed improved performance, sometimes with a speedup of 60%. In a few cases there was a small slowdown, which we think is a reasonable price to pay for the added code clarity, especially taking into account that there is room for improvement in the current implementation.

Among the immediate future plans, we want to experiment re-implementing the abstract domains with an optimized representation of the abstract substitutions, and also use constraint logic

programming techniques to propagate the effects of updates. We also expect that, using constraints, we will be able to define widening heuristics independently of the fixpoint algorithm thereby increasing the resulting flexibility, precision and performance w.r.t. the state of the art.

## Acknowledgements

We would like to thank Maximiliano Klemen, who helped us understand the intricacies of the CiaoPP implementation of PLAI. Thanks are also due to Manuel Hermenegildo, who gave us very valuable feedback on the paper manuscript and also a historical account on the early relationship between tabling and efficient abstract interpretation implementations.

## References

ARIAS, J. AND CARRO, M. 2019a. Description, Implementation, and Evaluation of a Generic Design for Tabled CLP. Theory and Practice of Logic Programming 19, 3, 412-448.

- ARIAS, J. AND CARRO, M. 2019b. Incremental evaluation of lattice-based aggregates in logic programming using modular TCLP. In Practical Aspects of Declarative Languages - 21st International Symposium (PADL 2019) , J. J. Alferes and M. Johansson, Eds. Lecture Notes in Computer Science, vol. 11372. Springer, 98-114.
- BRUYNOOGHE, M. 1991. A Practical Framework for the Abstract Interpretation of Logic Programs. Journal of Logic Programming 10 , 91-124.
- BUENO, F., LOPEZ-GARCIA, P., AND HERMENEGILDO, M. V. 2004. Multivariant Non-Failure Analysis via Standard Abstract Interpretation. In FLOPS'04 . Number 2998 in LNCS. Springer-Verlag, 100-116.
- CHICO DE GUZMÁN, P., CARRO, M., HERMENEGILDO, M. V., AND STUCKEY, P. 2012. A General Implementation Framework for Tabled CLP. In Int'l. Symposium on Functional and Logic Programming (FLOPS'12) . Number 7294 in LNCS. Springer Verlag, 104-119.
- COUSOT, P. AND COUSOT, R. 1977. Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In ACM Symposium on Principles of Programming Languages (POPL'77) . ACM Press, 238-252.
- CUI, B. AND WARREN, D. S. 2000. A system for Tabled Constraint Logic Programming. In Int'l. Conference on Computational Logic . LNCS, vol. 1861. 478-492.
- DEMOEN, B. AND SAGONAS, K. 1998. CAT: The Copying Approach to Tabling. In Programming Language Implementation and Logic Programming . Lecture Notes in Computer Science, vol. 1490. SpringerVerlag, 21-35.
- DIETRICH, S. W. 1987. Extension Tables: Memo Relations in Logic Programming. In Fourth IEEE Symposium on Logic Programming . 264-272.
- FREIRE, J., SWIFT, T., AND WARREN, D. S. 2001. Beyond Depth-First: Improving Tabled Logic Programs through Alternative Scheduling Strategies. In International Symposium on Programming Language Implementation and Logic Programming . Number 1140 in LNCS. Springer-Verlag, 243-258.
- GANGE, G., NAVAS, J. A., SCHACHTE, P., SØNDERGAARD, H., AND STUCKEY, P. J. 2013. Failure Tabled Constraint Logic Programming by Interpolation. TPLP 13, 4-5, 593-607.
- GUO, H.-F. AND GUPTA, G. 2008. Simplifying Dynamic Programming via Mode-directed Tabling. Software: Practice and Experience 1 (Jan), 75-94.
- HERMENEGILDO, M. V., BUENO, F., CARRO, M., LOPEZ-GARCIA, P., MERA, E., MORALES, J., AND PUEBLA, G. 2012. An Overview of Ciao and its Design Philosophy. Theory and Practice of Logic Programming 12, 1-2 (January), 219-252. http://arxiv.org/abs/1102.5497.
- HERMENEGILDO, M. V., PUEBLA, G., BUENO, F., AND LOPEZ-GARCIA, P. 2005. Integrated Program Debugging, Verification, and Optimization Using Abstract Interpretation (and The Ciao System Preprocessor). Science of Computer Programming 58, 1-2 (October), 115-140.

HOLZBAUR, C. 1992. Metastructures vs. Attributed Variables in the Context of Extensible Unification. In Int'l. Symposium on Programming Language Implementation and Logic Programming . Number 631 in LNCS. Springer Verlag, 260-268.

- JAFFAR, J. AND MAHER, M. 1994. Constraint Logic Programming: A Survey. Journal of Logic Programming 19/20 , 503-581.
- JANSSENS, G., BRUYNOOGHE, M., AND DUMORTIER, V. 1995. A blueprint for an abstract machine for abstract interpretation of (constraint) logic programs. In ILPS . 336-350.
- JANSSENS, G. AND SAGONAS, K. 1998. On the Use of Tabling for Abstract Interpretation: An Experiment with Abstract Equation Systems. In Tabulation in Parsing and Deduction .
- KANAMORI, T. AND KAWAMURA, T. 1993. Abstract Interpretation Based on OLDT Resolution. Journal of Logic Programming 15 , 1-30.
- MUTHUKUMAR, K. AND HERMENEGILDO, M. 1989. Determination of Variable Dependence Information at Compile-Time Through Abstract Interpretation. In 1989 North American Conference on Logic Programming . MIT Press, 166-189.
- MUTHUKUMAR, K. AND HERMENEGILDO, M. 1990. Deriving A Fixpoint Computation Algorithm for Top-down Abstract Interpretation of Logic Programs. Technical Report ACT-DC-153-90, Microelectronics and Computer Technology Corporation (MCC), Austin, TX 78759. April.
- MUTHUKUMAR, K. AND HERMENEGILDO, M. 1991. Combined Determination of Sharing and Freeness of Program Variables Through Abstract Interpretation. In International Conference on Logic Programming (ICLP 1991) . MIT Press, 49-63.

MUTHUKUMAR, K. AND HERMENEGILDO, M. 1992. Compile-time Derivation of Variable Dependency Using Abstract Interpretation. JLP 13, 2/3 (July), 315-347.

- NIELSON, F., NIELSON, H. R., AND HANKIN, C. 2005. Principles of Program Analysis . Springer. Second Ed.
- SANTOS COSTA, V., ROCHA, R., AND DAMAS, L. 2012. The YAP Prolog system. Theory and Practice of Logic Programming 12, 1-2, 5-34.
- SCHRIJVERS, T., DEMOEN, B., AND WARREN, D. S. 2008. TCHR: a Framework for Tabled CLP. Theory and Practice of Logic Programming 4 (Jul), 491-526.
- SWIFT, T. AND WARREN, D. S. 2010. Tabling with answer subsumption: Implementation, applications and performance. In Logics in Artificial Intelligence . Vol. 6341. 300-312.
- TAMAKI, H. AND SATO, M. 1986. OLD Resolution with Tabulation. In Third International Conference on Logic Programming . Lecture Notes in Computer Science, Springer-Verlag, London, 84-98.
- VAUCHERET, C. AND BUENO, F. 2002. More Precise yet Efficient Type Inference for Logic Programs. In 9th International Static Analysis Symposium (SAS'02) . Lecture Notes in Computer Science, vol. 2477. Springer-Verlag, 102-116.

WARREN, D. S. 1992. Memoing for Logic Programs. Communications of the ACM 35, 3, 93-111.

WARREN, D. S. 1999. Programming in Tabled Prolog. https://www3.cs.stonybrook.edu/~warren/ xsbbook/book.html . Unpublished manuscript. Accessed on May 15, 2019.

WARREN, R., HERMENEGILDO, M., AND DEBRAY, S. K. 1988. On the Practicality of Global Flow Analysis of Logic Programs. In Fifth International Conference and Symposium on Logic Programming . MIT Press, 684-699.

WIELEMAKER, J., SCHRIJVERS, T., TRISKA, M., AND LAGER, T. 2012. SWI-Prolog. Theory and Practice of Logic Programming 12, 1-2, 67-96.

- ZHOU, N.-F., KAMEYA, Y., AND SATO, T. 2010. Mode-Directed Tabling for Dynamic Programming, Machine Learning, and Constraint Solving. In Int'l. Conference on Tools with Artificial Intelligence . Number 2. IEEE, 213-218.

## Appendix A PLAI Algorithm Implementation Using TCLP

In this appendix we include the code corresponding to the reimplementation of PLAI using TCLP. It is not expected to be used to understand the code (we did not add any facility or improve its functionality), but rather to compare the code length and complexity with that of the original PLAI in CiaoPP, which we include in Appendix B. Therefore, we have removed the comments that appear in the original files. The files with comments can be accessed at http://www.cliplab.org/papers/tclp-plai-iclp2019 .

```
                                                                                                                                                                                                       
                                                                                                                                                                                                       

                                                                                                                                                                                                        <?                                                                                                                                                                                                        </?>                                                                                                                                                                                                        >                                                                                                                                                                                                        |                                                                                                                                                                                                        \
                                                                                                                                                                                                      

                                                                                                                                                                                                       <!                                                                                                                                                                                                        &?                                                                                                                                                                                                       <&?                                                                                                                                                                                                      
	                                                                                                                                                                                                        +                                                                                                                                                                                                        -?                                                                                                                                                                                                       |
                                                                                                                                                                                                       +
                                                                                                                                                                                                       -
                                                                                                                                                                                                       </!
```

| cleanup_fixpoint(_AbsInt).                                                                                                                                                     |                   |
|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|-------------------|
| %------------------------------------------------------------------------% % call_to_success(+,+,+,+,+,+,-)                                                                    | %                 |
| %------------------------------------------------------------------------%                                                                                                     |                   |
| call_to_success(SgKey,Call,Proj,Sg,Sv,AbsInt,Succ) :- call_to_success_fixpoint(SgKey,Sg,                                                                                       |                   |
| st(Sv,Call,Proj,AbsInt,Prime)), each_extend(Sg,Prime,AbsInt,Sv,Call,Succ). %%%%%%%%%%%% TCLP interface %%%%%%%%%%%%% :- use_package(tclp_aggregate).                           |                   |
| singleton(Prime,Primes). Clause = clause(Head,Vars_u,K,Body), clause_applies(Head,Sg), !,                                                                                      |                   |
| do_nr_cl(Clause,Sg,Sv,Call,Proj,AbsInt,Primes):- varset(Head,Hv), sort(Vars_u,Vars),                                                                                           |                   |
| ord_subtract(Vars,Hv,Fv), process_body(Body,K,AbsInt,Sg,Hv,Fv,Vars_u,Head,Sv,Call,                                                                                             |                   |
| do_nr_cl(_Clause,_Sg,_Sv,_Call,_Proj,_AbsInt,[[]]). process_body(Body,K,AbsInt,Sg,Hv,_Fv,_,Head,Sv,Call,Proj,LPrime,_Id):- Body = g(_,[],'$built'(_,true,_),'true/0',true), !, |                   |
| singleton(Prime,LPrime), call_to_success_fact(AbsInt,Sg,Hv,Head,K,Sv,Call,Proj,Prime,_Succ). singleton(Entry,LEntry),                                                          |                   |
|                                                                                                                                                                                | %                 |
| % entry_to_exit(+,+,+,-,+,-,+,+,+)                                                                                                                                             |                   |
| entry_to_exit((Sg,Rest),K,Call,Exit,OldList,NewList,Vars_u,AbsInt,NewN):- !, body_succ(Call,Sg,Succ,OldList,IntList,Vars_u,AbsInt,K,NewN,_),                                   |                   |
| %------------------------------------------------------------------------%                                                                                                     |                   |
| %------------------------------------------------------------------------%                                                                                                     |                   |
| apply_answer(abst_lub, st(V,_,_,Ab,A), st(V,_,_,Ab,B)) trans_clause(SgKey,_,Clause),                                                                                           | :- A = B.         |
| call_to_success_fixpoint(SgKey,Sg,st(Sv,Call,Proj,AbsInt,Primes))                                                                                                              | :-                |
| do_nr_cl(Clause,Sg,Sv,Call,Proj,AbsInt,Primes). call_to_success_fixpoint(SgKey,Sg,st(Sv,_Call,Proj,AbsInt,Primes)) \+ trans_clause(SgKey,_,_),                                 |                   |
| apply_trusted0(Proj,SgKey,Sg,Sv,AbsInt,_ClId,Prime),                                                                                                                           |                   |
|                                                                                                                                                                                | :-                |
|                                                                                                                                                                                | Proj,Primes,_Id). |
| entry_to_exit(Body,K,LEntry,Exit,[],_,Vars_u,AbsInt,Id),                                                                                                                       |                   |
| call_to_entry(AbsInt,Sv,Sg,Hv,Head,K,Fv,Proj,Entry,ExtraInfo),                                                                                                                 |                   |
| each_exit_to_prime(Exit,AbsInt,Sg,Hv,Head,Sv,ExtraInfo,Prime).                                                                                                                 |                   |
| process_body(Body,K,AbsInt,Sg,Hv,Fv,Vars_u,Head,Sv,_,Proj,Prime,Id):-                                                                                                          |                   |

## Abstract Interpretation Fixpoint using TCLP

| 121 122             | entry_to_exit(Rest,K,Succ,Exit,IntList,NewList,Vars_u,AbsInt,NewN). entry_to_exit(true,_,Call,Call,List,List,_,_,_):- !. entry_to_exit(Sg,Key,Call,Exit,OldList,NewList,Vars_u,AbsInt,NewN):-   |
|---------------------|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| 123 124 125         | body_succ(Call,Sg,Exit,OldList,NewList,Vars_u,AbsInt,Key,NewN,_), true.                                                                                                                         |
| 127                 | body_succ(Call,_Atom,Succ,List,List,_HvFv_u,_AbsInt,_ClId,_ParentId,no):- bottom(Call), !, Succ = Call.                                                                                         |
| 128                 | body_succ(Call,Atom,Succ,List,NewList,HvFv_u,AbsInt,ClId,ParentId,Id):- Atom=g(Key,Sv,Info,SgKey,Sg),                                                                                           |
| 129 130 131 132 133 | body_succ_(Info,SgKey,Sg,Sv,HvFv_u,Call,Succ,List,NewList,AbsInt,                                                                                                                               |
| 134                 | ClId,Key,ParentId,Id).                                                                                                                                                                          |
| 135                 |                                                                                                                                                                                                 |
| 136 137             | body_succ_(Info,SgKey,Sg,Sv,HFv,Call,Succ,L,NewL,AbsInt,ClId,Key,PId,Id):- Info = [_|_], !, split_combined_domain(AbsInt,Call,Calls,Domains),                                                   |
| 138 139 140         | map_body_succ(Info,SgKey,Sg,Sv,HFv,Calls,Succs,L,NewL,Domains, ClId,Key,PId,Id), split_combined_domain(AbsInt,Succ,Succs,Domains).                                                              |
|                     | body_succ_(Info,SgKey,Sg,Sv,HFv,Call,Succ,L,NewL,AbsInt,ClId,Key,PId,Id):- body_succ0(Info,SgKey,Sg,Sv,HFv,Call,Succ,L,NewL,AbsInt,                                                             |
| 141                 |                                                                                                                                                                                                 |
| 142 143 144         | ClId,Key,PId,Id).                                                                                                                                                                               |
| 145 146             |                                                                                                                                                                                                 |
|                     | map_body_succ([],_SgKey,_Sg,_Sv,_HFv,[],[],L,L,[],_ClId,_Key,_PId,no). map_body_succ([I|Info],SgKey,Sg,Sv,HFv,[Call|Calls],[Succ|Succs],L,NewL,                                                 |
| 147 148             | [AbsInt|Domains],ClId,Key,PId,Id):-                                                                                                                                                             |
|                     | body_succ0(I,SgKey,Sg,Sv,HFv,Call,Succ,L,_NewL,AbsInt,                                                                                                                                          |
| 149                 | ClId,Key,PId,_Id), !,                                                                                                                                                                           |
| 150                 |                                                                                                                                                                                                 |
| 151                 |                                                                                                                                                                                                 |
| 152 153 154         | map_body_succ(Info,SgKey,Sg,Sv,HFv,Calls,Succs,L,NewL,Domains, ClId,Key,PId,Id).                                                                                                                |
| 155                 | body_succ0('$var',SgKey,Sg,_Sv_u,HvFv_u,Calls,Succs,List0,List,AbsInt, _ClId,F,_N,_Id):-                                                                                                        |
| 156 157             | !, ( Calls=[Call],                                                                                                                                                                              |
| 158                 | concrete(AbsInt,Sg,Call,Concretes), concretes_to_body(Concretes,SgKey,AbsInt,B)                                                                                                                 |
| 159                 | ->                                                                                                                                                                                              |
| 160                 | ; List=List0,                                                                                                                                                                                   |
|                     | meta_call(B,HvFv_u,Calls,[],Succs,List0,List,AbsInt,_ClId,_Id,_Ids)                                                                                                                             |
| 161                 | each_unknown_call(Calls,AbsInt,[Sg],Succs) % Sg is a variable                                                                                                                                   |
| 162                 |                                                                                                                                                                                                 |
|                     | ).                                                                                                                                                                                              |
| 163 164 165         | body_succ0('$meta'(T,B,_),SgKey,Sg,Sv_u,HvFv_u,Call,Succ,List0,List,AbsInt,                                                                                                                     |
| 166                 | _ClId,_F,_N,_Id):- !,                                                                                                                                                                           |
|                     | meta_call(B,HvFv_u,Call,[],Exits,List0,List,AbsInt,ClId,Id,_Ids), ( body_succ_meta(T,AbsInt,Sv_u,HvFv_u,Call,Exits,Succ) ->                                                                     |
| 167 168             |                                                                                                                                                                                                 |
| 169                 | true                                                                                                                                                                                            |
| 170                 | ; % for the trusts, if any:                                                                                                                                                                     |
|                     | varset(Sg,Sv_r), % Sv_u contains extra vars (from meta-term)                                                                                                                                    |
| 171                 |                                                                                                                                                                                                 |
| 172                 | % which will confuse apply_trusted                                                                                                                                                              |
| 173                 |                                                                                                                                                                                                 |
| 174                 |                                                                                                                                                                                                 |
| 175                 |                                                                                                                                                                                                 |
| 178 179             | _ClId,_F,_N,_Id0)                                                                                                                                                                               |
| 180                 | ). _ClId,_F,_N,_Id):-                                                                                                                                                                           |
| 181                 | List=List0, sort(Sv_u,Sv),                                                                                                                                                                      |
|                     | _ClId,_F,_N,_Id):-                                                                                                                                                                              |
|                     | body_succ0(_RFlag,SgKey,Sg,Sv_u,HvFv_u,Call,Succ,_List0,_List,AbsInt,                                                                                                                           |
|                     | !,                                                                                                                                                                                              |
|                     | body_succ0(nr,SgKey,Sg,Sv_r,HvFv_u,Call,Succ,[],_List,AbsInt,                                                                                                                                   |
| 183                 | sort(Sv_u,Sv), each_call_to_success(Call,SgKey,Sg,Sv,HvFv_u,AbsInt,Succ).                                                                                                                       |
| 182                 |                                                                                                                                                                                                 |
| 176 177             |                                                                                                                                                                                                 |
|                     | body_succ0('$built'(T,Tg,Vs),SgKey,Sg,Sv_u,HvFv_u,Call,Succ,List0,List,AbsInt,                                                                                                                  |
|                     | each_body_succ_builtin_(Call,AbsInt,T,Tg,Vs,SgKey,Sg,Sv,HvFv_u,Succ).                                                                                                                           |

| 187 each_body_succ_builtin_([],_,_T,_Tg,_,_,_Sg,_Sv,_HvFv_u,[]).                                                                                                                                                                                                                    |                                                                                                                                                                                                                                                                                                                   |
|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| 188 189 project(AbsInt,Sg,Sv,HvFv_u,Call,Proj), 190 191 192 !,                                                                                                                                                                                                                      | each_body_succ_builtin_([Call|Calls],AbsInt,T,Tg,Vs,SgKey,Sg,Sv,HvFv_u,[Succ|Succs]):- body_succ_builtin(T,AbsInt,Tg,Vs,Sv,HvFv_u,Call,Proj,Succ),!, %% Doamin call each_body_succ_builtin_tabling_(Calls,AbsInt,T,Tg,Vs,SgKey,Sg,Sv,HvFv_u,Succs). each_call_to_success([Call],SgKey,Sg,Sv,HvFv_u,AbsInt,Succ):- |
| 193 project(AbsInt,Sg,Sv,HvFv_u,Call,Proj), call_to_success(SgKey,Call,Proj,Sg,Sv,AbsInt,Succ). each_call_to_success0(LCall,SgKey,Sg,Sv,HvFv_u,AbsInt, LSucc). LSucc):-                                                                                                             | meta_call_([Body|Bodies],HvFv_u,Call,Succ0,Succ,L0,List,AbsInt,ClId,Id,Ids). body_succ(Call,Sg,Succ,OldList,IntList,Vars_u,AbsInt,K,PId,Id),                                                                                                                                                                      |
| 194 195 196 197 198 each_call_to_success(LCall,SgKey,Sg,Sv,HvFv_u,AbsInt,LSucc):- 199 200 201 202 each_call_to_success0([],_SgK,_Sg,_Sv,_HvFv,_AbsInt,[]). 203 each_call_to_success0([Call|LCall],SgKey,Sg,Sv,HvFv_u,AbsInt, 204 205 206 207 208 209 210 223 224 CIds=[Id|Ids], 225 | %                                                                                                                                                                                                                                                                                                                 |
| 233 234 235 236 %------------------------------------------------------------------------% 237 % query(+,+,+,+,+,+,+,-) 238 %------------------------------------------------------------------------% 239                                                                          |                                                                                                                                                                                                                                                                                                                   |
| 240 :- 241 "The success pattern of 242 @var{Succ} in the analysis 243 called is identified by 244 variables @var{Qv}.").                                                                                                                                                            |                                                                                                                                                                                                                                                                                                                   |
| 245 246                                                                                                                                                                                                                                                                             |                                                                                                                                                                                                                                                                                                                   |
| query(AbsInt,QKey,Query,Qv,_RFlag,_N,Call,Succ) 247 project(AbsInt,Query,Qv,Qv,Call,Proj), 248                                                                                                                                                                                      |                                                                                                                                                                                                                                                                                                                   |
|                                                                                                                                                                                                                                                                                     | has                                                                                                                                                                                                                                                                                                               |
| project(AbsInt,Sg,Sv,HvFv_u,Call,Proj),                                                                                                                                                                                                                                             | call_to_success(SgKey,Call,Proj,Sg,Sv,AbsInt,LSucc0),                                                                                                                                                                                                                                                             |
| each_call_to_success0(LCall,SgKey,Sg,Sv,HvFv_u,AbsInt, LSucc1).                                                                                                                                                                                                                     |                                                                                                                                                                                                                                                                                                                   |
| append(LSucc0,LSucc1,LSucc),                                                                                                                                                                                                                                                        |                                                                                                                                                                                                                                                                                                                   |
| 211 meta_call([],_HvFv_u,Call,[],Call,List,List,_AbsInt,_ClId,_Id,[]).                                                                                                                                                                                                              |                                                                                                                                                                                                                                                                                                                   |
| 212 meta_call([Body|Bodies],HvFv_u,Call,Succ0,Succ,L0,List,AbsInt,ClId,Id,Ids):- 213 214 meta_call_([Body|Bodies],HvFv_u,Call,Succ0,Succ,L0,List,AbsInt,ClId,Id,Ids):- 215                                                                                                          |                                                                                                                                                                                                                                                                                                                   |
| 216 217 218                                                                                                                                                                                                                                                                         | meta_call_body(Body,ClId,Call,Succ1,L0,L1,HvFv_u,AbsInt,Id,Ids0),                                                                                                                                                                                                                                                 |
| 219                                                                                                                                                                                                                                                                                 |                                                                                                                                                                                                                                                                                                                   |
| widen_succ(AbsInt,Succ0,Succ1,Succ2), append(Succ0,Succ1,Succ2),                                                                                                                                                                                                                    |                                                                                                                                                                                                                                                                                                                   |
| append(Ids0,Ids1,Ids), 220                                                                                                                                                                                                                                                          |                                                                                                                                                                                                                                                                                                                   |
| meta_call_(Bodies,HvFv_u,Call,Succ2,Succ,L1,List,AbsInt,ClId,Id,Ids1). meta_call_([],_HvFv_u,_Call,Succ,Succ,List,List,_AbsInt,_ClId,_Id,[]). 221 222 meta_call_body((Sg,Rest),K,Call,Exit,OldList,NewList,Vars_u,AbsInt,PId,CIds):- !,                                             |                                                                                                                                                                                                                                                                                                                   |
| 226 227 228 229                                                                                                                                                                                                                                                                     |                                                                                                                                                                                                                                                                                                                   |
| 230                                                                                                                                                                                                                                                                                 |                                                                                                                                                                                                                                                                                                                   |
|                                                                                                                                                                                                                                                                                     | !.                                                                                                                                                                                                                                                                                                                |
| 231                                                                                                                                                                                                                                                                                 |                                                                                                                                                                                                                                                                                                                   |
| concretes_to_body([],_SgKey,_AbsInt,[]).                                                                                                                                                                                                                                            |                                                                                                                                                                                                                                                                                                                   |
| 232 concretes_to_body([Sg|Sgs],SgKey,AbsInt,[B|Bs]):- body_info0(Sg:SgKey,[],AbsInt,B), concretes_to_body(Sgs,SgKey,AbsInt,Bs).                                                                                                                                                     |                                                                                                                                                                                                                                                                                                                   |
| doc(query(AbsInt,QKey,Query,Qv,RFlag,N,Call,Succ), @var{Query} with domain                                                                                                                                                                                                          |                                                                                                                                                                                                                                                                                                                   |
| @var{QKey}. The goal                                                                                                                                                                                                                                                                |                                                                                                                                                                                                                                                                                                                   |
| @var{AbsInt}.                                                                                                                                                                                                                                                                       | @var{Call} is The predicate @var{Query}                                                                                                                                                                                                                                                                           |
| :-                                                                                                                                                                                                                                                                                  |                                                                                                                                                                                                                                                                                                                   |
| call_to_success(QKey,Call,Proj,Query,Qv,AbsInt,Succ),                                                                                                                                                                                                                               | !.                                                                                                                                                                                                                                                                                                                |
|                                                                                                                                                                                                                                                                                     | body_succ(Call,Sg,Exit,OldList,NewList,Vars_u,AbsInt,Key,PId,Id).                                                                                                                                                                                                                                                 |
|                                                                                                                                                                                                                                                                                     | meta_call_body(Rest,K,Succ,Exit,IntList,NewList,Vars_u,AbsInt,PId,Ids).                                                                                                                                                                                                                                           |
| 250 query(_AbsInt,_QKey,_Query,_Qv,_RFlag,_N,_Call,_Succ):- % should never happen, but...                                                                                                                                                                                           |                                                                                                                                                                                                                                                                                                                   |
| meta_call_body(true,_,Call,Call,List,List,_,_,_,[no]):-                                                                                                                                                                                                                             |                                                                                                                                                                                                                                                                                                                   |
| meta_call_body(Sg,Key,Call,Exit,OldList,NewList,Vars_u,AbsInt,PId,[Id]):-                                                                                                                                                                                                           |                                                                                                                                                                                                                                                                                                                   |

## Appendix B PLAI Algorithm Implementation in Ciao Prolog

We include here the Ciao Prolog implementation of PLAI. As mentioned before, we have removed the comments from the file since the goal of this appendix it to make it easier for the reader to compare the Ciao Prolog code w.r.t. the code using TCLP, which we include in Appendix A. The original version is available at http://www.cliplab.org/papers/tclp-plai-iclp2019 .

```
<_FORTRAN_>
```

]).

| :- data :- data                                                                                                       | fixpoint_variant/6. approx_variant/7.                                                                                 |
|-----------------------------------------------------------------------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------------|
| init_fixpoint:-                                                                                                       | init_fixpoint:-                                                                                                       |
| retractall_fact(approx(_,_,_,_,_,_)),                                                                                 | retractall_fact(approx(_,_,_,_,_,_)),                                                                                 |
| retractall_fact(fixpoint(_,_,_,_,_,_)),                                                                               | retractall_fact(fixpoint(_,_,_,_,_,_)),                                                                               |
| retractall_fact('$depend_list'(_,_,_)),                                                                               | retractall_fact('$depend_list'(_,_,_)),                                                                               |
| retractall_fact(ch_id(_,_)),                                                                                          | retractall_fact(ch_id(_,_)),                                                                                          |
| retractall_fact(fixpoint_variant(_,_,_,_,_,_)),                                                                       | retractall_fact(fixpoint_variant(_,_,_,_,_,_)),                                                                       |
| retractall_fact(approx_variant(_,_,_,_,_,_,_)),                                                                       | retractall_fact(approx_variant(_,_,_,_,_,_,_)),                                                                       |
| trace_fixp:cleanup. cleanup_fixpoint(AbsInt):-                                                                        | trace_fixp:cleanup. cleanup_fixpoint(AbsInt):-                                                                        |
| cleanup_plai_db(AbsInt),                                                                                              | cleanup_plai_db(AbsInt),                                                                                              |
| cleanup_trusts(AbsInt),                                                                                               | cleanup_trusts(AbsInt),                                                                                               |
| retractall_fact(fixp_id(_)),                                                                                          | retractall_fact(fixp_id(_)),                                                                                          |
| asserta_fact(fixp_id(0)), % there is no way to recover this init_fixpoint. % if several analyses coexist!             | asserta_fact(fixp_id(0)), % there is no way to recover this init_fixpoint. % if several analyses coexist!             |
| approx_to_completes(AbsInt):-                                                                                         | approx_to_completes(AbsInt):-                                                                                         |
| current_fact(approx(SgKey,Sg,Proj,Prime,Pid,Fs),Ref),                                                                 | current_fact(approx(SgKey,Sg,Proj,Prime,Pid,Fs),Ref),                                                                 |
| asserta_fact(complete(SgKey,AbsInt,Sg,Proj,Prime,Pid,Fs)),                                                            | asserta_fact(complete(SgKey,AbsInt,Sg,Proj,Prime,Pid,Fs)),                                                            |
| erase(Ref),                                                                                                           | erase(Ref),                                                                                                           |
| fail.                                                                                                                 | fail.                                                                                                                 |
| approx_to_completes(AbsInt):-                                                                                         | approx_to_completes(AbsInt):-                                                                                         |
| current_fact(approx_variant(_Id,Pid,SgKey,Sg,Proj,Prime,Fs),Ref),                                                     | current_fact(approx_variant(_Id,Pid,SgKey,Sg,Proj,Prime,Fs),Ref),                                                     |
| asserta_fact(complete(SgKey,AbsInt,Sg,Proj,Prime,Pid,Fs)),                                                            | asserta_fact(complete(SgKey,AbsInt,Sg,Proj,Prime,Pid,Fs)),                                                            |
| erase(Ref),                                                                                                           | erase(Ref),                                                                                                           |
| fail.                                                                                                                 | fail.                                                                                                                 |
| %------------------------------------------------------------------------%                                            | %------------------------------------------------------------------------%                                            |
| call_to_success(+,+,+,+,+,+,+,-,-,+,+,+) % %------------------------------------------------------------------------% | call_to_success(+,+,+,+,+,+,+,-,-,+,+,+) % %------------------------------------------------------------------------% |
| call_to_success(_RFlag,SgKey,Call,Proj,Sg,Sv,AbsInt,_ClId,Succ,List,F,N,Id):-                                         | call_to_success(_RFlag,SgKey,Call,Proj,Sg,Sv,AbsInt,_ClId,Succ,List,F,N,Id):-                                         |
| % ClId = number identifying the clause?... for an entry point is 0...                                                 | % ClId = number identifying the clause?... for an entry point is 0...                                                 |
| % F = program point of the call. clauseId+/0 for an entry call                                                        | % F = program point of the call. clauseId+/0 for an entry call                                                        |
| current_fact(complete(SgKey,AbsInt,Subg,Proj1,Prime1,Id,Fs),R),                                                       | current_fact(complete(SgKey,AbsInt,Subg,Proj1,Prime1,Id,Fs),R),                                                       |
| identical_proj(AbsInt,Sg,Proj,Subg,Proj1), !,                                                                         | identical_proj(AbsInt,Sg,Proj,Subg,Proj1), !,                                                                         |
| patch_parents(R,complete(SgKey,AbsInt,Subg,Proj1,Prime1,Id,Ps),F,N,Ps,Fs), List = [],                                 | patch_parents(R,complete(SgKey,AbsInt,Subg,Proj1,Prime1,Id,Ps),F,N,Ps,Fs), List = [],                                 |
| each_abs_sort(Prime1,AbsInt,Prime), each_extend(Sg,Prime,AbsInt,Sv,Call,Succ).                                        | each_abs_sort(Prime1,AbsInt,Prime), each_extend(Sg,Prime,AbsInt,Sv,Call,Succ).                                        |
| call_to_success(r,SgKey,Call,Proj,Sg,Sv,AbsInt,_ClId,Succ,List,F,N,Id) :-                                             | call_to_success(r,SgKey,Call,Proj,Sg,Sv,AbsInt,_ClId,Succ,List,F,N,Id) :-                                             |
| current_fact(approx(SgKey,Subg,Proj1,Prime1,Id,Fs),Ref),                                                              | current_fact(approx(SgKey,Subg,Proj1,Prime1,Id,Fs),Ref),                                                              |
| identical_proj(AbsInt,Sg,Proj,Subg,Proj1), !,                                                                         | identical_proj(AbsInt,Sg,Proj,Subg,Proj1), !,                                                                         |
| each_abs_sort(Prime1,AbsInt,TempPrime),                                                                               | each_abs_sort(Prime1,AbsInt,TempPrime),                                                                               |
| current_fact('$depend_list'(Id,SgKey,IdList)),                                                                        | current_fact('$depend_list'(Id,SgKey,IdList)),                                                                        |
| call_to_success_approx(SgKey,Subg,Call,Proj,Proj1,Sg,Sv,AbsInt,F,N,Fs, Id,Ref,IdList,Prime1,TempPrime,List,Prime),    | call_to_success_approx(SgKey,Subg,Call,Proj,Proj1,Sg,Sv,AbsInt,F,N,Fs, Id,Ref,IdList,Prime1,TempPrime,List,Prime),    |
| each_extend(Sg,Prime,AbsInt,Sv,Call,Succ).                                                                            | each_extend(Sg,Prime,AbsInt,Sv,Call,Succ).                                                                            |
| call_to_success(r,SgKey,Call,Proj,Sg,Sv,AbsInt,_ClId,Succ,List,F,N,Id):-                                              | call_to_success(r,SgKey,Call,Proj,Sg,Sv,AbsInt,_ClId,Succ,List,F,N,Id):-                                              |
| current_fact(fixpoint(SgKey,Subg,Proj1,Prime1,Id,Fs),Ref), identical_proj(AbsInt,Sg,Proj,Subg,Proj1), !,              | current_fact(fixpoint(SgKey,Subg,Proj1,Prime1,Id,Fs),Ref), identical_proj(AbsInt,Sg,Proj,Subg,Proj1), !,              |
| patch_parents(Ref,fixpoint(SgKey,Subg,Proj1,Prime1,Id,Ps),F,N,Ps,Fs),                                                 | patch_parents(Ref,fixpoint(SgKey,Subg,Proj1,Prime1,Id,Ps),F,N,Ps,Fs),                                                 |
| current_fact(ch_id(Id,Num)),                                                                                          | current_fact(ch_id(Id,Num)),                                                                                          |
| List = [Id/Num],                                                                                                      | List = [Id/Num],                                                                                                      |
| each_abs_sort(Prime1,AbsInt,Prime),                                                                                   | each_abs_sort(Prime1,AbsInt,Prime),                                                                                   |
| each_extend(Sg,Prime,AbsInt,Sv,Call,Succ).                                                                            | each_extend(Sg,Prime,AbsInt,Sv,Call,Succ).                                                                            |
| current_pp_flag(variants,on),                                                                                         | current_pp_flag(variants,on),                                                                                         |
| current_fact(complete(SgKey,AbsInt,Subg,Proj1,Prime1,_Id1,_Fs),_R),                                                   | current_fact(complete(SgKey,AbsInt,Subg,Proj1,Prime1,_Id1,_Fs),_R),                                                   |
| identical_proj_1(AbsInt,Sg,Proj,Subg,Proj1,Prime1,Prime2), !,                                                         | identical_proj_1(AbsInt,Sg,Proj,Subg,Proj1,Prime1,Prime2), !,                                                         |
| call_to_success(_RFlag,SgKey,Call,Proj,Sg,Sv,AbsInt,_ClId,Succ,List,F,N,Id):-                                         | call_to_success(_RFlag,SgKey,Call,Proj,Sg,Sv,AbsInt,_ClId,Succ,List,F,N,Id):-                                         |

## 23

| 123 124         | ( current_pp_flag(reuse_fixp_id,on) -> fixpoint_id_reuse_prev(SgKey,AbsInt,Sg,Proj,Id)                                                         |                                  |                                                                        |         |
|-----------------|------------------------------------------------------------------------------------------------------------------------------------------------|----------------------------------|------------------------------------------------------------------------|---------|
| 125             | ;                                                                                                                                              |                                  |                                                                        |         |
| 126 127         | fixpoint_id(Id)                                                                                                                                |                                  |                                                                        |         |
| 128             | ), each_abs_sort(Prime2,AbsInt,Prime),                                                                                                         |                                  |                                                                        |         |
| 129             | List = [],                                                                                                                                     |                                  |                                                                        |         |
| 130             | asserta_fact(complete(SgKey,AbsInt,Sg,Proj,Prime,Id,[(F,N)])),                                                                                 |                                  |                                                                        |         |
| 131             | each_extend(Sg,Prime,AbsInt,Sv,Call,Succ).                                                                                                     |                                  |                                                                        |         |
| 132             | call_to_success(r,SgKey,Call,Proj,Sg,Sv,AbsInt,_ClId,Succ,List,F,N,Id) :-                                                                      |                                  |                                                                        |         |
| 133             | current_pp_flag(variants,on),                                                                                                                  |                                  |                                                                        |         |
| 134             | current_fact(approx(SgKey,Subg,Proj1,Prime1,Id1,Fs),Ref), identical_proj_1(AbsInt,Sg,Proj,Subg,Proj1,Prime1,Prime2), !,                        |                                  |                                                                        |         |
| 135             | each_abs_sort(Prime2,AbsInt,TempPrime),                                                                                                        |                                  |                                                                        |         |
| 136             |                                                                                                                                                |                                  |                                                                        |         |
| 137             | current_fact('$depend_list'(Id1,SgKey,IdList)),                                                                                                |                                  |                                                                        |         |
| 138             | call_to_success_approx_variant(SgKey,Subg,Call,Proj,Proj1,Sg,Sv,AbsInt,F,N,Fs,                                                                 |                                  |                                                                        |         |
| 139             | Id,Id1,Ref,IdList,Prime1,TempPrime,List,Prime), each_extend(Sg,Prime,AbsInt,Sv,Call,Succ).                                                     |                                  |                                                                        |         |
| 140 141         | call_to_success(r,SgKey,Call,Proj,Sg,Sv,AbsInt,_ClId,Succ,List,F,N,Id):- current_pp_flag(variants,on),                                         |                                  |                                                                        |         |
| 142             | current_fact(fixpoint(SgKey,Subg,Proj1,Prime1,Id1,_Fs),_Ref),                                                                                  |                                  |                                                                        |         |
| 143             | identical_proj_1(AbsInt,Sg,Proj,Subg,Proj1,Prime1,Prime2), !, (                                                                                |                                  |                                                                        |         |
| 144             | current_fact(fixpoint_variant(Id1,Id,SgKey,Sgv,Projv,Fsv),Refv),                                                                               |                                  |                                                                        |         |
| 145 146         | identical_proj(AbsInt,Sg,Proj,Sgv,Projv) ->                                                                                                    |                                  |                                                                        |         |
| 147 148 149     | patch_parents(Refv,fixpoint_variant(Id1,Id,SgKey,Sgv,Projv,Ps),F,N,Ps,Fsv)                                                                     | ;                                |                                                                        |         |
|                 | ( current_pp_flag(reuse_fixp_id,on) ->                                                                                                         |                                  |                                                                        |         |
| 150 151 152 153 | fixpoint_id_reuse_prev(SgKey,AbsInt,Sg,Proj,Id)                                                                                                |                                  |                                                                        |         |
|                 | ; fixpoint_id(Id)                                                                                                                              |                                  |                                                                        |         |
| 154 155 156     | ),                                                                                                                                             |                                  |                                                                        |         |
| 157             | asserta_fact(fixpoint_variant(Id1,Id,SgKey,Sg,Proj,[(F,N)])) ),                                                                                |                                  |                                                                        |         |
| 158             | each_abs_sort(Prime2,AbsInt,Prime),                                                                                                            |                                  |                                                                        |         |
| 159             | current_fact(ch_id(Id1,Num)), = [Id1/Num],                                                                                                     |                                  |                                                                        |         |
| 160 161 162     | List each_extend(Sg,Prime,AbsInt,Sv,Call,Succ). :-                                                                                             |                                  |                                                                        |         |
|                 | call_to_success(r,SgKey,Call,Proj,Sg,Sv,AbsInt,_ClId,Succ,List,F,N,Id) init_fixpoint0(SgKey,Call,Proj,Sg,Sv,AbsInt,F,N,[(F,N)],Id,List,Prime), |                                  |                                                                        |         |
|                 | each_extend(Sg,Prime,AbsInt,Sv,Call,Succ). call_to_success(nr,SgKey,Call,Proj,Sg,Sv,AbsInt,ClId,Succ,[],F,N,Id):-                              |                                  |                                                                        |         |
| 163 164         |                                                                                                                                                |                                  |                                                                        |         |
|                 | ( current_pp_flag(reuse_fixp_id,on) -> fixpoint_id_reuse_prev(SgKey,AbsInt,Sg,Proj,Id)                                                         |                                  |                                                                        |         |
| 167             | ;                                                                                                                                              |                                  |                                                                        |         |
| 168 169 170     | fixpoint_id(Id) ),                                                                                                                             |                                  |                                                                        |         |
|                 | proj_to_prime_nr(SgKey,Sg,Sv,Call,Proj,AbsInt,ClId,Prime,Id), asserta_fact(complete(SgKey,AbsInt,Sg,Proj,Prime,Id,[(F,N)])),                   |                                  |                                                                        |         |
| 171             | each_extend(Sg,Prime,AbsInt,Sv,Call,Succ).                                                                                                     |                                  |                                                                        |         |
| 172             |                                                                                                                                                |                                  |                                                                        |         |
| 173 174 175 176 | call_to_success_approx(SgKey,Subg,_Call,Proj,Proj1,Sg,_Sv,_AbsInt,F,N,Fs,                                                                      |                                  |                                                                        |         |
| 177 178 179     | patch_parents(Ref,approx(SgKey,Subg,Proj1,Prime1,Id,Ps),F,N,Ps,Fs), Prime = TempPrime, List = IdList.                                          |                                  |                                                                        |         |
| 180 181         | call_to_success_approx(SgKey,_Subg,Call,Proj,_Proj1,Sg,Sv,AbsInt,F,N,Fs,                                                                       |                                  |                                                                        |         |
| 182             | Id,Ref,_IdList,_Prime1,TempPrime,List,Prime):-                                                                                                 |                                  |                                                                        |         |
|                 | erase(Ref),                                                                                                                                    |                                  |                                                                        |         |
|                 | TempPrime,List,Prime).                                                                                                                         |                                  |                                                                        |         |
| 184 185         |                                                                                                                                                |                                  |                                                                        |         |
|                 | init_fixpoint_(SgKey,Call,Proj,Sg,Sv,AbsInt,F,N,Fs,Id,                                                                                         |                                  |                                                                        |         |
| 183             |                                                                                                                                                |                                  |                                                                        |         |
| 165 166         |                                                                                                                                                |                                  |                                                                        |         |
|                 | Id,Ref,IdList,Prime1,TempPrime,List,Prime):- not_modified(IdList), !,                                                                          |                                  |                                                                        |         |
| 186             |                                                                                                                                                |                                  |                                                                        |         |
|                 |                                                                                                                                                | aproxs_to_fixpoint_variant(Id):- | current_fact(approx_variant(Id,Idv,SgKey,Sgv,Projv,_Primev,Fs),Ref),!, | 187 188 |

| asserta_fact(fixpoint_variant(Id,Idv,SgKey,Sgv,Projv,Fs)),                                                                                                                                                 |
|------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| aproxs_to_fixpoint_variant(Id). aproxs_to_fixpoint_variant(_).                                                                                                                                             |
| call_to_success_approx_variant(SgKey,_Subg,_Call,Proj,_Proj1,Sg,_Sv,AbsInt,F,N,_Fs, Id,Id1,_Ref,IdList,_Prime1,TempPrime,List,Prime):- not_modified(IdList), !,                                            |
| ( current_fact(approx_variant(Id1,Id,SgKey,Sgv,Projv,Primev,Fsv),Refv), identical_proj(AbsInt,Sg,Proj,Sgv,Projv) ->                                                                                        |
| patch_parents(Refv,approx_variant(Id1,Id,SgKey,Sgv,Projv,Primev,Ps),F,N,Ps,Fsv) ; (                                                                                                                        |
| current_pp_flag(reuse_fixp_id,on) -> fixpoint_id_reuse_prev(SgKey,AbsInt,Sg,Proj,Id)                                                                                                                       |
| ;                                                                                                                                                                                                          |
| fixpoint_id(Id)                                                                                                                                                                                            |
| ),                                                                                                                                                                                                         |
| asserta_fact(approx_variant(Id1,Id,SgKey,Sg,Proj,TempPrime,[(F,N)])) ), = TempPrime,                                                                                                                       |
| Prime List                                                                                                                                                                                                 |
| = IdList. call_to_success_approx_variant(SgKey,Subg,Call,Proj,Proj1,Sg,Sv,AbsInt,F,N,Fs, Id,Id1,Ref,_IdList,Prime1,_TempPrime,List,Prime):-                                                                |
| ( current_fact(approx_variant(Id1,Id,SgKey,Sgv,Projv,_Primev,Fsv),Refv),                                                                                                                                   |
| identical_proj(AbsInt,Sg,Proj,Sgv,Projv) -> erase(Refv),                                                                                                                                                   |
| ( member((F,N),Fsv) -> NewFs = Fsv ; NewFs = [(F,N)|Fsv] %) ;                                                                                                                                              |
| ( current_pp_flag(reuse_fixp_id,on) ->                                                                                                                                                                     |
| fixpoint_id_reuse_prev(SgKey,AbsInt,Sg,Proj,Id)                                                                                                                                                            |
| ; fixpoint_id(Id)                                                                                                                                                                                          |
| ), NewFs = [(F,N)]                                                                                                                                                                                         |
| ),                                                                                                                                                                                                         |
| aproxs_to_fixpoint_variant(Id1),                                                                                                                                                                           |
| erase(Ref), asserta_fact(fixpoint_variant(Id1,Id,SgKey,Sg,Proj,NewFs)), varset(Subg,Subv),                                                                                                                 |
| init_fixpoint_(SgKey,Call,Proj1,Subg,Subv,AbsInt,F,N,Fs,Id1,                                                                                                                                               |
| Prime1,List,Prime0),                                                                                                                                                                                       |
| each_exit_to_prime(Prime0,AbsInt,Sg,Subv,Subg,Sv,(no,Proj),Prime).                                                                                                                                         |
| init_fixpoint2(SgKey,Call,Proj,Sg,Sv,AbsInt,F,N,Fs,Id,List,Prime). init_fixpoint1(SgKey,_Call,Proj,Sg,_Sv,AbsInt,F,N,_Fs0,Id,List,Prime):- current_fact(complete(SgKey,AbsInt,Subg,Proj1,Prime1,Id,Fs),R), |
| patch_parents(R,complete(SgKey,AbsInt,Subg,Proj1,Prime1,Id,Ps),F,N,Ps,Fs), = [],                                                                                                                           |
| List each_abs_sort(Prime1,AbsInt,Prime).                                                                                                                                                                   |
| init_fixpoint1(SgKey,Call,Proj,Sg,Sv,AbsInt,F,N,_Fs0,Id,List,Prime):-                                                                                                                                      |
| identical_proj(AbsInt,Sg,Proj,Subg,Proj1), !,                                                                                                                                                              |
| current_fact(approx(SgKey,Subg,Proj1,Prime1,Id,Fs),Ref),                                                                                                                                                   |
| each_abs_sort(Prime1,AbsInt,TempPrime), current_fact('$depend_list'(Id,SgKey,IdList)),                                                                                                                     |
| !,                                                                                                                                                                                                         |
| identical_proj(AbsInt,Sg,Proj,Subg,Proj1),                                                                                                                                                                 |
| init_fixpoint0(SgKey,Call,Proj,Sg,Sv,AbsInt,F,N,Fs,Id,List,Prime):-                                                                                                                                        |
| init_fixpoint1(SgKey,_,Proj,Sg,_Sv,AbsInt,F,N,_Fs0,Id,List,Prime):- current_fact(fixpoint(SgKey,Subg,Proj1,Prime1,Id,Fs),Ref),                                                                             |
| call_to_success_approx(SgKey,Subg,Call,Proj,Proj1,Sg,Sv,AbsInt,F,N,Fs,                                                                                                                                     |
| Id,Ref,IdList,Prime1,TempPrime,List,Prime).                                                                                                                                                                |

| identical_proj(AbsInt,Sg,Proj,Subg,Proj1), !, patch_parents(Ref,fixpoint(SgKey,Subg,Proj1,Prime1,Id,Ps),F,N,Ps,Fs),   |    |
|-----------------------------------------------------------------------------------------------------------------------|----|
| current_fact(ch_id(Id,Num)),                                                                                          |    |
| List = [Id/Num],                                                                                                      |    |
| each_abs_sort(Prime1,AbsInt,Prime). init_fixpoint1(SgKey,_Call,Proj,Sg,_Sv,AbsInt,F,N,_Fs0,Id,List,Prime):-           |    |
| current_pp_flag(variants,on),                                                                                         |    |
| current_fact(complete(SgKey,AbsInt,Subg,Proj1,Prime1,_Id1,_Fs),_R),                                                   |    |
| identical_proj_1(AbsInt,Sg,Proj,Subg,Proj1,Prime1,Prime2), !,                                                         |    |
| ( current_pp_flag(reuse_fixp_id,on) ->                                                                                |    |
| fixpoint_id_reuse_prev(SgKey,AbsInt,Sg,Proj,Id) ;                                                                     |    |
| fixpoint_id(Id)                                                                                                       |    |
| ), each_abs_sort(Prime2,AbsInt,Prime),                                                                                |    |
| List = [],                                                                                                            |    |
| asserta_fact(complete(SgKey,AbsInt,Sg,Proj,Prime,Id,[(F,N)])).                                                        |    |
| init_fixpoint1(SgKey,Call,Proj,Sg,Sv,AbsInt,F,N,_Fs0,Id,List,Prime):-                                                 |    |
| current_pp_flag(variants,on),                                                                                         |    |
| current_fact(approx(SgKey,Subg,Proj1,Prime1,Id1,Fs),Ref),                                                             |    |
| identical_proj_1(AbsInt,Sg,Proj,Subg,Proj1,Prime1,Prime2), !, each_abs_sort(Prime2,AbsInt,TempPrime),                 |    |
| current_fact('$depend_list'(Id1,SgKey,IdList)),                                                                       |    |
| call_to_success_approx_variant(SgKey,Subg,Call,Proj,Proj1,Sg,Sv,AbsInt,F,N,Fs,                                        |    |
| Id,Id1,Ref,IdList,Prime1,TempPrime,List,Prime). init_fixpoint1(SgKey,_,Proj,Sg,_Sv,AbsInt,F,N,_Fs0,Id,List,Prime):-   |    |
| current_pp_flag(variants,on),                                                                                         |    |
| current_fact(fixpoint(SgKey,Subg,Proj1,Prime1,Id1,_Fs),_Ref),                                                         |    |
| identical_proj_1(AbsInt,Sg,Proj,Subg,Proj1,Prime1,Prime2), !,                                                         | (  |
| current_fact(fixpoint_variant(Id1,Id,SgKey,Sgv,Projv,Fsv),Refv), identical_proj(AbsInt,Sg,Proj,Sgv,Projv) ->          |    |
| patch_parents(Refv,fixpoint_variant(Id1,Id,SgKey,Sgv,Projv,Ps),F,N,Ps,Fsv)                                            | ;  |
| (                                                                                                                     |    |
| current_pp_flag(reuse_fixp_id,on) ->                                                                                  |    |
| fixpoint_id_reuse_prev(SgKey,AbsInt,Sg,Proj,Id)                                                                       |    |
| ; fixpoint_id(Id)                                                                                                     |    |
| ), asserta_fact(fixpoint_variant(Id1,Id,SgKey,Sg,Proj,[(F,N)]))                                                       |    |
| init_fixpoint1(SgKey,Call,Proj,Sg,Sv,AbsInt,F,N,Fs,Id,List,Prime):-                                                   |    |
| init_fixpoint2(SgKey,Call,Proj,Sg,Sv,AbsInt,F,N,Fs,Id,List,Prime).                                                    |    |
| init_fixpoint2(SgKey,Call,Proj,Sg,Sv,AbsInt,F,N,Fs,Id,List,Prime):-                                                   |    |
| current_pp_flag(reuse_fixp_id,on) -> fixpoint_id_reuse_prev(SgKey,AbsInt,Sg,Proj,Id)                                  |    |
| fixpoint_id(Id)                                                                                                       |    |
| ),                                                                                                                    |    |
| asserta_fact(ch_id(Id,1)),                                                                                            |    |
| TempPrime,List,Prime).                                                                                                |    |
| normalize_asub0(AbsInt,Prime0,TempPrime),                                                                             |    |
| asserta_fact(fixpoint(SgKey,Sg,Proj,TempPrime,Id,Fs)),                                                                |    |
| X^(trans_clause(SgKey,r,X)),Clauses),!,                                                                               |    |
| fixpoint_compute(Clauses,SgKey,Sg,Sv,Call,Proj, AbsInt,_LEntry,TempPrime,Prime1,Id,TempList),                         |    |
| = [Id1/Num].                                                                                                          |    |
| ),                                                                                                                    |    |
| each_abs_sort(Prime2,AbsInt,Prime),                                                                                   |    |
| current_fact(ch_id(Id1,Num)),                                                                                         |    |
| List                                                                                                                  |    |
| bagof(X,                                                                                                              |    |
| init_fixpoint_(SgKey,Call,Proj,Sg,Sv,AbsInt,F,N,Fs,Id,Prime0,List,Prime):-                                            |    |
| proj_to_prime_r(SgKey,Sg,Sv,Call,Proj,AbsInt,TempPrime,Id),                                                           |    |
|                                                                                                                       | ;  |
| (                                                                                                                     |    |
| init_fixpoint_(SgKey,Call,Proj,Sg,Sv,AbsInt,F,N,Fs,Id,                                                                |    |

| 321                                                   | current_fact(fixpoint(SgKey,Sg,_,_,Id,Fs2),Ref),                                                                                                                     |     |     |
|-------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------|-----|-----|
| 322                                                   | erase(Ref),                                                                                                                                                          |     |     |
| 323                                                   | ( current_fact('$depend_list'(Id,SgKey,_),RefDep) ->                                                                                                                 |     |     |
| 324                                                   | erase(RefDep) ;                                                                                                                                                      |     |     |
| 325                                                   | true                                                                                                                                                                 |     |     |
| 326                                                   | ), update_if_member_idlist(TempList,Id,AddList),                                                                                                                     |     |     |
| 327 328                                               | ( member((F,N),Fs2) -> NewFs = Fs2 ; NewFs = [(F,N)|Fs2]                                                                                                             |     |     |
| 329                                                   | ), decide_approx(AddList,Id,NewFs,AbsInt,SgKey,Sg,Proj,Prime),                                                                                                       |     |     |
| 330                                                   |                                                                                                                                                                      |     |     |
|                                                       | List = AddList.                                                                                                                                                      |     |     |
| 331 332 333 334                                       | widen_call(AbsInt,SgKey,Sg,F1,Id0,Proj1,Proj):- ( current_pp_flag(widencall,off) -> fail ; true ), widen_call0(AbsInt,SgKey,Sg,F1,Id0,[Id0],Proj1,Proj), !.          |     |     |
| 335 336 337                                           | widen_call0(AbsInt,SgKey,Sg,F1,Id0,Ids,Proj1,Proj):-                                                                                                                 |     |     |
|                                                       | widen_call1(AbsInt,SgKey,Sg,F1,Id0,Ids,Proj1,Proj). widen_call0(AbsInt,SgKey,Sg,F1,Id0,Ids,Proj1,Proj):-                                                             |     |     |
| 338                                                   | current_pp_flag(widencall,com_child),                                                                                                                                |     |     |
| 339 340                                               |                                                                                                                                                                      |     |     |
|                                                       | widen_call2(AbsInt,SgKey,Sg,F1,Id0,Ids,Proj1,Proj).                                                                                                                  |     |     |
| 342                                                   | widen_call1(AbsInt,SgKey,Sg,F1,Id0,Ids,Proj1,Proj):- current_fact(fixpoint(SgKey0,Sg0,Proj0,_Prime0,Id0,Fs0)),                                                       |     |     |
| 343 344                                               | ( SgKey=SgKey0, % same program point:                                                                                                                                |     |     |
| 345 346                                               | member((F1,_NewId0),Fs0)                                                                                                                                             |     |     |
| 347                                                   | -> Sg0=Sg,                                                                                                                                                           |     |     |
| 348                                                   |                                                                                                                                                                      |     |     |
| 349                                                   | abs_sort(AbsInt,Proj0,Proj0_s), abs_sort(AbsInt,Proj1,Proj1_s),                                                                                                      |     |     |
| 350 351                                               | widencall(AbsInt,Proj0_s,Proj1_s,Proj)                                                                                                                               |     |     |
| 352 353                                               | ; % continue with the parents:                                                                                                                                       |     |     |
|                                                       | member((_F1,NewId0),Fs0),                                                                                                                                            |     |     |
| 354 355                                               | \+ member(NewId0,Ids),                                                                                                                                               |     |     |
|                                                       | widen_call1(AbsInt,SgKey,Sg,F1,NewId0,[NewId0|Ids],Proj1,Proj)                                                                                                       |     |     |
| 356                                                   |                                                                                                                                                                      |     |     |
| widen_call2(AbsInt,SgKey,Sg,F1,_Id,_Ids,Proj1,Proj):- | ).                                                                                                                                                                   |     |     |
| 357 358                                               | current_fact(complete(SgKey,AbsInt,Sg0,Proj0,_Prime0,_Id0,Fs0)), member((F1,Id0),Fs0), Sg0=Sg,                                                                       |     |     |
| 359 360 361                                           | same_fixpoint_ancestor(Id0,[Id0],AbsInt),                                                                                                                            |     |     |
| 362 363                                               |                                                                                                                                                                      |     |     |
| 364                                                   | abs_sort(AbsInt,Proj1,Proj1_s),                                                                                                                                      |     |     |
| 365                                                   | widencall(AbsInt,Proj0_s,Proj1_s,Proj).                                                                                                                              |     |     |
| 366                                                   | same_fixpoint_ancestor(Id0,_Ids,_AbsInt):- !.                                                                                                                        |     |     |
|                                                       | current_fact(fixpoint(_SgKey0,_Sg0,_Proj0,_Prime0,Id0,_Fs0)), same_fixpoint_ancestor(Id0,_Ids,_AbsInt):- current_fact(approx(_SgKey0,_Sg0,_Proj0,_Prime0,Id0,_Fs0)), |     |     |
| 367 368 369                                           | !. same_fixpoint_ancestor(Id0,Ids,AbsInt):-                                                                                                                          |     |     |
|                                                       | current_fact(complete(_SgKey0,AbsInt,_Sg0,_Proj0,_Prime0,Id0,Fs0)),                                                                                                  |     |     |
| 370                                                   | member((_F1,Id),Fs0),                                                                                                                                                |     |     |
| 371 372 373                                           | \+ member(Id,Ids),                                                                                                                                                   |     |     |
| 374 375 376                                           |                                                                                                                                                                      |     |     |
|                                                       | same_fixpoint_ancestor(Id,[Id|Ids],AbsInt).                                                                                                                          |     |     |
| 377                                                   | fixpoint_variants_update(Id,AbsInt,Sg,Prime):- current_fact(fixpoint_variant(Id,Idv,SgKey,Sgv,Projv,Fs),Ref),!, erase(Ref), varset(Sg,Hv),                           |     |     |
| 378 379 380                                           | each_exit_to_prime(Prime,AbsInt,Sgv,Hv,Sg,Hvv,(no,Projv),Prime2), asserta_fact(complete(SgKey,AbsInt,Sgv,Projv,Prime2,Idv,Fs)),                                      |     |     |
| 383 384                                               |                                                                                                                                                                      |     |     |
|                                                       | fixpoint_variants_update(Id,AbsInt,Sg,Prime).                                                                                                                        |     |     |
|                                                       | varset(Sgv,Hvv),                                                                                                                                                     |     |     |
| 381                                                   |                                                                                                                                                                      |     |     |
| 382                                                   |                                                                                                                                                                      |     |     |
|                                                       | abs_sort(AbsInt,Proj0,Proj0_s),                                                                                                                                      |     |     |
|                                                       | fixpoint_variants_update(_,_,_,_).                                                                                                                                   |     |     |
|                                                       | approx_variants_update(Id,AbsInt,Sg,Prime):-                                                                                                                         |     |     |
|                                                       |                                                                                                                                                                      | 386 | 385 |

| 387                                                                          | current_fact(fixpoint_variant(Id,Idv,SgKey,Sgv,Projv,Fs),Ref),!, erase(Ref),                                                                                            |
|------------------------------------------------------------------------------|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| 388 389                                                                      | varset(Sg,Hv),                                                                                                                                                          |
| 390                                                                          | varset(Sgv,Hvv),                                                                                                                                                        |
| 391                                                                          | each_exit_to_prime(Prime,AbsInt,Sgv,Hv,Sg,Hvv,(no,Projv),Prime2),                                                                                                       |
| 392 393                                                                      | asserta_fact(approx_variant(Id,Idv,SgKey,Sgv,Projv,Prime2,Fs)), approx_variants_update(Id,AbsInt,Sg,Prime).                                                             |
| 394                                                                          | approx_variants_update(_,_,_,_).                                                                                                                                        |
| current_fact(ch_id(Id,_),Ref3), 398 399                                      | erase(Ref3), % Not needed for correctness: only book-keeping                                                                                                            |
| 400                                                                          | % update_depend_list_approx(Id,AbsInt),                                                                                                                                 |
| 401                                                                          | asserta_fact(complete(SgKey,AbsInt,Sg,Proj,Prime,Id,Fs)),                                                                                                               |
| 402 ( 403                                                                    | current_pp_flag(variants,on) ->                                                                                                                                         |
| 404 405                                                                      | each_abs_sort(Prime,AbsInt,Prime_s), fixpoint_variants_update(Id,AbsInt,Sg,Prime_s)                                                                                     |
| ; 407 408                                                                    | true                                                                                                                                                                    |
| 409                                                                          | ). decide_approx(AddList,Id,Fs,_AbsInt,SgKey,Sg,Proj,Prime):-                                                                                                           |
| 410                                                                          | asserta_fact('$depend_list'(Id,SgKey,AddList)),                                                                                                                         |
| 411 (                                                                        | asserta_fact(approx(SgKey,Sg,Proj,Prime,Id,Fs),_),                                                                                                                      |
| 413                                                                          | current_pp_flag(variants,on) ->                                                                                                                                         |
| 414 415                                                                      | each_abs_sort(Prime,AbsInt,Prime_s), approx_variants_update(Id,AbsInt,Sg,Prime_s)                                                                                       |
| 416 ;                                                                        |                                                                                                                                                                         |
| 417 ).                                                                       | true                                                                                                                                                                    |
| 419 420 421                                                                  |                                                                                                                                                                         |
| not_modified([]).                                                            |                                                                                                                                                                         |
| not_modified([Id/N|List]):-                                                  | current_fact(ch_id(Id,N)), !, not_modified(List).                                                                                                                       |
| 422 423                                                                      |                                                                                                                                                                         |
| 424 425                                                                      | proj_to_prime_nr(SgKey,Sg,Sv,Call,Proj,AbsInt,_ClId,LPrime,Id) :- X^(trans_clause(SgKey,nr,X)),Clauses), !,                                                             |
| 427 428                                                                      | proj_to_prime(Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,LPrime1,Id), :-                                                                                                      |
| 429 430                                                                      | compute_clauses_lub(AbsInt,Proj,LPrime1,LPrime). proj_to_prime_nr(SgKey,Sg,Sv,_Call,Proj,AbsInt,ClId,LPrime,_Id) apply_trusted0(Proj,SgKey,Sg,Sv,AbsInt,ClId,Prime), !, |
| 432                                                                          | :-                                                                                                                                                                      |
| 431                                                                          | singleton(Prime,LPrime).                                                                                                                                                |
| 434                                                                          | In Java programs, mode and type information is Therefore, in case of a method with we can still infer useful information.                                               |
| 435 436                                                                      | % % ( current_pp_flag(prog_lang,java) ->                                                                                                                                |
| 437                                                                          | unknown_call(AbsInt,Sg,Sv,Call,Succ),                                                                                                                                   |
| 438 439 ;                                                                    | singleton(Succ,LSucc)                                                                                                                                                   |
|                                                                              | fail                                                                                                                                                                    |
| 440                                                                          | ).                                                                                                                                                                      |
| 441 442 proj_to_prime_nr(SgKey,_Sg,_Sv,_Call,_Proj,_AbsInt,ClId,Bot,_Id) 443 | :- bottom(Bot),                                                                                                                                                         |
| 444 445 446                                                                  | inexistent(SgKey,ClId).                                                                                                                                                 |
|                                                                              | proj_to_prime_r(SgKey,Sg,Sv,Call,Proj,AbsInt,Prime,Id) :- bagof(X, X^(trans_clause(SgKey,nr,X)),Clauses), !,                                                            |
|                                                                              | proj_to_prime(Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,Prime,Id).                                                                                                           |
| 447 448                                                                      | proj_to_prime_r(_SgKey,_Sg,_Sv,_Call,_Proj,_AbsInt,Bot,_Id):-                                                                                                           |
| 450 451                                                                      | bottom(Bot).                                                                                                                                                            |
|                                                                              | proj_to_prime(Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,Prime,Id) :-                                                                                                         |
| 452                                                                          |                                                                                                                                                                         |
| 449                                                                          |                                                                                                                                                                         |
| 426                                                                          | bagof(X,                                                                                                                                                                |
|                                                                              | proj_to_prime_nr(_SgKey,Sg,Sv,Call,_Proj,AbsInt,_ClId,LSucc,_Id)                                                                                                        |
| 433                                                                          | known for any method.                                                                                                                                                   |
|                                                                              | unavailable                                                                                                                                                             |
|                                                                              | code                                                                                                                                                                    |
|                                                                              | %                                                                                                                                                                       |

| 453 454             | proj_to_prime_loop(Clauses,Sg,Sv,Call,Proj,AbsInt,ListPrime0,Id), reduce_equivalent(ListPrime0,AbsInt,ListPrime1),                                                                                                                                      |         |     |                              |        |     |
|---------------------|---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|---------|-----|------------------------------|--------|-----|
| 455 456             | each_apply_trusted(Proj,SgKey,Sg,Sv,AbsInt,ListPrime1,Prime). proj_to_prime_loop([],_,_,_,_,_,[],_).                                                                                                                                                    |         |     |                              |        |     |
| 457 458             | proj_to_prime_loop([Clause|Rest],Sg,Sv,Call,Proj,AbsInt,Primes,Id):-                                                                                                                                                                                    |         |     |                              |        |     |
| 459                 | do_nr_cl(Clause,Sg,Sv,Call,Proj,AbsInt,Primes,TailPrimes,Id),!,                                                                                                                                                                                         |         |     |                              |        |     |
| 460 461 462         | proj_to_prime_loop(Rest,Sg,Sv,Call,Proj,AbsInt,TailPrimes,Id).                                                                                                                                                                                          |         |     |                              |        |     |
|                     | do_nr_cl(Clause,Sg,Sv,Call,Proj,AbsInt,Primes,TailPrimes,Id):- Clause = clause(Head,Vars_u,K,Body),                                                                                                                                                     |         |     |                              |        |     |
| 463                 | clause_applies(Head,Sg), !, varset(Head,Hv),                                                                                                                                                                                                            |         |     |                              |        |     |
| 464 465 466         | sort(Vars_u,Vars),                                                                                                                                                                                                                                      |         |     |                              |        |     |
| 467                 |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
| 468                 |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
|                     | ord_subtract(Vars,Hv,Fv), process_body(Body,K,AbsInt,Sg,Hv,Fv,Vars_u,Head,Sv,Call,                                                                                                                                                                      |         |     |                              |        |     |
| 469 470             | Proj,LPrime,Id), append_(LPrime,TailPrimes,Primes).                                                                                                                                                                                                     |         |     |                              |        |     |
| 471 472             | do_nr_cl(_Clause,_Sg,_Sv,_Call,_Proj,_AbsInt,Primes,Primes,_Id). append_([Prime],TailPrimes,Primes):- !, Primes=[Prime|TailPrimes].                                                                                                                     |         |     |                              |        |     |
| 473 474             | append_(LPrime,TailPrimes,Primes):- append(LPrime,TailPrimes,Primes).                                                                                                                                                                                   |         |     |                              |        |     |
|                     | Help=(Sv,Sg,Hv,Fv,AbsInt), singleton(Prime,LPrime), call_to_success_fact(AbsInt,Sg,Hv,Head,K,Sv,Call,Proj,Prime,_Succ), ( current_pp_flag(fact_info,on) -> call_to_entry(AbsInt,Sv,Sg,Hv,Head,K,[],Prime,Exit,_), decide_memo(AbsInt,K,Id,no,Hv,[Exit]) |         |     |                              |        |     |
| 475 476 477 478 479 | Body = g(_,[],'$built'(_,true,_),'true/0',true), !,                                                                                                                                                                                                     |         |     |                              |        |     |
|                     | process_body(Body,K,AbsInt,Sg,Hv,Fv,_,Head,Sv,Call,Proj,LPrime,Id):-                                                                                                                                                                                    |         |     |                              |        |     |
| 480 481 482 483     | ;                                                                                                                                                                                                                                                       |         |     |                              |        |     |
| 484 485             |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
|                     | true                                                                                                                                                                                                                                                    |         |     |                              |        |     |
| 486                 | ).                                                                                                                                                                                                                                                      |         |     |                              |        |     |
| 487                 | process_body(Body,K,AbsInt,Sg,Hv,Fv,Vars_u,Head,Sv,_,Proj,Prime,Id):-                                                                                                                                                                                   |         |     |                              |        |     |
|                     | call_to_entry(AbsInt,Sv,Sg,Hv,Head,K,Fv,Proj,Entry,ExtraInfo), singleton(Entry,LEntry), entry_to_exit(Body,K,LEntry,Exit,[],_,Vars_u,AbsInt,Id),                                                                                                        |         |     |                              |        |     |
| 488 489 490 491     |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
|                     | each_exit_to_prime(Exit,AbsInt,Sg,Hv,Head,Sv,ExtraInfo,Prime).                                                                                                                                                                                          |         |     |                              |        |     |
|                     | Prime0,Prime1,Id,List),                                                                                                                                                                                                                                 |         |     |                              |        |     |
|                     | compute_clauses_lub(AbsInt,Proj,Prime1,Prime).                                                                                                                                                                                                          |         |     |                              |        |     |
|                     | TempPrime,Prime,Id,List) :-                                                                                                                                                                                                                             |         |     |                              |        |     |
|                     | TempPrime,Prime1,Id,[],NewList,Flag),                                                                                                                                                                                                                   |         |     |                              |        |     |
| 501 502 503         |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
|                     | fixpoint(NewList,Flag,Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,LEntryInf,                                                                                                                                                                                   |         |     |                              |        |     |
|                     | Prime1,Prime,Id,List), !.                                                                                                                                                                                                                               |         |     |                              |        |     |
|                     | Prime = Prime1, List = [].                                                                                                                                                                                                                              |         |     |                              |        |     |
| 508                 | var(Flag),!,                                                                                                                                                                                                                                            |         |     |                              |        |     |
| 509                 | Prime = Prime1,                                                                                                                                                                                                                                         |         |     |                              |        |     |
| 510                 |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
| 511                 | List = NewList.                                                                                                                                                                                                                                         |         |     |                              |        |     |
|                     | fixpoint(_,_,Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,LEntryInf,Prime1,Prime,Id,List):- fixpoint_compute_(Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,LEntryInf,                                                                                                   |         |     |                              |        |     |
| 512 513             |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
|                     | fixpoint_compute_(Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,LEntryInf, compute(Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,LEntryInf,                                                                                                                               |         |     |                              |        |     |
| 514                 |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
| 498 499 500         |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
| 492                 |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
| 493                 | fixpoint_compute(Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,LEntryInf,                                                                                                                                                                                        |         |     |                              |        |     |
|                     | Prime0,Prime,Id,List) :-                                                                                                                                                                                                                                |         |     |                              |        |     |
|                     | fixpoint_compute_(Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,LEntryInf,                                                                                                                                                                                       |         |     |                              |        |     |
| 494 495             |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
| 496                 |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
| 497                 |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
| 504 505 506         |                                                                                                                                                                                                                                                         |         |     |                              |        |     |
| 507                 | !,                                                                                                                                                                                                                                                      |         |     |                              |        |     |
|                     | fixpoint([],_,_,_,_,_,_,_,_,_,Prime1,Prime,_,List):-                                                                                                                                                                                                    |         |     |                              |        |     |
|                     | fixpoint(NewList,Flag,_,_,_,_,_,_,_,_,Prime1,Prime,_,List):-                                                                                                                                                                                            |         |     |                              |        |     |
|                     | Prime1,Prime,Id,List).                                                                                                                                                                                                                                  |         |     |                              |        |     |
|                     | widening:                                                                                                                                                                                                                                               |         |     |                              |        |     |
|                     |                                                                                                                                                                                                                                                         | 516 517 | 515 | normalization to perform the | % some |     |
|                     | need                                                                                                                                                                                                                                                    |         |     |                              |        |     |
|                     | domains                                                                                                                                                                                                                                                 |         |     |                              |        | 518 |

## Abstract Interpretation Fixpoint using TCLP

| 519                                                                     | current_pp_flag(widen,on), !, normalize_asub(AbsInt,Prime0,Prime).                                                                                                             | current_pp_flag(widen,on), !, normalize_asub(AbsInt,Prime0,Prime).                                                                                                             |
|-------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| 521                                                                     | normalize_asub0(_AbsInt,Prime,Prime).                                                                                                                                          | normalize_asub0(_AbsInt,Prime,Prime).                                                                                                                                          |
| 523 524                                                                 | compute([],_,_,_,_,_,_,[],Prime,Prime,_,List,List,_). compute([Clause|Rest],SgKey,Sg,Sv,Call,Proj,AbsInt,[EntryInf|LEntryInf],                                                 | compute([],_,_,_,_,_,_,[],Prime,Prime,_,List,List,_). compute([Clause|Rest],SgKey,Sg,Sv,Call,Proj,AbsInt,[EntryInf|LEntryInf],                                                 |
| 526 527 528                                                             | TempPrime,Prime,Id,List,NewList,Flag) :- TempPrime,NewPrime,Flag),                                                                                                             | TempPrime,Prime,Id,List,NewList,Flag) :- TempPrime,NewPrime,Flag),                                                                                                             |
|                                                                         | do_r_cl(Clause,SgKey,Sg,Sv,Proj,AbsInt,EntryInf,Id,List,IntList, compute(Rest,SgKey,Sg,Sv,Call,Proj,AbsInt,LEntryInf,NewPrime,Prime,                                           | do_r_cl(Clause,SgKey,Sg,Sv,Proj,AbsInt,EntryInf,Id,List,IntList, compute(Rest,SgKey,Sg,Sv,Call,Proj,AbsInt,LEntryInf,NewPrime,Prime,                                           |
| 529 530 531                                                             |                                                                                                                                                                                |                                                                                                                                                                                |
|                                                                         | Id,IntList,NewList,Flag).                                                                                                                                                      | Id,IntList,NewList,Flag).                                                                                                                                                      |
| 532                                                                     |                                                                                                                                                                                |                                                                                                                                                                                |
| do_r_cl(Clause,SgKey,Sg,Sv,Proj,AbsInt,EntryInf,Id,OldL,List,TempPrime, |                                                                                                                                                                                |                                                                                                                                                                                |
| 533 534                                                                 | NewPrime,Flag):- Clause=clause(Head,Vars_u,K,Body), clause_applies(Head,Sg), !,                                                                                                | NewPrime,Flag):- Clause=clause(Head,Vars_u,K,Body), clause_applies(Head,Sg), !,                                                                                                |
| 535 536 537 538                                                         | erase_previous_memo_tables_and_parents(Body,AbsInt,K,Id),                                                                                                                      | erase_previous_memo_tables_and_parents(Body,AbsInt,K,Id),                                                                                                                      |
|                                                                         | varset(Head,Hv), singleton(Entry,LEntry),                                                                                                                                      | varset(Head,Hv), singleton(Entry,LEntry),                                                                                                                                      |
|                                                                         | reuse_entry(EntryInf,Vars_u,AbsInt,Sv,Sg,Hv,Head,K,Proj,Entry,ExtraInfo), entry_to_exit(Body,K,LEntry,Exit,OldL,List,Vars_u,AbsInt,Id),                                        | reuse_entry(EntryInf,Vars_u,AbsInt,Sv,Sg,Hv,Head,K,Proj,Entry,ExtraInfo), entry_to_exit(Body,K,LEntry,Exit,OldL,List,Vars_u,AbsInt,Id),                                        |
| 539                                                                     |                                                                                                                                                                                |                                                                                                                                                                                |
| 540                                                                     |                                                                                                                                                                                |                                                                                                                                                                                |
|                                                                         | each_exit_to_prime(Exit,AbsInt,Sg,Hv,Head,Sv,ExtraInfo,Prime1),                                                                                                                | each_exit_to_prime(Exit,AbsInt,Sg,Hv,Head,Sv,ExtraInfo,Prime1),                                                                                                                |
| 541                                                                     |                                                                                                                                                                                |                                                                                                                                                                                |
|                                                                         | widen_succ(AbsInt,TempPrime,Prime1,NewPrime),                                                                                                                                  | widen_succ(AbsInt,TempPrime,Prime1,NewPrime),                                                                                                                                  |
| 542                                                                     |                                                                                                                                                                                |                                                                                                                                                                                |
| 543                                                                     | decide_flag(AbsInt,TempPrime,NewPrime,SgKey,Sg,Id,Proj,Flag).                                                                                                                  | decide_flag(AbsInt,TempPrime,NewPrime,SgKey,Sg,Id,Proj,Flag).                                                                                                                  |
| 544                                                                     | do_r_cl(_,_,_,_,_,_,_,_,List,List,Prime,Prime,_). widen_succ_off(AbsInt,Prime0,Prime1,LPrime):-                                                                                | do_r_cl(_,_,_,_,_,_,_,_,List,List,Prime,Prime,_). widen_succ_off(AbsInt,Prime0,Prime1,LPrime):-                                                                                |
| 545 546                                                                 | current_pp_flag(multi_success,on), !, reduce_equivalent([Prime0,Prime1],AbsInt,LPrime).                                                                                        | current_pp_flag(multi_success,on), !, reduce_equivalent([Prime0,Prime1],AbsInt,LPrime).                                                                                        |
| 547 548 549 550                                                         | widen_succ_off(AbsInt,Prime0,Prime1,Prime):- singleton(P0,Prime0),                                                                                                             | widen_succ_off(AbsInt,Prime0,Prime1,Prime):- singleton(P0,Prime0),                                                                                                             |
| 551                                                                     | singleton(P1,Prime1),                                                                                                                                                          | singleton(P1,Prime1),                                                                                                                                                          |
|                                                                         | singleton(P,Prime), compute_lub(AbsInt,[P0,P1],P).                                                                                                                             | singleton(P,Prime), compute_lub(AbsInt,[P0,P1],P).                                                                                                                             |
| 552 553 554                                                             |                                                                                                                                                                                |                                                                                                                                                                                |
| 555                                                                     | reuse_entry(EntryInf,Vars_u,AbsInt,Sv,Sg,Hv,Head,K,Proj,Entry,ExtraInfo):- var(EntryInf), !,                                                                                   | reuse_entry(EntryInf,Vars_u,AbsInt,Sv,Sg,Hv,Head,K,Proj,Entry,ExtraInfo):- var(EntryInf), !,                                                                                   |
| 556                                                                     | sort(Vars_u,Vars), ord_subtract(Vars,Hv,Fv),                                                                                                                                   | sort(Vars_u,Vars), ord_subtract(Vars,Hv,Fv),                                                                                                                                   |
| 557 558 559                                                             |                                                                                                                                                                                |                                                                                                                                                                                |
| 560                                                                     | call_to_entry(AbsInt,Sv,Sg,Hv,Head,K,Fv,Proj,Entry,ExtraInfo), EntryInf = (Entry,ExtraInfo).                                                                                   | call_to_entry(AbsInt,Sv,Sg,Hv,Head,K,Fv,Proj,Entry,ExtraInfo), EntryInf = (Entry,ExtraInfo).                                                                                   |
|                                                                         | reuse_entry(EntryInf,_Vars_u,_AbsInt,_Sv,_Sg,_Hv,_Head,_K,_Proj,Entry,ExtraInfo):- EntryInf = (Entry,ExtraInfo).                                                               | reuse_entry(EntryInf,_Vars_u,_AbsInt,_Sv,_Sg,_Hv,_Head,_K,_Proj,Entry,ExtraInfo):- EntryInf = (Entry,ExtraInfo).                                                               |
|                                                                         | decide_flag(AbsInt,TempPrime,NewPrime,_SgKey,_Sg,_Id,_Proj,_Flag):- abs_subset_(NewPrime,AbsInt,TempPrime), !. decide_flag(_AbsInt,TempPrime,NewPrime,SgKey,Sg,Id,Proj,Flag):- | decide_flag(AbsInt,TempPrime,NewPrime,_SgKey,_Sg,_Id,_Proj,_Flag):- abs_subset_(NewPrime,AbsInt,TempPrime), !. decide_flag(_AbsInt,TempPrime,NewPrime,SgKey,Sg,Id,Proj,Flag):- |
| 564 565                                                                 | Flag = notend, merge_(NewPrime,TempPrime,LPrime),                                                                                                                              | Flag = notend, merge_(NewPrime,TempPrime,LPrime),                                                                                                                              |
| 566 567 568                                                             | current_fact(fixpoint(SgKey,Sg,_,_,Id,Fs),Ref), erase(Ref),                                                                                                                    | current_fact(fixpoint(SgKey,Sg,_,_,Id,Fs),Ref), erase(Ref),                                                                                                                    |
|                                                                         | asserta_fact(fixpoint(SgKey,Sg,Proj,LPrime,Id,Fs)),                                                                                                                            | asserta_fact(fixpoint(SgKey,Sg,Proj,LPrime,Id,Fs)),                                                                                                                            |
| 569 570 571 572 573                                                     | current_fact(ch_id(Id,Num),Ref3),                                                                                                                                              | current_fact(ch_id(Id,Num),Ref3),                                                                                                                                              |
|                                                                         | erase(Ref3),                                                                                                                                                                   | erase(Ref3),                                                                                                                                                                   |
|                                                                         | Num1 is Num+1,                                                                                                                                                                 | Num1 is Num+1,                                                                                                                                                                 |
|                                                                         | asserta_fact(ch_id(Id,Num1)).                                                                                                                                                  | asserta_fact(ch_id(Id,Num1)).                                                                                                                                                  |
| 574                                                                     |                                                                                                                                                                                |                                                                                                                                                                                |
| 575                                                                     |                                                                                                                                                                                |                                                                                                                                                                                |
| 576                                                                     |                                                                                                                                                                                |                                                                                                                                                                                |
|                                                                         | !,                                                                                                                                                                             | !,                                                                                                                                                                             |
|                                                                         | merge_([NewPrime],_TempPrime,LPrime):- merge_(NewPrime,TempPrime,LPrime):-                                                                                                     | merge_([NewPrime],_TempPrime,LPrime):- merge_(NewPrime,TempPrime,LPrime):-                                                                                                     |
|                                                                         | LPrime=[NewPrime].                                                                                                                                                             | LPrime=[NewPrime].                                                                                                                                                             |
| 577                                                                     |                                                                                                                                                                                |                                                                                                                                                                                |
| 578 579                                                                 |                                                                                                                                                                                |                                                                                                                                                                                |
| 580                                                                     |                                                                                                                                                                                |                                                                                                                                                                                |
|                                                                         | merge(NewPrime,TempPrime,LPrime).                                                                                                                                              | merge(NewPrime,TempPrime,LPrime).                                                                                                                                              |
| 581                                                                     |                                                                                                                                                                                |                                                                                                                                                                                |
|                                                                         | %------------------------------------------------------------------------%                                                                                                     | %------------------------------------------------------------------------%                                                                                                     |
| 582 %                                                                   |                                                                                                                                                                                |                                                                                                                                                                                |
|                                                                         | entry_to_exit(+,+,+,-,+,-,+,+,+)                                                                                                                                               |                                                                                                                                                                                |
|                                                                         | %------------------------------------------------------------------------%                                                                                                     | %------------------------------------------------------------------------%                                                                                                     |

584

| 585 entry_to_exit((Sg,Rest),K,Call,Exit,OldList,NewList,Vars_u,AbsInt,NewN):- 586 body_succ(Call,Sg,Succ,OldList,IntList,Vars_u,AbsInt,K,NewN,_), 587 entry_to_exit(Rest,K,Succ,Exit,IntList,NewList,Vars_u,AbsInt,NewN).                           | 585 entry_to_exit((Sg,Rest),K,Call,Exit,OldList,NewList,Vars_u,AbsInt,NewN):- 586 body_succ(Call,Sg,Succ,OldList,IntList,Vars_u,AbsInt,K,NewN,_), 587 entry_to_exit(Rest,K,Succ,Exit,IntList,NewList,Vars_u,AbsInt,NewN).                           |
|-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| body_succ_(Info,SgKey,Sg,Sv,HFv,Call,Succ,L,NewL,AbsInt,ClId,Key,PId,Id):- Info = [_|_], !, split_combined_domain(AbsInt,Call,Calls,Domains), map_body_succ(Info,SgKey,Sg,Sv,HFv,Calls,Succs,L,NewL,Domains,                                        | body_succ_(Info,SgKey,Sg,Sv,HFv,Call,Succ,L,NewL,AbsInt,ClId,Key,PId,Id):- Info = [_|_], !, split_combined_domain(AbsInt,Call,Calls,Domains), map_body_succ(Info,SgKey,Sg,Sv,HFv,Calls,Succs,L,NewL,Domains,                                        |
| body_succ(Call,Sg,Exit,OldList,NewList,Vars_u,AbsInt,Key,NewN,_), decide_memo(AbsInt,Key,NewN,no,Vars_u,Exit),!. body_succ(Call,Atom,Succ,List,List,HvFv_u,AbsInt,_ClId,ParentId,no):- bottom(Call), !, Succ = Call, Atom=g(Key,_Av,_I,_SgKey,_Sg), | body_succ(Call,Sg,Exit,OldList,NewList,Vars_u,AbsInt,Key,NewN,_), decide_memo(AbsInt,Key,NewN,no,Vars_u,Exit),!. body_succ(Call,Atom,Succ,List,List,HvFv_u,AbsInt,_ClId,ParentId,no):- bottom(Call), !, Succ = Call, Atom=g(Key,_Av,_I,_SgKey,_Sg), |
| body_succ0('$var',SgKey,Sg,_Sv_u,HvFv_u,Calls,Succs,List0,List,AbsInt, ClId,F,_N,Id):- !, ( Calls=[Call],                                                                                                                                           | body_succ0('$var',SgKey,Sg,_Sv_u,HvFv_u,Calls,Succs,List0,List,AbsInt, ClId,F,_N,Id):- !, ( Calls=[Call],                                                                                                                                           |
| concrete(AbsInt,Sg,Call,Concretes), concretes_to_body(Concretes,SgKey,AbsInt,B)                                                                                                                                                                     | concrete(AbsInt,Sg,Call,Concretes), concretes_to_body(Concretes,SgKey,AbsInt,B)                                                                                                                                                                     |
| -> fixpoint_id(Id), meta_call(B,HvFv_u,Calls,[],Succs,List0,List,AbsInt,ClId,Id,Ids),                                                                                                                                                               | -> fixpoint_id(Id), meta_call(B,HvFv_u,Calls,[],Succs,List0,List,AbsInt,ClId,Id,Ids),                                                                                                                                                               |
| asserta_fact(memo_table(Key,AbsInt,ParentId,no,HvFv_u,Succ)).                                                                                                                                                                                       | asserta_fact(memo_table(Key,AbsInt,ParentId,no,HvFv_u,Succ)).                                                                                                                                                                                       |
| body_succ(Call,Atom,Succ,List,NewList,HvFv_u,AbsInt,ClId,ParentId,Id):- Atom=g(Key,Sv,Info,SgKey,Sg), body_succ_(Info,SgKey,Sg,Sv,HvFv_u,Call,Succ,List,NewList,AbsInt,                                                                             | body_succ(Call,Atom,Succ,List,NewList,HvFv_u,AbsInt,ClId,ParentId,Id):- Atom=g(Key,Sv,Info,SgKey,Sg), body_succ_(Info,SgKey,Sg,Sv,HvFv_u,Call,Succ,List,NewList,AbsInt,                                                                             |
| ClId,Key,ParentId,Id),                                                                                                                                                                                                                              | ClId,Key,ParentId,Id),                                                                                                                                                                                                                              |
| decide_memo(AbsInt,Key,ParentId,Id,HvFv_u,Call).                                                                                                                                                                                                    | decide_memo(AbsInt,Key,ParentId,Id,HvFv_u,Call).                                                                                                                                                                                                    |
| ClId,Key,PId,Id), split_combined_domain(AbsInt,Succ,Succs,Domains).                                                                                                                                                                                 | ClId,Key,PId,Id), split_combined_domain(AbsInt,Succ,Succs,Domains).                                                                                                                                                                                 |
| body_succ0(Info,SgKey,Sg,Sv,HFv,Call,Succ,L,NewL,AbsInt,                                                                                                                                                                                            | body_succ0(Info,SgKey,Sg,Sv,HFv,Call,Succ,L,NewL,AbsInt,                                                                                                                                                                                            |
| body_succ_(Info,SgKey,Sg,Sv,HFv,Call,Succ,L,NewL,AbsInt,ClId,Key,PId,Id):- ClId,Key,PId,Id).                                                                                                                                                        | body_succ_(Info,SgKey,Sg,Sv,HFv,Call,Succ,L,NewL,AbsInt,ClId,Key,PId,Id):- ClId,Key,PId,Id).                                                                                                                                                        |
| map_body_succ([],_SgKey,_Sg,_Sv,_HFv,[],[],L,L,[],_ClId,_Key,_PId,no). map_body_succ([I|Info],SgKey,Sg,Sv,HFv,[Call|Calls],[Succ|Succs],L,NewL,                                                                                                     | map_body_succ([],_SgKey,_Sg,_Sv,_HFv,[],[],L,L,[],_ClId,_Key,_PId,no). map_body_succ([I|Info],SgKey,Sg,Sv,HFv,[Call|Calls],[Succ|Succs],L,NewL,                                                                                                     |
| [AbsInt|Domains],ClId,Key,PId,Id):- body_succ0(I,SgKey,Sg,Sv,HFv,Call,Succ,L,_NewL,AbsInt, ClId,Key,PId,_Id), !,                                                                                                                                    | [AbsInt|Domains],ClId,Key,PId,Id):- body_succ0(I,SgKey,Sg,Sv,HFv,Call,Succ,L,_NewL,AbsInt, ClId,Key,PId,_Id), !,                                                                                                                                    |
| map_body_succ(Info,SgKey,Sg,Sv,HFv,Calls,Succs,L,NewL,Domains, ClId,Key,PId,Id).                                                                                                                                                                    | map_body_succ(Info,SgKey,Sg,Sv,HFv,Calls,Succs,L,NewL,Domains, ClId,Key,PId,Id).                                                                                                                                                                    |
| assertz_fact(memo_call(F,Id,AbsInt,Concretes,Ids))                                                                                                                                                                                                  | assertz_fact(memo_call(F,Id,AbsInt,Concretes,Ids))                                                                                                                                                                                                  |
| ; Id=no,                                                                                                                                                                                                                                            | ; Id=no,                                                                                                                                                                                                                                            |
| List=List0, variable                                                                                                                                                                                                                                | List=List0, variable                                                                                                                                                                                                                                |
| variable(F,ClId),                                                                                                                                                                                                                                   | variable(F,ClId),                                                                                                                                                                                                                                   |
| each_unknown_call(Calls,AbsInt,[Sg],Succs) % Sg is a                                                                                                                                                                                                | each_unknown_call(Calls,AbsInt,[Sg],Succs) % Sg is a                                                                                                                                                                                                |
| ).                                                                                                                                                                                                                                                  | ).                                                                                                                                                                                                                                                  |
| body_succ0('$meta'(T,B,_),SgKey,Sg,Sv_u,HvFv_u,Call,Succ,List0,List,AbsInt, ClId,F,N,Id):- !,                                                                                                                                                       | body_succ0('$meta'(T,B,_),SgKey,Sg,Sv_u,HvFv_u,Call,Succ,List0,List,AbsInt, ClId,F,N,Id):- !,                                                                                                                                                       |
| ( current_pp_flag(reuse_fixp_id,on) -> ( Call=[C] -> sort(Sv_u,Sv), project(AbsInt,Sg,Sv,HvFv_u,C,Proj),                                                                                                                                            | ( current_pp_flag(reuse_fixp_id,on) -> ( Call=[C] -> sort(Sv_u,Sv), project(AbsInt,Sg,Sv,HvFv_u,C,Proj),                                                                                                                                            |
| ; true                                                                                                                                                                                                                                              | ; true                                                                                                                                                                                                                                              |
| fixpoint_id_reuse_prev(SgKey,AbsInt,Sg,Proj,Id) )                                                                                                                                                                                                   | fixpoint_id_reuse_prev(SgKey,AbsInt,Sg,Proj,Id) )                                                                                                                                                                                                   |
| ;                                                                                                                                                                                                                                                   | ;                                                                                                                                                                                                                                                   |
| fixpoint_id(Id)                                                                                                                                                                                                                                     | fixpoint_id(Id)                                                                                                                                                                                                                                     |
| ),                                                                                                                                                                                                                                                  | ),                                                                                                                                                                                                                                                  |
| meta_call(B,HvFv_u,Call,[],Exits,List0,List,AbsInt,ClId,Id,_Ids),                                                                                                                                                                                   | meta_call(B,HvFv_u,Call,[],Exits,List0,List,AbsInt,ClId,Id,_Ids),                                                                                                                                                                                   |
| ( body_succ_meta(T,AbsInt,Sv_u,HvFv_u,Call,Exits,Succ) ->                                                                                                                                                                                           | ( body_succ_meta(T,AbsInt,Sv_u,HvFv_u,Call,Exits,Succ) ->                                                                                                                                                                                           |
| 646 647                                                                                                                                                                                                                                             | 646 647                                                                                                                                                                                                                                             |
| 648                                                                                                                                                                                                                                                 | 648                                                                                                                                                                                                                                                 |
| 645                                                                                                                                                                                                                                                 |                                                                                                                                                                                                                                                     |

| 651                                                                               |                                                                                                                                                                                                                        |                                                                    |                                                                              |
|-----------------------------------------------------------------------------------|------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------|------------------------------------------------------------------------------|
| 652                                                                               | sort(Sv_u,Sv),                                                                                                                                                                                                         |                                                                    |                                                                              |
| 653                                                                               | project(AbsInt,Sg,Sv,HvFv_u,C,Proj),                                                                                                                                                                                   |                                                                    |                                                                              |
| 654                                                                               | each_project(Exits,AbsInt,Sg,Sv,HvFv_u,Prime), asserta_fact(complete(SgKey,AbsInt,Sg,Proj,Prime,Id,[(F,N)]))                                                                                                           |                                                                    |                                                                              |
| 655                                                                               | ; true                                                                                                                                                                                                                 |                                                                    |                                                                              |
| 656 657                                                                           | )                                                                                                                                                                                                                      |                                                                    |                                                                              |
| 658                                                                               | ; % for the trusts, if any:                                                                                                                                                                                            |                                                                    |                                                                              |
| 659 660 661                                                                       | varset(Sg,Sv_r), % Sv_u contains extra vars (from meta-term) % which will confuse apply_trusted body_succ0(nr,SgKey,Sg,Sv_r,HvFv_u,Call,Succ,[],_List,AbsInt,                                                          |                                                                    |                                                                              |
| 662 663                                                                           | ClId,F,N,Id0), retract_fact(complete(SgKey,AbsInt,Sg,Proj,Prime,Id0,Ps)),                                                                                                                                              |                                                                    |                                                                              |
| 664                                                                               | asserta_fact(complete(SgKey,AbsInt,Sg,Proj,Prime,Id,Ps))                                                                                                                                                               |                                                                    |                                                                              |
| 665 666                                                                           |                                                                                                                                                                                                                        |                                                                    |                                                                              |
| ). body_succ0('$built'(T,Tg,Vs),SgKey,Sg,Sv_u,HvFv_u,Call,Succ,List0,List,AbsInt, |                                                                                                                                                                                                                        |                                                                    |                                                                              |
| 667 !,                                                                            | _ClId,F,N,Id):-                                                                                                                                                                                                        |                                                                    |                                                                              |
| 668 669                                                                           | Id=no,                                                                                                                                                                                                                 |                                                                    |                                                                              |
| 670                                                                               |                                                                                                                                                                                                                        |                                                                    |                                                                              |
|                                                                                   | List=List0,                                                                                                                                                                                                            |                                                                    |                                                                              |
| 671                                                                               | sort(Sv_u,Sv),                                                                                                                                                                                                         |                                                                    |                                                                              |
| 672                                                                               | each_body_succ_builtin(Call,AbsInt,T,Tg,Vs,SgKey,Sg,Sv,HvFv_u,F,N,Succ).                                                                                                                                               |                                                                    |                                                                              |
| 673                                                                               | body_succ0(RFlag,SgKey,Sg,Sv_u,HvFv_u,Call,Succ,List0,List,AbsInt,                                                                                                                                                     |                                                                    |                                                                              |
| 674                                                                               | ClId,F,N,Id):-                                                                                                                                                                                                         |                                                                    |                                                                              |
| 675                                                                               | sort(Sv_u,Sv),                                                                                                                                                                                                         |                                                                    |                                                                              |
| 676 677                                                                           | each_call_to_success(Call,RFlag,SgKey,Sg,Sv,HvFv_u,AbsInt,ClId, Succ,List0,List,F,N,Id).                                                                                                                               |                                                                    |                                                                              |
| 679                                                                               | each_call_to_success([Call],RFlag,SgKey,Sg,Sv,HvFv_u,AbsInt,ClId,Succ,L0,L, F,N,Id):-                                                                                                                                  |                                                                    |                                                                              |
| 680 681                                                                           |                                                                                                                                                                                                                        |                                                                    |                                                                              |
| 682 683 684                                                                       | !, project(AbsInt,Sg,Sv,HvFv_u,Call,Proj), call_to_success(RFlag,SgKey,Call,Proj,Sg,Sv,AbsInt,ClId,Succ,L1,F,N,Id),                                                                                                    |                                                                    |                                                                              |
| 685                                                                               | merge(L1,L0,L).                                                                                                                                                                                                        |                                                                    |                                                                              |
| 686                                                                               | each_call_to_success(LCall,RFlag,SgKey,Sg,Sv,HvFv_u,AbsInt,ClId,LSucc,L0,L, F,N,Id):-                                                                                                                                  |                                                                    |                                                                              |
| 687 688 689                                                                       | each_call_to_success0(LCall,RFlag,SgKey,Sg,Sv,HvFv_u,AbsInt,ClId, LSucc,L0,L,F,N,Id).                                                                                                                                  |                                                                    |                                                                              |
|                                                                                   | each_call_to_success0([],_Flag,_SgK,_Sg,_Sv,_HvFv,_AbsInt,_,[],L,L,_F,_N,_NN). each_call_to_success0([Call|LCall],RFlag,SgKey,Sg,Sv,HvFv_u,AbsInt,ClId, LSucc,L0,L,F,N,NewN):- project(AbsInt,Sg,Sv,HvFv_u,Call,Proj), |                                                                    |                                                                              |
| 693                                                                               |                                                                                                                                                                                                                        |                                                                    |                                                                              |
| 694 695 696                                                                       | call_to_success(RFlag,SgKey,Call,Proj,Sg,Sv,AbsInt,ClId,LSucc0,L1,F,N,_), merge(L0,L1,L2), append(LSucc0,LSucc1,LSucc),                                                                                                |                                                                    |                                                                              |
|                                                                                   | each_call_to_success0(LCall,RFlag,SgKey,Sg,Sv,HvFv_u,AbsInt,ClId,                                                                                                                                                      |                                                                    |                                                                              |
|                                                                                   | LSucc1,L2,L,F,N,NewN).                                                                                                                                                                                                 |                                                                    |                                                                              |
| 697 698 699                                                                       |                                                                                                                                                                                                                        |                                                                    |                                                                              |
| 700 701 702 703 704                                                               |                                                                                                                                                                                                                        |                                                                    |                                                                              |
|                                                                                   | meta_call_body(Body,ClId,Call,Succ1,L0,L1,HvFv_u,AbsInt,Id,Ids0), widen_succ(AbsInt,Succ0,Succ1,Succ2), append(Succ0,Succ1,Succ2),                                                                                     |                                                                    |                                                                              |
|                                                                                   | append(Ids0,Ids1,Ids),                                                                                                                                                                                                 |                                                                    |                                                                              |
| 709 710                                                                           |                                                                                                                                                                                                                        |                                                                    |                                                                              |
|                                                                                   | meta_call_(Bodies,HvFv_u,Call,Succ2,Succ,L1,List,AbsInt,ClId,Id,Ids1).                                                                                                                                                 |                                                                    |                                                                              |
|                                                                                   | meta_call_([],_HvFv_u,_Call,Succ,Succ,List,List,_AbsInt,_ClId,_Id,[]).                                                                                                                                                 |                                                                    |                                                                              |
| 711 712                                                                           | meta_call_body((Sg,Rest),K,Call,Exit,OldList,NewList,Vars_u,AbsInt,PId,CIds):-                                                                                                                                         |                                                                    |                                                                              |
|                                                                                   | !,                                                                                                                                                                                                                     |                                                                    |                                                                              |
| 713                                                                               | CIds=[Id|Ids],                                                                                                                                                                                                         |                                                                    |                                                                              |
| 714 715 716                                                                       | body_succ(Call,Sg,Succ,OldList,IntList,Vars_u,AbsInt,K,PId,Id),                                                                                                                                                        |                                                                    |                                                                              |
|                                                                                   | meta_call_([Body|Bodies],HvFv_u,Call,Succ0,Succ,L0,List,AbsInt,ClId,Id,Ids). meta_call_([Body|Bodies],HvFv_u,Call,Succ0,Succ,L0,List,AbsInt,ClId,Id,Ids):-                                                             |                                                                    |                                                                              |
| 705 706 707 708                                                                   |                                                                                                                                                                                                                        |                                                                    |                                                                              |
| 690 691 692                                                                       |                                                                                                                                                                                                                        |                                                                    |                                                                              |
|                                                                                   |                                                                                                                                                                                                                        | meta_call([],_HvFv_u,Call,[],Call,List,List,_AbsInt,_ClId,_Id,[]). | meta_call([Body|Bodies],HvFv_u,Call,Succ0,Succ,L0,List,AbsInt,ClId,Id,Ids):- |

## 32 J. Arias and M. Carro

| 717         | meta_call_body(Rest,K,Succ,Exit,IntList,NewList,Vars_u,AbsInt,PId,Ids).                 |
|-------------|-----------------------------------------------------------------------------------------|
| 718         | meta_call_body(true,_,Call,Call,List,List,_,_,_,[no]):- !.                              |
| 719         | meta_call_body(Sg,Key,Call,Exit,OldList,NewList,Vars_u,AbsInt,PId,[Id]):-               |
| 720         | body_succ(Call,Sg,Exit,OldList,NewList,Vars_u,AbsInt,Key,PId,Id).                       |
| 721 722     | concretes_to_body([],_SgKey,_AbsInt,[]).                                                |
| 723         | concretes_to_body([Sg|Sgs],SgKey,AbsInt,[B|Bs]):-                                       |
| 724         | body_info0(Sg:SgKey,[],AbsInt,B),                                                       |
| 725         | concretes_to_body(Sgs,SgKey,AbsInt,Bs).                                                 |
| 726         |                                                                                         |
| 727         | %------------------------------------------------------------------------% %            |
| 728         | query(+,+,+,+,+,+,+,-) %                                                                |
| 729         | %------------------------------------------------------------------------%              |
| 730 731     | :- doc(query(AbsInt,QKey,Query,Qv,RFlag,N,Call,Succ),                                   |
| 732         | "The success pattern of @var{Query} with @var{Call} is                                  |
| 733         | @var{Succ} in the analysis domain @var{AbsInt}. The predicate                           |
| 734         | called is identified by @var{QKey}, and @var{RFlag} says if it                          |
| 735         | is recursive or not. The goal @var{Query} has variables @var{Qv},                       |
| 736         | and the call pattern is uniquely identified by @var{N}.").                              |
| 738         | query(AbsInt,QKey,Query,Qv,RFlag,N,Call,Succ) :- project(AbsInt,Query,Qv,Qv,Call,Proj), |
| 737 739 740 | call_to_success(RFlag,QKey,Call,Proj,Query,Qv,AbsInt,0,Succ,_,N,0,Id),                  |
| 742         |                                                                                         |
| 741         |                                                                                         |
|             | approx_to_completes(AbsInt).                                                            |
|             | query(_AbsInt,_QKey,_Query,_Qv,_RFlag,_N,_Call,_Succ):-                                 |
| 743         |                                                                                         |
| 744         | % should never happen, but...                                                           |
| 745         | error_message("SOMETHING HAS FAILED!").                                                 |
Joaquin Arias Manuel Carro
Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP
CiaoPP is an analyzer and optimizer for logic programs, part of the Ciao
Prolog system. It includes PLAI, a fixpoint algorithm for the abstract
interpretation of logic programs which we adapt to use tabled constraint logic
programming. In this adaptation, the tabling engine drives the fixpoint
computation, while the constraint solver handles the LUB of the abstract
substitutions of different clauses. That simplifies the code and improves
performance, since termination, dependencies, and some crucial operations
(e.g., branch switching and resumption) are directly handled by the tabling
engine. Determining whether the fixpoint has been reached uses semantic
equivalence, which can decide that two syntactically different abstract
substitutions represent the same element in the abstract domain. Therefore, the
tabling analyzer can reuse answers in more cases than an analyzer using
syntactical equality. This helps achieve better performance, even taking into
account the additional cost associated to these checks. Our implementation is
based on the TCLP framework available in Ciao Prolog and is one-third the size
of the initial fixpoint implementation in CiaoPP. Its performance has been
evaluated by analyzing several programs using different abstract domains. This
paper is under consideration for publication in Theory and Practice of Logic
Programming (TPLP).