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

detail

Browse source
This commit is contained in:
Simon Cruanes 2021-09-13 06:46:54 -04:00
parent b108d9f3df
commit 45de142b22
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/th-dyn-trans/Sidekick_th_dyn_trans.ml
View file

@ -133,9 +133,6 @@ module Make(A: ARG)
let emit_proof = A.proof_trans c in let emit_proof = A.proof_trans c in
CC.add_clause ~pool:self.cpool cc c emit_proof) CC.add_clause ~pool:self.cpool cc c emit_proof)
end; end;
(* TODO: find some potential dyn-trans axioms; add them to self.sat
if they're not in done_inst *)
() ()
let on_conflict (self:t) (cc:CC.t) ~th lits : unit = let on_conflict (self:t) (cc:CC.t) ~th lits : unit =