summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/quantifiers/ematching/trigger_term_info.cpp2
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.cpp2
-rw-r--r--src/theory/quantifiers/term_database.cpp2
-rw-r--r--src/theory/quantifiers/term_util.cpp8
-rw-r--r--src/theory/sep/theory_sep.cpp20
-rw-r--r--src/theory/sets/cardinality_extension.cpp18
-rw-r--r--src/theory/sets/kinds4
-rw-r--r--src/theory/sets/solver_state.cpp2
-rw-r--r--src/theory/sets/term_registry.cpp2
-rw-r--r--src/theory/sets/theory_sets.cpp2
-rw-r--r--src/theory/sets/theory_sets_private.cpp4
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp10
-rw-r--r--src/theory/sets/theory_sets_type_rules.cpp4
13 files changed, 39 insertions, 41 deletions
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp
index 75a353dbe..24efc60c3 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.cpp
+++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp
@@ -54,7 +54,7 @@ bool TriggerTermInfo::isAtomicTriggerKind(Kind k)
// where these two things require those kinds respectively.
return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR
|| k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL
- || k == APPLY_TESTER || k == SET_UNION || k == SET_INTERSECTION
+ || k == APPLY_TESTER || k == SET_UNION || k == SET_INTER
|| k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER
|| k == SET_SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT
|| k == INT_TO_BITVECTOR || k == HO_APPLY || k == STRING_LENGTH
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 034f5f23c..99170427e 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -990,7 +990,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
sdts[i].addConstructor(lambda, "singleton", cargsSingleton);
// add for union, difference, intersection
- std::vector<Kind> bin_kinds = {SET_UNION, SET_INTERSECTION, SET_MINUS};
+ std::vector<Kind> bin_kinds = {SET_UNION, SET_INTER, SET_MINUS};
std::vector<TypeNode> cargsBinary;
cargsBinary.push_back(unres_t);
cargsBinary.push_back(unres_t);
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5c9e91d32..0408d27da 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -186,7 +186,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
Node TermDb::getMatchOperator( Node n ) {
Kind k = n.getKind();
//datatype operators may be parametric, always assume they are
- if (k == SELECT || k == STORE || k == SET_UNION || k == SET_INTERSECTION
+ if (k == SELECT || k == STORE || k == SET_UNION || k == SET_INTER
|| k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER
|| k == SET_SINGLETON || k == APPLY_SELECTOR_TOTAL || k == APPLY_SELECTOR
|| k == APPLY_TESTER || k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index de4c56552..704951f52 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -283,7 +283,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry)
{
if (reqNAry)
{
- if (k == SET_UNION || k == SET_INTERSECTION)
+ if (k == SET_UNION || k == SET_INTER)
{
return false;
}
@@ -292,7 +292,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry)
|| k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT
|| k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
|| k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT
- || k == SET_UNION || k == SET_INTERSECTION || k == RELATION_JOIN
+ || k == SET_UNION || k == SET_INTER || k == RELATION_JOIN
|| k == RELATION_PRODUCT || k == SEP_STAR;
}
@@ -300,7 +300,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry)
{
if (reqNAry)
{
- if (k == SET_UNION || k == SET_INTERSECTION)
+ if (k == SET_UNION || k == SET_INTER)
{
return false;
}
@@ -308,7 +308,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry)
return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND
|| k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT
|| k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
- || k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTERSECTION
+ || k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTER
|| k == SEP_STAR;
}
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 218c09804..3ee4fa012 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -385,7 +385,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
{
for (size_t j = (i + 1); j < lsize; j++)
{
- Node s = nm->mkNode(SET_INTERSECTION, labels[i], labels[j]);
+ Node s = nm->mkNode(SET_INTER, labels[i], labels[j]);
Node ilem = s.eqNode(empSet);
Trace("sep-lemma-debug")
<< "Sep::Lemma : star reduction, disjoint : " << ilem
@@ -401,7 +401,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
Trace("sep-lemma-debug")
<< "Sep::Lemma : wand reduction, union : " << ulem << std::endl;
c_lems.push_back(ulem);
- Node s = nm->mkNode(SET_INTERSECTION, slbl, labels[0]);
+ Node s = nm->mkNode(SET_INTER, slbl, labels[0]);
Node ilem = s.eqNode(empSet);
Trace("sep-lemma-debug")
<< "Sep::Lemma : wand reduction, disjoint : " << ilem << std::endl;
@@ -1427,10 +1427,9 @@ Node TheorySep::instantiateLabel(Node n,
Node sub_lbl = itl->second;
Node lbl_mval = d_label_model[sub_lbl].getValue( rtn );
for( unsigned j=0; j<vs.size(); j++ ){
- bchildren.push_back(
- NodeManager::currentNM()
- ->mkNode(kind::SET_INTERSECTION, lbl_mval, vs[j])
- .eqNode(empSet));
+ bchildren.push_back(NodeManager::currentNM()
+ ->mkNode(kind::SET_INTER, lbl_mval, vs[j])
+ .eqNode(empSet));
}
vs.push_back( lbl_mval );
if( vsu.isNull() ){
@@ -1476,11 +1475,10 @@ Node TheorySep::instantiateLabel(Node n,
//disjoint constraints
Node sub_lbl_0 = d_label_map[n][lbl][0];
Node lbl_mval_0 = d_label_model[sub_lbl_0].getValue( rtn );
- wchildren.push_back(
- NodeManager::currentNM()
- ->mkNode(kind::SET_INTERSECTION, lbl_mval_0, lbl)
- .eqNode(empSet)
- .negate());
+ wchildren.push_back(NodeManager::currentNM()
+ ->mkNode(kind::SET_INTER, lbl_mval_0, lbl)
+ .eqNode(empSet)
+ .negate());
//return the lemma
wchildren.push_back( children[0].negate() );
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index f65c41b53..c35eaf49a 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -242,7 +242,7 @@ void CardinalityExtension::checkRegister()
// if setminus, do for intersection instead
if (n.getKind() == SET_MINUS)
{
- n = rewrite(nm->mkNode(SET_INTERSECTION, n[0], n[1]));
+ n = rewrite(nm->mkNode(SET_INTER, n[0], n[1]));
}
registerCardinalityTerm(n);
}
@@ -268,7 +268,7 @@ void CardinalityExtension::registerCardinalityTerm(Node n)
NodeManager* nm = NodeManager::currentNM();
Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
std::vector<Node> cterms;
- if (n.getKind() == SET_INTERSECTION)
+ if (n.getKind() == SET_INTER)
{
for (unsigned e = 0; e < 2; e++)
{
@@ -381,7 +381,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
for (const Node& n : nvsets)
{
Kind nk = n.getKind();
- if (nk != SET_INTERSECTION && nk != SET_MINUS)
+ if (nk != SET_INTER && nk != SET_MINUS)
{
continue;
}
@@ -389,7 +389,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
<< std::endl;
std::vector<Node> sib;
unsigned true_sib = 0;
- if (n.getKind() == SET_INTERSECTION)
+ if (n.getKind() == SET_INTER)
{
d_localBase[n] = n;
for (unsigned e = 0; e < 2; e++)
@@ -401,7 +401,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
}
else
{
- Node si = rewrite(nm->mkNode(SET_INTERSECTION, n[0], n[1]));
+ Node si = rewrite(nm->mkNode(SET_INTER, n[0], n[1]));
sib.push_back(si);
d_localBase[n] = si;
Node osm = rewrite(nm->mkNode(SET_MINUS, n[1], n[0]));
@@ -490,7 +490,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
<< "Sibling " << sib[si] << " is already empty." << std::endl;
}
}
- if (!is_union && nk == SET_INTERSECTION && !u.isNull())
+ if (!is_union && nk == SET_INTER && !u.isNull())
{
// union is equal to other parent
if (!d_state.areEqual(u, n[1 - e]))
@@ -578,7 +578,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
<< " are equal, ids = " << card_parent_ids[l]
<< " " << card_parent_ids[k] << std::endl;
dup = true;
- if (n.getKind() != SET_INTERSECTION)
+ if (n.getKind() != SET_INTER)
{
continue;
}
@@ -817,7 +817,7 @@ void CardinalityExtension::checkNormalForm(Node eqc,
Node r1 = e == 0 ? o0 : o1;
Node r2 = e == 0 ? o1 : o0;
// check if their intersection exists modulo equality
- Node r1r2i = d_state.getBinaryOpTerm(SET_INTERSECTION, r1, r2);
+ Node r1r2i = d_state.getBinaryOpTerm(SET_INTER, r1, r2);
if (!r1r2i.isNull())
{
Trace("sets-nf-debug")
@@ -838,7 +838,7 @@ void CardinalityExtension::checkNormalForm(Node eqc,
Assert(o0 != o1);
Node kca = d_treg.getProxy(o0);
Node kcb = d_treg.getProxy(o1);
- Node intro = rewrite(nm->mkNode(SET_INTERSECTION, kca, kcb));
+ Node intro = rewrite(nm->mkNode(SET_INTER, kca, kcb));
Trace("sets-nf") << " Intro split : " << o0 << " against " << o1
<< ", term is " << intro << std::endl;
intro_sets.push_back(intro);
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index f5ed7cd87..71d5fce4a 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -37,7 +37,7 @@ enumerator SET_TYPE \
# operators
operator SET_UNION 2 "set union"
-operator SET_INTERSECTION 2 "set intersection"
+operator SET_INTER 2 "set intersection"
operator SET_MINUS 2 "set subtraction"
operator SET_SUBSET 2 "subset predicate; first parameter a subset of second"
operator SET_MEMBER 2 "set membership predicate; first parameter a member of second"
@@ -88,7 +88,7 @@ operator RELATION_JOIN_IMAGE 2 "relation join image"
operator RELATION_IDEN 1 "relation identity"
typerule SET_UNION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
-typerule SET_INTERSECTION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
+typerule SET_INTER ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
typerule SET_MINUS ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
typerule SET_SUBSET ::cvc5::theory::sets::SubsetTypeRule
typerule SET_MEMBER ::cvc5::theory::sets::MemberTypeRule
diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 023a8a6af..3f619dcad 100644
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -90,7 +90,7 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
}
}
}
- else if (nk == SET_SINGLETON || nk == SET_UNION || nk == SET_INTERSECTION
+ else if (nk == SET_SINGLETON || nk == SET_UNION || nk == SET_INTER
|| nk == SET_MINUS || nk == SET_EMPTY || nk == SET_UNIVERSE)
{
if (nk == SET_SINGLETON)
diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp
index 41fe0b4c8..d4b5aa824 100644
--- a/src/theory/sets/term_registry.cpp
+++ b/src/theory/sets/term_registry.cpp
@@ -44,7 +44,7 @@ TermRegistry::TermRegistry(Env& env,
Node TermRegistry::getProxy(Node n)
{
Kind nk = n.getKind();
- if (nk != SET_EMPTY && nk != SET_SINGLETON && nk != SET_INTERSECTION
+ if (nk != SET_EMPTY && nk != SET_SINGLETON && nk != SET_INTER
&& nk != SET_MINUS && nk != SET_UNION && nk != SET_UNIVERSE)
{
return n;
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index b2eb80f75..c3d0b9bbe 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -76,7 +76,7 @@ void TheorySets::finishInit()
// functions we are doing congruence over
d_equalityEngine->addFunctionKind(SET_SINGLETON);
d_equalityEngine->addFunctionKind(SET_UNION);
- d_equalityEngine->addFunctionKind(SET_INTERSECTION);
+ d_equalityEngine->addFunctionKind(SET_INTER);
d_equalityEngine->addFunctionKind(SET_MINUS);
d_equalityEngine->addFunctionKind(SET_MEMBER);
d_equalityEngine->addFunctionKind(SET_SUBSET);
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 7b596be86..50ff3f09c 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -523,7 +523,7 @@ void TheorySetsPrivate::checkUpwardsClosure()
// see if there are members in second argument
const std::map<Node, Node>& r2mem = d_state.getMembers(r2);
const std::map<Node, Node>& r2nmem = d_state.getNegativeMembers(r2);
- if (!r2mem.empty() || k != kind::SET_INTERSECTION)
+ if (!r2mem.empty() || k != kind::SET_INTER)
{
Trace("sets-debug")
<< "Checking " << term << ", members = " << (!r1mem.empty())
@@ -546,7 +546,7 @@ void TheorySetsPrivate::checkUpwardsClosure()
{
valid = true;
}
- else if (k == kind::SET_INTERSECTION)
+ else if (k == kind::SET_INTER)
{
// conclude x is in term
// if also existing in members of r2
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 181a659c5..277b6bc84 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -81,7 +81,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
nm->mkNode(kind::EQUAL, node[0], node[1][0]));
}
else if (node[1].getKind() == kind::SET_UNION
- || node[1].getKind() == kind::SET_INTERSECTION
+ || node[1].getKind() == kind::SET_INTER
|| node[1].getKind() == kind::SET_MINUS)
{
std::vector<Node> children;
@@ -157,7 +157,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
else if (node[1].getKind() == kind::SET_MINUS && node[1][0] == node[0])
{
// (setminus A (setminus A B)) = (intersection A B)
- Node intersection = nm->mkNode(SET_INTERSECTION, node[0], node[1][1]);
+ Node intersection = nm->mkNode(SET_INTER, node[0], node[1][1]);
return RewriteResponse(REWRITE_AGAIN, intersection);
}
else if (node[1].getKind() == kind::SET_UNIVERSE)
@@ -185,7 +185,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
break;
} // kind::SET_MINUS
- case kind::SET_INTERSECTION:
+ case kind::SET_INTER:
{
if(node[0] == node[1]) {
Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
@@ -289,7 +289,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
NodeManager::currentNM()->mkNode(
kind::SET_CARD,
NodeManager::currentNM()->mkNode(
- kind::SET_INTERSECTION, node[0][0], node[0][1])));
+ kind::SET_INTER, node[0][0], node[0][1])));
return RewriteResponse(REWRITE_DONE, ret );
}
else if (node[0].getKind() == kind::SET_MINUS)
@@ -300,7 +300,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
NodeManager::currentNM()->mkNode(
kind::SET_CARD,
NodeManager::currentNM()->mkNode(
- kind::SET_INTERSECTION, node[0][0], node[0][1])));
+ kind::SET_INTER, node[0][0], node[0][1])));
return RewriteResponse(REWRITE_DONE, ret );
}
break;
diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp
index 0793f011b..6602e7d03 100644
--- a/src/theory/sets/theory_sets_type_rules.cpp
+++ b/src/theory/sets/theory_sets_type_rules.cpp
@@ -30,7 +30,7 @@ TypeNode SetsBinaryOperatorTypeRule::computeType(NodeManager* nodeManager,
TNode n,
bool check)
{
- Assert(n.getKind() == kind::SET_UNION || n.getKind() == kind::SET_INTERSECTION
+ Assert(n.getKind() == kind::SET_UNION || n.getKind() == kind::SET_INTER
|| n.getKind() == kind::SET_MINUS);
TypeNode setType = n[0].getType(check);
if (check)
@@ -57,7 +57,7 @@ bool SetsBinaryOperatorTypeRule::computeIsConst(NodeManager* nodeManager,
TNode n)
{
// only SET_UNION has a const rule in kinds.
- // SET_INTERSECTION and SET_MINUS are not used in the canonical representation
+ // SET_INTER and SET_MINUS are not used in the canonical representation
// of sets and therefore they do not have const rules in kinds
Assert(n.getKind() == kind::SET_UNION);
return NormalForm::checkNormalConstant(n);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback