Merge pull request #584 from vprover/martin-fix-fmb

Fixes several model printing bugs (and more)
vprover · Sep 2, 2024 · 2d67dfb · 2d67dfb
2 parents e5a912c + 740f67a
commit 2d67dfb
Show file tree

Hide file tree

Showing 44 changed files with 1,535 additions and 1,207 deletions.
diff --git a/Debug/Assertion.hpp b/Debug/Assertion.hpp
@@ -164,6 +164,7 @@ template <typename T>
   catch (Exception& e) { e.cry(std::cout); ASSERTION_VIOLATION } \
   catch (...)          {                   ASSERTION_VIOLATION } \
 
+#define RELEASE_CODE(X) {}
 #define DEBUG_CODE(X) X
 #define ALWAYS(Cond) ASS(Cond)
 #define NEVER(Cond) ASS(!(Cond))
@@ -192,6 +193,7 @@ template <typename T>
   }
 #endif
 
+#define RELEASE_CODE(X) X
 #define DEBUG_CODE(X) {}
 
 #define ASS(Cond)  {}

diff --git a/Debug/RuntimeStatistics.cpp b/Debug/RuntimeStatistics.cpp
@@ -28,7 +28,7 @@ using namespace std;
 
 void RSMultiCounter::print(ostream& out)
 {
-  out << name() << ":"<< endl;
+  out << "% " << name() << ":"<< endl;
   for(size_t i=0;i<_counters.size();i++) {
     if(_counters[i]) {
       out << "  " << i << ": " << _counters[i] <<endl;
@@ -45,7 +45,7 @@ RSMultiStatistic::~RSMultiStatistic()
 
 void RSMultiStatistic::print(ostream& out)
 {
-  out << name() << ":"<< endl;
+  out << "% " << name() << ":"<< endl;
   for(size_t i=0;i<_values.size();i++) {
     if(_values[i]) {
 
@@ -67,8 +67,7 @@ void RSMultiStatistic::print(ostream& out)
 	  max=val;
 	}
       }
-
-      out << "  " << i << ": " << 
+      out << "  " << i << ": " <<
               "cnt: "+Int::toString(cnt)+
               ", avg: "+Int::toString(static_cast<float>(sum)/cnt)+
               ", min: "+Int::toString(min)+
@@ -98,14 +97,14 @@ RuntimeStatistics::~RuntimeStatistics()
 
 void RuntimeStatistics::print(ostream& out)
 {
-  out<<"----  Runtime statistics ----"<<endl;
+  out<<"% ----  Runtime statistics ----"<<endl;
 
   ObjSkipList::Iterator it(_objs);
   while(it.hasNext()) {
     it.next()->print(out);
   }
 
-  out<<"-----------------------------"<<endl;
+  out<<"% -----------------------------"<<endl;
 }
 
 

diff --git a/Debug/RuntimeStatistics.hpp b/Debug/RuntimeStatistics.hpp
@@ -111,7 +111,7 @@ class RSCounter
 public:
   RSCounter(const char* name) : RSObject(name), _counter(0) {}
 
-  void print(std::ostream& out) { out << name() << ": " << _counter << std::endl; }
+  void print(std::ostream& out) { out << "% " << name() << ": " << _counter << std::endl; }
   void inc() { _counter++; }
   void inc(size_t num) { _counter+=num; }
 private:

diff --git a/FMB/FiniteModel.cpp b/FMB/FiniteModel.cpp
@@ -427,7 +427,7 @@ bool FiniteModel::evaluate(Unit* unit)
     formula = fu->getFormula();
   }
 
-  formula = partialEvaluate(formula);
+  formula = partialEvaluate(formula,0);
   formula = SimplifyFalseTrue::simplify(formula);
   return evaluate(formula);
 }
@@ -549,7 +549,7 @@ bool FiniteModel::evaluate(Formula* formula,unsigned depth)
      * TODO: This is recursive, which could be problematic in the long run
      *
      */
-    Formula* FiniteModel::partialEvaluate(Formula* formula)
+    Formula* FiniteModel::partialEvaluate(Formula* formula,unsigned depth)
     {
 #if DEBUG_MODEL
         for(unsigned i=0;i<depth;i++){ cout << "."; }
@@ -572,7 +572,7 @@ bool FiniteModel::evaluate(Formula* formula,unsigned depth)
                     return formula;
                 case NOT:
                 {
-                  Formula* inner = partialEvaluate(formula->uarg());
+                  Formula* inner = partialEvaluate(formula->uarg(),depth+1);
                   return new NegatedFormula(inner);
                 }
                 case AND:
@@ -582,7 +582,7 @@ bool FiniteModel::evaluate(Formula* formula,unsigned depth)
                 FormulaList* newArgs = 0;
                 FormulaList::Iterator fit(args);
                 while(fit.hasNext()){
-                    Formula* newArg = partialEvaluate(fit.next());
+                    Formula* newArg = partialEvaluate(fit.next(),depth+1);
                     FormulaList::push(newArg,newArgs);
                 }
                 return new JunctionFormula(formula->connective(),newArgs); 
@@ -594,8 +594,8 @@ bool FiniteModel::evaluate(Formula* formula,unsigned depth)
             {
                 Formula* left = formula->left();
                 Formula* right = formula->right();
-                Formula* newLeft = partialEvaluate(left);
-                Formula* newRight = partialEvaluate(right);
+                Formula* newLeft = partialEvaluate(left,depth+1);
+                Formula* newRight = partialEvaluate(right,depth+1);
 
                 return new BinaryFormula(formula->connective(),newLeft,newRight); 
             }
@@ -605,7 +605,7 @@ bool FiniteModel::evaluate(Formula* formula,unsigned depth)
             {
                 VList* vs = formula->vars();
                 Formula* inner  = formula->qarg();
-                Formula* newInner = partialEvaluate(inner);
+                Formula* newInner = partialEvaluate(inner,depth+1);
                 return new QuantifiedFormula(formula->connective(),vs,0,newInner);
             }
             default:

diff --git a/FMB/FiniteModel.hpp b/FMB/FiniteModel.hpp
@@ -58,7 +58,7 @@ class FiniteModel {
 
 private:
 
- Formula* partialEvaluate(Formula* formula);
+ Formula* partialEvaluate(Formula* formula,unsigned depth);
  // currently private as requires formula to be rectified
  bool evaluate(Formula* formula,unsigned depth=0);
 
@@ -82,6 +82,8 @@ class FiniteModel {
    if(_domainConstants.find(c,t)) return t;
    std::string name = "domainConstant";//+Lib::Int::toString(c);
    unsigned f = env.signature->addFreshFunction(0,name.c_str()); 
+   Signature::Symbol* fSym = env.signature->getFunction(f);
+   fSym->setType(OperatorType::getConstantsType(AtomicSort::defaultSort()));
    t = Term::createConstant(f);
    _domainConstants.insert(c,t);
    _domainConstantsRev.insert(t,c);