simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 13:14:09 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

api: sat_state takes formulas, not atoms

Browse source
This commit is contained in:
Simon Cruanes 2019-01-28 19:00:10 -06:00 • committed by Guillaume Bury
parent a58c940c6d
commit 1736b4a99e
3 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/core/Internal.ml
View file

@ -1990,7 +1990,7 @@ module Make(Plugin : PLUGIN)
(* Result type *) (* Result type *)
type res = type res =
| Sat of (term,atom,value) Solver_intf.sat_state | Sat of (term,Formula.t,value) Solver_intf.sat_state
| Unsat of (atom,clause,Proof.t) Solver_intf.unsat_state | Unsat of (atom,clause,Proof.t) Solver_intf.unsat_state
let pp_all st lvl status = let pp_all st lvl status =
@ -2004,19 +2004,19 @@ module Make(Plugin : PLUGIN)
(Vec.pp ~sep:"" Clause.debug) (history st) (Vec.pp ~sep:"" Clause.debug) (history st)
) )
let mk_sat (st:t) : _ Solver_intf.sat_state = let mk_sat (st:t) : (Term.t, Formula.t, _) Solver_intf.sat_state =
pp_all st 99 "SAT"; pp_all st 99 "SAT";
let t = trail st in let t = trail st in
let iter f f' = let iter_trail f f' =
Vec.iter (function Vec.iter (function
| Atom a -> f a | Atom a -> f (Atom.formula a)
| Lit l -> f' l.term) | Lit l -> f' l.term)
t t
in in
let[@inline] eval f = eval st (mk_atom st f) in
let[@inline] eval_level f = eval_level st (mk_atom st f) in
{ Solver_intf. { Solver_intf.
eval = eval st; eval; eval_level; iter_trail;
eval_level = eval_level st;
iter_trail = iter;
model = (fun () -> model st); model = (fun () -> model st);
} }
@ -2061,7 +2061,7 @@ module Make(Plugin : PLUGIN)
let c = Clause.make c Hyp in let c = Clause.make c Hyp in
add_clause_ st c add_clause_ st c
let solve (st:t) ?(assumptions=[]) () = let solve (st:t) ?(assumptions=[]) () : res =
cancel_until st 0; cancel_until st 0;
Vec.clear st.assumptions; Vec.clear st.assumptions;
List.iter (Vec.push st.assumptions) assumptions; List.iter (Vec.push st.assumptions) assumptions;

2
src/core/Solver_intf.ml
View file

@ -414,7 +414,7 @@ module type S = sig
(** Result type for the solver *) (** Result type for the solver *)
type res = type res =
| Sat of (term,atom,Value.t) sat_state (** Returned when the solver reaches SAT, with a model *) | Sat of (term,formula,Value.t) sat_state (** Returned when the solver reaches SAT, with a model *)
| Unsat of (atom,clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) | Unsat of (atom,clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
exception UndecidedLit exception UndecidedLit

2
src/main/main.ml
View file

@ -29,7 +29,7 @@ module Process = struct
let check_clause c = let check_clause c =
let l = List.map (function a -> let l = List.map (function a ->
Log.debugf 99 Log.debugf 99
(fun k -> k "Checking value of %a" S.Atom.pp a); (fun k -> k "Checking value of %a" S.Formula.pp a);
sat.Msat.eval a) c in sat.Msat.eval a) c in
List.exists (fun x -> x) l List.exists (fun x -> x) l
in in