Implementation of :binder

This allows a more SMT-LIB compliant syntax for binders.
cvc5 · Jan 30, 2024 · 685b750 · 685b750
2 parents 53ec3f6 + 837d16e
commit 685b750
Show file tree

Hide file tree

Showing 10 changed files with 150 additions and 39 deletions.
diff --git a/src/attr.cpp b/src/attr.cpp
@@ -23,6 +23,7 @@ std::ostream& operator<<(std::ostream& o, Attr a)
     case Attr::PREMISE_LIST: o << "PREMISE_LIST"; break;
     case Attr::PROGRAM: o << "PROGRAM"; break;
     case Attr::ORACLE: o << "ORACLE"; break;
+    case Attr::BINDER: o << "BINDER"; 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;
@@ -32,7 +33,6 @@ std::ostream& operator<<(std::ostream& o, Attr a)
     case Attr::DATATYPE: o << "DATATYPE"; break;
     case Attr::CODATATYPE: o << "CODATATYPE"; break;
     case Attr::DATATYPE_CONSTRUCTOR: o << "DATATYPE_CONSTRUCTOR"; break;
-    case Attr::CLOSURE: o << "CLOSURE"; break;
     default: o << "UnknownAttr(" << unsigned(a) << ")"; break;
   }
   return o;

diff --git a/src/attr.h b/src/attr.h
@@ -29,6 +29,7 @@ enum class Attr
   SYNTAX,
   PROGRAM,
   ORACLE,
+  BINDER,
 
   // indicate how to construct proof rule steps
   PREMISE_LIST,
@@ -44,10 +45,7 @@ enum class Attr
   // datatypes
   DATATYPE,
   DATATYPE_CONSTRUCTOR,
-  CODATATYPE,
-
-  // internal
-  CLOSURE
+  CODATATYPE
 };
 
 /** Print a kind to the stream, for debugging */

diff --git a/src/expr_parser.cpp b/src/expr_parser.cpp
@@ -73,8 +73,8 @@ enum class ParseCtx
   TERM_ANNOTATE_BODY
 };
 
-ExprParser::ExprParser(Lexer& lex, State& state)
-    : d_lex(lex), d_state(state)
+ExprParser::ExprParser(Lexer& lex, State& state, bool isReference)
+    : d_lex(lex), d_state(state), d_isReference(isReference)
 {
   d_strToAttr[":var"] = Attr::VAR;
   d_strToAttr[":implicit"] = Attr::IMPLICIT;
@@ -87,6 +87,7 @@ ExprParser::ExprParser(Lexer& lex, State& state)
   d_strToAttr[":right-assoc-nil"] = Attr::RIGHT_ASSOC_NIL;
   d_strToAttr[":chainable"] = Attr::CHAINABLE;
   d_strToAttr[":pairwise"] = Attr::PAIRWISE;
+  d_strToAttr[":binder"] = Attr::BINDER;
 
   d_strToLiteralKind["<boolean>"] = Kind::BOOLEAN;
   d_strToLiteralKind["<numeral>"] = Kind::NUMERAL;
@@ -172,19 +173,31 @@ Expr ExprParser::parseExpr()
             Expr v = getVar(name);
             args.push_back(v);
             size_t nscopes = 0;
-            // if a closure, read a variable list and push a scope
-            if (d_state.isClosure(v.getValue()))
+            // if a binder, read a variable list and push a scope
+            if (d_state.isBinder(v.getValue()))
             {
-              nscopes = 1;
-              // if it is a closure, immediately read the bound variable list
-              d_state.pushScope();
-              std::vector<Expr> vs = parseAndBindSortedVarList();
-              if (vs.empty())
+              // If it is a binder, immediately read the bound variable list.
+              // If option d_binderFresh is true, we parse and bind fresh
+              // variables. Otherwise, we make calls to State::getBoundVar
+              // meaning the bound variables are unique for each (name, type)
+              // pair.
+              // We only do this if there are two left parentheses. Otherwise we
+              // will parse a tuple term that stands for a symbolic bound
+              // variable list. We do this because there are no terms that
+              // begin ((... currently allowed in this parser.
+              if (d_lex.peekToken()==Token::LPAREN && d_lex.peekToken()==Token::LPAREN)
               {
-                d_lex.parseError("Expected non-empty sorted variable list");
+                nscopes = 1;
+                bool isLookup = !d_state.getOptions().d_binderFresh;
+                d_state.pushScope();
+                std::vector<Expr> vs = parseAndBindSortedVarList(isLookup);
+                if (vs.empty())
+                {
+                  d_lex.parseError("Expected non-empty sorted variable list");
+                }
+                Expr vl = d_state.mkBinderList(v.getValue(), vs);
+                args.push_back(vl);
               }
-              Expr vl = d_state.mkExpr(Kind::TUPLE, vs);
-              args.push_back(vl);
             }
             pstack.emplace_back(ParseCtx::NEXT_ARG, nscopes, args);
           }
@@ -654,7 +667,7 @@ std::vector<Expr> ExprParser::parseExprPairList()
   return terms;
 }
 
-std::vector<Expr> ExprParser::parseAndBindSortedVarList()
+std::vector<Expr> ExprParser::parseAndBindSortedVarList(bool isLookup)
 {
   std::vector<Expr> varList;
   d_lex.eatToken(Token::LPAREN);
@@ -667,22 +680,33 @@ std::vector<Expr> ExprParser::parseAndBindSortedVarList()
   {
     name = parseSymbol();
     t = parseType();
-    Expr v = d_state.mkSymbol(Kind::PARAM, name, t);
-    bind(name, v);
-    // parse attribute list
-    AttrMap attrs;
-    parseAttributeList(v, attrs);
+    Expr v;
     bool isImplicit = false;
-    if (attrs.find(Attr::IMPLICIT)!=attrs.end())
+    if (isLookup)
     {
-      attrs.erase(Attr::IMPLICIT);
-      isImplicit = true;
+      // lookup and type check
+      v = d_state.getBoundVar(name, t);
+      // bind it for now
+      bind(name, v);
     }
-    if (processAttributeMap(attrs, ck, cons))
+    else
     {
-      d_state.markConstructorKind(v, ck, cons);
-      ck = Attr::NONE;
-      cons = d_null;
+      v = d_state.mkSymbol(Kind::PARAM, name, t);
+      bind(name, v);
+      // parse attribute list
+      AttrMap attrs;
+      parseAttributeList(v, attrs);
+      if (attrs.find(Attr::IMPLICIT)!=attrs.end())
+      {
+        attrs.erase(Attr::IMPLICIT);
+        isImplicit = true;
+      }
+      if (processAttributeMap(attrs, ck, cons))
+      {
+        d_state.markConstructorKind(v, ck, cons);
+        ck = Attr::NONE;
+        cons = d_null;
+      }
     }
     d_lex.eatToken(Token::RPAREN);
     if (!isImplicit)
@@ -1009,6 +1033,7 @@ void ExprParser::parseAttributeList(const Expr& e, AttrMap& attrs, bool& pushedS
         break;
       case Attr::CHAINABLE:
       case Attr::PAIRWISE:
+      case Attr::BINDER:
       {
         // requires an expression that follows
         val = parseExpr();
@@ -1211,6 +1236,8 @@ bool ExprParser::processAttributeMap(const AttrMap& attrs, Attr& ck, Expr& cons)
         case Attr::RIGHT_ASSOC_NIL:
         case Attr::CHAINABLE:
         case Attr::PAIRWISE:
+        case Attr::BINDER:
+        {
           if (ck!=Attr::NONE)
           {
             std::stringstream ss;
@@ -1222,6 +1249,7 @@ bool ExprParser::processAttributeMap(const AttrMap& attrs, Attr& ck, Expr& cons)
           // it specifies how to construct terms involving this term
           ck = a.first;
           cons = av;
+        }
           break;
         default:
           std::stringstream ss;

diff --git a/src/expr_parser.h b/src/expr_parser.h
@@ -24,7 +24,7 @@ namespace alfc {
 class ExprParser
 {
  public:
-  ExprParser(Lexer& lex, State& state);
+  ExprParser(Lexer& lex, State& state, bool isReference);
   virtual ~ExprParser() {}
 
   /** Parses an SMT-LIB term <term> */
@@ -46,8 +46,11 @@ class ExprParser
   /**
    * Parse parentheses-enclosed sorted variable list of the form:
    * ((<symbol> <sort>)*)
+   * 
+   * @param isLookup If true, we expect the variable list to be already bound
+   * variables and throw an error if a variable does not match.
    */
-  std::vector<Expr> parseAndBindSortedVarList();
+  std::vector<Expr> parseAndBindSortedVarList(bool isLookup=false);
   /**
    * Parse symbol, which returns the string of the parsed symbol if the next
    * token is a valid smt2 symbol.
@@ -152,6 +155,8 @@ class ExprParser
   Lexer& d_lex;
   /** The state */
   State& d_state;
+  /** */
+  bool d_isReference;
   /** Strings to attributes */
   std::map<std::string, Attr> d_strToAttr;
   /** Mapping symbols to literal kinds */

diff --git a/src/main.cpp b/src/main.cpp
@@ -32,7 +32,11 @@ int main( int argc, char* argv[] )
   {
     std::string arg(argv[i]);
     i++;
-    if (arg=="--gen-compile")
+    if (arg=="--binder-fresh")
+    {
+      opts.d_binderFresh = true;
+    }
+    else if (arg=="--gen-compile")
     {
       opts.d_compile = true;
     }
@@ -64,6 +68,7 @@ int main( int argc, char* argv[] )
     else if (arg=="--help")
     {
       std::stringstream out;
+      out << "     --binder-fresh: binders generate fresh variables when parsed in proof files." << std::endl;
       out << "      --gen-compile: output the C++ code for all included signatures from the input file." << std::endl;
       out << "             --help: displays this message." << std::endl;
       out << " --no-normalize-dec: do not treat decimal literals as syntax sugar for rational literals." << std::endl;

diff --git a/src/parser.cpp b/src/parser.cpp
@@ -13,7 +13,7 @@ namespace alfc {
 Parser::Parser(State& s, bool isReference)
     : d_lex(),
       d_state(s),
-      d_eparser(d_lex, d_state),
+      d_eparser(d_lex, d_state, isReference),
       d_cmdParser(d_lex, d_state, d_eparser, isReference)
 {
 }

diff --git a/src/state.cpp b/src/state.cpp
@@ -26,6 +26,7 @@ Options::Options()
   d_ruleSymTable = true;
   d_normalizeDecimal = true;
   d_normalizeHexadecimal = true;
+  d_binderFresh = false;
 }
 
 State::State(Options& opts, Stats& stats)
@@ -482,7 +483,18 @@ Expr State::mkBuiltinType(Kind k)
 
 Expr State::mkAnnotatedType(const Expr& t, Attr ck, const Expr& cons)
 {
-  if (ck!=Attr::RIGHT_ASSOC_NIL && ck!=Attr::LEFT_ASSOC_NIL)
+  if (ck==Attr::BINDER)
+  {
+    // prepend to argument types the return type of the constructor
+    Expr c = cons;
+    const Expr& ct = d_tc.getType(c);
+    if (ct.getKind()!=Kind::FUNCTION_TYPE || ct[1].getKind()!=Kind::FUNCTION_TYPE)
+    {
+      return d_null;
+    }
+    return mkFunctionType({ct[1][1]}, t);
+  }
+  else if (ck!=Attr::RIGHT_ASSOC_NIL && ck!=Attr::LEFT_ASSOC_NIL)
   {
     return t;
   }
@@ -1004,9 +1016,20 @@ bool State::bind(const std::string& name, const Expr& e)
   return true;
 }
 
-bool State::isClosure(const ExprValue* e) const
+bool State::isBinder(const ExprValue* e) const
+{
+  return getConstructorKind(e) == Attr::BINDER;
+}
+
+Expr State::mkBinderList(const ExprValue* ev, const std::vector<Expr>& vs)
 {
-  return getConstructorKind(e) == Attr::CLOSURE;
+  Assert (!vs.empty());
+  std::map<const ExprValue *, AppInfo>::const_iterator it = d_appData.find(ev);
+  Assert (it!=d_appData.end());
+  std::vector<Expr> vlist;
+  vlist.push_back(it->second.d_attrConsTerm);
+  vlist.insert(vlist.end(), vs.begin(), vs.end());
+  return mkExpr(Kind::APPLY, vlist);
 }
 
 Attr State::getConstructorKind(const ExprValue* v) const
@@ -1029,6 +1052,19 @@ Expr State::getVar(const std::string& name) const
   return d_null;
 }
 
+Expr State::getBoundVar(const std::string& name, const Expr& type)
+{
+  std::pair<std::string, const ExprValue*> key(name, type.getValue());
+  std::map<std::pair<std::string, const ExprValue*>, Expr>::iterator it = d_boundVars.find(key);
+  if (it!=d_boundVars.end())
+  {
+    return it->second;
+  }
+  Expr ret = mkSymbol(Kind::VARIABLE, name, type);
+  d_boundVars[key] = ret;
+  return ret;
+}
+
 Expr State::getProofRule(const std::string& name) const
 {
   const std::map<std::string, Expr>& t = d_opts.d_ruleSymTable ? d_ruleSymTable : d_symTable;

diff --git a/src/state.h b/src/state.h
@@ -37,6 +37,8 @@ class Options
   bool d_ruleSymTable;
   bool d_normalizeDecimal;
   bool d_normalizeHexadecimal;
+  /** Binders generate fresh variables in proof and reference files */
+  bool d_binderFresh;
 };
 
 /**
@@ -123,10 +125,17 @@ class State
    */
   Expr mkLiteral(Kind k, const std::string& s);
   //--------------------------------------
-  /** is closure */
-  bool isClosure(const ExprValue* ev) const;
+  /** is binder */
+  bool isBinder(const ExprValue* ev) const;
+  /** make binder list */
+  Expr mkBinderList(const ExprValue* ev, const std::vector<Expr>& vs);
   /** Get the variable with the given name or nullptr if it does not exist */
   Expr getVar(const std::string& name) const;
+  /**
+   * Get the bound variable with the given type. This method always returns the
+   * same variable for the same name and type.
+   */
+  Expr getBoundVar(const std::string& name, const Expr& type);
   /** Get the proof rule with the given name or nullptr if it does not exist */
   Expr getProofRule(const std::string& name) const;
   /** Get actual premises */
@@ -204,6 +213,8 @@ class State
   std::map<std::string, Expr> d_symTable;
   /** Symbol table for proof rules, if using separate table */
   std::map<std::string, Expr> d_ruleSymTable;
+  /** The (canonical) bound variables for binders */
+  std::map<std::pair<std::string, const ExprValue*>, Expr> d_boundVars;
   /** Context stacks */
   std::vector<std::pair<std::string, size_t>> d_decls;
   /** Context size */

diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
@@ -96,6 +96,7 @@ set(alfc_test_file_list
     match-variants.smt3
     tiny_oracle.smt3
     arity-overload.smt3
+    binder-ex.smt3
 )
 
 macro(alfc_test file)

diff --git a/tests/binder-ex.smt3 b/tests/binder-ex.smt3
@@ -0,0 +1,27 @@
+(declare-sort @List 0)
+(declare-const @list.nil @List)
+(declare-const @list.cons (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil)
+
+(declare-sort Int 0)
+
+(declare-const P (-> Int Bool))
+(declare-const forall (-> Bool Bool) :binder @list.cons)
+
+(declare-rule id ((y Bool)) :premises (y) :conclusion y)
+
+(assume @p0 (forall ((x Int)) (P x)))
+(assume @p2 (forall ((x Int)) false))
+
+
+; should match
+(step @p1 (forall ((x Int)) (P x)) :rule id :premises (@p0))
+
+; wrong
+; (step @p1 (forall ((z Int)) (P z)) :rule id :premises (@p0))
+
+
+(declare-rule q-rule ((xs @List))
+  :premises ((forall xs false))
+  :conclusion false)
+
+(step @p3 false :rule q-rule :premises (@p2))