Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.

* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line

1 files changed, 43 insertions, 5 deletions

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 2ff857a2f..8a3cec494 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -241,6 +241,7 @@ function handle_option {
   predicates=
   links=
   links_alternate=
+  smt_links=
 
   options_already_documented=false
   alternate_options_already_documented=false
@@ -412,10 +413,28 @@ function handle_option {
            links_alternate="${links_alternate} $(echo "${args[$i]}" | sed 's,[^/]*/,,')"
          else
            links="${links} ${args[$i]}"
-           links_alternate="${links_alternate} ${args[$i]}"
          fi
        done
        ;;
+    :link-smt)
+       j=0
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
+         let ++i
+         let ++j
+         if [ $j -eq 3 ]; then
+           echo "$kf:$lineno: error: attribute :link-smt can only take two arguments" >&2
+           exit 1
+         fi
+         if expr "${args[$i]}" : '.*/' &>/dev/null; then
+           echo "$kf:$lineno: error: attribute :link-smt cannot take alternates" >&2
+           exit 1
+         fi
+         smt_links="${smt_links} ${args[$i]}"
+       done
+       if [ $j -eq 1 ]; then
+         smt_links="${smt_links} \"true\""
+       fi
+       ;;
     :include)
        while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
          let ++i
@@ -544,14 +563,33 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
   fi
   run_links=
   run_links_alternate=
+  run_smt_links=
+  if [ -n "$links" -a -z "$smt_links" -a -n "$smtname" ]; then
+    echo "$kf:$lineno: warning: $smtname has no :link-smt, but equivalent command-line has :link" >&2
+  elif [ -n "$smt_links" -a -z "$links" ] && [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o "$long_option_alternate" ]; then
+    echo "$kf:$lineno: warning: $smtname has a :link-smt, but equivalent command-line has no :link" >&2
+  fi
   if [ -n "$links" ]; then
+    # command-line links
     for link in $links; do
       run_links="$run_links
 #line $lineno \"$kf\"
       preemptGetopt(extra_argc, extra_argv, \"$link\");"
     done
   fi
+  if [ -n "$smt_links" ]; then
+    # smt links
+    smt_links=($smt_links)
+    i=0
+    while [ $i -lt ${#smt_links[@]} ]; do
+      run_smt_links="$run_smt_links
+#line $lineno \"$kf\"
+    smt->setOption(std::string(\"${smt_links[$i]}\"), SExpr(${smt_links[$(($i+1))]}));"
+      i=$((i+2))
+    done
+  fi
   if [ -n "$links_alternate" ]; then
+    # command-line links
     for link in $links_alternate; do
       run_links_alternate="$run_links_alternate
 #line $lineno \"$kf\"
@@ -732,7 +770,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_links
+    Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_smt_links
     return;
   }"
     elif [ -n "$expect_arg" -a "$internal" != - ]; then
@@ -749,7 +787,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_links
+    Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_smt_links
     return;
   }"
     elif [ -n "$expect_arg" ]; then
@@ -764,7 +802,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    $run_handlers$run_links
+    $run_handlers$run_smt_links
     return;
   }"
     else
@@ -779,7 +817,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    $run_handlers$run_links
+    $run_handlers$run_smt_links
     return;
   }"
     fi