From eb40cfa5e362840c8dcaca8581c7eaca2ba314eb Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 9 May 2018 18:14:06 -0500 Subject: [PATCH] wip --- src/main/main.ml | 4 +- src/sat/Internal.ml | 92 +++++++++++++++++++++++++---------------- src/sat/Solver.ml | 2 +- src/smt/Ast.ml | 4 +- src/smt/Ast.mli | 1 + src/smt/Solver_types.ml | 2 +- src/smt/Term.ml | 2 +- src/smt/Term.mli | 2 +- src/smt/Term_cell.ml | 2 +- src/smt/Term_cell.mli | 2 +- 10 files changed, 69 insertions(+), 44 deletions(-) diff --git a/src/main/main.ml b/src/main/main.ml index 1fe66323..22a21ef5 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -135,7 +135,9 @@ let main () = Dagon_smtlib.parse !file | Dimacs -> Dagon_dimacs.parse !file >|= fun cs -> - List.map (fun c -> Ast.Assert_bool c) cs + List.rev_append + (List.rev_map (fun c -> Ast.Assert_bool c) cs) + [Ast.CheckSat] end >>= fun input -> (* process statements *) diff --git a/src/sat/Internal.ml b/src/sat/Internal.ml index f7975411..c3b23f17 100644 --- a/src/sat/Internal.ml +++ b/src/sat/Internal.ml @@ -113,6 +113,10 @@ module Make mutable clause_incr : float; (* increment for clauses' activity *) + to_add : (bool * clause) CCVector.vector; + (* clauses to add, from the user *) + + (* TODO: remove *) mutable dirty: bool; (* is there a [pop()] on top of the stack for examining current model/proof? *) @@ -140,6 +144,7 @@ module Make user_levels = Vec.make 0 (-1); order = H.create(); + to_add = CCVector.create(); var_incr = 1.; clause_incr = 1.; @@ -323,7 +328,8 @@ module Make ) ) in - partition_aux [] [] [] [] 0 + try partition_aux [] [] [] [] 0 + with Trivial -> Array.to_list atoms, [] (* Making a decision. @@ -435,9 +441,8 @@ module Make be able to build a correct proof at the end of proof search. *) let simpl_reason : reason -> reason = function | (Bcp cl) as r -> - let l, history = partition cl.atoms in - begin match l with - | [_] -> + begin match partition cl.atoms with + | [_] as l, history -> if history = [] then ( (* no simplification has been done, so [cl] is actually a clause with only [a], so it is a valid reason for propagating [a]. *) @@ -453,7 +458,7 @@ module Make Clause.debug cl Clause.debug c'); Bcp c' ) - | _ -> + | l, _history -> Log.debugf 1 (fun k -> k "@[Failed at reason simplification:@,%a@,%a@]" @@ -461,6 +466,7 @@ module Make (Vec.from_list l Atom.dummy) Clause.debug cl); assert false + | exception Trivial -> r end | r -> r @@ -820,6 +826,9 @@ module Make ) ) + let[@inline] add_clause_user ~permanent st (c:clause): unit = + CCVector.push st.to_add (permanent,c) + type watch_res = | Watch_kept | Watch_removed @@ -1092,39 +1101,49 @@ module Make if is_unsat st then raise Unsat; let n_of_conflicts = ref (to_float restart_first) in let n_of_learnts = ref ((to_float (nb_clauses st)) *. learntsize_factor) in - try - while true do - begin - try - search st (to_int !n_of_conflicts) (to_int !n_of_learnts) - with - | Restart -> - n_of_conflicts := !n_of_conflicts *. restart_inc; - n_of_learnts := !n_of_learnts *. learntsize_inc - | Sat -> - assert (st.elt_head = Vec.size st.trail); - pp_trail st; - begin match Th.if_sat (theory st) (full_slice st) with - | Theory_intf.Sat -> - (* if no propagation is to be done, exit; - otherwise continue loop *) - if propagation_fixpoint st then ( - raise Sat - ) - | Theory_intf.Unsat (l, p) -> - let atoms = List.rev_map (new_atom ~permanent:false st) l in - let c = Clause.make_l atoms (Lemma p) in - Log.debugf 3 - (fun k -> k "(@[@{sat.theory_conflict_clause@}@ %a@])" Clause.debug c); - (* must backtrack *) - (* TODO: assert that this is indeed a conflict, - then call [add_boolean_conflict st c] *) - add_clause ~permanent:false st c - end; + (* add clauses that are waiting in [to_add] *) + let rec add_clauses () = + match + CCVector.filter' (fun (permanent,c) -> add_clause ~permanent st c; false) st.to_add + with + | () -> call_solve() + | exception Conflict c -> + add_boolean_conflict st c; + call_solve() + and call_solve() = + match search st (to_int !n_of_conflicts) (to_int !n_of_learnts) with + | () -> () + | exception Restart -> + n_of_conflicts := !n_of_conflicts *. restart_inc; + n_of_learnts := !n_of_learnts *. learntsize_inc + | exception Conflict c -> + add_boolean_conflict st c; + call_solve() + | exception Sat -> + assert (st.elt_head = Vec.size st.trail); + pp_trail st; + begin match Th.if_sat (theory st) (full_slice st) with + | Theory_intf.Sat -> + (* if no propagation is to be done, exit; + otherwise continue loop *) + if propagation_fixpoint st then ( + raise Sat + ) + | Theory_intf.Unsat (l, p) -> + let atoms = List.rev_map (new_atom ~permanent:false st) l in + let c = Clause.make_l atoms (Lemma p) in + Log.debugf 3 + (fun k -> k "(@[@{sat.theory_conflict_clause@}@ %a@])" Clause.debug c); + (* must backtrack *) + (* TODO: assert that this is indeed a conflict, + then call [add_boolean_conflict st c] *) + add_clause ~permanent:false st c end - done + in + try add_clauses() with Sat -> () + (* TODO: merge with add_clause_user *) let assume ~permanent st ?tag cnf = let cs = List.rev_map (fun atoms -> @@ -1143,12 +1162,13 @@ module Make then redo_down_to_level_0 st add_clauses else add_clauses() + (* TODO: remove push/pop *) (* create a factice decision level for local assumptions *) let push st : unit = Log.debug 5 "(sat.push-new-user-level)"; cancel_until st (base_level st); Log.debugf 5 - (fun k -> k "(@[sat.status@ :trail %d - %d@ %a@]" + (fun k -> k "(@[sat.status@ :trail %d - %d@ %a@])" st.elt_head st.th_head (Vec.print ~sep:"" Atom.debug) st.trail); begin match propagate st with | Some confl -> diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 8521302c..b25f2688 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -88,7 +88,7 @@ module Make let[@inline] add_clause ~permanent st c : unit = cleanup_ st; - S.add_clause ~permanent st c + S.add_clause_user ~permanent st c let solve (st:t) ?(assumptions=[]) () = cleanup_ st; diff --git a/src/smt/Ast.ml b/src/smt/Ast.ml index 26840918..a0cbe71a 100644 --- a/src/smt/Ast.ml +++ b/src/smt/Ast.ml @@ -161,6 +161,7 @@ type statement = | Decl of ID.t * Ty.t | Define of definition list | Assert of term + | Assert_bool of int list | Goal of var list * term | CheckSat | Exit @@ -437,6 +438,7 @@ let pp_statement out = function Fmt.fprintf out "(@[<1>declare-fun@ %a (@[%a@])@ %a@])" ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret | Assert t -> Fmt.fprintf out "(@[assert@ %a@])" pp_term t + | Assert_bool l -> Fmt.fprintf out "(@[assert-bool@ %a@])" (Util.pp_list Fmt.int) l | Goal (vars,g) -> Fmt.fprintf out "(@[assert-not@ %a@])" pp_term (forall_l vars (not_ g)) | Exit -> Fmt.string out "(exit)" @@ -480,7 +482,7 @@ let env_add_statement env st = List.fold_left (fun map (id,ty,def) -> add_def id (E_defined (ty,def)) map) env l - | Goal _ | Assert _ | CheckSat | Exit + | Goal _ | Assert _ | Assert_bool _ | CheckSat | Exit | SetLogic _ | SetOption _ | SetInfo _ -> env diff --git a/src/smt/Ast.mli b/src/smt/Ast.mli index 2abd401f..4eb14b9d 100644 --- a/src/smt/Ast.mli +++ b/src/smt/Ast.mli @@ -129,6 +129,7 @@ type statement = | Decl of ID.t * Ty.t | Define of definition list | Assert of term + | Assert_bool of int list | Goal of var list * term | CheckSat | Exit diff --git a/src/smt/Solver_types.ml b/src/smt/Solver_types.ml index 75a9ac69..3c0459f8 100644 --- a/src/smt/Solver_types.ml +++ b/src/smt/Solver_types.ml @@ -54,7 +54,7 @@ and term_view_tc = { tc_t_is_semantic : 'a. 'a term_view_custom -> bool; (* is this a semantic term? semantic terms must be solvable *) tc_t_solve: cc_node term_view_custom -> cc_node term_view_custom -> solve_result; (* solve an equation between classes *) tc_t_sub : 'a. 'a term_view_custom -> 'a Sequence.t; (* iter on immediate subterms *) - tc_t_abs : 'a. self:'a -> 'a term_view_custom -> 'a * bool; (* remove the sign? *) + tc_t_abs : self:term -> term term_view_custom -> term * bool; (* remove the sign? *) tc_t_relevant : 'a. 'a term_view_custom -> 'a Sequence.t; (* iter on relevant immediate subterms *) tc_t_subst : 'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom option; (* substitute immediate subterms and canonize *) tc_t_explain : 'a. 'a CCEqual.t -> 'a term_view_custom -> 'a term_view_custom -> ('a * 'a) list; diff --git a/src/smt/Term.ml b/src/smt/Term.ml index 02e623cc..39fe2bef 100644 --- a/src/smt/Term.ml +++ b/src/smt/Term.ml @@ -24,7 +24,7 @@ type tc = Solver_types.term_view_tc = { tc_t_is_semantic : 'a. 'a custom -> bool; tc_t_solve : cc_node custom -> cc_node custom -> solve_result; tc_t_sub : 'a. 'a custom -> 'a Sequence.t; - tc_t_abs : 'a. self:'a -> 'a custom -> 'a * bool; + tc_t_abs : self:term -> term custom -> term * bool; tc_t_relevant : 'a. 'a custom -> 'a Sequence.t; tc_t_subst : 'a 'b. ('a -> 'b) -> 'a custom -> 'b custom option; tc_t_explain : 'a. 'a CCEqual.t -> 'a custom -> 'a custom -> ('a * 'a) list; diff --git a/src/smt/Term.mli b/src/smt/Term.mli index 904372e2..01f9c124 100644 --- a/src/smt/Term.mli +++ b/src/smt/Term.mli @@ -24,7 +24,7 @@ type tc = Solver_types.term_view_tc = { tc_t_is_semantic : 'a. 'a custom -> bool; tc_t_solve : cc_node custom -> cc_node custom -> solve_result; tc_t_sub : 'a. 'a custom -> 'a Sequence.t; - tc_t_abs : 'a. self:'a -> 'a custom -> 'a * bool; + tc_t_abs : self:term -> term custom -> term * bool; tc_t_relevant : 'a. 'a custom -> 'a Sequence.t; tc_t_subst : 'a 'b. ('a -> 'b) -> 'a custom -> 'b custom option; tc_t_explain : 'a. 'a CCEqual.t -> 'a custom -> 'a custom -> ('a * 'a) list; diff --git a/src/smt/Term_cell.ml b/src/smt/Term_cell.ml index 6a312761..3a14203d 100644 --- a/src/smt/Term_cell.ml +++ b/src/smt/Term_cell.ml @@ -23,7 +23,7 @@ type tc = Solver_types.term_view_tc = { tc_t_is_semantic : 'a. 'a term_view_custom -> bool; tc_t_solve : cc_node term_view_custom -> cc_node term_view_custom -> solve_result; tc_t_sub : 'a. 'a term_view_custom -> 'a Sequence.t; - tc_t_abs : 'a. self:'a -> 'a custom -> 'a * bool; + tc_t_abs : self:term -> term custom -> term * bool; tc_t_relevant : 'a. 'a term_view_custom -> 'a Sequence.t; tc_t_subst : 'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom option; diff --git a/src/smt/Term_cell.mli b/src/smt/Term_cell.mli index 99fdfe90..f25967da 100644 --- a/src/smt/Term_cell.mli +++ b/src/smt/Term_cell.mli @@ -21,7 +21,7 @@ type tc = Solver_types.term_view_tc = { tc_t_is_semantic : 'a. 'a term_view_custom -> bool; tc_t_solve : cc_node term_view_custom -> cc_node term_view_custom -> solve_result; tc_t_sub : 'a. 'a term_view_custom -> 'a Sequence.t; - tc_t_abs : 'a. self:'a -> 'a custom -> 'a * bool; + tc_t_abs : self:term -> term custom -> term * bool; tc_t_relevant : 'a. 'a term_view_custom -> 'a Sequence.t; tc_t_subst : 'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom option;