Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory.cpp	Lines:	265	310	85.5 %
Date:	2021-09-29	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	81565	Theory::Theory(TheoryId id,
63		Env& env,
64		OutputChannel& out,
65		Valuation valuation,
66	81565	std::string name)
67		: EnvObj(env),
68		d_id(id),
69	81565	d_facts(d_env.getContext()),
70	81565	d_factsHead(d_env.getContext(), 0),
71	81565	d_sharedTermsIndex(d_env.getContext(), 0),
72		d_careGraph(nullptr),
73		d_instanceName(name),
74	163130	d_checkTime(statisticsRegistry().registerTimer(getStatsPrefix(id) + name
75	163130	+ "checkTime")),
76	81565	d_computeCareGraphTime(statisticsRegistry().registerTimer(
77	163130	getStatsPrefix(id) + name + "computeCareGraphTime")),
78	81565	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	81565	d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
87	734085	: nullptr)
88		{
89	81565	}
90
91	81526	Theory::~Theory() {
92	81526	}
93
94	12542	bool Theory::needsEqualityEngine(EeSetupInfo& esi)
95		{
96		// by default, this theory does not use an (official) equality engine
97	12542	return false;
98		}
99
100	81523	void Theory::setEqualityEngine(eq::EqualityEngine* ee)
101		{
102		// set the equality engine pointer
103	81523	d_equalityEngine = ee;
104	81523	if (d_theoryState != nullptr)
105		{
106	75252	d_theoryState->setEqualityEngine(ee);
107		}
108	81523	if (d_inferManager != nullptr)
109		{
110	75252	d_inferManager->setEqualityEngine(ee);
111		}
112	81523	}
113
114	81523	void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
115		{
116		// quantifiers engine may be null if not in quantified logic
117	81523	d_quantEngine = qe;
118	81523	}
119
120	81523	void Theory::setDecisionManager(DecisionManager* dm)
121		{
122	81523	Assert(dm != nullptr);
123	81523	if (d_inferManager != nullptr)
124		{
125	75252	d_inferManager->setDecisionManager(dm);
126		}
127	81523	}
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	104885146	TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
144		{
145	104885146	TheoryId tid = THEORY_BUILTIN;
146	104885146	switch(mode) {
147	71063297	case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
148		// Constants, variables, 0-ary constructors
149	71063297	if (node.isVar())
150		{
151	2708582	if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
152		{
153	215629	tid = THEORY_UF;
154		}
155		else
156		{
157	2492953	tid = Theory::theoryOf(node.getType());
158		}
159		}
160	68354715	else if (node.getKind() == kind::EQUAL)
161		{
162		// Equality is owned by the theory that owns the domain
163	4219967	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	64134748	tid = kindToTheoryId(node.getKind());
171		}
172	71063297	break;
173	33821849	case options::TheoryOfMode::THEORY_OF_TERM_BASED:
174		// Variables
175	33821849	if (node.isVar())
176		{
177	2622239	if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
178		{
179		// We treat the variables as uninterpreted
180	2615687	tid = s_uninterpretedSortOwner;
181		}
182		else
183		{
184	6552	if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
185		{
186		// Boolean vars go to UF
187	3323	tid = THEORY_UF;
188		}
189		else
190		{
191		// Except for the Boolean ones
192	3229	tid = THEORY_BOOL;
193		}
194		}
195		}
196	31199610	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	2888450	if (node[0].getKind() == kind::ITE)
201		{
202	3274	tid = Theory::theoryOf(node[0].getType());
203		}
204	2885176	else if (node[1].getKind() == kind::ITE)
205		{
206	4819	tid = Theory::theoryOf(node[1].getType());
207		}
208		else
209		{
210	5760714	TNode l = node[0];
211	5760714	TNode r = node[1];
212	5760714	TypeNode ltype = l.getType();
213	5760714	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	2880357	if (ltype != rtype \|\| ltype.isBoolean())
218		{
219	51417	tid = Theory::theoryOf(ltype);
220		}
221		else
222		{
223		// If both sides belong to the same theory the choice is easy
224	2828940	TheoryId T1 = Theory::theoryOf(l);
225	2828940	TheoryId T2 = Theory::theoryOf(r);
226	2828940	if (T1 == T2)
227		{
228	1449131	tid = T1;
229		}
230		else
231		{
232	1379809	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	1379809	if (T1 == T3)
240		{
241	35795	tid = T2;
242		}
243	1344014	else if (T2 == T3)
244		{
245	1298102	tid = T1;
246		}
247		else
248		{
249		// If both are parametric, we take the smaller one (arbitrary)
250	45912	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	28311160	tid = kindToTheoryId(node.getKind());
261		}
262	33821849	break;
263		default:
264		Unreachable();
265		}
266	104885146	Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
267	104885146	return tid;
268		}
269
270	558119	void Theory::notifySharedTerm(TNode n)
271		{
272		// do nothing
273	558119	}
274
275	1642550	void Theory::notifyInConflict()
276		{
277	1642550	if (d_inferManager != nullptr)
278		{
279	1516200	d_inferManager->notifyInConflict();
280		}
281	1642550	}
282
283	5131	void Theory::computeCareGraph() {
284	5131	Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
285	5643	for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
286	1024	TNode a = d_sharedTerms[i];
287	1024	TypeNode aType = a.getType();
288	4958	for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
289	8436	TNode b = d_sharedTerms[j];
290	4446	if (b.getType() != aType) {
291		// We don't care about the terms of different types
292	456	continue;
293		}
294	3990	switch (d_valuation.getEqualityStatus(a, b)) {
295	3274	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	3274	break;
299	716	default:
300		// Let's split on it
301	716	addCarePair(a, b);
302	716	break;
303		}
304		}
305		}
306	5131	}
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	12465	bool Theory::isLegalElimination(TNode x, TNode val)
323		{
324	12465	Assert(x.isVar());
325	24930	if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE
326	12465	\|\| val.getKind() == kind::BOOLEAN_TERM_VARIABLE)
327		{
328		return false;
329		}
330	12465	if (expr::hasSubterm(val, x))
331		{
332	3197	return false;
333		}
334	9268	if (!val.getType().isSubtypeOf(x.getType()))
335		{
336		return false;
337		}
338	9268	if (!options::produceModels() && !logicInfo().isQuantified())
339		{
340		// Don't care about the model and logic is not quantified, we can eliminate.
341	2378	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	6890	TheoryModel* tm = d_valuation.getModel();
351	6890	Assert(tm != nullptr);
352	6890	return tm->isLegalElimination(x, val);
353		}
354
355	31021	std::unordered_set<TNode> Theory::currentlySharedTerms() const
356		{
357	31021	std::unordered_set<TNode> currentlyShared;
358	834561	for (shared_terms_iterator i = shared_terms_begin(),
359	31021	i_end = shared_terms_end(); i != i_end; ++i) {
360	803540	currentlyShared.insert (*i);
361		}
362	31021	return currentlyShared;
363		}
364
365	58226	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	58226	if (d_equalityEngine != nullptr && !termSet.empty())
369		{
370	47388	Trace("model-builder") << "Assert Equality engine for " << d_id
371	23694	<< std::endl;
372	23694	if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
373		{
374		return false;
375		}
376		}
377	58226	Trace("model-builder") << "Collect Model values for " << d_id << std::endl;
378		// now, collect theory-specific value assigments
379	58226	return collectModelValues(m, termSet);
380		}
381
382	55071	void Theory::computeRelevantTerms(std::set<Node>& termSet)
383		{
384		// by default, there are no additional relevant terms
385	55071	}
386
387	97927	void Theory::collectAssertedTerms(std::set<Node>& termSet,
388		bool includeShared) const
389		{
390		// Collect all terms appearing in assertions
391	97927	context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
392	97927	assert_it_end = facts_end();
393	8126763	for (; assert_it != assert_it_end; ++assert_it)
394		{
395	4014418	collectTerms(*assert_it, termSet);
396		}
397
398	97927	if (includeShared)
399		{
400		// Add terms that are shared terms
401	97927	context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(),
402	97927	shared_it_end = shared_terms_end();
403	2638495	for (; shared_it != shared_it_end; ++shared_it)
404		{
405	1270284	collectTerms(*shared_it, termSet);
406		}
407		}
408	97927	}
409
410	5284702	void Theory::collectTerms(TNode n, std::set<Node>& termSet) const
411		{
412		const std::set<Kind>& irrKinds =
413	5284702	d_theoryState->getModel()->getIrrelevantKinds();
414	10569404	std::vector<TNode> visit;
415	10569404	TNode cur;
416	5284702	visit.push_back(n);
417	12508002	do
418		{
419	17792704	cur = visit.back();
420	17792704	visit.pop_back();
421	17792704	if (termSet.find(cur) != termSet.end())
422		{
423		// already visited
424	9276776	continue;
425		}
426	8515928	Kind k = cur.getKind();
427		// only add to term set if a relevant kind
428	8515928	if (irrKinds.find(k) == irrKinds.end())
429		{
430	4238700	termSet.insert(cur);
431		}
432		// traverse owned terms, don't go under quantifiers
433	23897616	if ((k == kind::NOT \|\| k == kind::EQUAL \|\| Theory::theoryOf(cur) == d_id)
434	24678109	&& !cur.isClosure())
435		{
436	7625617	visit.insert(visit.end(), cur.begin(), cur.end());
437		}
438	17792704	} while (!visit.empty());
439	5284702	}
440
441	4180	bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
442		{
443	4180	return true;
444		}
445
446	29974	Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
447		TrustSubstitutionMap& outSubstitutions)
448		{
449	59948	TNode in = tin.getNode();
450	29974	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	53909	if (in[0].isVar() && isLegalElimination(in[0], in[1])
457	50781	&& in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
458		{
459	7302	outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
460	7302	return PP_ASSERT_STATUS_SOLVED;
461		}
462	21717	if (in[1].isVar() && isLegalElimination(in[1], in[0])
463	21717	&& in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
464		{
465	144	outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
466	144	return PP_ASSERT_STATUS_SOLVED;
467		}
468	7047	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	45247	else if (in.getKind() == kind::NOT && in[0].getKind() == kind::EQUAL
477	44940	&& in[0][0].getType().isBoolean())
478		{
479	27	TNode eq = in[0];
480	26	if (eq[0].isVar())
481		{
482	50	Node res = eq[0].eqNode(eq[1].notNode());
483	50	TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr);
484	25	return ppAssert(tn, outSubstitutions);
485		}
486	1	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	22503	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	21148	void Theory::addCarePair(TNode t1, TNode t2) {
503	21148	if (d_careGraph) {
504	21148	d_careGraph->insert(CarePair(t1, t2, d_id));
505		}
506	21148	}
507
508	52111	void Theory::getCareGraph(CareGraph* careGraph) {
509	52111	Assert(careGraph != NULL);
510
511	52111	Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
512	104222	TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
513	52111	d_careGraph = careGraph;
514	52111	computeCareGraph();
515	52111	d_careGraph = NULL;
516	52111	}
517
518		bool Theory::proofsEnabled() const
519		{
520		return d_env.getProofNodeManager() != nullptr;
521		}
522
523	18394	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	18394	if (d_equalityEngine == nullptr)
527		{
528	5762	return EQUALITY_UNKNOWN;
529		}
530	12632	Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl;
531	12632	Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
532
533		// Check for equality (simplest)
534	12632	if (d_equalityEngine->areEqual(a, b))
535		{
536		// The terms are implied to be equal
537	6925	return EQUALITY_TRUE;
538		}
539
540		// Check for disequality
541	5707	if (d_equalityEngine->areDisequal(a, b, false))
542		{
543		// The terms are implied to be dis-equal
544	2401	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	3306	return EQUALITY_UNKNOWN;
550		}
551
552	10107485	void Theory::check(Effort level)
553		{
554		// see if we are already done (as an optimization)
555	10107485	if (done() && level < EFFORT_FULL)
556		{
557	13045510	return;
558		}
559	3584730	Assert(d_theoryState!=nullptr);
560		// standard calls for resource, stats
561	3584730	d_out->spendResource(Resource::TheoryCheckStep);
562	7169460	TimerStat::CodeTimer checkTimer(d_checkTime);
563	7169460	Trace("theory-check") << "Theory::preCheck " << level << " " << d_id
564	3584730	<< std::endl;
565		// pre-check at level
566	3584730	if (preCheck(level))
567		{
568		// check aborted for a theory-specific reason
569		return;
570		}
571	3584730	Assert(d_theoryState != nullptr);
572	3584730	Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl;
573		// process the pending fact queue
574	21644988	while (!done() && !d_theoryState->isInConflict())
575		{
576		// Get the next assertion from the fact queue
577	14575473	Assertion assertion = get();
578	14575473	TNode fact = assertion.d_assertion;
579	18060264	Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id
580	9030132	<< std::endl;
581	9030132	bool polarity = fact.getKind() != kind::NOT;
582	14575473	TNode atom = polarity ? fact : fact[0];
583		// call the pre-notify method
584	9030132	if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false))
585		{
586		// handled in theory-specific way that doesn't involve equality engine
587	3484791	continue;
588		}
589	11090682	Trace("theory-check") << "Theory::assert " << fact << " " << d_id
590	5545341	<< std::endl;
591		// Theories that don't have an equality engine should always return true
592		// for preNotifyFact
593	5545341	Assert(d_equalityEngine != nullptr);
594		// assert to the equality engine
595	5545341	if (atom.getKind() == kind::EQUAL)
596		{
597	3827219	d_equalityEngine->assertEquality(atom, polarity, fact);
598		}
599		else
600		{
601	1718125	d_equalityEngine->assertPredicate(atom, polarity, fact);
602		}
603	11090676	Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id
604	5545338	<< std::endl;
605		// notify the theory of the new fact, which is not internal
606	5545338	notifyFact(atom, polarity, fact, false);
607		}
608	3584727	Trace("theory-check") << "Theory::postCheck " << d_id << std::endl;
609		// post-check at level
610	3584727	postCheck(level);
611	3584726	Trace("theory-check") << "Theory::finish check " << d_id << std::endl;
612		}
613
614	1210688	bool Theory::preCheck(Effort level) { return false; }
615
616	2	void Theory::postCheck(Effort level) {}
617
618	3762188	bool Theory::preNotifyFact(
619		TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
620		{
621	3762188	return false;
622		}
623
624	4478	void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal)
625		{
626	4478	}
627
628	13831	void Theory::preRegisterTerm(TNode node) {}
629
630	1124740	void Theory::addSharedTerm(TNode n)
631		{
632	2249480	Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")"
633	1124740	<< std::endl;
634	2249480	Debug("theory::assertions")
635	1124740	<< "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
636	1124740	d_sharedTerms.push_back(n);
637		// now call theory-specific method notifySharedTerm
638	1124740	notifySharedTerm(n);
639		// if we have an equality engine, add the trigger term
640	1124740	if (d_equalityEngine != nullptr)
641		{
642	1120577	d_equalityEngine->addTriggerTerm(n, d_id);
643		}
644	1124740	}
645
646	163663	eq::EqualityEngine* Theory::getEqualityEngine()
647		{
648		// get the assigned equality engine, which is a pointer stored in this class
649	163663	return d_equalityEngine;
650		}
651
652	140	bool Theory::usesCentralEqualityEngine() const
653		{
654	140	return usesCentralEqualityEngine(d_id);
655		}
656
657	19790049	bool Theory::usesCentralEqualityEngine(TheoryId id)
658		{
659	19790049	if (id == THEORY_BUILTIN)
660		{
661	7093934	return true;
662		}
663	12696115	if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
664		{
665	12692783	return false;
666		}
667	3332	if (id == THEORY_ARITH)
668		{
669		// conditional on whether we are using the equality solver
670	28	return options::arithEqSolver();
671		}
672	3112	return id == THEORY_UF \|\| id == THEORY_DATATYPES \|\| id == THEORY_BAGS
673	1908	\|\| id == THEORY_FP \|\| id == THEORY_SETS \|\| id == THEORY_STRINGS
674	5039	\|\| id == THEORY_SEP \|\| id == THEORY_ARRAYS \|\| id == THEORY_BV;
675		}
676
677	22711979	bool Theory::expUsingCentralEqualityEngine(TheoryId id)
678		{
679	22711979	return id != THEORY_ARITH && usesCentralEqualityEngine(id);
680		}
681
682		} // namespace theory
683	22746	} // namespace cvc5