simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 11:45:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(smt): ability for a theory to declare we're in incomplete fragment

Browse source
This commit is contained in:
Simon Cruanes 2022-01-10 16:50:55 -05:00
parent af8ab338e6
commit f7195bf980
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/core/Sidekick_core.ml
View file

@ -990,6 +990,11 @@ module type SOLVER_INTERNAL = sig
is given the whole trail.
*)
val declare_pb_is_incomplete : t -> unit
(** Declare that, in some theory, the problem is outside the logic fragment
that is decidable (e.g. if we meet proper NIA formulas).
The solver will not reply "SAT" from now on. *)
(** {3 Model production} *)
type model_hook =

8
src/smt-solver/Sidekick_smt_solver.ml
View file

@ -262,6 +262,7 @@ module Make(A : ARG)
mutable on_partial_check: (t -> theory_actions -> lit Iter.t -> unit) list;
mutable on_final_check: (t -> theory_actions -> lit Iter.t -> unit) list;
mutable level: int;
mutable complete: bool;
}
and preprocess_hook =
@ -633,6 +634,12 @@ module Make(A : ARG)
let[@inline] final_check (self:t) (acts:_ Sidekick_sat.acts) : unit =
check_ ~final:true self acts
let declare_pb_is_incomplete self =
if self.complete then (
Log.debug 1 "(solver.declare-pb-is-incomplete)";
);
self.complete <- false
let create ~stat ~proof (tst:Term.store) (ty_st:Ty.store) () : t =
let rec self = {
tst;
@ -658,6 +665,7 @@ module Make(A : ARG)
on_partial_check=[];
on_final_check=[];
level=0;
complete=true;
} in
ignore (Lazy.force @@ self.cc : CC.t);
self