Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory.cpp	Lines:	265	310	85.5 %
Date:	2021-09-21	Branches:	537	1083	49.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Tim King, Dejan Jovanovic
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Base for theory interface.
 */

#include "theory/theory.h"

#include <iostream>
#include <sstream>
#include <string>
#include <vector>

#include "base/check.h"
#include "expr/node_algorithm.h"
#include "options/arith_options.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/ee_setup_info.h"
#include "theory/ext_theory.h"
#include "theory/output_channel.h"
#include "theory/quantifiers_engine.h"
#include "theory/substitutions.h"
#include "theory/theory_inference_manager.h"
#include "theory/theory_model.h"
#include "theory/theory_rewriter.h"
#include "theory/theory_state.h"
#include "theory/trust_substitutions.h"

using namespace std;

namespace cvc5 {
namespace theory {

/** Default value for the uninterpreted sorts is the UF theory */
TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;

std::ostream& operator<<(std::ostream& os, Theory::Effort level){
  switch(level){
  case Theory::EFFORT_STANDARD:
    os << "EFFORT_STANDARD"; break;
  case Theory::EFFORT_FULL:
    os << "EFFORT_FULL"; break;
  case Theory::EFFORT_LAST_CALL:
    os << "EFFORT_LAST_CALL"; break;
  default:
      Unreachable();
  }
  return os;
}/* ostream& operator<<(ostream&, Theory::Effort) */

Theory::Theory(TheoryId id,
               Env& env,
               OutputChannel& out,
               Valuation valuation,
               std::string name)
    : EnvObj(env),
      d_id(id),
      d_facts(d_env.getContext()),
      d_factsHead(d_env.getContext(), 0),
      d_sharedTermsIndex(d_env.getContext(), 0),
      d_careGraph(nullptr),
      d_instanceName(name),
      d_checkTime(statisticsRegistry().registerTimer(getStatsPrefix(id) + name
                                                     + "checkTime")),
      d_computeCareGraphTime(statisticsRegistry().registerTimer(
          getStatsPrefix(id) + name + "computeCareGraphTime")),
      d_sharedTerms(d_env.getContext()),
      d_out(&out),
      d_valuation(valuation),
      d_equalityEngine(nullptr),
      d_allocEqualityEngine(nullptr),
      d_theoryState(nullptr),
      d_inferManager(nullptr),
      d_quantEngine(nullptr),
      d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
                                           : nullptr)
{
}

Theory::~Theory() {
}

bool Theory::needsEqualityEngine(EeSetupInfo& esi)
{
  // by default, this theory does not use an (official) equality engine
  return false;
}

void Theory::setEqualityEngine(eq::EqualityEngine* ee)
{
  // set the equality engine pointer
  d_equalityEngine = ee;
  if (d_theoryState != nullptr)
  {
    d_theoryState->setEqualityEngine(ee);
  }
  if (d_inferManager != nullptr)
  {
    d_inferManager->setEqualityEngine(ee);
  }
}

void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
{
  // quantifiers engine may be null if not in quantified logic
  d_quantEngine = qe;
}

void Theory::setDecisionManager(DecisionManager* dm)
{
  Assert(dm != nullptr);
  if (d_inferManager != nullptr)
  {
    d_inferManager->setDecisionManager(dm);
  }
}

void Theory::finishInitStandalone()
{
  EeSetupInfo esi;
  if (needsEqualityEngine(esi))
  {
    // always associated with the same SAT context as the theory
    d_allocEqualityEngine.reset(new eq::EqualityEngine(
        *esi.d_notify, context(), esi.d_name, esi.d_constantsAreTriggers));
    // use it as the official equality engine
    setEqualityEngine(d_allocEqualityEngine.get());
  }
  finishInit();
}

TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
{
  TheoryId tid = THEORY_BUILTIN;
  switch(mode) {
    case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
      // Constants, variables, 0-ary constructors
      if (node.isVar())
      {
        if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
        {
          tid = THEORY_UF;
        }
        else
        {
          tid = Theory::theoryOf(node.getType());
        }
      }
      else if (node.getKind() == kind::EQUAL)
      {
        // Equality is owned by the theory that owns the domain
        tid = Theory::theoryOf(node[0].getType());
      }
      else
      {
        // Regular nodes are owned by the kind. Notice that constants are a
        // special case here, where the theory of the kind of a constant
        // always coincides with the type of that constant.
        tid = kindToTheoryId(node.getKind());
      }
      break;
    case options::TheoryOfMode::THEORY_OF_TERM_BASED:
      // Variables
      if (node.isVar())
      {
        if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
        {
          // We treat the variables as uninterpreted
          tid = s_uninterpretedSortOwner;
        }
        else
        {
          if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
          {
            // Boolean vars go to UF
            tid = THEORY_UF;
          }
          else
          {
            // Except for the Boolean ones
            tid = THEORY_BOOL;
          }
        }
      }
      else if (node.getKind() == kind::EQUAL)
      {  // Equality
        // If one of them is an ITE, it's irelevant, since they will get
        // replaced out anyhow
        if (node[0].getKind() == kind::ITE)
        {
          tid = Theory::theoryOf(node[0].getType());
        }
        else if (node[1].getKind() == kind::ITE)
        {
          tid = Theory::theoryOf(node[1].getType());
        }
        else
        {
          TNode l = node[0];
          TNode r = node[1];
          TypeNode ltype = l.getType();
          TypeNode rtype = r.getType();
          // If the types are different, we must assign based on type due
          // to handling subtypes (limited to arithmetic). Also, if we are
          // a Boolean equality, we must assign THEORY_BOOL.
          if (ltype != rtype || ltype.isBoolean())
          {
            tid = Theory::theoryOf(ltype);
          }
          else
          {
            // If both sides belong to the same theory the choice is easy
            TheoryId T1 = Theory::theoryOf(l);
            TheoryId T2 = Theory::theoryOf(r);
            if (T1 == T2)
            {
              tid = T1;
            }
            else
            {
              TheoryId T3 = Theory::theoryOf(ltype);
              // This is a case of
              // * x*y = f(z) -> UF
              // * x = c      -> UF
              // * f(x) = read(a, y) -> either UF or ARRAY
              // at least one of the theories has to be parametric, i.e. theory
              // of the type is different from the theory of the term
              if (T1 == T3)
              {
                tid = T2;
              }
              else if (T2 == T3)
              {
                tid = T1;
              }
              else
              {
                // If both are parametric, we take the smaller one (arbitrary)
                tid = T1 < T2 ? T1 : T2;
              }
            }
          }
        }
      }
      else
      {
        // Regular nodes are owned by the kind, which includes constants as a
        // special case.
        tid = kindToTheoryId(node.getKind());
      }
    break;
  default:
    Unreachable();
  }
  Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
  return tid;
}

void Theory::notifySharedTerm(TNode n)
{
  // do nothing
}

void Theory::notifyInConflict()
{
  if (d_inferManager != nullptr)
  {
    d_inferManager->notifyInConflict();
  }
}

void Theory::computeCareGraph() {
  Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
  for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
    TNode a = d_sharedTerms[i];
    TypeNode aType = a.getType();
    for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
      TNode b = d_sharedTerms[j];
      if (b.getType() != aType) {
        // We don't care about the terms of different types
        continue;
      }
      switch (d_valuation.getEqualityStatus(a, b)) {
      case EQUALITY_TRUE_AND_PROPAGATED:
      case EQUALITY_FALSE_AND_PROPAGATED:
        // If we know about it, we should have propagated it, so we can skip
        break;
      default:
        // Let's split on it
        addCarePair(a, b);
        break;
      }
    }
  }
}

void Theory::printFacts(std::ostream& os) const {
  unsigned i, n = d_facts.size();
  for(i = 0; i < n; i++){
    const Assertion& a_i = d_facts[i];
    Node assertion  = a_i;
    os << d_id << '[' << i << ']' << " " << assertion << endl;
  }
}

void Theory::debugPrintFacts() const{
  DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
  printFacts(DebugChannel.getStream());
}

bool Theory::isLegalElimination(TNode x, TNode val)
{
  Assert(x.isVar());
  if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE
      || val.getKind() == kind::BOOLEAN_TERM_VARIABLE)
  {
    return false;
  }
  if (expr::hasSubterm(val, x))
  {
    return false;
  }
  if (!val.getType().isSubtypeOf(x.getType()))
  {
    return false;
  }
  if (!options::produceModels() && !logicInfo().isQuantified())
  {
    // Don't care about the model and logic is not quantified, we can eliminate.
    return true;
  }
  // If models are enabled, then it depends on whether the term contains any
  // unevaluable operators like FORALL, SINE, etc. Having such operators makes
  // model construction contain non-constant values for variables, which is
  // not ideal from a user perspective.
  // We also insist on this check since the term to eliminate should never
  // contain quantifiers, or else variable shadowing issues may arise.
  // there should be a model object
  TheoryModel* tm = d_valuation.getModel();
  Assert(tm != nullptr);
  return tm->isLegalElimination(x, val);
}

std::unordered_set<TNode> Theory::currentlySharedTerms() const
{
  std::unordered_set<TNode> currentlyShared;
  for (shared_terms_iterator i = shared_terms_begin(),
           i_end = shared_terms_end(); i != i_end; ++i) {
    currentlyShared.insert (*i);
  }
  return currentlyShared;
}

bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet)
{
  // if we are using an equality engine, assert it to the model
  if (d_equalityEngine != nullptr && !termSet.empty())
  {
    Trace("model-builder") << "Assert Equality engine for " << d_id
                           << std::endl;
    if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
    {
      return false;
    }
  }
  Trace("model-builder") << "Collect Model values for " << d_id << std::endl;
  // now, collect theory-specific value assigments
  return collectModelValues(m, termSet);
}

void Theory::computeRelevantTerms(std::set<Node>& termSet)
{
  // by default, there are no additional relevant terms
}

void Theory::collectAssertedTerms(std::set<Node>& termSet,
                                  bool includeShared) const
{
  // Collect all terms appearing in assertions
  context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
                                             assert_it_end = facts_end();
  for (; assert_it != assert_it_end; ++assert_it)
  {
    collectTerms(*assert_it, termSet);
  }

  if (includeShared)
  {
    // Add terms that are shared terms
    context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(),
                                           shared_it_end = shared_terms_end();
    for (; shared_it != shared_it_end; ++shared_it)
    {
      collectTerms(*shared_it, termSet);
    }
  }
}

void Theory::collectTerms(TNode n, std::set<Node>& termSet) const
{
  const std::set<Kind>& irrKinds =
      d_theoryState->getModel()->getIrrelevantKinds();
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    if (termSet.find(cur) != termSet.end())
    {
      // already visited
      continue;
    }
    Kind k = cur.getKind();
    // only add to term set if a relevant kind
    if (irrKinds.find(k) == irrKinds.end())
    {
      termSet.insert(cur);
    }
    // traverse owned terms, don't go under quantifiers
    if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == d_id)
        && !cur.isClosure())
    {
      visit.insert(visit.end(), cur.begin(), cur.end());
    }
  } while (!visit.empty());
}

bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
{
  return true;
}

Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
                                        TrustSubstitutionMap& outSubstitutions)
{
  TNode in = tin.getNode();
  if (in.getKind() == kind::EQUAL)
  {
    // (and (= x t) phi) can be replaced by phi[x/t] if
    // 1) x is a variable
    // 2) x is not in the term t
    // 3) x : T and t : S, then S <: T
    if (in[0].isVar() && isLegalElimination(in[0], in[1])
        && in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
    {
      outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
      return PP_ASSERT_STATUS_SOLVED;
    }
    if (in[1].isVar() && isLegalElimination(in[1], in[0])
        && in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
    {
      outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
      return PP_ASSERT_STATUS_SOLVED;
    }
    if (in[0].isConst() && in[1].isConst())
    {
      if (in[0] != in[1])
      {
        return PP_ASSERT_STATUS_CONFLICT;
      }
    }
  }
  else if (in.getKind() == kind::NOT && in[0].getKind() == kind::EQUAL
           && in[0][0].getType().isBoolean())
  {
    TNode eq = in[0];
    if (eq[0].isVar())
    {
      Node res = eq[0].eqNode(eq[1].notNode());
      TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr);
      return ppAssert(tn, outSubstitutions);
    }
    else if (eq[1].isVar())
    {
      Node res = eq[1].eqNode(eq[0].notNode());
      TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr);
      return ppAssert(tn, outSubstitutions);
    }
  }

  return PP_ASSERT_STATUS_UNSOLVED;
}

std::pair<bool, Node> Theory::entailmentCheck(TNode lit)
{
  return make_pair(false, Node::null());
}

void Theory::addCarePair(TNode t1, TNode t2) {
  if (d_careGraph) {
    d_careGraph->insert(CarePair(t1, t2, d_id));
  }
}

void Theory::getCareGraph(CareGraph* careGraph) {
  Assert(careGraph != NULL);

  Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
  TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
  d_careGraph = careGraph;
  computeCareGraph();
  d_careGraph = NULL;
}

bool Theory::proofsEnabled() const
{
  return d_env.getProofNodeManager() != nullptr;
}

EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
{
  // if not using an equality engine, then by default we don't know the status
  if (d_equalityEngine == nullptr)
  {
    return EQUALITY_UNKNOWN;
  }
  Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl;
  Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));

  // Check for equality (simplest)
  if (d_equalityEngine->areEqual(a, b))
  {
    // The terms are implied to be equal
    return EQUALITY_TRUE;
  }

  // Check for disequality
  if (d_equalityEngine->areDisequal(a, b, false))
  {
    // The terms are implied to be dis-equal
    return EQUALITY_FALSE;
  }

  // All other terms are unknown, which is conservative. A theory may override
  // this method if it knows more information.
  return EQUALITY_UNKNOWN;
}

void Theory::check(Effort level)
{
  // see if we are already done (as an optimization)
  if (done() && level < EFFORT_FULL)
  {
    return;
  }
  Assert(d_theoryState!=nullptr);
  // standard calls for resource, stats
  d_out->spendResource(Resource::TheoryCheckStep);
  TimerStat::CodeTimer checkTimer(d_checkTime);
  Trace("theory-check") << "Theory::preCheck " << level << " " << d_id
                        << std::endl;
  // pre-check at level
  if (preCheck(level))
  {
    // check aborted for a theory-specific reason
    return;
  }
  Assert(d_theoryState != nullptr);
  Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl;
  // process the pending fact queue
  while (!done() && !d_theoryState->isInConflict())
  {
    // Get the next assertion from the fact queue
    Assertion assertion = get();
    TNode fact = assertion.d_assertion;
    Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id
                          << std::endl;
    bool polarity = fact.getKind() != kind::NOT;
    TNode atom = polarity ? fact : fact[0];
    // call the pre-notify method
    if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false))
    {
      // handled in theory-specific way that doesn't involve equality engine
      continue;
    }
    Trace("theory-check") << "Theory::assert " << fact << " " << d_id
                          << std::endl;
    // Theories that don't have an equality engine should always return true
    // for preNotifyFact
    Assert(d_equalityEngine != nullptr);
    // assert to the equality engine
    if (atom.getKind() == kind::EQUAL)
    {
      d_equalityEngine->assertEquality(atom, polarity, fact);
    }
    else
    {
      d_equalityEngine->assertPredicate(atom, polarity, fact);
    }
    Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id
                          << std::endl;
    // notify the theory of the new fact, which is not internal
    notifyFact(atom, polarity, fact, false);
  }
  Trace("theory-check") << "Theory::postCheck " << d_id << std::endl;
  // post-check at level
  postCheck(level);
  Trace("theory-check") << "Theory::finish check " << d_id << std::endl;
}

bool Theory::preCheck(Effort level) { return false; }

void Theory::postCheck(Effort level) {}

bool Theory::preNotifyFact(
    TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
{
  return false;
}

void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal)
{
}

void Theory::preRegisterTerm(TNode node) {}

void Theory::addSharedTerm(TNode n)
{
  Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")"
                   << std::endl;
  Debug("theory::assertions")
      << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
  d_sharedTerms.push_back(n);
  // now call theory-specific method notifySharedTerm
  notifySharedTerm(n);
  // if we have an equality engine, add the trigger term
  if (d_equalityEngine != nullptr)
  {
    d_equalityEngine->addTriggerTerm(n, d_id);
  }
}

eq::EqualityEngine* Theory::getEqualityEngine()
{
  // get the assigned equality engine, which is a pointer stored in this class
  return d_equalityEngine;
}

bool Theory::usesCentralEqualityEngine() const
{
  return usesCentralEqualityEngine(d_id);
}

bool Theory::usesCentralEqualityEngine(TheoryId id)
{
  if (id == THEORY_BUILTIN)
  {
    return true;
  }
  if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
  {
    return false;
  }
  if (id == THEORY_ARITH)
  {
    // conditional on whether we are using the equality solver
    return options::arithEqSolver();
  }
  return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS
         || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS
         || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV;
}

bool Theory::expUsingCentralEqualityEngine(TheoryId id)
{
  return id != THEORY_ARITH && usesCentralEqualityEngine(id);
}

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Tim King, Dejan Jovanovic
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		* Base for theory interface.
14		*/
15
16		#include "theory/theory.h"
17
18		#include <iostream>
19		#include <sstream>
20		#include <string>
21		#include <vector>
22
23		#include "base/check.h"
24		#include "expr/node_algorithm.h"
25		#include "options/arith_options.h"
26		#include "options/smt_options.h"
27		#include "options/theory_options.h"
28		#include "smt/smt_statistics_registry.h"
29		#include "theory/ee_setup_info.h"
30		#include "theory/ext_theory.h"
31		#include "theory/output_channel.h"
32		#include "theory/quantifiers_engine.h"
33		#include "theory/substitutions.h"
34		#include "theory/theory_inference_manager.h"
35		#include "theory/theory_model.h"
36		#include "theory/theory_rewriter.h"
37		#include "theory/theory_state.h"
38		#include "theory/trust_substitutions.h"
39
40		using namespace std;
41
42		namespace cvc5 {
43		namespace theory {
44
45		/** Default value for the uninterpreted sorts is the UF theory */
46		TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
47
48		std::ostream& operator<<(std::ostream& os, Theory::Effort level){
49		switch(level){
50		case Theory::EFFORT_STANDARD:
51		os << "EFFORT_STANDARD"; break;
52		case Theory::EFFORT_FULL:
53		os << "EFFORT_FULL"; break;
54		case Theory::EFFORT_LAST_CALL:
55		os << "EFFORT_LAST_CALL"; break;
56		default:
57		Unreachable();
58		}
59		return os;
60		}/* ostream& operator<<(ostream&, Theory::Effort) */
61
62	129301	Theory::Theory(TheoryId id,
63		Env& env,
64		OutputChannel& out,
65		Valuation valuation,
66	129301	std::string name)
67		: EnvObj(env),
68		d_id(id),
69	129301	d_facts(d_env.getContext()),
70	129301	d_factsHead(d_env.getContext(), 0),
71	129301	d_sharedTermsIndex(d_env.getContext(), 0),
72		d_careGraph(nullptr),
73		d_instanceName(name),
74	258602	d_checkTime(statisticsRegistry().registerTimer(getStatsPrefix(id) + name
75	258602	+ "checkTime")),
76	129301	d_computeCareGraphTime(statisticsRegistry().registerTimer(
77	258602	getStatsPrefix(id) + name + "computeCareGraphTime")),
78	129301	d_sharedTerms(d_env.getContext()),
79		d_out(&out),
80		d_valuation(valuation),
81		d_equalityEngine(nullptr),
82		d_allocEqualityEngine(nullptr),
83		d_theoryState(nullptr),
84		d_inferManager(nullptr),
85		d_quantEngine(nullptr),
86	129301	d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
87	1163709	: nullptr)
88		{
89	129301	}
90
91	129262	Theory::~Theory() {
92	129262	}
93
94	19886	bool Theory::needsEqualityEngine(EeSetupInfo& esi)
95		{
96		// by default, this theory does not use an (official) equality engine
97	19886	return false;
98		}
99
100	129259	void Theory::setEqualityEngine(eq::EqualityEngine* ee)
101		{
102		// set the equality engine pointer
103	129259	d_equalityEngine = ee;
104	129259	if (d_theoryState != nullptr)
105		{
106	119316	d_theoryState->setEqualityEngine(ee);
107		}
108	129259	if (d_inferManager != nullptr)
109		{
110	119316	d_inferManager->setEqualityEngine(ee);
111		}
112	129259	}
113
114	129259	void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
115		{
116		// quantifiers engine may be null if not in quantified logic
117	129259	d_quantEngine = qe;
118	129259	}
119
120	129259	void Theory::setDecisionManager(DecisionManager* dm)
121		{
122	129259	Assert(dm != nullptr);
123	129259	if (d_inferManager != nullptr)
124		{
125	119316	d_inferManager->setDecisionManager(dm);
126		}
127	129259	}
128
129		void Theory::finishInitStandalone()
130		{
131		EeSetupInfo esi;
132		if (needsEqualityEngine(esi))
133		{
134		// always associated with the same SAT context as the theory
135		d_allocEqualityEngine.reset(new eq::EqualityEngine(
136		*esi.d_notify, context(), esi.d_name, esi.d_constantsAreTriggers));
137		// use it as the official equality engine
138		setEqualityEngine(d_allocEqualityEngine.get());
139		}
140		finishInit();
141		}
142
143	187345298	TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
144		{
145	187345298	TheoryId tid = THEORY_BUILTIN;
146	187345298	switch(mode) {
147	128108682	case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
148		// Constants, variables, 0-ary constructors
149	128108682	if (node.isVar())
150		{
151	4937831	if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
152		{
153	228017	tid = THEORY_UF;
154		}
155		else
156		{
157	4709814	tid = Theory::theoryOf(node.getType());
158		}
159		}
160	123170851	else if (node.getKind() == kind::EQUAL)
161		{
162		// Equality is owned by the theory that owns the domain
163	7615614	tid = Theory::theoryOf(node[0].getType());
164		}
165		else
166		{
167		// Regular nodes are owned by the kind. Notice that constants are a
168		// special case here, where the theory of the kind of a constant
169		// always coincides with the type of that constant.
170	115555237	tid = kindToTheoryId(node.getKind());
171		}
172	128108682	break;
173	59236616	case options::TheoryOfMode::THEORY_OF_TERM_BASED:
174		// Variables
175	59236616	if (node.isVar())
176		{
177	5215201	if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
178		{
179		// We treat the variables as uninterpreted
180	5207664	tid = s_uninterpretedSortOwner;
181		}
182		else
183		{
184	7537	if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
185		{
186		// Boolean vars go to UF
187	3752	tid = THEORY_UF;
188		}
189		else
190		{
191		// Except for the Boolean ones
192	3785	tid = THEORY_BOOL;
193		}
194		}
195		}
196	54021415	else if (node.getKind() == kind::EQUAL)
197		{ // Equality
198		// If one of them is an ITE, it's irelevant, since they will get
199		// replaced out anyhow
200	4800599	if (node[0].getKind() == kind::ITE)
201		{
202	5719	tid = Theory::theoryOf(node[0].getType());
203		}
204	4794880	else if (node[1].getKind() == kind::ITE)
205		{
206	9416	tid = Theory::theoryOf(node[1].getType());
207		}
208		else
209		{
210	9570928	TNode l = node[0];
211	9570928	TNode r = node[1];
212	9570928	TypeNode ltype = l.getType();
213	9570928	TypeNode rtype = r.getType();
214		// If the types are different, we must assign based on type due
215		// to handling subtypes (limited to arithmetic). Also, if we are
216		// a Boolean equality, we must assign THEORY_BOOL.
217	4785464	if (ltype != rtype \|\| ltype.isBoolean())
218		{
219	67882	tid = Theory::theoryOf(ltype);
220		}
221		else
222		{
223		// If both sides belong to the same theory the choice is easy
224	4717582	TheoryId T1 = Theory::theoryOf(l);
225	4717582	TheoryId T2 = Theory::theoryOf(r);
226	4717582	if (T1 == T2)
227		{
228	2663223	tid = T1;
229		}
230		else
231		{
232	2054359	TheoryId T3 = Theory::theoryOf(ltype);
233		// This is a case of
234		// * x*y = f(z) -> UF
235		// * x = c -> UF
236		// * f(x) = read(a, y) -> either UF or ARRAY
237		// at least one of the theories has to be parametric, i.e. theory
238		// of the type is different from the theory of the term
239	2054359	if (T1 == T3)
240		{
241	49929	tid = T2;
242		}
243	2004430	else if (T2 == T3)
244		{
245	1944546	tid = T1;
246		}
247		else
248		{
249		// If both are parametric, we take the smaller one (arbitrary)
250	59884	tid = T1 < T2 ? T1 : T2;
251		}
252		}
253		}
254		}
255		}
256		else
257		{
258		// Regular nodes are owned by the kind, which includes constants as a
259		// special case.
260	49220816	tid = kindToTheoryId(node.getKind());
261		}
262	59236616	break;
263		default:
264		Unreachable();
265		}
266	187345298	Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
267	187345298	return tid;
268		}
269
270	1026231	void Theory::notifySharedTerm(TNode n)
271		{
272		// do nothing
273	1026231	}
274
275	2631369	void Theory::notifyInConflict()
276		{
277	2631369	if (d_inferManager != nullptr)
278		{
279	2428956	d_inferManager->notifyInConflict();
280		}
281	2631369	}
282
283	6293	void Theory::computeCareGraph() {
284	6293	Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
285	6821	for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
286	1056	TNode a = d_sharedTerms[i];
287	1056	TypeNode aType = a.getType();
288	5094	for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
289	8676	TNode b = d_sharedTerms[j];
290	4566	if (b.getType() != aType) {
291		// We don't care about the terms of different types
292	456	continue;
293		}
294	4110	switch (d_valuation.getEqualityStatus(a, b)) {
295	3304	case EQUALITY_TRUE_AND_PROPAGATED:
296		case EQUALITY_FALSE_AND_PROPAGATED:
297		// If we know about it, we should have propagated it, so we can skip
298	3304	break;
299	806	default:
300		// Let's split on it
301	806	addCarePair(a, b);
302	806	break;
303		}
304		}
305		}
306	6293	}
307
308		void Theory::printFacts(std::ostream& os) const {
309		unsigned i, n = d_facts.size();
310		for(i = 0; i < n; i++){
311		const Assertion& a_i = d_facts[i];
312		Node assertion = a_i;
313		os << d_id << '[' << i << ']' << " " << assertion << endl;
314		}
315		}
316
317		void Theory::debugPrintFacts() const{
318		DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
319		printFacts(DebugChannel.getStream());
320		}
321
322	17976	bool Theory::isLegalElimination(TNode x, TNode val)
323		{
324	17976	Assert(x.isVar());
325	35952	if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE
326	17976	\|\| val.getKind() == kind::BOOLEAN_TERM_VARIABLE)
327		{
328		return false;
329		}
330	17976	if (expr::hasSubterm(val, x))
331		{
332	4757	return false;
333		}
334	13219	if (!val.getType().isSubtypeOf(x.getType()))
335		{
336		return false;
337		}
338	13219	if (!options::produceModels() && !logicInfo().isQuantified())
339		{
340		// Don't care about the model and logic is not quantified, we can eliminate.
341	2951	return true;
342		}
343		// If models are enabled, then it depends on whether the term contains any
344		// unevaluable operators like FORALL, SINE, etc. Having such operators makes
345		// model construction contain non-constant values for variables, which is
346		// not ideal from a user perspective.
347		// We also insist on this check since the term to eliminate should never
348		// contain quantifiers, or else variable shadowing issues may arise.
349		// there should be a model object
350	10268	TheoryModel* tm = d_valuation.getModel();
351	10268	Assert(tm != nullptr);
352	10268	return tm->isLegalElimination(x, val);
353		}
354
355	42606	std::unordered_set<TNode> Theory::currentlySharedTerms() const
356		{
357	42606	std::unordered_set<TNode> currentlyShared;
358	1090102	for (shared_terms_iterator i = shared_terms_begin(),
359	42606	i_end = shared_terms_end(); i != i_end; ++i) {
360	1047496	currentlyShared.insert (*i);
361		}
362	42606	return currentlyShared;
363		}
364
365	68148	bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet)
366		{
367		// if we are using an equality engine, assert it to the model
368	68148	if (d_equalityEngine != nullptr && !termSet.empty())
369		{
370	56124	Trace("model-builder") << "Assert Equality engine for " << d_id
371	28062	<< std::endl;
372	28062	if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
373		{
374		return false;
375		}
376		}
377	68148	Trace("model-builder") << "Collect Model values for " << d_id << std::endl;
378		// now, collect theory-specific value assigments
379	68148	return collectModelValues(m, termSet);
380		}
381
382	65153	void Theory::computeRelevantTerms(std::set<Node>& termSet)
383		{
384		// by default, there are no additional relevant terms
385	65153	}
386
387	122078	void Theory::collectAssertedTerms(std::set<Node>& termSet,
388		bool includeShared) const
389		{
390		// Collect all terms appearing in assertions
391	122078	context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
392	122078	assert_it_end = facts_end();
393	10902806	for (; assert_it != assert_it_end; ++assert_it)
394		{
395	5390364	collectTerms(*assert_it, termSet);
396		}
397
398	122078	if (includeShared)
399		{
400		// Add terms that are shared terms
401	122078	context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(),
402	122078	shared_it_end = shared_terms_end();
403	3215230	for (; shared_it != shared_it_end; ++shared_it)
404		{
405	1546576	collectTerms(*shared_it, termSet);
406		}
407		}
408	122078	}
409
410	6936940	void Theory::collectTerms(TNode n, std::set<Node>& termSet) const
411		{
412		const std::set<Kind>& irrKinds =
413	6936940	d_theoryState->getModel()->getIrrelevantKinds();
414	13873880	std::vector<TNode> visit;
415	13873880	TNode cur;
416	6936940	visit.push_back(n);
417	17210194	do
418		{
419	24147134	cur = visit.back();
420	24147134	visit.pop_back();
421	24147134	if (termSet.find(cur) != termSet.end())
422		{
423		// already visited
424	12529975	continue;
425		}
426	11617159	Kind k = cur.getKind();
427		// only add to term set if a relevant kind
428	11617159	if (irrKinds.find(k) == irrKinds.end())
429		{
430	6044678	termSet.insert(cur);
431		}
432		// traverse owned terms, don't go under quantifiers
433	32621459	if ((k == kind::NOT \|\| k == kind::EQUAL \|\| Theory::theoryOf(cur) == d_id)
434	33755930	&& !cur.isClosure())
435		{
436	10492110	visit.insert(visit.end(), cur.begin(), cur.end());
437		}
438	24147134	} while (!visit.empty());
439	6936940	}
440
441	4722	bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
442		{
443	4722	return true;
444		}
445
446	46482	Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
447		TrustSubstitutionMap& outSubstitutions)
448		{
449	92964	TNode in = tin.getNode();
450	46482	if (in.getKind() == kind::EQUAL)
451		{
452		// (and (= x t) phi) can be replaced by phi[x/t] if
453		// 1) x is a variable
454		// 2) x is not in the term t
455		// 3) x : T and t : S, then S <: T
456	78170	if (in[0].isVar() && isLegalElimination(in[0], in[1])
457	73543	&& in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
458		{
459	10402	outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
460	10402	return PP_ASSERT_STATUS_SOLVED;
461		}
462	32182	if (in[1].isVar() && isLegalElimination(in[1], in[0])
463	32182	&& in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
464		{
465	247	outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
466	247	return PP_ASSERT_STATUS_SOLVED;
467		}
468	10398	if (in[0].isConst() && in[1].isConst())
469		{
470		if (in[0] != in[1])
471		{
472		return PP_ASSERT_STATUS_CONFLICT;
473		}
474		}
475		}
476	74409	else if (in.getKind() == kind::NOT && in[0].getKind() == kind::EQUAL
477	73978	&& in[0][0].getType().isBoolean())
478		{
479	36	TNode eq = in[0];
480	34	if (eq[0].isVar())
481		{
482	64	Node res = eq[0].eqNode(eq[1].notNode());
483	64	TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr);
484	32	return ppAssert(tn, outSubstitutions);
485		}
486	2	else if (eq[1].isVar())
487		{
488		Node res = eq[1].eqNode(eq[0].notNode());
489		TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr);
490		return ppAssert(tn, outSubstitutions);
491		}
492		}
493
494	35801	return PP_ASSERT_STATUS_UNSOLVED;
495		}
496
497		std::pair<bool, Node> Theory::entailmentCheck(TNode lit)
498		{
499		return make_pair(false, Node::null());
500		}
501
502	41530	void Theory::addCarePair(TNode t1, TNode t2) {
503	41530	if (d_careGraph) {
504	41530	d_careGraph->insert(CarePair(t1, t2, d_id));
505		}
506	41530	}
507
508	66760	void Theory::getCareGraph(CareGraph* careGraph) {
509	66760	Assert(careGraph != NULL);
510
511	66760	Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
512	133520	TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
513	66760	d_careGraph = careGraph;
514	66760	computeCareGraph();
515	66760	d_careGraph = NULL;
516	66760	}
517
518		bool Theory::proofsEnabled() const
519		{
520		return d_env.getProofNodeManager() != nullptr;
521		}
522
523	20114	EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
524		{
525		// if not using an equality engine, then by default we don't know the status
526	20114	if (d_equalityEngine == nullptr)
527		{
528	5768	return EQUALITY_UNKNOWN;
529		}
530	14346	Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl;
531	14346	Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
532
533		// Check for equality (simplest)
534	14346	if (d_equalityEngine->areEqual(a, b))
535		{
536		// The terms are implied to be equal
537	7253	return EQUALITY_TRUE;
538		}
539
540		// Check for disequality
541	7093	if (d_equalityEngine->areDisequal(a, b, false))
542		{
543		// The terms are implied to be dis-equal
544	2572	return EQUALITY_FALSE;
545		}
546
547		// All other terms are unknown, which is conservative. A theory may override
548		// this method if it knows more information.
549	4521	return EQUALITY_UNKNOWN;
550		}
551
552	14762754	void Theory::check(Effort level)
553		{
554		// see if we are already done (as an optimization)
555	14762754	if (done() && level < EFFORT_FULL)
556		{
557	19041930	return;
558		}
559	5241789	Assert(d_theoryState!=nullptr);
560		// standard calls for resource, stats
561	5241789	d_out->spendResource(Resource::TheoryCheckStep);
562	10483578	TimerStat::CodeTimer checkTimer(d_checkTime);
563	10483578	Trace("theory-check") << "Theory::preCheck " << level << " " << d_id
564	5241789	<< std::endl;
565		// pre-check at level
566	5241789	if (preCheck(level))
567		{
568		// check aborted for a theory-specific reason
569		return;
570		}
571	5241789	Assert(d_theoryState != nullptr);
572	5241789	Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl;
573		// process the pending fact queue
574	35632389	while (!done() && !d_theoryState->isInConflict())
575		{
576		// Get the next assertion from the fact queue
577	24406088	Assertion assertion = get();
578	24406088	TNode fact = assertion.d_assertion;
579	30390606	Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id
580	15195303	<< std::endl;
581	15195303	bool polarity = fact.getKind() != kind::NOT;
582	24406088	TNode atom = polarity ? fact : fact[0];
583		// call the pre-notify method
584	15195303	if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false))
585		{
586		// handled in theory-specific way that doesn't involve equality engine
587	5984518	continue;
588		}
589	18421570	Trace("theory-check") << "Theory::assert " << fact << " " << d_id
590	9210785	<< std::endl;
591		// Theories that don't have an equality engine should always return true
592		// for preNotifyFact
593	9210785	Assert(d_equalityEngine != nullptr);
594		// assert to the equality engine
595	9210785	if (atom.getKind() == kind::EQUAL)
596		{
597	6371559	d_equalityEngine->assertEquality(atom, polarity, fact);
598		}
599		else
600		{
601	2839229	d_equalityEngine->assertPredicate(atom, polarity, fact);
602		}
603	18421564	Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id
604	9210782	<< std::endl;
605		// notify the theory of the new fact, which is not internal
606	9210782	notifyFact(atom, polarity, fact, false);
607		}
608	5241786	Trace("theory-check") << "Theory::postCheck " << d_id << std::endl;
609		// post-check at level
610	5241786	postCheck(level);
611	5241785	Trace("theory-check") << "Theory::finish check " << d_id << std::endl;
612		}
613
614	1959801	bool Theory::preCheck(Effort level) { return false; }
615
616	2	void Theory::postCheck(Effort level) {}
617
618	5614306	bool Theory::preNotifyFact(
619		TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
620		{
621	5614306	return false;
622		}
623
624	9695	void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal)
625		{
626	9695	}
627
628	22328	void Theory::preRegisterTerm(TNode node) {}
629
630	1849646	void Theory::addSharedTerm(TNode n)
631		{
632	3699292	Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")"
633	1849646	<< std::endl;
634	3699292	Debug("theory::assertions")
635	1849646	<< "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
636	1849646	d_sharedTerms.push_back(n);
637		// now call theory-specific method notifySharedTerm
638	1849646	notifySharedTerm(n);
639		// if we have an equality engine, add the trigger term
640	1849646	if (d_equalityEngine != nullptr)
641		{
642	1844178	d_equalityEngine->addTriggerTerm(n, d_id);
643		}
644	1849646	}
645
646	377679	eq::EqualityEngine* Theory::getEqualityEngine()
647		{
648		// get the assigned equality engine, which is a pointer stored in this class
649	377679	return d_equalityEngine;
650		}
651
652	350	bool Theory::usesCentralEqualityEngine() const
653		{
654	350	return usesCentralEqualityEngine(d_id);
655		}
656
657	28838241	bool Theory::usesCentralEqualityEngine(TheoryId id)
658		{
659	28838241	if (id == THEORY_BUILTIN)
660		{
661	10694148	return true;
662		}
663	18144093	if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
664		{
665	18127651	return false;
666		}
667	16442	if (id == THEORY_ARITH)
668		{
669		// conditional on whether we are using the equality solver
670	70	return options::arithEqSolver();
671		}
672	15456	return id == THEORY_UF \|\| id == THEORY_DATATYPES \|\| id == THEORY_BAGS
673	9492	\|\| id == THEORY_FP \|\| id == THEORY_SETS \|\| id == THEORY_STRINGS
674	25288	\|\| id == THEORY_SEP \|\| id == THEORY_ARRAYS \|\| id == THEORY_BV;
675		}
676
677	33391379	bool Theory::expUsingCentralEqualityEngine(TheoryId id)
678		{
679	33391379	return id != THEORY_ARITH && usesCentralEqualityEngine(id);
680		}
681
682		} // namespace theory
683	29589	} // namespace cvc5