Parser fails to account for universe declarations in model with members

[tchajed]

The following test fails, with an error along the lines of "parse error: expected define-fun on declare-fun".

use rsmt2::print::SmtParser;

#[test]
fn test_declare_fun_in_model() {
    let txt = r"
(model
  ;; universe for thread:
  ;;   thread!val!0 thread!val!1
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun thread!val!0 () thread)
  (declare-fun thread!val!1 () thread)
  ;; cardinality constraint:
  (forall ((x thread)) (or (= x thread!val!0) (= x thread!val!1)))
  ;; -----------
  (define-fun t0 () thread
    thread!val!1)
  (define-fun q () Bool
    false)
  (define-fun p ((x!0 thread)) Bool
    false)
)";
    let mut parser = SmtParser::of_str(txt);
    parser
        .get_model(false, ())
        .map_err(|err| err.to_string())
        .expect("parse error");
}

I got that model from running 4.8.5 the following SMT2 file (4.11.2 also emits declare-funs):

; Command:
; > z3 -in -smt2

(declare-sort thread 0)

(declare-fun p ( 
thread 
) Bool)

(declare-fun q ( 
) Bool)

(declare-fun t0 ( 
) thread)

(assert
    (=> (forall ((t thread)) (p t)) q)
)

(assert
    (not q)
)

(assert (not (p t0)) )

(check-sat)

(get-model)

Note that CVC4/CVC5 do not do this.

[tchajed]

Actually the representation of a Model in rsmt2 doesn't account for these universe members, so it's not clear how to fix this. The universe members could simply be ignored and show up as free variables in the model, but this isn't ideal.

[AdrienChampion]

The notion of universe does not exist in the SMT-LIB standard, or maybe I missed it?

Whether it's z3-specific or not, could you provide a reference for what universes are? I've been out of the SMT game for a while now, it's the first time I hear about universes in this context :/

[tchajed]

Sorry, I'm also not that familiar with SMT so I might not be using standard terminology.

In the example above the model requires that the thread sort have at least two distinct members. Z3 reports the model in SMT-LIB by first providing declare-fun expressions that name them (thread!val!0 and thread!val!1). It also has a "cardinality constraint" for some reason that says these are the only values in the sort thread. The model then refers to these variables.

In CVC5, we get the following model representation:

(
; cardinality of thread is 2
; rep: (as @thread_0 thread)
; rep: (as @thread_1 thread)
(define-fun p ((_arg_1 thread)) Bool false)
(define-fun q () Bool false)
(define-fun t0 () thread (as @thread_0 thread))
)

Here the individuals in thread are given by (as @thread_0 thread) and (as @thread_1 thread), and the cardinality is simply listed in a comment (which is actually unfortunate, it's important to know the cardinality since this isn't a counter-example if thread has cardinality 1).

And finally CVC4 does something different still:

(model
; cardinality of thread is 2
(declare-sort thread 0)
; rep: @uc_thread_0
; rep: @uc_thread_1
(define-fun p ((BOUND_VARIABLE_323 thread)) Bool false)
(define-fun q () Bool false)
(define-fun t0 () thread @uc_thread_0)
)

Here the (declare-sort thread 0) confuses the rsmt2 model parser, and the cardinality is still only given in a comment.

[AdrienChampion]

Sorry, I'm also not that familiar with SMT so I might not be using standard terminology.

No need to apologize, as far as I can tell you are using proper terminology :D Also, thank you for going through the various solvers and listing their output.

I'm quite familiar with SMT-LIB myself, at least older versions, but this universe stuff is news to me. I can't find it in the standard, so it looks like a feature that's not been standardized yet (like check-sat-assuming in z3 a while ago).

I'd rather wait until it's part of the standard to do anything, but if you tell me you need this right now then we could add support for this and then feature-gate it.