From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 13 Aug 2013 21:58:30 +0000 (-0400)
Subject: Minor cleanup.
X-Git-Tag: cvc5-1.0.0~7287^2~36
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1af67a61059009407dd9833b126581d2c5e5c662;p=cvc5.git

Minor cleanup.
---

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index ce03a1877..a0b195a9c 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -1,4 +1,3 @@
-
 /*********************                                                        */
 /*! \file full_model_check.cpp
  ** \verbatim
@@ -553,7 +552,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
 
 void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){
   if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){
-    Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl;
+    Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl;
     Node mbn;
     if (!fm->d_rep_set.hasType(tn)) {
       mbn = fm->getSomeDomainElement(tn);
@@ -684,16 +683,16 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
             }
             d_triedLemmas++;
             if( d_qe->addInstantiation( f, m ) ){
-              Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
+              Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
               d_addedLemmas++;
             }else{
-              Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
+              Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
               //this can happen if evaluation is unknown
               //might try it next effort level
               d_star_insts[f].push_back(i);
             }
           }else{
-            Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl;
+            Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl;
             //might try it next effort level
             d_star_insts[f].push_back(i);
           }
@@ -1149,7 +1148,7 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, De
 }
 
 int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
-  Trace("fmc-debug3") << "isCompat " << c << std::endl;
+  Trace("fmc-debug3") << "isCompat " << c << std::endl;
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
     if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
@@ -1167,7 +1166,7 @@ int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & c
 }
 
 bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
-  Trace("fmc-debug3") << "doMeet " << c << std::endl;
+  Trace("fmc-debug3") << "doMeet " << c << std::endl;
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
     if( cond[i]!=c[i-1] ) {
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 93174677f..6bb375c34 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -10,6 +10,8 @@
  ** \brief Full model check class
  **/
 
+#include "cvc4_private.h"
+
 #ifndef FULL_MODEL_CHECK
 #define FULL_MODEL_CHECK