From: Andres Noetzli Date: Wed, 8 Apr 2020 21:38:09 +0000 (-0700) Subject: Perform theory widening eagerly (#4044) X-Git-Tag: cvc5-1.0.0~3395 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a48cafdd09c3ff8cb9984bad930343958c30ce56;p=cvc5.git Perform theory widening eagerly (#4044) Fixes #3971 and fixes #3991. In incremental mode, the logic can change from one (check-sat) call to another. In the reported issue, we start with QF_NIA but then switch to QF_UFNIA because there is a div term (which has a UF in its expanded form). Dealing with this issue is challenging in general. As a result, we have decided not to allow theory widening in Theory::expandDefinitions() anymore but instead to do it eagerly in SmtEngine::setDefaults(). --- diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index fd98064e3..d1eed0748 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -509,23 +509,25 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } } + ///////////////////////////////////////////////////////////////////////////// + // Theory widening + // + // Some theories imply the use of other theories to handle certain operators, + // e.g. UF to handle partial functions. + ///////////////////////////////////////////////////////////////////////////// + bool needsUf = false; // strings require LIA, UF; widen the logic if (logic.isTheoryEnabled(THEORY_STRINGS)) { LogicInfo log(logic.getUnlockedCopy()); // Strings requires arith for length constraints, and also UF - if (!logic.isTheoryEnabled(THEORY_UF)) - { - Trace("smt") << "because strings are enabled, also enabling UF" - << std::endl; - log.enableTheory(THEORY_UF); - } + needsUf = true; if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic() || !logic.areIntegersUsed()) { - Trace("smt") << "because strings are enabled, also enabling linear " - "integer arithmetic" - << std::endl; + Notice() + << "Enabling linear integer arithmetic because strings are enabled" + << std::endl; log.enableTheory(THEORY_ARITH); log.enableIntegers(); log.arithOnlyLinear(); @@ -533,21 +535,34 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) logic = log; logic.lock(); } - if (logic.isTheoryEnabled(THEORY_ARRAYS) + if (needsUf + // Arrays, datatypes and sets permit Boolean terms and thus require UF + || logic.isTheoryEnabled(THEORY_ARRAYS) || logic.isTheoryEnabled(THEORY_DATATYPES) - || logic.isTheoryEnabled(THEORY_SETS)) + || logic.isTheoryEnabled(THEORY_SETS) + // Non-linear arithmetic requires UF to deal with division/mod because + // their expansion introduces UFs for the division/mod-by-zero case. + || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()) + // If division/mod-by-zero is not treated as a constant value in BV, we + // need UF. + || (logic.isTheoryEnabled(THEORY_BV) + && !options::bitvectorDivByZeroConst()) + // FP requires UF since there are multiple operators that are partially + // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more + // details). + || logic.isTheoryEnabled(THEORY_FP)) { if (!logic.isTheoryEnabled(THEORY_UF)) { LogicInfo log(logic.getUnlockedCopy()); - Trace("smt") << "because a theory that permits Boolean terms is enabled, " - "also enabling UF" - << std::endl; + Notice() << "Enabling UF because " << logic << " requires it." + << std::endl; log.enableTheory(THEORY_UF); logic = log; logic.lock(); } } + ///////////////////////////////////////////////////////////////////////////// // by default, symmetry breaker is on only for non-incremental QF_UF if (!options::ufSymmetryBreaker.wasSetByUser()) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3ac719eed..dee3365fb 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1588,8 +1588,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_maptheoryOf(node); Assert(t != NULL); - LogicRequest req(d_smt); - node = t->expandDefinition(req, n); + node = t->expandDefinition(n); } // the partial functions can fall through, in which case we still diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e4aeca980..cdb6c77f3 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -63,8 +63,9 @@ void TheoryArith::preRegisterTerm(TNode n){ d_internal->preRegisterTerm(n); } -Node TheoryArith::expandDefinition(LogicRequest &logicRequest, Node node) { - return d_internal->expandDefinition(logicRequest, node); +Node TheoryArith::expandDefinition(Node node) +{ + return d_internal->expandDefinition(node); } void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index a16f1ed5e..f15db32a1 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -58,7 +58,7 @@ public: */ void preRegisterTerm(TNode n) override; - Node expandDefinition(LogicRequest& logicRequest, Node node) override; + Node expandDefinition(Node node) override; void setMasterEqualityEngine(eq::EqualityEngine* eq) override; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index bed59baf5..374de8562 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -5061,8 +5061,8 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{ return d_rowTracking[ridx]; } - -Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) { +Node TheoryArithPrivate::expandDefinition(Node node) +{ NodeManager* nm = NodeManager::currentNM(); // eliminate here since the rewritten form of these may introduce division @@ -5082,8 +5082,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) Node ret = nm->mkNode(kind::DIVISION_TOTAL, num, den); if (!den.isConst() || den.getConst().sgn() == 0) { - Node divByZeroNum = - getArithSkolemApp(logicRequest, num, ArithSkolemId::DIV_BY_ZERO); + Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO); Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret); } @@ -5098,8 +5097,8 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den); if (!den.isConst() || den.getConst().sgn() == 0) { - Node intDivByZeroNum = getArithSkolemApp( - logicRequest, num, ArithSkolemId::INT_DIV_BY_ZERO); + Node intDivByZeroNum = + getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO); Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret); } @@ -5114,8 +5113,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den); if (!den.isConst() || den.getConst().sgn() == 0) { - Node modZeroNum = - getArithSkolemApp(logicRequest, num, ArithSkolemId::MOD_BY_ZERO); + Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO); Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret); } @@ -5147,8 +5145,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) Node lem; if (k == kind::SQRT) { - Node skolemApp = - getArithSkolemApp(logicRequest, node[0], ArithSkolemId::SQRT); + Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT); Node uf = skolemApp.eqNode(var); Node nonNeg = nm->mkNode( kind::AND, nm->mkNode(kind::MULT, var, var).eqNode(node[0]), uf); @@ -5219,8 +5216,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) Unreachable(); } -Node TheoryArithPrivate::getArithSkolem(LogicRequest& logicRequest, - ArithSkolemId asi) +Node TheoryArithPrivate::getArithSkolem(ArithSkolemId asi) { std::map::iterator it = d_arith_skolem.find(asi); if (it == d_arith_skolem.end()) @@ -5268,7 +5264,6 @@ Node TheoryArithPrivate::getArithSkolem(LogicRequest& logicRequest, nm->mkFunctionType(tn, tn), desc, NodeManager::SKOLEM_EXACT_NAME); - logicRequest.widenLogic(THEORY_UF); } d_arith_skolem[asi] = skolem; return skolem; @@ -5276,11 +5271,9 @@ Node TheoryArithPrivate::getArithSkolem(LogicRequest& logicRequest, return it->second; } -Node TheoryArithPrivate::getArithSkolemApp(LogicRequest& logicRequest, - Node n, - ArithSkolemId asi) +Node TheoryArithPrivate::getArithSkolemApp(Node n, ArithSkolemId asi) { - Node skolem = getArithSkolem(logicRequest, asi); + Node skolem = getArithSkolem(asi); if (!options::arithNoPartialFun()) { skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index a4469f3b5..b5debe76d 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -432,7 +432,7 @@ public: * Does non-context dependent setup for a node connected to a theory. */ void preRegisterTerm(TNode n); - Node expandDefinition(LogicRequest &logicRequest, Node node); + Node expandDefinition(Node node); void setMasterEqualityEngine(eq::EqualityEngine* eq); @@ -860,10 +860,9 @@ private: /** get arithmetic skolem * * Returns the Skolem in the above map for the given id, creating it if it - * does not already exist. If a Skolem function is created, the logic is - * widened to include UF. + * does not already exist. */ - Node getArithSkolem(LogicRequest& logicRequest, ArithSkolemId asi); + Node getArithSkolem(ArithSkolemId asi); /** get arithmetic skolem application * * By default, this returns the term f( n ), where f is the Skolem function @@ -872,7 +871,7 @@ private: * If the option arithNoPartialFun is enabled, this returns f, where f is * the Skolem constant for the identifier asi. */ - Node getArithSkolemApp(LogicRequest& logicRequest, Node n, ArithSkolemId asi); + Node getArithSkolemApp(Node n, ArithSkolemId asi); /** * Maps for Skolems for to-integer, real/integer div-by-k, and inverse diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 94fc1e34c..32791415e 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -194,7 +194,8 @@ void TheoryBV::finishInit() tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM); } -Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { +Node TheoryBV::expandDefinition(Node node) +{ Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl; switch (node.getKind()) { @@ -221,7 +222,6 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { Node divByZero = getBVDivByZero(node.getKind(), width); Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); - logicRequest.widenLogic(THEORY_UF); return node; } break; @@ -234,7 +234,6 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { Unreachable(); } - void TheoryBV::preRegisterTerm(TNode node) { d_calledPreregister = true; Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index bc54a09e7..7f88d8388 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -79,7 +79,7 @@ public: void finishInit() override; - Node expandDefinition(LogicRequest& logicRequest, Node node) override; + Node expandDefinition(Node node) override; void preRegisterTerm(TNode n) override; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index b3244fe91..9c8e9e2fa 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -558,7 +558,8 @@ void TheoryDatatypes::finishInit() { } } -Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { +Node TheoryDatatypes::expandDefinition(Node n) +{ NodeManager* nm = NodeManager::currentNM(); switch (n.getKind()) { diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index cc54241d0..c6ffb8907 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -302,7 +302,7 @@ private: bool needsCheckLastEffort() override; void preRegisterTerm(TNode n) override; void finishInit() override; - Node expandDefinition(LogicRequest& logicRequest, Node n) override; + Node expandDefinition(Node n) override; Node ppRewrite(TNode n) override; void presolve() override; void addSharedTerm(TNode t) override; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index b028184cd..68f3ad35a 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -318,17 +318,6 @@ Node TheoryFp::toRealUF(Node node) { return nm->mkNode(kind::APPLY_UF, fun, node[0]); } -void TheoryFp::enableUF(LogicRequest &lr) -{ - if (!this->d_expansionRequested) { - // Needed for conversions to/from real and min/max - lr.widenLogic(THEORY_UF); - // THEORY_BV has to be enabled when the logic is set - this->d_expansionRequested = true; - } - return; -} - Node TheoryFp::abstractRealToFloat(Node node) { Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL); @@ -393,7 +382,7 @@ Node TheoryFp::abstractFloatToReal(Node node) return uf; } -Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) +Node TheoryFp::expandDefinition(Node node) { Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node << std::endl; @@ -404,17 +393,14 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) res = removeToFPGeneric::removeToFPGeneric(node); } else if (node.getKind() == kind::FLOATINGPOINT_MIN) { - enableUF(lr); res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MIN_TOTAL, node[0], node[1], minUF(node)); } else if (node.getKind() == kind::FLOATINGPOINT_MAX) { - enableUF(lr); res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MAX_TOTAL, node[0], node[1], maxUF(node)); } else if (node.getKind() == kind::FLOATINGPOINT_TO_UBV) { - enableUF(lr); FloatingPointToUBV info = node.getOperator().getConst(); FloatingPointToUBVTotal newInfo(info); @@ -424,7 +410,6 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) toUBVUF(node)); } else if (node.getKind() == kind::FLOATINGPOINT_TO_SBV) { - enableUF(lr); FloatingPointToSBV info = node.getOperator().getConst(); FloatingPointToSBVTotal newInfo(info); @@ -434,7 +419,6 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) toSBVUF(node)); } else if (node.getKind() == kind::FLOATINGPOINT_TO_REAL) { - enableUF(lr); res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL, node[0], toRealUF(node)); @@ -442,13 +426,6 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) // Do nothing } - // We will need to enable UF to abstract these in ppRewrite - if (res.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL - || res.getKind() == kind::FLOATINGPOINT_TO_FP_REAL) - { - enableUF(lr); - } - if (res != node) { Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node << " rewritten to " << res << std::endl; diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index ae4a2a1cb..de629b000 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -41,7 +41,7 @@ class TheoryFp : public Theory { TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } - Node expandDefinition(LogicRequest& lr, Node node) override; + Node expandDefinition(Node node) override; void preRegisterTerm(TNode node) override; void addSharedTerm(TNode node) override; @@ -105,9 +105,6 @@ class TheoryFp : public Theory { context::CDO d_conflict; context::CDO d_conflictNode; - /** Uninterpretted functions for partially defined functions. **/ - void enableUF(LogicRequest& lr); - typedef context::CDHashMap ComparisonUFMap; diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index f4b265d98..8430987f2 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -95,7 +95,8 @@ void TheorySets::preRegisterTerm(TNode node) { d_internal->preRegisterTerm(node); } -Node TheorySets::expandDefinition(LogicRequest &logicRequest, Node n) { +Node TheorySets::expandDefinition(Node n) +{ Kind nk = n.getKind(); if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE || nk == COMPREHENSION) @@ -118,7 +119,7 @@ Node TheorySets::expandDefinition(LogicRequest &logicRequest, Node n) { throw LogicException(ss.str()); } } - return d_internal->expandDefinition(logicRequest, n); + return d_internal->expandDefinition(n); } Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 5fc1a61a3..1bb515cc6 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -55,7 +55,7 @@ class TheorySets : public Theory Node getModelValue(TNode) override; std::string identify() const override { return "THEORY_SETS"; } void preRegisterTerm(TNode node) override; - Node expandDefinition(LogicRequest& logicRequest, Node n) override; + Node expandDefinition(Node n) override; PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; void presolve() override; void propagate(Effort) override; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index b949be76c..e3db6887b 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1485,7 +1485,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) } } -Node TheorySetsPrivate::expandDefinition(LogicRequest& logicRequest, Node n) +Node TheorySetsPrivate::expandDefinition(Node n) { Debug("sets-proc") << "expandDefinition : " << n << std::endl; return n; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index ab9071793..84cea99a1 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -209,7 +209,7 @@ class TheorySetsPrivate { * Another option to fix this is to make TheoryModel::getValue more general * so that it makes theory-specific calls to evaluate interpreted symbols. */ - Node expandDefinition(LogicRequest &logicRequest, Node n); + Node expandDefinition(Node n); Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index da8c3583d..609822fe1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -640,7 +640,8 @@ void TheoryStrings::preRegisterTerm(TNode n) { } } -Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { +Node TheoryStrings::expandDefinition(Node node) +{ Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl; if (node.getKind() == STRING_FROM_CODE) diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 84e0a0a00..453e4eca9 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -293,7 +293,7 @@ private: /** preregister term */ void preRegisterTerm(TNode n) override; /** Expand definition */ - Node expandDefinition(LogicRequest& logicRequest, Node n) override; + Node expandDefinition(Node n) override; /** Check at effort e */ void check(Effort e) override; /** needs check last effort */ diff --git a/src/theory/theory.h b/src/theory/theory.h index a6751e1ec..c777f164f 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -424,22 +424,21 @@ public: virtual void finishInit() { } /** - * Some theories have kinds that are effectively definitions and - * should be expanded before they are handled. Definitions allow - * a much wider range of actions than the normal forms given by the - * rewriter; they can enable other theories and create new terms. - * However no assumptions can be made about subterms having been - * expanded or rewritten. Where possible rewrite rules should be - * used, definitions should only be used when rewrites are not - * possible, for example in handling under-specified operations - * using partially defined functions. + * Some theories have kinds that are effectively definitions and should be + * expanded before they are handled. Definitions allow a much wider range of + * actions than the normal forms given by the rewriter. However no + * assumptions can be made about subterms having been expanded or rewritten. + * Where possible rewrite rules should be used, definitions should only be + * used when rewrites are not possible, for example in handling + * under-specified operations using partially defined functions. * * Some theories like sets use expandDefinition as a "context * independent preRegisterTerm". This is required for cases where * a theory wants to be notified about a term before preprocessing * and simplification but doesn't necessarily want to rewrite it. */ - virtual Node expandDefinition(LogicRequest &logicRequest, Node node) { + virtual Node expandDefinition(Node node) + { // by default, do nothing return node; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 809ef5139..9c631ca60 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -587,7 +587,7 @@ class TheoryEngine { * @param assertion the normalized assertion being sent * @param originalAssertion the actual assertion that was sent * @param toTheoryId the theory that is on the receiving end - * @param fromTheoryId the theory that sent the assertino + * @param fromTheoryId the theory that sent the assertion * @return true if a new assertion, false if theory already got it */ bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp index 260bec418..2a061b017 100644 --- a/src/theory/theory_id.cpp +++ b/src/theory/theory_id.cpp @@ -20,6 +20,7 @@ std::ostream& operator<<(std::ostream& out, TheoryId theoryId) case THEORY_FP: out << "THEORY_FP"; break; case THEORY_ARRAYS: out << "THEORY_ARRAYS"; break; case THEORY_DATATYPES: out << "THEORY_DATATYPES"; break; + case THEORY_SAT_SOLVER: out << "THEORY_SAT_SOLVER"; break; case THEORY_SEP: out << "THEORY_SEP"; break; case THEORY_SETS: out << "THEORY_SETS"; break; case THEORY_STRINGS: out << "THEORY_STRINGS"; break; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 3b42fa6a1..1098d42ce 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -201,7 +201,8 @@ unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) { return node.getKind()==kind::APPLY_UF ? 0 : 1; } -Node TheoryUF::expandDefinition(LogicRequest &logicRequest, Node node) { +Node TheoryUF::expandDefinition(Node node) +{ Trace("uf-exp-def") << "TheoryUF::expandDefinition: expanding definition : " << node << std::endl; if( node.getKind()==kind::HO_APPLY ){ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 50b7a65cb..8627eb3f0 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -195,7 +195,7 @@ private: void finishInit() override; void check(Effort) override; - Node expandDefinition(LogicRequest& logicRequest, Node node) override; + Node expandDefinition(Node node) override; void preRegisterTerm(TNode term) override; Node explain(TNode n) override; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1f3d4f623..649178f91 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -582,6 +582,8 @@ set(regress_0_tests regress0/nl/issue3719.smt2 regress0/nl/issue3729-cm-solved-tf.smt2 regress0/nl/issue3959.smt2 + regress0/nl/issue3971.smt2 + regress0/nl/issue3991.smt2 regress0/nl/issue4007-rint-uf.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 diff --git a/test/regress/regress0/nl/issue3971.smt2 b/test/regress/regress0/nl/issue3971.smt2 new file mode 100644 index 000000000..93d370659 --- /dev/null +++ b/test/regress/regress0/nl/issue3971.smt2 @@ -0,0 +1,145 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +(set-logic QF_NIA) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const i4 Int) +(declare-const i5 Int) +(declare-const i6 Int) +(declare-const i7 Int) +(declare-const i8 Int) +(declare-const i9 Int) +(declare-const i12 Int) +(declare-const i13 Int) +(declare-const i14 Int) +(declare-const v4 Bool) +(assert (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6)))) +(declare-const v5 Bool) +(assert v1) +(declare-const i15 Int) +(declare-const v6 Bool) +(assert (distinct v5 (<= i8 i15))) +(declare-const i16 Int) +(assert v0) +(declare-const i17 Int) +(assert (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) +(declare-const i18 Int) +(declare-const v7 Bool) +(assert (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6)) +(declare-const v8 Bool) +(declare-const v9 Bool) +(assert (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) +(assert (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) +(assert (=> v4 (<= i13 i6))) +(declare-const v10 Bool) +(declare-const v11 Bool) +(assert v9) +(check-sat) +(assert (> (abs i7) i4)) +(assert v2) +(declare-const v12 Bool) +(assert (distinct v5 (<= i8 i15))) +(declare-const i19 Int) +(assert (xor (not (< (div i4 i8) 79)) (> (- 888) i15) (distinct i6 i12) (distinct i6 i12) (= (or v1 v3 v2) v1) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) v10)) +(check-sat) +(declare-const v13 Bool) +(push 1) +(assert (< i9 i8)) +(assert (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8)) +(push 1) +(push 1) +(declare-const v14 Bool) +(assert v7) +(assert v10) +(declare-const v15 Bool) +(declare-const v16 Bool) +(declare-const i20 Int) +(assert (or v1 v3 v2)) +(declare-const i21 Int) +(declare-const v17 Bool) +(assert (=> (> i6 (abs 79)) (or (= (- i8) 36) v6 v1))) +(declare-const v18 Bool) +(assert (distinct i6 i12)) +(declare-const v19 Bool) +(assert (< i9 i8)) +(declare-const v20 Bool) +(assert (= v16 (>= i19 (abs i14)) (= (or (= (- i8) 36) v6 v1) (distinct i6 i12) (> 546 i8) (> 546 i8) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) (> i6 (abs 79)) v11 (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) (<= i13 i6))) +(declare-const v21 Bool) +(declare-const v22 Bool) +(assert (> 79 34)) +(declare-const i22 Int) +(assert v9) +(declare-const i23 Int) +(declare-const v23 Bool) +(declare-const v24 Bool) +(declare-const i24 Int) +(pop 1) +(declare-const i25 Int) +(assert (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6)))) +(declare-const v25 Bool) +(pop 1) +(declare-const v26 Bool) +(declare-const i26 Int) +(declare-const i27 Int) +(assert (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1)) +(push 1) +(assert (and (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8) (>= i14 i19) (> (abs i7) i4))) +(declare-const v27 Bool) +(declare-const v28 Bool) +(declare-const v29 Bool) +(declare-const i28 Int) +(assert (distinct v5 (<= i8 i15))) +(assert (xor (> (- 888) i15) v3 (< i9 i8) (=> v4 (<= i13 i6)) (>= 162 43) (and (>= 162 43) (distinct 623 752) (= i15 960)) (and (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8) (>= i14 i19) (> (abs i7) i4)))) +(assert (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) +(declare-const v30 Bool) +(assert (or (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) v6 (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (>= 162 43) v30 (< (div i4 i8) 79) v2 (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6))) +(assert (= (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) v28 v28)) +(declare-const v31 Bool) +(assert (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1)) +(declare-const v32 Bool) +(pop 1) +(declare-const i29 Int) +(assert (xor v2 v2 v3 v0 v0 v2 v3 v1 v2)) +(declare-const v33 Bool) +(assert v9) +(push 1) +(declare-const v34 Bool) +(assert (or (>= 162 43) (>= i14 i19) (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (< (div i4 i8) 79) (< i6 (div i4 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (or (not (< (div i4 i8) 79)) (> (abs i7) i4) (= (or (= (- i8) 36) v6 v1) (distinct i6 i12) (> 546 i8) (> 546 i8) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) (> i6 (abs 79)) v11 (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (< i9 i8) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) v5)) +(declare-const i30 Int) +(declare-const v35 Bool) +(push 1) +(assert (and (>= 162 43) (distinct 623 752) (= i15 960))) +(declare-const v36 Bool) +(assert (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6)))) +(push 1) +(declare-const v37 Bool) +(declare-const v38 Bool) +(assert (distinct (= v3 v4 (<= i13 i6) v0 v10 v6) (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (> 546 i8) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (< i6 (div i4 i8)) (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (< (div i4 i8) 79))) +(assert (and (= v3 v4 (<= i13 i6) v0 v10 v6) (>= (abs 969) (* i6 162 i4 i4)))) +(assert v0) +(assert (<= 12 i4)) +(check-sat) +(assert (distinct (>= (abs 969) (* i6 162 i4 i4)) (xor (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (< (div i4 i8) 79) v11 (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) v4 (> 546 i8) (> i6 (abs 79))))) +(assert (=> (or (= (- i8) 36) v6 v1) (distinct v5 (<= i8 i15)))) +(declare-const v39 Bool) +(push 1) +(declare-const v40 Bool) +(declare-const v41 Bool) +(declare-const v42 Bool) +(check-sat) +(assert (or (= (- i8) 36) v6 v1)) +(assert (=> (=> v4 (<= i13 i6)) (< i6 (div i4 i8)))) +(pop 1) +(declare-const v43 Bool) +(pop 1) +(assert (or v1 v3 v2)) +(push 1) +(assert (not (> (abs i7) i4))) +(check-sat) +(exit) diff --git a/test/regress/regress0/nl/issue3991.smt2 b/test/regress/regress0/nl/issue3991.smt2 new file mode 100644 index 000000000..c006b2885 --- /dev/null +++ b/test/regress/regress0/nl/issue3991.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --incremental --check-unsat-cores +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +(set-logic QF_NIA) +(declare-const i7 Int) +(check-sat) +(declare-const v18 Bool) +(assert (and (= i7 93) (or (> 19 i7) v18) v18)) +(check-sat) +(assert (> 19 i7)) +(assert (> (div i7 0) 0)) +(check-sat)