read_only = true
help = "consider ground terms within bodies of quantified formulas for matching"
-[[option]]
- name = "inferArithTriggerEq"
- category = "regular"
- long = "infer-arith-trigger-eq"
- type = "bool"
- default = "false"
- read_only = true
- help = "infer equalities for trigger terms based on solving arithmetic equalities"
-
[[option]]
name = "strictTriggers"
category = "regular"
namespace theory {
namespace quantifiers {
-EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){
-
+EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
+ context::Context* c, QuantifiersEngine* qe)
+ : d_qe(qe), d_eqi_counter(c), d_reset_count(0)
+{
}
EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
d_int_rep.clear();
d_reset_count++;
- return processInferences( e );
-}
-
-bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
- if( options::inferArithTriggerEq() ){
- eq::EqualityEngine* ee = getEngine();
- //updated implementation
- EqualityInference * ei = d_qe->getEqualityInference();
- while( d_eqi_counter.get()<ei->getNumPendingMerges() ){
- Node eq = ei->getPendingMerge( d_eqi_counter.get() );
- Node eq_exp = ei->getPendingMergeExplanation( d_eqi_counter.get() );
- Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl;
- Trace("quant-engine-ee-proc") << " explanation : " << eq_exp << std::endl;
- Assert( ee->hasTerm( eq[0] ) );
- Assert( ee->hasTerm( eq[1] ) );
- if( areDisequal( eq[0], eq[1] ) ){
- Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl;
- if( Trace.isOn("term-db-lemma") ){
- Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl;
- if( !d_qe->getTheoryEngine()->needCheck() ){
- Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl;
- //this should really never happen (implies arithmetic is incomplete when sharing is enabled)
- Assert( false );
- }
- Trace("term-db-lemma") << " add split on : " << eq << std::endl;
- }
- eq = Rewriter::rewrite(eq);
- Node split = NodeManager::currentNM()->mkNode(OR, eq, eq.negate());
- d_qe->addLemma(split);
- return false;
- }else{
- ee->assertEquality( eq, true, eq_exp );
- d_eqi_counter = d_eqi_counter.get() + 1;
- }
- }
- Assert( ee->consistent() );
- }
return true;
}
namespace quantifiers {
/** EqualityQueryQuantifiersEngine class
-* This is a wrapper class around an equality engine that is used for
-* queries required by algorithms in the quantifiers theory.
-* It uses an equality engine, as determined by the quantifiers engine it points
-* to.
-*
-* The main extension of this class wrt EqualityQuery is the function
-* getInternalRepresentative, which is used by instantiation-based methods
-* that are agnostic with respect to choosing terms within an equivalence class.
-* Examples of such methods are finite model finding and enumerative
-* instantiation.
-* Method getInternalRepresentative returns the "best" representative based on
-* the internal heuristic,
-* which is currently based on choosing the term that was previously chosen as a
-* representative
-* earliest.
-*/
+ *
+ * This is a wrapper class around an equality engine that is used for
+ * queries required by algorithms in the quantifiers theory. It uses an equality
+ * engine, as determined by the quantifiers engine it points to.
+ *
+ * The main extension of this class wrt EqualityQuery is the function
+ * getInternalRepresentative, which is used by instantiation-based methods
+ * that are agnostic with respect to choosing terms within an equivalence class.
+ * Examples of such methods are finite model finding and enumerative
+ * instantiation. Method getInternalRepresentative returns the "best"
+ * 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 EqualityQuery
{
public:
TheoryEngine* te)
: d_te(te),
d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
- d_eq_inference(nullptr),
d_tr_trie(new inst::TriggerTrie),
d_model(nullptr),
d_rel_dom(nullptr),
d_instantiate->addNotify(d_private->d_inst_prop->getInstantiationNotify());
}
- if( options::inferArithTriggerEq() ){
- d_eq_inference.reset(new quantifiers::EqualityInference(c, false));
- }
d_util.push_back(d_instantiate.get());
{
return d_eq_query.get();
}
-quantifiers::EqualityInference* QuantifiersEngine::getEqualityInference() const
-{
- return d_eq_inference.get();
-}
quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const
{
return d_rel_dom.get();
void QuantifiersEngine::eqNotifyNewClass(TNode t) {
addTermToDatabase( t );
- if( d_eq_inference ){
- d_eq_inference->eqNotifyNewClass( t );
- }
-}
-
-void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) {
- if( d_eq_inference ){
- d_eq_inference->eqNotifyMerge( t1, t2 );
- }
-}
-
-void QuantifiersEngine::eqNotifyPostMerge(TNode t1, TNode t2) {
-
-}
-
-void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
- //if( d_qcf ){
- // d_qcf->assertDisequal( t1, t2 );
- //}
}
bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
#include "expr/attribute.h"
#include "expr/term_canonize.h"
#include "theory/quantifiers/ematching/trigger.h"
-#include "theory/quantifiers/equality_infer.h"
#include "theory/quantifiers/equality_query.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/model_builder.h"
inst::TriggerTrie* getTriggerDatabase() const;
//---------------------- end utilities
//---------------------- utilities (TODO move these utilities #1163)
- /** get the equality inference */
- quantifiers::EqualityInference* getEqualityInference() const;
/** get relevant domain */
quantifiers::RelevantDomain* getRelevantDomain() const;
//---------------------- end utilities
void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
/** notification when master equality engine is updated */
void eqNotifyNewClass(TNode t);
- void eqNotifyPreMerge(TNode t1, TNode t2);
- void eqNotifyPostMerge(TNode t1, TNode t2);
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
/** use model equality engine */
bool usingModelEqualityEngine() const { return d_useModelEe; }
/** debug print equality engine */
//------------- quantifiers utilities
/** equality query class */
std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
- /** equality inference class */
- std::unique_ptr<quantifiers::EqualityInference> d_eq_inference;
/** all triggers will be stored in this trie */
std::unique_ptr<inst::TriggerTrie> d_tr_trie;
/** extended model object */
}
}
-void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
- if (d_logicInfo.isQuantified()) {
- d_quantEngine->eqNotifyPreMerge( t1, t2 );
- }
-}
-
-void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
- if (d_logicInfo.isQuantified()) {
- d_quantEngine->eqNotifyPostMerge( t1, t2 );
- }
-}
-
-void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
- if (d_logicInfo.isQuantified()) {
- d_quantEngine->eqNotifyDisequal( t1, t2, reason );
- }
-}
-
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
RemoveTermFormulas& iteRemover,
void eqNotifyNewClass(TNode t) override { d_te.eqNotifyNewClass(t); }
void eqNotifyPreMerge(TNode t1, TNode t2) override
{
- d_te.eqNotifyPreMerge(t1, t2);
}
void eqNotifyPostMerge(TNode t1, TNode t2) override
{
- d_te.eqNotifyPostMerge(t1, t2);
}
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
{
- d_te.eqNotifyDisequal(t1, t2, reason);
}
};/* class TheoryEngine::NotifyClass */
NotifyClass d_masterEENotify;
-; COMMAND-LINE: --infer-arith-trigger-eq
-; EXPECT: unsat
(set-info :smt-lib-version 2.6)
(set-logic UFLIA)
(set-info :status unsat)
projects / cvc5.git / commitdiff