From: ajreynol Date: Tue, 7 Mar 2017 17:17:34 +0000 (-0600) Subject: More fixes for printing/parsing sets, fix kind name. X-Git-Tag: cvc5-1.0.0~5897 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ab68adfc44049598ee79a3c8b4379694d786d9aa;p=cvc5.git More fixes for printing/parsing sets, fix kind name. --- 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 */ diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 629e8a8a0..06bd6cbf1 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -76,7 +76,8 @@ TESTS = \ abt-te-exh.smt2 \ abt-te-exh2.smt2 \ univset-simp.smt2 \ - compliment.cvc + complement.cvc \ + complement2.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/complement.cvc b/test/regress/regress0/sets/complement.cvc new file mode 100644 index 000000000..6181cbee7 --- /dev/null +++ b/test/regress/regress0/sets/complement.cvc @@ -0,0 +1,9 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +a : SET OF [Atom]; +b : SET OF [Atom]; + +ASSERT a = (NOT b); + +CHECKSAT; diff --git a/test/regress/regress0/sets/complement2.cvc b/test/regress/regress0/sets/complement2.cvc new file mode 100644 index 000000000..6802065f1 --- /dev/null +++ b/test/regress/regress0/sets/complement2.cvc @@ -0,0 +1,11 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +a : SET OF Atom; +b : SET OF Atom; +c : Atom; + +ASSERT a = NOT(a); +ASSERT c IS_IN a; + +CHECKSAT; diff --git a/test/regress/regress0/sets/compliment.cvc b/test/regress/regress0/sets/compliment.cvc deleted file mode 100644 index 6181cbee7..000000000 --- a/test/regress/regress0/sets/compliment.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -Atom: TYPE; -a : SET OF [Atom]; -b : SET OF [Atom]; - -ASSERT a = (NOT b); - -CHECKSAT; diff --git a/test/regress/regress0/sets/univset-simp.smt2 b/test/regress/regress0/sets/univset-simp.smt2 index 5d10e27cb..ec9750776 100644 --- a/test/regress/regress0/sets/univset-simp.smt2 +++ b/test/regress/regress0/sets/univset-simp.smt2 @@ -15,7 +15,7 @@ (assert (not (member 1 c))) (assert (member 2 d)) (assert (= e (as univset (Set Int)))) -(assert (= f (compliment d))) +(assert (= f (complement d))) (assert (not (member x (as univset (Set Int))))) (check-sat)