pith. sign in

arxiv: 2508.11447 · v2 · submitted 2025-08-15 · 💻 cs.LO

Encoding and Reasoning about Arrays in Constraint Logic Programming with Sets

Maximiliano Cristi\'a , Gianfranco Rossi This is my paper

Pith reviewed 2026-05-18 23:25 UTC · model grok-4.3

classification 💻 cs.LO
keywords arrayssetsfunctionsconstraint logic programmingdecision proceduressatisfiabilityset theoryarray programs
0
0 comments X

The pith

Arrays encoded as sets of ordered pairs reduce array reasoning to set reasoning via a new decision procedure.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper encodes arrays as functions, themselves represented as sets of ordered pairs, such that the cardinality of each set equals the length of the corresponding array. Specifications for a non-trivial class of array programs are then written in a defined fragment of set theory, converting array problems into set problems. A decision procedure for satisfiability in this fragment is developed and implemented inside the {log} constraint logic programming tool. This allows users to handle sets, functions, and arrays together in one language and solver, extending earlier decision procedures that lacked array support.

Core claim

Arrays are represented as functions encoded as sets of ordered pairs where the cardinality of the set equals the length of the array. A fragment of set theory is defined to capture specifications of a non-trivial class of array programs, turning array reasoning into set reasoning. A decision procedure for this fragment is provided and implemented in the {log} constraint logic programming language and satisfiability solver, extending prior procedures for set theory fragments.

What carries the argument

Encoding arrays as sets of ordered pairs whose cardinality equals array length, allowing reduction to a decidable fragment of set theory.

If this is right

  • Programs mixing arrays with sets and functions can be specified and solved for satisfiability in a single tool without separate encodings.
  • The decision procedure extends earlier set-theory procedures to cover array operations directly.
  • Constraint logic programming gains native support for array data structures through the existing set and relation solver.
  • Users can reason about array-manipulating code by writing constraints in the set fragment and invoking the built-in solver.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar cardinality-based encodings could be tested on other indexed structures such as matrices or hash tables.
  • The approach opens a route to verify array algorithms by reducing them to existing set-solver calls rather than building new array-specific engines.
  • If the fragment proves too restrictive in practice, targeted extensions to the decision procedure could be checked for decidability.

Load-bearing premise

The chosen fragment of set theory is expressive enough to capture a non-trivial class of array programs and the decision procedure correctly decides satisfiability for all formulas in that fragment.

What would settle it

An array program specification expressible in the fragment for which the implemented solver returns the wrong satisfiability answer, such as a satisfiable formula declared unsatisfiable.

Figures

Figures reproduced from arXiv: 2508.11447 by Gianfranco Rossi, Maximiliano Cristi\'a.

Figure 1
Figure 1. Figure 1: Some key rewrite rules inherited from SAT[ ]. 𝑁 , 𝑁𝑖 , 𝑛 are fresh variables [PITH_FULL_IMAGE:figures/full_fig_p013_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Rewrite rules for RUQ. 𝑁 is a fresh variable. Hence, the rule decides the satisfiability of [𝑘,𝑚] = {𝑦 ⊔ 𝐵} by deciding the satisfiability of {𝑦 ⊔ 𝐵} ⊆ [𝑘,𝑚] ∧𝑠𝑖𝑧𝑒 ({𝑦 ⊔ 𝐵},𝑚 − 𝑘 + 1). Observe that (18) is correctly applied as 𝑘 ≤ 𝑚 is implicit because {𝑦 ⊔ 𝐵} is a non-empty set. Finally, rule (17), based again on (18), is crucial as it permits to reconstruct an integer interval from the union of two sets.… view at source ↗
Figure 3
Figure 3. Figure 3: An implementation of binary search. Gray boxes are program annotations. [PITH_FULL_IMAGE:figures/full_fig_p022_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Verification conditions for the program of Figure [PITH_FULL_IMAGE:figures/full_fig_p023_4.png] view at source ↗
read the original abstract

We encode arrays as functions which, in turn, are encoded as sets of ordered pairs. The set cardinality of each of these functions coincides with the length of the array it is representing. Then we define a fragment of set theory that is used to give the specifications of a non-trivial class of programs with arrays. In this way, array reasoning becomes set reasoning. Furthermore, a decision procedure for this fragment is also provided and implemented as part of the {log} (read 'setlog') tool. {log} is a constraint logic programming language and satisfiability solver where sets and binary relations are first-class citizens. The tool already implements a few decision procedures for different fragments of set theory. In this way, arrays are seamlessly integrated into {log} thus allowing users to reason about sets, functions and arrays all in the same language and with the same solver. The decision procedure presented in this paper is an extension of decision procedures defined in earlier works not supporting arrays.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper encodes arrays as finite functions represented by sets of ordered pairs whose cardinality equals the array length. It defines a fragment of set theory sufficient to specify a non-trivial class of array programs, reduces array access and update operations to set constraints, and supplies a decision procedure for the resulting fragment that is implemented as an extension of existing procedures inside the {log} constraint logic programming solver.

Significance. If the reduction and decision procedure are correct for the stated fragment, the work provides a uniform way to reason about sets, functions and arrays inside a single CLP language and solver. This integration is practically useful for constraint-based program analysis and verification tasks that mix array and set data structures. The explicit implementation in an existing tool and the conservative extension of prior decision procedures are concrete strengths.

minor comments (2)
  1. [Abstract] Abstract, paragraph 3: the phrase 'a non-trivial class of programs with arrays' is used without a brief characterization of the class (e.g., bounded-length arrays with index expressions drawn from a fixed set of operations). Adding one sentence would clarify the scope of the claimed decision procedure.
  2. [Introduction] The manuscript states that the decision procedure is an extension of earlier works; the introduction should list the specific prior papers (with section references) that supply the base rewrite rules so readers can trace the conservative addition of array rules.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our work on encoding arrays as sets of ordered pairs within the {log} solver and for recommending minor revision. The recognition that this provides a uniform approach to reasoning about sets, functions, and arrays is appreciated.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper explicitly defines the encoding of arrays as functions (sets of ordered pairs whose cardinality equals array length) and reduces array constraints to set constraints within a newly specified fragment of set theory. This mapping and the associated rewrite rules for access, update, and cardinality are presented directly as the core contribution. The decision procedure is described as an extension of earlier procedures, but the paper states that it provides and implements the extension for the array fragment inside {log}, with the fragment restricted to finite sets with explicit cardinality and functional constraints. No equation or claim in the abstract reduces the new array encoding or the satisfiability result to a prior self-citation by construction; the extension is characterized as a conservative addition of array-specific rules. The overall derivation therefore remains self-contained and independently verifiable through the stated fragment definition and implementation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on one domain assumption (the encoding) and the claim that the new fragment is decidable; no free parameters or invented entities are introduced.

axioms (1)
  • domain assumption Arrays can be faithfully represented as functions encoded as sets of ordered pairs whose cardinality equals the array length.
    This encoding is invoked to reduce array reasoning to set reasoning (abstract, sentence 2).

pith-pipeline@v0.9.0 · 5696 in / 1216 out tokens · 36369 ms · 2026-05-18T23:25:19.799701+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [1]

    Jean-Raymond Abrial. 1996. The B-book: Assigning Programs to Meanings . Cambridge University Press, New York, NY, USA

    work page 1996

  2. [2]

    Jean-Raymond Abrial. 2010. Modeling in Event-B: System and Software Engineering (1st ed.). Cambridge University Press, New York, NY, USA

    work page 2010

  3. [3]

    Francesco Alberti, Silvio Ghilardi, and Elena Pagani. 2017. Cardinality constraints for arrays (decidability results and applications). Formal Methods Syst. Des. 51, 3 (2017), 545–574. https://doi.org/10.1007/S10703-017-0279-6

    work page doi:10.1007/s10703-017-0279-6 2017

  4. [4]

    Francesco Alberti, Silvio Ghilardi, and Natasha Sharygina. 2015. Decision Procedures for Flat Array Properties. J. Autom. Reason. 54, 4 (2015), 327–352. https://doi.org/10.1007/S10817-015-9323-7

    work page doi:10.1007/s10817-015-9323-7 2015

  5. [5]

    Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konecný, and Tomás Vojnar. [n. d.]. Automatic Verification of Integer Array Programs. InComputer Aided Verification, 21st International Conference, CA V 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings (2009) (Lecture Notes in Computer Science, Vol. 5643), Ahmed Bouajjani and Oded Maler (Eds.). S...

    work page doi:10.1007/978-3-642-02658-4_15 2009

  6. [6]

    Bradley, Zohar Manna, and Henny B

    Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What’s Decidable About Arrays?. In Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 3855), E. Allen Emerson and Kedar S. Namjoshi (Eds.). Springer, 427–44...

    work page doi:10.1007/11609773_28 2006

  7. [7]

    Domenico Cantone and Cristiano Longo. 2014. A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions. Theor. Comput. Sci. 560 (2014), 307–325. https://doi.org/10.1016/j.tcs.2014.03.021

    work page doi:10.1016/j.tcs.2014.03.021 2014

  8. [8]

    Omodeo, and Alberto Policriti

    Domenico Cantone, Eugenio G. Omodeo, and Alberto Policriti. 2001. Set Theory for Computing - From Decision Procedures to Declarative Programming with Sets. Springer. https://doi.org/10.1007/978-1-4757-3452-2

    work page doi:10.1007/978-1-4757-3452-2 2001

  9. [9]

    Alfredo Capozucca, Maximiliano Cristiá, Ross Horne, and Ricardo Katz. 2024. Brewer-Nash Scrutinised: Mechanised Checking of Policies Featuring Write Revocation. In 37th IEEE Computer Security Foundations Symposium, CSF 2024, Enschede, Netherlands, July 8-12, 2024 . IEEE, 112–126. https://doi.org/10.1109/CSF61375.2024.00042

    work page doi:10.1109/csf61375.2024.00042 2024

  10. [10]

    Maximiliano Cristiá, Alfredo Capozucca, and Gianfranco Rossi. 2025. From a Constraint Logic Programming Language to a Formal Verification Tool. CoRR abs/2505.17350 (2025). https://doi.org/10.48550/ARXIV.2505.17350 arXiv:2505.17350

    work page doi:10.48550/arxiv.2505.17350 2025

  11. [11]

    Maximiliano Cristiá, Guido De Luca, and Carlos Luna. 2023. An Automatically Verified Prototype of the Android Permissions System. J. Autom. Reason. 67, 2 (2023), 17. https://doi.org/10.1007/s10817-023-09666-2

    work page doi:10.1007/s10817-023-09666-2 2023

  12. [12]

    Maximiliano Cristiá and Gianfranco Rossi. 2018. A Set Solver for Finite Set Relation Algebra. InRelational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 - November 1, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 11194), Jules Desharnais, Walter Guttmann, and Ste...

    work page doi:10.1007/978-3-030-02149-8_20 2018

  13. [13]

    Maximiliano Cristiá and Gianfranco Rossi. 2019. Rewrite Rules for a Solver for Sets, Binary Relations and Partial Functions . Technical Report. https://www.clpset.unipr.it/SETLOG/calculus.pdf

    work page 2019

  14. [14]

    Maximiliano Cristiá and Gianfranco Rossi. 2020. Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations. J. Autom. Reason. 64, 2 (2020), 295–330. https://doi.org/10.1007/s10817-019-09520-4

    work page doi:10.1007/s10817-019-09520-4 2020

  15. [15]

    Maximiliano Cristiá and Gianfranco Rossi. 2021. Automated Proof of Bell-LaPadula Security Properties. J. Autom. Reason. 65, 4 (2021), 463–478. https://doi.org/10.1007/s10817-020-09577-6

    work page doi:10.1007/s10817-020-09577-6 2021

  16. [16]

    Maximiliano Cristiá and Gianfranco Rossi. 2021. Automated Reasoning with Restricted Intensional Sets. J. Autom. Reason. 65, 6 (2021), 809–890. https://doi.org/10.1007/s10817-021-09589-w

    work page doi:10.1007/s10817-021-09589-w 2021

  17. [17]

    Maximiliano Cristiá and Gianfranco Rossi. 2021. An Automatically Verified Prototype of the Tokeneer ID Station Specification. J. Autom. Reason. 65, 8 (2021), 1125–1151. https://doi.org/10.1007/s10817-021-09602-2

    work page doi:10.1007/s10817-021-09602-2 2021

  18. [18]

    Maximiliano Cristiá and Gianfranco Rossi. 2023. Integrating Cardinality Constraints into Constraint Logic Programming with Sets. Theory Pract. Log. Program. 23, 2 (2023), 468–502. https://doi.org/10.1017/S1471068421000521

    work page doi:10.1017/s1471068421000521 2023

  19. [19]

    Maximiliano Cristiá and Gianfranco Rossi. 2024. A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals. ACM Trans. Comput. Log. 25, 1 (2024), 3:1–3:34. https://doi.org/10.1145/3625230

    work page doi:10.1145/3625230 2024

  20. [20]

    Maximiliano Cristiá and Gianfranco Rossi. 2024. A Practical Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted Quantifiers. J. Autom. Reason. 68, 4 (2024), 23. https://doi.org/10.1007/S10817-024-09713-6

    work page doi:10.1007/s10817-024-09713-6 2024

  21. [21]

    Maximiliano Cristiá, Gianfranco Rossi, and Claudia S. Frydman. 2013. {𝑙𝑜𝑔 } as a Test Case Generator for the Test Template Framework. In SEFM (Lecture Notes in Computer Science, Vol. 8137) , Robert M. Hierons, Mercedes G. Merayo, and Mario Bravetti (Eds.). Springer, 229–243. Manuscript submitted to ACM Encoding and Reasoning About Arrays in Set Theory 27

    work page 2013

  22. [22]

    Henzinger, and Andrey Kupriyanov

    Przemyslaw Daca, Thomas A. Henzinger, and Andrey Kupriyanov. [n. d.]. Array Folds Logic. InComputer Aided Verification - 28th International Conference, CA V 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II (2016) (Lecture Notes in Computer Science, Vol. 9780) , Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer, 230–248. https://doi.org/...

    work page doi:10.1007/978-3-319-41540-6_13 2016

  23. [23]

    Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, and Maurizio Proietti. 2017. Program Verification using Constraint Handling Rules and Array Constraint Generalizations. Fundam. Inform. 150, 1 (2017), 73–117. https://doi.org/10.3233/FI-2017-1461

    work page doi:10.3233/fi-2017-1461 2017

  24. [24]

    Leonardo Mendonça de Moura and Nikolaj Bjørner. 2009. Generalized, efficient array decision procedures. In Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA . IEEE, 45–52. https://doi.org/10. 1109/FMCAD.2009.5351142

    work page arXiv 2009

  25. [25]

    Omodeo, Enrico Pontelli, and Gianfranco Rossi

    Agostino Dovier, Eugenio G. Omodeo, Enrico Pontelli, and Gianfranco Rossi. 1996. A Language for Programming in Logic with Finite Sets. J. Log. Program. 28, 1 (1996), 1–44. https://doi.org/10.1016/0743-1066(95)00147-6

    work page doi:10.1016/0743-1066(95)00147-6 1996

  26. [26]

    Agostino Dovier, Carla Piazza, Enrico Pontelli, and Gianfranco Rossi. 2000. Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22, 5 (2000), 861–931

    work page 2000

  27. [27]

    Agostino Dovier, Enrico Pontelli, and Gianfranco Rossi. 2006. Set unification. Theory Pract. Log. Program. 6, 6 (2006), 645–701. https://doi.org/10. 1017/S1471068406002730

    work page 2006

  28. [28]

    Stephan Falke, Florian Merz, and Carsten Sinz. [n. d.]. Extending the Theory of Arrays: memset, memcpy, and Beyond. In Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Menlo Park, CA, USA, May 17-19, 2013, Revised Selected Papers (2013) (Lecture Notes in Computer Science, Vol. 8164), Ernie Cohen and Andrey Rybalc...

    work page doi:10.1007/978-3-642-54108-7_6 2013

  29. [29]

    Peter Habermehl, Radu Iosif, and Tomás Vojnar. 2008. What Else Is Decidable about Integer Arrays?. In Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedi...

    work page doi:10.1007/978-3-540-78499-9_33 2008

  30. [30]

    Christian Holzbaur. 1995. OFAI CLP(Q,R) manual. Technical Report. edition 1.3.3. Technical Report TR-95-09, Austrian Research Institute for Artificial Intelligence. http://www.ofai.at/cgi-bin/tr-online?number+95-09

    work page 1995

  31. [31]

    Quentin Plazar, Mathieu Acher, Sébastien Bardin, and Arnaud Gotlieb. [n. d.]. Efficient and Complete FD-solving for extended array constraints. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017 (2017), Carles Sierra (Ed.). ijcai.org, 1231–1238. https://doi.org...

    work page doi:10.24963/ijcai.2017/171 2017

  32. [32]

    Rodrigo Raya and Viktor Kuncak. 2024. On algebraic array theories. J. Log. Algebraic Methods Program. 136 (2024), 100906. https://doi.org/10.1016/J. JLAMP.2023.100906

    work page doi:10.1016/j 2024

  33. [33]

    Gianfranco Rossi and Maximiliano Cristiá. 2000. {𝑙𝑜𝑔 } home page. http://www.clpset.unipr.it/setlog.Home.html Last access 2025

    work page 2000

  34. [34]

    Gianfranco Rossi and Maximiliano Cristiá. 2025. {𝑙𝑜𝑔 } User’s Manual. Technical Report. Dipartimento di Matematica, Universitá di Parma. https://www.clpset.unipr.it/SETLOG/setlog-man.pdf

    work page 2025

  35. [35]

    Schwartz, Robert B

    Jacob T. Schwartz, Robert B. K. Dewar, Ed Dubinsky, and Edith Schonberg. 1986. Programming with Sets - An Introduction to SETL . Springer. https://doi.org/10.1007/978-1-4613-9575-1

    work page doi:10.1007/978-1-4613-9575-1 1986

  36. [36]

    J. M. Spivey. 1992. The Z notation: a reference manual . Prentice Hall International (UK) Ltd., Hertfordshire, UK, UK

    work page 1992

  37. [37]

    Stocks and D

    P. Stocks and D. Carrington. 1996. A Framework for Specification-Based Testing. IEEE Transactions on Software Engineering 22, 11 (Nov. 1996), 777–793

    work page 1996

  38. [38]

    Qinshi Wang and Andrew W. Appel. 2023. A Solver for Arrays with Concatenation. J. Autom. Reason. 67, 1 (2023), 4. https://doi.org/10.1007/S10817- 022-09654-Y Received 20 February 2007; revised 12 March 2009; accepted 5 June 2009 Manuscript submitted to ACM

    work page doi:10.1007/s10817- 2023