Request for feedback on SMT-LIB 2.7 draft

[Tinelli, Cesare]

Dear all,

In the process of moving to SMT-LIB 3, we received suggestions to create a bridge version, Version 2.7, capturing the features of Version 3 that would be relevant to users and solver developers (as opposed to theory specifiers) but could be accommodated in Version 2 already.

The features in question are:

1. User-level prenex polymorphism, in particular with assertions containing terms with polymorphic sort.
2. A theory of higher-order maps as a stand-in for higher-order functions.
3. Stronger requirements for the result of the get-model command.

A draft of Version 2.7 is available at here. The relevant text is written in red. 

We believe this version is fully in the spirit of the suggestions we received. However, we would appreciate the feedback of the SMT community on the new features. If you have any, please share them as a reply to this message by December 15, 2024. 

For your convenience, a brief description of the new features and the rationale behind the choices we made in designing them are included below. However, please check the draft for more details before providing your feedback.

Best,


Cesare, Clark and Pascal
SMT-LIB Coordinators


========================================

Feature 1: User-level prenex polymorphism

We have added a new command, declare-sort-parameter, to globally declare sort parameters. These are symbols ranging over sorts and can be used to assert formulas with terms of polymorphic sort in SMT-LIB scripts. Semantically, the sort parameters are treated as implicitly universally quantified sort variables in each asserted formula (global declarations but local quantification). 

This has the effect of allowing prenex, or rank-1, polymorphism (but not more general forms of polymorphism) in assertions, with no changes to previous commands and only minor changes to the syntax of terms.

--------------------------------
 Example
--------------------------------

(declare-sort-parameter E)

; definition of polymorphic function parametrized by E
(define-fun-rec occurs ((a (Array Int E)) (e E) (n Int)) Bool
 (and (>= n 0) 
   (or (= e (select a n)) (occurs a e (- n 1)))))

; declaration of polymorphic function parametrized by E
(declare-fun find ((Array Int E) E Int) Int)

; polymorphic assertion parametrized by E
(assert 
 (forall ((a (Array Int E)) (e E) (n Int))
   (= (find a e n) 
  (ite (= n 0) (- 1) 
   (ite (= e (select a n)) n (find a e (- n 1))))))

(declare-sort S 0)

; negation of polymorphic consequence of previous assertions
; using uninterpreted sort S as a Skolem constant for parameter E
(assert (not 
  (forall ((a (Array Int S)) (e S) (i Int))
   (occurs (store a i e) e i))))

It should be noted that in the logical semantics of SMT-LIB 2.7, sort parameters actually range over sort terms, and not over sets of individuals, as in more powerful logics. This restriction leads to a weaker notion of satisfiability (more formulas are satisfiable, see the draft for more details) but is usually not a problem, since sort parameters are always universally quantified -- allowing one to consider only models where every possible sort domain is denoted by a ground sort term.

This is one of the motivations of the restriction to prenex polymorphism, a good compromise between expressiveness and complexity of the language.

We have also considered a binder like par, already used in theory definitions, to allow the introduction of sort parameters locally, as in, for instance,

(declare-fun find (par (E) ((Array Int E) E Int) Int))

and

(assert (par (E) 
  (forall ((a (Array Int E)) (e E) (n Int))
   (ite (= n 0) (- 1) 
    (ite (= e (select a n)) n (find a e (- n 1)))))))

There are mainly several reasons to avoid a par-like binder. 

1. It would require declare-fun to have a variable number of arguments (3 for monomorphic functions and 2 for polymorphic ones), which has so far being avoided in the language;
2. It would complicate the syntax, and hence the parsing, of commands  such as assert and check-sat-assuming, in order to enforce prenex polymorphism.
3. Enforcing prenex polymorphism is not trivial, when considering formula naming or assumptions, that can hide a negation in a subtle way

Feature 2: Higher-order maps

We have added a theory of maps, HO-Core, which can be used like first-class functions, that is, constructed as terms, passed as arguments, and returned as results. The new theory introduces

• a new binary sort constructor, ->, for the sort of maps from one set to another (e.g., (-> Int Real) ),
• a new binder, lambda, for constructing maps (e.g., (lambda ((x Int) (y Int)) (+ x y)) ), and 
• an application symbol, _,  for applying a map to a value (e.g., (_ f x) ).

Values of sorts of the form (-> T1 T2) are data, as with any other sorts. That is, they can be passed to and returned by functions. Note that they are different from SMT-LIB 2 functions (those declared with declare-fun) but it is easy to convert between the two.

--------------------------------
Example
--------------------------------

(declare-sort-parameter E)

; (array-all a p) is true iff all elements of a satisfy  
; the predicate represented by the Boolean mapping p
;
(define-fun-rec array-all 
 ((a (Array Int E)) (p (-> E Bool)) (n Int)) Bool
 (or (= n 0) 
  (and (_ p (select a n)) (array-all a p (- n 1)))))

(declare-const a (Array Int Int))

(assert (array-all a (lambda ((x Int)) (> x 0))))


--------------------------------
Example
--------------------------------

; function declaration
(declare-fun f1 (Int Int) Int)

; function-to-mapping conversion
(define-fun m1 () (-> Int Int Int) 
 (lambda ((x Int) (y Int)) (f1 x y)))

; mapping declaration
(declare-const m2 (-> Int Int Int))

; mapping-to-function conversion
(define-fun f2 ((x Int) (y Int)) Int 
 (_ m2 x y))
--------------------------------

Introducing maps is a way to have the analogous of first-class functions in a logic, like that of SMT-LIB 2, which has only first-order syntax. Maps and functions will be merged in Version 3, where -> will become part of the underlying, higher-order logic and denote the function type constructor, lambda will denote the usual function abstraction, and the syntax of function application (f x) will be seen as a shorthand of (_ f x).


Feature 3: Stronger requirements on get-model

In SMT-LIB 2.6, the result of the get-model command is a list of definitions, using the define-fun and define-fun(s)-rec commands, that provide values for each uninterpreted symbol in the context at the time get-model is executed. (Theory symbols are not defined in a model, as they are considered to be builtin, but they can be used in definitions.)

SMT-LIB 2.7 adds the restriction of disallowing forward references in symbol definitions, for both user-defined and solver-defined symbols. More precisely, each symbol defined in a model can occur in the body of a definition only if it has been previously defined in the model or is one of the symbols being recursively defined by that definition.

This restriction is stronger than necessary since forward references that do not introduce circularity can always be resolved, for instance with two passes over the model. However, it simplifies model parsing without sacrificing expressiveness, while ruling out the possibility of circular definitions.

Note that this is a strictly syntactic restriction. It rules out models like the following:

(
 (define-fun-rec f ((x Int)) Int
  (ite (< x 0) (g x) (f (- x 1))))

 (define-fun g ((x Int)) Int (+ x 1))
)

which can however be rewritten as 

(
 (define-fun g ((x Int)) Int (+ x 1))

 (define-fun-rec f ((x Int)) Int
  (ite (< x 0) (g x) (f (- x 1)))
 )
)

Nevertheless, it does not prevent models like this one:

(
 (define-funs-rec (
   (f ((x Int)) Int (g x))
   (g ((x Int)) Int (f x))
  )
 )
)

where the mutual recursion between f and g is not well-founded, something that is much harder to check in general without additional annotations, such as a decreasing measure for the input of the recursive functions.