From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 22 Jun 2020 17:23:36 +0000 (-0500)
Subject: (proof-new) Add proof-new to options file (#4641)
X-Git-Tag: cvc5-1.0.0~3184
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d85e90bfcc0bebe52b2da0bad638bc2fe9ef50b0;p=cvc5.git

(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 449c0c31e..303448d1b 100644
--- 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 e3b1163fc..23ae65044 100644
--- 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