// get model bounds for all transcendental functions
Trace("nl-ext-cm-debug") << " get bounds for transcendental functions..."
<< std::endl;
- for (std::pair<const Kind, std::map<Node, Node> >& tfs : d_tf_rep_map)
+ for (std::pair<const Kind, std::vector<Node> >& tfs : d_f_map)
{
Kind k = tfs.first;
- for (std::pair<const Node, Node>& tfr : tfs.second)
+ for (const Node& tf : tfs.second)
{
- // Figure 3 : tf( x )
- Node tf = tfr.second;
+ // tf is Figure 3 : tf( x )
Node atf = computeModelValue(tf, 0);
if (k == PI)
{
return lemmas;
}
+/** An argument trie, for computing congruent terms */
+class ArgTrie
+{
+ public:
+ /** children of this node */
+ std::map<Node, ArgTrie> d_children;
+ /** the data of this node */
+ Node d_data;
+ /**
+ * Set d as the data on the node whose path is [args], return either d if
+ * that node has no data, or the data that already occurs there.
+ */
+ Node add(Node d, const std::vector<Node>& args)
+ {
+ ArgTrie* at = this;
+ for (const Node& a : args)
+ {
+ at = &(at->d_children[a]);
+ }
+ if (at->d_data.isNull())
+ {
+ at->d_data = d;
+ }
+ return at->d_data;
+ }
+};
+
int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
const std::vector<Node>& xts)
d_ci.clear();
d_ci_exp.clear();
d_ci_max.clear();
- d_tf_rep_map.clear();
+ d_f_map.clear();
d_tf_region.clear();
d_waiting_lemmas.clear();
std::map< Node, Node > mvarg_to_term;
std::vector<Node> tr_no_base;
bool needPi = false;
+ // for computing congruence
+ std::map<Kind, ArgTrie> argTrie;
for (unsigned i = 0, xsize = xts.size(); i < xsize; i++)
{
Node a = xts[i];
}
}
*/
- }else if( a.getNumChildren()==1 ){
+ }
+ else if (a.getNumChildren() > 0)
+ {
if (ak == SINE)
{
needPi = true;
// applied to a trancendental, purify.
if (isTranscendentalKind(ak))
{
- if ((ak == SINE && d_tr_is_base.find(a) == d_tr_is_base.end())
- || isTranscendentalKind(a[0].getKind()))
+ if (ak == SINE && d_tr_is_base.find(a) == d_tr_is_base.end())
{
consider = false;
+ }
+ else
+ {
+ for (const Node& ac : a)
+ {
+ if (isTranscendentalKind(ac.getKind()))
+ {
+ consider = false;
+ break;
+ }
+ }
+ }
+ if (!consider)
+ {
tr_no_base.push_back(a);
}
}
if( consider ){
- Node r = d_containing.getValuation().getModel()->getRepresentative(a[0]);
- std::map<Node, Node>::iterator itrm = d_tf_rep_map[ak].find(r);
- if (itrm != d_tf_rep_map[ak].end())
+ std::vector<Node> repList;
+ for (const Node& ac : a)
+ {
+ Node r =
+ d_containing.getValuation().getModel()->getRepresentative(a[0]);
+ repList.push_back(r);
+ }
+ Node aa = argTrie[ak].add(a, repList);
+ if (aa != a)
{
- //verify they have the same model value
- if( d_mv[1][a]!=d_mv[1][itrm->second] ){
- // if not, add congruence lemma
- Node cong_lemma = nm->mkNode(
- IMPLIES, a[0].eqNode(itrm->second[0]), a.eqNode(itrm->second));
+ // apply congruence to pairs of terms that are disequal and congruent
+ Assert(aa.getNumChildren() == a.getNumChildren());
+ if (d_mv[1][a] != d_mv[1][aa])
+ {
+ std::vector<Node> exp;
+ for (unsigned j = 0, size = a.getNumChildren(); j < size; j++)
+ {
+ exp.push_back(a[j].eqNode(aa[j]));
+ }
+ Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
+ Node cong_lemma = nm->mkNode(OR, expn.negate(), a.eqNode(aa));
lemmas.push_back( cong_lemma );
- //Assert( false );
}
- }else{
- d_tf_rep_map[ak][r] = a;
+ }
+ else
+ {
+ d_f_map[ak].push_back(a);
}
}
}
else if (ak == PI)
{
needPi = true;
- d_tf_rep_map[ak][a] = a;
+ d_f_map[ak].push_back(a);
}
else
{
{
Trace("nl-ext-mv") << "Arguments of trancendental functions : "
<< std::endl;
- for (std::map<Kind, std::map<Node, Node> >::iterator it =
- d_tf_rep_map.begin();
- it != d_tf_rep_map.end();
- ++it)
+ for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
{
- Kind k = it->first;
+ Kind k = tfl.first;
if (k == SINE || k == EXPONENTIAL)
{
- for (std::map<Node, Node>::iterator itt = it->second.begin();
- itt != it->second.end();
- ++itt)
+ for (const Node& tf : tfl.second)
{
- Node v = itt->second[0];
+ Node v = tf[0];
computeModelValue(v, 0);
computeModelValue(v, 1);
printModelValue("nl-ext-mv", v);
std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() {
std::vector< Node > lemmas;
Trace("nl-ext") << "Get initial refinement lemmas for transcendental functions..." << std::endl;
- for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){
- for( std::map< Node, Node >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
- Node t = itt->second;
+ for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+ {
+ Kind k = tfl.first;
+ for (const Node& t : tfl.second)
+ {
Assert( d_mv[1].find( t )!=d_mv[1].end() );
//initial refinements
if( d_tf_initial_refine.find( t )==d_tf_initial_refine.end() ){
d_tf_initial_refine[t] = true;
Node lem;
- if (it->first == SINE)
+ if (k == SINE)
{
Node symn = NodeManager::currentNM()->mkNode(
SINE, NodeManager::currentNM()->mkNode(MULT, d_neg_one, t[0]));
NodeManager::currentNM()->mkNode(
MINUS, d_pi_neg, t[0])))));
}
- else if (it->first == EXPONENTIAL)
+ else if (k == EXPONENTIAL)
{
// ( exp(x) > 0 ) ^ ( x=0 <=> exp( x ) = 1 ) ^ ( x < 0 <=> exp( x ) <
// 1 ) ^ ( x <= 0 V exp( x ) > x + 1 )
//sort arguments of all transcendentals
std::map< Kind, std::vector< Node > > sorted_tf_args;
std::map< Kind, std::map< Node, Node > > tf_arg_to_term;
-
- for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){
- Kind k = it->first;
+
+ for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+ {
+ Kind k = tfl.first;
if (k == EXPONENTIAL || k == SINE)
{
- for (std::map<Node, Node>::iterator itt = it->second.begin();
- itt != it->second.end();
- ++itt)
+ for (const Node& tf : tfl.second)
{
- Node a = itt->second[0];
+ Node a = tf[0];
computeModelValue(a, 1);
Assert(d_mv[1].find(a) != d_mv[1].end());
if (d_mv[1][a].isConst())
{
Trace("nl-ext-tf-mono-debug") << "...tf term : " << a << std::endl;
sorted_tf_args[k].push_back(a);
- tf_arg_to_term[k][a] = itt->second;
+ tf_arg_to_term[k][a] = tf;
}
}
}
//sort by concrete values
smv.d_order_type = 0;
smv.d_reverse_order = true;
- for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){
- Kind k = it->first;
+ for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+ {
+ Kind k = tfl.first;
if( !sorted_tf_args[k].empty() ){
std::sort( sorted_tf_args[k].begin(), sorted_tf_args[k].end(), smv );
Trace("nl-ext-tf-mono") << "Sorted transcendental function list for " << k << " : " << std::endl;
- for( unsigned i=0; i<sorted_tf_args[it->first].size(); i++ ){
+ for (unsigned i = 0; i < sorted_tf_args[k].size(); i++)
+ {
Node targ = sorted_tf_args[k][i];
Assert( d_mv[1].find( targ )!=d_mv[1].end() );
Trace("nl-ext-tf-mono") << " " << targ << " -> " << d_mv[1][targ] << std::endl;
}
std::vector< Node > mpoints;
std::vector< Node > mpoints_vals;
- if (it->first == SINE)
+ if (k == SINE)
{
mpoints.push_back( d_pi );
mpoints.push_back( d_pi_2 );
mpoints.push_back( d_pi_neg_2 );
mpoints.push_back( d_pi_neg );
}
- else if (it->first == EXPONENTIAL)
+ else if (k == EXPONENTIAL)
{
mpoints.push_back( Node::null() );
}
int monotonic_dir = -1;
Node mono_bounds[2];
Node targ, targval, t, tval;
- for( unsigned i=0; i<sorted_tf_args[it->first].size(); i++ ){
+ for (unsigned i = 0, size = sorted_tf_args[k].size(); i < size; i++)
+ {
Node sarg = sorted_tf_args[k][i];
Assert( d_mv[1].find( sarg )!=d_mv[1].end() );
Node sargval = d_mv[1][sarg];
tval = Node::null();
mono_bounds[1] = mpoints[mdir_index];
mdir_index++;
- monotonic_dir = regionToMonotonicityDir(it->first, mdir_index);
+ monotonic_dir = regionToMonotonicityDir(k, mdir_index);
if (mdir_index < mpoints.size())
{
mono_bounds[0] = mpoints[mdir_index];
<< std::endl;
// this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions
// via Incremental Linearization" by Cimatti et al
- for (std::pair<const Kind, std::map<Node, Node> >& tfs : d_tf_rep_map)
+ for (std::pair<const Kind, std::vector<Node> >& tfs : d_f_map)
{
Kind k = tfs.first;
if (k == PI)
// we substitute into the Taylor sum P_{n,f(0)}( x )
- for (std::pair<const Node, Node>& tfr : tfs.second)
+ for (const Node& tf : tfs.second)
{
- // Figure 3 : tf( x )
- Node tf = tfr.second;
+ // tf is Figure 3 : tf( x )
if (isRefineableTfFun(tf))
{
Trace("nl-ext-tftp") << "Compute tangent planes " << tf << std::endl;
projects / cvc5.git / commitdiff