/********************* */
/*! \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
**
#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 {
namespace theory {
+class TheoryModel;
+
/**
* The status of an equality in the current context.
*/
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);
d_engine(engine) {
}
- /*
+ /**
* Return true if n has an associated SAT literal
*/
bool isSatLiteral(TNode n) const;
*/
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
*/
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 */