CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort);
CVC5_API_SOLVER_CHECK_TERM(term);
- // We are permissive with subtypes so that integers are allowed to define
- // the body of a function whose codomain is real. This is to accomodate
- // SMT-LIB inputs in the Reals theory, where NUMERAL can be used to specify
- // reals. Instead of making our parser for numerals dependent on the logic,
- // we instead allow integers here in this case.
+ // the sort of the body must match the return sort
CVC5_API_CHECK(term.d_node->getType() == *sort.d_type)
<< "Invalid sort of function body '" << term << "', expected '" << sort
<< "'";
CVC5_API_SOLVER_CHECK_TERM(term);
CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort);
- // we are permissive with subtypes, similar to defineFun
CVC5_API_CHECK(term.d_node->getType() == *sort.d_type)
<< "Invalid sort of function body '" << term << "', expected '" << sort
<< "'";
std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts);
Sort codomain = fun.getSort().getFunctionCodomainSort();
- // we are permissive with subtypes, similar to defineFun
CVC5_API_CHECK(*codomain.d_type == term.d_node->getType())
<< "Invalid sort of function body '" << term << "', expected '"
<< codomain << "'";
recurse = false;
}
}
- else if (!var.getType().isSubtypeOf(cn.getType()))
+ else if (var.getType() != cn.getType())
{
recurse = false;
}
{
currChildren.push_back(next);
syms.pop_back();
- // check subtyping in the (non-list) case
- if (!var.getType().isSubtypeOf(next.getType()))
+ // check types in the (non-list) case
+ if (var.getType() != next.getType())
{
next = Node::null();
}
visited.insert(curr);
if (curr.first.getNumChildren() == 0)
{
- if (!curr.first.getType().isComparableTo(curr.second.getType()))
+ if (curr.first.getType() != curr.second.getType())
{
// the two subterms have different types
return false;
void Subs::add(const Node& v, const Node& s)
{
- Assert(s.isNull() || v.getType().isComparableTo(s.getType()));
+ Assert(s.isNull() || v.getType() == s.getType());
d_vars.push_back(v);
d_subs.push_back(s);
}
return kind::isWellFounded(*this);
}
-bool TypeNode::isStringLike() const { return isString() || isSequence(); }
-
-// !!! Note that this will change to isReal() || isInteger() when subtyping is
-// eliminated
-bool TypeNode::isRealOrInt() const { return isReal(); }
-
-bool TypeNode::isSubtypeOf(TypeNode t) const {
- if(*this == t) {
- return true;
- }
- if (isInteger())
- {
- return t.isReal();
- }
- if (isFunction() && t.isFunction())
- {
- if (!getRangeType().isSubtypeOf(t.getRangeType()))
- {
- // range is not subtype, return false
- return false;
- }
- // must have equal arguments
- std::vector<TypeNode> t0a = getArgTypes();
- std::vector<TypeNode> t1a = t.getArgTypes();
- if (t0a.size() != t1a.size())
- {
- // different arities
- return false;
- }
- for (size_t i = 0, nargs = t0a.size(); i < nargs; i++)
- {
- if (t0a[i] != t1a[i])
- {
- // an argument is different
- return false;
- }
- }
- return true;
- }
- // this should only return true for types T1, T2 where we handle equalities between T1 and T2
- // (more cases go here, if we want to support such cases)
- return false;
+bool TypeNode::isInteger() const
+{
+ return getKind() == kind::TYPE_CONSTANT
+ && getConst<TypeConstant>() == INTEGER_TYPE;
}
-bool TypeNode::isComparableTo(TypeNode t) const {
- if (*this == t)
- {
- return true;
- }
- return isSubtypeOf(t) || t.isSubtypeOf(*this);
+bool TypeNode::isReal() const
+{
+ return getKind() == kind::TYPE_CONSTANT
+ && getConst<TypeConstant>() == REAL_TYPE;
}
+bool TypeNode::isStringLike() const { return isString() || isSequence(); }
+
+bool TypeNode::isRealOrInt() const { return isReal() || isInteger(); }
+
TypeNode TypeNode::getDatatypeTesterDomainType() const
{
Assert(isDatatypeTester());
return dt.getParameter(n) != (*this)[n + 1];
}
-TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
- if (t0 == t1)
- {
- return t0;
- }
- if (t0.isSubtypeOf(t1))
- {
- return t1;
- }
- else if (t1.isSubtypeOf(t0))
- {
- return t0;
- }
- return TypeNode();
-}
-
/** Is this a sort kind */
bool TypeNode::isUninterpretedSort() const
{
*/
bool isWellFounded() const;
- /**
- * Is this type a subtype of the given type?
- */
- bool isSubtypeOf(TypeNode t) const;
-
- /**
- * Is this type comparable to the given type (i.e., do they share
- * a common ancestor in the subtype tree)?
- */
- bool isComparableTo(TypeNode t) const;
-
/** Is this the Boolean type? */
bool isBoolean() const;
*/
TypeNode getUninterpretedSortConstructor() const;
- /**
- * Returns the leastUpperBound in the extended type lattice of the two types.
- * If this is \top, i.e. there is no inhabited type that contains both,
- * a TypeNode such that isNull() is true is returned.
- */
- static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
-
private:
/**
( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE );
}
-inline bool TypeNode::isInteger() const {
- return
- ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE );
-}
-
-inline bool TypeNode::isReal() const {
- return
- ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) ||
- isInteger();
-}
-
inline bool TypeNode::isString() const {
return getKind() == kind::TYPE_CONSTANT &&
getConst<TypeConstant>() == STRING_TYPE;
for (Node child : n) {
TypeNode originalType = child.getType();
TypeNode newType = cache[child].getType();
- if (! newType.isSubtypeOf(originalType)) {
+ if (newType != originalType)
+ {
return true;
}
}
if (parent[0].getType() != parent[1].getType())
{
TNode other = (parent[0] == current) ? parent[1] : parent[0];
- if (current.getType().isSubtypeOf(other.getType()))
+ if (current.getType() == other.getType())
{
break;
}
if (formals.size() > 0)
{
TypeNode rangeType = funcType.getRangeType();
- if (!formulaType.isComparableTo(rangeType))
+ if (formulaType != rangeType)
{
stringstream ss;
ss << "Type of defined function does not match its declaration\n"
}
else
{
- if (!formulaType.isComparableTo(funcType))
+ if (formulaType != funcType)
{
stringstream ss;
ss << "Declared type of defined constant does not match its definition\n"
Trace("smt") << "--- expected type " << expectedType << endl;
// type-check the result we got
- // Notice that lambdas have function type, which does not respect the subtype
- // relation, so we ignore them here.
- Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA
- || resultNode.getType().isSubtypeOf(expectedType))
+ Assert(resultNode.isNull() || resultNode.getType() == expectedType)
<< "Run with -t smt for details.";
// Ensure it's a value (constant or const-ish like real algebraic
operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)"
operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)"
-operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in cvc5, as integer is a subtype of real)"
+operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term)"
typerule ADD ::cvc5::internal::theory::arith::ArithOperatorTypeRule
typerule MULT ::cvc5::internal::theory::arith::ArithOperatorTypeRule
bool NlModel::addBound(TNode v, TNode l, TNode u)
{
- Assert(l.getType().isSubtypeOf(v.getType()));
- Assert(u.getType().isSubtypeOf(v.getType()));
+ Assert(l.getType() == v.getType());
+ Assert(u.getType() == v.getType());
Trace("nl-ext-model") << "* check model bound : " << v << " -> [" << l << " "
<< u << "]" << std::endl;
if (l == u)
// We also ensure types are correct here, which avoids substituting
// a term of non-integer type for a variable of integer type.
if (veqc.isNull() && !expr::hasSubterm(slv, uv)
- && slv.getType().isSubtypeOf(uv.getType()))
+ && slv.getType() == uv.getType())
{
Trace("nl-ext-cm")
<< "check-model-subs : " << uv << " -> " << slv << std::endl;
}
TypeNode indexType = n[1].getType(check);
TypeNode valueType = n[2].getType(check);
- if (!indexType.isSubtypeOf(arrayType.getArrayIndexType()))
+ if (indexType != arrayType.getArrayIndexType())
{
throw TypeCheckingExceptionPrivate(
n, "array store not indexed with correct type for array");
}
- if (!valueType.isSubtypeOf(arrayType.getArrayConstituentType()))
+ if (valueType != arrayType.getArrayConstituentType())
{
Trace("array-types")
<< "array type: " << arrayType.getArrayConstituentType()
TypeNode indexType = n0_type.getArrayIndexType();
TypeNode indexRangeType1 = n[2].getType(check);
TypeNode indexRangeType2 = n[3].getType(check);
- if (!indexRangeType1.isSubtypeOf(indexType))
+ if (indexRangeType1 != indexType)
{
throw TypeCheckingExceptionPrivate(
n, "eqrange lower index type does not match array index type");
}
- if (!indexRangeType2.isSubtypeOf(indexType))
+ if (indexRangeType2 != indexType)
{
throw TypeCheckingExceptionPrivate(
n, "eqrange upper index type does not match array index type");
Node B = n[1];
TypeNode typeA = A.getType().getBagElementType();
TypeNode typeB = B.getType().getBagElementType();
- Assert(e1.getType().isSubtypeOf(typeA));
- Assert(e2.getType().isSubtypeOf(typeB));
+ Assert(e1.getType() == typeA);
+ Assert(e2.getType() == typeB);
TypeNode productTupleType = n.getType().getBagElementType();
Node tuple = TupleUtils::concatTuples(productTupleType, e1, e2);
InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
{
Assert(n.getType().isBag());
- Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
+ Assert(e.getType() == n.getType().getBagElementType());
InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT);
Node count = d_nm->mkNode(BAG_COUNT, e, n);
InferInfo InferenceGenerator::bagMake(Node n, Node e)
{
Assert(n.getKind() == BAG_MAKE);
- Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
+ Assert(e.getType() == n.getType().getBagElementType());
/*
* (ite (and (= e x) (>= c 1))
InferInfo InferenceGenerator::empty(Node n, Node e)
{
Assert(n.getKind() == BAG_EMPTY);
- Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
+ Assert(e.getType() == n.getType().getBagElementType());
InferInfo inferInfo(d_im, InferenceId::BAGS_EMPTY);
Node skolem = registerAndAssertSkolemLemma(n, "skolem_bag");
InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
{
Assert(n.getKind() == BAG_UNION_DISJOINT && n[0].getType().isBag());
- Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
+ Assert(e.getType() == n[0].getType().getBagElementType());
Node A = n[0];
Node B = n[1];
InferInfo InferenceGenerator::unionMax(Node n, Node e)
{
Assert(n.getKind() == BAG_UNION_MAX && n[0].getType().isBag());
- Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
+ Assert(e.getType() == n[0].getType().getBagElementType());
Node A = n[0];
Node B = n[1];
InferInfo InferenceGenerator::intersection(Node n, Node e)
{
Assert(n.getKind() == BAG_INTER_MIN && n[0].getType().isBag());
- Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
+ Assert(e.getType() == n[0].getType().getBagElementType());
Node A = n[0];
Node B = n[1];
InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
{
Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT && n[0].getType().isBag());
- Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
+ Assert(e.getType() == n[0].getType().getBagElementType());
Node A = n[0];
Node B = n[1];
InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
{
Assert(n.getKind() == BAG_DIFFERENCE_REMOVE && n[0].getType().isBag());
- Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
+ Assert(e.getType() == n[0].getType().getBagElementType());
Node A = n[0];
Node B = n[1];
InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e)
{
Assert(n.getKind() == BAG_DUPLICATE_REMOVAL && n[0].getType().isBag());
- Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
+ Assert(e.getType() == n[0].getType().getBagElementType());
Node A = n[0];
InferInfo inferInfo(d_im, InferenceId::BAGS_DUPLICATE_REMOVAL);
InferInfo InferenceGenerator::filterDownwards(Node n, Node e)
{
Assert(n.getKind() == BAG_FILTER && n[1].getType().isBag());
- Assert(e.getType().isSubtypeOf(n[1].getType().getBagElementType()));
+ Assert(e.getType() == n[1].getType().getBagElementType());
Node P = n[0];
Node A = n[1];
InferInfo InferenceGenerator::filterUpwards(Node n, Node e)
{
Assert(n.getKind() == BAG_FILTER && n[1].getType().isBag());
- Assert(e.getType().isSubtypeOf(n[1].getType().getBagElementType()));
+ Assert(e.getType() == n[1].getType().getBagElementType());
Node P = n[0];
Node A = n[1];
InferInfo InferenceGenerator::productDown(Node n, Node e)
{
Assert(n.getKind() == TABLE_PRODUCT);
- Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
+ Assert(e.getType() == n.getType().getBagElementType());
Node A = n[0];
Node B = n[1];
InferInfo InferenceGenerator::joinDown(Node n, Node e)
{
Assert(n.getKind() == TABLE_JOIN);
- Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
+ Assert(e.getType() == n.getType().getBagElementType());
Node A = n[0];
Node B = n[1];
void SolverState::registerCountTerm(Node bag, Node element, Node skolem)
{
Assert(bag.getType().isBag() && bag == getRepresentative(bag));
- Assert(element.getType().isSubtypeOf(bag.getType().getBagElementType())
+ Assert(element.getType() == bag.getType().getBagElementType()
&& element == getRepresentative(element));
Assert(skolem.isVar() && skolem.getType().isInteger());
std::pair<Node, Node> pair = std::make_pair(element, skolem);
Trace("builtin-rewrite") << "Witness rewrite: " << node << " --> "
<< node[1][1 - i] << std::endl;
// also must be a legal elimination: the other side of the equality
- // cannot contain the variable, and it must be a subtype of the
+ // cannot contain the variable, and it must be the same type as the
// variable
if (!expr::hasSubterm(node[1][1 - i], node[0][0])
- && node[1][i].getType().isSubtypeOf(node[0][0].getType()))
+ && node[1][i].getType() == node[0][0].getType())
{
return node[1][1 - i];
}
{
TypeNode originalType = child.getType();
TypeNode newType = d_intblastCache[child].get().getType();
- if (!newType.isSubtypeOf(originalType))
+ if (newType != originalType)
{
result = true;
break;
{
// If there is no reason to cast, return the
// original node.
- if (n.getType().isSubtypeOf(tn))
+ if (n.getType() == tn)
{
return n;
}
Node ret = sygusToBuiltinEval(ev, args);
Trace("dt-sygus-util") << "...got " << ret << "\n";
Trace("dt-sygus-util") << "Type is " << ret.getType() << std::endl;
- Assert(in.getType().isComparableTo(ret.getType()));
+ Assert(in.getType() == ret.getType());
return RewriteResponse(REWRITE_AGAIN_FULL, ret);
}
}
bool isVarAgnostic,
bool doSym)
{
- Assert(n.getType().isComparableTo(nv.getType()));
+ Assert(n.getType() == nv.getType());
TypeNode tn = n.getType();
if (!tn.isDatatype())
{
* - The head is a datatype T,
* - The remaining children are either MATCH_BIND_CASE or MATCH_CASE,
* - The patterns for the cases are over the same datatype as the head term,
- * - The return types for the cases are comparable,
+ * - The return types for the cases are the same,
* - The patterns specified by the children are exhaustive for T.
*
- * The type rule returns the (least common subtype) of the return types of the
- * cases.
+ * The type rule returns the return type of the cases.
*/
class MatchTypeRule
{
{
// By using internal representation of terms, we ensure polymorphism is
// handled correctly.
- Assert(vars[i].getType().isComparableTo(subs[i].getType()));
+ Assert(vars[i].getType() == subs[i].getType());
}
#endif
// must convert the inferred substitution to original form
Node n = it->second;
Trace("cegqi-inst-debug") << " " << d_input_vars[i] << " -> " << n
<< std::endl;
- Assert(n.getType().isComparableTo(d_input_vars[i].getType()));
+ Assert(n.getType() == d_input_vars[i].getType());
subs.push_back( n );
}
}
Node v = d_input_vars[i];
Trace("cegqi-inst") << i << " (" << d_curr_iphase[v] << ") : "
<< v << " -> " << subs[i] << std::endl;
- Assert(subs[i].getType().isComparableTo(v.getType()));
+ Assert(subs[i].getType() == v.getType());
}
}
Trace("cegqi-inst-debug") << "Do the instantiation...." << std::endl;
Trace("sygus-si-apply-subs-debug") << "is_basic = " << is_basic << " " << tn << std::endl;
for( unsigned i=0; i<subs.size(); i++ ){
Trace("sygus-si-apply-subs-debug") << " " << vars[i] << " -> " << subs[i] << " types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl;
- Assert(subs[i].getType().isSubtypeOf(vars[i].getType()));
+ Assert(subs[i].getType() == vars[i].getType());
}
}
Node nret;
Node v = msum_term[it->first];
if (!v.isNull())
{
- Assert(v.getType().isComparableTo(type));
+ Assert(v.getType() == type);
c = nm->mkNode(MULT, c, v);
}
children.push_back( c );
Node n = (*d_eqc_false);
++d_eqc_false;
if( n.getKind()==d_match_pattern.getKind() ){
- if (n[0].getType().isComparableTo(d_match_pattern_type)
- && isLegalCandidate(n))
+ if (n[0].getType() == d_match_pattern_type && isLegalCandidate(n))
{
//found an iff or equality, try to match it
//DO_THIS: cache to avoid redundancies?
while( !d_eq.isFinished() ){
TNode n = (*d_eq);
++d_eq;
- if( n.getType().isComparableTo( d_match_pattern_type ) ){
+ if (n.getType() == d_match_pattern_type)
+ {
TNode nh = tdb->getEligibleTermInEqc(n);
if( !nh.isNull() ){
if (options::instMaxLevel() != -1)
//if t not null, try to fit it into match m
if( !t.isNull() ){
if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
- Assert(t.getType().isComparableTo(d_match_pattern_type));
+ Assert(t.getType() == d_match_pattern_type);
Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl;
success = getMatch(t, m);
if( d_independent_gen && success<0 ){
{
Node t = tt.first;
// using representatives, just check if equal
- Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
+ Assert(t.getType() == d_match_pattern_arg_types[argIndex]);
bool wasSet = !m.get(v).isNull();
if (!m.set(v, t))
{
Trace("var-trigger-matching")
<< "...got " << s << ", " << s.getKind() << std::endl;
d_eq_class = Node::null();
- // if( s.getType().isSubtypeOf( d_var_type ) ){
d_rm_prev = m.get(index).isNull();
if (!m.set(index, s))
{
Trace("internal-rep-select")
<< "...Choose " << r_best << " with score " << r_best_score
<< " and type " << r_best.getType() << std::endl;
- Assert(r_best.getType().isSubtypeOf(v_tn));
+ Assert(r_best.getType() == v_tn);
v_int_rep[r] = r_best;
if (TraceIsOn("internal-rep-debug"))
{
{ // reject
return -2;
}
- else if (!n.getType().isSubtypeOf(v_tn))
+ else if (n.getType() != v_tn)
{ // reject if incorrect type
return -2;
}
* Choose a term that is equivalent to a in the current context that is the
* best term for instantiating the index^th variable of quantified formula q.
* If no legal term can be found, we return null. This can occur if:
- * - a's type is not a subtype of the type of the index^th variable of q,
+ * - a's type is not the type of the index^th variable of q,
* - a is in an equivalent class with all terms that are restricted not to
* appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
* guided instantiation.
{
Trace("inst-add-debug2") << "Ensure " << n << " : " << tn << std::endl;
TypeNode ntn = n.getType();
- Assert(ntn.isComparableTo(tn));
if (ntn == tn)
{
return n;
{
d_qni.push_back(it);
// set the match
- if (it->first.getType().isComparableTo(d_qi->d_var_types[repVar])
+ if (it->first.getType() == d_qi->d_var_types[repVar]
&& d_qi->setMatch(d_qni_bound[index], it->first, true, true))
{
Trace("qcf-match-debug")
}
TNode op = n.getOperator();
TNode fdeft = fdef;
- Assert(op.getType().isComparableTo(fdef.getType()));
+ Assert(op.getType() == fdef.getType());
return op.eqNode(fdef);
}
bool QuantifiersRewriter::isVarElim(Node v, Node s)
{
Assert(v.getKind() == BOUND_VARIABLE);
- return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType());
+ return !expr::hasSubterm(s, v) && s.getType() == v.getType();
}
Node QuantifiersRewriter::getVarElimEq(Node lit,
<< "Variable eliminate based on theory-specific solving : " << var
<< " -> " << slv << std::endl;
Assert(!expr::hasSubterm(slv, var));
- Assert(slv.getType().isSubtypeOf(var.getType()));
+ Assert(slv.getType() == var.getType());
vars.push_back(var);
subs.push_back(slv);
args.erase(ita);
//-------------------------------------variable elimination utilities
/** is variable elimination
*
- * Returns true if v is not a subterm of s, and the type of s is a subtype of
+ * Returns true if v is not a subterm of s, and the type of s is the same as
* the type of v.
*/
static bool isVarElim(Node v, Node s);
TypeNode expectedType = d.first[0][dd.first].getType();
for (const Node& t : r->d_terms)
{
- if (!t.getType().isComparableTo(expectedType))
+ if (t.getType() != expectedType)
{
Unhandled() << "Relevant domain: bad type " << t.getType()
<< ", expected " << expectedType;
for (unsigned j = 0, psize = vsProc.size(); j < psize; j++)
{
evalVisited[vsProc[j]] = msProc[j];
- Assert(vsProc[j].getType().isComparableTo(msProc[j].getType()));
+ Assert(vsProc[j].getType() == msProc[j].getType());
}
}
}
TypeNode tn = value.getType();
Node var_list = tn.getDType().getSygusVarList();
NodeManager* nm = NodeManager::currentNM();
- // get subtypes in value's type
+ // get subfield types in value's type
SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
std::vector<TypeNode> sf_types;
ti.getSubfieldTypes(sf_types);
std::map<Node, Node> cons_var;
for (const Node& v : var_list)
{
- // collect constructors for variable in all subtypes
+ // collect constructors for variable in all subfield types
for (const TypeNode& stn : sf_types)
{
const DType& dt = stn.getDType();
d_tn = tn;
// get variables in value's type
Node var_list = tn.getDType().getSygusVarList();
- // get subtypes in value's type
+ // get subfield types in value's type
NodeManager* nm = NodeManager::currentNM();
SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
std::vector<TypeNode> sf_types;
// associate variables with constructors in all subfield types
for (const Node& v : var_list)
{
- // collect constructors for variable in all subtypes
+ // collect constructors for variable in all subfield types
for (const TypeNode& stn : sf_types)
{
const DType& dt = stn.getDType();
{
clearEvaluationCache(bv);
}
- Assert(ret.getType().isComparableTo(bv.getType()));
+ Assert(ret.getType() == bv.getType());
return ret;
}
{
// since builtin types occur in grammar, types are comparable but not
// necessarily equal
- Assert(n.getType().isComparableTo(n.getType()));
+ Assert(n.getType() == vn.getType());
if (n == vn)
{
return;
int& sz)
{
Assert(vnr.isNull() || vn != vnr);
- Assert(n.getType().isComparableTo(vn.getType()));
+ Assert(n.getType() == vn.getType());
TypeNode ntn = n.getType();
if (!ntn.isDatatype())
{
++it)
{
Assert(it->first < d_arg_vars.size());
- Assert(
- it->second.getType().isComparableTo(d_arg_vars[it->first].getType()));
+ Assert(it->second.getType() == d_arg_vars[it->first].getType());
vars.push_back(d_arg_vars[it->first]);
subs.push_back(it->second);
}
// since we don't have function subtyping, this assertion should only
// check the return type
Assert(fvar.getType().isFunction());
- Assert(fvar.getType().getRangeType().isComparableTo(bsol.getType()));
+ Assert(fvar.getType().getRangeType() == bsol.getType());
bsol = nm->mkNode(LAMBDA, bvl, bsol);
}
else
{
- Assert(fvar.getType().isComparableTo(bsol.getType()));
+ Assert(fvar.getType() == bsol.getType());
}
// store in map
smc[fvar] = bsol;
{
Assert(tn.isDatatype());
Assert(tn.getDType().isSygus());
- Assert(tn.getDType().getSygusType().isComparableTo(c.getType()));
+ Assert(tn.getDType().getSygusType() == c.getType());
std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c);
if (it == d_proxy_vars[tn].end())
}
Trace("sygus-db-canon") << " ...normalized " << n << " --> " << ret
<< std::endl;
- Assert(ret.getType().isComparableTo(n.getType()));
+ Assert(ret.getType() == n.getType());
return ret;
}
// if its a constant, we use the datatype utility version
return datatypes::utils::sygusToBuiltin(n);
}
- Assert(n.getType().isComparableTo(tn));
+ Assert(n.getType() == tn);
if (!tn.isDatatype())
{
return n;
Trace("sygus-db") << " registering symmetry breaking clauses..."
<< std::endl;
// depending on if we are using symbolic constructors, introduce symmetry
- // breaking lemma templates for each relevant subtype of the grammar
+ // breaking lemma templates for each relevant subfield type of the grammar
SygusTypeInfo& eti = getTypeInfo(et);
std::vector<TypeNode> sf_types;
eti.getSubfieldTypes(sf_types);
// terms, so the term created by mkGeneric will also be well-typed here.
Node g = tds->mkGeneric(dt, i);
TypeNode gtn = g.getType();
- AlwaysAssert(gtn.isSubtypeOf(btn))
+ AlwaysAssert(gtn == btn)
<< "Sygus datatype " << dt.getName()
<< " encodes terms that are not of type " << btn << std::endl
<< "Due to " << g << " of type " << gtn << std::endl;
d.initialize();
for (const Node& i : initValue)
{
- Assert(i.getType().isComparableTo(p.getType().getSetElementType()));
+ Assert(i.getType() == p.getType().getSetElementType());
d.add(i);
}
}
terms[variableIx] = t;
Trace("inst-alg-rd") << t << " ";
Assert(!t.isNull());
- Assert(t.getType().isComparableTo(d_quantifier[0][variableIx].getType()))
+ Assert(t.getType() == d_quantifier[0][variableIx].getType())
<< "Bad type: " << t << " " << t.getType() << " "
<< d_quantifier[0][variableIx].getType();
}
}
}
Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
- Assert(n.getType().isSubtypeOf(tn));
+ Assert(n.getType() == tn);
d_tmap[ n ] = (int)d_type_reps[tn].size();
d_type_reps[tn].push_back( n );
}
TypeNode tn1 = atom[0].getType();
TypeNode tn2 = atom[1].getType();
// already declared, ensure compatible
- if ((!tn1.isNull() && !tn1.isComparableTo(d_type_ref))
- || (!tn2.isNull() && !tn2.isComparableTo(d_type_data)))
+ if ((!tn1.isNull() && tn1 != d_type_ref)
+ || (!tn2.isNull() && tn2 != d_type_data))
{
std::stringstream ss;
ss << "ERROR: the separation logic heap type has already been set to "
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
// if no sort was inferred for this node, return original
- if( tn.isNull() || tn.isComparableTo( old.getType() ) ){
+ if (tn.isNull() || tn == old.getType())
+ {
return old;
- }else if( old.isConst() ){
+ }
+ else if (old.isConst())
+ {
//must make constant of type tn
if( d_const_map[tn].find( old )==d_const_map[tn].end() ){
std::stringstream ss;
"constant created during sort inference"); // use mkConst???
}
return d_const_map[tn][ old ];
- }else if( old.getKind()==kind::BOUND_VARIABLE ){
+ }
+ else if (old.getKind() == kind::BOUND_VARIABLE)
+ {
std::stringstream ss;
ss << "b_" << old;
return nm->mkBoundVar(ss.str(), tn);
}else if( n.getKind()==kind::EQUAL ){
TypeNode tn1 = children[0].getType();
TypeNode tn2 = children[1].getType();
- if( !tn1.isComparableTo( tn2 ) ){
+ if (tn1 != tn2)
+ {
Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl;
Trace("sort-inference-warn") << " Types : " << children[0].getType() << " " << children[1].getType() << std::endl;
Assert(false);
{
TypeNode tn = children[i+1].getType();
TypeNode tna = getTypeForId( d_op_arg_types[op][i] );
- if (!tn.isSubtypeOf(tna))
+ if (tn != tna)
{
Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl;
Assert(false);
{
// (seq.unit x) = (seq.unit y) => x=y, or
// (seq.unit x) = (seq.unit c) => x=c
- Assert(s.getType().isComparableTo(t.getType()));
+ Assert(s.getType() == t.getType());
d_im.sendInference(exp, s.eqNode(t), InferenceId::STRINGS_UNIT_INJ);
}
}
Assert(v.getKind() == SEQ_UNIT);
vc = v[0];
}
- Assert(u[0].getType().isComparableTo(vc.getType()));
+ Assert(u[0].getType() == vc.getType());
// if already disequal, we are done
if (d_state.areDisequal(u[0], vc))
{
EqcInfo* eb)
{
Assert(eb != nullptr && ea != nullptr);
- Assert(a.getType().isComparableTo(b.getType()))
+ Assert(a.getType() == b.getType())
<< "bad types for merge " << a << ", " << b;
// usages of isRealOrInt are only due to subtyping, where seq.nth for
// sequences of Real are merged to integer equivalence classes
TypeNode etn = c.getType().getSequenceElementType();
for (const Node& snv : snvec)
{
- Assert(snv.getType().isSubtypeOf(etn));
+ Assert(snv.getType() == etn);
Node v = bvm->mkBoundVar<SeqModelVarAttribute>(snv, etn);
// use a skolem, not a bound variable
Node kv = sm->mkPurifySkolem(v, "smv");
{
return false;
}
- if (!val.getType().isSubtypeOf(x.getType()))
+ if (val.getType() != x.getType())
{
+ Assert(false) << "isLegalElimination for disequal typed terms " << x
+ << " -> " << val;
return false;
}
if (!options().smt.produceModels || options().smt.modelVarElimUneval)
*
* The following criteria imply that x -> val is *not* a legal elimination:
* (1) If x is contained in val,
- * (2) If the type of val is not a subtype of the type of x,
+ * (2) If the type of val is not the same as the type of x,
* (3) If val contains an operator that cannot be evaluated, and
* produceModels is true. For example, x -> sqrt(2) is not a legal
* elimination if we are producing models. This is because we care about the
Node n = *eqc_i;
static int repCheckInstance = 0;
++repCheckInstance;
- AlwaysAssert(rep.getType().isSubtypeOf(n.getType()))
+ AlwaysAssert(rep.getType() == n.getType())
<< "Representative " << rep << " of " << n
<< " violates type constraints (" << rep.getType() << " and "
<< n.getType() << ")";
Node hni = m->getRepresentative(hn[1]);
Trace("model-builder-debug2") << " get rep : " << hn[0]
<< " returned " << hni << std::endl;
- Assert(hni.getType().isSubtypeOf(args[0].getType()));
+ Assert(hni.getType() == args[0].getType());
hni = rewrite(args[0].eqNode(hni));
Node hnv = m->getRepresentative(hn);
Trace("model-builder-debug2") << " get rep val : " << hn
largs.begin(), largs.end(), apply_args.begin(), apply_args.end());
hnv = rewrite(hnv);
}
- Assert(!TypeNode::leastCommonTypeNode(hnv.getType(), curr.getType())
- .isNull());
+ Assert(hnv.getType() == curr.getType());
curr = NodeManager::currentNM()->mkNode(kind::ITE, hni, hnv, curr);
}
}
if (!c1.isNull() && !c2.isNull())
{
simpTrans = false;
- Assert(c1.getType().isComparableTo(c2.getType()));
+ Assert(c1.getType() == c2.getType());
std::shared_ptr<EqProof> eqpmc = std::make_shared<EqProof>();
eqpmc->d_id = MERGED_THROUGH_CONSTANTS;
eqpmc->d_node = c1.eqNode(c2).eqNode(d_false);
a[2], bvl, bvlIndex + 1, visited);
if (!val.isNull())
{
- Assert(!TypeNode::leastCommonTypeNode(a[1].getType(),
- bvl[bvlIndex].getType())
- .isNull());
- Assert(!TypeNode::leastCommonTypeNode(val.getType(), body.getType())
- .isNull());
+ Assert(a[1].getType() == bvl[bvlIndex].getType());
+ Assert(val.getType() == body.getType());
Node cond = bvl[bvlIndex].eqNode(a[1]);
ret = NodeManager::currentNM()->mkNode(kind::ITE, cond, val, body);
}
Trace("builtin-rewrite-debug2")
<< " make array store all " << curr.getType()
<< " annotated : " << array_type << std::endl;
- Assert(curr.getType().isSubtypeOf(array_type.getArrayConstituentType()));
+ Assert(curr.getType() == array_type.getArrayConstituentType());
curr = nm->mkConst(ArrayStoreAll(array_type, curr));
Trace("builtin-rewrite-debug2") << " build array..." << std::endl;
// can only build if default value is constant (since array store all must
for (size_t i = 0, numCond = conds.size(); i < numCond; i++)
{
size_t ii = (numCond - 1) - i;
- Assert(conds[ii].getType().isSubtypeOf(first_arg.getType()));
+ Assert(conds[ii].getType() == first_arg.getType());
curr = nm->mkNode(kind::STORE, curr, conds[ii], vals[ii]);
// normalize it using the array rewriter utility, which must be done at
// each iteration of this loop
if (currentArgument != currentArgumentType)
{
std::stringstream ss;
- ss << "argument type is not a subtype of the function's argument "
+ ss << "argument type is not the type of the function's argument "
<< "type:\n"
<< "argument: " << *argument_it << "\n"
<< "has type: " << (*argument_it).getType() << "\n"
- << "not subtype: " << *argument_type_it << "\n"
+ << "not type: " << *argument_type_it << "\n"
<< "in term : " << n;
throw TypeCheckingExceptionPrivate(n, ss.str());
}
std::vector<Node> formals;
formals.push_back(x);
d_slvEngine->defineFunction(lambda, formals, xPos);
-
- ASSERT_FALSE(realType.isComparableTo(booleanType));
- ASSERT_TRUE(realType.isComparableTo(integerType));
- ASSERT_TRUE(realType.isComparableTo(realType));
- ASSERT_FALSE(realType.isComparableTo(arrayType));
- ASSERT_FALSE(realType.isComparableTo(bvType));
-
- ASSERT_FALSE(booleanType.isComparableTo(integerType));
- ASSERT_FALSE(booleanType.isComparableTo(realType));
- ASSERT_TRUE(booleanType.isComparableTo(booleanType));
- ASSERT_FALSE(booleanType.isComparableTo(arrayType));
- ASSERT_FALSE(booleanType.isComparableTo(bvType));
-
- ASSERT_TRUE(integerType.isComparableTo(realType));
- ASSERT_TRUE(integerType.isComparableTo(integerType));
- ASSERT_FALSE(integerType.isComparableTo(booleanType));
- ASSERT_FALSE(integerType.isComparableTo(arrayType));
- ASSERT_FALSE(integerType.isComparableTo(bvType));
-
- ASSERT_FALSE(arrayType.isComparableTo(booleanType));
- ASSERT_FALSE(arrayType.isComparableTo(integerType));
- ASSERT_FALSE(arrayType.isComparableTo(realType));
- ASSERT_TRUE(arrayType.isComparableTo(arrayType));
- ASSERT_FALSE(arrayType.isComparableTo(bvType));
-
- ASSERT_FALSE(bvType.isComparableTo(booleanType));
- ASSERT_FALSE(bvType.isComparableTo(integerType));
- ASSERT_FALSE(bvType.isComparableTo(realType));
- ASSERT_FALSE(bvType.isComparableTo(arrayType));
- ASSERT_TRUE(bvType.isComparableTo(bvType));
}
} // namespace test
} // namespace cvc5::internal
{
};
-TEST_F(TestTheoryWhiteSetsTypeRuleInternal, is_comparable_to)
-{
- TypeNode setRealType = d_nodeManager->mkSetType(d_nodeManager->realType());
- TypeNode setIntType = d_nodeManager->mkSetType(d_nodeManager->integerType());
- ASSERT_FALSE(setIntType.isComparableTo(setRealType));
- ASSERT_FALSE(setIntType.isSubtypeOf(setRealType));
- ASSERT_FALSE(setRealType.isComparableTo(setIntType));
- ASSERT_FALSE(setRealType.isComparableTo(setIntType));
-}
-
TEST_F(TestTheoryWhiteSetsTypeRuleApi, singleton_term)
{
Sort realSort = d_solver.getRealSort();
ASSERT_NE(pairIntInt, pairIntReal);
ASSERT_NE(pairIntInt, pairRealInt);
ASSERT_NE(pairIntReal, pairRealInt);
-
- ASSERT_TRUE(pairRealReal.isComparableTo(pairRealReal));
- ASSERT_FALSE(pairIntReal.isComparableTo(pairRealReal));
- ASSERT_FALSE(pairRealInt.isComparableTo(pairRealReal));
- ASSERT_FALSE(pairIntInt.isComparableTo(pairRealReal));
- ASSERT_FALSE(pairRealReal.isComparableTo(pairRealInt));
- ASSERT_FALSE(pairIntReal.isComparableTo(pairRealInt));
- ASSERT_TRUE(pairRealInt.isComparableTo(pairRealInt));
- ASSERT_FALSE(pairIntInt.isComparableTo(pairRealInt));
- ASSERT_FALSE(pairRealReal.isComparableTo(pairIntReal));
- ASSERT_TRUE(pairIntReal.isComparableTo(pairIntReal));
- ASSERT_FALSE(pairRealInt.isComparableTo(pairIntReal));
- ASSERT_FALSE(pairIntInt.isComparableTo(pairIntReal));
- ASSERT_FALSE(pairRealReal.isComparableTo(pairIntInt));
- ASSERT_FALSE(pairIntReal.isComparableTo(pairIntInt));
- ASSERT_FALSE(pairRealInt.isComparableTo(pairIntInt));
- ASSERT_TRUE(pairIntInt.isComparableTo(pairIntInt));
-
- ASSERT_TRUE(pairRealReal.isSubtypeOf(pairRealReal));
- ASSERT_FALSE(pairIntReal.isSubtypeOf(pairRealReal));
- ASSERT_FALSE(pairRealInt.isSubtypeOf(pairRealReal));
- ASSERT_FALSE(pairIntInt.isSubtypeOf(pairRealReal));
- ASSERT_FALSE(pairRealReal.isSubtypeOf(pairRealInt));
- ASSERT_FALSE(pairIntReal.isSubtypeOf(pairRealInt));
- ASSERT_TRUE(pairRealInt.isSubtypeOf(pairRealInt));
- ASSERT_FALSE(pairIntInt.isSubtypeOf(pairRealInt));
- ASSERT_FALSE(pairRealReal.isSubtypeOf(pairIntReal));
- ASSERT_TRUE(pairIntReal.isSubtypeOf(pairIntReal));
- ASSERT_FALSE(pairRealInt.isSubtypeOf(pairIntReal));
- ASSERT_FALSE(pairIntInt.isSubtypeOf(pairIntReal));
- ASSERT_FALSE(pairRealReal.isSubtypeOf(pairIntInt));
- ASSERT_FALSE(pairIntReal.isSubtypeOf(pairIntInt));
- ASSERT_FALSE(pairRealInt.isSubtypeOf(pairIntInt));
- ASSERT_TRUE(pairIntInt.isSubtypeOf(pairIntInt));
-
- ASSERT_EQ(TypeNode::leastCommonTypeNode(pairRealReal, pairRealReal),
- pairRealReal);
- ASSERT_TRUE(
- TypeNode::leastCommonTypeNode(pairIntReal, pairRealReal).isNull());
- ASSERT_TRUE(
- TypeNode::leastCommonTypeNode(pairRealInt, pairRealReal).isNull());
- ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntInt, pairRealReal).isNull());
- ASSERT_TRUE(
- TypeNode::leastCommonTypeNode(pairRealReal, pairRealInt).isNull());
- ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntReal, pairRealInt).isNull());
- ASSERT_EQ(TypeNode::leastCommonTypeNode(pairRealInt, pairRealInt),
- pairRealInt);
- ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntInt, pairRealInt).isNull());
- ASSERT_TRUE(
- TypeNode::leastCommonTypeNode(pairRealReal, pairIntReal).isNull());
- ASSERT_EQ(TypeNode::leastCommonTypeNode(pairIntReal, pairIntReal),
- pairIntReal);
- ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairRealInt, pairIntReal).isNull());
- ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntInt, pairIntReal).isNull());
- ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairRealReal, pairIntInt).isNull());
- ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntReal, pairIntInt).isNull());
- ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairRealInt, pairIntInt).isNull());
- ASSERT_EQ(TypeNode::leastCommonTypeNode(pairIntInt, pairIntInt), pairIntInt);
}
} // namespace test
} // namespace cvc5::internal
projects / cvc5.git / commitdiff