This commit adds a new parser option, --hol, which marks that HOL is being used. This option has the effect of prepending the problem's logic with "HO_", which teels the solver that the logic is higher order. The parser builder, base parser, and SMT2 and TPTP parsers are all updated to work with this new setting, as is the logic info class.
For now this parser option is enabling the --uf-ho option for internal use, since for now higher-order solving relies it. In a future PR this dependency will be removed (since this information is already given to the SMT solver via the logic).
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.");
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);
* 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);
/**
* 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
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,
/** 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? */
return *this;
}
-ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic) {
+ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic)
+{
d_logicIsForced = true;
d_forcedLogic = logic;
return *this;
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;
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())
{
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_.");
}
}
}
}
}
- // 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())
{
}
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_.");
}
}
}
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;
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]
#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
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);
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.");
}
}
}
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;
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);
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);
bool d_cnf; // in a cnf formula
bool d_fof; // in an fof formula
+ bool d_hol; // in a thf formula
};/* class Tptp */
// 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())
{
}
// 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))))
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
: options::DecisionMode::INTERNAL);
bool stoponly =
- // ALL
+ // ALL or its supersets
logic.hasEverything() || logic.isTheoryEnabled(THEORY_STRINGS)
? false
: ( // QF_AUFLIA
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)
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)
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) */
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_";
if(d_theories[THEORY_FP]) {
ss << "FP";
++seen;
- }
+ }
if(d_theories[THEORY_DATATYPES]) {
ss << "DT";
++seen;
if(seen == 0) {
ss << "SAT";
}
-
- d_logicString = ss.str();
}
+ d_logicString = ss.str();
}
return d_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")) {
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;
else if (!strcmp(p, "HORN"))
{
// the HORN logic
- enableEverything();
+ enableEverything(d_higherOrder);
enableQuantifiers();
arithNonLinear();
p += 4;
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() {
enableTheory(THEORY_UF);
enableTheory(THEORY_DATATYPES);
enableIntegers();
- enableHigherOrder();
}
void LogicInfo::enableSeparationLogic()
/** 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) */
/**
* 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
; 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)
; 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))
-; 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)
-; 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)
-% COMMAND-LINE: --uf-ho
% EXPECT: % SZS status Unsatisfiable for bug_nodbuilding_interpreted_SYO042^1
%------------------------------------------------------------------------------
-; 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)
-; 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)
-; 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))
-; 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))
-; 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)
-; 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)
-; 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)
-; 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)
-; 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)
-; COMMAND-LINE: --uf-ho
; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
(declare-datatype Unit ((unit)))
-; 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)
-; 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)
-; 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)))
-; 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)
-; 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)
-; COMMAND-LINE: --uf-ho
; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
(set-info :status unsat)
(declare-sort U 0)
-; COMMAND-LINE: --uf-ho
; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
(set-info :status unsat)
(declare-sort U 0)
-; COMMAND-LINE: --uf-ho
; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
(set-info :status unsat)
(declare-sort U 0)
-; 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)
-; 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)
-; 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)
-; 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))
-; 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)
-; COMMAND-LINE: --uf-ho
; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
(set-info :status sat)
(declare-fun f (Int) Int)
-; 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)
-; 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)
-; COMMAND-LINE: --uf-ho
; EXPECT: unknown
-(set-logic ALL)
+(set-logic HO_ALL)
(declare-sort $$unsorted 0)
(declare-sort mu 0)
-; 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)
-; 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)
-; 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)
; 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)
(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)))
(constraint (holds (Op1 G (phi X0 X1)) 0))
(check-synth)
-
-
-
-; 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))
-; 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)
-; 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)
-% COMMAND-LINE: --uf-ho --ho-elim
+% COMMAND-LINE: --ho-elim
% EXPECT: % SZS status Theorem for NUM925^1
%------------------------------------------------------------------------------
-% COMMAND-LINE: --uf-ho --finite-model-find
+% COMMAND-LINE: --finite-model-find
% EXPECT: % SZS status CounterSatisfiable for SYO056^1
%------------------------------------------------------------------------------
-% 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 ) ; }
-% 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,
-; 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)
-% 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 ) ; }
-; 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)
-; 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)
-(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)))
-; 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)
-; 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)
-; 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)
-; 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)
-% COMMAND-LINE: --uf-ho --finite-model-find
+% COMMAND-LINE: --finite-model-find
% EXPECT: % SZS status GaveUp for soundness_fmf_SYO362^5-delta
%------------------------------------------------------------------------------
-% 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)).
-; 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)))
)
-(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)
; 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))
(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)))
; 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)))
; 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)))
; 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)
; 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))
; 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))
-; 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)))
-; 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)
-% 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
%------------------------------------------------------------------------------
-; 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)
-% COMMAND-LINE: --uf-ho --ho-elim
+% COMMAND-LINE: --ho-elim
% EXPECT: % SZS status Theorem for involved_parsing_ALG248^3
%------------------------------------------------------------------------------
-% 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
%------------------------------------------------------------------------------
-% 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,(
-(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)
projects / cvc5.git / commitdiff