Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/simplex.cpp	Lines:	58	162	35.8 %
Date:	2021-09-14	Branches:	81	586	13.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Gereon Kremer, Andres Noetzli
 *
 * 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 is an implementation of the Simplex Module for the Simplex for
 * DPLL(T) decision procedure.
 */

#include "theory/arith/simplex.h"

#include "base/output.h"
#include "options/arith_options.h"
#include "theory/arith/constraint.h"
#include "theory/arith/error_set.h"
#include "theory/arith/linear_equality.h"
#include "theory/arith/tableau.h"
#include "util/statistics_value.h"

using namespace std;

namespace cvc5 {
namespace theory {
namespace arith {


SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
  : d_pivots(0)
  , d_conflictVariables()
  , d_linEq(linEq)
  , d_variables(d_linEq.getVariables())
  , d_tableau(d_linEq.getTableau())
  , d_errorSet(errors)
  , d_numVariables(0)
  , d_conflictChannel(conflictChannel)
  , d_conflictBuilder(NULL)
  , d_arithVarMalloc(tvmalloc)
  , d_errorSize(0)
  , d_zero(0)
  , d_posOne(1)
  , d_negOne(-1)
{
  d_heuristicRule = options::arithErrorSelectionRule();
  d_errorSet.setSelectionRule(d_heuristicRule);
  d_conflictBuilder = new FarkasConflictBuilder();
}

SimplexDecisionProcedure::~SimplexDecisionProcedure(){
  delete d_conflictBuilder;
}


bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat& conflicts) {
  TimerStat::CodeTimer codeTimer(timer);
  Assert(d_conflictVariables.empty());

  while(d_errorSet.moreSignals()){
    ArithVar curr = d_errorSet.topSignal();
    if(d_tableau.isBasic(curr) && !d_variables.assignmentIsConsistent(curr)){
      Assert(d_linEq.basicIsTracked(curr));

      if(!d_conflictVariables.isMember(curr) && checkBasicForConflict(curr)){

        Debug("recentlyViolated")
          << "It worked? "
          << conflicts.get()
          << " " << curr
          << " "  << checkBasicForConflict(curr) << endl;
        reportConflict(curr);
        ++conflicts;
      }
    }
    // Pop signal afterwards in case d_linEq.trackVariable(curr);
    // is needed for for the ErrorSet
    d_errorSet.popSignal();
  }
  d_errorSize = d_errorSet.errorSize();

  Assert(d_errorSet.noSignals());
  return !d_conflictVariables.empty();
}

/** Reports a conflict to on the output channel. */
void SimplexDecisionProcedure::reportConflict(ArithVar basic){
  Assert(!d_conflictVariables.isMember(basic));
  Assert(checkBasicForConflict(basic));

  ConstraintCP conflicted = generateConflictForBasic(basic);
  Assert(conflicted != NullConstraint);
  d_conflictChannel.raiseConflict(conflicted, InferenceId::ARITH_CONF_SIMPLEX);

  d_conflictVariables.add(basic);
}

ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic) const {
  Assert(d_tableau.isBasic(basic));
  Assert(checkBasicForConflict(basic));

  if(d_variables.cmpAssignmentLowerBound(basic) < 0){
    Assert(d_linEq.nonbasicsAtUpperBounds(basic));
    return d_linEq.generateConflictBelowLowerBound(basic, *d_conflictBuilder);
  }else if(d_variables.cmpAssignmentUpperBound(basic) > 0){
    Assert(d_linEq.nonbasicsAtLowerBounds(basic));
    return d_linEq.generateConflictAboveUpperBound(basic, *d_conflictBuilder);
  }else{
    Unreachable();
    return NullConstraint;
  }
}
bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(ArithVar basic) const {
  if(checkBasicForConflict(basic)){
    ConstraintCP conflicted = generateConflictForBasic(basic);
    d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
    return true;
  }else{
    return false;
  }
}

bool SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic) const {
  Assert(d_tableau.isBasic(basic));
  Assert(d_linEq.basicIsTracked(basic));

  if(d_variables.cmpAssignmentLowerBound(basic) < 0){
    if(d_linEq.nonbasicsAtUpperBounds(basic)){
      return true;
    }
  }else if(d_variables.cmpAssignmentUpperBound(basic) > 0){
    if(d_linEq.nonbasicsAtLowerBounds(basic)){
      return true;
    }
  }
  return false;
}

void SimplexDecisionProcedure::tearDownInfeasiblityFunction(TimerStat& timer, ArithVar tmp){
  TimerStat::CodeTimer codeTimer(timer);
  Assert(tmp != ARITHVAR_SENTINEL);
  Assert(d_tableau.isBasic(tmp));

  RowIndex ri = d_tableau.basicToRowIndex(tmp);
  d_linEq.stopTrackingRowIndex(ri);
  d_tableau.removeBasicRow(tmp);
  releaseVariable(tmp);
}

void SimplexDecisionProcedure::shrinkInfeasFunc(TimerStat& timer, ArithVar inf, const ArithVarVec& dropped){
  TimerStat::CodeTimer codeTimer(timer);
  for(ArithVarVec::const_iterator i=dropped.begin(), i_end = dropped.end(); i != i_end; ++i){
    ArithVar back = *i;

    int focusSgn = d_errorSet.focusSgn(back);
    Rational chg(-focusSgn);

    d_linEq.substitutePlusTimesConstant(inf, back, chg);
  }
}

void SimplexDecisionProcedure::adjustInfeasFunc(TimerStat& timer, ArithVar inf, const AVIntPairVec& focusChanges){
  TimerStat::CodeTimer codeTimer(timer);
  for(AVIntPairVec::const_iterator i=focusChanges.begin(), i_end = focusChanges.end(); i != i_end; ++i){
    ArithVar v = (*i).first;
    int focusChange = (*i).second;

    Rational chg(focusChange);
    if(d_tableau.isBasic(v)){
      d_linEq.substitutePlusTimesConstant(inf, v, chg);
    }else{
      d_linEq.directlyAddToCoefficient(inf, v, chg);
    }
  }
}

void SimplexDecisionProcedure::addToInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e){
  AVIntPairVec justE;
  int sgn  = d_errorSet.getSgn(e);
  justE.push_back(make_pair(e, sgn));
  adjustInfeasFunc(timer, inf, justE);
}

void SimplexDecisionProcedure::removeFromInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e){
  AVIntPairVec justE;
  int opSgn  = -d_errorSet.getSgn(e);
  justE.push_back(make_pair(e, opSgn));
  adjustInfeasFunc(timer, inf, justE);
}

ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set){
  Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction start" << endl;

  TimerStat::CodeTimer codeTimer(timer);
  Assert(!d_errorSet.focusEmpty());
  Assert(debugIsASet(set));

  ArithVar inf = requestVariable();
  Assert(inf != ARITHVAR_SENTINEL);

  std::vector<Rational> coeffs;
  std::vector<ArithVar> variables;

  for(ArithVarVec::const_iterator iter = set.begin(), iend = set.end(); iter != iend; ++iter){
    ArithVar e = *iter;

    Assert(d_tableau.isBasic(e));
    Assert(!d_variables.assignmentIsConsistent(e));

    int sgn = d_errorSet.getSgn(e);
    Assert(sgn == -1 || sgn == 1);
    const Rational& violatedCoeff = sgn < 0 ? d_negOne : d_posOne;
    coeffs.push_back(violatedCoeff);
    variables.push_back(e);

    Debug("constructInfeasiblityFunction") << violatedCoeff << " " << e << endl;

  }
  d_tableau.addRow(inf, coeffs, variables);
  DeltaRational newAssignment = d_linEq.computeRowValue(inf, false);
  d_variables.setAssignment(inf, newAssignment);

  //d_linEq.trackVariable(inf);
  d_linEq.trackRowIndex(d_tableau.basicToRowIndex(inf));

  Debug("constructInfeasiblityFunction") << inf << " " << newAssignment << endl;
  Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction done" << endl;
  return inf;
}

ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer){
  ArithVarVec inError;
  d_errorSet.pushFocusInto(inError);
  return constructInfeasiblityFunction(timer, inError);
}

ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, ArithVar e){
  ArithVarVec justE;
  justE.push_back(e);
  return constructInfeasiblityFunction(timer, justE);
}

void SimplexDecisionProcedure::addSgn(sgn_table& sgns, ArithVar col, int sgn, ArithVar basic){
  pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
  sgns[p].push_back(basic);
}

void SimplexDecisionProcedure::addRowSgns(sgn_table& sgns, ArithVar basic, int norm){
  for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){
    const Tableau::Entry& entry = *i;
    ArithVar v = entry.getColVar();
    int sgn = (entry.getCoefficient().sgn());
    addSgn(sgns, v, norm * sgn, basic);
  }
}

ArithVar SimplexDecisionProcedure::find_basic_in_sgns(const sgn_table& sgns, ArithVar col, int sgn, const DenseSet& m, bool inside){
  pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
  sgn_table::const_iterator i = sgns.find(p);

  if(i != sgns.end()){
    const ArithVarVec& vec = (*i).second;
    for(ArithVarVec::const_iterator viter = vec.begin(), vend = vec.end(); viter != vend; ++viter){
      ArithVar curr = *viter;
      if(inside == m.isMember(curr)){
        return curr;
      }
    }
  }
  return ARITHVAR_SENTINEL;
}

SimplexDecisionProcedure::sgn_table::const_iterator SimplexDecisionProcedure::find_sgns(const sgn_table& sgns, ArithVar col, int sgn){
  pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
  return sgns.find(p);
}
}  // 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, Gereon Kremer, Andres Noetzli
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 is an implementation of the Simplex Module for the Simplex for
14		* DPLL(T) decision procedure.
15		*/
16
17		#include "theory/arith/simplex.h"
18
19		#include "base/output.h"
20		#include "options/arith_options.h"
21		#include "theory/arith/constraint.h"
22		#include "theory/arith/error_set.h"
23		#include "theory/arith/linear_equality.h"
24		#include "theory/arith/tableau.h"
25		#include "util/statistics_value.h"
26
27		using namespace std;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace arith {
32
33
34	39668	SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
35		: d_pivots(0)
36		, d_conflictVariables()
37		, d_linEq(linEq)
38	39668	, d_variables(d_linEq.getVariables())
39	39668	, d_tableau(d_linEq.getTableau())
40		, d_errorSet(errors)
41		, d_numVariables(0)
42		, d_conflictChannel(conflictChannel)
43		, d_conflictBuilder(NULL)
44		, d_arithVarMalloc(tvmalloc)
45		, d_errorSize(0)
46		, d_zero(0)
47		, d_posOne(1)
48	119004	, d_negOne(-1)
49		{
50	39668	d_heuristicRule = options::arithErrorSelectionRule();
51	39668	d_errorSet.setSelectionRule(d_heuristicRule);
52	39668	d_conflictBuilder = new FarkasConflictBuilder();
53	39668	}
54
55	79312	SimplexDecisionProcedure::~SimplexDecisionProcedure(){
56	39656	delete d_conflictBuilder;
57	39656	}
58
59
60	1061547	bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat& conflicts) {
61	2123094	TimerStat::CodeTimer codeTimer(timer);
62	1061547	Assert(d_conflictVariables.empty());
63
64	17964083	while(d_errorSet.moreSignals()){
65	8451268	ArithVar curr = d_errorSet.topSignal();
66	8451268	if(d_tableau.isBasic(curr) && !d_variables.assignmentIsConsistent(curr)){
67	693301	Assert(d_linEq.basicIsTracked(curr));
68
69	693301	if(!d_conflictVariables.isMember(curr) && checkBasicForConflict(curr)){
70
71	142374	Debug("recentlyViolated")
72	71187	<< "It worked? "
73	142374	<< conflicts.get()
74	71187	<< " " << curr
75	71187	<< " " << checkBasicForConflict(curr) << endl;
76	71187	reportConflict(curr);
77	71187	++conflicts;
78		}
79		}
80		// Pop signal afterwards in case d_linEq.trackVariable(curr);
81		// is needed for for the ErrorSet
82	8451268	d_errorSet.popSignal();
83		}
84	1061547	d_errorSize = d_errorSet.errorSize();
85
86	1061547	Assert(d_errorSet.noSignals());
87	2123094	return !d_conflictVariables.empty();
88		}
89
90		/** Reports a conflict to on the output channel. */
91	71187	void SimplexDecisionProcedure::reportConflict(ArithVar basic){
92	71187	Assert(!d_conflictVariables.isMember(basic));
93	71187	Assert(checkBasicForConflict(basic));
94
95	71187	ConstraintCP conflicted = generateConflictForBasic(basic);
96	71187	Assert(conflicted != NullConstraint);
97	71187	d_conflictChannel.raiseConflict(conflicted, InferenceId::ARITH_CONF_SIMPLEX);
98
99	71187	d_conflictVariables.add(basic);
100	71187	}
101
102	71187	ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic) const {
103	71187	Assert(d_tableau.isBasic(basic));
104	71187	Assert(checkBasicForConflict(basic));
105
106	71187	if(d_variables.cmpAssignmentLowerBound(basic) < 0){
107	39692	Assert(d_linEq.nonbasicsAtUpperBounds(basic));
108	39692	return d_linEq.generateConflictBelowLowerBound(basic, *d_conflictBuilder);
109	31495	}else if(d_variables.cmpAssignmentUpperBound(basic) > 0){
110	31495	Assert(d_linEq.nonbasicsAtLowerBounds(basic));
111	31495	return d_linEq.generateConflictAboveUpperBound(basic, *d_conflictBuilder);
112		}else{
113		Unreachable();
114		return NullConstraint;
115		}
116		}
117		bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(ArithVar basic) const {
118		if(checkBasicForConflict(basic)){
119		ConstraintCP conflicted = generateConflictForBasic(basic);
120		d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
121		return true;
122		}else{
123		return false;
124		}
125		}
126
127	896396	bool SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic) const {
128	896396	Assert(d_tableau.isBasic(basic));
129	896396	Assert(d_linEq.basicIsTracked(basic));
130
131	896396	if(d_variables.cmpAssignmentLowerBound(basic) < 0){
132	470052	if(d_linEq.nonbasicsAtUpperBounds(basic)){
133	158768	return true;
134		}
135	426344	}else if(d_variables.cmpAssignmentUpperBound(basic) > 0){
136	426344	if(d_linEq.nonbasicsAtLowerBounds(basic)){
137	125980	return true;
138		}
139		}
140	611648	return false;
141		}
142
143		void SimplexDecisionProcedure::tearDownInfeasiblityFunction(TimerStat& timer, ArithVar tmp){
144		TimerStat::CodeTimer codeTimer(timer);
145		Assert(tmp != ARITHVAR_SENTINEL);
146		Assert(d_tableau.isBasic(tmp));
147
148		RowIndex ri = d_tableau.basicToRowIndex(tmp);
149		d_linEq.stopTrackingRowIndex(ri);
150		d_tableau.removeBasicRow(tmp);
151		releaseVariable(tmp);
152		}
153
154		void SimplexDecisionProcedure::shrinkInfeasFunc(TimerStat& timer, ArithVar inf, const ArithVarVec& dropped){
155		TimerStat::CodeTimer codeTimer(timer);
156		for(ArithVarVec::const_iterator i=dropped.begin(), i_end = dropped.end(); i != i_end; ++i){
157		ArithVar back = *i;
158
159		int focusSgn = d_errorSet.focusSgn(back);
160		Rational chg(-focusSgn);
161
162		d_linEq.substitutePlusTimesConstant(inf, back, chg);
163		}
164		}
165
166		void SimplexDecisionProcedure::adjustInfeasFunc(TimerStat& timer, ArithVar inf, const AVIntPairVec& focusChanges){
167		TimerStat::CodeTimer codeTimer(timer);
168		for(AVIntPairVec::const_iterator i=focusChanges.begin(), i_end = focusChanges.end(); i != i_end; ++i){
169		ArithVar v = (*i).first;
170		int focusChange = (*i).second;
171
172		Rational chg(focusChange);
173		if(d_tableau.isBasic(v)){
174		d_linEq.substitutePlusTimesConstant(inf, v, chg);
175		}else{
176		d_linEq.directlyAddToCoefficient(inf, v, chg);
177		}
178		}
179		}
180
181		void SimplexDecisionProcedure::addToInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e){
182		AVIntPairVec justE;
183		int sgn = d_errorSet.getSgn(e);
184		justE.push_back(make_pair(e, sgn));
185		adjustInfeasFunc(timer, inf, justE);
186		}
187
188		void SimplexDecisionProcedure::removeFromInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e){
189		AVIntPairVec justE;
190		int opSgn = -d_errorSet.getSgn(e);
191		justE.push_back(make_pair(e, opSgn));
192		adjustInfeasFunc(timer, inf, justE);
193		}
194
195		ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set){
196		Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction start" << endl;
197
198		TimerStat::CodeTimer codeTimer(timer);
199		Assert(!d_errorSet.focusEmpty());
200		Assert(debugIsASet(set));
201
202		ArithVar inf = requestVariable();
203		Assert(inf != ARITHVAR_SENTINEL);
204
205		std::vector<Rational> coeffs;
206		std::vector<ArithVar> variables;
207
208		for(ArithVarVec::const_iterator iter = set.begin(), iend = set.end(); iter != iend; ++iter){
209		ArithVar e = *iter;
210
211		Assert(d_tableau.isBasic(e));
212		Assert(!d_variables.assignmentIsConsistent(e));
213
214		int sgn = d_errorSet.getSgn(e);
215		Assert(sgn == -1 \|\| sgn == 1);
216		const Rational& violatedCoeff = sgn < 0 ? d_negOne : d_posOne;
217		coeffs.push_back(violatedCoeff);
218		variables.push_back(e);
219
220		Debug("constructInfeasiblityFunction") << violatedCoeff << " " << e << endl;
221
222		}
223		d_tableau.addRow(inf, coeffs, variables);
224		DeltaRational newAssignment = d_linEq.computeRowValue(inf, false);
225		d_variables.setAssignment(inf, newAssignment);
226
227		//d_linEq.trackVariable(inf);
228		d_linEq.trackRowIndex(d_tableau.basicToRowIndex(inf));
229
230		Debug("constructInfeasiblityFunction") << inf << " " << newAssignment << endl;
231		Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction done" << endl;
232		return inf;
233		}
234
235		ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer){
236		ArithVarVec inError;
237		d_errorSet.pushFocusInto(inError);
238		return constructInfeasiblityFunction(timer, inError);
239		}
240
241		ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, ArithVar e){
242		ArithVarVec justE;
243		justE.push_back(e);
244		return constructInfeasiblityFunction(timer, justE);
245		}
246
247		void SimplexDecisionProcedure::addSgn(sgn_table& sgns, ArithVar col, int sgn, ArithVar basic){
248		pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
249		sgns[p].push_back(basic);
250		}
251
252		void SimplexDecisionProcedure::addRowSgns(sgn_table& sgns, ArithVar basic, int norm){
253		for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){
254		const Tableau::Entry& entry = *i;
255		ArithVar v = entry.getColVar();
256		int sgn = (entry.getCoefficient().sgn());
257		addSgn(sgns, v, norm * sgn, basic);
258		}
259		}
260
261		ArithVar SimplexDecisionProcedure::find_basic_in_sgns(const sgn_table& sgns, ArithVar col, int sgn, const DenseSet& m, bool inside){
262		pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
263		sgn_table::const_iterator i = sgns.find(p);
264
265		if(i != sgns.end()){
266		const ArithVarVec& vec = (*i).second;
267		for(ArithVarVec::const_iterator viter = vec.begin(), vend = vec.end(); viter != vend; ++viter){
268		ArithVar curr = *viter;
269		if(inside == m.isMember(curr)){
270		return curr;
271		}
272		}
273		}
274		return ARITHVAR_SENTINEL;
275		}
276
277		SimplexDecisionProcedure::sgn_table::const_iterator SimplexDecisionProcedure::find_sgns(const sgn_table& sgns, ArithVar col, int sgn){
278		pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
279		return sgns.find(p);
280		}
281		} // namespace arith
282		} // namespace theory
283	29517	} // namespace cvc5