Expr op = ..."f"...
em.mkExpr(op, children);
Operator kinds are automatically associated with the enclosing expression kind in the DSL and generated.
"basic types"
operator FUNCTION_TYPE 2: "function type"
variable SORT_TYPE "sort type"
+
+constant BITVECTOR_TYPE \
+ unsigned \
+ ::CVC4::UnsignedHashStrategy \
+ "util/bitvector.h" \
+ "bit-vector type"
+
\ No newline at end of file
return Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()));
}
+BitVectorType ExprManager::bitVectorType(unsigned size) const {
+ NodeManagerScope nms(d_nodeManager);
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->bitVectorType(size)));
+}
+
Expr ExprManager::mkExpr(Kind kind) {
const unsigned n = 0;
CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
}
+Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
+ const unsigned n = children.size();
+ Kind kind = kind::operatorKindToKind(opExpr.getKind());
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+
+ NodeManagerScope nms(d_nodeManager);
+
+ vector<Node> nodes;
+ vector<Expr>::const_iterator it = children.begin();
+ vector<Expr>::const_iterator it_end = children.end();
+ while(it != it_end) {
+ nodes.push_back(it->getNode());
+ ++it;
+ }
+ return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
+}
+
/** Make a function type from domain to range. */
FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) {
NodeManagerScope nms(d_nodeManager);
/** Get the type for integers */
IntegerType integerType() const;
+ /** The the type for bit-vectors */
+ BitVectorType bitVectorType(unsigned size) const;
+
/**
* Make a unary expression of a given kind (TRUE, FALSE,...).
* @param kind the kind of expression
*/
Expr mkExpr(Kind kind, const std::vector<Expr>& children);
+ /**
+ * Make an n-ary expression of given tre operator to appply and a vector of
+ * it's children
+ * @param opExpr the operator expression
+ * @param children the subexpressions
+ * @return the n-ary expression
+ */
+ Expr mkExpr(Expr opExpr, const std::vector<Expr>& children);
+
/** Create a constant of type T */
template <class T>
Expr mkConst(const T&);
return canBeAtomic[k];
}/* kindCanBeAtomic(k) */
+
+/**
+ * Map a kind of the operator to the kind of the enclosing expression. For
+ * example, since the kind of functions is just VARIABLE, it should map
+ * VARIABLE to APPLY_UF.
+ */
+static inline Kind operatorKindToKind(Kind k) {
+ static const Kind kind2kind[] = {
+ kind::UNDEFINED_KIND, /* NULL_EXPR */
+${metakind_operatorKinds}
+ kind::UNDEFINED_KIND /* LAST_KIND */
+ };
+
+ return kind2kind[k];
+}
}/* CVC4::kind namespace */
namespace expr {
}
function parameterized {
- # parameterized K #children ["comment"]
+ # parameterized K1 K2 #children ["comment"]
lineno=${BASH_LINENO[0]}
check_theory_seen
- register_kind "$1" "$2" "$3"
+ register_kind "$1" "$3" "$4"
}
function constant {
metakind_constPrinters=
metakind_ubchildren=
metakind_lbchildren=
+metakind_operatorKinds=
seen_theory=false
seen_theory_builtin=false
lineno=${BASH_LINENO[0]}
check_theory_seen
- register_metakind VARIABLE "$1" 0
+ register_metakind VARIABLE "$1" UNDEFINED_KIND 0
}
function operator {
lineno=${BASH_LINENO[0]}
check_theory_seen
- register_metakind OPERATOR "$1" "$2"
+ register_metakind OPERATOR "$1" UNDEFINED_KIND "$2"
}
function nonatomic_operator {
lineno=${BASH_LINENO[0]}
check_theory_seen
- register_metakind NONATOMIC_OPERATOR "$1" "$2"
+ register_metakind NONATOMIC_OPERATOR "$1" UNDEFINED_KIND "$2"
}
function parameterized {
- # parameterized K #children ["comment"]
+ # parameterized K1 K2 #children ["comment"]
lineno=${BASH_LINENO[0]}
check_theory_seen
- register_metakind PARAMETERIZED "$1" "$2"
+ register_metakind PARAMETERIZED "$1" "$2" "$3"
}
function constant {
metakind_includes="${metakind_includes}
#include \"$4\""
fi
- register_metakind CONSTANT "$1" 0
+ register_metakind CONSTANT "$1" UNDEFINED_KIND 0
metakind_constantMaps="${metakind_constantMaps}
}/* CVC4::kind::metakind namespace */
}/* CVC4::kind namespace */
function register_metakind {
mk=$1
k=$2
- nc=$3
+ k1=$3
+ nc=$4
+
+ metakind_operatorKinds="${metakind_operatorKinds} kind::$k1, /* $k */
+";
if [ $mk = NONATOMIC_OPERATOR ]; then
metakind_canbeatomic="${metakind_canbeatomic} false, /* $k */
"
metakind_canbeatomic="${metakind_canbeatomic}
/* from $b */
+"
+ metakind_operatorKinds="${metakind_operatorKinds}
+ /* from $b */
"
source "$kf"
check_theory_seen
metakind_constHashes \
metakind_constPrinters \
metakind_ubchildren \
- metakind_lbchildren; do
+ metakind_lbchildren \
+ metakind_operatorKinds; do
eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
error=`expr "$text" : '.*\${\([^}]*\)}.*'`
template <bool ref_count>
Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
+ /** Create a node by applying an operator to the children */
+ template <bool ref_count>
+ Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
+ template <bool ref_count>
+ Node* mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
+
/**
* Create a variable with the given name and type. NOTE that no
* lookup is done on the name. If you mkVar("a", type) and then
/** Get the (singleton) type for sorts. */
inline TypeNode kindType();
+ /** Get the type of bitvectors of size <code>size</code> */
+ inline TypeNode bitVectorType(unsigned size);
+
/**
* Make a function type from domain to range.
*
return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
}
+inline TypeNode NodeManager::bitVectorType(unsigned size) {
+ return TypeNode(mkTypeConst<unsigned>(kind::BITVECTOR_TYPE));
+}
+
/** Make a function type from domain to range. */
inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
std::vector<TypeNode> sorts;
return NodeBuilder<>(this, kind).append(children).constructNodePtr();
}
+// N-ary version for operators
+template <bool ref_count>
+inline Node NodeManager::mkNode(TNode opNode,
+ const std::vector<NodeTemplate<ref_count> >&
+ children) {
+ Assert(kind::metaKindOf(opNode.getKind()) == kind::metakind::PARAMETERIZED);
+ return NodeBuilder<>(this, kind::operatorKindToKind(opNode.getKind())).append(children);
+}
+
+template <bool ref_count>
+inline Node* NodeManager::mkNodePtr(TNode opNode,
+ const std::vector<NodeTemplate<ref_count> >&
+ children) {
+ return NodeBuilder<>(this, kind::operatorKindToKind(opNode.getKind())).constructNodePtr();
+}
+
+
// N-ary version for types
inline TypeNode NodeManager::mkTypeNode(Kind kind, const std::vector<TypeNode>& children) {
return NodeBuilder<>(this, kind).append(children).constructTypeNode();
return d_typeNode->isInteger();
}
-/** Cast to a integer type */
+/** Cast to a real type */
Type::operator RealType() const throw (AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isReal());
return RealType(*this);
}
+/** Is this the bit-vector type? */
+bool Type::isBitVector() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->isBitVector();
+}
+
+/** Cast to a bit-vector type */
+Type::operator BitVectorType() const throw (AssertionException) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert(isBitVector());
+ return BitVectorType(*this);
+}
+
/** Is this a function type? */
bool Type::isFunction() const {
NodeManagerScope nms(d_nodeManager);
Assert(isReal());
}
+BitVectorType::BitVectorType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+ Assert(isBitVector());
+}
+
FunctionType::FunctionType(const Type& t) throw (AssertionException)
: Type(t)
{
}
+unsigned BitVectorType::getSize() const {
+ return d_typeNode->getBitVectorSize();
+}
+
}/* CVC4 namespace */
class BooleanType;
class IntegerType;
class RealType;
+class BitVectorType;
class FunctionType;
class KindType;
class SortType;
*/
operator RealType() const throw (AssertionException);
+ /**
+ * Is this the bit-vector type?
+ * @return true if the type is a bit-vector type
+ */
+ bool isBitVector() const;
+
+ /**
+ * Cast this type to a bit-vector type
+ * @return the BitVectorType
+ */
+ operator BitVectorType() const throw (AssertionException);
+
/**
* Is this a function type?
* @return true if the type is a Boolean type
KindType(const Type& type) throw (AssertionException);
};
+
+/**
+ * Class encapsulating the bit-vector type.
+ */
+class CVC4_PUBLIC BitVectorType : public Type {
+
+public:
+
+ /** Construct from the base type */
+ BitVectorType(const Type& type) throw (AssertionException);
+
+ /**
+ * Returns the size of the bit-vector type.
+ * @return the width of the bit-vector type (> 0)
+ */
+ unsigned getSize() const;
+};
+
/**
* Output operator for types
* @param out the stream to output to
return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == KIND_TYPE;
}
+/** Is this a bit-vector type */
+bool TypeNode::isBitVector() const {
+ return getKind() == kind::BITVECTOR_TYPE;
+}
+
+/** Is this a bit-vector type of size <code>size</code> */
+bool TypeNode::isBitVector(unsigned size) const {
+ return getKind() == kind::BITVECTOR_TYPE && getConst<unsigned>() == size;
+}
+
+/** Get the size of this bit-vector type */
+unsigned TypeNode::getBitVectorSize() const {
+ Assert(isBitVector());
+ return getConst<unsigned>();
+}
+
+
}/* CVC4 namespace */
function types. */
bool isPredicate() const;
+ /** Is this a bit-vector type */
+ bool isBitVector() const;
+
+ /** Is this a bit-vector type of size <code>size</code> */
+ bool isBitVector(unsigned size) const;
+
+ /** Get the size of this bit-vector type */
+ unsigned getBitVectorSize() const;
+
/** Is this a sort kind */
bool isSort() const;
** A collection of state for use by parser implementations.
**/
-#include "cvc4parser_private.h"
+#include "cvc4parser_public.h"
#ifndef __CVC4__PARSER__PARSER_STATE_H
#define __CVC4__PARSER__PARSER_STATE_H
Kind kind;
std::string name;
std::vector<Expr> args; /* = getExprVector(); */
+ Expr op; /* Operator expression FIXME: move away kill it */
}
: /* a built-in operator application */
LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK
// Semantic predicate not necessary if parenthesized subexpressions
// are disallowed
- // { isFunction(LT(2)->getText()) }?
-
+ // { isFunction(LT(2)->getText()) }?
LPAREN_TOK
- functionSymbol[expr]
- { args.push_back(expr); }
+ parameterizedOperator[op]
annotatedFormulas[args,expr] RPAREN_TOK
// TODO: check arity
- { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); }
+ { expr = MK_EXPR(op,args); }
| /* An ite expression */
LPAREN_TOK ITE_TOK
| STAR_TOK { $kind = CVC4::kind::MULT; }
| TILDE_TOK { $kind = CVC4::kind::UMINUS; }
| MINUS_TOK { $kind = CVC4::kind::MINUS; }
+ // Bit-vectors
// NOTE: Theory operators go here
/* TODO: lt, gt, plus, minus, etc. */
;
+/**
+ * Matches an operator.
+ */
+parameterizedOperator[CVC4::Expr& op]
+ : functionSymbol[op]
+ ;
+
/**
* Matches a (possibly undeclared) predicate identifier (returning the string).
* @param check what kind of check to do with the symbol
::CVC4::BitVector \
::CVC4::BitVectorHashStrategy \
"util/bitvector.h" \
- "a fixed-width bit-vector constant"
\ No newline at end of file
+ "a fixed-width bit-vector constant"
+
+operator BITVECTOR_CONCAT 2 "bit-vector concatenation"
+constant BITVECTOR_EXTRACT_OP \
+ ::CVC4::BitVectorExtract \
+ ::CVC4::BitVectorExtractHashStrategy \
+ "util/bitvector.h" \
+ "operator for the bit-vector extract"
+
+parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 2 "disequality"
+
+
+
+
\ No newline at end of file
theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"
-parameterized APPLY_UF 1: "uninterpreted function application"
+parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
return os << bv.toString();
}
+std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
+ return os << "[" << bv.high << ":" << bv.low << "]";
+}
+
}
}
};
+/**
+ * Hash function for the BitVector constants.
+ */
struct BitVectorHashStrategy {
static inline size_t hash(const BitVector& bv) {
return bv.hash();
}
};
-std::ostream& operator <<(std::ostream& os, const BitVector& bv);
+/**
+ * The structure representing the extraction operation for bit-vectors. The
+ * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
+ * by taking the bits at indices <code>high ... low</code>
+ */
+struct BitVectorExtract {
+ /** The high bit of the range for this extract */
+ unsigned high;
+ /** The low bit of the range for this extract */
+ unsigned low;
+
+ bool operator == (const BitVectorExtract& extract) const {
+ return high == extract.high && low == extract.low;
+ }
+};
+/**
+ * Hash function for the BitVectorExtract objects.
+ */
+class BitVectorExtractHashStrategy {
+public:
+ static size_t hash(const BitVectorExtract& extract) {
+ size_t hash = extract.low;
+ hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
+ return hash;
+ }
+};
+
+/**
+ * Hash function for the unsigned integers.
+ */
+struct UnsignedHashStrategy {
+ static inline size_t hash(unsigned x) {
+ return (size_t)x;
+ }
+};
+
+std::ostream& operator <<(std::ostream& os, const BitVector& bv);
+std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv);
}
projects / cvc5.git / commitdiff