Merge pull request #39 from cvc5/opaque

This is key for supporting cvc5-style skolems.

src/attr.cpp

@@ -24,6 +24,7 @@ std::ostream& operator<<(std::ostream& o, Attr a)
     case Attr::PROGRAM: o << "PROGRAM"; break;
     case Attr::ORACLE: o << "ORACLE"; break;
     case Attr::BINDER: o << "BINDER"; break;
+    case Attr::OPAQUE: o << "OPAQUE"; break;
     case Attr::RIGHT_ASSOC: o << "RIGHT_ASSOC"; break;
     case Attr::LEFT_ASSOC: o << "LEFT_ASSOC"; break;
     case Attr::RIGHT_ASSOC_NIL: o << "RIGHT_ASSOC_NIL"; break;

src/attr.h

@@ -30,6 +30,7 @@ enum class Attr
   PROGRAM,
   ORACLE,
   BINDER,
+  OPAQUE,
 
   // indicate how to construct proof rule steps
   PREMISE_LIST,

src/cmd_parser.cpp

@@ -153,41 +153,65 @@ bool CmdParser::parseNextCommand()
         d_state.pushScope();
         params = d_eparser.parseAndBindSortedVarList();
       }
-      Expr t = d_eparser.parseType();
-      if (!sorts.empty())
-      {
-        t = d_state.mkFunctionType(sorts, t, flattenFunction);
-      }
+      Expr ret = d_eparser.parseType();
       Attr ck = Attr::NONE;
       Expr cons;
       Kind sk;
-      Expr v;
+      Expr t;
+      sk = Kind::CONST;
       if (tok==Token::DECLARE_VAR)
       {
         // Don't permit attributes for variables
+        sk = Kind::VARIABLE;
+      }
+      if (tok==Token::DECLARE_ORACLE_FUN)
+      {
+        ck = Attr::ORACLE;
+        sk = Kind::ORACLE;
+        std::string oname = d_eparser.parseSymbol();
+        cons = d_state.mkLiteral(Kind::STRING, oname);
+      }
+      else if (tok==Token::DECLARE_CONST || tok==Token::DECLARE_FUN || tok==Token::DECLARE_PARAMETERIZED_CONST)
+      {
+        // possible attribute list
+        AttrMap attrs;
+        d_eparser.parseAttributeList(t, attrs);
+        // determine if an attribute specified a constructor kind
+        d_eparser.processAttributeMap(attrs, ck, cons, params);
+      }
+      t = ret;
+      if (!sorts.empty())
+      {
+        t = d_state.mkFunctionType(sorts, ret, flattenFunction);
+      }
+      std::vector<Expr> opaqueArgs;
+      while (t.getKind()==Kind::FUNCTION_TYPE && t[0].getKind()==Kind::OPAQUE_TYPE)
+      {
+        Assert (t.getNumChildren()==2);
+        Assert (t[0].getNumChildren()==1);
+        opaqueArgs.push_back(t[0][0]);
+        t = t[1];
+      }
+      if (!opaqueArgs.empty())
+      {
+        if (ck!=Attr::NONE)
+        {
+          d_lex.parseError("Can only use opaque argument on functions without attributes.");
+        }
+        // Reconstruct with opaque arguments, do not flatten function type.
+        t = d_state.mkFunctionType(opaqueArgs, t, false);
+        ck = Attr::OPAQUE;
+      }
+      Expr v;
+      if (sk==Kind::VARIABLE)
+      {
         // We get the canonical variable, not a fresh one. This ensures that
         // globally defined variables coincide with those that appear in
         // binders when applicable.
         v = d_state.getBoundVar(name, t);
       }
       else
       {
-        sk = Kind::CONST;
-        if (tok==Token::DECLARE_ORACLE_FUN)
-        {
-          ck = Attr::ORACLE;
-          sk = Kind::ORACLE;
-          std::string oname = d_eparser.parseSymbol();
-          cons = d_state.mkLiteral(Kind::STRING, oname);
-        }
-        else if (tok==Token::DECLARE_CONST || tok==Token::DECLARE_FUN || tok==Token::DECLARE_PARAMETERIZED_CONST)
-        {
-          // possible attribute list
-          AttrMap attrs;
-          d_eparser.parseAttributeList(t, attrs);
-          // determine if an attribute specified a constructor kind
-          d_eparser.processAttributeMap(attrs, ck, cons, params);
-        }
         v = d_state.mkSymbol(sk, name, t);
       }
       // if the type has a property, we mark it on the variable of this type

src/expr_parser.cpp

@@ -88,6 +88,7 @@ ExprParser::ExprParser(Lexer& lex, State& state, bool isReference)
   d_strToAttr[":chainable"] = Attr::CHAINABLE;
   d_strToAttr[":pairwise"] = Attr::PAIRWISE;
   d_strToAttr[":binder"] = Attr::BINDER;
+  d_strToAttr[":opaque"] = Attr::OPAQUE;
 
   d_strToLiteralKind["<boolean>"] = Kind::BOOLEAN;
   d_strToLiteralKind["<numeral>"] = Kind::NUMERAL;
@@ -456,6 +457,9 @@ Expr ExprParser::parseExpr()
                 }
                 ret = d_state.mkRequires(a.second, ret);
                 break;
+              case Attr::OPAQUE:
+                ret = d_state.mkExpr(Kind::OPAQUE_TYPE, {ret});
+                break;
               default:
                 std::stringstream ss;
                 ss << "Unprocessed attribute " << a.first << std::endl;
@@ -1036,6 +1040,10 @@ void ExprParser::parseAttributeList(const Expr& e, AttrMap& attrs, bool& pushedS
     {
       case Attr::VAR:
       {
+        if (e.isNull())
+        {
+          d_lex.parseError("Cannot use :var in this context");
+        }
         if (attrs.find(Attr::VAR)!=attrs.end())
         {
           d_lex.parseError("Cannot use :var on the same term more than once");
@@ -1056,6 +1064,7 @@ void ExprParser::parseAttributeList(const Expr& e, AttrMap& attrs, bool& pushedS
       case Attr::IMPLICIT:
       case Attr::RIGHT_ASSOC:
       case Attr::LEFT_ASSOC:
+      case Attr::OPAQUE:
         // requires no value
         break;
       case Attr::RIGHT_ASSOC_NIL:

src/kind.cpp

@@ -23,6 +23,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::ABSTRACT_TYPE: o << "ABSTRACT_TYPE"; break;
     case Kind::BOOL_TYPE: o << "BOOL_TYPE"; break;
     case Kind::QUOTE_TYPE: o << "QUOTE_TYPE"; break;
+    case Kind::OPAQUE_TYPE: o << "OPAQUE_TYPE"; break;
     // terms
     case Kind::APPLY: o << "APPLY"; break;
     case Kind::LAMBDA: o << "LAMBDA"; break;
@@ -37,6 +38,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::PROGRAM: o << "PROGRAM"; break;
     case Kind::AS: o << "AS"; break;
     case Kind::PARAMETERIZED: o << "PARAMETERIZED"; break;
+    case Kind::APPLY_OPAQUE: o << "APPLY_OPAQUE"; break;
     // literals
     case Kind::BOOLEAN: o << "BOOLEAN"; break;
     case Kind::NUMERAL: o << "NUMERAL"; break;
@@ -96,8 +98,10 @@ std::string kindToTerm(Kind k)
     case Kind::BOOL_TYPE: ss << "Bool"; break;
     case Kind::QUOTE_TYPE: ss << "Quote"; break;
     case Kind::NULL_EXPR: ss << "alf.nil"; break;
+    case Kind::TUPLE: ss << "alf.tuple"; break;
     // terms
     case Kind::APPLY: ss << "_"; break;
+    case Kind::APPLY_OPAQUE: ss << "_"; break;
     case Kind::LAMBDA: ss << "lambda"; break;
     case Kind::PROGRAM: ss << "program"; break;
     case Kind::AS: ss << "alf.as"; break;

src/kind.h

@@ -27,6 +27,7 @@ enum class Kind
   ABSTRACT_TYPE,
   BOOL_TYPE,
   QUOTE_TYPE,
+  OPAQUE_TYPE, // an argument marked :opaque, temporary during parsing
 
   // terms
   APPLY,
@@ -36,6 +37,7 @@ enum class Kind
   PROGRAM,
   AS,
   PARAMETERIZED,
+  APPLY_OPAQUE,
 
   // symbols
   PARAM,

src/state.cpp

@@ -713,6 +713,35 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
           return mkExpr(Kind::APPLY, cchildren);
         }
           break;
+        case Attr::OPAQUE:
+        {
+          // determine how many opaque children
+          Expr hdt = Expr(hd);
+          const Expr& t = d_tc.getType(hdt);
+          Assert (t.getKind()==Kind::FUNCTION_TYPE);
+          size_t nargs = t.getNumChildren()-1;
+          if (nargs>=children.size())
+          {
+            Warning() << "Too few arguments when applying opaque symbol " << hdt << std::endl;
+          }
+          else
+          {
+            std::vector<Expr> ochildren(children.begin(), children.begin()+1+nargs);
+            Expr op = mkExpr(Kind::APPLY_OPAQUE, ochildren);
+            Trace("opaque") << "Construct opaque operator " << op << std::endl;
+            if (nargs+1==children.size())
+            {
+              Trace("opaque") << "...return operator" << std::endl;
+              return op;
+            }
+            // higher order
+            std::vector<Expr> rchildren;
+            rchildren.push_back(op);
+            rchildren.insert(rchildren.end(), children.begin()+2+nargs, children.end());
+            Trace("opaque") << "...return operator" << std::endl;
+            return mkExpr(Kind::APPLY, rchildren);
+          }
+        }
         default:
           break;
       }

src/state.h

@@ -75,7 +75,13 @@ class State
   void setLiteralTypeRule(Kind k, const Expr& t);
   /** */
   bool bind(const std::string& name, const Expr& e);
-  /** Mark constructor kind */
+  /** 
+   * Mark constructor kind.
+   * @param v The function symbol we are marking.
+   * @param a The constructor kind we are marking v with.
+   * @param cons The constructor associated with v, e.g. the nil terminator
+   * if a is right associative with nil.
+   */
   bool markConstructorKind(const Expr& v, Attr a, const Expr& cons);
   /** Define program, where v is PROGRAM_CONST and prog is PROGRAM. */
   void defineProgram(const Expr& v, const Expr& prog);

src/type_checker.cpp

@@ -203,6 +203,7 @@ Expr TypeChecker::getTypeInternal(ExprValue* e, std::ostream* out)
   switch(k)
   {
     case Kind::APPLY:
+    case Kind::APPLY_OPAQUE:
     {
       Ctx ctx;
       return getTypeAppInternal(e->d_children, ctx, out);
@@ -250,6 +251,20 @@ Expr TypeChecker::getTypeInternal(ExprValue* e, std::ostream* out)
     case Kind::QUOTE_TYPE:
       // anything can be quoted
       return d_state.mkType();
+    case Kind::OPAQUE_TYPE:
+    {
+      ExprValue* ctype = d_state.lookupType(e->d_children[0]);
+      Assert(ctype != nullptr);
+      if (ctype->getKind()!=Kind::TYPE)
+      {
+        if (out)
+        {
+          (*out) << "Non-Type for argument of opaque type";
+        }
+        return d_null;
+      }
+    }
+      return d_state.mkType();
     case Kind::TUPLE:
       // not typed
       return d_state.mkAbstractType();
@@ -642,6 +657,7 @@ Expr TypeChecker::evaluate(ExprValue* e, Ctx& ctx)
         switch (ck)
         {
           case Kind::APPLY:
+          case Kind::APPLY_OPAQUE:
           {
             Trace("type_checker_debug")
                 << "evaluated args " << cchildren << std::endl;

tests/CMakeLists.txt

@@ -109,6 +109,9 @@ set(alfc_test_file_list
     nground-nil-v3.smt3
     ff-nil.smt3
     or-variant.smt3
+    substitution-opaque.smt3
+    opaque-inst.smt3
+    opaque-inst2.smt3
     mutual-rec.smt3
 )
 

tests/opaque-inst.smt3

@@ -0,0 +1,37 @@
+
+
+
+(declare-const = (-> (! Type :var T :implicit) T T Bool))
+
+(declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
+(declare-const and (-> Bool Bool Bool) :right-assoc-nil true)
+(declare-const not (-> Bool Bool))
+
+(declare-sort Array 2)
+(declare-sort Int 0)
+
+(declare-const select (-> (Array Int Int) Int Int))
+
+
+(declare-const @array_deq_diff 
+  (-> 
+    (! (Array Int Int) :opaque)
+    (! (Array Int Int) :opaque)
+    Int
+  )
+)
+
+
+(declare-rule array-ext
+   ((a (Array Int Int)) (b (Array Int Int)))
+   :premises ((not (= a b)))
+   :args ()
+   :conclusion (not (= (select a (@array_deq_diff a b)) (select b (@array_deq_diff a b))))
+)
+
+(declare-const n (Array Int Int))
+(declare-const m (Array Int Int))
+(declare-const v Int)
+
+(assume a1 (not (= n m)))
+(step a2 (not (= (select n (@array_deq_diff n m)) (select m (@array_deq_diff n m)))) :rule array-ext :premises (a1))

tests/opaque-inst2.smt3

@@ -0,0 +1,39 @@
+
+
+
+(declare-const = (-> (! Type :var T :implicit) T T Bool))
+
+(declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
+(declare-const and (-> Bool Bool Bool) :right-assoc-nil true)
+(declare-const not (-> Bool Bool))
+
+(declare-sort Array 2)
+(declare-sort Int 0)
+
+(declare-const select (-> (Array Int Int) Int Int))
+
+
+(declare-const @array_deq_diff 
+  (-> 
+    (! Type :implicit :var T)
+    (! Type :implicit :var U)
+    (! (Array T U) :opaque)
+    (! (Array T U) :opaque)
+    T
+  )
+)
+
+
+(declare-rule array-ext
+   ((a (Array Int Int)) (b (Array Int Int)))
+   :premises ((not (= a b)))
+   :args ()
+   :conclusion (not (= (select a (@array_deq_diff a b)) (select b (@array_deq_diff a b))))
+)
+
+(declare-const n (Array Int Int))
+(declare-const m (Array Int Int))
+(declare-const v Int)
+
+(assume a1 (not (= n m)))
+(step a2 (not (= (select n (@array_deq_diff n m)) (select m (@array_deq_diff n m)))) :rule array-ext :premises (a1))