theory_quant.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file theory_quant.cpp
 * 
 * Author: Daniel Wichs
 * 
 * Created: Wednesday July 2, 2003
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/


#include "theory_quant.h"
#include "typecheck_exception.h"
#include "parser_exception.h"
#include "smtlib_exception.h"
#include "quant_proof_rules.h"
#include "theory_core.h"
#include "command_line_flags.h"


using namespace std;
using namespace CVCL;



///////////////////////////////////////////////////////////////////////////////
// TheoryQuant Public Methods                                                //
///////////////////////////////////////////////////////////////////////////////


TheoryQuant::TheoryQuant(TheoryCore* core) //!< Constructor
  : Theory(core, "Quantified Expressions"),
    d_univs(core->getCM()->getCurrentContext()),
    d_savedTermsPos(core->getCM()->getCurrentContext(), 0, 0),
    d_univsSavedPos(core->getCM()->getCurrentContext(), 0, 0),
    d_univsPosFull(core->getCM()->getCurrentContext(), 0, 0),
    d_univsContextPos(core->getCM()->getCurrentContext(), 0, 0),
    d_instCount(core->getCM()->getCurrentContext(), 0,0),
    d_contextTerms(core->getCM()->getCurrentContext()),
    d_contextCache(core->getCM()->getCurrentContext()),
    d_maxQuantInst(&(core->getFlags()["max-quant-inst"].getInt())),
    d_useNew(&(core->getFlags()["quant-new"].getBool())),
    d_useLazyInst(&(core->getFlags()["quant-lazy"].getBool())),
    d_useSemMatch(&(core->getFlags()["quant-sem-match"].getBool())),
    d_useAtomSem(&(core->getFlags()["quant-const-match"].getBool())),
    d_allInstCount(core->getStatistics().counter("quantifier instantiations")),
    d_instRound(core->getCM()->getCurrentContext(), 0,0)
{
  IF_DEBUG(d_univs.setName("CDList[TheoryQuant::d_univs]"));
  vector<int> kinds;

  d_instCount = 0;

  d_rules=createProofRules();
  kinds.push_back(EXISTS);
  kinds.push_back(FORALL);
  registerTheory(this, kinds);
}

//! Destructor
TheoryQuant::~TheoryQuant() {
     if(d_rules != NULL) delete d_rules;
     for(std::map<Type, CDList<size_t>* ,TypeComp>::iterator 
           it = d_contextMap.begin(), iend = d_contextMap.end(); 
         it!= iend; ++it)
       delete it->second;
}

void TheoryQuant::setup(const Expr& e) {}
void TheoryQuant::update(const Theorem& e, const Expr& d) {}

void TheoryQuant::enqueueInst(const Theorem thm)
{
  enqueueFact(thm);
  d_allInstCount++;
  d_instThisRound++;
}
    

bool canGetHead(const Expr& e)
{
  return (e.getKind() == UFUNC || e.getKind() == 2001); 
  //I do not like 2001, but do we have another way to test if a term is an array?
}

//! get the head string of function and array
std::string TheoryQuant::getHead(const Expr& e)
{
  if (e.getKind() == UFUNC)
    return e.getOp().getExpr().getName();
  
  if (e.getKind() == 2001) 
    {
      std::string eStr = e.toString();
      size_t pos1 = eStr.find('[');
      size_t pos2 = eStr.find('(');
      if (std::string::npos == pos1)
        {
          cout<<"I do not know how this happen in get head"<<endl;
          return "";
        }
      else
        return eStr.substr(0,(pos1<pos2?pos1:pos2));
    }
  
  cout <<"cannot get the term head of "<<e.toString()<<endl;
  return "";
}

static void recursiveGetSubTerm(const Expr& e, std::vector<Expr> & res) {
 
  if(e.getFlag())
   return;

  if(e.isClosure())
    return recursiveGetSubTerm(e.getBody(),res); 

  //  if (e.isApply() || ( e.isTerm() && (!e.isVar())  )
  if  ( e.isTerm() && (!e.isVar()) && (e.getKind()!=RATIONAL_EXPR) )
  // if  ( (!e.isVar()) && (e.getKind()!=RATIONAL_EXPR) )
    {
      res.push_back(e);
    }
   
  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
    {   
      recursiveGetSubTerm(*i,res);
    }
  
  e.setFlag();
  return ;
}


std::vector<Expr> getSubTerms(const Expr& e)
{
  e.clearFlags();
  std::vector<Expr> res;
  recursiveGetSubTerm(e,res);
  e.clearFlags();
  TRACE("getsub","e is ", e.toString(),"");
  TRACE("getsub","have ", res.size()," subterms");
  return res;
}

//! get the bound vars in term e,
static void recursiveGetBoundVars(const Expr& e, std::set<Expr>& result) {
 
  if(e.getFlag())
   return ;
  
  if(e.isClosure())
    return recursiveGetBoundVars(e.getBody(),result); 
  
  if  (BOUND_VAR == e.getKind() ){
    result.insert(e);
  }
  else 
    for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i){        
      recursiveGetBoundVars(*i,result);
    }
  
  e.setFlag();
  return ;
}

//! get bound vars in term e, 
std::set<Expr>  getBoundVars(const Expr& e)
{
  e.clearFlags();
  std::set<Expr> result;  
  recursiveGetBoundVars(e,result);
  e.clearFlags();
  return result;
}

bool isGoodTrigger(const Expr& e, const std::vector<Expr>& bVarsThm)
{
  if(!canGetHead(e))
    return false;

  const std::set<Expr>& bvs = getBoundVars(e);
  if (bvs.size() >= bVarsThm.size())
    {
      for(size_t i=0; i<bVarsThm.size(); i++)
        {
          if (bvs.find(bVarsThm[i]) == bvs.end())
            return false;
        }
      return true;
    }
  else return false;
}


void TheoryQuant::setupTriggers(const Theorem& thm)
{
  const Expr & e = thm.getExpr();
  TRACE("triggers","====================","","");
  TRACE("triggers","setup  ",e.toString(),"");
 
  if  (0 == d_univsTriggers[e].size())
    {
      const std::vector<Expr>& bVarsThm = e.getVars(); 
      const std::vector<Expr> & subterms = getSubTerms(e);
      for( std::vector<Expr>::const_iterator i = subterms.begin(),iend=subterms.end(); i!=iend;i++)
        {
          if(isGoodTrigger(*i,bVarsThm))  
            {
              bool notfound = true;
              for(size_t index=0;index<d_univsTriggers[e].size();index++)
                { 
                  if (i->subExprOf(d_univsTriggers[e][index]))
                    {
                      (d_univsTriggers[e][index])=*i;
                      notfound=false;
                    }
                }
              if (notfound)                 
                d_univsTriggers[e].push_back(*i);
            }
        }
       
      for (size_t  i=0; i< d_univsTriggers[e].size();i++)
        {
          TRACE("triggers", "triggers:", d_univsTriggers[e][i].toString(),"");
          TRACE("triggers","------------","","");
        }
    }
}

/*! \brief Theory interface function to assert quantified formulas
 *
 * pushes in negations and converts to either universally or existentially 
 * quantified theorems. Universals are stored in a database while 
 * existentials are enqueued to be handled by the search engine.
 */

void TheoryQuant::assertFact(const Theorem& e)
{
  TRACE("quant", "assertFact => ", e.toString(), "{");
  Theorem rule, result;
  const Expr& expr = e.getExpr();
  // Ignore existentials
  if(expr.isExists()) {
    TRACE("quant", "assertFact => (ignoring existential) }", "", "");
    return;
  }
  DebugAssert(expr.isForall()
              || (expr.isNot() && (expr[0].isExists() || expr[0].isForall())),
              "Theory of quantifiers cannot handle expression "
              + expr.toString());

  if(expr.isNot()) {//find the right rule to eliminate negation
    if(expr[0].isForall()) {
        rule = d_rules->rewriteNotForall(expr);
      }
    else if(expr[0].isExists()) {
        rule = d_rules->rewriteNotExists(expr);
      }
    result = iffMP(e, rule);
  }
  else
    result = e;
  
  result = d_rules->boundVarElim(result); //eliminate useless bound variables
  
  if(result.getExpr().isExists()) 
  {
    TRACE("quant", "assertFact => enqueuing: ", result.toString(), "}");
    enqueueFact(result);
  }
  else if(result.getExpr().isForall())
  {
    TRACE("quant", "assertFact => storing: ", result.toString(), "}");
    d_univs.push_back(result);
    if(*d_useNew)
      setupTriggers(result);
    //    cout<<"use naieve:"<<(false==*d_useNaiveInst)<<endl;
  }
  else { //quantifier got eliminated in boundVarElim
    TRACE("quant", "assertFact => enqueueing: ", result.toString(), "}");
    enqueueFact(result);
  }

}

void TheoryQuant::recGoodSemMatch(const Expr& e,
                                  const std::vector<Expr>& bVars,
                                  std::vector<Expr>& newInst,
                                  std::set<std::vector<Expr> >& instSet)
{
  size_t curPos = newInst.size();
  if (bVars.size() == curPos)    {
    Expr simpleExpr = simplifyExpr(e.substExpr(bVars,newInst));
    if (simpleExpr.hasFind()){
      std::vector<Expr> temp = newInst;
      instSet.insert(temp);
      TRACE("quant yeting", "new inst found for ", e.toString()+" ==> ", simpleExpr.toString());
    };
  }
  else {
    Type t = getBaseType(bVars[curPos]);
    std::vector<Expr> tyExprs= d_typeExprMap[t];
    if (0 == tyExprs.size())  {
      //      cout <<"Cannot handle type of "<<t.toString()<<endl;;
      return;//has some problem
    }
    else{
      for (size_t i=0;i<tyExprs.size();i++){
        newInst.push_back(tyExprs[i]);
        recGoodSemMatch(e,bVars,newInst,instSet);
        newInst.pop_back();
      }
    }
  }
}


bool TheoryQuant::recSynMatch(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env)
{
  TRACE("quant match", "gterm "+gterm.toString()," e "+vterm.toString(),"");
  DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
  if (BOUND_VAR == vterm.getKind())
    {
      ExprMap<Expr>::iterator p = env.find(vterm);
      if ( p != env.end())
        {
          if (simplifyExpr(gterm) != simplifyExpr(p->second))
            { //TRACE ("match", (vterm.toString()+" bounded to more than one ground term"), "","");
              //cout<< "match" + vterm.toString()+" bounded to more than one ground term";
              return false; 
            }
          else
            return true;
        }
      else
        {
          env[vterm] = gterm;
          return true;
        }
    }
  else
    {
      if(simplifyExpr(vterm) == simplifyExpr(gterm))
        {
          return true;
        }
      else          
        if ( (vterm.arity() != gterm.arity()) || (vterm.getKind() != gterm.getKind() )) 
          //problem, should test whether vterm and gterm has the same kind
          //problem again, should test they have the same head?
          {
                    TRACE("quant match","different sub terms found, arity not same","gterm "+gterm.toString(), "vterm "+vterm.toString());
            return false;
          }
        else
          {
            if(canGetHead(vterm) && canGetHead(gterm)) //still problem here, should test cangethead here?
              {
                if (getHead(vterm) != getHead(gterm))
                  return false;
              }
            for(int i=0;i<vterm.arity();i++)
              {
                if (false == recSynMatch(gterm[i],vterm[i],env))
                  return false;
              }
            return true;
          }
    }
}

/*

std::string TheoryQuant::getHead(const Expr& e)
{
  TRACE("quant gethead", e.toString(),"","");
  //  TRACE("quant gethead", "e kind ",e.getKind()<<endl;
  TRACE("quant gethead", "e kind name ", getEM()->getKindName(e.getKind()), "");
  
  const int kind = e.getKind();

  if (e.isApply())
    return getHead(e.getFun());
  else if ( 2001 == kind ) 
    {
      return getHead(e[0]);
    }
  else if ( ID == kind || UCONST == kind)
    {
      return e.toString();
    }
  else if (BOUND_VAR == kind) 
    {
      return "";
    }
  else
    {
      cout<<"error in get head"<<endl;
      return NULL;
    }
}

*/

void TheoryQuant::goodSynMatch(const Expr& e,
                               const std::vector<Expr> & boundVars,
                               std::set<std::vector<Expr> >& instSet,
                               size_t tBegin)
{
  const CDList<Expr>& allterms = theoryCore()->getTerms();
  for (size_t i=tBegin; i<allterms.size(); i++)
    {
      Expr gterm = allterms[i];
      if (0 == gterm.arity() )
        continue;

      if(canGetHead(gterm) && (getHead(gterm) == getHead(e)) )
      {
        ExprMap<Expr> env;
        env.clear();
        bool found = recSynMatch(gterm,e,env); 
        if(found)
          {
            TRACE("quant yeting", "found one",gterm.toString()+" to " , e.toString());
            std::vector<Expr> inst;
            DebugAssert((boundVars.size() == env.size()),"bound var size != env.size()");
            for(size_t i=0; i<boundVars.size(); i++)
              {
                ExprMap<Expr>::iterator p = env.find(boundVars[i]);
                DebugAssert((p!=env.end()),"bound var cannot be found");
                inst.push_back(p->second);
              }
            instSet.insert(inst);
          }
      }
    }
}


bool TheoryQuant::hasGoodSynInst(const Expr& trig,
                                 std::vector<Expr> & boundVars,
                                 std::set<std::vector<Expr> >& instSet,
                                 size_t tBegin)
{
  const std::set<Expr>& bvs = getBoundVars(trig);
  
  boundVars.clear();
  for(std::set<Expr>::iterator i=bvs.begin(),iend=bvs.end(); i!=iend; ++i)
    boundVars.push_back(*i);
  
  instSet.clear();

  goodSynMatch(trig,boundVars,instSet,tBegin);
   
  if (instSet.size() > 0)
    return true;
  else
    return false;    
}



bool inStrCache(std::set<std::string> cache, std::string str)
{
  return (cache.find(str) != cache.end());
} 

//! find if a good instantiation can be get from a term e
//! if found, return boundVars used and inseSet of all good instantiations 
bool TheoryQuant::hasGoodSemInst(const Expr& e,
                              std::vector<Expr> & boundVars,
                              std::set<std::vector<Expr> >& instSet,
                              size_t tBegin)
{
  const std::set<Expr> bvs = getBoundVars(e);
  
  boundVars.clear();
  for(std::set<Expr>::iterator i=bvs.begin(),iend=bvs.end(); i!=iend; ++i)
    boundVars.push_back(*i);
  
  std::vector<Expr> newInst;
  instSet.clear();
  if(inStrCache(cacheHead,getHead(e)))
     recGoodSemMatch(e,boundVars,newInst,instSet);
   
  if (instSet.size() > 0)
    return true;
  else
    return false;    
}


void genInstSetThm(const std::vector<Expr>&  bVarsThm,
                   const std::vector<Expr>& bVarsTerm,
                   const std::set<std::vector<Expr> >& termInst,
                   std::set<std::vector<Expr> >& instSetThm)
{
  std::vector<int> bVmap;

  for(size_t i=0; i< bVarsThm.size(); ++i)
    {
      bVmap.push_back(-1);
      for (size_t j=0; j<bVarsTerm.size(); j++)
        {
          if (bVarsThm[i] == bVarsTerm[j])
            if(bVmap[i] != -1)
              {
                cout <<"I do not expect here";
              }
            else
              bVmap[i]=j;             
        }
    }

  for(size_t i=0; i< bVarsThm.size(); ++i)
    if( -1 == bVmap[i])
      {
        //      cout<<"well, -1 found"<<endl;;
        return;
      }

  for(std::set<std::vector<Expr> > ::iterator i=termInst.begin(),
        iend=termInst.end();i!=iend; i++)
    {
      std::vector<Expr> buf;
      buf.clear();
      for(size_t j=0; j< bVarsThm.size(); ++j)
        {
          buf.push_back((*i)[bVmap[j]]);
          // cout <<"j="<<j<<" "<< ((*i)[bVmap[j]]).toString()<<endl;
        }
      //      cout <<"end of one"<<endl;;
      instSetThm.insert(buf);
    }
}
        
void TheoryQuant::synInst(const Theorem & univ, size_t tBegin)
{
  const Expr& quantExpr = univ.getExpr();
  TRACE("quant inst", "now dealing with ", quantExpr.toString() , " ");
  const std::vector<Expr>& bVarsThm = quantExpr.getVars();
  const std::vector<Expr>& triggers = d_univsTriggers[quantExpr];
  std::set<std::vector<Expr> > instSetThm;

  for( std::vector<Expr>::const_iterator i= triggers.begin(), iend=triggers.end();i!=iend;++i) 
    {
      std::set<std::vector<Expr> > termInst;
      std::vector<Expr> bVarsTrig;
      const Expr& trig = *i;
       //later, we can add some conditions to handle
      //terms like (+ a b)
      TRACE("quant inst","handle trigger", trig.toString(),"");
      termInst.clear();
      bVarsTrig.clear();
      if(hasGoodSynInst(trig,bVarsTrig,termInst,tBegin))
        {
          genInstSetThm(bVarsThm,bVarsTrig,termInst,instSetThm);
          //here, bVarsThm and bVarsTerm are not the same, most of the time, I think,
          //even they contain the same elements, the order of the elements maybe different.
        }
    }
   
  if(0 == instSetThm.size()) 
    {
      TRACE("quant yeting","sorry, no instantiation found","","");
    }
  else  
    {
      for(std::set<std::vector<Expr> >::iterator i=instSetThm.begin(), iend=instSetThm.end(); i!=iend; ++i) 
        {
          Theorem t = d_rules->universalInst(univ,*i);
          enqueueInst(t);
          TRACE("quant yeting inst", "instantiating", univ.toString(), "|"+(t.toString()));  
        }
    } 
}

void TheoryQuant::semInst(const Theorem & univ, size_t tBegin)
{
  const Expr& quantExpr = univ.getExpr();
  TRACE("quant inst", "now dealing with ", quantExpr.toString() , " ");
  const std::vector<Expr>& bVarsThm = quantExpr.getVars();
  const std::vector<Expr>& triggers = d_univsTriggers[quantExpr];
  std::set<std::vector<Expr> > instSetThm;

  for( std::vector<Expr>::const_iterator i= triggers.begin(), iend=triggers.end();i!=iend;++i) 
    {
      std::set<std::vector<Expr> > termInst;
      std::vector<Expr> bVarsTrig;
      const Expr& trig = *i;
       //later, we can add some conditions to handle
      //terms like (+ a b)
      TRACE("quant inst","handle trigger", trig.toString(),"");
      termInst.clear();
      bVarsTrig.clear();
      if(hasGoodSemInst(trig,bVarsTrig,termInst,tBegin))
        {
          genInstSetThm(bVarsThm,bVarsTrig,termInst,instSetThm);
          //here, bVarsThm and bVarsTerm are not the same, most of the time, I think,
          //even they contain the same elements, the order of the elements maybe different.
        }
    }
   
  if(0 == instSetThm.size()) 
    {
      TRACE("quant yeting","sorry, no instantiation found","","");
    }
  else  
    {
      for(std::set<std::vector<Expr> >::iterator i=instSetThm.begin(), iend=instSetThm.end(); i!=iend; ++i) 
        {
          Theorem t = d_rules->universalInst(univ,*i);
          enqueueInst(t);
          TRACE("quant yeting inst", "instantiating", univ.toString(), "|"+(t.toString()));  
        }
    } 
}

void TheoryQuant::checkSat(bool fullEffort)
{
  d_instThisRound = 0;
  if (!(*d_useNew))
    naiveCheckSat(fullEffort);
  else if (*d_useSemMatch)
    semCheckSat(fullEffort);
  else synCheckSat(fullEffort);
  
  if( (*d_useNew) && (0 == d_instThisRound) && fullEffort )
    {
      naiveCheckSat(fullEffort);
    }
     
}

void TheoryQuant::synCheckSat(bool fullEffort)
{

  //  cout << theoryCore()->getCM()->scopeLevel()<<endl;  
  size_t uSize = d_univs.size() ;

  if (0 == uSize )
    return;

  if((*d_useLazyInst) && (!fullEffort) )
    return;

  if(fullEffort) 
    {
      setIncomplete("Quantifier instantiation");
    }

  if (d_callThisRound > 30)
    return;
  
  const CDList<Expr>& allterms = theoryCore()->getTerms();
  size_t tSize = allterms.size();
  
  TRACE("quant",uSize, " uSize and univsSavedPOS " , d_univsSavedPos);
  TRACE("quant",tSize, " tSize and TermsSavedPos ",d_savedTermsPos);

  if ( (uSize == d_univsSavedPos) && (tSize == d_savedTermsPos) )
    return;
  
  if ( (uSize > d_univsSavedPos) && (tSize > d_savedTermsPos) )
    {
      for(size_t id=d_univsSavedPos; id<uSize; id++) 
        {
          synInst(d_univs[id],0);
        }
      for(size_t id=0; id<d_univsSavedPos; id++) 
        {
          synInst(d_univs[id],d_savedTermsPos);
        }
    }
  
  else if ( (uSize == d_univsSavedPos) && (tSize > d_savedTermsPos) )
    {
      for(size_t id=0 ; id<uSize; id++) 
        {
          synInst(d_univs[id],d_savedTermsPos);
        }
    }
  
  else if ( (uSize > d_univsSavedPos) && (tSize == d_savedTermsPos) )
    {
      for(size_t id=d_univsSavedPos ; id<uSize; id++) 
        {
          synInst(d_univs[id],0);
        }
    }
  else 
    cout <<" I do not believe this"<<endl;;
  
  d_univsSavedPos.set(uSize);
  d_savedTermsPos.set(tSize);

  if(d_instRound==theoryCore()->getCM()->scopeLevel())
    d_callThisRound++;
  else
    {
      d_callThisRound=0;
      d_instRound.set(theoryCore()->getCM()->scopeLevel());
    }

  TRACE("quant","this round; ",d_callThisRound,"");
  return;
 
}


void TheoryQuant::semCheckSat(bool fullEffort)
{
  size_t uSize = d_univs.size() ;
  
  if (0 == uSize )
    return;

  if((*d_useLazyInst) && (!fullEffort) )
    return;

  if(fullEffort) 
    {
      setIncomplete("Quantifier instantiation");
    }

  if (d_callThisRound > 30)
    return;

  
  const CDList<Expr>& allterms = theoryCore()->getTerms();
  size_t tSize = allterms.size();
  
  TRACE("quant",uSize, " uSize and univsSavedPOS " , d_univsSavedPos);
  TRACE("quant",tSize, " tSize and TermsSavedPos ",d_savedTermsPos);

  if ( (uSize == d_univsSavedPos) && (tSize == d_savedTermsPos) )
    return;

  d_typeExprMap.clear();
  cacheHead.clear();
  for (size_t i=0; i<tSize; i++)
    {
      Expr term = allterms[i];
      //      cout << "dealing "<<term.toString()<<" of  type "<<getBaseType(term).toString()<<endl;;
      if (*d_useAtomSem)
        {
          if (0 ==term.arity())
            {     
              Type t = getBaseType(term);
              (d_typeExprMap[t]).push_back(term);
            }
        }
      else
        {      Type t = getBaseType(term);
              (d_typeExprMap[t]).push_back(term);
        }
      if(canGetHead(term))
        cacheHead.insert(getHead(term));
    }
  
  if ( (uSize > d_univsSavedPos) && (tSize > d_savedTermsPos) )
    {
      for(size_t id=d_univsSavedPos; id<uSize; id++) 
        {
          semInst(d_univs[id],0);
        }
      for(size_t id=0; id<d_univsSavedPos; id++) 
        {
          semInst(d_univs[id],d_savedTermsPos);
        }
    }
  
  else if ( (uSize == d_univsSavedPos) && (tSize > d_savedTermsPos) )
    {
      for(size_t id=0 ; id<uSize; id++) 
        {
          semInst(d_univs[id],d_savedTermsPos);
        }
    }
  
  else if ( (uSize > d_univsSavedPos) && (tSize == d_savedTermsPos) )
    {
      for(size_t id=d_univsSavedPos ; id<uSize; id++) 
        {
          semInst(d_univs[id],0);
        }
    }
  else
    cout <<" I do not believe this"<<endl;;
  
  d_univsSavedPos.set(uSize);
  d_savedTermsPos.set(tSize);
  if(d_instRound==theoryCore()->getCM()->scopeLevel())
    d_callThisRound++;
  else
    {
      d_callThisRound=0;
      d_instRound.set(theoryCore()->getCM()->scopeLevel());
    }
  TRACE("quant","this round; ",d_callThisRound,"");
  return;
}



void TheoryQuant::naiveCheckSat(bool fullEffort)
{
  TRACE("quant", "checkSat ", fullEffort, "{");
  IF_DEBUG(int instCount = d_instCount);
  size_t uSize = d_univs.size(), stSize = d_savedTerms.size();
  if(fullEffort && uSize > 0) {
    // First of all, this algorithm is incomplete
    setIncomplete("Quantifier instantiation");
    
    if(d_instCount>=*d_maxQuantInst)
      return;
    //first attempt to instantiate with the saved terms
    //only do this if there are new saved terms or new theroems and 
    // at least some saved terms
    bool savedOnly = ((uSize > d_univsSavedPos.get()  && stSize > 0) ||
                      (stSize > d_savedTermsPos.get()));
    int origCount = d_instCount;
    if(savedOnly)
      {
        TRACE("quant", "checkSat [saved insts]: univs size = ", uSize , " ");
        for(size_t i=0, pos = d_univsSavedPos.get(); i<uSize; i++) {
          if(d_instCount>= *d_maxQuantInst)
            break;
          else
            instantiate(d_univs[i], i>=pos, true,  d_savedTermsPos.get());
        }
        d_univsSavedPos.set(d_univs.size());
        d_savedTermsPos.set(stSize);
      }
    if(!savedOnly || d_instCount == origCount)
      { //instantiate with context dependent assertions terms
        TRACE("quant", "checkSat [context insts]: univs size = ", uSize , " ");
        const CDList<Expr>& assertions = theoryCore()->getTerms();
        int origSize = d_contextTerms.size();
//      for(size_t i=0; i<uSize; i++)
//        assertions.push_back(d_univs[i].getExpr());
        //build the map of all terms grouped into vectors by types
        mapTermsByType(assertions);
        for(size_t i=0, pos = d_univsContextPos.get(); i<uSize; i++) {
          if(d_instCount>= *d_maxQuantInst)
            break;
          else
            instantiate(d_univs[i], i>=pos, false, origSize);
        }
        d_univsContextPos.set(d_univs.size());
      }
    TRACE("quant terse", "checkSat total insts: ",
          d_instCount, ", new "+int2string(d_instCount - instCount));
  }
  TRACE("quant", "checkSat total insts: ", d_instCount, " ");
  TRACE("quant", "checkSat new insts: ", d_instCount - instCount, " ");
  TRACE("quant", "checkSat effort:",  fullEffort, " }");

}


/*! \brief Queues up all possible instantiations of bound
 * variables.
 *
 * The savedMap boolean indicates whether to use savedMap or
 * d_contextMap the all boolean indicates weather to use all
 * instantiation or only new ones and newIndex is the index where
 * new instantiations begin.
 */
void TheoryQuant::instantiate(Theorem univ, bool all, bool savedMap, 
                              size_t newIndex)
{
  
  if(!all && ((savedMap &&  newIndex == d_savedTerms.size())
              ||(!savedMap && newIndex == d_contextTerms.size())))
    return;

  TRACE("quant", "instanitate", all , "{");
  std::vector<Expr> varReplacements;
  recInstantiate(univ, all, savedMap, newIndex, varReplacements);
  TRACE("quant", "instanitate", "", "}");
  
}

 //! does most of the work of the instantiate function.
void TheoryQuant::recInstantiate(Theorem& univ, bool all, bool savedMap,
                                 size_t newIndex, 
                                 std::vector<Expr>& varReplacements)
{
  Expr quantExpr = univ.getExpr();
  const vector<Expr>& boundVars = quantExpr.getVars();
  
  size_t curPos = varReplacements.size(); 
  TRACE("quant", "recInstantiate: ", boundVars.size() - curPos, "");
  //base case: a full vector of instantiations exists
  if(curPos == boundVars.size()) {
    if(!all)
      return;
    Theorem t = d_rules->universalInst(univ, varReplacements);
    d_insts[t.getExpr()] = varReplacements;
    TRACE("quant", "recInstantiate => " , t.toString(), "");
    if(d_instCount< *d_maxQuantInst) {
      d_instCount=d_instCount+1;
      enqueueInst(t);
    }
    return;
  }
  //recursively add all possible instantiations in the next 
  //available space of the vector
  else {
    Type t = getBaseType(boundVars[curPos]);
    int iendC=0, iendS=0, iend;
    std::vector<size_t>* typeVec = NULL; // = d_savedMap[t];
    CDList<size_t>* typeList = NULL; // = *d_contextMap[t];
    if(d_savedMap.count(t) > 0) {
      typeVec = &(d_savedMap[t]);
      iendS = typeVec->size();
      TRACE("quant", "adding from savedMap: ", iendS, "");
    }
    if(!savedMap) {
      if(d_contextMap.count(t) > 0) {
        typeList = d_contextMap[t];
        iendC = typeList->size();
        TRACE("quant", "adding from contextMap:", iendC , "");
      }
    }
    iend = iendC + iendS;
    for(int i =0; i<iend; i++) {
      TRACE("quant", "I must have gotten here!", "", "");
      size_t index;
      if(i<iendS){
        index = (*typeVec)[i];
        varReplacements.push_back(d_savedTerms[index]);
      }
      else {
        index = (*typeList)[i-iendS];
        varReplacements.push_back(d_contextTerms[index]);
      }
      if((index <  newIndex) || (!savedMap && i<iendS))
        recInstantiate(univ, all, savedMap, newIndex,  varReplacements);
      else
        recInstantiate(univ, true, savedMap, newIndex,  varReplacements);
      varReplacements.pop_back();   
    }


  }
}

/*! \brief categorizes all the terms contained in a vector of  expressions by
 * type.
 *
 * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
 */
void TheoryQuant::mapTermsByType(const CDList<Expr>& terms)
{
  Expr trExpr=trueExpr(), flsExpr = falseExpr();
  Type boolT = boolType();
  if(d_contextMap.count(boolT) == 0)
    {
      d_contextMap[boolT] =
        new CDList<size_t>(theoryCore()->getCM()->getCurrentContext());
      size_t pos = d_contextTerms.size();
      d_contextTerms.push_back(trExpr);
      d_contextTerms.push_back(flsExpr);
      (*d_contextMap[boolT]).push_back(pos);
      (*d_contextMap[boolT]).push_back(pos+1);
    }
  for(size_t i=0; i<terms.size(); i++)
    recursiveMap(terms[i]);
  // Add all our saved universals to the pool
  for(size_t i=0; i<d_univs.size(); i++)
    recursiveMap(d_univs[i].getExpr());
}

/*! \brief categorizes all the terms contained in an expressions by
 * type. 
 *
 * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
 * returns true if the expression does not contain bound variables, false
 * otherwise.
 */
bool TheoryQuant::recursiveMap(const Expr& e)
{
  if(d_contextCache.count(e)>0) {
    return(d_contextCache[e]);
  }
  if(e.arity()>0)  {
    for(Expr::iterator it = e.begin(), iend = e.end(); it!=iend; ++it)
      //maps the children and returns a bool
      if(recursiveMap(*it) == false) {
        d_contextCache[e] = false;
      }
  }
  else if(e.getKind() == EXISTS || e.getKind() == FORALL){
    //maps the body
    if(recursiveMap(e.getBody())==false) {
      d_contextCache[e]=false;
    }
  }
  //found a bound variable in the children
  if(d_contextCache.count(e)>0) {
    return false;
  }
  
  if(d_savedCache.count(e) > 0) {
    return true;
  }
  
  Type type = getBaseType(e);
  
  if(!type.isBool() && !(e.getKind()==BOUND_VAR)){
     TRACE("quant", "recursiveMap: found ", 
           e.toString() + " of type " + type.toString(), "");
    int pos = d_contextTerms.size();
    d_contextTerms.push_back(e);
    if(d_contextMap.count(type)==0)
      d_contextMap[type] =
        new CDList<size_t>(theoryCore()->getCM()->getCurrentContext());
    (*d_contextMap[type]).push_back(pos);
  }

  if(e.getKind() == BOUND_VAR) {
    d_contextCache[e] = false;
    return false;
  }
  else {
    d_contextCache[e] = true;
    return true;
  }
  //need  to implement: 
  //insert all instantiations if type is finite and reasonable
  //also need to implement instantiations of subtypes
}

/*!\brief Used to notify the quantifier algorithm of possible 
 * instantiations that were used in proving a context inconsistent.
 */
void TheoryQuant::notifyInconsistent(const Theorem& thm)
{
  // Reset the instantiation count
  // d_instCount = 0;

  if(d_univs.size() == 0)
    return;
  DebugAssert(thm.getExpr().getKind()== FALSE, "notifyInconsistent called with"
        " theorem: " + thm.toString() + " which is not a derivation of false");
  TRACE("quant", "notifyInconsistent: { " , thm.toString(), "}");
  thm.clearAllFlags();
  findInstAssumptions(thm);
  TRACE("quant terse", "notifyInconsistent: savedTerms size = ",
        d_savedTerms.size(), "");
  TRACE("quant terse", "last term: ", 
        d_savedTerms.size()? d_savedTerms.back() : Expr(), "");
}
/*! \brief A recursive function used to find instantiated universals
 * in the hierarchy of assumptions.
 */
void TheoryQuant::findInstAssumptions(const Theorem& thm)
{
  if(thm.isFlagged() || thm.isNull())
    return;
  thm.setFlag();
  const Expr& e = thm.getExpr();
  if(d_insts.count(e) > 0) {
    vector<Expr>& insts = d_insts[e];
    int pos;
    for(vector<Expr>::iterator it = insts.begin(), iend = insts.end(); it!=iend
          ; ++it)
      {
        if(d_savedCache.count(*it) ==  0) {
          TRACE("quant", "notifyInconsistent: found:", (*it).toString(), "");
          d_savedCache[*it] = true;
          pos = d_savedTerms.size();
          d_savedTerms.push_back(*it);
          d_savedMap[getBaseType(*it)].push_back(pos);
        }
      }
  }
  if(thm.isAssump())
    return;
  const Assumptions& a = thm.getAssumptionsRef();
  for(Assumptions::iterator it =a.begin(), iend = a.end(); it!=iend; ++it){
    findInstAssumptions(*it);
  }
}

//! computes the type of a quantified term. Always a  boolean.
void TheoryQuant::computeType(const Expr& e)
{
  switch (e.getKind()) {
  case FORALL:
  case EXISTS: {
    if(!e.getBody().getType().isBool())
      throw TypecheckException("Type mismatch for expression:\n\n   "
                              + e.getBody().toString()
                              + "\n\nhas the following type:\n\n  "
                              + e.getBody().getType().toString()
                              + "\n\nbut the expected type is Boolean:\n\n  ");
    else
      
      e.setType(e.getBody().getType());
    break;
  }
  default:
    DebugAssert(false,"Unexpected kind in Quantifier Theory: " 
                + e.toString());
    break;
  }
}

/*!
 * TCC(forall x.phi(x)) = (forall x. TCC(phi(x)))
 *                         OR (exists x. TCC(phi(x)) & !phi(x))
 * TCC(exists x.phi(x)) = (forall x. TCC(phi(x)))
 *                         OR (exists x. TCC(phi(x)) & phi(x))
 */


Expr TheoryQuant::computeTCC(const Expr& e) {
  DebugAssert(e.isQuantifier(), "Unexpected expression in Quantifier Theory: " 
              + e.toString());

  bool forall(e.getKind() == FORALL);
  const Expr& phi = e.getBody();
  Expr tcc_phi = getTCC(phi);
  Expr forall_tcc = getEM()->newClosureExpr(FORALL, e.getVars(), tcc_phi);
  Expr exists_tcc = getEM()->newClosureExpr(EXISTS, e.getVars(),
                                            tcc_phi && (forall? !phi : phi));
  return (forall_tcc || exists_tcc);  
}


ExprStream&
TheoryQuant::print(ExprStream& os, const Expr& e) {
  switch(os.lang()) {
  case PRESENTATION_LANG: {
    switch(e.getKind()){
    case FORALL:
    case EXISTS: {
      if(!e.isQuantifier()) {
        e.printAST(os);
        break;
      }
      os << "(" << push << ((e.getKind() == FORALL)? "FORALL" : "EXISTS")
         << space << push;
      const vector<Expr>& vars = e.getVars();
      bool first(true);
      os << "(" << push;
      for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
          i!=iend; ++i) {
        if(first) first = false;
        else os << push << "," << pop << space;
        os << *i;
        // The quantifier may be in a raw parsed form, in which case
        // the type is not assigned yet
        if(i->isVar())
          os << ":" << space << pushdag << (*i).getType() << popdag;
      }
      os << push << "): " << pushdag << push
         << e.getBody() << push << ")";
    }
      break;
    default:
      e.printAST(os);
      break;
    }
    break;
  }
  case SMTLIB_LANG: {
    d_theoryUsed = true;
    switch(e.getKind()){
      case FORALL:
      case EXISTS: {
        if(!e.isQuantifier()) {
          e.printAST(os);
          break;
        }
        os << "(" << push << ((e.getKind() == FORALL)? "forall" : "exists")
           << space;
        const vector<Expr>& vars = e.getVars();
        bool first(true);
        //      os << "(" << push;
        for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
            i!=iend; ++i) {
          if(first) first = false;
          else os << space;
          os << "(" << push << *i;
          // The quantifier may be in a raw parsed form, in which case
          // the type is not assigned yet
          if(i->isVar())
            os << space << pushdag << (*i).getType() << popdag;
          os << push << ")" << pop << pop;
        }
        os << pushdag
           << e.getBody() << push << ")";
        break;
      }
      default:
        throw SmtlibException("TheoryQuant::print: SMTLIB_LANG: Unexpected expression: "
                              +getEM()->getKindName(e.getKind()));
        break;
    }
    break;
  } // End of SMTLIB_LANG
  case LISP_LANG: {
    switch(e.getKind()){
    case FORALL:
    case EXISTS: {
      if(!e.isQuantifier()) {
        e.printAST(os);
        break;
      }
      os << "(" << push << ((e.getKind() == FORALL)? "FORALL" : "EXISTS")
         << space;
      const vector<Expr>& vars = e.getVars();
      bool first(true);
      os << "(" << push;
      for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
          i!=iend; ++i) {
        if(first) first = false;
        else os << space;
        os << "(" << push << *i;
        // The quantifier may be in a raw parsed form, in which case
        // the type is not assigned yet
        if(i->isVar())
          os << space << pushdag << (*i).getType() << popdag;
        os << push << ")" << pop << pop;
      }
      os << push << ")" << pop << pop << pushdag
         << e.getBody() << push << ")";
    }
      break;
    default:
      e.printAST(os);
      break;
    }
    break;
  }
  default:
    e.printAST(os);
    break;
  }
  return os;
}

///////////////////////////////////////////////////////////////////////////////
//parseExprOp:
//translating special Exprs to regular EXPR??
///////////////////////////////////////////////////////////////////////////////
Expr
TheoryQuant::parseExprOp(const Expr& e) {
  TRACE("parser", "TheoryQuant::parseExprOp(", e, ")");
  // If the expression is not a list, it must have been already
  // parsed, so just return it as is.
  if(RAW_LIST != e.getKind()) return e;

  DebugAssert(e.arity() > 0,
              "TheoryQuant::parseExprOp:\n e = "+e.toString());
  
  const Expr& c1 = e[0][0];
  const string& opName(c1.getString());
  int kind = getEM()->getKind(opName);
  switch(kind) {
  case FORALL:
  case EXISTS: { // (OP ((v1 ... vn tp1) ...) body)
    if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() > 0))
      throw ParserException("Bad "+opName+" expression: "+e.toString());
    // Iterate through the groups of bound variables
    vector<pair<string,Type> > vars; // temporary stack of bound variables
    for(Expr::iterator i=e[1].begin(), iend=e[1].end(); i!=iend; ++i) {
      if(i->getKind() != RAW_LIST || i->arity() < 2)
        throw ParserException("Bad variable declaration block in "+opName
                            +" expression: "+i->toString()
                            +"\n e = "+e.toString());
      // Iterate through individual bound vars in the group.  The
      // last element is the type, which we have to rebuild and
      // parse, since it is used in the creation of bound variables.
      Type tp(parseExpr((*i)[i->arity()-1]));
      for(int j=0, jend=i->arity()-1; j<jend; ++j) {
        if((*i)[j].getKind() != ID)
          throw ParserException("Bad variable declaration in "+opName+""
                              " expression: "+(*i)[j].toString()+
                              "\n e = "+e.toString());
        vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp));
      }
    }
    // Create all the bound vars and save them in a vector
    vector<Expr> boundVars;
    for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end();
        i!=iend; ++i)
      boundVars.push_back(addBoundVar(i->first, i->second));
    // Rebuild the body
    Expr body(parseExpr(e[2]));
    // Build the resulting Expr as (OP (vars) body)
    Expr res = getEM()->newClosureExpr((kind == FORALL) ? FORALL : EXISTS,
                                       boundVars, body);
    return res;
    break;
  }
//       vector<Expr> bvarDecls, bvars;
//       Expr bvarDeclsExpr;
//       for(Expr::iterator i = e[1].begin(), iend=e[1].end(); i!=iend; ++i) {
//         bvars = i->getKids();
//      bvars.insert(bvars.begin(), Expr(e.getEM(), ID, Expr(e.getEM(), STRING_EXPR, "VARDECL")));
//      bvarDecls.push_back(Expr(e.getEM(), RAW_LIST, bvars));
//      }
//       bvarDeclsExpr = Expr(e.getEM(), RAW_LIST, bvarDecls);
//       return Expr(e.getEM(), kind, parseExpr(bvarDeclsExpr), parseExpr(e[2]));
//     }
  default:
    DebugAssert(false,
                "TheoryQuant::parseExprOp: invalid command or expression: " + e.toString());
    break;
  }
  return e;
}

---