From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 17 Mar 2021 20:45:26 +0000 (-0500)
Subject: (proof-new) Fixes to set defaults (#6163)
X-Git-Tag: cvc5-1.0.0~2060
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a3e250159a0179c61965f4c9f059f99758f79e8e;p=cvc5.git

(proof-new) Fixes to set defaults (#6163)

This copies most of the remaining changes to set_defaults.cpp from proof-new.

In particular, it recognizes when proofs must be disabled.

This is required to fix the regressions (locally) and the nightlies.
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 761ff8701..535c14560 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -27,6 +27,7 @@
 #include "options/open_ostream.h"
 #include "options/option_exception.h"
 #include "options/printer_options.h"
+#include "options/proof_options.h"
 #include "options/prop_options.h"
 #include "options/quantifiers_options.h"
 #include "options/sep_options.h"
@@ -89,7 +90,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     options::bitvectorAlgebraicSolver.set(true);
   }
 
-  bool is_sygus = language::isInputLangSygus(options::inputLanguage());
+  bool isSygus = language::isInputLangSygus(options::inputLanguage());
+  bool usesSygus = isSygus;
 
   if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
@@ -263,6 +265,20 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     // Note we allow E-matching by default to support combinations of sequences
     // and quantifiers.
   }
+  // whether we must disable proofs
+  bool disableProofs = false;
+  if (options::globalNegate())
+  {
+    // When global negate answers "unsat", it is not due to showing a set of
+    // formulas is unsat. Thus, proofs do not apply.
+    disableProofs = true;
+  }
+  // !!! must disable proofs if using the old unsat core infrastructure
+  // TODO (#project 37) remove this
+  if (options::unsatCores() && !options::checkUnsatCoresNew())
+  {
+    disableProofs = true;
+  }
 
   if (options::arraysExp())
   {
@@ -285,21 +301,44 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::produceAbducts()
         || options::produceInterpols() != options::ProduceInterpols::NONE
-        || options::sygusInference() || options::sygusRewSynthInput()
-        || options::sygusInst())
+        || options::sygusInference() || options::sygusRewSynthInput())
     {
       // since we are trying to recast as sygus, we assume the input is sygus
-      is_sygus = true;
+      isSygus = true;
+      usesSygus = true;
+    }
+    else if (options::sygusInst())
+    {
+      // sygus instantiation uses sygus, but it is not a sygus problem
+      usesSygus = true;
     }
   }
 
-  // We now know whether the input is sygus. Update the logic to incorporate
+  // We now know whether the input uses sygus. Update the logic to incorporate
   // the theories we need internally for handling sygus problems.
-  if (is_sygus)
+  if (usesSygus)
   {
     logic = logic.getUnlockedCopy();
     logic.enableSygus();
     logic.lock();
+    if (isSygus)
+    {
+      // When sygus answers "unsat", it is not due to showing a set of
+      // formulas is unsat in the standard way. Thus, proofs do not apply.
+      disableProofs = true;
+    }
+  }
+
+  // if we requiring disabling proofs, disable them now
+  if (disableProofs && options::produceProofs())
+  {
+    if (options::produceProofs())
+    {
+      Notice() << "SmtEngine: turning off produce-proofs." << std::endl;
+    }
+    options::produceProofs.set(false);
+    options::checkProofs.set(false);
+    options::proofEagerChecking.set(false);
   }
 
   // sygus core connective requires unsat cores
@@ -547,7 +586,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // cases where we need produce models
   if (!options::produceModels()
       && (options::produceAssignments() || options::sygusRewSynthCheck()
-          || is_sygus))
+          || usesSygus))
   {
     Notice() << "SmtEngine: turning on produce-models" << std::endl;
     options::produceModels.set(true);
@@ -798,9 +837,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (!options::decisionMode.wasSetByUser())
   {
     options::DecisionMode decMode =
-        // sygus uses internal
-        is_sygus ? options::DecisionMode::INTERNAL :
-                 // ALL
+        // anything that uses sygus uses internal
+        usesSygus ? options::DecisionMode::INTERNAL :
+                  // ALL
             logic.hasEverything()
                 ? options::DecisionMode::JUSTIFICATION
                 : (  // QF_BV
@@ -961,7 +1000,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
   // apply sygus options
   // if we are attempting to rewrite everything to SyGuS, use sygus()
-  if (is_sygus)
+  if (usesSygus)
   {
     if (!options::sygus())
     {