UNSURE: SMT: omit prop equations, only encode logical equations

Author: mtzguido

src/smtencoding/FStarC.SMTEncoding.Encode.fst

@@ -925,13 +925,12 @@ let encode_top_level_let :
                                          (univ_terms @ List.map mkFreeV vars)
                 in
                 let is_logical =
-                  // match (SS.compress t_body).n with
-                  // | Tm_fvar fv when S.fv_eq_lid fv FStarC.Parser.Const.prop_lid -> true
-                  // | _ -> false
-
+                  match (SS.compress t_body).n with
+                  | Tm_fvar fv when S.fv_eq_lid fv FStarC.Parser.Const.prop_lid -> true
+                  | _ -> false
                   // GE: this is a cute idea, but the formula axiom shouldn't
                   // replace the default equation axiom, so disabling this for now
-                  false
+                  // false
                 in
                 let is_smt_theory_symbol =
                     let fv = Inr?.v lbn in
@@ -941,29 +940,32 @@ let encode_top_level_let :
                     not is_smt_theory_symbol
                     && (quals |> List.contains Logic || is_logical)
                 in
-                let make_eqn name pat app body =
-                    //NS 05.25: This used to be mkImp(mk_and_l guards, mkEq(app, body))),
-                    //But the guard is unnecessary given the pattern
+                (* Emit an axiom for the equality between lhs and rhs, guarded
+                by pattern pat. The free variables in both terms and the pattern (vars),
+                are all quantified universally. *)
+                let make_eqn name (pat lhs rhs : term) : ML _ =
+                    // NS 2016.05.25: This used to be mkImp(mk_and_l guards, mkEq(lhs, rhs))),
+                    // But the guard is unnecessary given the pattern
+                    // GM: ^ Is this still true?
                     Util.mkAssume(mkForall (S.range_of_lbname lbn)
-                                           ([[pat]], vars, mkEq(app,body)),
+                                           ([[pat]], vars, mkEq(lhs, rhs)),
                                   Some (Format.fmt1 "Equation for %s" (string_of_lid flid)),
                                   (name ^ "_" ^ fvb.smt_id))
                 in
-                let eqns,decls2 =
-                  let basic_eqn_name =
-                    if should_encode_logical
-                    then "defn_equation"
-                    else "equation"
-                  in
+                let eqns, decls2 =
                   let basic_eqn, decls =
                     let body, decls = encode_term body env' in
-                    make_eqn basic_eqn_name app app body, decls
+                    if is_logical then
+                      Caption "omitting eqn for prop", []
+                    else
+                      let pat = app in
+                      make_eqn "definition_equation" pat app body, decls
                   in
                   if should_encode_logical
                   then let pat, app, (body, decls2) =
                            app, mk_Valid app, encode_formula body env'
                        in
-                       let logical_eqn = make_eqn "equation" pat app body in
+                       let logical_eqn = make_eqn "logical_equation" pat app body in
                        [logical_eqn; basic_eqn], decls@decls2
                   else [basic_eqn], decls
                 in