Native support for non-core evaluation operators

src/cmd_parser.cpp

@@ -828,15 +828,15 @@ bool CmdParser::parseNextCommand()
       if (concType.getKind() != Kind::PROOF_TYPE)
       {
         std::stringstream ss;
-        ss << "Non-proof conclusion for step, got " << concType;
+        ss << "Non-proof conclusion for rule " << ruleName << ", got " << concType;
         d_lex.parseError(ss.str());
       }
       if (!proven.isNull())
       {
         if (concType[0]!=proven)
         {
           std::stringstream ss;
-          ss << "Unexpected conclusion for step " << ruleName << ":" << std::endl;
+          ss << "Unexpected conclusion for rule " << ruleName << ":" << std::endl;
           ss << "    Proves: " << concType << std::endl;
           ss << "  Expected: (Proof " << proven << ")";
           d_lex.parseError(ss.str());

src/kind.cpp

@@ -54,6 +54,13 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::EVAL_VAR: o << "EVAL_VAR"; break;
     case Kind::EVAL_TYPE_OF: o << "EVAL_TYPE_OF"; break;
     case Kind::EVAL_NAME_OF: o << "EVAL_NAME_OF"; break;
+    case Kind::EVAL_COMPARE: o << "EVAL_COMPARE"; break;
+    case Kind::EVAL_IS_Z: o << "EVAL_IS_Z"; break;
+    case Kind::EVAL_IS_Q: o << "EVAL_IS_Q"; break;
+    case Kind::EVAL_IS_BIN: o << "EVAL_IS_BIN"; break;
+    case Kind::EVAL_IS_STR: o << "EVAL_IS_STR"; break;
+    case Kind::EVAL_IS_BOOL: o << "EVAL_IS_BOOL"; break;
+    case Kind::EVAL_IS_VAR: o << "EVAL_IS_VAR"; break;
     // lists
     case Kind::EVAL_NIL: o << "EVAL_NIL";break;
     case Kind::EVAL_CONS: o << "EVAL_CONS"; break;
@@ -74,6 +81,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::EVAL_INT_MOD: o << "EVAL_INT_MOD"; break;
     case Kind::EVAL_RAT_DIV: o << "EVAL_RAT_DIV"; break;
     case Kind::EVAL_IS_NEG: o << "EVAL_IS_NEG"; break;
+    case Kind::EVAL_GT: o << "EVAL_GT"; break;
     // strings
     case Kind::EVAL_LENGTH: o << "EVAL_LENGTH"; break;
     case Kind::EVAL_CONCAT: o << "EVAL_CONCAT"; break;
@@ -122,6 +130,13 @@ std::string kindToTerm(Kind k)
         case Kind::EVAL_VAR: ss << "var"; break;
         case Kind::EVAL_TYPE_OF: ss << "typeof"; break;
         case Kind::EVAL_NAME_OF: ss << "nameof"; break;
+        case Kind::EVAL_COMPARE: ss << "cmp"; break;
+        case Kind::EVAL_IS_Z: ss << "is_z"; break;
+        case Kind::EVAL_IS_Q: ss << "is_q"; break;
+        case Kind::EVAL_IS_BIN: ss << "is_bin"; break;
+        case Kind::EVAL_IS_STR: ss << "is_str"; break;
+        case Kind::EVAL_IS_BOOL: ss << "is_bool"; break;
+        case Kind::EVAL_IS_VAR: ss << "is_var"; break;
         // lists
         case Kind::EVAL_NIL: ss << "nil"; break;
         case Kind::EVAL_CONS: ss << "cons"; break;
@@ -204,6 +219,13 @@ bool isLiteralOp(Kind k)
     case Kind::EVAL_VAR:
     case Kind::EVAL_TYPE_OF:
     case Kind::EVAL_NAME_OF:
+    case Kind::EVAL_COMPARE:
+    case Kind::EVAL_IS_Z:
+    case Kind::EVAL_IS_Q:
+    case Kind::EVAL_IS_BIN:
+    case Kind::EVAL_IS_STR:
+    case Kind::EVAL_IS_BOOL:
+    case Kind::EVAL_IS_VAR:
     // lists
     case Kind::EVAL_NIL:
     case Kind::EVAL_CONS:
@@ -224,6 +246,7 @@ bool isLiteralOp(Kind k)
     case Kind::EVAL_INT_MOD:
     case Kind::EVAL_RAT_DIV:
     case Kind::EVAL_IS_NEG:
+    case Kind::EVAL_GT:
     // strings
     case Kind::EVAL_LENGTH:
     case Kind::EVAL_CONCAT:

src/kind.h

@@ -64,6 +64,13 @@ enum class Kind
   EVAL_VAR,
   EVAL_TYPE_OF,
   EVAL_NAME_OF,
+  EVAL_COMPARE,
+  EVAL_IS_Z,
+  EVAL_IS_Q,
+  EVAL_IS_BIN,
+  EVAL_IS_STR,
+  EVAL_IS_BOOL,
+  EVAL_IS_VAR,
   // lists
   EVAL_NIL,
   EVAL_CONS,
@@ -84,6 +91,7 @@ enum class Kind
   EVAL_INT_MOD,
   EVAL_RAT_DIV,
   EVAL_IS_NEG,
+  EVAL_GT,
   // strings
   EVAL_LENGTH,
   EVAL_CONCAT,

src/literal.cpp

@@ -453,6 +453,20 @@ Literal Literal::evaluate(Kind k, const std::vector<const Literal*>& args)
         default: break;
       }
       break;
+    case Kind::EVAL_GT:
+      switch (ka)
+      {
+        case Kind::NUMERAL:
+          return Literal(args[0]->d_int>args[0]->d_int);
+        case Kind::DECIMAL:
+        case Kind::RATIONAL:
+          return Literal(args[0]->d_rat>args[0]->d_rat);
+        case Kind::HEXADECIMAL:
+        case Kind::BINARY:
+          return Literal(args[0]->d_bv.toInteger()>args[0]->d_bv.toInteger());
+        default: break;
+      }
+      break;
     case Kind::EVAL_FIND:
       switch (ka)
       {

src/state.cpp

@@ -55,7 +55,13 @@ State::State(Options& opts, Stats& stats)
   bindBuiltinEval("nameof", Kind::EVAL_NAME_OF);
   bindBuiltinEval("typeof", Kind::EVAL_TYPE_OF);
   bindBuiltinEval("var", Kind::EVAL_VAR);
-  // TODO: compare?
+  bindBuiltinEval("cmp", Kind::EVAL_COMPARE);
+  bindBuiltinEval("is_z", Kind::EVAL_IS_Z);
+  bindBuiltinEval("is_q", Kind::EVAL_IS_Q);
+  bindBuiltinEval("is_bin", Kind::EVAL_IS_BIN);
+  bindBuiltinEval("is_str", Kind::EVAL_IS_STR);
+  bindBuiltinEval("is_bool", Kind::EVAL_IS_BOOL);
+  bindBuiltinEval("is_var", Kind::EVAL_IS_VAR);
   // lists
   bindBuiltinEval("nil", Kind::EVAL_NIL);
   bindBuiltinEval("cons", Kind::EVAL_CONS);
@@ -80,6 +86,7 @@ State::State(Options& opts, Stats& stats)
   bindBuiltinEval("to_q", Kind::EVAL_TO_RAT);
   bindBuiltinEval("to_bin", Kind::EVAL_TO_BIN);
   bindBuiltinEval("to_str", Kind::EVAL_TO_STRING);
+  bindBuiltinEval("gt", Kind::EVAL_GT);
   // strings
   bindBuiltinEval("len", Kind::EVAL_LENGTH);
   bindBuiltinEval("concat", Kind::EVAL_CONCAT);

src/type_checker.cpp

@@ -141,6 +141,8 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
     case Kind::EVAL_RAT_DIV:
     case Kind::EVAL_TO_BIN:
     case Kind::EVAL_FIND:
+    case Kind::EVAL_COMPARE:
+    case Kind::EVAL_GT:
     case Kind::EVAL_LIST_LENGTH:
       ret = (nargs==2);
       break;
@@ -166,6 +168,12 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
     case Kind::EVAL_TO_INT:
     case Kind::EVAL_TO_RAT:
     case Kind::EVAL_TO_STRING:
+    case Kind::EVAL_IS_Z:
+    case Kind::EVAL_IS_Q:
+    case Kind::EVAL_IS_BIN:
+    case Kind::EVAL_IS_STR:
+    case Kind::EVAL_IS_BOOL:
+    case Kind::EVAL_IS_VAR:
       ret = (nargs==1);
       break;
     case Kind::EVAL_NIL:
@@ -1076,6 +1084,48 @@ Expr TypeChecker::evaluateLiteralOpInternal(
       return d_null;
     }
     break;
+    case Kind::EVAL_COMPARE:
+    {
+      if (args[0]->isGround() && args[1]->isGround())
+      {
+        size_t h1 = d_state.getHash(args[0]);
+        size_t h2 = d_state.getHash(args[1]);
+        Literal lb(h1>h2);
+        return Expr(d_state.mkLiteralInternal(lb));
+      }
+      return d_null;
+    }
+    break;
+    case Kind::EVAL_IS_Z:
+    {
+      Literal lb(args[0]->getKind()==Kind::NUMERAL);
+      return Expr(d_state.mkLiteralInternal(lb));
+    }
+    case Kind::EVAL_IS_Q:
+    {
+      Literal lb(args[0]->getKind()==Kind::RATIONAL);
+      return Expr(d_state.mkLiteralInternal(lb));
+    }
+    case Kind::EVAL_IS_BIN:
+    {
+      Literal lb(args[0]->getKind()==Kind::BINARY);
+      return Expr(d_state.mkLiteralInternal(lb));
+    }
+    case Kind::EVAL_IS_STR:
+    {
+      Literal lb(args[0]->getKind()==Kind::STRING);
+      return Expr(d_state.mkLiteralInternal(lb));
+    }
+    case Kind::EVAL_IS_BOOL:
+    {
+      Literal lb(args[0]->getKind()==Kind::BOOLEAN);
+      return Expr(d_state.mkLiteralInternal(lb));
+    }
+    case Kind::EVAL_IS_VAR:
+    {
+      Literal lb(args[0]->getKind()==Kind::VARIABLE);
+      return Expr(d_state.mkLiteralInternal(lb));
+    }
     case Kind::EVAL_TYPE_OF:
     {
       // get the type if ground
@@ -1358,6 +1408,13 @@ ExprValue* TypeChecker::getLiteralOpType(Kind k,
       return childTypes[0];
     case Kind::EVAL_IS_EQ:
     case Kind::EVAL_IS_NEG:
+    case Kind::EVAL_COMPARE:
+    case Kind::EVAL_IS_Z:
+    case Kind::EVAL_IS_Q:
+    case Kind::EVAL_IS_BIN:
+    case Kind::EVAL_IS_STR:
+    case Kind::EVAL_IS_BOOL:
+    case Kind::EVAL_IS_VAR:
       return d_state.mkBoolType().getValue();
     case Kind::EVAL_HASH:
     case Kind::EVAL_INT_DIV:

src/util/rational.h

@@ -100,6 +100,10 @@ class Rational
   {
     return Rational(d_value / y.d_value);
   }
+  bool operator>(const Rational& y) const
+  {
+    return d_value > y.d_value;
+  }
 
   bool isIntegral() const;
 

user_manual.md

@@ -474,6 +474,11 @@ We say a *bitwise value* is a binary or hexadecimal value.
 A 32-bit numeral value is a numeral value between `0` and `2^32-1`.
 Binary values are considered to be in little endian form.
 
+Some of the following operators can be defined in terms of the other operators.
+For these operators, we provide the equivalent formulation.
+A signature defining these files can be found in [non-core-eval](#non-core-eval).
+Note however that the evaluation of these operators is handled by more efficient methods internally in the ALF checker, that is, they are not treated as syntax sugar internally.
+
 Core operators:
 - `(alf.is_eq t1 t2)`
     - Returns `true` if `t1` is (syntactically) equal to `t2`, or `false` if `t1` and `t2` are distinct and ground. Otherwise, it does not evaluate.
@@ -489,7 +494,21 @@ Core operators:
     - If `t1` is a ground constant or variable, this returns the name of `t1`, i.e. the string corresponding to the symbol it was declared with.
 - `(alf.var t1 t2)`
     - If `t1` is a string value and `t2` is ground type, this returns the variable whose name is `t1` and whose type is `t2`.
-
+- `(alf.cmp t1 t2)`
+    - Equivalent to `(alf.is_neg (alf.add (alf.neg (alf.hash t1)) (alf.hash t2)))`. Note that this method corresponds to an arbitrary total order on terms.
+- `(alf.is_z t)`
+    - Equivalent to `(alf.is_eq (alf.to_z t) t)`.
+- `(alf.is_q t)`
+    - Equivalent to `(alf.is_eq (alf.to_q t) t)`. Note this returns false for decimal literals when `--no-normalize-dec` is enabled.
+- `(alf.is_bin t)`
+    - Equivalent to `(alf.is_eq (alf.to_bin (alf.len t) t) t)`. Note this returns false for hexadecimal literals  when `--no-normalize-hex` is enabled.
+- `(alf.is_str t)`
+    - Equivalent to `(alf.is_eq (alf.to_str t) t)`.
+- `(alf.is_bool t)`
+    - Equivalent to `(alf.or (alf.is_eq t true) (alf.is_eq t false))`.
+- `(alf.is_var t)`
+    - Equivalent to `(alf.is_eq (alf.var (alf.nameof t) (alf.typeof t)) t)`.
+
 Boolean operators:
 - `(alf.and t1 t2)`
     - Boolean conjunction if `t1` and `t2` are Boolean values (`true` or `false`).
@@ -524,7 +543,9 @@ Arithmetic operators:
     - If `t1` and `t2` are bitwise values of the same category and bitwidth, then this returns their (total, unsigned) remainder, where remainder by zero returns `t1`.
 - `(alf.is_neg t1)`
     - If `t1` is an arithmetic value, this returns `true` if `t1` is strictly negative and `false` otherwise. Otherwise, this operator is not evaluated.
-
+- `(alf.gt t1 t2)`
+    - Equivalent to `(alf.is_neg (alf.add (alf.neg t1) t2))`.
+
 String operators:
 - `(alf.len t1)`
     - Binary length (bitwidth) if `t1` is a binary value.
@@ -775,7 +796,7 @@ The type `z2` in the above example is `(BitVec (alf.add a b))`, where the applic
 Although the above term does not lead to a type checking error, further use of `z2` would lead to errors if given as an argument to a function that did not expect this type verbatim.
 For example, given a function `f` of type `(-> (BitVec (alf.add b a)) T)`, the term `(f z2)` is not well-typed, since `(alf.add a b)` is not syntactically equal to `(alf.add b a)`.
 
-### Example: Type rule for BitVector constants
+### <a name="bv-literals"></a>Example: Type rule for BitVector constants
 
 ```
 (declare-sort Int 0)
@@ -1611,6 +1632,48 @@ Valid inputs to the ALF checker are `<alf-command>*`, where:
 Moreover, a valid input for a file included by the ALF command `<reference>` is `<smtlib2-command>*`;
 a valid input for a file included by the ALF command `<include>` is `<alf-command>*`.
 
+### <a name="bv-literals"></a>Definitions of Non-Core Evaluation Operators
+
+The following signature can be used to define operators that are not required to be supported as core evaluation operators.
+
+```
+
+; Returns true if x is a numeral literal.
+(define alf.is_z ((T Type :implicit) (x T))
+  (alf.is_eq (alf.to_z x) x))
+
+; Returns true if x is a rational literal.
+(define alf.is_q ((T Type :implicit) (x T))
+  (alf.is_eq (alf.to_q x) x))
+
+; Returns true if x is a binary literal.
+(define alf.is_bin ((T Type :implicit) (x T))
+  (alf.is_eq (alf.to_bin (alf.len x) x) x))
+
+; Returns true if x is a string literal.
+(define alf.is_str ((T Type :implicit) (x T))
+  (alf.is_eq (alf.to_str x) x))
+
+; Returns true if x is a Boolean literal.
+(define alf.is_bool ((T Type :implicit) (x T))
+  (alf.ite (alf.is_eq x true) true (alf.is_eq x false)))
+
+; Returns true if x is a variable.
+(define alf.is_var ((T Type :implicit) (x T))
+  (alf.is_eq (alf.var (alf.nameof x) (alf.typeof x)) x))
+
+; Compare arithmetic greater than. Assumes x and y are values.
+; Returns true if x > y.
+(define alf.gt ((T Type :implicit) (x T) (y T))
+  (alf.is_neg (alf.add (alf.neg x) y)))
+
+; An arbitrary deterministic comparison of terms. Returns true if a > b based
+; on this ordering.
+(define alf.com ((T Type :implicit) (U Type :implicit) (a T) (b U))
+  (alf.is_neg (alf.add (alf.hash b) (alf.neg (alf.hash a)))))
+
+```
+
 ## Proofs as terms
 
 This section overviews the semantics of proofs in the ALF language.