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.

2 files changed, 11 insertions, 7 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 03029f27e..69ba63a47 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -392,18 +392,22 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     case kind::APPLY_SELECTOR:
     case kind::APPLY_SELECTOR_TOTAL: {
-        TypeNode t = n.getType();
+        TypeNode t = n[0].getType();
+        Node opn = n.getOperator();
         if( t.isTuple() ){
           toStream(out, n[0], depth, types, true);
-          out << '.' << Datatype::indexOf( n.getOperator().toExpr() );
+          const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
+          int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
+          out << '.' << sindex;
         }else if( t.isRecord() ){
           toStream(out, n[0], depth, types, true);
           const Record& rec = t.getRecord();
-          unsigned index = Datatype::indexOf( n.getOperator().toExpr() );
-          std::pair<std::string, Type> fld = rec[index];
+          const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
+          int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
+          std::pair<std::string, Type> fld = rec[sindex];
           out << '.' << fld.first;
         }else{
-          toStream(op, n.getOperator(), depth, types, false);
+          toStream(op, opn, depth, types, false);
         }
       }
       break;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 923574fae..074041262 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -825,10 +825,10 @@ static string smtKindString(Kind k) throw() {
   case kind::GEQ: return ">=";
   case kind::DIVISION:
   case kind::DIVISION_TOTAL: return "/";
+  case kind::INTS_DIVISION_TOTAL: 
   case kind::INTS_DIVISION: return "div";
-  case kind::INTS_DIVISION_TOTAL: return "INTS_DIVISION_TOTAL";
+  case kind::INTS_MODULUS_TOTAL: 
   case kind::INTS_MODULUS: return "mod";
-  case kind::INTS_MODULUS_TOTAL: return "INTS_MODULUS_TOTAL";
   case kind::ABS: return "abs";
   case kind::IS_INTEGER: return "is_int";
   case kind::TO_INTEGER: return "to_int";