Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/dual_simplex.cpp	Lines:	105	120	87.5 %
Date:	2021-11-06	Branches:	195	538	36.2 %


/******************************************************************************
 * 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/env.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(
    Env& env,
    LinearEqualityModule& linEq,
    ErrorSet& errors,
    RaiseConflict conflictChannel,
    TempVarMalloc tvmalloc)
    : SimplexDecisionProcedure(env, 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;

  exactResult |= d_varOrderPivotLimit < 0;

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

      d_errorSet.setSelectionRule(d_heuristicRule);
      if(searchForFeasibleSolution(numDifferencePivots)){
        result = Result::UNSAT;
      }
    }
  }
  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 (d_varOrderPivotLimit > 0)
    {
      d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
      if (searchForFeasibleSolution(d_varOrderPivotLimit))
      {
        result = Result::UNSAT;
      }
    }
  }

  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().arith.arithPivotThreshold;
    if(!useVarOrderPivot){
      d_pivotsInRound.add(x_i);
    }

    Debug("arith::update") << "pivots in rounds: " << d_pivotsInRound.count(x_i)
                           << " use " << useVarOrderPivot << " threshold "
                           << options().arith.arithPivotThreshold << std::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/env.h"
21		#include "smt/smt_statistics_registry.h"
22		#include "theory/arith/constraint.h"
23		#include "theory/arith/error_set.h"
24		#include "theory/arith/linear_equality.h"
25
26
27		using namespace std;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace arith {
32
33	15272	DualSimplexDecisionProcedure::DualSimplexDecisionProcedure(
34		Env& env,
35		LinearEqualityModule& linEq,
36		ErrorSet& errors,
37		RaiseConflict conflictChannel,
38	15272	TempVarMalloc tvmalloc)
39		: SimplexDecisionProcedure(env, linEq, errors, conflictChannel, tvmalloc),
40		d_pivotsInRound(),
41	15272	d_statistics(d_pivots)
42	15272	{ }
43
44	15272	DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots)
45	15272	: d_statUpdateConflicts(smtStatisticsRegistry().registerInt(
46	30544	"theory::arith::dual::UpdateConflicts")),
47	15272	d_processSignalsTime(smtStatisticsRegistry().registerTimer(
48	30544	"theory::arith::dual::findConflictOnTheQueueTime")),
49	15272	d_simplexConflicts(smtStatisticsRegistry().registerInt(
50	30544	"theory::arith::dual::simplexConflicts")),
51	15272	d_recentViolationCatches(smtStatisticsRegistry().registerInt(
52	30544	"theory::arith::dual::recentViolationCatches")),
53	15272	d_searchTime(smtStatisticsRegistry().registerTimer(
54	30544	"theory::arith::dual::searchTime")),
55		d_finalCheckPivotCounter(
56	15272	smtStatisticsRegistry().registerReference<uint32_t>(
57	91632	"theory::arith::dual::lastPivots", pivots))
58		{
59	15272	}
60
61	2388335	Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
62	2388335	Assert(d_conflictVariables.empty());
63
64		static thread_local unsigned int instance = 0;
65	2388335	instance = instance + 1;
66	2388335	d_pivots = 0;
67
68	2388335	if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
69	1353125	Debug("arith::findModel") << "dualFindModel("<< instance <<") trivial" << endl;
70	1353125	return Result::SAT;
71		}
72
73		// We need to reduce this because of
74	1035210	d_errorSet.reduceToSignals();
75	1035210	d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
76
77	1035210	if(processSignals()){
78	35498	d_conflictVariables.purge();
79
80	35498	Debug("arith::findModel") << "dualFindModel("<< instance <<") early conflict" << endl;
81	35498	return Result::UNSAT;
82	999712	}else if(d_errorSet.errorEmpty()){
83	892188	Debug("arith::findModel") << "dualFindModel("<< instance <<") fixed itself" << endl;
84	892188	Assert(!d_errorSet.moreSignals());
85	892188	return Result::SAT;
86		}
87
88	107524	Debug("arith::findModel") << "dualFindModel(" << instance <<") start non-trivial" << endl;
89
90	107524	Result::Sat result = Result::SAT_UNKNOWN;
91
92	107524	exactResult \|= d_varOrderPivotLimit < 0;
93
94	107524	uint32_t checkPeriod = options().arith.arithSimplexCheckPeriod;
95	107524	if(result == Result::SAT_UNKNOWN){
96	107524	uint32_t numDifferencePivots = options().arith.arithHeuristicPivots < 0
97	14168	? d_numVariables + 1
98	121692	: options().arith.arithHeuristicPivots;
99		// The signed to unsigned conversion is safe.
100	107524	if(numDifferencePivots > 0){
101
102	94448	d_errorSet.setSelectionRule(d_heuristicRule);
103	94448	if(searchForFeasibleSolution(numDifferencePivots)){
104	13428	result = Result::UNSAT;
105		}
106		}
107		}
108	107524	Assert(!d_errorSet.moreSignals());
109
110	107524	if(!d_errorSet.errorEmpty() && result != Result::UNSAT){
111	15465	if(exactResult){
112	15465	d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
113	46547	while(!d_errorSet.errorEmpty() && result != Result::UNSAT){
114	15541	Assert(checkPeriod > 0);
115	15541	if(searchForFeasibleSolution(checkPeriod)){
116	3946	result = Result::UNSAT;
117		}
118		}
119		}
120		else if (d_varOrderPivotLimit > 0)
121		{
122		d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
123		if (searchForFeasibleSolution(d_varOrderPivotLimit))
124		{
125		result = Result::UNSAT;
126		}
127		}
128		}
129
130	107524	Assert(!d_errorSet.moreSignals());
131	107524	if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
132	90150	result = Result::SAT;
133		}
134
135	107524	d_pivotsInRound.purge();
136		// ensure that the conflict variable is still in the queue.
137	107524	d_conflictVariables.purge();
138
139	107524	Debug("arith::findModel") << "end findModel() " << instance << " " << result << endl;
140
141	107524	return result;
142		}
143
144		//corresponds to Check() in dM06
145		//template <SimplexDecisionProcedure::PreferenceFunction pf>
146	109989	bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
147	219978	TimerStat::CodeTimer codeTimer(d_statistics.d_searchTime);
148
149	109989	Debug("arith") << "searchForFeasibleSolution" << endl;
150	109989	Assert(remainingIterations > 0);
151
152	581893	while(remainingIterations > 0 && !d_errorSet.focusEmpty()){
153	253326	if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
154	253326	Assert(d_conflictVariables.empty());
155	253326	ArithVar x_i = d_errorSet.topFocusVariable();
156
157	253326	Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
158	253326	if(x_i == ARITHVAR_SENTINEL){
159		Debug("arith::update") << "No inconsistent variables" << endl;
160	17374	return false; //sat
161		}
162
163	253326	--remainingIterations;
164
165		bool useVarOrderPivot =
166	253326	d_pivotsInRound.count(x_i) >= options().arith.arithPivotThreshold;
167	253326	if(!useVarOrderPivot){
168	237188	d_pivotsInRound.add(x_i);
169		}
170
171	506652	Debug("arith::update") << "pivots in rounds: " << d_pivotsInRound.count(x_i)
172	253326	<< " use " << useVarOrderPivot << " threshold "
173	253326	<< options().arith.arithPivotThreshold << std::endl;
174
175	253326	LinearEqualityModule::VarPreferenceFunction pf = useVarOrderPivot ?
176		&LinearEqualityModule::minVarOrder : &LinearEqualityModule::minBoundAndColLength;
177
178		//DeltaRational beta_i = d_variables.getAssignment(x_i);
179	253326	ArithVar x_j = ARITHVAR_SENTINEL;
180
181	253326	int32_t prevErrorSize CVC5_UNUSED = d_errorSet.errorSize();
182
183	253326	if(d_variables.cmpAssignmentLowerBound(x_i) < 0 ){
184	140661	x_j = d_linEq.selectSlackUpperBound(x_i, pf);
185	140661	if(x_j == ARITHVAR_SENTINEL ){
186		Unreachable();
187		// ++(d_statistics.d_statUpdateConflicts);
188		// reportConflict(x_i);
189		// ++(d_statistics.d_simplexConflicts);
190		// Node conflict = d_linEq.generateConflictBelowLowerBound(x_i); //unsat
191		// d_conflictVariable = x_i;
192		// reportConflict(conflict);
193		// return true;
194		}else{
195	140661	const DeltaRational& l_i = d_variables.getLowerBound(x_i);
196	140661	d_linEq.pivotAndUpdate(x_i, x_j, l_i);
197		}
198	112665	}else if(d_variables.cmpAssignmentUpperBound(x_i) > 0){
199	112665	x_j = d_linEq.selectSlackLowerBound(x_i, pf);
200	112665	if(x_j == ARITHVAR_SENTINEL ){
201		Unreachable();
202		// ++(d_statistics.d_statUpdateConflicts);
203		// reportConflict(x_i);
204		// ++(d_statistics.d_simplexConflicts);
205		// Node conflict = d_linEq.generateConflictAboveUpperBound(x_i); //unsat
206		// d_conflictVariable = x_i;
207		// reportConflict(conflict);
208		// return true;
209		}else{
210	112665	const DeltaRational& u_i = d_variables.getUpperBound(x_i);
211	112665	d_linEq.pivotAndUpdate(x_i, x_j, u_i);
212		}
213		}
214	253326	Assert(x_j != ARITHVAR_SENTINEL);
215
216	253326	bool conflict = processSignals();
217	253326	int32_t currErrorSize CVC5_UNUSED = d_errorSet.errorSize();
218	253326	d_pivots++;
219
220	253326	if(Debug.isOn("arith::dual")){
221		Debug("arith::dual")
222		<< "#" << d_pivots
223		<< " c" << conflict
224		<< " d" << (prevErrorSize - currErrorSize)
225		<< " f" << d_errorSet.inError(x_j)
226		<< " h" << d_conflictVariables.isMember(x_j)
227		<< " " << x_i << "->" << x_j
228		<< endl;
229		}
230
231	253326	if(conflict){
232	17374	return true;
233		}
234		}
235	92615	Assert(!d_errorSet.focusEmpty() \|\| d_errorSet.errorEmpty());
236	92615	Assert(remainingIterations == 0 \|\| d_errorSet.focusEmpty());
237	92615	Assert(d_errorSet.noSignals());
238
239	92615	return false;
240		}
241
242		} // namespace arith
243		} // namespace theory
244	31137	} // namespace cvc5