This simplifies the initialization of quantifiers engine.
This PR also makes general improvements to EqualityQuery.
#include "options/quantifiers_options.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
+#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/inst_match.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_state.h"
if( !nh.isNull() ){
if (options::instMaxLevel() != -1)
{
- nh = d_qe->getInternalRepresentative( nh, d_f, d_index );
+ nh = d_qe->getModel()->getInternalRepresentative(nh, d_f, d_index);
//don't consider this if already the instantiation is ineligible
if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f))
{
#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_util.h"
using namespace std;
namespace theory {
namespace quantifiers {
-EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
- QuantifiersState& qs, FirstOrderModel* m)
+EqualityQuery::EqualityQuery(QuantifiersState& qs, FirstOrderModel* m)
: d_qstate(qs),
d_model(m),
d_eqi_counter(qs.getSatContext()),
{
}
-EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
-}
+EqualityQuery::~EqualityQuery() {}
-bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
+bool EqualityQuery::reset(Theory::Effort e)
+{
d_int_rep.clear();
d_reset_count++;
return true;
}
-Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
- Node q,
- int index)
+Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index)
{
Assert(q.isNull() || q.getKind() == FORALL);
Node r = d_qstate.getRepresentative(a);
TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
if (options::quantRepMode() == options::QuantRepMode::EE)
{
- int score = getRepScore(r, q, index, v_tn);
+ int32_t score = getRepScore(r, q, index, v_tn);
if (score >= 0)
{
return r;
Trace("internal-rep-select")
<< "Choose representative for equivalence class : " << eqc
<< ", type = " << v_tn << std::endl;
- int r_best_score = -1;
+ int32_t r_best_score = -1;
for (const Node& n : eqc)
{
- int score = getRepScore(n, q, index, v_tn);
+ int32_t score = getRepScore(n, q, index, v_tn);
if (score != -2)
{
if (r_best.isNull()
//helper functions
-Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
+Node EqualityQuery::getInstance(
+ Node n,
+ const std::vector<Node>& eqc,
+ std::unordered_map<TNode, Node, TNodeHashFunction>& cache)
+{
if(cache.find(n) != cache.end()) {
return cache[n];
}
}
//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
-int EqualityQueryQuantifiersEngine::getRepScore(Node n,
- Node q,
- int index,
- TypeNode v_tn)
+int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn)
{
if( options::cegqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject
return -2;
//score prefer lowest instantiation level
if( n.hasAttribute(InstLevelAttribute()) ){
return n.getAttribute(InstLevelAttribute());
- }else{
- return options::instLevelInputOnly() ? -1 : 0;
- }
- }else{
- if (options::quantRepMode() == options::QuantRepMode::FIRST)
- {
- //score prefers earliest use of this term as a representative
- return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
- }
- else
- {
- Assert(options::quantRepMode() == options::QuantRepMode::DEPTH);
- return quantifiers::TermUtil::getTermDepth( n );
}
+ return options::instLevelInputOnly() ? -1 : 0;
+ }
+ else if (options::quantRepMode() == options::QuantRepMode::FIRST)
+ {
+ // score prefers earliest use of this term as a representative
+ return d_rep_score.find(n) == d_rep_score.end() ? -1 : d_rep_score[n];
}
+ Assert(options::quantRepMode() == options::QuantRepMode::DEPTH);
+ return quantifiers::TermUtil::getTermDepth(n);
}
} /* CVC4::theory::quantifiers namespace */
#include "context/context.h"
#include "expr/node.h"
#include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/quantifiers_state.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
class FirstOrderModel;
+class QuantifiersState;
-/** EqualityQueryQuantifiersEngine class
+/** EqualityQuery class
*
* The main method of this class is the function
* getInternalRepresentative, which is used by instantiation-based methods
* representative based on the internal heuristic, which is currently based on
* choosing the term that was previously chosen as a representative earliest.
*/
-class EqualityQueryQuantifiersEngine : public QuantifiersUtil
+class EqualityQuery : public QuantifiersUtil
{
public:
- EqualityQueryQuantifiersEngine(QuantifiersState& qs,
- FirstOrderModel* m);
- virtual ~EqualityQueryQuantifiersEngine();
+ EqualityQuery(QuantifiersState& qs, FirstOrderModel* m);
+ virtual ~EqualityQuery();
+
/** reset */
bool reset(Theory::Effort e) override;
/* Called for new quantifiers */
void registerQuantifier(Node q) override {}
/** identify */
- std::string identify() const override { return "EqualityQueryQE"; }
+ std::string identify() const override { return "EqualityQuery"; }
/** gets the current best representative in the equivalence
* class of a, based on some heuristic. Currently, the default heuristic
* chooses terms that were previously chosen as representatives
* Node::null() if all terms in the equivalence class of a
* are ineligible.
*/
- Node getInternalRepresentative(Node a, Node q, int index);
+ Node getInternalRepresentative(Node a, Node q, size_t index);
private:
/** the quantifiers state */
/** internal representatives */
std::map< TypeNode, std::map< Node, Node > > d_int_rep;
/** rep score */
- std::map< Node, int > d_rep_score;
+ std::map<Node, int32_t> d_rep_score;
/** the number of times reset( e ) has been called */
- int d_reset_count;
+ size_t d_reset_count;
/** processInferences : will merge equivalence classes in master equality engine, if possible */
bool processInferences( Theory::Effort e );
/** node contains */
Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
/** get score */
- int getRepScore( Node n, Node f, int index, TypeNode v_tn );
-}; /* EqualityQueryQuantifiersEngine */
+ int32_t getRepScore(Node n, Node f, size_t index, TypeNode v_tn);
+}; /* EqualityQuery */
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
-using namespace std;
using namespace CVC4::kind;
using namespace CVC4::context;
-using namespace CVC4::theory::quantifiers::fmcheck;
namespace CVC4 {
namespace theory {
d_qe(nullptr),
d_qreg(qr),
d_treg(tr),
+ d_eq_query(qs, this),
d_forall_asserts(qs.getSatContext()),
d_forallRlvComputed(false)
{
//!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
void FirstOrderModel::finishInit(QuantifiersEngine* qe) { d_qe = qe; }
+Node FirstOrderModel::getInternalRepresentative(Node a, Node q, size_t index)
+{
+ return d_eq_query.getInternalRepresentative(a, q, index);
+}
+
void FirstOrderModel::assertQuantifier( Node n ){
if( n.getKind()==FORALL ){
d_forall_asserts.push_back( n );
return n.getAttribute(ModelBasisAttribute());
}
+EqualityQuery* FirstOrderModel::getEqualityQuery() { return &d_eq_query; }
+
/** needs check */
bool FirstOrderModel::checkNeeded() {
return d_forall_asserts.size()>0;
#define CVC4__FIRST_ORDER_MODEL_H
#include "context/cdlist.h"
-#include "expr/attribute.h"
+#include "theory/quantifiers/equality_query.h"
#include "theory/theory_model.h"
#include "theory/uf/theory_uf_model.h"
class TermRegistry;
class QuantifiersRegistry;
-namespace fmcheck {
- class FirstOrderModelFmc;
-}/* CVC4::theory::quantifiers::fmcheck namespace */
-
-struct IsStarAttributeId {};
-typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
-
// TODO (#1301) : document and refactor this class
class FirstOrderModel : public TheoryModel
{
//!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
/** finish initialize */
void finishInit(QuantifiersEngine* qe);
+ /** get internal representative
+ *
+ * Choose a term that is equivalent to a in the current context that is the
+ * best term for instantiating the index^th variable of quantified formula q.
+ * If no legal term can be found, we return null. This can occur if:
+ * - a's type is not a subtype of the type of the index^th variable of q,
+ * - a is in an equivalent class with all terms that are restricted not to
+ * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
+ * guided instantiation.
+ */
+ Node getInternalRepresentative(Node a, Node q, size_t index);
/** assert quantifier */
void assertQuantifier( Node n );
* Has the term been marked as a model basis term?
*/
static bool isModelBasis(TNode n);
+ /** Get the equality query */
+ EqualityQuery* getEqualityQuery();
protected:
//!!!!!!!!!!!!!!!!!!!!!!! TODO (project #15): temporarily available
QuantifiersRegistry& d_qreg;
/** Reference to the term registry */
TermRegistry& d_treg;
+ /** equality query class */
+ EqualityQuery d_eq_query;
/** list of quantifiers asserted in the current context */
context::CDList<Node> d_forall_asserts;
/**
#include "theory/quantifiers/fmf/first_order_model_fmc.h"
+#include "expr/attribute.h"
#include "theory/quantifiers/fmf/full_model_check.h"
#include "theory/rewriter.h"
namespace quantifiers {
namespace fmcheck {
+/**
+ * Marks that a term represents the entire domain of quantified formula for
+ * the finite model finding fmc algorithm.
+ */
+struct IsStarAttributeId
+{
+};
+using IsStarAttribute = expr::Attribute<IsStarAttributeId, bool>;
+
FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs,
QuantifiersRegistry& qr,
TermRegistry& tr,
Trace("model-engine-debug") << std::endl;
Trace("model-engine-debug") << " Term reps : ";
for( size_t i=0; i<it->second.size(); i++ ){
- Node r = d_quantEngine->getInternalRepresentative( it->second[i], Node::null(), 0 );
+ Node r = fm->getInternalRepresentative(it->second[i], Node::null(), 0);
if (r.isNull())
{
// there was an invalid equivalence class
{
// pick the best possible representative for instantiation, based on past
// use and simplicity of term
- terms[i] = d_qe->getInternalRepresentative(terms[i], q, i);
+ terms[i] = d_qe->getModel()->getInternalRepresentative(terms[i], q, i);
}
Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
if (terms[i].isNull())
d_treg(tr),
d_tr_trie(new inst::TriggerTrie),
d_model(qm),
- d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, qm)),
d_instantiate(
new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)),
d_quants_red(qstate.getUserContext())
{
// initialize the utilities
- d_util.push_back(d_eq_query.get());
+ d_util.push_back(d_model->getEqualityQuery());
// quantifiers registry must come before the remaining utilities
d_util.push_back(&d_qreg);
d_util.push_back(tr.getTermDatabase());
smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
}
-Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
- return d_eq_query->getInternalRepresentative(a, q, index);
-}
-
Node QuantifiersEngine::getNameForQuant(Node q) const
{
return d_qreg.getNameForQuant(q);
class TriggerTrie;
}
namespace quantifiers {
-class EqualityQueryQuantifiersEngine;
class FirstOrderModel;
class Instantiate;
class QModelBuilder;
/** mark relevant quantified formula, this will indicate it should be checked
* before the others */
void markRelevant(Node q);
- /** get internal representative
- *
- * Choose a term that is equivalent to a in the current context that is the
- * best term for instantiating the index^th variable of quantified formula q.
- * If no legal term can be found, we return null. This can occur if:
- * - a's type is not a subtype of the type of the index^th variable of q,
- * - a is in an equivalent class with all terms that are restricted not to
- * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
- * guided instantiation.
- */
- Node getInternalRepresentative(Node a, Node q, int index);
/**
* Get quantifiers name, which returns a variable corresponding to the name of
* quantified formula q if q has a name, or otherwise returns q itself.
std::unique_ptr<inst::TriggerTrie> d_tr_trie;
/** extended model object */
quantifiers::FirstOrderModel* d_model;
- /** equality query class */
- std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
/** instantiate utility */
std::unique_ptr<quantifiers::Instantiate> d_instantiate;
/** skolemize utility */
projects / cvc5.git / commitdiff