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.

diff --git a/src/expr/node.h b/src/expr/node.h
index 7a8bafe3801a86f9dd9aa0f6ed5c89d8d05d8eb4..9b2ea19350e27b59d26fac9dd6b6e4a4704762ee 100644 (file)
--- 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 2d45d03675cc79440c8d375b3447d96c301b8b4c..45ac02f107f51f3508c0893c7a4d68af85c3d0ad 100644 (file)
--- 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 b2f7d6ccce9159570c22ce408dbdfb6e602f1a1f..af4510ff108141c6ac05d5a8752499d566397c3c 100644 (file)
--- 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 296a2f475ec9274b9756c5fbc7aabdcac1418bd4..8dddf50659e4dd0aa6e75b9b9303c18bbf07dd64 100644 (file)
--- 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 59a52a048d92500d11e6a06e409534e9b9fba78e..892b331ea86a98fe68e04756da5617ba73c824b9 100644 (file)
--- 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 7dd3f57a61d159b490db8bdc080087bc6db50124..3ae0b840b74091e3e7c5b85d9d0bdfca05c986c6 100644 (file)
--- 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;