src/theory/arith/equality_solver.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   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 equality solver
  14  */
  15
  16 #include "theory/arith/equality_solver.h"
  17
  18 #include "theory/arith/inference_manager.h"
  19
  20 using namespace cvc5::kind;
  21
  22 namespace cvc5 {
  23 namespace theory {
  24 namespace arith {
  25
  26 EqualitySolver::EqualitySolver(ArithState& astate, InferenceManager& aim)
  27     : d_astate(astate),
  28       d_aim(aim),
  29       d_notify(*this),
  30       d_ee(nullptr),
  31       d_propLits(astate.getSatContext())
  32 {
  33 }
  34
  35 bool EqualitySolver::needsEqualityEngine(EeSetupInfo& esi)
  36 {
  37   esi.d_notify = &d_notify;
  38   esi.d_name = "arith::ee";
  39   return true;
  40 }
  41
  42 void EqualitySolver::finishInit()
  43 {
  44   d_ee = d_astate.getEqualityEngine();
  45   // add the function kinds
  46   d_ee->addFunctionKind(kind::NONLINEAR_MULT);
  47   d_ee->addFunctionKind(kind::EXPONENTIAL);
  48   d_ee->addFunctionKind(kind::SINE);
  49   d_ee->addFunctionKind(kind::IAND);
  50   d_ee->addFunctionKind(kind::POW2);
  51 }
  52
  53 bool EqualitySolver::preNotifyFact(
  54     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
  55 {
  56   if (atom.getKind() != EQUAL)
  57   {
  58     // finished processing, since not beneficial to add non-equality facts
  59     return true;
  60   }
  61   Trace("arith-eq-solver") << "EqualitySolver::preNotifyFact: " << fact
  62                            << std::endl;
  63   // we will process
  64   return false;
  65 }
  66
  67 TrustNode EqualitySolver::explain(TNode lit)
  68 {
  69   Trace("arith-eq-solver-debug") << "explain " << lit << "?" << std::endl;
  70   // check if we propagated it?
  71   if (d_propLits.find(lit) == d_propLits.end())
  72   {
  73     Trace("arith-eq-solver-debug") << "...did not propagate" << std::endl;
  74     return TrustNode::null();
  75   }
  76   Trace("arith-eq-solver-debug")
  77       << "...explain via inference manager" << std::endl;
  78   // if we did, explain with the arithmetic inference manager
  79   return d_aim.explainLit(lit);
  80 }
  81 bool EqualitySolver::propagateLit(Node lit)
  82 {
  83   // if we've already propagated, ignore
  84   if (d_aim.hasPropagated(lit))
  85   {
  86     return true;
  87   }
  88   // notice this is only used when ee-mode=distributed
  89   // remember that this was a literal we propagated
  90   Trace("arith-eq-solver-debug") << "propagate lit " << lit << std::endl;
  91   d_propLits.insert(lit);
  92   return d_aim.propagateLit(lit);
  93 }
  94 void EqualitySolver::conflictEqConstantMerge(TNode a, TNode b)
  95 {
  96   d_aim.conflictEqConstantMerge(a, b);
  97 }
  98
  99 bool EqualitySolver::EqualitySolverNotify::eqNotifyTriggerPredicate(
 100     TNode predicate, bool value)
 101 {
 102   Trace("arith-eq-solver") << "...propagate (predicate) " << predicate << " -> "
 103                            << value << std::endl;
 104   if (value)
 105   {
 106     return d_es.propagateLit(predicate);
 107   }
 108   return d_es.propagateLit(predicate.notNode());
 109 }
 110
 111 bool EqualitySolver::EqualitySolverNotify::eqNotifyTriggerTermEquality(
 112     TheoryId tag, TNode t1, TNode t2, bool value)
 113 {
 114   Trace("arith-eq-solver") << "...propagate (term eq) " << t1.eqNode(t2)
 115                            << " -> " << value << std::endl;
 116   if (value)
 117   {
 118     return d_es.propagateLit(t1.eqNode(t2));
 119   }
 120   return d_es.propagateLit(t1.eqNode(t2).notNode());
 121 }
 122
 123 void EqualitySolver::EqualitySolverNotify::eqNotifyConstantTermMerge(TNode t1,
 124                                                                      TNode t2)
 125 {
 126   Trace("arith-eq-solver") << "...conflict merge " << t1 << " " << t2
 127                            << std::endl;
 128   d_es.conflictEqConstantMerge(t1, t2);
 129 }
 130
 131 }  // namespace arith
 132 }  // namespace theory
 133 }  // namespace cvc5