theory/quantifiers/conjecture_generator.cpp \
theory/quantifiers/ce_guided_instantiation.h \
theory/quantifiers/ce_guided_instantiation.cpp \
+ theory/quantifiers/local_theory_ext.h \
+ theory/quantifiers/local_theory_ext.cpp \
theory/quantifiers/fun_def_process.h \
theory/quantifiers/fun_def_process.cpp \
theory/quantifiers/options_handlers.h \
}
-void FirstOrderModel::assertQuantifier( Node n ){
- if( n.getKind()==FORALL ){
- d_forall_asserts.push_back( n );
- if( n.getAttribute(AxiomAttribute()) ){
- d_axiom_asserted = true;
+void FirstOrderModel::assertQuantifier( Node n, bool reduced ){
+ if( !reduced ){
+ if( n.getKind()==FORALL ){
+ d_forall_asserts.push_back( n );
+ if( n.getAttribute(AxiomAttribute()) ){
+ d_axiom_asserted = true;
+ }
+ }else if( n.getKind()==NOT ){
+ Assert( n[0].getKind()==FORALL );
}
- }else if( n.getKind()==NOT ){
- Assert( n[0].getKind()==FORALL );
+ }else{
+ Assert( n.getKind()==FORALL );
+ Assert( d_forall_to_reduce.find( n )==d_forall_to_reduce.end() );
+ d_forall_to_reduce[n] = true;
+ Trace("quant") << "Mark to reduce : " << n << std::endl;
}
}
return d_rep_set.d_type_reps[tn][0];
}
+/** needs check */
+bool FirstOrderModel::checkNeeded() {
+ return d_forall_asserts.size()>0 || !d_forall_to_reduce.empty();
+}
+
+/** mark reduced */
+void FirstOrderModel::markQuantifierReduced( Node q ) {
+ Assert( d_forall_to_reduce.find( q )!=d_forall_to_reduce.end() );
+ d_forall_to_reduce.erase( q );
+ Trace("quant") << "Mark reduced : " << q << std::endl;
+}
+
void FirstOrderModel::reset_round() {
d_quant_active.clear();
}
context::CDO< bool > d_axiom_asserted;
/** list of quantifiers asserted in the current context */
context::CDList<Node> d_forall_asserts;
+ /** list of quantifiers that have been marked to reduce */
+ std::map< Node, bool > d_forall_to_reduce;
/** is model set */
context::CDO< bool > d_isModelSet;
/** get variable id */
virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
public: //for Theory Quantifiers:
/** assert quantifier */
- void assertQuantifier( Node n );
+ void assertQuantifier( Node n, bool reduced = false );
/** get number of asserted quantifiers */
int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
/** get asserted quantifier */
Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
+ /** get number to reduce quantifiers */
+ unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); }
/** bool axiom asserted */
bool isAxiomAsserted() { return d_axiom_asserted; }
/** initialize model for term */
}
/** get some domain element */
Node getSomeDomainElement(TypeNode tn);
+ /** do we need to do any work? */
+ bool checkNeeded();
+ /** mark reduced */
+ void markQuantifierReduced( Node q );
private:
//list of inactive quantified formulas
std::map< TNode, bool > d_quant_active;
#include "theory/theory_engine.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
using namespace std;
using namespace CVC4;
//}
}
Debug(c) << std::endl;
-
- for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){
- Node f = d_quantEngine->getQuantifier( q );
+
+ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
Debug(c) << f << std::endl;
Debug(c) << " Inst constants: ";
for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
d_instStrategies.push_back( d_i_ag );
}
- //local theory extensions
- if( options::localTheoryExt() ){
- d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine );
- d_instStrategies.push_back( d_i_lte );
- }
+ //local theory extensions TODO?
+ //if( options::localTheoryExt() ){
+ // d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine );
+ // d_instStrategies.push_back( d_i_lte );
+ //}
//full saturation : instantiate from relevant domain, then arbitrary terms
if( options::fullSaturateQuant() ){
--- /dev/null
+/********************* */
+/*! \file quant_util.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of local theory ext utilities
+ **/
+
+#include "theory/quantifiers/local_theory_ext.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+
+LtePartialInst::LtePartialInst( QuantifiersEngine * qe, context::Context* c ) :
+QuantifiersModule( qe ), d_wasInvoked( false ), d_needsCheck( false ){
+
+}
+
+/** add quantifier */
+bool LtePartialInst::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();
+ d_pat_var_order[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?
+ std::map< Node, int > var_order;
+ 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] );
+ var_order[q[0][i]] = i;
+ }else{
+ Trace("lte-partial-inst-debug") << "...do not consider, variable " << q[0][i] << " was not found in correct position in body." << std::endl;
+ doInst = false;
+ break;
+ }
+ }
+ if( doInst ){
+ //also needs patterns
+ if( q.getNumChildren()==3 && q[2].getNumChildren()==1 ){
+ for( unsigned i=0; i<q[2][0].getNumChildren(); i++ ){
+ Node pat = q[2][0][i];
+ if( pat.getKind()==APPLY_UF ){
+ for( unsigned j=0; j<pat.getNumChildren(); j++ ){
+ if( !addVariableToPatternList( pat[j], d_pat_var_order[q], var_order ) ){
+ doInst = false;
+ }
+ }
+ }else if( !addVariableToPatternList( pat, d_pat_var_order[q], var_order ) ){
+ doInst = false;
+ }
+ if( !doInst ){
+ Trace("lte-partial-inst-debug") << "...do not consider, cannot resolve pattern : " << pat << std::endl;
+ break;
+ }
+ }
+ }else{
+ Trace("lte-partial-inst-debug") << "...do not consider (must have exactly one pattern)." << std::endl;
+ }
+ }
+
+
+ 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 );
+ d_needsCheck = true;
+ }
+ return doInst;
+ }
+}
+
+bool LtePartialInst::addVariableToPatternList( Node v, std::vector< int >& pat_var_order, std::map< Node, int >& var_order ) {
+ std::map< Node, int >::iterator it = var_order.find( v );
+ if( it==var_order.end() ){
+ return false;
+ }else if( std::find( pat_var_order.begin(), pat_var_order.end(), it->second )!=pat_var_order.end() ){
+ return false;
+ }else{
+ pat_var_order.push_back( it->second );
+ return true;
+ }
+}
+
+void LtePartialInst::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 );
+ }
+}
+
+/* whether this module needs to check this round */
+bool LtePartialInst::needsCheck( Theory::Effort e ) {
+ return e>=Theory::EFFORT_FULL && d_needsCheck;
+}
+/* Call during quantifier engine's check */
+void LtePartialInst::check( Theory::Effort e, unsigned quant_e ) {
+ //flush lemmas ASAP (they are a reduction)
+ if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT && d_needsCheck ){
+ std::vector< Node > lemmas;
+ getInstantiations( lemmas );
+ //add lemmas to quantifiers engine
+ for( unsigned i=0; i<lemmas.size(); i++ ){
+ d_quantEngine->addLemma( lemmas[i], false );
+ }
+ d_needsCheck = false;
+ }
+}
+
+
+void LtePartialInst::reset() {
+ d_reps.clear();
+ eq::EqualityEngine* ee = d_quantEngine->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 LtePartialInst::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() );
+ terms.push_back( Node::null() );
+ }
+
+ getPartialInstantiations( conj, q, bvl, d_vars[q], terms, types, NULL, 0, 0, 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;
+ d_quantEngine->getModel()->markQuantifierReduced( q );
+ }
+ }
+}
+
+void LtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
+ std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, TermArgTrie * curr,
+ unsigned pindex, unsigned paindex, unsigned iindex ){
+ if( iindex==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{
+ Assert( pindex<q[2][0].getNumChildren() );
+ Node pat = q[2][0][pindex];
+ Assert( pat.getNumChildren()==0 || paindex<=pat.getNumChildren() );
+ if( pat.getKind()==APPLY_UF ){
+ Assert( paindex<=pat.getNumChildren() );
+ if( paindex==pat.getNumChildren() ){
+ getPartialInstantiations( conj, q, bvl, vars, terms, types, NULL, pindex+1, 0, iindex );
+ }else{
+ if( !curr ){
+ Assert( paindex==0 );
+ //start traversing term index for the operator
+ curr = d_quantEngine->getTermDatabase()->getTermArgTrie( pat.getOperator() );
+ }
+ for( std::map< TNode, TermArgTrie >::iterator it = curr->d_data.begin(); it != curr->d_data.end(); ++it ){
+ terms[d_pat_var_order[q][iindex]] = it->first;
+ getPartialInstantiations( conj, q, bvl, vars, terms, types, &it->second, pindex, paindex+1, iindex+1 );
+ }
+ }
+ }else{
+ std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[iindex] );
+ if( it!=d_reps.end() ){
+ Trace("lte-partial-inst-debug") << it->second.size() << " reps of type " << types[iindex] << std::endl;
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ terms[d_pat_var_order[q][iindex]] = it->second[i];
+ getPartialInstantiations( conj, q, bvl, vars, terms, types, NULL, pindex+1, 0, iindex+1 );
+ }
+ }else{
+ Trace("lte-partial-inst-debug") << "No reps found of type " << types[iindex] << std::endl;
+ }
+ }
+ }
+}
--- /dev/null
+/********************* */
+/*! \file local_theory_ext.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief local theory extensions util
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__LOCAL_THEORY_EXT_H
+#define __CVC4__THEORY__LOCAL_THEORY_EXT_H
+
+#include "theory/quantifiers_engine.h"
+#include "context/cdo.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermArgTrie;
+
+class LtePartialInst : public QuantifiersModule {
+private:
+ // was this module invoked
+ bool d_wasInvoked;
+ // needs check
+ bool d_needsCheck;
+ //representatives per type
+ 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;
+ std::map< Node, std::vector< int > > d_pat_var_order;
+ /** list of relevant quantifiers asserted in the current context */
+ std::vector< Node > d_lte_asserts;
+ /** reset */
+ void reset();
+ /** get instantiations */
+ void getInstantiations( std::vector< Node >& lemmas );
+ void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
+ std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, TermArgTrie * curr,
+ unsigned pindex, unsigned paindex, unsigned iindex );
+ /** get eligible inst variables */
+ void getEligibleInstVars( Node n, std::map< Node, bool >& vars );
+
+ bool addVariableToPatternList( Node v, std::vector< int >& pat_var_order, std::map< Node, int >& var_order );
+public:
+ LtePartialInst( QuantifiersEngine * qe, context::Context* c );
+ /** add quantifier : special form of registration */
+ bool addQuantifier( Node q );
+ /** was invoked */
+ bool wasInvoked() { return d_wasInvoked; }
+
+ /* whether this module needs to check this round */
+ bool needsCheck( Theory::Effort e );
+ /* Call during quantifier engine's check */
+ void check( Theory::Effort e, unsigned quant_e );
+ /* Called for new quantifiers */
+ void registerQuantifier( Node q ) {}
+ void assertNode( Node n ) {}
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ std::string identify() const { return "LtePartialInst"; }
+
+};
+
+}
+}
+}
+
+#endif
}
}
}
-
-
-QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_wasInvoked( false ), 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 ) ) );
- d_wasInvoked = true;
- }
- }
-}
-
-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;
- }
- }
-}
virtual void setLiberal( bool l ) = 0;
};/* class EqualityQuery */
-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;
- // 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 );
- /** was invoked */
- bool wasInvoked() { return d_wasInvoked; }
-};
-
}
}
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/conjecture_generator.h"
#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/quantifiers/local_theory_ext.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/uf/options.h"
#include "theory/uf/theory_uf.h"
d_ceg_inst = NULL;
}
if( options::ltePartialInst() ){
- d_lte_part_inst = new QuantLtePartialInst( this, c );
+ d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
+ d_modules.push_back( d_lte_part_inst );
}else{
d_lte_part_inst = NULL;
}
}
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 needsModel = false;
bool needsFullModel = false;
std::vector< QuantifiersModule* > qm;
- if( d_model->getNumAssertedQuantifiers()>0 ){
- needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call
+ if( d_model->checkNeeded() ){
+ needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call
for( int i=0; i<(int)d_modules.size(); i++ ){
if( d_modules[i]->needsCheck( e ) ){
qm.push_back( d_modules[i] );
}
if( needsCheck ){
Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
- Trace("quant-engine-debug") << " modules to check : ";
- for( unsigned i=0; i<qm.size(); i++ ){
- Trace("quant-engine-debug") << qm[i]->identify() << " ";
+ if( Trace.isOn("quant-engine-debug") ){
+ Trace("quant-engine-debug") << " modules to check : ";
+ for( unsigned i=0; i<qm.size(); i++ ){
+ Trace("quant-engine-debug") << qm[i]->identify() << " ";
+ }
+ Trace("quant-engine-debug") << std::endl;
+ Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
+ if( d_model->getNumToReduceQuantifiers()>0 ){
+ Trace("quant-engine-debug") << " # quantified formulas to reduce = " << d_model->getNumToReduceQuantifiers() << 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-debug") << "Resetting all modules..." << std::endl;
}
- 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;
+ if( Trace.isOn("quant-engine-ee") ){
+ Trace("quant-engine-ee") << "Equality engine : " << std::endl;
+ debugPrintEqualityEngine( "quant-engine-ee" );
}
- Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl;
- Trace("quant-engine-ee") << "Equality engine : " << std::endl;
- debugPrintEqualityEngine( "quant-engine-ee" );
-
- Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
//reset relevant information
d_conflict = false;
d_hasAddedLemma = false;
}
}
-void QuantifiersEngine::registerQuantifier( Node f ){
- if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
+bool QuantifiersEngine::registerQuantifier( Node f ){
+ std::map< Node, bool >::iterator it = d_quants.find( f );
+ if( it==d_quants.end() ){
Trace("quant") << "QuantifiersEngine : Register quantifier ";
Trace("quant") << " : " << f << std::endl;
- d_quants.push_back( f );
-
++(d_statistics.d_num_quant);
Assert( f.getKind()==FORALL );
- //make instantiation constants for f
- d_term_db->makeInstantiationConstantsFor( f );
- d_term_db->computeAttributes( f );
- QuantifiersModule * qm = getOwner( f );
- if( qm!=NULL ){
- Trace("quant") << " Owner : " << qm->identify() << std::endl;
- }
- //register with quantifier relevance
- if( d_quant_rel ){
- d_quant_rel->registerQuantifier( f );
- }
- //register with each module
- for( int i=0; i<(int)d_modules.size(); i++ ){
- d_modules[i]->registerQuantifier( f );
+
+ //check whether we should apply a reduction
+ bool reduced = false;
+ 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 ) ){
+ reduced = true;
+ }
}
- Node ceBody = d_term_db->getInstConstantBody( f );
- //generate the phase requirements
- d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
- //also register it with the strong solver
- if( options::finiteModelFind() ){
- ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
+ if( reduced ){
+ d_model->assertQuantifier( f, true );
+ d_quants[f] = false;
+ return false;
+ }else{
+ //make instantiation constants for f
+ d_term_db->makeInstantiationConstantsFor( f );
+ d_term_db->computeAttributes( f );
+ QuantifiersModule * qm = getOwner( f );
+ if( qm!=NULL ){
+ Trace("quant") << " Owner : " << qm->identify() << std::endl;
+ }
+ //register with quantifier relevance
+ if( d_quant_rel ){
+ d_quant_rel->registerQuantifier( f );
+ }
+ //register with each module
+ for( int i=0; i<(int)d_modules.size(); i++ ){
+ d_modules[i]->registerQuantifier( f );
+ }
+ Node ceBody = d_term_db->getInstConstantBody( f );
+ //generate the phase requirements
+ d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
+ //also register it with the strong solver
+ if( options::finiteModelFind() ){
+ ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
+ }
+ d_quants[f] = true;
+ return true;
}
+ }else{
+ return it->second;
}
}
}
//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 );
+ bool nreduced = registerQuantifier( f );
//assert it to each module
- d_model->assertQuantifier( f );
- for( int i=0; i<(int)d_modules.size(); i++ ){
- d_modules[i]->assertNode( f );
+ if( nreduced ){
+ d_model->assertQuantifier( f );
+ for( int i=0; i<(int)d_modules.size(); i++ ){
+ d_modules[i]->assertNode( f );
+ }
}
}
}
class QModelBuilder;
class ConjectureGenerator;
class CegInstantiation;
+ class LtePartialInst;
}/* CVC4::theory::quantifiers */
namespace inst {
/** ceg instantiation */
quantifiers::CegInstantiation * d_ceg_inst;
/** lte partial instantiation */
- QuantLtePartialInst * d_lte_part_inst;
+ quantifiers::LtePartialInst * d_lte_part_inst;
public: //effort levels
enum {
QEFFORT_CONFLICT,
};
private:
/** list of all quantifiers seen */
- std::vector< Node > d_quants;
+ std::map< Node, bool > d_quants;
/** list of all lemmas produced */
//std::map< Node, bool > d_lemmas_produced;
BoolMap d_lemmas_produced_c;
quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
/** ceg instantiation */
quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
+ /** local theory ext partial inst */
+ quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
private:
/** owner of quantified formulas */
std::map< Node, QuantifiersModule * > d_owner;
/** check at level */
void check( Theory::Effort e );
/** register quantifier */
- void registerQuantifier( Node f );
+ bool registerQuantifier( Node f );
/** register quantifier */
void registerPattern( std::vector<Node> & pattern);
/** assert universal quantifier */
bool getInstWhenNeedsCheck( Theory::Effort e );
/** set instantiation level attr */
static void setInstantiationLevelAttr( Node n, uint64_t level );
-public:
- /** get number of quantifiers */
- int getNumQuantifiers() { return (int)d_quants.size(); }
- /** get quantifier */
- Node getQuantifier( int i ) { return d_quants[i]; }
public:
/** get model */
quantifiers::FirstOrderModel* getModel() { return d_model; }
projects / cvc5.git / commitdiff