This ensures that we explicitly mark x -> 0 as part of the arithmetic model coming from nonlinear for unconstrained variables x that nonlinear extension assumes to be 0.
This fixes #5348.
return d_model->getRepresentative(n);
}
-Node NlModel::getValueInternal(Node n) const
+Node NlModel::getValueInternal(Node n)
{
if (n.isConst())
{
AlwaysAssert(it->second.isConst());
return it->second;
}
- // It is unconstrained in the model, return 0.
+ // It is unconstrained in the model, return 0. We additionally add it
+ // to mapping from the linear solver. This ensures that if the nonlinear
+ // solver assumes that n = 0, then this assumption is recorded in the overall
+ // model.
+ d_arithVal[n] = d_zero;
return d_zero;
}
bool NlModel::checkModel(const std::vector<Node>& assertions,
unsigned d,
- std::vector<NlLemma>& lemmas,
- std::vector<Node>& gs)
+ std::vector<NlLemma>& lemmas)
{
Trace("nl-ext-cm-debug") << " solve for equalities..." << std::endl;
for (const Node& atom : assertions)
return false;
}
Trace("nl-ext-cm") << "...simple check succeeded!" << std::endl;
-
- // must assert and re-check if produce models is true
- if (options::produceModels())
- {
- NodeManager* nm = NodeManager::currentNM();
- // model guard whose semantics is "the model we constructed holds"
- Node mg = nm->mkSkolem("model", nm->booleanType());
- gs.push_back(mg);
- // assert the constructed model as assertions
- for (const std::pair<const Node, std::pair<Node, Node>> cb :
- d_check_model_bounds)
- {
- Node l = cb.second.first;
- Node u = cb.second.second;
- Node v = cb.first;
- Node pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v));
- pred = nm->mkNode(OR, mg.negate(), pred);
- lemmas.emplace_back(pred);
- }
- }
return true;
}
std::map<Node, Node>& witnesses)
{
Trace("nl-model") << "NlModel::getModelValueRepair:" << std::endl;
-
+ // If we extended the model with entries x -> 0 for unconstrained values,
+ // we first update the map to the extended one.
+ if (d_arithVal.size() > arithModel.size())
+ {
+ arithModel = d_arithVal;
+ }
// Record the approximations we used. This code calls the
// recordApproximation method of the model, which overrides the model
// values for variables that we solved for, using techniques specific to
*/
bool checkModel(const std::vector<Node>& assertions,
unsigned d,
- std::vector<NlLemma>& lemmas,
- std::vector<Node>& gs);
+ std::vector<NlLemma>& lemmas);
/**
* Set that we have used an approximation during this check. This flag is
* reset on a call to resetCheck. It is set when we use reasoning that
/** The current model */
TheoryModel* d_model;
/** Get the model value of n from the model object above */
- Node getValueInternal(Node n) const;
+ Node getValueInternal(Node n);
/** Does the equality engine of the model have term n? */
bool hasTerm(Node n) const;
/** Get the representative of n in the model */
Node d_null;
/**
* The values that the arithmetic theory solver assigned in the model. This
- * corresponds to exactly the set of equalities that TheoryArith is currently
- * sending to TheoryModel during collectModelInfo.
+ * corresponds to the set of equalities that linear solver (via TheoryArith)
+ * is currently sending to TheoryModel during collectModelValues, plus
+ * additional entries x -> 0 for variables that were unassigned by the linear
+ * solver.
*/
std::map<Node, Node> d_arithVal;
/**
return false_asserts;
}
-bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
- std::vector<Node>& gs)
+bool NonlinearExtension::checkModel(const std::vector<Node>& assertions)
{
Trace("nl-ext-cm") << "--- check-model ---" << std::endl;
Trace("nl-ext-cm") << "-----" << std::endl;
unsigned tdegree = d_trSlv.getTaylorDegree();
std::vector<NlLemma> lemmas;
- bool ret = d_model.checkModel(passertions, tdegree, lemmas, gs);
+ bool ret = d_model.checkModel(passertions, tdegree, lemmas);
for (const auto& al: lemmas)
{
d_im.addPendingArithLemma(al);
<< std::endl;
// check the model based on simple solving of equalities and using
// error bounds on the Taylor approximation of transcendental functions.
- std::vector<Node> gs;
- if (checkModel(assertions, gs))
+ if (checkModel(assertions))
{
complete_status = 1;
}
- for (const Node& mg : gs)
- {
- Node mgr = Rewriter::rewrite(mg);
- mgr = d_containing.getValuation().ensureLiteral(mgr);
- d_containing.getOutputChannel().requirePhase(mgr, true);
- d_builtModel = true;
- }
if (d_im.hasUsed())
{
d_im.clearWaitingLemmas();
d_containing.getOutputChannel().setIncomplete();
}
}
+ else
+ {
+ // we have built a model
+ d_builtModel = true;
+ }
d_im.clearWaitingLemmas();
} while (needsRecheck);
*
* For details, see Section 3 of Cimatti et al CADE 2017 under the heading
* "Detecting Satisfiable Formulas".
- *
- * The arguments lemmas and gs store the lemmas and guard literals to be sent
- * out on the output channel of TheoryArith as lemmas and calls to
- * ensureLiteral respectively.
*/
- bool checkModel(const std::vector<Node>& assertions,
- std::vector<Node>& gs);
+ bool checkModel(const std::vector<Node>& assertions);
//---------------------------end check model
/** compute relevant assertions */
void computeRelevantAssertions(const std::vector<Node>& assertions,
regress0/model-core.smt2
regress0/nl/coeff-sat.smt2
regress0/nl/ext-rew-aggr-test.smt2
+ regress0/nl/iand-no-init.smt2
regress0/nl/issue3003.smt2
regress0/nl/issue3407.smt2
regress0/nl/issue3411.smt2
regress1/quantifiers/quant-wf-int-ind.smt2
regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
regress1/quantifiers/recfact.cvc
- regress1/quantifiers/rel-trigger-unusable.smt2
regress1/quantifiers/repair-const-nterm.smt2
regress1/quantifiers/rew-to-0211-dd.smt2
regress1/quantifiers/ricart-agrawala6.smt2
regress1/quantifiers/macro-subtype-param.smt2
# times out with competition build:
regress1/quantifiers/model_6_1_bv.smt2
+ # timeout after changes to nonlinear on PR #5351
+ regress1/quantifiers/rel-trigger-unusable.smt2
# ajreynol: different error messages on production and debug:
regress1/quantifiers/subtype-param-unk.smt2
regress1/quantifiers/subtype-param.smt2
--- /dev/null
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun y () Int)
+(assert (= 0 ((_ iand 5) y 1)))
+(check-sat)
projects / cvc5.git / commitdiff