fix Tseitin CNF conversion;

more combinators to build formulas;
Smt.eval function to extract the propositional model

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
 

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
+    | Comb ((Imp | Not), _) -> assert false
-    | f -> f
+    | 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

smt/smt.mli

@@ -217,6 +217,23 @@ and Formula : sig
   (** [make cmb [f_1; ...; f_n]] creates the formula
       [(f_1 <cmb> ... <cmb> 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.*)
 

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

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
 

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"