Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/error_set.cpp	Lines:	197	308	64.0 %
Date:	2021-09-07	Branches:	167	625	26.7 %


/******************************************************************************
 * 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(NULL)
  , d_metric(0)
{
  Debug("arith::error::mem") << "def constructor " << d_variable << " "  << d_amount << 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(NULL)
  , d_metric(0)
{
  Assert(debugInitialized());
  Debug("arith::error::mem") << "constructor " << d_variable << " "  << d_amount << endl;
}


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

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 == NULL){
    d_amount = NULL;
  }else{
    d_amount = new DeltaRational(*ei.d_amount);
  }
  Debug("arith::error::mem") << "copy const " << d_variable << " "  << d_amount << 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 != NULL && ei.d_amount != NULL){
    Debug("arith::error::mem") << "assignment assign " << d_variable << " "  << d_amount << endl;
    *d_amount = *ei.d_amount;
  }else if(ei.d_amount != NULL){
    d_amount = new DeltaRational(*ei.d_amount);
    Debug("arith::error::mem") << "assignment alloc " << d_variable << " "  << d_amount << endl;
  }else if(d_amount != NULL){
    Debug("arith::error::mem") << "assignment release " << d_variable << " "  << d_amount << endl;
    delete d_amount;
    d_amount = NULL;
  }else{
    d_amount = NULL;
  }
  return *this;
}

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

  if(d_amount != NULL){
    delete d_amount;
    Debug("arith::error::mem") << "reset " << d_variable << " "  << d_amount << endl;
    d_amount = NULL;
  }
}

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