summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/theory_arith_private.cpp7
-rw-r--r--src/theory/arith/theory_arith_private.h3
-rwxr-xr-xsrc/theory/quantifiers/bounded_integers.cpp202
-rwxr-xr-xsrc/theory/quantifiers/bounded_integers.h55
-rwxr-xr-xsrc/theory/quantifiers/full_model_check.cpp20
-rw-r--r--src/theory/quantifiers/model_builder.cpp2
-rw-r--r--src/theory/quantifiers/model_engine.cpp14
-rw-r--r--src/theory/quantifiers/model_engine.h2
-rw-r--r--src/theory/quantifiers/quant_util.cpp8
-rw-r--r--src/theory/quantifiers/quant_util.h1
-rw-r--r--src/theory/quantifiers_engine.cpp2
-rw-r--r--src/theory/quantifiers_engine.h2
-rw-r--r--src/theory/rep_set.cpp88
-rw-r--r--src/theory/rep_set.h21
14 files changed, 375 insertions, 52 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index d911ecf77..060f6dbba 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -67,6 +67,8 @@
#include "theory/arith/options.h"
+#include "theory/quantifiers/bounded_integers.h"
+
#include <stdint.h>
#include <vector>
@@ -89,6 +91,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
d_unknownsInARow(0),
d_hasDoneWorkSinceCut(false),
d_learner(u),
+ d_quantEngine(qe),
d_assertionsThatDoNotMatchTheirLiterals(c),
d_nextIntegerCheckVar(0),
d_constantIntegerVariables(c),
@@ -1373,6 +1376,10 @@ Constraint TheoryArithPrivate::constraintFromFactQueue(){
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){
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 2ea3bb68e..86c8e213e 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -132,7 +132,8 @@ private:
/** Static learner. */
ArithStaticLearner d_learner;
-
+ /** quantifiers engine */
+ QuantifiersEngine * d_quantEngine;
//std::vector<ArithVar> d_pool;
public:
void releaseArithVar(ArithVar v);
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 03a52539e..a9eb72b03 100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -14,6 +14,7 @@
#include "theory/quantifiers/bounded_integers.h"
#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/first_order_model.h"
using namespace CVC4;
using namespace std;
@@ -21,15 +22,123 @@ using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
using namespace CVC4::kind;
-BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe) : QuantifiersModule(qe){
+void BoundedIntegers::RangeModel::initialize() {
+ //add initial split lemma
+ Node ltr = NodeManager::currentNM()->mkNode( LT, d_range, NodeManager::currentNM()->mkConst( Rational(0) ) );
+ ltr = Rewriter::rewrite( ltr );
+ Trace("bound-integers-lemma") << " *** bound int: initial split on " << ltr << std::endl;
+ d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );
+ Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;
+ d_range_literal[-1] = ltr_lit;
+ d_lit_to_range[ltr_lit] = -1;
+ d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;
+ //register with bounded integers
+ Trace("bound-integers-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl;
+ d_bi->addLiteralFromRange(ltr_lit, d_range);
+}
+
+void BoundedIntegers::RangeModel::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() ){
+ Trace("bound-integers-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")";
+ Trace("bound-integers-assert") << ", found literal " << nlit;
+ Trace("bound-integers-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl;
+ d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]);
+ if( pol!=d_lit_to_pol[nlit] ){
+ //check if we need a new split?
+ if( !d_has_range ){
+ bool needsRange = true;
+ for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
+ if( d_range_assertions.find( it->first )==d_range_assertions.end() ){
+ needsRange = false;
+ break;
+ }
+ }
+ if( needsRange ){
+ allocateRange();
+ }
+ }
+ }else{
+ if (!d_has_range || d_lit_to_range[nlit]<d_curr_range ){
+ Trace("bound-integers-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;
+ d_curr_range = d_lit_to_range[nlit];
+ }
+ //set the range
+ d_has_range = true;
+ }
+ }else{
+ Message() << "Could not find literal " << nlit << " for range " << d_range << std::endl;
+ exit(0);
+ }
+}
+
+void BoundedIntegers::RangeModel::allocateRange() {
+ d_curr_max++;
+ int newBound = d_curr_max;
+ Trace("bound-integers-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;
+ //TODO: newBound should be chosen in a smarter way
+ Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) );
+ ltr = Rewriter::rewrite( ltr );
+ Trace("bound-integers-lemma") << " *** bound int: split on " << ltr << std::endl;
+ d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );
+ Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;
+ d_range_literal[newBound] = ltr_lit;
+ d_lit_to_range[ltr_lit] = newBound;
+ d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;
+ //register with bounded integers
+ d_bi->addLiteralFromRange(ltr_lit, d_range);
+}
+
+Node BoundedIntegers::RangeModel::getNextDecisionRequest() {
+ //request the current cardinality as a decision literal, if not already asserted
+ for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
+ int i = it->second;
+ if( !d_has_range || i<d_curr_range ){
+ Node rn = it->first;
+ Assert( !rn.isNull() );
+ if( d_range_assertions.find( rn )==d_range_assertions.end() ){
+ if (!d_lit_to_pol[it->first]) {
+ rn = rn.negate();
+ }
+ Trace("bound-integers-dec") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl;
+ return rn;
+ }
+ }
+ }
+ return Node::null();
+}
+
+
+BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) :
+QuantifiersModule(qe), d_assertions(c){
+
+}
+bool BoundedIntegers::isBound( Node f, Node v ) {
+ return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();
+}
+
+bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
+ if( b.getKind()==BOUND_VARIABLE ){
+ if( isBound( f, b ) ){
+ return true;
+ }
+ }else{
+ for( unsigned i=0; i<b.getNumChildren(); i++ ){
+ if( hasNonBoundVar( f, b[i] ) ){
+ return true;
+ }
+ }
+ }
+ return false;
}
void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){
std::map< Node, Node > msum;
if (QuantArith::getMonomialSumLit( lit, msum )){
- Trace("bound-integers") << "Literal " << lit << " is monomial sum : " << std::endl;
+ Trace("bound-integers") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
Trace("bound-integers") << " ";
if( !it->second.isNull() ){
@@ -48,7 +157,27 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){
Node veq;
if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){
- Trace("bound-integers") << "Isolated for " << it->first << " : " << veq << std::endl;
+ 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-integers") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
+ Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2;
+ if( !isBound( f, bv ) ){
+ if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) {
+ Trace("bound-integers") << "The bound is relevant." << std::endl;
+ d_bounds[n1.getKind()==BOUND_VARIABLE ? 0 : 1][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);
+ }
+ }
}
}
}
@@ -76,6 +205,15 @@ void BoundedIntegers::check( Theory::Effort e ) {
}
+
+void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) {
+ d_lit_to_ranges[lit].push_back(r);
+ //check if it is already asserted?
+ if(d_assertions.find(lit)!=d_assertions.end()){
+ d_rms[r]->assertNode( d_assertions[lit] ? lit : lit.negate() );
+ }
+}
+
void BoundedIntegers::registerQuantifier( Node f ) {
Trace("bound-integers") << "Register quantifier " << f << std::endl;
bool hasIntType = false;
@@ -86,14 +224,68 @@ void BoundedIntegers::registerQuantifier( Node f ) {
}
}
if( hasIntType ){
- process( f, f[1], true );
+ bool success;
+ do{
+ success = false;
+ process( f, f[1], true );
+ 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);
+ success = true;
+ }
+ }
+ }
+ }while( success );
+ Trace("bound-integers") << "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 );
+ Trace("bound-integers") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
+ }
+ if( d_set[f].size()==f[0].getNumChildren() ){
+ 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( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){
+ d_ranges.push_back( r );
+ d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );
+ d_rms[r]->initialize();
+ }
+ }
+ }
}
}
void BoundedIntegers::assertNode( Node n ) {
-
+ Trace("bound-integers-assert") << "Assert " << n << std::endl;
+ Node nlit = n.getKind()==NOT ? n[0] : n;
+ if( d_lit_to_ranges.find(nlit)!=d_lit_to_ranges.end() ){
+ Trace("bound-integers-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl;
+ for( unsigned i=0; i<d_lit_to_ranges[nlit].size(); i++) {
+ Node r = d_lit_to_ranges[nlit][i];
+ Trace("bound-integers-assert") << " ...this is a bounding literal for " << r << std::endl;
+ d_rms[r]->assertNode( n );
+ }
+ }
+ d_assertions[nlit] = n.getKind()!=NOT;
}
Node BoundedIntegers::getNextDecisionRequest() {
+ Trace("bound-integers-dec") << "bi: Get next decision request?" << std::endl;
+ for( unsigned i=0; i<d_ranges.size(); i++) {
+ Node d = d_rms[d_ranges[i]]->getNextDecisionRequest();
+ if (!d.isNull()) {
+ return d;
+ }
+ }
return Node::null();
}
+
+
+Node BoundedIntegers::getValueInModel( Node n ) {
+ return d_quantEngine->getModel()->getValue( n );
+} \ No newline at end of file
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 570e27a10..4445493c9 100755
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -18,26 +18,73 @@
#include "theory/quantifiers_engine.h"
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdchunk_list.h"
+
namespace CVC4 {
namespace theory {
namespace quantifiers {
class BoundedIntegers : public QuantifiersModule
{
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+ typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
private:
- std::map< Node, std::map< Node, Node > > d_lowers;
- std::map< Node, std::map< Node, Node > > d_uppers;
- std::map< Node, std::map< Node, bool > > d_set;
+ //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];
+ std::map< Node, std::vector< Node > > d_set;
+ std::map< Node, std::map< Node, Node > > d_range;
void hasFreeVar( Node f, Node n );
void process( Node f, Node n, bool pol );
void processLiteral( Node f, Node lit, bool pol );
+ std::vector< Node > d_bound_quants;
+private:
+ class RangeModel {
+ private:
+ BoundedIntegers * d_bi;
+ void allocateRange();
+ public:
+ RangeModel(BoundedIntegers * bi, Node r, context::Context* c) : d_bi(bi),
+ d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) {}
+ Node d_range;
+ int d_curr_max;
+ std::map< int, Node > d_range_literal;
+ std::map< Node, bool > d_lit_to_pol;
+ std::map< Node, int > d_lit_to_range;
+ NodeBoolMap d_range_assertions;
+ context::CDO< bool > d_has_range;
+ context::CDO< int > d_curr_range;
+ void initialize();
+ void assertNode(Node n);
+ Node getNextDecisionRequest();
+ };
+ Node getValueInModel( Node n );
+private:
+ //information for minimizing ranges
+ std::vector< Node > d_ranges;
+ //map to range model objects
+ std::map< Node, RangeModel * > d_rms;
+ //literal to range
+ std::map< Node, std::vector< Node > > d_lit_to_ranges;
+ //list of currently asserted arithmetic literals
+ NodeBoolMap d_assertions;
+private:
+ void addLiteralFromRange( Node lit, Node r );
public:
- BoundedIntegers( QuantifiersEngine* qe );
+ BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
void check( Theory::Effort e );
void registerQuantifier( Node f );
void assertNode( Node n );
Node getNextDecisionRequest();
+ Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; }
+ Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; }
+ Node getLowerBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[0][f][v] ); }
+ Node getUpperBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[1][f][v] ); }
};
}
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 4ce9dba21..4904368a2 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -535,31 +535,33 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c
Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
debugPrintCond("fmc-exh", c, true);
Trace("fmc-exh")<< std::endl;
- if( riter.setQuantifier( f ) ){
+ if( riter.setQuantifier( d_qe, f ) ){
std::vector< RepDomain > dom;
for (unsigned i=0; i<c.getNumChildren(); i++) {
TypeNode tn = c[i].getType();
if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
- RepDomain rd;
+ //RepDomain rd;
if( isStar(c[i]) ){
//add the full range
- for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();
- it != d_rep_ids[tn].end(); ++it ){
- rd.push_back(it->second);
- }
+ //for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();
+ // it != d_rep_ids[tn].end(); ++it ){
+ // rd.push_back(it->second);
+ //}
}else{
if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
- rd.push_back(d_rep_ids[tn][c[i]]);
+ //rd.push_back(d_rep_ids[tn][c[i]]);
+ riter.d_domain[i].clear();
+ riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
}else{
return -1;
}
}
- dom.push_back(rd);
+ //dom.push_back(rd);
}else{
return -1;
}
}
- riter.setDomain(dom);
+ //riter.setDomain(dom);
//now do full iteration
while( !riter.isFinished() ){
Trace("fmc-exh-debug") << "Inst : ";
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 25e07de5d..677f0c94b 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -69,7 +69,7 @@ void ModelEngineBuilder::debugModel( FirstOrderModel* fm ){
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++ ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 90b8c62ba..bc900d9a9 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -216,7 +216,7 @@ int ModelEngine::checkModel( int checkOption ){
}
//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;
@@ -241,7 +241,7 @@ int ModelEngine::checkModel( int checkOption ){
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();
@@ -263,18 +263,16 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain, int effor
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;
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index d2cd8807a..d88a36d01 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -54,7 +54,7 @@ private:
//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;
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 6b07a87e0..53f67853b 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -71,7 +71,7 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
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() ){
@@ -111,6 +111,12 @@ Node QuantArith::negate( Node t ) {
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
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index d248a8999..86c7bc3a0 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -36,6 +36,7 @@ public:
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 );
};
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 5c24f89b7..ef8169433 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -62,7 +62,7 @@ d_lemmas_produced_c(u){
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;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 85da53087..2ff2100b2 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -158,6 +158,8 @@ public:
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();
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index f6da32bbf..fe3e39d45 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -14,6 +14,7 @@
#include "theory/rep_set.h"
#include "theory/type_enumerator.h"
+#include "theory/quantifiers/bounded_integers.h"
using namespace std;
using namespace CVC4;
@@ -99,25 +100,33 @@ RepSetIterator::RepSetIterator( RepSet* rs ) : d_rep_set( rs ){
}
-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
@@ -126,13 +135,48 @@ bool RepSetIterator::initialize(){
//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
@@ -142,12 +186,15 @@ bool RepSetIterator::initialize(){
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;
@@ -161,7 +208,7 @@ void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
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() );
@@ -172,14 +219,14 @@ void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
}
}
}
-
+*/
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 ){
@@ -203,10 +250,17 @@ bool RepSetIterator::isFinished(){
}
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 ){
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 24fa7473e..b92d9d2c6 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -23,6 +23,8 @@
namespace CVC4 {
namespace theory {
+class QuantifiersEngine;
+
/** this class stores a representative set */
class RepSet {
public:
@@ -53,15 +55,26 @@ typedef std::vector< int > RepDomain;
/** 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;
@@ -90,7 +103,7 @@ public:
/** 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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback