/******************************************************************************

 * Top contributors (to current version):

 *   Tim King, Alex Ozdemir, Haniel Barbosa

 *

 * 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.

 * ****************************************************************************

 *

 * Defines Constraint and ConstraintDatabase which is the internal

 * representation of variables in arithmetic

 *

 * This file defines Constraint and ConstraintDatabase.

 * A Constraint is the internal representation of literals in TheoryArithmetic.

 * Constraints are fundamentally a triple:

 *  - ArithVar associated with the constraint,

 *  - a DeltaRational value,

 *  - and a ConstraintType.

 *

 * Literals:

 *   The constraint may also keep track of a node corresponding to the

 *   Constraint.

 *   This can be accessed by getLiteral() in O(1) if it has been set.

 *   This node must be in normal form and may be used for communication with

 *   the TheoryEngine.

 *

 * In addition, Constraints keep track of the following:

 *  - A Constraint that is the negation of the Constraint.

 *  - An iterator into a set of Constraints for the ArithVar sorted by

 *    DeltaRational value.

 *  - A context dependent internal proof of the node that can be used for

 *    explanations.

 *  - Whether an equality/disequality has been split in the user context via a

 *    lemma.

 *  - Whether a constraint, be be used in explanations sent to the context

 *

 * Looking up constraints:

 *  - All of the Constraints with associated nodes in the ConstraintDatabase

 *    can be accessed via a single hashtable lookup until the Constraint is

 *    removed.

 *  - Nodes that have not been associated to a constraints can be

 *    inserted/associated to existing nodes in O(log n) time.

 *

 * Implications:

 *  - A Constraint can be used to find unate implications.

 *  - A unate implication is an implication based purely on the ArithVar

 *    matching  and the DeltaRational value.

 *    (implies (<= x c) (<= x d)) given c <= d

 *  - This is done using the iterator into the sorted set of constraints.

 *  - Given a tight constraint and previous tightest constraint, this will

 *    efficiently propagate internally.

 *

 * Additing and Removing Constraints

 *  - Adding Constraints takes O(log n) time where n is the number of

 *    constraints associated with the ArithVar.

 *  - Removing Constraints takes O(1) time.

 *

 * Internals:

 *  - Constraints are pointers to ConstraintValues.

 *  - Undefined Constraints are NullConstraint.

 *

 * Assumption vs. Assertion:

 * - An assertion is anything on the theory d_fact queue.

 *   This includes any thing propagated and returned to the fact queue.

 *   These can be used in external conflicts and propagations of earlier

 *   proofs.

 * - An assumption is anything on the theory d_fact queue that has no further

 *   explanation i.e. this theory did not propagate it.

 * - To set something an assumption, first set it as being as assertion.

 * - Internal assumptions have no explanations and must be regressed out of the

 *   proof.

 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__ARITH__CONSTRAINT_H

#define CVC5__THEORY__ARITH__CONSTRAINT_H

#include <unordered_map>

#include <vector>

#include "base/configuration_private.h"

#include "context/cdlist.h"

#include "context/cdqueue.h"

#include "expr/node.h"

#include "proof/trust_node.h"

#include "smt/env_obj.h"

#include "theory/arith/arithvar.h"

#include "theory/arith/callbacks.h"

#include "theory/arith/constraint_forward.h"

#include "theory/arith/delta_rational.h"

#include "util/statistics_stats.h"

namespace cvc5 {

class ProofNodeManager;

class EagerProofGenerator;

namespace context {

class Context;

}

namespace theory {

namespace arith {

class Comparison;

class ArithCongruenceManager;

class ArithVariables;

/**

 * Logs the types of different proofs.

 * Current, proof types:

 * - NoAP             : This constraint is not known to be true.

 * - AssumeAP         : This is an input assertion. There is no proof.

 *                    : Something can be both asserted and have a proof.

 * - InternalAssumeAP : An internal assumption. This has no guarantee of having an external proof.

 *                    : This must be removed by regression.

 * - FarkasAP         : A proof with Farka's coefficients, i.e.

 *                    :  \sum lambda_i ( asNode(x_i) <= c_i  ) |= 0 < 0

 *                    : If proofs are on, coefficients will be logged.

 *                    : If proofs are off, coefficients will not be logged.

 *                    : A unate implication is a FarkasAP.

 * - TrichotomyAP     : This is any entailment using (x<= a and x >=a) => x = a

 *                    : Equivalently, (x > a or x < a or x = a)

 *                    : There are 3 candidate ways this can propagate:

 *                    :   !(x > a) and !(x = a) => x < a

 *                    :   !(x < a) and !(x = a) => x > a

 *                    :   !(x > a) and !(x < a) => x = a

 * - EqualityEngineAP : This is propagated by the equality engine.

 *                    : Consult this for the proof.

 * - IntTightenAP     : This is indicates that a bound involving integers was tightened.

 *                    : e.g. i < 5.5 became i <= 5, when i is an integer.

 * - IntHoleAP        : This is currently a catch-all for all integer specific reason.

 */

enum ArithProofType

  { NoAP,

    AssumeAP,

    InternalAssumeAP,

    FarkasAP,

    TrichotomyAP,

    EqualityEngineAP,

    IntTightenAP,

    IntHoleAP};

/**

 * The types of constraints.

 * The convex constraints are the constraints are LowerBound, Equality,

 * and UpperBound.

 */

enum ConstraintType {LowerBound, Equality, UpperBound, Disequality};

typedef context::CDList<ConstraintCP> CDConstraintList;

typedef std::unordered_map<Node, ConstraintP> NodetoConstraintMap;

typedef size_t ConstraintRuleID;

static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max();

typedef size_t AntecedentId;

static const AntecedentId AntecedentIdSentinel = std::numeric_limits<AntecedentId>::max();

typedef size_t AssertionOrder;

static const AssertionOrder AssertionOrderSentinel = std::numeric_limits<AssertionOrder>::max();

/**

 * A ValueCollection binds together convex constraints that have the same

 * DeltaRational value.

 */

class ValueCollection {

private:

  ConstraintP d_lowerBound;

  ConstraintP d_upperBound;

  ConstraintP d_equality;

  ConstraintP d_disequality;

public:

  ValueCollection();

  static ValueCollection mkFromConstraint(ConstraintP c);

  bool hasLowerBound() const;

  bool hasUpperBound() const;

  bool hasEquality() const;

  bool hasDisequality() const;

  bool hasConstraintOfType(ConstraintType t) const;

  ConstraintP getLowerBound() const;

  ConstraintP getUpperBound() const;

  ConstraintP getEquality() const;

  ConstraintP getDisequality() const;

  ConstraintP getConstraintOfType(ConstraintType t) const;

  /** Returns true if any of the constraints are non-null. */

  bool empty() const;

  /**

   * Remove the constraint of the type t from the collection.

   * Returns true if the ValueCollection is now empty.

   * If true is returned, d_value is now NULL.

   */

  void remove(ConstraintType t);

  /**

   * Adds a constraint to the set.

   * The collection must not have a constraint of that type already.

   */

  void add(ConstraintP c);

  void push_into(std::vector<ConstraintP>& vec) const;

  ConstraintP nonNull() const;

  ArithVar getVariable() const;

  const DeltaRational& getValue() const;

};

/**

 * A Map of ValueCollections sorted by the associated DeltaRational values.

 *

 * Discussion:

 * While it is more natural to consider this a set, this cannot be a set as in

 * sets the type of both iterator and const_iterator in sets are

 * "constant iterators".  We require iterators that dereference to

 * ValueCollection&.

 *

 * See:

 * http://gcc.gnu.org/onlinedocs/libstdc++/ext/lwg-defects.html#103

 */

typedef std::map<DeltaRational, ValueCollection> SortedConstraintMap;

typedef SortedConstraintMap::iterator SortedConstraintMapIterator;

typedef SortedConstraintMap::const_iterator SortedConstraintMapConstIterator;

/** A Pair associating a variables and a Sorted ConstraintSet. */

  ArithVar d_var;

  SortedConstraintMap d_constraints;

  // x ? c_1, x ? c_2, x ? c_3, ...

  // where ? is a non-empty subset of {lb, ub, eq}

  // c_1 < c_2 < c_3 < ...

  }

  }

};

/**

 * If proofs are on, there is a vector of rationals for farkas coefficients.

 * This is the owner of the memory for the vector, and calls delete upon

 * cleanup.

 *

 */

struct ConstraintRule {

  ConstraintP d_constraint;

  ArithProofType d_proofType;

  AntecedentId d_antecedentEnd;

  /**

   * In this comment, we abbreviate ConstraintDatabase::d_antecedents

   * and d_farkasCoefficients as ans and fc.

   *

   * This list is always empty if proofs are not enabled.

   *

   * If proofs are enabled, the proof of constraint c at p in ans[p] of length n

   * is (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p])

   *

   * Farkas' proofs show a contradiction with the negation of c, c_not =

   * c->getNegation().

   *

   * We treat the position for NullConstraint (p-n) as the position for the

   * farkas coefficient for so we pretend c_not is ans[p-n]. So this correlation

   * for the constraints we are going to use: (c_not, ans[p-n+(1)], ... ,

   * ans[p-n+(n-1)], ans[p-n+(n)]) With the coefficients at positions: (fc[0],

   * fc[1)], ... fc[n])

   *

   * The index of the constraints in the proof are {i | i <= 0 <= n] } (with

   * c_not being p-n). Partition the indices into L, U, and E, the lower bounds,

   * the upper bounds and equalities.

   *

   * We standardize the proofs to be upper bound oriented following the

   * convention: A x <= b with the proof witness of the form (lambda) Ax <=

   * (lambda) b and lambda >= 0.

   *

   * To accomplish this cleanly, the fc coefficients must be negative for lower

   * bounds. The signs of equalities can be either positive or negative.

   *

   * Thus the proof corresponds to (with multiplication over inequalities):

   *    \sum_{u in U} fc[u] ans[p-n+u] + \sum_{e in E} fc[e] ans[p-n+e]

   *  + \sum_{l in L} fc[l] ans[p-n+l]

   * |= 0 < 0

   * where fc[u] > 0, fc[l] < 0, and fc[e] != 0 (i.e. it can be either +/-).

   *

   * There is no requirement that the proof is minimal.

   * We do however use all of the constraints by requiring non-zero

   * coefficients.

   */

  RationalVectorCP d_farkasCoefficients;

  ConstraintRule();

  ConstraintRule(ConstraintP con, ArithProofType pt);

  ConstraintRule(ConstraintP con,

                 ArithProofType pt,

                 AntecedentId antecedentEnd);

  ConstraintRule(ConstraintP con,

                 ArithProofType pt,

                 AntecedentId antecedentEnd,

                 RationalVectorCP coeffs);

  void print(std::ostream& out, bool produceProofs) const;

  void debugPrint() const;

}; /* class ConstraintRule */

class Constraint {

  friend class ConstraintDatabase;

 public:

  /**

   * This begins construction of a minimal constraint.

   *

   * This should only be called by ConstraintDatabase.

   *

   * Because of circular dependencies a Constraint is not fully valid until

   * initialize has been called on it.

   */

  Constraint(ArithVar x,

             ConstraintType t,

             const DeltaRational& v,

             bool produceProofs);

  /**

   * Destructor for a constraint.

   * This should only be called if safeToGarbageCollect() is true.

   */

  ~Constraint();

  static ConstraintType constraintTypeOfComparison(const Comparison& cmp);

  }

  }

  }

  }

  }

  }

  }

  }

  }

  }

  }

  /**

   * Splits the node in the user context.

   * Returns a lemma that is assumed to be true for the rest of the user context.

   * Constraint must be an equality or disequality.

   */

  TrustNode split();

  }

  void setCanBePropagated();

  /**

   * Light wrapper for calling setCanBePropagated(),

   * on this and this->d_negation.

   */

  }

  }

  }

  /**

   * Sets the witness literal for a node being on the assertion stack.

   *

   * If the negation of the node is true, inConflict must be true.

   * If the negation of the node is false, inConflict must be false.

   * Hence, negationHasProof() == inConflict.

   *

   * This replaces:

   *   void setAssertedToTheTheory(TNode witness);

   *   void setAssertedToTheTheoryWithNegationTrue(TNode witness);

   */

  void setAssertedToTheTheory(TNode witness, bool inConflict);

  }

  void setLiteral(Node n);

  }

  /** Gets a literal in the normal form suitable for proofs.

   * That is, (sum of non-const monomials) >< const.

   *

   * This is a sister method to `getLiteral`, which returns a normal form

   * literal, suitable for external solving use.

   */

  Node getProofLiteral() const;

  /**

   * Set the node as having a proof and being an assumption.

   * The node must be assertedToTheTheory().

   *

   * Precondition: negationHasProof() == inConflict.

   *

   * Replaces:

   *  selfExplaining().

   *  selfExplainingWithNegationTrue().

   */

  void setAssumption(bool inConflict);

  /** Returns true if the node is an assumption.*/

  bool isAssumption() const;

  /** Whether we produce proofs */

  /** Set the constraint to have an EqualityEngine proof. */

  void setEqualityEngineProof();

  bool hasEqualityEngineProof() const;

  /** Returns true if the node has a Farkas' proof. */

  bool hasFarkasProof() const;

  /**

   * @brief Returns whether this constraint is provable using a Farkas

   * proof applied to (possibly tightened) input assertions.

   *

   * An example of a constraint that has a simple Farkas proof:

   *    x <= 0 proven from x + y <= 0 and x - y <= 0.

   *

   * An example of another constraint that has a simple Farkas proof:

   *    x <= 0 proven from x + y <= 0 and x - y <= 0.5 for integers x, y

   *       (integer bound-tightening is applied first!).

   *

   * An example of a constraint that might be proven **without** a simple

   * Farkas proof:

   *    x < 0 proven from not(x == 0) and not(x > 0).

   *

   * This could be proven internally by the arithmetic theory using

   * `TrichotomyAP` as the proof type.

   *

   */

  bool hasSimpleFarkasProof() const;

  /**

   * Returns whether this constraint is an assumption or a tightened

   * assumption.

   */

  bool isPossiblyTightenedAssumption() const;

  /** Returns true if the node has a int bound tightening proof. */

  bool hasIntTightenProof() const;

  /** Returns true if the node has a int hole proof. */

  bool hasIntHoleProof() const;

  /** Returns true if the node has a trichotomy proof. */

  bool hasTrichotomyProof() const;

  void printProofTree(std::ostream & out, size_t depth = 0) const;

  /**

   * A sets the constraint to be an internal assumption.

   *

   * This does not need to have a witness or an associated literal.

   * This is always itself in the explanation fringe for both conflicts

   * and propagation.

   * This cannot be converted back into a Node conflict or explanation.

   *

   * This cannot have a proof or be asserted to the theory!

   *

   */

  void setInternalAssumption(bool inConflict);

  bool isInternalAssumption() const;

  /**

   * Returns a explanation of the constraint that is appropriate for conflicts.

   *

   * This is not appropriate for propagation!

   *

   * This is the minimum fringe of the implication tree s.t.

   * every constraint is assertedToTheTheory() or hasEqualityEngineProof().

   */

  TrustNode externalExplainByAssertions() const;

  /**

   * Writes an explanation of a constraint into the node builder.

   * Pushes back an explanation that is acceptable to send to the sat solver.

   * nb is assumed to be an AND.

   *

   * This is the minimum fringe of the implication tree s.t.

   * every constraint is assertedToTheTheory() or hasEqualityEngineProof().

   *

   * This is not appropriate for propagation!

   * Use explainForPropagation() instead.

   */

  {

  }

  /* Equivalent to calling externalExplainByAssertions on all constraints in b */

  static Node externalExplainByAssertions(const ConstraintCPVec& b);

  static Node externalExplainByAssertions(ConstraintCP a, ConstraintCP b);

  static Node externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c);

  /**

   * This is the minimum fringe of the implication tree s.t. every constraint is

   * - assertedToTheTheory(),

   * - isInternalDecision() or

   * - hasEqualityEngineProof().

   */

  static void assertionFringe(ConstraintCPVec& v);

  static void assertionFringe(ConstraintCPVec& out, const ConstraintCPVec& in);

  /** The fringe of a farkas' proof. */

  }

  /**

   * Returns an explanation of a propagation by the ConstraintDatabase.

   * The constraint must have a proof.

   * The constraint cannot be an assumption.

   *

   * This is the minimum fringe of the implication tree (excluding the

   * constraint itself) s.t. every constraint is assertedToTheTheory() or

   * hasEqualityEngineProof().

   *

   * All return conjuncts were asserted before this constraint.

   *

   * Requires the given node to rewrite to the canonical literal for this

   * constraint.

   *

   * @params n the literal to prove

   *           n must rewrite to the constraint's canonical literal

   *

   * @returns a trust node of the form:

   *         (=> explanation n)

   */

  TrustNode externalExplainForPropagation(TNode n) const;

  /**

   * Explain the constraint and its negation in terms of assertions.

   * The constraint must be in conflict.

   */

  TrustNode externalExplainConflict() const;

  /** The constraint is known to be true. */

  }

  /** The negation of the constraint is known to hold. */

  }

  /** Neither the contraint has a proof nor the negation has a proof.*/

  }

  /** This is a synonym for hasProof(). */

  }

  /** Both the constraint and its negation are true. */

  }

  /**

   * Returns the constraint that corresponds to taking

   *    x r ceiling(getValue()) where r is the node's getType().

   * Esstentially this is an up branch.

   */

  ConstraintP getCeiling();

  /**

   * Returns the constraint that corresponds to taking

   *    x r floor(getValue()) where r is the node's getType().

   * Esstentially this is a down branch.

   */

  ConstraintP getFloor();

  static ConstraintP makeNegation(ArithVar v,

                                  ConstraintType t,

                                  const DeltaRational& r,

                                  bool produceProofs);

  const ValueCollection& getValueCollection() const;

  ConstraintP getStrictlyWeakerUpperBound(bool hasLiteral, bool mustBeAsserted) const;

  ConstraintP getStrictlyWeakerLowerBound(bool hasLiteral, bool mustBeAsserted) const;

  /**

   * Marks a the constraint c as being entailed by a.

   * The Farkas proof 1*(a) + -1 (c) |= 0<0

   *

   * After calling impliedByUnate(), the caller should either raise a conflict

   * or try call tryToPropagate().

   */

  void impliedByUnate(ConstraintCP a, bool inConflict);

  /**

   * Marks a the constraint c as being entailed by a.

   * The reason has to do with integer bound tightening.

   *

   * After calling impliedByIntTighten(), the caller should either raise a conflict

   * or try call tryToPropagate().

   */

  void impliedByIntTighten(ConstraintCP a, bool inConflict);

  /**

   * Marks a the constraint c as being entailed by a.

   * The reason has to do with integer reasoning.

   *

   * After calling impliedByIntHole(), the caller should either raise a conflict

   * or try call tryToPropagate().

   */

  void impliedByIntHole(ConstraintCP a, bool inConflict);

  /**

   * Marks a the constraint c as being entailed by a.

   * The reason has to do with integer reasoning.

   *

   * After calling impliedByIntHole(), the caller should either raise a conflict

   * or try call tryToPropagate().

   */

  void impliedByIntHole(const ConstraintCPVec& b, bool inConflict);

  /**

   * This is a lemma of the form:

   *   x < d or x = d or x > d

   * The current constraint c is one of the above constraints and {a,b}

   * are the negation of the other two constraints.

   *

   * Preconditions:

   * - negationHasProof() == inConflict.

   *

   * After calling impliedByTrichotomy(), the caller should either raise a conflict

   * or try call tryToPropagate().

   */

  void impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool inConflict);

  /**

   * Marks the node as having a Farkas proof.

   *

   * Preconditions:

   * - coeffs == NULL if proofs are off.

   * - See the comments for ConstraintRule for the form of coeffs when

   *   proofs are on.

   * - negationHasProof() == inConflict.

   *

   * After calling impliedByFarkas(), the caller should either raise a conflict

   * or try call tryToPropagate().

   */

  void impliedByFarkas(const ConstraintCPVec& b, RationalVectorCP coeffs, bool inConflict);

  /**

   * Generates an implication node, B => getLiteral(),

   * where B is the result of externalExplainByAssertions(b).

   * Does not guarantee b is the explanation of the constraint.

   */

  Node externalImplication(const ConstraintCPVec& b) const;

  /**

   * Returns true if the variable is assigned the value dr,

   * the constraint would be satisfied.

   */

  bool satisfiedBy(const DeltaRational& dr) const;

  /**

   * The node must have a proof already and be eligible for propagation!

   * You probably want to call tryToPropagate() instead.

   *

   * Preconditions:

   * - hasProof()

   * - canBePropagated()

   * - !assertedToTheTheory()

   */

  void propagate();

  /**

   * If the constraint

   *   canBePropagated() and

   *   !assertedToTheTheory(),

   * the constraint is added to the database's propagation queue.

   *

   * Precondition:

   * - hasProof()

   */

  void tryToPropagate();

  /**

   * Returns a reference to the containing database.

   * Precondition: the constraint must be initialized.

   */

  const ConstraintDatabase& getDatabase() const;

  /** Returns the constraint rule at the position. */

  const ConstraintRule& getConstraintRule() const;

 private:

  /**  Returns true if the constraint has been initialized. */

  bool initialized() const;

  /**

   * This initializes the fields that cannot be set in the constructor due to

   * circular dependencies.

   */

  void initialize(ConstraintDatabase* db,

                  SortedConstraintMapIterator v,

                  ConstraintP negation);

  class ConstraintRuleCleanup

  {

   public:

    {

      {

        {

        }

      }

  };

  class CanBePropagatedCleanup

  {

   public:

    {

  };

  class AssertionOrderCleanup

  {

   public:

    {

  };

  class SplitCleanup

  {

   public:

    {

  };

  /**

   * Returns true if the node is safe to garbage collect.

   * Both it and its negation must have no context dependent data set.

   */

  bool safeToGarbageCollect() const;

  /**

   * Returns true if the constraint has no context dependent data set.

   */

  bool contextDependentDataIsSet() const;

  /**

   * Returns true if the node correctly corresponds to the constraint that is

   * being set.

   */

  bool sanityChecking(Node n) const;

  /** Returns a reference to the map for d_variable. */

  SortedConstraintMap& constraintSet() const;

  /** Returns coefficients for the proofs for farkas cancellation. */

  static std::pair<int, int> unateFarkasSigns(ConstraintCP a, ConstraintCP b);

  Node externalExplain(AssertionOrder order) const;

  /**

   * Returns an explanation of that was assertedBefore(order).

   * The constraint must have a proof.

   * The constraint cannot be selfExplaining().

   *

   * This is the minimum fringe of the implication tree

   * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof().

   */

  std::shared_ptr<ProofNode> externalExplain(NodeBuilder& nb,

                                             AssertionOrder order) const;

  static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order);

  }

  }

  {

  }

  void debugPrint() const;

  /**

   * The proof of the node is empty.

   * The proof must be a special proof. Either

   *   isSelfExplaining() or

   *    hasEqualityEngineProof()

   */

  bool antecentListIsEmpty() const;

  bool antecedentListLengthIsOne() const;

  /** Return true if every element in b has a proof. */

  static bool allHaveProof(const ConstraintCPVec& b);

  /** Precondition: hasFarkasProof()

   * Computes the combination implied by the farkas coefficients. Sees if it is

   * a contradiction.

   */

  bool wellFormedFarkasProof() const;

  /** The ArithVar associated with the constraint. */

  const ArithVar d_variable;

  /** The type of the Constraint. */

  const ConstraintType d_type;

  /** The DeltaRational value with the constraint. */

  const DeltaRational d_value;

  /** A pointer to the associated database for the Constraint. */

  ConstraintDatabase* d_database;

  /**

   * The node to be communicated with the TheoryEngine.

   *

   * This is not context dependent, but may be set once.

   *

   * This must be set if the constraint canBePropagated().

   * This must be set if the constraint assertedToTheTheory().

   * Otherwise, this may be null().

   */

  Node d_literal;

  /** Pointer to the negation of the Constraint. */

  ConstraintP d_negation;

  /**

   * This is true if the associated node can be propagated.

   *

   * This should be enabled if the node has been preregistered.

   *

   * Sat Context Dependent.

   * This is initially false.

   */

  bool d_canBePropagated;

  /**

   * This is the order the constraint was asserted to the theory.

   * If this has been set, the node can be used in conflicts.

   * If this is c.d_assertedOrder < d.d_assertedOrder, then c can be used in the

   * explanation of d.

   *

   * This should be set after the literal is dequeued by Theory::get().

   *

   * Sat Context Dependent.

   * This is initially AssertionOrderSentinel.

   */

  AssertionOrder d_assertionOrder;

  /**

   * This is guaranteed to be on the fact queue.

   * For example if x + y = x + 1 is on the fact queue, then use this

   */

  TNode d_witness;

  /**

   * The position of the constraint in the constraint rule id.

   *

   * Sat Context Dependent.

   * This is initially

   */

  ConstraintRuleID d_crid;

  /**

   * True if the equality has been split.

   * Only meaningful if ConstraintType == Equality.

   *

   * User Context Dependent.

   * This is initially false.

   */

  bool d_split;

  /**

   * Position in sorted constraint set for the variable.

   * Unset if d_type is Disequality.

   */

  SortedConstraintMapIterator d_variablePosition;

  /** Whether to produce proofs, */

  bool d_produceProofs;

}; /* class ConstraintValue */

std::ostream& operator<<(std::ostream& o, const Constraint& c);

std::ostream& operator<<(std::ostream& o, const ConstraintP c);

std::ostream& operator<<(std::ostream& o, const ConstraintCP c);

std::ostream& operator<<(std::ostream& o, const ConstraintType t);

std::ostream& operator<<(std::ostream& o, const ValueCollection& c);

std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v);

std::ostream& operator<<(std::ostream& o, const ArithProofType);

class ConstraintDatabase : protected EnvObj

{

 private:

  /**

   * The map from ArithVars to their unique databases.

   * When the vector changes size, we cannot allow the maps to move so this

   * is a vector of pointers.

   */

  std::vector<PerVariableDatabase*> d_varDatabases;

  SortedConstraintMap& getVariableSCM(ArithVar v) const;

  /** Maps literals to constraints.*/

  NodetoConstraintMap d_nodetoConstraintMap;

  /**

   * A queue of propagated constraints.

   * ConstraintCP are pointers.

   * The elements of the queue do not require destruction.

   */

  context::CDQueue<ConstraintCP> d_toPropagate;

  /**

   * Proofs are lists of valid constraints terminated by the first null

   * sentinel value in the proof list.

   * We abbreviate d_antecedents as ans in the comment.

   *

   * The proof at p in ans[p] of length n is

   *  (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p])

   *

   * The proof at p corresponds to the conjunction:

   *  (and x_i)

   *

   * So the proof of a Constraint c corresponds to the horn clause:

   *  (implies (and x_i) c)

   * where (and x_i) is the proof at c.d_crid d_antecedentEnd.

   *

   * Constraints are pointers so this list is designed not to require any destruction.

   */

  CDConstraintList d_antecedents;

  typedef context::CDList<ConstraintRule, Constraint::ConstraintRuleCleanup> ConstraintRuleList;

  typedef context::CDList<ConstraintP, Constraint::CanBePropagatedCleanup> CBPList;

  typedef context::CDList<ConstraintP, Constraint::AssertionOrderCleanup> AOList;

  typedef context::CDList<ConstraintP, Constraint::SplitCleanup> SplitList;

  /**

   * The watch lists are collected together as they need to be garbage collected

   * carefully.

   */

    /**

     * Contains the exact list of constraints that have a proof.

     * Upon pop, this unsets d_crid to NoAP.

     *

     * The index in this list is the proper ordering of the proofs.

     */

    ConstraintRuleList d_constraintProofs;

    /**

     * Contains the exact list of constraints that can be used for propagation.

     */

    CBPList d_canBePropagatedWatches;

    /**

     * Contains the exact list of constraints that have been asserted to the theory.

     */

    AOList d_assertionOrderWatches;

    /**

     * Contains the exact list of atoms that have been preregistered.

     * This is a pointer as it must be destroyed before the elements of

     * d_varDatabases.

     */

    SplitList d_splitWatches;

    Watches(context::Context* satContext, context::Context* userContext);

  };

  Watches* d_watches;

  void pushSplitWatch(ConstraintP c);

  void pushCanBePropagatedWatch(ConstraintP c);

  void pushAssertionOrderWatch(ConstraintP c, TNode witness);

  /** Assumes that antecedents have already been pushed. */

  void pushConstraintRule(const ConstraintRule& crp);

  /** Returns true if all of the entries of the vector are empty. */

  static bool emptyDatabase(const std::vector<PerVariableDatabase>& vec);

  /** Map from nodes to arithvars. */

  const ArithVariables& d_avariables;

  }

  ArithCongruenceManager& d_congruenceManager;

  /** Owned by the TheoryArithPrivate, used here. */

  EagerProofGenerator* d_pfGen;

  /** Owned by the TheoryArithPrivate, used here. */

  ProofNodeManager* d_pnm;

  RaiseConflict d_raiseConflict;

  const Rational d_one;

  const Rational d_negOne;

  friend class Constraint;

 public:

  ConstraintDatabase(Env& env,

                     const ArithVariables& variables,

                     ArithCongruenceManager& dm,

                     RaiseConflict conflictCallBack,

                     EagerProofGenerator* pfGen);

  ~ConstraintDatabase();

  /** Adds a literal to the database. */

  ConstraintP addLiteral(TNode lit);

  /**

   * If hasLiteral() is true, returns the constraint.

   * Otherwise, returns NullConstraint.

   */

  ConstraintP lookup(TNode literal) const;

  /**

   * Returns true if the literal has been added to the database.

   * This is a hash table lookup.

   * It does not look in the database for an equivalent corresponding constraint.

   */

  bool hasLiteral(TNode literal) const;