/*! \file first_order_model.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King, Paul Meng
+ ** Andrew Reynolds, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** 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
#include "cvc4_private.h"
-#ifndef __CVC4__FIRST_ORDER_MODEL_H
-#define __CVC4__FIRST_ORDER_MODEL_H
+#ifndef CVC4__FIRST_ORDER_MODEL_H
+#define CVC4__FIRST_ORDER_MODEL_H
+#include "expr/attribute.h"
#include "theory/theory_model.h"
#include "theory/uf/theory_uf_model.h"
-#include "expr/attribute.h"
namespace CVC4 {
namespace theory {
struct IsStarAttributeId {};
typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
-/** Quantifiers representative bound
- *
- * This class is used for computing (finite)
- * bounds for the domain of a quantifier
- * in the context of a RepSetIterator
- * (see theory/rep_set.h).
- */
-class QRepBoundExt : public RepBoundExt
-{
- public:
- QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
- virtual ~QRepBoundExt() {}
- /** set bound */
- RepSetIterator::RsiEnumType setBound(Node owner,
- unsigned i,
- std::vector<Node>& elements) override;
- /** reset index */
- bool resetIndex(RepSetIterator* rsi,
- Node owner,
- unsigned i,
- bool initial,
- std::vector<Node>& elements) override;
- /** initialize representative set for type */
- bool initializeRepresentativesForType(TypeNode tn) override;
- /** get variable order */
- bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override;
-
- private:
- /** quantifiers engine associated with this bound */
- QuantifiersEngine* d_qe;
- /** indices that are bound integer enumeration */
- std::map<unsigned, bool> d_bound_int;
-};
-
// TODO (#1301) : document and refactor this class
class FirstOrderModel : public TheoryModel
{
void reset_round();
/** mark quantified formula relevant */
void markRelevant( Node q );
- /** get relevance value */
- int getRelevanceValue( Node q );
- /** set quantified formula active/inactive
- * a quantified formula may be set inactive if for instance:
- * - it is entailed by other quantified formulas
+ /** set quantified formula active/inactive
+ *
+ * This indicates that quantified formula is "inactive", that is, it need
+ * not be considered during this instantiation round.
+ *
+ * A quantified formula may be set inactive if for instance:
+ * - It is entailed by other quantified formulas, or
+ * - All of its instances are known to be true in the current model.
+ *
+ * This method should be called after a call to FirstOrderModel::reset_round,
+ * and before calls to QuantifiersModule check calls. A common place to call
+ * this method is during QuantifiersModule reset_round calls.
*/
void setQuantifierActive( TNode q, bool active );
- /** is quantified formula active */
- bool isQuantifierActive( TNode q );
+ /** is quantified formula active?
+ *
+ * Returns false if there has been a call to setQuantifierActive( q, false )
+ * during this instantiation round.
+ */
+ bool isQuantifierActive(TNode q) const;
/** is quantified formula asserted */
- bool isQuantifierAsserted( TNode q );
+ bool isQuantifierAsserted(TNode q) const;
/** get model basis term */
Node getModelBasisTerm(TypeNode tn);
/** is model basis term */
QuantifiersEngine* d_qe;
/** list of quantifiers asserted in the current context */
context::CDList<Node> d_forall_asserts;
- /** quantified formulas marked as relevant */
- unsigned d_rlv_count;
- std::map<Node, unsigned> d_forall_rlv;
+ /**
+ * The (ordered) list of quantified formulas marked as relevant using
+ * markRelevant, where the quantified formula q in the most recent
+ * call to markRelevant comes last in the list.
+ */
std::vector<Node> d_forall_rlv_vec;
+ /** The last quantified formula marked as relevant, if one exists. */
Node d_last_forall_rlv;
+ /**
+ * The list of asserted quantified formulas, ordered by relevance.
+ * Relevance is a dynamic partial ordering where q1 < q2 if there has been
+ * a call to markRelevant( q1 ) after the last call to markRelevant( q2 )
+ * (or no call to markRelevant( q2 ) has been made).
+ *
+ * This list is used primarily as an optimization for conflict-based
+ * instantiation so that quantifed formulas that have been instantiated
+ * most recently are processed first, since these are (statistically) more
+ * likely to have conflicting instantiations.
+ */
std::vector<Node> d_forall_rlv_assert;
+ /**
+ * Whether the above list has been computed. This flag is updated during
+ * reset_round and is valid within a full effort check.
+ */
+ bool d_forallRlvComputed;
/** get variable id */
std::map<Node, std::map<Node, int> > d_quant_var_id;
/** process initialize model for term */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__FIRST_ORDER_MODEL_H */
+#endif /* CVC4__FIRST_ORDER_MODEL_H */
projects / cvc5.git / blobdiff