glift: Add `-create-imprecise` command, rename other commands, and re-work the help text.

9 files changed, 13 insertions, 12 deletions

diff --git a/examples/smtbmc/glift/C7552.ys b/examples/smtbmc/glift/C7552.ys
index 0b39fadc7..139b0df43 100644
--- a/examples/smtbmc/glift/C7552.ys
+++ b/examples/smtbmc/glift/C7552.ys
@@ -2,7 +2,7 @@ read_verilog C7552.v
 techmap
 flatten
 select C7552_lev2
-glift -optimize-precise
+glift -create-sketch
 techmap
 opt
 rename C7552_lev2 uut
diff --git a/examples/smtbmc/glift/C880.ys b/examples/smtbmc/glift/C880.ys
index fe2678088..93f929c89 100644
--- a/examples/smtbmc/glift/C880.ys
+++ b/examples/smtbmc/glift/C880.ys
@@ -2,7 +2,7 @@ read_verilog C880.v
 techmap
 flatten
 select C880_lev2
-glift -optimize-precise
+glift -create-sketch
 techmap
 opt
 rename C880_lev2 uut
diff --git a/examples/smtbmc/glift/alu2.ys b/examples/smtbmc/glift/alu2.ys
index b0d7b3164..72cdaceba 100644
--- a/examples/smtbmc/glift/alu2.ys
+++ b/examples/smtbmc/glift/alu2.ys
@@ -2,7 +2,7 @@ read_verilog alu2.v
 techmap
 flatten
 select alu2_lev2
-glift -optimize-precise
+glift -create-sketch
 techmap
 opt
 rename alu2_lev2 uut
diff --git a/examples/smtbmc/glift/alu4.ys b/examples/smtbmc/glift/alu4.ys
index d5ab7fb3b..b4337e699 100644
--- a/examples/smtbmc/glift/alu4.ys
+++ b/examples/smtbmc/glift/alu4.ys
@@ -2,7 +2,7 @@ read_verilog alu4.v
 techmap
 flatten
 select alu4_lev2
-glift -optimize-precise
+glift -create-sketch
 techmap
 opt
 rename alu4_lev2 uut
diff --git a/examples/smtbmc/glift/mux2.ys b/examples/smtbmc/glift/mux2.ys
index 6b2b98c89..c6670d741 100644
--- a/examples/smtbmc/glift/mux2.ys
+++ b/examples/smtbmc/glift/mux2.ys
@@ -18,18 +18,19 @@ module mux2(a, b, s, y);
 endmodule
 EOT
 techmap
-copy mux2 uut
 copy mux2 spec
+copy mux2 uut
+copy mux2 solved
 delete mux2
-glift -optimize-precise uut
 glift -create-precise spec
+glift -create-sketch uut
+glift -create-sketch -no-cost-model solved
 design -push-copy
 miter -equiv spec uut qbfmiter
 flatten
-delete spec uut
+delete spec uut solved
 qbfsat -assume-outputs -assume-negative-polarity -write-solution mux2.soln qbfmiter
 design -pop
-copy uut solved
 qbfsat -specialize-from-file mux2.soln solved
 opt
 miter -equiv spec solved proofmiter
diff --git a/examples/smtbmc/glift/t481.ys b/examples/smtbmc/glift/t481.ys
index 2f54ed252..249a9eb71 100644
--- a/examples/smtbmc/glift/t481.ys
+++ b/examples/smtbmc/glift/t481.ys
@@ -2,7 +2,7 @@ read_verilog t481.v
 techmap
 flatten
 select t481_lev2
-glift -optimize-precise
+glift -create-sketch
 techmap
 opt
 rename t481_lev2 uut
diff --git a/examples/smtbmc/glift/too_large.ys b/examples/smtbmc/glift/too_large.ys
index e14c2b7b6..2bb6105ea 100644
--- a/examples/smtbmc/glift/too_large.ys
+++ b/examples/smtbmc/glift/too_large.ys
@@ -2,7 +2,7 @@ read_verilog too_large.v
 techmap
 flatten
 select too_large_lev2
-glift -optimize-precise
+glift -create-sketch
 techmap
 opt
 rename too_large_lev2 uut
diff --git a/examples/smtbmc/glift/ttt2.ys b/examples/smtbmc/glift/ttt2.ys
index 8c649e642..62054a86c 100644
--- a/examples/smtbmc/glift/ttt2.ys
+++ b/examples/smtbmc/glift/ttt2.ys
@@ -2,7 +2,7 @@ read_verilog ttt2.v
 techmap
 flatten
 select ttt2_lev2
-glift -optimize-precise
+glift -create-sketch
 techmap
 opt
 rename ttt2_lev2 uut
diff --git a/examples/smtbmc/glift/x1.ys b/examples/smtbmc/glift/x1.ys
index c5b4797d3..b010fe9ee 100644
--- a/examples/smtbmc/glift/x1.ys
+++ b/examples/smtbmc/glift/x1.ys
@@ -2,7 +2,7 @@ read_verilog x1.v
 techmap
 flatten
 select x1_lev2
-glift -optimize-precise
+glift -create-sketch
 techmap
 opt
 rename x1_lev2 uut