(proof-new) Add proof-new to options file (#4641)

Adds proof-new as an option. This is required for adding code that is guarded by this option while we are in the process of merging work on the new proofs infrastructure.

Enabling the option currently throws an option exception.

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 449c0c31ecc1785055f5b180d3290d1c4edd8391..303448d1be512d994cc70659654e356b569f55b5 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -164,6 +164,23 @@ header = "options/smt_options.h"
   read_only  = true
   help       = "output proofs after every UNSAT/VALID response"
 
+[[option]]
+  name       = "proofNew"
+  category   = "regular"
+  long       = "proof-new"
+  type       = "bool"
+  default    = "false"
+  help       = "do proof production using the new infrastructure"
+
+[[option]]
+  name       = "proofNewPedantic"
+  category   = "regular"
+  long       = "proof-new-pedantic"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "assertion failure for any incorrect rule application or untrusted lemma for fully supported portions with proof-new"
+
 [[option]]
   name       = "dumpInstantiations"
   category   = "regular"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index e3b1163fce9ac5e27cfd2129dd061acc7f8ca22b..23ae65044b365fc803b3b3bfe12d16e47d95066b 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -266,6 +266,11 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
                    << std::endl;
     }
   }
+  // !!!!!!!!!!!!!!!! temporary, to support CI check for old proof system
+  if (options::proof())
+  {
+    options::proofNew.set(false);
+  }
 
   // sygus inference may require datatypes
   if (!smte.isInternalSubsolver())
@@ -877,6 +882,16 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   }
   if (options::ufHo())
   {
+    // if higher-order, disable proof production
+    if (options::proofNew())
+    {
+      if (options::proofNew.wasSetByUser())
+      {
+        Warning() << "SmtEngine: turning off proof production (not yet "
+                     "supported with --uf-ho)\n";
+      }
+      options::proofNew.set(false);
+    }
     // if higher-order, then current variants of model-based instantiation
     // cannot be used
     if (options::mbqiMode() != options::MbqiMode::NONE)
@@ -1108,6 +1123,16 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     {
       options::cegqiPreRegInst.set(true);
     }
+    // not compatible with proofs
+    if (options::proofNew())
+    {
+      if (options::proofNew.wasSetByUser())
+      {
+        Notice() << "SmtEngine: setting proof-new to false to support SyGuS"
+                 << std::endl;
+      }
+      options::proofNew.set(false);
+    }
   }
   // counterexample-guided instantiation for non-sygus
   // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
@@ -1464,6 +1489,11 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
         "division. "
         "Try --bv-div-zero-const to interpret division by zero as a constant.");
   }
+  // !!!!!!!!!!!!!!!! temporary, until proof-new is functional
+  if (options::proofNew())
+  {
+    throw OptionException("--proof-new is not yet supported.");
+  }
 }
 
 }  // namespace smt