From 5cafed748989602263b8ad1a27ac6b9bd159a441 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 3 Nov 2017 15:36:38 -0500 Subject: [PATCH] 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. --- src/main/driver_unified.cpp | 10 ---- src/options/Makefile.am | 1 + src/options/options.h | 2 - src/options/options_handler.cpp | 51 ++++++++++++++++++- src/options/options_handler.h | 6 ++- src/options/options_public_functions.cpp | 7 --- src/options/quantifiers_options | 2 +- src/options/smt_options | 2 + src/options/sygus_out_mode.h | 39 ++++++++++++++ src/smt/command.cpp | 37 ++++++++++++-- src/smt/command.h | 14 +++-- src/smt/smt_engine.cpp | 7 +++ test/regress/regress0/expect/scrub.07.sy | 2 +- test/regress/regress0/expect/scrub.08.sy | 2 +- test/regress/regress0/sygus/General_plus10.sy | 2 +- test/regress/regress0/sygus/array_search_2.sy | 2 +- test/regress/regress0/sygus/array_sum_2_5.sy | 2 +- test/regress/regress0/sygus/cegar1.sy | 2 +- test/regress/regress0/sygus/cggmp.sy | 2 +- .../regress/regress0/sygus/clock-inc-tuple.sy | 2 +- test/regress/regress0/sygus/commutative.sy | 2 +- test/regress/regress0/sygus/const-var-test.sy | 2 +- test/regress/regress0/sygus/constant.sy | 2 +- test/regress/regress0/sygus/dt-no-syntax.sy | 2 +- test/regress/regress0/sygus/dt-test-ns.sy | 2 +- test/regress/regress0/sygus/dup-op.sy | 2 +- test/regress/regress0/sygus/enum-test.sy | 2 +- test/regress/regress0/sygus/fg_polynomial3.sy | 2 +- test/regress/regress0/sygus/hd-01-d1-prog.sy | 2 +- test/regress/regress0/sygus/icfp_14.12.sy | 2 +- test/regress/regress0/sygus/icfp_28_10.sy | 2 +- test/regress/regress0/sygus/icfp_easy-ite.sy | 2 +- test/regress/regress0/sygus/inv-example.sy | 2 +- test/regress/regress0/sygus/let-ringer.sy | 2 +- test/regress/regress0/sygus/let-simp.sy | 2 +- test/regress/regress0/sygus/list-head-x.sy | 2 +- test/regress/regress0/sygus/max.sy | 2 +- test/regress/regress0/sygus/max2-univ.sy | 2 +- .../regress0/sygus/multi-fun-polynomial2.sy | 2 +- test/regress/regress0/sygus/nflat-fwd-3.sy | 2 +- test/regress/regress0/sygus/nflat-fwd.sy | 2 +- .../regress0/sygus/nia-max-square-ns.sy | 2 +- test/regress/regress0/sygus/no-flat-simp.sy | 2 +- test/regress/regress0/sygus/no-mention.sy | 2 +- .../regress0/sygus/no-syntax-test-bool.sy | 2 +- .../regress0/sygus/no-syntax-test-no-si.sy | 2 +- test/regress/regress0/sygus/no-syntax-test.sy | 2 +- test/regress/regress0/sygus/parity-AIG-d0.sy | 2 +- test/regress/regress0/sygus/parse-bv-let.sy | 2 +- test/regress/regress0/sygus/qe.sy | 2 +- .../regress0/sygus/strings-concat-3-args.sy | 2 +- test/regress/regress0/sygus/strings-small.sy | 2 +- .../regress0/sygus/strings-template-infer.sy | 2 +- .../regress0/sygus/strings-trivial-simp.sy | 2 +- .../regress/regress0/sygus/strings-trivial.sy | 2 +- .../regress0/sygus/strings-unconstrained.sy | 2 +- test/regress/regress0/sygus/sygus-dt.sy | 2 +- test/regress/regress0/sygus/tl-type-0.sy | 2 +- test/regress/regress0/sygus/tl-type-4x.sy | 2 +- test/regress/regress0/sygus/tl-type.sy | 2 +- .../regress0/sygus/triv-type-mismatch-si.sy | 2 +- test/regress/regress0/sygus/twolets1.sy | 2 +- test/regress/regress0/sygus/twolets2-orig.sy | 2 +- test/regress/regress0/sygus/uminus_one.sy | 2 +- .../regress0/sygus/unbdd_inv_gen_winf1.sy | 2 +- test/regress/regress1/sygus/MPwL_d1s3.sy | 2 +- test/regress/regress1/sygus/VC22_a.sy | 2 +- test/regress/regress1/sygus/array_sum_dd.sy | 2 +- test/regress/regress1/sygus/hd-sdiv.sy | 2 +- .../regress1/sygus/icfp_easy_mt_ite.sy | 2 +- test/regress/regress1/sygus/inv_gen_fig8.sy | 2 +- test/regress/regress1/sygus/inv_gen_n_c11.sy | 2 +- test/regress/regress1/sygus/mpg_guard1-dd.sy | 2 +- test/regress/regress1/sygus/nia-max-square.sy | 2 +- test/regress/regress1/sygus/stopwatch-bt.sy | 2 +- test/regress/regress1/sygus/three.sy | 2 +- .../regress1/sygus/unbdd_inv_gen_ex7.sy | 2 +- 77 files changed, 211 insertions(+), 97 deletions(-) create mode 100644 src/options/sygus_out_mode.h diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 8ffb47e40..ebfc7266b 100644 --- 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 ff889bcb2..54027c128 100644 --- 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 f93663095..474ef0f96 100644 --- 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 351c8b608..3d74091fd 100644 --- 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 c525c9e0e..9d5f8cc6e 100644 --- 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 7d71c267a..b8db9d9da 100644 --- 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 ba7c8338a..c92813bf4 100644 --- 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 00424e103..c701d5c20 100644 --- 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 index 000000000..9f94be27f --- /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 + +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 8012c868c..fee109923 100644 --- 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 f5be9ddfe..a60c85a3c 100644 --- 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 f93d8bd7f..2ff115606 100644 --- 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 cf0e37c9f..79b917c7a 100644 --- 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 7f78dbc48..360474f84 100644 --- 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 ee26fac79..1792749e2 100755 --- 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 e6683ced9..41346e655 100644 --- 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 387ce9487..84a75d086 100644 --- 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 dd7f73e27..ee85db88a 100644 --- 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 1ae1f53c0..a3247e4f4 100644 --- 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 2409b82d2..43fd7c1ac 100644 --- 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 f675bddad..24201b453 100644 --- 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 b79b7eeec..305f5783a 100644 --- 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 5c48f5e39..1bb3e59fa 100644 --- 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 0a9fb9112..f4de9b055 100644 --- 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 0c28769b2..a6e8ac5c2 100644 --- 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 bed9972fd..e2c69282e 100644 --- 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 7b59f5f1a..47099eeed 100644 --- 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 dab92bb88..d70516bf1 100644 --- 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 2e6c6ef81..1379d4206 100644 --- 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 d9c19f8c1..51b86f0f5 100644 --- 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 74e054159..212ae37f5 100644 --- 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 248264698..f0cbbdc53 100644 --- 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 b56425964..ff68bc06c 100644 --- 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 d5d40ace4..d26edffd2 100644 --- 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 d07f6a717..6f9d9fff9 100644 --- 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 8d209a9a0..6c5c1a97b 100644 --- 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 e6e3de5fc..37ed848ef 100644 --- 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 927148d81..0e00cfd9b 100644 --- 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 c238de5dd..22a2e0a4b 100644 --- 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 d3624a731..a1776cf93 100644 --- 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 3f15d5915..da26a6c93 100644 --- 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 96baab7fe..6e7f70ff0 100644 --- 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 af1284f13..c0f0e4c0f 100644 --- 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 60efc1b74..f964d6039 100644 --- 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 ee27b30eb..c6c9383bb 100644 --- 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 bd8da1900..8f333811c 100644 --- 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 2b3d5f3e9..f27a07ee7 100644 --- 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 3cc577bd8..50c7d39a0 100644 --- 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 88ddcf139..1329918fc 100644 --- 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 eaff0fd9a..5661f4469 100644 --- 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 3c93c51d3..6628ff746 100644 --- 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 40346bcdf..7d976ff39 100644 --- 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 498e713e8..13c4d7dac 100644 --- 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 d37ac8bf4..f5e41a8f5 100644 --- 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 f4847922d..9af0a1bb1 100644 --- 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 38e69e337..39c392487 100644 --- 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 59560ed61..d496e3fdc 100644 --- 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 ef046c8e0..ceda89d78 100644 --- 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 a18d13052..bf8eee5ee 100644 --- 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 a6980425a..6f25a570e 100644 --- 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 e2935af51..37c5a7f53 100644 --- 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 b016872b4..06d2ecb71 100644 --- 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 70d1ffa02..50f7ad544 100644 --- 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 e98be942b..94040bf45 100644 --- 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 300b6b65c..d45cec38b 100644 --- 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 b5b848848..5178cf86b 100644 --- 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 75bed6a28..32e4723aa 100644 --- 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 dacd7347d..6d3354d2d 100644 --- 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 019b48a1c..37e1daf88 100644 --- 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 b7428fd51..799633fa3 100644 --- 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 5496f3c0a..19c36e4dc 100644 --- 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 946f284cb..9e04682a5 100644 --- 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 e574f7eb6..31800a36f 100644 --- 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 5858af98a..e023e837b 100644 --- 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 016280521..291ae6099 100644 --- 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 6e2ce3a2c..831e5beb1 100644 --- 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 f840fa519..73d410d51 100644 --- 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 ( -- 2.30.2