diff options
| author | Kevin Laeufer | 2021-09-08 15:00:46 -0700 |
|---|---|---|
| committer | GitHub | 2021-09-08 22:00:46 +0000 |
| commit | f76640d9dc4620a3b61975d54e5783c36e7c6936 (patch) | |
| tree | 714b0053f200f6c26d66f7443f24c158efa286f1 /src/main/scala/firrtl/backends/experimental/smt/SMTCommand.scala | |
| parent | 0c1ca581efe7fbad99ffc713a3802b5f2ffb68b6 (diff) | |
smt: refactor SMT expression library (#2347)
Diffstat (limited to 'src/main/scala/firrtl/backends/experimental/smt/SMTCommand.scala')
| -rw-r--r-- | src/main/scala/firrtl/backends/experimental/smt/SMTCommand.scala | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/main/scala/firrtl/backends/experimental/smt/SMTCommand.scala b/src/main/scala/firrtl/backends/experimental/smt/SMTCommand.scala new file mode 100644 index 00000000..21a64f98 --- /dev/null +++ b/src/main/scala/firrtl/backends/experimental/smt/SMTCommand.scala @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: Apache-2.0 +// Author: Kevin Laeufer <laeufer@cs.berkeley.edu> + +package firrtl.backends.experimental.smt + +private sealed trait SMTCommand +private case class Comment(msg: String) extends SMTCommand +private case class SetLogic(logic: String) extends SMTCommand +private case class DefineFunction(name: String, args: Seq[SMTFunctionArg], e: SMTExpr) extends SMTCommand +private case class DeclareFunction(sym: SMTSymbol, args: Seq[SMTFunctionArg]) extends SMTCommand +private case class DeclareUninterpretedSort(name: String) extends SMTCommand +private case class DeclareUninterpretedSymbol(name: String, tpe: String) extends SMTCommand |