Refactoring of model engine to separate individual implementations of model builder. Begin work on interval models for integers. Other minor cleanup.

1 files changed, 7 insertions, 24 deletions

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index e402a8969..37bf6436b 100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -218,16 +218,22 @@ void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) {
 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() ){

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

       for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){

@@ -248,7 +254,7 @@ void BoundedIntegers::registerQuantifier( Node f ) {
       d_range[f][v] = Rewriter::rewrite( r );

       Trace("bound-int") << "  " << 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() ){

+    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];

@@ -256,29 +262,6 @@ void BoundedIntegers::registerQuantifier( Node f ) {
         if( quantifiers::TermDb::hasBoundVarAttr(r) ){

           //introduce a new bound

           Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" );

-          /*

-          std::vector< Node > bvs;

-          quantifiers::TermDb::getBoundVars(r, bvs);

-          Assert(bvs.size()>0);

-          Node body = NodeManager::currentNM()->mkNode( LEQ, r, new_range );

-          std::vector< Node > children;

-          //get all the other bounds

-          for( unsigned j=0; j<bvs.size(); j++) {

-            Node l = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst(Rational(0)), bvs[j]);

-            Node u = NodeManager::currentNM()->mkNode( LEQ, bvs[j], d_range[f][bvs[j]] );

-            children.push_back(l);

-            children.push_back(u);

-          }

-          Node antec = NodeManager::currentNM()->mkNode( AND, children );

-          body = NodeManager::currentNM()->mkNode( IMPLIES, antec, body );

-

-          Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );

-

-          Node lem = NodeManager::currentNM()->mkNode( FORALL, bvl, body );

-          Trace("bound-int") << "For " << v << ", the quantified formula " << lem << " will be used to minimize the bound." << std::endl;

-          Trace("bound-int-lemma") << " *** bound int: bounding quantified lemma " << lem << std::endl;

-          d_quantEngine->getOutputChannel().lemma( lem );

-          */

           d_nground_range[f][v] = d_range[f][v];

           d_range[f][v] = new_range;

           r = new_range;