search.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file search.h
 * \brief Abstract API to the proof search engine
 * 
 * Author: Clark Barrett, Vijay Ganesh (Clausal Normal Form Converter)
 * 
 * Created: Fri Jan 17 13:35:03 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__search_h_
#define _cvcl__include__search_h_

#include <vector>
#include "cdo.h"

namespace CVCL {

class SearchEngineRules;
class Theorem;
class Expr;
class Proof;
class TheoryCore;
class CommonProofRules;

template<class Data> class ExprMap;

  /*! \defgroup SE Search Engine 
   * \ingroup VC
   * The search engine includes Boolean reasoning and coordinates with theory
   * reasoning.  It consists of a generic abstract API (class SearchEngine) and
   * subclasses implementing concrete instances of search engines.
   */

  //! API to to a generic proof search engine
  /*! \ingroup SE */
class SearchEngine {

protected:
  /*! \addtogroup SE 
   * @{
   */

  //! Access to theory reasoning
  TheoryCore* d_core;

  //! Common proof rules
  CommonProofRules* d_commonRules;

  //! Proof rules for the search engine
  SearchEngineRules* d_rules;

  //! Create the trusted component
  /*! This function is defined in search_theorem_producer.cpp */
  SearchEngineRules* createRules();

 public:

  //! Constructor
  SearchEngine(TheoryCore* core);

  //! Destructor
  virtual ~SearchEngine();

  //! Name of this search engine
  virtual const std::string& getName() = 0;

  //! Accessor for TheoryCore
  TheoryCore* theoryCore() { return d_core; }

  //! Register an atomic formula of interest.
  /*! Registered atoms are tracked by the decision procedures.  If one of them
      is deduced to be true or false, it is added to a list of implied literals.
      Implied literals can be retrieved with the getImpliedLiteral function */
  virtual void registerAtom(const Expr& e) = 0;

  //! Return next literal implied by last assertion.  Null Expr if none.
  /*! Returned literals are either registered atomic formulas or their negation
   */
  virtual Theorem getImpliedLiteral() = 0;

  //! Checks the validity of a formula in the current context
  /*! If the query is valid, it returns a theorem and the scope and context
   * should be the same as when called.  If the query is invalid, it returns
   * a NULL theorem and the context will be one which falsifies the query. */
  virtual Theorem checkValid(const Expr& e) = 0;

  //! Reruns last check with e as an additional assumption
  /*! This method should only be called after a query which is invalid.
   */
  virtual Theorem restart(const Expr& e) = 0;

  //! Returns to context immediately before last call to checkValid
  /*! This method should only be called after a query which is invalid.
   */
  virtual void returnFromCheck() = 0;

  //! Returns the result of the most recent valid theorem
  /*! Returns Null Theorem if last call was not valid */
  virtual Theorem lastThm() = 0;

  /*! @brief Generate and add an assumption to the set of
   * assumptions in the current context. */
  /*! By default, the assumption is added at the current scope.  The default
   * can be overridden by specifying the scope parameter. */
  virtual Theorem newUserAssumption(const Expr& e, int scope = -1) = 0;

  //! Get all user assumptions made in this and all previous contexts.
  /*! User assumptions are created either by calls to newUserAssumption or
   * a call to checkValid.  In the latter case, the negated query is added
   * as an assumption.
   * \param assumptions should be empty on entry.
  */
  virtual void getUserAssumptions(std::vector<Expr>& assumptions) = 0;

  //! Get assumptions made internally in this and all previous contexts.
  /*! Internal assumptions are literals assumed by the sat solver.
   * \param assumptions should be empty on entry.
  */
  virtual void getInternalAssumptions(std::vector<Expr>& assumptions) = 0;

  //! Get all assumptions made in this and all previous contexts.
  /*! \param assumption should be an empty vector which will be filled \
    with the assumption */
  virtual void getAssumptions(std::vector<Expr>& assumptions) = 0;

  //! Check if the formula has already been assumed previously
  virtual bool isAssumption(const Expr& e) = 0;

  //! Will return the set of assertions which make the queried formula false.
  /*! This method should only be called after an invalid query It will try to
   * return the simplest possible set of assertions which are sufficient to make
   * the queried expression false.
   * \param assertions should be empty on entry.
   * \param inOrder if true, returns the assertions in the order they were
   * asserted.  This is slightly more expensive than inOrder = false.
  */
  virtual void getCounterExample(std::vector<Expr>& assertions,
                                 bool inOrder = true) = 0;

  //! Returns the proof term for the last proven query
  /*! It should be called only after a valid query.
   * In any other case, it returns Null. */
  virtual Proof getProof() = 0;

  /*! @brief Build a concrete Model (assign values to variables),
   * should only be called after an invalid query. */
  void getConcreteModel(ExprMap<Expr>& m);

  /* @} */ // end of group SE

};


}

#endif

---