Sketching evaluation interface in compiler

cvc5 · Jul 27, 2023 · b2d2af6 · b2d2af6
1 parent 4b7b0f3
commit b2d2af6
Show file tree

Hide file tree

Showing 8 changed files with 65 additions and 33 deletions.
diff --git a/src/compiled.cpp b/src/compiled.cpp
@@ -12,7 +12,12 @@ Expr TypeChecker::run_getTypeInternal(Expr& hdType, std::vector<Expr>& args, std
   return nullptr;
 }
 
-Expr TypeChecker::run_evaluate(Expr& hd, std::vector<Expr>& args)
+Expr TypeChecker::run_evaluate(Expr& e, Ctx& ctx)
+{
+  return nullptr;
+}
+
+Expr TypeChecker::run_evaluateProgram(Expr& hd, std::vector<Expr>& args, Ctx& ctx)
 {
   return nullptr;
 }

diff --git a/src/compiler.cpp b/src/compiler.cpp
@@ -72,19 +72,23 @@ Compiler::Compiler(State& s) : d_state(s), d_nscopes(0), d_global(d_decl, d_init
   // TODO: write error?
   d_tcEnd << "  return nullptr;" << std::endl;
   d_tcEnd << "}" << std::endl;
-  d_eval << "Expr TypeChecker::run_evaluate(Expr& e, std::vector<Expr>& args)" << std::endl;
+  d_eval << "Expr TypeChecker::run_evaluate(Expr& e, Ctx& ctx)" << std::endl;
   d_eval << "{" << std::endl;
-  d_eval << "  std::map<ExprValue*, size_t>::iterator itr = _runId.find(e.get());" << std::endl;
-  d_eval << "  switch(itr->second)" << std::endl;
-  d_eval << "  {" << std::endl;
-  d_evalEnd << "  default: break;" << std::endl;
-  d_evalEnd << "  }" << std::endl;
-  // otherwise just return itself (unevaluated)
-  d_evalEnd << "  std::vector<Expr> eargs;" << std::endl;
-  d_evalEnd << "  eargs.push_back(e);" << std::endl;
-  d_evalEnd << "  eargs.insert(eargs.end(), args.begin(), args.end());" << std::endl;
-  d_evalEnd << "  return d_state.mkExprInternal(Kind::APPLY, eargs);" << std::endl;
+  d_evalEnd << "  return nullptr;" << std::endl;
   d_evalEnd << "}" << std::endl;
+  d_evalp << "Expr TypeChecker::run_evaluateProgram(Expr& e, std::vector<Expr>& args, Ctx& ctx)" << std::endl;
+  d_evalp << "{" << std::endl;
+  d_evalp << "  std::map<ExprValue*, size_t>::iterator itr = _runId.find(e.get());" << std::endl;
+  d_evalp << "  switch(itr->second)" << std::endl;
+  d_evalp << "  {" << std::endl;
+  d_evalpEnd << "  default: break;" << std::endl;
+  d_evalpEnd << "  }" << std::endl;
+  // otherwise just return itself (unevaluated)
+  d_evalpEnd << "  std::vector<Expr> eargs;" << std::endl;
+  d_evalpEnd << "  eargs.push_back(e);" << std::endl;
+  d_evalpEnd << "  eargs.insert(eargs.end(), args.begin(), args.end());" << std::endl;
+  d_evalpEnd << "  return d_state.mkExprInternal(Kind::APPLY, eargs);" << std::endl;
+  d_evalpEnd << "}" << std::endl;
 }
 
 Compiler::~Compiler(){}
@@ -533,6 +537,8 @@ std::string Compiler::toString()
   ss << d_tcEnd.str() << std::endl;
   ss << d_eval.str();
   ss << d_evalEnd.str() << std::endl;
+  ss << d_evalp.str();
+  ss << d_evalpEnd.str() << std::endl;
   ss << "}" << std::endl;
   return ss.str();
 }

diff --git a/src/compiler.h b/src/compiler.h
@@ -99,6 +99,11 @@ class Compiler
    */
   std::stringstream d_eval;
   std::stringstream d_evalEnd;
+  /**
+   * Code to be called for evaluating programs, returns the case
+   */
+  std::stringstream d_evalp;
+  std::stringstream d_evalpEnd;
   /** Identifier counts */
   CompilerScope d_global;
   /**

diff --git a/src/expr.cpp b/src/expr.cpp
@@ -89,11 +89,16 @@ void ExprValue::computeFlags()
     else
     {
       visit.pop_back();
-      if (cur->getKind()==Kind::APPLY && 
-          children[0]->getKind()==Kind::PROGRAM_CONST)
+      Kind ck = cur->getKind();
+      if (ck==Kind::APPLY && children[0]->getKind()==Kind::PROGRAM_CONST)
       {
         cur->setFlag(Flag::IS_EVAL, true);
       }
+      else if (ck==Kind::REQUIRES_TYPE)
+      {
+        // requires type may evaluate
+        cur->setFlag(Flag::IS_EVAL, true);
+      }
       for (Expr& c : children)
       {
         if (c->getFlag(Flag::IS_NON_GROUND))

diff --git a/src/state.cpp b/src/state.cpp
@@ -502,7 +502,7 @@ void State::defineProgram(const Expr& v, const Expr& prog)
   }
 }
 
-Expr State::evaluate(const std::vector<Expr>& children, Ctx& newCtx)
+Expr State::evaluateProgram(const std::vector<Expr>& children, Ctx& newCtx)
 {
   Expr hd = children[0];
   std::map<Expr, Expr>::iterator it = d_programs.find(hd);

diff --git a/src/state.h b/src/state.h
@@ -92,7 +92,7 @@ class State
   /** Define program */
   void defineProgram(const Expr& v, const Expr& prog);
   /** Maybe evaluate */
-  Expr evaluate(const std::vector<Expr>& children, Ctx& newCtx);
+  Expr evaluateProgram(const std::vector<Expr>& children, Ctx& newCtx);
 private:
   /** */
   ExprInfo* getOrMkInfo(const ExprValue* e);

diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -133,6 +133,7 @@ Expr TypeChecker::getTypeInternal(Expr& e, std::ostream* out)
       // if compiled, run the compiled version of the type checker
       if (hdType->isCompiled())
       {
+        std::cout << "RUN type check " << hdType << std::endl;
         return run_getTypeInternal(hdType, ctypes, out);
       }
       Ctx ctx;
@@ -350,7 +351,8 @@ Expr TypeChecker::evaluate(Expr& e, Ctx& ctx)
     while (!visit.empty())
     {
       cur = visit.back();
-      // unevaluatable terms stay the same
+      // the term will stay the same if it is not evaluatable and either it
+      // is ground, or the context is empty.
       if (!cur->isEvaluatable() && (cur->isGround() || cctx.empty()))
       {
         visited[cur] = cur;
@@ -373,6 +375,13 @@ Expr TypeChecker::evaluate(Expr& e, Ctx& ctx)
         // TODO: error, variable not filled?
         //std::cout << "WARNING: unfilled variable " << cur << std::endl;
       }
+      // if it is compiled, we run its evaluation here
+      if (cur->isCompiled())
+      {
+        visited[cur] = run_evaluate(cur, cctx);
+        continue;
+      }
+
       std::vector<Expr>& children = cur->d_children;
       it = visited.find(cur);
       if (it == visited.end())
@@ -428,28 +437,28 @@ Expr TypeChecker::evaluate(Expr& e, Ctx& ctx)
             // maybe evaluate the program?
             if (cchildren[0]->getKind()==Kind::PROGRAM_CONST)
             {
+              ctxs.emplace_back();
               if (cchildren[0]->isCompiled())
               {
                 std::vector<Expr> pargs(cchildren.begin()+1, cchildren.end());
-                evaluated = run_evaluate(cchildren[0], pargs);
+                evaluated = run_evaluateProgram(cchildren[0], pargs, ctxs.back());
               }
               else
               {
-                ctxs.emplace_back();
                 // see if we evaluate
-                evaluated = d_state.evaluate(cchildren, ctxs.back());
-                if (ctxs.back().empty())
-                {
-                  // if there is no context, we don't have to push a scope
-                  ctxs.pop_back();
-                }
-                else
-                {
-                  // otherwise push an evaluation scope
-                  newContext = true;
-                  visits.emplace_back(std::vector<Expr>{evaluated});
-                  visiteds.emplace_back();
-                }
+                evaluated = d_state.evaluateProgram(cchildren, ctxs.back());
+              }
+              if (ctxs.back().empty())
+              {
+                // if there is no context, we don't have to push a scope
+                ctxs.pop_back();
+              }
+              else
+              {
+                // otherwise push an evaluation scope
+                newContext = true;
+                visits.emplace_back(std::vector<Expr>{evaluated});
+                visiteds.emplace_back();
               }
             }
             break;

diff --git a/src/type_checker.h b/src/type_checker.h
@@ -43,7 +43,9 @@ class TypeChecker
   /** Return its type */
   Expr getTypeInternal(Expr& e, std::ostream* out);
   /** Compiled version */
-  Expr run_evaluate(Expr& hd, std::vector<Expr>& args);
+  Expr run_evaluate(Expr& e, Ctx& ctx);
+  /** Compiled version */
+  Expr run_evaluateProgram(Expr& hd, std::vector<Expr>& args, Ctx& ctx);
   /** The state */
   State& d_state;
   /** The builtin literal kinds */