src/theory/arith/attempt_solution_simplex.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Tim King, Morgan Deters, Mathias Preiner
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * This is an implementation of the Simplex Module for the Simplex for
  14  * DPLL(T) decision procedure.
  15  *
  16  * This implements the Simplex module for the Simpelx for DPLL(T) decision
  17  * procedure.
  18  * See the Simplex for DPLL(T) technical report for more background.(citation?)
  19  * This shares with the theory a Tableau, and a PartialModel that:
  20  *  - satisfies the equalities in the Tableau, and
  21  *  - the assignment for the non-basic variables satisfies their bounds.
  22  * This is required to either produce a conflict or satisifying PartialModel.
  23  * Further, we require being told when a basic variable updates its value.
  24  *
  25  * During the Simplex search we maintain a queue of variables.
  26  * The queue is required to contain all of the basic variables that voilate
  27  * their bounds.
  28  * As elimination from the queue is more efficient to be done lazily,
  29  * we do not maintain that the queue of variables needs to be only basic
  30  * variables or only variables that satisfy their bounds.
  31  *
  32  * The simplex procedure roughly follows Alberto's thesis. (citation?)
  33  * There is one round of selecting using a heuristic pivoting rule.
  34  * (See PreferenceFunction Documentation for the available options.)
  35  * The non-basic variable is the one that appears in the fewest pivots.
  36  * (Bruno says that Leonardo invented this first.)
  37  * After this, Bland's pivot rule is invoked.
  38  *
  39  * During this proccess, we periodically inspect the queue of variables to
  40  * 1) remove now extraneous extries,
  41  * 2) detect conflicts that are "waiting" on the queue but may not be detected
  42  *    by the current queue heuristics, and
  43  * 3) detect multiple conflicts.
  44  *
  45  * Conflicts are greedily slackened to use the weakest bounds that still
  46  * produce the conflict.
  47  *
  48  * Extra things tracked atm: (Subject to change at Tim's whims)
  49  * - A superset of all of the newly pivoted variables.
  50  * - A queue of additional conflicts that were discovered by Simplex.
  51  *   These are theory valid and are currently turned into lemmas
  52  */
  53
  54 #include "cvc5_private.h"
  55
  56 #pragma once
  57
  58 #include "theory/arith/approx_simplex.h"
  59 #include "theory/arith/simplex.h"
  60 #include "util/statistics_stats.h"
  61
  62 namespace cvc5 {
  63 namespace theory {
  64 namespace arith {
  65
  66 class AttemptSolutionSDP : public SimplexDecisionProcedure {
  67 public:
  68  AttemptSolutionSDP(Env& env,
  69                     LinearEqualityModule& linEq,
  70                     ErrorSet& errors,
  71                     RaiseConflict conflictChannel,
  72                     TempVarMalloc tvmalloc);
  73
  74  Result::Sat attempt(const ApproximateSimplex::Solution& sol);
  75
  76  Result::Sat findModel(bool exactResult) override { Unreachable(); }
  77
  78 private:
  79  bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const;
  80
  81  bool processSignals()
  82  {
  83    TimerStat& timer = d_statistics.d_queueTime;
  84    IntStat& conflictStat = d_statistics.d_conflicts;
  85    return standardProcessSignals(timer, conflictStat);
  86   }
  87   /** These fields are designed to be accessible to TheoryArith methods. */
  88   class Statistics {
  89   public:
  90     TimerStat d_searchTime;
  91     TimerStat d_queueTime;
  92     IntStat d_conflicts;
  93
  94     Statistics();
  95   } d_statistics;
  96 };/* class AttemptSolutionSDP */
  97
  98 }  // namespace arith
  99 }  // namespace theory
 100 }  // namespace cvc5