We now allow partial specifications. Recording approximations is arithmetic specific, and if necessary could be added as a post-processing analysis e.g. during check-model.
name = "none"
help = "(default) do not print declarations of uninterpreted elements in models."
-
-[[option]]
- name = "modelWitnessValue"
- category = "regular"
- long = "model-witness-value"
- type = "bool"
- default = "false"
- help = "in models, use a witness constant for choice functions"
-
[[option]]
name = "foreignTheoryRewrite"
category = "regular"
}
}
-void NlModel::getModelValueRepair(
- std::map<Node, Node>& arithModel,
- std::map<Node, std::pair<Node, Node>>& approximations,
- bool witnessToValue)
+void NlModel::getModelValueRepair(std::map<Node, Node>& arithModel)
{
Trace("nl-model") << "NlModel::getModelValueRepair:" << std::endl;
// If we extended the model with entries x -> 0 for unconstrained values,
// recordApproximation method of the model, which overrides the model
// values for variables that we solved for, using techniques specific to
// this class.
- NodeManager* nm = NodeManager::currentNM();
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 pred;
Node v = cb.first;
if (l != u)
{
- pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v));
- Trace("nl-model") << v << " approximated as " << pred << std::endl;
- Node witness;
- if (witnessToValue)
- {
- // witness is the midpoint
- witness = nm->mkNode(MULT,
- nm->mkConst(CONST_RATIONAL, Rational(1, 2)),
- nm->mkNode(ADD, l, u));
- witness = rewrite(witness);
- Trace("nl-model") << v << " witness is " << witness << std::endl;
- }
- approximations[v] = std::pair<Node, Node>(pred, witness);
+ Trace("nl-model") << v << " is in interval " << l << "..." << u
+ << std::endl;
}
else
{
* call to checkModel above.
*
* The mapping arithModel is updated by this method to map arithmetic terms v
- * to their (exact) value that was computed during checkModel; the mapping
- * approximations is updated to store approximate values in the form of a
- * pair (P, w), where P is a predicate that describes the possible values of
- * v and w is a witness point that satisfies this predicate.
+ * to their (exact) value that was computed during checkModel.
*/
- void getModelValueRepair(
- std::map<Node, Node>& arithModel,
- std::map<Node, std::pair<Node, Node>>& approximations,
- bool witnessToValue);
+ void getModelValueRepair(std::map<Node, Node>& arithModel);
private:
/** Cache for concrete model values */
if (res == Result::Sat::SAT)
{
Trace("nl-ext") << "interceptModel: do model repair" << std::endl;
- d_approximations.clear();
// modify the model values
- d_model.getModelValueRepair(arithModel,
- d_approximations,
- options().smt.modelWitnessValue);
- for (auto& am : arithModel)
- {
- Node val = getModelValue(am.first);
- if (!val.isNull())
- {
- am.second = val;
- }
- }
+ d_model.getModelValueRepair(arithModel);
}
// must post-process model with transcendental solver, to ensure we don't
// assign values for equivalence classes with transcendental function
d_trSlv.postProcessModel(arithModel, termSet);
}
-Node NonlinearExtension::getModelValue(TNode var) const
-{
- if (auto it = d_approximations.find(var); it != d_approximations.end())
- {
- if (it->second.second.isNull())
- {
- return it->second.first;
- }
- return Node::null();
- }
- return Node::null();
-}
-
-bool NonlinearExtension::assertModel(TheoryModel* tm, TNode var) const
-{
- if (auto it = d_approximations.find(var); it != d_approximations.end())
- {
- const auto& approx = it->second;
- if (approx.second.isNull())
- {
- tm->recordApproximation(var, approx.first);
- }
- else
- {
- tm->recordApproximation(var, approx.first, approx.second);
- }
- return true;
- }
- return false;
-}
-
Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet)
{
++(d_stats.d_mbrRuns);
void checkFullEffort(std::map<Node, Node>& arithModel,
const std::set<Node>& termSet);
- /**
- * Retrieve the model value for the given variable. It may be either an
- * arithmetic term or a witness.
- */
- Node getModelValue(TNode var) const;
- /**
- * Assert the model for the given variable to the theory model.
- */
- bool assertModel(TheoryModel* tm, TNode var) const;
-
/** Does this class need a call to check(...) at last call effort? */
bool hasNlTerms() const { return d_hasNlTerms; }
/** The strategy for the nonlinear extension. */
Strategy d_strategy;
-
- /**
- * The approximations computed during collectModelInfo. For details, see
- * NlModel::getModelValueRepair.
- */
- std::map<Node, std::pair<Node, Node>> d_approximations;
}; /* class NonlinearExtension */
} // namespace nl
{
continue;
}
- if (d_nonlinearExtension != nullptr)
- {
- if (d_nonlinearExtension->assertModel(m, p.first))
- {
- continue;
- }
- }
// maps to constant of comparable type
Assert(p.first.getType().isComparableTo(p.second.getType()));
if (m->assertEquality(p.first, p.second, true))
d_modelCache.clear();
d_sep_heap = Node::null();
d_sep_nil_eq = Node::null();
- d_approximations.clear();
- d_approx_list.clear();
d_reps.clear();
d_assignExcSet.clear();
d_aesMaster.clear();
return true;
}
-bool TheoryModel::hasApproximations() const { return !d_approx_list.empty(); }
-
-std::vector<std::pair<Node, Node> > TheoryModel::getApproximations() const
-{
- return d_approx_list;
-}
-
std::vector<Node> TheoryModel::getDomainElements(TypeNode tn) const
{
// must be an uninterpreted sort
return ret;
}
}
- // it might be approximate
- std::map<Node, Node>::const_iterator ita = d_approximations.find(n);
- if (ita != d_approximations.end())
- {
- // If the value of n is approximate based on predicate P(n), we return
- // witness z. P(z).
- Node v = nm->mkBoundVar(n.getType());
- Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
- Node answer = nm->mkNode(WITNESS, bvl, ita->second.substitute(n, v));
- d_modelCache[n] = answer;
- return answer;
- }
// must rewrite the term at this point
ret = rewrite(n);
// return the representative of the term in the equality engine, if it exists
return !d_assignExcSet.empty();
}
-void TheoryModel::recordApproximation(TNode n, TNode pred)
-{
- Trace("model-builder-debug")
- << "Record approximation : " << n << " satisfies the predicate " << pred
- << std::endl;
- Assert(d_approximations.find(n) == d_approximations.end());
- Assert(pred.getType().isBoolean());
- d_approximations[n] = pred;
- d_approx_list.push_back(std::pair<Node, Node>(n, pred));
- // model cache is invalid
- d_modelCache.clear();
-}
-void TheoryModel::recordApproximation(TNode n, TNode pred, Node witness)
-{
- Node predDisj = NodeManager::currentNM()->mkNode(OR, n.eqNode(witness), pred);
- recordApproximation(n, predDisj);
-}
bool TheoryModel::isUsingModelCore() const { return d_using_model_core; }
void TheoryModel::setUsingModelCore()
{
std::vector<Node>& eset);
/** have any assignment exclusion sets been created? */
bool hasAssignmentExclusionSets() const;
- /** record approximation
- *
- * This notifies this model that the value of n was approximated in this
- * model such that the predicate pred (involving n) holds. For example,
- * for transcendental functions, we may determine an error bound on the
- * value of a transcendental function, say c-e <= y <= c+e where
- * c and e are constants. We call this function with n set to sin( x ) and
- * pred set to c-e <= sin( x ) <= c+e.
- *
- * If recordApproximation is called at least once during the model
- * construction process, then check-model is not guaranteed to succeed.
- * However, there are cases where we can establish the input is satisfiable
- * without constructing an exact model. For example, if x=.77, sin(x)=.7, and
- * say we have computed c=.7 and e=.01 as an approximation in the above
- * example, then we may reason that the set of assertions { sin(x)>.6 } is
- * satisfiable, albiet without establishing an exact (irrational) value for
- * sin(x).
- *
- * This function is simply for bookkeeping, it does not affect the model
- * construction process.
- */
- void recordApproximation(TNode n, TNode pred);
- /**
- * Same as above, but with a witness constant. This ensures that the
- * approximation predicate is of the form (or (= n witness) pred). This
- * is useful if the user wants to know a possible concrete value in
- * the range of the predicate.
- */
- void recordApproximation(TNode n, TNode pred, Node witness);
/** set unevaluate/semi-evaluated kind
*
* This informs this model how it should interpret applications of terms with
bool getHeapModel(Node& h, Node& neq) const;
//---------------------------- end separation logic
- /** is the list of approximations non-empty? */
- bool hasApproximations() const;
- /** get approximations */
- std::vector<std::pair<Node, Node> > getApproximations() const;
/** get domain elements for uninterpreted sort t */
std::vector<Node> getDomainElements(TypeNode t) const;
/** get the representative set object */
std::string d_name;
/** equality engine containing all known equalities/disequalities */
eq::EqualityEngine* d_equalityEngine;
- /** approximations (see recordApproximation) */
- std::map<Node, Node> d_approximations;
- /** list of all approximations */
- std::vector<std::pair<Node, Node> > d_approx_list;
/** a set of kinds that are unevaluated */
std::unordered_set<Kind, kind::KindHashFunction> d_unevaluated_kinds;
/** a set of kinds that are semi-evaluated */
void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
{
- if (tm->hasApproximations())
- {
- // models with approximations may fail the assertions below
- return;
- }
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
std::map<Node, Node>::iterator itMap;
// Check that every term evaluates to its representative in the model
; SCRUBBER: sed -e 's/((x (_ real_algebraic_number .*/((x (_ real_algebraic_number/'
-; COMMAND-LINE: --produce-models --model-witness-value --no-check-models
+; COMMAND-LINE: --produce-models --no-check-models
; REQUIRES: poly
; EXPECT: sat
; EXPECT: ((x (_ real_algebraic_number
projects / cvc5.git / commitdiff