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_rewriter.h"
  23 #include "theory/arith/equality_solver.h"
  24 #include "theory/arith/infer_bounds.h"
  25 #include "theory/arith/nl/nonlinear_extension.h"
  26 #include "theory/arith/theory_arith_private.h"
  27 #include "theory/ext_theory.h"
  28 #include "theory/rewriter.h"
  29 #include "theory/theory_model.h"
  30
  31 using namespace std;
  32 using namespace cvc5::kind;
  33
  34 namespace cvc5 {
  35 namespace theory {
  36 namespace arith {
  37
  38 TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
  39     : Theory(THEORY_ARITH, env, out, valuation),
  40       d_ppRewriteTimer(smtStatisticsRegistry().registerTimer(
  41           "theory::arith::ppRewriteTimer")),
  42       d_astate(env, valuation),
  43       d_im(*this, d_astate, d_pnm),
  44       d_ppre(getSatContext(), d_pnm),
  45       d_bab(d_astate, d_im, d_ppre, d_pnm),
  46       d_eqSolver(nullptr),
  47       d_internal(new TheoryArithPrivate(*this, env, d_bab)),
  48       d_nonlinearExtension(nullptr),
  49       d_opElim(d_pnm, getLogicInfo()),
  50       d_arithPreproc(d_astate, d_im, d_pnm, d_opElim),
  51       d_rewriter(d_opElim)
  52 {
  53   // currently a cyclic dependency to TheoryArithPrivate
  54   d_astate.setParent(d_internal);
  55   // indicate we are using the theory state object and inference manager
  56   d_theoryState = &d_astate;
  57   d_inferManager = &d_im;
  58
  59   if (options::arithEqSolver())
  60   {
  61     d_eqSolver.reset(new EqualitySolver(d_astate, d_im));
  62   }
  63 }
  64
  65 TheoryArith::~TheoryArith(){
  66   delete d_internal;
  67 }
  68
  69 TheoryRewriter* TheoryArith::getTheoryRewriter() { return &d_rewriter; }
  70
  71 ProofRuleChecker* TheoryArith::getProofChecker()
  72 {
  73   return d_internal->getProofChecker();
  74 }
  75
  76 bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi)
  77 {
  78   // if the equality solver is enabled, then it is responsible for setting
  79   // up the equality engine
  80   if (d_eqSolver != nullptr)
  81   {
  82     return d_eqSolver->needsEqualityEngine(esi);
  83   }
  84   // otherwise, the linear arithmetic solver is responsible for setting up
  85   // the equality engine
  86   return d_internal->needsEqualityEngine(esi);
  87 }
  88 void TheoryArith::finishInit()
  89 {
  90   if (getLogicInfo().isTheoryEnabled(THEORY_ARITH)
  91       && getLogicInfo().areTranscendentalsUsed())
  92   {
  93     // witness is used to eliminate square root
  94     d_valuation.setUnevaluatedKind(kind::WITNESS);
  95     // we only need to add the operators that are not syntax sugar
  96     d_valuation.setUnevaluatedKind(kind::EXPONENTIAL);
  97     d_valuation.setUnevaluatedKind(kind::SINE);
  98     d_valuation.setUnevaluatedKind(kind::PI);
  99   }
 100   // only need to create nonlinear extension if non-linear logic
 101   const LogicInfo& logicInfo = getLogicInfo();
 102   if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
 103   {
 104     d_nonlinearExtension.reset(new nl::NonlinearExtension(*this, d_astate));
 105   }
 106   if (d_eqSolver != nullptr)
 107   {
 108     d_eqSolver->finishInit();
 109   }
 110   // finish initialize in the old linear solver
 111   d_internal->finishInit();
 112 }
 113
 114 void TheoryArith::preRegisterTerm(TNode n)
 115 {
 116   if (d_nonlinearExtension != nullptr)
 117   {
 118     d_nonlinearExtension->preRegisterTerm(n);
 119   }
 120   d_internal->preRegisterTerm(n);
 121 }
 122
 123 void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
 124
 125 TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
 126 {
 127   CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
 128   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 129
 130   if (atom.getKind() == kind::EQUAL)
 131   {
 132     return d_ppre.ppRewriteEq(atom);
 133   }
 134   Assert(Theory::theoryOf(atom) == THEORY_ARITH);
 135   // Eliminate operators. Notice we must do this here since other
 136   // theories may generate lemmas that involve non-standard operators. For
 137   // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
 138   // introduce non-standard arithmetic terms appearing in grammars.
 139   // call eliminate operators. In contrast to expandDefinitions, we eliminate
 140   // *all* extended arithmetic operators here, including total ones.
 141   return d_arithPreproc.eliminate(atom, lems, false);
 142 }
 143
 144 Theory::PPAssertStatus TheoryArith::ppAssert(
 145     TrustNode tin, TrustSubstitutionMap& outSubstitutions)
 146 {
 147   return d_internal->ppAssert(tin, outSubstitutions);
 148 }
 149
 150 void TheoryArith::ppStaticLearn(TNode n, NodeBuilder& learned)
 151 {
 152   d_internal->ppStaticLearn(n, learned);
 153 }
 154
 155 bool TheoryArith::preCheck(Effort level)
 156 {
 157   Trace("arith-check") << "TheoryArith::preCheck " << level << std::endl;
 158   return d_internal->preCheck(level);
 159 }
 160
 161 void TheoryArith::postCheck(Effort level)
 162 {
 163   Trace("arith-check") << "TheoryArith::postCheck " << level << std::endl;
 164   // check with the non-linear solver at last call
 165   if (level == Theory::EFFORT_LAST_CALL)
 166   {
 167     if (d_nonlinearExtension != nullptr)
 168     {
 169       d_nonlinearExtension->check(level);
 170     }
 171     return;
 172   }
 173   // otherwise, check with the linear solver
 174   if (d_internal->postCheck(level))
 175   {
 176     // linear solver emitted a conflict or lemma, return
 177     return;
 178   }
 179
 180   if (Theory::fullEffort(level))
 181   {
 182     if (d_nonlinearExtension != nullptr)
 183     {
 184       d_nonlinearExtension->check(level);
 185     }
 186     else if (d_internal->foundNonlinear())
 187     {
 188       // set incomplete
 189       d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED);
 190     }
 191   }
 192 }
 193
 194 bool TheoryArith::preNotifyFact(
 195     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 196 {
 197   Trace("arith-check") << "TheoryArith::preNotifyFact: " << fact
 198                        << ", isPrereg=" << isPrereg
 199                        << ", isInternal=" << isInternal << std::endl;
 200   // We do not assert to the equality engine of arithmetic in the standard way,
 201   // hence we return "true" to indicate we are finished with this fact.
 202   bool ret = true;
 203   if (d_eqSolver != nullptr)
 204   {
 205     // the equality solver may indicate ret = false, after which the assertion
 206     // will be asserted to the equality engine in the default way.
 207     ret = d_eqSolver->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
 208   }
 209   // we also always also notify the internal solver
 210   d_internal->preNotifyFact(atom, pol, fact);
 211   return ret;
 212 }
 213
 214 bool TheoryArith::needsCheckLastEffort() {
 215   if (d_nonlinearExtension != nullptr)
 216   {
 217     return d_nonlinearExtension->needsCheckLastEffort();
 218   }
 219   return false;
 220 }
 221
 222 TrustNode TheoryArith::explain(TNode n)
 223 {
 224   if (d_eqSolver != nullptr)
 225   {
 226     // if the equality solver has an explanation for it, use it
 227     TrustNode texp = d_eqSolver->explain(n);
 228     if (!texp.isNull())
 229     {
 230       return texp;
 231     }
 232   }
 233   return d_internal->explain(n);
 234 }
 235
 236 void TheoryArith::propagate(Effort e) {
 237   d_internal->propagate(e);
 238 }
 239
 240 bool TheoryArith::collectModelInfo(TheoryModel* m,
 241                                    const std::set<Node>& termSet)
 242 {
 243   // this overrides behavior to not assert equality engine
 244   return collectModelValues(m, termSet);
 245 }
 246
 247 bool TheoryArith::collectModelValues(TheoryModel* m,
 248                                      const std::set<Node>& termSet)
 249 {
 250   // get the model from the linear solver
 251   std::map<Node, Node> arithModel;
 252   d_internal->collectModelValues(termSet, arithModel);
 253   // Double check that the model from the linear solver respects integer types,
 254   // if it does not, add a branch and bound lemma. This typically should never
 255   // be necessary, but is needed in rare cases.
 256   bool addedLemma = false;
 257   bool badAssignment = false;
 258   for (const std::pair<const Node, Node>& p : arithModel)
 259   {
 260     if (p.first.getType().isInteger() && !p.second.getType().isInteger())
 261     {
 262       Assert(false) << "TheoryArithPrivate generated a bad model value for "
 263                        "integer variable "
 264                     << p.first << " : " << p.second;
 265       // must branch and bound
 266       TrustNode lem =
 267           d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>());
 268       if (d_im.trustedLemma(lem, InferenceId::ARITH_BB_LEMMA))
 269       {
 270         addedLemma = true;
 271       }
 272       badAssignment = true;
 273     }
 274   }
 275   if (addedLemma)
 276   {
 277     // we had to add a branch and bound lemma since the linear solver assigned
 278     // a non-integer value to an integer variable.
 279     return false;
 280   }
 281   // this would imply that linear arithmetic's model failed to satisfy a branch
 282   // and bound lemma
 283   AlwaysAssert(!badAssignment)
 284       << "Bad assignment from TheoryArithPrivate::collectModelValues, and no "
 285          "branching lemma was sent";
 286
 287   // if non-linear is enabled, intercept the model, which may repair its values
 288   if (d_nonlinearExtension != nullptr)
 289   {
 290     // Non-linear may repair values to satisfy non-linear constraints (see
 291     // documentation for NonlinearExtension::interceptModel).
 292     d_nonlinearExtension->interceptModel(arithModel, termSet);
 293   }
 294   // We are now ready to assert the model.
 295   for (const std::pair<const Node, Node>& p : arithModel)
 296   {
 297     // maps to constant of comparable type
 298     Assert(p.first.getType().isComparableTo(p.second.getType()));
 299     if (m->assertEquality(p.first, p.second, true))
 300     {
 301       continue;
 302     }
 303     // If we failed to assert an equality, it is likely due to theory
 304     // combination, namely the repaired model for non-linear changed
 305     // an equality status that was agreed upon by both (linear) arithmetic
 306     // and another theory. In this case, we must add a lemma, or otherwise
 307     // we would terminate with an invalid model. Thus, we add a splitting
 308     // lemma of the form ( x = v V x != v ) where v is the model value
 309     // assigned by the non-linear solver to x.
 310     if (d_nonlinearExtension != nullptr)
 311     {
 312       Node eq = p.first.eqNode(p.second);
 313       Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate());
 314       bool added = d_im.lemma(lem, InferenceId::ARITH_SPLIT_FOR_NL_MODEL);
 315       AlwaysAssert(added) << "The lemma was already in cache. Probably there is something wrong with theory combination...";
 316     }
 317     return false;
 318   }
 319   return true;
 320 }
 321
 322 void TheoryArith::notifyRestart(){
 323   d_internal->notifyRestart();
 324 }
 325
 326 void TheoryArith::presolve(){
 327   d_internal->presolve();
 328   if (d_nonlinearExtension != nullptr)
 329   {
 330     d_nonlinearExtension->presolve();
 331   }
 332 }
 333
 334 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
 335   return d_internal->getEqualityStatus(a,b);
 336 }
 337
 338 Node TheoryArith::getModelValue(TNode var) {
 339   return d_internal->getModelValue( var );
 340 }
 341
 342 std::pair<bool, Node> TheoryArith::entailmentCheck(TNode lit)
 343 {
 344   ArithEntailmentCheckParameters def;
 345   def.addLookupRowSumAlgorithms();
 346   ArithEntailmentCheckSideEffects ase;
 347   std::pair<bool, Node> res = d_internal->entailmentCheck(lit, def, ase);
 348   return res;
 349 }
 350 eq::ProofEqEngine* TheoryArith::getProofEqEngine()
 351 {
 352   return d_im.getProofEqEngine();
 353 }
 354
 355 }  // namespace arith
 356 }  // namespace theory
 357 }  // namespace cvc5