Add proof in missing case in arith congruence manager (cvc5#11114)

ajreynol · Aug 1, 2024 · dd79405 · dd79405
1 parent beff2e4
commit dd79405
Show file tree

Hide file tree

Showing 3 changed files with 71 additions and 3 deletions.
diff --git a/src/theory/arith/linear/congruence_manager.cpp b/src/theory/arith/linear/congruence_manager.cpp
@@ -18,6 +18,7 @@
 
 #include "base/output.h"
 #include "options/arith_options.h"
+#include "proof/proof_checker.h"
 #include "proof/proof_node.h"
 #include "proof/proof_node_manager.h"
 #include "smt/env.h"
@@ -361,11 +362,69 @@ bool ArithCongruenceManager::propagate(TNode x){
     ConstraintCP negC = c->getNegation();
     Node neg = Constraint::externalExplainByAssertions({negC});
     Node conf = expC.andNode(neg);
-    Node final = flattenAnd(conf);
+    Node finalPf = flattenAnd(conf);
 
     ++(d_statistics.d_conflicts);
-    raiseConflict(final);
-    Trace("arith::congruenceManager") << "congruenceManager found a conflict " << final << std::endl;
+    if (isProofEnabled())
+    {
+      // we have a proof of (=> C L1) and need a proof of
+      // (not (and C L2)), where L1 and L2 are contradictory literals,
+      // stored in proven[1] and neg respectively below.
+      NodeManager* nm = NodeManager::currentNM();
+      std::vector<Node> conj(finalPf.begin(), finalPf.end());
+      CDProof cdp(d_env);
+      Node falsen = nm->mkConst(false);
+      Node finalPfNeg = finalPf.notNode();
+      cdp.addProof(texpC.toProofNode());
+      Node proven = texpC.getProven();
+      Node antec = proven[0];
+      std::vector<Node> antecc(antec.begin(), antec.end());
+      cdp.addStep(antec, ProofRule::AND_INTRO, antecc, {});
+      cdp.addStep(proven[1], ProofRule::MODUS_PONENS, {antec, proven}, {});
+      std::shared_ptr<ProofNode> pf;
+      bool success = false;
+      if (neg.getKind() == Kind::NOT && neg[0] == proven[1])
+      {
+        // L1 and L2 are negation of one another, just use CONTRA
+        cdp.addStep(falsen, ProofRule::CONTRA, {proven[1], neg}, {});
+        success = true;
+      }
+      else if (proven[1].getKind() == Kind::EQUAL)
+      {
+        // otherwise typically proven[1] is of the form (= t c) or (= c t) where
+        // neg is the (negation of) a relation involving t.
+        Node peq = proven[1][0].isConst() ? proven[1][1].eqNode(proven[1][0])
+                                          : proven[1];
+        if (peq[1].isConst())
+        {
+          ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
+          Node res = pc->checkDebug(
+              ProofRule::MACRO_SR_PRED_TRANSFORM, {neg, peq}, {falsen}, falsen);
+          Assert(!res.isNull());
+          if (!res.isNull())
+          {
+            cdp.addStep(falsen,
+                        ProofRule::MACRO_SR_PRED_TRANSFORM,
+                        {neg, peq},
+                        {falsen});
+            success = true;
+          }
+        }
+      }
+      if (success)
+      {
+        cdp.addStep(finalPfNeg, ProofRule::SCOPE, {falsen}, conj);
+        pf = cdp.getProofFor(finalPfNeg);
+      }
+      Assert(pf != nullptr) << "Failed from " << neg << " " << proven[1];
+      raiseConflict(finalPf, pf);
+    }
+    else
+    {
+      raiseConflict(finalPf);
+    }
+    Trace("arith::congruenceManager")
+        << "congruenceManager found a conflict " << finalPf << std::endl;
     return false;
   }
 

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -1844,6 +1844,7 @@ set(regress_0_tests
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/nterm-pc-zalig.smt2
   regress0/strings/parser-syms.cvc.smt2
+  regress0/strings/prefix-simple-no-pf.smt2
   regress0/strings/proj-issue316-regexp-ite.smt2
   regress0/strings/proj-issue390-update-rev-rewrite.smt2
   regress0/strings/proj-issue409-re-loop-none.smt2

diff --git a/test/regress/cli/regress0/strings/prefix-simple-no-pf.smt2 b/test/regress/cli/regress0/strings/prefix-simple-no-pf.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --preregister-mode=lazy
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const x Int)
+(declare-const y String)
+(assert (str.prefixof "a" (str.substr y 0 x)))
+(assert (not (str.prefixof "a" y)))
+(check-sat)