Squashed merge of SygusComp 2015 branch.

1 files changed, 27 insertions, 0 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 53241709d..9c2c7f7be 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -42,6 +42,33 @@ class FunctionType;
 class Type;
 class ResourceManager;
 
+//for sygus gterm two-pass parsing
+class CVC4_PUBLIC SygusGTerm {
+public:
+  enum{
+    gterm_op,
+    gterm_let,
+    gterm_constant,
+    gterm_variable,
+    gterm_input_variable,
+    gterm_local_variable,
+    gterm_nested_sort,
+    gterm_unresolved,
+    gterm_ignore,
+  };
+  Type d_type;
+  Expr d_expr;
+  std::vector< Expr > d_let_vars;
+  unsigned d_gterm_type;
+  std::string d_name;
+  std::vector< SygusGTerm > d_children;
+  
+  unsigned getNumChildren() { return d_children.size(); }
+  void addChild(){
+    d_children.push_back( SygusGTerm() );
+  }
+};
+
 namespace parser {
 
 class Input;