Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/dual_simplex.cpp	Lines:	109	120	90.8 %
Date:	2021-09-14	Branches:	204	544	37.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Aina Niemetz, Morgan Deters
 *
 * 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/dual_simplex.h"

#include "base/output.h"
#include "options/arith_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/arith/constraint.h"
#include "theory/arith/error_set.h"
#include "theory/arith/linear_equality.h"


using namespace std;

namespace cvc5 {
namespace theory {
namespace arith {

DualSimplexDecisionProcedure::DualSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
  : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
  , d_pivotsInRound()
  , d_statistics(d_pivots)
{ }

DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots)
    : d_statUpdateConflicts(smtStatisticsRegistry().registerInt(
        "theory::arith::dual::UpdateConflicts")),
      d_processSignalsTime(smtStatisticsRegistry().registerTimer(
          "theory::arith::dual::findConflictOnTheQueueTime")),
      d_simplexConflicts(smtStatisticsRegistry().registerInt(
          "theory::arith::dual::simplexConflicts")),
      d_recentViolationCatches(smtStatisticsRegistry().registerInt(
          "theory::arith::dual::recentViolationCatches")),
      d_searchTime(smtStatisticsRegistry().registerTimer(
          "theory::arith::dual::searchTime")),
      d_finalCheckPivotCounter(
          smtStatisticsRegistry().registerReference<uint32_t>(
              "theory::arith::dual::lastPivots", pivots))
{
}

Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
  Assert(d_conflictVariables.empty());

  static thread_local unsigned int instance = 0;
  instance = instance + 1;
  d_pivots = 0;

  if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
    Debug("arith::findModel") << "dualFindModel("<< instance <<") trivial" << endl;
    return Result::SAT;
  }

  // We need to reduce this because of
  d_errorSet.reduceToSignals();
  d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);

  if(processSignals()){
    d_conflictVariables.purge();

    Debug("arith::findModel") << "dualFindModel("<< instance <<") early conflict" << endl;
    return Result::UNSAT;
  }else if(d_errorSet.errorEmpty()){
    Debug("arith::findModel") << "dualFindModel("<< instance <<") fixed itself" << endl;
    Assert(!d_errorSet.moreSignals());
    return Result::SAT;
  }

  Debug("arith::findModel") << "dualFindModel(" << instance <<") start non-trivial" << endl;

  Result::Sat result = Result::SAT_UNKNOWN;

  static const bool verbose = false;
  exactResult |= options::arithStandardCheckVarOrderPivots() < 0;


  uint32_t checkPeriod = options::arithSimplexCheckPeriod();
  if(result == Result::SAT_UNKNOWN){
    uint32_t numDifferencePivots = options::arithHeuristicPivots() < 0 ?
      d_numVariables + 1 : options::arithHeuristicPivots();
    // The signed to unsigned conversion is safe.
    if(numDifferencePivots > 0){

      d_errorSet.setSelectionRule(d_heuristicRule);
      if(searchForFeasibleSolution(numDifferencePivots)){
        result = Result::UNSAT;
      }
    }

    if (verbose && numDifferencePivots > 0)
    {
      if (result == Result::UNSAT)
      {
        CVC5Message() << "diff order found unsat" << endl;
      }
      else if (d_errorSet.errorEmpty())
      {
        CVC5Message() << "diff order found model" << endl;
      }
      else
      {
        CVC5Message() << "diff order missed" << endl;
      }
    }
  }
  Assert(!d_errorSet.moreSignals());

  if(!d_errorSet.errorEmpty() && result != Result::UNSAT){
    if(exactResult){
      d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
      while(!d_errorSet.errorEmpty() && result != Result::UNSAT){
        Assert(checkPeriod > 0);
        if(searchForFeasibleSolution(checkPeriod)){
          result = Result::UNSAT;
        }
      }
    }else if( options::arithStandardCheckVarOrderPivots() > 0){
      d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
      if(searchForFeasibleSolution(options::arithStandardCheckVarOrderPivots())){
        result = Result::UNSAT;
      }
      if (verbose)
      {
        if (result == Result::UNSAT)
        {
          CVC5Message() << "restricted var order found unsat" << endl;
        }
        else if (d_errorSet.errorEmpty())
        {
          CVC5Message() << "restricted var order found model" << endl;
        }
        else
        {
          CVC5Message() << "restricted var order missed" << endl;
        }
      }
    }
  }

  Assert(!d_errorSet.moreSignals());
  if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
    result = Result::SAT;
  }

  d_pivotsInRound.purge();
  // ensure that the conflict variable is still in the queue.
  d_conflictVariables.purge();

  Debug("arith::findModel") << "end findModel() " << instance << " " << result <<  endl;

  return result;
}

//corresponds to Check() in dM06
//template <SimplexDecisionProcedure::PreferenceFunction pf>
bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
  TimerStat::CodeTimer codeTimer(d_statistics.d_searchTime);

  Debug("arith") << "searchForFeasibleSolution" << endl;
  Assert(remainingIterations > 0);

  while(remainingIterations > 0 && !d_errorSet.focusEmpty()){
    if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
    Assert(d_conflictVariables.empty());
    ArithVar x_i = d_errorSet.topFocusVariable();

    Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
    if(x_i == ARITHVAR_SENTINEL){
      Debug("arith::update") << "No inconsistent variables" << endl;
      return false; //sat
    }

    --remainingIterations;

    bool useVarOrderPivot = d_pivotsInRound.count(x_i) >=  options::arithPivotThreshold();
    if(!useVarOrderPivot){
      d_pivotsInRound.add(x_i);
    }


    Debug("arith::update")
      << "pivots in rounds: " <<  d_pivotsInRound.count(x_i)
      << " use " << useVarOrderPivot
      << " threshold " << options::arithPivotThreshold()
      << endl;

    LinearEqualityModule::VarPreferenceFunction pf = useVarOrderPivot ?
      &LinearEqualityModule::minVarOrder : &LinearEqualityModule::minBoundAndColLength;

    //DeltaRational beta_i = d_variables.getAssignment(x_i);
    ArithVar x_j = ARITHVAR_SENTINEL;

    int32_t prevErrorSize CVC5_UNUSED = d_errorSet.errorSize();

    if(d_variables.cmpAssignmentLowerBound(x_i) < 0 ){
      x_j = d_linEq.selectSlackUpperBound(x_i, pf);
      if(x_j == ARITHVAR_SENTINEL ){
        Unreachable();
        // ++(d_statistics.d_statUpdateConflicts);
        // reportConflict(x_i);
        // ++(d_statistics.d_simplexConflicts);
        // Node conflict = d_linEq.generateConflictBelowLowerBound(x_i); //unsat
        // d_conflictVariable = x_i;
        // reportConflict(conflict);
        // return true;
      }else{
        const DeltaRational& l_i = d_variables.getLowerBound(x_i);
        d_linEq.pivotAndUpdate(x_i, x_j, l_i);
      }
    }else if(d_variables.cmpAssignmentUpperBound(x_i) > 0){
      x_j = d_linEq.selectSlackLowerBound(x_i, pf);
      if(x_j == ARITHVAR_SENTINEL ){
        Unreachable();
        // ++(d_statistics.d_statUpdateConflicts);
        // reportConflict(x_i);
        // ++(d_statistics.d_simplexConflicts);
        // Node conflict = d_linEq.generateConflictAboveUpperBound(x_i); //unsat
        // d_conflictVariable = x_i;
        // reportConflict(conflict);
        // return true;
      }else{
        const DeltaRational& u_i = d_variables.getUpperBound(x_i);
        d_linEq.pivotAndUpdate(x_i, x_j, u_i);
      }
    }
    Assert(x_j != ARITHVAR_SENTINEL);

    bool conflict = processSignals();
    int32_t currErrorSize CVC5_UNUSED = d_errorSet.errorSize();
    d_pivots++;

    if(Debug.isOn("arith::dual")){
      Debug("arith::dual")
        << "#" << d_pivots
        << " c" << conflict
        << " d" << (prevErrorSize - currErrorSize)
        << " f"  << d_errorSet.inError(x_j)
        << " h" << d_conflictVariables.isMember(x_j)
        << " " << x_i << "->" << x_j
        << endl;
    }

    if(conflict){
      return true;
    }
  }
  Assert(!d_errorSet.focusEmpty() || d_errorSet.errorEmpty());
  Assert(remainingIterations == 0 || d_errorSet.focusEmpty());
  Assert(d_errorSet.noSignals());

  return false;
}

}  // 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, Aina Niemetz, Morgan Deters
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		#include "theory/arith/dual_simplex.h"
17
18		#include "base/output.h"
19		#include "options/arith_options.h"
20		#include "smt/smt_statistics_registry.h"
21		#include "theory/arith/constraint.h"
22		#include "theory/arith/error_set.h"
23		#include "theory/arith/linear_equality.h"
24
25
26		using namespace std;
27
28		namespace cvc5 {
29		namespace theory {
30		namespace arith {
31
32	9917	DualSimplexDecisionProcedure::DualSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
33		: SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
34		, d_pivotsInRound()
35	9917	, d_statistics(d_pivots)
36	9917	{ }
37
38	9917	DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots)
39	9917	: d_statUpdateConflicts(smtStatisticsRegistry().registerInt(
40	19834	"theory::arith::dual::UpdateConflicts")),
41	9917	d_processSignalsTime(smtStatisticsRegistry().registerTimer(
42	19834	"theory::arith::dual::findConflictOnTheQueueTime")),
43	9917	d_simplexConflicts(smtStatisticsRegistry().registerInt(
44	19834	"theory::arith::dual::simplexConflicts")),
45	9917	d_recentViolationCatches(smtStatisticsRegistry().registerInt(
46	19834	"theory::arith::dual::recentViolationCatches")),
47	9917	d_searchTime(smtStatisticsRegistry().registerTimer(
48	19834	"theory::arith::dual::searchTime")),
49		d_finalCheckPivotCounter(
50	9917	smtStatisticsRegistry().registerReference<uint32_t>(
51	59502	"theory::arith::dual::lastPivots", pivots))
52		{
53	9917	}
54
55	1837994	Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
56	1837994	Assert(d_conflictVariables.empty());
57
58		static thread_local unsigned int instance = 0;
59	1837994	instance = instance + 1;
60	1837994	d_pivots = 0;
61
62	1837994	if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
63	987646	Debug("arith::findModel") << "dualFindModel("<< instance <<") trivial" << endl;
64	987646	return Result::SAT;
65		}
66
67		// We need to reduce this because of
68	850348	d_errorSet.reduceToSignals();
69	850348	d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
70
71	850348	if(processSignals()){
72	29245	d_conflictVariables.purge();
73
74	29245	Debug("arith::findModel") << "dualFindModel("<< instance <<") early conflict" << endl;
75	29245	return Result::UNSAT;
76	821103	}else if(d_errorSet.errorEmpty()){
77	724493	Debug("arith::findModel") << "dualFindModel("<< instance <<") fixed itself" << endl;
78	724493	Assert(!d_errorSet.moreSignals());
79	724493	return Result::SAT;
80		}
81
82	96610	Debug("arith::findModel") << "dualFindModel(" << instance <<") start non-trivial" << endl;
83
84	96610	Result::Sat result = Result::SAT_UNKNOWN;
85
86		static const bool verbose = false;
87	96610	exactResult \|= options::arithStandardCheckVarOrderPivots() < 0;
88
89
90	96610	uint32_t checkPeriod = options::arithSimplexCheckPeriod();
91	96610	if(result == Result::SAT_UNKNOWN){
92	96610	uint32_t numDifferencePivots = options::arithHeuristicPivots() < 0 ?
93	96610	d_numVariables + 1 : options::arithHeuristicPivots();
94		// The signed to unsigned conversion is safe.
95	96610	if(numDifferencePivots > 0){
96
97	83633	d_errorSet.setSelectionRule(d_heuristicRule);
98	83633	if(searchForFeasibleSolution(numDifferencePivots)){
99	12025	result = Result::UNSAT;
100		}
101		}
102
103		if (verbose && numDifferencePivots > 0)
104		{
105		if (result == Result::UNSAT)
106		{
107		CVC5Message() << "diff order found unsat" << endl;
108		}
109		else if (d_errorSet.errorEmpty())
110		{
111		CVC5Message() << "diff order found model" << endl;
112		}
113		else
114		{
115		CVC5Message() << "diff order missed" << endl;
116		}
117		}
118		}
119	96610	Assert(!d_errorSet.moreSignals());
120
121	96610	if(!d_errorSet.errorEmpty() && result != Result::UNSAT){
122	14758	if(exactResult){
123	1550	d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
124	4662	while(!d_errorSet.errorEmpty() && result != Result::UNSAT){
125	1556	Assert(checkPeriod > 0);
126	1556	if(searchForFeasibleSolution(checkPeriod)){
127	207	result = Result::UNSAT;
128		}
129		}
130	13208	}else if( options::arithStandardCheckVarOrderPivots() > 0){
131	13208	d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
132	13208	if(searchForFeasibleSolution(options::arithStandardCheckVarOrderPivots())){
133	3625	result = Result::UNSAT;
134		}
135		if (verbose)
136		{
137		if (result == Result::UNSAT)
138		{
139		CVC5Message() << "restricted var order found unsat" << endl;
140		}
141		else if (d_errorSet.errorEmpty())
142		{
143		CVC5Message() << "restricted var order found model" << endl;
144		}
145		else
146		{
147		CVC5Message() << "restricted var order missed" << endl;
148		}
149		}
150		}
151		}
152
153	96610	Assert(!d_errorSet.moreSignals());
154	96610	if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
155	80753	result = Result::SAT;
156		}
157
158	96610	d_pivotsInRound.purge();
159		// ensure that the conflict variable is still in the queue.
160	96610	d_conflictVariables.purge();
161
162	96610	Debug("arith::findModel") << "end findModel() " << instance << " " << result << endl;
163
164	96610	return result;
165		}
166
167		//corresponds to Check() in dM06
168		//template <SimplexDecisionProcedure::PreferenceFunction pf>
169	98397	bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
170	196794	TimerStat::CodeTimer codeTimer(d_statistics.d_searchTime);
171
172	98397	Debug("arith") << "searchForFeasibleSolution" << endl;
173	98397	Assert(remainingIterations > 0);
174
175	489081	while(remainingIterations > 0 && !d_errorSet.focusEmpty()){
176	211199	if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
177	211199	Assert(d_conflictVariables.empty());
178	211199	ArithVar x_i = d_errorSet.topFocusVariable();
179
180	211199	Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
181	211199	if(x_i == ARITHVAR_SENTINEL){
182		Debug("arith::update") << "No inconsistent variables" << endl;
183	15857	return false; //sat
184		}
185
186	211199	--remainingIterations;
187
188	211199	bool useVarOrderPivot = d_pivotsInRound.count(x_i) >= options::arithPivotThreshold();
189	211199	if(!useVarOrderPivot){
190	211083	d_pivotsInRound.add(x_i);
191		}
192
193
194	422398	Debug("arith::update")
195	422398	<< "pivots in rounds: " << d_pivotsInRound.count(x_i)
196	211199	<< " use " << useVarOrderPivot
197	422398	<< " threshold " << options::arithPivotThreshold()
198	211199	<< endl;
199
200	211199	LinearEqualityModule::VarPreferenceFunction pf = useVarOrderPivot ?
201		&LinearEqualityModule::minVarOrder : &LinearEqualityModule::minBoundAndColLength;
202
203		//DeltaRational beta_i = d_variables.getAssignment(x_i);
204	211199	ArithVar x_j = ARITHVAR_SENTINEL;
205
206	211199	int32_t prevErrorSize CVC5_UNUSED = d_errorSet.errorSize();
207
208	211199	if(d_variables.cmpAssignmentLowerBound(x_i) < 0 ){
209	112495	x_j = d_linEq.selectSlackUpperBound(x_i, pf);
210	112495	if(x_j == ARITHVAR_SENTINEL ){
211		Unreachable();
212		// ++(d_statistics.d_statUpdateConflicts);
213		// reportConflict(x_i);
214		// ++(d_statistics.d_simplexConflicts);
215		// Node conflict = d_linEq.generateConflictBelowLowerBound(x_i); //unsat
216		// d_conflictVariable = x_i;
217		// reportConflict(conflict);
218		// return true;
219		}else{
220	112495	const DeltaRational& l_i = d_variables.getLowerBound(x_i);
221	112495	d_linEq.pivotAndUpdate(x_i, x_j, l_i);
222		}
223	98704	}else if(d_variables.cmpAssignmentUpperBound(x_i) > 0){
224	98704	x_j = d_linEq.selectSlackLowerBound(x_i, pf);
225	98704	if(x_j == ARITHVAR_SENTINEL ){
226		Unreachable();
227		// ++(d_statistics.d_statUpdateConflicts);
228		// reportConflict(x_i);
229		// ++(d_statistics.d_simplexConflicts);
230		// Node conflict = d_linEq.generateConflictAboveUpperBound(x_i); //unsat
231		// d_conflictVariable = x_i;
232		// reportConflict(conflict);
233		// return true;
234		}else{
235	98704	const DeltaRational& u_i = d_variables.getUpperBound(x_i);
236	98704	d_linEq.pivotAndUpdate(x_i, x_j, u_i);
237		}
238		}
239	211199	Assert(x_j != ARITHVAR_SENTINEL);
240
241	211199	bool conflict = processSignals();
242	211199	int32_t currErrorSize CVC5_UNUSED = d_errorSet.errorSize();
243	211199	d_pivots++;
244
245	211199	if(Debug.isOn("arith::dual")){
246		Debug("arith::dual")
247		<< "#" << d_pivots
248		<< " c" << conflict
249		<< " d" << (prevErrorSize - currErrorSize)
250		<< " f" << d_errorSet.inError(x_j)
251		<< " h" << d_conflictVariables.isMember(x_j)
252		<< " " << x_i << "->" << x_j
253		<< endl;
254		}
255
256	211199	if(conflict){
257	15857	return true;
258		}
259		}
260	82540	Assert(!d_errorSet.focusEmpty() \|\| d_errorSet.errorEmpty());
261	82540	Assert(remainingIterations == 0 \|\| d_errorSet.focusEmpty());
262	82540	Assert(d_errorSet.noSignals());
263
264	82540	return false;
265		}
266
267		} // namespace arith
268		} // namespace theory
269	29517	} // namespace cvc5