Sygus clean main (#1297)

* Remove front end hack for sygus.

* Remove other hack, add sygus solution output mode.

* Clang format

* Minor

* Fix

* Minor

* Remove unused field.

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 8ffb47e40fbddd589808b57a21b9b0fcf2273bba..ebfc7266bbb2d150cb4260dc30f3a743688a2221 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -187,16 +187,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
   }
 
-  // if doing sygus, turn on CEGQI by default
-  if(opts.getInputLanguage() == language::input::LANG_SYGUS ){
-    if( !opts.wasSetByUserCeGuidedInst()) {
-      opts.setCeGuidedInst(true);
-    }
-    if( !opts.wasSetByUserDumpSynth()) {
-      opts.setDumpSynth(true);
-    }
-  }
-
   // Determine which messages to show based on smtcomp_mode and verbosity
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(&CVC4::null_os);

diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index ff889bcb237e5b96e92b589e526662e7ccf5ba4f..54027c128679cf958926a31fab1b73b6cef08511 100644 (file)
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -252,6 +252,7 @@ liboptions_la_SOURCES = \
        set_language.h \
        simplification_mode.cpp \
        simplification_mode.h \
+       sygus_out_mode.h \
        theoryof_mode.cpp \
        theoryof_mode.h \
        ufss_mode.h

diff --git a/src/options/options.h b/src/options/options.h
index f9366309595104ebf7fd5e322625eb468ca35e1c..474ef0f964be342d448da1fca1918a226eebbfab 100644 (file)
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -242,8 +242,6 @@ public:
 
 
   // TODO: Document these.
-  void setCeGuidedInst(bool);
-  void setDumpSynth(bool);
   void setInputLanguage(InputLanguage);
   void setInteractive(bool);
   void setOut(std::ostream*);

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 351c8b608153b817e7bac00c5b52f6505fef1f87..3d74091fd22b32ec3fff9393f158b4538545d535 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -554,7 +554,6 @@ all \n\
 \n\
 ";
 
-
 theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg == "pre-full") {
     return theory::quantifiers::INST_WHEN_PRE_FULL;
@@ -1311,6 +1310,56 @@ SimplificationMode OptionsHandler::stringToSimplificationMode(std::string option
   }
 }
 
+const std::string OptionsHandler::s_sygusSolutionOutModeHelp =
+    "\
+Modes for finite model finding bound minimization, supported by --sygus-out:\n\
+\n\
+status \n\
++ Print only status for check-synth calls.\n\
+\n\
+status-and-def (default) \n\
++ Print status followed by definition corresponding to solution.\n\
+\n\
+status-or-def \n\
++ Print status if infeasible, or definition corresponding to\n\
+  solution if feasible.\n\
+\n\
+sygus-standard \n\
++ Print based on SyGuS standard.\n\
+\n\
+";
+
+SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode(
+    std::string option, std::string optarg) throw(OptionException)
+{
+  if (optarg == "status")
+  {
+    return SYGUS_SOL_OUT_STATUS;
+  }
+  else if (optarg == "status-and-def")
+  {
+    return SYGUS_SOL_OUT_STATUS_AND_DEF;
+  }
+  else if (optarg == "status-or-def")
+  {
+    return SYGUS_SOL_OUT_STATUS_OR_DEF;
+  }
+  else if (optarg == "sygus-standard")
+  {
+    return SYGUS_SOL_OUT_STANDARD;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_sygusSolutionOutModeHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --sygus-out: `")
+                          + optarg
+                          + "'.  Try --sygus-out help.");
+  }
+}
 
 void OptionsHandler::setProduceAssertions(std::string option, bool value) throw() {
   options::produceAssertions.set(value);

diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index c525c9e0e7c1053f77ff0dd42c1a77a64ad7a1b6..9d5f8cc6eae5e4cdbc589eb380f6d887fc1e983f 100644 (file)
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -28,14 +28,15 @@
 #include "options/arith_unate_lemma_mode.h"
 #include "options/base_handlers.h"
 #include "options/bv_bitblast_mode.h"
-#include "options/decision_mode.h"
 #include "options/datatypes_modes.h"
+#include "options/decision_mode.h"
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/options.h"
 #include "options/printer_modes.h"
 #include "options/quantifiers_modes.h"
 #include "options/simplification_mode.h"
+#include "options/sygus_out_mode.h"
 #include "options/theoryof_mode.h"
 #include "options/ufss_mode.h"
 
@@ -143,6 +144,8 @@ public:
   void notifyBeforeSearch(const std::string& option) throw(ModalException);
   void notifyDumpMode(std::string option) throw(OptionException);
   SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException);
+  SygusSolutionOutMode stringToSygusSolutionOutMode(
+      std::string option, std::string optarg) throw(OptionException);
   void setProduceAssertions(std::string option, bool value) throw();
   void proofEnabledBuild(std::string option, bool value) throw(OptionException);
   void LFSCEnabledBuild(std::string option, bool value);
@@ -218,6 +221,7 @@ public:
   static const std::string s_qcfModeHelp;
   static const std::string s_qcfWhenModeHelp;
   static const std::string s_simplificationHelp;
+  static const std::string s_sygusSolutionOutModeHelp;
   static const std::string s_cbqiBvIneqModeHelp;
   static const std::string s_cegqiSingleInvHelp;
   static const std::string s_sygusInvTemplHelp;

diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 7d71c267a95f100f02ceef7b5cb7a65ff19a7b8c..b8db9d9daa4a4fa5ce0b5dd05c77b1aac575d8b1 100644 (file)
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -241,13 +241,6 @@ std::ostream* Options::currentGetOut() {
 
 
 // TODO: Document these.
-void Options::setCeGuidedInst(bool value) {
-  set(options::ceGuidedInst, value);
-}
-
-void Options::setDumpSynth(bool value) {
-  set(options::dumpSynth, value);
-}
 
 void Options::setInputLanguage(InputLanguage value) {
   set(options::inputLanguage, value);

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index ba7c8338a103aa2723fce3e9d451be6230fb18ca..c92813bf4e4a20733646759233d7c267bbd90973 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -246,7 +246,7 @@ option conjectureGenMaxDepth --conjecture-gen-max-depth=N int :default 3
 ### synthesis options 
 
 option ceGuidedInst --cegqi bool :default false :read-write
-  counterexample-guided quantifier instantiation
+  counterexample-guided quantifier instantiation for sygus
 option cegqiSingleInvMode --cegqi-si=MODE CVC4::theory::quantifiers::CegqiSingleInvMode :default CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToCegqiSingleInvMode :read-write
   mode for processing single invocation synthesis conjectures
 option cegqiSingleInvPartial --cegqi-si-partial bool :default false

diff --git a/src/options/smt_options b/src/options/smt_options
index 00424e10315f5cb0e42ee297be02a198959ea7f7..c701d5c203ef92edc586c52f38ab4ffd7caac42d 100644 (file)
--- a/src/options/smt_options
+++ b/src/options/smt_options
@@ -39,6 +39,8 @@ option dumpProofs --dump-proofs bool :default false :link --proof :link-smt prod
  output proofs after every UNSAT/VALID response
 option dumpInstantiations --dump-instantiations bool :default false
  output instantiations of quantified formulas after every UNSAT/VALID response
+option sygusOut --sygus-out=MODE SygusSolutionOutMode :default SYGUS_SOL_OUT_STATUS_AND_DEF :include "options/sygus_out_mode.h" :handler stringToSygusSolutionOutMode :read-write
+  output mode for sygus
 option dumpSynth --dump-synth bool :read-write :default false
  output solution for synthesis conjectures after every UNSAT/VALID response
 option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch

diff --git a/src/options/sygus_out_mode.h b/src/options/sygus_out_mode.h
new file mode 100644 (file)
index 0000000..9f94be2
--- /dev/null
+++ b/src/options/sygus_out_mode.h
@@ -0,0 +1,39 @@
+/*********************                                                        */
+/*! \file sygus_out_mode.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Options for sygus solution output.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__SYGUS_OUT_MODE_H
+#define __CVC4__SMT__SYGUS_OUT_MODE_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+
+/** Mode for printing sygus solutions. */
+enum SygusSolutionOutMode
+{
+  /** print status */
+  SYGUS_SOL_OUT_STATUS,
+  /** (default) print status and solution */
+  SYGUS_SOL_OUT_STATUS_AND_DEF,
+  /** print status if infeasible, or solution if feasible */
+  SYGUS_SOL_OUT_STATUS_OR_DEF,
+  /** print output specified by sygus standard */
+  SYGUS_SOL_OUT_STANDARD,
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__SMT__SYGUS_OUT_MODE_H */

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 8012c868ca2b0be80295d423c8b717e1426fc026..fee1099234b69b0fb8586fffd96c95b6b23d64a7 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -383,8 +383,8 @@ CheckSynthCommand::CheckSynthCommand() throw() :
   d_expr() {
 }
 
-CheckSynthCommand::CheckSynthCommand(const Expr& expr, bool inUnsatCore) throw() :
-  d_expr(expr), d_inUnsatCore(inUnsatCore) {
+CheckSynthCommand::CheckSynthCommand(const Expr& expr) throw() :
+  d_expr(expr) {
 }
 
 Expr CheckSynthCommand::getExpr() const throw() {
@@ -395,6 +395,33 @@ void CheckSynthCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->checkSynth(d_expr);
     d_commandStatus = CommandSuccess::instance();
+    smt::SmtScope scope(smtEngine);
+    d_solution.clear();
+    // check whether we should print the status
+    if (d_result.asSatisfiabilityResult() != Result::UNSAT
+        || options::sygusOut() == SYGUS_SOL_OUT_STATUS_AND_DEF
+        || options::sygusOut() == SYGUS_SOL_OUT_STATUS)
+    {
+      if (options::sygusOut() == SYGUS_SOL_OUT_STANDARD)
+      {
+        d_solution << "(fail)" << endl;
+      }
+      else
+      {
+        d_solution << d_result << endl;
+      }
+    }
+    // check whether we should print the solution
+    if (d_result.asSatisfiabilityResult() == Result::UNSAT
+        && options::sygusOut() != SYGUS_SOL_OUT_STATUS)
+    {
+      // printing a synthesis solution is a non-constant
+      // method, since it invokes a sophisticated algorithm
+      // (Figure 5 of Reynolds et al. CAV 2015).
+      // Hence, we must call here print solution here,
+      // instead of during printResult.
+      smtEngine->printSynthSolution(d_solution);
+    }
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
@@ -408,18 +435,18 @@ void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
-    out << d_result << endl;
+    out << d_solution.str();
   }
 }
 
 Command* CheckSynthCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+  CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap));
   c->d_result = d_result;
   return c;
 }
 
 Command* CheckSynthCommand::clone() const {
-  CheckSynthCommand* c = new CheckSynthCommand(d_expr, d_inUnsatCore);
+  CheckSynthCommand* c = new CheckSynthCommand(d_expr);
   c->d_result = d_result;
   return c;
 }

diff --git a/src/smt/command.h b/src/smt/command.h
index f5be9ddfee195225a2be8f0ee63e541c12c5fa4b..a60c85a3cf1ae5e9a4593d260d10cfcc20829d00 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -529,13 +529,9 @@ public:
 };/* class QueryCommand */
 
 class CVC4_PUBLIC CheckSynthCommand : public Command {
-protected:
-  Expr d_expr;
-  Result d_result;
-  bool d_inUnsatCore;
 public:
   CheckSynthCommand() throw();
-  CheckSynthCommand(const Expr& expr, bool inUnsatCore = true) throw();
+  CheckSynthCommand(const Expr& expr) throw();
   ~CheckSynthCommand() throw() {}
   Expr getExpr() const throw();
   void invoke(SmtEngine* smtEngine);
@@ -544,6 +540,14 @@ public:
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
   Command* clone() const;
   std::string getCommandName() const throw();
+
+ protected:
+  /** the assertion of check-synth */
+  Expr d_expr;
+  /** result of the check-synth call */
+  Result d_result;
+  /** string stream that stores the output of the solution */
+  std::stringstream d_solution;
 };/* class CheckSynthCommand */
 
 // this is TRANSFORM in the CVC presentation language

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f93d8bd7ffcd4c028e717e20464921e5fb129971..2ff1156061d9bdf696da06a1ff893017770391bf 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1294,6 +1294,13 @@ void SmtEngine::setDefaults() {
     options::bitvectorDivByZeroConst.set(options::inputLanguage()
                                          == language::input::LANG_SMTLIB_V2_6);
   }
+  if (options::inputLanguage() == language::input::LANG_SYGUS)
+  {
+    if (!options::ceGuidedInst.wasSetByUser())
+    {
+      options::ceGuidedInst.set(true);
+    }
+  }
 
   if(options::forceLogicString.wasSetByUser()) {
     d_logic = LogicInfo(options::forceLogicString());

diff --git a/test/regress/regress0/expect/scrub.07.sy b/test/regress/regress0/expect/scrub.07.sy
index cf0e37c9f1689960d7148a1b1adfca83b8810283..79b917c7a9a9cf5a46e9a811cb912e980b881f49 100644 (file)
--- a/test/regress/regress0/expect/scrub.07.sy
+++ b/test/regress/regress0/expect/scrub.07.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (declare-var n Int)
 

diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
index 7f78dbc481fc357d0ee7949559749fd5a82a1eaa..360474f84239ff799feed70e5ea9e2a2c06f89f8 100644 (file)
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
 ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 ; EXPECT: The fact in question: TERM

diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy
index ee26fac79bc4e3049dc9143fa1dcd60ddebef33d..1792749e275e781cfa2a855efa0e745bde80b61b 100755 (executable)
--- a/test/regress/regress0/sygus/General_plus10.sy
+++ b/test/regress/regress0/sygus/General_plus10.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (synth-fun fb () Int ((Start Int ((Constant Int)))))

diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy
index e6683ced98c0300afc414056789d186192693274..41346e65530a891a74db580c2fcbb238848ee10f 100644 (file)
--- a/test/regress/regress0/sygus/array_search_2.sy
+++ b/test/regress/regress0/sygus/array_search_2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)

diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy
index 387ce94870ff3920fcb9946fe794d35dc6786358..84a75d0861ed936e9e5ac7606e7f6a0dee3cb80d 100644 (file)
--- a/test/regress/regress0/sygus/array_sum_2_5.sy
+++ b/test/regress/regress0/sygus/array_sum_2_5.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start)    (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)

diff --git a/test/regress/regress0/sygus/cegar1.sy b/test/regress/regress0/sygus/cegar1.sy
index dd7f73e272c96ba350a37a15cebba33d1184e010..ee85db88aeac32fd7c061bd06e730a630e59d20c 100644 (file)
--- a/test/regress/regress0/sygus/cegar1.sy
+++ b/test/regress/regress0/sygus/cegar1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth
+; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status
 (set-logic LIA)
 
 (synth-inv inv-f ((x Int) (y Int)))

diff --git a/test/regress/regress0/sygus/cggmp.sy b/test/regress/regress0/sygus/cggmp.sy
index 1ae1f53c05cc6ed85337f2ac97043606b5372040..a3247e4f4bcc7b053aea6dfce4c25b2104391d4a 100644 (file)
--- a/test/regress/regress0/sygus/cggmp.sy
+++ b/test/regress/regress0/sygus/cggmp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=pre --no-dump-synth
+; COMMAND-LINE: --sygus-inv-templ=pre --sygus-out=status
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy
index 2409b82d266a2d7eddf9b409b5abade22f83aa8b..43fd7c1ac17bfe731a309a81ae10b953996d77e5 100644 (file)
--- a/test/regress/regress0/sygus/clock-inc-tuple.sy
+++ b/test/regress/regress0/sygus/clock-inc-tuple.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 
 (set-logic ALL_SUPPORTED)
 (declare-var m Int)

diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy
index f675bddad7cae1c87d0e072c4d070922b12a77e3..24201b45366ac40fe6dd5a19fe26f04c2e57b6eb 100644 (file)
--- a/test/regress/regress0/sygus/commutative.sy
+++ b/test/regress/regress0/sygus/commutative.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy
index b79b7eeec6b4118a0af2a30c194675b252d2d6ef..305f5783a5a0f499436fdcb5a58452cec9527f50 100644 (file)
--- a/test/regress/regress0/sygus/const-var-test.sy
+++ b/test/regress/regress0/sygus/const-var-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy
index 5c48f5e39cc80a9f1ce8d4ee2c9f988bce78105b..1bb3e59fa551d0f9e7c352e9adf8e2f7d5b143f2 100644 (file)
--- a/test/regress/regress0/sygus/constant.sy
+++ b/test/regress/regress0/sygus/constant.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy
index 0a9fb9112ce57f74be10ed5de18fd7d6d528d92a..f4de9b055e6ffaaeefdc22b6a13700b60c127d61 100644 (file)
--- a/test/regress/regress0/sygus/dt-no-syntax.sy
+++ b/test/regress/regress0/sygus/dt-no-syntax.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 ; EXPECT: unsat
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy
index 0c28769b2e0cd553da207b07e6702e5cb8b2f96c..a6e8ac5c2ee0192175bd9e7627159cc1bf07351f 100644 (file)
--- a/test/regress/regress0/sygus/dt-test-ns.sy
+++ b/test/regress/regress0/sygus/dt-test-ns.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))

diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy
index bed9972fdba7a6499dab6c26b216e7cb7a56de85..e2c69282e08a88ca15a81c79fb49fc998b529939 100644 (file)
--- a/test/regress/regress0/sygus/dup-op.sy
+++ b/test/regress/regress0/sygus/dup-op.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ Start Start) x))

diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy
index 7b59f5f1a6ee0489740e1599b92d362dd2eeb12d..47099eeed3ae74c912b3e17cb9d3e8eb412e0f86 100644 (file)
--- a/test/regress/regress0/sygus/enum-test.sy
+++ b/test/regress/regress0/sygus/enum-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (define-sort D (Enum (a b)))
 (define-fun f ((x D)) Int (ite (= x D::a) 3 7))

diff --git a/test/regress/regress0/sygus/fg_polynomial3.sy b/test/regress/regress0/sygus/fg_polynomial3.sy
index dab92bb88c540af2a8f7b2b4776c33e17f6f0858..d70516bf156e3029125dca28e1d18ce9905a43a9 100644 (file)
--- a/test/regress/regress0/sygus/fg_polynomial3.sy
+++ b/test/regress/regress0/sygus/fg_polynomial3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy
index 2e6c6ef8108be63a1c16e613832386b32ec07596..1379d42063fb5e0a2f6cb3d3f106d12013fbaf56 100644 (file)
--- a/test/regress/regress0/sygus/hd-01-d1-prog.sy
+++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --cegqi --sygus-out=status
 
 (set-logic BV)
 

diff --git a/test/regress/regress0/sygus/icfp_14.12.sy b/test/regress/regress0/sygus/icfp_14.12.sy
index d9c19f8c19b1e591985b13746043c6877990a15d..51b86f0f5db4bdc23471ba856397e9b87036cf29 100644 (file)
--- a/test/regress/regress0/sygus/icfp_14.12.sy
+++ b/test/regress/regress0/sygus/icfp_14.12.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))

diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy
index 74e054159e229aad9bb6660a300becab0fab6144..212ae37f5ea2faf6ca12bed78473386dcfb8faad 100644 (file)
--- a/test/regress/regress0/sygus/icfp_28_10.sy
+++ b/test/regress/regress0/sygus/icfp_28_10.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic BV)
 

diff --git a/test/regress/regress0/sygus/icfp_easy-ite.sy b/test/regress/regress0/sygus/icfp_easy-ite.sy
index 248264698a0eaa865e316d5803a85e0403b3006b..f0cbbdc534b5c0661dbc7b83f6be0cb06fdc9dab 100644 (file)
--- a/test/regress/regress0/sygus/icfp_easy-ite.sy
+++ b/test/regress/regress0/sygus/icfp_easy-ite.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))

diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy
index b5642596417d532c1761cd13329942ce639fe7c7..ff68bc06c219554e5f5b31a05c943df0b8e537f5 100644 (file)
--- a/test/regress/regress0/sygus/inv-example.sy
+++ b/test/regress/regress0/sygus/inv-example.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-inv inv-f ((x Int) (y Int) (b Bool)))
 (declare-primed-var x Int)

diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index d5d40ace4d30d4dd7c4b2e596eafe2a942f7bc89..d26edffd2ee919abfb98f117dcd9c6c81045926b 100644 (file)
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
 (synth-fun f ((x Int)) Int

diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy
index d07f6a717d9c67127824a09b0f4a8f910bcddf3b..6f9d9fff9c760e8f048601a2f939958f75c5f4db 100644 (file)
--- a/test/regress/regress0/sygus/let-simp.sy
+++ b/test/regress/regress0/sygus/let-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int) (y Int)) Int
     ((Start Int (x

diff --git a/test/regress/regress0/sygus/list-head-x.sy b/test/regress/regress0/sygus/list-head-x.sy
index 8d209a9a00d341134717a645d3a3e1e4f3ea3a0d..6c5c1a97b2418d5ecfdecb246c3bae809463e75e 100644 (file)
--- a/test/regress/regress0/sygus/list-head-x.sy
+++ b/test/regress/regress0/sygus/list-head-x.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic ALL_SUPPORTED)
 
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))

diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy
index e6e3de5fc91c44011a3659987d7ab4f7e739b7eb..37ed848efbf93ddb886622840b8daa5b4a06ac01 100644 (file)
--- a/test/regress/regress0/sygus/max.sy
+++ b/test/regress/regress0/sygus/max.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (synth-fun max ((x Int) (y Int)) Int

diff --git a/test/regress/regress0/sygus/max2-univ.sy b/test/regress/regress0/sygus/max2-univ.sy
index 927148d81178390f03105a1945efacfd94d9032c..0e00cfd9b95faecf6a83d95bad4b1ada0ef42c50 100644 (file)
--- a/test/regress/regress0/sygus/max2-univ.sy
+++ b/test/regress/regress0/sygus/max2-univ.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 ; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes)
 (set-logic LIA)
 (synth-fun max2 ((x Int) (y Int)) Int)

diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
index c238de5ddf3b69030316c4ee5c64228e4f663686..22a2e0a4b8ddbcfbe6004cb46e6ccd5b5078afe0 100644 (file)
--- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy
+++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy
index d3624a731306bec07f82ec56cad9e544bc38b92e..a1776cf93e152f7a1ec7674227b29160c08fe569 100644 (file)
--- a/test/regress/regress0/sygus/nflat-fwd-3.sy
+++ b/test/regress/regress0/sygus/nflat-fwd-3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ (+ Con Con) Con) x))

diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy
index 3f15d59151ce272929b8b8f577a9ad74379b5382..da26a6c931347b1c3dd48c48390e504f5b30294e 100644 (file)
--- a/test/regress/regress0/sygus/nflat-fwd.sy
+++ b/test/regress/regress0/sygus/nflat-fwd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x))

diff --git a/test/regress/regress0/sygus/nia-max-square-ns.sy b/test/regress/regress0/sygus/nia-max-square-ns.sy
index 96baab7fe32df5dc1b269c5e120596fda8328acb..6e7f70ff0d60b88fa90f81c3ea602c9ddf20efdc 100644 (file)
--- a/test/regress/regress0/sygus/nia-max-square-ns.sy
+++ b/test/regress/regress0/sygus/nia-max-square-ns.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth --nl-ext-tplanes
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --nl-ext-tplanes
 (set-logic NIA)
 
 (synth-fun max ((x Int) (y Int)) Int)

diff --git a/test/regress/regress0/sygus/no-flat-simp.sy b/test/regress/regress0/sygus/no-flat-simp.sy
index af1284f133e9a03509b8b449927266e70e68d080..c0f0e4c0f8f0d048bff83f26a197cca6001dcf26 100644 (file)
--- a/test/regress/regress0/sygus/no-flat-simp.sy
+++ b/test/regress/regress0/sygus/no-flat-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/no-mention.sy b/test/regress/regress0/sygus/no-mention.sy
index 60efc1b74df87fa7cecd5639922f9033539ae87b..f964d6039e1b74637660303227ae9a271bff3d48 100644 (file)
--- a/test/regress/regress0/sygus/no-mention.sy
+++ b/test/regress/regress0/sygus/no-mention.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun p ((x Int) (y Int)) Int)

diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy
index ee27b30eb12ba18e854f9e7bff46881373831c8f..c6c9383bbf929e4e908ff0cf896e15c44990a5cd 100644 (file)
--- a/test/regress/regress0/sygus/no-syntax-test-bool.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
index bd8da19008726a76655f9ec03de1b2d06736dbf4..8f333811c1ea3f9708bd8126e0016bd1be3d4f30 100644 (file)
--- a/test/regress/regress0/sygus/no-syntax-test-no-si.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy
index 2b3d5f3e95f3465ffda5f514cb71c2108a9e68ae..f27a07ee7912d6d6cda9f6242e407131a5eca87f 100644 (file)
--- a/test/regress/regress0/sygus/no-syntax-test.sy
+++ b/test/regress/regress0/sygus/no-syntax-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy
index 3cc577bd8659e39d782afb3c9c404ef0447429cd..50c7d39a04171e8c97f95e905b0ca9b62bb15104 100644 (file)
--- a/test/regress/regress0/sygus/parity-AIG-d0.sy
+++ b/test/regress/regress0/sygus/parity-AIG-d0.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic BV)
 
 (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool

diff --git a/test/regress/regress0/sygus/parse-bv-let.sy b/test/regress/regress0/sygus/parse-bv-let.sy
index 88ddcf1397dd8e57897954e1e8f48d0359910f06..1329918fc6640493b97669f18f74056e134aa8eb 100644 (file)
--- a/test/regress/regress0/sygus/parse-bv-let.sy
+++ b/test/regress/regress0/sygus/parse-bv-let.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun bit-reset ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32)

diff --git a/test/regress/regress0/sygus/qe.sy b/test/regress/regress0/sygus/qe.sy
index eaff0fd9a0314767a1827baa9083548951f90d63..5661f4469ad916faa6697f44c8385bb64d7fe450 100644 (file)
--- a/test/regress/regress0/sygus/qe.sy
+++ b/test/regress/regress0/sygus/qe.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (synth-fun f ((x Int)) Int)

diff --git a/test/regress/regress0/sygus/strings-concat-3-args.sy b/test/regress/regress0/sygus/strings-concat-3-args.sy
index 3c93c51d32c93a5048c4b75ba0b97033c47adf27..6628ff74654ef92b77c2f12e40e5b01084286da9 100644 (file)
--- a/test/regress/regress0/sygus/strings-concat-3-args.sy
+++ b/test/regress/regress0/sygus/strings-concat-3-args.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((x String)) String
 ((Start String (ntString))

diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy
index 40346bcdfb1f33e4fdd7060cc39999235787c9c0..7d976ff39bdc1f6ffc22ace6a7bb2c6b433819b2 100644 (file)
--- a/test/regress/regress0/sygus/strings-small.sy
+++ b/test/regress/regress0/sygus/strings-small.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((firstname String) (lastname String)) String
 ((Start String (ntString))

diff --git a/test/regress/regress0/sygus/strings-template-infer.sy b/test/regress/regress0/sygus/strings-template-infer.sy
index 498e713e840a942be6c46a64136e656838ea1b95..13c4d7dac00edff8d14c1798f38183c4f4221c0b 100644 (file)
--- a/test/regress/regress0/sygus/strings-template-infer.sy
+++ b/test/regress/regress0/sygus/strings-template-infer.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
  
 (define-fun cA ((x String) (y String)) String (str.++ (str.++ x "A") y))

diff --git a/test/regress/regress0/sygus/strings-trivial-simp.sy b/test/regress/regress0/sygus/strings-trivial-simp.sy
index d37ac8bf46cb3790c5fd57fdb98bebe38e69c2f3..f5e41a8f5e7b74bdfb2392036e15d4d6a46ac8a6 100644 (file)
--- a/test/regress/regress0/sygus/strings-trivial-simp.sy
+++ b/test/regress/regress0/sygus/strings-trivial-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
  
 (synth-fun f ((name String)) String

diff --git a/test/regress/regress0/sygus/strings-trivial.sy b/test/regress/regress0/sygus/strings-trivial.sy
index f4847922d047d77e54692c0bac9792372220533a..9af0a1bb17801e3f76a95b4cc8510871b85f62ae 100644 (file)
--- a/test/regress/regress0/sygus/strings-trivial.sy
+++ b/test/regress/regress0/sygus/strings-trivial.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
  
 (synth-fun f ((name String)) String

diff --git a/test/regress/regress0/sygus/strings-unconstrained.sy b/test/regress/regress0/sygus/strings-unconstrained.sy
index 38e69e337220c6281c73d3e6a86cb2d6614227da..39c39248750921bbc827054354c48650a068b482 100644 (file)
--- a/test/regress/regress0/sygus/strings-unconstrained.sy
+++ b/test/regress/regress0/sygus/strings-unconstrained.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((firstname String) (lastname String)) String
 ((Start String (ntString))

diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy
index 59560ed61f838673f1f38de6b60da12713bc8faf..d496e3fdca7824d2b5edc2dc7cf1ba2bc556c051 100644 (file)
--- a/test/regress/regress0/sygus/sygus-dt.sy
+++ b/test/regress/regress0/sygus/sygus-dt.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/tl-type-0.sy b/test/regress/regress0/sygus/tl-type-0.sy
index ef046c8e00e9e4c167c4747ef2cd7c39faf5ad18..ceda89d78a816cab4ca47fc0246ce7856cef33e9 100644 (file)
--- a/test/regress/regress0/sygus/tl-type-0.sy
+++ b/test/regress/regress0/sygus/tl-type-0.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Term Term)))

diff --git a/test/regress/regress0/sygus/tl-type-4x.sy b/test/regress/regress0/sygus/tl-type-4x.sy
index a18d130527874ecef13af7fe864a554dafa7b901..bf8eee5ee514b00f3221da2dd3834029b17302f8 100644 (file)
--- a/test/regress/regress0/sygus/tl-type-4x.sy
+++ b/test/regress/regress0/sygus/tl-type-4x.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int (Term (+ Start Start)))

diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy
index a6980425a4372044fb00dd7fe72cad84f0f3afad..6f25a570ecca6f1e3668e8c8c7feaac2d4e6224d 100644 (file)
--- a/test/regress/regress0/sygus/tl-type.sy
+++ b/test/regress/regress0/sygus/tl-type.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int (Term (+ Start Start)))

diff --git a/test/regress/regress0/sygus/triv-type-mismatch-si.sy b/test/regress/regress0/sygus/triv-type-mismatch-si.sy
index e2935af51ff111b083e8eb1a6bed7360ecdc34db..37c5a7f53445cb84962cdc43381362cd802a1014 100644 (file)
--- a/test/regress/regress0/sygus/triv-type-mismatch-si.sy
+++ b/test/regress/regress0/sygus/triv-type-mismatch-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun R ((y Int)) Bool)

diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy
index b016872b4ab94e8e69a45a89beeb15e2f6d1c4f3..06d2ecb717a67b073e9adef42bb43cfb3d9d15fd 100644 (file)
--- a/test/regress/regress0/sygus/twolets1.sy
+++ b/test/regress/regress0/sygus/twolets1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 ;; f1 is x plus 2 ;; f2 is 2x plus 5

diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy
index 70d1ffa0248cf21342ff55e4df1c405ad9190705..50f7ad54499a0c28ebff7c1010a98c6a97679154 100644 (file)
--- a/test/regress/regress0/sygus/twolets2-orig.sy
+++ b/test/regress/regress0/sygus/twolets2-orig.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun f1 ((x Int)) Int
      (

diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy
index e98be942b3d4abfd47fd584afa321e97d4d5018e..94040bf4533e9d9fe9bb726a677ac71df4e586c2 100644 (file)
--- a/test/regress/regress0/sygus/uminus_one.sy
+++ b/test/regress/regress0/sygus/uminus_one.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int ((Start Int ((- 1)))))
 (declare-var x Int)

diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
index 300b6b65cd4af87ff5526ec1414ffeca8438af8f..d45cec38b604a283e16ce3b7732caec7d37edea0 100644 (file)
--- a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
+++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 (synth-fun inv ((x Int)) Bool

diff --git a/test/regress/regress1/sygus/MPwL_d1s3.sy b/test/regress/regress1/sygus/MPwL_d1s3.sy
index b5b848848ab67d585c02d528cfac3d9b28bbed2d..5178cf86be5d96f1e9914de400912d8210616831 100644 (file)
--- a/test/regress/regress1/sygus/MPwL_d1s3.sy
+++ b/test/regress/regress1/sygus/MPwL_d1s3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth 
+; COMMAND-LINE: --sygus-out=status 
 (set-logic LIA)
 
 (define-fun get-y ((currPoint Int)) Int 

diff --git a/test/regress/regress1/sygus/VC22_a.sy b/test/regress/regress1/sygus/VC22_a.sy
index 75bed6a28cf2e2983bdc52de38259da3230f34a5..32e4723aa060e80265768d762db3347a83b4b866 100644 (file)
--- a/test/regress/regress1/sygus/VC22_a.sy
+++ b/test/regress/regress1/sygus/VC22_a.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun f ((x1 Int) (x2 Int)) Int

diff --git a/test/regress/regress1/sygus/array_sum_dd.sy b/test/regress/regress1/sygus/array_sum_dd.sy
index dacd7347d085ac71529c9790fa12bf59e4f2b082..6d3354d2d458a25a1a4661864509a134de1d1719 100644 (file)
--- a/test/regress/regress1/sygus/array_sum_dd.sy
+++ b/test/regress/regress1/sygus/array_sum_dd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun findSum ( (y1 Int) (y2 Int) )Int (
 (Start Int ( 0 1 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) 

diff --git a/test/regress/regress1/sygus/hd-sdiv.sy b/test/regress/regress1/sygus/hd-sdiv.sy
index 019b48a1c1624ed1a848c4a01f3fb0fb48ec2c6b..37e1daf88508653eeaa224248c7657611b07cb82 100644 (file)
--- a/test/regress/regress1/sygus/hd-sdiv.sy
+++ b/test/regress/regress1/sygus/hd-sdiv.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic BV)
 
 (define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001))

diff --git a/test/regress/regress1/sygus/icfp_easy_mt_ite.sy b/test/regress/regress1/sygus/icfp_easy_mt_ite.sy
index b7428fd5147e9ecc777ac4412a3cf60cfb23f43a..799633fa3f48950f827251a844b76e95b2d70d1e 100644 (file)
--- a/test/regress/regress1/sygus/icfp_easy_mt_ite.sy
+++ b/test/regress/regress1/sygus/icfp_easy_mt_ite.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))

diff --git a/test/regress/regress1/sygus/inv_gen_fig8.sy b/test/regress/regress1/sygus/inv_gen_fig8.sy
index 5496f3c0a12e3d7bd8abb92aec49fa5306cf4c25..19c36e4dc4fe654c6aecb2380b8c2e7000f5c0a7 100644 (file)
--- a/test/regress/regress1/sygus/inv_gen_fig8.sy
+++ b/test/regress/regress1/sygus/inv_gen_fig8.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun inv ((l Int)) Bool
     (

diff --git a/test/regress/regress1/sygus/inv_gen_n_c11.sy b/test/regress/regress1/sygus/inv_gen_n_c11.sy
index 946f284cb6a44551a99bcff3f9061bde4d6af59d..9e04682a50ee7fd4bde946f99779930e091e3f94 100644 (file)
--- a/test/regress/regress1/sygus/inv_gen_n_c11.sy
+++ b/test/regress/regress1/sygus/inv_gen_n_c11.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun inv ((i Int) (l Int)) Bool
     (

diff --git a/test/regress/regress1/sygus/mpg_guard1-dd.sy b/test/regress/regress1/sygus/mpg_guard1-dd.sy
index e574f7eb6c0dba7cdc69fc940957fec009c7fb39..31800a36f406657c409056a034eb6f5d8b851572 100644 (file)
--- a/test/regress/regress1/sygus/mpg_guard1-dd.sy
+++ b/test/regress/regress1/sygus/mpg_guard1-dd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun eq1 ( (x Int) (y Int) ) Int

diff --git a/test/regress/regress1/sygus/nia-max-square.sy b/test/regress/regress1/sygus/nia-max-square.sy
index 5858af98a3bde239e62b1ca0a39501403e3ab713..e023e837b4c5dfc8d2f1316a6b37898a71cf7108 100644 (file)
--- a/test/regress/regress1/sygus/nia-max-square.sy
+++ b/test/regress/regress1/sygus/nia-max-square.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth --nl-ext-tplanes
+; COMMAND-LINE: --sygus-out=status --nl-ext-tplanes
 (set-logic NIA)
 
 (synth-fun max ((x Int) (y Int)) Int

diff --git a/test/regress/regress1/sygus/stopwatch-bt.sy b/test/regress/regress1/sygus/stopwatch-bt.sy
index 016280521e4bfed5d5ef2978d1cea5cbf9727870..291ae6099ff3fe767c0a433ba1af490b6e6bdc89 100644 (file)
--- a/test/regress/regress1/sygus/stopwatch-bt.sy
+++ b/test/regress/regress1/sygus/stopwatch-bt.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth
+; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status
 (set-logic LIA)
 
 (define-fun

diff --git a/test/regress/regress1/sygus/three.sy b/test/regress/regress1/sygus/three.sy
index 6e2ce3a2c413ca6ed6985abf2a62f4e8cd8653a5..831e5beb1e49983930881a7a2a6aee2c2141fdc6 100644 (file)
--- a/test/regress/regress1/sygus/three.sy
+++ b/test/regress/regress1/sygus/three.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth 
+; COMMAND-LINE: --sygus-out=status 
 
 (set-logic LIA)
 

diff --git a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
index f840fa51955a0969e541735179671fb67164b2f4..73d410d512d5e891f19280c673a67f6934bad544 100644 (file)
--- a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
+++ b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun inv ((i Int) (y Int) (l Int)) Bool
     (