Merge branch 'boogie-expresiments' of https://github.com/easychair/va…

…mpire into boogie-expresiments
ModelWriter · Oct 17, 2017 · f4bdd1e · f4bdd1e
2 parents 1f28823 + a0ab013
commit f4bdd1e
Show file tree

Hide file tree

Showing 3 changed files with 55 additions and 7 deletions.
diff --git a/Shell/NewCNF.cpp b/Shell/NewCNF.cpp
@@ -589,11 +589,6 @@ TermList NewCNF::eliminateLet(Term::SpecialTermData *sd, TermList contents)
 
     TermList detupledContents = contents;
 
-    // TODO: replace $let([a,b] := ..., ...[a,b]...) with $let(t := ... , ...t...)
-//    Term::createTuple(tupleType->arity(), );
-//    SymbolDefinitionInlining test(symbol, 0, projectedArgument, 0);
-//    detupledContents = test.process(detupledContents);
-
     for (unsigned proj = 0; proj < tupleType->arity(); proj++) {
       unsigned symbol = (unsigned) IntList::nth(symbols, proj);
       bool isPredicate = tupleType->arg(proj) == Sorts::SRT_BOOL;

diff --git a/Shell/SymbolDefinitionInlining.cpp b/Shell/SymbolDefinitionInlining.cpp
@@ -114,11 +114,18 @@ TermList SymbolDefinitionInlining::process(TermList ts) {
         TermList tuple = process(TermList(sd->getTupleTerm()));
         ASS(tuple.isTerm());
 
-        if (tuple.term() == sd->getTupleTerm()) {
+        Term* t = tuple.term();
+        if (t == sd->getTupleTerm()) {
           return ts;
         }
 
-        return TermList(Term::createTuple(tuple.term()));
+        // Replace [$proj(0, t), ..., $proj(n, t)] with t
+        TermList tupleConstant;
+        if (mirroredTuple(t, tupleConstant)) {
+          return tupleConstant;
+        }
+
+        return TermList(Term::createTuple(t));
       }
 
       default:
@@ -150,6 +157,50 @@ TermList SymbolDefinitionInlining::process(TermList ts) {
   return TermList(Term::create(term, args.begin()));
 }
 
+bool SymbolDefinitionInlining::mirroredTuple(Term* tuple, TermList &tupleConstant) {
+  bool foundTupleConstant = false;
+  unsigned tupleSort = env.signature->getFunction(tuple->functor())->fnType()->result();
+  ASS(env.sorts->hasStructuredSort(tupleSort, StructuredSort::TUPLE));
+  for (unsigned i = 0; i < tuple->arity(); i++) {
+    if (!tuple->nthArgument(i)->isTerm()) {
+      return false;
+    }
+    Term* arg = (tuple->nthArgument(i))->term();
+    TermList possibleTupleConstant;
+    if (arg->isSpecial()) {
+      if (arg->getSpecialData()->getType() != Term::SF_FORMULA) {
+        return false;
+      }
+      Formula* f = arg->getSpecialData()->getFormula();
+      if (f->connective() != LITERAL) {
+        return false;
+      }
+      Literal* l = f->literal();
+      if (l->functor() != Theory::tuples()->getProjectionFunctor(i, tupleSort)) {
+        return false;
+      }
+      possibleTupleConstant = *l->nthArgument(0);
+    } else {
+      if (arg->functor() != Theory::tuples()->getProjectionFunctor(i, tupleSort)) {
+        return false;
+      }
+      possibleTupleConstant = *arg->nthArgument(0);
+    }
+    if (!possibleTupleConstant.isTerm()) {
+      return false;
+    }
+    if (!foundTupleConstant) {
+      tupleConstant = possibleTupleConstant;
+      foundTupleConstant = true;
+    } else {
+      if (possibleTupleConstant != tupleConstant) {
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
 Formula* SymbolDefinitionInlining::process(Formula* formula) {
   CALL("SymbolDefinitionInlining::process(Formula*)");
 

diff --git a/Shell/SymbolDefinitionInlining.hpp b/Shell/SymbolDefinitionInlining.hpp
@@ -34,6 +34,8 @@ class SymbolDefinitionInlining {
 
     TermList substitute(Term::Iterator tit);
 
+    bool mirroredTuple(Term* tuple, TermList &tupleConstant);
+
     unsigned _counter;
     unsigned _freshVarOffset;
     List<pair<unsigned, unsigned>>* _varRenames;