Driver.h

 
#pragma once
 
#include <istream>
#include <string>
#include <utility>
#include <variant>
#include <vector>
 
#include "dlinear/parser/Driver.h"
#include "dlinear/parser/smt2/FunctionDefinition.h"
#include "dlinear/parser/smt2/Term.h"
#include "dlinear/parser/smt2/scanner.h"
#include "dlinear/solver/Context.h"
#include "dlinear/util/ScopedUnorderedMap.hpp"
 
namespace dlinear::smt2 {
 
class Smt2Driver : public Driver {
 public:
  explicit Smt2Driver(Context &context);  // NOLINT(runtime/references): Reference context filled during parsing.
 
  static void error(const location &l, const std::string &m);
 
  bool ParseStreamCore(std::istream &in) override;
 
  static Formula EliminateBooleanVariables(const Variables &vars, const Formula &f);
 
  void DefineFun(const std::string &name, const std::vector<Variable> &parameters, Sort return_type, const Term &body);
 
  Variable RegisterVariable(const std::string &name, Sort sort);
 
  Variable DeclareVariable(const std::string &name, Sort sort);
 
  void DeclareVariable(const std::string &name, Sort sort, const Term &lb, const Term &ub);
 
  Variable DeclareLocalVariable(const std::string &name, Sort sort);
 
  void DefineLocalConstant(const std::string &name, const Expression &value);
 
  void GetValue(const std::vector<Term> &term_list) const;
 
  std::variant<const Expression *, const Variable *> LookupDefinedName(const std::string &name) const;
  const Expression &LookupConstant(const std::string &name) const;
  const Variable &LookupVariable(const std::string &name) const;
  Term LookupFunction(const std::string &name, const std::vector<Term> &arguments) const;
 
  void PushScope() { scope_variables_.push(); }
 
  void PopScope() { scope_variables_.pop(); }
 
  std::string MakeUniqueName(const std::string &name);
 
  Smt2Scanner *scanner() { return scanner_; }
 
 private:
  Smt2Scanner *scanner_{nullptr};  
 
  ScopedUnorderedMap<std::string, Expression> scope_constants_;          
  ScopedUnorderedMap<std::string, Variable> scope_variables_;            
  ScopedUnorderedMap<std::string, FunctionDefinition> scope_functions_;  
 
  int64_t nextUniqueId_{};  
};
 
}  // namespace dlinear::smt2