theory.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file theory.cpp
 * 
 * Author: Clark Barrett
 * 
 * Created: Thu Jan 30 15:11:55 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_core.h"
#include "common_proof_rules.h"
#include "typecheck_exception.h"
#include "theorem_manager.h"


using namespace CVCL;
using namespace std;


Theory::Theory(void) : d_theoryCore(NULL) { }


Theory::Theory(TheoryCore* theoryCore, const string& name)
  : d_em(theoryCore->getEM()),
    d_theoryCore(theoryCore),
    d_commonRules(theoryCore->getTM()->getRules()),
    d_name(name), d_theoryUsed(false) {
}


Theory::~Theory(void) { }


void Theory::computeModelTerm(const Expr& e, vector<Expr>& v) {
  TRACE("model", "Theory::computeModelTerm(", e, "): is a variable");
  //  v.push_back(e);
}


Theorem Theory::simplifyOp(const Expr& e) {
  int ar = e.arity();
  if (ar > 0) {
    vector<Theorem> newChildrenThm;
    vector<unsigned> changed;
    for(int k = 0; k < ar; ++k) {
      // Recursively simplify the kids
      Theorem thm = simplifyRec(e[k]);
      if (thm.getLHS() != thm.getRHS()) {
        newChildrenThm.push_back(thm);
        changed.push_back(k);
      }
    }
    if(changed.size() > 0)
      return d_commonRules->substitutivityRule(e, changed, newChildrenThm);
  }
  return reflexivityRule(e);
}


Expr Theory::computeTCC(const Expr& e) {
  vector<Expr> kids;
  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
    kids.push_back(getTCC(*i));
  return (kids.size()>0) ?
    d_commonRules->rewriteAnd(andExpr(kids)).getRHS() : trueExpr();
}


bool Theory::inconsistent()
{
  return d_theoryCore->inconsistent();
}


void Theory::setInconsistent(const Theorem& e)
{
  TRACE("facts assertFact", ("setInconsistent[" + getName() + "->]("), e, ")");
  TRACE("conflict", ("setInconsistent[" + getName() + "->]("), e, ")");
  IF_DEBUG(debugger.counter("conflicts from DPs")++);
  d_theoryCore->setInconsistent(e);
}


void Theory::setIncomplete(const string& reason)
{
  TRACE("facts assertFact", "setIncomplete["+getName()+"](", reason, ")");
  d_theoryCore->setIncomplete(reason);
}


Theorem Theory::simplify(const Expr& e, bool forceRebuild)
{
  TRACE("simplify", ("simplify[" + getName() + "->]("), e, ") {");
  Theorem res(d_theoryCore->simplify(e, forceRebuild));
  TRACE("simplify", "simplify[" + getName() + "] => ", res, "}");
  return res;
}


Theorem Theory::simplifyRec(const Expr& e)
{
  TRACE("simplifyRec", ("simplifyRec[" + getName() + "->]("), e, ") {");
  Theorem res(d_theoryCore->simplifyRec(e));
  TRACE("simplifyRec", "simplifyRec[" + getName() + "] => ", res, "}");
  return res;
}


void Theory::enqueueFact(const Theorem& e)
{
  TRACE("facts assertFact", ("enqueueFact[" + getName() + "->]("), e, ")");
  d_theoryCore->enqueueFact(e);
}


void Theory::enqueueEquality(const Theorem& e)
{
  TRACE("facts assertFact", ("enqueueEquality[" + getName() + "->]("), e, ")");
  DebugAssert(e.isRewrite(), "Theory::enqueueEquality("+e.toString()+")");
//   DebugAssert(leavesAreSimp(e.getRHS()),
//            "Theory::enqueueEquality("+e.toString()+")");
  d_theoryCore->enqueueEquality(e);
}


void Theory::assertEqualities(const Theorem& e)
{
  d_theoryCore->assertEqualities(e);
}


void Theory::addSplitter(const Expr& e, int priority) {
  TRACE("facts assertFact", "addSplitter[" + getName() + "->](", e,
        ", pri="+int2string(priority)+")");
  d_theoryCore->d_coreSatAPI->addSplitter(e, priority);
}


void Theory::assignValue(const Expr& t, const Expr& val) {
  TRACE("facts assertFact", "assignValue["+getName()+"](", t, ", "+
        val.toString()+") {");
  d_theoryCore->assignValue(t, val);
  TRACE("facts assertFact", "assignValue[", getName(), "] => }");
}


void Theory::assignValue(const Theorem& thm) {
  TRACE("facts assertFact", "assignValue["+getName()+"](", thm, ") {");
  d_theoryCore->assignValue(thm);
  TRACE("facts assertFact", "assignValue[", getName(), "] => }");
}


void Theory::registerKinds(Theory* theory, vector<int>& kinds)
{
  vector<int>::const_iterator k;
  vector<int>::const_iterator kEnd;
  for (k = kinds.begin(), kEnd = kinds.end(); k != kEnd; ++k) {
    DebugAssert(d_theoryCore->d_theoryMap.count(*k) == 0,
                "kind already registered: "+getEM()->getKindName(*k)
                +" = "+int2string(*k));
    d_theoryCore->d_theoryMap[*k] = theory;
  }
}


void Theory::registerTheory(Theory* theory, vector<int>& kinds,
                            bool hasSolver)
{
  registerKinds(theory, kinds);
  d_theoryCore->d_theories.push_back(theory);
  if (hasSolver) {
    DebugAssert(!d_theoryCore->d_solver,"Solver already registered");
    d_theoryCore->d_solver = theory;
  }
}


int Theory::getNumTheories()
{
  return d_theoryCore->d_theories.size();
}


bool Theory::hasTheory(int kind) {
  return (d_theoryCore->d_theoryMap.count(kind) > 0);
}


Theory* Theory::theoryOf(int kind)
{
  DebugAssert(d_theoryCore->d_theoryMap.count(kind) > 0,
              "Unknown operator: " + getEM()->getKindName(kind));
  return d_theoryCore->d_theoryMap[kind];
}


Theory* Theory::theoryOf(const Expr& e)
{
  if (e.isNot() || e.isEq()) {
    return theoryOf(e[0]);
  }
  if (e.isApply()) {
    return theoryOf(e.getOpKind());
  }
  if (!e.isVar()) {
    return theoryOf(e.getKind());
  }
  // Theory of a var is determined by its *base* type, since SUBTYPE
  // may have different base types, but SUBTYPE itself belongs to
  // TheoryCore.
  const Expr& typeExpr = getBaseType(e).getExpr();
  DebugAssert(!typeExpr.isNull(),"Null type");
  int kind = typeExpr.getKind();
  if (typeExpr.isApply()) kind = typeExpr.getOpKind();
  DebugAssert(d_theoryCore->d_theoryMap.count(kind) > 0,
              "Unknown operator: " + getEM()->getKindName(kind));
  return d_theoryCore->d_theoryMap[kind];
}


Theorem Theory::find(const Expr& e)
{
  Theorem thm1 = e.hasFind() ? e.getFind() : reflexivityRule(e);
  const Expr& e1 = thm1.getRHS();
  if (e1 == e || !e1.hasFind()) return thm1;
  Theorem thm2 = find(e1);
  DebugAssert(thm2.getLHS()==e1,"");
  if (thm2.getLHS() != thm2.getRHS()) {
    e.setFind(transitivityRule(thm1,thm2));
    return e.getFind();
  }
  return thm1;
}


Expr Theory::getTCC(const Expr& e)
{
  const Expr& tccCached = e.lookupTCC();
  if (!tccCached.isNull()) return tccCached;
  if(e.isVar()) {
    e.setTCC(trueExpr());
    return trueExpr();
  }
  Theory* i = theoryOf(e.getKind());
  TRACE("tccs", "computeTCC["+i->getName()+"](", e, ") {");
  e.setTCC(i->computeTCC(e));
  TRACE("tccs", "computeTCC["+i->getName()+"] => ", e.lookupTCC(), " }");
  return e.lookupTCC();
}


Type Theory::getBaseType(const Expr& e)
{
  return getBaseType(e.getType());
}


Type Theory::getBaseType(const Type& tp)
{
  const Expr& e = tp.getExpr();
  DebugAssert(!e.isNull(), "Theory::getBaseType(Type(Null))");
  // See if we have it cached
  Type res(e.lookupType());
  if(!res.isNull()) return res;

  DebugAssert(theoryOf(e) != NULL,
              "Theory::getBaseType(): No theory for the type: "
              +tp.toString());
  TRACE("types", "getBaseType["+theoryOf(e)->getName()+"](", e, ") {");
  res= theoryOf(e)->computeBaseType(tp);
  TRACE("types", "getBaseType["+theoryOf(e)->getName()+"] => ", res, " }");
  e.setType(res);
  return res;
}


Expr Theory::getTypePred(const Type& t, const Expr& e)
{
  Expr pred;
  Theory *i = theoryOf(t.getExpr().getKind());
  TRACE("typePred", "computeTypePred["+i->getName()+"]("+t.toString()+", ", e, ") {");
  pred = i->computeTypePred(t, e);
  TRACE("typePred", "computeTypePred["+i->getName()+"] => ", pred, " }");
  return pred;
}


Theorem Theory::updateHelper(const Expr& e)
{
  vector<Theorem> newChildrenThm;
  vector<unsigned> changed;
  int k(0), ar(e.arity());
  Theorem thm;
  for (; k < ar; ++k) {
    thm = find(e[k]);
    if (thm.getLHS() != thm.getRHS()) {
      newChildrenThm.push_back(thm);
      changed.push_back(k);
    }
  }
  if (changed.size() == 0) thm = reflexivityRule(e);
  else thm = d_commonRules->substitutivityRule(e, changed, newChildrenThm);
  return thm;
}


//! Setup a term for congruence closure (must have sig and rep attributes)
void Theory::setupCC(const Expr& e) {
  TRACE("facts setup", "setupCC["+getName()+"](", e, ") {");
  for (int k = 0; k < e.arity(); ++k) {
    e[k].addToNotify(this, e);
  }
  Theorem thm = reflexivityRule(e);
  e.setSig(thm);
  e.setRep(thm);
  TRACE_MSG("facts setup", "setupCC["+getName()+"]() => }");
}


//! Update a term w.r.t. congruence closure (must be setup with setupCC())
void Theory::updateCC(const Theorem& e, const Expr& d) {
  TRACE("facts update", "updateCC["+getName()+"]("+e.getExpr().toString()+", ",
        d, ") {");
  int k, ar(d.arity());
  const Theorem& dEQdsig = d.getSig();
  if (!dEQdsig.isNull()) {
    const Expr& dsig = dEQdsig.getRHS();
    Theorem thm = updateHelper(d);
    const Expr& sigNew = thm.getRHS();
    if (sigNew == dsig) {
      TRACE_MSG("facts update", "updateCC["+getName()+"]() [no change] => }");
      return;
    }
    dsig.setRep(Theorem());
    const Theorem& repEQsigNew = sigNew.getRep();
    if (!repEQsigNew.isNull()) {
      d.setSig(Theorem());
      enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
    }
    else {
      for (k = 0; k < ar; ++k) {
        if (sigNew[k] != dsig[k]) {
          sigNew[k].addToNotify(this, d);
        }
      }
      d.setSig(thm);
      sigNew.setRep(thm);
    }
  }
  TRACE_MSG("facts update", "updateCC["+getName()+"]() => }");
}


//! Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
Theorem Theory::rewriteCC(const Expr& e) {
  const Theorem& rep = e.getRep();
  if (rep.isNull()) return reflexivityRule(e);
  else return symmetryRule(rep);
}


Expr Theory::parseExpr(const Expr& e) {
  TRACE("facts parseExpr", "parseExpr(", e, ") {");
  Expr res(d_theoryCore->parseExpr(e));
  TRACE("facts parseExpr", "parseExpr => ", res, " }");
  return res;
}


void Theory::getModelTerm(const Expr& e, vector<Expr>& v)
{
  Theory *i = theoryOf(getBaseType(e).getExpr());
  TRACE("model", "computeModelTerm["+i->getName()+"](", e, ") {");
  IF_DEBUG(unsigned size = v.size();)
  i->computeModelTerm(e, v);
  TRACE("model", "computeModelTerm[", i->getName(), "] => }");
  DebugAssert(v.size() <= size || v.back() != e, "Primitive var was pushed on "
              "the stack in computeModelTerm["+i->getName()
              +"]: "+e.toString());
  
}


Theorem Theory::getModelValue(const Expr& e) {
  return d_theoryCore->getModelValue(e);
}


bool Theory::isLeafIn(const Expr& e1, const Expr& e2)
{
  DebugAssert(isLeaf(e1),"Expected leaf");
  if (e1 == e2) return true;
  if (theoryOf(e2) != this) return false;
  for(Expr::iterator i=e2.begin(), iend=e2.end(); i != iend; ++i)
    if (isLeafIn(e1, *i)) return true;
  return false;
}


bool Theory::leavesAreSimp(const Expr& e)
{
  if (isLeaf(e)) {
    bool res(e.getFind().getRHS() == e);
    IF_DEBUG(if(!res) TRACE("facts leavesAreSimp", "leavesAreSimp(", e, 
                            " = "+e.getFind().getRHS().toString()
                            +") => false"));
    return res;
  }
  for (int k = 0; k < e.arity(); ++k) {
    if (!leavesAreSimp(e[k])) return false;
  }
  return true;
}


Expr Theory::newVar(const string& name, const Type& type)
{
  DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
  Expr res = resolveID(name);
  Type t;
//   Expr res = lookupVar(name, &t);
  if (!res.isNull()) {
    t = res.getType();
    if (t != type) {
      throw TypecheckException
        ("incompatible redefinition of variable "+name+":\n "
         "already defined with type: "+t.toString()
         +"\n the new type is: "+type.toString());
    }
    return res;
  }
  // Replace TYPEDEF with its definition
  t = type;
  while(t.getExpr().getKind() == TYPEDEF) {
    DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
    t = t[1];
  }
  if (type.isBool()) res = d_em->newSymbolExpr(name, UCONST);
  else res = getEM()->newVarExpr(name);

  // Add the variable for constructing a concrete model
  d_theoryCore->addToVarDB(res);
  // Add the new global declaration
  installID(name, res);
  
  DebugAssert(type.getExpr().getKind() != ARROW,"");
  DebugAssert(res.lookupType().isNull(), 
              "newVarExpr: redefining a variable "
               + name);
  res.setType(type);
  return res;
}


Expr Theory::newVar(const string& name, const Type& type, const Expr& def)
{
  DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
  Type t;
  Expr res = resolveID(name);
  if (!res.isNull()) {
    throw TypecheckException
      ("Redefinition of variable "+name+":\n "
       "This variable is already defined.");
  }
  Expr v;
  if (type.isBool()) v = getEM()->newSymbolExpr(name, UCONST);
  else v = getEM()->newVarExpr(name);
  res = Expr(CONSTDEF, v, def);

  // Replace TYPEDEF with its definition
  t = type;
  while(t.getExpr().getKind() == TYPEDEF) {
    DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
    t = t[1];
  }
  v.setType(type);

  // Typecheck
  if(getBaseType(def) != getBaseType(v)) {
    throw TypecheckException("Type mismatch in constant definition:\n"
                             "Constant "+v.toString()+
                             " is declared with type:\n  "
                             +v.getType().toString()
                             +"\nBut the type of definition is\n  "
                             +def.getType().toString());
  }
  DebugAssert(type.getExpr().getKind() != ARROW,"");
  DebugAssert(res.lookupType().isNull(), 
              "newVarExpr: redefining a variable "
               + name);

  // Add the new global declaration
  installID(name, res);
  
  return res;
}


Op Theory::newFunction(const string& name, const Type& type,
                       bool computeTransClosure) {
  DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
  Expr res = resolveID(name);
  Type t;
  if (!res.isNull()) {
    t = res.getType();
    throw TypecheckException
      ("Redefinition of variable "+name+":\n "
       "already defined with type: "+t.toString()
       +"\n the new type is: "+type.toString());
  }
  res = getEM()->newSymbolExpr(name, UFUNC);
  // Replace TYPEDEF with its definition
  t = type;
  while(t.getExpr().getKind() == TYPEDEF) {
    DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
    t = t[1];
  }
  res.setType(t);
  // Add it to the database of variables for concrete model generation
  d_theoryCore->addToVarDB(res);
  // Add the new global declaration
  installID(name, res);
  if (computeTransClosure &&
      t.isFunction() && t.arity() == 3 && t[2].isBool())
    res.setComputeTransClosure();
  return res.mkOp();
}


Op Theory::newFunction(const string& name, const Type& type,
                       const Expr& def) {
  DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
  Expr res = resolveID(name);
  Type t;
  if (!res.isNull()) {
    t = res.getType();
    throw TypecheckException
      ("Redefinition of variable "+name+":\n "
       "already defined with type: "+t.toString()
       +"\n the new type is: "+type.toString());
  }
  res = getEM()->newSymbolExpr(name, UFUNC);
  // Replace TYPEDEF with its definition
  t = type;
  while(t.getExpr().getKind() == TYPEDEF) {
    DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
    t = t[1];
  }
  res.setType(t);
  // Add the new global declaration
  installID(name, res);
  return res.mkOp();
}


static int boundVarCount = 0;


Expr Theory::addBoundVar(const string& name, const Type& type) {
  ostringstream ss;
  ss << boundVarCount++;
  Expr v(getEM()->newBoundVarExpr(name, ss.str(), type));
  d_theoryCore->d_boundVarStack.push_back(pair<string,Expr>(name,v));
  TRACE("vars", "addBoundVar("+name+", ", type, ") => "+v.toString());
  return v;
}


Expr Theory::addBoundVar(const string& name, const Type& type,
                         const Expr& def) {
  Expr res;
  // Without the type, just replace the bound variable with the definition
  if(type.isNull())
    res = def;
  else {
    // When type is given, construct (LETDECL var, def) for the typechecker
    ostringstream ss;
    ss << boundVarCount++;
    res = Expr(LETDECL,
               getEM()->newBoundVarExpr(name, ss.str(), type), def);
  }
  d_theoryCore->d_boundVarStack.push_back(pair<string,Expr>(name,res));
  TRACE("vars", "addBoundVar("+name+", "+type.toString()+", ", def,
        ") => "+res.toString());
  return res;
}


Expr Theory::lookupVar(const string& name, Type* type)
{
  Expr e = getEM()->newVarExpr(name);
  *type = e.lookupType();
//   if ((*type).isNull()) {
//     e = newApplyExpr(Op(UFUNC, e));
//     *type = e.lookupType();
    if ((*type).isNull()) return Expr();
//   }
  return e;
}


// TODO: reconcile this with parser-driven new type expressions
Type Theory::newTypeExpr(const string& name)
{
  Expr res = resolveID(name);
  if (!res.isNull()) {
    throw TypecheckException
      ("Redefinition of type variable "+name+":\n "
       "This variable is already defined.");
  }
  res = Expr(TYPEDECL, getEM()->newStringExpr(name));
  // Add the new global declaration
  installID(name, res);
  return Type(res);
}

//! Create a new type abbreviation with the given name 
Type Theory::newTypeExpr(const string& name, const Type& def)
{
  Expr res = resolveID(name);
  if (!res.isNull()) {
    throw TypecheckException
      ("Redefinition of type variable "+name+":\n "
       "This variable is already defined.");
  }
  res = def.getExpr();
  // Add the new global declaration
  installID(name, res);
  return Type(res);
}


Expr Theory::resolveID(const string& name) {
  TRACE("vars", "resolveID(", name, ") {");
  Expr res; // Result is Null by default
  // First, look up the bound variable stack
  for(vector<pair<string, Expr> >::iterator
        i=d_theoryCore->d_boundVarStack.begin(),
        iend=d_theoryCore->d_boundVarStack.end();
      i!=iend && res.isNull(); ++i) {
    if(i->first == name)
      res = i->second;
  }
  if(res.isNull()) {
    // Next, check in the globals
    map<string,Expr>::iterator i=d_theoryCore->d_globals.find(name),
      iend=d_theoryCore->d_globals.end();
    if(i!=iend)
      res = i->second;
  }
  TRACE("vars", "resolveID => ", res, " }");
  return res;
}


void Theory::installID(const string& name, const Expr& e)
{
  DebugAssert(resolveID(name).isNull(),
              "installID called on existing identifier");
  d_theoryCore->d_globals[name] = e;
}


Theorem Theory::typePred(const Expr& e) {
  return d_theoryCore->typePred(e);
}


Theorem Theory::subtypePredicate(const Expr& e) {
  return d_theoryCore->subtypePredicate(e);
}

---