metakind.h
node_manager.cpp
type_checker.cpp
+ type_properties.cpp
type_properties.h
)
DEPENDS mkkind type_properties_template.h ${KINDS_FILES}
)
+add_custom_command(
+ OUTPUT type_properties.cpp
+ COMMAND
+ ${mkkind_script}
+ ${CMAKE_CURRENT_LIST_DIR}/type_properties_template.cpp
+ ${KINDS_FILES}
+ > ${CMAKE_CURRENT_BINARY_DIR}/type_properties.cpp
+ DEPENDS mkkind type_properties_template.cpp type_properties.h ${KINDS_FILES}
+)
+
add_custom_command(
OUTPUT metakind.h
COMMAND
metakind.h
node_manager.cpp
type_checker.cpp
+ type_properties.cpp
type_properties.h
)
if (!hasConstant)
{
// add an arbitrary one
- Node op = st.mkGroundTerm();
+ NodeManager* nm = NodeManager::currentNM();
+ Node op = nm->mkGroundTerm(st);
// use same naming convention as SygusDatatype
std::stringstream ss;
ss << getName() << "_" << getNumConstructors() << "_" << op;
else
{
// call mkGroundValue or mkGroundTerm based on isValue
- arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm();
+ arg = isValue ? nm->mkGroundValue(selType) : nm->mkGroundTerm(selType);
}
if (arg.isNull())
{
if (ret.getMetaKind() == kind::metakind::PARAMETERIZED)
{
// push the operator
- nb << ret.getOperator();
+ nb << NodeManager::operatorFromType(ret);
}
for (TypeNode::const_iterator j = ret.begin(), iend = ret.end();
j != iend;
*/
static bool isNAryKind(Kind k);
+ /**
+ * Returns a node representing the operator of this `TypeNode`.
+ * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these) have an
+ * operator. "Little-p parameterized" types (like Array), are OPERATORs, not
+ * PARAMETERIZEDs.
+ */
+ static Node operatorFromType(const TypeNode& tn)
+ {
+ Assert(tn.getMetaKind() == kind::metakind::PARAMETERIZED);
+ return Node(tn.d_nv->getOperator());
+ }
+
private:
/**
* Instead of creating an instance using the constructor,
Node mkBoundVar(const TypeNode& type);
+ /**
+ * Construct and return a ground term of a given type. If the type is not
+ * well founded, this function throws an exception.
+ *
+ * @param tn The type
+ * @return a ground term of the type
+ */
+ Node mkGroundTerm(const TypeNode& tn);
+
+ /**
+ * Construct and return a ground value of a given type. If the type is not
+ * well founded, this function throws an exception.
+ *
+ * @param tn The type
+ * @return a ground value of the type
+ */
+ Node mkGroundValue(const TypeNode& tn);
+
/** get the canonical bound variable list for function type tn */
Node getBoundVarListForFunctionType( TypeNode tn );
#include "expr/node_manager_attributes.h"
#include "expr/skolem_manager.h"
#include "expr/type_checker.h"
+#include "expr/type_properties.h"
#include "theory/bags/bag_make_op.h"
#include "theory/sets/singleton_op.h"
+#include "theory/type_enumerator.h"
#include "util/abstract_value.h"
#include "util/bitvector.h"
#include "util/rational.h"
return NodeClass(nv);
}
+Node NodeManager::mkGroundTerm(const TypeNode& tn)
+{
+ return kind::mkGroundTerm(tn);
+}
+
+Node NodeManager::mkGroundValue(const TypeNode& tn)
+{
+ theory::TypeEnumerator te(tn);
+ return *te;
+}
+
bool NodeManager::safeToReclaimZombies() const
{
// FIXME multithreading
return kind::isWellFounded(*this);
}
-Node TypeNode::mkGroundTerm() const {
- return kind::mkGroundTerm(*this);
-}
-
-Node TypeNode::mkGroundValue() const
-{
- theory::TypeEnumerator te(*this);
- return *te;
-}
-
bool TypeNode::isStringLike() const { return isString() || isSequence(); }
// !!! Note that this will change to isReal() || isInteger() when subtyping is
}
}
-Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
- TypeNode ntn = n.getType();
- Assert(ntn.isComparableTo(tn));
- if( !ntn.isSubtypeOf( tn ) ){
- if( tn.isInteger() ){
- if( tn.isSubtypeOf( ntn ) ){
- return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n );
- }
- }else if( tn.isDatatype() && ntn.isDatatype() ){
- if( tn.isTuple() && ntn.isTuple() ){
- const DType& dt1 = tn.getDType();
- const DType& dt2 = ntn.getDType();
- NodeManager* nm = NodeManager::currentNM();
- if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
- std::vector< Node > conds;
- for( unsigned i=0; i<dt2[0].getNumArgs(); i++ ){
- Node s = nm->mkNode(
- kind::APPLY_SELECTOR_TOTAL, dt2[0][i].getSelector(), n);
- Node etc = getEnsureTypeCondition(s, dt1[0][i].getRangeType());
- if( etc.isNull() ){
- return Node::null();
- }else{
- conds.push_back( etc );
- }
- }
- if( conds.empty() ){
- return nm->mkConst(true);
- }else if( conds.size()==1 ){
- return conds[0];
- }else{
- return nm->mkNode(kind::AND, conds);
- }
- }
- }
- }
- return Node::null();
- }else{
- return NodeManager::currentNM()->mkConst( true );
- }
-}
-
/** Is this a sort kind */
bool TypeNode::isSort() const {
return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) );
return getConst<BitVectorSize>();
}
+TypeNode TypeNode::getRangeType() const
+{
+ if (isTester())
+ {
+ return NodeManager::currentNM()->booleanType();
+ }
+ Assert(isFunction() || isConstructor() || isSelector())
+ << "Cannot get range type of " << *this;
+ return (*this)[getNumChildren() - 1];
+}
+
} // namespace cvc5
namespace std {
return TypeNode(d_nv->getChild(i));
}
- /**
- * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these)
- * have an operator. "Little-p parameterized" types (like Array),
- * are OPERATORs, not PARAMETERIZEDs.
- */
- inline Node getOperator() const {
- Assert(getMetaKind() == kind::metakind::PARAMETERIZED);
- return Node(d_nv->getOperator());
- }
-
/**
* Returns the unique id of this node
*
*/
bool isWellFounded() const;
- /**
- * Construct and return a ground term of this type. If the type is
- * not well founded, this function throws an exception.
- *
- * @return a ground term of the type
- */
- Node mkGroundTerm() const;
-
- /**
- * Construct and return a ground value of this type. If the type is
- * not well founded, this function throws an exception.
- *
- * @return a ground value of the type
- */
- Node mkGroundValue() const;
-
/**
* Is this type a subtype of the given type?
*/
static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1);
- /** get ensure type condition
- * Return value is a condition that implies that n has type tn.
- */
- static Node getEnsureTypeCondition( Node n, TypeNode tn );
private:
static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
return isFunctionLike() && getRangeType().isBoolean();
}
-inline TypeNode TypeNode::getRangeType() const {
- if(isTester()) {
- return NodeManager::currentNM()->booleanType();
- }
- Assert(isFunction() || isConstructor() || isSelector())
- << "Cannot get range type of " << *this;
- return (*this)[getNumChildren() - 1];
-}
-
/** Is this a floating-point type of with <code>exp</code> exponent bits
and <code>sig</code> significand bits */
inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const {
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Template for the Type properties source file.
+ */
+
+#include "expr/type_properties.h"
+
+namespace cvc5 {
+namespace kind {
+
+Node mkGroundTerm(TypeConstant tc)
+{
+ switch (tc)
+ {
+ // clang-format off
+${type_constant_groundterms}
+ // clang-format on
+ default:
+ InternalError() << "No ground term known for type constant: " << tc;
+ }
+}
+
+Node mkGroundTerm(TypeNode typeNode)
+{
+ AssertArgument(!typeNode.isNull(), typeNode);
+ switch (Kind k = typeNode.getKind())
+ {
+ case TYPE_CONSTANT:
+ return mkGroundTerm(typeNode.getConst<TypeConstant>());
+ // clang-format off
+${type_groundterms}
+ // clang-format on
+ default:
+ InternalError() << "A theory kinds file did not provide a ground term "
+ << "or ground term computer for type:\n"
+ << typeNode << "\nof kind " << k;
+ }
+}
+
+} // namespace kind
+} // namespace cvc5
}
}/* isWellFounded(TypeNode) */
-inline Node mkGroundTerm(TypeConstant tc)
-{
- switch (tc)
- {
- // clang-format off
-${type_constant_groundterms}
- // clang-format on
- default:
- InternalError() << "No ground term known for type constant: " << tc;
- }
-} /* mkGroundTerm(TypeConstant) */
-
-inline Node mkGroundTerm(TypeNode typeNode)
-{
- AssertArgument(!typeNode.isNull(), typeNode);
- switch (Kind k = typeNode.getKind())
- {
- case TYPE_CONSTANT:
- return mkGroundTerm(typeNode.getConst<TypeConstant>());
- // clang-format off
-${type_groundterms}
- // clang-format on
- default:
- InternalError() << "A theory kinds file did not provide a ground term "
- << "or ground term computer for type:\n"
- << typeNode << "\nof kind " << k;
- }
-} /* mkGroundTerm(TypeNode) */
+Node mkGroundTerm(TypeConstant tc);
+Node mkGroundTerm(TypeNode typeNode);
} // namespace kind
} // namespace cvc5
Node ArraysProperties::mkGroundTerm(TypeNode type)
{
Assert(type.getKind() == kind::ARRAY_TYPE);
+ NodeManager* nm = NodeManager::currentNM();
TypeNode elemType = type.getArrayConstituentType();
- Node elem = elemType.mkGroundTerm();
+ Node elem = nm->mkGroundTerm(elemType);
if (elem.isConst())
{
return NodeManager::currentNM()->mkConst(ArrayStoreAll(type, elem));
else if (k == kind::APPLY_SELECTOR_TOTAL)
{
// evaluates to the first ground value of type tn.
- Node gt = tn.mkGroundValue();
+ NodeManager* nm = NodeManager::currentNM();
+ Node gt = nm->mkGroundValue(tn);
Assert(!gt.isNull());
if (tn.isDatatype() && !tn.isInstantiatedDatatype())
{
const DTypeConstructor& dtc = dt[constructorIndex];
int selectorIndex = dtc.getSelectorIndexInternal(selector);
Node r =
- selectorIndex < 0 ? t.getType().mkGroundTerm() : t[0][selectorIndex];
+ selectorIndex < 0 ? nm->mkGroundTerm(t.getType()) : t[0][selectorIndex];
return t.eqNode(r);
}
else if (id == PfRule::DT_SPLIT)
// uninterpreted sorts and arrays, where the solver does not fully
// handle values of the sort. The call to mkGroundTerm does not introduce
// values for these sorts.
- rrs = r.getType().mkGroundTerm();
+ NodeManager* nm = NodeManager::currentNM();
+ rrs = nm->mkGroundTerm(r.getType());
Trace("datatypes-wrong-sel")
<< "Bad apply " << r << " term = " << rrs
- << ", value = " << r.getType().mkGroundValue() << std::endl;
+ << ", value = " << nm->mkGroundValue(r.getType()) << std::endl;
}
else
{
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
Trace("rr-check") << "...rewrite does not hold for: " << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
is_unique_term = true;
std::vector<Node> vars;
d_sampler->getVariables(vars);
if (itf == d_fv_to_skolem.end())
{
// not in conjecture, can use arbitrary value
- val = v.getType().mkGroundTerm();
+ val = nm->mkGroundTerm(v.getType());
}
else
{
else if (type.isArray() || type.isSet())
{
// generate constant array over the first element of the constituent type
- Node c = type.mkGroundTerm();
+ Node c = nm->mkGroundTerm(type);
// note that c should never contain an uninterpreted constant
Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c));
ops.push_back(c);
{
// if there are not constructors yet by this point, which can happen,
// e.g. for unimplemented types that have no variables in the argument
- // list of the function-to-synthesize, create a fresh ground term
- sdts[i].addConstructor(types[i].mkGroundTerm(), "", {});
+ // list of the function-to-synthesize, create a fresh ground term
+ sdts[i].addConstructor(nm->mkGroundTerm(types[i]), "", {});
}
// always add ITE
std::unordered_map<TNode, TNode> subs;
// generate a ground value for each one of those variables
+ NodeManager* nm = NodeManager::currentNM();
for (const TNode& var : vars)
{
- subs.emplace(var, var.getType().mkGroundValue());
+ subs.emplace(var, nm->mkGroundValue(var.getType()));
}
// substitute the variables with ground values
{
if (sol_templ_children[j].isNull())
{
- sol_templ_children[j] = cop_to_sks[cop][j].getType().mkGroundTerm();
+ sol_templ_children[j] =
+ nm->mkGroundTerm(cop_to_sks[cop][j].getType());
}
}
sol_templ_children.insert(sol_templ_children.begin(), cop);
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
// default model
+ NodeManager* nm = NodeManager::currentNM();
for (const Node& v : vars)
{
- modelVals.push_back(v.getType().mkGroundTerm());
+ modelVals.push_back(nm->mkGroundTerm(v.getType()));
}
}
return r;
if (node.getKind() == SEQ_NTH_TOTAL)
{
// return arbitrary term
- Node ret = s.getType().getSequenceElementType().mkGroundValue();
+ NodeManager* nm = NodeManager::currentNM();
+ Node ret = nm->mkGroundValue(s.getType().getSequenceElementType());
return returnRewrite(node, ret, Rewrite::SEQ_NTH_TOTAL_OOB);
}
else
{
// This is called when t is a sort that does not occur in this model.
// Sorts are always interpreted as non-empty, thus we add a single element.
- elements.push_back(tn.mkGroundTerm());
+ NodeManager* nm = NodeManager::currentNM();
+ elements.push_back(nm->mkGroundTerm(tn));
return elements;
}
return *type_refs;
{
NodeManager* nm = NodeManager::currentNM();
Node bvl = nm->getBoundVarListForFunctionType(type);
- Node ret = type.getRangeType().mkGroundTerm();
+ Node ret = nm->mkGroundTerm(type.getRangeType());
return nm->mkNode(kind::LAMBDA, bvl, ret);
}
ASSERT_TRUE(colorsType.getDType().isWellFounded());
Debug("groundterms") << "ground term of " << colorsType.getDType().getName()
<< std::endl
- << " is " << colorsType.mkGroundTerm() << std::endl;
- ASSERT_EQ(colorsType.mkGroundTerm().getType(), colorsType);
+ << " is " << d_nodeManager->mkGroundTerm(colorsType)
+ << std::endl;
+ ASSERT_EQ(d_nodeManager->mkGroundTerm(colorsType).getType(), colorsType);
}
TEST_F(TestUtilBlackDatatype, nat)
ASSERT_TRUE(natType.getDType().isWellFounded());
Debug("groundterms") << "ground term of " << natType.getDType().getName()
<< std::endl
- << " is " << natType.mkGroundTerm() << std::endl;
- ASSERT_TRUE(natType.mkGroundTerm().getType() == natType);
+ << " is " << d_nodeManager->mkGroundTerm(natType)
+ << std::endl;
+ ASSERT_TRUE(d_nodeManager->mkGroundTerm(natType).getType() == natType);
}
TEST_F(TestUtilBlackDatatype, tree)
ASSERT_TRUE(treeType.getDType().isWellFounded());
Debug("groundterms") << "ground term of " << treeType.getDType().getName()
<< std::endl
- << " is " << treeType.mkGroundTerm() << std::endl;
- ASSERT_TRUE(treeType.mkGroundTerm().getType() == treeType);
+ << " is " << d_nodeManager->mkGroundTerm(treeType)
+ << std::endl;
+ ASSERT_TRUE(d_nodeManager->mkGroundTerm(treeType).getType() == treeType);
}
TEST_F(TestUtilBlackDatatype, list_int)
ASSERT_TRUE(listType.getDType().isWellFounded());
Debug("groundterms") << "ground term of " << listType.getDType().getName()
<< std::endl
- << " is " << listType.mkGroundTerm() << std::endl;
- ASSERT_TRUE(listType.mkGroundTerm().getType() == listType);
+ << " is " << d_nodeManager->mkGroundTerm(listType)
+ << std::endl;
+ ASSERT_TRUE(d_nodeManager->mkGroundTerm(listType).getType() == listType);
}
TEST_F(TestUtilBlackDatatype, list_real)
ASSERT_TRUE(listType.getDType().isWellFounded());
Debug("groundterms") << "ground term of " << listType.getDType().getName()
<< std::endl
- << " is " << listType.mkGroundTerm() << std::endl;
- ASSERT_TRUE(listType.mkGroundTerm().getType() == listType);
+ << " is " << d_nodeManager->mkGroundTerm(listType)
+ << std::endl;
+ ASSERT_TRUE(d_nodeManager->mkGroundTerm(listType).getType() == listType);
}
TEST_F(TestUtilBlackDatatype, list_boolean)
ASSERT_TRUE(listType.getDType().isWellFounded());
Debug("groundterms") << "ground term of " << listType.getDType().getName()
<< std::endl
- << " is " << listType.mkGroundTerm() << std::endl;
- ASSERT_TRUE(listType.mkGroundTerm().getType() == listType);
+ << " is " << d_nodeManager->mkGroundTerm(listType)
+ << std::endl;
+ ASSERT_TRUE(d_nodeManager->mkGroundTerm(listType).getType() == listType);
}
TEST_F(TestUtilBlackDatatype, listIntUpdate)
TypeNode listType = d_nodeManager->mkDatatypeType(list);
const DType& ldt = listType.getDType();
Node updater = ldt[0][0].getUpdater();
- Node gt = listType.mkGroundTerm();
+ Node gt = d_nodeManager->mkGroundTerm(listType);
Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
Node truen = d_nodeManager->mkConst(true);
// construct an update term
ASSERT_TRUE(dtts[0].getDType().isWellFounded());
Debug("groundterms") << "ground term of " << dtts[0].getDType().getName()
<< std::endl
- << " is " << dtts[0].mkGroundTerm() << std::endl;
- ASSERT_TRUE(dtts[0].mkGroundTerm().getType() == dtts[0]);
+ << " is " << d_nodeManager->mkGroundTerm(dtts[0])
+ << std::endl;
+ ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts[0]).getType() == dtts[0]);
ASSERT_FALSE(dtts[1].getDType().isFinite());
ASSERT_TRUE(dtts[1].getDType().getCardinality().compare(Cardinality::INTEGERS)
ASSERT_TRUE(dtts[1].getDType().isWellFounded());
Debug("groundterms") << "ground term of " << dtts[1].getDType().getName()
<< std::endl
- << " is " << dtts[1].mkGroundTerm() << std::endl;
- ASSERT_TRUE(dtts[1].mkGroundTerm().getType() == dtts[1]);
+ << " is " << d_nodeManager->mkGroundTerm(dtts[1])
+ << std::endl;
+ ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts[1]).getType() == dtts[1]);
}
TEST_F(TestUtilBlackDatatype, mutual_list_trees2)
ASSERT_TRUE(dtts2[0].getDType().isWellFounded());
Debug("groundterms") << "ground term of " << dtts2[0].getDType().getName()
<< std::endl
- << " is " << dtts2[0].mkGroundTerm() << std::endl;
- ASSERT_TRUE(dtts2[0].mkGroundTerm().getType() == dtts2[0]);
+ << " is " << d_nodeManager->mkGroundTerm(dtts2[0])
+ << std::endl;
+ ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts2[0]).getType() == dtts2[0]);
ASSERT_FALSE(dtts2[1].getDType().isParametric());
ASSERT_FALSE(dtts2[1].getDType().isFinite());
ASSERT_TRUE(dtts2[1].getDType().isWellFounded());
Debug("groundterms") << "ground term of " << dtts2[1].getDType().getName()
<< std::endl
- << " is " << dtts2[1].mkGroundTerm() << std::endl;
- ASSERT_TRUE(dtts2[1].mkGroundTerm().getType() == dtts2[1]);
+ << " is " << d_nodeManager->mkGroundTerm(dtts2[1])
+ << std::endl;
+ ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts2[1]).getType() == dtts2[1]);
}
TEST_F(TestUtilBlackDatatype, not_so_well_founded)
treeType.getDType().getCardinality().compare(Cardinality::INTEGERS)
== Cardinality::EQUAL);
ASSERT_FALSE(treeType.getDType().isWellFounded());
- ASSERT_TRUE(treeType.mkGroundTerm().isNull());
+ ASSERT_TRUE(d_nodeManager->mkGroundTerm(treeType).isNull());
ASSERT_TRUE(treeType.getDType().mkGroundTerm(treeType).isNull());
}
projects / cvc5.git / commitdiff