summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.h
diff options
context:
space:
mode:
authorChristopher L. Conway <christopherleeconway@gmail.com>2010-06-01 20:19:30 +0000
committerChristopher L. Conway <christopherleeconway@gmail.com>2010-06-01 20:19:30 +0000
commitb8f8e92c5cdd2d556d06e722e2e27b7c18a36216 (patch)
tree16d5ba574505ec2007d085bcc2044654e896a533 /src/parser/smt2/smt2.h
parente681d67764508a94b812f309a714745eca027ad6 (diff)
Adding SMT v2 parsing support for: QF_IDL, QF_NIA, QF_RDL, QF_UFIDL
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r--src/parser/smt2/smt2.h9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 0bb3020a3..5eae90fa3 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -35,11 +35,20 @@ class Smt2 : public Parser {
public:
enum Logic {
+ AUFLIA,
+ AUFLIRA,
+ AUFNIRA,
+ QF_AUFBV,
+ QF_AUFLIA,
QF_AX,
QF_BV,
+ QF_IDL,
QF_LIA,
QF_LRA,
+ QF_NIA,
+ QF_RDL,
QF_UF,
+ QF_UFIDL
};
enum Theory {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback