theory_core.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file theory_core.h
 * 
 * Author: Clark Barrett
 * 
 * Created: Thu Jan 30 16:58:05 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>
 * 
 */
/*****************************************************************************/

#ifndef _cvcl__include__theory_core_h_
#define _cvcl__include__theory_core_h_

#include <queue>
#include "theory.h"
#include "cdmap.h"

namespace CVCL {

class ExprTransform;
class Statistics;
class CoreProofRules;

/*****************************************************************************/
/*!
 *\class TheoryCore
 *\ingroup Theories
 *\brief This theory handles the built-in logical connectives plus equality.
 * It also handles the registration and cooperation among all other theories.
 *
 * Author: Clark Barrett
 *
 * Created: Sat Feb 8 14:54:05 2003
 */
/*****************************************************************************/
class TheoryCore :public Theory {
  friend class Theory;

  //! Context manager
  ContextManager* d_cm;

  //! Theorem manager
  TheoremManager* d_tm;

  //! Core proof rules
  CoreProofRules* d_rules;

  //! Reference to command line flags
  const CLFlags& d_flags;

  //! Reference to statistics
  Statistics& d_statistics;

  //! PrettyPrinter (we own it)
  PrettyPrinter* d_printer;

  //! Type Computer
  ExprManager::TypeComputer* d_typeComputer;

  //! Expr Transformer
  ExprTransform* d_exprTrans;

  //! Assertion queue
  std::queue<Theorem> d_queue;
  //! Queue of facts to be sent to the SearchEngine
  std::vector<Theorem> d_queueSE;

  //! Equality queue
  /*!
   * Contains Theorems in the form of e1==e2, where e2 is i-leaf
   * simplified in the current context.  
   *
   * \sa enqueueEquality().
   */
  std::vector<Theorem> d_equalityQueue;

  //! Inconsistent flag
  CDO<bool> d_inconsistent;
  //! The set of reasons for incompleteness (empty when we are complete)
  CDMap<std::string, bool> d_incomplete;
  //! List of known disequalities (to be processed at every checkSat() call)
  CDList<Theorem> d_diseq;

  //! Proof of inconsistent
  CDO<Theorem> d_incThm;
  //! List of all active terms in the system (for quantifier instantiation)
  CDList<Expr> d_terms;
  //! List of variables that were created up to this point
  CDList<Expr> d_vars;
  //! Database of declared identifiers
  std::map<std::string, Expr> d_globals;
  //! Bound variable stack: a vector of pairs <name, var>
  std::vector<std::pair<std::string, Expr> > d_boundVarStack;

  //! List of all terms that are shared between theories (alien subterms)
  /*! Maps each shared term to its own theory. */
  CDMap<Expr, Theory*> d_sharedTerms;

  std::map<Expr, bool> d_typePredAsserted;

  //! Array of registered theories
  std::vector<Theory*> d_theories;

  //! Array mapping kinds to theories
  std::map<int, Theory*> d_theoryMap;

  //! The theory which has the solver (if any)
  Theory* d_solver;

  //! Mapping of compound type variables to simpler types (model generation)
  ExprHashMap<std::vector<Expr> > d_varModelMap;
  //! Mapping of intermediate variables to their valies
  ExprHashMap<Theorem> d_varAssignments;
  //! List of basic variables (temporary storage for model generation)
  std::vector<Expr> d_basicModelVars;
  //! Mapping of basic variables to simplified expressions (temp. storage)
  /*! There may be some vars which simplify to something else; we save
   * those separately, and keep only those which simplify to
   * themselves.  Once the latter vars are assigned, we'll re-simplify
   * the former variables and use the results as concrete values.
  */
  ExprHashMap<Theorem> d_simplifiedModelVars;

  //! Command line flag whether to simplify in place
  const bool* d_simplifyInPlace;
  //! Which recursive simplifier to use
  Theorem (TheoryCore::*d_currentRecursiveSimplifier)(const Expr&);

  //! Command line flag whether to convert to CNF
  const bool* d_cnfOption;

  //! Resource limit (0==unlimited, 1==no more resources, >=2 - available).
  /*! Currently, it is the number of enqueued facts.  Once the
   * resource is exhausted, the remaining facts will be dropped, and
   * an incomplete flag is set. 
   */
  unsigned d_resourceLimit;

  //! Command line flag whether to dump debugging info on every new fact
  IF_DEBUG(const std::string* d_dumpTrace);
  IF_DEBUG(bool d_inCheckSATCore);
  IF_DEBUG(bool d_inAddFact);
  IF_DEBUG(bool d_inSimplify);
  IF_DEBUG(bool d_inRegisterAtom);

  //! So we get notified every time there's a pop
  friend class CoreNotifyObj;
  class CoreNotifyObj :public ContextNotifyObj {
    TheoryCore* d_theoryCore;
  public:
    CoreNotifyObj(TheoryCore* tc, Context* context)
      : ContextNotifyObj(context), d_theoryCore(tc) {}
    void notify() { d_theoryCore->getEM()->invalidateSimpCache(); }
  };
  CoreNotifyObj d_notifyObj;

  // Equivalence checking variables

  //! Memory Manager index for equiv. check Expr
  size_t d_equivCheckMMidx;

  //! List of implied literals, based on registered atomic formulas of interest
  CDList<Theorem> d_impliedLiterals;

  //! Next index in d_impliedLiterals that has not yet been fetched
  CDO<unsigned> d_impliedLiteralsIdx;

  //! List of theorems from calls to update()
  // These are stored here until the equality lists are finished and then
  // processed by processUpdates()
  std::vector<Theorem> d_update_thms;

  //! List of data accompanying above theorems from calls to update()
  std::vector<Expr> d_update_data;

public:
  /***************************************************************************/
  /*!
   *\class TheoryCore::CoreSatAPI
   *\brief Interface class for callbacks to SAT from Core
   *
   * Author: Clark Barrett
   *
   * Created: Mon Dec  5 18:42:15 2005
   */
  /***************************************************************************/
  class CoreSatAPI {
  public:
    CoreSatAPI() {}
    virtual ~CoreSatAPI() {}
    //! Add a new lemma derived by theory core
    virtual void addLemma(const Theorem& thm) = 0;
    //! Get the bottom-most scope where conflict clauses are still valid
    virtual int getBottomScope() = 0;
    //! Add an assumption to the set of assumptions in the current context
    /*! Assumptions have the form e |- e */
    virtual Theorem addAssumption(const Expr& assump) = 0;
    //! Suggest a splitter to the Sat engine
    /*! \param e is a literal.
     * \param priority is between -10 and 10.  A priority above 0 indicates
     * that the splitter should be favored.  A priority below 0 indicates that
     * the splitter should be delayed. 
     */
    virtual void addSplitter(const Expr& e, int priority) = 0;
  };
private:
  CoreSatAPI* d_coreSatAPI;

private:

  IF_DEBUG(
    //! Print an entry to the dump-trace file: new fact (splitter, BCP...)
    void dumpTrace(const Expr& fact, const std::string& title);
  )

  //! Set the find pointer of an atomic formula and notify SearchEngine
  /*! \param thm is a Theorem(phi) or Theorem(NOT phi), where phi is
   * an atomic formula to get a find pointer to TRUE or FALSE,
   * respectively.
   * \param notifySAT indicates whether to notify the Search Engine of
   * this literal.
   */
  void setFindLiteral(const Theorem& thm, bool notifySAT);
  //! Derived rule for rewriting ITE
  Theorem rewriteIte(const Expr& e);
  //! Core rewrites for literals (NOT and EQ)
  Theorem rewriteLitCore(const Expr& e);
  //! Rewrite n levels deep.  WARNING: no caching here, be careful.
  Theorem rewriteN(const Expr& e, int n);
  /*! @brief An auxiliary function for assertEqualities(); return true
   *  if inconsistency is derived.
   */
  bool processEquality(const Theorem& thm, ExprMap<Theorem>& q);
  //! Private method to get a new theorem producer.
  /*! This method is used ONLY by the TheoryCore constructor.  The
    only reason to have this method is to separate the trusted part of
    the constructor into a separate .cpp file (Alternative is to make
    the entire constructer trusted, which is not very safe). */
  CoreProofRules* createProofRules(TheoremManager* tm);
  //! Enqueue a fact to be sent to the SearchEngine
  void enqueueSE(const Theorem& thm);
  //! Fetch the concrete assignment to the variable during model generation
  Theorem getModelValue(const Expr& e);

  //! Create a new equiv. check Expr (private, only TheoryCore can do that)
  Expr newEquivCkExpr(const Expr& e0, const Expr& e1);

  //! An auxiliary recursive function to process COND expressions into ITE
  Expr processCond(const Expr& e, int i);

  //! Request a unit of resource
  /*! It will be subtracted from the resource limit. 
   *
   * \return true if resource unit is granted, false if no more
   * resources available.
   */
  bool getResource();

public:
  //! Register a SatAPI for TheoryCore
  void registerCoreSatAPI(CoreSatAPI* coreSatAPI)
    { d_coreSatAPI = coreSatAPI; }

  //! Check if the expr is Equiv. Check Expr
  bool isEquivCheckExpr(const Expr& e);
  //! Access LHS of the equiv. check expr
  const Expr& getE0(const Expr& e);
  //! Access RHS of the equiv. check expr
  const Expr& getE1(const Expr& e);

  //! Constructor
  TheoryCore(ContextManager* cm, ExprManager* em,
             TheoremManager* tm, const CLFlags& flags,
             Statistics& statistics);
  //! Destructor
  ~TheoryCore();

  ContextManager* getCM() const { return d_cm; }
  TheoremManager* getTM() const { return d_tm; }
  const CLFlags& getFlags() const { return d_flags; }
  Statistics& getStatistics() const { return d_statistics; }
  ExprTransform* getExprTrans() const { return d_exprTrans; }
  CoreProofRules* getCoreRules() const { return d_rules; }

  //! Get list of terms
  const CDList<Expr>& getTerms() { return d_terms; }

  // Implementation of Theory API
  /*! Variables of uninterpreted types may be sent here, and they
    should be ignored. */
  void addSharedTerm(const Expr& e) { }
  void assertFact(const Theorem& e);
  void checkSat(bool fullEffort);
  Theorem rewrite(const Expr& e);
  void setup(const Expr& e);
  void update(const Theorem& e, const Expr& d);
  Theorem solve(const Theorem& e);

  Theorem simplifyOp(const Expr& e);
  void checkType(const Expr& e);
  void computeType(const Expr& e);
  Type computeBaseType(const Type& t);
  Expr computeTCC(const Expr& e);
  Expr computeTypePred(const Type& t,const Expr& e);
  Expr parseExprOp(const Expr& e);
  ExprStream& print(ExprStream& os, const Expr& e);
  //! Calls for other theories to add facts to refine a coutnerexample.
  void refineCounterExample();
  void computeModelBasic(const std::vector<Expr>& v);

  // User-level API methods

  //! Set the resource limit (0==unlimited).
  void setResourceLimit(unsigned limit);

  //! Check if the current context is inconsistent
  bool inconsistent() { return d_inconsistent ; }
  //! Get the proof of inconsistency for the current context
  /*! \return Theorem(FALSE) */
  Theorem inconsistentThm() { return d_incThm; } 

  /*! @brief Add a new assertion to the core from the user or a SAT
    solver.  Do NOT use it in a decision procedure; use
    enqueueFact(). */
  /*! \sa enqueueFact */
  void addFact(const Theorem& e);

  //! Top-level simplifier
  Theorem simplify(const Expr& e, bool forceRebuild = true);

  /*! @brief To be called by SearchEngine when it believes the context
   * is satisfiable.
   *
   * \return true if definitely consistent or inconsistent and false if
   * consistency is unknown.
   */
  bool checkSATCore();

  //! Register an atomic formula of interest.
  /*! If e or its negation is later deduced, we will add the implied
      literal to d_impliedLiterals */
  void registerAtom(const Expr& e);

  //! Return the next implied literal (NULL Theorem if none)
  Theorem getImpliedLiteral(void);

  //! Return total number of implied literals
  unsigned numImpliedLiterals() { return d_impliedLiterals.size(); }

  //! Return an implied literal by index
  Theorem getImpliedLiteralByIndex(unsigned index);

  //! Check if the current decision branch is marked as incomplete
  bool incomplete() { return d_incomplete.size() > 0 ; }
  //! Check if the branch is incomplete, and return the reasons (strings)
  bool incomplete(std::vector<std::string>& reasons);

  //! Called by search engine
  Theorem rewriteLiteral(const Expr& e);

  //! Parse the generic expression.
  /*! This method should be used in parseExprOp() for recursive calls
   *  to subexpressions, and is the method called by the command
   *  processor.
   */
  Expr parseExpr(const Expr& e);
  //! Top-level call to parseExpr, clears the bound variable stack.
  /*! Use it in VCL instead of parseExpr(). */
  Expr parseExprTop(const Expr& e) {
    d_boundVarStack.clear();
    return parseExpr(e);
  }

  //! Assign t a concrete value val.  Used in model generation.
  void assignValue(const Expr& t, const Expr& val);
  //! Record a derived assignment to a variable (LHS).
  void assignValue(const Theorem& thm);

  //! Adds expression to var database
  void addToVarDB(const Expr & e);
  //! Split compound vars into basic type variables
  /*! The results are saved in d_basicModelVars and
   *  d_simplifiedModelVars.  Also, add new basic vars as shared terms
   *  whenever their type belongs to a different theory than the term
   *  itself.
   */
  void collectBasicVars();
  //! Calls theory specific computeModel, results are placed in map
  void buildModel(ExprMap<Expr>& m);
  //! Recursively build a compound-type variable assignment for e
  void collectModelValues(const Expr& e, ExprMap<Expr>& m);

  Theorem typePred(const Expr& e);

  //! Compute and cache the subtyping predicates for the expression
  /*!
   * Note: e caches the conjunction of <em>all</em> predicates for its
   * subexpressions.  So, when doing a look-up, it is sufficient to
   * assert just the predicate for the top-level e, without traversing
   * e recursively.
   */
  Theorem subtypePredicate(const Expr& e);

  // TODO: These should be private
  //! Enqueue a new fact
  void enqueueFact(const Theorem& e);

  // Must provide proof of inconsistency
  void setInconsistent(const Theorem& e);

  //! Setup additional terms within a theory-specific setup().
  void setupTerm(const Expr& e, Theory* i);

private:
  // Methods provided for benefit of theories.  Access is made available through theory.h

  //! Enqueue a new equality
  void enqueueEquality(const Theorem& e);
  //! Assert a system of equations (1 or more).
  /*! e is either a single equation, or a conjunction of equations
   */
  void assertEqualities(const Theorem& e);

  //! Mark the branch as incomplete
  void setIncomplete(const std::string& reason);

private:
  // Helper functions

  //! A helper function for addFact()
  void processFactQueue();
  //! Process a notify list triggered as a result of new theorem e
  void processNotify(const Theorem& e, NotifyList* L);
  //! The recursive simplifier (to be used only in DP-specific simplifyOp())
  Theorem simplifyRec(const Expr& e);
  //! The full recursive simplifier
  Theorem simplifyFullRec(const Expr& e);
  //! The recursive simplifier with the in-place rewriting optimization
  Theorem simplifyInPlaceRec(const Expr& e);
  //! Transitive composition of other rewrites with the above
  Theorem rewriteCore(const Theorem& e);
  //! Helper for registerAtom
  void setupSubFormulas(const Expr& s, const Expr& e);
  //! Process updates recorded by calls to update()
  void processUpdates();
  /*! @brief The assumptions for e must be in H or phi.  "Core" added
   * to avoid conflict with theory interface function name
   */
  void assertFactCore(const Theorem& e);
  //! Process a newly derived formula
  void assertFormula(const Theorem& e);
  /*! @brief Returns phi |= e = rewriteCore(e).  "Core" added to avoid
    conflict with theory interface function name */
  Theorem rewriteCore(const Expr& e);

  public:
  // Used by vcl.cpp: TODO: tcc stuff should be consolidated
  Theorem3 queryTCC(const Theorem& phi, const Theorem& D_phi);
  Theorem3 implIntro3(const Theorem3& phi,
                      const std::vector<Expr>& assump,
                      const std::vector<Theorem>& tccs);
  

};

//! Printing NotifyList class
std::ostream& operator<<(std::ostream& os, const NotifyList& l); 

}

#endif

---