Head

GCC Code Coverage Report

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