Add branch and bound (#6865)

This PR moves https://github.com/cvc5/cvc5/blob/master/src/theory/arith/theory_arith_private.cpp#L3451 to its own module.

The next PR will connect this module to theory_arith / theory_arith_private.

Towards ensuring type constraints are met for linear arithmetic models.

1 files changed, 73 insertions, 0 deletions

diff --git a/src/theory/arith/branch_and_bound.h b/src/theory/arith/branch_and_bound.h
new file mode 100644
index 000000000..4281ba678
--- /dev/null
+++ b/src/theory/arith/branch_and_bound.h
@@ -0,0 +1,73 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Branch and bound for arithmetic
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__ARITH__BRANCH_AND_BOUND__H
+#define CVC5__THEORY__ARITH__BRANCH_AND_BOUND__H
+
+#include <map>
+
+#include "expr/node.h"
+#include "proof/proof_node_manager.h"
+#include "proof/trust_node.h"
+#include "theory/arith/arith_state.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/pp_rewrite_eq.h"
+#include "util/rational.h"
+
+namespace cvc5 {
+namespace theory {
+namespace arith {
+
+/**
+ * Class is responsible for constructing branch and bound lemmas. It is
+ * agnostic to the state of solver; instead is simply given (variable, value)
+ * pairs in branchIntegerVariable below and constructs the appropriate lemma.
+ */
+class BranchAndBound
+{
+ public:
+  BranchAndBound(ArithState& s,
+                 InferenceManager& im,
+                 PreprocessRewriteEq& ppre,
+                 ProofNodeManager* pnm);
+  ~BranchAndBound() {}
+  /**
+   * Branch variable, called when integer var has given value
+   * in the current model, returns a split to eliminate this model.
+   */
+  TrustNode branchIntegerVariable(TNode var, Rational value);
+
+ private:
+  /** Are proofs enabled? */
+  bool proofsEnabled() const;
+  /** Reference to the state */
+  ArithState& d_astate;
+  /** Reference to the inference manager */
+  InferenceManager& d_im;
+  /** Reference to the preprocess rewriter for equality */
+  PreprocessRewriteEq& d_ppre;
+  /** Proof generator. */
+  std::unique_ptr<EagerProofGenerator> d_pfGen;
+  /** Proof node manager */
+  ProofNodeManager* d_pnm;
+};
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace cvc5
+
+#endif