Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/simplex.cpp	Lines:	59	163	36.2 %
Date:	2021-11-05	Branches:	83	590	14.1 %


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