| FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
- | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; }
-
| FP_TOK { $kind = CVC4::kind::FLOATINGPOINT_FP; }
| FP_EQ_TOK { $kind = CVC4::kind::FLOATINGPOINT_EQ; }
| FP_ABS_TOK { $kind = CVC4::kind::FLOATINGPOINT_ABS; }
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
# 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
+option ltePartialInst --lte-partial-inst bool :default false
+ partially instantiate local theory quantifiers
endmodule
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/inst_match.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
using namespace std;
using namespace CVC4;
newHasPol = false;
}
}
-}
\ No newline at end of file
+}
+
+
+QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_lte_asserts( c ){
+
+}
+
+/** add quantifier */
+bool QuantLtePartialInst::addQuantifier( Node q ) {
+ if( d_do_inst.find( q )!=d_do_inst.end() ){
+ if( d_do_inst[q] ){
+ d_lte_asserts.push_back( q );
+ return true;
+ }else{
+ return false;
+ }
+ }else{
+ d_vars[q].clear();
+ //check if this quantified formula is eligible for partial instantiation
+ std::map< Node, bool > vars;
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ 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++ ){
+ if( vars[q[0][i]] ){
+ d_vars[q].push_back( q[0][i] );
+ }else{
+ doInst = false;
+ break;
+ }
+ }
+ Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl;
+ d_do_inst[q] = doInst;
+ if( doInst ){
+ d_lte_asserts.push_back( q );
+ }
+ return doInst;
+ }
+}
+
+void QuantLtePartialInst::getEligibleInstVars( Node n, std::map< Node, bool >& vars ) {
+ if( n.getKind()!=APPLY_UF || n.getType().isBoolean() ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( vars.find( n[i] )!=vars.end() ){
+ vars[n[i]] = false;
+ }
+ }
+ }
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ getEligibleInstVars( n[i], vars );
+ }
+}
+
+void QuantLtePartialInst::reset() {
+ d_reps.clear();
+ eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+ while( !eqcs_i.isFinished() ){
+ TNode r = (*eqcs_i);
+ TypeNode tn = r.getType();
+ d_reps[tn].push_back( r );
+ ++eqcs_i;
+ }
+}
+
+/** get instantiations */
+void QuantLtePartialInst::getInstantiations( std::vector< Node >& lemmas ) {
+ Trace("lte-partial-inst") << "LTE : get instantiations, # quant = " << d_lte_asserts.size() << std::endl;
+ reset();
+ for( unsigned i=0; i<d_lte_asserts.size(); i++ ){
+ Node q = d_lte_asserts[i];
+ Assert( d_do_inst.find( q )!=d_do_inst.end() && d_do_inst[q] );
+ if( d_inst.find( q )==d_inst.end() ){
+ Trace("lte-partial-inst") << "LTE : Get partial instantiations for " << q << "..." << std::endl;
+ d_inst[q] = true;
+ Assert( !d_vars[q].empty() );
+ //make bound list
+ Node bvl;
+ std::vector< Node > bvs;
+ for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+ if( std::find( d_vars[q].begin(), d_vars[q].end(), q[0][j] )==d_vars[q].end() ){
+ bvs.push_back( q[0][j] );
+ }
+ }
+ if( !bvs.empty() ){
+ bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );
+ }
+ std::vector< Node > conj;
+ std::vector< Node > terms;
+ std::vector< TypeNode > types;
+ for( unsigned j=0; j<d_vars[q].size(); j++ ){
+ types.push_back( d_vars[q][j].getType() );
+ }
+ 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 ) ) );
+ }
+ }
+}
+
+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() );
+ if( bvl.isNull() ){
+ conj.push_back( body );
+ Trace("lte-partial-inst") << " - ground conjunct : " << body << std::endl;
+ }else{
+ Node nq;
+ if( q.getNumChildren()==3 ){
+ Node ipl = q[2].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+ nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body, ipl );
+ }else{
+ nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
+ }
+ Trace("lte-partial-inst") << " - quantified conjunct : " << nq << std::endl;
+ LtePartialInstAttribute ltpia;
+ nq.setAttribute(ltpia,true);
+ conj.push_back( nq );
+ }
+ }else{
+ std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[index] );
+ if( it!=d_reps.end() ){
+ terms.push_back( Node::null() );
+ Trace("lte-partial-inst-debug") << it->second.size() << " reps of type " << types[index] << std::endl;
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ terms[index] = it->second[i];
+ getPartialInstantiations( conj, q, bvl, vars, terms, types, index+1 );
+ }
+ terms.pop_back();
+ }else{
+ Trace("lte-partial-inst-debug") << "No reps found of type " << types[index] << std::endl;
+ }
+ }
+}
namespace CVC4 {
namespace theory {
-
+class QuantifiersEngine;
+
class QuantArith
{
public:
virtual void setLiberal( bool l ) = 0;
};/* class EqualityQuery */
+class QuantLtePartialInst {
+private:
+ std::map< TypeNode, std::vector< Node > > d_reps;
+ // should we instantiate quantifier
+ std::map< Node, bool > d_do_inst;
+ // have we instantiated quantifier
+ std::map< Node, bool > d_inst;
+ std::map< Node, std::vector< Node > > d_vars;
+ /** pointer to quant engine */
+ QuantifiersEngine * d_qe;
+ /** list of relevant quantifiers asserted in the current context */
+ context::CDList<Node> d_lte_asserts;
+ /** reset */
+ void reset();
+ /** get instantiations */
+ 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 );
+public:
+ QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c );
+ /** add quantifier */
+ bool addQuantifier( Node q );
+ /** get instantiations */
+ void getInstantiations( std::vector< Node >& lemmas );
+};
+
+
}
}
}
}
-void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool withinInstClosure ){
+void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
//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?
}
}
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 );
+ addTerm( n[i], added, withinQuant );
}
}
}
}
bool TermDb::hasTermCurrent( Node n ) {
- if( options::termDbInstClosure() && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
- return false;
+ //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{
- //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;
- }
+ Assert( false );
+ return false;
}
}
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() ){
}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();
}
+ */
+ //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc
+ return Node::null();
}
}
struct RrPriorityAttributeId {};
typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
+/** Attribute true for quantifiers that do not need to be partially instantiated */
+struct LtePartialInstAttributeId {};
+typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
+
class QuantifiersEngine;
namespace inst{
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;
/** 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, bool withinInstClosure = false );
+ void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
/** reset (calculate which terms are active) */
void reset( Theory::Effort effort );
/** get operator*/
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;
}
};/* 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:
}else{
d_ceg_inst = NULL;
}
+ if( options::ltePartialInst() ){
+ d_lte_part_inst = new QuantLtePartialInst( this, c );
+ }else{
+ d_lte_part_inst = NULL;
+ }
if( needsBuilder ){
Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
delete d_eq_query;
delete d_sg_gen;
delete d_ceg_inst;
+ delete d_lte_part_inst;
for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
delete (*i).second;
}
}
if( e==Theory::EFFORT_FULL ){
d_ierCounter++;
+ //process partial instantiations for LTE
+ if( d_lte_part_inst ){
+ d_lte_part_inst->getInstantiations( d_lemmas_waiting );
+ }
}else if( e==Theory::EFFORT_LAST_CALL ){
d_ierCounter_lc++;
}
- bool needsCheck = false;
+ bool needsCheck = !d_lemmas_waiting.empty();
bool needsModel = false;
bool needsFullModel = false;
std::vector< QuantifiersModule* > qm;
}
Trace("quant-engine-debug") << std::endl;
Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
+ if( !d_lemmas_waiting.empty() ){
+ Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
+ }
Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl;
Trace("quant-engine-ee") << "Equality engine : " << std::endl;
d_conflict = false;
d_hasAddedLemma = false;
- //flush previous lemmas (for instance, if was interupted)
+ //flush previous lemmas (for instance, if was interupted), or other lemmas to process
flushLemmas();
if( d_hasAddedLemma ){
return;
}
//assert to modules TODO : handle !pol
if( pol ){
+ if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){
+ Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl;
+ if( d_lte_part_inst->addQuantifier( f ) ){
+ return;
+ }
+ }
//register the quantifier
registerQuantifier( f );
//assert it to each module
return Node::null();
}
-void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
+void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
std::set< Node > added;
- getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
+ getTermDatabase()->addTerm( n, added, withinQuant );
//maybe have triggered instantiations if we are doing eager instantiation
if( options::eagerInstQuant() ){
flushLemmas();
quantifiers::ConjectureGenerator * d_sg_gen;
/** ceg instantiation */
quantifiers::CegInstantiation * d_ceg_inst;
+ /** lte partial instantiation */
+ QuantLtePartialInst * d_lte_part_inst;
public: //effort levels
enum {
QEFFORT_CONFLICT,
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
/** add term to database */
- void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
+ void addTermToDatabase( Node n, bool withinQuant = false );
/** get the master equality engine */
eq::EqualityEngine* getMasterEqualityEngine() ;
/** debug print equality engine */
projects / cvc5.git / commitdiff