Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/error_set.cpp	Lines:	201	314	64.0 %
Date:	2021-11-06	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	667004	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	667004	d_metric(0)
39		{
40	1334008	Debug("arith::error::mem")
41	667004	<< "def constructor " << d_variable << " " << d_amount.get() << endl;
42	667004	}
43
44	506597	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	506597	d_metric(0)
53		{
54	506597	Assert(debugInitialized());
55	1013194	Debug("arith::error::mem")
56	506597	<< "constructor " << d_variable << " " << d_amount.get() << endl;
57	506597	}
58
59
60	2679526	ErrorInformation::~ErrorInformation() {
61	1339763	Assert(d_relaxed != true);
62	1339763	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	1339763	}
70
71	166162	ErrorInformation::ErrorInformation(const ErrorInformation& ei)
72	166162	: d_variable(ei.d_variable)
73	166162	, d_violated(ei.d_violated)
74	166162	, d_sgn(ei.d_sgn)
75	166162	, d_relaxed(ei.d_relaxed)
76	166162	, d_inFocus(ei.d_inFocus)
77		, d_handle(ei.d_handle)
78	830810	, d_metric(0)
79		{
80	166162	if (ei.d_amount == nullptr)
81		{
82	165718	d_amount = nullptr;
83		}
84		else
85		{
86	444	d_amount = std::make_unique<DeltaRational>(*ei.d_amount);
87		}
88	332324	Debug("arith::error::mem")
89	166162	<< "copy const " << d_variable << " " << d_amount.get() << endl;
90	166162	}
91
92	1012287	ErrorInformation& ErrorInformation::operator=(const ErrorInformation& ei){
93	1012287	d_variable = ei.d_variable;
94	1012287	d_violated = ei.d_violated;
95	1012287	d_sgn = ei.d_sgn;
96	1012287	d_relaxed = (ei.d_relaxed);
97	1012287	d_inFocus = (ei.d_inFocus);
98	1012287	d_handle = (ei.d_handle);
99	1012287	d_metric = ei.d_metric;
100	1012287	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	1012287	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	1012287	else if (d_amount != nullptr)
113		{
114	594718	Debug("arith::error::mem")
115	297359	<< "assignment release " << d_variable << " " << d_amount.get() << endl;
116	297359	d_amount = nullptr;
117		}
118		else
119		{
120	714928	d_amount = nullptr;
121		}
122	1012287	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	382148	void ErrorInformation::setAmount(const DeltaRational& am){
140	382148	if (d_amount == nullptr)
141		{
142	298315	d_amount = std::make_unique<DeltaRational>();
143	596630	Debug("arith::error::mem")
144	298315	<< "setAmount " << d_variable << " " << d_amount.get() << endl;
145		}
146	382148	(*d_amount) = am;
147	382148	}
148
149	15272	ErrorSet::Statistics::Statistics()
150		: d_enqueues(
151	30544	smtStatisticsRegistry().registerInt("theory::arith::pqueue::enqueues")),
152	15272	d_enqueuesCollection(smtStatisticsRegistry().registerInt(
153	30544	"theory::arith::pqueue::enqueuesCollection")),
154	15272	d_enqueuesDiffMode(smtStatisticsRegistry().registerInt(
155	30544	"theory::arith::pqueue::enqueuesDiffMode")),
156	15272	d_enqueuesVarOrderMode(smtStatisticsRegistry().registerInt(
157	30544	"theory::arith::pqueue::enqueuesVarOrderMode")),
158	15272	d_enqueuesCollectionDuplicates(smtStatisticsRegistry().registerInt(
159	30544	"theory::arith::pqueue::enqueuesCollectionDuplicates")),
160	15272	d_enqueuesVarOrderModeDuplicates(smtStatisticsRegistry().registerInt(
161	91632	"theory::arith::pqueue::enqueuesVarOrderModeDuplicates"))
162		{
163	15272	}
164
165	15272	ErrorSet::ErrorSet(ArithVariables& vars,
166		TableauSizes tabSizes,
167	15272	BoundCountingLookup lookups)
168		: d_variables(vars),
169		d_errInfo(),
170		d_selectionRule(options::ErrorSelectionRule::VAR_ORDER),
171	30544	d_focus(ComparatorPivotRule(this, d_selectionRule)),
172		d_outOfFocus(),
173		d_signals(),
174		d_tableauSizes(tabSizes),
175	45816	d_boundLookup(lookups)
176	15272	{}
177
178	3242387	options::ErrorSelectionRule ErrorSet::getSelectionRule() const
179		{
180	3242387	return d_selectionRule;
181		}
182
183	215092	void ErrorSet::recomputeAmount(ErrorInformation& ei,
184		options::ErrorSelectionRule rule)
185		{
186	215092	switch(rule){
187	194728	case options::ErrorSelectionRule::MINIMUM_AMOUNT:
188		case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
189	194728	ei.setAmount(computeDiff(ei.getVariable()));
190	194728	break;
191		case options::ErrorSelectionRule::SUM_METRIC:
192		ei.setMetric(sumMetric(ei.getVariable()));
193		break;
194	20364	case options::ErrorSelectionRule::VAR_ORDER:
195		// do nothing
196	20364	break;
197		}
198	215092	}
199
200	1206211	void ErrorSet::setSelectionRule(options::ErrorSelectionRule rule)
201		{
202	1206211	if(rule != getSelectionRule()){
203	413720	FocusSet into(ComparatorPivotRule(this, rule));
204	206860	FocusSet::const_iterator iter = d_focus.begin();
205	206860	FocusSet::const_iterator i_end = d_focus.end();
206	637044	for(; iter != i_end; ++iter){
207	215092	ArithVar v = *iter;
208	215092	ErrorInformation& ei = d_errInfo.get(v);
209	215092	if(ei.inFocus()){
210	215092	recomputeAmount(ei, rule);
211	215092	FocusSetHandle handle = into.push(v);
212	215092	ei.setHandle(handle);
213		}
214		}
215	206860	d_focus.swap(into);
216	206860	d_selectionRule = rule;
217		}
218	1206211	Assert(getSelectionRule() == rule);
219	1206211	}
220
221	222132	ComparatorPivotRule::ComparatorPivotRule(const ErrorSet* es,
222	222132	options::ErrorSelectionRule r)
223	222132	: d_errorSet(es), d_rule(r)
224	222132	{}
225
226	1409874	bool ComparatorPivotRule::operator()(ArithVar v, ArithVar u) const {
227	1409874	switch(d_rule){
228	749083	case options::ErrorSelectionRule::VAR_ORDER:
229		// This needs to be the reverse of the minVariableOrder
230	749083	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	660791	case options::ErrorSelectionRule::MINIMUM_AMOUNT:
242		{
243	660791	const DeltaRational& vamt = d_errorSet->getAmount(v);
244	660791	const DeltaRational& uamt = d_errorSet->getAmount(u);
245	660791	int cmp = vamt.cmp(uamt);
246	660791	if(cmp == 0){
247	252346	return v > u;
248		}else{
249	408445	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	323368	void ErrorSet::update(ErrorInformation& ei){
268	323368	if(ei.inFocus()){
269
270	323368	switch(getSelectionRule()){
271	84179	case options::ErrorSelectionRule::MINIMUM_AMOUNT:
272		case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
273	84179	ei.setAmount(computeDiff(ei.getVariable()));
274	84179	d_focus.update(ei.getHandle(), ei.getVariable());
275	84179	break;
276		case options::ErrorSelectionRule::SUM_METRIC:
277		ei.setMetric(sumMetric(ei.getVariable()));
278		d_focus.update(ei.getHandle(), ei.getVariable());
279		break;
280	239189	case options::ErrorSelectionRule::VAR_ORDER:
281		// do nothing
282	239189	break;
283		}
284		}
285	323368	}
286
287		/** A variable becomes satisfied. */
288	377151	void ErrorSet::transitionVariableOutOfError(ArithVar v) {
289	377151	Assert(!inconsistent(v));
290	377151	ErrorInformation& ei = d_errInfo.get(v);
291	377151	Assert(ei.debugInitialized());
292	377151	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	377151	if(ei.inFocus()){
303	377151	d_focus.erase(ei.getHandle());
304	377151	ei.setInFocus(false);
305		}
306	377151	d_errInfo.remove(v);
307	377151	}
308
309
310	506597	void ErrorSet::transitionVariableIntoError(ArithVar v) {
311	506597	Assert(inconsistent(v));
312	506597	bool vilb = d_variables.cmpAssignmentLowerBound(v) < 0;
313	506597	int sgn = vilb ? 1 : -1;
314	1013194	ConstraintP c = vilb ?
315	1013194	d_variables.getLowerBoundConstraint(v) : d_variables.getUpperBoundConstraint(v);
316	506597	d_errInfo.set(v, ErrorInformation(v, c, sgn));
317	506597	ErrorInformation& ei = d_errInfo.get(v);
318
319	506597	switch(getSelectionRule()){
320	103241	case options::ErrorSelectionRule::MINIMUM_AMOUNT:
321		case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
322	103241	ei.setAmount(computeDiff(v));
323	103241	break;
324		case options::ErrorSelectionRule::SUM_METRIC:
325		ei.setMetric(sumMetric(ei.getVariable()));
326		break;
327	403356	case options::ErrorSelectionRule::VAR_ORDER:
328		// do nothing
329	403356	break;
330		}
331	506597	ei.setInFocus(true);
332	506597	FocusSetHandle handle = d_focus.push(v);
333	506597	ei.setHandle(handle);
334	506597	}
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	10656995	int ErrorSet::popSignal() {
381	10656995	ArithVar back = d_signals.back();
382	10656995	d_signals.pop_back();
383
384	10656995	if(inError(back)){
385	700519	ErrorInformation& ei = d_errInfo.get(back);
386	700519	int prevSgn = ei.sgn();
387	700519	int focusSgn = ei.focusSgn();
388	700519	bool vilb = d_variables.cmpAssignmentLowerBound(back) < 0;
389	700519	bool viub = d_variables.cmpAssignmentUpperBound(back) > 0;
390	700519	if(vilb \|\| viub){
391	323368	Assert(!vilb \|\| !viub);
392	323368	int currSgn = vilb ? 1 : -1;
393	323368	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	323368	update(ei);
399		}else{
400	377151	transitionVariableOutOfError(back);
401		}
402	700519	return focusSgn;
403	9956476	}else if(inconsistent(back)){
404	506597	transitionVariableIntoError(back);
405		}
406	9956476	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	1035210	void ErrorSet::reduceToSignals(){
427	1163749	for(error_iterator ei=errorBegin(), ei_end=errorEnd(); ei != ei_end; ++ei){
428	128539	ArithVar curr = *ei;
429	128539	signalVariable(curr);
430		}
431
432	1035210	d_errInfo.purge();
433	1035210	d_focus.clear();
434	1035210	d_outOfFocus.clear();
435	1035210	}
436
437	382148	DeltaRational ErrorSet::computeDiff(ArithVar v) const{
438	382148	Assert(inconsistent(v));
439	382148	const DeltaRational& beta = d_variables.getAssignment(v);
440	382148	DeltaRational diff = d_variables.cmpAssignmentLowerBound(v) < 0 ?
441	197528	d_variables.getLowerBound(v) - beta:
442	579676	beta - d_variables.getUpperBound(v);
443
444	382148	Assert(diff.sgn() > 0);
445	382148	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