Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * This is an implementation of the Simplex Module for the Simplex for
      11                 :            :  * DPLL(T) decision procedure.
      12                 :            :  */
      13                 :            : #include "theory/arith/linear/dual_simplex.h"
      14                 :            : 
      15                 :            : #include "base/output.h"
      16                 :            : #include "options/arith_options.h"
      17                 :            : #include "smt/env.h"
      18                 :            : #include "theory/arith/linear/constraint.h"
      19                 :            : #include "theory/arith/linear/error_set.h"
      20                 :            : #include "theory/arith/linear/linear_equality.h"
      21                 :            : 
      22                 :            : using namespace std;
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : namespace theory {
      26                 :            : namespace arith::linear {
      27                 :            : 
      28                 :      51329 : DualSimplexDecisionProcedure::DualSimplexDecisionProcedure(
      29                 :            :     Env& env,
      30                 :            :     LinearEqualityModule& linEq,
      31                 :            :     ErrorSet& errors,
      32                 :            :     RaiseConflict conflictChannel,
      33                 :      51329 :     TempVarMalloc tvmalloc)
      34                 :            :     : SimplexDecisionProcedure(env, linEq, errors, conflictChannel, tvmalloc),
      35                 :      51329 :       d_pivotsInRound(),
      36                 :      51329 :       d_statistics(statisticsRegistry(), d_pivots)
      37                 :            : {
      38                 :      51329 : }
      39                 :            : 
      40                 :      51329 : DualSimplexDecisionProcedure::Statistics::Statistics(StatisticsRegistry& sr,
      41                 :      51329 :                                                      uint32_t& pivots)
      42                 :            :     : d_statUpdateConflicts(
      43                 :      51329 :           sr.registerInt("theory::arith::dual::UpdateConflicts")),
      44                 :            :       d_processSignalsTime(
      45                 :      51329 :           sr.registerTimer("theory::arith::dual::findConflictOnTheQueueTime")),
      46                 :            :       d_simplexConflicts(
      47                 :      51329 :           sr.registerInt("theory::arith::dual::simplexConflicts")),
      48                 :            :       d_recentViolationCatches(
      49                 :      51329 :           sr.registerInt("theory::arith::dual::recentViolationCatches")),
      50                 :      51329 :       d_searchTime(sr.registerTimer("theory::arith::dual::searchTime")),
      51                 :      51329 :       d_finalCheckPivotCounter(sr.registerReference<uint32_t>(
      52                 :            :           "theory::arith::dual::lastPivots", pivots))
      53                 :            : {
      54                 :      51329 : }
      55                 :            : 
      56                 :    3294447 : Result::Status DualSimplexDecisionProcedure::dualFindModel(bool exactResult)
      57                 :            : {
      58 [ -  + ][ -  + ]:    3294447 :   Assert(d_conflictVariables.empty());
                 [ -  - ]
      59                 :            : 
      60                 :    3294447 :   d_pivots = 0;
      61                 :            : 
      62 [ +  + ][ +  + ]:    3294447 :   if (d_errorSet.errorEmpty() && !d_errorSet.moreSignals())
                 [ +  + ]
      63                 :            :   {
      64         [ +  - ]:    1868320 :     Trace("arith::findModel") << "dualFindModel() trivial" << endl;
      65                 :    1868320 :     return Result::SAT;
      66                 :            :   }
      67                 :            : 
      68                 :            :   // We need to reduce this because of
      69                 :    1426127 :   d_errorSet.reduceToSignals();
      70                 :    1426127 :   d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
      71                 :            : 
      72         [ +  + ]:    1426127 :   if (processSignals())
      73                 :            :   {
      74                 :      45034 :     d_conflictVariables.purge();
      75                 :            : 
      76         [ +  - ]:      45034 :     Trace("arith::findModel") << "dualFindModel() early conflict" << endl;
      77                 :      45034 :     return Result::UNSAT;
      78                 :            :   }
      79         [ +  + ]:    1381093 :   else if (d_errorSet.errorEmpty())
      80                 :            :   {
      81         [ +  - ]:    1210726 :     Trace("arith::findModel") << "dualFindModel() fixed itself" << endl;
      82 [ -  + ][ -  + ]:    1210726 :     Assert(!d_errorSet.moreSignals());
                 [ -  - ]
      83                 :    1210726 :     return Result::SAT;
      84                 :            :   }
      85                 :            : 
      86         [ +  - ]:     170367 :   Trace("arith::findModel") << "dualFindModel() start non-trivial" << endl;
      87                 :            : 
      88                 :     170367 :   Result::Status result = Result::UNKNOWN;
      89                 :            : 
      90                 :     170367 :   exactResult |= d_varOrderPivotLimit < 0;
      91                 :            : 
      92                 :     170367 :   uint32_t checkPeriod = options().arith.arithSimplexCheckPeriod;
      93                 :            : 
      94                 :     170367 :   uint32_t numDifferencePivots = options().arith.arithHeuristicPivots < 0
      95                 :      25685 :                                      ? d_numVariables + 1
      96         [ +  + ]:     170367 :                                      : options().arith.arithHeuristicPivots;
      97                 :            :   // The signed to unsigned conversion is safe.
      98         [ +  + ]:     170367 :   if (numDifferencePivots > 0)
      99                 :            :   {
     100                 :     159060 :     d_errorSet.setSelectionRule(d_heuristicRule);
     101         [ +  + ]:     159060 :     if (searchForFeasibleSolution(numDifferencePivots))
     102                 :            :     {
     103                 :      17594 :       result = Result::UNSAT;
     104                 :            :     }
     105                 :            :   }
     106 [ -  + ][ -  + ]:     170367 :   Assert(!d_errorSet.moreSignals());
                 [ -  - ]
     107                 :            : 
     108 [ +  + ][ +  + ]:     170367 :   if (!d_errorSet.errorEmpty() && result != Result::UNSAT)
                 [ +  + ]
     109                 :            :   {
     110         [ +  + ]:      13776 :     if (exactResult)
     111                 :            :     {
     112                 :       2155 :       d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
     113 [ +  + ][ +  + ]:       4322 :       while (!d_errorSet.errorEmpty() && result != Result::UNSAT)
                 [ +  + ]
     114                 :            :       {
     115 [ -  + ][ -  + ]:       2167 :         Assert(checkPeriod > 0);
                 [ -  - ]
     116         [ +  + ]:       2167 :         if (searchForFeasibleSolution(checkPeriod))
     117                 :            :         {
     118                 :        308 :           result = Result::UNSAT;
     119                 :            :         }
     120                 :            :       }
     121                 :            :     }
     122         [ +  - ]:      11621 :     else if (d_varOrderPivotLimit > 0)
     123                 :            :     {
     124                 :      11621 :       d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
     125         [ +  + ]:      11621 :       if (searchForFeasibleSolution(d_varOrderPivotLimit))
     126                 :            :       {
     127                 :       3209 :         result = Result::UNSAT;
     128                 :            :       }
     129                 :            :     }
     130                 :            :   }
     131                 :            : 
     132 [ -  + ][ -  + ]:     170367 :   Assert(!d_errorSet.moreSignals());
                 [ -  - ]
     133 [ +  + ][ +  - ]:     170367 :   if (result == Result::UNKNOWN && d_errorSet.errorEmpty())
                 [ +  + ]
     134                 :            :   {
     135                 :     149256 :     result = Result::SAT;
     136                 :            :   }
     137                 :            : 
     138                 :     170367 :   d_pivotsInRound.purge();
     139                 :            :   // ensure that the conflict variable is still in the queue.
     140                 :     170367 :   d_conflictVariables.purge();
     141                 :            : 
     142         [ +  - ]:     170367 :   Trace("arith::findModel") << "end findModel() " << result << endl;
     143                 :            : 
     144                 :     170367 :   return result;
     145                 :            : }
     146                 :            : 
     147                 :            : // corresponds to Check() in dM06
     148                 :            : // template <SimplexDecisionProcedure::PreferenceFunction pf>
     149                 :     172848 : bool DualSimplexDecisionProcedure::searchForFeasibleSolution(
     150                 :            :     uint32_t remainingIterations)
     151                 :            : {
     152                 :     172848 :   TimerStat::CodeTimer codeTimer(d_statistics.d_searchTime);
     153                 :            : 
     154         [ +  - ]:     172848 :   Trace("arith") << "searchForFeasibleSolution" << endl;
     155 [ -  + ][ -  + ]:     172848 :   Assert(remainingIterations > 0);
                 [ -  - ]
     156                 :            : 
     157 [ +  + ][ +  + ]:     482072 :   while (remainingIterations > 0 && !d_errorSet.focusEmpty())
                 [ +  + ]
     158                 :            :   {
     159         [ -  + ]:     330335 :     if (TraceIsOn("paranoid:check_tableau"))
     160                 :            :     {
     161                 :          0 :       d_linEq.debugCheckTableau();
     162                 :            :     }
     163 [ -  + ][ -  + ]:     330335 :     Assert(d_conflictVariables.empty());
                 [ -  - ]
     164                 :     330335 :     ArithVar x_i = d_errorSet.topFocusVariable();
     165                 :            : 
     166         [ +  - ]:     660670 :     Trace("arith::update::select")
     167                 :     330335 :         << "selectSmallestInconsistentVar()=" << x_i << endl;
     168         [ -  + ]:     330335 :     if (x_i == ARITHVAR_SENTINEL)
     169                 :            :     {
     170         [ -  - ]:          0 :       Trace("arith::update") << "No inconsistent variables" << endl;
     171                 :      21111 :       return false;  // sat
     172                 :            :     }
     173                 :            : 
     174                 :     330335 :     --remainingIterations;
     175                 :            : 
     176                 :            :     bool useVarOrderPivot =
     177                 :     330335 :         d_pivotsInRound.count(x_i) >= options().arith.arithPivotThreshold;
     178         [ +  + ]:     330335 :     if (!useVarOrderPivot)
     179                 :            :     {
     180                 :     330098 :       d_pivotsInRound.add(x_i);
     181                 :            :     }
     182                 :            : 
     183         [ +  - ]:     660670 :     Trace("arith::update") << "pivots in rounds: " << d_pivotsInRound.count(x_i)
     184                 :          0 :                            << " use " << useVarOrderPivot << " threshold "
     185                 :     330335 :                            << options().arith.arithPivotThreshold << std::endl;
     186                 :            : 
     187         [ +  + ]:     330335 :     LinearEqualityModule::VarPreferenceFunction pf =
     188                 :            :         useVarOrderPivot ? &LinearEqualityModule::minVarOrder
     189                 :            :                          : &LinearEqualityModule::minBoundAndColLength;
     190                 :            : 
     191                 :            :     // DeltaRational beta_i = d_variables.getAssignment(x_i);
     192                 :     330335 :     ArithVar x_j = ARITHVAR_SENTINEL;
     193                 :            : 
     194                 :     330335 :     int32_t prevErrorSize CVC5_UNUSED = d_errorSet.errorSize();
     195                 :            : 
     196         [ +  + ]:     330335 :     if (d_variables.cmpAssignmentLowerBound(x_i) < 0)
     197                 :            :     {
     198                 :     164837 :       x_j = d_linEq.selectSlackUpperBound(x_i, pf);
     199         [ -  + ]:     164837 :       if (x_j == ARITHVAR_SENTINEL)
     200                 :            :       {
     201                 :          0 :         Unreachable();
     202                 :            :         // ++(d_statistics.d_statUpdateConflicts);
     203                 :            :         // reportConflict(x_i);
     204                 :            :         // ++(d_statistics.d_simplexConflicts);
     205                 :            :         // Node conflict = d_linEq.generateConflictBelowLowerBound(x_i); //unsat
     206                 :            :         // d_conflictVariable = x_i;
     207                 :            :         // reportConflict(conflict);
     208                 :            :         // return true;
     209                 :            :       }
     210                 :            :       else
     211                 :            :       {
     212                 :     164837 :         const DeltaRational& l_i = d_variables.getLowerBound(x_i);
     213                 :     164837 :         d_linEq.pivotAndUpdate(x_i, x_j, l_i);
     214                 :            :       }
     215                 :            :     }
     216         [ +  - ]:     165498 :     else if (d_variables.cmpAssignmentUpperBound(x_i) > 0)
     217                 :            :     {
     218                 :     165498 :       x_j = d_linEq.selectSlackLowerBound(x_i, pf);
     219         [ -  + ]:     165498 :       if (x_j == ARITHVAR_SENTINEL)
     220                 :            :       {
     221                 :          0 :         Unreachable();
     222                 :            :         // ++(d_statistics.d_statUpdateConflicts);
     223                 :            :         // reportConflict(x_i);
     224                 :            :         // ++(d_statistics.d_simplexConflicts);
     225                 :            :         // Node conflict = d_linEq.generateConflictAboveUpperBound(x_i); //unsat
     226                 :            :         // d_conflictVariable = x_i;
     227                 :            :         // reportConflict(conflict);
     228                 :            :         // return true;
     229                 :            :       }
     230                 :            :       else
     231                 :            :       {
     232                 :     165498 :         const DeltaRational& u_i = d_variables.getUpperBound(x_i);
     233                 :     165498 :         d_linEq.pivotAndUpdate(x_i, x_j, u_i);
     234                 :            :       }
     235                 :            :     }
     236 [ -  + ][ -  + ]:     330335 :     Assert(x_j != ARITHVAR_SENTINEL);
                 [ -  - ]
     237                 :            : 
     238                 :     330335 :     bool conflict = processSignals();
     239                 :     330335 :     int32_t currErrorSize CVC5_UNUSED = d_errorSet.errorSize();
     240                 :     330335 :     d_pivots++;
     241                 :            : 
     242         [ -  + ]:     330335 :     if (TraceIsOn("arith::dual"))
     243                 :            :     {
     244         [ -  - ]:          0 :       Trace("arith::dual") << "#" << d_pivots << " c" << conflict << " d"
     245                 :          0 :                            << (prevErrorSize - currErrorSize) << " f"
     246                 :          0 :                            << d_errorSet.inError(x_j) << " h"
     247                 :          0 :                            << d_conflictVariables.isMember(x_j) << " " << x_i
     248                 :          0 :                            << "->" << x_j << endl;
     249                 :            :     }
     250                 :            : 
     251         [ +  + ]:     330335 :     if (conflict)
     252                 :            :     {
     253                 :      21111 :       return true;
     254                 :            :     }
     255                 :            :   }
     256 [ +  + ][ +  - ]:     151737 :   Assert(!d_errorSet.focusEmpty() || d_errorSet.errorEmpty());
         [ -  + ][ -  + ]
                 [ -  - ]
     257 [ +  + ][ +  - ]:     151737 :   Assert(remainingIterations == 0 || d_errorSet.focusEmpty());
         [ -  + ][ -  + ]
                 [ -  - ]
     258 [ -  + ][ -  + ]:     151737 :   Assert(d_errorSet.noSignals());
                 [ -  - ]
     259                 :            : 
     260                 :     151737 :   return false;
     261                 :     172848 : }
     262                 :            : 
     263                 :            : }  // namespace arith::linear
     264                 :            : }  // namespace theory
     265                 :            : }  // namespace cvc5::internal