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, 72 insertions, 0 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 21ad032f3..b34abba13 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -531,3 +531,75 @@ Node QuantEPR::mkEPRAxiom( TypeNode tn ) {
   }
 }
 
+
+void TermRecBuild::addTerm( Node n ) {
+  d_term.push_back( n );
+  std::vector< Node > currc;
+  d_kind.push_back( n.getKind() );
+  if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){
+    currc.push_back( n.getOperator() );
+    d_has_op.push_back( true );
+  }else{
+    d_has_op.push_back( false );
+  }
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    currc.push_back( n[i] );
+  }
+  d_children.push_back( currc );  
+}
+
+void TermRecBuild::init( Node n ) {
+  Assert( d_term.empty() );
+  addTerm( n );
+}
+
+void TermRecBuild::push( unsigned p ) {
+  Assert( !d_term.empty() );
+  unsigned curr = d_term.size()-1;
+  Assert( d_pos.size()==curr );
+  Assert( d_pos.size()+1==d_children.size() );
+  Assert( p<d_term[curr].getNumChildren() );
+  addTerm( d_term[curr][p] );
+  d_pos.push_back( p );
+}
+
+void TermRecBuild::pop() {
+  Assert( !d_pos.empty() );
+  d_pos.pop_back();
+  d_kind.pop_back();
+  d_has_op.pop_back();
+  d_children.pop_back();
+  d_term.pop_back(); 
+}
+
+void TermRecBuild::replaceChild( unsigned i, Node n ) {
+  Assert( !d_term.empty() );
+  unsigned curr = d_term.size()-1;
+  unsigned o = d_has_op[curr] ? 1 : 0;
+  d_children[curr][i+o] = n;
+}
+
+Node TermRecBuild::getChild( unsigned i ) {
+  unsigned curr = d_term.size()-1;
+  unsigned o = d_has_op[curr] ? 1 : 0;
+  return d_children[curr][i+o];
+}
+
+Node TermRecBuild::build( unsigned d ) {
+  Assert( d_pos.size()+1==d_term.size() );
+  Assert( d<d_term.size() );
+  int p = d<d_pos.size() ? d_pos[d] : -2;
+  std::vector< Node > children;
+  unsigned o = d_has_op[d] ? 1 : 0;
+  for( unsigned i=0; i<d_children[d].size(); i++ ){
+    Node nc;
+    if( p+o==i ){
+      nc = build( d+1 );
+    }else{
+      nc = d_children[d][i];
+    }
+    children.push_back( nc );
+  }
+  return NodeManager::currentNM()->mkNode( d_kind[d], children );
+}
+