From ab2924e8a6cc34f29167b1ff50273d59dd7a6707 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Sep 2017 14:12:22 -0500 Subject: [PATCH] Remove unhandled subtypes (#1098) * Remove unhandled subtypes, which consequently makes typing rules uniformly stricter based on weakening the subtype relation. Ensure coercions in the smt2 and cvc parser for Real decimal constants whose type is Integer. Ensure type annotations are computed during preRewrite to ensure rewriting (which does not preserve types) does not impact term construction for parametric datatypes. This fixes issue #1048 (we now give an type exception). * Update unit test for parametric datatypes to reflect new subtyping relation. * Remove deprecated test. * Make array construction for lambdas work with new subtype relations to handle lambdas like (lambda ((x Int) (y Int)) (ite (= x 0) 0.5 0.0)). --- src/expr/type_node.cpp | 126 +----------------- src/parser/cvc/Cvc.g | 7 +- src/parser/smt2/Smt2.g | 7 +- .../builtin/theory_builtin_rewriter.cpp | 26 ++-- src/theory/builtin/theory_builtin_rewriter.h | 2 + src/theory/datatypes/datatypes_rewriter.h | 67 ++++++---- .../datatypes/theory_datatypes_type_rules.h | 3 + test/regress/regress0/Makefile.am | 1 + .../regress0/datatypes/tuple-no-clash.cvc | 2 +- .../regress0/issue1048-arrays-int-real.smt2 | 6 + test/regress/regress0/quantifiers/Makefile.am | 8 +- .../quantifiers/macro-subtype-param.smt2 | 8 +- .../quantifiers/subtype-param-unk.smt2 | 8 +- .../regress0/quantifiers/subtype-param.smt2 | 8 +- .../regress/regress0/sets/sets-tuple-poly.cvc | 2 +- test/unit/util/datatype_black.h | 63 ++++----- 16 files changed, 146 insertions(+), 198 deletions(-) create mode 100644 test/regress/regress0/issue1048-arrays-int-real.smt2 diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index a4ab2f3b7..c06691d08 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -106,50 +106,11 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { return false; } } - if(isTuple() && t.isTuple()) { - const Datatype& dt1 = getDatatype(); - const Datatype& dt2 = t.getDatatype(); - if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){ - return false; - } - // r1's fields must be subtypes of r2's, in order - for( unsigned i=0; irealType())) { return t.isSubtypeOf(NodeManager::currentNM()->realType()); } - if(isTuple() && t.isTuple()) { - const Datatype& dt1 = getDatatype(); - const Datatype& dt2 = t.getDatatype(); - if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){ - return false; - } - // r1's fields must be subtypes of r2's, in order - for( unsigned i=0; imkArrayType(indexType, elementType); - } else { - return TypeNode(); - } - } case kind::SEXPR_TYPE: Unimplemented("haven't implemented leastCommonType for symbolic expressions yet"); return TypeNode(); - case kind::DATATYPE_TYPE: - if( t0.isTuple() && t1.isTuple() ){ - const Datatype& dt1 = t0.getDatatype(); - const Datatype& dt2 = t1.getDatatype(); - if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){ - std::vector< TypeNode > lc_types; - for( unsigned i=0; imkTupleType( lc_types ); - } - } - //else if( t0.isRecord() && t1.isRecord() ){ - //record types are not related in current implementation - //} - // otherwise no common ancestor - return TypeNode(); - case kind::PARAMETRIC_DATATYPE: { - if(!t1.isParametricDatatype()) { - return TypeNode(); - } - if(t0[0] != t1[0] || t0.getNumChildren() != t1.getNumChildren()) { - return TypeNode(); - } - vector v; - for(size_t i = 1; i < t0.getNumChildren(); ++i) { - v.push_back(commonTypeNode(t0[i], t1[i], isLeast).toType()); - } - return TypeNode::fromType(t0[0].getDatatype().getDatatypeType(v)); - } default: Unimplemented("don't have a commonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str()); return TypeNode(); diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 6cc5c29a4..d0324cc45 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2104,7 +2104,12 @@ simpleTerm[CVC4::Expr& f] /* syntactic predicate: never match INTEGER.DIGIT as an integer and a dot! * This is a rational constant! Otherwise the parser interprets it as a tuple * selector! */ - | DECIMAL_LITERAL { f = MK_CONST(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } + | DECIMAL_LITERAL { + f = MK_CONST(AntlrInput::tokenToRational($DECIMAL_LITERAL)); + if(f.getType().isInteger()) { + f = MK_EXPR(kind::TO_REAL, f); + } + } | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } /* bitvector literals */ | HEX_LITERAL diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 86c0b3126..92f6b36d8 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2254,7 +2254,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | DECIMAL_LITERAL { // FIXME: This doesn't work because an SMT rational is not a // valid GMP rational string - expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } + expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); + if(expr.getType().isInteger()) { + //must cast to Real to ensure correct type is passed to parametric type constructors + expr = MK_EXPR(kind::TO_REAL, expr); + } + } | LPAREN_TOK INDEX_TOK ( bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 57249e181..4948216e5 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -150,7 +150,7 @@ Node TheoryBuiltinRewriter::getLambdaForArrayRepresentation( TNode a, TNode bvl } } -Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqConst ){ +Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec( TNode n, bool reqConst, TypeNode retType ){ Assert( n.getKind()==kind::LAMBDA ); Trace("builtin-rewrite-debug") << "Get array representation for : " << n << std::endl; @@ -165,7 +165,6 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo } Trace("builtin-rewrite-debug2") << " process body..." << std::endl; - TypeNode retType; std::vector< Node > conds; std::vector< Node > vals; Node curr = n[1]; @@ -214,7 +213,7 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo if( !curr_index.isNull() ){ if( !rec_bvl.isNull() ){ curr_val = NodeManager::currentNM()->mkNode( kind::LAMBDA, rec_bvl, curr_val ); - curr_val = getArrayRepresentationForLambda( curr_val, reqConst ); + curr_val = getArrayRepresentationForLambdaRec( curr_val, reqConst, retType ); if( curr_val.isNull() ){ Trace("builtin-rewrite-debug2") << " ...non-constant value." << std::endl; return Node::null(); @@ -228,18 +227,22 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo conds.push_back( curr_index ); vals.push_back( curr_val ); TypeNode vtype = curr_val.getType(); - retType = retType.isNull() ? vtype : TypeNode::leastCommonTypeNode( retType, vtype ); //recurse curr = next; } if( !rec_bvl.isNull() ){ curr = NodeManager::currentNM()->mkNode( kind::LAMBDA, rec_bvl, curr ); - curr = getArrayRepresentationForLambda( curr ); + curr = getArrayRepresentationForLambdaRec( curr, reqConst, retType ); } if( !curr.isNull() && curr.isConst() ){ - TypeNode ctype = curr.getType(); - retType = retType.isNull() ? ctype : TypeNode::leastCommonTypeNode( retType, ctype ); - TypeNode array_type = NodeManager::currentNM()->mkArrayType( first_arg.getType(), retType ); + // compute the return type + TypeNode array_type = retType; + for( unsigned i=0; imkArrayType( n[0][index].getType(), array_type ); + } + Trace("builtin-rewrite-debug2") << " make array store all " << curr.getType() << " annotated : " << array_type << std::endl; + Assert( curr.getType().isSubtypeOf( array_type.getArrayConstituentType() ) ); curr = NodeManager::currentNM()->mkConst(ArrayStoreAll(((ArrayType)array_type.toType()), curr.toExpr())); Trace("builtin-rewrite-debug2") << " build array..." << std::endl; // can only build if default value is constant (since array store all must be constant) @@ -257,6 +260,13 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo } } +Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqConst ){ + Assert( n.getKind()==kind::LAMBDA ); + // must carry the overall return type to deal with cases like (lambda ((x Int)(y Int)) (ite (= x _) 0.5 0.0)), + // where the inner construction for the else case about should be (arraystoreall (Array Int Real) 0.0) + return getArrayRepresentationForLambdaRec( n, reqConst, n[1].getType() ); +} + }/* CVC4::theory::builtin namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index d9ae5b447..3667cf159 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -59,6 +59,8 @@ private: /** recursive helper for getLambdaForArrayRepresentation */ static Node getLambdaForArrayRepresentationRec( TNode a, TNode bvl, unsigned bvlIndex, std::unordered_map< TNode, Node, TNodeHashFunction >& visited ); + /** recursive helper for getArrayRepresentationForLambda */ + static Node getArrayRepresentationForLambdaRec( TNode n, bool reqConst, TypeNode retType ); public: /** * Given an array constant a, returns a lambda expression that it corresponds to, with bound variable list bvl. diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 025fe0349..49e8a6888 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -36,29 +36,11 @@ public: Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl; if(in.getKind() == kind::APPLY_CONSTRUCTOR ){ + /* TypeNode tn = in.getType(); Type t = tn.toType(); DatatypeType dt = DatatypeType(t); - //check for parametric datatype constructors - // to ensure a normal form, all parameteric datatype constructors must have a type ascription - if( dt.isParametric() ){ - if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){ - Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl; - Node op = in.getOperator(); - //get the constructor object - const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())]; - //create ascribed constructor type - Node tc = NodeManager::currentNM()->mkConst(AscriptionType(dtc.getSpecializedConstructorType(t))); - Node op_new = NodeManager::currentNM()->mkNode( kind::APPLY_TYPE_ASCRIPTION, tc, op ); - //make new node - std::vector< Node > children; - children.push_back( op_new ); - children.insert( children.end(), in.begin(), in.end() ); - Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); - Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl; - return RewriteResponse(REWRITE_DONE, inr); - } - } + // enable this rewrite if we support subtypes of tuples if( tn.isTuple() ){ Node nn = normalizeTupleConstructorApp( in ); if( nn!=in ){ @@ -66,6 +48,7 @@ public: return RewriteResponse(REWRITE_AGAIN_FULL, nn); } } + */ if( in.isConst() ){ Trace("datatypes-rewrite-debug") << "Normalizing constant " << in << std::endl; Node inn = normalizeConstant( in ); @@ -241,6 +224,33 @@ public: static RewriteResponse preRewrite(TNode in) { Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl; + //must prewrite to apply type ascriptions since rewriting does not preserve types + if(in.getKind() == kind::APPLY_CONSTRUCTOR ){ + TypeNode tn = in.getType(); + Type t = tn.toType(); + DatatypeType dt = DatatypeType(t); + + //check for parametric datatype constructors + // to ensure a normal form, all parameteric datatype constructors must have a type ascription + if( dt.isParametric() ){ + if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){ + Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl; + Node op = in.getOperator(); + //get the constructor object + const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())]; + //create ascribed constructor type + Node tc = NodeManager::currentNM()->mkConst(AscriptionType(dtc.getSpecializedConstructorType(t))); + Node op_new = NodeManager::currentNM()->mkNode( kind::APPLY_TYPE_ASCRIPTION, tc, op ); + //make new node + std::vector< Node > children; + children.push_back( op_new ); + children.insert( children.end(), in.begin(), in.end() ); + Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); + Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl; + return RewriteResponse(REWRITE_DONE, inr); + } + } + } return RewriteResponse(REWRITE_DONE, in); } @@ -251,10 +261,11 @@ public: Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl; if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) { if( n1.getOperator() != n2.getOperator()) { - if( n1.getNumChildren() != n2.getNumChildren() || !n1.getType().isTuple() || !n2.getType().isTuple() ){ - Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl; - return true; - } + //enable this check if we support subtypes with tuples + //if( n1.getNumChildren() != n2.getNumChildren() || !n1.getType().isTuple() || !n2.getType().isTuple() ){ + Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl; + return true; + //} } Assert( n1.getNumChildren() == n2.getNumChildren() ); for( unsigned i=0; i children; diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index e787ebc49..d6045404d 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -101,6 +101,8 @@ struct DatatypeConstructorTypeRule { return false; } } + //if we support subtyping for tuples, enable this + /* //check whether it is in normal form? TypeNode tn = n.getType(); if( tn.isTuple() ){ @@ -114,6 +116,7 @@ struct DatatypeConstructorTypeRule { }else if( tn.isCodatatype() ){ //TODO? } + */ return true; } }; /* struct DatatypeConstructorTypeRule */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 17a2ea2ef..1368dd067 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -189,6 +189,7 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) # we have a minimized version still getting tested # bug639 -- still fails, reopened bug # bug585 -- contains subrange type (not supported) +# issue1048-arrays-int-real.smt2 -- different errors on debug and production DISABLED_TESTS = \ bug512.smt2 \ bug585.cvc diff --git a/test/regress/regress0/datatypes/tuple-no-clash.cvc b/test/regress/regress0/datatypes/tuple-no-clash.cvc index 4d7345a54..ecdc8198f 100644 --- a/test/regress/regress0/datatypes/tuple-no-clash.cvc +++ b/test/regress/regress0/datatypes/tuple-no-clash.cvc @@ -6,6 +6,6 @@ y : REAL; z : REAL; ASSERT x = (y, z) OR x = (z, y); -ASSERT x = (0,0) OR x = (1,1); +ASSERT x = (0.0,0.0) OR x = (1.0,1.0); CHECKSAT; diff --git a/test/regress/regress0/issue1048-arrays-int-real.smt2 b/test/regress/regress0/issue1048-arrays-int-real.smt2 new file mode 100644 index 000000000..6bbfe4cb7 --- /dev/null +++ b/test/regress/regress0/issue1048-arrays-int-real.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_ALIRA) +(declare-fun a () (Array Int Real)) +(declare-fun b () (Array Int Int)) +(assert (= a b)) +(assert (= (select a 0) 0.5)) +(check-sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index c5a81c960..cdf2ec9bc 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -70,10 +70,7 @@ TESTS = \ agg-rew-test-cf.smt2 \ rew-to-0211-dd.smt2 \ rew-to-scala.smt2 \ - macro-subtype-param.smt2 \ macros-real-arg.smt2 \ - subtype-param-unk.smt2 \ - subtype-param.smt2 \ anti-sk-simp.smt2 \ pure_dt_cbqi.smt2 \ florian-case-ax.smt2 \ @@ -108,6 +105,11 @@ TESTS = \ # clock-10.smt2 # +# FIXME: I've disabled these since they give different error messages on production and debug +# macro-subtype-param.smt2 +# subtype-param-unk.smt2 +# subtype-param.smt2 + EXTRA_DIST = $(TESTS) \ bug291.smt2.expect diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 index f44d75195..97ff827a7 100644 --- a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 +++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 @@ -1,5 +1,11 @@ ; COMMAND-LINE: --macros-quant -; EXPECT: unknown +; EXPECT: (error "argument type is not a subtype of the function's argument type: +; EXPECT: argument: x +; EXPECT: has type: (List Int) +; EXPECT: not subtype: (List Real) +; EXPECT: in term : (R (as x (List Real)))") +; EXIT: 1 + (set-logic ALL_SUPPORTED) (declare-datatypes ((List 1)) ((par (T) ((cons (hd T) (tl (List T))) (nil))))) diff --git a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 index e3008772d..f3ee6a86a 100644 --- a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 +++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 @@ -1,5 +1,11 @@ ; COMMAND-LINE: --lang=smt2.5 -; EXPECT: unknown +; EXPECT: (error "argument type is not a subtype of the function's argument type: +; EXPECT: argument: x +; EXPECT: has type: (List Int) +; EXPECT: not subtype: (List Real) +; EXPECT: in term : (R (as x (List Real)))") +; EXIT: 1 + ; this will fail if type rule for APPLY_UF requires arguments to be subtypes (set-logic ALL_SUPPORTED) diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2 index 42d7a5b60..860c03b6f 100644 --- a/test/regress/regress0/quantifiers/subtype-param.smt2 +++ b/test/regress/regress0/quantifiers/subtype-param.smt2 @@ -1,5 +1,11 @@ ; COMMAND-LINE: --lang=smt2.5 -; EXPECT: unsat +; EXPECT: (error "argument type is not a subtype of the function's argument type: +; EXPECT: argument: x +; EXPECT: has type: (Array Int Int) +; EXPECT: not subtype: (Array Int Real) +; EXPECT: in term : (Q (as x (Array Int Real)))") +; EXIT: 1 + (set-logic ALL_SUPPORTED) (set-info :status unsat) diff --git a/test/regress/regress0/sets/sets-tuple-poly.cvc b/test/regress/regress0/sets/sets-tuple-poly.cvc index 64fb310be..4cac9a24e 100644 --- a/test/regress/regress0/sets/sets-tuple-poly.cvc +++ b/test/regress/regress0/sets/sets-tuple-poly.cvc @@ -7,7 +7,7 @@ b : SET OF [INT, REAL]; x : [ REAL, REAL ]; -ASSERT NOT x = (0,0); +ASSERT NOT x = (0.0,0.0); ASSERT (x.0, FLOOR(x.1)) IS_IN a; ASSERT (FLOOR(x.0), x.1) IS_IN b; diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 9f26312dc..15c380c31 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -363,60 +363,55 @@ public: TS_ASSERT_DIFFERS(pairIntInt, pairRealInt); TS_ASSERT_DIFFERS(pairIntReal, pairRealInt); - TS_ASSERT_EQUALS(pairRealReal.getBaseType(), pairRealReal); - TS_ASSERT_EQUALS(pairRealInt.getBaseType(), pairRealReal); - TS_ASSERT_EQUALS(pairIntReal.getBaseType(), pairRealReal); - TS_ASSERT_EQUALS(pairIntInt.getBaseType(), pairRealReal); - TS_ASSERT(pairRealReal.isComparableTo(pairRealReal)); - TS_ASSERT(pairIntReal.isComparableTo(pairRealReal)); - TS_ASSERT(pairRealInt.isComparableTo(pairRealReal)); - TS_ASSERT(pairIntInt.isComparableTo(pairRealReal)); - TS_ASSERT(pairRealReal.isComparableTo(pairRealInt)); - TS_ASSERT(pairIntReal.isComparableTo(pairRealInt)); + TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal)); + TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal)); + TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal)); + TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt)); + TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt)); TS_ASSERT(pairRealInt.isComparableTo(pairRealInt)); - TS_ASSERT(pairIntInt.isComparableTo(pairRealInt)); - TS_ASSERT(pairRealReal.isComparableTo(pairIntReal)); + TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt)); + TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal)); TS_ASSERT(pairIntReal.isComparableTo(pairIntReal)); - TS_ASSERT(pairRealInt.isComparableTo(pairIntReal)); - TS_ASSERT(pairIntInt.isComparableTo(pairIntReal)); - TS_ASSERT(pairRealReal.isComparableTo(pairIntInt)); - TS_ASSERT(pairIntReal.isComparableTo(pairIntInt)); - TS_ASSERT(pairRealInt.isComparableTo(pairIntInt)); + TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal)); + TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal)); + TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt)); + TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt)); + TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt)); TS_ASSERT(pairIntInt.isComparableTo(pairIntInt)); TS_ASSERT(pairRealReal.isSubtypeOf(pairRealReal)); - TS_ASSERT(pairIntReal.isSubtypeOf(pairRealReal)); - TS_ASSERT(pairRealInt.isSubtypeOf(pairRealReal)); - TS_ASSERT(pairIntInt.isSubtypeOf(pairRealReal)); + TS_ASSERT(!pairIntReal.isSubtypeOf(pairRealReal)); + TS_ASSERT(!pairRealInt.isSubtypeOf(pairRealReal)); + TS_ASSERT(!pairIntInt.isSubtypeOf(pairRealReal)); TS_ASSERT(!pairRealReal.isSubtypeOf(pairRealInt)); TS_ASSERT(!pairIntReal.isSubtypeOf(pairRealInt)); TS_ASSERT(pairRealInt.isSubtypeOf(pairRealInt)); - TS_ASSERT(pairIntInt.isSubtypeOf(pairRealInt)); + TS_ASSERT(!pairIntInt.isSubtypeOf(pairRealInt)); TS_ASSERT(!pairRealReal.isSubtypeOf(pairIntReal)); TS_ASSERT(pairIntReal.isSubtypeOf(pairIntReal)); TS_ASSERT(!pairRealInt.isSubtypeOf(pairIntReal)); - TS_ASSERT(pairIntInt.isSubtypeOf(pairIntReal)); + TS_ASSERT(!pairIntInt.isSubtypeOf(pairIntReal)); TS_ASSERT(!pairRealReal.isSubtypeOf(pairIntInt)); TS_ASSERT(!pairIntReal.isSubtypeOf(pairIntInt)); TS_ASSERT(!pairRealInt.isSubtypeOf(pairIntInt)); TS_ASSERT(pairIntInt.isSubtypeOf(pairIntInt)); TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealReal)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealReal)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealReal)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealReal)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealInt)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealInt)).toType(), pairRealReal); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealReal)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealReal)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealReal)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealInt)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealInt)).isNull()); TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealInt)).toType(), pairRealInt); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealInt)).toType(), pairRealInt); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntReal)).toType(), pairRealReal); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealInt)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntReal)).isNull()); TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntReal)).toType(), pairIntReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntReal)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntReal)).toType(), pairIntReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntInt)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntInt)).toType(), pairIntReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntInt)).toType(), pairRealInt); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntReal)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntReal)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntInt)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntInt)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntInt)).isNull()); TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntInt)).toType(), pairIntInt); } -- 2.30.2