summaryrefslogtreecommitdiff
path: root/src/theory/arith/nonlinear_extension.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/nonlinear_extension.cpp')
-rw-r--r--src/theory/arith/nonlinear_extension.cpp46
1 files changed, 23 insertions, 23 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 4747727c8..839520c0b 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -975,7 +975,7 @@ bool NonlinearExtension::addCheckModelSubstitution(TNode v, TNode s)
{
Trace("nl-ext-model") << "...ERROR: already has value." << std::endl;
// this should never happen since substitutions should be applied eagerly
- Assert( false );
+ Assert(false);
return false;
}
// if we previously had an approximate bound, the exact bound should be in its
@@ -1876,8 +1876,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
/*
//mark processed if has a "one" factor (will look at reduced monomial)
std::map< Node, std::map< Node, unsigned > >::iterator itme =
- d_m_exp.find( a ); Assert( itme!=d_m_exp.end() ); for( std::map< Node,
- unsigned >::iterator itme2 = itme->second.begin(); itme2 !=
+ d_m_exp.find( a ); Assert( itme!=d_m_exp.end() ); for( std::map<
+ Node, unsigned >::iterator itme2 = itme->second.begin(); itme2 !=
itme->second.end(); ++itme2 ){ Node v = itme->first; Assert(
d_mv[0].find( v )!=d_mv[0].end() ); Node mvv = d_mv[0][ v ]; if(
mvv==d_one || mvv==d_neg_one ){ ms_proc[ a ] = true;
@@ -1957,7 +1957,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
}
else
{
- Assert( false );
+ Assert(false);
}
}
// initialize pi if necessary
@@ -2669,7 +2669,7 @@ void NonlinearExtension::printModelValue(const char* c,
int NonlinearExtension::compare_value(Node i, Node j,
unsigned orderType) const {
Assert(orderType >= 0 && orderType <= 3);
- Assert( i.isConst() && j.isConst() );
+ Assert(i.isConst() && j.isConst());
Trace("nl-ext-debug") << "compare value " << i << " " << j
<< ", o = " << orderType << std::endl;
int ret;
@@ -2725,8 +2725,8 @@ int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index,
Node av = d_m_vlist[a][a_index];
unsigned aexp = d_m_exp[a][av];
// take current sign in model
- Assert( d_mv[1].find(av) != d_mv[0].end() );
- Assert( d_mv[1][av].isConst() );
+ Assert(d_mv[1].find(av) != d_mv[0].end());
+ Assert(d_mv[1][av].isConst());
int sgn = d_mv[1][av].getConst<Rational>().sgn();
Trace("nl-ext-debug") << "Process var " << av << "^" << aexp
<< ", model sign = " << sgn << std::endl;
@@ -3032,7 +3032,7 @@ std::vector<Node> NonlinearExtension::checkMonomialMagnitude( unsigned c ) {
// compare magnitude against variables
for (unsigned k = 0; k < d_ms_vars.size(); k++) {
Node v = d_ms_vars[k];
- Assert( d_mv[0].find( v )!=d_mv[0].end() );
+ Assert(d_mv[0].find(v) != d_mv[0].end());
if( d_mv[0][v].isConst() ){
std::vector<Node> exp;
NodeMultiset a_exp_proc;
@@ -3185,7 +3185,7 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() {
Node curr_v = p<=1 ? a_v_c : b_v_c;
if( prevRefine ){
Node pt_v = d_tangent_val_bound[p][a][b];
- Assert( !pt_v.isNull() );
+ Assert(!pt_v.isNull());
if( curr_v!=pt_v ){
Node do_extend =
nm->mkNode((p == 1 || p == 3) ? GT : LT, curr_v, pt_v);
@@ -3424,8 +3424,8 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds(
Kind type = itcr->second;
for (unsigned j = 0; j < itm->second.size(); j++) {
Node y = itm->second[j];
- Assert(d_m_contain_mult[x].find(y) !=
- d_m_contain_mult[x].end());
+ Assert(d_m_contain_mult[x].find(y)
+ != d_m_contain_mult[x].end());
Node mult = d_m_contain_mult[x][y];
// x <k> t => m*x <k'> t where y = m*x
// get the sign of mult
@@ -3583,7 +3583,7 @@ std::vector<Node> NonlinearExtension::checkFactoring(
poly.push_back(NodeManager::currentNM()->mkNode(MULT, x, kf));
std::map<Node, std::vector<Node> >::iterator itfo =
factor_to_mono_orig.find(x);
- Assert( itfo!=factor_to_mono_orig.end() );
+ Assert(itfo != factor_to_mono_orig.end());
for( std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
if( std::find( itfo->second.begin(), itfo->second.end(), itm->first )==itfo->second.end() ){
poly.push_back(ArithMSum::mkCoeffTerm(
@@ -3781,7 +3781,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() {
Kind k = tfl.first;
for (const Node& t : tfl.second)
{
- Assert( d_mv[1].find( t )!=d_mv[1].end() );
+ 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;
@@ -3921,10 +3921,10 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
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() );
+ Assert(d_mv[1].find(targ) != d_mv[1].end());
Trace("nl-ext-tf-mono") << " " << targ << " -> " << d_mv[1][targ] << std::endl;
Node t = tf_arg_to_term[k][targ];
- Assert( d_mv[1].find( t )!=d_mv[1].end() );
+ Assert(d_mv[1].find(t) != d_mv[1].end());
Trace("nl-ext-tf-mono") << " f-val : " << d_mv[1][t] << std::endl;
}
std::vector< Node > mpoints;
@@ -3947,7 +3947,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
Node mpv;
if( !mpoints[i].isNull() ){
mpv = computeModelValue( mpoints[i], 1 );
- Assert( mpv.isConst() );
+ Assert(mpv.isConst());
}
mpoints_vals.push_back( mpv );
}
@@ -3959,14 +3959,14 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
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() );
+ Assert(d_mv[1].find(sarg) != d_mv[1].end());
Node sargval = d_mv[1][sarg];
- Assert( sargval.isConst() );
+ Assert(sargval.isConst());
Node s = tf_arg_to_term[k][ sarg ];
- Assert( d_mv[1].find( s )!=d_mv[1].end() );
+ Assert(d_mv[1].find(s) != d_mv[1].end());
Node sval = d_mv[1][s];
- Assert( sval.isConst() );
-
+ Assert(sval.isConst());
+
//increment to the proper monotonicity region
bool increment = true;
while (increment && mdir_index < mpoints.size())
@@ -3976,7 +3976,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
increment = true;
}else{
Node pval = mpoints_vals[mdir_index];
- Assert( pval.isConst() );
+ Assert(pval.isConst());
if( sargval.getConst<Rational>() < pval.getConst<Rational>() ){
increment = true;
Trace("nl-ext-tf-mono") << "...increment at " << sarg << " since model value is less than " << mpoints[mdir_index] << std::endl;
@@ -4017,7 +4017,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
}
if( !mono_lem.isNull() ){
if( !mono_bounds[0].isNull() ){
- Assert( !mono_bounds[1].isNull() );
+ Assert(!mono_bounds[1].isNull());
mono_lem = NodeManager::currentNM()->mkNode(
IMPLIES,
NodeManager::currentNM()->mkNode(
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback