[proof] ITE translation fix (#3484)

* Bugfix: convert ifte arms to formulas for printing

We have two kinds of ITEs in our LFSC proofs:
   * ite: for sort-typed expressions
   * ifte: for formulas
Say that we have a Bool-sorted ITE. We had machinery for emitting an
`ifte` for it, but this machinery didn't actually convert the arms of
the ITE into formulas... Facepalm.

Fixed now.

* Test the lifting of ITEs from arithmetic.

This test verifies that booleans ITEs are correctly lifted to formula
ITEs in LRA proofs.

It used to fail, but now passes.

* clang-format

* Typos.

* Add test to CMake

* Set --check-proofs in test

* Address Yoni

* Expand printsAsBool documentation
* Assert ITE typing soundness

* Assert a subtype relation for ITEs, not equality

* Update src/proof/arith_proof.h

Thanks Yoni!

Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 77f4b1630a3cbd4ce5e7dd8eaad0f2a100dc883e..ba38a314c51d93ec1464dba3ecec1ca93abb6d50 100644 (file)
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -1193,4 +1193,11 @@ void LFSCArithProof::printAliasingDeclarations(std::ostream& os, std::ostream& p
   // Nothing to do here at this point.
 }
 
+bool LFSCArithProof::printsAsBool(const Node& n)
+{
+  // Our boolean variables and constants print as sort Bool.
+  // All complex booleans print as formulas.
+  return n.getType().isBoolean() and (n.isVar() or n.isConst());
+}
+
 } /* CVC4  namespace */

diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index a1df24fac7d9be9ff8a2610285e8748b36a1ea09..c70754a1f18e5c154b95ae91ba6cb36c988af03e 100644 (file)
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -167,6 +167,11 @@ public:
   void printAliasingDeclarations(std::ostream& os,
                                  std::ostream& paren,
                                  const ProofLetMap& globalLetMap) override;
+
+  /**
+   * Return whether this node, when serialized to LFSC, has sort `Bool`. Otherwise, the sort is `formula`.
+   */
+  bool printsAsBool(const Node& n) override;
 };
 
 

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index d95572820c2346ecd787e140c86b0f78a1cd93ca..eee75e6126fbf8b0413e160935c22d602882b7c0 100644 (file)
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -872,6 +872,23 @@ void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const Pr
   printTheoryTerm(term, os, map);
 }
 
+void LFSCTheoryProofEngine::printBoundFormula(Expr term,
+                                              std::ostream& os,
+                                              const ProofLetMap& map)
+{
+  Assert(term.getType().isBoolean() or term.getType().isPredicate());
+  bool wrapWithBoolToPred = term.getType().isBoolean() and printsAsBool(term);
+  if (wrapWithBoolToPred)
+  {
+    os << "(p_app ";
+  }
+  printBoundTerm(term, os, map);
+  if (wrapWithBoolToPred)
+  {
+    os << ")";
+  }
+}
+
 void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   if (term.isVariable()) {
     os << ProofManager::sanitize(term);
@@ -882,17 +899,30 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
 
   switch(k) {
   case kind::ITE: {
-    os << (term.getType().isBoolean() ? "(ifte ": "(ite _ ");
-
-    bool booleanCase = term[0].getType().isBoolean();
-    if (booleanCase && printsAsBool(term[0])) os << "(p_app ";
-    printBoundTerm(term[0], os, map);
-    if (booleanCase && printsAsBool(term[0])) os << ")";
+    bool useFormulaType = term.getType().isBoolean();
+    Assert(term[1].getType().isSubtypeOf(term.getType()));
+    Assert(term[2].getType().isSubtypeOf(term.getType()));
+    os << (useFormulaType ? "(ifte " : "(ite _ ");
 
+    printBoundFormula(term[0], os, map);
     os << " ";
-    printBoundTerm(term[1], os, map);
+    if (useFormulaType)
+    {
+      printBoundFormula(term[1], os, map);
+    }
+    else
+    {
+      printBoundTerm(term[1], os, map);
+    }
     os << " ";
-    printBoundTerm(term[2], os, map);
+    if (useFormulaType)
+    {
+      printBoundFormula(term[2], os, map);
+    }
+    else
+    {
+      printBoundTerm(term[2], os, map);
+    }
     os << ")";
     return;
   }

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index b487b62a8b4ef71020e2afa2421f462c77c3f36c..577f0c03226935bf17af65184fd914c9878f61eb 100644 (file)
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -197,6 +197,11 @@ public:
 private:
   static void dumpTheoryLemmas(const IdToSatClause& lemmas);
 
+  // Prints this boolean term as a formula.
+  // If necessary, it prints a wrapper converting a `Bool`-sorted term to a
+  // formula.
+  void printBoundFormula(Expr term, std::ostream& os, const ProofLetMap& map);
+
   // TODO: this function should be moved into the BV prover.
 
   std::map<Node, std::string> d_assertionToRewrite;
@@ -353,7 +358,14 @@ protected:
    */
   virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
 
-  // Return true if node prints as bool, false if it prints as a formula.
+  /**
+   * Return whether this node, when serialized as an LFSC proof, has sort `Bool`.
+   *
+   * This is virtual because it ultimately, theories control the serialization
+   * of their proofs, so a theory will need to override this appropriately.
+   *
+   * This should only be called on nodes of type `Bool`.
+   */
   virtual bool printsAsBool(const Node &n) {
     // Most nodes print as formulas, so this is the default.
     return false;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c85065ef9ad60b300c186680b120e17c4fb68717..e27cff94d3150cbde7de2523b5568ee19c22074b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -28,6 +28,7 @@ set(regress_0_tests
   regress0/arith/issue1399.smt2
   regress0/arith/issue3412.smt2
   regress0/arith/issue3413.smt2
+  regress0/arith/ite-lift.smt2
   regress0/arith/leq.01.smtv1.smt2
   regress0/arith/miplib.cvc
   regress0/arith/miplib2.cvc

diff --git a/test/regress/regress0/arith/ite-lift.smt2 b/test/regress/regress0/arith/ite-lift.smt2
new file mode 100644 (file)
index 0000000..bd2df3d
--- /dev/null
+++ b/test/regress/regress0/arith/ite-lift.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --check-proofs
+(set-option :incremental false)
+(set-info :status unsat)
+(set-info :category "crafted")
+(set-info :difficulty "0")
+(set-logic QF_LRA)
+
+(declare-fun x_0 () Real)
+(declare-fun x_1 () Real)
+(declare-fun b_f () Bool)
+(assert (<= x_0 0))
+(assert (<= x_1 0))
+(assert (not b_f))
+(assert (ite b_f b_f (>= (+ x_0 x_1) 1)))
+(check-sat)