~cypheon/kicad2spice

bc76afef93e72f7d317c3420fb27c6393dadd1e6 — Johann Rudloff 1 year, 10 months ago 9502f7f master
Use labelled assertions to get a REALLY useful unsat-core.
1 files changed, 3 insertions(+), 3 deletions(-)

M test/nlcompare.ml
M test/nlcompare.ml => test/nlcompare.ml +3 -3
@@ 12,12 12,12 @@ module StrSet = Set.Make(String)
let curry f = fun (a,b) -> f a b

let write_smtlib_comparison write nl_a nl_b =
  write "(set-option :produce-proofs true)\n(declare-sort Net)\n";
  write "(set-option :produce-unsat-cores true)\n(set-option :produce-proofs true)\n(declare-sort Net)\n";
  let write_asserts nl nlname1 nlname2 =
    let prefix1 = nlname1 ^ "__" in
    let prefix2 = nlname2 ^ "__" in
    let write_generic_device name nets = List.iteri (fun i _ ->
      write (Printf.sprintf "(assert (= %scomp_%s_pin_%d %scomp_%s_pin_%d))\n" prefix1 name i prefix2 name i)
      write (Printf.sprintf "(assert (! (= %scomp_%s_pin_%d %scomp_%s_pin_%d) :named comp_%s_pin_%d_match))\n" prefix1 name i prefix2 name i name i)
    ) nets in
    let write_device name = let open Device in function
      | Resistor c -> write_generic_device name [c.net_neg;c.net_pos]


@@ 61,7 61,7 @@ let write_smtlib_comparison write nl_a nl_b =
  write_netlist nl_a "a";
  write_netlist nl_b "b";
  write_asserts nl_a "a" "b";
  write "(check-sat)\n(get-model)\n(get-proof)\n"
  write "(check-sat)\n(get-unsat-core)\n;(get-model)\n;(get-proof)\n"


let test () =