Preliminary version of finite model finding over bounded integer quantification. Minor update to casc script.

8 files changed, 275 insertions, 29 deletions

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 );
 };