quoting, skip some interpreted sorts

vprover · Mar 18, 2024 · b8bbdca · b8bbdca
1 parent f01c2a7
commit b8bbdca
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 7 deletions.
diff --git a/FMB/FiniteModelMultiSorted.cpp b/FMB/FiniteModelMultiSorted.cpp
@@ -190,15 +190,20 @@ vstring FiniteModelMultiSorted::toString()
 
   //Output sorts and their sizes 
   for(unsigned s=0;s<env.signature->typeCons();s++){
-
     unsigned size = _sizes.get(s);
     if(size==0) continue;
 
+    // don't output interpreted sorts at all, we know what they are
+    if(env.signature->isInterpretedNonDefault(s))
+      continue;
+
     vstring sortName = env.signature->typeConName(s);
     vstring sortNameLabel = (env.signature->isBoolCon(s)) ? "bool" : sortName;
 
-    // Sort declaration
-    modelStm << "tff(" << prepend("declare_", sortNameLabel) << ",type,"<<sortName<<":$tType)." <<endl;
+    // skip declaring $i, we know what it is
+    if(!env.signature->isDefaultSortCon(s))
+      // Sort declaration
+      modelStm << "tff(" << prepend("declare_", sortNameLabel) << ",type,"<<sortName<<":$tType)." <<endl;
 
     cnames[s].ensure(size+1);
 
@@ -207,7 +212,7 @@ vstring FiniteModelMultiSorted::toString()
     for(unsigned i=1;i<=size;i++){
       modelStm << "tff(" << append(prepend("declare_", sortNameLabel), Int::toString(i).c_str()) << ",type,";
       int frep = sortRepr[s][i];
-      vstring cname = "fmb_"+sortNameLabel+"_"+Lib::Int::toString(i);
+      vstring cname = prepend("fmb_", sortNameLabel+"_"+Lib::Int::toString(i));
       if(frep >= 0){
         cname = env.signature->functionName(frep);
       }
@@ -216,7 +221,7 @@ vstring FiniteModelMultiSorted::toString()
     }
 
     //Output domain
-    modelStm << "tff(finite_domain,axiom," << endl;
+    modelStm << "tff(" << prepend("finite_domain_", sortNameLabel) << ",axiom," << endl;
     modelStm << "      ! [X:" << sortName << "] : (" << endl;
     modelStm << "         ";
     for(unsigned i=1;i<=size;i++){
@@ -229,7 +234,7 @@ vstring FiniteModelMultiSorted::toString()
     //Distinctness of domain
     modelStm << endl;
     if(size>1){
-    modelStm << "tff(distinct_domain,axiom," << endl;
+    modelStm << "tff(" << prepend("distinct_domain_", sortNameLabel) << ",axiom," << endl;
     modelStm << "         ";
     unsigned c=0;
     for(unsigned i=1;i<=size;i++){
@@ -352,7 +357,7 @@ vstring FiniteModelMultiSorted::toString()
     if(arity>0) continue;
     if(!printIntroduced && env.signature->getPredicate(f)->introduced()) continue;
     vstring name = env.signature->predicateName(f);
-    modelStm << "tff("<<prepend("declare_", name)<<",type,"<<name<<": $o).";
+    modelStm << "tff("<<prepend("declare_", name)<<",type,"<<name<<": $o)."<<endl;
     unsigned res = p_interpretation[p_offsets[f]];
     if(res==2){
       modelStm << "tff("<<append(name,"_definition")<<",axiom,"<<name<< ")."<<endl;

diff --git a/FMB/FiniteModelMultiSorted.hpp b/FMB/FiniteModelMultiSorted.hpp
@@ -109,6 +109,8 @@ class FiniteModelMultiSorted {
  vstring prepend(const char* prefix, vstring name) {
    if (name.empty()) {
      return vstring(prefix);
+   } else if(name[0] == '$') {
+     return vstring("'") + prefix + name + "'";
    } else if (name[0] == '\'') {
      vstring dequoted = name.substr(1, name.length() - 1);
      return vstring("'") + prefix + dequoted;
@@ -119,6 +121,8 @@ class FiniteModelMultiSorted {
  vstring append(vstring name, const char* suffix) {
    if (name.empty()) {
      return vstring(suffix);
+   } else if(name[0] == '$') {
+     return vstring("'") + name + suffix + "'";
    } else if (name[0] == '\'') {
      vstring dequoted = name.substr(0, name.length() - 1);
      return dequoted + suffix + "'";