diff options
80 files changed, 229 insertions, 222 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index f6592a931..d96e94d43 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -109,8 +109,8 @@ api::Term Parser::getExpressionForNameAndType(const std::string& name, if(expr.isNull()) { // the variable is overloaded, try with type if the type exists if(!t.isNull()) { - // if we decide later to support annotations for function types, this will update to - // separate t into ( argument types, return type ) + // if we decide later to support annotations for function types, this will + // update to separate t into ( argument types, return type ) expr = getOverloadedConstantForType(name, t); if(expr.isNull()) { parseError("Cannot get overloaded constant for type ascription."); diff --git a/src/parser/parser.h b/src/parser/parser.h index 8add1c698..4b04c77b7 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -303,9 +303,10 @@ public: virtual api::Term getExpressionForName(const std::string& name); /** - * Returns the expression that name should be interpreted as, based on the current binding. + * Returns the expression that name should be interpreted as, based on the + * current binding. * - * This is the same as above but where the name has been type cast to t. + * This is the same as above but where the name has been type cast to t. */ virtual api::Term getExpressionForNameAndType(const std::string& name, api::Sort t); @@ -331,9 +332,9 @@ public: * This is a generalization of ExprManager::operatorToKind that also * handles variables whose types are "function-like", i.e. where * checkFunctionLike(fun) returns true. - * + * * For examples of the latter, this function returns - * APPLY_UF if fun has function type, + * APPLY_UF if fun has function type, * APPLY_CONSTRUCTOR if fun has constructor type. */ api::Kind getKindForFunction(api::Term fun); @@ -379,7 +380,7 @@ public: /** * Checks whether the given expression is function-like, i.e. - * it expects arguments. This is checked by looking at the type + * it expects arguments. This is checked by looking at the type * of fun. Examples of function types are function, constructor, * selector, tester. * @param fun the expression to check @@ -443,11 +444,12 @@ public: std::vector<api::Term> bindBoundVars(const std::vector<std::string> names, const api::Sort& type); - /** Create a new variable definition (e.g., from a let binding). + /** Create a new variable definition (e.g., from a let binding). * levelZero is set if the binding must be done at level 0. * If a symbol with name already exists, * then if doOverload is true, we create overloaded operators. - * else if doOverload is false, the existing expression is shadowed by the new expression. + * else if doOverload is false, the existing expression is shadowed by the + * new expression. */ void defineVar(const std::string& name, const api::Term& val, @@ -648,9 +650,10 @@ public: /** Is the symbol bound to a boolean variable? */ bool isBoolean(const std::string& name); - /** Is fun a function (or function-like thing)? - * Currently this means its type is either a function, constructor, tester, or selector. - */ + /** Is fun a function (or function-like thing)? + * Currently this means its type is either a function, constructor, tester, or + * selector. + */ bool isFunctionLike(api::Term fun); /** Is the symbol bound to a predicate? */ diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index e4f46326f..1f25e00dd 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -143,7 +143,8 @@ ParserBuilder& ParserBuilder::withIncludeFile(bool flag) { return *this; } -ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic) { +ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic) +{ d_logicIsForced = true; d_forcedLogic = logic; return *this; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 5961de587..56aebdcf7 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -315,10 +315,7 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const return d_logic.isTheoryEnabled(theory); } -bool Smt2::isHoEnabled() const -{ - return getLogic().isHigherOrder() && options::getUfHo(d_solver->getOptions()); -} +bool Smt2::isHoEnabled() const { return d_logic.isHigherOrder(); } bool Smt2::logicIsSet() { return d_logicSet; @@ -505,8 +502,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) d_logicSet = true; d_logic = name; - // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and - // higher-order + // if sygus is enabled, we must enable UF, datatypes, and integer arithmetic if(sygus()) { if (!d_logic.isQuantified()) { @@ -772,7 +768,7 @@ void Smt2::checkLogicAllowsFunctions() parseError( "Functions (of non-zero arity) cannot " "be declared in logic " - + d_logic.getLogicString() + " unless option --uf-ho is used"); + + d_logic.getLogicString() + ". Try adding the prefix HO_."); } } @@ -1012,8 +1008,6 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) } } } - // Second phase: apply the arguments to the parse op - const Options& opts = d_solver->getOptions(); // handle special cases if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull()) { @@ -1102,17 +1096,17 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) } else if (isBuiltinOperator) { - if (!options::getUfHo(opts) - && (kind == api::EQUAL || kind == api::DISTINCT)) + if (!isHoEnabled() && (kind == api::EQUAL || kind == api::DISTINCT)) { - // need --uf-ho if these operators are applied over function args + // need hol if these operators are applied over function args for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); ++i) { if ((*i).getSort().isFunction()) { parseError( - "Cannot apply equalty to functions unless --uf-ho is set."); + "Cannot apply equalty to functions unless logic is prefixed by " + "HO_."); } } } @@ -1155,9 +1149,11 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) unsigned arity = argt.getFunctionArity(); if (args.size() - 1 < arity) { - if (!options::getUfHo(opts)) + if (!isHoEnabled()) { - parseError("Cannot partially apply functions unless --uf-ho is set."); + parseError( + "Cannot partially apply functions unless logic is prefixed by " + "HO_."); } Debug("parser") << "Partial application of " << args[0]; Debug("parser") << " : #argTypes = " << arity; diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 5f078cab7..c96fbf07d 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -194,7 +194,11 @@ parseCommand returns [cvc5::Command* cmd = NULL] cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); } ) RPAREN_TOK DOT_TOK - | THF_TOK LPAREN_TOK nameN[name] COMMA_TOK + | THF_TOK + { + PARSER_STATE->setHol(); + } + LPAREN_TOK nameN[name] COMMA_TOK // Supported THF formulas: either a logic formula or a typing atom (i.e. we // ignore subtyping and logic sequents). Also, only TH0 ( TYPE_TOK COMMA_TOK thfAtomTyping[cmd] diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 764e83361..91fcc7a12 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -25,6 +25,7 @@ #include "options/options_public.h" #include "parser/parser.h" #include "smt/command.h" +#include "theory/logic_info.h" // ANTLR defines these, which is really bad! #undef true @@ -37,7 +38,10 @@ Tptp::Tptp(api::Solver* solver, SymbolManager* sm, bool strictMode, bool parseOnly) - : Parser(solver, sm, strictMode, parseOnly), d_cnf(false), d_fof(false) + : Parser(solver, sm, strictMode, parseOnly), + d_cnf(false), + d_fof(false), + d_hol(false) { addTheory(Tptp::THEORY_CORE); @@ -312,21 +316,18 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) isBuiltinKind = true; } Assert(kind != api::NULL_EXPR); - const Options& opts = d_solver->getOptions(); // Second phase: apply parse op to the arguments if (isBuiltinKind) { - if (!options::getUfHo(opts) - && (kind == api::EQUAL || kind == api::DISTINCT)) + if (!hol() && (kind == api::EQUAL || kind == api::DISTINCT)) { - // need --uf-ho if these operators are applied over function args + // need hol if these operators are applied over function args for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); ++i) { if ((*i).getSort().isFunction()) { - parseError( - "Cannot apply equalty to functions unless --uf-ho is set."); + parseError("Cannot apply equalty to functions unless THF."); } } } @@ -364,9 +365,9 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) unsigned arity = argt.getFunctionArity(); if (args.size() - 1 < arity) { - if (!options::getUfHo(opts)) + if (!hol()) { - parseError("Cannot partially apply functions unless --uf-ho is set."); + parseError("Cannot partially apply functions unless THF."); } Debug("parser") << "Partial application of " << args[0]; Debug("parser") << " : #argTypes = " << arity; @@ -438,6 +439,17 @@ api::Term Tptp::mkDecimal( return d_solver->mkReal(ss.str()); } +bool Tptp::hol() const { return d_hol; } +void Tptp::setHol() +{ + if (d_hol) + { + return; + } + d_hol = true; + d_solver->setLogic("HO_UF"); +} + void Tptp::forceLogic(const std::string& logic) { Parser::forceLogic(logic); diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 964c0bdfb..258394486 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -47,6 +47,9 @@ class Tptp : public Parser { bool fof() const { return d_fof; } void setFof(bool fof) { d_fof = fof; } + bool hol() const; + void setHol(); + void forceLogic(const std::string& logic) override; void addFreeVar(api::Term var); @@ -209,6 +212,7 @@ class Tptp : public Parser { bool d_cnf; // in a cnf formula bool d_fof; // in an fof formula + bool d_hol; // in a thf formula };/* class Tptp */ diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 67c5c5647..cd05b84c4 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -271,11 +271,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // Set default options associated with strings-exp. We also set these options // if we are using eager string preprocessing, which may introduce quantified // formulas at preprocess time. + // + // We don't want to set this option when we are in logics that contain ALL. if (!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS)) { // If the user explicitly set a logic that includes strings, but is not // the generic "ALL" logic, then enable stringsExp. opts.strings.stringExp = true; + Trace("smt") << "Turning stringExp on since logic does not have everything " + "and string theory is enabled\n"; } if (options::stringExp() || !options::stringLazyPreproc()) { @@ -753,7 +757,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // If in arrays, set the UF handler to arrays - if (logic.isTheoryEnabled(THEORY_ARRAYS) && !options::ufHo() + if (logic.isTheoryEnabled(THEORY_ARRAYS) && !logic.isHigherOrder() && !options::finiteModelFind() && (!logic.isQuantified() || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF)))) @@ -890,7 +894,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) options::DecisionMode decMode = // anything that uses sygus uses internal usesSygus ? options::DecisionMode::INTERNAL : - // ALL + // ALL or its supersets logic.hasEverything() ? options::DecisionMode::JUSTIFICATION : ( // QF_BV @@ -922,7 +926,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) : options::DecisionMode::INTERNAL); bool stoponly = - // ALL + // ALL or its supersets logic.hasEverything() || logic.isTheoryEnabled(THEORY_STRINGS) ? false : ( // QF_AUFLIA @@ -986,8 +990,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE; } } - if (options::ufHo()) + if (logic.isHigherOrder()) { + opts.uf.ufHo = true; // if higher-order, then current variants of model-based instantiation // cannot be used if (options::mbqiMode() != options::MbqiMode::NONE) diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index ecebd27c9..05f8c7a9f 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -39,7 +39,7 @@ LogicInfo::LogicInfo() d_linear(false), d_differenceLogic(false), d_cardinalityConstraints(false), - d_higherOrder(true), + d_higherOrder(false), d_locked(false) { for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) @@ -117,13 +117,25 @@ bool LogicInfo::isHigherOrder() const return d_higherOrder; } -/** Is this the all-inclusive logic? */ -bool LogicInfo::hasEverything() const { - PrettyCheckArgument(d_locked, *this, +bool LogicInfo::hasEverything() const +{ + PrettyCheckArgument(d_locked, + *this, "This LogicInfo isn't locked yet, and cannot be queried"); - LogicInfo everything; - everything.lock(); - return *this == everything; + // A logic has everything if all theories are enabled as well as quantifiers + bool doesNotHaveEverything = !isQuantified(); + for (TheoryId id = THEORY_FIRST; !doesNotHaveEverything && id < THEORY_LAST; + ++id) + { + // if not configured with symfpu, we allow THEORY_FP to be disabled and + // still *this to contain the ALL logic + if (!this->d_theories[id] + && (id != THEORY_FP || Configuration::isBuiltWithSymFPU())) + { + doesNotHaveEverything = true; + } + } + return !doesNotHaveEverything; } /** Is this the all-exclusive logic? (Here, that means propositional logic) */ @@ -275,17 +287,22 @@ std::string LogicInfo::getLogicString() const { LogicInfo qf_all_supported; qf_all_supported.disableQuantifiers(); qf_all_supported.lock(); - if(hasEverything()) { - d_logicString = "ALL"; - } else if(*this == qf_all_supported) { - d_logicString = "QF_ALL"; - } else { + stringstream ss; + if (isHigherOrder()) + { + ss << "HO_"; + } + if (!isQuantified()) + { + ss << "QF_"; + } + if (*this == qf_all_supported || hasEverything()) + { + ss << "ALL"; + } + else + { size_t seen = 0; // make sure we support all the active theories - - stringstream ss; - if(!isQuantified()) { - ss << "QF_"; - } if (d_theories[THEORY_SEP]) { ss << "SEP_"; @@ -309,7 +326,7 @@ std::string LogicInfo::getLogicString() const { if(d_theories[THEORY_FP]) { ss << "FP"; ++seen; - } + } if(d_theories[THEORY_DATATYPES]) { ss << "DT"; ++seen; @@ -350,9 +367,8 @@ std::string LogicInfo::getLogicString() const { if(seen == 0) { ss << "SAT"; } - - d_logicString = ss.str(); } + d_logicString = ss.str(); } return d_logicString; } @@ -374,6 +390,11 @@ void LogicInfo::setLogicString(std::string logicString) enableTheory(THEORY_BOOL); const char* p = logicString.c_str(); + if (!strncmp(p, "HO_", 3)) + { + enableHigherOrder(); + p += 3; + } if(*p == '\0') { // propositional logic only; we're done. } else if(!strcmp(p, "QF_SAT")) { @@ -384,14 +405,14 @@ void LogicInfo::setLogicString(std::string logicString) enableQuantifiers(); p += 3; } else if(!strcmp(p, "QF_ALL")) { - // the "all theories included" logic, no quantifiers - enableEverything(); + // the "all theories included" logic, no quantifiers. + enableEverything(d_higherOrder); disableQuantifiers(); arithNonLinear(); p += 6; } else if(!strcmp(p, "ALL")) { - // the "all theories included" logic, with quantifiers - enableEverything(); + // the "all theories included" logic, with quantifiers. + enableEverything(d_higherOrder); enableQuantifiers(); arithNonLinear(); p += 3; @@ -399,7 +420,7 @@ void LogicInfo::setLogicString(std::string logicString) else if (!strcmp(p, "HORN")) { // the HORN logic - enableEverything(); + enableEverything(d_higherOrder); enableQuantifiers(); arithNonLinear(); p += 4; @@ -541,9 +562,11 @@ void LogicInfo::setLogicString(std::string logicString) d_logicString = logicString; } -void LogicInfo::enableEverything() { +void LogicInfo::enableEverything(bool enableHigherOrder) +{ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(); + this->d_higherOrder = enableHigherOrder; } void LogicInfo::disableEverything() { @@ -584,7 +607,6 @@ void LogicInfo::enableSygus() enableTheory(THEORY_UF); enableTheory(THEORY_DATATYPES); enableIntegers(); - enableHigherOrder(); } void LogicInfo::enableSeparationLogic() diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 107093a5c..c6aa71ad0 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -120,7 +120,11 @@ public: /** Is this a quantified logic? */ bool isQuantified() const; - /** Is this the all-inclusive logic? */ + /** Is this a logic that includes the all-inclusive logic? + * + * @return Yields true if the logic corresponds to "ALL" or its super + * set including , such as "HO_ALL". + */ bool hasEverything() const; /** Is this the all-exclusive logic? (Here, that means propositional logic) */ @@ -168,8 +172,11 @@ public: /** * Enable all functionality. All theories, plus quantifiers, will be * enabled. + * + * @param enableHigherOrder Whether HOL should be enable together with the + * above. */ - void enableEverything(); + void enableEverything(bool enableHigherOrder = false); /** * Disable all functionality. The result will be a LogicInfo with diff --git a/test/regress/regress0/declare-fun-is-match.smt2 b/test/regress/regress0/declare-fun-is-match.smt2 index f3877edca..0b69011c8 100644 --- a/test/regress/regress0/declare-fun-is-match.smt2 +++ b/test/regress/regress0/declare-fun-is-match.smt2 @@ -1,7 +1,6 @@ ; EXPECT: sat -; COMMAND-LINE: --uf-ho (set-info :smt-lib-version 2.6) -(set-logic UFIDL) +(set-logic HO_UFIDL) (set-info :status sat) (declare-fun match (Int Int) Int) (declare-fun is (Int Int) Int) diff --git a/test/regress/regress0/fp/issue4277-assign-func.smt2 b/test/regress/regress0/fp/issue4277-assign-func.smt2 index 6a516a3ca..c42bad235 100644 --- a/test/regress/regress0/fp/issue4277-assign-func.smt2 +++ b/test/regress/regress0/fp/issue4277-assign-func.smt2 @@ -1,8 +1,7 @@ ; COMMAND-LINE: -q ; EXPECT: sat ; REQUIRES: symfpu -(set-logic ALL) -(set-option :uf-ho true) +(set-logic HO_ALL) (set-option :assign-function-values false) (set-info :status sat) (declare-fun b () (_ BitVec 1)) diff --git a/test/regress/regress0/ho/apply-collapse-sat.smt2 b/test/regress/regress0/ho/apply-collapse-sat.smt2 index 74a9df660..64aaa797d 100644 --- a/test/regress/regress0/ho/apply-collapse-sat.smt2 +++ b/test/regress/regress0/ho/apply-collapse-sat.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic UF) +(set-logic HO_UF) (set-info :status sat) (declare-sort U 0) (declare-fun f (U U) U) diff --git a/test/regress/regress0/ho/apply-collapse-unsat.smt2 b/test/regress/regress0/ho/apply-collapse-unsat.smt2 index 101de9081..45eeb23a7 100644 --- a/test/regress/regress0/ho/apply-collapse-unsat.smt2 +++ b/test/regress/regress0/ho/apply-collapse-unsat.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UF) +(set-logic HO_UF) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U U) U) diff --git a/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p index 0ed7fe44b..c4b517e56 100644 --- a/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p +++ b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p @@ -1,4 +1,3 @@ -% COMMAND-LINE: --uf-ho % EXPECT: % SZS status Unsatisfiable for bug_nodbuilding_interpreted_SYO042^1 %------------------------------------------------------------------------------ diff --git a/test/regress/regress0/ho/cong-full-apply.smt2 b/test/regress/regress0/ho/cong-full-apply.smt2 index 0ff147b97..493bbf140 100644 --- a/test/regress/regress0/ho/cong-full-apply.smt2 +++ b/test/regress/regress0/ho/cong-full-apply.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UFLIA) +(set-logic HO_UFLIA) (set-info :status unsat) (declare-fun f (Int) Int) (declare-fun g (Int) Int) diff --git a/test/regress/regress0/ho/cong.smt2 b/test/regress/regress0/ho/cong.smt2 index 531356568..b1feafe3e 100644 --- a/test/regress/regress0/ho/cong.smt2 +++ b/test/regress/regress0/ho/cong.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UF) +(set-logic HO_UF) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U) U) diff --git a/test/regress/regress0/ho/declare-fun-variants.smt2 b/test/regress/regress0/ho/declare-fun-variants.smt2 index 990423fb3..de37f7044 100644 --- a/test/regress/regress0/ho/declare-fun-variants.smt2 +++ b/test/regress/regress0/ho/declare-fun-variants.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status sat) (declare-fun f (Int Int) Int) (declare-fun g (Int) (-> Int Int)) diff --git a/test/regress/regress0/ho/def-fun-flatten.smt2 b/test/regress/regress0/ho/def-fun-flatten.smt2 index af33098f5..81af169a7 100644 --- a/test/regress/regress0/ho/def-fun-flatten.smt2 +++ b/test/regress/regress0/ho/def-fun-flatten.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-fun f (Int Int) Int) (define-fun g ((x Int)) (-> Int Int) (f x)) diff --git a/test/regress/regress0/ho/ext-finite-unsat.smt2 b/test/regress/regress0/ho/ext-finite-unsat.smt2 index 1719d5ad1..282cc3bda 100644 --- a/test/regress/regress0/ho/ext-finite-unsat.smt2 +++ b/test/regress/regress0/ho/ext-finite-unsat.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UF) +(set-logic HO_UF) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U) U) diff --git a/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2 b/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2 index 7031829d4..175ced858 100644 --- a/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2 +++ b/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status sat) (declare-sort U 0) (declare-fun f ((-> U U)) U) diff --git a/test/regress/regress0/ho/ext-ho.smt2 b/test/regress/regress0/ho/ext-ho.smt2 index 02e51654e..613533ebd 100644 --- a/test/regress/regress0/ho/ext-ho.smt2 +++ b/test/regress/regress0/ho/ext-ho.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status sat) (declare-sort U 0) (declare-fun f ((-> U U)) U) diff --git a/test/regress/regress0/ho/ext-sat-partial-eval.smt2 b/test/regress/regress0/ho/ext-sat-partial-eval.smt2 index f3392f1ba..cc63c52ea 100644 --- a/test/regress/regress0/ho/ext-sat-partial-eval.smt2 +++ b/test/regress/regress0/ho/ext-sat-partial-eval.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic UF) +(set-logic HO_UF) (set-info :status sat) (declare-sort U 0) (declare-fun f (U U) U) diff --git a/test/regress/regress0/ho/ext-sat.smt2 b/test/regress/regress0/ho/ext-sat.smt2 index 772b6eaa0..f91fb8240 100644 --- a/test/regress/regress0/ho/ext-sat.smt2 +++ b/test/regress/regress0/ho/ext-sat.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic UF) +(set-logic HO_UF) (set-info :status sat) (declare-sort U 0) (declare-fun f (U U) U) diff --git a/test/regress/regress0/ho/finite-fun-ext.smt2 b/test/regress/regress0/ho/finite-fun-ext.smt2 index 005a2109a..63e25cb03 100644 --- a/test/regress/regress0/ho/finite-fun-ext.smt2 +++ b/test/regress/regress0/ho/finite-fun-ext.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-datatype Unit ((unit))) diff --git a/test/regress/regress0/ho/fta0144-alpha-eq.smt2 b/test/regress/regress0/ho/fta0144-alpha-eq.smt2 index 0fc536bd9..747bfd48e 100644 --- a/test/regress/regress0/ho/fta0144-alpha-eq.smt2 +++ b/test/regress/regress0/ho/fta0144-alpha-eq.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort Nat$ 0) (declare-sort Complex$ 0) (declare-sort Real_set$ 0) diff --git a/test/regress/regress0/ho/fta0210.smt2 b/test/regress/regress0/ho/fta0210.smt2 index 9f0a39f25..864bb9859 100644 --- a/test/regress/regress0/ho/fta0210.smt2 +++ b/test/regress/regress0/ho/fta0210.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort A$ 0) (declare-sort Nat$ 0) (declare-sort A_poly$ 0) diff --git a/test/regress/regress0/ho/fun-subtyping.smt2 b/test/regress/regress0/ho/fun-subtyping.smt2 index 8eae3d073..e7cc01772 100644 --- a/test/regress/regress0/ho/fun-subtyping.smt2 +++ b/test/regress/regress0/ho/fun-subtyping.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (declare-fun g (Int) Real) (declare-fun h (Int) Real) (assert (not (= g h))) diff --git a/test/regress/regress0/ho/ho-exponential-model.smt2 b/test/regress/regress0/ho/ho-exponential-model.smt2 index 3f0011828..964a45f77 100644 --- a/test/regress/regress0/ho/ho-exponential-model.smt2 +++ b/test/regress/regress0/ho/ho-exponential-model.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic UFLIA) +(set-logic HO_UFLIA) (set-info :status sat) (declare-fun f1 (Int Int Int Int) Int) (declare-fun f2 (Int Int Int) Int) diff --git a/test/regress/regress0/ho/ho-match-fun-suffix.smt2 b/test/regress/regress0/ho/ho-match-fun-suffix.smt2 index 1e4ad243c..4418b156f 100644 --- a/test/regress/regress0/ho/ho-match-fun-suffix.smt2 +++ b/test/regress/regress0/ho/ho-match-fun-suffix.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-fun f (Int Int) Int) (declare-fun a () Int) diff --git a/test/regress/regress0/ho/ho-matching-enum-2.smt2 b/test/regress/regress0/ho/ho-matching-enum-2.smt2 index 9581e4c4f..e73afdce2 100644 --- a/test/regress/regress0/ho/ho-matching-enum-2.smt2 +++ b/test/regress/regress0/ho/ho-matching-enum-2.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/regress0/ho/ho-matching-enum.smt2 b/test/regress/regress0/ho/ho-matching-enum.smt2 index bd1d2837f..df3a920ec 100644 --- a/test/regress/regress0/ho/ho-matching-enum.smt2 +++ b/test/regress/regress0/ho/ho-matching-enum.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/regress0/ho/ho-matching-nested-app.smt2 b/test/regress/regress0/ho/ho-matching-nested-app.smt2 index d6de559e6..506cd55cf 100644 --- a/test/regress/regress0/ho/ho-matching-nested-app.smt2 +++ b/test/regress/regress0/ho/ho-matching-nested-app.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/regress0/ho/ho-std-fmf.smt2 b/test/regress/regress0/ho/ho-std-fmf.smt2 index 61d82d00c..1b23fdb6f 100644 --- a/test/regress/regress0/ho/ho-std-fmf.smt2 +++ b/test/regress/regress0/ho/ho-std-fmf.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --uf-ho --finite-model-find +; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic UF) +(set-logic HO_UF) (set-info :status sat) (declare-sort U 0) (declare-fun P (U U) Bool) diff --git a/test/regress/regress0/ho/hoa0008.smt2 b/test/regress/regress0/ho/hoa0008.smt2 index f4833aadf..b43920c21 100644 --- a/test/regress/regress0/ho/hoa0008.smt2 +++ b/test/regress/regress0/ho/hoa0008.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort A$ 0) (declare-sort Com$ 0) (declare-sort Loc$ 0) diff --git a/test/regress/regress0/ho/issue4990-care-graph.smt2 b/test/regress/regress0/ho/issue4990-care-graph.smt2 index 6c44a94a8..93c87d3c9 100644 --- a/test/regress/regress0/ho/issue4990-care-graph.smt2 +++ b/test/regress/regress0/ho/issue4990-care-graph.smt2 @@ -1,7 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic QF_AUFBVLIA) -(set-option :uf-ho true) +(set-logic HO_QF_AUFBVLIA) (declare-fun a () Int) (declare-fun b () Int) (declare-fun c (Int) Int) diff --git a/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 index e97b914a2..9091cf8bd 100644 --- a/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 +++ b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 @@ -1,7 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic QF_AUFBVLIA) -(set-option :uf-ho true) +(set-logic HO_QF_AUFBVLIA) (declare-fun a (Int) Int) (declare-fun b (Int) Int) (assert (distinct a b)) diff --git a/test/regress/regress0/ho/ite-apply-eq.smt2 b/test/regress/regress0/ho/ite-apply-eq.smt2 index 474f6887e..2e21d3081 100644 --- a/test/regress/regress0/ho/ite-apply-eq.smt2 +++ b/test/regress/regress0/ho/ite-apply-eq.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic UFLIA) +(set-logic HO_UFLIA) (set-info :status sat) (declare-fun x () Int) (declare-fun f (Int) Int) diff --git a/test/regress/regress0/ho/lambda-equality-non-canon.smt2 b/test/regress/regress0/ho/lambda-equality-non-canon.smt2 index 80f3db417..61753d90a 100644 --- a/test/regress/regress0/ho/lambda-equality-non-canon.smt2 +++ b/test/regress/regress0/ho/lambda-equality-non-canon.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status sat) (declare-fun f (Int) Int) diff --git a/test/regress/regress0/ho/match-middle.smt2 b/test/regress/regress0/ho/match-middle.smt2 index 0485f9a6f..225faa1a5 100644 --- a/test/regress/regress0/ho/match-middle.smt2 +++ b/test/regress/regress0/ho/match-middle.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UFLIA) +(set-logic HO_UFLIA) (set-info :status unsat) (declare-fun f (Int Int Int) Int) (declare-fun h (Int Int Int) Int) diff --git a/test/regress/regress0/ho/modulo-func-equality.smt2 b/test/regress/regress0/ho/modulo-func-equality.smt2 index 8e300ac72..984835be7 100644 --- a/test/regress/regress0/ho/modulo-func-equality.smt2 +++ b/test/regress/regress0/ho/modulo-func-equality.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UFLIA) +(set-logic HO_UFLIA) (set-info :status unsat) (declare-fun P (Int) Bool) (declare-fun Q (Int) Bool) diff --git a/test/regress/regress0/ho/shadowing-defs.smt2 b/test/regress/regress0/ho/shadowing-defs.smt2 index 722e970b6..fb5ac3ec6 100644 --- a/test/regress/regress0/ho/shadowing-defs.smt2 +++ b/test/regress/regress0/ho/shadowing-defs.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unknown -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-sort mu 0) diff --git a/test/regress/regress0/ho/simple-matching-partial.smt2 b/test/regress/regress0/ho/simple-matching-partial.smt2 index 41b2a0bca..18c578367 100644 --- a/test/regress/regress0/ho/simple-matching-partial.smt2 +++ b/test/regress/regress0/ho/simple-matching-partial.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U U) U) diff --git a/test/regress/regress0/ho/simple-matching.smt2 b/test/regress/regress0/ho/simple-matching.smt2 index 8e2315b2f..cbd70f072 100644 --- a/test/regress/regress0/ho/simple-matching.smt2 +++ b/test/regress/regress0/ho/simple-matching.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U) U) diff --git a/test/regress/regress0/ho/trans.smt2 b/test/regress/regress0/ho/trans.smt2 index 088abbab1..b33644db3 100644 --- a/test/regress/regress0/ho/trans.smt2 +++ b/test/regress/regress0/ho/trans.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UF) +(set-logic HO_UF) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U) U) diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy index 848ae0349..6a149cc71 100644 --- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy +++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy @@ -1,16 +1,16 @@ ; REQUIRES: no-competition ; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 ; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type -; EXPECT-ERROR: +; EXPECT-ERROR: ; EXPECT-ERROR: (Op2 <O2> <F>) ; EXPECT-ERROR: ^ ; EXPECT-ERROR: ") ; EXIT: 1 -(set-logic ALL) +(set-logic HO_ALL) (set-option :lang sygus2) ;(set-option :sygus-out status) (set-option :sygus-rec-fun true) -(set-option :uf-ho true) + (define-sort Time () Int) @@ -47,19 +47,19 @@ (and (<= 0 t tn) (match f ( ((P i) (val t i)) - - ((Op1 op g) + + ((Op1 op g) (match op ( - (NOT (not (holds g t))) + (NOT (not (holds g t))) - (Y (and (< 0 t) (holds g (- t 1)))) + (Y (and (< 0 t) (holds g (- t 1)))) (G (and (holds g t) (or (= t tn) (holds f (+ t 1))))) (H (and (holds g t) (or (= t 0) (holds f (- t 1))))) ))) - ((Op2 op f g) + ((Op2 op f g) (match op ( (AND (and (holds f t) (holds g t))) @@ -88,6 +88,3 @@ (constraint (holds (Op1 G (phi X0 X1)) 0)) (check-synth) - - - diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy index b08aa8929..2f59598ec 100644 --- a/test/regress/regress0/sygus/sygus-uf.sy +++ b/test/regress/regress0/sygus/sygus-uf.sy @@ -1,6 +1,6 @@ -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho +; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-var uf (-> Int Int)) diff --git a/test/regress/regress1/fmf/issue4225-univ-fun.smt2 b/test/regress/regress1/fmf/issue4225-univ-fun.smt2 index 9946a4567..af1f1e1a6 100644 --- a/test/regress/regress1/fmf/issue4225-univ-fun.smt2 +++ b/test/regress/regress1/fmf/issue4225-univ-fun.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --finite-model-find --uf-ho +; COMMAND-LINE: --finite-model-find ; EXPECT: unknown -(set-logic ALL) +(set-logic HO_ALL) ; this is not handled by fmf (assert (forall ((a (-> Int Int)) (b Int)) (not (= (a b) 0)))) (check-sat) diff --git a/test/regress/regress1/ho/NUM638^1.smt2 b/test/regress/regress1/ho/NUM638^1.smt2 index 59391ce8c..11683b1a7 100644 --- a/test/regress/regress1/ho/NUM638^1.smt2 +++ b/test/regress/regress1/ho/NUM638^1.smt2 @@ -1,8 +1,8 @@ -; COMMAND-LINE: --uf-ho --finite-model-find +; COMMAND-LINE: --finite-model-find ; EXPECT: unsat (set-option :incremental false) -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-sort nat 0) (declare-fun x () nat) diff --git a/test/regress/regress1/ho/NUM925^1.p b/test/regress/regress1/ho/NUM925^1.p index e162a63a4..e07ad784f 100644 --- a/test/regress/regress1/ho/NUM925^1.p +++ b/test/regress/regress1/ho/NUM925^1.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --ho-elim +% COMMAND-LINE: --ho-elim % EXPECT: % SZS status Theorem for NUM925^1 %------------------------------------------------------------------------------ diff --git a/test/regress/regress1/ho/SYO056^1.p b/test/regress/regress1/ho/SYO056^1.p index a8a6bafca..deda234da 100644 --- a/test/regress/regress1/ho/SYO056^1.p +++ b/test/regress/regress1/ho/SYO056^1.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --finite-model-find +% COMMAND-LINE: --finite-model-find % EXPECT: % SZS status CounterSatisfiable for SYO056^1 %------------------------------------------------------------------------------ diff --git a/test/regress/regress1/ho/bound_var_bug.p b/test/regress/regress1/ho/bound_var_bug.p index 0dc946d6a..23bda7fb2 100644 --- a/test/regress/regress1/ho/bound_var_bug.p +++ b/test/regress/regress1/ho/bound_var_bug.p @@ -1,4 +1,3 @@ -% COMMAND-LINE: --uf-ho % EXPECT: % SZS status GaveUp for bound_var_bug % TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/misc/leo --foatp e --atp e="$E_HOME"/eprover --atp epclextract="$E_HOME"/epclextract --proofoutput 1 --timeout 30 /Users/blanchette/hgs/afp_mining/tools/judgment_day_2017/data_afp/leo2-mepo/Call_Arity_SestoftGC_data/prob_308__3244432_1 ) ; } diff --git a/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p b/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p index 6c35270fd..22c1d1dd1 100644 --- a/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p +++ b/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --finite-model-find +% COMMAND-LINE: --finite-model-find % EXPECT: % SZS status Satisfiable for bug_freeVar_BDD_General_data_270 thf(ty_n_t__Nat__Onat, type, diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 index 21405dfdb..7c9de4c49 100644 --- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 +++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --uf-ho --finite-model-find -q --decision=justification-old +; COMMAND-LINE: --finite-model-find -q --decision=justification-old ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-sort qML_mu 0) (declare-sort qML_i 0) diff --git a/test/regress/regress1/ho/fta0328.lfho.p b/test/regress/regress1/ho/fta0328.lfho.p index c33b43ca5..f67c6db58 100644 --- a/test/regress/regress1/ho/fta0328.lfho.p +++ b/test/regress/regress1/ho/fta0328.lfho.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --uf-ho --finite-model-find +% COMMAND-LINE: --finite-model-find % EXPECT: % SZS status CounterSatisfiable for fta0328.lfho % TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/.isabelle/contrib/e-2.0-2/x86_64-darwin/eprover --auto-schedule --tstp-in --tstp-out --silent --cpu-limit=2 --proof-object=1 /Users/blanchette/hgs/matryoshka/papers/2019-TACAS-ehoh/eval/judgment_day/judgment_day_lifting_32/fta/prob_804__4064966_1 ) ; } diff --git a/test/regress/regress1/ho/hoa0102.smt2 b/test/regress/regress1/ho/hoa0102.smt2 index 6be063783..c5840e6a9 100644 --- a/test/regress/regress1/ho/hoa0102.smt2 +++ b/test/regress/regress1/ho/hoa0102.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --uf-ho --full-saturate-quant +; COMMAND-LINE: --full-saturate-quant ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort Com$ 0) (declare-sort Glb$ 0) diff --git a/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 b/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 index d536e51a1..d15095123 100644 --- a/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 +++ b/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --uf-ho --ho-elim +; COMMAND-LINE: --ho-elim ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-sort num 0) (declare-fun agent_THFTYPE_i () $$unsorted) diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2 index 9852150d9..a13aa2bae 100644 --- a/test/regress/regress1/ho/issue4065-no-rep.smt2 +++ b/test/regress/regress1/ho/issue4065-no-rep.smt2 @@ -1,7 +1,6 @@ -(set-logic AUFBV) +(set-logic HO_AUFBV) (set-info :status unsat) (set-option :fmf-bound-int true) -(set-option :uf-ho true) (declare-fun _substvar_20_ () Bool) (declare-sort S4 0) (assert (forall ((q15 S4) (q16 (_ BitVec 20)) (q17 (_ BitVec 13))) (xor (= (_ bv0 13) (_ bv0 13) q17 (bvsrem (_ bv0 13) (_ bv0 13)) q17) _substvar_20_ true))) diff --git a/test/regress/regress1/ho/issue4092-sinf.smt2 b/test/regress/regress1/ho/issue4092-sinf.smt2 index d3066c282..83a3e08b9 100644 --- a/test/regress/regress1/ho/issue4092-sinf.smt2 +++ b/test/regress/regress1/ho/issue4092-sinf.smt2 @@ -1,10 +1,9 @@ -; COMMAND-LINE: --uf-ho --sort-inference +; COMMAND-LINE: --sort-inference ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (set-option :sort-inference true) -(set-option :uf-ho true) (set-info :status sat) -(declare-fun a ( Int ) Int) -(declare-fun b ( Int ) Int) -(assert (and (distinct 0 (b 5)) (distinct a b ))) -(check-sat) +(declare-fun a ( Int ) Int) +(declare-fun b ( Int ) Int) +(assert (and (distinct 0 (b 5)) (distinct a b ))) +(check-sat) diff --git a/test/regress/regress1/ho/issue4134-sinf.smt2 b/test/regress/regress1/ho/issue4134-sinf.smt2 index 60a754aad..0003bc91e 100644 --- a/test/regress/regress1/ho/issue4134-sinf.smt2 +++ b/test/regress/regress1/ho/issue4134-sinf.smt2 @@ -1,7 +1,6 @@ -; COMMAND-LINE: --uf-ho --sort-inference +; COMMAND-LINE: --sort-inference ; EXPECT: sat -(set-logic ALL) -(set-option :uf-ho true) +(set-logic HO_ALL) (set-option :sort-inference true) (set-info :status sat) (declare-fun a () Int) diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 index 313ff68a1..6a8feba5c 100644 --- a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 +++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-produce-models --ho-elim +; COMMAND-LINE: --no-check-unsat-cores --no-produce-models --ho-elim ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-sort mu 0) (declare-fun meq_ind (mu mu $$unsorted) Bool) diff --git a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 index 6743e00d4..3f02e56fd 100644 --- a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 +++ b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 @@ -1,8 +1,7 @@ -; COMMAND-LINE: --uf-ho --finite-model-find --no-check-models +; COMMAND-LINE: --finite-model-find --no-check-models ; EXPECT: sat - -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-fun mvalid ((-> $$unsorted Bool)) Bool) diff --git a/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p b/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p index baabd675a..4068cc42e 100644 --- a/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p +++ b/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --finite-model-find +% COMMAND-LINE: --finite-model-find % EXPECT: % SZS status GaveUp for soundness_fmf_SYO362^5-delta %------------------------------------------------------------------------------ diff --git a/test/regress/regress1/ho/store-ax-min.p b/test/regress/regress1/ho/store-ax-min.p index d67eb8dad..d000a17d0 100644 --- a/test/regress/regress1/ho/store-ax-min.p +++ b/test/regress/regress1/ho/store-ax-min.p @@ -1,5 +1,5 @@ -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim-store-ax -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim +% COMMAND-LINE: --full-saturate-quant --ho-elim-store-ax +% COMMAND-LINE: --full-saturate-quant --ho-elim % EXPECT: % SZS status Theorem for store-ax-min thf(a, type, (a: $i)). diff --git a/test/regress/regress1/quantifiers/issue3724-quant.smt2 b/test/regress/regress1/quantifiers/issue3724-quant.smt2 index 6dd874fbf..32e82a8b5 100644 --- a/test/regress/regress1/quantifiers/issue3724-quant.smt2 +++ b/test/regress/regress1/quantifiers/issue3724-quant.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --uf-ho +; COMMAND-LINE: ; EXPECT: unknown -(set-logic ALL) +(set-logic HO_ALL) (assert (forall ((BOUND_VARIABLE_313 Bool) (BOUND_VARIABLE_314 (-> Int Bool)) (BOUND_VARIABLE_315 (-> Int Int)) (BOUND_VARIABLE_316 Int) (BOUND_VARIABLE_317 (-> Int Bool)) (BOUND_VARIABLE_318 Int)) (! (not (and (not (and (= (ite (and (not (= BOUND_VARIABLE_318 0)) (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))) (ite (BOUND_VARIABLE_317 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9))))))) BOUND_VARIABLE_316 0) 0) 0) (not (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))))) true)) :pattern (true))) ) diff --git a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 index 03bbd9469..9cb5cdac3 100644 --- a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 +++ b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 @@ -1,9 +1,9 @@ -(set-logic ALL) +; COMMAND-LINE: +(set-logic HO_ALL) (set-option :ag-miniscope-quant true) (set-option :conjecture-gen true) (set-option :int-wf-ind true) (set-option :sygus-inference true) -(set-option :uf-ho true) (set-info :status unsat) (declare-fun a () Real) (declare-fun b () Real) diff --git a/test/regress/regress1/sygus/eval-uc.sy b/test/regress/regress1/sygus/eval-uc.sy index e2bf9d144..e007eec51 100644 --- a/test/regress/regress1/sygus/eval-uc.sy +++ b/test/regress/regress1/sygus/eval-uc.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho -(set-logic ALL) +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic HO_ALL) (declare-sort S 0) (declare-var f Bool) (declare-var u (-> S Bool)) @@ -9,7 +9,7 @@ (define-fun init ((f Bool) (u (-> S Bool))) Bool (and f (forall ((x S)) (not (u x))))) (define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and (not new_f) (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x))))))) ;(define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and new_f (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x))))))) -(synth-fun inv_matrix ((f Bool) (u (-> S Bool)) (x S)) Bool ((Start Bool)) ((Start Bool ( (or (not +(synth-fun inv_matrix ((f Bool) (u (-> S Bool)) (x S)) Bool ((Start Bool)) ((Start Bool ( (or (not (u x)) (not f)))))) (define-fun inv ((f Bool) (u (-> S Bool))) Bool (forall ((x S)) (inv_matrix f u x))) (constraint (=> (and (inv f u) (trans f u new_f new_u)) (inv new_f new_u))) diff --git a/test/regress/regress1/sygus/ho-sygus.sy b/test/regress/regress1/sygus/ho-sygus.sy index 893c2034e..d46d8ecde 100644 --- a/test/regress/regress1/sygus/ho-sygus.sy +++ b/test/regress/regress1/sygus/ho-sygus.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho -(set-logic ALL) +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic HO_ALL) (synth-fun f ((y (-> Int Int)) (z Int)) Int) (declare-var z (-> Int Int)) (constraint (= (f z 0) (z 1))) diff --git a/test/regress/regress1/sygus/issue3507.smt2 b/test/regress/regress1/sygus/issue3507.smt2 index c8700f37b..1bbcb2984 100644 --- a/test/regress/regress1/sygus/issue3507.smt2 +++ b/test/regress/regress1/sygus/issue3507.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat -; COMMAND-LINE: --sygus-inference --uf-ho --quiet -(set-logic ALL) +; COMMAND-LINE: --sygus-inference --quiet +(set-logic HO_ALL) (declare-fun f (Int) Bool) (declare-fun g (Int) Bool) (assert (and (distinct f g) (g 0))) diff --git a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 index bc882fc8a..711afb2d8 100644 --- a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 +++ b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 @@ -1,6 +1,6 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-inference --fmf-bound --uf-ho -(set-logic ALL) +; COMMAND-LINE: --sygus-inference --fmf-bound +(set-logic HO_ALL) (declare-fun a () (_ BitVec 1)) (assert (bvsgt (bvsmod a a) #b0)) (check-sat) diff --git a/test/regress/regress1/sygus/list_recursor.sy b/test/regress/regress1/sygus/list_recursor.sy index 2e10a0c71..cb1ae2721 100644 --- a/test/regress/regress1/sygus/list_recursor.sy +++ b/test/regress/regress1/sygus/list_recursor.sy @@ -1,23 +1,23 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --lang=sygus2 --uf-ho +; COMMAND-LINE: --sygus-out=status --lang=sygus2 -(set-logic ALL) +(set-logic HO_ALL) (declare-datatype List ((cons (head Int) (tail List)) (nil))) (define-fun-rec List_rec ((x Int) (y (-> Int List Int Int)) (l List)) Int - (ite ((_ is nil) l) x + (ite ((_ is nil) l) x (y (head l) (tail l) (List_rec x y (tail l))))) (synth-fun f () Int ((I Int)) ((I Int (0 1 (+ I I))))) - + (synth-fun g ((x Int) (y List) (z Int)) Int ((I Int) (L List)) ((I Int (x z (+ I I) (head L) 0 1)) (L List (y (tail y))))) - + (constraint (= (List_rec f g (cons 0 (cons 1 nil))) 2)) (constraint (= (List_rec f g (cons 0 (cons 0 nil))) 2)) diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy index 7e1cd80b3..c74ce79b7 100644 --- a/test/regress/regress1/sygus/sygus-uf-ex.sy +++ b/test/regress/regress1/sygus/sygus-uf-ex.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho -(set-logic ALL) +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic HO_ALL) (declare-var uf (-> Int Int)) diff --git a/test/regress/regress1/sygus/uf-abduct.smt2 b/test/regress/regress1/sygus/uf-abduct.smt2 index 690e57290..bfcfe39fd 100644 --- a/test/regress/regress1/sygus/uf-abduct.smt2 +++ b/test/regress/regress1/sygus/uf-abduct.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --produce-abducts --uf-ho +; COMMAND-LINE: --produce-abducts ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 -(set-logic UFLIA) +(set-logic HO_UFLIA) (declare-fun f (Int) Int) (declare-fun a () Int) (assert (and (<= 0 a) (< a 4))) diff --git a/test/regress/regress2/ho/auth0068.smt2 b/test/regress/regress2/ho/auth0068.smt2 index eb0bb5d36..fc788a15c 100644 --- a/test/regress/regress2/ho/auth0068.smt2 +++ b/test/regress/regress2/ho/auth0068.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort Msg$ 0) (declare-sort Nat$ 0) diff --git a/test/regress/regress2/ho/bug_instfalse_SEU882^5.p b/test/regress/regress2/ho/bug_instfalse_SEU882^5.p index a62a2080a..bf58b95d8 100644 --- a/test/regress/regress2/ho/bug_instfalse_SEU882^5.p +++ b/test/regress/regress2/ho/bug_instfalse_SEU882^5.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim +% COMMAND-LINE: --full-saturate-quant --ho-elim % EXPECT: % SZS status Theorem for bug_instfalse_SEU882^5 %------------------------------------------------------------------------------ diff --git a/test/regress/regress2/ho/fta0409.smt2 b/test/regress/regress2/ho/fta0409.smt2 index 51ac5f2da..5516c804a 100644 --- a/test/regress/regress2/ho/fta0409.smt2 +++ b/test/regress/regress2/ho/fta0409.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort Nat$ 0) (declare-sort Complex$ 0) diff --git a/test/regress/regress2/ho/involved_parsing_ALG248^3.p b/test/regress/regress2/ho/involved_parsing_ALG248^3.p index d0577dd1f..47a89143d 100644 --- a/test/regress/regress2/ho/involved_parsing_ALG248^3.p +++ b/test/regress/regress2/ho/involved_parsing_ALG248^3.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --ho-elim +% COMMAND-LINE: --ho-elim % EXPECT: % SZS status Theorem for involved_parsing_ALG248^3 %------------------------------------------------------------------------------ diff --git a/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p b/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p index 37c7a02e8..5f87519d1 100644 --- a/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p +++ b/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim +% COMMAND-LINE: --full-saturate-quant --ho-elim % EXPECT: % SZS status Theorem for partial_app_interpreted_SWW474^2 %------------------------------------------------------------------------------ diff --git a/test/regress/regress3/ho/SYO362^5.p b/test/regress/regress3/ho/SYO362^5.p index b9537fd0e..41fe3d541 100644 --- a/test/regress/regress3/ho/SYO362^5.p +++ b/test/regress/regress3/ho/SYO362^5.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim --decision=justification-old +% COMMAND-LINE: --full-saturate-quant --ho-elim --decision=justification-old % EXPECT: % SZS status Theorem for SYO362^5 thf(cK,type,( diff --git a/test/regress/regress3/issue4170.smt2 b/test/regress/regress3/issue4170.smt2 index 0dee146c0..25e0c7f8d 100644 --- a/test/regress/regress3/issue4170.smt2 +++ b/test/regress/regress3/issue4170.smt2 @@ -1,6 +1,5 @@ -(set-logic ALL) +(set-logic HO_ALL) (set-option :sygus-inference true) -(set-option :uf-ho true) (set-option :sygus-ext-rew false) (set-info :status sat) (declare-fun a (Int) Int) |