parsing projection variables, not complete - getting errors

meelgroup · Nov 7, 2024 · c88e102 · c88e102
1 parent 1fe2b2b
commit c88e102
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 2 deletions.
diff --git a/include/stp/cpp_interface.h b/include/stp/cpp_interface.h
@@ -96,18 +96,21 @@ class Cpp_interface
 
     // Obtain the symbols for the current frame
     ASTVec& getSymbols();
+    ASTVec& getProjSymbols();
 
   private:
     vector<std::string> _scoped_functions;
     ASTVec _scoped_symbols;
+    ASTVec _scoped_proj_symbols;
     std::unordered_map<std::string, Function>* _global_function_context;
   };
 
   // The vector of all frames that have been created by calling push
-  std::vector< SolverFrame* > frames;
+  std::vector<SolverFrame*> frames;
 
   // Obtain the symbols/functions for the current frame
   ASTVec& getCurrentSymbols();
+  ASTVec& getCurrentProjSymbols();
   vector<std::string>& getCurrentFunctions();
 
   void checkInvariant();
@@ -196,6 +199,7 @@ class Cpp_interface
 
   DLL_PUBLIC void deleteNode(ASTNode* n);
   DLL_PUBLIC void addSymbol(ASTNode& s);
+  DLL_PUBLIC void addProjSymbol(ASTNode& s);
 
   DLL_PUBLIC void success();
   DLL_PUBLIC void error(std::string msg);

diff --git a/lib/Interface/cpp_interface.cpp b/lib/Interface/cpp_interface.cpp
@@ -92,6 +92,11 @@ ASTVec& Cpp_interface::getCurrentSymbols()
   return frames.back()->getSymbols();
 }
 
+ASTVec& Cpp_interface::getCurrentProjSymbols()
+{
+  return frames.back()->getProjSymbols();
+}
+
 vector<std::string>& Cpp_interface::getCurrentFunctions()
 {
   return frames.back()->getFunctions();
@@ -334,6 +339,11 @@ void Cpp_interface::addSymbol(ASTNode& s)
   getCurrentSymbols().push_back(s);
 }
 
+void Cpp_interface::addProjSymbol(ASTNode& s)
+{
+  getCurrentSymbols().push_back(s);
+}
+
 void Cpp_interface::success()
 {
   if (print_success)
@@ -709,4 +719,9 @@ ASTVec& Cpp_interface::SolverFrame::getSymbols()
 {
   return _scoped_symbols;
 }
+
+ASTVec& Cpp_interface::SolverFrame::getProjSymbols()
+{
+  return _scoped_proj_symbols;
 }
+} // namespace stp
diff --git a/lib/Parser/smt2.lex b/lib/Parser/smt2.lex
@@ -194,6 +194,7 @@ bv{DIGIT}+             { smt2lval.str = new std::string(smt2text+2); return BVCO
 "check-sat-assuming"      { return CHECK_SAT_ASSUMING_TOK;}
 "declare-const"           { return DECLARE_CONST_TOK;}
 "declare-fun"             { return DECLARE_FUNCTION_TOK; }
+"proj-var"                { return DECLARE_PROJ_VAR_TOK; }
 "declare-sort"            { return DECLARE_SORT_TOK;}
 "define-fun"              { return DEFINE_FUNCTION_TOK; }
 "define-fun-rec"          { return DECLARE_FUN_REC_TOK;}

diff --git a/lib/Parser/smt2.y b/lib/Parser/smt2.y
@@ -366,6 +366,7 @@
 %token CHECK_SAT_ASSUMING_TOK
 %token DECLARE_CONST_TOK
 %token DECLARE_FUNCTION_TOK
+%token DECLARE_PROJ_VAR_TOK
 %token DECLARE_SORT_TOK
 %token DEFINE_FUNCTION_TOK
 %token DECLARE_FUN_REC_TOK
@@ -432,6 +433,11 @@ cmdi:
     {
       stp::GlobalParserInterface->success();
     }
+|
+     DECLARE_PROJ_VAR_TOK projvar_decl
+    {
+      stp::GlobalParserInterface->success();
+    }
 |
      DECLARE_FUNCTION_TOK var_decl
     {
@@ -692,7 +698,18 @@ SOURCE_TOK
 | LICENSE_TOK
 ;
 
-
+projvar_decl:
+STRING_TOK
+{
+  // TODO AS: There should be a check saying that the variable is already declared.
+  ASTNode s = stp::GlobalParserInterface->LookupOrCreateSymbol($1->c_str());
+  stp::GlobalParserInterface->addProjSymbol(s);
+  //Sort_symbs has the indexwidth/valuewidth. Set those fields in
+  //var
+  s.SetIndexWidth(0);
+  delete $1;
+}
+;
 
 var_decl:
 STRING_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK