/********************* */
/*! \file first_order_model.h
** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Paul Meng, Morgan Deters
** 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 Model extended classes
**/
#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 {
class QuantifiersEngine;
+struct ModelBasisAttributeId
+{
+};
+typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
+// for APPLY_UF terms, 1 : term has direct child with model basis attribute,
+// 0 : term has no direct child with model basis attribute.
+struct ModelBasisArgAttributeId
+{
+};
+typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t>
+ ModelBasisArgAttribute;
+
namespace quantifiers {
class TermDb;
-class FirstOrderModelIG;
-
namespace fmcheck {
class FirstOrderModelFmc;
}/* CVC4::theory::quantifiers::fmcheck namespace */
-class FirstOrderModelQInt;
-class FirstOrderModelAbs;
-
struct IsStarAttributeId {};
typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
+// TODO (#1301) : document and refactor this class
class FirstOrderModel : public TheoryModel
{
-protected:
- /** quant engine */
- QuantifiersEngine * d_qe;
- /** whether an axiom is asserted */
- context::CDO< bool > d_axiom_asserted;
- /** list of quantifiers asserted in the current context */
- context::CDList<Node> d_forall_asserts;
- /** is model set */
- context::CDO< bool > d_isModelSet;
- /** get variable id */
- std::map< Node, std::map< Node, int > > d_quant_var_id;
- /** get current model value */
- virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
-public: //for Theory Quantifiers:
+ public:
+ FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
+
+ virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
/** assert quantifier */
void assertQuantifier( Node n );
/** get number of asserted quantifiers */
- int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
+ unsigned getNumAssertedQuantifiers();
/** get asserted quantifier */
- Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
- /** bool axiom asserted */
- bool isAxiomAsserted() { return d_axiom_asserted; }
+ Node getAssertedQuantifier( unsigned i, bool ordered = false );
/** initialize model for term */
- void initializeModelForTerm( Node n );
- virtual void processInitializeModelForTerm( Node n ) = 0;
- virtual void processInitializeQuantifier( Node q ) {}
-public:
- FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
- virtual ~FirstOrderModel() {}
- virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
- virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
- virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
- virtual FirstOrderModelAbs * asFirstOrderModelAbs() { return NULL; }
+ void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
// initialize the model
- void initialize( bool considerAxioms = true );
- virtual void processInitialize( bool ispre ) = 0;
- /** mark model set */
- void markModelSet() { d_isModelSet = true; }
- /** is model set */
- bool isModelSet() { return d_isModelSet; }
- /** get current model value */
- Node getCurrentModelValue( Node n, bool partial = false );
+ void initialize();
/** get variable id */
int getVariableId(TNode q, TNode n) {
return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
}
- /** get some domain element */
- Node getSomeDomainElement(TypeNode tn);
-private:
- //list of inactive quantified formulas
- std::map< TNode, bool > d_quant_active;
-public:
+ /** do we need to do any work? */
+ bool checkNeeded();
/** reset round */
void reset_round();
- /** set quantified formula active/inactive
- * a quantified formula may be set inactive if for instance:
- * - it is entailed by other quantified formulas
+ /** mark quantified formula relevant */
+ void markRelevant( Node q );
+ /** 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 );
-};/* class FirstOrderModel */
-
-
-class FirstOrderModelIG : public FirstOrderModel
-{
-public: //for Theory UF:
- //models for each UF operator
- std::map< Node, uf::UfModelTree > d_uf_model_tree;
- //model generators
- std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
-private:
- //map from terms to the models used to calculate their value
- std::map< Node, bool > d_eval_uf_use_default;
- std::map< Node, uf::UfModelTree > d_eval_uf_model;
- void makeEvalUfModel( Node n );
- //index ordering to use for each term
- std::map< Node, std::vector< int > > d_eval_term_index_order;
- void makeEvalUfIndexOrder( Node n );
- /** get current model value */
- Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
-//the following functions are for evaluating quantifier bodies
-public:
- FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
- FirstOrderModelIG * asFirstOrderModelIG() { return this; }
- // initialize the model
- void processInitialize( bool ispre );
- //for initialize model
- void processInitializeModelForTerm( Node n );
- /** reset evaluation */
- void resetEvaluate();
- /** evaluate functions */
- int evaluate( Node n, int& depIndex, RepSetIterator* ri );
- Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri );
-public:
- //statistics
- int d_eval_formulas;
- int d_eval_uf_terms;
- int d_eval_lits;
- int d_eval_lits_unknown;
-private:
- //default evaluate term function
- Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri );
- //temporary storing which literals have failed
- void clearEvalFailed( int index );
- std::map< Node, bool > d_eval_failed;
- std::map< int, std::vector< Node > > d_eval_failed_lits;
-};/* class FirstOrderModelIG */
+ /** 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) const;
+ /** get model basis term */
+ Node getModelBasisTerm(TypeNode tn);
+ /** is model basis term */
+ bool isModelBasisTerm(Node n);
+ /** get model basis term for op */
+ Node getModelBasisOpTerm(Node op);
+ /** get model basis */
+ Node getModelBasis(Node q, Node n);
+ /** get model basis arg */
+ unsigned getModelBasisArg(Node n);
+ /** get some domain element */
+ Node getSomeDomainElement(TypeNode tn);
+ /** initialize representative set for type
+ *
+ * This ensures that TheoryModel::d_rep_set
+ * is initialized for type tn. In particular:
+ * (1) If tn is an uninitialized (unconstrained)
+ * uninterpreted sort, then we interpret it
+ * as a set of size one,
+ * (2) If tn is a "small" enumerable finite type,
+ * then we ensure that all its values are in
+ * TheoryModel::d_rep_set.
+ *
+ * Returns true if the initialization was complete,
+ * in that the set for tn in TheoryModel::d_rep_set
+ * has all representatives of type tn.
+ */
+ bool initializeRepresentativesForType(TypeNode tn);
+ protected:
+ /** quant engine */
+ QuantifiersEngine* d_qe;
+ /** list of quantifiers asserted in the current context */
+ context::CDList<Node> d_forall_asserts;
+ /**
+ * 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 */
+ virtual void processInitializeModelForTerm(Node n) {}
+ /** process initialize quantifier */
+ virtual void processInitializeQuantifier(Node q) {}
+ /** process initialize */
+ virtual void processInitialize(bool ispre) {}
+
+ private:
+ // list of inactive quantified formulas
+ std::map<TNode, bool> d_quant_active;
+ /** map from types to model basis terms */
+ std::map<TypeNode, Node> d_model_basis_term;
+ /** map from ops to model basis terms */
+ std::map<Node, Node> d_model_basis_op_term;
+ /** map from instantiation terms to their model basis equivalent */
+ std::map<Node, Node> d_model_basis_body;
+ /** map from universal quantifiers to model basis terms */
+ std::map<Node, std::vector<Node> > d_model_basis_terms;
+ /** compute model basis arg */
+ void computeModelBasisArgAttribute(Node n);
+};/* class FirstOrderModel */
namespace fmcheck {
class FirstOrderModelFmc : public FirstOrderModel
{
friend class FullModelChecker;
-private:
+
+ private:
/** models for UF */
std::map<Node, Def * > d_models;
- std::map<TypeNode, Node > d_model_basis_rep;
std::map<TypeNode, Node > d_type_star;
- Node intervalOp;
- Node getUsedRepresentative(Node n, bool strict = false);
/** get current model value */
- Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
- void processInitializeModelForTerm(Node n);
-public:
+ void processInitializeModelForTerm(Node n) override;
+
+ public:
FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
- virtual ~FirstOrderModelFmc();
- FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
+ ~FirstOrderModelFmc() override;
+ FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
// initialize the model
- void processInitialize( bool ispre );
+ void processInitialize(bool ispre) override;
Node getFunctionValue(Node op, const char* argPrefix );
bool isStar(Node n);
Node getStar(TypeNode tn);
- Node getStarElement(TypeNode tn);
- bool isModelBasisTerm(Node n);
- Node getModelBasisTerm(TypeNode tn);
- bool isInterval(Node n);
- Node getInterval( Node lb, Node ub );
- bool isInRange( Node v, Node i );
};/* class FirstOrderModelFmc */
}/* CVC4::theory::quantifiers::fmcheck namespace */
-
-class QIntDef;
-class QuantVarOrder;
-class FirstOrderModelQInt : public FirstOrderModel
-{
- friend class QIntervalBuilder;
-private:
- /** uf op to some representation */
- std::map<Node, QIntDef * > d_models;
- /** representatives to ids */
- std::map< Node, int > d_rep_id;
- std::map< TypeNode, Node > d_min;
- std::map< TypeNode, Node > d_max;
- /** quantifiers to information regarding variable ordering */
- std::map<Node, QuantVarOrder * > d_var_order;
- /** get current model value */
- Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
- void processInitializeModelForTerm(Node n);
-public:
- FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name);
- FirstOrderModelQInt * asFirstOrderModelQInt() { return this; }
- void processInitialize( bool ispre );
- Node getFunctionValue(Node op, const char* argPrefix );
-
- Node getUsedRepresentative( Node n );
- int getRepId( Node n ) { return d_rep_id.find( n )==d_rep_id.end() ? -1 : d_rep_id[n]; }
- bool isLessThan( Node v1, Node v2 );
- Node getMin( Node v1, Node v2 );
- Node getMax( Node v1, Node v2 );
- Node getMinimum( TypeNode tn ) { return getNext( tn, Node::null() ); }
- Node getMaximum( TypeNode tn );
- bool isMinimum( Node n ) { return n==getMinimum( n.getType() ); }
- bool isMaximum( Node n ) { return n==getMaximum( n.getType() ); }
- Node getNext( TypeNode tn, Node v );
- Node getPrev( TypeNode tn, Node v );
- bool doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur );
- QuantVarOrder * getVarOrder( Node q ) { return d_var_order[q]; }
-
- void processInitializeQuantifier( Node q ) ;
- unsigned getOrderedNumVars( Node q );
- TypeNode getOrderedVarType( Node q, int i );
- int getOrderedVarNumToVarNum( Node q, int i );
-};/* class FirstOrderModelQInt */
-
-class AbsDef;
-
-class FirstOrderModelAbs : public FirstOrderModel
-{
-public:
- std::map< Node, AbsDef * > d_models;
- std::map< Node, bool > d_models_valid;
- std::map< TNode, unsigned > d_rep_id;
- std::map< TypeNode, unsigned > d_domain;
- std::map< Node, std::vector< int > > d_var_order;
- std::map< Node, std::map< int, int > > d_var_index;
-private:
- /** get current model value */
- Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
- void processInitializeModelForTerm(Node n);
- void processInitializeQuantifier( Node q );
- void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
-public:
- FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
- FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
- void processInitialize( bool ispre );
- unsigned getRepresentativeId( TNode n );
- TNode getUsedRepresentative( TNode n );
- bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
- Node getFunctionValue(Node op, const char* argPrefix );
- Node getVariable( Node q, unsigned i );
-};
-
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__FIRST_ORDER_MODEL_H */
+#endif /* CVC4__FIRST_ORDER_MODEL_H */
projects / cvc5.git / blobdiff