diff --git a/src/basic/FStarC.Options.fst b/src/basic/FStarC.Options.fst index 612d2906dca..af563bbb45c 100644 --- a/src/basic/FStarC.Options.fst +++ b/src/basic/FStarC.Options.fst @@ -2179,7 +2179,7 @@ let retry () = get_retry () let reuse_hint_for () = get_reuse_hint_for () let report_assumes () = get_report_assumes () let silent () = get_silent () -let smt () = get_smt () +let smt () = if Ext.enabled "cvc" then Some "cvc5" else get_smt () let smtencoding_elim_box () = get_smtencoding_elim_box () let smtencoding_nl_arith_native () = get_smtencoding_nl_arith_repr () = "native" let smtencoding_nl_arith_wrapped () = get_smtencoding_nl_arith_repr () = "wrapped" diff --git a/src/smtencoding/FStarC.SMTEncoding.Encode.fst b/src/smtencoding/FStarC.SMTEncoding.Encode.fst index af55146bd80..661ec5f40eb 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Encode.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Encode.fst @@ -438,7 +438,7 @@ let encode_free_var uninterpreted env fv tt t_norm quals :decls_t & env_t = let guard, decls1 = match pre_opt with | None -> mk_and_l guards, decls1 | Some p -> let g, ds = encode_formula p env' in mk_and_l (g::guards), decls1@ds in - let dummy_var = mk_fv ("@dummy", dummy_sort) in + let dummy_var = mk_fv ("_dummy", dummy_sort) in let dummy_tm = Term.mkFreeV dummy_var Range.dummyRange in let should_thunk () = //See note [Thunking Nullary Constants] in FStarC.SMTEncoding.Term.fs @@ -782,7 +782,7 @@ let encode_top_level_let : let vars, binder_guards, env', binder_decls, _ = encode_binders None binders env' in let vars, app = if fvb.fvb_thunked && vars = [] - then let dummy_var = mk_fv ("@dummy", dummy_sort) in + then let dummy_var = mk_fv ("_dummy", dummy_sort) in let dummy_tm = Term.mkFreeV dummy_var Range.dummyRange in let app = Term.mkApp (fvb.smt_id, [dummy_tm]) (S.range_of_lbname lbn) in [dummy_var], app @@ -941,10 +941,10 @@ let encode_top_level_let : "equation_with_fuel_" ^g) in let eqn_f = Util.mkAssume(mkForall (S.range_of_lbname lbn) ([[app]], vars, mkEq(app, gmax)), Some "Correspondence of recursive function to instrumented version", - ("@fuel_correspondence_"^g)) in + ("_fuel_correspondence_"^g)) in let eqn_g' = Util.mkAssume(mkForall (S.range_of_lbname lbn) ([[gsapp]], fuel::vars, mkEq(gsapp, mk_g_app (Term.n_fuel 0::vars_tm))), Some "Fuel irrelevance", - ("@fuel_irrelevance_" ^g)) in + ("_fuel_irrelevance_" ^g)) in let aux_decls, g_typing = let gapp = mk_g_app (fuel_tm::vars_tm) in let tok_corr = @@ -2029,8 +2029,13 @@ let encode_query use_env_msg (tcenv:Env.env) (q:S.term) @qdecls @(caption |> mk_decls_trivial) |> recover_caching_and_update_env env |> decls_list_of in //recover caching and flatten - let qry = Util.mkAssume(mkNot phi, Some "query", (varops.mk_unique "@query")) in - let suffix = [Term.Echo ""] @ label_suffix @ [Term.Echo ""; Term.Echo "Done!"] in + let qry = Util.mkAssume(mkNot phi, Some "query", (varops.mk_unique "_query")) in + let suffix = + if Options.Ext.enabled "cvc" + then [] + else [Term.Echo ""] @ label_suffix @ [Term.Echo ""] + in + let suffix = suffix @ [ Term.Echo "Done!"] in if Debug.medium () || !dbg_SMTEncoding || !dbg_SMTQuery then Format.print_string "} Done encoding\n"; if Debug.medium () || !dbg_SMTEncoding || !dbg_Time diff --git a/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst b/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst index ad05501ff2d..110f710af9a 100644 --- a/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst +++ b/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst @@ -682,7 +682,7 @@ and encode_term (t:typ) (env:env_t) : (term (* encoding of t, expects t match tok.tm with | FreeV _ | App(_, []) -> - let sym_name = "@kick_partial_app_" ^ (BU.digest_of_string tkey_hash) in //the '@' retains this for hints + let sym_name = "_kick_partial_app_" ^ (BU.digest_of_string tkey_hash) in //the '@' retains this for hints [Util.mkAssume(kick_partial_app tok, Some "kick_partial_app", sym_name)], sym_name diff --git a/src/smtencoding/FStarC.SMTEncoding.Solver.fst b/src/smtencoding/FStarC.SMTEncoding.Solver.fst index 2b693ffe683..41a3af0328f 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Solver.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Solver.fst @@ -256,12 +256,16 @@ let with_fuel_and_diagnostics settings label_assumptions = Term.Caption (Format.fmt2 "" (show n) (show i)); - Util.mkAssume(mkEq(mkApp("MaxFuel", []), n_fuel n), None, "@MaxFuel_assumption"); - Util.mkAssume(mkEq(mkApp("MaxIFuel", []), n_fuel i), None, "@MaxIFuel_assumption"); + Util.mkAssume(mkEq(mkApp("MaxFuel", []), n_fuel n), None, "_MaxFuel_assumption"); + Util.mkAssume(mkEq(mkApp("MaxIFuel", []), n_fuel i), None, "_MaxIFuel_assumption"); settings.query_decl //the query itself ] @label_assumptions //the sub-goals that are currently disabled - @[ Term.SetOption ("rlimit", show rlimit); //the rlimit setting for the check-sat + @ + (if Options.Ext.enabled "cvc" + then [] + else [ Term.SetOption ("rlimit", show rlimit); ]) //the rlimit setting for the check-sat + @[ // Print stats just before the query, so we know the initial rlimit. Term.Echo ""; @@ -269,7 +273,12 @@ let with_fuel_and_diagnostics settings label_assumptions = Term.Echo ""; Term.CheckSat; //go Z3! - Term.SetOption ("rlimit", "0"); //back to using infinite rlimit + ] + @ (if Options.Ext.enabled "cvc" + then [] + else [ + Term.SetOption ("rlimit", "0");]) //back to using infinite rlimit + @[ Term.GetReasonUnknown; //explain why it failed ]@ (if settings.query_record_hints @@ -1331,6 +1340,11 @@ type solver_cfg = { z3version : string; context_pruning : bool; record_hints : bool; + cvc_rlimit : int; + (* ^ The rlimit, but only for CVC5. Z3 can change the rlimit + without restarting, so we just set it to zero here for Z3 + and essentially ignore it. For CVC5, changing the rlimit will trigger + a restart. *) } let _last_cfg : ref (option solver_cfg) = mk_ref None @@ -1345,6 +1359,10 @@ let get_cfg env : solver_cfg = ; z3version = Options.z3_version () ; context_pruning = Options.Ext.enabled "context_pruning" ; record_hints = Options.record_hints () + ; cvc_rlimit = + if Options.Ext.enabled "cvc" + then Options.z3_rlimit () + else 0 } let save_cfg env = diff --git a/src/smtencoding/FStarC.SMTEncoding.Term.fst b/src/smtencoding/FStarC.SMTEncoding.Term.fst index 253fb5d6762..62f9f5d2bef 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Term.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Term.fst @@ -236,8 +236,8 @@ let op_to_string = function | Not -> "not" | And -> "and" | Or -> "or" - | Imp -> "implies" - | Iff -> "iff" + | Imp -> "=>" + | Iff -> "=" | Eq -> "=" | LT -> "<" | LTE -> "<=" @@ -268,10 +268,12 @@ let op_to_string = function | Var s -> s let weightToSmtStr : option int -> string = function + | _ when Options.Ext.enabled "cvc" -> "" | None -> "" | Some i -> Format.fmt1 ":weight %s\n" (show i) let weightToSmt : option int -> list document = function + | _ when Options.Ext.enabled "cvc" -> [] | None -> [] | Some i -> [nest 1 (group (doc_of_string ":weight" ^/^ doc_of_string (show i)))] @@ -917,16 +919,19 @@ and declToSmt z3options decl = and mkPrelude z3options = let basic = z3options ^ - "(declare-sort FString)\n\ + "(declare-sort FString 0)\n\ (declare-fun FString_constr_id (FString) Int)\n\ \n\ - (declare-sort Term)\n\ + (declare-sort Term 0)\n\ (declare-fun Term_constr_id (Term) Int)\n\ - (declare-sort Dummy_sort)\n\ + (declare-sort Dummy_sort 0)\n\ (declare-fun Dummy_value () Dummy_sort)\n\ - (declare-datatypes () ((Fuel \n\ - (ZFuel) \n\ - (SFuel (prec Fuel)))))\n\ +(declare-datatypes\n\ + ((Fuel 0))\n\ + ((\n\ + (ZFuel)\n\ + (SFuel (prec Fuel))\n\ + )))\n\ (declare-fun MaxIFuel () Fuel)\n\ (declare-fun MaxFuel () Fuel)\n\ (declare-fun PreType (Term) Term)\n\ @@ -953,10 +958,10 @@ and mkPrelude z3options = (declare-fun ApplyTT (Term Term) Term)\n\ (declare-fun Prec (Term Term) Bool)\n\ (assert (forall ((x Term) (y Term) (z Term))\n\ - (! (implies (and (Prec x y) (Prec y z)) (Prec x z))\n\ + (! (=> (and (Prec x y) (Prec y z)) (Prec x z))\n\ :pattern ((Prec x z) (Prec x y)))))\n\ (assert (forall ((x Term) (y Term))\n\ - (implies (Prec x y)\n\ + (=> (Prec x y)\n\ (not (Prec y x)))))\n\ (declare-fun Closure (Term) Term)\n\ (declare-fun ConsTerm (Term Term) Term)\n\ @@ -1009,17 +1014,17 @@ and mkPrelude z3options = let lex_ordering = "\n(declare-fun Prims.lex_t () Term)\n\ (assert (forall ((t1 Term) (t2 Term) (e1 Term) (e2 Term))\n\ - (! (iff (Valid (Prims.precedes t1 t2 e1 e2))\n\ - (Valid (Prims.precedes Prims.lex_t Prims.lex_t e1 e2)))\n\ - :pattern (Prims.precedes t1 t2 e1 e2))))\n\ + (! (= (Valid (Prims.precedes t1 t2 e1 e2))\n\ + (Valid (Prims.precedes Prims.lex_t Prims.lex_t e1 e2)))\n\ + :pattern ((Prims.precedes t1 t2 e1 e2)))))\n\ (assert (forall ((t1 Term) (t2 Term))\n\ - (! (iff (Valid (Prims.precedes Prims.lex_t Prims.lex_t t1 t2)) \n\ - (Prec t1 t2))\n\ + (! (= (Valid (Prims.precedes Prims.lex_t Prims.lex_t t1 t2)) \n\ + (Prec t1 t2))\n\ :pattern ((Prims.precedes Prims.lex_t Prims.lex_t t1 t2)))))\n" in let valid_intro = "(assert (forall ((e Term) (t Term))\n\ - (! (implies (HasType e t)\n\ + (! (=> (HasType e t)\n\ (Valid t))\n\ :pattern ((HasType e t)\n\ (Valid t))\n\ @@ -1027,7 +1032,7 @@ and mkPrelude z3options = in let valid_elim = "(assert (forall ((t Term))\n\ - (! (implies (Valid t)\n\ + (! (=> (Valid t)\n\ (exists ((e Term)) (HasType e t)))\n\ :pattern ((Valid t))\n\ :qid __prelude_valid_elim)))\n" diff --git a/src/smtencoding/FStarC.SMTEncoding.Z3.fst b/src/smtencoding/FStarC.SMTEncoding.Z3.fst index 0e26547c1fc..ee6b189132d 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Z3.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Z3.fst @@ -137,9 +137,12 @@ let z3_cmd_and_args () = @ Find.Z3.z3_install_suggestion ver) in let cmd_args = - List.append ["-smt2"; - "-in"] - (Options.z3_cliopt ()) in + if Options.Ext.enabled "cvc" then + [ "-" ] + else + ["-smt2"; "-in"] + in + let cmd_args = cmd_args @ Options.z3_cliopt () in (cmd, cmd_args) let warn_handler (suf:Errors.error_message) (s:string) : unit = @@ -199,7 +202,7 @@ let check_z3version (p:proc) : unit = let new_z3proc (id:string) (cmd_and_args : string & list string) : BU.proc = let proc = try - BU.start_process id (fst cmd_and_args) (snd cmd_and_args) (fun s -> s = "Done!") + BU.start_process id (fst cmd_and_args) (snd cmd_and_args) (fun s -> s = "Done!" || s = "\"Done!\"") with | e -> let open FStarC.Pprint in @@ -212,7 +215,8 @@ let new_z3proc (id:string) (cmd_and_args : string & list string) : BU.proc = (Util.print_exn e |> arbitrary_string); ] in - check_z3version proc; + if not (Options.Ext.enabled "cvc") then + check_z3version proc; proc let new_z3proc_with_id = @@ -330,7 +334,7 @@ let smt_output_sections (log_file:option string) (r:Range.t) (lines:list string) match lines with | [] -> None | l::lines -> - if tag = l then Some ([], lines) + if tag = l || "\"" ^ tag ^ "\"" = l then Some ([], lines) else until tag lines |> Option.map (fun (until_tag, rest) -> (l::until_tag, rest)) in @@ -521,9 +525,9 @@ let doZ3Exe (log_file:_) (r:Range.t) (fresh:bool) (input:string) (label_messages core |> List.filter (fun name -> not (BU.for_some (fun wl -> BU.contains name wl) whitelist) && not (BU.starts_with name "binder_") && - not (BU.starts_with name "@query") && - not (BU.starts_with name "@MaxFuel") && - not (BU.starts_with name "@MaxIFuel") && + not (BU.starts_with name "_query") && + not (BU.starts_with name "_MaxFuel") && + not (BU.starts_with name "_MaxIFuel") && not (BU.for_some (fun name' -> name=name') names)) in // Format.print2 "Query %s: Pruned theory would keep %s\n" queryid (String.concat ", " names); @@ -621,7 +625,16 @@ let mk_input (fresh : bool) (theory : list decl) : string & option string & opti (!Options._version) (!Options._commit) ver ) :: EmptyLine :: theory in - let options = z3_options ver in + let options = + if Options.Ext.enabled "cvc" + then Format.fmt1 + "(set-logic ALL)\n\ + (set-option :incremental true)\n\ + (set-option :produce-unsat-cores true)\n\ + (set-option :rlimit-per %s)\n" (show (Options.z3_rlimit () `op_Multiply` 500000)) + // ^ NB: For CVC5, we restart after every rlimit change. + else z3_options ver + in let options = options ^ Format.fmt1 "(set-option :random-seed %s)\n" (show (Options.z3_seed ()))