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

fix: typo in Th_bool

Browse source
This commit is contained in:
Simon Cruanes 2018-06-16 20:47:23 -05:00
parent 1f79809644
commit c8ca60461a
3 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/Model.ml
View file

@ -144,7 +144,6 @@ let eval (m:t) (t:Term.t) : Value.t option =
| Some v -> v | Some v -> v
end end
| exception Not_found -> | exception Not_found ->
Log.debugf 5 (fun k->k "(@[model.eval.undef@ %a@])" Term.pp t);
raise No_value (* no particular interpretation *) raise No_value (* no particular interpretation *)
end end
end end

5
src/smt/th_bool/Sidekick_th_bool.ml
View file

@ -13,9 +13,6 @@ type term = Term.t
(* TODO: Tseitin on the fly when a composite boolean term is asserted. (* TODO: Tseitin on the fly when a composite boolean term is asserted.
--> maybe, cache the clause inside the literal *) --> maybe, cache the clause inside the literal *)
(* TODO: in theory (or terms?) have a way to evaluate custom terms
(like formulas) in a given model, for checking models *)
let id_not = ID.make "not" let id_not = ID.make "not"
let id_and = ID.make "and" let id_and = ID.make "and"
let id_or = ID.make "or" let id_or = ID.make "or"
@ -127,7 +124,7 @@ let and_l st l =
| args -> Term.app_cst st C.and_ (IArray.of_list args) | args -> Term.app_cst st C.and_ (IArray.of_list args)
let or_l st l = let or_l st l =
match flatten_id id_and l with match flatten_id id_or l with
| [] -> Term.false_ st | [] -> Term.false_ st
| l when List.exists Term.is_true l -> Term.true_ st | l when List.exists Term.is_true l -> Term.true_ st
| [x] -> x | [x] -> x

3
src/smtlib/Process.ml
View file

@ -237,6 +237,9 @@ let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : un
if (is_true || is_false) && ((b && is_false) || (not b && is_true)) then ( if (is_true || is_false) && ((b && is_false) || (not b && is_true)) then (
Error.errorf "(@[check-model.error@ :atom %a@ :model-val %B@ :sat-val %B@])" Error.errorf "(@[check-model.error@ :atom %a@ :model-val %B@ :sat-val %B@])"
S.Atom.pp a b (if is_true then true else not is_false) S.Atom.pp a b (if is_true then true else not is_false)
) else (
Log.debugf 5
(fun k->k "(@[check-model@ :atom %a@ :model-val %B@ :no-sat-val@])" S.Atom.pp a b);
) )
| Some v -> | Some v ->
Error.errorf "(@[check-model.error@ :atom %a@ :non-bool-value %a@])" Error.errorf "(@[check-model.error@ :atom %a@ :non-bool-value %a@])"