This makes it so that we don't assign concrete values to equivalence classes with transcendental functions.
It also removes some unused infrastructure.
void CadSolver::addToModel(TNode var, TNode value) const
{
Trace("nl-cad") << "-> " << var << " = " << value << std::endl;
- if (value.getType().isRealOrInt())
- {
- d_model.addSubstitution(var, value);
- }
- else
- {
- d_model.addWitness(var, value);
- }
+ Assert(value.getType().isRealOrInt());
+ d_model.addSubstitution(var, value);
}
} // namespace nl
d_used_approx = false;
d_check_model_solved.clear();
d_check_model_bounds.clear();
- d_check_model_witnesses.clear();
d_substitutions.clear();
}
return false;
}
}
- Assert(d_check_model_witnesses.find(v) == d_check_model_witnesses.end())
- << "We tried to add a substitution where we already had a witness term."
- << std::endl;
Subs tmp;
tmp.add(v, s);
for (auto& sub : d_substitutions.d_subs)
return true;
}
-bool NlModel::addWitness(TNode v, TNode w)
-{
- Trace("nl-ext-model") << "* check model witness : " << v << " -> " << w
- << std::endl;
- // should not set a witness for a value that is already set
- if (d_substitutions.contains(v))
- {
- Trace("nl-ext-model") << "...ERROR: setting witness for variable that "
- "already has a constant value."
- << std::endl;
- Assert(false);
- return false;
- }
- d_check_model_witnesses.emplace(v, w);
- return true;
-}
-
void NlModel::setUsedApproximate() { d_used_approx = true; }
bool NlModel::usedApproximate() const { return d_used_approx; }
}
else
{
- Assert(d_check_model_witnesses.find(vc)
- == d_check_model_witnesses.end())
- << "No variable should be assigned a witness term if we get "
- "here. "
- << vc << " is, though." << std::endl;
Trace("nl-ext-cms-debug") << std::endl;
Trace("nl-ext-cms")
<< " failed due to unknown bound for " << vc << std::endl;
void NlModel::getModelValueRepair(
std::map<Node, Node>& arithModel,
std::map<Node, std::pair<Node, Node>>& approximations,
- std::map<Node, Node>& witnesses,
bool witnessToValue)
{
Trace("nl-model") << "NlModel::getModelValueRepair:" << std::endl;
Trace("nl-model") << v << " exact approximation is " << l << std::endl;
}
}
- for (const auto& vw : d_check_model_witnesses)
- {
- Trace("nl-model") << vw.first << " witness is " << vw.second << std::endl;
- witnesses.emplace(vw.first, vw.second);
- }
// Also record the exact values we used. An exact value can be seen as a
// special kind approximation of the form (witness x. x = exact_value).
// Notice that the above term gets rewritten such that the choice function
{
return true;
}
- if (d_check_model_witnesses.find(v) != d_check_model_witnesses.end())
- {
- return true;
- }
return (d_substitutions.contains(v));
}
* bounds.
*/
bool addBound(TNode v, TNode l, TNode u);
- /**
- * Adds a model witness v -> w to the underlying theory model.
- * The witness should only contain a single variable v and evaluate to true
- * for exactly one value of v. The variable v is then (implicitly,
- * declaratively) assigned to this single value that satisfies the witness w.
- */
- bool addWitness(TNode v, TNode w);
/**
* Checks the current model based on solving for equalities, and using error
* bounds on the Taylor approximation.
* 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; the mapping
- * witnesses is filled with witness terms that are satisfied by a single
- * value.
+ * v and w is a witness point that satisfies this predicate.
*/
void getModelValueRepair(
std::map<Node, Node>& arithModel,
std::map<Node, std::pair<Node, Node>>& approximations,
- std::map<Node, Node>& witnesses,
bool witnessToValue);
private:
* involves approximations of square roots.
*/
std::map<Node, std::pair<Node, Node>> d_check_model_bounds;
- /**
- * witnesses for check model
- *
- * Stores witnesses for vatiables that define implicit variable assignments.
- * For some variable v, we map to a formulas that is true for exactly one
- * value of v.
- */
- std::map<Node, Node> d_check_model_witnesses;
/**
* The map from literals that our model construction solved, to the variable
* that was solved for. Examples of such literals are:
d_extTheoryCb(state.getEqualityEngine()),
d_extTheory(env, d_extTheoryCb, d_im),
d_model(env),
- d_trSlv(d_env, d_im, d_model),
+ d_trSlv(d_env, d_astate, d_im, d_model),
d_extState(d_im, d_model, d_env),
d_factoringSlv(d_env, &d_extState),
d_monomialBoundsSlv(d_env, &d_extState),
{
Trace("nl-ext") << "interceptModel: do model repair" << std::endl;
d_approximations.clear();
- d_witnesses.clear();
// modify the model values
d_model.getModelValueRepair(arithModel,
d_approximations,
- d_witnesses,
options().smt.modelWitnessValue);
for (auto& am : arithModel)
{
}
}
}
+ // must post-process model with transcendental solver, to ensure we don't
+ // assign values for equivalence classes with transcendental function
+ // applications
+ d_trSlv.postProcessModel(arithModel, termSet);
}
Node NonlinearExtension::getModelValue(TNode var) const
}
return Node::null();
}
- if (auto it = d_witnesses.find(var); it != d_witnesses.end())
- {
- return it->second;
- }
return Node::null();
}
}
return true;
}
- if (auto it = d_witnesses.find(var); it != d_witnesses.end())
- {
- tm->recordApproximation(var, it->second);
- return true;
- }
return false;
}
* NlModel::getModelValueRepair.
*/
std::map<Node, std::pair<Node, Node>> d_approximations;
- /**
- * The witnesses computed during collectModelInfo. For details, see
- * NlModel::getModelValueRepair.
- */
- std::map<Node, Node> d_witnesses;
}; /* class NonlinearExtension */
} // namespace nl
#include "expr/skolem_manager.h"
#include "options/arith_options.h"
#include "theory/arith/arith_msum.h"
+#include "theory/arith/arith_state.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/inference_manager.h"
#include "theory/arith/nl/nl_model.h"
namespace transcendental {
TranscendentalSolver::TranscendentalSolver(Env& env,
+ ArithState& state,
InferenceManager& im,
NlModel& m)
: EnvObj(env),
+ d_astate(state),
d_tstate(env, im, m),
d_expSlv(env, &d_tstate),
d_sineSlv(env, &d_tstate)
return 0;
}
+void TranscendentalSolver::postProcessModel(std::map<Node, Node>& arithModel,
+ const std::set<Node>& termSet)
+{
+ Trace("nl-ext") << "TranscendentalSolver::postProcessModel" << std::endl;
+ std::unordered_set<Node> trReps;
+ for (const Node& n : termSet)
+ {
+ if (isTranscendentalKind(n.getKind()))
+ {
+ Node r = d_astate.getRepresentative(n);
+ trReps.insert(r);
+ }
+ }
+ if (trReps.empty())
+ {
+ Trace("nl-ext") << "...no transcendental functions" << std::endl;
+ return;
+ }
+ std::vector<Node> rmFromModel;
+ for (auto& am : arithModel)
+ {
+ Node r = d_astate.getRepresentative(am.first);
+ if (trReps.find(r) != trReps.end())
+ {
+ Trace("nl-ext") << "...erase value for " << am.first
+ << ", since approximate" << std::endl;
+ rmFromModel.push_back(am.first);
+ }
+ else
+ {
+ Trace("nl-ext") << "...keep model value for " << am.first << std::endl;
+ }
+ }
+ for (const Node& n : rmFromModel)
+ {
+ arithModel.erase(n);
+ }
+}
+
} // namespace transcendental
} // namespace nl
} // namespace arith
namespace theory {
namespace arith {
+class ArithState;
class InferenceManager;
namespace nl {
class TranscendentalSolver : protected EnvObj
{
public:
- TranscendentalSolver(Env& env, InferenceManager& im, NlModel& m);
+ TranscendentalSolver(Env& env,
+ ArithState& state,
+ InferenceManager& im,
+ NlModel& m);
~TranscendentalSolver();
/** init last call
*/
void checkTranscendentalTangentPlanes();
+ /**
+ * Post-process model. This ensures that the domain of arithModel does not
+ * contain terms that are equal to any transcendental function applications,
+ * as their values cannot be properly represented in the model.
+ */
+ void postProcessModel(std::map<Node, Node>& arithModel,
+ const std::set<Node>& termSet);
+
private:
/** check transcendental function refinement for tf
*
*/
int regionToConcavity(Kind k, int region);
+ /** A reference to the arithmetic state object */
+ ArithState& d_astate;
/** taylor degree
*
* Indicates that the degree of the polynomials in the Taylor approximation of
d_nonlinearExtension(nullptr),
d_opElim(d_env),
d_arithPreproc(env, d_astate, d_im, d_pnm, d_opElim),
- d_rewriter(d_opElim)
+ d_rewriter(d_opElim),
+ d_arithModelCacheSet(false)
{
// currently a cyclic dependency to TheoryArithPrivate
d_astate.setParent(d_internal);
if (Theory::fullEffort(level))
{
d_arithModelCache.clear();
+ d_arithModelCacheSet = false;
std::set<Node> termSet;
if (d_nonlinearExtension != nullptr)
{
void TheoryArith::updateModelCache(std::set<Node>& termSet)
{
- if (d_arithModelCache.empty())
+ if (!d_arithModelCacheSet)
{
+ d_arithModelCacheSet = true;
collectAssertedTerms(termSet);
d_internal->collectModelValues(termSet, d_arithModelCache);
}
}
void TheoryArith::updateModelCache(const std::set<Node>& termSet)
{
- if (d_arithModelCache.empty())
+ if (!d_arithModelCacheSet)
{
+ d_arithModelCacheSet = true;
d_internal->collectModelValues(termSet, d_arithModelCache);
}
}
* used to augment the TheoryModel.
*/
std::map<Node, Node> d_arithModelCache;
+ /** Is the above map computed? */
+ bool d_arithModelCacheSet;
};/* class TheoryArith */
-; COMMAND-LINE: --check-model
-; EXPECT: (error "Cannot run check-model on a model with approximate values.")
-; EXIT: 1
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic QF_UFNRAT)
(set-option :produce-models true)
(declare-fun b (Real) Real)
-; COMMAND-LINE: --check-models
-; EXPECT: (error "Cannot run check-model on a model with approximate values.")
-; EXIT: 1
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic QF_NRAT)
(set-option :re-elim-agg true)
(declare-fun r6 () Real)
(assert (= 0.0 (cos r6)))
-(check-sat)
\ No newline at end of file
+(check-sat)
projects / cvc5.git / commitdiff