Floating point symfpu support (#1093)

Changes needed for the bit-blasting floating-point solver which are outside of it's area and / or applicable independently.

6 files changed, 10 insertions, 6 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 7a8bafe38..9b2ea1935 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -460,6 +460,7 @@ public:
 
   /**
    * Returns true if this node represents a variable
+   * @return true if variable
    */
   inline bool isVar() const {
     assertTNodeNotExpired();
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 2d45d0367..45ac02f10 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1302,7 +1302,8 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
   }
 
   Assert(nb.d_nvMaxChildren <= d_nvMaxChildren);
-  Assert(nb.d_nv->nv_end() - nb.d_nv->nv_begin() <= d_nvMaxChildren, "realloced:%s, d_nvMax:%u, size:%u, nc:%u", realloced ? "true" : "false", d_nvMaxChildren, nb.d_nv->nv_end() - nb.d_nv->nv_begin(), nb.d_nv->getNumChildren());
+  Assert(nb.d_nv->nv_end() >= nb.d_nv->nv_begin());
+  Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren, "realloced:%s, d_nvMax:%u, size:%u, nc:%u", realloced ? "true" : "false", d_nvMaxChildren, nb.d_nv->nv_end() - nb.d_nv->nv_begin(), nb.d_nv->getNumChildren());
   std::copy(nb.d_nv->nv_begin(),
             nb.d_nv->nv_end(),
             d_nv->nv_begin());
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b2f7d6ccc..af4510ff1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4955,7 +4955,7 @@ void SmtEngine::checkModel(bool hardFailure) {
   TheoryModel* m = d_theoryEngine->getModel();
 
   // Check individual theory assertions
-  d_theoryEngine->checkTheoryAssertionsWithModel();
+  d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure);
 
   // Output the model
   Notice() << *m;
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index 296a2f475..8dddf5065 100644
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -180,7 +180,7 @@ class FloatingPointRoundingOperationTypeRule {
       for (size_t i = 2; i < children; ++i) {
         if (!(n[i].getType(check) == firstOperand)) {
           throw TypeCheckingExceptionPrivate(
-              n, "floating-point test applied to mixed sorts");
+              n, "floating-point operation applied to mixed sorts");
         }
       }
     }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 59a52a048..892b331ea 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2208,7 +2208,7 @@ void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) {
   d_attr_handle[ str ].push_back( t );
 }
 
-void TheoryEngine::checkTheoryAssertionsWithModel() {
+void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
   for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
     Theory* theory = d_theoryTable[theoryId];
     if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
@@ -2223,7 +2223,9 @@ void TheoryEngine::checkTheoryAssertionsWithModel() {
           ss << theoryId << " has an asserted fact that the model doesn't satisfy." << endl
              << "The fact: " << assertion << endl
              << "Model value: " << val << endl;
-          InternalError(ss.str());
+	  if(hardFailure) {
+	    InternalError(ss.str());
+	  }
         }
       }
     }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7dd3f57a6..3ae0b840b 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -883,7 +883,7 @@ public:
    * Check that the theory assertions are satisfied in the model.
    * This function is called from the smt engine's checkModel routine.
    */
-  void checkTheoryAssertionsWithModel();
+  void checkTheoryAssertionsWithModel(bool hardFailure);
 
 private:
   IntStat d_arithSubstitutionsAdded;