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 448d055d4fba87492b2ecdb73e7c4cf02068df1a..01b33eb99da51298bdd6d6fc2c7607c2d5ebece4 100644 (file)
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file valuation.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Tim King, Clark Barrett, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** 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
  **
  ** \brief A "valuation" proxy for TheoryEngine
  **
@@ -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 "theory/theoryof_mode.h"
+#include "options/theory_options.h"
 
 namespace CVC4 {
 
@@ -30,8 +30,7 @@ class TheoryEngine;
 
 namespace theory {
 
-class EntailmentCheckParameters;
-class EntailmentCheckSideEffects;
+class TheoryModel;
 
 /**
  * The status of an equality in the current context.
@@ -53,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).
@@ -105,6 +106,30 @@ public:
    */
   Node getModelValue(TNode var);
 
+  /**
+   * 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
@@ -133,11 +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 */