More

src/expr_parser.cpp

@@ -671,12 +671,9 @@ std::vector<Expr> ExprParser::parseAndBindSortedVarList(bool isLookup)
     if (isLookup)
     {
       // lookup and type check
-      v = getVar(name);
-      typeCheck(v, t);
-      if (v.getKind()!=Kind::VARIABLE)
-      {
-        d_lex.parseError("Expected a variable in binder");
-      }
+      v = d_state.getBoundVar(name, t);
+      // bind it for now
+      bind(name, v);
     }
     else
     {

src/state.cpp

@@ -1028,6 +1028,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;

src/state.h

@@ -121,6 +121,11 @@ class State
   bool isBinder(const ExprValue* ev) const;
   /** 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 */
@@ -198,6 +203,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 */

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)

tests/binder-ex.smt3

@@ -2,8 +2,6 @@
 
 (declare-const P (-> Int Bool))
 (declare-const forall (-> Bool Bool) :binder)
-(declare-var x Int)
-(declare-var z Int)
 
 (declare-rule id ((y Bool)) :premises (y) :conclusion y)