From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 27 Apr 2022 19:12:07 +0000 (-0500)
Subject: Add option to apply constant propagation for all learned literals (#8668)
X-Git-Tag: cvc5-1.0.1~214
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c938a904ea20f8511ae3344a9e9246a792d01a2d;p=cvc5.git

Add option to apply constant propagation for all learned literals (#8668)

Adds `--simplification-bcp`, disabled by default.
---

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 7aaf05f93..b24e48644 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -25,6 +25,14 @@ name   = "SMT Layer"
   name = "batch"
   help = "Save up all ASSERTions; run nonclausal simplification and clausal (MiniSat) propagation for all of them only after reaching a querying command (CHECKSAT or QUERY or predicate SUBTYPE declaration)."
 
+[[option]]
+  name       = "simplificationBoolConstProp"
+  category   = "expert"
+  long       = "simplification-bcp"
+  type       = "bool"
+  default    = "false"
+  help       = "apply Boolean constant propagation as a substituion during simplification"
+
 [[option]]
   name       = "doStaticLearning"
   category   = "regular"
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 72d2d8947..cca0f72b9 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -116,6 +116,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       << "Iterate through " << propagator->getLearnedLiterals().size()
       << " learned literals." << std::endl;
   // No conflict, go through the literals and solve them
+  NodeManager* nm = NodeManager::currentNM();
   context::Context* u = userContext();
   Rewriter* rw = d_env.getRewriter();
   TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions();
@@ -173,7 +174,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
         Trace("non-clausal-simplify")
             << "conflict with " << learned_literals[i].getNode() << std::endl;
         assertionsToPreprocess->clear();
-        Node n = NodeManager::currentNM()->mkConst<bool>(false);
+        Node n = nm->mkConst<bool>(false);
         assertionsToPreprocess->push_back(n, false, false, d_llpg.get());
         return PreprocessingPassResult::CONFLICT;
       }
@@ -206,17 +207,17 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
         Trace("non-clausal-simplify")
             << "conflict while solving " << learnedLiteral << std::endl;
         assertionsToPreprocess->clear();
-        Node n = NodeManager::currentNM()->mkConst<bool>(false);
+        Node n = nm->mkConst<bool>(false);
         assertionsToPreprocess->push_back(n);
         return PreprocessingPassResult::CONFLICT;
       }
       default:
+        TNode t;
+        TNode c;
         if (learnedLiteral.getKind() == kind::EQUAL
             && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst()))
         {
           // constant propagation
-          TNode t;
-          TNode c;
           if (learnedLiteral[0].isConst())
           {
             t = learnedLiteral[1];
@@ -227,6 +228,18 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
             t = learnedLiteral[0];
             c = learnedLiteral[1];
           }
+        }
+        else if (options().smt.simplificationBoolConstProp)
+        {
+          // From non-equalities, learn the Boolean equality. Notice that
+          // the equality case above is strictly more powerful that this, since
+          // e.g. (= t c) * { t -> c } also simplifies to true.
+          bool pol = learnedLiteral.getKind() != kind::NOT;
+          c = nm->mkConst(pol);
+          t = pol ? learnedLiteral : learnedLiteral[0];
+        }
+        if (!t.isNull())
+        {
           Assert(!t.isConst());
           Assert(rewrite(cps.apply(t)) == t);
           Assert(top_level_substs.apply(t) == t);
@@ -244,7 +257,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
         }
         else
         {
-          // Keep the literal
+          // Keep the learned literal
           learned_literals[j++] = learned_literals[i];
         }
         // Its a literal that could not be processed as a substitution or
@@ -400,7 +413,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   if (!learnedLitsToConjoin.empty())
   {
     size_t replIndex = assertionsToPreprocess->getRealAssertionsEnd() - 1;
-    Node newConj = NodeManager::currentNM()->mkAnd(learnedLitsToConjoin);
+    Node newConj = nm->mkAnd(learnedLitsToConjoin);
     Trace("non-clausal-simplify")
         << "non-clausal simplification, reassert: " << newConj << std::endl;
     ProofGenerator* pg = nullptr;
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 9acdec976..e28459708 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -380,6 +380,18 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
       throw OptionException(ss.str());
     }
   }
+  // check if we have separation logic heap types
+  if (d_env.hasSepHeap())
+  {
+    std::stringstream reasonNoSepLogic;
+    if (incompatibleWithSeparationLogic(opts, reasonNoSepLogic))
+    {
+      std::stringstream ss;
+      ss << reasonNoSepLogic.str()
+         << " not supported when using separation logic.";
+      throw OptionException(ss.str());
+    }
+  }
 }
 
 void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
@@ -1274,6 +1286,22 @@ bool SetDefaults::incompatibleWithQuantifiers(Options& opts,
   return false;
 }
 
+bool SetDefaults::incompatibleWithSeparationLogic(Options& opts,
+                                                  std::ostream& reason) const
+{
+  if (options().smt.simplificationBoolConstProp)
+  {
+    // Spatial formulas in separation logic have a semantics that depends on
+    // their position in the AST (e.g. their nesting beneath separation
+    // conjunctions). Thus, we cannot apply BCP as a substitution for spatial
+    // predicates to the input formula. We disable this option altogether to
+    // ensure this is the case
+    notifyModifyOption("simplification-bcp", "false", "separation logic");
+    options().smt.simplificationBoolConstProp = false;
+  }
+  return false;
+}
+
 void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const
 {
   bool needsUf = false;
diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index 671af8e7e..cee7dd3ab 100644
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -111,6 +111,13 @@ class SetDefaults : protected EnvObj
    * The output stream reason is similar to above.
    */
   bool incompatibleWithQuantifiers(Options& opts, std::ostream& reason) const;
+  /**
+   * Check if incompatible with separation logic. Notice this method may
+   * modify the options to ensure that we are compatible with separation logic.
+   * The output stream reason is similar to above.
+   */
+  bool incompatibleWithSeparationLogic(Options& opts,
+                                       std::ostream& reason) const;
   //------------------------- options setting, prior finalization of logic
   /**
    * Set defaults pre, which sets all options prior to finalizing the logic.