TNode n = (*d_eq);
++d_eq;
if( n.getType().isSubtypeOf( d_match_pattern_type ) ){
- TNode nh = d_qe->getTermDatabase()->getHasTermEqc( n );
+ TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n );
if( !nh.isNull() ){
if( options::instMaxLevel()!=-1 ){
nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index );
}
-QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_lte_asserts( c ){
-
+QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_wasInvoked( false ), d_qe( qe ), d_lte_asserts( c ){
+
}
/** add quantifier */
vars[q[0][i]] = true;
}
getEligibleInstVars( q[1], vars );
-
+
//TODO : instantiate only if we would force ground instances?
bool doInst = true;
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
}
}
Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl;
- d_do_inst[q] = doInst;
+ d_do_inst[q] = doInst;
if( doInst ){
d_lte_asserts.push_back( q );
}
getPartialInstantiations( conj, q, bvl, d_vars[q], terms, types, 0 );
Assert( !conj.empty() );
lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) );
+ d_wasInvoked = true;
}
}
}
-void QuantLtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
+void QuantLtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, unsigned index ){
if( index==vars.size() ){
Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
namespace theory {
class QuantifiersEngine;
-
+
class QuantArith
{
public:
class QuantLtePartialInst {
private:
+ // was this module invoked
+ bool d_wasInvoked;
+ //representatives per type
std::map< TypeNode, std::vector< Node > > d_reps;
// should we instantiate quantifier
std::map< Node, bool > d_do_inst;
/** reset */
void reset();
/** get instantiations */
- void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
+ void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, unsigned index );
/** get eligible inst variables */
void getEligibleInstVars( Node n, std::map< Node, bool >& vars );
bool addQuantifier( Node q );
/** get instantiations */
void getInstantiations( std::vector< Node >& lemmas );
+ /** was invoked */
+ bool wasInvoked() { return d_wasInvoked; }
};
}
}
-Node TermDb::getHasTermEqc( Node r ) {
- if( hasTermCurrent( r ) ){
+bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) {
+ if( options::lteRestrictInstClosure() ){
+ //has to be both in inst closure and in ground assertions
+ if( !isInstClosure( n ) ){
+ Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl;
+ return false;
+ }
+ // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this
+ if( !hasTermCurrent( n, false ) ){
+ Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl;
+ return false;
+ }
+ }
+ if( options::instMaxLevel()!=-1 ){
+ if( n.hasAttribute(InstLevelAttribute()) ){
+ int fml = f.isNull() ? -1 : getQAttrQuantInstLevel( f );
+ unsigned ml = fml>=0 ? fml : options::instMaxLevel();
+
+ if( n.getAttribute(InstLevelAttribute())>ml ){
+ Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
+ Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
+ return false;
+ }
+ }else{
+ if( options::instLevelInputOnly() ){
+ Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
+Node TermDb::getEligibleTermInEqc( TNode r ) {
+ if( isTermEligibleForInstantiation( r, TNode::null() ) ){
return r;
}else{
- /*
- if( options::termDbInstClosure() ){
- std::map< Node, Node >::iterator it = d_has_eqc.find( r );
- if( it==d_has_eqc.end() ){
- Node h;
- eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
- eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
- while( h.isNull() && !eqc_i.isFinished() ){
- TNode n = (*eqc_i);
- ++eqc_i;
- if( hasTermCurrent( n ) ){
- h = n;
- }
+ std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
+ if( it==d_term_elig_eqc.end() ){
+ Node h;
+ eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+ while( h.isNull() && !eqc_i.isFinished() ){
+ TNode n = (*eqc_i);
+ ++eqc_i;
+ if( hasTermCurrent( n ) ){
+ h = n;
}
- d_has_eqc[r] = h;
- return h;
- }else{
- return it->second;
}
+ d_term_elig_eqc[r] = h;
+ return h;
+ }else{
+ return it->second;
}
- */
- //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc
- return Node::null();
}
}
//compute has map
if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){
d_has_map.clear();
- d_has_eqc.clear();
+ d_term_elig_eqc.clear();
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
while( !eqcs_i.isFinished() ){
TNode r = (*eqcs_i);
/** has map */
std::map< Node, bool > d_has_map;
/** map from reps to a term in eqc in d_has_map */
- std::map< Node, Node > d_has_eqc;
+ std::map< Node, Node > d_term_elig_eqc;
/** map from APPLY_UF functions to trie */
std::map< Node, TermArgTrie > d_func_map_trie;
std::map< Node, TermArgTrie > d_func_map_eqc_trie;
bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
/** has term */
bool hasTermCurrent( Node n, bool useMode = true );
+ /** is term eligble for instantiation? */
+ bool isTermEligibleForInstantiation( TNode n, TNode f, bool print = false );
/** get has term eqc */
- Node getHasTermEqc( Node r );
+ Node getEligibleTermInEqc( TNode r );
/** is inst closure */
bool isInstClosure( Node r );
//for model basis
}
}
}
- bool defaultBuildModel = false;
if( needsCheck ){
Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
Trace("quant-engine-debug") << " modules to check : ";
}
}
Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
-
- //build the model if not done so already
- // this happens if no quantifiers are currently asserted and no model-building module is enabled
- if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
- if( options::produceModels() && !d_model->isModelSet() ){
- defaultBuildModel = true;
- }
- if( Trace.isOn("inst-per-quant") ){
- for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
- Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl;
- }
- }
- }else{
+ if( d_hasAddedLemma ){
+ //debug information
if( Trace.isOn("inst-per-quant-round") ){
for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){
Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl;
}
}
Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
- }else{
- if( e==Theory::EFFORT_LAST_CALL && options::produceModels() ){
- defaultBuildModel = true;
- }
}
-
- if( defaultBuildModel ){
- Trace("quant-engine-debug") << "Build the model..." << std::endl;
- d_te->getModelBuilder()->buildModel( d_model, true );
- Trace("quant-engine-debug") << "Done building the model." << std::endl;
+ //SAT case
+ if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
+ if( options::produceModels() && !d_model->isModelSet() ){
+ //use default model builder when no module built the model
+ Trace("quant-engine-debug") << "Build the model..." << std::endl;
+ d_te->getModelBuilder()->buildModel( d_model, true );
+ Trace("quant-engine-debug") << "Done building the model." << std::endl;
+ }
+ //check other sources of incompleteness
+ bool setInc = false;
+ if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){
+ setInc = true;
+ }
+ if( setInc ){
+ getOutputChannel().setIncomplete();
+ }
+ //output debug stats
+ if( Trace.isOn("inst-per-quant") ){
+ for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
+ Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl;
+ }
+ }
}
}
}
}
-bool QuantifiersEngine::isTermEligibleForInstantiation( Node n, Node f, bool print ) {
- if( options::lteRestrictInstClosure() ){
- //has to be both in inst closure and in ground assertions
- if( !d_term_db->isInstClosure( n ) ){
- Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl;
- return false;
- }
- // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this
- if( !d_term_db->hasTermCurrent( n, false ) ){
- Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl;
- return false;
- }
- }
- if( options::instMaxLevel()!=-1 ){
- if( n.hasAttribute(InstLevelAttribute()) ){
- int fml = d_term_db->getQAttrQuantInstLevel( f );
- unsigned ml = fml>=0 ? fml : options::instMaxLevel();
-
- if( n.getAttribute(InstLevelAttribute())>ml ){
- Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
- Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
- return false;
- }
- }else{
- if( options::instLevelInputOnly() ){
- Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
- return false;
- }
- }
- }
- return true;
-}
-
-
Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){
if( n.getKind()==INST_CONSTANT ){
Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
//check based on instantiation level
if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
for( unsigned i=0; i<terms.size(); i++ ){
- if( !isTermEligibleForInstantiation( terms[i], f, true ) ){
+ if( !d_term_db->isTermEligibleForInstantiation( terms[i], f, true ) ){
return false;
}
}
bool getInstWhenNeedsCheck( Theory::Effort e );
/** set instantiation level attr */
static void setInstantiationLevelAttr( Node n, uint64_t level );
- /** is term eligble for instantiation? */
- bool isTermEligibleForInstantiation( Node n, Node f, bool print = false );
public:
/** get number of quantifiers */
int getNumQuantifiers() { return (int)d_quants.size(); }
projects / cvc5.git / commitdiff