Added the capability to construct expressions by passing the operator instead of the kind, i.e.

Expr op = ..."f"...
em.mkExpr(op, children);

Operator kinds are automatically associated with the enclosing expression kind in the DSL and generated.

17 files changed, 263 insertions, 20 deletions

diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds
index eb41c788e..1c24b045c 100644
--- a/src/expr/builtin_kinds
+++ b/src/expr/builtin_kinds
@@ -128,3 +128,10 @@ constant TYPE_CONSTANT \
     "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
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 3480cc0e6..b957019fb 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -66,6 +66,11 @@ IntegerType ExprManager::integerType() const {
   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,
@@ -161,6 +166,27 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
   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);
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 5ef6ef984..b3a1b68df 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -96,6 +96,9 @@ public:
   /** 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
@@ -163,6 +166,15 @@ public:
    */
   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&);
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index fda2801be..57bfc51e5 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -141,6 +141,21 @@ ${metakind_canbeatomic}
   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 {
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 294dc5d7e..d9c64b660 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -93,12 +93,12 @@ function nonatomic_operator {
 }
 
 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 {
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 84d18e218..e8f3724f1 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -46,6 +46,7 @@ metakind_constHashes=
 metakind_constPrinters=
 metakind_ubchildren=
 metakind_lbchildren=
+metakind_operatorKinds=
 
 seen_theory=false
 seen_theory_builtin=false
@@ -86,7 +87,7 @@ function variable {
   lineno=${BASH_LINENO[0]}
 
   check_theory_seen
-  register_metakind VARIABLE "$1" 0
+  register_metakind VARIABLE "$1" UNDEFINED_KIND 0
 }
 
 function operator {
@@ -95,7 +96,7 @@ function operator {
   lineno=${BASH_LINENO[0]}
 
   check_theory_seen
-  register_metakind OPERATOR "$1" "$2"
+  register_metakind OPERATOR "$1" UNDEFINED_KIND "$2"
 }
 
 function nonatomic_operator {
@@ -104,16 +105,16 @@ 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 {
@@ -141,7 +142,7 @@ 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 */
@@ -206,7 +207,11 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
 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 */
@@ -290,6 +295,9 @@ while [ $# -gt 0 ]; do
   metakind_canbeatomic="${metakind_canbeatomic}
     /* from $b */
 "
+  metakind_operatorKinds="${metakind_operatorKinds}
+    /* from $b */
+"
   source "$kf"
   check_theory_seen
   shift
@@ -308,7 +316,8 @@ for var in \
     metakind_constHashes \
     metakind_constPrinters \
     metakind_ubchildren \
-    metakind_lbchildren; do
+    metakind_lbchildren \
+    metakind_operatorKinds; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
 error=`expr "$text" : '.*\${\([^}]*\)}.*'`
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 39c1c91b9..ab8199d1e 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -285,6 +285,12 @@ public:
   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
@@ -454,6 +460,9 @@ public:
   /** 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.
    *
@@ -624,6 +633,10 @@ inline TypeNode NodeManager::kindType() {
   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;
@@ -845,6 +858,23 @@ inline Node* NodeManager::mkNodePtr(Kind kind,
   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();
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index c76349fe3..faadfb0a6 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -120,13 +120,26 @@ bool Type::isReal() const {
   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);
@@ -214,6 +227,12 @@ RealType::RealType(const Type& t) throw (AssertionException)
   Assert(isReal());
 }
 
+BitVectorType::BitVectorType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+  Assert(isBitVector());
+}
+
 FunctionType::FunctionType(const Type& t) throw (AssertionException)
 : Type(t)
 {
@@ -233,4 +252,8 @@ SortType::SortType(const Type& t) throw (AssertionException)
 }
 
 
+unsigned BitVectorType::getSize() const {
+  return d_typeNode->getBitVectorSize();
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/type.h b/src/expr/type.h
index c61b67f77..f513ef5de 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -34,6 +34,7 @@ class TypeNode;
 class BooleanType;
 class IntegerType;
 class RealType;
+class BitVectorType;
 class FunctionType;
 class KindType;
 class SortType;
@@ -153,6 +154,18 @@ public:
   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
    */
@@ -278,6 +291,24 @@ public:
   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
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 08e50844b..b935c837e 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -67,4 +67,21 @@ bool TypeNode::isKind() const {
   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 */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 12df5513f..1d32fffda 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -314,6 +314,15 @@ public:
       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;
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index a84021c10..f56ec03ac 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -13,7 +13,7 @@
  ** 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
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 2dd680f09..5cd94ec0d 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -178,6 +178,7 @@ annotatedFormula[CVC4::Expr& expr]
   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 
@@ -195,14 +196,12 @@ annotatedFormula[CVC4::Expr& expr]
 
     // 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 
@@ -283,11 +282,19 @@ builtinOp[CVC4::Kind& kind]
   | 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
  */
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 8a4c6b6f7..aeb425474 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -10,4 +10,17 @@ constant CONST_BITVECTOR \
     ::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
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 8cbf975f2..f95bfb582 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -6,4 +6,4 @@
 
 theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"
 
-parameterized APPLY_UF 1: "uninterpreted function application"
+parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index bea06f71a..125065118 100644
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -13,4 +13,8 @@ std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
   return os << bv.toString();
 }
 
+std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
+  return os << "[" << bv.high << ":" << bv.low << "]";
+}
+
 }
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 3859fa407..e1c0131d9 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -85,14 +85,54 @@ public:
   }
 };
 
+/**
+ * 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);
 }