implement the beginnings of generic translation to SMT

Github: related to #13 "partial order reduction"

librumur/CMakeLists.txt

@@ -70,7 +70,9 @@ add_library(librumur
   src/Property.cc
   src/resolve-symbols.cc
   src/Rule.cc
+  src/smt.cc
   src/Stmt.cc
+  src/SymContext.cc
   src/traverse.cc
   src/TypeExpr.cc
   src/validate.cc

librumur/include/rumur/SymContext.h

@@ -0,0 +1,54 @@
+#pragma once
+
+#include <cstddef>
+#include <rumur/Node.h>
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+namespace rumur {
+
+// Symbolic context, for maintaining a mapping between Murphi variables and
+// external (generated) symbols. This has extremely limited functionality, only
+// enough to support the translation to SMT (see smt.h).
+class SymContext {
+
+ private:
+  // stack of symbol tables, mapping AST unique IDs to external names
+  std::vector<std::unordered_map<size_t, std::string>> scope;
+
+  // monotonic counter used for generating unique symbols
+  size_t counter = 0;
+
+ public:
+  SymContext();
+
+  // descend into or ascend from a variable scope
+  void open_scope();
+  void close_scope();
+
+  /// add a new known symbol
+  ///
+  /// This registers the symbol in the current innermost scope.
+  ///
+  /// \param id Unique identifier of the source AST node
+  /// \return A unique name created for this symbol
+  std::string register_symbol(size_t id);
+
+  /// lookup a previously registered symbol
+  ///
+  /// This lookup is performed in all known variable scopes, going from
+  /// innermost to outermost in preference order
+  ///
+  /// \param id Unique identifier of the AST node being looked up
+  /// \param origin The node that caused this lookup (used for error
+  ///   diagnostics)
+  /// \return The unique name this symbol maps to
+  std::string lookup_symbol(size_t id, const Node &origin) const;
+
+ private:
+  std::string make_symbol();
+
+};
+
+}

librumur/include/rumur/rumur.h

@@ -20,7 +20,9 @@
 #include <rumur/resolve-symbols.h>
 #include <rumur/Rule.h>
 #include <rumur/scanner.h>
+#include <rumur/smt.h>
 #include <rumur/Stmt.h>
+#include <rumur/SymContext.h>
 #include <rumur/Symtab.h>
 #include <rumur/traverse.h>
 #include <rumur/TypeExpr.h>

librumur/include/rumur/smt.h

@@ -0,0 +1,52 @@
+// functionality related to interacting with a Satisfiability Modulo Theories
+// solver
+
+#pragma once
+
+#include <cstddef>
+#include <gmpxx.h>
+#include <rumur/Expr.h>
+#include <rumur/Node.h>
+#include <rumur/Number.h>
+#include <rumur/SymContext.h>
+#include <string>
+#include <unordered_map>
+
+namespace rumur {
+
+struct SMTConfig {
+
+  // use bitvectors instead of integers for numeric values?
+  bool prefer_bitvectors = false;
+
+  // bit width to use to represent numerical values if using bitvectors
+  size_t bitvector_width = 64;
+
+  // various SMT operators whose selection is dependent on context
+  std::string add (const Node &origin) const;
+  std::string band(const Node &origin) const;
+  std::string bnot(const Node &origin) const;
+  std::string bor (const Node &origin) const;
+  std::string bxor(const Node &origin) const;
+  std::string div (const Node &origin) const;
+  std::string geq (const Node &origin) const;
+  std::string gt  (const Node &origin) const;
+  std::string leq (const Node &origin) const;
+  std::string lsh (const Node &origin) const;
+  std::string lt  (const Node &origin) const;
+  std::string mod (const Node &origin) const;
+  std::string mul (const Node &origin) const;
+  std::string neg (const Node &origin) const;
+  std::string rsh (const Node &origin) const;
+  std::string sub (const Node &origin) const;
+  std::string numeric_literal(const mpz_class &value, const Number &origin) const;
+
+};
+
+// translate a given expression to SMTLIBv2
+void to_smt(std::ostream &out, const Expr &n, SymContext &ctxt, SMTConfig &conf);
+
+// wrapper around the above for when you do not need a long lived output buffer
+std::string to_smt(const Expr &n, SymContext &ctxt, SMTConfig &conf);
+
+}

librumur/src/SymContext.cc

@@ -0,0 +1,49 @@
+#include <cstddef>
+#include <rumur/except.h>
+#include <rumur/Node.h>
+#include <rumur/SymContext.h>
+#include <string>
+#include <unordered_map>
+
+namespace rumur {
+
+SymContext::SymContext() {
+  open_scope();
+}
+
+void SymContext::open_scope() {
+  scope.push_back(std::unordered_map<size_t, std::string>{});
+}
+
+void SymContext::close_scope() {
+  scope.pop_back();
+  // TODO: we probably need to record symbols somewhere
+}
+
+std::string SymContext::register_symbol(size_t id) {
+  // invent a new symbol and map this ID to it
+  std::string s = make_symbol();
+  scope.back()[id] = s;
+  return s;
+}
+
+std::string SymContext::lookup_symbol(size_t id, const Node &origin) const {
+
+  // lookup the symbol in enclosing scopes from innermost to outermost
+  for (auto it = scope.rbegin(); it != scope.rend(); ++it) {
+    auto it2 = it->find(id);
+    if (it2 != it->end())
+      return it2->second;
+  }
+
+  // we expect any symbol encountered in a well-formed AST to be associated with
+  // a previously encountered definition
+  throw Error("unknown symbol encountered; applying SMT translation to an "
+    "unvalidated AST?", origin.loc);
+}
+
+std::string SymContext::make_symbol() {
+  return "s" + std::to_string(counter++);
+}
+
+}