Skip to content

WIP: Supporting CVC5 #3990

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
mtzguido wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

WIP: Supporting CVC5 #3990

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
33d4962
SMT: avoid identifiers starting with @
mtzguido Aug 25, 2025
bd75900
SMT: use => and = for implies/iff
mtzguido Aug 25, 2025
e141102
SMT: Fix some datatype declarations
mtzguido Aug 25, 2025
d6e8a7b
WIP: First steps in enabling use of CVC5
mtzguido Aug 25, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/basic/FStarC.Options.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
17 changes: 11 additions & 6 deletions src/smtencoding/FStarC.SMTEncoding.Encode.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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 "<labels>"] @ label_suffix @ [Term.Echo "</labels>"; 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 "<labels>"] @ label_suffix @ [Term.Echo "</labels>"]
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
Expand Down
2 changes: 1 addition & 1 deletion src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
26 changes: 22 additions & 4 deletions src/smtencoding/FStarC.SMTEncoding.Solver.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -256,20 +256,29 @@ let with_fuel_and_diagnostics settings label_assumptions =
Term.Caption (Format.fmt2 "<fuel='%s' ifuel='%s'>"
(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 "<initial_stats>";
Term.GetStatistics;
Term.Echo "</initial_stats>";

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
Expand Down Expand Up @@ -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
Expand All @@ -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 =
Expand Down
39 changes: 22 additions & 17 deletions src/smtencoding/FStarC.SMTEncoding.Term.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -236,8 +236,8 @@ let op_to_string = function
| Not -> "not"
| And -> "and"
| Or -> "or"
| Imp -> "implies"
| Iff -> "iff"
| Imp -> "=>"
| Iff -> "="
| Eq -> "="
| LT -> "<"
| LTE -> "<="
Expand Down Expand Up @@ -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)))]

Expand Down Expand Up @@ -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\
Expand All @@ -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\
Expand Down Expand Up @@ -1009,25 +1014,25 @@ 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\
:qid __prelude_valid_intro)))\n"
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"
Expand Down
33 changes: 23 additions & 10 deletions src/smtencoding/FStarC.SMTEncoding.Z3.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down Expand Up @@ -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
Expand All @@ -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 =
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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 ()))
Expand Down
Loading