Succinct ordering and aggregation constraints in algebraic array theories

被引:0
作者
Raya, Rodrigo [1 ]
Kuncak, Viktor [1 ]
机构
[1] Ecole Polytech Fed Lausanne EPFL, Sch Comp & Commun Sci, Lausanne, Switzerland
关键词
Decision procedures; Satisfiability modulo theories; Arrays; Feferman-Vaught; Composition theorems; BOOLEAN-ALGEBRA; COMPLEXITY;
D O I
10.1016/j.jlamp.2024.100978
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We discuss two extensions to a recently introduced theory of arrays, which are based on considerations coming from the model theory of power structures. First, we discuss how the ordering relation on the index set can be expressed succinctly by referring to arbitrary Venn regions. Second, we show how to add general aggregators to the calculus. The result is a logic that subsumes four previous fragments discussed in the literature and is distinct from array fold logic, in that it can express summations, while its satisfiability problem remains in non -deterministic polynomial time.
引用
收藏
页数:22
相关论文
共 75 条
[1]   GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts [J].
Albert, Elvira ;
Correas, Jesus ;
Gordillo, Pablo ;
Roman-Diez, Guillermo ;
Rubio, Albert .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2020, 2020, 12079 :118-125
[2]   Cardinality constraints for arrays (decidability results and applications) [J].
Alberti, F. ;
Ghilardi, S. ;
Pagani, E. .
FORMAL METHODS IN SYSTEM DESIGN, 2017, 51 (03) :545-574
[3]   SolCMC: Solidity Compiler's Model Checker [J].
Alt, Leonardo ;
Blicha, Martin ;
Hyvarinen, Antti E. J. ;
Sharygina, Natasha .
COMPUTER AIDED VERIFICATION (CAV 2022), PT I, 2022, 13371 :325-338
[4]  
[Anonymous], 1979, The Computational Complexity of Logical Theories
[5]  
[Anonymous], 2012, Cengage Learning
[6]  
Arora S, 2009, COMPUTATIONAL COMPLEXITY: A MODERN APPROACH, P1, DOI 10.1017/CBO9780511804090
[7]   A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT [J].
Bansal, Kshitij ;
Reynolds, Andrew ;
Barrett, Clark ;
Tinelli, Cesare .
AUTOMATED REASONING (IJCAR 2016), 2016, 9706 :82-98
[8]   cvc5: A Versatile and Industrial-Strength SMT Solver [J].
Barbosa, Haniel ;
Barrett, Clark ;
Brain, Martin ;
Kremer, Gereon ;
Lachnitt, Hanna ;
Mann, Makai ;
Mohamed, Abdalrhman ;
Mohamed, Mudathir ;
Niemetz, Aina ;
Notzli, Andres ;
Ozdemir, Alex ;
Preiner, Mathias ;
Reynolds, Andrew ;
Sheng, Ying ;
Tinelli, Cesare ;
Zohar, Yoni .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT I, 2022, 13243 :415-442
[9]  
Bradley Aaron, 2007, Calculus of computation: decision procedures with applications to verification
[10]  
Bradley AR, 2006, LECT NOTES COMPUT SC, V3855, P427