Simplification is leftover from the sine symmetry heuristic, now the mapping from terms to what purifies them is injective.
Also makes the mapping context-dependent.
It also ensures that we keep model values for purification arguments. Fixes #8160.
namespace nl {
namespace transcendental {
-struct TranscendentalState;
+class TranscendentalState;
/** Transcendental solver class
*
if (d_tf_initial_refine.find(t) == d_tf_initial_refine.end())
{
d_tf_initial_refine[t] = true;
- Node symn = nm->mkNode(Kind::SINE,
- nm->mkNode(Kind::MULT, d_data->d_neg_one, t[0]));
- symn = rewrite(symn);
- // Can assume it is its own master since phase is split over 0,
- // hence -pi <= t[0] <= pi implies -pi <= -t[0] <= pi.
- d_data->d_trMaster[symn] = symn;
- d_data->d_trSlaves[symn].insert(symn);
- Assert(d_data->d_trSlaves.find(t) != d_data->d_trSlaves.end());
-
+ Assert(d_data->isPurified(t));
{
// sine bounds: -1 <= sin(t) <= 1
Node lem = nm->mkNode(Kind::AND,
for (const Node& a : needsMaster)
{
// should not have processed this already
- Assert(d_tstate.d_trMaster.find(a) == d_tstate.d_trMaster.end());
+ Assert(d_tstate.d_trPurify.find(a) == d_tstate.d_trPurify.end());
Kind k = a.getKind();
Assert(k == Kind::SINE || k == Kind::EXPONENTIAL);
Node y = sm->mkSkolemFunction(
SkolemFunId::TRANSCENDENTAL_PURIFY_ARG, nm->realType(), a);
Node new_a = nm->mkNode(k, y);
- d_tstate.d_trSlaves[new_a].insert(new_a);
- d_tstate.d_trSlaves[new_a].insert(a);
- d_tstate.d_trMaster[a] = new_a;
- d_tstate.d_trMaster[new_a] = new_a;
+ Assert(d_tstate.d_trPurify.find(new_a) == d_tstate.d_trPurify.end());
+ Assert(d_tstate.d_trPurifies.find(new_a) == d_tstate.d_trPurifies.end());
+ d_tstate.d_trPurify[a] = new_a;
+ d_tstate.d_trPurify[new_a] = new_a;
+ d_tstate.d_trPurifies[new_a] = a;
+ d_tstate.d_trPurifyVars.insert(y);
switch (k)
{
case Kind::SINE: d_sineSlv.doPhaseShift(a, new_a, y); break;
std::vector<Node>& assertions)
{
Subs subs;
- for (const auto& sub : d_tstate.d_trMaster)
+ for (const auto& sub : d_tstate.d_trPurify)
{
subs.add(sub.first, sub.second);
}
// for each function in the congruence classe
for (const Node& ctf : d_tstate.d_funcCongClass[tf])
{
- // each term in congruence classes should be master terms
- Assert(d_tstate.d_trSlaves.find(ctf) != d_tstate.d_trSlaves.end());
- // we set the bounds for each slave of tf
- for (const Node& stf : d_tstate.d_trSlaves[ctf])
+ std::vector<Node> mset{ctf};
+ // if this purifies another term, we set a bound on the term it
+ // purifies as well
+ context::CDHashMap<Node, Node>::const_iterator itp =
+ d_tstate.d_trPurifies.find(ctf);
+ if (itp != d_tstate.d_trPurifies.end() && itp->second != ctf)
+ {
+ mset.push_back(itp->second);
+ }
+ for (const Node& stf : mset)
{
Trace("nl-ext-cm")
<< "...bound for " << stf << " : [" << bounds.first << ", "
{
NodeManager* nm = NodeManager::currentNM();
Kind k = tf.getKind();
- // this should only be run on master applications
- Assert(d_tstate.d_trSlaves.find(tf) != d_tstate.d_trSlaves.end());
+ // this should only be run on purified applications
+ Assert(d_tstate.isPurified(tf));
// Figure 3 : c
Node c = d_tstate.d_model.computeAbstractModelValue(tf[0]);
// skip integer variables
if (am.first.getType().isInteger())
{
+ Trace("nl-ext") << "...keep model value for integer " << am.first
+ << std::endl;
+ continue;
+ }
+ // cannot erase values for purification arguments
+ if (d_tstate.d_trPurifyVars.find(am.first) != d_tstate.d_trPurifyVars.end())
+ {
+ Trace("nl-ext") << "...keep model value for purification variable "
+ << am.first << std::endl;
continue;
}
Node r = d_astate.getRepresentative(am.first);
TranscendentalState::TranscendentalState(Env& env,
InferenceManager& im,
NlModel& model)
- : EnvObj(env), d_im(im), d_model(model)
+ : EnvObj(env),
+ d_im(im),
+ d_model(model),
+ d_trPurify(userContext()),
+ d_trPurifies(userContext()),
+ d_trPurifyVars(userContext())
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
void TranscendentalState::init(const std::vector<Node>& xts,
- std::vector<Node>& needsMaster)
+ std::vector<Node>& needsPurify)
{
d_funcCongClass.clear();
d_funcMap.clear();
bool needPi = false;
// for computing congruence
std::map<Kind, ArgTrie> argTrie;
+ NodeMap::const_iterator itp;
for (std::size_t i = 0, xsize = xts.size(); i < xsize; ++i)
{
// Ignore if it is not a transcendental
Node a = xts[i];
Kind ak = a.getKind();
bool consider = true;
- // if we've already computed master for a
- if (d_trMaster.find(a) != d_trMaster.end())
+ // if we've already assigned a purified term
+ itp = d_trPurify.find(a);
+ if (itp != d_trPurify.end())
{
- // a master has at least one slave
- consider = (d_trSlaves.find(a) != d_trSlaves.end());
+ consider = itp->second == a;
}
else
{
}
if (!consider)
{
- // wait to assign a master below
- needsMaster.push_back(a);
+ // must assign a purified term
+ needsPurify.push_back(a);
}
else
{
- d_trMaster[a] = a;
- d_trSlaves[a].insert(a);
+ // assume own purified
+ d_trPurify[a] = a;
+ d_trPurifies[a] = a;
}
}
if (ak == Kind::EXPONENTIAL || ak == Kind::SINE)
}
}
+bool TranscendentalState::isPurified(TNode n) const
+{
+ return d_trPurifies.find(n) != d_trPurifies.end();
+}
+
} // namespace transcendental
} // namespace nl
} // namespace arith
#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
#include "expr/node.h"
#include "proof/proof_set.h"
#include "smt/env.h"
* This includes common lookups and caches as well as generic utilities for
* secant plane lemmas and taylor approximations.
*/
-struct TranscendentalState : protected EnvObj
+class TranscendentalState : protected EnvObj
{
+ using NodeMap = context::CDHashMap<Node, Node>;
+ using NodeSet = context::CDHashSet<Node>;
+
+ public:
TranscendentalState(Env& env, InferenceManager& im, NlModel& model);
/**
*
* This call may add lemmas to lems based on registering term
* information (for example to ensure congruence of terms).
- * It puts terms that need to be treated further as a master term on their own
- * (for example purification of sine terms) into needsMaster.
+ * It puts terms that need to be treated further as a purified term on their
+ * own (for example purification of sine terms) into needsPurify.
*/
- void init(const std::vector<Node>& xts, std::vector<Node>& needsMaster);
+ void init(const std::vector<Node>& xts, std::vector<Node>& needsPurify);
/**
* Checks for terms that are congruent but disequal to a.
Convexity convexity,
unsigned d,
unsigned actual_d);
+ /**
+ * Is term t purified? (See d_trPurify below).
+ */
+ bool isPurified(TNode n) const;
Node d_true;
Node d_false;
/**
* Some transcendental functions f(t) are "purified", e.g. we add
* t = y ^ f(t) = f(y) where y is a fresh variable. Those that are not
- * purified we call "master terms".
+ * purified we call "purified terms".
*
- * The maps below maintain a master/slave relationship over
- * transcendental functions (SINE, EXPONENTIAL, PI), where above
- * f(y) is the master of itself and of f(t).
+ * The maps below maps transcendental function applications (SINE,
+ * EXPONENTIAL, PI) to their purified version, where above
+ * f(y) is the purified version of itself and of f(t).
*
* This is used for ensuring that the argument y of SINE we process is on
* the interval [-pi .. pi], and that exponentials are not applied to
* arguments that contain transcendental functions.
*/
- std::map<Node, Node> d_trMaster;
- std::map<Node, std::unordered_set<Node>> d_trSlaves;
+ NodeMap d_trPurify;
+ /** inverse mapping of above, which is injective */
+ NodeMap d_trPurifies;
+ /** The set of purification variables we have introduced */
+ NodeSet d_trPurifyVars;
/** concavity region for transcendental functions
*
regress0/nl/nta/exp1-ub.smt2
regress0/nl/nta/issue7938-tf-model.smt2
regress0/nl/nta/issue8147-unc-model.smt2
+ regress0/nl/nta/issue8160-model-purify.smt2
regress0/nl/nta/real-pi.smt2
regress0/nl/nta/sin-sym.smt2
regress0/nl/nta/sqrt-simple.smt2
--- /dev/null
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun b (Int Int) Int)
+(declare-fun v () Real)
+(declare-fun a () Real)
+(assert (forall ((V Real)) (and (= 0 (b 0 0)) (forall ((V Real)) (= 0.0 (sin v))) (exists ((V Real)) (= 1.0 (* a a))))))
+(check-sat)
projects / cvc5.git / commitdiff