Add branch and bound lemma if linear arithmetic generates a non-integer assignment (#6868)

This double checks that TheoryArithPrivate generates a model that does not assign real values to integer variables.

This is done outside of TheoryArithPrivate intentionally, so that it can be checked independently.

This code should very rarely be applied but would have caught the incorrect model which led to wrong results in the UFNIA division of smtcomp 2021.

6 files changed, 67 insertions, 154 deletions

diff --git a/src/theory/arith/arith_state.cpp b/src/theory/arith/arith_state.cpp
index 4af7b8b8d..93d410bf8 100644
--- a/src/theory/arith/arith_state.cpp
+++ b/src/theory/arith/arith_state.cpp
@@ -21,19 +21,20 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-ArithState::ArithState(TheoryArithPrivate& parent,
-                       context::Context* c,
+ArithState::ArithState(context::Context* c,
                        context::UserContext* u,
                        Valuation val)
-    : TheoryState(c, u, val), d_parent(parent)
+    : TheoryState(c, u, val), d_parent(nullptr)
 {
 }
 
 bool ArithState::isInConflict() const
 {
-  return d_parent.anyConflict() || d_conflict;
+  return d_parent->anyConflict() || d_conflict;
 }
 
+void ArithState::setParent(TheoryArithPrivate* p) { d_parent = p; }
+
 }  // namespace arith
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h
index 0aa848f46..a54ae6bf0 100644
--- a/src/theory/arith/arith_state.h
+++ b/src/theory/arith/arith_state.h
@@ -38,17 +38,16 @@ class TheoryArithPrivate;
 class ArithState : public TheoryState
 {
  public:
-  ArithState(TheoryArithPrivate& parent,
-             context::Context* c,
-             context::UserContext* u,
-             Valuation val);
+  ArithState(context::Context* c, context::UserContext* u, Valuation val);
   ~ArithState() {}
   /** Are we currently in conflict? */
   bool isInConflict() const override;
+  /** Set parent */
+  void setParent(TheoryArithPrivate* p);
 
  private:
   /** reference to parent */
-  TheoryArithPrivate& d_parent;
+  TheoryArithPrivate* d_parent;
 };
 
 }  // namespace arith
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 5c4678cb4..980714d53 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -41,18 +41,20 @@ TheoryArith::TheoryArith(context::Context* c,
                          const LogicInfo& logicInfo,
                          ProofNodeManager* pnm)
     : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm),
-      d_internal(
-          new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)),
       d_ppRewriteTimer(smtStatisticsRegistry().registerTimer(
           "theory::arith::ppRewriteTimer")),
-      d_ppPfGen(pnm, c, "Arith::ppRewrite"),
-      d_astate(*d_internal, c, u, valuation),
+      d_astate(c, u, valuation),
       d_im(*this, d_astate, pnm),
+      d_ppre(c, pnm),
+      d_bab(d_astate, d_im, d_ppre, pnm),
+      d_internal(new TheoryArithPrivate(*this, c, u, d_bab, pnm)),
       d_nonlinearExtension(nullptr),
       d_opElim(pnm, logicInfo),
       d_arithPreproc(d_astate, d_im, pnm, d_opElim),
       d_rewriter(d_opElim)
 {
+  // currently a cyclic dependency to TheoryArithPrivate
+  d_astate.setParent(d_internal);
   // indicate we are using the theory state object and inference manager
   d_theoryState = &d_astate;
   d_inferManager = &d_im;
@@ -114,7 +116,7 @@ TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
 
   if (atom.getKind() == kind::EQUAL)
   {
-    return ppRewriteEq(atom);
+    return d_ppre.ppRewriteEq(atom);
   }
   Assert(Theory::theoryOf(atom) == THEORY_ARITH);
   // Eliminate operators. Notice we must do this here since other
@@ -126,30 +128,6 @@ TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
   return d_arithPreproc.eliminate(atom, lems, false);
 }
 
-TrustNode TheoryArith::ppRewriteEq(TNode atom)
-{
-  Assert(atom.getKind() == kind::EQUAL);
-  if (!options::arithRewriteEq())
-  {
-    return TrustNode::null();
-  }
-  Assert(atom[0].getType().isReal());
-  Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1];
-  Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1];
-  Node rewritten = Rewriter::rewrite(leq.andNode(geq));
-  Debug("arith::preprocess")
-      << "arith::preprocess() : returning " << rewritten << endl;
-  // don't need to rewrite terms since rewritten is not a non-standard op
-  if (proofsEnabled())
-  {
-    return d_ppPfGen.mkTrustedRewrite(
-        atom,
-        rewritten,
-        d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)}));
-  }
-  return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
-}
-
 Theory::PPAssertStatus TheoryArith::ppAssert(
     TrustNode tin, TrustSubstitutionMap& outSubstitutions)
 {
@@ -239,6 +217,40 @@ bool TheoryArith::collectModelValues(TheoryModel* m,
   // get the model from the linear solver
   std::map<Node, Node> arithModel;
   d_internal->collectModelValues(termSet, arithModel);
+  // Double check that the model from the linear solver respects integer types,
+  // if it does not, add a branch and bound lemma. This typically should never
+  // be necessary, but is needed in rare cases.
+  bool addedLemma = false;
+  bool badAssignment = false;
+  for (const std::pair<const Node, Node>& p : arithModel)
+  {
+    if (p.first.getType().isInteger() && !p.second.getType().isInteger())
+    {
+      Assert(false) << "TheoryArithPrivate generated a bad model value for "
+                       "integer variable "
+                    << p.first << " : " << p.second;
+      // must branch and bound
+      TrustNode lem =
+          d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>());
+      if (d_im.trustedLemma(lem, InferenceId::ARITH_BB_LEMMA))
+      {
+        addedLemma = true;
+      }
+      badAssignment = true;
+    }
+  }
+  if (addedLemma)
+  {
+    // we had to add a branch and bound lemma since the linear solver assigned
+    // a non-integer value to an integer variable.
+    return false;
+  }
+  // this would imply that linear arithmetic's model failed to satisfy a branch
+  // and bound lemma
+  AlwaysAssert(!badAssignment)
+      << "Bad assignment from TheoryArithPrivate::collectModelValues, and no "
+         "branching lemma was sent";
+
   // if non-linear is enabled, intercept the model, which may repair its values
   if (d_nonlinearExtension != nullptr)
   {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 43c962e30..decbf93bd 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -21,7 +21,9 @@
 #include "theory/arith/arith_preprocess.h"
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_state.h"
+#include "theory/arith/branch_and_bound.h"
 #include "theory/arith/inference_manager.h"
+#include "theory/arith/pp_rewrite_eq.h"
 #include "theory/theory.h"
 
 namespace cvc5 {
@@ -39,16 +41,7 @@ class TheoryArithPrivate;
  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  */
 class TheoryArith : public Theory {
- private:
   friend class TheoryArithPrivate;
-
-  TheoryArithPrivate* d_internal;
-
-  TimerStat d_ppRewriteTimer;
-
-  /** Used to prove pp-rewrites */
-  EagerProofGenerator d_ppPfGen;
-
  public:
   TheoryArith(context::Context* c,
               context::UserContext* u,
@@ -136,17 +129,20 @@ class TheoryArith : public Theory {
   }
 
  private:
-  /**
-   * Preprocess equality, applies ppRewrite for equalities. This method is
-   * distinct from ppRewrite since it is not allowed to construct lemmas.
-   */
-  TrustNode ppRewriteEq(TNode eq);
   /** Get the proof equality engine */
   eq::ProofEqEngine* getProofEqEngine();
+  /** Timer for ppRewrite */
+  TimerStat d_ppRewriteTimer;
   /** The state object wrapping TheoryArithPrivate  */
   ArithState d_astate;
   /** The arith::InferenceManager. */
   InferenceManager d_im;
+  /** The preprocess rewriter for equality */
+  PreprocessRewriteEq d_ppre;
+  /** The branch and bound utility */
+  BranchAndBound d_bab;
+  /** The (old) linear arithmetic solver */
+  TheoryArithPrivate* d_internal;
 
   /**
    * The non-linear extension, responsible for all approaches for non-linear
@@ -159,7 +155,6 @@ class TheoryArith : public Theory {
   ArithPreprocess d_arithPreproc;
   /** The theory rewriter for this theory. */
   ArithRewriter d_rewriter;
-
 };/* class TheoryArith */
 
 }  // namespace arith
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 98de1eeee..fb9de9641 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -87,13 +87,12 @@ static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap);
 TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
                                        context::Context* c,
                                        context::UserContext* u,
-                                       OutputChannel& out,
-                                       Valuation valuation,
-                                       const LogicInfo& logicInfo,
+                                       BranchAndBound& bab,
                                        ProofNodeManager* pnm)
     : d_containing(containing),
       d_foundNl(false),
       d_rowTracking(),
+      d_bab(bab),
       d_pnm(pnm),
       d_checker(),
       d_pfGen(new EagerProofGenerator(d_pnm, u)),
@@ -3455,102 +3454,9 @@ TrustNode TheoryArithPrivate::branchIntegerVariable(ArithVar x) const
   const Rational& r = d.getNoninfinitesimalPart();
   const Rational& i = d.getInfinitesimalPart();
   Trace("integers") << "integers: assignment to [[" << d_partialModel.asNode(x) << "]] is " << r << "[" << i << "]" << endl;
-
   Assert(!(r.getDenominator() == 1 && i.getNumerator() == 0));
-  Assert(!d.isIntegral());
   TNode var = d_partialModel.asNode(x);
-  Integer floor_d = d.floor();
-
-  TrustNode lem = TrustNode::null();
-  NodeManager* nm = NodeManager::currentNM();
-  if (options::brabTest())
-  {
-    Trace("integers") << "branch-round-and-bound enabled" << endl;
-    Integer ceil_d = d.ceiling();
-    Rational f = r - floor_d;
-    // Multiply by -1 to get abs value.
-    Rational c = (r - ceil_d) * (-1);
-    Integer nearest = (c > f) ? floor_d : ceil_d;
-
-    // Prioritize trying a simple rounding of the real solution first,
-    // it that fails, fall back on original branch and bound strategy.
-    Node ub = Rewriter::rewrite(
-        nm->mkNode(kind::LEQ, var, mkRationalNode(nearest - 1)));
-    Node lb = Rewriter::rewrite(
-        nm->mkNode(kind::GEQ, var, mkRationalNode(nearest + 1)));
-    Node right = nm->mkNode(kind::OR, ub, lb);
-    Node rawEq = nm->mkNode(kind::EQUAL, var, mkRationalNode(nearest));
-    Node eq = Rewriter::rewrite(rawEq);
-    // Also preprocess it before we send it out. This is important since
-    // arithmetic may prefer eliminating equalities.
-    TrustNode teq;
-    if (Theory::theoryOf(eq) == THEORY_ARITH)
-    {
-      teq = d_containing.ppRewriteEq(eq);
-      eq = teq.isNull() ? eq : teq.getNode();
-    }
-    Node literal = d_containing.getValuation().ensureLiteral(eq);
-    Trace("integers") << "eq: " << eq << "\nto: " << literal << endl;
-    d_containing.getOutputChannel().requirePhase(literal, true);
-    Node l = nm->mkNode(kind::OR, literal, right);
-    Trace("integers") << "l: " << l << endl;
-    if (proofsEnabled())
-    {
-      Node less = nm->mkNode(kind::LT, var, mkRationalNode(nearest));
-      Node greater = nm->mkNode(kind::GT, var, mkRationalNode(nearest));
-      // TODO (project #37): justify. Thread proofs through *ensureLiteral*.
-      Debug("integers::pf") << "less: " << less << endl;
-      Debug("integers::pf") << "greater: " << greater << endl;
-      Debug("integers::pf") << "literal: " << literal << endl;
-      Debug("integers::pf") << "eq: " << eq << endl;
-      Debug("integers::pf") << "rawEq: " << rawEq << endl;
-      Pf pfNotLit = d_pnm->mkAssume(literal.negate());
-      // rewrite notLiteral to notRawEq, using teq.
-      Pf pfNotRawEq =
-          literal == rawEq
-              ? pfNotLit
-              : d_pnm->mkNode(
-                  PfRule::MACRO_SR_PRED_TRANSFORM,
-                  {pfNotLit, teq.getGenerator()->getProofFor(teq.getProven())},
-                  {rawEq.negate()});
-      Pf pfBot =
-          d_pnm->mkNode(PfRule::CONTRA,
-                        {d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY,
-                                       {d_pnm->mkAssume(less.negate()), pfNotRawEq},
-                                       {greater}),
-                         d_pnm->mkAssume(greater.negate())},
-                        {});
-      std::vector<Node> assumptions = {
-          literal.negate(), less.negate(), greater.negate()};
-      // Proof of (not (and (not (= v i)) (not (< v i)) (not (> v i))))
-      Pf pfNotAnd = d_pnm->mkScope(pfBot, assumptions);
-      Pf pfL = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
-                             {d_pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})},
-                             {l});
-      lem = d_pfGen->mkTrustNode(l, pfL);
-    }
-    else
-    {
-      lem = TrustNode::mkTrustLemma(l, nullptr);
-    }
-  }
-  else
-  {
-    Node ub =
-        Rewriter::rewrite(nm->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
-    Node lb = ub.notNode();
-    if (proofsEnabled())
-    {
-      lem = d_pfGen->mkTrustNode(
-          nm->mkNode(kind::OR, ub, lb), PfRule::SPLIT, {}, {ub});
-    }
-    else
-    {
-      lem = TrustNode::mkTrustLemma(nm->mkNode(kind::OR, ub, lb), nullptr);
-    }
-  }
-
-  Trace("integers") << "integers: branch & bound: " << lem << endl;
+  TrustNode lem = d_bab.branchIntegerVariable(var, r);
   if (Debug.isOn("integers"))
   {
     Node l = lem.getNode();
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index dc3c8bbb8..4afe121b9 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -33,6 +33,7 @@
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/attempt_solution_simplex.h"
+#include "theory/arith/branch_and_bound.h"
 #include "theory/arith/congruence_manager.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/delta_rational.h"
@@ -94,7 +95,8 @@ private:
   bool d_foundNl;
 
   BoundInfoMap d_rowTracking;
-
+  /** Branch and bound utility */
+  BranchAndBound& d_bab;
   // For proofs
   /** Manages the proof nodes of this theory. */
   ProofNodeManager* d_pnm;
@@ -424,9 +426,7 @@ private:
   TheoryArithPrivate(TheoryArith& containing,
                      context::Context* c,
                      context::UserContext* u,
-                     OutputChannel& out,
-                     Valuation valuation,
-                     const LogicInfo& logicInfo,
+                     BranchAndBound& bab,
                      ProofNodeManager* pnm);
   ~TheoryArithPrivate();