/*! \file bounded_integers.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Andres Noetzli, Tim King
+ ** Andrew Reynolds, Andres Noetzli, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
return lem;
}
-BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe)
- : QuantifiersModule(qe)
+BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : QuantifiersModule(qs, qim, qr, qe)
{
}
{
Trace("bound-int-lemma")
<< "*** bound int : proxy lemma : " << prangeLem << std::endl;
- d_quantEngine->addLemma(prangeLem);
+ d_qim.addPendingLemma(prangeLem);
addedLemma = true;
}
}
}
}else if( d_bound_type[f][v]==BOUND_FIXED_SET ){
Trace("bound-int") << " " << v << " in { ";
- for( unsigned i=0; i<d_fixed_set_ngr_range[f][v].size(); i++ ){
- Trace("bound-int") << d_fixed_set_ngr_range[f][v][i] << " ";
+ for (TNode fnr : d_fixed_set_ngr_range[f][v])
+ {
+ Trace("bound-int") << fnr << " ";
}
- for( unsigned i=0; i<d_fixed_set_gr_range[f][v].size(); i++ ){
- Trace("bound-int") << d_fixed_set_gr_range[f][v][i] << " ";
+ for (TNode fgr : d_fixed_set_gr_range[f][v])
+ {
+ Trace("bound-int") << fgr << " ";
}
Trace("bound-int") << "}" << std::endl;
}else if( d_bound_type[f][v]==BOUND_FINITE ){
d_ranges.push_back( r );
d_rms[r].reset(
new IntRangeDecisionHeuristic(r,
- d_quantEngine->getSatContext(),
- d_quantEngine->getUserContext(),
+ d_qstate.getSatContext(),
+ d_qstate.getUserContext(),
d_quantEngine->getValuation(),
isProxy));
d_quantEngine->getTheoryEngine()
choices.pop_back();
Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i);
Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConst(Rational(i)));
- choice_i = nm->mkNode(CHOICE, bvl, nm->mkNode(OR, cMinCard, cBody));
+ choice_i = nm->mkNode(WITNESS, bvl, nm->mkNode(OR, cMinCard, cBody));
d_setm_choice[sro].push_back(choice_i);
}
Assert(i < d_setm_choice[sro].size());
choice_i = d_setm_choice[sro][i];
choices.push_back(choice_i);
- Node sChoiceI = nm->mkNode(SINGLETON, choice_i);
+ Node sChoiceI = nm->mkSingleton(choice_i.getType(), choice_i);
if (nsr.isNull())
{
nsr = sChoiceI;
// e.g.
// singleton(0) union singleton(1)
// becomes
- // C1 union ( choice y. card(S)<=1 OR ( y in S AND distinct( y, C1 ) ) )
- // where C1 = ( choice x. card(S)<=0 OR x in S ).
+ // C1 union ( witness y. card(S)<=1 OR ( y in S AND distinct( y, C1 ) ) )
+ // where C1 = ( witness x. card(S)<=0 OR x in S ).
Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl;
return nsr;
}
for( int i=0; i<vindex; i++) {
Assert(d_set_nums[q][d_set[q][i]] == i);
Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl;
- int v = rsi->getVariableOrder( i );
- Assert(q[0][v] == d_set[q][i]);
- Node t = rsi->getCurrentTerm(v, true);
+ int vo = rsi->getVariableOrder(i);
+ Assert(q[0][vo] == d_set[q][i]);
+ Node t = rsi->getCurrentTerm(vo, true);
Trace("bound-int-rsi") << "term : " << t << std::endl;
vars.push_back( d_set[q][i] );
subs.push_back( t );
nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] );
Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
- d_quantEngine->getOutputChannel().lemma(lem, false, true);
+ d_quantEngine->getOutputChannel().lemma(lem);
}
return false;
}else{