feat: handle get-model/get-value from smtlib inputs

src/base/Base_types.ml

@@ -328,6 +328,8 @@ type statement =
   | Stmt_assert of term
   | Stmt_assert_clause of term list
   | Stmt_check_sat of (bool * term) list
+  | Stmt_get_model
+  | Stmt_get_value of term list
   | Stmt_exit
 
 let[@inline] term_equal_ (a:term) b = a==b
@@ -1382,6 +1384,8 @@ module Statement = struct
     | Stmt_assert of term
     | Stmt_assert_clause of term list
     | Stmt_check_sat of (bool * term) list
+    | Stmt_get_model
+    | Stmt_get_value of term list
     | Stmt_exit
 
   (** Pretty print a statement *)
@@ -1404,5 +1408,8 @@ module Statement = struct
     | Stmt_exit -> Fmt.string out "(exit)"
     | Stmt_data l ->
       Fmt.fprintf out "(@[declare-datatypes@ %a@])" (Util.pp_list Data.pp) l
+    | Stmt_get_model -> Fmt.string out "(get-model)"
+    | Stmt_get_value l ->
+      Fmt.fprintf out "(@[get-value@ (@[%a@])@])" (Util.pp_list pp_term) l
     | Stmt_define _ -> assert false (* TODO *)
 end

src/core/Sidekick_core.ml

@@ -1238,6 +1238,9 @@ module type SOLVER = sig
         must stop (returning [Unknown]), [false] if solving can proceed.
       @param on_exit functions to be run before this returns *)
 
+  val last_res : t -> res option
+  (** Last result, if any. Some operations will erase this (e.g. {!assert_term}). *)
+
   val push_assumption : t -> lit -> unit
   (** Pushes an assumption onto the assumption stack. It will remain
       there until it's pop'd by {!pop_assumptions}. *)

src/lia/Sidekick_arith_lia.ml

@@ -90,10 +90,10 @@ module Make(A : ARG) : S with module A = A = struct
     | LIA_other t when A.has_ty_int t ->
       SI.declare_pb_is_incomplete si;
       None
-    | LIA_const _ | LIA_op _ | LIA_mult _ ->
+    | LIA_op _ | LIA_mult _ ->
       SI.declare_pb_is_incomplete si;
       None (* TODO: theory combination?*)
-    | LIA_other _ ->
+    | LIA_const _ | LIA_other _ ->
       None
 
   let create_and_setup si =

src/lra/sidekick_arith_lra.ml

@@ -244,11 +244,11 @@ module Make(A : ARG) : S with module A = A = struct
         (* TODO: define proxy *)
         self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le;
         Log.debugf 50
-          (fun k->k "(@[lra.encode-le@ `%a`@ :into-var %a@])" LE_.Comb.pp le_comb T.pp proxy);
+          (fun k->k "(@[lra.encode-linexp@ `%a`@ :into-var %a@])" LE_.Comb.pp le_comb T.pp proxy);
 
         (* it's actually 0 *)
         if LE_.Comb.is_empty le_comb then (
-          Log.debug 50 "(lra.encode-le.is-trivially-0)";
+          Log.debug 50 "(lra.encode-linexp.is-trivially-0)";
           SimpSolver.add_constraint self.simplex
             ~on_propagate:(fun _ ~reason:_ -> ())
             (SimpSolver.Constraint.leq proxy A.Q.zero) Tag.By_def;
@@ -409,7 +409,7 @@ module Make(A : ARG) : S with module A = A = struct
           ((A.Q.minus_one, proxy) :: LE_.Comb.to_list le_comb);
 
         Log.debugf 50
-          (fun k->k "(@[lra.encode-le.with-offset@ %a@ :var %a@ :diff-var %a@])"
+          (fun k->k "(@[lra.encode-linexp.with-offset@ %a@ :var %a@ :diff-var %a@])"
               LE_.Comb.pp le_comb T.pp proxy T.pp proxy2);
 
         declare_term_to_cc proxy;

src/smt-solver/Sidekick_smt_solver.ml

@@ -674,20 +674,7 @@ module Make(A : ARG)
   (** the parametrized SAT Solver *)
   module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal)
 
-  (* main solver state *)
-  type t = {
-    si: Solver_internal.t;
-    solver: Sat_solver.t;
-    stat: Stat.t;
-    proof: P.t;
-    count_clause: int Stat.counter;
-    count_solve: int Stat.counter;
-    (* config: Config.t *)
-  }
-  type solver = t
-
   module Registry = Solver_internal.Registry
-  let[@inline] registry self = Solver_internal.registry self.si
 
   module type THEORY = sig
     type t
@@ -700,93 +687,6 @@ module Make(A : ARG)
   type theory = (module THEORY)
   type 'a theory_p = (module THEORY with type t = 'a)
 
-  (** {2 Main} *)
-
-  let add_theory_p (type a) (self:t) (th:a theory_p) : a =
-    let (module Th) = th in
-    Log.debugf 2
-      (fun k-> k "(@[smt-solver.add-theory@ :name %S@])" Th.name);
-    let st = Th.create_and_setup self.si in
-    (* add push/pop to the internal solver *)
-    begin
-      let open Solver_internal in
-      self.si.th_states <- Ths_cons {
-          st;
-          push_level=Th.push_level;
-          pop_levels=Th.pop_levels;
-          next=self.si.th_states;
-        };
-    end;
-    st
-
-  let add_theory (self:t) (th:theory) : unit =
-    let (module Th) = th in
-    ignore (add_theory_p self (module Th))
-
-  let add_theory_l self = List.iter (add_theory self)
-
-  (* create a new solver *)
-  let create ?(stat=Stat.global) ?size ~proof ~theories tst ty_st () : t =
-    Log.debug 5 "smt-solver.create";
-    let si = Solver_internal.create ~stat ~proof tst ty_st () in
-    let self = {
-      si; proof;
-      solver=Sat_solver.create ~proof ?size ~stat si;
-      stat;
-      count_clause=Stat.mk_int stat "solver.add-clause";
-      count_solve=Stat.mk_int stat "solver.solve";
-    } in
-    add_theory_l self theories;
-    (* assert [true] and [not false] *)
-    begin
-      let tst = Solver_internal.tst self.si in
-      let t_true = Term.bool tst true in
-      Sat_solver.add_clause self.solver
-        [Lit.atom tst t_true]
-        (P.lemma_true t_true self.proof)
-    end;
-    self
-
-  let[@inline] solver self = self.solver
-  let[@inline] cc self = Solver_internal.cc self.si
-  let[@inline] stats self = self.stat
-  let[@inline] tst self = Solver_internal.tst self.si
-  let[@inline] ty_st self = Solver_internal.ty_st self.si
-  let[@inline] proof self = self.si.proof
-
-  let preprocess_acts_of_solver_
-      (self:t) : (module Solver_internal.PREPROCESS_ACTS) =
-    (module struct
-      let proof = self.proof
-      let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.si.tst t
-      let mk_lit ?sign t = Lit.atom ?sign self.si.tst t, None
-      let add_lit ?default_pol lit =
-        Sat_solver.add_lit self.solver ?default_pol lit
-      let add_clause c pr =
-        Sat_solver.add_clause self.solver c pr
-    end)
-
-  (* preprocess literal *)
-  let preprocess_lit_ ~steps (self:t) (lit:lit) : lit =
-    let pacts = preprocess_acts_of_solver_ self in
-    Solver_internal.preprocess_lit_ ~steps self.si pacts lit
-
-  (* preprocess clause, return new proof *)
-  let preprocess_clause_ (self:t)
-      (c:lit IArray.t) (pr:proof_step) : lit IArray.t * proof_step =
-    let steps = ref [] in
-    let c = IArray.map (preprocess_lit_ self ~steps) c in
-    let pr =
-      P.lemma_rw_clause pr
-        ~res:(IArray.to_iter c) ~using:(Iter.of_list !steps) self.proof
-    in
-    c, pr
-
-  (* make a literal from a term, ensuring it is properly preprocessed *)
-  let mk_lit_t (self:t) ?sign (t:term) : lit =
-    let pacts = preprocess_acts_of_solver_ self in
-    Solver_internal.mk_plit self.si pacts ?sign t
-
   (** {2 Result} *)
 
   module Unknown = struct
@@ -837,6 +737,110 @@ module Make(A : ARG)
     | Unknown of Unknown.t
     (** Result of solving for the current set of clauses *)
 
+  (* main solver state *)
+  type t = {
+    si: Solver_internal.t;
+    solver: Sat_solver.t;
+    mutable last_res: res option;
+    stat: Stat.t;
+    proof: P.t;
+    count_clause: int Stat.counter;
+    count_solve: int Stat.counter;
+    (* config: Config.t *)
+  }
+  type solver = t
+
+  (** {2 Main} *)
+
+  let add_theory_p (type a) (self:t) (th:a theory_p) : a =
+    let (module Th) = th in
+    Log.debugf 2
+      (fun k-> k "(@[smt-solver.add-theory@ :name %S@])" Th.name);
+    let st = Th.create_and_setup self.si in
+    (* add push/pop to the internal solver *)
+    begin
+      let open Solver_internal in
+      self.si.th_states <- Ths_cons {
+          st;
+          push_level=Th.push_level;
+          pop_levels=Th.pop_levels;
+          next=self.si.th_states;
+        };
+    end;
+    st
+
+  let add_theory (self:t) (th:theory) : unit =
+    let (module Th) = th in
+    ignore (add_theory_p self (module Th))
+
+  let add_theory_l self = List.iter (add_theory self)
+
+  (* create a new solver *)
+  let create ?(stat=Stat.global) ?size ~proof ~theories tst ty_st () : t =
+    Log.debug 5 "smt-solver.create";
+    let si = Solver_internal.create ~stat ~proof tst ty_st () in
+    let self = {
+      si; proof; last_res=None;
+      solver=Sat_solver.create ~proof ?size ~stat si;
+      stat;
+      count_clause=Stat.mk_int stat "solver.add-clause";
+      count_solve=Stat.mk_int stat "solver.solve";
+    } in
+    add_theory_l self theories;
+    (* assert [true] and [not false] *)
+    begin
+      let tst = Solver_internal.tst self.si in
+      let t_true = Term.bool tst true in
+      Sat_solver.add_clause self.solver
+        [Lit.atom tst t_true]
+        (P.lemma_true t_true self.proof)
+    end;
+    self
+
+  let[@inline] solver self = self.solver
+  let[@inline] cc self = Solver_internal.cc self.si
+  let[@inline] stats self = self.stat
+  let[@inline] tst self = Solver_internal.tst self.si
+  let[@inline] ty_st self = Solver_internal.ty_st self.si
+  let[@inline] proof self = self.si.proof
+  let[@inline] last_res self = self.last_res
+  let[@inline] registry self = Solver_internal.registry self.si
+
+  let reset_last_res_ self = self.last_res <- None
+
+  let preprocess_acts_of_solver_
+      (self:t) : (module Solver_internal.PREPROCESS_ACTS) =
+    (module struct
+      let proof = self.proof
+      let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.si.tst t
+      let mk_lit ?sign t = Lit.atom ?sign self.si.tst t, None
+      let add_lit ?default_pol lit =
+        Sat_solver.add_lit self.solver ?default_pol lit
+      let add_clause c pr =
+        Sat_solver.add_clause self.solver c pr
+    end)
+
+  (* preprocess literal *)
+  let preprocess_lit_ ~steps (self:t) (lit:lit) : lit =
+    let pacts = preprocess_acts_of_solver_ self in
+    Solver_internal.preprocess_lit_ ~steps self.si pacts lit
+
+  (* preprocess clause, return new proof *)
+  let preprocess_clause_ (self:t)
+      (c:lit IArray.t) (pr:proof_step) : lit IArray.t * proof_step =
+    let steps = ref [] in
+    let c = IArray.map (preprocess_lit_ self ~steps) c in
+    let pr =
+      P.lemma_rw_clause pr
+        ~res:(IArray.to_iter c) ~using:(Iter.of_list !steps) self.proof
+    in
+    c, pr
+
+  (* make a literal from a term, ensuring it is properly preprocessed *)
+  let mk_lit_t (self:t) ?sign (t:term) : lit =
+    let pacts = preprocess_acts_of_solver_ self in
+    Solver_internal.mk_plit self.si pacts ?sign t
+
   (** {2 Main} *)
 
   let pp_stats out (self:t) : unit =
@@ -845,6 +849,7 @@ module Make(A : ARG)
   (* add [c], without preprocessing its literals *)
   let add_clause_nopreproc_ (self:t) (c:lit IArray.t) (proof:proof_step) : unit =
     Stat.incr self.count_clause;
+    reset_last_res_ self;
     Log.debugf 50 (fun k->
         k "(@[solver.add-clause@ %a@])"
           (Util.pp_iarray Lit.pp) c);
@@ -944,42 +949,51 @@ module Make(A : ARG)
     in
     self.si.on_progress <- on_progress;
 
-    match
-      Stat.incr self.count_solve;
-      Sat_solver.solve ~on_progress ~assumptions (solver self)
-    with
-    | Sat_solver.Sat _ when not self.si.complete ->
-      Log.debugf 1
-        (fun k->k "(@[sidekick.smt-solver: SAT@ actual: UNKNOWN@ :reason incomplete-fragment@])");
-      Unknown Unknown.U_incomplete
+    let res =
+      match
+        Stat.incr self.count_solve;
+        Sat_solver.solve ~on_progress ~assumptions (solver self)
+      with
+      | Sat_solver.Sat _ when not self.si.complete ->
+        Log.debugf 1
+          (fun k->k "(@[sidekick.smt-solver: SAT@ actual: UNKNOWN@ :reason incomplete-fragment@])");
+        Unknown Unknown.U_incomplete
 
-    | Sat_solver.Sat (module SAT) ->
-      Log.debug 1 "(sidekick.smt-solver: SAT)";
+      | Sat_solver.Sat (module SAT) ->
+        Log.debug 1 "(sidekick.smt-solver: SAT)";
 
-      Log.debugf 50
-        (fun k->
-           let ppc out n =
-             Fmt.fprintf out "{@[<hv>class@ %a@]}" (Util.pp_iter N.pp) (N.iter_class n) in
-           k "(@[sidekick.smt-solver.classes@ (@[%a@])@])"
-            (Util.pp_iter ppc) (CC.all_classes @@ Solver_internal.cc self.si));
+        Log.debugf 50
+          (fun k->
+             let ppc out n =
+               Fmt.fprintf out "{@[<hv>class@ %a@]}" (Util.pp_iter N.pp) (N.iter_class n) in
+             k "(@[sidekick.smt-solver.classes@ (@[%a@])@])"
+              (Util.pp_iter ppc) (CC.all_classes @@ Solver_internal.cc self.si));
 
-      let _lits f = SAT.iter_trail f in
-      let m = mk_model self _lits in
-      (* TODO: check model *)
-      let _ = check in
+        let _lits f = SAT.iter_trail f in
+        let m = mk_model self _lits in
+        (* TODO: check model *)
+        let _ = check in
 
-      do_on_exit ();
-      Sat m
+        do_on_exit ();
+        Sat m
 
-    | Sat_solver.Unsat (module UNSAT) ->
-      let unsat_core () = UNSAT.unsat_assumptions () in
-      let unsat_proof_step () = Some (UNSAT.unsat_proof()) in
-      do_on_exit ();
-      Unsat {unsat_core; unsat_proof_step}
-    | exception Should_stop -> Unknown Unknown.U_asked_to_stop
+      | Sat_solver.Unsat (module UNSAT) ->
+        let unsat_core () = UNSAT.unsat_assumptions () in
+        let unsat_proof_step () = Some (UNSAT.unsat_proof()) in
+        do_on_exit ();
+        Unsat {unsat_core; unsat_proof_step}
+      | exception Should_stop -> Unknown Unknown.U_asked_to_stop
+    in
+    self.last_res <- Some res;
+    res
 
-  let push_assumption self a = Sat_solver.push_assumption self.solver a
-  let pop_assumptions self n = Sat_solver.pop_assumptions self.solver n
+  let push_assumption self a =
+    reset_last_res_ self;
+    Sat_solver.push_assumption self.solver a
+
+  let pop_assumptions self n =
+    reset_last_res_ self;
+    Sat_solver.pop_assumptions self.solver n
 
   type propagation_result =
     | PR_sat
@@ -991,6 +1005,7 @@ module Make(A : ARG)
       }
 
   let check_sat_propagations_only ~assumptions self : propagation_result =
+    reset_last_res_ self;
     match
       Sat_solver.check_sat_propagations_only ~assumptions self.solver
     with

src/smtlib/Process.ml

@@ -147,7 +147,7 @@ let solve
     ?(check=false)
     ?time:_ ?memory:_ ?(progress=false)
     ~assumptions
-    s : unit =
+    s : Solver.res =
   let t1 = Sys.time() in
   let on_progress =
     if progress then Some (mk_progress s) else None in
@@ -208,7 +208,8 @@ let solve
 
     | Solver.Unknown reas ->
       Format.printf "Unknown (:reason %a)" Solver.Unknown.pp reas
-  end
+  end;
+  res
 
 let known_logics = [
   "QF_UF";
@@ -260,11 +261,11 @@ let process_stmt
           (fun (sign,t) -> Solver.mk_lit_t solver ~sign t)
           l
       in
-      solve
+      ignore (solve
         ?gc ?restarts ~check ?pp_model ?proof_file
         ?time ?memory ?progress
         ~assumptions
-        solver;
+        solver : Solver.res);
       E.return()
     | Statement.Stmt_ty_decl (id,n) ->
       decl_sort id n;
@@ -300,6 +301,29 @@ let process_stmt
       Solver.add_clause solver (IArray.of_list c) pr;
       E.return()
 
+    | Statement.Stmt_get_model ->
+      begin match Solver.last_res solver with
+        | Some (Solver.Sat m) ->
+          Fmt.printf "(@[model@ %a@])@." Solver.Model.pp m
+        | _ -> Error.errorf "cannot access model"
+      end;
+      E.return ()
+
+    | Statement.Stmt_get_value l ->
+      begin match Solver.last_res solver with
+        | Some (Solver.Sat m) ->
+          let l = List.map
+              (fun t -> match Solver.Model.eval m t with
+                 | None -> Error.errorf "cannot evaluate %a" Term.pp t
+                 | Some u -> t, u)
+              l
+          in
+          let pp_pair out (t,u) = Fmt.fprintf out "(@[%a@ %a@])" Term.pp t Term.pp u in
+          Fmt.printf "(@[%a@])@." (Util.pp_list pp_pair) l
+        | _ -> Error.errorf "cannot access model"
+      end;
+      E.return ()
+
     | Statement.Stmt_data _ ->
       E.return()
     | Statement.Stmt_define _ ->

src/smtlib/Typecheck.ml

@@ -573,10 +573,13 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list =
         l
     in
     [Stmt.Stmt_check_sat l]
+  | PA.Stmt_get_model -> [Stmt.Stmt_get_model]
+  | PA.Stmt_get_value l ->
+    let l = List.map (conv_term ctx) l in
+    [Stmt.Stmt_get_value l]
   | PA.Stmt_get_assertions
   | PA.Stmt_get_option _
   | PA.Stmt_get_info _
-  | PA.Stmt_get_model
   | PA.Stmt_get_proof
   | PA.Stmt_get_unsat_core
   | PA.Stmt_get_unsat_assumptions
@@ -585,7 +588,6 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list =
   | PA.Stmt_reset_assertions
   | PA.Stmt_push _
   | PA.Stmt_pop _
-  | PA.Stmt_get_value _
     ->
     (* TODO: handle more of these *)
     errorf_ctx ctx "cannot handle statement %a" PA.pp_stmt stmt