From c2d379de108e1e3bf4e0f251e39879d396a545c5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 6 Mar 2014 10:53:56 +0100 Subject: [PATCH] fix Tseitin CNF conversion; more combinators to build formulas; Smt.eval function to extract the propositional model --- Makefile.in | 4 ++ smt/smt.ml | 109 +++++++++++++++++++++++++++++++++++++------------ smt/smt.mli | 29 ++++++++++++- smt/solver.ml | 5 ++- smt/solver.mli | 1 + tests/eval.ml | 32 +++++++++++++++ 6 files changed, 152 insertions(+), 28 deletions(-) create mode 100644 tests/eval.ml diff --git a/Makefile.in b/Makefile.in index d445df88..2548b3a6 100644 --- a/Makefile.in +++ b/Makefile.in @@ -158,12 +158,16 @@ ocamlfind-remove: doc: smt/smt.mli mkdir -p $(doc) ocamldoc -html -d doc/ -I smt -I common smt/smt.mli + ####### +test: + ocamlfind ocamlopt -package num,unix -linkpkg aez.cmxa tests/eval.ml -o tests/eval.native clean:: @rm -f *.cm[itox] *.cmti *.o *~ *.annot @rm -f common/*.cm[itox] common/*.cmti common/*.o common/*~ common/*.annot @rm -f smt/*.cm[itox] smt/*.cmti smt/*.o smt/*~ smt/*.annot + @rm -f tests/*.cm[itox] tests/*.cmti tests/*.o tests/*~ tests/*.annot @rm -f $(GENERATED) *.output @rm -f $(NAME).byte $(NAME).opt diff --git a/smt/smt.ml b/smt/smt.ml index 4476257c..cb259921 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -320,6 +320,20 @@ and Formula : sig val make : combinator -> t list -> t val make_cnf : t -> Literal.LT.t list list + val make_pred : ?sign:bool -> Term.t -> t + val make_not : t -> t + val make_and : t list -> t + val make_or : t list -> t + val make_imply : t -> t -> t + val make_equiv : t -> t -> t + val make_xor : t -> t -> t + val make_eq : Term.t -> Term.t -> t + val make_neq : Term.t -> Term.t -> t + val make_le : Term.t -> Term.t -> t + val make_lt : Term.t -> Term.t -> t + val make_ge : Term.t -> Term.t -> t + val make_gt : Term.t -> Term.t -> t + val print_list : string -> Format.formatter -> t list -> unit val print : Format.formatter -> t -> unit @@ -388,7 +402,7 @@ end Literal.Eq (t1, t2) | Neq, ts -> let ts = - List.map (function Term.T x -> x | _ -> assert false) ts in + List.rev_map (function Term.T x -> x | _ -> assert false) ts in Literal.Distinct (false, ts) | Le, [Term.T t1; Term.T t2] -> Literal.Builtin (true, Hstring.make "<=", [t1; t2]) @@ -401,25 +415,48 @@ end let make_lit op l = lift_ite [] op l + let make_pred ?(sign=true) p = + if sign + then make_lit Eq [p; Term.t_true] + else make_lit Eq [p; Term.t_false] + + let make_eq t1 t2 = make_lit Eq [t1; t2] + let make_neq t1 t2 = make_lit Neq [t1; t2] + let make_le t1 t2 = make_lit Le [t1; t2] + let make_lt t1 t2 = make_lit Lt [t1; t2] + let make_ge t1 t2 = make_lit Le [t2; t1] + let make_gt t1 t2 = make_lit Lt [t2; t1] + let make_not f = make Not [f] + let make_and l = make And l + let make_imply f1 f2 = make Imp [f1; f2] + let make_equiv f1 f2 = make And [ make_imply f1 f2; make_imply f2 f1] + let make_xor f1 f2 = make Or [ make And [ make Not [f1]; f2 ]; + make And [ f1; make Not [f2] ] ] + + (* simplify formula *) let rec sform = function | Comb (Not, [Lit a]) -> Lit (Literal.LT.neg a) | Comb (Not, [Comb (Not, [f])]) -> sform f | Comb (Not, [Comb (Or, l)]) -> - let nl = List.map (fun a -> sform (Comb (Not, [a]))) l in + let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in Comb (And, nl) | Comb (Not, [Comb (And, l)]) -> - let nl = List.map (fun a -> sform (Comb (Not, [a]))) l in + let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in Comb (Or, nl) | Comb (Not, [Comb (Imp, [f1; f2])]) -> Comb (And, [sform f1; sform (Comb (Not, [f2]))]) | Comb (And, l) -> - Comb (And, List.map sform l) + Comb (And, List.rev_map sform l) | Comb (Or, l) -> - Comb (Or, List.map sform l) + Comb (Or, List.rev_map sform l) | Comb (Imp, [f1; f2]) -> Comb (Or, [sform (Comb (Not, [f1])); sform f2]) - | Comb (Imp, _) -> assert false - | f -> f + | Comb ((Imp | Not), _) -> assert false + | Lit _ as f -> f + + + let ( @@ ) l1 l2 = List.rev_append l1 l2 + let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *) let make_or = function | [] -> assert false @@ -430,11 +467,11 @@ end let l = if l_or = [] then l_and else - List.map + List.rev_map (fun x -> match x with | Lit _ -> Comb (Or, x::l_or) - | Comb (Or, l) -> Comb (Or, l@l_or) + | Comb (Or, l) -> Comb (Or, l @@ l_or) | _ -> assert false ) l_and in @@ -442,13 +479,13 @@ end let rec flatten_or = function | [] -> [] - | Comb (Or, l)::r -> l@(flatten_or r) + | Comb (Or, l)::r -> l @@ (flatten_or r) | Lit a :: r -> (Lit a)::(flatten_or r) | _ -> assert false let rec flatten_and = function | [] -> [] - | Comb (And, l)::r -> l@(flatten_and r) + | Comb (And, l)::r -> l @@ (flatten_and r) | a :: r -> a::(flatten_and r) @@ -456,7 +493,7 @@ end match f with | Comb (Or, l) -> begin - let l = List.map cnf l in + let l = List.rev_map cnf l in let l_and, l_or = List.partition (function Comb(And,_) -> true | _ -> false) l in match l_and with @@ -477,12 +514,9 @@ end end end | Comb (And, l) -> - Comb (And, List.map cnf l) + Comb (And, List.rev_map cnf l) | f -> f - - let ( @@ ) l1 l2 = List.rev_append l1 l2 - let rec mk_cnf = function | Comb (And, l) -> List.fold_left (fun acc f -> (mk_cnf f) @@ acc) [] l @@ -537,6 +571,9 @@ end let acc_or = ref [] let acc_and = ref [] + (* build a clause by flattening (if sub-formulas have the + same combinator) and proxy-ing sub-formulas that have the + opposite operator. *) let rec cnf f = match f with | Lit a -> None, [a] | Comb (Not, [Lit a]) -> None, [Literal.LT.neg a] @@ -546,9 +583,9 @@ end (fun (_, acc) f -> match cnf f with | _, [] -> assert false - | cmb, [a] -> cmb, a :: acc + | cmb, [a] -> Some And, a :: acc | Some And, l -> - Some And, l @ acc + Some And, l @@ acc (* let proxy = mk_proxy () in *) (* acc_and := (proxy, l) :: !acc_and; *) (* proxy :: acc *) @@ -556,6 +593,7 @@ end let proxy = mk_proxy () in acc_or := (proxy, l) :: !acc_or; Some And, proxy :: acc + | None, l -> Some And, l @@ acc | _ -> assert false ) (None, []) l @@ -564,9 +602,9 @@ end (fun (_, acc) f -> match cnf f with | _, [] -> assert false - | cmb, [a] -> cmb, a :: acc + | cmb, [a] -> Some Or, a :: acc | Some Or, l -> - Some Or, l @ acc + Some Or, l @@ acc (* let proxy = mk_proxy () in *) (* acc_or := (proxy, l) :: !acc_or; *) (* proxy :: acc *) @@ -574,6 +612,7 @@ end let proxy = mk_proxy () in acc_and := (proxy, l) :: !acc_and; Some Or, proxy :: acc + | None, l -> Some Or, l @@ acc | _ -> assert false ) (None, []) l @@ -585,11 +624,15 @@ end | _ -> [snd (cnf f)] in let proxies = ref [] in + (* encore clauses that make proxies in !acc_and equivalent to + their clause *) let acc = List.fold_left (fun acc (p,l) -> proxies := p :: !proxies; let np = Literal.LT.neg p in + (* build clause [cl = l1 & l2 & ... & ln => p] where [l = [l1;l2;..]] + also add clauses [p => l1], [p => l2], etc. *) let cl, acc = List.fold_left (fun (cl,acc) a -> (Literal.LT.neg a :: cl), [np; a] :: acc) @@ -597,10 +640,14 @@ end cl :: acc )acc !acc_and in + (* encore clauses that make proxies in !acc_or equivalent to + their clause *) let acc = List.fold_left (fun acc (p,l) -> proxies := p :: !proxies; + (* add clause [p => l1 | l2 | ... | ln], and add clauses + [l1 => p], [l2 => p], etc. *) let acc = List.fold_left (fun acc a -> [p; Literal.LT.neg a]::acc) acc l in (Literal.LT.neg p :: l) :: acc @@ -612,11 +659,11 @@ end acc_or := []; acc_and := []; cnf (sform f) - - (* Naive CNF *) - let make_cnf f = mk_cnf (sform f) end + (* Naive CNF XXX remove??? + let make_cnf f = mk_cnf (sform f) + *) end exception Unsat of int list @@ -633,6 +680,8 @@ module type Solver = sig val assume : ?profiling:bool -> id:int -> Formula.t -> unit val check : ?profiling:bool -> unit -> unit + + val eval : Term.t -> bool val save_state : unit -> state val restore_state : state -> unit val entails : ?profiling:bool -> id:int -> Formula.t -> bool @@ -656,7 +705,7 @@ module Make (Dummy : sig end) = struct List.iter (fun c -> eprintf "%a@." (Formula.print_list "or") - (List.map (fun x -> Formula.Lit x) c)) uc; + (List.rev_map (fun x -> Formula.Lit x) c)) uc; eprintf "@."; try clear (); @@ -671,7 +720,7 @@ module Make (Dummy : sig end) = struct assert false let export_unsatcore cl = - let uc = List.map (fun {Solver_types.atoms=atoms} -> + let uc = List.rev_map (fun {Solver_types.atoms=atoms} -> let l = ref [] in for i = 0 to Vec.size atoms - 1 do l := (Vec.get atoms i).Solver_types.lit :: !l @@ -711,9 +760,17 @@ module Make (Dummy : sig end) = struct | Solver.Unsat ex -> if profiling then Time.pause (); raise (Unsat (export_unsatcore2 ex)) - + type state = CSolver.state + let eval t = + match t with + | Term.T t' -> + let lit = Literal.LT.mk_pred t' in + CSolver.eval lit + | Term.Tite _ -> + failwith "cannot evaluate \"if-then-else\" term" + let save_state = CSolver.save let restore_state = CSolver.restore diff --git a/smt/smt.mli b/smt/smt.mli index b01c3b77..2920a1ef 100644 --- a/smt/smt.mli +++ b/smt/smt.mli @@ -217,6 +217,23 @@ and Formula : sig (** [make cmb [f_1; ...; f_n]] creates the formula [(f_1 ... f_n)].*) + val make_pred : ?sign:bool -> Term.t -> t + (** [make_pred p] builds the atomic formula [p = true]. + @param sign the polarity of the atomic formula *) + + val make_not : t -> t + val make_and : t list -> t + val make_or : t list -> t + val make_imply : t -> t -> t + val make_equiv : t -> t -> t + val make_xor : t -> t -> t + val make_eq : Term.t -> Term.t -> t + val make_neq : Term.t -> Term.t -> t + val make_le : Term.t -> Term.t -> t + val make_lt : Term.t -> Term.t -> t + val make_ge : Term.t -> Term.t -> t + val make_gt : Term.t -> Term.t -> t + val make_cnf : t -> Literal.LT.t list list (** [make_cnf f] returns a conjunctive normal form of [f] under the form: a list (which is a conjunction) of lists (which are disjunctions) of @@ -273,7 +290,7 @@ module type Solver = sig val assume : ?profiling:bool -> id:int -> Formula.t -> unit (** [assume ~profiling:b f id] adds the formula [f] to the context of the - solver with idetifier [id]. + solver with identifier [id]. This function only performs unit propagation. @param profiling if set to [true] then profiling information (time) will @@ -293,6 +310,16 @@ module type Solver = sig [id_1, ..., id_n] is the unsat core (returned as the identifiers of the formulas given to the solver). *) + val eval : Term.t -> bool + (** [eval lit] returns the current truth value for the literal. The term + must be a boolean proposition that occurred in the problem, + because the only information returned by [eval] is its boolean + truth value in the current model (no theories!). + + @raise Invalid_argument if the context is not checked or if it's + unsatisfiable. + @raise Error if the term isn't a known propositional atom. *) + val save_state : unit -> state (** [save_state ()] returns a {b copy} of the current state of the solver.*) diff --git a/smt/solver.ml b/smt/solver.ml index 22f519ce..7481ff3e 100644 --- a/smt/solver.ml +++ b/smt/solver.ml @@ -1026,5 +1026,8 @@ let restore { env = s_env; st_cpt_mk_var = st_cpt_mk_var; st_ma = st_ma } = Solver_types.cpt_mk_var := st_cpt_mk_var; Solver_types.ma := st_ma - + let eval lit = + let var, negated = make_var lit in + let truth = var.pa.is_true in + if negated then not truth else truth end diff --git a/smt/solver.mli b/smt/solver.mli index 6e988d80..096192eb 100644 --- a/smt/solver.mli +++ b/smt/solver.mli @@ -21,6 +21,7 @@ module Make (Dummy : sig end) : sig val assume : Literal.LT.t list list -> cnumber : int -> unit val clear : unit -> unit + val eval : Literal.LT.t -> bool val save : unit -> state val restore : state -> unit diff --git a/tests/eval.ml b/tests/eval.ml new file mode 100644 index 00000000..5e8676ca --- /dev/null +++ b/tests/eval.ml @@ -0,0 +1,32 @@ +(** Random tests *) + +open Aez + +let hs = Hstring.make + +module S = Smt.Make(struct end) + +let ty = Smt.Type.type_proc;; (hs "tau");; +Smt.Symbol.declare (hs "a") [] ty;; +Smt.Symbol.declare (hs "b") [] ty;; +Smt.Symbol.declare (hs "c") [] ty;; + +let a = Smt.Term.make_app (hs "a") [];; +let b = Smt.Term.make_app (hs "b") [];; +let c = Smt.Term.make_app (hs "c") [];; + +S.assume ~id:0 Smt.Formula.(make_imply (make_pred ~sign:false a) (make_pred b));; +S.assume ~id:1 Smt.Formula.(make_imply (make_pred b) (make_pred c));; +S.assume ~id:2 Smt.Formula.(make_not (make_pred c));; + +try + S.check (); + Printf.printf "problem is sat, checking model...\n"; + let v_a = S.eval a in + let v_b = S.eval b in + let v_c = S.eval c in + Printf.printf "a=%B, b=%B, c=%B\n" v_a v_b v_c; + assert (v_a && not v_b && not v_c); + () +with Smt.Unsat l -> + Printf.printf "problem deemed unsat, shouldn't be\n"