This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.
theory/quantifiers/term_database.h
theory/quantifiers/term_enumeration.cpp
theory/quantifiers/term_enumeration.h
+ theory/quantifiers/term_registry.cpp
+ theory/quantifiers/term_registry.h
theory/quantifiers/term_util.cpp
theory/quantifiers/term_util.h
theory/quantifiers/theory_quantifiers.cpp
#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
using namespace std;
namespace quantifiers {
EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
- QuantifiersState& qs, TermDb* tdb, FirstOrderModel* m)
+ QuantifiersState& qs, FirstOrderModel* m)
: d_qstate(qs),
- d_tdb(tdb),
d_model(m),
d_eqi_counter(qs.getSatContext()),
d_reset_count(0)
namespace theory {
namespace quantifiers {
-class TermDb;
class FirstOrderModel;
/** EqualityQueryQuantifiersEngine class
{
public:
EqualityQueryQuantifiersEngine(QuantifiersState& qs,
- TermDb* tdb,
FirstOrderModel* m);
virtual ~EqualityQueryQuantifiersEngine();
/** reset */
private:
/** the quantifiers state */
QuantifiersState& d_qstate;
- /** Pointer to the term database */
- TermDb* d_tdb;
/** Pointer to the model */
FirstOrderModel* d_model;
/** quantifiers equality inference */
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
-#include "theory/arith/arith_msum.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_inference_manager.h"
#include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
using namespace CVC4::kind;
return os;
}
-TermDbSygus::TermDbSygus(QuantifiersEngine* qe,
- QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : d_quantEngine(qe),
- d_qstate(qs),
+TermDbSygus::TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim)
+ : d_qstate(qs),
d_qim(qim),
d_syexp(new SygusExplain(this)),
d_ext_rw(new ExtendedRewriter(true)),
// TODO :issue #1235 split and document this class
class TermDbSygus {
public:
- TermDbSygus(QuantifiersEngine* qe,
- QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim);
~TermDbSygus() {}
/** Reset this utility */
bool reset(Theory::Effort e);
static void toStreamSygus(std::ostream& out, Node n);
private:
- /** reference to the quantifiers engine */
- QuantifiersEngine* d_quantEngine;
/** Reference to the quantifiers state */
QuantifiersState& d_qstate;
/** The quantifiers inference manager */
--- /dev/null
+/********************* */
+/*! \file term_registry.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** 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 term registry class
+ **/
+
+#include "theory/quantifiers/term_registry.h"
+
+#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "theory/quantifiers/quantifiers_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+TermRegistry::TermRegistry(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : d_presolve(qs.getUserContext(), true),
+ d_presolveCache(qs.getUserContext()),
+ d_termEnum(new TermEnumeration),
+ d_termDb(new TermDb(qs, qim, qr)),
+ d_sygusTdb(nullptr)
+{
+ if (options::sygus() || options::sygusInst())
+ {
+ // must be constructed here since it is required for datatypes finistInit
+ d_sygusTdb.reset(new TermDbSygus(qs, qim));
+ }
+}
+
+void TermRegistry::presolve()
+{
+ d_termDb->presolve();
+ d_presolve = false;
+ // add all terms to database
+ if (options::incrementalSolving() && !options::termDbCd())
+ {
+ Trace("quant-engine-proc")
+ << "Add presolve cache " << d_presolveCache.size() << std::endl;
+ for (const Node& t : d_presolveCache)
+ {
+ addTerm(t);
+ }
+ Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
+ }
+}
+
+void TermRegistry::addTerm(Node n, bool withinQuant)
+{
+ // don't add terms in quantifier bodies
+ if (withinQuant && !options::registerQuantBodyTerms())
+ {
+ return;
+ }
+ if (options::incrementalSolving() && !options::termDbCd())
+ {
+ d_presolveCache.insert(n);
+ }
+ // only wait if we are doing incremental solving
+ if (!d_presolve || !options::incrementalSolving() || options::termDbCd())
+ {
+ d_termDb->addTerm(n);
+ if (d_sygusTdb.get() && options::sygusEvalUnfold())
+ {
+ d_sygusTdb->getEvalUnfold()->registerEvalTerm(n);
+ }
+ }
+}
+
+TermDb* TermRegistry::getTermDatabase() const { return d_termDb.get(); }
+
+TermDbSygus* TermRegistry::getTermDatabaseSygus() const
+{
+ return d_sygusTdb.get();
+}
+
+TermEnumeration* TermRegistry::getTermEnumeration() const
+{
+ return d_termEnum.get();
+}
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file term_registry.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** 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 term registry class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H
+#define CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H
+
+#include <map>
+#include <unordered_set>
+
+#include "context/cdhashset.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * Term Registry, which manages notifying modules within quantifiers about
+ * (ground) terms that exist in the current context.
+ */
+class TermRegistry
+{
+ using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+
+ public:
+ TermRegistry(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
+ /** Presolve */
+ void presolve();
+
+ /**
+ * Add term n, which notifies the term database that the ground term n
+ * exists in the current context.
+ *
+ * @param n the term to add
+ * @param withinQuant whether n occurs within a quantified formula body
+ */
+ void addTerm(Node n, bool withinQuant = false);
+
+ /** get term database */
+ TermDb* getTermDatabase() const;
+ /** get term database sygus */
+ TermDbSygus* getTermDatabaseSygus() const;
+ /** get term enumeration utility */
+ TermEnumeration* getTermEnumeration() const;
+
+ private:
+ /** has presolve been called */
+ context::CDO<bool> d_presolve;
+ /** the set of terms we have seen before presolve */
+ NodeSet d_presolveCache;
+ /** term enumeration utility */
+ std::unique_ptr<TermEnumeration> d_termEnum;
+ /** term database */
+ std::unique_ptr<TermDb> d_termDb;
+ /** sygus term database */
+ std::unique_ptr<TermDbSygus> d_sygusTdb;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H */
d_decManager(nullptr),
d_pnm(pnm),
d_qreg(),
+ d_treg(qstate, qim, d_qreg),
d_tr_trie(new inst::TriggerTrie),
d_model(nullptr),
d_builder(nullptr),
- d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg)),
d_eq_query(nullptr),
- d_sygus_tdb(nullptr),
d_instantiate(
new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)),
- d_term_enum(new quantifiers::TermEnumeration),
d_quants_prereg(qstate.getUserContext()),
- d_quants_red(qstate.getUserContext()),
- d_presolve(qstate.getUserContext(), true),
- d_presolve_in(qstate.getUserContext()),
- d_presolve_cache(qstate.getUserContext())
+ d_quants_red(qstate.getUserContext())
{
//---- utilities
// quantifiers registry must come before the other utilities
d_util.push_back(&d_qreg);
- d_util.push_back(d_term_db.get());
-
- if (options::sygus() || options::sygusInst())
- {
- // must be constructed here since it is required for datatypes finistInit
- d_sygus_tdb.reset(new quantifiers::TermDbSygus(this, qstate, qim));
- }
+ d_util.push_back(d_treg.getTermDatabase());
d_util.push_back(d_instantiate.get());
d_model.reset(new quantifiers::FirstOrderModel(
this, qstate, d_qreg, "FirstOrderModel"));
}
- d_eq_query.reset(new quantifiers::EqualityQueryQuantifiersEngine(
- qstate, d_term_db.get(), d_model.get()));
+ d_eq_query.reset(
+ new quantifiers::EqualityQueryQuantifiersEngine(qstate, d_model.get()));
d_util.insert(d_util.begin(), d_eq_query.get());
}
}
quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
{
- return d_term_db.get();
+ return d_treg.getTermDatabase();
}
quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
{
- return d_sygus_tdb.get();
+ return d_treg.getTermDatabaseSygus();
+}
+quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
+{
+ return d_treg.getTermEnumeration();
}
quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
{
{
return d_skolemize.get();
}
-quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
-{
- return d_term_enum.get();
-}
inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
{
return d_tr_trie.get();
{
return true;
}
- else if (d_term_enum->mayComplete(tn))
+ else if (d_treg.getTermEnumeration()->mayComplete(tn))
{
return true;
}
for( unsigned i=0; i<d_modules.size(); i++ ){
d_modules[i]->presolve();
}
- d_term_db->presolve();
- d_presolve = false;
- //add all terms to database
- if (options::incrementalSolving() && !options::termDbCd())
- {
- Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl;
- for (const Node& t : d_presolve_cache)
- {
- addTermToDatabase(t);
- }
- Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
- }
+ // presolve with term registry, which populates the term database based on
+ // terms registered before presolve when in incremental mode
+ d_treg.presolve();
}
void QuantifiersEngine::ppNotifyAssertions(
{
mdl->assertNode(f);
}
- addTermToDatabase(d_qreg.getInstConstantBody(f), true);
+ // add term to the registry
+ d_treg.addTerm(d_qreg.getInstConstantBody(f), true);
}
-void QuantifiersEngine::addTermToDatabase(Node n, bool withinQuant)
-{
- // don't add terms in quantifier bodies
- if (withinQuant && !options::registerQuantBodyTerms())
- {
- return;
- }
- if (options::incrementalSolving() && !options::termDbCd())
- {
- if( d_presolve_in.find( n )==d_presolve_in.end() ){
- d_presolve_in.insert( n );
- d_presolve_cache.push_back( n );
- }
- }
- //only wait if we are doing incremental solving
- if (!d_presolve || !options::incrementalSolving() || options::termDbCd())
- {
- d_term_db->addTerm(n);
- if (d_sygus_tdb && options::sygusEvalUnfold())
- {
- d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
- }
- }
-}
-
-void QuantifiersEngine::eqNotifyNewClass(TNode t) {
- addTermToDatabase( t );
-}
+void QuantifiersEngine::eqNotifyNewClass(TNode t) { d_treg.addTerm(t); }
void QuantifiersEngine::markRelevant( Node q ) {
d_model->markRelevant( q );
#include "context/cdlist.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/quantifiers_registry.h"
+#include "theory/quantifiers/term_registry.h"
#include "util/statistics_registry.h"
namespace CVC4 {
quantifiers::TermDb* getTermDatabase() const;
/** get term database sygus */
quantifiers::TermDbSygus* getTermDatabaseSygus() const;
+ /** get term enumeration utility */
+ quantifiers::TermEnumeration* getTermEnumeration() const;
/** get instantiate utility */
quantifiers::Instantiate* getInstantiate() const;
/** get skolemize utility */
quantifiers::Skolemize* getSkolemize() const;
- /** get term enumeration utility */
- quantifiers::TermEnumeration* getTermEnumeration() const;
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() const;
//---------------------- end utilities
bool reduceQuantifier(Node q);
public:
+ /** notification when master equality engine is updated */
+ void eqNotifyNewClass(TNode t);
/** mark relevant quantified formula, this will indicate it should be checked
* before the others */
void markRelevant(Node q);
- /** add term to database */
- void addTermToDatabase(Node n, bool withinQuant = false);
- /** notification when master equality engine is updated */
- void eqNotifyNewClass(TNode t);
/** get internal representative
*
* Choose a term that is equivalent to a in the current context that is the
//------------- quantifiers utilities
/** The quantifiers registry */
quantifiers::QuantifiersRegistry d_qreg;
+ /** The term registry */
+ quantifiers::TermRegistry d_treg;
/** all triggers will be stored in this trie */
std::unique_ptr<inst::TriggerTrie> d_tr_trie;
/** extended model object */
std::unique_ptr<quantifiers::FirstOrderModel> d_model;
/** model builder */
std::unique_ptr<quantifiers::QModelBuilder> d_builder;
- /** term database */
- std::unique_ptr<quantifiers::TermDb> d_term_db;
/** equality query class */
std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
- /** sygus term database */
- std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb;
/** instantiate utility */
std::unique_ptr<quantifiers::Instantiate> d_instantiate;
/** skolemize utility */
std::unique_ptr<quantifiers::Skolemize> d_skolemize;
- /** term enumeration utility */
- std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
//------------- end quantifiers utilities
/**
* The modules utility, which contains all of the quantifiers modules.
/** quantifiers reduced */
BoolMap d_quants_red;
std::map<Node, Node> d_quants_red_lem;
- /** has presolve been called */
- context::CDO<bool> d_presolve;
- /** presolve cache */
- NodeSet d_presolve_in;
- NodeList d_presolve_cache;
};/* class QuantifiersEngine */
}/* CVC4::theory namespace */
projects / cvc5.git / commitdiff