summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/bounded_integers.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.cpp')
-rwxr-xr-x[-rw-r--r--]src/theory/quantifiers/bounded_integers.cpp365
1 files changed, 248 insertions, 117 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index d32ef59a1..7184624da 100644..100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -28,7 +28,7 @@ using namespace CVC4::theory::quantifiers;
using namespace CVC4::kind;
-BoundedIntegers::RangeModel::RangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy) : d_bi(bi),
+BoundedIntegers::IntRangeModel::IntRangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy) : d_bi(bi),
d_range(r), d_curr_max(-1), d_lit_to_range(u), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1), d_ranges_proxied(u) {
if( options::fmfBoundIntLazy() ){
d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() );
@@ -40,7 +40,7 @@ BoundedIntegers::RangeModel::RangeModel(BoundedIntegers * bi, Node r, context::C
}
}
-void BoundedIntegers::RangeModel::initialize() {
+void BoundedIntegers::IntRangeModel::initialize() {
//add initial split lemma
Node ltr = NodeManager::currentNM()->mkNode( LT, d_proxy_range, NodeManager::currentNM()->mkConst( Rational(0) ) );
ltr = Rewriter::rewrite( ltr );
@@ -55,7 +55,7 @@ void BoundedIntegers::RangeModel::initialize() {
d_bi->addLiteralFromRange(ltr_lit, d_range);
}
-void BoundedIntegers::RangeModel::assertNode(Node n) {
+void BoundedIntegers::IntRangeModel::assertNode(Node n) {
bool pol = n.getKind()!=NOT;
Node nlit = n.getKind()==NOT ? n[0] : n;
if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){
@@ -93,7 +93,7 @@ void BoundedIntegers::RangeModel::assertNode(Node n) {
}
}
-void BoundedIntegers::RangeModel::allocateRange() {
+void BoundedIntegers::IntRangeModel::allocateRange() {
d_curr_max++;
int newBound = d_curr_max;
Trace("bound-int-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;
@@ -110,7 +110,7 @@ void BoundedIntegers::RangeModel::allocateRange() {
d_bi->addLiteralFromRange(ltr_lit, d_range);
}
-Node BoundedIntegers::RangeModel::getNextDecisionRequest() {
+Node BoundedIntegers::IntRangeModel::getNextDecisionRequest() {
//request the current cardinality as a decision literal, if not already asserted
for( NodeIntMap::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
int i = (*it).second;
@@ -129,7 +129,7 @@ Node BoundedIntegers::RangeModel::getNextDecisionRequest() {
return Node::null();
}
-bool BoundedIntegers::RangeModel::proxyCurrentRange() {
+bool BoundedIntegers::IntRangeModel::proxyCurrentRange() {
//Trace("model-engine") << "Range(" << d_range << ") currently is " << d_curr_max.get() << std::endl;
if( d_range!=d_proxy_range ){
//int curr = d_curr_range.get();
@@ -148,11 +148,24 @@ bool BoundedIntegers::RangeModel::proxyCurrentRange() {
}
+
+
+
BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) :
QuantifiersModule(qe), d_assertions(c){
}
+BoundedIntegers::~BoundedIntegers() {
+ for( std::map< Node, RangeModel * >::iterator it = d_rms.begin(); it != d_rms.end(); ++it ){
+ delete it->second;
+ }
+}
+
+void BoundedIntegers::presolve() {
+ d_bnd_it.clear();
+}
+
bool BoundedIntegers::isBound( Node f, Node v ) {
return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();
}
@@ -172,62 +185,79 @@ bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
return false;
}
-void BoundedIntegers::processLiteral( Node f, Node lit, bool pol,
+void BoundedIntegers::processLiteral( Node q, Node lit, bool pol,
+ std::map< Node, unsigned >& bound_lit_type_map,
std::map< int, std::map< Node, Node > >& bound_lit_map,
- std::map< int, std::map< Node, bool > >& bound_lit_pol_map ) {
- if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){
- std::map< Node, Node > msum;
- if (QuantArith::getMonomialSumLit( lit, msum )){
- Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
- QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" );
- for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
- if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){
- Node veq;
- if( QuantArith::isolate( it->first, msum, veq, GEQ )!=0 ){
- Node n1 = veq[0];
- Node n2 = veq[1];
- if(pol){
- //flip
- n1 = veq[1];
- n2 = veq[0];
- if( n1.getKind()==BOUND_VARIABLE ){
- n2 = QuantArith::offset( n2, 1 );
+ std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
+ std::map< int, std::map< Node, Node > >& bound_int_range_term ) {
+ if( lit.getKind()==GEQ ){
+ if( lit[0].getType().isInteger() ){
+ std::map< Node, Node > msum;
+ if( QuantArith::getMonomialSumLit( lit, msum ) ){
+ Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
+ QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" );
+ for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+ if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( q, it->first ) ){
+ Node veq;
+ if( QuantArith::isolate( it->first, msum, veq, GEQ )!=0 ){
+ Node n1 = veq[0];
+ Node n2 = veq[1];
+ if(pol){
+ //flip
+ n1 = veq[1];
+ n2 = veq[0];
+ if( n1.getKind()==BOUND_VARIABLE ){
+ n2 = QuantArith::offset( n2, 1 );
+ }else{
+ n1 = QuantArith::offset( n1, -1 );
+ }
+ veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
+ }
+ Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
+ Node t = n1==it->first ? n2 : n1;
+ if( !hasNonBoundVar( q, t ) ) {
+ Trace("bound-int-debug") << "The bound is relevant." << std::endl;
+ int loru = n1==it->first ? 0 : 1;
+ bound_lit_type_map[it->first] = BOUND_INT_RANGE;
+ bound_int_range_term[loru][it->first] = t;
+ bound_lit_map[loru][it->first] = lit;
+ bound_lit_pol_map[loru][it->first] = pol;
}else{
- n1 = QuantArith::offset( n1, -1 );
+ Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
}
- veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
- }
- Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
- Node t = n1==it->first ? n2 : n1;
- if( !hasNonBoundVar( f, t ) ) {
- Trace("bound-int-debug") << "The bound is relevant." << std::endl;
- int loru = n1==it->first ? 0 : 1;
- d_bounds[loru][f][it->first] = t;
- bound_lit_map[loru][it->first] = lit;
- bound_lit_pol_map[loru][it->first] = pol;
- }else{
- Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
}
}
}
}
}
+ }else if( lit.getKind()==MEMBER ){
+ //TODO: enable this when sets models are fixed
+ /*
+ if( !pol && lit[0].getKind()==BOUND_VARIABLE && !isBound( q, lit[0] ) && !lit[1].hasBoundVar() ){
+ Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is membership." << std::endl;
+ bound_lit_type_map[lit[0]] = BOUND_SET_MEMBER;
+ bound_lit_map[0][lit[0]] = lit;
+ bound_lit_pol_map[0][lit[0]] = pol;
+ }
+ */
}else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {
Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;
}
}
-void BoundedIntegers::process( Node f, Node n, bool pol,
+void BoundedIntegers::process( Node q, Node n, bool pol,
+ std::map< Node, unsigned >& bound_lit_type_map,
std::map< int, std::map< Node, Node > >& bound_lit_map,
- std::map< int, std::map< Node, bool > >& bound_lit_pol_map ){
+ std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
+ std::map< int, std::map< Node, Node > >& bound_int_range_term ){
if( (n.getKind()==OR && pol) || (n.getKind()==AND && !pol) ){
for( unsigned i=0; i<n.getNumChildren(); i++) {
- process( f, n[i], pol, bound_lit_map, bound_lit_pol_map );
+ process( q, n[i], pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
}
}else if( n.getKind()==NOT ){
- process( f, n[0], !pol, bound_lit_map, bound_lit_pol_map );
+ process( q, n[0], !pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
}else {
- processLiteral( f, n, pol, bound_lit_map, bound_lit_pol_map );
+ processLiteral( q, n, pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
}
}
@@ -258,58 +288,99 @@ void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) {
}
}
+void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) {
+ d_bound_type[q][v] = bound_type;
+ d_set_nums[q][v] = d_set[q].size();
+ d_set[q].push_back( v );
+ Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl;
+}
+
void BoundedIntegers::registerQuantifier( Node f ) {
Trace("bound-int") << "Register quantifier " << f << std::endl;
- bool hasIntType = false;
- int finiteTypes = 0;
- std::map< Node, int > numMap;
- for( unsigned i=0; i<f[0].getNumChildren(); i++) {
- numMap[f[0][i]] = i;
- if( f[0][i].getType().isInteger() ){
- hasIntType = true;
- }
- else if( f[0][i].getType().isSort() || f[0][i].getType().getCardinality().isFinite() ){
- finiteTypes++;
- }
- }
- if( hasIntType ){
- bool success;
- do{
- std::map< int, std::map< Node, Node > > bound_lit_map;
- std::map< int, std::map< Node, bool > > bound_lit_pol_map;
- success = false;
- process( f, f[1], true, bound_lit_map, bound_lit_pol_map );
- for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){
- Node v = it->first;
- if( !isBound(f,v) ){
- if( d_bounds[1][f].find(v)!=d_bounds[1][f].end() ){
- d_set[f].push_back(v);
- d_set_nums[f].push_back(numMap[v]);
+
+ bool success;
+ do{
+ std::map< Node, unsigned > bound_lit_type_map;
+ std::map< int, std::map< Node, Node > > bound_lit_map;
+ std::map< int, std::map< Node, bool > > bound_lit_pol_map;
+ std::map< int, std::map< Node, Node > > bound_int_range_term;
+ success = false;
+ process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
+ //for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){
+ for( std::map< Node, unsigned >::iterator it = bound_lit_type_map.begin(); it != bound_lit_type_map.end(); ++it ){
+ Node v = it->first;
+ if( !isBound( f, v ) ){
+ bool setBoundVar = false;
+ if( it->second==BOUND_INT_RANGE ){
+ //must have both
+ if( bound_lit_map[0].find( v )!=bound_lit_map[0].end() && bound_lit_map[1].find( v )!=bound_lit_map[1].end() ){
+ setBoundedVar( f, v, BOUND_INT_RANGE );
+ setBoundVar = true;
success = true;
- //set Attributes on literals
for( unsigned b=0; b<2; b++ ){
- Assert( bound_lit_map[b].find( v )!=bound_lit_map[b].end() );
+ //set the bounds
+ Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() );
+ d_bounds[b][f][v] = bound_int_range_term[b][v];
+ }
+ Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );
+ d_range[f][v] = Rewriter::rewrite( r );
+ Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
+ }
+ }else if( it->second==BOUND_SET_MEMBER ){
+ setBoundedVar( f, v, BOUND_SET_MEMBER );
+ setBoundVar = true;
+ d_setm_range[f][v] = bound_lit_map[0][v][1];
+ Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[0][v] << std::endl;
+ }
+ if( setBoundVar ){
+ //set Attributes on literals
+ for( unsigned b=0; b<2; b++ ){
+ if( bound_lit_map[b].find( v )!=bound_lit_map[b].end() ){
Assert( bound_lit_pol_map[b].find( v )!=bound_lit_pol_map[b].end() );
BoundIntLitAttribute bila;
bound_lit_map[b][v].setAttribute( bila, bound_lit_pol_map[b][v] ? 1 : 0 );
+ }else{
+ Assert( it->second!=BOUND_INT_RANGE );
}
- Trace("bound-int") << "Variable " << v << " is bound because of literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
}
}
}
- }while( success );
- Trace("bound-int") << "Bounds are : " << std::endl;
- for( unsigned i=0; i<d_set[f].size(); i++) {
- Node v = d_set[f][i];
- Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );
- d_range[f][v] = Rewriter::rewrite( r );
+ }
+ }while( success );
+
+ Trace("bound-int") << "Bounds are : " << std::endl;
+ for( unsigned i=0; i<d_set[f].size(); i++) {
+ Node v = d_set[f][i];
+ if( d_bound_type[f][v]==BOUND_INT_RANGE ){
Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
+ }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
+ Trace("bound-int") << " " << v << " in " << d_setm_range[f][v] << std::endl;
+ }
+ }
+
+ bool bound_success = true;
+ for( unsigned i=0; i<f[0].getNumChildren(); i++) {
+ if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
+ TypeNode tn = f[0][i].getType();
+ if( !tn.isSort() && !getTermDatabase()->mayComplete( tn ) ){
+ Trace("bound-int-warn") << "Warning : Bounded Integers : Due to quantification on " << f[0][i] << ", could not find bounds for " << f << std::endl;
+ bound_success = false;
+ break;
+ }
}
- if( d_set[f].size()==(f[0].getNumChildren()-finiteTypes) ){
- d_bound_quants.push_back( f );
- for( unsigned i=0; i<d_set[f].size(); i++) {
- Node v = d_set[f][i];
- Node r = d_range[f][v];
+ }
+
+ if( bound_success ){
+ d_bound_quants.push_back( f );
+ for( unsigned i=0; i<d_set[f].size(); i++) {
+ Node v = d_set[f][i];
+ if( d_bound_type[f][v]==BOUND_INT_RANGE || d_bound_type[f][v]==BOUND_SET_MEMBER ){
+ Node r;
+ if( d_bound_type[f][v]==BOUND_INT_RANGE ){
+ r = d_range[f][v];
+ }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
+ r = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] );
+ }
bool isProxy = false;
if( r.hasBoundVar() ){
//introduce a new bound
@@ -319,18 +390,15 @@ void BoundedIntegers::registerQuantifier( Node f ) {
r = new_range;
isProxy = true;
}
- if( r.getKind()!=CONST_RATIONAL ){
+ if( !r.isConst() ){
if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){
- Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl;
+ Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl;
d_ranges.push_back( r );
- d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext(), d_quantEngine->getUserContext(), isProxy );
+ d_rms[r] = new IntRangeModel( this, r, d_quantEngine->getSatContext(), d_quantEngine->getUserContext(), isProxy );
d_rms[r]->initialize();
}
}
}
- }else{
- Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f << std::endl;
- //Message() << "Bound integers : Cannot infer bounds of " << f << std::endl;
}
}
}
@@ -376,39 +444,28 @@ Node BoundedIntegers::getNextDecisionRequest() {
return Node::null();
}
+unsigned BoundedIntegers::getBoundVarType( Node q, Node v ) {
+ std::map< Node, unsigned >::iterator it = d_bound_type[q].find( v );
+ if( it==d_bound_type[q].end() ){
+ return BOUND_NONE;
+ }else{
+ return it->second;
+ }
+}
+
void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
l = d_bounds[0][f][v];
u = d_bounds[1][f][v];
if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){
- //must create substitution
+ //get the substitution
std::vector< Node > vars;
std::vector< Node > subs;
- Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl;
- for( unsigned i=0; i<d_set[f].size(); i++) {
- if( d_set[f][i]!=v ){
- Trace("bound-int-rsi") << "Look up the value for " << d_set[f][i] << " " << rsi->d_var_order[d_set_nums[f][i]] << std::endl;
- Trace("bound-int-rsi") << "term : " << rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]) << std::endl;
- vars.push_back(d_set[f][i]);
- subs.push_back(rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]));
- }else{
- break;
- }
- }
- Trace("bound-int-rsi") << "Do substitution..." << std::endl;
- //check if it has been instantiated
- if (!vars.empty() && !d_bnd_it[f][v].hasInstantiated(subs)){
- //must add the lemma
- Node nn = d_nground_range[f][v];
- nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[f][v] );
- Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
- d_quantEngine->getOutputChannel().lemma(lem, false, true);
- l = Node::null();
- u = Node::null();
- return;
- }else{
+ if( getRsiSubsitution( f, v, vars, subs, rsi ) ){
u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ }else{
+ u = Node::null();
+ l = Node::null();
}
}
}
@@ -416,12 +473,86 @@ void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l,
void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
getBounds( f, v, rsi, l, u );
Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;
- l = d_quantEngine->getModel()->getCurrentModelValue( l );
- u = d_quantEngine->getModel()->getCurrentModelValue( u );
+ if( !l.isNull() ){
+ l = d_quantEngine->getModel()->getCurrentModelValue( l );
+ }
+ if( !u.isNull() ){
+ u = d_quantEngine->getModel()->getCurrentModelValue( u );
+ }
Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;
return;
}
-bool BoundedIntegers::isGroundRange(Node f, Node v) {
- return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar();
+bool BoundedIntegers::isGroundRange( Node q, Node v ) {
+ if( isBoundVar(q,v) ){
+ if( d_bound_type[q][v]==BOUND_INT_RANGE ){
+ return !getLowerBound(q,v).hasBoundVar() && !getUpperBound(q,v).hasBoundVar();
+ }else if( d_bound_type[q][v]==BOUND_SET_MEMBER ){
+ return !d_setm_range[q][v].hasBoundVar();
+ }
+ }
+ return false;
}
+
+Node BoundedIntegers::getSetRange( Node q, Node v, RepSetIterator * rsi ) {
+ Node sr = d_setm_range[q][v];
+ if( d_nground_range[q].find(v)!=d_nground_range[q].end() ){
+ //get the substitution
+ std::vector< Node > vars;
+ std::vector< Node > subs;
+ if( getRsiSubsitution( q, v, vars, subs, rsi ) ){
+ sr = sr.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ }else{
+ sr = Node::null();
+ }
+ }
+ return sr;
+}
+
+Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
+ Node sr = getSetRange( q, v, rsi );
+ if( !sr.isNull() ){
+ Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
+ sr = d_quantEngine->getModel()->getCurrentModelValue( sr );
+ Trace("bound-int-rsi") << "Value is " << sr << std::endl;
+ }
+ return sr;
+}
+
+bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ) {
+
+ Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl;
+ Assert( d_set_nums[q].find( v )!=d_set_nums[q].end() );
+ int vindex = d_set_nums[q][v];
+ Assert( d_set_nums[q][v]==vindex );
+ Trace("bound-int-rsi-debug") << " index order is " << vindex << std::endl;
+ //must take substitution for all variables that are iterating at higher level
+ 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 );
+ Trace("bound-int-rsi") << "term : " << t << std::endl;
+ vars.push_back( d_set[q][i] );
+ subs.push_back( t );
+ }
+
+ //check if it has been instantiated
+ if( !vars.empty() && !d_bnd_it[q][v].hasInstantiated(subs) ){
+ if( d_bound_type[q][v]==BOUND_INT_RANGE ){
+ //must add the lemma
+ Node nn = d_nground_range[q][v];
+ 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);
+ }else{
+ //TODO : sets
+ }
+ return false;
+ }else{
+ return true;
+ }
+}
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback