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() );
}
}
-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 );
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() ){
}
}
-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;
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;
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();
}
+
+
+
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();
}
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 );
}
}
}
}
+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
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;
}
}
}
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();
}
}
}
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;
+ }
+}
+
typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
typedef context::CDHashMap<int, bool> IntBoolMap;
+public:
+ enum {
+ BOUND_FINITE,
+ BOUND_INT_RANGE,
+ BOUND_SET_MEMBER,
+ BOUND_NONE
+ };
private:
//for determining bounds
bool isBound( Node f, Node v );
bool hasNonBoundVar( Node f, Node b );
- std::map< Node, std::map< Node, Node > > d_bounds[2];
+ //bound type
+ std::map< Node, std::map< Node, unsigned > > d_bound_type;
std::map< Node, std::vector< Node > > d_set;
- std::map< Node, std::vector< int > > d_set_nums;
+ std::map< Node, std::map< Node, int > > d_set_nums;
+ //integer lower/upper bounds
+ std::map< Node, std::map< Node, Node > > d_bounds[2];
std::map< Node, std::map< Node, Node > > d_range;
std::map< Node, std::map< Node, Node > > d_nground_range;
+ //set membership range
+ std::map< Node, std::map< Node, Node > > d_setm_range;
void hasFreeVar( Node f, Node n );
void process( Node f, 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 );
void processLiteral( Node f, 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 );
+ std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
+ std::map< int, std::map< Node, Node > >& bound_int_range_term );
std::vector< Node > d_bound_quants;
private:
class RangeModel {
+ public:
+ RangeModel(){}
+ virtual ~RangeModel(){}
+ virtual void initialize() = 0;
+ virtual void assertNode(Node n) = 0;
+ virtual Node getNextDecisionRequest() = 0;
+ virtual bool proxyCurrentRange() = 0;
+ };
+ class IntRangeModel : public RangeModel {
private:
BoundedIntegers * d_bi;
void allocateRange();
Node d_proxy_range;
public:
- RangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy);
+ IntRangeModel( BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy);
+ virtual ~IntRangeModel(){}
Node d_range;
int d_curr_max;
std::map< int, Node > d_range_literal;
std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
private:
void addLiteralFromRange( Node lit, Node r );
+
+ void setBoundedVar( Node f, Node v, unsigned bound_type );
public:
BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
- ~BoundedIntegers() throw() {}
-
+ virtual ~BoundedIntegers();
+
+ void presolve();
bool needsCheck( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
void registerQuantifier( Node f );
void assertNode( Node n );
Node getNextDecisionRequest();
- bool isBoundVar( Node f, Node v ) { return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); }
- unsigned getNumBoundVars( Node f ) { return d_set[f].size(); }
- Node getBoundVar( Node f, int i ) { return d_set[f][i]; }
- int getBoundVarNum( Node f, int i ) { return d_set_nums[f][i]; }
- Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; }
- Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; }
+ bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
+ unsigned getBoundVarType( Node q, Node v );
+ unsigned getNumBoundVars( Node q ) { return d_set[q].size(); }
+ Node getBoundVar( Node q, int i ) { return d_set[q][i]; }
+ //for integer range
+ Node getLowerBound( Node q, Node v ){ return d_bounds[0][q][v]; }
+ Node getUpperBound( Node q, Node v ){ return d_bounds[1][q][v]; }
void getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
bool isGroundRange(Node f, Node v);
+ //for set range
+ Node getSetRange( Node q, Node v, RepSetIterator * rsi );
+ Node getSetRangeValue( Node q, Node v, RepSetIterator * rsi );
/** Identify this module */
std::string identify() const { return "BoundedIntegers"; }
+private:
+ bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
};
}
//check the type of n
if( n.getKind()==INST_CONSTANT ){
int v = n.getAttribute(InstVarNumAttribute());
- depIndex = ri->d_var_order[ v ];
- val = ri->getTerm( v );
+ depIndex = ri->getIndexOrder( v );
+ val = ri->getCurrentTerm( v );
}else if( n.getKind()==ITE ){
int depIndex1, depIndex2;
int eval = evaluate( n[0], depIndex1, ri );
Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
//set the domains based on the entry
for (unsigned i=0; i<c.getNumChildren(); i++) {
- if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {
+ if( riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS || riter.d_enum_type[i]==RepSetIterator::ENUM_SET_MEMBERS ){
TypeNode tn = c[i].getType();
if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
if( fm->isInterval(c[i]) || fm->isStar(c[i]) ){
if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
riter.d_domain[i].clear();
riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
+ riter.d_enum_type[i] = RepSetIterator::ENUM_DOMAIN_ELEMENTS;
}else{
Trace("fmc-exh") << "---- Does not have rep : " << c[i] << " for type " << tn << std::endl;
return false;
std::vector< Node > ev_inst;
std::vector< Node > inst;
for( int i=0; i<riter.getNumTerms(); i++ ){
- Node rr = riter.getTerm( i );
+ Node rr = riter.getCurrentTerm( i );
Node r = rr;
//if( r.getType().isSort() ){
r = fm->getUsedRepresentative( r );
int index = riter.increment();
Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
if( !riter.isFinished() ){
- if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {
+ if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_INT_RANGE) {
Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;
riter.increment2( index-1 );
}
}
}
d_addedLemmas += addedLemmas;
- Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl;
- return addedLemmas>0 || !riter.d_incomplete;
+ Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.isIncomplete() << std::endl;
+ return addedLemmas>0 || !riter.isIncomplete();
}else{
Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl;
- return false;
+ return !riter.isIncomplete();
}
}
Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
for( unsigned i=0; i<patTermsF.size(); i++ ){
Assert( tinfo.find( patTermsF[i] )!=tinfo.end() );
- Trace("auto-gen-trigger-debug") << " " << patTermsF[i];
- Trace("auto-gen-trigger-debug") << " info[" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl;
+ Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << std::endl;
+ Trace("auto-gen-trigger-debug2") << " info = [" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl;
}
Trace("auto-gen-trigger-debug") << std::endl;
}
tests++;
std::vector< Node > terms;
for( int k=0; k<riter.getNumTerms(); k++ ){
- terms.push_back( riter.getTerm( k ) );
+ terms.push_back( riter.getCurrentTerm( k ) );
}
Node n = d_qe->getInstantiation( f, vars, terms );
Node val = fm->getValue( n );
}
Trace("quant-check-model") << "." << std::endl;
}else{
- Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl;
+ if( riter.isIncomplete() ){
+ Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl;
+ }
}
}
}
Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
d_triedLemmas++;
- for( int i=0; i<(int)riter.d_index.size(); i++ ){
- Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl;
+ if( Debug.isOn("inst-fmf-ei-debug") ){
+ for( int i=0; i<(int)riter.d_index.size(); i++ ){
+ Debug("inst-fmf-ei-debug") << i << " : " << riter.d_index[i] << " : " << riter.getCurrentTerm( i ) << std::endl;
+ }
}
int eval = 0;
int depIndex;
//see if instantiation is already true in current model
- Debug("fmf-model-eval") << "Evaluating ";
- riter.debugPrintSmall("fmf-model-eval");
- Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+ if( Debug.isOn("fmf-model-eval") ){
+ Debug("fmf-model-eval") << "Evaluating ";
+ riter.debugPrintSmall("fmf-model-eval");
+ Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+ }
//if evaluate(...)==1, then the instantiation is already true in the model
// depIndex is the index of the least significant variable that this evaluation relies upon
depIndex = riter.getNumTerms()-1;
//instantiation was not shown to be true, construct the match
InstMatch m( f );
for( int i=0; i<riter.getNumTerms(); i++ ){
- m.set( d_qe, riter.d_index_order[i], riter.getTerm( i ) );
+ m.set( d_qe, i, riter.getCurrentTerm( i ) );
}
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
//add as instantiation
Trace("model-engine-warn") << std::endl;
}
}
- //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
- d_incomplete_check = riter.d_incomplete;
+ //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+ d_incomplete_check = riter.isIncomplete();
return true;
}else{
return false;
//create a rep set iterator and iterate over the (relevant) domain of the quantifier
RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
if( riter.setQuantifier( f ) ){
- Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.d_incomplete << "..." << std::endl;
- if( !riter.d_incomplete ){
+ Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
+ if( !riter.isIncomplete() ){
int triedLemmas = 0;
int addedLemmas = 0;
while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
//instantiation was not shown to be true, construct the match
InstMatch m( f );
for( int i=0; i<riter.getNumTerms(); i++ ){
- m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) );
+ m.set( d_quantEngine, i, riter.getCurrentTerm( i ) );
}
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
triedLemmas++;
d_statistics.d_exh_inst_lemmas += addedLemmas;
}
}else{
- Trace("fmf-exh-inst") << "...exhaustive instantiation failed to set, incomplete=" << riter.d_incomplete << "..." << std::endl;
- Assert( riter.d_incomplete );
+ Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
}
//if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
- d_incomplete_check = d_incomplete_check || riter.d_incomplete;
+ d_incomplete_check = d_incomplete_check || riter.isIncomplete();
}
}
}
Node op = getMatchOperator( n );
+ Trace("term-db-debug") << " match operator is : " << op << std::endl;
d_op_map[op].push_back( n );
added.insert( n );
Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl;
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
d_vars[q].push_back( q[0][i] );
+ d_var_num[q][q[0][i]] = i;
//make instantiation constants
Node ic = NodeManager::currentNM()->mkInstConstant( q[0][i].getType() );
d_inst_constants_map[ic] = q;
private:
/** map from universal quantifiers to the list of variables */
std::map< Node, std::vector< Node > > d_vars;
+ std::map< Node, std::map< Node, unsigned > > d_var_num;
/** map from universal quantifiers to the list of instantiation constants */
std::map< Node, std::vector< Node > > d_inst_constants;
/** map from universal quantifiers to their inst constant body */
/** make instantiation constants for */
void makeInstantiationConstantsFor( Node q );
public:
+ /** get variable number */
+ unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; }
/** get the i^th instantiation constant of q */
Node getInstantiationConstant( Node q, int i ) const;
/** get number of instantiation constants for q */
//check whether we should apply a reduction
if( reduceQuantifier( f ) ){
+ Trace("quant") << "...reduced." << std::endl;
d_quants[f] = false;
return false;
}else{
}
void RepSet::toStream(std::ostream& out){
-#if 0
- for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
- out << it->first << " : " << std::endl;
- for( int i=0; i<(int)it->second.size(); i++ ){
- out << " " << i << ": " << it->second[i] << std::endl;
- }
- }
-#else
for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
if( !it->first.isFunction() && !it->first.isPredicate() ){
out << "(" << it->first << " " << it->second.size();
out << " (";
- for( int i=0; i<(int)it->second.size(); i++ ){
+ for( unsigned i=0; i<it->second.size(); i++ ){
if( i>0 ){ out << " "; }
out << it->second[i];
}
out << ")" << std::endl;
}
}
-#endif
}
int RepSetIterator::domainSize( int i ) {
Assert(i>=0);
- if( d_enum_type[i]==ENUM_DOMAIN_ELEMENTS ){
- return d_domain[i].size();
+ int v = d_var_order[i];
+ if( d_enum_type[v]==ENUM_DOMAIN_ELEMENTS ){
+ return d_domain[v].size();
}else{
- return d_domain[i][0];
+ return d_domain[v][0];
}
}
bool RepSetIterator::initialize(){
Trace("rsi") << "Initialize rep set iterator..." << std::endl;
- for( size_t i=0; i<d_types.size(); i++ ){
+ for( unsigned v=0; v<d_types.size(); v++ ){
d_index.push_back( 0 );
//store default index order
- d_index_order.push_back( i );
- d_var_order[i] = i;
+ d_index_order.push_back( v );
+ d_var_order[v] = v;
//store default domain
d_domain.push_back( RepDomain() );
- TypeNode tn = d_types[i];
- Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl;
+ TypeNode tn = d_types[v];
+ Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl;
if( tn.isSort() ){
//must ensure uninterpreted type is non-empty.
if( !d_rep_set->hasType( tn ) ){
Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
d_rep_set->add( tn, var );
}
- }else if( tn.isInteger() ){
- bool inc = false;
- //check if it is bound
+ }else{
+ bool inc = true;
+ //check if it is bound by bounded integer module
if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
- if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){
+ unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] );
+ if( bvt==quantifiers::BoundedIntegers::BOUND_INT_RANGE ){
Trace("rsi") << " variable is bounded integer." << std::endl;
- d_enum_type.push_back( ENUM_RANGE );
- }else{
- inc = true;
+ d_enum_type.push_back( ENUM_INT_RANGE );
+ inc = false;
+ }else if( bvt==quantifiers::BoundedIntegers::BOUND_SET_MEMBER ){
+ Trace("rsi") << " variable is bounded by set membership." << std::endl;
+ d_enum_type.push_back( ENUM_SET_MEMBERS );
+ inc = false;
}
- }else{
- inc = true;
}
if( inc ){
//check if it is otherwise bound
- if( d_bounds[0].find(i)!=d_bounds[0].end() && d_bounds[1].find(i)!=d_bounds[1].end() ){
+ if( d_bounds[0].find( v )!=d_bounds[0].end() && d_bounds[1].find( v )!=d_bounds[1].end() ){
Trace("rsi") << " variable is bounded." << std::endl;
- d_enum_type.push_back( ENUM_RANGE );
+ d_enum_type.push_back( ENUM_INT_RANGE );
+ }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){
+ Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
+ d_rep_set->complete( tn );
+ //must have succeeded
+ Assert( d_rep_set->hasType( tn ) );
}else{
Trace("rsi") << " variable cannot be bounded." << std::endl;
- Trace("fmf-incomplete") << "Incomplete because of integer quantification of " << d_owner[0][i] << "." << std::endl;
+ Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
d_incomplete = true;
}
}
- //enumerate if the sort is reasonably small
- }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){
- Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
- d_rep_set->complete( tn );
- //must have succeeded
- Assert( d_rep_set->hasType( tn ) );
- }else{
- Trace("rsi") << " variable cannot be bounded." << std::endl;
- Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
- d_incomplete = true;
}
//if we have yet to determine the type of enumeration
- if( d_enum_type.size()<=i ){
+ if( d_enum_type.size()<=v ){
d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
if( d_rep_set->hasType( tn ) ){
- for( size_t j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
- d_domain[i].push_back( j );
+ for( unsigned j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
+ d_domain[v].push_back( j );
}
}else{
+ Assert( d_incomplete );
return false;
}
}
}
//must set a variable index order based on bounded integers
- if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) {
+ if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
std::vector< int > varOrder;
- for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars(d_owner); i++ ){
- varOrder.push_back(d_qe->getBoundedIntegers()->getBoundVarNum(d_owner,i));
+ for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){
+ Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i );
+ Trace("bound-int-rsi") << " bound var #" << i << " is " << v << std::endl;
+ varOrder.push_back( d_qe->getTermDatabase()->getVariableNum( d_owner, v ) );
}
for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) {
if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) {
Trace("bound-int-rsi") << indexOrder[i] << " ";
}
Trace("bound-int-rsi") << std::endl;
- setIndexOrder(indexOrder);
+ setIndexOrder( indexOrder );
}
//now reset the indices
- for (unsigned i=0; i<d_index.size(); i++) {
- if (!resetIndex(i, true)){
- break;
- }
- }
+ do_reset_increment( -1, true );
return true;
}
d_index_order.clear();
d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
//make the d_var_order mapping
- for( int i=0; i<(int)d_index_order.size(); i++ ){
+ for( unsigned i=0; i<d_index_order.size(); i++ ){
d_var_order[d_index_order[i]] = i;
}
}
-/*
-void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
- d_domain.clear();
- d_domain.insert( d_domain.begin(), domain.begin(), domain.end() );
- //we are done if a domain is empty
- for( int i=0; i<(int)d_domain.size(); i++ ){
- if( d_domain[i].empty() ){
- d_index.clear();
- }
- }
-}
-*/
-bool RepSetIterator::resetIndex( int i, bool initial ) {
+
+int RepSetIterator::resetIndex( int i, bool initial ) {
d_index[i] = 0;
- int ii = d_index_order[i];
- Trace("bound-int-rsi") << "Reset " << i << " " << ii << " " << initial << std::endl;
+ int v = d_var_order[i];
+ Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl;
//determine the current range
- if( d_enum_type[ii]==ENUM_RANGE ){
- if( initial || ( d_qe->getBoundedIntegers() && !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ) ){
- Trace("bound-int-rsi") << "Getting range of " << d_owner[0][ii] << std::endl;
+ if( initial || ( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() &&
+ d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) &&
+ !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][v] ) ) ){
+ Trace("bound-int-rsi") << "Getting range of " << d_owner[0][v] << std::endl;
+ if( d_enum_type[v]==ENUM_INT_RANGE ){
Node actual_l;
Node l, u;
- if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){
- d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u );
+ if( d_qe->getBoundedIntegers() ){
+ unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] );
+ if( bvt==quantifiers::BoundedIntegers::BOUND_INT_RANGE ){
+ d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][v], this, l, u );
+ }
}
for( unsigned b=0; b<2; b++ ){
- if( d_bounds[b].find(ii)!=d_bounds[b].end() ){
- Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][ii] << std::endl;
- if( b==0 && (l.isNull() || d_bounds[b][ii].getConst<Rational>() > l.getConst<Rational>()) ){
+ if( d_bounds[b].find(v)!=d_bounds[b].end() ){
+ Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][v] << std::endl;
+ if( b==0 && (l.isNull() || d_bounds[b][v].getConst<Rational>() > l.getConst<Rational>()) ){
if( !l.isNull() ){
//bound was limited externally, record that the value lower bound is not equal to the term lower bound
- actual_l = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii], l );
+ actual_l = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][v], l );
}
- l = d_bounds[b][ii];
- }else if( b==1 && (u.isNull() || d_bounds[b][ii].getConst<Rational>() <= u.getConst<Rational>()) ){
- u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii],
+ l = d_bounds[b][v];
+ }else if( b==1 && (u.isNull() || d_bounds[b][v].getConst<Rational>() <= u.getConst<Rational>()) ){
+ u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][v],
NodeManager::currentNM()->mkConst( Rational(1) ) );
u = Rewriter::rewrite( u );
}
if( l.isNull() || u.isNull() ){
//failed, abort the iterator
- d_index.clear();
- return false;
+ return -1;
}else{
- Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " to " << l << "..." << u << std::endl;
+ Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][v] << " to " << l << "..." << u << std::endl;
Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
- d_domain[ii].clear();
+ d_domain[v].clear();
Node tl = l;
Node tu = u;
- if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){
- d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][ii], this, tl, tu );
+ if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){
+ d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][v], this, tl, tu );
}
- d_lower_bounds[ii] = tl;
+ d_lower_bounds[v] = tl;
if( !actual_l.isNull() ){
//if bound was limited externally, must consider the offset
- d_lower_bounds[ii] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) );
+ d_lower_bounds[v] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) );
}
- if( ra==NodeManager::currentNM()->mkConst(true) ){
+ if( ra==d_qe->getTermDatabase()->d_true ){
long rr = range.getConst<Rational>().getNumerator().getLong()+1;
Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl;
- d_domain[ii].push_back( (int)rr );
+ d_domain[v].push_back( (int)rr );
+ if( rr<=0 ){
+ return 0;
+ }
}else{
- Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][ii] << "." << std::endl;
- d_incomplete = true;
- d_domain[ii].push_back( 0 );
+ Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][v] << "." << std::endl;
+ return -1;
}
}
- }else{
- Trace("bound-int-rsi") << d_owner[0][ii] << " has ground range, skip." << std::endl;
+ }else if( d_enum_type[v]==ENUM_SET_MEMBERS ){
+ Assert( d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] )==quantifiers::BoundedIntegers::BOUND_SET_MEMBER );
+ Node srv = d_qe->getBoundedIntegers()->getSetRangeValue( d_owner, d_owner[0][v], this );
+ if( srv.isNull() ){
+ return -1;
+ }
+ Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl;
+ d_domain[v].clear();
+ d_setm_bounds[v].clear();
+ if( srv.getKind()!=EMPTYSET ){
+ //TODO: need term model, not value model
+ while( srv.getKind()==UNION ){
+ Assert( srv[1].getKind()==kind::SINGLETON );
+ d_setm_bounds[v].push_back( srv[1][0] );
+ srv = srv[0];
+ }
+ d_setm_bounds[v].push_back( srv[0] );
+ d_domain[v].push_back( d_setm_bounds[v].size() );
+ }else{
+ d_domain[v].push_back( 0 );
+ return 0;
+ }
}
}
- return true;
+ return 1;
}
-int RepSetIterator::increment2( int counter ){
+int RepSetIterator::increment2( int i ){
Assert( !isFinished() );
#ifdef DISABLE_EVAL_SKIP_MULTIPLE
- counter = (int)d_index.size()-1;
+ i = (int)d_index.size()-1;
#endif
//increment d_index
- if( counter>=0){
- Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
+ if( i>=0){
+ Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl;
}
- while( counter>=0 && d_index[counter]>=(int)(domainSize(counter)-1) ){
- counter--;
- if( counter>=0){
- Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
+ while( i>=0 && d_index[i]>=(int)(domainSize(i)-1) ){
+ i--;
+ if( i>=0){
+ Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl;
}
}
- if( counter==-1 ){
+ if( i==-1 ){
d_index.clear();
+ return -1;
}else{
- d_index[counter]++;
- bool emptyDomain = false;
- for( int i=(int)d_index.size()-1; i>counter; i-- ){
- if (!resetIndex(i)){
- break;
- }else if( domainSize(i)<=0 ){
- emptyDomain = true;
- }
+ Trace("rsi-debug") << "increment " << i << std::endl;
+ d_index[i]++;
+ return do_reset_increment( i );
+ }
+}
+
+int RepSetIterator::do_reset_increment( int i, bool initial ) {
+ bool emptyDomain = false;
+ for( unsigned ii=(i+1); ii<d_index.size(); ii++ ){
+ int ri_res = resetIndex( ii, initial );
+ if( ri_res==-1 ){
+ //failed
+ d_index.clear();
+ d_incomplete = true;
+ break;
+ }else if( ri_res==0 ){
+ emptyDomain = true;
}
+ //force next iteration if currently an empty domain
if( emptyDomain ){
- Trace("rsi-debug") << "This is an empty domain, increment again." << std::endl;
- return increment();
+ d_index[ii] = domainSize(ii)-1;
}
}
- return counter;
+ if( emptyDomain ){
+ Trace("rsi-debug") << "This is an empty domain, increment." << std::endl;
+ return increment();
+ }else{
+ return i;
+ }
}
int RepSetIterator::increment(){
return d_index.empty();
}
-Node RepSetIterator::getTerm( int i ){
- Trace("rsi-debug") << "rsi : get term " << i << ", index order = " << d_index_order[i] << std::endl;
- //int index = d_index_order[i];
- int index = i;
- if( d_enum_type[index]==ENUM_DOMAIN_ELEMENTS ){
- TypeNode tn = d_types[index];
+Node RepSetIterator::getCurrentTerm( int v ){
+ Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl;
+ int ii = d_index_order[v];
+ int curr = d_index[ii];
+ if( d_enum_type[v]==ENUM_DOMAIN_ELEMENTS ){
+ TypeNode tn = d_types[v];
Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() );
- return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]];
+ Assert( 0<=d_domain[v][curr] && d_domain[v][curr]<(int)d_rep_set->d_type_reps[tn].size() );
+ return d_rep_set->d_type_reps[tn][d_domain[v][curr]];
+ }else if( d_enum_type[v]==ENUM_SET_MEMBERS ){
+ Assert( 0<=curr && curr<(int)d_setm_bounds[v].size() );
+ return d_setm_bounds[v][curr];
}else{
- Trace("rsi-debug") << "Get, with offset : " << index << " " << d_lower_bounds[index] << " " << d_index[index] << std::endl;
- Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index],
- NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) );
+ Trace("rsi-debug") << "Get, with offset : " << v << " " << d_lower_bounds[v] << " " << curr << std::endl;
+ Assert( !d_lower_bounds[v].isNull() );
+ Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[v], NodeManager::currentNM()->mkConst( Rational(curr) ) );
t = Rewriter::rewrite( t );
return t;
}
}
void RepSetIterator::debugPrint( const char* c ){
- for( int i=0; i<(int)d_index.size(); i++ ){
- Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl;
+ for( unsigned v=0; v<d_index.size(); v++ ){
+ Debug( c ) << v << " : " << getCurrentTerm( v ) << std::endl;
}
}
void RepSetIterator::debugPrintSmall( const char* c ){
Debug( c ) << "RI: ";
- for( int i=0; i<(int)d_index.size(); i++ ){
- Debug( c ) << d_index[i] << ": " << getTerm( i ) << " ";
+ for( unsigned v=0; v<d_index.size(); v++ ){
+ Debug( c ) << v << ": " << getCurrentTerm( v ) << " ";
}
Debug( c ) << std::endl;
}
+
public:
enum {
ENUM_DOMAIN_ELEMENTS,
- ENUM_RANGE,
+ ENUM_INT_RANGE,
+ ENUM_SET_MEMBERS,
};
private:
QuantifiersEngine * d_qe;
//initialize function
bool initialize();
- //for enum ranges
+ //for int ranges
std::map< int, Node > d_lower_bounds;
+ //for set ranges
+ std::map< int, std::vector< Node > > d_setm_bounds;
//domain size
int domainSize( int i );
//node this is rep set iterator is for
Node d_owner;
- //reset index
- bool resetIndex( int i, bool initial = false );
+ //reset index, 1:success, 0:empty, -1:fail
+ int resetIndex( int i, bool initial = false );
/** set index order */
void setIndexOrder( std::vector< int >& indexOrder );
+ /** do reset increment the iterator at index=counter */
+ int do_reset_increment( int counter, bool initial = false );
+ //ordering for variables we are indexing over
+ // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
+ // then we consider instantiations in this order:
+ // a/x a/y a/z
+ // a/x b/y a/z
+ // b/x a/y a/z
+ // b/x b/y a/z
+ // ...
+ std::vector< int > d_index_order;
+ //variables to index they are considered at
+ // for example, if d_index_order = { 2, 0, 1 }
+ // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
+ std::map< int, int > d_var_order;
+ //are we only considering a strict subset of the domain of the quantifier?
+ bool d_incomplete;
public:
RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
~RepSetIterator(){}
RepSet* d_rep_set;
//enumeration type?
std::vector< int > d_enum_type;
- //index we are considering
+ //current tuple we are considering
std::vector< int > d_index;
//types we are considering
std::vector< TypeNode > d_types;
//domain we are considering
std::vector< RepDomain > d_domain;
- //are we only considering a strict subset of the domain of the quantifier?
- bool d_incomplete;
- //ordering for variables we are indexing over
- // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
- // then we consider instantiations in this order:
- // a/x a/y a/z
- // a/x b/y a/z
- // b/x a/y a/z
- // b/x b/y a/z
- // ...
- std::vector< int > d_index_order;
- //variables to index they are considered at
- // for example, if d_index_order = { 2, 0, 1 }
- // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
- std::map< int, int > d_var_order;
//intervals
std::map< int, Node > d_bounds[2];
public:
/** increment the iterator at index=counter */
- int increment2( int counter );
+ int increment2( int i );
/** increment the iterator */
int increment();
/** is the iterator finished? */
bool isFinished();
/** get the i_th term we are considering */
- Node getTerm( int i );
+ Node getCurrentTerm( int v );
/** get the number of terms we are considering */
int getNumTerms() { return (int)d_index_order.size(); }
/** debug print */
void debugPrint( const char* c );
void debugPrintSmall( const char* c );
+ //get index order, returns var #
+ int getIndexOrder( int v ) { return d_index_order[v]; }
+ //get variable order, returns index #
+ int getVariableOrder( int i ) { return d_var_order[i]; }
+ //is incomplete
+ bool isIncomplete() { return d_incomplete; }
};/* class RepSetIterator */
}/* CVC4::theory namespace */
}
TheoryStrings::~TheoryStrings() {
-
+ for( std::map< Node, EqcInfo* >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){
+ delete it->second;
+ }
}
Node TheoryStrings::getRepresentative( Node t ) {
ForElimination-scala-9.smt2 \
agree466.smt2 \
LeftistHeap.scala-8-ncm.smt2 \
- sc-crash-052316.smt2
+ sc-crash-052316.smt2 \
+ bound-int-alt.smt2
EXTRA_DIST = $(TESTS)
--- /dev/null
+; COMMAND-LINE: --fmf-bound-int
+; EXPECT: sat
+(set-logic UFLIA)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-sort V 0)
+(declare-fun P (U Int V Int U Int) Bool)
+
+(assert (forall ((x U) (y Int) (z V) (w Int) (v U) (d Int)) (=> (and (<= 0 d 1) (<= 2 y 6) (<= 40 w (+ 37 y))) (P x y z w v d))))
+
+(declare-fun a () U)
+(declare-fun b () V)
+
+(assert (not (P a 2 b 40 a 0)))
+(assert (not (P a 6 b 39 a 0)))
+(assert (not (P a 6 b 44 a 0)))
+
+(check-sat)
projects / cvc5.git / commitdiff