| DTSIZE_TOK { $kind = CVC4::kind::DT_SIZE; }
| FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
+
+ | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; }
// NOTE: Theory operators go here
;
FMFCARD_TOK : 'fmf.card';
+INST_CLOSURE_TOK : 'inst-closure';
+
EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
// Other set theory operators are not
// tokenized and handled directly when
Node CandidateGeneratorQEAll::getNextCandidate() {
while( !d_eq.isFinished() ){
- Node n = (*d_eq);
+ TNode n = (*d_eq);
++d_eq;
if( n.getType().isSubtypeOf( d_match_pattern_type ) ){
- if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
+ TNode nh = d_qe->getTermDatabase()->getHasTermEqc( n );
+ if( !nh.isNull() ){
if( options::instMaxLevel()!=-1 ){
- n = d_qe->getEqualityQuery()->getInternalRepresentative( n, d_f, d_index );
+ nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index );
}
d_firstTime = false;
//an equivalence class with the same type as the pattern, return it
- return n;
+ return nh;
}
}
}
for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
Node t = getModelTerm( conj->d_candidates[i] );
model_terms.push_back( t );
- Trace("cegqi-engine") << t << " ";
+ Trace("cegqi-engine") << conj->d_candidates[i] << " -> " << t << " ";
}
Trace("cegqi-engine") << std::endl;
d_quantEngine->addInstantiation( q, model_terms, false );
for( unsigned i=0; i<n.size(); i++ ){
Node nv = getModelValue( n[i] );
v.push_back( nv );
- Trace("cegqi-engine") << nv << " ";
+ Trace("cegqi-engine") << n[i] << " -> " << nv << " ";
if( nv.isNull() ){
success = false;
}
# a list of instantiation patterns
operator INST_PATTERN_LIST 1: "a list of instantiation patterns"
+operator INST_CLOSURE 1 "predicate for specifying term in instantiation closure."
+
typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule
typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule
typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule
typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule
typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule
typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule
+typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule
# for rewrite rules
# types...
option localTheoryExt --local-t-ext bool :default false
do instantiation based on local theory extensions
+option termDbInstClosure --term-db-inst-closure bool :default false
+ only consider inst closure terms for E-matching
endmodule
}
}
-void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
+void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool withinInstClosure ){
//don't add terms in quantifier bodies
if( withinQuant && !options::registerQuantBodyTerms() ){
return;
}
+ bool rec = false;
if( d_processed.find( n )==d_processed.end() ){
d_processed.insert(n);
+ if( withinInstClosure ){
+ d_iclosure_processed.insert( n );
+ }
d_type_map[ n.getType() ].push_back( n );
//if this is an atomic trigger, consider adding it
//Call the children?
d_op_map[op].push_back( n );
added.insert( n );
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- addTerm( n[i], added, withinQuant );
- if( options::eagerInstQuant() ){
+ if( options::eagerInstQuant() ){
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
int addedLemmas = 0;
for( size_t i=0; i<d_op_triggers[op].size(); i++ ){
}
}
}
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- addTerm( n[i], added, withinQuant );
- }
+ }
+ rec = true;
+ }else if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
+ d_iclosure_processed.insert( n );
+ rec = true;
+ }
+ if( rec ){
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ addTerm( n[i], added, withinQuant, withinInstClosure );
}
}
}
}
bool TermDb::hasTermCurrent( Node n ) {
- //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n );
- if( options::termDbMode()==TERM_DB_ALL ){
- return true;
- }else if( options::termDbMode()==TERM_DB_RELEVANT ){
- return d_has_map.find( n )!=d_has_map.end();
- }else{
- Assert( false );
+ if( options::termDbInstClosure() && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
return false;
+ }else{
+ //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
+ if( options::termDbMode()==TERM_DB_ALL ){
+ return true;
+ }else if( options::termDbMode()==TERM_DB_RELEVANT ){
+ return d_has_map.find( n )!=d_has_map.end();
+ }else{
+ Assert( false );
+ return false;
+ }
}
}
-void TermDb::setHasTerm( Node n ) {
- if( inst::Trigger::isAtomicTrigger( n ) ){
- if( d_has_map.find( n )==d_has_map.end() ){
- d_has_map[n] = true;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- setHasTerm( n[i] );
+Node TermDb::getHasTermEqc( Node r ) {
+ if( hasTermCurrent( r ) ){
+ 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;
+ }
+ }
+ d_has_eqc[r] = h;
+ return h;
+ }else{
+ return it->second;
}
+ }else{
+ //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc
+ return Node::null();
+ }
+ }
+}
+
+void TermDb::setHasTerm( Node n ) {
+ //if( inst::Trigger::isAtomicTrigger( n ) ){
+ if( d_has_map.find( n )==d_has_map.end() ){
+ d_has_map[n] = true;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ setHasTerm( n[i] );
}
+ }
+ /*
}else{
for( unsigned i=0; i<n.getNumChildren(); i++ ){
setHasTerm( n[i] );
}
}
+ */
}
void TermDb::reset( Theory::Effort effort ){
//compute has map
if( options::termDbMode()==TERM_DB_RELEVANT ){
d_has_map.clear();
+ d_has_eqc.clear();
eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
while( !eqcs_i.isFinished() ){
QuantifiersEngine* d_quantEngine;
/** terms processed */
std::hash_set< Node, NodeHashFunction > d_processed;
+ /** terms processed */
+ std::hash_set< Node, NodeHashFunction > d_iclosure_processed;
private:
/** select op map */
std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
std::map< Node, std::vector< Node > > d_op_map;
/** 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;
/** map from APPLY_UF functions to trie */
std::map< Node, TermArgTrie > d_func_map_trie;
std::map< Node, TermArgTrie > d_func_map_eqc_trie;
/** map from type nodes to terms of that type */
std::map< TypeNode, std::vector< Node > > d_type_map;
/** add a term to the database */
- void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
+ void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false );
/** reset (calculate which terms are active) */
void reset( Theory::Effort effort );
/** get operator*/
bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
/** has term */
bool hasTermCurrent( Node n );
+ /** get has term eqc */
+ Node getHasTermEqc( Node r );
//for model basis
private:
TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
- d_numRestarts(0),
d_masterEqualityEngine(0)
{
d_numInstantiations = 0;
}
}
+void TheoryQuantifiers::computeCareGraph() {
+ //do nothing
+}
+
void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) {
if(fullModel) {
for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
case kind::FORALL:
assertUniversal( assertion );
break;
+ case kind::INST_CLOSURE:
+ getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
+ break;
+ case kind::EQUAL:
+ //do nothing
+ break;
case kind::NOT:
{
switch( assertion[0].getKind()) {
case kind::FORALL:
assertExistential( assertion );
break;
+ case kind::EQUAL:
+ //do nothing
+ break;
+ case kind::INST_CLOSURE: //cannot negate inst closure
default:
Unhandled(assertion[0].getKind());
break;
//}else{
// return false;
//}
-
- if( !d_out->flipDecision() ){
- return restart();
- }
- return true;
-}
-
-bool TheoryQuantifiers::restart(){
- static const int restartLimit = 0;
- if( d_numRestarts==restartLimit ){
- Debug("quantifiers-flip") << "No more restarts." << std::endl;
- return false;
- }else{
- d_numRestarts++;
- Debug("quantifiers-flip") << "Do restart." << std::endl;
- return true;
- }
+ return false;
}
void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
/** number of instantiations */
int d_numInstantiations;
int d_baseDecLevel;
- /** number of restarts */
- int d_numRestarts;
eq::EqualityEngine* d_masterEqualityEngine;
-
+private:
+ void computeCareGraph();
public:
TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
~TheoryQuantifiers();
void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
void addSharedTerm(TNode t);
void notifyEq(TNode lhs, TNode rhs);
void preRegisterTerm(TNode n);
private:
void assertUniversal( Node n );
void assertExistential( Node n );
- bool restart();
};/* class TheoryQuantifiers */
}/* CVC4::theory::quantifiers namespace */
};/* struct QuantifierInstPatternListTypeRule */
+struct QuantifierInstClosureTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw(TypeCheckingExceptionPrivate) {
+ Assert(n.getKind() == kind::INST_CLOSURE );
+ if( check ){
+ TypeNode tn = n[0].getType(check);
+ if( tn.isBoolean() ){
+ throw TypeCheckingExceptionPrivate(n, "argument of inst-closure must be non-boolean");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};/* struct QuantifierInstClosureTypeRule */
+
class RewriteRuleTypeRule {
public:
return Node::null();
}
-void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
+void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
std::set< Node > added;
- getTermDatabase()->addTerm( n, added, withinQuant );
+ getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
//maybe have triggered instantiations if we are doing eager instantiation
if( options::eagerInstQuant() ){
flushLemmas();
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
/** add term to database */
- void addTermToDatabase( Node n, bool withinQuant = false );
+ void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
/** get the master equality engine */
eq::EqualityEngine* getMasterEqualityEngine() ;
/** debug print equality engine */
projects / cvc5.git / commitdiff