summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/parser/cvc/Cvc.g6
-rw-r--r--src/parser/smt2/smt2.cpp2
-rw-r--r--src/printer/cvc/cvc_printer.cpp4
-rw-r--r--src/printer/smt2/smt2_printer.cpp4
-rw-r--r--src/theory/quantifiers/term_database.cpp2
-rw-r--r--src/theory/quantifiers/trigger.cpp2
-rw-r--r--src/theory/sets/kinds6
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp2
-rw-r--r--src/theory/sets/theory_sets_type_rules.h10
9 files changed, 21 insertions, 17 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 267fe303e..fb0304045 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -448,7 +448,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
default: break;
}
Expr e = em->mkExpr(k, lhs, rhs);
- return negate ? em->mkExpr(e.getType().isSet() ? kind::COMPLIMENT : kind::NOT, e) : e;
+ return negate ? em->mkExpr(e.getType().isSet() ? kind::COMPLEMENT : kind::NOT, e) : e;
}/* createPrecedenceTree() recursive variant */
Expr createPrecedenceTree(Parser* parser, ExprManager* em,
@@ -474,7 +474,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
/** Add n NOTs to the front of e and return the result. */
Expr addNots(ExprManager* em, size_t n, Expr e) {
- Kind k = e.getType().isSet() ? kind::COMPLIMENT : kind::NOT;
+ Kind k = e.getType().isSet() ? kind::COMPLEMENT : kind::NOT;
while(n-- > 0) {
e = em->mkExpr(k, e);
}
@@ -1689,6 +1689,8 @@ bvNegTerm[CVC4::Expr& f]
/* BV neg */
: BVNEG_TOK bvNegTerm[f]
{ f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
+ | NOT_TOK bvNegTerm[f]
+ { f = MK_EXPR(CVC4::kind::COMPLEMENT, f); }
| TRANSPOSE_TOK bvNegTerm[f]
{ f = MK_EXPR(CVC4::kind::TRANSPOSE, f); }
| TRANSCLOSURE_TOK bvNegTerm[f]
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 88b2479ea..ebe730e29 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -236,7 +236,7 @@ void Smt2::addTheory(Theory theory) {
addOperator(kind::SINGLETON, "singleton");
addOperator(kind::INSERT, "insert");
addOperator(kind::CARD, "card");
- addOperator(kind::COMPLIMENT, "compliment");
+ addOperator(kind::COMPLEMENT, "complement");
break;
case THEORY_DATATYPES:
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index e0c434d5a..981e88a5c 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -90,6 +90,8 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
string s;
if(n.getAttribute(expr::VarNameAttr(), s)) {
out << s;
+ }else if( n.getKind() == kind::UNIVERSE_SET ){
+ out << "UNIVERSE :: " << n.getType();
} else {
if(n.getKind() == kind::VARIABLE) {
out << "var_";
@@ -780,7 +782,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
op << "IS_IN";
opType = INFIX;
break;
- case kind::COMPLIMENT:
+ case kind::COMPLEMENT:
op << "NOT";
opType = PREFIX;
break;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b3fcaf24b..2b7da63f7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -518,7 +518,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
case kind::MEMBER:
case kind::SET_TYPE:
case kind::SINGLETON:
- case kind::COMPLIMENT:out << smtKindString(k) << " "; break;
+ case kind::COMPLEMENT:out << smtKindString(k) << " "; break;
// fp theory
case kind::FLOATINGPOINT_FP:
@@ -807,7 +807,7 @@ static string smtKindString(Kind k) throw() {
case kind::SET_TYPE: return "Set";
case kind::SINGLETON: return "singleton";
case kind::INSERT: return "insert";
- case kind::COMPLIMENT: return "compliment";
+ case kind::COMPLEMENT: return "complement";
// fp theory
case kind::FLOATINGPOINT_FP: return "fp";
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 6b4b67a26..d394c8fef 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -137,7 +137,7 @@ Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) {
Node TermDb::getMatchOperator( Node n ) {
Kind k = n.getKind();
//datatype operators may be parametric, always assume they are
- if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || k==COMPLIMENT ||
+ if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ||
k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO ){
//since it is parametric, use a particular one as op
TypeNode tn = n[0].getType();
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index efd80a83c..1bfc53b41 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -353,7 +353,7 @@ bool Trigger::isAtomicTrigger( Node n ){
bool Trigger::isAtomicTriggerKind( Kind k ) {
return k==APPLY_UF || k==SELECT || k==STORE ||
k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
- k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || k==COMPLIMENT ||
+ k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ||
k==SEP_PTO || k==BITVECTOR_TO_NAT || k==INT_TO_BITVECTOR;
}
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 53905e47f..ab0ca3428 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -43,7 +43,7 @@ operator MEMBER 2 "set membership predicate; first parameter a member of
operator SINGLETON 1 "the set of the single element given as a parameter"
operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
operator CARD 1 "set cardinality operator"
-operator COMPLIMENT 1 "set compliment (with respect to finite universe)"
+operator COMPLEMENT 1 "set COMPLEMENT (with respect to finite universe)"
operator JOIN 2 "set join"
operator PRODUCT 2 "set cartesian product"
@@ -59,7 +59,7 @@ typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule
typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
typerule INSERT ::CVC4::theory::sets::InsertTypeRule
typerule CARD ::CVC4::theory::sets::CardTypeRule
-typerule COMPLIMENT ::CVC4::theory::sets::ComplimentTypeRule
+typerule COMPLEMENT ::CVC4::theory::sets::ComplementTypeRule
typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule
typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule
@@ -74,7 +74,7 @@ construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule
construle INSERT ::CVC4::theory::sets::InsertTypeRule
construle CARD ::CVC4::theory::sets::CardTypeRule
-construle COMPLIMENT ::CVC4::theory::sets::ComplimentTypeRule
+construle COMPLEMENT ::CVC4::theory::sets::ComplementTypeRule
construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule
construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index da4f8fb7a..9669561a6 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -305,7 +305,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
}
break;
}//kind::UNION
- case kind::COMPLIMENT: {
+ case kind::COMPLEMENT: {
Node univ = NodeManager::currentNM()->mkUniqueVar( node[0].getType(), kind::UNIVERSE_SET );
return RewriteResponse( REWRITE_AGAIN, NodeManager::currentNM()->mkNode( kind::SETMINUS, univ, node[0] ) );
}
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 66e06b038..11f375d5b 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -155,24 +155,24 @@ struct CardTypeRule {
}
};/* struct CardTypeRule */
-struct ComplimentTypeRule {
+struct ComplementTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw (TypeCheckingExceptionPrivate, AssertionException) {
- Assert(n.getKind() == kind::COMPLIMENT);
+ Assert(n.getKind() == kind::COMPLEMENT);
TypeNode setType = n[0].getType(check);
if( check ) {
if(!setType.isSet()) {
- throw TypeCheckingExceptionPrivate(n, "compliment operates on a set, non-set object found");
+ throw TypeCheckingExceptionPrivate(n, "COMPLEMENT operates on a set, non-set object found");
}
}
return setType;
}
inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
- Assert(n.getKind() == kind::COMPLIMENT);
+ Assert(n.getKind() == kind::COMPLEMENT);
return false;
}
-};/* struct ComplimentTypeRule */
+};/* struct ComplementTypeRule */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback