Add support for non-SMT-COMP features in a new flag

lexer.l

@@ -93,6 +93,7 @@ KEYWORD             :[a-zA-Z0-9._+\-*=%/?!$_~&^<>@]+
 "exit"           { return TK_EXIT; }
 "pop"            { return TK_POP; }
 "push"           { return TK_PUSH; }
+"reset"          { return TK_RESET; }
 "set-info"       { return TK_SET_INFO; }
 "set-logic"      { return TK_SET_LOGIC; }
 "set-option"     { return TK_SET_OPTION; }
@@ -101,6 +102,13 @@ KEYWORD             :[a-zA-Z0-9._+\-*=%/?!$_~&^<>@]+
 ":pattern"     { return TK_PATTERN; }
 ":named"       { return TK_NAMED; }
 
+":qid"         { return TK_QID; }
+":no-pattern"  { return TK_NOPATTERN; }
+":skolemid"    { return TK_SKOLEMID; }
+":lblpos"      { return TK_LBLPOS; }
+":lblneg"      { return TK_LBLNEG; }
+":weight"      { return TK_WEIGHT; }
+
 {NUMERAL}      { yylval.string = c_strdup(yytext); return NUMERAL; }
 {DECIMAL}      { yylval.string = c_strdup(yytext); return DECIMAL; }
 {HEXADECIMAL}  { yylval.string = c_strdup(yytext); return HEXADECIMAL; }

parser.y

@@ -44,6 +44,10 @@ void yyerror(const char *s);
 
 using namespace scrambler;
 
+extern bool support_non_smtcomp;
+
+extern bool support_z3;
+
 %}
 
 %locations
@@ -101,6 +105,18 @@ using namespace scrambler;
 %token TK_PATTERN       ":pattern"
 %token TK_NAMED         ":named"
 
+// begin non-smtcomp tokens
+
+%token TK_RESET         "reset"
+%token TK_QID           ":qid"
+%token TK_NOPATTERN     ":no-pattern"
+%token TK_SKOLEMID      ":skolemid"
+%token TK_LBLPOS        ":lblpos"
+%token TK_LBLNEG        ":lblneg"
+%token TK_WEIGHT        ":weight"
+
+// end non-smtcomp tokens
+
 %type <nodelist>    sort_dec_list
 %type <curnode>     sort_dec
 %type <nodelist>    datatype_dec_list
@@ -200,6 +216,7 @@ command :
 | cmd_exit
 | cmd_pop
 | cmd_push
+| cmd_reset
 | cmd_set_logic
 | cmd_set_info
 | cmd_set_option
@@ -344,6 +361,17 @@ cmd_push : '(' TK_PUSH NUMERAL ')'
   }
 ;
 
+cmd_reset : '(' TK_RESET ')'
+  {
+      if (!support_non_smtcomp) {
+          // not allowed in SMT-COMP
+          yyerror("Encountered non-SMT-COMP command: 'reset'. Maybe you "
+                  "want to re-run with '-support-non-smtcomp true'.");
+      }
+      add_node("reset");
+  }
+;
+
 cmd_set_info :
   '(' TK_SET_INFO KEYWORD ')'
   {
@@ -371,11 +399,16 @@ cmd_set_logic : '(' TK_SET_LOGIC SYMBOL ')'
 // core track only
 cmd_set_option : '(' TK_SET_OPTION KEYWORD attribute_value ')'
   {
-      if (strcmp($3, ":produce-unsat-cores") != 0 || $4->symbol != "true") {
-        yyerror("set-option"); // not allowed in SMT-COMP
+      if (!support_non_smtcomp) {
+          if (strcmp($3, ":produce-unsat-cores") != 0 || $4->symbol != "true") {
+            // not allowed in SMT-COMP
+            yyerror("Encountered non-SMT-COMP command: 'set-option'. Maybe you "
+                    "want to re-run with '-support-non-smtcomp true'.");
+          }
+          delete $4;
+      } else {
+        add_node("set-option", make_node($3), $4);
       }
-      //add_node("set-option", make_node($3), $4);
-      /*//*/delete $4;
       free($3);
   }
 ;
@@ -762,6 +795,80 @@ attribute :
       $$->set_parens_needed(false);
       delete $3;
   }
+| TK_QID SYMBOL
+  {
+      // z3
+      if (!support_z3) {
+          // not allowed in SMT-COMP
+          yyerror("Encountered z3-specific attribute: ':qid'. Maybe you "
+                  "want to re-run with '-support-z3 true'.");
+      }
+      set_new_name($2);
+      $$ = make_node(":qid", make_name_node($2));
+      $$->set_parens_needed(false);
+      delete $2;
+  }
+| TK_NOPATTERN '(' term_list ')'
+  {
+      // z3
+      if (!support_z3) {
+          // not allowed in SMT-COMP
+          yyerror("Encountered z3-specific attribute: ':no-pattern'. Maybe you "
+                  "want to re-run with '-support-z3 true'.");
+      }
+      $$ = make_node(":no-pattern", make_node($3));
+      $$->set_parens_needed(false);
+      delete $3;
+  }
+| TK_SKOLEMID SYMBOL
+  {
+      // z3
+      if (!support_z3) {
+          // not allowed in SMT-COMP
+          yyerror("Encountered z3-specific attribute: ':skolemid'. Maybe you "
+                  "want to re-run with '-support-z3 true'.");
+      }
+      set_new_name($2);
+      $$ = make_node(":skolemid", make_name_node($2));
+      $$->set_parens_needed(false);
+      delete $2;
+  }
+| TK_LBLPOS SYMBOL
+  {
+      // z3
+      if (!support_z3) {
+          // not allowed in SMT-COMP
+          yyerror("Encountered z3-specific attribute: ':lblpos'. Maybe you "
+                  "want to re-run with '-support-z3 true'.");
+      }
+      $$ = make_node(":lblpos", make_node($2));
+      $$->set_parens_needed(false);
+      delete $2;
+  }
+| TK_LBLNEG SYMBOL
+  {
+      // z3
+      if (!support_z3) {
+          // not allowed in SMT-COMP
+          yyerror("Encountered z3-specific attribute: ':lblneg'. Maybe you "
+                  "want to re-run with '-support-z3 true'.");
+      }
+      $$ = make_node(":lblneg", make_node($2));
+      $$->set_parens_needed(false);
+      delete $2;
+  }
+| TK_WEIGHT NUMERAL
+  {
+      // z3
+      if (!support_z3) {
+          // not allowed in SMT-COMP
+          yyerror("Encountered z3-specific attribute: ':weight'. Maybe you "
+                  "want to re-run with '-support-z3 true'.");
+      }
+      $$ = make_node(":weight", make_node($2));
+      $$->set_parens_needed(false);
+      delete $2;
+  }
 ;
 
 ////////////////////////////////////////////////////////////////////////////////

process.non-smtcomp

@@ -0,0 +1,11 @@
+#!/bin/sh
+
+# This is a wrapper script that allows the scrambler to be used as a
+# preprocessor on StarExec.
+
+# $1: benchmark filename
+# $2: seed
+
+ulimit -s 131072
+./scrambler -support-non-smtcomp true -seed "$2" < "$1"
+

process.z3

@@ -0,0 +1,10 @@
+#!/bin/sh
+
+# This is a wrapper script that allows the scrambler to be used as a
+# preprocessor on StarExec.
+
+# $1: benchmark filename
+# $2: seed
+
+ulimit -s 131072
+./scrambler -support-z3 true -seed "$2" < "$1"

scrambler.cpp

@@ -88,6 +88,17 @@ bool gen_ucore = false;
  */
 bool gen_mval = false;
 
+/*
+ * If set to true, support SMTLIB files that have features not supported by
+ * SMTCOMP
+ */
+bool support_non_smtcomp = false;
+
+/*
+ * If set to true, support SMTLIB files that have Z3-specific features
+ */
+bool support_z3 = false;
+
 ////////////////////////////////////////////////////////////////////////////////
 
 /*
@@ -821,23 +832,38 @@ void usage(const char *program)
     std::cout << "Syntax: " << program << " [OPTIONS] < INPUT_FILE.smt2\n"
               << "\n"
               << "    -term_annot [true|false]\n"
-              << "        controls whether term annotations are printed (default: true)\n"
+              << "        controls whether term annotations are printed "
+                 "(default: true)\n"
               << "\n"
               << "    -seed N\n"
-              << "        seed value (>= 0) for pseudo-random choices; if 0, no scrambling is\n"
+              << "        seed value (>= 0) for pseudo-random choices; if 0, "
+                 "no scrambling is\n"
               << "        performed (default: time(0))\n"
               << "\n"
               << "    -core FILE\n"
-              << "        print only those (named) assertions whose name is contained in the\n"
+              << "        print only those (named) assertions whose name is "
+                 "contained in the\n"
               << "        specified FILE (default: print all assertions)\n"
               << "\n"
               << "    -gen-unsat-core [true|false]\n"
-              << "        controls whether the output is in a format suitable for the unsat-core\n"
+              << "        controls whether the output is in a format suitable "
+                 "for the unsat-core\n"
               << "        track of SMT-COMP (default: false)\n"
               << "\n"
               << "    -gen-model-val [true|false]\n"
-              << "        controls whether the output is in a format suitable for the model\n"
-              << "        track of SMT-COMP (default: false)\n";
+              << "        controls whether the output is in a format suitable "
+                 "for the model\n"
+              << "        track of SMT-COMP (default: false)\n"
+              << "\n"
+              << "    -support-non-smtcomp [true|false]\n"
+              << "        controls whether to support SMTLIB commands that are "
+                 "not supported\n"
+              << "        by SMTCOMP (default: false)\n"
+              << "\n"
+              << "    -support-z3 [true|false]\n"
+              << "        controls whether to support non-SMTLIB commands that "
+                 "are supported\n"
+              << "        by Z3 (default: false)\n";
     std::cout.flush();
     exit(1);
 }
@@ -903,6 +929,25 @@ int main(int argc, char **argv)
                 usage(argv[0]);
             }
             i += 2;
+        } else if (strcmp(argv[i], "-support-non-smtcomp") == 0 &&
+                   i + 1 < argc) {
+            if (strcmp(argv[i + 1], "true") == 0) {
+                support_non_smtcomp = true;
+            } else if (strcmp(argv[i + 1], "false") == 0) {
+                support_non_smtcomp = false;
+            } else {
+                usage(argv[0]);
+            }
+            i += 2;
+        } else if (strcmp(argv[i], "-support-z3") == 0 && i + 1 < argc) {
+            if (strcmp(argv[i + 1], "true") == 0) {
+                support_z3 = true;
+            } else if (strcmp(argv[i + 1], "false") == 0) {
+                support_z3 = false;
+            } else {
+                usage(argv[0]);
+            }
+            i += 2;
         } else {
             usage(argv[0]);
         }

test/extensions/non-smtcomp/expect/test-non-smtcomp.0.non-smtcomp.expect

@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-option :print-success false)
+(declare-fun x () Bool)
+(assert (and (not x) x))
+(check-sat)
+(reset)
+(declare-fun x () Bool)
+(assert x)
+(check-sat)
+(exit)

test/extensions/non-smtcomp/expect/test-non-smtcomp.1234.non-smtcomp.expect

@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-option :print-success false)
+(declare-fun x1 () Bool)
+(assert (and x1 (not x1)))
+(check-sat)
+(reset)
+(declare-fun x1 () Bool)
+(assert x1)
+(check-sat)
+(exit)

test/extensions/non-smtcomp/test-non-smtcomp.smt2

@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-option :print-success false)
+(declare-fun x () Bool)
+(assert (and (not x) x))
+(check-sat)
+(reset)
+(declare-fun x () Bool)
+(assert x)
+(check-sat)
+(exit)

test/extensions/z3/expect/test-z3.0.z3.expect

@@ -0,0 +1,15 @@
+(set-logic ALL)
+(declare-sort |T@U| 0)
+(declare-fun UOrdering2 (|T@U| |T@U|) Bool)
+(declare-fun U_2_int (T@U) Int)
+(declare-fun U_2_bool (T@U) Bool)
+(declare-fun Inv0_TBitvector (T@U) Int)
+(declare-fun TBitvector (Int) T@U)
+(declare-fun %lbl%+0 () Bool)
+(declare-fun %lbl%@1 () Bool)
+(assert (forall ((x@@3 T@U)) (! (UOrdering2 x@@3 x@@3) :qid |id1| :no-pattern (U_2_int x@@3) :no-pattern (U_2_bool x@@3))))
+(assert (forall ((w Int)) (! (= (Inv0_TBitvector (TBitvector w)) w) :qid |id2| :skolemid |0| :pattern ((TBitvector w)) :weight 0)))
+(assert (! (and %lbl%+0 true) :lblpos +0))
+(assert (! (or %lbl%@1 true) :lblneg @1))
+(check-sat)
+(exit)

test/extensions/z3/expect/test-z3.1234.z3.expect

@@ -0,0 +1,15 @@
+(set-logic ALL)
+(declare-sort x2 0)
+(declare-fun x8 () Bool)
+(declare-fun x5 (x2) Int)
+(declare-fun x7 (Int) x2)
+(declare-fun x3 (x2) Bool)
+(declare-fun x10 (x2 x2) Bool)
+(declare-fun x4 () Bool)
+(declare-fun x1 (x2) Int)
+(assert (! (or true x8) :lblneg @1))
+(assert (forall ((x11 x2)) (! (x10 x11 x11) :qid x13 :no-pattern (x5 x11) :no-pattern (x3 x11))))
+(assert (! (and x4 true) :lblpos +0))
+(assert (forall ((x12 Int)) (! (= (x1 (x7 x12)) x12) :qid x9 :skolemid x6 :pattern ((x7 x12)) :weight 0)))
+(check-sat)
+(exit)

test/extensions/z3/test-z3.smt2

@@ -0,0 +1,25 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.0)
+(declare-sort |T@U| 0)
+(declare-fun UOrdering2 (|T@U| |T@U|) Bool)
+(declare-fun U_2_int (T@U) Int)
+(declare-fun U_2_bool (T@U) Bool)
+(declare-fun Inv0_TBitvector (T@U) Int)
+(declare-fun TBitvector (Int) T@U)
+(declare-fun %lbl%+0 () Bool)
+(declare-fun %lbl%@1 () Bool)
+(assert (forall ((x@@3 T@U) ) (! (UOrdering2 x@@3 x@@3)
+ :qid |id1|
+ :no-pattern (U_2_int x@@3)
+ :no-pattern (U_2_bool x@@3)
+)))
+(assert (forall ((w Int) ) (! (= (Inv0_TBitvector (TBitvector w)) w)
+ :qid |id2|
+ :skolemid |0|
+ :pattern ( (TBitvector w))
+ :weight 0
+)))
+(assert (! (and %lbl%+0 true) :lblpos +0))
+(assert (! (or %lbl%@1 true) :lblneg @1))
+(check-sat)
+(exit)