More

src/theory/builtin/generic_op.cpp

@@ -23,6 +23,7 @@
 #include "theory/datatypes/project_op.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "util/bitvector.h"
+#include "util/divisible.h"
 #include "util/floatingpoint.h"
 #include "util/iand.h"
 #include "util/rational.h"
@@ -55,7 +56,7 @@ bool GenericOp::operator==(const GenericOp& op) const
 
 bool GenericOp::isNumeralIndexedOperatorKind(Kind k)
 {
-  return k == Kind::REGEXP_LOOP || k == Kind::BITVECTOR_EXTRACT
+  return k == Kind::DIVISIBLE || k == Kind::REGEXP_LOOP || k == Kind::BITVECTOR_EXTRACT
          || k == Kind::BITVECTOR_REPEAT || k == Kind::BITVECTOR_ZERO_EXTEND
          || k == Kind::BITVECTOR_SIGN_EXTEND || k == Kind::BITVECTOR_ROTATE_LEFT
          || k == Kind::BITVECTOR_ROTATE_RIGHT || k == Kind::INT_TO_BITVECTOR
@@ -86,6 +87,12 @@ std::vector<Node> GenericOp::getIndicesForOperator(Kind k, Node n)
   std::vector<Node> indices;
   switch (k)
   {
+    case Kind::DIVISIBLE:
+    {
+      const Divisible& op = n.getConst<Divisible>();
+      indices.push_back(nm->mkConstInt(Rational(op.k)));
+      break;
+    }
     case Kind::REGEXP_LOOP:
     {
       const RegExpLoop& op = n.getConst<RegExpLoop>();
@@ -283,6 +290,9 @@ Node GenericOp::getOperatorForIndices(NodeManager* nm,
     }
     switch (k)
     {
+      case Kind::DIVISIBLE:
+        Assert(numerals.size() == 1);
+        return nm->mkConst(Divisible(numerals[0]));
       case Kind::REGEXP_LOOP:
         Assert(numerals.size() == 2);
         return nm->mkConst(RegExpLoop(numerals[0], numerals[1]));