Project

Profile

Help

HostedRedmine.com has moved to the Planio platform. All logins and passwords remained the same. All users will be able to login and use Redmine just as before. *Read more...*

Feature #154542

open

define and add new theory of constructible arrays

Added by Cesare Tinelli almost 10 years ago. Updated almost 10 years ago.

Status:
New
Priority:
Low
Start date:
2013-03-01
Due date:
% Done:

0%

Estimated time:

Description

This theory adds to store and select a constructor

const: B -> (Array A B)

where const(v) is an array with constant value v.

The theory's model are limited to those where each array is either constant or the result of finitely many applications of store to a constant array.

Need to find references showing that it universal fragment is decidable.

Actions #1

Updated by Cesare Tinelli almost 10 years ago

A similar theory and its decision procedure are described in the paper below. But it is restricted to arrays with integer index.

Stephan Falke, Carsten Sinz, and Florian Merz:
A Theory of Arrays with Set and Copy Operations (Extended Abstract)
In Proceedings of the 10th International Workshop on Satisfiability Modulo Theories (SMT '12), Manchester, UK.

Also available in: Atom PDF