src/theory/arith/theory_arith.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Tim King, Alex Ozdemir
   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  * Arithmetic theory.
  14  */
  15
  16 #include "theory/arith/theory_arith.h"
  17
  18 #include "options/smt_options.h"
  19 #include "proof/proof_checker.h"
  20 #include "proof/proof_rule.h"
  21 #include "smt/smt_statistics_registry.h"
  22 #include "theory/arith/arith_evaluator.h"
  23 #include "theory/arith/arith_rewriter.h"
  24 #include "theory/arith/equality_solver.h"
  25 #include "theory/arith/infer_bounds.h"
  26 #include "theory/arith/nl/nonlinear_extension.h"
  27 #include "theory/arith/theory_arith_private.h"
  28 #include "theory/ext_theory.h"
  29 #include "theory/rewriter.h"
  30 #include "theory/theory_model.h"
  31
  32 using namespace std;
  33 using namespace cvc5::kind;
  34
  35 namespace cvc5 {
  36 namespace theory {
  37 namespace arith {
  38
  39 TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
  40     : Theory(THEORY_ARITH, env, out, valuation),
  41       d_ppRewriteTimer(
  42           statisticsRegistry().registerTimer("theory::arith::ppRewriteTimer")),
  43       d_astate(env, valuation),
  44       d_im(env, *this, d_astate),
  45       d_ppre(d_env),
  46       d_bab(env, d_astate, d_im, d_ppre, d_pnm),
  47       d_eqSolver(nullptr),
  48       d_internal(new TheoryArithPrivate(*this, env, d_bab)),
  49       d_nonlinearExtension(nullptr),
  50       d_opElim(d_env),
  51       d_arithPreproc(env, d_astate, d_im, d_pnm, d_opElim),
  52       d_rewriter(d_opElim),
  53       d_arithModelCacheSet(false)
  54 {
  55   // currently a cyclic dependency to TheoryArithPrivate
  56   d_astate.setParent(d_internal);
  57   // indicate we are using the theory state object and inference manager
  58   d_theoryState = &d_astate;
  59   d_inferManager = &d_im;
  60
  61   if (options().arith.arithEqSolver)
  62   {
  63     d_eqSolver.reset(new EqualitySolver(env, d_astate, d_im));
  64   }
  65 }
  66
  67 TheoryArith::~TheoryArith(){
  68   delete d_internal;
  69 }
  70
  71 TheoryRewriter* TheoryArith::getTheoryRewriter() { return &d_rewriter; }
  72
  73 ProofRuleChecker* TheoryArith::getProofChecker()
  74 {
  75   return d_internal->getProofChecker();
  76 }
  77
  78 bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi)
  79 {
  80   // if the equality solver is enabled, then it is responsible for setting
  81   // up the equality engine
  82   if (d_eqSolver != nullptr)
  83   {
  84     return d_eqSolver->needsEqualityEngine(esi);
  85   }
  86   // otherwise, the linear arithmetic solver is responsible for setting up
  87   // the equality engine
  88   return d_internal->needsEqualityEngine(esi);
  89 }
  90 void TheoryArith::finishInit()
  91 {
  92   const LogicInfo& logic = logicInfo();
  93   if (logic.isTheoryEnabled(THEORY_ARITH) && logic.areTranscendentalsUsed())
  94   {
  95     // witness is used to eliminate square root
  96     d_valuation.setUnevaluatedKind(kind::WITNESS);
  97     // we only need to add the operators that are not syntax sugar
  98     d_valuation.setUnevaluatedKind(kind::EXPONENTIAL);
  99     d_valuation.setUnevaluatedKind(kind::SINE);
 100     d_valuation.setUnevaluatedKind(kind::PI);
 101   }
 102   // only need to create nonlinear extension if non-linear logic
 103   if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())
 104   {
 105     d_nonlinearExtension.reset(
 106         new nl::NonlinearExtension(d_env, *this, d_astate));
 107   }
 108   if (d_eqSolver != nullptr)
 109   {
 110     d_eqSolver->finishInit();
 111   }
 112   // finish initialize in the old linear solver
 113   d_internal->finishInit();
 114 }
 115
 116 void TheoryArith::preRegisterTerm(TNode n)
 117 {
 118   if (d_nonlinearExtension != nullptr)
 119   {
 120     d_nonlinearExtension->preRegisterTerm(n);
 121   }
 122   d_internal->preRegisterTerm(n);
 123 }
 124
 125 void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
 126
 127 TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
 128 {
 129   CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
 130   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 131
 132   if (atom.getKind() == kind::EQUAL)
 133   {
 134     return d_ppre.ppRewriteEq(atom);
 135   }
 136   Assert(d_env.theoryOf(atom) == THEORY_ARITH);
 137   // Eliminate operators. Notice we must do this here since other
 138   // theories may generate lemmas that involve non-standard operators. For
 139   // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
 140   // introduce non-standard arithmetic terms appearing in grammars.
 141   // call eliminate operators. In contrast to expandDefinitions, we eliminate
 142   // *all* extended arithmetic operators here, including total ones.
 143   return d_arithPreproc.eliminate(atom, lems, false);
 144 }
 145
 146 Theory::PPAssertStatus TheoryArith::ppAssert(
 147     TrustNode tin, TrustSubstitutionMap& outSubstitutions)
 148 {
 149   return d_internal->ppAssert(tin, outSubstitutions);
 150 }
 151
 152 void TheoryArith::ppStaticLearn(TNode n, NodeBuilder& learned)
 153 {
 154   d_internal->ppStaticLearn(n, learned);
 155 }
 156
 157 bool TheoryArith::preCheck(Effort level)
 158 {
 159   Trace("arith-check") << "TheoryArith::preCheck " << level << std::endl;
 160   return d_internal->preCheck(level);
 161 }
 162
 163 void TheoryArith::postCheck(Effort level)
 164 {
 165   d_im.reset();
 166   Trace("arith-check") << "TheoryArith::postCheck " << level << std::endl;
 167   if (Theory::fullEffort(level))
 168   {
 169     // Make sure we don't have old lemmas floating around. This can happen if we
 170     // didn't actually reach a last call effort check, but backtracked for some
 171     // other reason. In such a case, these lemmas are likely to be irrelevant
 172     // and possibly even harmful. If we produce proofs, their proofs have most
 173     // likely been deallocated already as well.
 174     d_im.clearPending();
 175     d_im.clearWaitingLemmas();
 176   }
 177   // check with the non-linear solver at last call
 178   if (level == Theory::EFFORT_LAST_CALL)
 179   {
 180     // If we computed lemmas in the last FULL_EFFORT check, send them now.
 181     if (d_im.hasPendingLemma())
 182     {
 183       d_im.doPendingFacts();
 184       d_im.doPendingLemmas();
 185       d_im.doPendingPhaseRequirements();
 186     }
 187     return;
 188   }
 189   // otherwise, check with the linear solver
 190   if (d_internal->postCheck(level))
 191   {
 192     // linear solver emitted a conflict or lemma, return
 193     return;
 194   }
 195   if (d_im.hasSent())
 196   {
 197     return;
 198   }
 199
 200   if (Theory::fullEffort(level))
 201   {
 202     d_arithModelCache.clear();
 203     d_arithModelCacheSet = false;
 204     std::set<Node> termSet;
 205     if (d_nonlinearExtension != nullptr)
 206     {
 207       updateModelCache(termSet);
 208       d_nonlinearExtension->checkFullEffort(d_arithModelCache, termSet);
 209     }
 210     else if (d_internal->foundNonlinear())
 211     {
 212       // set incomplete
 213       d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED);
 214     }
 215     // If we won't be doing a last call effort check (which implies that
 216     // models will be computed), we must sanity check the integer model
 217     // from the linear solver now. We also must update the model cache
 218     // if we did not do so above.
 219     if (d_nonlinearExtension == nullptr)
 220     {
 221       updateModelCache(termSet);
 222     }
 223     sanityCheckIntegerModel();
 224   }
 225 }
 226
 227 bool TheoryArith::preNotifyFact(
 228     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 229 {
 230   Trace("arith-check") << "TheoryArith::preNotifyFact: " << fact
 231                        << ", isPrereg=" << isPrereg
 232                        << ", isInternal=" << isInternal << std::endl;
 233   // We do not assert to the equality engine of arithmetic in the standard way,
 234   // hence we return "true" to indicate we are finished with this fact.
 235   bool ret = true;
 236   if (d_eqSolver != nullptr)
 237   {
 238     // the equality solver may indicate ret = false, after which the assertion
 239     // will be asserted to the equality engine in the default way.
 240     ret = d_eqSolver->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
 241   }
 242   // we also always also notify the internal solver
 243   d_internal->preNotifyFact(atom, pol, fact);
 244   return ret;
 245 }
 246
 247 bool TheoryArith::needsCheckLastEffort() {
 248   if (d_nonlinearExtension != nullptr)
 249   {
 250     return d_nonlinearExtension->hasNlTerms();
 251   }
 252   return false;
 253 }
 254
 255 TrustNode TheoryArith::explain(TNode n)
 256 {
 257   if (d_eqSolver != nullptr)
 258   {
 259     // if the equality solver has an explanation for it, use it
 260     TrustNode texp = d_eqSolver->explain(n);
 261     if (!texp.isNull())
 262     {
 263       return texp;
 264     }
 265   }
 266   return d_internal->explain(n);
 267 }
 268
 269 void TheoryArith::propagate(Effort e) {
 270   d_internal->propagate(e);
 271 }
 272
 273 bool TheoryArith::collectModelInfo(TheoryModel* m,
 274                                    const std::set<Node>& termSet)
 275 {
 276   // this overrides behavior to not assert equality engine
 277   return collectModelValues(m, termSet);
 278 }
 279
 280 bool TheoryArith::collectModelValues(TheoryModel* m,
 281                                      const std::set<Node>& termSet)
 282 {
 283   if (Trace.isOn("arith::model"))
 284   {
 285     Trace("arith::model") << "arithmetic model after pruning" << std::endl;
 286     for (const auto& p : d_arithModelCache)
 287     {
 288       Trace("arith::model") << "\t" << p.first << " -> " << p.second << std::endl;
 289     }
 290   }
 291
 292   updateModelCache(termSet);
 293
 294   // We are now ready to assert the model.
 295   for (const std::pair<const Node, Node>& p : d_arithModelCache)
 296   {
 297     if (termSet.find(p.first) == termSet.end())
 298     {
 299       continue;
 300     }
 301     // maps to constant of comparable type
 302     Assert(p.first.getType().isComparableTo(p.second.getType()));
 303     if (m->assertEquality(p.first, p.second, true))
 304     {
 305       continue;
 306     }
 307     Assert(false) << "A model equality could not be asserted: " << p.first
 308                         << " == " << p.second << std::endl;
 309     // If we failed to assert an equality, it is likely due to theory
 310     // combination, namely the repaired model for non-linear changed
 311     // an equality status that was agreed upon by both (linear) arithmetic
 312     // and another theory. In this case, we must add a lemma, or otherwise
 313     // we would terminate with an invalid model. Thus, we add a splitting
 314     // lemma of the form ( x = v V x != v ) where v is the model value
 315     // assigned by the non-linear solver to x.
 316     if (d_nonlinearExtension != nullptr)
 317     {
 318       Node eq = p.first.eqNode(p.second);
 319       Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate());
 320       bool added = d_im.lemma(lem, InferenceId::ARITH_SPLIT_FOR_NL_MODEL);
 321       AlwaysAssert(added) << "The lemma was already in cache. Probably there is something wrong with theory combination...";
 322     }
 323     return false;
 324   }
 325   return true;
 326 }
 327
 328 void TheoryArith::notifyRestart(){
 329   d_internal->notifyRestart();
 330 }
 331
 332 void TheoryArith::presolve(){
 333   d_internal->presolve();
 334 }
 335
 336 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
 337   Debug("arith") << "TheoryArith::getEqualityStatus(" << a << ", " << b << ")" << std::endl;
 338   if (a == b)
 339   {
 340     return EQUALITY_TRUE_IN_MODEL;
 341   }
 342   if (d_arithModelCache.empty())
 343   {
 344     return d_internal->getEqualityStatus(a,b);
 345   }
 346   Node diff = d_env.getNodeManager()->mkNode(Kind::SUB, a, b);
 347   std::optional<bool> isZero = isExpressionZero(d_env, diff, d_arithModelCache);
 348   if (isZero)
 349   {
 350     return *isZero ? EQUALITY_TRUE_IN_MODEL : EQUALITY_FALSE_IN_MODEL;
 351   }
 352   return EQUALITY_UNKNOWN;
 353 }
 354
 355 Node TheoryArith::getModelValue(TNode var) {
 356   std::map<Node, Node>::iterator it = d_arithModelCache.find(var);
 357   if (it != d_arithModelCache.end())
 358   {
 359     return it->second;
 360   }
 361   return d_internal->getModelValue( var );
 362 }
 363
 364 std::pair<bool, Node> TheoryArith::entailmentCheck(TNode lit)
 365 {
 366   ArithEntailmentCheckParameters def;
 367   def.addLookupRowSumAlgorithms();
 368   ArithEntailmentCheckSideEffects ase;
 369   std::pair<bool, Node> res = d_internal->entailmentCheck(lit, def, ase);
 370   return res;
 371 }
 372 eq::ProofEqEngine* TheoryArith::getProofEqEngine()
 373 {
 374   return d_im.getProofEqEngine();
 375 }
 376
 377 void TheoryArith::updateModelCache(std::set<Node>& termSet)
 378 {
 379   if (!d_arithModelCacheSet)
 380   {
 381     d_arithModelCacheSet = true;
 382     collectAssertedTerms(termSet);
 383     d_internal->collectModelValues(termSet, d_arithModelCache);
 384   }
 385 }
 386 void TheoryArith::updateModelCache(const std::set<Node>& termSet)
 387 {
 388   if (!d_arithModelCacheSet)
 389   {
 390     d_arithModelCacheSet = true;
 391     d_internal->collectModelValues(termSet, d_arithModelCache);
 392   }
 393 }
 394 bool TheoryArith::sanityCheckIntegerModel()
 395 {
 396
 397     // Double check that the model from the linear solver respects integer types,
 398     // if it does not, add a branch and bound lemma. This typically should never
 399     // be necessary, but is needed in rare cases.
 400     bool addedLemma = false;
 401     bool badAssignment = false;
 402     Trace("arith-check") << "model:" << std::endl;
 403     for (const auto& p : d_arithModelCache)
 404     {
 405       Trace("arith-check") << p.first << " -> " << p.second << std::endl;
 406       if (p.first.getType().isInteger() && !p.second.getType().isInteger())
 407       {
 408         warning() << "TheoryArithPrivate generated a bad model value for "
 409                      "integer variable "
 410                   << p.first << " : " << p.second << std::endl;
 411         // must branch and bound
 412         TrustNode lem =
 413             d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>());
 414         if (d_im.trustedLemma(lem, InferenceId::ARITH_BB_LEMMA))
 415         {
 416           addedLemma = true;
 417         }
 418         badAssignment = true;
 419       }
 420     }
 421     if (addedLemma)
 422     {
 423       // we had to add a branch and bound lemma since the linear solver assigned
 424       // a non-integer value to an integer variable.
 425       return true;
 426     }
 427     // this would imply that linear arithmetic's model failed to satisfy a branch
 428     // and bound lemma
 429     AlwaysAssert(!badAssignment)
 430         << "Bad assignment from TheoryArithPrivate::collectModelValues, and no "
 431           "branching lemma was sent";
 432     return false;
 433 }
 434
 435 }  // namespace arith
 436 }  // namespace theory
 437 }  // namespace cvc5