TODO.txt

//
//
//
// QUESTIONs
//
//
//

Incremental solvers and push/pop 




Interpreter code that should probably be implemented ...:

// case PlainSymbol("or") =>
    //   (connect(for (s <- flatten("or", args))
    //   yield asFormula(translateTerm(s, polarity)),
    //     IBinJunctor.Or),
    //     SMTBool)
      
    // case PlainSymbol("=>") => {
    //   if (args.size == 0)
    //     throw new Parser2InputAbsy.TranslationException(
    //       "Operator \"=>\" has to be applied to at least one argument")

    //   (connect((for (a <- args.init) yield
    //     !asFormula(translateTerm(a, -polarity))) ++
    //     List(asFormula(translateTerm(args.last, polarity))),
    //     IBinJunctor.Or),
    //     SMTBool)
    // }
      
    // case PlainSymbol("xor") => {
    //   if (args.size == 0)
    //     throw new Parser2InputAbsy.TranslationException(
    //       "Operator \"xor\" has to be applied to at least one argument")

    //   (connect(List(asFormula(translateTerm(args.head, polarity))) ++
    //     (for (a <- args.tail) yield
    //       !asFormula(translateTerm(a, -polarity))),
    //     IBinJunctor.Eqv),
    //     SMTBool)
    // }
      
    // case PlainSymbol("ite") => {
    //   checkArgNum("ite", 3, args)
    //   val transArgs = for (a <- args) yield translateTerm(a, 0)
    //     (transArgs map (_._2)) match {
    //     case Seq(SMTBool, SMTBool, SMTBool) =>
    //       (IFormulaITE(asFormula(transArgs(0)),
    //         asFormula(transArgs(1)), asFormula(transArgs(2))),
    //         SMTBool)
    //     case Seq(SMTBool, t1, t2) =>
    //       (ITermITE(asFormula(transArgs(0)),
    //         asTerm(transArgs(1)), asTerm(transArgs(2))),
    //         t1)
    //   }
    // }
    
    // case PlainSymbol("<=") =>
    //   (translateChainablePred(args, _ <= _), SMTBool)
    // case PlainSymbol("<") =>
    //   (translateChainablePred(args, _ < _), SMTBool)
    // case PlainSymbol(">=") =>
    //   (translateChainablePred(args, _ >= _), SMTBool)
    // case PlainSymbol(">") =>
    //   (translateChainablePred(args, _ > _), SMTBool)
      
    // case IndexedSymbol("divisible", denomStr) => {
    //   checkArgNum("divisible", 1, args)
    //   val denom = i(IdealInt(denomStr))
    //   val num = VariableShiftVisitor(asTerm(translateTerm(args.head, 0)), 0, 1)
    //   (ex(num === v(0) * denom), SMTBool)
    // }
      
    //   ////////////////////////////////////////////////////////////////////////////
    //   // Hardcoded integer operations


    // case PlainSymbol("-") if (args.length == 1) =>
    //   (-asTerm(translateTerm(args.head, 0), SMTInteger), SMTInteger)

    // case PlainSymbol("~") if (args.length == 1) => {
    //   if (!tildeWarning) {
    //     warn("interpreting \"~\" as unary minus, like in SMT-LIB 1")
    //     tildeWarning = true
    //   }unintFunApp
    //   (-asTerm(translateTerm(args.head, 0), SMTInteger), SMTInteger)
    // }

    // case PlainSymbol("-") => {
    //   (asTerm(translateTerm(args.head, 0), SMTInteger) -
    //     sum(for (a <- args.tail)
    //     yield asTerm(translateTerm(a, 0), SMTInteger)),
    //     SMTInteger)
    // }

    // case PlainSymbol("*") =>
    //   ((for (s <- flatten("*", args))
    //   yield asTerm(translateTerm(s, 0), SMTInteger))
    //     reduceLeft (mult _),
    //     SMTInteger)

    // case PlainSymbol("div") => {
    //   checkArgNum("div", 2, args)
    //   val Seq(num, denom) = for (a <- args) yield asTerm(translateTerm(a, 0))
    //   (mulTheory.eDiv(num, denom), SMTInteger)
    // }
      
    // case PlainSymbol("mod") => {
    //   checkArgNum("mod", 2, args)
    //   val Seq(num, denom) = for (a <- args) yield asTerm(translateTerm(a, 0))
    //   (mulTheory.eMod(num, denom), SMTInteger)
    // }

    // case PlainSymbol("abs") => {
    //   checkArgNum("abs", 1, args)
    //   (abs(asTerm(translateTerm(args.head, 0))), SMTInteger)
    // }
      
      ////////////////////////////////////////////////////////////////////////////
      // Array operations
      
    // case PlainSymbol("select") => {
    //   val transArgs = for (a <- args) yield translateTerm(a, 0)
    //   transArgs.head._2 match {
    //     case SMTArray(_, resultType) =>
    //       (MyFunApp(SimpleArray(args.size - 1).select,
    //         for (a <- transArgs) yield asTerm(a)),
    //         resultType)
    //     case s =>
    //       throw new Exception(
    //         "select has to be applied to an array expression, not " + s)
    //   }
    // }

    // case PlainSymbol("store") => {
    //   val transArgs = for (a <- args) yield translateTerm(a, 0)
    //   transArgs.head._2 match {
    //     case s : SMTArray =>
    //       (IFunApp(SimpleArray(args.size - 2).store,
    //         for (a <- transArgs) yield asTerm(a)),
    //         s)
    //     case s =>
    //       throw new Exception(
    //         "store has to be applied to an array expression, not " + s)
    //   }
    // }
      // TODO: What does this do?
  private def unintFunApp(id : String,
    sym : SymbolRef, args : Seq[Term], polarity : Int)
      : uppsat.ast.AST = {
    val funSort = myEnv.lookup(id)
    throw new Exception("Cannot handle uninterpreted function applications")    
  }

    // (env lookupSym id) match {
    //   case Environment.Predicate(pred, _, _) => {
    //     checkArgNumLazy(printer print sym, pred.arity, args)
    //     (IAtom(pred, for (a <- args) yield asTerm(translateTerm(a, 0))),
    //       SMTBool)
    //   }
        
    //   case Environment.Function(fun, SMTFunctionType(_, resultType)) => {
    //     checkArgNumLazy(printer print sym, fun.arity, args)
    //       (functionDefs get fun) match {
    //       case Some((body, t)) => {
    //         var translatedArgs = List[ITerm]()
    //         for (a <- args)
    //           translatedArgs = asTerm(translateTerm(a, 0)) :: translatedArgs
    //         (VariableSubstVisitor(body, (translatedArgs, 0)), t)
    //       }
    //       case None =>
    //         (IFunApp(fun, for (a <- args) yield asTerm(translateTerm(a, 0))),
    //           resultType)
    //     }
    //   }

    //   case Environment.Constant(c, _, t) =>
    //     (c, t)
        
    //   case Environment.Variable(i, BoundVariable(t)) =>
    //     (v(i), t)
        
    //   case Environment.Variable(i, SubstExpression(e, t)) =>
    //     (e, t)
    // }
        


Old interpreter code:

  // Should we give warning for decl-const (Which is not SMT2)?
  private var declareConstWarning = false
  
  

object IBinJunctor extends Enumeration {
    val And, Or, Eqv, EqualitySign = Value
  }

  protected def checkArgNum(op : String, expected : Int, args : Seq[Term]) : Unit =
    if (expected != args.size)
      throw new Exception(
          "Operator \"" + op +
          "\" is applied to a wrong number of arguments: " +
          ((for (a <- args) yield (printer print a)) mkString ", "))

 // TODO: What does this do?
//  protected def asFormula(expr : (MyExpression, SMTType)) : uppsat.ast.AST = expr match {
//    case (expr : MyFormula, SMTBool) =>
//      expr
//    // case (expr : MyTerm, SMTBool) =>
//    case (expr : MyTerm, _) =>
//      // then we assume that an integer encoding of boolean values was chosen
//      StrangeFormula(expr.toString())
//    // IIntFormula(IIntRelation.EqZero, expr)
//    case (expr, _) =>
//      println(expr.getClass)
//      throw new Exception(
//        "Expected a formula, not " + expr)
//  }

      // TODO: Do we have to handle SetOptionCommand?
      // val annot = cmd.optionc_.asInstanceOf[Option]
      //   .annotation_.asInstanceOf[AttrAnnotation]

      // val handled =
      //   handleBooleanAnnot(":print-success", annot) {
      //     value => printSuccess = value
      //   } ||
      // handleBooleanAnnot(":produce-models", annot) {
      //   value => // nothing
      // } ||
      // handleBooleanAnnot(":boolean-functions-as-predicates", annot) {
      //   value => booleanFunctionsAsPredicates = value
      // } ||
      // handleBooleanAnnot(":inline-let", annot) {
      //   value => inlineLetExpressions = value
      // } ||
      // handleBooleanAnnot(":inline-definitions", annot) {
      //   value => inlineDefinedFuns = value
      // } ||
      // handleBooleanAnnot(":totality-axiom", annot) {
      //   value => totalityAxiom = value
      // } ||
      // handleBooleanAnnot(":functionality-axiom", annot) {
      //   value => functionalityAxiom = value
      // } ||
      // handleBooleanAnnot(":produce-interpolants", annot) {
      //   value => {
      //     genInterpolants = value
      //     if (incremental)
      //       prover.setConstructProofs(value)
      //   }
      // } ||
      // handleNumAnnot(":timeout-per", annot) {
      //   value => timeoutPer = (value min IdealInt(Int.MaxValue)).intValue
      // }

      // if (handled) {
      //   success
      // } else {
      //   if (incremental)
      //     unsupported
      //   else
      //     warn("ignoring option " + annot.annotattribute_)
      // }
      
// case t : QuantifierTerm =>
    //   translateQuantifier(t, polarity)
      
    // case t : AnnotationTerm => {
    //   val triggers = for (annot <- t.listannotation_;
    //     a = annot.asInstanceOf[AttrAnnotation];
    //     if (a.annotattribute_ == ":pattern")) yield {
    //     a.attrparam_ match {
    //       case p : SomeAttrParam => p.sexpr_ match {
    //         case e : ParenSExpr =>
    //           for (expr <- e.listsexpr_.toList;
    //             transTriggers = {
    //               try { List(translateTrigger(expr)) }
    //               catch { case _ : TranslationException |
    //                 _ : Environment.EnvironmentException => {
    //                   warn("could not parse trigger " +
    //                     (printer print expr) +
    //                     ", ignoring")
    //                   List()
    //                 } }
    //             };
    //             t <- transTriggers) yield t
    //         case _ =>
    //           throw new Parser2InputAbsy.TranslationException(
    //             "Expected list of patterns after \":pattern\"")
    //       }
    //       case _ : NoAttrParam =>
    //         throw new Parser2InputAbsy.TranslationException(
    //           "Expected trigger patterns after \":pattern\"")
    //     }
    //   }

    //   val baseExpr =
    //     if (genInterpolants) {
    //       val names = for (annot <- t.listannotation_;
    //         a = annot.asInstanceOf[AttrAnnotation];
    //         if (a.annotattribute_ == ":named")) yield {
    //         a.attrparam_ match {
    //           case p : SomeAttrParam => p.sexpr_ match {
    //             case e : SymbolSExpr =>
    //               printer print e
    //             case _ =>
    //               throw new Parser2InputAbsy.TranslationException(
    //                 "Expected name after \":named\"")
    //           }
    //           case _ : NoAttrParam =>
    //             throw new Parser2InputAbsy.TranslationException(
    //               "Expected name after \":named\"")
    //         }
    //       }
          
    //       translateTerm(t.term_, polarity) match {
    //         case p@(expr, SMTBool) =>
    //           ((asFormula(p) /: names) {
    //             case (res, name) => INamedPart(env lookupPartName name, res)
    //           }, SMTBool)
    //         case p =>
    //           // currently names for terms are ignored
    //           p
    //       }
    //     } else {
    //       translateTerm(t.term_, polarity)
    //     }

    //   if (triggers.isEmpty)
    //     baseExpr
    //   else
    //     ((asFormula(baseExpr) /: triggers) {
    //       case (res, trigger) => ITrigger(ITrigger.extractTerms(trigger), res)
    //     }, SMTBool)
    // }
      
    // case t : LetTerm =>
    //   translateLet(t, polarity)      
    
  // private def translateQuantifier(t : QuantifierTerm, polarity : Int)
  //     : (IExpression, SMTType) = {
  //   val quant : Quantifier = t.quantifier_ match {
  //     case _ : AllQuantifier => Quantifier.ALL
  //     case _ : ExQuantifier => Quantifier.EX
  //   }

  //   val quantNum = pushVariables(t.listsortedvariablec_)
    
  //   val body = asFormula(translateTerm(t.term_, polarity))

  //   // we might need guards 0 <= x <= 1 for quantifiers ranging over booleans
  //   val guard = connect(
  //     for (binderC <- t.listsortedvariablec_.iterator;
  //       binder = binderC.asInstanceOf[SortedVariable];
  //       if (translateSort(binder.sort_) == SMTBool)) yield {
  //       (env lookupSym asString(binder.symbol_)) match {
  //         case Environment.Variable(ind, _) => (v(ind) >= 0) & (v(ind) <= 1)
  //         case _ => { // just prevent a compiler warning
  //                     //-BEGIN-ASSERTION-///////////////////////////////////////////////
  //           Debug.assertInt(SMTParser2InputAbsy.AC, false)
  //           //-END-ASSERTION-/////////////////////////////////////////////////
  //           null
  //         }
  //       }
  //     },
  //     IBinJunctor.And)
    
  //   val matrix = guard match {
  //     case IBoolLit(true) =>
  //       body
  //     case _ => {
  //       // we need to insert the guard underneath possible triggers
  //       def insertGuard(f : IFormula) : IFormula = f match {
  //         case ITrigger(pats, subF) =>
  //           ITrigger(pats, insertGuard(subF))
  //         case _ => quant match {
  //           case Quantifier.ALL => guard ===> f
  //           case Quantifier.EX => guard &&& f
  //         }
  //       }
        
  //       insertGuard(body)
  //     }
  //   }
    
  //   val res = quan(Array.fill(quantNum){quant}, matrix)

  //   // pop the variables from the environment
  //   for (_ <- PlainRange(quantNum)) env.popVar
    
  //   (res, SMTBool)
  // }
      
      
       // private def importProverSymbol(name : String,
  //                                args : Seq[SMTType],
  //                                res : SMTType) : Boolean =
  //   incremental &&
  //   ((reusedSymbols get name) match {
  //      case None =>
  //        false
  //      case Some(c : ConstantTerm) if (args.isEmpty) => {
  //        env.addConstant(c, Environment.NullaryFunction, res)
  //        true
  //      }
  //      case Some(f : IFunction) if (args.size == f.arity) => {
  //        env.addFunction(f, SMTFunctionType(args.toList, res))
  //        true
  //      }
  //      case Some(p : Predicate) if (args.size == p.arity && res == SMTBool) => {
  //        env.addPredicate(p, ())
  //        true
  //      }
  //      case Some(_) => {
  //        warn("inconsistent definition of symbol " + name)
  //        false
  //      }
  //    })
  
      // ensureEnvironmentCopy

      // if (!importProverSymbol(name, args, res)) {
      //   if (args.length > 0) {
      //     if (!booleanFunctionsAsPredicates || res != SMTBool) {
      //       // use a real function
      //       val f = new IFunction(name, args.length,
      //         !totalityAxiom, !functionalityAxiom)
      //       env.addFunction(f, SMTFunctionType(args.toList, res))
      //       if (incremental)
      //         prover.addFunction(f,
      //           if (functionalityAxiom)
      //             SimpleAPI.FunctionalityMode.Full
      //           else
      //             SimpleAPI.FunctionalityMode.None)
      //     } else {
      //       // use a predicate
      //       val p = new Predicate(name, args.length)
      //       env.addPredicate(p, ())
      //       if (incremental)
      //         prover.addRelation(p)
      //     }
      //   } else if (res != SMTBool) {
      //     // use a constant
      //     addConstant(new ConstantTerm(name), res)
      //   } else {
      //     // use a nullary predicate (propositional variable)
      //     val p = new Predicate(name, 0)
      //     env.addPredicate(p, ())
      //     if (incremental)
      //       prover.addRelation(p)
      //   }
      // }  
      
       // for (Seq(a, b) <- (transArgs map (asFormula(_))) sliding 2)
      // yield (
      //   // println("transArgs: " + transArgs.mkString(", "))
      //   (if (transArgs forall (_._2 == SMTBool)) {
      //     connect(for (Seq(a, b) <- (transArgs map (asFormula(_))) sliding 2)
      //     yield (a <===> b),
      //       IBinJunctor.And)
      // } else {
      //   val types = (transArgs map (_._2)).toSet
      //   if (types.size > 1)
      //     throw new Parser2InputAbsy.TranslationException(
      //       "Can only compare terms of same type using =")
      //   connect(for (Seq(a, b) <- (transArgs map (asTerm(_))) sliding 2)
      //   yield translateEq(a, b, types.iterator.next, polarity),
      //     IBinJunctor.And)
      // },
      //   SMTBool)
      
  // private def checkArgNumLazy(op : => String, expected : Int, args : Seq[Term]) : Unit =
  //   if (expected != args.size) checkArgNum(op, expected, args)
  
  // protected def checkArgNum(op : String, expected : Int, args : Seq[Term]) : Unit =
  //   if (expected != args.size)
  //     throw new Parser2InputAbsy.TranslationException(
  //       "Operator \"" + op +
  //         "\" is applied to a wrong number of arguments: " +
  //         ((for (a <- args) yield (printer print a)) mkString ", "))
  
  // private def checkArgNumSExpr(op : => String, expected : Int, args : Seq[SExpr]) : Unit =
  //   if (expected != args.size)
  //     throw new Parser2InputAbsy.TranslationException(
  //       "Operator \"" + op +
  //         "\" is applied to a wrong number of arguments: " +
  //         ((for (a <- args) yield (printer print a)) mkString ", "))
  
  // private object SMTConnective extends ASTConnective {
  //   def unapplySeq(t : Term) : scala.Option[Seq[Term]] = t match {
  //     case t : NullaryTerm => Some(List())
  //     case t : FunctionTerm => Some(t.listterm_.toList)
  //   }
  // }      
  
      // case s : CompositeSort => asString(s.identifier_) match {
    //   case "Array" => {
    //     val args =
    //       for (t <- s.listsort_.toList) yield translateSort(t)
    //     if (args.size < 2)
    //       throw new Parser2InputAbsy.TranslationException(
    //         "Expected at least two sort arguments in " + (printer print s))
    //     SMTArray(args.init, args.last)
    //   }
    //   case id => {
    //     warn("treating sort " + (printer print s) + " as Int")
    //     SMTInteger
    //   }
    // }