Fix numerous compiler warnings on various platforms

1 files changed, 184 insertions, 184 deletions

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index e278de9e1..107a99014 100755
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -1,184 +1,184 @@
-/*********************                                                        */

-/*! \file bounded_integers.cpp

- ** \verbatim

- ** Original author: Andrew Reynolds

- ** This file is part of the CVC4 project.

- ** Copyright (c) 2009-2013  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief Rewrite engine module

- **

- ** This class manages rewrite rules for quantifiers

- **/

-

-#include "theory/quantifiers/rewrite_engine.h"

-#include "theory/quantifiers/quant_util.h"

-#include "theory/quantifiers/first_order_model.h"

-#include "theory/quantifiers/model_engine.h"

-#include "theory/quantifiers/options.h"

-#include "theory/quantifiers/inst_match_generator.h"

-#include "theory/theory_engine.h"

-

-using namespace CVC4;

-using namespace std;

-using namespace CVC4::theory;

-using namespace CVC4::theory::quantifiers;

-using namespace CVC4::kind;

-

-struct PrioritySort {

-  std::vector< double > d_priority;

-  bool operator() (int i,int j) {

-    return d_priority[i] < d_priority[j];

-  }

-};

-

-

-RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {

-

-}

-

-double RewriteEngine::getPriority( Node f ) {

-  Node rr = f.getAttribute(QRewriteRuleAttribute());

-  Node rrr = rr[2];

-  Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl;

-  bool deterministic = rrr[1].getKind()!=OR;

-  if( rrr.getKind()==RR_REWRITE ){

-    return deterministic ? 0.0 : 3.0;

-  }else if( rrr.getKind()==RR_DEDUCTION ){

-    return deterministic ? 1.0 : 4.0;

-  }else if( rrr.getKind()==RR_REDUCTION ){

-    return deterministic ? 2.0 : 5.0;

-  }else{

-    return 6.0;

-  }

-}

-

-void RewriteEngine::check( Theory::Effort e ) {

-  if( e==Theory::EFFORT_LAST_CALL ){

-    if( !d_quantEngine->getModel()->isModelSet() ){

-      d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true );

-    }

-    if( d_true.isNull() ){

-      d_true = NodeManager::currentNM()->mkConst( true );

-    }

-    std::vector< Node > priority_order;

-    PrioritySort ps;

-    std::vector< int > indicies;

-    for( int i=0; i<(int)d_rr_quant.size(); i++ ){

-      ps.d_priority.push_back( getPriority( d_rr_quant[i] ) );

-      indicies.push_back( i );

-    }

-    std::sort( indicies.begin(), indicies.end(), ps );

-    for( unsigned i=0; i<indicies.size(); i++ ){

-      priority_order.push_back( d_rr_quant[indicies[i]] );

-    }

-

-    //apply rewrite rules

-    int addedLemmas = 0;

-    //per priority level

-    int index = 0;

-    bool success = true;

-    while( success && index<(int)priority_order.size() ) {

-      addedLemmas += checkRewriteRule( priority_order[index] );

-      index++;

-      if( index<(int)priority_order.size() ){

-        success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] );

-      }

-    }

-

-    Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl;

-    if (addedLemmas==0) {

-    }else{

-      //otherwise, the search will continue

-      d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );

-    }

-  }

-}

-

-int RewriteEngine::checkRewriteRule( Node f ) {

-  Trace("rewrite-engine-inst") << "Check " << f << ", priority = " << getPriority( f ) << "..." << std::endl;

-  int addedLemmas = 0;

-  //reset triggers

-  Node rr = f.getAttribute(QRewriteRuleAttribute());

-  if( d_rr_triggers.find(f)==d_rr_triggers.end() ){

-    std::vector< inst::Trigger * > triggers;

-    if( f.getNumChildren()==3 ){

-      for(unsigned i=0; i<f[2].getNumChildren(); i++ ){

-        Node pat = f[2][i];

-        std::vector< Node > nodes;

-        Trace("rewrite-engine-trigger") << "Trigger is : ";

-        for( int j=0; j<(int)pat.getNumChildren(); j++ ){

-          Node p = d_quantEngine->getTermDatabase()->getInstConstantNode( pat[j], f );

-          nodes.push_back( p );

-          Trace("rewrite-engine-trigger") << p << " " << p.getKind() << " ";

-        }

-        Trace("rewrite-engine-trigger") << std::endl;

-        Assert( inst::Trigger::isUsableTrigger( nodes, f ) );

-        inst::Trigger * tr = inst::Trigger::mkTrigger( d_quantEngine, f, nodes, 0, true, inst::Trigger::TR_MAKE_NEW, false );

-        tr->getGenerator()->setActiveAdd(false);

-        triggers.push_back( tr );

-      }

-    }

-    d_rr_triggers[f].insert( d_rr_triggers[f].end(), triggers.begin(), triggers.end() );

-  }

-  for( unsigned i=0; i<d_rr_triggers[f].size(); i++ ){

-    Trace("rewrite-engine-inst") << "Try trigger " << *d_rr_triggers[f][i] << std::endl;

-    d_rr_triggers[f][i]->resetInstantiationRound();

-    d_rr_triggers[f][i]->reset( Node::null() );

-    bool success;

-    do

-    {

-      InstMatch m;

-      success = d_rr_triggers[f][i]->getNextMatch( f, m );

-      if( success ){

-        //see if instantiation is true in the model

-        Node rr = f.getAttribute(QRewriteRuleAttribute());

-        Node rrg = rr[1];

-        std::vector< Node > vars;

-        std::vector< Node > terms;

-        d_quantEngine->computeTermVector( f, m, vars, terms );

-        Trace("rewrite-engine-inst-debug") << "Instantiation : " << m << std::endl;

-        Node inst = d_rr_guard[f];

-        inst = inst.substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );

-        Trace("rewrite-engine-inst-debug") << "Try instantiation, guard : " << inst << std::endl;

-        FirstOrderModel * fm = d_quantEngine->getModel();

-        Node v = fm->getValue( inst );

-        Trace("rewrite-engine-inst-debug") << "Evaluated to " << v << std::endl;

-        if( v==d_true ){

-          Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl;

-          if( d_quantEngine->addInstantiation( f, m ) ){

-            addedLemmas++;

-            Trace("rewrite-engine-inst-debug") << "success" << std::endl;

-            //set the no-match attribute (the term is rewritten and can be ignored)

-            //Trace("rewrite-engine-inst-debug") << "We matched on : " << m.d_matched << std::endl;

-            //if( !m.d_matched.isNull() ){

-            //  NoMatchAttribute nma;

-            //  m.d_matched.setAttribute(nma,true);

-            //}

-          }else{

-            Trace("rewrite-engine-inst-debug") << "failure." << std::endl;

-          }

-        }

-      }

-    }while(success);

-  }

-  Trace("rewrite-engine-inst") << "Rule " << f << " generated " << addedLemmas << " lemmas." << std::endl;

-  return addedLemmas;

-}

-

-void RewriteEngine::registerQuantifier( Node f ) {

-  if( f.hasAttribute(QRewriteRuleAttribute()) ){

-    Trace("rewrite-engine") << "Register quantifier " << f << std::endl;

-    Node rr = f.getAttribute(QRewriteRuleAttribute());

-    Trace("rewrite-engine") << "  rewrite rule is : " << rr << std::endl;

-    d_rr_quant.push_back( f );

-    d_rr_guard[f] = rr[1];

-    Trace("rewrite-engine") << "  guard is : " << d_rr_guard[f] << std::endl;

-  }

-}

-

-void RewriteEngine::assertNode( Node n ) {

-

-}

-

+/*********************                                                        */
+/*! \file bounded_integers.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Rewrite engine module
+ **
+ ** This class manages rewrite rules for quantifiers
+ **/
+
+#include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/inst_match_generator.h"
+#include "theory/theory_engine.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+struct PrioritySort {
+  std::vector< double > d_priority;
+  bool operator() (int i,int j) {
+    return d_priority[i] < d_priority[j];
+  }
+};
+
+
+RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {
+
+}
+
+double RewriteEngine::getPriority( Node f ) {
+  Node rr = f.getAttribute(QRewriteRuleAttribute());
+  Node rrr = rr[2];
+  Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl;
+  bool deterministic = rrr[1].getKind()!=OR;
+  if( rrr.getKind()==RR_REWRITE ){
+    return deterministic ? 0.0 : 3.0;
+  }else if( rrr.getKind()==RR_DEDUCTION ){
+    return deterministic ? 1.0 : 4.0;
+  }else if( rrr.getKind()==RR_REDUCTION ){
+    return deterministic ? 2.0 : 5.0;
+  }else{
+    return 6.0;
+  }
+}
+
+void RewriteEngine::check( Theory::Effort e ) {
+  if( e==Theory::EFFORT_LAST_CALL ){
+    if( !d_quantEngine->getModel()->isModelSet() ){
+      d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true );
+    }
+    if( d_true.isNull() ){
+      d_true = NodeManager::currentNM()->mkConst( true );
+    }
+    std::vector< Node > priority_order;
+    PrioritySort ps;
+    std::vector< int > indicies;
+    for( int i=0; i<(int)d_rr_quant.size(); i++ ){
+      ps.d_priority.push_back( getPriority( d_rr_quant[i] ) );
+      indicies.push_back( i );
+    }
+    std::sort( indicies.begin(), indicies.end(), ps );
+    for( unsigned i=0; i<indicies.size(); i++ ){
+      priority_order.push_back( d_rr_quant[indicies[i]] );
+    }
+
+    //apply rewrite rules
+    int addedLemmas = 0;
+    //per priority level
+    int index = 0;
+    bool success = true;
+    while( success && index<(int)priority_order.size() ) {
+      addedLemmas += checkRewriteRule( priority_order[index] );
+      index++;
+      if( index<(int)priority_order.size() ){
+        success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] );
+      }
+    }
+
+    Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl;
+    if (addedLemmas==0) {
+    }else{
+      //otherwise, the search will continue
+      d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
+    }
+  }
+}
+
+int RewriteEngine::checkRewriteRule( Node f ) {
+  Trace("rewrite-engine-inst") << "Check " << f << ", priority = " << getPriority( f ) << "..." << std::endl;
+  int addedLemmas = 0;
+  //reset triggers
+  Node rr = f.getAttribute(QRewriteRuleAttribute());
+  if( d_rr_triggers.find(f)==d_rr_triggers.end() ){
+    std::vector< inst::Trigger * > triggers;
+    if( f.getNumChildren()==3 ){
+      for(unsigned i=0; i<f[2].getNumChildren(); i++ ){
+        Node pat = f[2][i];
+        std::vector< Node > nodes;
+        Trace("rewrite-engine-trigger") << "Trigger is : ";
+        for( int j=0; j<(int)pat.getNumChildren(); j++ ){
+          Node p = d_quantEngine->getTermDatabase()->getInstConstantNode( pat[j], f );
+          nodes.push_back( p );
+          Trace("rewrite-engine-trigger") << p << " " << p.getKind() << " ";
+        }
+        Trace("rewrite-engine-trigger") << std::endl;
+        Assert( inst::Trigger::isUsableTrigger( nodes, f ) );
+        inst::Trigger * tr = inst::Trigger::mkTrigger( d_quantEngine, f, nodes, 0, true, inst::Trigger::TR_MAKE_NEW, false );
+        tr->getGenerator()->setActiveAdd(false);
+        triggers.push_back( tr );
+      }
+    }
+    d_rr_triggers[f].insert( d_rr_triggers[f].end(), triggers.begin(), triggers.end() );
+  }
+  for( unsigned i=0; i<d_rr_triggers[f].size(); i++ ){
+    Trace("rewrite-engine-inst") << "Try trigger " << *d_rr_triggers[f][i] << std::endl;
+    d_rr_triggers[f][i]->resetInstantiationRound();
+    d_rr_triggers[f][i]->reset( Node::null() );
+    bool success;
+    do
+    {
+      InstMatch m;
+      success = d_rr_triggers[f][i]->getNextMatch( f, m );
+      if( success ){
+        //see if instantiation is true in the model
+        Node rr = f.getAttribute(QRewriteRuleAttribute());
+        Node rrg = rr[1];
+        std::vector< Node > vars;
+        std::vector< Node > terms;
+        d_quantEngine->computeTermVector( f, m, vars, terms );
+        Trace("rewrite-engine-inst-debug") << "Instantiation : " << m << std::endl;
+        Node inst = d_rr_guard[f];
+        inst = inst.substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+        Trace("rewrite-engine-inst-debug") << "Try instantiation, guard : " << inst << std::endl;
+        FirstOrderModel * fm = d_quantEngine->getModel();
+        Node v = fm->getValue( inst );
+        Trace("rewrite-engine-inst-debug") << "Evaluated to " << v << std::endl;
+        if( v==d_true ){
+          Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl;
+          if( d_quantEngine->addInstantiation( f, m ) ){
+            addedLemmas++;
+            Trace("rewrite-engine-inst-debug") << "success" << std::endl;
+            //set the no-match attribute (the term is rewritten and can be ignored)
+            //Trace("rewrite-engine-inst-debug") << "We matched on : " << m.d_matched << std::endl;
+            //if( !m.d_matched.isNull() ){
+            //  NoMatchAttribute nma;
+            //  m.d_matched.setAttribute(nma,true);
+            //}
+          }else{
+            Trace("rewrite-engine-inst-debug") << "failure." << std::endl;
+          }
+        }
+      }
+    }while(success);
+  }
+  Trace("rewrite-engine-inst") << "Rule " << f << " generated " << addedLemmas << " lemmas." << std::endl;
+  return addedLemmas;
+}
+
+void RewriteEngine::registerQuantifier( Node f ) {
+  if( f.hasAttribute(QRewriteRuleAttribute()) ){
+    Trace("rewrite-engine") << "Register quantifier " << f << std::endl;
+    Node rr = f.getAttribute(QRewriteRuleAttribute());
+    Trace("rewrite-engine") << "  rewrite rule is : " << rr << std::endl;
+    d_rr_quant.push_back( f );
+    d_rr_guard[f] = rr[1];
+    Trace("rewrite-engine") << "  guard is : " << d_rr_guard[f] << std::endl;
+  }
+}
+
+void RewriteEngine::assertNode( Node n ) {
+
+}
+