Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/simplex_update.cpp	Lines:	1	116	0.9 %
Date:	2021-08-03	Branches:	2	321	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 {


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