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