#!/bin/bash
-cvc4=cvc4
+cvc4=./cvc4
bench="$1"
file=${bench##*/}
#include "theory/arith/options.h"
+#include "theory/quantifiers/bounded_integers.h"
+
#include <stdint.h>
#include <vector>
d_unknownsInARow(0),
d_hasDoneWorkSinceCut(false),
d_learner(u),
+ d_quantEngine(qe),
d_assertionsThatDoNotMatchTheirLiterals(c),
d_nextIntegerCheckVar(0),
d_constantIntegerVariables(c),
Assert(!done());
TNode assertion = get();
+ if( options::finiteModelFind() ){
+ d_quantEngine->getBoundedIntegers()->assertNode(assertion);
+ }
+
Kind simpleKind = Comparison::comparisonKind(assertion);
Constraint constraint = d_constraintDatabase.lookup(assertion);
if(constraint == NullConstraint){
/** Static learner. */
ArithStaticLearner d_learner;
-
+ /** quantifiers engine */
+ QuantifiersEngine * d_quantEngine;
//std::vector<ArithVar> d_pool;
public:
void releaseArithVar(ArithVar v);
\r
#include "theory/quantifiers/bounded_integers.h"\r
#include "theory/quantifiers/quant_util.h"\r
+#include "theory/quantifiers/first_order_model.h"\r
\r
using namespace CVC4;\r
using namespace std;\r
using namespace CVC4::theory::quantifiers;\r
using namespace CVC4::kind;\r
\r
-BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe) : QuantifiersModule(qe){\r
+void BoundedIntegers::RangeModel::initialize() {\r
+ //add initial split lemma\r
+ Node ltr = NodeManager::currentNM()->mkNode( LT, d_range, NodeManager::currentNM()->mkConst( Rational(0) ) );\r
+ ltr = Rewriter::rewrite( ltr );\r
+ Trace("bound-integers-lemma") << " *** bound int: initial split on " << ltr << std::endl;\r
+ d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );\r
+ Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;\r
+ d_range_literal[-1] = ltr_lit;\r
+ d_lit_to_range[ltr_lit] = -1;\r
+ d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;\r
+ //register with bounded integers\r
+ Trace("bound-integers-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl;\r
+ d_bi->addLiteralFromRange(ltr_lit, d_range);\r
+}\r
+\r
+void BoundedIntegers::RangeModel::assertNode(Node n) {\r
+ bool pol = n.getKind()!=NOT;\r
+ Node nlit = n.getKind()==NOT ? n[0] : n;\r
+ if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){\r
+ Trace("bound-integers-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")";\r
+ Trace("bound-integers-assert") << ", found literal " << nlit;\r
+ Trace("bound-integers-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl;\r
+ d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]);\r
+ if( pol!=d_lit_to_pol[nlit] ){\r
+ //check if we need a new split?\r
+ if( !d_has_range ){\r
+ bool needsRange = true;\r
+ for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){\r
+ if( d_range_assertions.find( it->first )==d_range_assertions.end() ){\r
+ needsRange = false;\r
+ break;\r
+ }\r
+ }\r
+ if( needsRange ){\r
+ allocateRange();\r
+ }\r
+ }\r
+ }else{\r
+ if (!d_has_range || d_lit_to_range[nlit]<d_curr_range ){\r
+ Trace("bound-integers-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;\r
+ d_curr_range = d_lit_to_range[nlit];\r
+ }\r
+ //set the range\r
+ d_has_range = true;\r
+ }\r
+ }else{\r
+ Message() << "Could not find literal " << nlit << " for range " << d_range << std::endl;\r
+ exit(0);\r
+ }\r
+}\r
+\r
+void BoundedIntegers::RangeModel::allocateRange() {\r
+ d_curr_max++;\r
+ int newBound = d_curr_max;\r
+ Trace("bound-integers-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;\r
+ //TODO: newBound should be chosen in a smarter way\r
+ Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) );\r
+ ltr = Rewriter::rewrite( ltr );\r
+ Trace("bound-integers-lemma") << " *** bound int: split on " << ltr << std::endl;\r
+ d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );\r
+ Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;\r
+ d_range_literal[newBound] = ltr_lit;\r
+ d_lit_to_range[ltr_lit] = newBound;\r
+ d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;\r
+ //register with bounded integers\r
+ d_bi->addLiteralFromRange(ltr_lit, d_range);\r
+}\r
+\r
+Node BoundedIntegers::RangeModel::getNextDecisionRequest() {\r
+ //request the current cardinality as a decision literal, if not already asserted\r
+ for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){\r
+ int i = it->second;\r
+ if( !d_has_range || i<d_curr_range ){\r
+ Node rn = it->first;\r
+ Assert( !rn.isNull() );\r
+ if( d_range_assertions.find( rn )==d_range_assertions.end() ){\r
+ if (!d_lit_to_pol[it->first]) {\r
+ rn = rn.negate();\r
+ }\r
+ Trace("bound-integers-dec") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl;\r
+ return rn;\r
+ }\r
+ }\r
+ }\r
+ return Node::null();\r
+}\r
+\r
+\r
+BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) :\r
+QuantifiersModule(qe), d_assertions(c){\r
+\r
+}\r
\r
+bool BoundedIntegers::isBound( Node f, Node v ) {\r
+ return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();\r
+}\r
+\r
+bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {\r
+ if( b.getKind()==BOUND_VARIABLE ){\r
+ if( isBound( f, b ) ){\r
+ return true;\r
+ }\r
+ }else{\r
+ for( unsigned i=0; i<b.getNumChildren(); i++ ){\r
+ if( hasNonBoundVar( f, b[i] ) ){\r
+ return true;\r
+ }\r
+ }\r
+ }\r
+ return false;\r
}\r
\r
void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {\r
if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){\r
std::map< Node, Node > msum;\r
if (QuantArith::getMonomialSumLit( lit, msum )){\r
- Trace("bound-integers") << "Literal " << lit << " is monomial sum : " << std::endl;\r
+ Trace("bound-integers") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;\r
for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){\r
Trace("bound-integers") << " ";\r
if( !it->second.isNull() ){\r
if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){\r
Node veq;\r
if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){\r
- Trace("bound-integers") << "Isolated for " << it->first << " : " << veq << std::endl;\r
+ Node n1 = veq[0];\r
+ Node n2 = veq[1];\r
+ if(pol){\r
+ //flip\r
+ n1 = veq[1];\r
+ n2 = veq[0];\r
+ if( n1.getKind()==BOUND_VARIABLE ){\r
+ n2 = QuantArith::offset( n2, 1 );\r
+ }else{\r
+ n1 = QuantArith::offset( n1, -1 );\r
+ }\r
+ veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );\r
+ }\r
+ Trace("bound-integers") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;\r
+ Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2;\r
+ if( !isBound( f, bv ) ){\r
+ if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) {\r
+ Trace("bound-integers") << "The bound is relevant." << std::endl;\r
+ d_bounds[n1.getKind()==BOUND_VARIABLE ? 0 : 1][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);\r
+ }\r
+ }\r
}\r
}\r
}\r
\r
}\r
\r
+\r
+void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) {\r
+ d_lit_to_ranges[lit].push_back(r);\r
+ //check if it is already asserted?\r
+ if(d_assertions.find(lit)!=d_assertions.end()){\r
+ d_rms[r]->assertNode( d_assertions[lit] ? lit : lit.negate() );\r
+ }\r
+}\r
+\r
void BoundedIntegers::registerQuantifier( Node f ) {\r
Trace("bound-integers") << "Register quantifier " << f << std::endl;\r
bool hasIntType = false;\r
}\r
}\r
if( hasIntType ){\r
- process( f, f[1], true );\r
+ bool success;\r
+ do{\r
+ success = false;\r
+ process( f, f[1], true );\r
+ for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){\r
+ Node v = it->first;\r
+ if( !isBound(f,v) ){\r
+ if( d_bounds[1][f].find(v)!=d_bounds[1][f].end() ){\r
+ d_set[f].push_back(v);\r
+ success = true;\r
+ }\r
+ }\r
+ }\r
+ }while( success );\r
+ Trace("bound-integers") << "Bounds are : " << std::endl;\r
+ for( unsigned i=0; i<d_set[f].size(); i++) {\r
+ Node v = d_set[f][i];\r
+ Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );\r
+ d_range[f][v] = Rewriter::rewrite( r );\r
+ Trace("bound-integers") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;\r
+ }\r
+ if( d_set[f].size()==f[0].getNumChildren() ){\r
+ d_bound_quants.push_back( f );\r
+ for( unsigned i=0; i<d_set[f].size(); i++) {\r
+ Node v = d_set[f][i];\r
+ Node r = d_range[f][v];\r
+ if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){\r
+ d_ranges.push_back( r );\r
+ d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );\r
+ d_rms[r]->initialize();\r
+ }\r
+ }\r
+ }\r
}\r
}\r
\r
void BoundedIntegers::assertNode( Node n ) {\r
-\r
+ Trace("bound-integers-assert") << "Assert " << n << std::endl;\r
+ Node nlit = n.getKind()==NOT ? n[0] : n;\r
+ if( d_lit_to_ranges.find(nlit)!=d_lit_to_ranges.end() ){\r
+ Trace("bound-integers-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl;\r
+ for( unsigned i=0; i<d_lit_to_ranges[nlit].size(); i++) {\r
+ Node r = d_lit_to_ranges[nlit][i];\r
+ Trace("bound-integers-assert") << " ...this is a bounding literal for " << r << std::endl;\r
+ d_rms[r]->assertNode( n );\r
+ }\r
+ }\r
+ d_assertions[nlit] = n.getKind()!=NOT;\r
}\r
\r
Node BoundedIntegers::getNextDecisionRequest() {\r
+ Trace("bound-integers-dec") << "bi: Get next decision request?" << std::endl;\r
+ for( unsigned i=0; i<d_ranges.size(); i++) {\r
+ Node d = d_rms[d_ranges[i]]->getNextDecisionRequest();\r
+ if (!d.isNull()) {\r
+ return d;\r
+ }\r
+ }\r
return Node::null();\r
}\r
+\r
+\r
+Node BoundedIntegers::getValueInModel( Node n ) {\r
+ return d_quantEngine->getModel()->getValue( n );\r
+}
\ No newline at end of file
\r
#include "theory/quantifiers_engine.h"\r
\r
+#include "context/context.h"\r
+#include "context/context_mm.h"\r
+#include "context/cdchunk_list.h"\r
+\r
namespace CVC4 {\r
namespace theory {\r
namespace quantifiers {\r
\r
class BoundedIntegers : public QuantifiersModule\r
{\r
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;\r
+ typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;\r
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;\r
private:\r
- std::map< Node, std::map< Node, Node > > d_lowers;\r
- std::map< Node, std::map< Node, Node > > d_uppers;\r
- std::map< Node, std::map< Node, bool > > d_set;\r
+ //for determining bounds\r
+ bool isBound( Node f, Node v );\r
+ bool hasNonBoundVar( Node f, Node b );\r
+ std::map< Node, std::map< Node, Node > > d_bounds[2];\r
+ std::map< Node, std::vector< Node > > d_set;\r
+ std::map< Node, std::map< Node, Node > > d_range;\r
void hasFreeVar( Node f, Node n );\r
void process( Node f, Node n, bool pol );\r
void processLiteral( Node f, Node lit, bool pol );\r
+ std::vector< Node > d_bound_quants;\r
+private:\r
+ class RangeModel {\r
+ private:\r
+ BoundedIntegers * d_bi;\r
+ void allocateRange();\r
+ public:\r
+ RangeModel(BoundedIntegers * bi, Node r, context::Context* c) : d_bi(bi),\r
+ d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) {}\r
+ Node d_range;\r
+ int d_curr_max;\r
+ std::map< int, Node > d_range_literal;\r
+ std::map< Node, bool > d_lit_to_pol;\r
+ std::map< Node, int > d_lit_to_range;\r
+ NodeBoolMap d_range_assertions;\r
+ context::CDO< bool > d_has_range;\r
+ context::CDO< int > d_curr_range;\r
+ void initialize();\r
+ void assertNode(Node n);\r
+ Node getNextDecisionRequest();\r
+ };\r
+ Node getValueInModel( Node n );\r
+private:\r
+ //information for minimizing ranges\r
+ std::vector< Node > d_ranges;\r
+ //map to range model objects\r
+ std::map< Node, RangeModel * > d_rms;\r
+ //literal to range\r
+ std::map< Node, std::vector< Node > > d_lit_to_ranges;\r
+ //list of currently asserted arithmetic literals\r
+ NodeBoolMap d_assertions;\r
+private:\r
+ void addLiteralFromRange( Node lit, Node r );\r
public:\r
- BoundedIntegers( QuantifiersEngine* qe );\r
+ BoundedIntegers( context::Context* c, QuantifiersEngine* qe );\r
\r
void check( Theory::Effort e );\r
void registerQuantifier( Node f );\r
void assertNode( Node n );\r
Node getNextDecisionRequest();\r
+ Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; }\r
+ Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; }\r
+ Node getLowerBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[0][f][v] ); }\r
+ Node getUpperBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[1][f][v] ); }\r
};\r
\r
}\r
Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";\r
debugPrintCond("fmc-exh", c, true);\r
Trace("fmc-exh")<< std::endl;\r
- if( riter.setQuantifier( f ) ){\r
+ if( riter.setQuantifier( d_qe, f ) ){\r
std::vector< RepDomain > dom;\r
for (unsigned i=0; i<c.getNumChildren(); i++) {\r
TypeNode tn = c[i].getType();\r
if( d_rep_ids.find(tn)!=d_rep_ids.end() ){\r
- RepDomain rd;\r
+ //RepDomain rd;\r
if( isStar(c[i]) ){\r
//add the full range\r
- for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();\r
- it != d_rep_ids[tn].end(); ++it ){\r
- rd.push_back(it->second);\r
- }\r
+ //for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();\r
+ // it != d_rep_ids[tn].end(); ++it ){\r
+ // rd.push_back(it->second);\r
+ //}\r
}else{\r
if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {\r
- rd.push_back(d_rep_ids[tn][c[i]]);\r
+ //rd.push_back(d_rep_ids[tn][c[i]]);\r
+ riter.d_domain[i].clear();\r
+ riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);\r
}else{\r
return -1;\r
}\r
}\r
- dom.push_back(rd);\r
+ //dom.push_back(rd);\r
}else{\r
return -1;\r
}\r
}\r
- riter.setDomain(dom);\r
+ //riter.setDomain(dom);\r
//now do full iteration\r
while( !riter.isFinished() ){\r
Trace("fmc-exh-debug") << "Inst : ";\r
vars.push_back( f[0][j] );
}
RepSetIterator riter( &(fm->d_rep_set) );
- riter.setQuantifier( f );
+ riter.setQuantifier( d_qe, f );
while( !riter.isFinished() ){
std::vector< Node > terms;
for( int i=0; i<riter.getNumTerms(); i++ ){
}
//if we need to consider this quantifier on this iteration
if( checkQuant ){
- addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain(), e );
+ addedLemmas += exhaustiveInstantiate( f, e );
if( Trace.isOn("model-engine-warn") ){
if( addedLemmas>10000 ){
Debug("fmf-exit") << std::endl;
return addedLemmas;
}
-int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain, int effort ){
+int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
int addedLemmas = 0;
bool useModel = d_builder->optUseModel();
Debug("inst-fmf-ei") << std::endl;
//create a rep set iterator and iterate over the (relevant) domain of the quantifier
RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
- if( riter.setQuantifier( f ) ){
- Debug("inst-fmf-ei") << "Set domain..." << std::endl;
- //set the domain for the iterator (the sufficient set of instantiations to try)
- if( useRelInstDomain ){
- riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
- }
+ if( riter.setQuantifier( d_quantEngine, f ) ){
Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
d_quantEngine->getModel()->resetEvaluate();
Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
int tests = 0;
int triedLemmas = 0;
while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
+ for( int i=0; i<(int)riter.d_index.size(); i++ ){
+ Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl;
+ }
d_testLemmas++;
int eval = 0;
int depIndex;
//check model
int checkModel( int checkOption );
//exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
- int exhaustiveInstantiate( Node f, bool useRelInstDomain = false, int effort = 0 );
+ int exhaustiveInstantiate( Node f, int effort = 0 );
private:
//temporary statistics
int d_triedLemmas;
Rational r = msum[v].isNull() ? Rational(1) : msum[v].getConst<Rational>();
if ( r.sgn()!=0 ){
for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
- if( it->first!=v ){
+ if( it->first.isNull() || it->first!=v ){
Node m;
if( !it->first.isNull() ){
if ( !it->second.isNull() ){
return tt;
}
+Node QuantArith::offset( Node t, int i ) {
+ Node tt = NodeManager::currentNM()->mkNode( PLUS, NodeManager::currentNM()->mkConst( Rational(i) ), t );
+ tt = Rewriter::rewrite( tt );
+ return tt;
+}
+
void QuantRelevance::registerQuantifier( Node f ){
//compute symbols in f
static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum );
static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k );
static Node negate( Node t );
+ static Node offset( Node t, int i );
};
d_model_engine = new quantifiers::ModelEngine( c, this );
d_modules.push_back( d_model_engine );
- d_bint = new quantifiers::BoundedIntegers( this );
+ d_bint = new quantifiers::BoundedIntegers( c, this );
d_modules.push_back( d_bint );
}else{
d_model_engine = NULL;
void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
/** get efficient e-matching utility */
EfficientEMatcher* getEfficientEMatcher() { return d_eem; }
+ /** get bounded integers utility */
+ quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
public:
/** initialize */
void finishInit();
#include "theory/rep_set.h"
#include "theory/type_enumerator.h"
+#include "theory/quantifiers/bounded_integers.h"
using namespace std;
using namespace CVC4;
}
-bool RepSetIterator::setQuantifier( Node f ){
+int RepSetIterator::domainSize( int i ) {
+ if( d_enum_type[i]==ENUM_DOMAIN_ELEMENTS ){
+ return d_domain[i].size();
+ }else{
+ return d_domain[i][0];
+ }
+}
+
+bool RepSetIterator::setQuantifier( QuantifiersEngine * qe, Node f ){
Assert( d_types.empty() );
//store indicies
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
d_types.push_back( f[0][i].getType() );
}
- return initialize();
+ return initialize(qe, f);
}
-bool RepSetIterator::setFunctionDomain( Node op ){
+bool RepSetIterator::setFunctionDomain( QuantifiersEngine * qe, Node op ){
Assert( d_types.empty() );
TypeNode tn = op.getType();
for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
d_types.push_back( tn[i] );
}
- return initialize();
+ return initialize(qe, Node::null());
}
-bool RepSetIterator::initialize(){
+bool RepSetIterator::initialize(QuantifiersEngine * qe, Node f){
for( size_t i=0; i<d_types.size(); i++ ){
d_index.push_back( 0 );
//store default index order
//store default domain
d_domain.push_back( RepDomain() );
TypeNode tn = d_types[i];
+ bool isSet = false;
if( tn.isSort() ){
if( !d_rep_set->hasType( tn ) ){
Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" );
Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
d_rep_set->add( var );
}
- }else if( tn.isInteger() || tn.isReal() ){
+ }else if( tn.isInteger() ){
+ //check if it is bound
+ if( !f.isNull() && qe && qe->getBoundedIntegers() ){
+ Node l = qe->getBoundedIntegers()->getLowerBoundValue( f, f[0][i] );
+ Node u = qe->getBoundedIntegers()->getUpperBoundValue( f, f[0][i] );
+ if( !l.isNull() && !u.isNull() ){
+ Trace("bound-int-reps") << "Can limit bounds of " << f[0][i] << " 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 ) ) ) );
+ if( ra==NodeManager::currentNM()->mkConst(true) ){
+ long rr = range.getConst<Rational>().getNumerator().getLong()+1;
+ if (rr<0) {
+ Trace("bound-int-reps") << "Empty bound range." << std::endl;
+ //empty
+ d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
+ }else{
+ Trace("bound-int-reps") << "Actual bound range is " << rr << std::endl;
+ d_lower_bounds[i] = l;
+ d_domain[i].push_back( (int)rr );
+ d_enum_type.push_back( ENUM_RANGE );
+ }
+ isSet = true;
+ }else{
+ Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big." << std::endl;
+ d_incomplete = true;
+ }
+ }else{
+ Trace("fmf-incomplete") << "Incomplete because of integer quantification, no bounds found." << std::endl;
+ d_incomplete = true;
+ }
+ }else{
+ Trace("fmf-incomplete") << "Incomplete because of integer quantification." << std::endl;
+ d_incomplete = true;
+ }
+ }else if( tn.isReal() ){
Trace("fmf-incomplete") << "Incomplete because of infinite type " << tn << std::endl;
d_incomplete = true;
//enumerate if the sort is reasonably small, the upper bound of 128 is chosen arbitrarily for now
Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;
d_incomplete = true;
}
- 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 );
+ if( !isSet ){
+ 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 );
+ }
+ }else{
+ return false;
}
- }else{
- return false;
}
}
return true;
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() );
}
}
}
-
+*/
void RepSetIterator::increment2( int counter ){
Assert( !isFinished() );
#ifdef DISABLE_EVAL_SKIP_MULTIPLE
counter = (int)d_index.size()-1;
#endif
//increment d_index
- while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){
+ while( counter>=0 && d_index[counter]==(int)(domainSize(counter)-1) ){
counter--;
}
if( counter==-1 ){
}
Node RepSetIterator::getTerm( int i ){
- TypeNode tn = d_types[d_index_order[i]];
- Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() );
int index = d_index_order[i];
- return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]];
+ if( d_enum_type[index]==ENUM_DOMAIN_ELEMENTS ){
+ TypeNode tn = d_types[index];
+ 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]]];
+ }else{
+ Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index],
+ NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) );
+ t = Rewriter::rewrite( t );
+ return t;
+ }
}
void RepSetIterator::debugPrint( const char* c ){
namespace CVC4 {
namespace theory {
+class QuantifiersEngine;
+
/** this class stores a representative set */
class RepSet {
public:
/** this class iterates over a RepSet */
class RepSetIterator {
private:
+ enum {
+ ENUM_DOMAIN_ELEMENTS,
+ ENUM_RANGE,
+ };
+
//initialize function
- bool initialize();
+ bool initialize(QuantifiersEngine * qe, Node f);
+ //enumeration type?
+ std::vector< int > d_enum_type;
+ //for enum ranges
+ std::map< int, Node > d_lower_bounds;
+ //domain size
+ int domainSize( int i );
public:
RepSetIterator( RepSet* rs );
~RepSetIterator(){}
//set that this iterator will be iterating over instantiations for a quantifier
- bool setQuantifier( Node f );
+ bool setQuantifier( QuantifiersEngine * qe, Node f );
//set that this iterator will be iterating over the domain of a function
- bool setFunctionDomain( Node op );
+ bool setFunctionDomain( QuantifiersEngine * qe, Node op );
public:
//pointer to model
RepSet* d_rep_set;
/** set index order */
void setIndexOrder( std::vector< int >& indexOrder );
/** set domain */
- void setDomain( std::vector< RepDomain >& domain );
+ //void setDomain( std::vector< RepDomain >& domain );
/** increment the iterator at index=counter */
void increment2( int counter );
/** increment the iterator */
projects / cvc5.git / commitdiff