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                 :            :  * Implementation of new non-linear solver.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/arith/nl/coverings_solver.h"
      14                 :            : 
      15                 :            : #include "expr/skolem_manager.h"
      16                 :            : #include "options/arith_options.h"
      17                 :            : #include "smt/env.h"
      18                 :            : #include "theory/arith/inference_manager.h"
      19                 :            : #include "theory/arith/nl/coverings/cdcac.h"
      20                 :            : #include "theory/arith/nl/nl_model.h"
      21                 :            : #include "theory/arith/nl/poly_conversion.h"
      22                 :            : #include "theory/inference_id.h"
      23                 :            : #include "theory/theory.h"
      24                 :            : #include "util/rational.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : namespace theory {
      28                 :            : namespace arith {
      29                 :            : namespace nl {
      30                 :            : 
      31                 :      33060 : CoveringsSolver::CoveringsSolver(Env& env, InferenceManager& im, NlModel& model)
      32                 :            :     :
      33                 :            :       EnvObj(env),
      34                 :            : #ifdef CVC5_POLY_IMP
      35                 :      33060 :       d_CAC(env),
      36                 :            : #endif
      37                 :      33060 :       d_foundSatisfiability(false),
      38                 :      33060 :       d_im(im),
      39                 :      33060 :       d_model(model),
      40                 :      66120 :       d_eqsubs(env)
      41                 :            : {
      42                 :      33060 :   NodeManager* nm = nodeManager();
      43                 :      33060 :   d_ranVariable = NodeManager::mkDummySkolem("__z", nm->realType());
      44                 :      33060 : }
      45                 :            : 
      46                 :      32776 : CoveringsSolver::~CoveringsSolver() {}
      47                 :            : 
      48                 :        292 : void CoveringsSolver::initLastCall(const std::vector<Node>& assertions)
      49                 :            : {
      50                 :            : #ifdef CVC5_POLY_IMP
      51         [ -  + ]:        292 :   if (TraceIsOn("nl-cov"))
      52                 :            :   {
      53         [ -  - ]:          0 :     Trace("nl-cov") << "CoveringsSolver::initLastCall" << std::endl;
      54         [ -  - ]:          0 :     Trace("nl-cov") << "* Assertions: " << std::endl;
      55         [ -  - ]:          0 :     for (const Node& a : assertions)
      56                 :            :     {
      57         [ -  - ]:          0 :       Trace("nl-cov") << "  " << a << std::endl;
      58                 :            :     }
      59                 :            :   }
      60         [ +  + ]:        292 :   if (options().arith.nlCovVarElim)
      61                 :            :   {
      62                 :        178 :     d_eqsubs.reset();
      63                 :        178 :     std::vector<Node> processed = d_eqsubs.eliminateEqualities(assertions);
      64         [ +  + ]:        178 :     if (d_eqsubs.hasConflict())
      65                 :            :     {
      66                 :         12 :       Node lem = nodeManager()->mkAnd(d_eqsubs.getConflict()).negate();
      67                 :         12 :       d_im.addPendingLemma(
      68                 :            :           lem, InferenceId::ARITH_NL_COVERING_CONFLICT, nullptr);
      69         [ +  - ]:         12 :       Trace("nl-cov") << "Found conflict: " << lem << std::endl;
      70                 :         12 :       return;
      71                 :         12 :     }
      72         [ -  + ]:        166 :     if (TraceIsOn("nl-cov"))
      73                 :            :     {
      74         [ -  - ]:          0 :       Trace("nl-cov") << "After simplifications" << std::endl;
      75         [ -  - ]:          0 :       Trace("nl-cov") << "* Assertions: " << std::endl;
      76         [ -  - ]:          0 :       for (const Node& a : processed)
      77                 :            :       {
      78         [ -  - ]:          0 :         Trace("nl-cov") << "  " << a << std::endl;
      79                 :            :       }
      80                 :            :     }
      81                 :        166 :     d_CAC.reset();
      82         [ +  + ]:       4190 :     for (const Node& a : processed)
      83                 :            :     {
      84 [ -  + ][ -  + ]:       4024 :       Assert(!a.isConst());
                 [ -  - ]
      85                 :       4024 :       d_CAC.getConstraints().addConstraint(a);
      86                 :            :     }
      87         [ +  + ]:        178 :   }
      88                 :            :   else
      89                 :            :   {
      90                 :        114 :     d_CAC.reset();
      91         [ +  + ]:       1941 :     for (const Node& a : assertions)
      92                 :            :     {
      93 [ -  + ][ -  + ]:       1827 :       Assert(!a.isConst());
                 [ -  - ]
      94                 :       1827 :       d_CAC.getConstraints().addConstraint(a);
      95                 :            :     }
      96                 :            :   }
      97                 :        280 :   d_CAC.computeVariableOrdering();
      98                 :        280 :   d_CAC.retrieveInitialAssignment(d_model, d_ranVariable);
      99                 :            : #else
     100                 :            :   warning() << "Tried to use CoveringsSolver but libpoly is not available. Compile "
     101                 :            :                "with --poly."
     102                 :            :             << std::endl;
     103                 :            : #endif
     104                 :            : }
     105                 :            : 
     106                 :        280 : void CoveringsSolver::checkFull()
     107                 :            : {
     108                 :            : #ifdef CVC5_POLY_IMP
     109         [ -  + ]:        280 :   if (d_CAC.getConstraints().getConstraints().empty()) {
     110                 :          0 :     d_foundSatisfiability = true;
     111         [ -  - ]:          0 :     Trace("nl-cov") << "No constraints. Return." << std::endl;
     112                 :          0 :     return;
     113                 :            :   }
     114                 :        280 :   d_CAC.startNewProof();
     115                 :        280 :   auto covering = d_CAC.getUnsatCover();
     116         [ +  + ]:        280 :   if (covering.empty())
     117                 :            :   {
     118                 :        145 :     d_foundSatisfiability = true;
     119         [ +  - ]:        145 :     Trace("nl-cov") << "SAT: " << d_CAC.getModel() << std::endl;
     120                 :            :   }
     121                 :            :   else
     122                 :            :   {
     123                 :        135 :     d_foundSatisfiability = false;
     124                 :        135 :     auto mis = collectConstraints(covering);
     125         [ +  - ]:        135 :     Trace("nl-cov") << "Collected MIS: " << mis << std::endl;
     126 [ -  + ][ -  + ]:        135 :     Assert(!mis.empty()) << "Infeasible subset can not be empty";
                 [ -  - ]
     127         [ +  - ]:        135 :     Trace("nl-cov") << "UNSAT with MIS: " << mis << std::endl;
     128                 :        135 :     d_eqsubs.postprocessConflict(mis);
     129         [ +  - ]:        135 :     Trace("nl-cov") << "After postprocessing: " << mis << std::endl;
     130                 :        135 :     Node lem = nodeManager()->mkAnd(mis).notNode();
     131                 :        135 :     ProofGenerator* proof = d_CAC.closeProof(mis);
     132                 :        135 :     d_im.addPendingLemma(lem, InferenceId::ARITH_NL_COVERING_CONFLICT, proof);
     133                 :        135 :   }
     134                 :            : #else
     135                 :            :   warning() << "Tried to use CoveringsSolver but libpoly is not available. Compile "
     136                 :            :                "with --poly."
     137                 :            :             << std::endl;
     138                 :            : #endif
     139                 :        280 : }
     140                 :            : 
     141                 :          0 : void CoveringsSolver::checkPartial()
     142                 :            : {
     143                 :            : #ifdef CVC5_POLY_IMP
     144         [ -  - ]:          0 :   if (d_CAC.getConstraints().getConstraints().empty()) {
     145         [ -  - ]:          0 :     Trace("nl-cov") << "No constraints. Return." << std::endl;
     146                 :          0 :     return;
     147                 :            :   }
     148                 :          0 :   auto covering = d_CAC.getUnsatCover(true);
     149         [ -  - ]:          0 :   if (covering.empty())
     150                 :            :   {
     151                 :          0 :     d_foundSatisfiability = true;
     152         [ -  - ]:          0 :     Trace("nl-cov") << "SAT: " << d_CAC.getModel() << std::endl;
     153                 :            :   }
     154                 :            :   else
     155                 :            :   {
     156                 :          0 :     auto* nm = nodeManager();
     157                 :            :     Node first_var =
     158                 :          0 :         d_CAC.getConstraints().varMapper()(d_CAC.getVariableOrdering()[0]);
     159         [ -  - ]:          0 :     for (const auto& interval : covering)
     160                 :            :     {
     161                 :          0 :       Node premise;
     162                 :          0 :       Assert(!interval.d_origins.empty());
     163         [ -  - ]:          0 :       if (interval.d_origins.size() == 1)
     164                 :            :       {
     165                 :          0 :         premise = interval.d_origins[0];
     166                 :            :       }
     167                 :            :       else
     168                 :            :       {
     169                 :          0 :         premise = nm->mkNode(Kind::AND, interval.d_origins);
     170                 :            :       }
     171                 :            :       Node conclusion =
     172                 :          0 :           excluding_interval_to_lemma(first_var, interval.d_interval, false);
     173         [ -  - ]:          0 :       if (!conclusion.isNull())
     174                 :            :       {
     175                 :          0 :         Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion);
     176         [ -  - ]:          0 :         Trace("nl-cov") << "Excluding " << first_var << " -> "
     177                 :          0 :                         << interval.d_interval << " using " << lemma
     178                 :          0 :                         << std::endl;
     179                 :          0 :         d_im.addPendingLemma(lemma,
     180                 :            :                              InferenceId::ARITH_NL_COVERING_EXCLUDED_INTERVAL);
     181                 :          0 :       }
     182                 :          0 :     }
     183                 :          0 :   }
     184                 :            : #else
     185                 :            :   warning() << "Tried to use CoveringsSolver but libpoly is not available. Compile "
     186                 :            :                "with --poly."
     187                 :            :             << std::endl;
     188                 :            : #endif
     189                 :          0 : }
     190                 :            : 
     191                 :        136 : bool CoveringsSolver::constructModelIfAvailable(std::vector<Node>& assertions)
     192                 :            : {
     193                 :            : #ifdef CVC5_POLY_IMP
     194         [ -  + ]:        136 :   if (!d_foundSatisfiability)
     195                 :            :   {
     196                 :          0 :     return false;
     197                 :            :   }
     198                 :        136 :   bool foundNonVariable = false;
     199         [ +  + ]:        551 :   for (const auto& v : d_CAC.getVariableOrdering())
     200                 :            :   {
     201                 :        415 :     Node variable = d_CAC.getConstraints().varMapper()(v);
     202         [ -  + ]:        415 :     if (!Theory::isLeafOf(variable, TheoryId::THEORY_ARITH))
     203                 :            :     {
     204         [ -  - ]:          0 :       Trace("nl-cov") << "Not a variable: " << variable << std::endl;
     205                 :          0 :       foundNonVariable = true;
     206                 :            :     }
     207                 :        415 :     Node value = value_to_node(d_CAC.getModel().get(v), variable);
     208         [ -  + ]:        415 :     if (!addToModel(variable, value))
     209                 :            :     {
     210                 :          0 :       DebugUnhandled() << "Failed to add variable assignment to model";
     211                 :            :     }
     212                 :        415 :   }
     213         [ +  + ]:        449 :   for (const auto& sub : d_eqsubs.getSubstitutions())
     214                 :            :   {
     215         [ +  - ]:        626 :     Trace("nl-cov") << "EqSubs: " << sub.first << " -> " << sub.second
     216                 :        313 :                     << std::endl;
     217         [ -  + ]:        313 :     if (!addToModel(sub.first, sub.second))
     218                 :            :     {
     219                 :          0 :       DebugUnhandled() << "Failed to add equality substitution to model";
     220                 :            :     }
     221                 :            :   }
     222         [ -  + ]:        136 :   if (foundNonVariable)
     223                 :            :   {
     224         [ -  - ]:          0 :     Trace("nl-cov")
     225                 :          0 :         << "Some variable was an extended term, don't clear list of assertions."
     226                 :          0 :         << std::endl;
     227                 :          0 :     return false;
     228                 :            :   }
     229         [ +  - ]:        272 :   Trace("nl-cov") << "Constructed a full assignment, clear list of assertions."
     230                 :        136 :                   << std::endl;
     231                 :        136 :   assertions.clear();
     232                 :        136 :   return true;
     233                 :            : #else
     234                 :            :   warning() << "Tried to use CoveringsSolver but libpoly is not available. Compile "
     235                 :            :                "with --poly."
     236                 :            :             << std::endl;
     237                 :            :   return false;
     238                 :            : #endif
     239                 :            : }
     240                 :            : 
     241                 :        728 : bool CoveringsSolver::addToModel(TNode var, TNode value) const
     242                 :            : {
     243 [ -  + ][ -  + ]:        728 :   Assert(value.getType().isRealOrInt());
                 [ -  - ]
     244                 :            :   // we must take its substituted form here, since other solvers (e.g. the
     245                 :            :   // reductions inference of the sine solver) may have introduced substitutions
     246                 :            :   // internally during check.
     247                 :        728 :   Node svalue = d_model.getSubstitutedForm(value);
     248                 :            :   // ensure the value has integer type if var has integer type
     249         [ +  + ]:        728 :   if (var.getType().isInteger())
     250                 :            :   {
     251         [ -  + ]:        140 :     if (svalue.getKind() == Kind::TO_REAL)
     252                 :            :     {
     253                 :          0 :       svalue = svalue[0];
     254                 :            :     }
     255         [ +  + ]:        140 :     else if (svalue.getKind() == Kind::CONST_RATIONAL)
     256                 :            :     {
     257 [ -  + ][ -  + ]:         57 :       Assert(svalue.getConst<Rational>().isIntegral());
                 [ -  - ]
     258                 :         57 :       svalue = nodeManager()->mkConstInt(svalue.getConst<Rational>());
     259                 :            :     }
     260                 :            :   }
     261         [ +  - ]:        728 :   Trace("nl-cov") << "-> " << var << " = " << svalue << std::endl;
     262                 :       1456 :   return d_model.addSubstitution(var, svalue);
     263                 :        728 : }
     264                 :            : 
     265                 :            : }  // namespace nl
     266                 :            : }  // namespace arith
     267                 :            : }  // namespace theory
     268                 :            : }  // namespace cvc5::internal