Use canonical lookup for declare-var

cvc5 · Jan 31, 2024 · 70d37fa · 70d37fa
1 parent 97fe9d4
commit 70d37fa
Show file tree

Hide file tree

Showing 3 changed files with 44 additions and 20 deletions.
diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp
@@ -152,32 +152,39 @@ bool CmdParser::parseNextCommand()
       Attr ck = Attr::NONE;
       Expr cons;
       Kind sk;
-      if (tok==Token::DECLARE_ORACLE_FUN)
+      Expr v;
+      if (tok==Token::DECLARE_VAR)
       {
-        ck = Attr::ORACLE;
-        sk = Kind::ORACLE;
-        std::string oname = d_eparser.parseSymbol();
-        cons = d_state.mkLiteral(Kind::STRING, oname);
+        // Don't permit attributes for variables
+        // 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 if (tok==Token::DECLARE_CONST || tok==Token::DECLARE_FUN)
+      else
       {
-        sk = Kind::CONST;
-        // possible attribute list
-        AttrMap attrs;
-        d_eparser.parseAttributeList(t, attrs);
-        // determine if an attribute specified a constructor kind
-        if (d_eparser.processAttributeMap(attrs, ck, cons))
+        if (tok==Token::DECLARE_ORACLE_FUN)
         {
-          // if so, this may transform the type
-          t = d_state.mkAnnotatedType(t, ck, cons);
+          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)
+        {
+          sk = Kind::CONST;
+          // possible attribute list
+          AttrMap attrs;
+          d_eparser.parseAttributeList(t, attrs);
+          // determine if an attribute specified a constructor kind
+          if (d_eparser.processAttributeMap(attrs, ck, cons))
+          {
+            // if so, this may transform the type
+            t = d_state.mkAnnotatedType(t, ck, cons);
+          }
+        }
+        v = d_state.mkSymbol(sk, name, t);
       }
-      else
-      {
-        sk = Kind::VARIABLE;
-        // don't permit attributes for variables
-      }
-      Expr v = d_state.mkSymbol(sk, name, t);
       // if the type has a property, we mark it on the variable of this type
       if (ck!=Attr::NONE)
       {

diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
@@ -98,6 +98,7 @@ set(alfc_test_file_list
     arity-overload.smt3
     binder-ex.smt3
     typeof.smt3
+    binder-subterm-share.smt3
 )
 
 macro(alfc_test file)

diff --git a/tests/binder-subterm-share.smt3 b/tests/binder-subterm-share.smt3
@@ -0,0 +1,16 @@
+(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)
+
+(declare-var x Int)
+(define Q () (P x))
+
+(assume @p0 (forall ((x Int)) Q))
+(step @p1 (forall ((x Int)) (P x)) :rule id :premises (@p0))
+
+