Fresh names in polymorphic model

[Halbaroth]

Consider the following input file (which is a polymorphic version of our list.models.smt2):

(set-option :produce-models true)
(set-logic ALL)
(declare-datatypes ((List 1)) (
  (par (T) (
    (nil)
    (cons (head T) (tail (List T)))
  ))
))
(declare-sort T 0)
(declare-const a (List T))
(declare-const b (List T))
(declare-const c (List T))
(declare-const d (List T))
(assert (= (tail a) b))
(assert ((_ is cons) c))
(assert (= (tail c) d))
(check-sat)
(get-model)

Alt-Ergo outputs:

(
  (define-fun a () (List T) nil)
  (define-fun b () (List T) nil)
  (define-fun c () (List T) (cons .k2 nil))
  (define-fun d () (List T) nil)
)

which is not correct as .k2 is defined (and as it starts by a dot, it should not appear in models). We expect to get an abstract value instead of .k2.

I tried to fix this bug but it is actually very annoying. A simple fix consists in replace fresh_name by mk_abstract at some places in relation modules but it makes sense to use fresh_name here. Most of the times, there are not supposed to appear in models!

I think that a decent fix consists in applying a substitution on representative terms before generating model terms. This substitution replaces fresh leaves by abstract ones and we have to ensure that we never generate two different abstract values for the same fresh ones.

[bclement-ocp]

I think that a decent fix consists in applying a substitution on representative terms before generating model terms. This substitution replaces fresh leaves by abstract ones and we have to ensure that we never generate two different abstract values for the same fresh ones.

This should be the job of Uf.assign_next / X.assign_value, which they are not doing properly because our definition of model terms (called "value terms" in the SMT-LIB standard) is wrong: only abstract constants should be treated as such.

[Halbaroth]

Of course, I tried to fix this bug by modifying Uf.assign_next and X.assign_value but it is not sufficient. I will investigate later.

[bclement-ocp]

Quick proof of concept (the code for array models needs to be adapted):

diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml
index cb8e1170..b14b3d56 100644
--- a/src/lib/reasoners/records.ml
+++ b/src/lib/reasoners/records.ml
@@ -390,12 +390,12 @@ module Shostak (X : ALIEN) = struct
     | Record (_, ty) ->
       if List.exists (fun (t,_) -> Expr.is_model_term t) eq
       then None
-      else Some (Expr.fresh_name ty, false)
+      else Some (Expr.mk_abstract ty, false)
 
     | Other (_,ty) ->
       match ty with
       | Ty.Trecord { Ty.lbs; _ } ->
-        let rev_lbs = List.rev_map (fun (_, ty) -> Expr.fresh_name ty) lbs in
+        let rev_lbs = List.rev_map (fun (_, ty) -> Expr.mk_abstract ty) lbs in
         let s = E.mk_term (Symbols.Op Symbols.Record) (List.rev rev_lbs) ty in
         Some (s, false) (* false <-> not a case-split *)
       | _ -> assert false
diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml
index 8b308859..bd7df537 100644
--- a/src/lib/reasoners/shostak.ml
+++ b/src/lib/reasoners/shostak.ml
@@ -579,13 +579,6 @@ struct
       | _, Ty.Treal     -> ARITH.assign_value r distincts eq
       | _, Ty.Trecord _ -> RECORDS.assign_value r distincts eq
       | _, Ty.Tbitv _   -> BITV.assign_value r distincts eq
-      | Term t, Ty.Tfarray _ ->
-        begin
-          if List.exists (fun (t,_) -> Expr.is_model_term t) eq then None
-          else
-            Some (Expr.fresh_name (Expr.type_info t), false)
-        end
-
       | _, Ty.Tadt _    when not (Options.get_disable_adts()) ->
         ADT.assign_value r distincts eq
 
@@ -610,7 +603,7 @@ struct
       | Term t, ty      -> (* case disable_adts() handled here *)
         if Expr.is_model_term t ||
            List.exists (fun (t,_) -> Expr.is_model_term t) eq then None
-        else Some (Expr.fresh_name ty, false) (* false <-> not a case-split *)
+        else Some (Expr.mk_abstract ty, false) (* false <-> not a case-split *)
       | _               ->
         (* There is no model-generation support for the AC symbols yet.
            The function [AC.assign_value] always returns [None]. *)
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index b9bd5fc4..b9d95b1b 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -927,8 +927,16 @@ let mk_trigger ?user:(from_user = false) ?depth ?(hyp = []) content =
 let mk_term s l ty =
   assert (match s with Sy.Lit _ | Sy.Form _ -> false | _ -> true);
   let d = match l with
-    | [] ->
-      1 (*no args ? depth = 1 (ie. current app s, ie constant)*)
+    | [] -> (
+        match s with
+        | Sy.Name { ns = Abstract; _ } ->
+          (* make sure abstract constants are smaller than other terms, since
+             they are used as values in models. *)
+          0
+        | _ ->
+          (* no args ? depth = 1 (ie. current app s, ie constant) *)
+          1
+      )
     | _ ->
       (* if args, d is 1 + max_depth of args (equals at least to 1 *)
       1 + List.fold_left (fun z t -> max z t.depth) 1 l
@@ -1114,7 +1122,8 @@ let rec is_model_term e =
   | Op Div, [{ f = Real _; _ }; { f = Real _; _ }] -> true
   | Op Minus, [{ f = Real q; _ }; { f = Real _; _ }] -> Q.equal q Q.zero
   | Op Minus, [{ f = Int i; _ }; { f = Int _; _ }] -> Z.equal i Z.zero
-  | (True | False | Name _ | Int _ | Real _ | Bitv _), [] -> true
+  | Name { ns = Abstract; _ }, [] -> true
+  | (True | False | Int _ | Real _ | Bitv _), [] -> true
   | _ -> false
 
 let[@inline always] is_value_term e =

[Halbaroth]

I think we have to accept Name { ns = User; _ } in is_model_term too?

[Halbaroth]

Basically, that was my patch but I changed Expr.compare instead of changing the depth of formula. I still got issues with arrays but I did not search further because it is no a priority.

[bclement-ocp]

I think we have to accept Name { ns = User; _ } in is_model_term too?

I don't think so (and I think that is the source of the bug). is_model_term should return true if the term is a value, and user-defined constants are not values.

[Halbaroth]

Uhm I see. I thought it was okay to use a User defined term as a value.