Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/simplex.h	Lines:	2	14	14.3 %
Date:	2021-09-18	Branches:	0	2	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Gereon Kremer, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * This is an implementation of the Simplex Module for the Simplex for
 * DPLL(T) decision procedure.
 *
 * This implements the Simplex module for the Simpelx for DPLL(T) decision
 * procedure.
 * See the Simplex for DPLL(T) technical report for more background.(citation?)
 * This shares with the theory a Tableau, and a PartialModel that:
 *  - satisfies the equalities in the Tableau, and
 *  - the assignment for the non-basic variables satisfies their bounds.
 * This is required to either produce a conflict or satisifying PartialModel.
 * Further, we require being told when a basic variable updates its value.
 *
 * During the Simplex search we maintain a queue of variables.
 * The queue is required to contain all of the basic variables that voilate
 * their bounds.
 * As elimination from the queue is more efficient to be done lazily,
 * we do not maintain that the queue of variables needs to be only basic
 * variables or only variables that satisfy their bounds.
 *
 * The simplex procedure roughly follows Alberto's thesis. (citation?)
 * There is one round of selecting using a heuristic pivoting rule.
 * (See PreferenceFunction Documentation for the available options.)
 * The non-basic variable is the one that appears in the fewest pivots.
 * (Bruno says that Leonardo invented this first.)
 * After this, Bland's pivot rule is invoked.
 *
 * During this proccess, we periodically inspect the queue of variables to
 * 1) remove now extraneous extries,
 * 2) detect conflicts that are "waiting" on the queue but may not be detected
 *    by the current queue heuristics, and
 * 3) detect multiple conflicts.
 *
 * Conflicts are greedily slackened to use the weakest bounds that still
 * produce the conflict.
 *
 * Extra things tracked atm: (Subject to change at Tim's whims)
 * - A superset of all of the newly pivoted variables.
 * - A queue of additional conflicts that were discovered by Simplex.
 *   These are theory valid and are currently turned into lemmas
 */

#include "cvc5_private.h"

#pragma once

#include <unordered_map>

#include "options/arith_options.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/partial_model.h"
#include "util/dense_map.h"
#include "util/result.h"
#include "util/statistics_stats.h"

namespace cvc5 {
namespace theory {
namespace arith {

class ErrorSet;
class LinearEqualityModule;
class Tableau;

class SimplexDecisionProcedure {
protected:
  typedef std::vector< std::pair<ArithVar, int> > AVIntPairVec;

  /** Pivot count of the current round of pivoting. */
  uint32_t d_pivots;

  /** The set of variables that are in conflict in this round. */
  DenseSet d_conflictVariables;

  /** The rule to use for heuristic selection mode. */
  options::ErrorSelectionRule d_heuristicRule;

  /** Linear equality module. */
  LinearEqualityModule& d_linEq;

  /**
   * Manages information about the assignment and upper and lower bounds on
   * variables.
   * Partial model matches that in LinearEqualityModule.
   */
  ArithVariables& d_variables;

  /**
   * Stores the linear equalities used by Simplex.
   * Tableau from the LinearEquality module.
   */
  Tableau& d_tableau;

  /** Contains a superset of the basic variables in violation of their bounds. */
  ErrorSet& d_errorSet;

  /** Number of variables in the system. This is used for tuning heuristics. */
  ArithVar d_numVariables;

  /** This is the call back channel for Simplex to report conflicts. */
  RaiseConflict d_conflictChannel;

  /** This is the call back channel for Simplex to report conflicts. */
  FarkasConflictBuilder* d_conflictBuilder;

  /** Used for requesting d_opt, bound and error variables for primal.*/
  TempVarMalloc d_arithVarMalloc;

  /** The size of the error set. */
  uint32_t d_errorSize;

  /** A local copy of 0. */
  const Rational d_zero;

  /** A local copy of 1. */
  const Rational d_posOne;

  /** A local copy of -1. */
  const Rational d_negOne;

  /**
   * Locally cached value of arithStandardCheckVarOrderPivots option. It is
   * cached here to allow for single runs with a different (lower) limit.
   */
  int64_t d_varOrderPivotLimit = -1;

  ArithVar constructInfeasiblityFunction(TimerStat& timer);
  ArithVar constructInfeasiblityFunction(TimerStat& timer, ArithVar e);
  ArithVar constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set);

  void tearDownInfeasiblityFunction(TimerStat& timer, ArithVar inf);
  void adjustInfeasFunc(TimerStat& timer, ArithVar inf, const AVIntPairVec& focusChanges);
  void addToInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e);
  void removeFromInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e);
  void shrinkInfeasFunc(TimerStat& timer, ArithVar inf, const ArithVarVec& dropped);

public:
  SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
  virtual ~SimplexDecisionProcedure();

  /**
   * Tries to update the assignments of variables such that all of the
   * assignments are consistent with their bounds.
   * This is done by a simplex search through the possible bases of the tableau.
   *
   * If all of the variables can be made consistent with their bounds
   * SAT is returned. Otherwise UNSAT is returned, and at least 1 conflict
   * was reported on the conflictCallback passed to the Module.
   *
   * Tableau pivoting is performed so variables may switch from being basic to
   * nonbasic and vice versa.
   *
   * Corresponds to the "check()" procedure in [Cav06].
   */
  virtual Result::Sat findModel(bool exactResult) = 0;

  void increaseMax() { d_numVariables++; }


  uint32_t getPivots() const { return d_pivots; }

  /** Set the variable ordering pivot limit */
  void setVarOrderPivotLimit(int64_t value) { d_varOrderPivotLimit = value; }

 protected:

  /** Reports a conflict to on the output channel. */
  void reportConflict(ArithVar basic);

  /**
   * Checks a basic variable, b, to see if it is in conflict.
   * If a conflict is discovered a node summarizing the conflict is returned.
   * Otherwise, Node::null() is returned.
   */
  bool maybeGenerateConflictForBasic(ArithVar basic) const;

  /** Returns true if a tracked basic variable has a conflict on it. */
  bool checkBasicForConflict(ArithVar b) const;

  /**
   * If a basic variable has a conflict on its row,
   * this produces a minimized row on the conflict channel.
   */
  ConstraintCP generateConflictForBasic(ArithVar basic) const;


  /** Gets a fresh variable from TheoryArith. */
  ArithVar requestVariable(){
    return d_arithVarMalloc.request();
  }

  /** Releases a requested variable from TheoryArith.*/
  void releaseVariable(ArithVar v){
    d_arithVarMalloc.release(v);
  }

  /** Post condition: !d_queue.moreSignals() */
  bool standardProcessSignals(TimerStat &timer, IntStat& conflictStat);

  struct ArithVarIntPairHashFunc {
    size_t operator()(const std::pair<ArithVar, int>& p) const {
      size_t h1 = std::hash<ArithVar>()(p.first);
      size_t h2 = std::hash<int>()(p.second);
      return h1 + 3389 * h2;
    }
  };

  typedef std::unordered_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table;

  static inline int determinizeSgn(int sgn){
    return sgn < 0 ? -1 : (sgn == 0 ? 0 : 1);
  }

  void addSgn(sgn_table& sgns, ArithVar col, int sgn, ArithVar basic);
  void addRowSgns(sgn_table& sgns, ArithVar basic, int norm);
  ArithVar find_basic_in_sgns(const sgn_table& sgns, ArithVar col, int sgn, const DenseSet& m, bool inside);

  sgn_table::const_iterator find_sgns(const sgn_table& sgns, ArithVar col, int sgn);

};/* class SimplexDecisionProcedure */

}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Gereon Kremer, 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 <unordered_map>
59
60		#include "options/arith_options.h"
61		#include "theory/arith/arithvar.h"
62		#include "theory/arith/partial_model.h"
63		#include "util/dense_map.h"
64		#include "util/result.h"
65		#include "util/statistics_stats.h"
66
67		namespace cvc5 {
68		namespace theory {
69		namespace arith {
70
71		class ErrorSet;
72		class LinearEqualityModule;
73		class Tableau;
74
75		class SimplexDecisionProcedure {
76		protected:
77		typedef std::vector< std::pair<ArithVar, int> > AVIntPairVec;
78
79		/** Pivot count of the current round of pivoting. */
80		uint32_t d_pivots;
81
82		/** The set of variables that are in conflict in this round. */
83		DenseSet d_conflictVariables;
84
85		/** The rule to use for heuristic selection mode. */
86		options::ErrorSelectionRule d_heuristicRule;
87
88		/** Linear equality module. */
89		LinearEqualityModule& d_linEq;
90
91		/**
92		* Manages information about the assignment and upper and lower bounds on
93		* variables.
94		* Partial model matches that in LinearEqualityModule.
95		*/
96		ArithVariables& d_variables;
97
98		/**
99		* Stores the linear equalities used by Simplex.
100		* Tableau from the LinearEquality module.
101		*/
102		Tableau& d_tableau;
103
104		/** Contains a superset of the basic variables in violation of their bounds. */
105		ErrorSet& d_errorSet;
106
107		/** Number of variables in the system. This is used for tuning heuristics. */
108		ArithVar d_numVariables;
109
110		/** This is the call back channel for Simplex to report conflicts. */
111		RaiseConflict d_conflictChannel;
112
113		/** This is the call back channel for Simplex to report conflicts. */
114		FarkasConflictBuilder* d_conflictBuilder;
115
116		/** Used for requesting d_opt, bound and error variables for primal.*/
117		TempVarMalloc d_arithVarMalloc;
118
119		/** The size of the error set. */
120		uint32_t d_errorSize;
121
122		/** A local copy of 0. */
123		const Rational d_zero;
124
125		/** A local copy of 1. */
126		const Rational d_posOne;
127
128		/** A local copy of -1. */
129		const Rational d_negOne;
130
131		/**
132		* Locally cached value of arithStandardCheckVarOrderPivots option. It is
133		* cached here to allow for single runs with a different (lower) limit.
134		*/
135		int64_t d_varOrderPivotLimit = -1;
136
137		ArithVar constructInfeasiblityFunction(TimerStat& timer);
138		ArithVar constructInfeasiblityFunction(TimerStat& timer, ArithVar e);
139		ArithVar constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set);
140
141		void tearDownInfeasiblityFunction(TimerStat& timer, ArithVar inf);
142		void adjustInfeasFunc(TimerStat& timer, ArithVar inf, const AVIntPairVec& focusChanges);
143		void addToInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e);
144		void removeFromInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e);
145		void shrinkInfeasFunc(TimerStat& timer, ArithVar inf, const ArithVarVec& dropped);
146
147		public:
148		SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
149		virtual ~SimplexDecisionProcedure();
150
151		/**
152		* Tries to update the assignments of variables such that all of the
153		* assignments are consistent with their bounds.
154		* This is done by a simplex search through the possible bases of the tableau.
155		*
156		* If all of the variables can be made consistent with their bounds
157		* SAT is returned. Otherwise UNSAT is returned, and at least 1 conflict
158		* was reported on the conflictCallback passed to the Module.
159		*
160		* Tableau pivoting is performed so variables may switch from being basic to
161		* nonbasic and vice versa.
162		*
163		* Corresponds to the "check()" procedure in [Cav06].
164		*/
165		virtual Result::Sat findModel(bool exactResult) = 0;
166
167	165282	void increaseMax() { d_numVariables++; }
168
169
170	1789149	uint32_t getPivots() const { return d_pivots; }
171
172		/** Set the variable ordering pivot limit */
173		void setVarOrderPivotLimit(int64_t value) { d_varOrderPivotLimit = value; }
174
175		protected:
176
177		/** Reports a conflict to on the output channel. */
178		void reportConflict(ArithVar basic);
179
180		/**
181		* Checks a basic variable, b, to see if it is in conflict.
182		* If a conflict is discovered a node summarizing the conflict is returned.
183		* Otherwise, Node::null() is returned.
184		*/
185		bool maybeGenerateConflictForBasic(ArithVar basic) const;
186
187		/** Returns true if a tracked basic variable has a conflict on it. */
188		bool checkBasicForConflict(ArithVar b) const;
189
190		/**
191		* If a basic variable has a conflict on its row,
192		* this produces a minimized row on the conflict channel.
193		*/
194		ConstraintCP generateConflictForBasic(ArithVar basic) const;
195
196
197		/** Gets a fresh variable from TheoryArith. */
198		ArithVar requestVariable(){
199		return d_arithVarMalloc.request();
200		}
201
202		/** Releases a requested variable from TheoryArith.*/
203		void releaseVariable(ArithVar v){
204		d_arithVarMalloc.release(v);
205		}
206
207		/** Post condition: !d_queue.moreSignals() */
208		bool standardProcessSignals(TimerStat &timer, IntStat& conflictStat);
209
210		struct ArithVarIntPairHashFunc {
211		size_t operator()(const std::pair<ArithVar, int>& p) const {
212		size_t h1 = std::hash<ArithVar>()(p.first);
213		size_t h2 = std::hash<int>()(p.second);
214		return h1 + 3389 * h2;
215		}
216		};
217
218		typedef std::unordered_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table;
219
220		static inline int determinizeSgn(int sgn){
221		return sgn < 0 ? -1 : (sgn == 0 ? 0 : 1);
222		}
223
224		void addSgn(sgn_table& sgns, ArithVar col, int sgn, ArithVar basic);
225		void addRowSgns(sgn_table& sgns, ArithVar basic, int norm);
226		ArithVar find_basic_in_sgns(const sgn_table& sgns, ArithVar col, int sgn, const DenseSet& m, bool inside);
227
228		sgn_table::const_iterator find_sgns(const sgn_table& sgns, ArithVar col, int sgn);
229
230		};/* class SimplexDecisionProcedure */
231
232		} // namespace arith
233		} // namespace theory
234		} // namespace cvc5