Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/simplex_update.cpp	Lines:	1	118	0.8 %
Date:	2021-09-16	Branches:	2	323	0.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King
 *
 * 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 implements the UpdateInfo.
 */

#include "theory/arith/simplex_update.h"

#include "theory/arith/constraint.h"

using namespace std;

namespace cvc5 {
namespace theory {
namespace arith {

/*
 * Generates a string representation of std::optional and inserts it into a
 * stream.
 *
 * Note: We define this function here in the cvc5::theory::arith namespace,
 * because it would otherwise not be found for std::optional<int>. This is due
 * to the argument-dependent lookup rules.
 *
 * @param out The stream
 * @param m The value
 * @return The stream
 */
std::ostream& operator<<(std::ostream& out, const std::optional<int>& m)
{
  return cvc5::operator<<(out, m);
}

UpdateInfo::UpdateInfo():
  d_nonbasic(ARITHVAR_SENTINEL),
  d_nonbasicDirection(0),
  d_nonbasicDelta(),
  d_foundConflict(false),
  d_errorsChange(),
  d_focusDirection(),
  d_tableauCoefficient(),
  d_limiting(NullConstraint),
  d_witness(AntiProductive)
{}

UpdateInfo::UpdateInfo(ArithVar nb, int dir):
  d_nonbasic(nb),
  d_nonbasicDirection(dir),
  d_nonbasicDelta(),
  d_foundConflict(false),
  d_errorsChange(),
  d_focusDirection(),
  d_tableauCoefficient(),
  d_limiting(NullConstraint),
  d_witness(AntiProductive)
{
  Assert(dir == 1 || dir == -1);
}

UpdateInfo::UpdateInfo(bool conflict, ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP c):
  d_nonbasic(nb),
  d_nonbasicDirection(delta.sgn()),
  d_nonbasicDelta(delta),
  d_foundConflict(true),
  d_errorsChange(),
  d_focusDirection(),
  d_tableauCoefficient(&r),
  d_limiting(c),
  d_witness(ConflictFound)
{
  Assert(conflict);
}

UpdateInfo UpdateInfo::conflict(ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP lim){
  return UpdateInfo(true, nb, delta, r, lim);
}

void UpdateInfo::updateUnbounded(const DeltaRational& delta, int ec, int f){
  d_limiting = NullConstraint;
  d_nonbasicDelta = delta;
  d_errorsChange = ec;
  d_focusDirection = f;
  d_tableauCoefficient.reset();
  updateWitness();
  Assert(unbounded());
  Assert(improvement(d_witness));
  Assert(!describesPivot());
  Assert(debugSgnAgreement());
}
void UpdateInfo::updatePureFocus(const DeltaRational& delta, ConstraintP c){
  d_limiting = c;
  d_nonbasicDelta = delta;
  d_errorsChange.reset();
  d_focusDirection = 1;
  d_tableauCoefficient.reset();
  updateWitness();
  Assert(!describesPivot());
  Assert(improvement(d_witness));
  Assert(debugSgnAgreement());
}

void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, ConstraintP c){
  d_limiting = c;
  d_nonbasicDelta = delta;
  d_errorsChange.reset();
  d_focusDirection.reset();
  updateWitness();
  Assert(describesPivot());
  Assert(debugSgnAgreement());
}

void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, ConstraintP c, int ec){
  d_limiting = c;
  d_nonbasicDelta = delta;
  d_errorsChange = ec;
  d_focusDirection.reset();
  d_tableauCoefficient = &r;
  updateWitness();
  Assert(describesPivot());
  Assert(debugSgnAgreement());
}

void UpdateInfo::witnessedUpdate(const DeltaRational& delta, ConstraintP c, int ec, int fd){
  d_limiting = c;
  d_nonbasicDelta = delta;
  d_errorsChange = ec;
  d_focusDirection = fd;
  d_tableauCoefficient.reset();
  updateWitness();
  Assert(describesPivot() || improvement(d_witness));
  Assert(debugSgnAgreement());
}

void UpdateInfo::update(const DeltaRational& delta, const Rational& r, ConstraintP c, int ec, int fd){
  d_limiting = c;
  d_nonbasicDelta = delta;
  d_errorsChange = ec;
  d_focusDirection = fd;
  d_tableauCoefficient = &r;
  updateWitness();
  Assert(describesPivot() || improvement(d_witness));
  Assert(debugSgnAgreement());
}

bool UpdateInfo::describesPivot() const {
  return !unbounded() && d_nonbasic != d_limiting->getVariable();
}

void UpdateInfo::output(std::ostream& out) const{
  out << "{UpdateInfo"
      << ", nb = " << d_nonbasic
      << ", dir = " << d_nonbasicDirection
      << ", delta = " << d_nonbasicDelta
      << ", conflict = " << d_foundConflict
      << ", errorChange = " << d_errorsChange
      << ", focusDir = " << d_focusDirection
      << ", witness = " << d_witness
      << ", limiting = " << d_limiting
      << "}";
}

ArithVar UpdateInfo::leaving() const{
  Assert(describesPivot());

  return d_limiting->getVariable();
}

std::ostream& operator<<(std::ostream& out, const UpdateInfo& up){
  up.output(out);
  return out;
}


std::ostream& operator<<(std::ostream& out,  WitnessImprovement w){
  switch(w){
  case ConflictFound:
    out << "ConflictFound"; break;
  case ErrorDropped:
    out << "ErrorDropped"; break;
  case FocusImproved:
    out << "FocusImproved"; break;
  case FocusShrank:
    out << "FocusShrank"; break;
  case Degenerate:
    out << "Degenerate"; break;
  case BlandsDegenerate:
    out << "BlandsDegenerate"; break;
  case HeuristicDegenerate:
    out << "HeuristicDegenerate"; break;
  case AntiProductive:
    out << "AntiProductive"; break;
  }
  return out;
}

}  // 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
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 implements the UpdateInfo.
14		*/
15
16		#include "theory/arith/simplex_update.h"
17
18		#include "theory/arith/constraint.h"
19
20		using namespace std;
21
22		namespace cvc5 {
23		namespace theory {
24		namespace arith {
25
26		/*
27		* Generates a string representation of std::optional and inserts it into a
28		* stream.
29		*
30		* Note: We define this function here in the cvc5::theory::arith namespace,
31		* because it would otherwise not be found for std::optional<int>. This is due
32		* to the argument-dependent lookup rules.
33		*
34		* @param out The stream
35		* @param m The value
36		* @return The stream
37		*/
38		std::ostream& operator<<(std::ostream& out, const std::optional<int>& m)
39		{
40		return cvc5::operator<<(out, m);
41		}
42
43		UpdateInfo::UpdateInfo():
44		d_nonbasic(ARITHVAR_SENTINEL),
45		d_nonbasicDirection(0),
46		d_nonbasicDelta(),
47		d_foundConflict(false),
48		d_errorsChange(),
49		d_focusDirection(),
50		d_tableauCoefficient(),
51		d_limiting(NullConstraint),
52		d_witness(AntiProductive)
53		{}
54
55		UpdateInfo::UpdateInfo(ArithVar nb, int dir):
56		d_nonbasic(nb),
57		d_nonbasicDirection(dir),
58		d_nonbasicDelta(),
59		d_foundConflict(false),
60		d_errorsChange(),
61		d_focusDirection(),
62		d_tableauCoefficient(),
63		d_limiting(NullConstraint),
64		d_witness(AntiProductive)
65		{
66		Assert(dir == 1 \|\| dir == -1);
67		}
68
69		UpdateInfo::UpdateInfo(bool conflict, ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP c):
70		d_nonbasic(nb),
71		d_nonbasicDirection(delta.sgn()),
72		d_nonbasicDelta(delta),
73		d_foundConflict(true),
74		d_errorsChange(),
75		d_focusDirection(),
76		d_tableauCoefficient(&r),
77		d_limiting(c),
78		d_witness(ConflictFound)
79		{
80		Assert(conflict);
81		}
82
83		UpdateInfo UpdateInfo::conflict(ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP lim){
84		return UpdateInfo(true, nb, delta, r, lim);
85		}
86
87		void UpdateInfo::updateUnbounded(const DeltaRational& delta, int ec, int f){
88		d_limiting = NullConstraint;
89		d_nonbasicDelta = delta;
90		d_errorsChange = ec;
91		d_focusDirection = f;
92		d_tableauCoefficient.reset();
93		updateWitness();
94		Assert(unbounded());
95		Assert(improvement(d_witness));
96		Assert(!describesPivot());
97		Assert(debugSgnAgreement());
98		}
99		void UpdateInfo::updatePureFocus(const DeltaRational& delta, ConstraintP c){
100		d_limiting = c;
101		d_nonbasicDelta = delta;
102		d_errorsChange.reset();
103		d_focusDirection = 1;
104		d_tableauCoefficient.reset();
105		updateWitness();
106		Assert(!describesPivot());
107		Assert(improvement(d_witness));
108		Assert(debugSgnAgreement());
109		}
110
111		void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, ConstraintP c){
112		d_limiting = c;
113		d_nonbasicDelta = delta;
114		d_errorsChange.reset();
115		d_focusDirection.reset();
116		updateWitness();
117		Assert(describesPivot());
118		Assert(debugSgnAgreement());
119		}
120
121		void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, ConstraintP c, int ec){
122		d_limiting = c;
123		d_nonbasicDelta = delta;
124		d_errorsChange = ec;
125		d_focusDirection.reset();
126		d_tableauCoefficient = &r;
127		updateWitness();
128		Assert(describesPivot());
129		Assert(debugSgnAgreement());
130		}
131
132		void UpdateInfo::witnessedUpdate(const DeltaRational& delta, ConstraintP c, int ec, int fd){
133		d_limiting = c;
134		d_nonbasicDelta = delta;
135		d_errorsChange = ec;
136		d_focusDirection = fd;
137		d_tableauCoefficient.reset();
138		updateWitness();
139		Assert(describesPivot() \|\| improvement(d_witness));
140		Assert(debugSgnAgreement());
141		}
142
143		void UpdateInfo::update(const DeltaRational& delta, const Rational& r, ConstraintP c, int ec, int fd){
144		d_limiting = c;
145		d_nonbasicDelta = delta;
146		d_errorsChange = ec;
147		d_focusDirection = fd;
148		d_tableauCoefficient = &r;
149		updateWitness();
150		Assert(describesPivot() \|\| improvement(d_witness));
151		Assert(debugSgnAgreement());
152		}
153
154		bool UpdateInfo::describesPivot() const {
155		return !unbounded() && d_nonbasic != d_limiting->getVariable();
156		}
157
158		void UpdateInfo::output(std::ostream& out) const{
159		out << "{UpdateInfo"
160		<< ", nb = " << d_nonbasic
161		<< ", dir = " << d_nonbasicDirection
162		<< ", delta = " << d_nonbasicDelta
163		<< ", conflict = " << d_foundConflict
164		<< ", errorChange = " << d_errorsChange
165		<< ", focusDir = " << d_focusDirection
166		<< ", witness = " << d_witness
167		<< ", limiting = " << d_limiting
168		<< "}";
169		}
170
171		ArithVar UpdateInfo::leaving() const{
172		Assert(describesPivot());
173
174		return d_limiting->getVariable();
175		}
176
177		std::ostream& operator<<(std::ostream& out, const UpdateInfo& up){
178		up.output(out);
179		return out;
180		}
181
182
183		std::ostream& operator<<(std::ostream& out, WitnessImprovement w){
184		switch(w){
185		case ConflictFound:
186		out << "ConflictFound"; break;
187		case ErrorDropped:
188		out << "ErrorDropped"; break;
189		case FocusImproved:
190		out << "FocusImproved"; break;
191		case FocusShrank:
192		out << "FocusShrank"; break;
193		case Degenerate:
194		out << "Degenerate"; break;
195		case BlandsDegenerate:
196		out << "BlandsDegenerate"; break;
197		case HeuristicDegenerate:
198		out << "HeuristicDegenerate"; break;
199		case AntiProductive:
200		out << "AntiProductive"; break;
201		}
202		return out;
203		}
204
205		} // namespace arith
206		} // namespace theory
207	29577	} // namespace cvc5