Updates to theory preprocess equality (#5776)

[cvc5.git] / src / theory / valuation.h

diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 54af14fdd4c23bd4889ef13d236442689ae7d208..01b33eb99da51298bdd6d6fc2c7607c2d5ebece4 100644 (file)
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -2,10 +2,10 @@
 /*! \file valuation.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Dejan Jovanovic, Andrew Reynolds
+ **   Morgan Deters, Andrew Reynolds, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -18,11 +18,11 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__VALUATION_H
-#define __CVC4__THEORY__VALUATION_H
+#ifndef CVC4__THEORY__VALUATION_H
+#define CVC4__THEORY__VALUATION_H
 
 #include "expr/node.h"
-#include "options/theoryof_mode.h"
+#include "options/theory_options.h"
 
 namespace CVC4 {
 
@@ -30,8 +30,6 @@ class TheoryEngine;
 
 namespace theory {
 
-class EntailmentCheckParameters;
-class EntailmentCheckSideEffects;
 class TheoryModel;
 
 /**
@@ -54,6 +52,8 @@ enum EqualityStatus {
   EQUALITY_UNKNOWN
 };/* enum EqualityStatus */
 
+std::ostream& operator<<(std::ostream& os, EqualityStatus s);
+
 /**
  * Returns true if the two statuses are compatible, i.e. both TRUE
  * or both FALSE (regardless of inmodel/propagation).
@@ -107,10 +107,29 @@ public:
   Node getModelValue(TNode var);
 
   /**
-   * Returns pointer to model.
+   * Returns pointer to model. This model is only valid during last call effort
+   * check.
    */
   TheoryModel* getModel();
-  
+
+  //-------------------------------------- static configuration of the model
+  /**
+   * Set that k is an unevaluated kind in the TheoryModel, if it exists.
+   * See TheoryModel::setUnevaluatedKind for details.
+   */
+  void setUnevaluatedKind(Kind k);
+  /**
+   * Set that k is an unevaluated kind in the TheoryModel, if it exists.
+   * See TheoryModel::setSemiEvaluatedKind for details.
+   */
+  void setSemiEvaluatedKind(Kind k);
+  /**
+   * Set that k is an irrelevant kind in the TheoryModel, if it exists.
+   * See TheoryModel::setIrrelevantKind for details.
+   */
+  void setIrrelevantKind(Kind k);
+  //-------------------------------------- end static configuration of the model
+
   /**
    * Ensure that the given node will have a designated SAT literal
    * that is definitionally equal to it.  The result of this function
@@ -139,14 +158,20 @@ public:
    * Request an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().
    */
-  std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL);
+  std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
 
   /** need check ? */
   bool needCheck() const;
-  
+
+  /**
+   * Is the literal lit (possibly) critical for satisfying the input formula in
+   * the current context? This call is applicable only during collectModelInfo
+   * or during LAST_CALL effort.
+   */
+  bool isRelevant(Node lit) const;
 };/* class Valuation */
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__VALUATION_H */
+#endif /* CVC4__THEORY__VALUATION_H */