1 files changed, 146 insertions, 0 deletions
diff --git a/src/theory/decision_strategy.h b/src/theory/decision_strategy.h
new file mode 100644
index 000000000..04788f515
--- /dev/null
+++ b/src/theory/decision_strategy.h
@@ -0,0 +1,146 @@
+/*********************                                                        */
+/*! \file decision_strategy.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 Base classes for decision strategies used by theory solvers
+ ** for use in the DecisionManager of TheoryEngine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__DECISION_STRATEGY__H
+#define __CVC4__THEORY__DECISION_STRATEGY__H
+
+#include <map>
+#include "context/cdo.h"
+#include "expr/node.h"
+#include "theory/valuation.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * Virtual base class for decision strategies.
+ */
+class DecisionStrategy
+{
+ public:
+  DecisionStrategy() {}
+  virtual ~DecisionStrategy() {}
+  /**
+   * Initalize this strategy, This is called once per satisfiability call by
+   * the DecisionManager, prior to using this strategy.
+   */
+  virtual void initialize() = 0;
+  /**
+   * If this method returns a non-null node n, then n is the required next
+   * decision of this strategy. It must be the case that n is a literal in
+   * the current CNF stream.
+   */
+  virtual Node getNextDecisionRequest() = 0;
+  /** identify this strategy (for debugging) */
+  virtual std::string identify() const = 0;
+};
+
+/**
+ * Decision strategy finite model finding.
+ *
+ * This is a virtual base class for decision strategies that follow the
+ * "finite model finding" pattern for decisions. Such strategies have the
+ * distinguishing feature that they are interested in a stream of literals
+ * L_1, L_2, L_3, ... and so on. At any given time, they request that L_i is
+ * asserted true for a minimal i.
+ *
+ * To enforce this strategy, this class maintains a SAT-context dependent
+ * index d_curr_literal, which corresponds to the minimal index of a literal
+ * in the above list that is not asserted false. A call to
+ * getNextDecisionRequest increments this value until we find a literal L_j
+ * that is not assigned false. If L_j is unassigned, we return it as a decision,
+ * otherwise we return no decisions.
+ */
+class DecisionStrategyFmf : public DecisionStrategy
+{
+ public:
+  DecisionStrategyFmf(context::Context* satContext, Valuation valuation);
+  virtual ~DecisionStrategyFmf() {}
+  /** initialize */
+  void initialize() override;
+  /** get next decision request */
+  Node getNextDecisionRequest() override;
+  /** Make the n^th literal of this strategy */
+  virtual Node mkLiteral(unsigned n) = 0;
+  /**
+   * This method returns true iff there exists a (minimal) i such that L_i
+   * is a literal allocated by this class, and is asserted true in the current
+   * context. If it returns true, the argument i is set to this i.
+   */
+  bool getAssertedLiteralIndex(unsigned& i) const;
+  /**
+   * This method returns the literal L_i allocated by this class that
+   * has been asserted true in the current context and is such that i is
+   * minimal. It returns null if no such literals exist.
+   */
+  Node getAssertedLiteral();
+  /** Get the n^th literal of this strategy */
+  Node getLiteral(unsigned lit);
+
+ protected:
+  /**
+   * The valuation of this class, used for knowing what literals are asserted,
+   * and with what polarity.
+   */
+  Valuation d_valuation;
+  /**
+   * The (SAT-context-dependent) flag that is true if there exists a literal
+   * of this class that is asserted true in the current context, according to
+   * d_valuation.
+   */
+  context::CDO<bool> d_has_curr_literal;
+  /**
+   * The (SAT-context-dependent) index of the current literal of this strategy.
+   * This corresponds to the first literal that is not asserted false in the
+   * current context, according to d_valuation.
+   */
+  context::CDO<unsigned> d_curr_literal;
+  /** the list of literals of this strategy */
+  std::vector<Node> d_literals;
+};
+
+/**
+ * Special case of above where we only wish to allocate a single literal L_1.
+ */
+class DecisionStrategySingleton : public DecisionStrategyFmf
+{
+ public:
+  DecisionStrategySingleton(const char* name,
+                            Node lit,
+                            context::Context* satContext,
+                            Valuation valuation);
+  /**
+   * Make the n^th literal of this strategy. This method returns d_literal if
+   * n=0, null otherwise.
+   */
+  Node mkLiteral(unsigned n) override;
+  /** Get single literal */
+  Node getSingleLiteral();
+  /** identify */
+  std::string identify() const override { return d_name; }
+
+ private:
+  /** the name of this strategy */
+  std::string d_name;
+  /** the literal to decide on */
+  Node d_literal;
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__DECISION_STRATEGY__H */