src/theory/arith/nl/ext_theory_callback.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Tim King, Tianyi Liang
   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  * The extended theory callback for non-linear arithmetic
  14  */
  15
  16 #include "theory/arith/nl/ext_theory_callback.h"
  17
  18 #include "theory/arith/arith_utilities.h"
  19 #include "theory/uf/equality_engine.h"
  20
  21 using namespace cvc5::kind;
  22
  23 namespace cvc5 {
  24 namespace theory {
  25 namespace arith {
  26 namespace nl {
  27
  28 NlExtTheoryCallback::NlExtTheoryCallback(eq::EqualityEngine* ee) : d_ee(ee)
  29 {
  30   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
  31 }
  32
  33 bool NlExtTheoryCallback::getCurrentSubstitution(
  34     int effort,
  35     const std::vector<Node>& vars,
  36     std::vector<Node>& subs,
  37     std::map<Node, std::vector<Node>>& exp)
  38 {
  39   // get the constant equivalence classes
  40   std::map<Node, std::vector<int>> rep_to_subs_index;
  41
  42   bool retVal = false;
  43   for (unsigned i = 0; i < vars.size(); i++)
  44   {
  45     Node n = vars[i];
  46     if (d_ee->hasTerm(n))
  47     {
  48       Node nr = d_ee->getRepresentative(n);
  49       if (nr.isConst())
  50       {
  51         subs.push_back(nr);
  52         Trace("nl-subs") << "Basic substitution : " << n << " -> " << nr
  53                          << std::endl;
  54         exp[n].push_back(n.eqNode(nr));
  55         retVal = true;
  56       }
  57       else
  58       {
  59         rep_to_subs_index[nr].push_back(i);
  60         subs.push_back(n);
  61       }
  62     }
  63     else
  64     {
  65       subs.push_back(n);
  66     }
  67   }
  68
  69   // return true if the substitution is non-trivial
  70   return retVal;
  71 }
  72
  73 bool NlExtTheoryCallback::isExtfReduced(
  74     int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id)
  75 {
  76   if (n != d_zero)
  77   {
  78     Kind k = n.getKind();
  79     if (k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND)
  80     {
  81       id = ExtReducedId::ARITH_SR_LINEAR;
  82       return true;
  83     }
  84     return false;
  85   }
  86   Assert(n == d_zero);
  87   id = ExtReducedId::ARITH_SR_ZERO;
  88   if (on.getKind() == NONLINEAR_MULT)
  89   {
  90     Trace("nl-ext-zero-exp")
  91         << "Infer zero : " << on << " == " << n << std::endl;
  92     // minimize explanation if a substitution+rewrite results in zero
  93     const std::set<Node> vars(on.begin(), on.end());
  94
  95     for (unsigned i = 0, size = exp.size(); i < size; i++)
  96     {
  97       Trace("nl-ext-zero-exp")
  98           << "  exp[" << i << "] = " << exp[i] << std::endl;
  99       std::vector<Node> eqs;
 100       if (exp[i].getKind() == EQUAL)
 101       {
 102         eqs.push_back(exp[i]);
 103       }
 104       else if (exp[i].getKind() == AND)
 105       {
 106         for (const Node& ec : exp[i])
 107         {
 108           if (ec.getKind() == EQUAL)
 109           {
 110             eqs.push_back(ec);
 111           }
 112         }
 113       }
 114
 115       for (unsigned j = 0; j < eqs.size(); j++)
 116       {
 117         for (unsigned r = 0; r < 2; r++)
 118         {
 119           if (eqs[j][r] == d_zero && vars.find(eqs[j][1 - r]) != vars.end())
 120           {
 121             Trace("nl-ext-zero-exp")
 122                 << "...single exp : " << eqs[j] << std::endl;
 123             exp.clear();
 124             exp.push_back(eqs[j]);
 125             return true;
 126           }
 127         }
 128       }
 129     }
 130   }
 131   return true;
 132 }
 133
 134 }  // namespace nl
 135 }  // namespace arith
 136 }  // namespace theory
 137 }  // namespace cvc5