diff --git a/proofs/eo/cpc/theories/BitVectors.eo b/proofs/eo/cpc/theories/BitVectors.eo index 258365b1310..833d4eb1ff0 100644 --- a/proofs/eo/cpc/theories/BitVectors.eo +++ b/proofs/eo/cpc/theories/BitVectors.eo @@ -343,8 +343,6 @@ (BitVec m) Int) ) -(declare-const BITVECTOR_EAGER_ATOM (-> Bool Bool)) - ; internal operators (declare-const @bit diff --git a/proofs/eo/cpc/theories/Datatypes.eo b/proofs/eo/cpc/theories/Datatypes.eo index 47545f10e53..8b396d30c31 100644 --- a/proofs/eo/cpc/theories/Datatypes.eo +++ b/proofs/eo/cpc/theories/Datatypes.eo @@ -59,5 +59,5 @@ ; disclaimer: This function is not in the SMT-LIB standard. (declare-const nullable.lift (-> (! Type :var F :implicit) F ($get_type_nullable_lift F))) -; skolems -;SHARED_SELECTOR +; shared selector +(declare-const @shared_selector (-> (! Type :var D) (! Type :var T) Int D T)) diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 21d3f7d5bb8..678c2a2d886 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -83,6 +83,7 @@ void AstPrinter::toStream(std::ostream& out, { for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) { + out << ' '; // body is re-letified if (i == 1) { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 0bee9b74bad..a32b812166e 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1116,6 +1116,10 @@ void Smt2Printer::toStream(std::ostream& out, { visit.pop_back(); out << "(...)"; + if (cur.getNumChildren() > 0) + { + out << ')'; + } continue; } } diff --git a/src/proof/alf/alf_node_converter.cpp b/src/proof/alf/alf_node_converter.cpp index 17852b3776c..c0ae25145fd 100644 --- a/src/proof/alf/alf_node_converter.cpp +++ b/src/proof/alf/alf_node_converter.cpp @@ -25,6 +25,7 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/sequence.h" +#include "expr/sort_to_term.h" #include "printer/smt2/smt2_printer.h" #include "theory/builtin/generic_op.h" #include "theory/bv/theory_bv_utils.h" @@ -294,6 +295,13 @@ Node AlfNodeConverter::postConvert(Node n) return mkInternalApp("to_fp_bv", children, tn); } } + else if (k == Kind::BITVECTOR_EAGER_ATOM) + { + // For now, we explicity remove the application. + // https://github.com/cvc5/cvc5-wishues/issues/156: if the smt2 printer + // is refactored to silently ignore this kind, this case can be deleted. + return n[0]; + } else if (GenericOp::isIndexedOperatorKind(k)) { TypeNode tn = n.getType(); @@ -545,22 +553,30 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n, bool reqCast) else if (k == Kind::APPLY_SELECTOR) { // maybe a shared selector - ret = maybeMkSkolemFun(op); - if (!ret.isNull()) - { - return ret; - } - unsigned index = DType::indexOf(op); - const DType& dt = DType::datatypeOf(op); - if (dt.isTuple()) + if (op.getSkolemId() == SkolemId::SHARED_SELECTOR) { - indices.push_back(d_nm->mkConstInt(index)); - opName << "tuple.select"; + std::vector kindices = op.getSkolemIndices(); + opName << "@shared_selector"; + indices.push_back( + typeAsNode(kindices[0].getConst().getType())); + indices.push_back( + typeAsNode(kindices[1].getConst().getType())); + indices.push_back(kindices[2]); } else { - unsigned cindex = DType::cindexOf(op); - opName << dt[cindex][index].getSelector(); + unsigned index = DType::indexOf(op); + const DType& dt = DType::datatypeOf(op); + if (dt.isTuple()) + { + indices.push_back(d_nm->mkConstInt(index)); + opName << "tuple.select"; + } + else + { + unsigned cindex = DType::cindexOf(op); + opName << dt[cindex][index].getSelector(); + } } } else diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index 10659b62407..aa7c771d697 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -180,6 +180,7 @@ bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn) case ProofRule::QUANT_VAR_REORDERING: case ProofRule::ENCODE_EQ_INTRO: case ProofRule::HO_APP_ENCODE: + case ProofRule::BV_EAGER_ATOM: case ProofRule::ACI_NORM: case ProofRule::ARITH_POLY_NORM: case ProofRule::ARITH_POLY_NORM_REL: @@ -496,7 +497,8 @@ std::string AlfPrinter::getRuleName(const ProofNode* pfn) const ss << id; return ss.str(); } - else if (r == ProofRule::ENCODE_EQ_INTRO || r == ProofRule::HO_APP_ENCODE) + else if (r == ProofRule::ENCODE_EQ_INTRO || r == ProofRule::HO_APP_ENCODE + || r == ProofRule::BV_EAGER_ATOM) { // ENCODE_EQ_INTRO proves (= t (convert t)) from argument t, // where (convert t) is indistinguishable from t according to the proof. diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 168abd5ceaa..6e6ee0d5e50 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -218,20 +218,11 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id, { TrustId tid; getTrustId(args[0], tid); - // we don't do this for steps that are already extended theory rewrite - // steps, or we would get an infinite loop in reconstruction. - if (tid == TrustId::EXT_THEORY_REWRITE) - { - return Node::null(); - } - // maybe we can show it rewrites to true based on (extended) rewriting + // maybe we can show it rewrites to true based on rewriting // modulo original forms (MACRO_SR_PRED_INTRO). TheoryProofStepBuffer psb(d_pc); - if (psb.applyPredIntro(res, - {}, - MethodId::SB_DEFAULT, - MethodId::SBA_SEQUENTIAL, - MethodId::RW_EXT_REWRITE)) + if (psb.applyPredIntro( + res, {}, MethodId::SB_DEFAULT, MethodId::SBA_SEQUENTIAL)) { cdp->addSteps(psb); return res; diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 9fa4d1c959a..66a888d2e9d 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1139,11 +1139,12 @@ bool SetDefaults::incompatibleWithProofs(Options& opts, if (opts.smt.proofMode == options::ProofMode::FULL_STRICT) { // symmetry breaking does not have proof support - SET_AND_NOTIFY_VAL_SYM(uf, ufSymmetryBreaker, false, "full strict proofs"); + SET_AND_NOTIFY(uf, ufSymmetryBreaker, false, "full strict proofs"); // CEGQI with deltas and infinities is not supported SET_AND_NOTIFY(quantifiers, cegqiMidpoint, true, "full strict proofs"); SET_AND_NOTIFY(quantifiers, cegqiUseInfInt, false, "full strict proofs"); SET_AND_NOTIFY(quantifiers, cegqiUseInfReal, false, "full strict proofs"); + // shared selectors are not supported SET_AND_NOTIFY(datatypes, dtSharedSelectors, false, "full strict proofs"); } return false; diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index b57b00912e0..aa3cba4b47c 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -78,8 +78,10 @@ Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) Assert(tn.isDatatype()); const DType& dt = tn.getDType(); size_t i = utils::indexOf(n.getOperator()); - bool sharedSel = d_opts.datatypes.dtSharedSelectors; - Node ticons = utils::getInstCons(t, dt, i, sharedSel); + // Note that we set shared selectors to false. This proof rule will + // be (unintentionally) unsuccessful when reconstructing proofs of the + // rewriter when using shared selectors. + Node ticons = utils::getInstCons(t, dt, i, false); return t.eqNode(ticons); } case ProofRewriteRule::DT_COLLAPSE_SELECTOR: @@ -90,6 +92,11 @@ Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) return Node::null(); } Node selector = n.getOperator(); + // shared selectors are not supported + if (selector.getSkolemId() == SkolemId::SHARED_SELECTOR) + { + return Node::null(); + } size_t constructorIndex = utils::indexOf(n[0].getOperator()); const DType& dt = utils::datatypeOf(selector); const DTypeConstructor& c = dt[constructorIndex]; diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 6b3e3e48b5f..38b1532a7b8 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -150,11 +150,6 @@ Node InferenceManager::prepareDtInference(Node conc, { Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp << " by " << id << std::endl; - if (conc.getKind() == Kind::EQUAL && conc[0].getType().isBoolean()) - { - // must turn (= conc false) into (not conc) - conc = rewrite(conc); - } if (isProofEnabled()) { Assert(ipc != nullptr); diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp index 623f5e0d28c..3260fce7e5c 100644 --- a/src/theory/datatypes/proof_checker.cpp +++ b/src/theory/datatypes/proof_checker.cpp @@ -23,9 +23,8 @@ namespace cvc5::internal { namespace theory { namespace datatypes { -DatatypesProofRuleChecker::DatatypesProofRuleChecker(NodeManager* nm, - bool sharedSel) - : ProofRuleChecker(nm), d_sharedSel(sharedSel) +DatatypesProofRuleChecker::DatatypesProofRuleChecker(NodeManager* nm) + : ProofRuleChecker(nm) { } diff --git a/src/theory/datatypes/proof_checker.h b/src/theory/datatypes/proof_checker.h index 42bab401b50..c31a51ac5a2 100644 --- a/src/theory/datatypes/proof_checker.h +++ b/src/theory/datatypes/proof_checker.h @@ -30,7 +30,7 @@ namespace datatypes { class DatatypesProofRuleChecker : public ProofRuleChecker { public: - DatatypesProofRuleChecker(NodeManager* nm, bool sharedSel); + DatatypesProofRuleChecker(NodeManager* nm); /** Register all rules owned by this rule checker into pc. */ void registerTo(ProofChecker* pc) override; @@ -40,8 +40,6 @@ class DatatypesProofRuleChecker : public ProofRuleChecker Node checkInternal(ProofRule id, const std::vector& children, const std::vector& args) override; - /** Whether we are using shared selectors */ - bool d_sharedSel; }; } // namespace datatypes diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index edbab9eefba..055e6b79239 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -64,7 +64,7 @@ TheoryDatatypes::TheoryDatatypes(Env& env, d_state(env, valuation), d_im(env, *this, d_state), d_notify(d_im, *this), - d_checker(nodeManager(), options().datatypes.dtSharedSelectors), + d_checker(nodeManager()), d_cpacb(*this) { d_true = nodeManager()->mkConst(true); diff --git a/src/theory/quantifiers/ho_term_database.cpp b/src/theory/quantifiers/ho_term_database.cpp index dfd81376a5c..7a057c77931 100644 --- a/src/theory/quantifiers/ho_term_database.cpp +++ b/src/theory/quantifiers/ho_term_database.cpp @@ -155,7 +155,6 @@ bool HoTermDb::checkCongruentDisequal(TNode a, TNode b, std::vector& exp) { return false; } - exp.push_back(a.eqNode(b)); // operators might be disequal Node af = getMatchOperator(a); Node bf = getMatchOperator(b); @@ -163,7 +162,7 @@ bool HoTermDb::checkCongruentDisequal(TNode a, TNode b, std::vector& exp) { if (a.getKind() == Kind::APPLY_UF && b.getKind() == Kind::APPLY_UF) { - exp.push_back(af.eqNode(bf).negate()); + exp.push_back(af.eqNode(bf)); Assert(d_qstate.areEqual(af, bf)) << af << " and " << bf << " are not equal"; } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 915d46b031c..4402c9017f8 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -23,6 +23,10 @@ #include "options/smt_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "proof/proof.h" +#include "proof/proof_generator.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_manager.h" #include "theory/quantifiers/ematching/trigger_term_info.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" @@ -39,6 +43,68 @@ namespace cvc5::internal { namespace theory { namespace quantifiers { +/** + * A proof generator for proving simple congruence lemmas discovered by TermDb. + */ +class DeqCongProofGenerator : protected EnvObj, public ProofGenerator +{ + public: + DeqCongProofGenerator(Env& env) : EnvObj(env) {} + virtual ~DeqCongProofGenerator() {} + /** + * The lemma is of the form: + * (=> (and (= ti si) .. (= tj sj)) (= (f t1 ... tn) (f s1 ... sn))) + * which can be proven by a congruence step. + */ + std::shared_ptr getProofFor(Node fact) override + { + Assert(fact.getKind() == Kind::IMPLIES); + Assert(fact[1].getKind() == Kind::EQUAL); + Node a = fact[1][0]; + Node b = fact[1][1]; + std::vector assumps; + if (fact[0].getKind() == Kind::AND) + { + assumps.insert(assumps.end(), fact[0].begin(), fact[0].end()); + } + else + { + assumps.push_back(fact[0]); + } + CDProof cdp(d_env); + if (a.getOperator() != b.getOperator()) + { + // TODO: wishue #158, likely corresponds to a higher-order term + // indexing conflict. + cdp.addTrustedStep(fact, TrustId::QUANTIFIERS_PREPROCESS, {}, {}); + return cdp.getProofFor(fact); + } + Assert(a.getNumChildren() == b.getNumChildren()); + std::vector cargs; + ProofRule cr = expr::getCongRule(a, cargs); + size_t nchild = a.getNumChildren(); + std::vector premises; + for (size_t i = 0; i < nchild; i++) + { + Node eq = a[i].eqNode(b[i]); + premises.push_back(eq); + if (a[i] == b[i]) + { + cdp.addStep(eq, ProofRule::REFL, {}, {a[i]}); + } + else + { + Assert(std::find(assumps.begin(), assumps.end(), eq) != assumps.end()); + } + } + cdp.addStep(fact[1], cr, premises, cargs); + std::shared_ptr pfn = cdp.getProofFor(fact[1]); + return d_env.getProofNodeManager()->mkScope(pfn, assumps); + } + /** identify */ + std::string identify() const override { return "DeqCongProofGenerator"; } +}; + TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) : QuantifiersUtil(env), d_qstate(qs), @@ -48,7 +114,9 @@ TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) d_typeMap(context()), d_ops(context()), d_opMap(context()), - d_inactive_map(context()) + d_inactive_map(context()), + d_dcproof(options().smt.produceProofs ? new DeqCongProofGenerator(d_env) + : nullptr) { d_true = nodeManager()->mkConst(true); d_false = nodeManager()->mkConst(false); @@ -390,19 +458,19 @@ void TermDb::computeUfTerms( TNode f ) { congruentCount++; continue; } - std::vector lits; - if (checkCongruentDisequal(at, n, lits)) + std::vector antec; + if (checkCongruentDisequal(at, n, antec)) { Assert(at.getNumChildren() == n.getNumChildren()); for (size_t k = 0, size = at.getNumChildren(); k < size; k++) { if (at[k] != n[k]) { - lits.push_back(nm->mkNode(Kind::EQUAL, at[k], n[k]).negate()); + antec.push_back(nm->mkNode(Kind::EQUAL, at[k], n[k])); Assert(d_qstate.areEqual(at[k], n[k])); } } - Node lem = nm->mkOr(lits); + Node lem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(antec), at.eqNode(n)); if (TraceIsOn("term-db-lemma")) { Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " @@ -415,7 +483,10 @@ void TermDb::computeUfTerms( TNode f ) { } Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } - d_qim->addPendingLemma(lem, InferenceId::QUANTIFIERS_TDB_DEQ_CONG); + d_qim->addPendingLemma(lem, + InferenceId::QUANTIFIERS_TDB_DEQ_CONG, + LemmaProperty::NONE, + d_dcproof.get()); d_qstate.notifyInConflict(); return; } @@ -442,7 +513,6 @@ bool TermDb::checkCongruentDisequal(TNode a, TNode b, std::vector& exp) { if (d_qstate.areDisequal(a, b)) { - exp.push_back(a.eqNode(b)); return true; } return false; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index baa52fa2082..957fb56cf73 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -36,6 +36,7 @@ namespace quantifiers { class QuantifiersState; class QuantifiersInferenceManager; class QuantifiersRegistry; +class DeqCongProofGenerator; /** Context-dependent list of nodes */ class DbList @@ -263,6 +264,8 @@ class TermDb : public QuantifiersUtil { * of equality engine (for higher-order). */ std::map d_ho_type_match_pred; + /** A proof generator for disequal congruent terms */ + std::shared_ptr d_dcproof; //----------------------------- implementation-specific /** * Finish reset internal, called at the end of reset(e). Returning false will @@ -279,8 +282,8 @@ class TermDb : public QuantifiersUtil { * This method is called when terms a and b are indexed by the same operator, * and have equivalent arguments. This method checks if we are in conflict, * which is the case if a and b are disequal in the equality engine. - * If so, it adds the set of literals that are implied but do not hold, e.g. - * the equality (= a b). + * If so, it adds any additional arguments that explain why a = b, e.g. the + * equivalence of their operators if their operators are different. */ virtual bool checkCongruentDisequal(TNode a, TNode b, std::vector& exp); //----------------------------- end implementation-specific diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 71ae0c13d55..175c419f4c6 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -724,6 +724,7 @@ set(regress_0_tests regress0/datatypes/pair-real-bool.smt2 regress0/datatypes/par-updater-type-rule.smt2 regress0/datatypes/parametric-alt-list.cvc.smt2 + regress0/datatypes/pf-v2l60078.smt2 regress0/datatypes/proj-issue172.smt2 regress0/datatypes/proj-issue474-app-cons-value.smt2 regress0/datatypes/proj-issue578-clash-pf.smt2 @@ -1460,6 +1461,7 @@ set(regress_0_tests regress0/quantifiers/cond-var-elim-binary.smt2 regress0/quantifiers/dd_german169_semi_eval.smt2 regress0/quantifiers/dd_spark2014-pat.smt2 + regress0/quantifiers/dd_SA10-027-dt-ipc.smt2 regress0/quantifiers/dd.german169-ieval.smt2 regress0/quantifiers/dd.german169-lemma-inp.smt2 regress0/quantifiers/dd.ho-matching-enum.smt2 @@ -2878,6 +2880,7 @@ set(regress_1_tests regress1/quantifiers/nra-interleave-inst.smt2 regress1/quantifiers/opisavailable-12.smt2 regress1/quantifiers/parametric-lists.smt2 + regress1/quantifiers/pivc-deq-cong.smt2 regress1/quantifiers/pool-decidable-arrays-1.smt2 regress1/quantifiers/pool-example.smt2 regress1/quantifiers/pool-tuple.smt2 diff --git a/test/regress/cli/regress0/datatypes/pf-v2l60078.smt2 b/test/regress/cli/regress0/datatypes/pf-v2l60078.smt2 new file mode 100644 index 00000000000..f58dabb38a8 --- /dev/null +++ b/test/regress/cli/regress0/datatypes/pf-v2l60078.smt2 @@ -0,0 +1,6 @@ +; EXPECT: unsat +(set-logic QF_DT) +(declare-datatypes ((n 0) (l 0) (t 0)) (((z)) ((ln) (n (r l))) ((f)))) +(declare-fun x () l) +(assert (and (not (= ln (r x))) (not ((_ is n) (r x))))) +(check-sat) diff --git a/test/regress/cli/regress0/quantifiers/dd_SA10-027-dt-ipc.smt2 b/test/regress/cli/regress0/quantifiers/dd_SA10-027-dt-ipc.smt2 new file mode 100644 index 00000000000..19723e2c7eb --- /dev/null +++ b/test/regress/cli/regress0/quantifiers/dd_SA10-027-dt-ipc.smt2 @@ -0,0 +1,15 @@ +; EXPECT: unsat +; DISABLE-TESTER: cpc +; Disabled cpc due to congruence on overloaded user functions. +(set-logic ALL) +(declare-sort i 0) +(declare-sort s 0) +(declare-datatypes ((u 0)) (((us (r Bool) (e Int) (c s))))) +(declare-datatypes ((us_ 0)) (((us (c i) (e u))))) +(declare-datatypes ((_r 0)) (((s_ (_s us_))))) +(declare-fun s_ (s) _r) +(declare-fun us (_r) s) +(assert (forall ((x _r)) (= x (s_ (us x))))) +(declare-const n u) +(assert (exists ((x_ us_)) (not (=> (r n) (= (s_ x_) (s_ (c (us false 0 (us (s_ (us (c (_s (s_ (c n)))) n))))))) (forall ((o u)) (or (forall ((x us_)) (or (forall ((o u)) (or (forall ((x us_)) (or (forall ((o u)) (or (forall ((x us_)) (or (exists ((t u)) (= (r o) (= (r o) (r (e (_s (s_ (c t)))))))) (= (s_ x_) (s_ (c (us false 0 (us (s_ (us (c (_s (s_ (c o)))) (us (r (e (_s (s_ (c (us false 0 (us (s_ x_)))))))) (e (e (_s (s_ (c o))))) (us (s_ x_)))))))))))))))))))))))))) +(check-sat) diff --git a/test/regress/cli/regress1/quantifiers/pivc-deq-cong.smt2 b/test/regress/cli/regress1/quantifiers/pivc-deq-cong.smt2 new file mode 100644 index 00000000000..8597415dae3 --- /dev/null +++ b/test/regress/cli/regress1/quantifiers/pivc-deq-cong.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --enum-inst +; EXPECT: unsat +(set-logic ALL) +(declare-fun V () Int) +(declare-fun e () Int) +(declare-fun a2 () (Array Int Int)) +(declare-fun a () (Array Int Int)) +(declare-fun i () Int) +(assert (and (< i V) (<= 0 i) (forall ((? Int)) (= 1 (select a2 i))) (forall ((? Int)) (= (select a ?) (select a2 ?))) (forall ((? Int)) (forall ((? Int)) (= 1 (select a2 ?)))) (forall ((? Int)) (or (distinct e (select a ?)) (> ? (- i 1)))) (or (and (= 1 V) (exists ((? Int)) (> 1 (select a 0)))) (exists ((? Int)) (and (<= ? i) (= e (select a ?))))))) +(check-sat)