Use side effect utility for non-linear lemmas (#3780)

Fixes #3647.

Previously, when doing incremental linearization for transcedental functions, we would add points to the list of secant points at the time when linearization lemmas were generated. However, our strategy has been updated such that lemmas may be abandoned (say in the case that a higher priority lemma is found). Thus, our list of secant points had spurious points corresponding to lemmas that weren't sent. This led to assertion failures, and likely led to gaps in our linearization, hindering our ability to say sat/unsat.

This PR introduces a "lemma side effect" class to ensure that modifications to the state of the nonlinear solver are in sync with the lemmas we send out.

1 files changed, 53 insertions, 0 deletions

diff --git a/src/theory/arith/nl_lemma_utils.h b/src/theory/arith/nl_lemma_utils.h
new file mode 100644
index 000000000..74886a1fb
--- /dev/null
+++ b/src/theory/arith/nl_lemma_utils.h
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file nl_lemma_utils.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Utilities for processing lemmas from the non-linear solver
+ **/
+
+#ifndef CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H
+#define CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H
+
+#include <tuple>
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/**
+ * A side effect of adding a lemma in the non-linear solver. This is used
+ * to specify how the state of the non-linear solver should update. This
+ * includes:
+ * - A set of secant points to record (for transcendental secant plane
+ * inferences).
+ */
+struct NlLemmaSideEffect
+{
+  NlLemmaSideEffect() {}
+  ~NlLemmaSideEffect() {}
+  /** secant points to add
+   *
+   * A member (tf, d, c) in this vector indicates that point c should be added
+   * to the list of secant points for an application of a transcendental
+   * function tf for Taylor degree d. This is used for incremental linearization
+   * for underapproximation (resp. overapproximations) of convex (resp.
+   * concave) regions of transcendental functions. For details, see
+   * Cimatti et al., CADE 2017.
+   */
+  std::vector<std::tuple<Node, unsigned, Node> > d_secantPoint;
+};
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H */