Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.

1 files changed, 18 insertions, 0 deletions

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 42fb7381c..40a5b5849 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -207,6 +207,24 @@ public:
   bool hasEPRAxiom( TypeNode tn ) const { return d_epr_axiom.find( tn )!=d_epr_axiom.end(); }
 };
 
+class TermRecBuild {
+private:
+  std::vector< Node > d_term;
+  std::vector< std::vector< Node > > d_children;
+  std::vector< Kind > d_kind;
+  std::vector< bool > d_has_op;
+  std::vector< unsigned > d_pos;
+  void addTerm( Node n );
+public:
+  TermRecBuild(){}
+  void init( Node n );
+  void push( unsigned p );
+  void pop();
+  void replaceChild( unsigned i, Node n );
+  Node getChild( unsigned i );
+  Node build( unsigned p=0 );
+};
+
 }
 }