Standardizes a few new methods in theory to support this.
This should not change the behavior, only refactors.
This is in preparation for adding efficient care graph computation for bags, and towards possible fixes for arrays.
theory/bv/theory_bv_utils.h
theory/bv/type_enumerator.h
theory/care_graph.h
+ theory/care_pair_argument_callback.cpp
+ theory/care_pair_argument_callback.cpp
theory/combination_care_graph.cpp
theory/combination_care_graph.h
theory/combination_engine.cpp
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * The care pair argument callback.
+ */
+
+#include "theory/care_pair_argument_callback.h"
+
+namespace cvc5 {
+namespace theory {
+
+CarePairArgumentCallback::CarePairArgumentCallback(Theory& t) : d_theory(t) {}
+
+bool CarePairArgumentCallback::considerPath(TNode a, TNode b)
+{
+ // interested in finding pairs that are not disequal
+ return !d_theory.areCareDisequal(a, b);
+}
+
+void CarePairArgumentCallback::processData(TNode fa, TNode fb)
+{
+ d_theory.processCarePairArgs(fa, fb);
+}
+
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * The care pair argument callback.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__CARE_PAIR_ARGUMENT_CALLBACK_H
+#define CVC5__THEORY__CARE_PAIR_ARGUMENT_CALLBACK_H
+
+#include "expr/node_trie_algorithm.h"
+#include "theory/theory.h"
+
+namespace cvc5 {
+namespace theory {
+
+/**
+ * The standard callback for computing the care pairs from a node trie.
+ */
+class CarePairArgumentCallback : public NodeTriePathPairProcessCallback
+{
+ public:
+ CarePairArgumentCallback(Theory& t);
+ ~CarePairArgumentCallback() {}
+ /**
+ * Call on the arguments a and b of two function applications we are
+ * computing care pairs for. Returns true if a and b are not already
+ * disequal according to theory combination (Theory::areCareDisequal).
+ */
+ bool considerPath(TNode a, TNode b) override;
+ /**
+ * Called when we have two function applications that do not have pairs
+ * of disequal arguments at any position. We call Theory::processCarePairArgs
+ * to add all relevant care pairs.
+ */
+ void processData(TNode fa, TNode fb) override;
+
+ private:
+ /** Reference to theory */
+ Theory& d_theory;
+};
+
+} // namespace theory
+} // namespace cvc5
+
+#endif /* CVC5__THEORY__CARE_ARGUMENT_CALLBACK_H */
d_rewriter(env.getEvaluator()),
d_state(env, valuation),
d_im(env, *this, d_state),
- d_notify(d_im, *this)
+ d_notify(d_im, *this),
+ d_cpacb(*this)
{
d_true = NodeManager::currentNM()->mkConst( true );
return EQUALITY_FALSE_IN_MODEL;
}
-void TheoryDatatypes::addCarePairs(TNodeTrie* t1,
- TNodeTrie* t2,
- unsigned arity,
- unsigned depth,
- unsigned& n_pairs)
-{
- Trace("dt-cg") << "Process at depth " << depth << "/" << arity << std::endl;
- if( depth==arity ){
- Assert(t2 != nullptr);
- Node f1 = t1->getData();
- Node f2 = t2->getData();
- if (!areEqual(f1, f2))
- {
- Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
- std::vector<std::pair<TNode, TNode> > currentPairs;
- for (size_t k = 0, nchild = f1.getNumChildren(); k < nchild; ++k)
- {
- TNode x = f1[k];
- TNode y = f2[k];
- Assert(d_equalityEngine->hasTerm(x));
- Assert(d_equalityEngine->hasTerm(y));
- Assert(!areDisequal(x, y));
- Assert(!areCareDisequal(x, y));
- if (!d_equalityEngine->areEqual(x, y))
- {
- Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y
- << std::endl;
- if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES)
- && d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES))
- {
- TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
- x, THEORY_DATATYPES);
- TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
- y, THEORY_DATATYPES);
- currentPairs.push_back(make_pair(x_shared, y_shared));
- }
- }
- }
- for (std::pair<TNode, TNode>& p : currentPairs)
- {
- Trace("dt-cg-pair")
- << "Pair : " << p.first << " " << p.second << std::endl;
- addCarePair(p.first, p.second);
- n_pairs++;
- }
- }
- return;
- }
- if (t2 == nullptr)
- {
- if (depth + 1 < arity)
- {
- // add care pairs internal to each child
- for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
- {
- Trace("dt-cg-debug") << "Traverse into arg " << tt.first << " at depth "
- << depth << std::endl;
- addCarePairs(&tt.second, nullptr, arity, depth + 1, n_pairs);
- }
- }
- // add care pairs based on each pair of non-disequal arguments
- for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
- it != t1->d_data.end();
- ++it)
- {
- std::map<TNode, TNodeTrie>::iterator it2 = it;
- ++it2;
- for (; it2 != t1->d_data.end(); ++it2)
- {
- if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
- {
- if (!areCareDisequal(it->first, it2->first))
- {
- addCarePairs(&it->second, &it2->second, arity, depth + 1, n_pairs);
- }
- }
- }
- }
- return;
- }
- // add care pairs based on product of indices, non-disequal arguments
- for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
- {
- for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
- {
- if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
- {
- if (!areCareDisequal(tt1.first, tt2.first))
- {
- Trace("dt-cg-debug")
- << "Traverse into " << tt1.first << " " << tt2.first
- << " at depth " << depth << std::endl;
- addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
- }
- }
- }
- }
-}
-
void TheoryDatatypes::computeCareGraph(){
- unsigned n_pairs = 0;
Trace("dt-cg-summary") << "Compute graph for dt..." << d_functionTerms.size() << " " << d_sharedTerms.size() << std::endl;
Trace("dt-cg") << "Build indices..." << std::endl;
std::map<TypeNode, std::map<Node, TNodeTrie> > index;
{
Trace("dt-cg") << "Process index " << tt.first << ", " << t.first << "..."
<< std::endl;
- addCarePairs(&t.second, nullptr, arity[t.first], 0, n_pairs);
+ nodeTriePathPairProcess(&t.second, arity[t.first], d_cpacb);
Trace("dt-cg") << "...finish" << std::endl;
}
}
- Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
+ Trace("dt-cg-summary") << "...done" << std::endl;
}
bool TheoryDatatypes::collectModelValues(TheoryModel* m,
}
}
-bool TheoryDatatypes::areCareDisequal( TNode x, TNode y ) {
- Trace("datatypes-cg") << "areCareDisequal: " << x << " " << y << std::endl;
- Assert(d_equalityEngine->hasTerm(x));
- Assert(d_equalityEngine->hasTerm(y));
- if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES)
- && d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES))
- {
- TNode x_shared =
- d_equalityEngine->getTriggerTermRepresentative(x, THEORY_DATATYPES);
- TNode y_shared =
- d_equalityEngine->getTriggerTermRepresentative(y, THEORY_DATATYPES);
- EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
- if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
- return true;
- }
- }
- return false;
-}
-
TNode TheoryDatatypes::getRepresentative( TNode a ){
if( hasTerm( a ) ){
return d_equalityEngine->getRepresentative(a);
#include "context/cdlist.h"
#include "expr/attribute.h"
#include "expr/node_trie.h"
+#include "theory/care_pair_argument_callback.h"
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/inference_manager.h"
#include "theory/datatypes/proof_checker.h"
bool hasTerm( TNode a );
bool areEqual( TNode a, TNode b );
bool areDisequal( TNode a, TNode b );
- bool areCareDisequal( TNode x, TNode y );
TNode getRepresentative( TNode a );
/** Collect model values in m based on the relevant terms given by termSet */
NotifyClass d_notify;
/** Proof checker for datatypes */
DatatypesProofRuleChecker d_checker;
+ /** The care pair argument callback, used for theory combination */
+ CarePairArgumentCallback d_cpacb;
};/* class TheoryDatatypes */
} // namespace datatypes
d_skCache(env.getRewriter()),
d_state(env, valuation, d_skCache),
d_im(env, *this, d_state),
- d_internal(
- new TheorySetsPrivate(env, *this, d_state, d_im, d_skCache, d_pnm)),
+ d_cpacb(*this),
+ d_internal(new TheorySetsPrivate(
+ env, *this, d_state, d_im, d_skCache, d_pnm, d_cpacb)),
d_notify(*d_internal.get(), d_im)
{
// use the official theory state and inference manager objects
return d_internal->isEntailed( n, pol );
}
+void TheorySets::processCarePairArgs(TNode a, TNode b)
+{
+ // Usually when (= (f x) (f y)), we don't care whether (= x y) is true or
+ // not for the shared variables x, y in the care graph.
+ // However, this does not apply to the membership operator since the
+ // equality or disequality between members affects the number of elements
+ // in a set. Therefore we need to split on (= x y) for kind SET_MEMBER.
+ // Example:
+ // Suppose (= (member x S) member(y S)) is true and there are
+ // no other members in S. We would get S = {x} if (= x y) is true.
+ // Otherwise we would get S = {x, y}.
+ if (a.getKind() != SET_MEMBER && d_state.areEqual(a, b))
+ {
+ return;
+ }
+ // otherwise, we add pairs for each of their arguments
+ addCarePairArgs(a, b);
+
+ d_internal->processCarePairArgs(a, b);
+}
+
/**************************** eq::NotifyClass *****************************/
void TheorySets::NotifyClass::eqNotifyNewClass(TNode t)
#include <memory>
#include "smt/logic_exception.h"
+#include "theory/care_pair_argument_callback.h"
#include "theory/sets/inference_manager.h"
#include "theory/sets/skolem_cache.h"
#include "theory/sets/solver_state.h"
bool isEntailed(Node n, bool pol);
private:
+ /**
+ * Overrides to handle a special case of set membership.
+ */
+ void processCarePairArgs(TNode a, TNode b) override;
/** Functions to handle callbacks from equality engine */
class NotifyClass : public TheoryEqNotifyClass
{
SolverState d_state;
/** The inference manager */
InferenceManager d_im;
+ /** The care pair argument callback, used for theory combination */
+ CarePairArgumentCallback d_cpacb;
/** The internal theory */
std::unique_ptr<TheorySetsPrivate> d_internal;
/** Instance of the above class */
SolverState& state,
InferenceManager& im,
SkolemCache& skc,
- ProofNodeManager* pnm)
+ ProofNodeManager* pnm,
+ CarePairArgumentCallback& cpacb)
: EnvObj(env),
d_deq(context()),
d_termProcessed(userContext()),
d_rels(new TheorySetsRels(d_env, state, im, skc, d_treg)),
d_cardSolver(new CardinalityExtension(d_env, state, im, d_treg)),
d_rels_enabled(false),
- d_card_enabled(false)
+ d_card_enabled(false),
+ d_cpacb(cpacb)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
}
-bool TheorySetsPrivate::areCareDisequal(Node a, Node b)
-{
- if (d_equalityEngine->isTriggerTerm(a, THEORY_SETS)
- && d_equalityEngine->isTriggerTerm(b, THEORY_SETS))
- {
- TNode a_shared =
- d_equalityEngine->getTriggerTermRepresentative(a, THEORY_SETS);
- TNode b_shared =
- d_equalityEngine->getTriggerTermRepresentative(b, THEORY_SETS);
- EqualityStatus eqStatus =
- d_external.d_valuation.getEqualityStatus(a_shared, b_shared);
- if (eqStatus == EQUALITY_FALSE_AND_PROPAGATED || eqStatus == EQUALITY_FALSE
- || eqStatus == EQUALITY_FALSE_IN_MODEL)
- {
- return true;
- }
- }
- return false;
-}
-
void TheorySetsPrivate::fullEffortReset()
{
Assert(d_equalityEngine->consistent());
}
//--------------------------------- end standard check
-/************************ Sharing ************************/
-/************************ Sharing ************************/
-/************************ Sharing ************************/
-
-void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
- TNodeTrie* t2,
- unsigned arity,
- unsigned depth,
- unsigned& n_pairs)
-{
- if (depth == arity)
- {
- if (t2 != NULL)
- {
- Node f1 = t1->getData();
- Node f2 = t2->getData();
-
- // Usually when (= (f x) (f y)), we don't care whether (= x y) is true or
- // not for the shared variables x, y in the care graph.
- // However, this does not apply to the membership operator since the
- // equality or disequality between members affects the number of elements
- // in a set. Therefore we need to split on (= x y) for kind SET_MEMBER.
- // Example:
- // Suppose (= (member x S) member( y, S)) is true and there are
- // no other members in S. We would get S = {x} if (= x y) is true.
- // Otherwise we would get S = {x, y}.
- if (f1.getKind() == SET_MEMBER || !d_state.areEqual(f1, f2))
- {
- Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
- vector<pair<TNode, TNode> > currentPairs;
- for (unsigned k = 0; k < f1.getNumChildren(); ++k)
- {
- TNode x = f1[k];
- TNode y = f2[k];
- Assert(d_equalityEngine->hasTerm(x));
- Assert(d_equalityEngine->hasTerm(y));
- Assert(!d_state.areDisequal(x, y));
- Assert(!areCareDisequal(x, y));
- if (!d_equalityEngine->areEqual(x, y))
- {
- Trace("sets-cg")
- << "Arg #" << k << " is " << x << " " << y << std::endl;
- if (d_equalityEngine->isTriggerTerm(x, THEORY_SETS)
- && d_equalityEngine->isTriggerTerm(y, THEORY_SETS))
- {
- TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
- x, THEORY_SETS);
- TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
- y, THEORY_SETS);
- currentPairs.push_back(make_pair(x_shared, y_shared));
- }
- else if (isCareArg(f1, k) && isCareArg(f2, k))
- {
- // splitting on sets (necessary for handling set of sets properly)
- if (x.getType().isSet())
- {
- Assert(y.getType().isSet());
- if (!d_state.areDisequal(x, y))
- {
- Trace("sets-cg-lemma")
- << "Should split on : " << x << "==" << y << std::endl;
- d_im.split(x.eqNode(y), InferenceId::SETS_CG_SPLIT);
- }
- }
- }
- }
- }
- for (unsigned c = 0; c < currentPairs.size(); ++c)
- {
- Trace("sets-cg-pair") << "Pair : " << currentPairs[c].first << " "
- << currentPairs[c].second << std::endl;
- d_external.addCarePair(currentPairs[c].first, currentPairs[c].second);
- n_pairs++;
- }
- }
- }
- }
- else
- {
- if (t2 == NULL)
- {
- if (depth < (arity - 1))
- {
- // add care pairs internal to each child
- for (std::pair<const TNode, TNodeTrie>& t : t1->d_data)
- {
- addCarePairs(&t.second, NULL, arity, depth + 1, n_pairs);
- }
- }
- // add care pairs based on each pair of non-disequal arguments
- for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
- it != t1->d_data.end();
- ++it)
- {
- std::map<TNode, TNodeTrie>::iterator it2 = it;
- ++it2;
- for (; it2 != t1->d_data.end(); ++it2)
- {
- if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
- {
- if (!areCareDisequal(it->first, it2->first))
- {
- addCarePairs(
- &it->second, &it2->second, arity, depth + 1, n_pairs);
- }
- }
- }
- }
- }
- else
- {
- // add care pairs based on product of indices, non-disequal arguments
- for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
- {
- for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
- {
- if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
- {
- if (!areCareDisequal(tt1.first, tt2.first))
- {
- addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
- }
- }
- }
- }
- }
- }
-}
-
void TheorySetsPrivate::computeCareGraph()
{
const std::map<Kind, std::vector<Node> >& ol = d_state.getOperatorList();
{
Trace("sets-cg") << "Process index " << tt.first << "..."
<< std::endl;
- addCarePairs(&tt.second, nullptr, arity, 0, n_pairs);
+ nodeTriePathPairProcess(&tt.second, arity, d_cpacb);
}
}
Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
{
return true;
}
- else
- {
- return false;
- }
+ return false;
}
/******************** Model generation ********************/
return d_state.isEntailed(n, pol);
}
+void TheorySetsPrivate::processCarePairArgs(TNode a, TNode b)
+{
+ for (size_t k = 0, nchild = a.getNumChildren(); k < nchild; ++k)
+ {
+ TNode x = a[k];
+ TNode y = b[k];
+ if (!d_equalityEngine->areEqual(x, y))
+ {
+ if (isCareArg(a, k) && isCareArg(b, k))
+ {
+ // splitting on sets (necessary for handling set of sets properly)
+ if (x.getType().isSet())
+ {
+ Assert(y.getType().isSet());
+ Trace("sets-cg-lemma")
+ << "Should split on : " << x << "==" << y << std::endl;
+ d_im.split(x.eqNode(y), InferenceId::SETS_CG_SPLIT);
+ }
+ }
+ }
+ }
+}
+
Node TheorySetsPrivate::explain(TNode literal)
{
Trace("sets") << "TheorySetsPrivate::explain(" << literal << ")" << std::endl;
#include "context/cdqueue.h"
#include "expr/node_trie.h"
#include "smt/env_obj.h"
+#include "theory/care_pair_argument_callback.h"
#include "theory/sets/cardinality_extension.h"
#include "theory/sets/inference_manager.h"
#include "theory/sets/solver_state.h"
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
private:
- /** Are a and b trigger terms in the equality engine that may be disequal? */
- bool areCareDisequal(Node a, Node b);
/**
* Invoke the decision procedure for this theory, which is run at
* full effort. This will either send a lemma or conflict on the output
*/
void checkReduceComprehensions();
- void addCarePairs(TNodeTrie* t1,
- TNodeTrie* t2,
- unsigned arity,
- unsigned depth,
- unsigned& n_pairs);
-
Node d_true;
Node d_false;
Node d_zero;
SolverState& state,
InferenceManager& im,
SkolemCache& skc,
- ProofNodeManager* pnm);
+ ProofNodeManager* pnm,
+ CarePairArgumentCallback& cpacb);
~TheorySetsPrivate();
/** Is formula n entailed to have polarity pol in the current context? */
bool isEntailed(Node n, bool pol);
+ /**
+ * Adds inferences for splitting on arguments of a and b that are not
+ * equal nor disequal and are sets.
+ */
+ void processCarePairArgs(TNode a, TNode b);
+
private:
TheorySets& d_external;
/** The state of the sets solver at full effort */
/** a map that maps each set to an existential quantifier generated for
* operator is_singleton */
std::map<Node, Node> d_isSingletonNodes;
+ /** Reference to care pair argument callback, used for theory combination */
+ CarePairArgumentCallback& d_cpacb;
}; /* class TheorySetsPrivate */
} // namespace sets
d_regexp_elim(options().strings.regExpElimAgg, d_pnm, userContext()),
d_stringsFmf(env, valuation, d_termReg),
d_strat(d_env),
- d_absModelCounter(0)
+ d_absModelCounter(0),
+ d_cpacb(*this)
{
d_termReg.finishInit(&d_im);
return std::string("TheoryStrings");
}
-bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
- Assert(d_equalityEngine->hasTerm(x));
- Assert(d_equalityEngine->hasTerm(y));
- if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS)
- && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS))
- {
- TNode x_shared =
- d_equalityEngine->getTriggerTermRepresentative(x, THEORY_STRINGS);
- TNode y_shared =
- d_equalityEngine->getTriggerTermRepresentative(y, THEORY_STRINGS);
- EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
- if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
- return true;
- }
- }
- return false;
-}
-
bool TheoryStrings::propagateLit(TNode literal)
{
return d_im.propagateLit(literal);
}
}
-void TheoryStrings::addCarePairs(TNodeTrie* t1,
- TNodeTrie* t2,
- unsigned arity,
- unsigned depth)
-{
- if( depth==arity ){
- if( t2!=NULL ){
- Node f1 = t1->getData();
- Node f2 = t2->getData();
- if (!d_equalityEngine->areEqual(f1, f2))
- {
- Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
- vector< pair<TNode, TNode> > currentPairs;
- for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
- TNode x = f1[k];
- TNode y = f2[k];
- Assert(d_equalityEngine->hasTerm(x));
- Assert(d_equalityEngine->hasTerm(y));
- Assert(!d_equalityEngine->areDisequal(x, y, false));
- Assert(!areCareDisequal(x, y));
- if (!d_equalityEngine->areEqual(x, y))
- {
- if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS)
- && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS))
- {
- TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
- x, THEORY_STRINGS);
- TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
- y, THEORY_STRINGS);
- currentPairs.push_back(make_pair(x_shared, y_shared));
- }
- }
- }
- for (unsigned c = 0; c < currentPairs.size(); ++ c) {
- Trace("strings-cg-pair") << "TheoryStrings::computeCareGraph(): pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
- addCarePair(currentPairs[c].first, currentPairs[c].second);
- }
- }
- }
- }else{
- if( t2==NULL ){
- if( depth<(arity-1) ){
- //add care pairs internal to each child
- for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
- {
- addCarePairs(&tt.second, nullptr, arity, depth + 1);
- }
- }
- //add care pairs based on each pair of non-disequal arguments
- for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
- it != t1->d_data.end();
- ++it)
- {
- std::map<TNode, TNodeTrie>::iterator it2 = it;
- ++it2;
- for( ; it2 != t1->d_data.end(); ++it2 ){
- if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
- {
- if( !areCareDisequal(it->first, it2->first) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1 );
- }
- }
- }
- }
- }else{
- //add care pairs based on product of indices, non-disequal arguments
- for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
- {
- for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
- {
- if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
- {
- if (!areCareDisequal(tt1.first, tt2.first))
- {
- addCarePairs(&tt1.second, &tt2.second, arity, depth + 1);
- }
- }
- }
- }
- }
- }
-}
-
void TheoryStrings::computeCareGraph(){
//computing the care graph here is probably still necessary, due to operators that take non-string arguments TODO: verify
Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl;
Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index "
<< ti.first << "..." << std::endl;
Node op = ti.first.second;
- addCarePairs(&ti.second, nullptr, arity[op], 0);
+ nodeTriePathPairProcess(&ti.second, arity[op], d_cpacb);
}
}
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "expr/node_trie.h"
+#include "theory/care_pair_argument_callback.h"
#include "theory/ext_theory.h"
#include "theory/strings/array_solver.h"
#include "theory/strings/base_solver.h"
};/* class TheoryStrings::NotifyClass */
/** compute care graph */
void computeCareGraph() override;
- /**
- * Are x and y shared terms that are not equal? This is used for constructing
- * the care graph in the above function.
- */
- bool areCareDisequal(TNode x, TNode y);
- /** Add care pairs */
- void addCarePairs(TNodeTrie* t1,
- TNodeTrie* t2,
- unsigned arity,
- unsigned depth);
/** Collect model info for type tn
*
* Assigns model values (in m) to all relevant terms of the string-like type
* we have built, so that unique debug names can be assigned.
*/
size_t d_absModelCounter;
+ /** The care pair argument callback, used for theory combination */
+ CarePairArgumentCallback d_cpacb;
};/* class TheoryStrings */
} // namespace strings
}
void Theory::addCarePair(TNode t1, TNode t2) {
- if (d_careGraph) {
- d_careGraph->insert(CarePair(t1, t2, d_id));
+ Assert(d_careGraph != nullptr);
+ Trace("sharing") << "Theory::addCarePair: add pair " << d_id << " " << t1
+ << " " << t2 << std::endl;
+ d_careGraph->insert(CarePair(t1, t2, d_id));
+}
+void Theory::addCarePairArgs(TNode a, TNode b)
+{
+ Assert(d_careGraph != nullptr);
+ Assert(d_equalityEngine != nullptr);
+ Assert(a.hasOperator() && b.hasOperator());
+ Assert(a.getOperator() == b.getOperator());
+ Assert(a.getNumChildren() == b.getNumChildren());
+ Trace("sharing") << "Theory::addCarePairArgs: checking function " << d_id
+ << " " << a << " " << b << std::endl;
+ for (size_t k = 0, nchildren = a.getNumChildren(); k < nchildren; ++k)
+ {
+ TNode x = a[k];
+ TNode y = b[k];
+ if (d_equalityEngine->isTriggerTerm(x, d_id)
+ && d_equalityEngine->isTriggerTerm(y, d_id)
+ && !d_equalityEngine->areEqual(x, y))
+ {
+ TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(x, d_id);
+ TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(y, d_id);
+ addCarePair(x_shared, y_shared);
+ }
+ }
+}
+
+void Theory::processCarePairArgs(TNode a, TNode b)
+{
+ // if a and b are already equal, we ignore this pair
+ if (d_theoryState->areEqual(a, b))
+ {
+ return;
+ }
+ // otherwise, we add pairs for each of their arguments
+ addCarePairArgs(a, b);
+}
+
+bool Theory::areCareDisequal(TNode x, TNode y)
+{
+ Assert(d_equalityEngine != nullptr);
+ Assert(d_equalityEngine->hasTerm(x));
+ Assert(d_equalityEngine->hasTerm(y));
+ if (!d_equalityEngine->isTriggerTerm(x, d_id)
+ || !d_equalityEngine->isTriggerTerm(y, d_id))
+ {
+ return false;
}
+ TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(x, d_id);
+ TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(y, d_id);
+ EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
+ return eqStatus == EQUALITY_FALSE_AND_PROPAGATED || eqStatus == EQUALITY_FALSE
+ || eqStatus == EQUALITY_FALSE_IN_MODEL;
}
void Theory::getCareGraph(CareGraph* careGraph) {
- Assert(careGraph != NULL);
+ Assert(careGraph != nullptr);
Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
d_careGraph = careGraph;
computeCareGraph();
- d_careGraph = NULL;
+ d_careGraph = nullptr;
}
bool Theory::proofsEnabled() const
namespace theory {
+class CarePairArgumentCallback;
class DecisionManager;
struct EeSetupInfo;
class OutputChannel;
*/
class Theory : protected EnvObj
{
+ friend class CarePairArgumentCallback;
friend class ::cvc5::TheoryEngine;
protected:
/** time spent in theory combination */
TimerStat d_computeCareGraphTime;
+ /** Add (t1, t2) to the care graph */
+ void addCarePair(TNode t1, TNode t2);
/**
- * The only method to add suff to the care graph.
+ * Assuming a is f(a1, ..., an) and b is f(b1, ..., bn), this method adds
+ * (ai, bi) to the care graph for each i where ai is not equal to bi.
*/
- void addCarePair(TNode t1, TNode t2);
+ void addCarePairArgs(TNode a, TNode b);
+ /**
+ * Process care pair arguments for a and b. By default, this calls the
+ * method above if a and b are not equal according to the equality engine
+ * of this theory.
+ */
+ virtual void processCarePairArgs(TNode a, TNode b);
+ /**
+ * Are care disequal? Return true if x and y are shared terms that are
+ * disequal according to the valuation.
+ */
+ virtual bool areCareDisequal(TNode x, TNode y);
/**
* The function should compute the care graph over the shared terms.
d_rewriter(logicInfo().isHigherOrder()),
d_state(env, valuation),
d_im(env, *this, d_state, "theory::uf::" + instanceName, false),
- d_notify(d_im, *this)
+ d_notify(d_im, *this),
+ d_cpacb(*this)
{
d_true = NodeManager::currentNM()->mkConst( true );
// indicate we are using the default theory state and inference managers
}
}
-static Node mkAnd(const std::vector<TNode>& conjunctions) {
- Assert(conjunctions.size() > 0);
-
- std::set<TNode> all;
- all.insert(conjunctions.begin(), conjunctions.end());
-
- if (all.size() == 1) {
- // All the same, or just one
- return conjunctions[0];
- }
-
- NodeBuilder conjunction(kind::AND);
- std::set<TNode>::const_iterator it = all.begin();
- std::set<TNode>::const_iterator it_end = all.end();
- while (it != it_end) {
- conjunction << *it;
- ++ it;
- }
-
- return conjunction;
-}/* mkAnd() */
-
//--------------------------------- standard check
bool TheoryUF::needsCheckLastEffort()
{
d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr);
}
- exp = mkAnd(assumptions);
+ exp = NodeManager::currentNM()->mkAnd(assumptions);
}
TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); }
return false;
}
-void TheoryUF::addCarePairs(const TNodeTrie* t1,
- const TNodeTrie* t2,
- unsigned arity,
- unsigned depth)
+void TheoryUF::processCarePairArgs(TNode a, TNode b)
{
- // Note we use d_state instead of d_equalityEngine in this method in several
- // places to be robust to cases where the tries have terms that do not
- // exist in the equality engine, which can be the case if higher order.
- if( depth==arity ){
- if( t2!=NULL ){
- Node f1 = t1->getData();
- Node f2 = t2->getData();
- if (!d_state.areEqual(f1, f2))
- {
- Trace("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
- vector< pair<TNode, TNode> > currentPairs;
- for (size_t k = 0, nchildren = f1.getNumChildren(); k < nchildren; ++k)
- {
- TNode x = f1[k];
- TNode y = f2[k];
- Assert(!d_state.areDisequal(x, y));
- Assert(!areCareDisequal(x, y));
- if (!d_state.areEqual(x, y))
- {
- if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
- && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
- {
- TNode x_shared =
- d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF);
- TNode y_shared =
- d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF);
- currentPairs.push_back(make_pair(x_shared, y_shared));
- }
- }
- }
- for (unsigned c = 0; c < currentPairs.size(); ++ c) {
- Trace("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl;
- addCarePair(currentPairs[c].first, currentPairs[c].second);
- }
- }
- }
- }else{
- if( t2==NULL ){
- if( depth<(arity-1) ){
- //add care pairs internal to each child
- for (const std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
- {
- addCarePairs(&tt.second, NULL, arity, depth + 1);
- }
- }
- //add care pairs based on each pair of non-disequal arguments
- for (std::map<TNode, TNodeTrie>::const_iterator it = t1->d_data.begin();
- it != t1->d_data.end();
- ++it)
- {
- std::map<TNode, TNodeTrie>::const_iterator it2 = it;
- ++it2;
- for( ; it2 != t1->d_data.end(); ++it2 ){
- if (!d_state.areDisequal(it->first, it2->first))
- {
- if( !areCareDisequal(it->first, it2->first) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1 );
- }
- }
- }
- }
- }else{
- //add care pairs based on product of indices, non-disequal arguments
- for (const std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
- {
- for (const std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
- {
- if (!d_state.areDisequal(tt1.first, tt2.first))
- {
- if (!areCareDisequal(tt1.first, tt2.first))
- {
- addCarePairs(&tt1.second, &tt2.second, arity, depth + 1);
- }
- }
- }
- }
- }
+ // if a and b are already equal, we ignore this pair
+ if (d_state.areEqual(a, b))
+ {
+ return;
}
+ // otherwise, we add pairs for each of their arguments
+ addCarePairArgs(a, b);
}
void TheoryUF::computeCareGraph() {
Trace("uf::sharing") << "TheoryUf::computeCareGraph(): Process index "
<< tt.first << "..." << std::endl;
Assert(arity.find(tt.first) != arity.end());
- addCarePairs(&tt.second, nullptr, arity[tt.first], 0);
+ nodeTriePathPairProcess(&tt.second, arity[tt.first], d_cpacb);
}
for (std::pair<const TypeNode, TNodeTrie>& tt : hoIndex)
{
Trace("uf::sharing") << "TheoryUf::computeCareGraph(): Process ho index "
<< tt.first << "..." << std::endl;
// the arity of HO_APPLY is always two
- addCarePairs(&tt.second, nullptr, 2, 0);
+ nodeTriePathPairProcess(&tt.second, 2, d_cpacb);
}
Trace("uf::sharing") << "TheoryUf::computeCareGraph(): finished."
<< std::endl;
#define CVC5__THEORY__UF__THEORY_UF_H
#include "expr/node.h"
-#include "expr/node_trie.h"
+#include "theory/care_pair_argument_callback.h"
#include "theory/theory.h"
#include "theory/theory_eq_notify.h"
#include "theory/theory_state.h"
/** Explain why this literal is true by building an explanation */
void explain(TNode literal, Node& exp);
- bool areCareDisequal(TNode x, TNode y);
- void addCarePairs(const TNodeTrie* t1,
- const TNodeTrie* t2,
- unsigned arity,
- unsigned depth);
+ /** Overrides to ensure that pairs of lambdas are not considered disequal. */
+ bool areCareDisequal(TNode x, TNode y) override;
+ /**
+ * Overrides to use the theory state instead of the equality engine, since
+ * for higher-order, some terms that do not occur in the equality engine are
+ * considered.
+ */
+ void processCarePairArgs(TNode a, TNode b) override;
/**
* Is t a higher order type? A higher-order type is a function type having
* an argument type that is also a function type. This is used for checking
NotifyClass d_notify;
/** Cache for isHigherOrderType */
std::map<TypeNode, bool> d_isHoType;
+ /** The care pair argument callback, used for theory combination */
+ CarePairArgumentCallback d_cpacb;
};/* class TheoryUF */
} // namespace uf
projects / cvc5.git / commitdiff