Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/simplex.cpp	Lines:	58	162	35.8 %
Date:	2021-09-29	Branches:	82	588	13.9 %


/******************************************************************************
 * 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 "options/smt_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(options::produceProofs());
}

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