Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/error_set.cpp	Lines:	201	314	64.0 %
Date:	2021-11-07	Branches:	164	617	26.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "theory/arith/error_set.h"

#include "smt/smt_statistics_registry.h"
#include "theory/arith/constraint.h"

using namespace std;

namespace cvc5 {
namespace theory {
namespace arith {

ErrorInformation::ErrorInformation()
    : d_variable(ARITHVAR_SENTINEL),
      d_violated(NullConstraint),
      d_sgn(0),
      d_relaxed(false),
      d_inFocus(false),
      d_handle(),
      d_amount(nullptr),
      d_metric(0)
{
  Debug("arith::error::mem")
      << "def constructor " << d_variable << " " << d_amount.get() << endl;
}

ErrorInformation::ErrorInformation(ArithVar var, ConstraintP vio, int sgn)
    : d_variable(var),
      d_violated(vio),
      d_sgn(sgn),
      d_relaxed(false),
      d_inFocus(false),
      d_handle(),
      d_amount(nullptr),
      d_metric(0)
{
  Assert(debugInitialized());
  Debug("arith::error::mem")
      << "constructor " << d_variable << " " << d_amount.get() << endl;
}


ErrorInformation::~ErrorInformation() {
  Assert(d_relaxed != true);
  if (d_amount != nullptr)
  {
    Debug("arith::error::mem") << d_amount.get() << endl;
    Debug("arith::error::mem")
        << "destroy " << d_variable << " " << d_amount.get() << endl;
    d_amount = nullptr;
  }
}

ErrorInformation::ErrorInformation(const ErrorInformation& ei)
  : d_variable(ei.d_variable)
  , d_violated(ei.d_violated)
  , d_sgn(ei.d_sgn)
  , d_relaxed(ei.d_relaxed)
  , d_inFocus(ei.d_inFocus)
  , d_handle(ei.d_handle)
  , d_metric(0)
{
  if (ei.d_amount == nullptr)
  {
    d_amount = nullptr;
  }
  else
  {
    d_amount = std::make_unique<DeltaRational>(*ei.d_amount);
  }
  Debug("arith::error::mem")
      << "copy const " << d_variable << " " << d_amount.get() << endl;
}

ErrorInformation& ErrorInformation::operator=(const ErrorInformation& ei){
  d_variable = ei.d_variable;
  d_violated = ei.d_violated;
  d_sgn = ei.d_sgn;
  d_relaxed = (ei.d_relaxed);
  d_inFocus = (ei.d_inFocus);
  d_handle = (ei.d_handle);
  d_metric = ei.d_metric;
  if (d_amount != nullptr && ei.d_amount != nullptr)
  {
    Debug("arith::error::mem")
        << "assignment assign " << d_variable << " " << d_amount.get() << endl;
    *d_amount = *ei.d_amount;
  }
  else if (ei.d_amount != nullptr)
  {
    d_amount = std::make_unique<DeltaRational>(*ei.d_amount);
    Debug("arith::error::mem")
        << "assignment alloc " << d_variable << " " << d_amount.get() << endl;
  }
  else if (d_amount != nullptr)
  {
    Debug("arith::error::mem")
        << "assignment release " << d_variable << " " << d_amount.get() << endl;
    d_amount = nullptr;
  }
  else
  {
    d_amount = nullptr;
  }
  return *this;
}

void ErrorInformation::reset(ConstraintP c, int sgn){
  Assert(!isRelaxed());
  Assert(c != NullConstraint);
  d_violated = c;
  d_sgn = sgn;

  if (d_amount != nullptr)
  {
    Debug("arith::error::mem")
        << "reset " << d_variable << " " << d_amount.get() << endl;
    d_amount = nullptr;
  }
}

void ErrorInformation::setAmount(const DeltaRational& am){
  if (d_amount == nullptr)
  {
    d_amount = std::make_unique<DeltaRational>();
    Debug("arith::error::mem")
        << "setAmount " << d_variable << " " << d_amount.get() << endl;
  }
  (*d_amount) = am;
}

ErrorSet::Statistics::Statistics()
    : d_enqueues(
        smtStatisticsRegistry().registerInt("theory::arith::pqueue::enqueues")),
      d_enqueuesCollection(smtStatisticsRegistry().registerInt(
          "theory::arith::pqueue::enqueuesCollection")),
      d_enqueuesDiffMode(smtStatisticsRegistry().registerInt(
          "theory::arith::pqueue::enqueuesDiffMode")),
      d_enqueuesVarOrderMode(smtStatisticsRegistry().registerInt(
          "theory::arith::pqueue::enqueuesVarOrderMode")),
      d_enqueuesCollectionDuplicates(smtStatisticsRegistry().registerInt(
          "theory::arith::pqueue::enqueuesCollectionDuplicates")),
      d_enqueuesVarOrderModeDuplicates(smtStatisticsRegistry().registerInt(
          "theory::arith::pqueue::enqueuesVarOrderModeDuplicates"))
{
}

ErrorSet::ErrorSet(ArithVariables& vars,
                   TableauSizes tabSizes,
                   BoundCountingLookup lookups)
    : d_variables(vars),
      d_errInfo(),
      d_selectionRule(options::ErrorSelectionRule::VAR_ORDER),
      d_focus(ComparatorPivotRule(this, d_selectionRule)),
      d_outOfFocus(),
      d_signals(),
      d_tableauSizes(tabSizes),
      d_boundLookup(lookups)
{}

options::ErrorSelectionRule ErrorSet::getSelectionRule() const
{
  return d_selectionRule;
}

void ErrorSet::recomputeAmount(ErrorInformation& ei,
                               options::ErrorSelectionRule rule)
{
  switch(rule){
    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
      ei.setAmount(computeDiff(ei.getVariable()));
      break;
    case options::ErrorSelectionRule::SUM_METRIC:
      ei.setMetric(sumMetric(ei.getVariable()));
      break;
    case options::ErrorSelectionRule::VAR_ORDER:
      // do nothing
      break;
  }
}

void ErrorSet::setSelectionRule(options::ErrorSelectionRule rule)
{
  if(rule != getSelectionRule()){
    FocusSet into(ComparatorPivotRule(this, rule));
    FocusSet::const_iterator iter = d_focus.begin();
    FocusSet::const_iterator i_end = d_focus.end();
    for(; iter != i_end; ++iter){
      ArithVar v = *iter;
      ErrorInformation& ei = d_errInfo.get(v);
      if(ei.inFocus()){
        recomputeAmount(ei, rule);
        FocusSetHandle handle = into.push(v);
        ei.setHandle(handle);
      }
    }
    d_focus.swap(into);
    d_selectionRule = rule;
  }
  Assert(getSelectionRule() == rule);
}

ComparatorPivotRule::ComparatorPivotRule(const ErrorSet* es,
                                         options::ErrorSelectionRule r)
    : d_errorSet(es), d_rule(r)
{}

bool ComparatorPivotRule::operator()(ArithVar v, ArithVar u) const {
  switch(d_rule){
    case options::ErrorSelectionRule::VAR_ORDER:
      // This needs to be the reverse of the minVariableOrder
      return v > u;
    case options::ErrorSelectionRule::SUM_METRIC:
    {
      uint32_t v_metric = d_errorSet->getMetric(v);
      uint32_t u_metric = d_errorSet->getMetric(u);
      if(v_metric == u_metric){
        return v > u;
      }else{
        return v_metric > u_metric;
      }
    }
    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
    {
      const DeltaRational& vamt = d_errorSet->getAmount(v);
      const DeltaRational& uamt = d_errorSet->getAmount(u);
      int cmp = vamt.cmp(uamt);
      if(cmp == 0){
        return v > u;
      }else{
        return cmp > 0;
      }
    }
    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
    {
      const DeltaRational& vamt = d_errorSet->getAmount(v);
      const DeltaRational& uamt = d_errorSet->getAmount(u);
      int cmp = vamt.cmp(uamt);
      if(cmp == 0){
        return v > u;
      }else{
        return cmp < 0;
      }
    }
  }
  Unreachable();
}

void ErrorSet::update(ErrorInformation& ei){
  if(ei.inFocus()){

    switch(getSelectionRule()){
      case options::ErrorSelectionRule::MINIMUM_AMOUNT:
      case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
        ei.setAmount(computeDiff(ei.getVariable()));
        d_focus.update(ei.getHandle(), ei.getVariable());
        break;
      case options::ErrorSelectionRule::SUM_METRIC:
        ei.setMetric(sumMetric(ei.getVariable()));
        d_focus.update(ei.getHandle(), ei.getVariable());
        break;
      case options::ErrorSelectionRule::VAR_ORDER:
        // do nothing
        break;
    }
  }
}

/** A variable becomes satisfied. */
void ErrorSet::transitionVariableOutOfError(ArithVar v) {
  Assert(!inconsistent(v));
  ErrorInformation& ei = d_errInfo.get(v);
  Assert(ei.debugInitialized());
  if(ei.isRelaxed()){
    ConstraintP viol = ei.getViolated();
    if(ei.sgn() > 0){
      d_variables.setLowerBoundConstraint(viol);
    }else{
      d_variables.setUpperBoundConstraint(viol);
    }
    Assert(!inconsistent(v));
    ei.setUnrelaxed();
  }
  if(ei.inFocus()){
    d_focus.erase(ei.getHandle());
    ei.setInFocus(false);
  }
  d_errInfo.remove(v);
}


void ErrorSet::transitionVariableIntoError(ArithVar v) {
  Assert(inconsistent(v));
  bool vilb = d_variables.cmpAssignmentLowerBound(v) < 0;
  int sgn = vilb ? 1 : -1;
  ConstraintP c = vilb ?
    d_variables.getLowerBoundConstraint(v) : d_variables.getUpperBoundConstraint(v);
  d_errInfo.set(v, ErrorInformation(v, c, sgn));
  ErrorInformation& ei = d_errInfo.get(v);

  switch(getSelectionRule()){
    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
      ei.setAmount(computeDiff(v));
      break;
    case options::ErrorSelectionRule::SUM_METRIC:
      ei.setMetric(sumMetric(ei.getVariable()));
      break;
    case options::ErrorSelectionRule::VAR_ORDER:
      // do nothing
      break;
  }
  ei.setInFocus(true);
  FocusSetHandle handle = d_focus.push(v);
  ei.setHandle(handle);
}

void ErrorSet::dropFromFocus(ArithVar v) {
  Assert(inError(v));
  ErrorInformation& ei = d_errInfo.get(v);
  Assert(ei.inFocus());
  d_focus.erase(ei.getHandle());
  ei.setInFocus(false);
  d_outOfFocus.push_back(v);
}

void ErrorSet::addBackIntoFocus(ArithVar v) {
  Assert(inError(v));
  ErrorInformation& ei = d_errInfo.get(v);
  Assert(!ei.inFocus());
  switch(getSelectionRule()){
    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
      ei.setAmount(computeDiff(v));
      break;
    case options::ErrorSelectionRule::SUM_METRIC:
      ei.setMetric(sumMetric(v));
      break;
    case options::ErrorSelectionRule::VAR_ORDER:
      // do nothing
      break;
  }

  ei.setInFocus(true);
  FocusSetHandle handle = d_focus.push(v);
  ei.setHandle(handle);
}

void ErrorSet::blur(){
  while(!d_outOfFocus.empty()){
    ArithVar v = d_outOfFocus.back();
    d_outOfFocus.pop_back();

    if(inError(v) && !inFocus(v)){
      addBackIntoFocus(v);
    }
  }
}



int ErrorSet::popSignal() {
  ArithVar back = d_signals.back();
  d_signals.pop_back();

  if(inError(back)){
    ErrorInformation& ei = d_errInfo.get(back);
    int prevSgn = ei.sgn();
    int focusSgn = ei.focusSgn();
    bool vilb = d_variables.cmpAssignmentLowerBound(back) < 0;
    bool viub = d_variables.cmpAssignmentUpperBound(back) > 0;
    if(vilb || viub){
      Assert(!vilb || !viub);
      int currSgn = vilb ? 1 : -1;
      if(currSgn != prevSgn){
        ConstraintP curr = vilb ?  d_variables.getLowerBoundConstraint(back)
          : d_variables.getUpperBoundConstraint(back);
        ei.reset(curr, currSgn);
      }
      update(ei);
    }else{
      transitionVariableOutOfError(back);
    }
    return focusSgn;
  }else if(inconsistent(back)){
    transitionVariableIntoError(back);
  }
  return 0;
}

void ErrorSet::clear(){
  // Nothing should be relaxed!
  d_signals.clear();
  d_errInfo.purge();
  d_focus.clear();
}

void ErrorSet::clearFocus(){
  for(ErrorSet::focus_iterator i =focusBegin(), i_end = focusEnd(); i != i_end; ++i){
    ArithVar f = *i;
    ErrorInformation& fei = d_errInfo.get(f);
    fei.setInFocus(false);
    d_outOfFocus.push_back(f);
  }
  d_focus.clear();
}

void ErrorSet::reduceToSignals(){
  for(error_iterator ei=errorBegin(), ei_end=errorEnd(); ei != ei_end; ++ei){
    ArithVar curr = *ei;
    signalVariable(curr);
  }

  d_errInfo.purge();
  d_focus.clear();
  d_outOfFocus.clear();
}

DeltaRational ErrorSet::computeDiff(ArithVar v) const{
  Assert(inconsistent(v));
  const DeltaRational& beta = d_variables.getAssignment(v);
  DeltaRational diff = d_variables.cmpAssignmentLowerBound(v) < 0 ?
    d_variables.getLowerBound(v) - beta:
    beta - d_variables.getUpperBound(v);

  Assert(diff.sgn() > 0);
  return diff;
}

void ErrorSet::debugPrint(std::ostream& out) const {
  static int instance = 0;
  ++instance;
  out << "error set debugprint " << instance << endl;
  for(error_iterator i = errorBegin(), i_end = errorEnd();
      i != i_end; ++i){
    ArithVar e = *i;
    const ErrorInformation& ei = d_errInfo[e];
    ei.print(out);
    out << "  ";
    d_variables.printModel(e, out);
    out << endl;
  }
  out << "focus ";
  for(focus_iterator i = focusBegin(), i_end = focusEnd();
      i != i_end; ++i){
    out << *i << " ";
  }
  out << ";" << endl;
}

void ErrorSet::focusDownToJust(ArithVar v) {
  clearFocus();

  ErrorInformation& vei = d_errInfo.get(v);
  vei.setInFocus(true);
  FocusSetHandle handle = d_focus.push(v);
  vei.setHandle(handle);
}

void ErrorSet::pushErrorInto(ArithVarVec& vec) const{
  for(error_iterator i = errorBegin(), e = errorEnd(); i != e; ++i ){
    vec.push_back(*i);
  }
}

void ErrorSet::pushFocusInto(ArithVarVec& vec) const{
  for(focus_iterator i = focusBegin(), e = focusEnd(); i != e; ++i ){
    vec.push_back(*i);
  }
}

}  // 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, 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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18
19		#include "theory/arith/error_set.h"
20
21		#include "smt/smt_statistics_registry.h"
22		#include "theory/arith/constraint.h"
23
24		using namespace std;
25
26		namespace cvc5 {
27		namespace theory {
28		namespace arith {
29
30	666971	ErrorInformation::ErrorInformation()
31		: d_variable(ARITHVAR_SENTINEL),
32		d_violated(NullConstraint),
33		d_sgn(0),
34		d_relaxed(false),
35		d_inFocus(false),
36		d_handle(),
37		d_amount(nullptr),
38	666971	d_metric(0)
39		{
40	1333942	Debug("arith::error::mem")
41	666971	<< "def constructor " << d_variable << " " << d_amount.get() << endl;
42	666971	}
43
44	507861	ErrorInformation::ErrorInformation(ArithVar var, ConstraintP vio, int sgn)
45		: d_variable(var),
46		d_violated(vio),
47		d_sgn(sgn),
48		d_relaxed(false),
49		d_inFocus(false),
50		d_handle(),
51		d_amount(nullptr),
52	507861	d_metric(0)
53		{
54	507861	Assert(debugInitialized());
55	1015722	Debug("arith::error::mem")
56	507861	<< "constructor " << d_variable << " " << d_amount.get() << endl;
57	507861	}
58
59
60	2679378	ErrorInformation::~ErrorInformation() {
61	1339689	Assert(d_relaxed != true);
62	1339689	if (d_amount != nullptr)
63		{
64	978	Debug("arith::error::mem") << d_amount.get() << endl;
65	1956	Debug("arith::error::mem")
66	978	<< "destroy " << d_variable << " " << d_amount.get() << endl;
67	978	d_amount = nullptr;
68		}
69	1339689	}
70
71	164857	ErrorInformation::ErrorInformation(const ErrorInformation& ei)
72	164857	: d_variable(ei.d_variable)
73	164857	, d_violated(ei.d_violated)
74	164857	, d_sgn(ei.d_sgn)
75	164857	, d_relaxed(ei.d_relaxed)
76	164857	, d_inFocus(ei.d_inFocus)
77		, d_handle(ei.d_handle)
78	824285	, d_metric(0)
79		{
80	164857	if (ei.d_amount == nullptr)
81		{
82	164413	d_amount = nullptr;
83		}
84		else
85		{
86	444	d_amount = std::make_unique<DeltaRational>(*ei.d_amount);
87		}
88	329714	Debug("arith::error::mem")
89	164857	<< "copy const " << d_variable << " " << d_amount.get() << endl;
90	164857	}
91
92	1014819	ErrorInformation& ErrorInformation::operator=(const ErrorInformation& ei){
93	1014819	d_variable = ei.d_variable;
94	1014819	d_violated = ei.d_violated;
95	1014819	d_sgn = ei.d_sgn;
96	1014819	d_relaxed = (ei.d_relaxed);
97	1014819	d_inFocus = (ei.d_inFocus);
98	1014819	d_handle = (ei.d_handle);
99	1014819	d_metric = ei.d_metric;
100	1014819	if (d_amount != nullptr && ei.d_amount != nullptr)
101		{
102		Debug("arith::error::mem")
103		<< "assignment assign " << d_variable << " " << d_amount.get() << endl;
104		d_amount = ei.d_amount;
105		}
106	1014819	else if (ei.d_amount != nullptr)
107		{
108		d_amount = std::make_unique<DeltaRational>(*ei.d_amount);
109		Debug("arith::error::mem")
110		<< "assignment alloc " << d_variable << " " << d_amount.get() << endl;
111		}
112	1014819	else if (d_amount != nullptr)
113		{
114	593742	Debug("arith::error::mem")
115	296871	<< "assignment release " << d_variable << " " << d_amount.get() << endl;
116	296871	d_amount = nullptr;
117		}
118		else
119		{
120	717948	d_amount = nullptr;
121		}
122	1014819	return *this;
123		}
124
125	1912	void ErrorInformation::reset(ConstraintP c, int sgn){
126	1912	Assert(!isRelaxed());
127	1912	Assert(c != NullConstraint);
128	1912	d_violated = c;
129	1912	d_sgn = sgn;
130
131	1912	if (d_amount != nullptr)
132		{
133	844	Debug("arith::error::mem")
134	422	<< "reset " << d_variable << " " << d_amount.get() << endl;
135	422	d_amount = nullptr;
136		}
137	1912	}
138
139	381439	void ErrorInformation::setAmount(const DeltaRational& am){
140	381439	if (d_amount == nullptr)
141		{
142	297827	d_amount = std::make_unique<DeltaRational>();
143	595654	Debug("arith::error::mem")
144	297827	<< "setAmount " << d_variable << " " << d_amount.get() << endl;
145		}
146	381439	(*d_amount) = am;
147	381439	}
148
149	15273	ErrorSet::Statistics::Statistics()
150		: d_enqueues(
151	30546	smtStatisticsRegistry().registerInt("theory::arith::pqueue::enqueues")),
152	15273	d_enqueuesCollection(smtStatisticsRegistry().registerInt(
153	30546	"theory::arith::pqueue::enqueuesCollection")),
154	15273	d_enqueuesDiffMode(smtStatisticsRegistry().registerInt(
155	30546	"theory::arith::pqueue::enqueuesDiffMode")),
156	15273	d_enqueuesVarOrderMode(smtStatisticsRegistry().registerInt(
157	30546	"theory::arith::pqueue::enqueuesVarOrderMode")),
158	15273	d_enqueuesCollectionDuplicates(smtStatisticsRegistry().registerInt(
159	30546	"theory::arith::pqueue::enqueuesCollectionDuplicates")),
160	15273	d_enqueuesVarOrderModeDuplicates(smtStatisticsRegistry().registerInt(
161	91638	"theory::arith::pqueue::enqueuesVarOrderModeDuplicates"))
162		{
163	15273	}
164
165	15273	ErrorSet::ErrorSet(ArithVariables& vars,
166		TableauSizes tabSizes,
167	15273	BoundCountingLookup lookups)
168		: d_variables(vars),
169		d_errInfo(),
170		d_selectionRule(options::ErrorSelectionRule::VAR_ORDER),
171	30546	d_focus(ComparatorPivotRule(this, d_selectionRule)),
172		d_outOfFocus(),
173		d_signals(),
174		d_tableauSizes(tabSizes),
175	45819	d_boundLookup(lookups)
176	15273	{}
177
178	3261390	options::ErrorSelectionRule ErrorSet::getSelectionRule() const
179		{
180	3261390	return d_selectionRule;
181		}
182
183	214918	void ErrorSet::recomputeAmount(ErrorInformation& ei,
184		options::ErrorSelectionRule rule)
185		{
186	214918	switch(rule){
187	194568	case options::ErrorSelectionRule::MINIMUM_AMOUNT:
188		case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
189	194568	ei.setAmount(computeDiff(ei.getVariable()));
190	194568	break;
191		case options::ErrorSelectionRule::SUM_METRIC:
192		ei.setMetric(sumMetric(ei.getVariable()));
193		break;
194	20350	case options::ErrorSelectionRule::VAR_ORDER:
195		// do nothing
196	20350	break;
197		}
198	214918	}
199
200	1214426	void ErrorSet::setSelectionRule(options::ErrorSelectionRule rule)
201		{
202	1214426	if(rule != getSelectionRule()){
203	413420	FocusSet into(ComparatorPivotRule(this, rule));
204	206710	FocusSet::const_iterator iter = d_focus.begin();
205	206710	FocusSet::const_iterator i_end = d_focus.end();
206	636546	for(; iter != i_end; ++iter){
207	214918	ArithVar v = *iter;
208	214918	ErrorInformation& ei = d_errInfo.get(v);
209	214918	if(ei.inFocus()){
210	214918	recomputeAmount(ei, rule);
211	214918	FocusSetHandle handle = into.push(v);
212	214918	ei.setHandle(handle);
213		}
214		}
215	206710	d_focus.swap(into);
216	206710	d_selectionRule = rule;
217		}
218	1214426	Assert(getSelectionRule() == rule);
219	1214426	}
220
221	221983	ComparatorPivotRule::ComparatorPivotRule(const ErrorSet* es,
222	221983	options::ErrorSelectionRule r)
223	221983	: d_errorSet(es), d_rule(r)
224	221983	{}
225
226	1408125	bool ComparatorPivotRule::operator()(ArithVar v, ArithVar u) const {
227	1408125	switch(d_rule){
228	748702	case options::ErrorSelectionRule::VAR_ORDER:
229		// This needs to be the reverse of the minVariableOrder
230	748702	return v > u;
231		case options::ErrorSelectionRule::SUM_METRIC:
232		{
233		uint32_t v_metric = d_errorSet->getMetric(v);
234		uint32_t u_metric = d_errorSet->getMetric(u);
235		if(v_metric == u_metric){
236		return v > u;
237		}else{
238		return v_metric > u_metric;
239		}
240		}
241	659423	case options::ErrorSelectionRule::MINIMUM_AMOUNT:
242		{
243	659423	const DeltaRational& vamt = d_errorSet->getAmount(v);
244	659423	const DeltaRational& uamt = d_errorSet->getAmount(u);
245	659423	int cmp = vamt.cmp(uamt);
246	659423	if(cmp == 0){
247	251720	return v > u;
248		}else{
249	407703	return cmp > 0;
250		}
251		}
252		case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
253		{
254		const DeltaRational& vamt = d_errorSet->getAmount(v);
255		const DeltaRational& uamt = d_errorSet->getAmount(u);
256		int cmp = vamt.cmp(uamt);
257		if(cmp == 0){
258		return v > u;
259		}else{
260		return cmp < 0;
261		}
262		}
263		}
264		Unreachable();
265		}
266
267	324677	void ErrorSet::update(ErrorInformation& ei){
268	324677	if(ei.inFocus()){
269
270	324677	switch(getSelectionRule()){
271	83958	case options::ErrorSelectionRule::MINIMUM_AMOUNT:
272		case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
273	83958	ei.setAmount(computeDiff(ei.getVariable()));
274	83958	d_focus.update(ei.getHandle(), ei.getVariable());
275	83958	break;
276		case options::ErrorSelectionRule::SUM_METRIC:
277		ei.setMetric(sumMetric(ei.getVariable()));
278		d_focus.update(ei.getHandle(), ei.getVariable());
279		break;
280	240719	case options::ErrorSelectionRule::VAR_ORDER:
281		// do nothing
282	240719	break;
283		}
284		}
285	324677	}
286
287		/** A variable becomes satisfied. */
288	377000	void ErrorSet::transitionVariableOutOfError(ArithVar v) {
289	377000	Assert(!inconsistent(v));
290	377000	ErrorInformation& ei = d_errInfo.get(v);
291	377000	Assert(ei.debugInitialized());
292	377000	if(ei.isRelaxed()){
293		ConstraintP viol = ei.getViolated();
294		if(ei.sgn() > 0){
295		d_variables.setLowerBoundConstraint(viol);
296		}else{
297		d_variables.setUpperBoundConstraint(viol);
298		}
299		Assert(!inconsistent(v));
300		ei.setUnrelaxed();
301		}
302	377000	if(ei.inFocus()){
303	377000	d_focus.erase(ei.getHandle());
304	377000	ei.setInFocus(false);
305		}
306	377000	d_errInfo.remove(v);
307	377000	}
308
309
310	507861	void ErrorSet::transitionVariableIntoError(ArithVar v) {
311	507861	Assert(inconsistent(v));
312	507861	bool vilb = d_variables.cmpAssignmentLowerBound(v) < 0;
313	507861	int sgn = vilb ? 1 : -1;
314	1015722	ConstraintP c = vilb ?
315	1015722	d_variables.getLowerBoundConstraint(v) : d_variables.getUpperBoundConstraint(v);
316	507861	d_errInfo.set(v, ErrorInformation(v, c, sgn));
317	507861	ErrorInformation& ei = d_errInfo.get(v);
318
319	507861	switch(getSelectionRule()){
320	102913	case options::ErrorSelectionRule::MINIMUM_AMOUNT:
321		case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
322	102913	ei.setAmount(computeDiff(v));
323	102913	break;
324		case options::ErrorSelectionRule::SUM_METRIC:
325		ei.setMetric(sumMetric(ei.getVariable()));
326		break;
327	404948	case options::ErrorSelectionRule::VAR_ORDER:
328		// do nothing
329	404948	break;
330		}
331	507861	ei.setInFocus(true);
332	507861	FocusSetHandle handle = d_focus.push(v);
333	507861	ei.setHandle(handle);
334	507861	}
335
336		void ErrorSet::dropFromFocus(ArithVar v) {
337		Assert(inError(v));
338		ErrorInformation& ei = d_errInfo.get(v);
339		Assert(ei.inFocus());
340		d_focus.erase(ei.getHandle());
341		ei.setInFocus(false);
342		d_outOfFocus.push_back(v);
343		}
344
345		void ErrorSet::addBackIntoFocus(ArithVar v) {
346		Assert(inError(v));
347		ErrorInformation& ei = d_errInfo.get(v);
348		Assert(!ei.inFocus());
349		switch(getSelectionRule()){
350		case options::ErrorSelectionRule::MINIMUM_AMOUNT:
351		case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
352		ei.setAmount(computeDiff(v));
353		break;
354		case options::ErrorSelectionRule::SUM_METRIC:
355		ei.setMetric(sumMetric(v));
356		break;
357		case options::ErrorSelectionRule::VAR_ORDER:
358		// do nothing
359		break;
360		}
361
362		ei.setInFocus(true);
363		FocusSetHandle handle = d_focus.push(v);
364		ei.setHandle(handle);
365		}
366
367		void ErrorSet::blur(){
368		while(!d_outOfFocus.empty()){
369		ArithVar v = d_outOfFocus.back();
370		d_outOfFocus.pop_back();
371
372		if(inError(v) && !inFocus(v)){
373		addBackIntoFocus(v);
374		}
375		}
376		}
377
378
379
380	10661745	int ErrorSet::popSignal() {
381	10661745	ArithVar back = d_signals.back();
382	10661745	d_signals.pop_back();
383
384	10661745	if(inError(back)){
385	701677	ErrorInformation& ei = d_errInfo.get(back);
386	701677	int prevSgn = ei.sgn();
387	701677	int focusSgn = ei.focusSgn();
388	701677	bool vilb = d_variables.cmpAssignmentLowerBound(back) < 0;
389	701677	bool viub = d_variables.cmpAssignmentUpperBound(back) > 0;
390	701677	if(vilb \|\| viub){
391	324677	Assert(!vilb \|\| !viub);
392	324677	int currSgn = vilb ? 1 : -1;
393	324677	if(currSgn != prevSgn){
394	2768	ConstraintP curr = vilb ? d_variables.getLowerBoundConstraint(back)
395	2768	: d_variables.getUpperBoundConstraint(back);
396	1912	ei.reset(curr, currSgn);
397		}
398	324677	update(ei);
399		}else{
400	377000	transitionVariableOutOfError(back);
401		}
402	701677	return focusSgn;
403	9960068	}else if(inconsistent(back)){
404	507861	transitionVariableIntoError(back);
405		}
406	9960068	return 0;
407		}
408
409		void ErrorSet::clear(){
410		// Nothing should be relaxed!
411		d_signals.clear();
412		d_errInfo.purge();
413		d_focus.clear();
414		}
415
416		void ErrorSet::clearFocus(){
417		for(ErrorSet::focus_iterator i =focusBegin(), i_end = focusEnd(); i != i_end; ++i){
418		ArithVar f = *i;
419		ErrorInformation& fei = d_errInfo.get(f);
420		fei.setInFocus(false);
421		d_outOfFocus.push_back(f);
422		}
423		d_focus.clear();
424		}
425
426	1043504	void ErrorSet::reduceToSignals(){
427	1173462	for(error_iterator ei=errorBegin(), ei_end=errorEnd(); ei != ei_end; ++ei){
428	129958	ArithVar curr = *ei;
429	129958	signalVariable(curr);
430		}
431
432	1043504	d_errInfo.purge();
433	1043504	d_focus.clear();
434	1043504	d_outOfFocus.clear();
435	1043504	}
436
437	381439	DeltaRational ErrorSet::computeDiff(ArithVar v) const{
438	381439	Assert(inconsistent(v));
439	381439	const DeltaRational& beta = d_variables.getAssignment(v);
440	381439	DeltaRational diff = d_variables.cmpAssignmentLowerBound(v) < 0 ?
441	197392	d_variables.getLowerBound(v) - beta:
442	578831	beta - d_variables.getUpperBound(v);
443
444	381439	Assert(diff.sgn() > 0);
445	381439	return diff;
446		}
447
448		void ErrorSet::debugPrint(std::ostream& out) const {
449		static int instance = 0;
450		++instance;
451		out << "error set debugprint " << instance << endl;
452		for(error_iterator i = errorBegin(), i_end = errorEnd();
453		i != i_end; ++i){
454		ArithVar e = *i;
455		const ErrorInformation& ei = d_errInfo[e];
456		ei.print(out);
457		out << " ";
458		d_variables.printModel(e, out);
459		out << endl;
460		}
461		out << "focus ";
462		for(focus_iterator i = focusBegin(), i_end = focusEnd();
463		i != i_end; ++i){
464		out << *i << " ";
465		}
466		out << ";" << endl;
467		}
468
469		void ErrorSet::focusDownToJust(ArithVar v) {
470		clearFocus();
471
472		ErrorInformation& vei = d_errInfo.get(v);
473		vei.setInFocus(true);
474		FocusSetHandle handle = d_focus.push(v);
475		vei.setHandle(handle);
476		}
477
478		void ErrorSet::pushErrorInto(ArithVarVec& vec) const{
479		for(error_iterator i = errorBegin(), e = errorEnd(); i != e; ++i ){
480		vec.push_back(*i);
481		}
482		}
483
484		void ErrorSet::pushFocusInto(ArithVarVec& vec) const{
485		for(focus_iterator i = focusBegin(), e = focusEnd(); i != e; ++i ){
486		vec.push_back(*i);
487		}
488		}
489
490		} // namespace arith
491		} // namespace theory
492	31137	} // namespace cvc5