Merge branch 'master' into issue6453issue6453

1 files changed, 265 insertions, 0 deletions

diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h
new file mode 100644
index 000000000..2fa216487
--- /dev/null
+++ b/src/decision/justification_strategy.h
@@ -0,0 +1,265 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Implementation of the justification SAT decision strategy
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__DECISION__JUSTIFICATION_STRATEGY_H
+#define CVC5__DECISION__JUSTIFICATION_STRATEGY_H
+
+#include "context/cdinsert_hashmap.h"
+#include "context/cdo.h"
+#include "decision/assertion_list.h"
+#include "decision/justify_info.h"
+#include "decision/justify_stack.h"
+#include "decision/justify_stats.h"
+#include "expr/node.h"
+#include "options/decision_options.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver.h"
+#include "prop/sat_solver_types.h"
+
+namespace cvc5 {
+
+namespace prop {
+class SkolemDefManager;
+}
+
+namespace decision {
+
+/**
+ * An implementation of justification SAT decision heuristic. This class
+ * is given access to the set of input formulas, and chooses next decisions
+ * based on the structure of the input formula.
+ *
+ * Notice that the SAT solver still propagates values for literals in the
+ * normal way based on BCP when using this SAT decision heuristic. This means
+ * that values for literals can be assigned between calls to get next
+ * decision. Thus, this module has access to the SAT solver for the purpose
+ * of looking up values already assigned to literals.
+ *
+ * One novel feature of this module is that it maintains a SAT-context-dependent
+ * stack corresponding to the current path in the input formula we are trying
+ * to satisfy. This means that computing the next decision does not require
+ * traversing the current assertion.
+ *
+ * As an example, say our input formulas are:
+ *   (or (and A B) C D), (or E F)
+ * where A, B, C, D, E, F are theory literals. Moreover, say we are in a
+ * state where the SAT solver has initially assigned values:
+ *   { A -> false, E -> true }
+ * Given a call to getNext, this module will analyze what is the next
+ * literal that would contribute towards making the input formulas evaluate to
+ * true. Assuming it works on assertions and terms left-to-right, it will
+ * perform the following reasoning:
+ * - The desired value of (or (and A B) C D) is true
+ *   - The desired value of (and A B) is true
+ *     - The desired value of A is true,
+ *       ...The value of A was assigned false
+ *     ...The value of (and A B) is false
+ *   - Moving to the next literal, the desired value of C is true
+ *     ...The value of C is unassigned, return C as a decision.
+ * After deciding C, assuming no backtracking occurs, we end up in a state
+ * where we have assigned:
+ *   { A -> false, E -> true, C -> true }
+ * In the next call to getNext, this module will proceed, keeping the stack
+ * from the previous call:
+ *     ... The value of C is true
+ *   ... The value of (or (and A B) C D) is true
+ * - Moving to the next assertion, the desired value of (or E F) is true
+ *   - The desired value of E is true
+ *     ... The value of E is (already) assigned true
+ *   ... the value of (or E F) is true.
+ * - The are no further assertions.
+ * Hence it will return the null SAT decision literal, indicating that no
+ * further decisions are necessary to satisfy the input assertions.
+ *
+ * This class has special handling of "skolem definitions", which arise when
+ * lemmas are introduced that correspond to the behavior of skolems. As an
+ * example, say our input, prior to preprocessing, is:
+ *   (or (P (ite A 1 2)) Q)
+ * where P is an uninterpreted predicate of type Int -> Bool. After
+ * preprocessing, in particular term formula removal which replaces term-level
+ * ITE terms with fresh skolems, we get this set of assertions:
+ *   (or (P k) Q), (ite A (= k 1) (= k 2))
+ * The second assertion is the skolem definition for k. Conceptually, this
+ * lemma is only relevant if we have asserted a literal that contains k.
+ * This module thus maintains two separate assertion lists, one for
+ * input assertions, and one for skolem definitions. The latter is populated
+ * only as skolems appear in assertions. In this example, we have initially:
+ *   input assertions = { (or (P k) Q) }
+ *   relevant skolem definitions =  {}
+ *   SAT context = {}
+ * Say this module returns (P k) as a decision. When this is asserted to
+ * the theory engine, a call to notifyAsserted is made with (P k). The
+ * skolem definition manager will recognize that (P k) contains k and hence
+ * its skolem definition is activated, giving us this state:
+ *   input assertions = { (or (P k) Q) }
+ *   relevant skolem definitions =  { (ite A (= k 1) (= k 2)) }
+ *   SAT context = { (P k) }
+ * We then proceed by satisfying (ite A (= k 1) (= k 2)), e.g. by returning
+ * A as a decision for getNext.
+ *
+ * Notice that the above policy allows us to ignore certain skolem definitions
+ * entirely. For example, if Q were to have been asserted instead of (P k),
+ * then (ite A (= k 1) (= k 2)) would not be added as a relevant skolem
+ * definition, and Q alone would have sufficed to show the input formula
+ * was satisfied.
+ */
+class JustificationStrategy
+{
+ public:
+  /** Constructor */
+  JustificationStrategy(context::Context* c,
+                        context::UserContext* u,
+                        prop::SkolemDefManager* skdm);
+
+  /** Finish initialize */
+  void finishInit(prop::CDCLTSatSolverInterface* ss, prop::CnfStream* cs);
+
+  /** Presolve, called at the beginning of each check-sat call */
+  void presolve();
+
+  /**
+   * Gets the next decision based on the current assertion to satisfy. This
+   * returns undefSatLiteral if there are no more assertions. In this case,
+   * all relevant input assertions are already propositionally satisfied by
+   * the current assignment.
+   *
+   * @return The next SAT literal to decide on.
+   */
+  prop::SatLiteral getNext();
+
+  /**
+   * Are we finished assigning values to literals?
+   *
+   * @return true if and only if all relevant input assertions are already
+   * propositionally satisfied by the current assignment.
+   */
+  bool isDone();
+
+  /**
+   * Notify this class that assertion is an (input) assertion, not corresponding
+   * to a skolem definition.
+   */
+  void addAssertion(TNode assertion);
+  /**
+   * Notify this class that lem is the skolem definition for skolem, which is
+   * a part of the current assertions.
+   */
+  void addSkolemDefinition(TNode lem, TNode skolem);
+  /**
+   * Notify this class that literal n has been asserted. This is triggered when
+   * n is sent to TheoryEngine. This activates skolem definitions for skolems
+   * k that occur in n.
+   */
+  void notifyAsserted(TNode n);
+
+ private:
+  /**
+   * Helper method to insert assertions in `toProcess` to `d_assertions` or
+   * `d_skolemAssertions` based on `useSkolemList`.
+   */
+  void insertToAssertionList(std::vector<TNode>& toProcess, bool useSkolemList);
+  /**
+   * Refresh current assertion. This ensures that d_stack has a current
+   * assertion to satisfy. If it does not already have one, we take the next
+   * assertion from the list of input assertions, or from the relevant
+   * skolem definitions based on the JutificationSkolemMode mode.
+   *
+   * @return true if we successfully initialized d_stack with the next
+   * assertion to satisfy.
+   */
+  bool refreshCurrentAssertion();
+  /**
+   * Implements the above function for the case where d_stack must get a new
+   * assertion to satisfy.
+   *
+   * @param useSkolemList If this is true, we pull the next assertion from
+   * the list of relevant skolem definitions.
+   * @return true if we successfully initialized d_stack with the next
+   * assertion to satisfy.
+   */
+  bool refreshCurrentAssertionFromList(bool useSkolemList);
+  /**
+   * Let n be the node referenced by ji.
+   *
+   * This method is called either when we have yet to process any children of n,
+   * or we just determined that the last child we processed of n had value
+   * lastChildVal.
+   *
+   * Note that knowing which child of n we processed last is the value of
+   * ji->d_childIndex.
+   *
+   * @param ji The justify node to process
+   * @param lastChildVal The value determined for the last child of the node of
+   * ji.
+   * @return Either (1) the justify node corresponding to the next child of n to
+   * consider adding to the stack, and its desired polarity, or
+   * (2) a null justify node and updates lastChildVal to the value of n.
+   */
+  JustifyNode getNextJustifyNode(JustifyInfo* ji, prop::SatValue& lastChildVal);
+  /**
+   * Returns the value TRUE/FALSE for n, or UNKNOWN otherwise.
+   *
+   * We return a value for n only if we have justified its values based on its
+   * children. For example, we return UNKNOWN for n of the form (and A B) if
+   * A and B have UNKNOWN value, even if the SAT solver has assigned a value for
+   * (internal) node n. If n itself is a theory literal, we lookup its value
+   * in the SAT solver if it is not already cached.
+   */
+  prop::SatValue lookupValue(TNode n);
+  /** Is n a theory literal? */
+  static bool isTheoryLiteral(TNode n);
+  /** Is n a theory atom? */
+  static bool isTheoryAtom(TNode n);
+  /** Pointer to the SAT context */
+  context::Context* d_context;
+  /** Pointer to the CNF stream */
+  prop::CnfStream* d_cnfStream;
+  /** Pointer to the SAT solver */
+  prop::CDCLTSatSolverInterface* d_satSolver;
+  /** Pointer to the skolem definition manager */
+  prop::SkolemDefManager* d_skdm;
+  /** The assertions, which are user-context dependent. */
+  AssertionList d_assertions;
+  /** The skolem assertions */
+  AssertionList d_skolemAssertions;
+
+  /** Mapping from non-negated nodes to their SAT value */
+  context::CDInsertHashMap<Node, prop::SatValue> d_justified;
+  /** A justify stack */
+  JustifyStack d_stack;
+  /** The last decision literal */
+  context::CDO<TNode> d_lastDecisionLit;
+  //------------------------------------ activity
+  /** Current assertion we are checking for status (context-independent) */
+  Node d_currUnderStatus;
+  /** Whether we have added a decision while considering d_currUnderStatus */
+  bool d_currStatusDec;
+  //------------------------------------ options
+  /** using relevancy order */
+  bool d_useRlvOrder;
+  /** skolem mode */
+  options::JutificationSkolemMode d_jhSkMode;
+  /** skolem relevancy mode */
+  options::JutificationSkolemRlvMode d_jhSkRlvMode;
+  /** The statistics */
+  JustifyStatistics d_stats;
+};
+
+}  // namespace decision
+}  // namespace cvc5
+
+#endif /* CVC5__DECISION__JUSTIFICATION_STRATEGY_H */