/*
 *  JavaSMT is an API wrapper for a collection of SMT solvers.
 *  This file is part of JavaSMT.
 *
 *  Copyright (C) 2007-2016  Dirk Beyer
 *  All rights reserved.
 *
 *  Licensed under the Apache License, Version 2.0 (the "License");
 *  you may not use this file except in compliance with the License.
 *  You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 *  Unless required by applicable law or agreed to in writing, software
 *  distributed under the License is distributed on an "AS IS" BASIS,
 *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 *  See the License for the specific language governing permissions and
 *  limitations under the License.
 */
package org.sosy_lab.java_smt.solvers.mathsat5;

import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_apply_substitution;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_from_smtlib2;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2;

import com.google.common.collect.Collections2;
import com.google.common.primitives.Longs;

import org.sosy_lab.common.Appender;
import org.sosy_lab.common.Appenders;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.Formula;
import org.sosy_lab.java_smt.api.FormulaType;
import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;

import java.util.Collection;
import java.util.Map;
import java.util.Map.Entry;

final class Mathsat5FormulaManager extends AbstractFormulaManager<Long, Long, Long, Long> {

  @SuppressWarnings("checkstyle:parameternumber")
  Mathsat5FormulaManager(
      Mathsat5FormulaCreator creator,
      Mathsat5UFManager pFunctionManager,
      Mathsat5BooleanFormulaManager pBooleanManager,
      Mathsat5IntegerFormulaManager pIntegerManager,
      Mathsat5RationalFormulaManager pRationalManager,
      Mathsat5BitvectorFormulaManager pBitpreciseManager,
      Mathsat5FloatingPointFormulaManager pFloatingPointManager,
      Mathsat5ArrayFormulaManager pArrayManager) {
    super(
        creator,
        pFunctionManager,
        pBooleanManager,
        pIntegerManager,
        pRationalManager,
        pBitpreciseManager,
        pFloatingPointManager,
        null,
        pArrayManager);
  }

  static long getMsatTerm(Formula pT) {
    return ((Mathsat5Formula) pT).getTerm();
  }

  static long[] getMsatTerm(Collection<? extends Formula> pFormulas) {
    return Longs.toArray(Collections2.transform(pFormulas, Mathsat5FormulaManager::getMsatTerm));
  }

  @Override
  public BooleanFormula parse(String pS) throws IllegalArgumentException {
    long f = msat_from_smtlib2(getEnvironment(), pS);
    return getFormulaCreator().encapsulateBoolean(f);
  }

  @Override
  public Appender dumpFormula(final Long f) {
    assert getFormulaCreator().getFormulaType(f) == FormulaType.BooleanType
        : "Only BooleanFormulas may be dumped";

    // Lazy invocation of msat_to_smtlib2 wrapped in an Appender.
    return Appenders.fromToStringMethod(
        new Object() {
          @Override
          public String toString() {
            String msatString = msat_to_smtlib2(getEnvironment(), f);
            StringBuilder smtString = new StringBuilder();
            boolean needsLinebreak = true;
            for (String part : msatString.split("\n")) {
              smtString.append(part);
              if (part.startsWith("(assert")) {
                needsLinebreak = false;
              }
              if (needsLinebreak) {
                smtString.append('\n');
              }
            }
            return smtString.toString();
          }
        });
  }

  @Override
  public <T extends Formula> T substitute(
      final T f, final Map<? extends Formula, ? extends Formula> fromToMapping) {
    long[] changeFrom = new long[fromToMapping.size()];
    long[] changeTo = new long[fromToMapping.size()];
    int idx = 0;
    for (Entry<? extends Formula, ? extends Formula> e : fromToMapping.entrySet()) {
      changeFrom[idx] = extractInfo(e.getKey());
      changeTo[idx] = extractInfo(e.getValue());
      idx++;
    }
    FormulaType<T> type = getFormulaType(f);
    return getFormulaCreator()
        .encapsulate(
            type,
            msat_apply_substitution(
                getFormulaCreator().getEnv(),
                extractInfo(f),
                fromToMapping.size(),
                changeFrom,
                changeTo));
  }
}

@@ -1056,16 +1056,56 @@
 tlib2;%0A%0A
+import com.google.common.base.Splitter;%0A
 import c
@@ -1463,16 +1463,44 @@
 nager;%0A%0A
+import java.io.IOException;%0A
 import j
@@ -3111,16 +3111,20 @@
  return 
+new 
 Appender
@@ -3129,55 +3129,29 @@
 ers.
-fromToStringMethod(%0A        new Object
+AbstractAppender
 () %7B%0A
-    
     
@@ -3172,43 +3172,66 @@
     
-    
 public 
-String toString() %7B%0A    
+void appendTo(Appendable out) throws IOException %7B%0A
     
@@ -3304,58 +3304,98 @@
     
-    StringBuilder smtString = new StringBuilder();
+// Adjust line breaks: assert needs to be on last line, so we remove all following breaks.
 %0A   
@@ -3399,20 +3399,16 @@
         
-    
 boolean 
@@ -3438,20 +3438,16 @@
         
-    
 for (Str
@@ -3461,29 +3461,42 @@
 t : 
-msatString.split(%22%5Cn%22
+Splitter.on('%5Cn').split(msatString
 )) %7B
@@ -3502,37 +3502,27 @@
 %7B%0A          
-    smtString
+out
 .append(part
@@ -3534,24 +3534,38 @@
         
-    
 if (
+needsLinebreak && 
 part.sta
@@ -3598,20 +3598,16 @@
         
-    
 needsLin
@@ -3628,34 +3628,26 @@
 ;%0A          
- 
-   %7D%0A    
+%7D%0A
           if
@@ -3682,21 +3682,11 @@
     
-    
-smtString
+out
 .app
@@ -3702,34 +3702,26 @@
 ;%0A          
-  
-  %7D%0A    
+%7D%0A
         %7D%0A  
@@ -3722,53 +3722,8 @@
   %7D%0A
-            return smtString.toString();%0A    
     
@@ -3734,14 +3734,9 @@
     
-    %7D)
+%7D
 ;%0A  

Make dumpFormula more efficient for MathSAT: we can do lazy splitting and we can avoid recreating the whole string but write incrementally to the output.