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 36e62a402233895ea04c3035141f5fa842d68d30..01b33eb99da51298bdd6d6fc2c7607c2d5ebece4 100644 (file)
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file valuation.h
  ** \verbatim
- ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): taking, ajreynol, barrett
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Dejan Jovanovic
+ ** This file is part of the CVC4 project.
+ ** 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,10 +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/theory_options.h"
 
 namespace CVC4 {
 
@@ -29,6 +30,8 @@ class TheoryEngine;
 
 namespace theory {
 
+class TheoryModel;
+
 /**
  * The status of an equality in the current context.
  */
@@ -47,11 +50,13 @@ enum EqualityStatus {
   EQUALITY_FALSE_IN_MODEL,
   /** The equality is completely unknown */
   EQUALITY_UNKNOWN
-};
+};/* enum EqualityStatus */
+
+std::ostream& operator<<(std::ostream& os, EqualityStatus s);
 
 /**
- * Returns true if the two statuses are compatible, i.e. bot TRUE
- * or both FALSE (regardles of inmodel/propagation).
+ * Returns true if the two statuses are compatible, i.e. both TRUE
+ * or both FALSE (regardless of inmodel/propagation).
  */
 bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);
 
@@ -62,7 +67,7 @@ public:
     d_engine(engine) {
   }
 
-  /*
+  /**
    * Return true if n has an associated SAT literal
    */
   bool isSatLiteral(TNode n) const;
@@ -101,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
@@ -125,9 +154,24 @@ public:
    */
   unsigned getAssertionLevel() const;
 
+  /**
+   * Request an entailment check according to the given theoryOfMode.
+   * See theory.h for documentation on entailmentCheck().
+   */
+  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 */