print lemmas and instantiations as implications

HanielB · Mar 22, 2024 · d2acf40 · d2acf40
1 parent f7740c9
commit d2acf40
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 5 deletions.
diff --git a/src/parser/commands.cpp b/src/parser/commands.cpp
@@ -2137,13 +2137,18 @@ void GetHintsCommand::printResult(cvc5::Solver* solver, std::ostream& out) const
   //   - lemmas
   //   - instantiation
   //   - (rewrite rule + instances)*
+  bool first = true;
   for (size_t i = 0, size = d_result.size(); i < size; ++i)
   {
-    out << (i == 0   ? "Preprocess:"
-            : i == 1 ? "Theory lemmas:"
-            : i == 2 ? "Instantiations:"
-                     : "rewrites:")
+    out << (i == 0
+                ? "Preprocess:"
+                : i == 1 ? "\nTheory lemmas:"
+                         : i == 2 ? "\nInstantiations:"
+                                  : (first ? "\nRewrites (rules and their usages "
+                                             "in quantifier-free terms):"
+                                           : "Rewrites:"))
         << "\n";
+    first = i <= 2;
     for (const auto& l : d_result[i])
     {
       out << "\t" << l << "\n";

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
@@ -1790,6 +1790,30 @@ std::vector<Node> SolverEngine::getHints()
     r = SkolemManager::getOriginalForm(r);
     Trace("hints") << "\t" << r << "\n";
     Trace("hints-proofs") << "\t\t" << *p.get() << "\n";
+    // r will be a disjunction. If there is a positive atom and all others
+    // negatives, turn it into an implication
+    if (r.getKind() == Kind::OR)
+    {
+      std::vector<Node> negLits;
+      std::copy_if(r.begin(), r.end(), std::back_inserter(negLits), [](Node n) {
+        return n.getKind() == Kind::NOT;
+      });
+      if (negLits.size() == r.getNumChildren() - 1)
+      {
+        Node conc;
+        for (const Node& rc : r)
+        {
+          if (std::find(negLits.begin(), negLits.end(), rc) == negLits.end())
+          {
+            conc = rc;
+            break;
+          }
+        }
+        Assert(!conc.isNull());
+        currResults.push_back(nm->mkNode(Kind::IMPLIES, nm->mkAnd(negLits), conc));
+        continue;
+      }
+    }
     currResults.push_back(r);
   }
   result.push_back(nm->mkNode(Kind::SEXPR, currResults));
@@ -1806,7 +1830,7 @@ std::vector<Node> SolverEngine::getHints()
       r = SkolemManager::getOriginalForm(r);
       Trace("hints") << "\t" << r << "\n";
       Trace("hints-proofs") << "\t\t" << *p.get() << "\n";
-      currResults.push_back(r);
+      currResults.push_back(nm->mkNode(Kind::IMPLIES, r[0][0], r[1]));
     }
   }
   result.push_back(nm->mkNode(Kind::SEXPR, currResults));