Different behavior between API and direct call to z3

[franchouze]

Hello,

I am new user of z3 and I noticed a different behavior between API and direct call to z3.

What I have done so far is:

• Write using z3 api a piece of code (see below) that defines a function that calls a datatype accessor.
• In this code I got the solver content as string and put this in a smt file. I added before "(set-option :produce-models true)" and after "(check-sat) (get-model)". The smt file content is:

(set-option :produce-models true)
(declare-datatypes ((BB_record 0)) (((mk_record (f1 Bool) (f2 Bool)))))
(declare-fun rec_tt () BB_record)
(declare-fun rec_ft () BB_record)
(declare-fun rvar () BB_record)
(declare-fun R1 (BB_record) Bool)
(assert (= rec_tt (mk_record true true)))
(assert (= rec_ft (mk_record false true)))
(assert (forall ((rvar BB_record)) (= (R1 rvar) (= (f1 rvar) (not (f1 rec_tt))))))
(check-sat)
(get-model)

When calling z3 directly, the funtion R1 from the resulting model is what I expect:

	(define-fun R1 ((x!0 BB_record)) Bool
	  (not (f1 x!0)))

When calling the API, the function R1 is:

	(define-fun R1 ((x!0 BB_record)) Bool
	  false)	

To find outwhy the behavior is different I printed traces from z3 (also below) and saw

register rvar
(mk_record true false)

It seems that the forall has been removed and rvar has been set to {f1=true;f2=false} but I do not understand why. Any ideas ?

Thank you for your help.

François

code snippet:

(* create the datatype BB_record with two bool fields f1 and f2 *)
let create_r_datatype ctx  =
  let mk_record = Z3.Symbol.mk_string ctx "mk_record" in
  let recognizer_record = Z3.Symbol.mk_string ctx "mk_record" in
  let fields_symbol = [Z3.Symbol.mk_string ctx "f1"; Z3.Symbol.mk_string ctx "f2"] in
  let field_sorts = [Some (Z3.Boolean.mk_sort ctx); Some (Z3.Boolean.mk_sort ctx)] in
  let r_datatype_constructor = Z3.Datatype.mk_constructor ctx mk_record recognizer_record fields_symbol field_sorts [0;0] in
  Z3.Datatype.mk_sort_s ctx "BB_record" [r_datatype_constructor]
in

(* declare rec_tt () = (mk_record true true) and rec_ft () = (mk_record false true)*)
let declare_rec (r_name, l) ctx so r_datatype =
  let r_datatype_constructor_func_decl = List.hd (Z3.Datatype.get_constructors r_datatype) in
  let r_decl = Z3.FuncDecl.mk_const_decl_s ctx r_name r_datatype in
  let r_app = Z3.Expr.mk_app ctx r_decl [] in
  let fs_expr = List.map ( fun x -> (if x then Z3.Boolean.mk_true ctx  else Z3.Boolean.mk_false ctx)) l in
  let r_ctor_app = Z3.Expr.mk_app ctx r_datatype_constructor_func_decl fs_expr in
  let r_constraint = Z3.Boolean.mk_eq ctx r_app r_ctor_app in
  Z3.Solver.add so [r_constraint];
  r_decl
in

(*declare function R1 : R1 rvar = ((f1 rvar) == !(f1 rec_tt))*)
let declare_fun_f ctx so r_datatype r_None_app i =
  let r_name = Format.sprintf "R%d" i in
  let f = Z3.FuncDecl.mk_func_decl_s ctx r_name [r_datatype]  (Z3.Boolean.mk_sort ctx) in
  (* creates the function application*)
  let rvar = Z3.Symbol.mk_string ctx "rvar" in
  let rvar_expr = Z3.Expr.mk_const ctx rvar r_datatype in
  let r_app = Z3.Expr.mk_app ctx f [rvar_expr] in
  (* get the accessor of the i-th element *)
  let r_datatype_accessors = Array.of_list ( List.hd (Z3.Datatype.get_accessors r_datatype)) in
  let current_accessor = r_datatype_accessors.((i-1)) in
  (* apply the accessor on the no f case *)
  let no_r_accessor_expr = Z3.Boolean.mk_not ctx ( Z3.FuncDecl.apply current_accessor [r_None_app] ) in
  (* for input arg use for all quantifier *)
  let rvar_accessor_expr = Z3.FuncDecl.apply current_accessor [rvar_expr] in
  (* explicit the content of the function *)
  let r_body = Z3.Boolean.mk_eq ctx r_app (Z3.Boolean.mk_eq ctx rvar_accessor_expr no_r_accessor_expr) in
  let constr = Z3.Quantifier.expr_of_quantifier( Z3.Quantifier.mk_forall ctx [r_datatype] [rvar] r_body None [] [] None None) in
  Z3.Solver.add so [constr];
  r_app
in

let run () =
  Z3.enable_trace "simplifier";
  Z3.enable_trace "propagate-values";
  Z3.enable_trace "nlsat";
  Z3.enable_trace "model";
  Z3.enable_trace "model_constructor";
  Z3.enable_trace "context";
  Z3.enable_trace "expr_context_simplifier";
  Z3.enable_trace "expr2var";
  Z3.enable_trace "mk_quantifier";
  Z3.enable_trace "eliminate";
  Z3.enable_trace "eq";
  Z3.enable_trace "before_check_sat";
  Z3.enable_trace "ast";
  Z3.enable_trace "add_eq";
  Z3.enable_trace "tactic";
  Z3.enable_trace "cube";
  let cfg = [("proof", "false"); ("model", "true"); ("trace","true");("auto_config","true")] in
  let ctx = Z3.mk_context cfg in
  let so = Z3.Solver.mk_solver ctx None in
  let r_datatype = create_r_datatype ctx in
  let r_combinations = [("rec_tt",[ true; true ]); ("rec_ft",[ false; true ])] in
  let r_rvar_decl_list = List.map (fun  x -> (declare_rec x ctx so r_datatype))  r_combinations in
  let r_rvar_app_list = List.map (fun decl -> Z3.FuncDecl.apply  decl [] ) r_rvar_decl_list in
  let r_None_app = List.hd r_rvar_app_list in
  let _ = List.map (fun i -> (declare_fun_f ctx so r_datatype r_None_app i)) [1] in  
  Format.printf "%s@." (Z3.Solver.to_string so);
  match (Z3.Solver.check so []) with
  | Z3.Solver.SATISFIABLE ->
      begin
        let m_option = Z3.Solver.get_model so in
        match m_option with
        |None -> assert false;
        |Some valid_m ->  Format.printf "%s@." (Z3.Model.to_string valid_m);    
      end
  |_ -> assert false;
in
run ()

The .z3-trace file :

-------- [tactic] check_sat_core2 ../src/solver/tactic2solver.cpp:239 ---------
(goal
  (= rec_tt (mk_record true true))
  (= rec_ft (mk_record false true))
  (forall ((rvar BB_record)) (= (R1 rvar) (= (f1 rvar) (not (f1 rec_tt))))))
------------------------------------------------
-------- [simplifier] operator() ../src/tactic/core/simplify_tactic.cpp:65 ---------
(goal
  (= rec_tt (mk_record true true))
  (= rec_ft (mk_record false true))
  (not (= (= (f1 rec_tt) (f1 rvar)) (R1 rvar))))
------------------------------------------------
-------- [simplifier] operator() ../src/tactic/core/simplify_tactic.cpp:65 ---------
(goal
  (= rec_tt (mk_record true true))
  (= rec_ft (mk_record false true))
  (not (= (= (f1 rec_tt) (f1 rvar)) (R1 rvar))))
------------------------------------------------
-------- [simplifier] operator() ../src/tactic/core/simplify_tactic.cpp:65 ---------
(goal
  (= rec_tt (mk_record true true))
  (= rec_ft (mk_record false true))
  (not (= (f1 rvar) (R1 rvar))))
------------------------------------------------
-------- [simplifier] append ../src/ast/simplifiers/model_reconstruction_trail.cpp:172 ---------
rec_ft <- (mk_record false true)
rec_tt <- (mk_record true true)
(model-add rec_ft () BB_record (mk_record false true))
(model-add rec_tt () BB_record (mk_record true true))
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:470 ---------
assigning: #33 = #48
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:504 ---------
merging: #33 #48 n1: #33
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:470 ---------
assigning: #41 = #49
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:504 ---------
merging: #41 #49 n1: #41
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:470 ---------
assigning: #29 = #47
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:504 ---------
merging: #29 #47 n1: #29
------------------------------------------------
-------- [context] del_clause ../src/smt/smt_context.cpp:2022 ---------
deleting 1 -5 -6:
(or (f1 rvar) (not (R1 rvar)) (not (= (f1 rvar) (R1 rvar))))
------------------------------------------------
-------- [context] del_clause ../src/smt/smt_context.cpp:2022 ---------
deleting -1 5 -6:
(or (not (f1 rvar)) (R1 rvar) (not (= (f1 rvar) (R1 rvar))))
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:470 ---------
assigning: #33 = #1
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:504 ---------
merging: #48 #1 n1: #33
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:470 ---------
assigning: #48 = #1
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:480 ---------
redundant constraint.
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:470 ---------
assigning: #49 = #2
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:504 ---------
merging: #49 #2 n1: #49
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:470 ---------
assigning: #41 = #2
------------------------------------------------
-------- [add_eq] add_eq ../src/smt/smt_context.cpp:480 ---------
redundant constraint.
------------------------------------------------
-------- [context] get_proof ../src/smt/smt_clause_proof.cpp:240 ---------
get-proof 0
------------------------------------------------
-------- [context] get_proof ../src/smt/smt_context.cpp:4636 ---------
null
------------------------------------------------
-------- [model] register_decl ../src/model/model_core.cpp:56 ---------
register rvar
(mk_record true false)
------------------------------------------------
-------- [model] register_decl ../src/model/model_core.cpp:56 ---------
register rvar
(mk_record true false)
------------------------------------------------
-------- [model] mk_func_interps ../src/smt/smt_model_generator.cpp:433 ---------
insert new entry for:
(R1 rvar)
args: #29 
(mk_record true false) 
value: #30
false
------------------------------------------------
-------- [model] register_macros ../src/smt/smt_model_generator.cpp:489 ---------
num. macros: 0
------------------------------------------------
-------- [model] mk_model ../src/smt/smt_model_generator.cpp:510 ---------
rvar -> (mk_record true false)
R1 -> {
  (mk_record true false) -> false
  else -> ...
}
------------------------------------------------
-------- [model] register_decl ../src/model/model_core.cpp:56 ---------
register rvar
(mk_record true false)
------------------------------------------------
-------- [model] add_rec_funs ../src/model/model.cpp:636 ---------
(define-fun rvar () BB_record
  (mk_record true false))
(define-fun R1 ((x!0 BB_record)) Bool
  (ite (= x!0 (mk_record true false)) false
    false))
------------------------------------------------
-------- [add_eq] undo_add_eq ../src/smt/smt_context.cpp:920 ---------
undo_add_eq #49 #2
------------------------------------------------
-------- [add_eq] undo_add_eq ../src/smt/smt_context.cpp:920 ---------
undo_add_eq #48 #1
------------------------------------------------
-------- [add_eq] undo_add_eq ../src/smt/smt_context.cpp:920 ---------
undo_add_eq #29 #47
------------------------------------------------
-------- [add_eq] undo_add_eq ../src/smt/smt_context.cpp:920 ---------
undo_add_eq #41 #49
------------------------------------------------
-------- [add_eq] undo_add_eq ../src/smt/smt_context.cpp:920 ---------
undo_add_eq #33 #48
------------------------------------------------
-------- [tactic] check_sat ../src/tactic/tactic.cpp:192 ---------
r.size(): 1
(goal
  :precision precise :depth 6)
------------------------------------------------
-------- [model] register_decl ../src/model/model_core.cpp:56 ---------
register rvar
(mk_record true false)
------------------------------------------------
-------- [model] register_decl ../src/model/model_core.cpp:56 ---------
register rec_tt
(mk_record true true)
------------------------------------------------
-------- [model] register_decl ../src/model/model_core.cpp:56 ---------
register rec_ft
(mk_record false true)
------------------------------------------------
-------- [tactic] check_sat_core2 ../src/solver/tactic2solver.cpp:259 ---------
(define-fun rvar () BB_record
  (mk_record true false))
(define-fun rec_tt () BB_record
  (mk_record true true))
(define-fun rec_ft () BB_record
  (mk_record false true))
(define-fun R1 ((x!0 BB_record)) Bool
  (ite (= x!0 (mk_record true false)) false
    false))



------------------------------------------------

-------- [tactic] check_sat_core2 ../src/solver/tactic2solver.cpp:260 ---------
g:
(model-add rec_ft () BB_record (mk_record false true))
(model-add rec_tt () BB_record (mk_record true true))
(model-add rvar () BB_record (mk_record true false))
(model-add R1 ((x!1 BB_record)) Bool false)

model:
(define-fun rvar () BB_record
  (mk_record true false))
(define-fun rec_tt () BB_record
  (mk_record true true))
(define-fun rec_ft () BB_record
  (mk_record false true))
(define-fun R1 ((x!0 BB_record)) Bool
  (ite (= x!0 (mk_record true false)) false
    false))
------------------------------------------------
-------- [model] cleanup_expr ../src/model/model.cpp:439 ---------
cleaning up:
false
------------------------------------------------
-------- [model] cleanup_expr ../src/model/model.cpp:439 ---------
cleaning up:
(mk_record false true)
------------------------------------------------
-------- [model] cleanup_expr ../src/model/model.cpp:439 ---------
cleaning up:
(mk_record true false)
------------------------------------------------
-------- [model] cleanup_expr ../src/model/model.cpp:439 ---------
cleaning up:
(mk_record true true)
------------------------------------------------

[franchouze]

It was indeed a bug in my function. It seems that it was because I used mk_forall instead of mk_forall_const. The quantifier should be :

  let constr = Z3.Quantifier.expr_of_quantifier( Z3.Quantifier.mk_forall_const ctx [rvar_expr] r_body None [] [] None None) in