theory/quantifiers/fun_def_process.h \
theory/quantifiers/ho_trigger.cpp \
theory/quantifiers/ho_trigger.h \
+ theory/quantifiers/instantiate.cpp \
+ theory/quantifiers/instantiate.h \
theory/quantifiers/inst_match.cpp \
theory/quantifiers/inst_match.h \
+ theory/quantifiers/inst_match_trie.cpp \
+ theory/quantifiers/inst_match_trie.h \
theory/quantifiers/inst_match_generator.cpp \
theory/quantifiers/inst_match_generator.h \
theory/quantifiers/inst_propagator.cpp \
#include "theory/quantifiers/ambqi_builder.h"
#include "options/quantifiers_options.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
return true;
}else{
if( depth==q[0].getNumChildren() ){
- if( qe->addInstantiation( q, terms, true ) ){
+ if (qe->getInstantiate()->addInstantiation(q, terms, true))
+ {
Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;
inst++;
return true;
** \brief Implementation of theory uf candidate generator class
**/
-#include "options/quantifiers_options.h"
#include "theory/quantifiers/candidate_generator.h"
+#include "options/quantifiers_options.h"
#include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
if( d_firstTime ){
//must return something
d_firstTime = false;
- return d_qe->getTermForType(d_match_pattern_type);
+ return d_qe->getInstantiate()->getTermForType(d_match_pattern_type);
}
return Node::null();
}
#include "prop/prop_engine.h"
#include "smt/smt_statistics_registry.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/skolemize.h"
#include "theory/quantifiers/term_database_sygus.h"
}
Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl;
//construct base instantiation
- d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( d_embed_quant, vars, d_candidates ) );
+ d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation(
+ d_embed_quant, vars, d_candidates));
Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
// register this term with sygus database and other utilities that impact
getCandidateList( clist, true );
Assert( clist.size()==d_quant[0].getNumChildren() );
getModelValues( clist, model_terms );
- if( d_qe->addInstantiation( d_quant, model_terms ) ){
+ if (d_qe->getInstantiate()->addInstantiation(d_quant, model_terms))
+ {
//record the instantiation
recordInstantiation( model_terms );
}else{
#include "context/cdchunk_list.h"
#include "context/cdhashmap.h"
#include "theory/quantifiers/ce_guided_single_inv_sol.h"
+#include "theory/quantifiers/inst_match_trie.h"
#include "theory/quantifiers/inst_strategy_cbqi.h"
#include "theory/quantifiers/single_inv_partition.h"
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/equality_query.h"
#include "options/quantifiers_options.h"
-#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/equality_infer.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
** \brief Implementation of full model check class
**/
+#include "theory/quantifiers/full_model_check.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
}else{
//just add the instance
d_triedLemmas++;
- if( d_qe->addInstantiation( f, inst, true ) ){
+ if (d_qe->getInstantiate()->addInstantiation(f, inst, true))
+ {
Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
d_addedLemmas++;
if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
if (ev!=d_true) {
Trace("fmc-exh-debug") << ", add!";
//add as instantiation
- if( d_qe->addInstantiation( f, inst, true ) ){
+ if (d_qe->getInstantiate()->addInstantiation(f, inst, true))
+ {
Trace("fmc-exh-debug") << " ...success.";
addedLemmas++;
if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
#include <stack>
#include "theory/quantifiers/ho_trigger.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
else
{
// do not run higher-order matching
- return d_quantEngine->addInstantiation(d_f, m);
+ return d_quantEngine->getInstantiate()->addInstantiation(d_f, m);
}
}
if (var_index == d_ho_var_list.size())
{
// we now have an instantiation to try
- return d_quantEngine->addInstantiation(d_f, m);
+ return d_quantEngine->getInstantiate()->addInstantiation(d_f, m);
}
else
{
**/
#include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/term_database.h"
+
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers_engine.h"
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-
namespace CVC4 {
namespace theory {
namespace inst {
-InstMatch::InstMatch( TNode f ) {
- for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- d_vals.push_back( Node::null() );
- }
+InstMatch::InstMatch(TNode q)
+{
+ d_vals.resize(q[0].getNumChildren());
+ Assert(!d_vals.empty());
+ // resize must initialize with null nodes
+ Assert(d_vals[0].isNull());
}
InstMatch::InstMatch( InstMatch* m ) {
d_vals.insert( d_vals.end(), m->d_vals.begin(), m->d_vals.end() );
}
-bool InstMatch::add( InstMatch& m ){
- for( unsigned i=0; i<d_vals.size(); i++ ){
+void InstMatch::add(InstMatch& m)
+{
+ for (unsigned i = 0, size = d_vals.size(); i < size; i++)
+ {
if( d_vals[i].isNull() ){
d_vals[i] = m.d_vals[i];
}
}
- return true;
}
bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
- for( unsigned i=0; i<m.d_vals.size(); i++ ){
+ Assert(d_vals.size() == m.d_vals.size());
+ for (unsigned i = 0, size = d_vals.size(); i < size; i++)
+ {
if( !m.d_vals[i].isNull() ){
if( d_vals[i].isNull() ){
d_vals[i] = m.d_vals[i];
}
void InstMatch::debugPrint( const char* c ){
- for( unsigned i=0; i<d_vals.size(); i++ ){
+ for (unsigned i = 0, size = d_vals.size(); i < size; i++)
+ {
if( !d_vals[i].isNull() ){
Debug( c ) << " " << i << " -> " << d_vals[i] << std::endl;
}
}
bool InstMatch::isComplete() {
- for( unsigned i=0; i<d_vals.size(); i++ ){
- if( d_vals[i].isNull() ){
+ for (Node& v : d_vals)
+ {
+ if (v.isNull())
+ {
return false;
}
}
}
bool InstMatch::empty() {
- for( unsigned i=0; i<d_vals.size(); i++ ){
- if( !d_vals[i].isNull() ){
+ for (Node& v : d_vals)
+ {
+ if (!v.isNull())
+ {
return false;
}
}
return true;
}
-void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
- for( unsigned i=0; i<d_vals.size(); i++ ){
- if( !d_vals[i].isNull() ){
- if( qe->getEqualityQuery()->getEngine()->hasTerm( d_vals[i] ) ){
- d_vals[i] = qe->getEqualityQuery()->getEngine()->getRepresentative( d_vals[i] );
- }
- }
- }
-}
-
-void InstMatch::applyRewrite(){
- for( unsigned i=0; i<d_vals.size(); i++ ){
- if( !d_vals[i].isNull() ){
- d_vals[i] = Rewriter::rewrite( d_vals[i] );
- }
- }
-}
-
void InstMatch::clear() {
for( unsigned i=0; i<d_vals.size(); i++ ){
d_vals[i] = Node::null();
}
}
-/** get value */
-
-Node InstMatch::get( int i ) {
- return d_vals[i];
-}
-
-void InstMatch::getTerms( Node f, std::vector< Node >& inst ){
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- inst.push_back( d_vals[i] );
- }
+Node InstMatch::get(int i) const { return d_vals[i]; }
+void InstMatch::getInst(std::vector<Node>& inst) const
+{
+ inst.insert(inst.end(), d_vals.begin(), d_vals.end());
}
void InstMatch::setValue( int i, TNode n ) {
d_vals[i] = n;
}
-
-bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) {
+bool InstMatch::set(EqualityQuery* q, int i, TNode n)
+{
Assert( i>=0 );
if( !d_vals[i].isNull() ){
- if( qe->getEqualityQuery()->areEqual( d_vals[i], n ) ){
+ if (q->areEqual(d_vals[i], n))
+ {
return true;
}else{
return false;
}
}
-bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq,
- ImtIndexOrder* imtio, bool onlyExist, int index ) {
- if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
- return false;
- }else{
- int i_index = imtio ? imtio->d_order[index] : index;
- Node n = m[i_index];
- std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
- if( it!=d_data.end() ){
- bool ret = it->second.addInstMatch( qe, f, m, modEq, imtio, onlyExist, index+1 );
- if( !onlyExist || !ret ){
- return ret;
- }
- }
- if( modEq ){
- //check modulo equality if any other instantiation match exists
- if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
- eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
- qe->getEqualityQuery()->getEngine() );
- while( !eqc.isFinished() ){
- Node en = (*eqc);
- if( en!=n ){
- std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
- if( itc!=d_data.end() ){
- if( itc->second.addInstMatch( qe, f, m, modEq, imtio, true, index+1 ) ){
- return false;
- }
- }
- }
- ++eqc;
- }
- }
- }
- if( !onlyExist ){
- d_data[n].addInstMatch( qe, f, m, modEq, imtio, false, index+1 );
- }
- return true;
- }
-}
-
-bool InstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, ImtIndexOrder* imtio, int index ) {
- Assert( index<(int)q[0].getNumChildren() );
- Assert( !imtio || index<(int)imtio->d_order.size() );
- int i_index = imtio ? imtio->d_order[index] : index;
- Node n = m[i_index];
- std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
- if( it!=d_data.end() ){
- if( (index+1)==(int)q[0].getNumChildren() || ( imtio && (index+1)==(int)imtio->d_order.size() ) ){
- d_data.erase( n );
- return true;
- }else{
- return it->second.removeInstMatch( qe, q, m, imtio, index+1 );
- }
- }else{
- return false;
- }
-}
-
-bool InstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio, int index ){
- if( index==(int)q[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
- setInstLemma( lem );
- return true;
- }else{
- int i_index = imtio ? imtio->d_order[index] : index;
- std::map< Node, InstMatchTrie >::iterator it = d_data.find( m[i_index] );
- if( it!=d_data.end() ){
- return it->second.recordInstLemma( q, m, lem, imtio, index+1 );
- }else{
- return false;
- }
- }
-}
-
-void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const {
- if( terms.size()==q[0].getNumChildren() ){
- bool print;
- if( useActive ){
- if( hasInstLemma() ){
- Node lem = getInstLemma();
- print = std::find( active.begin(), active.end(), lem )!=active.end();
- }else{
- print = false;
- }
- }else{
- print = true;
- }
- if( print ){
- if( firstTime ){
- out << "(instantiation " << q << std::endl;
- firstTime = false;
- }
- out << " ( ";
- for( unsigned i=0; i<terms.size(); i++ ){
- if( i>0 ){ out << ", ";}
- out << terms[i];
- }
- out << " )" << std::endl;
- }
- }else{
- for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second.print( out, q, terms, firstTime, useActive, active );
- terms.pop_back();
- }
- }
-}
-
-void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const {
- if( terms.size()==q[0].getNumChildren() ){
- if( useActive ){
- if( hasInstLemma() ){
- Node lem = getInstLemma();
- if( std::find( active.begin(), active.end(), lem )!=active.end() ){
- insts.push_back( lem );
- }
- }
- }else{
- if( hasInstLemma() ){
- insts.push_back( getInstLemma() );
- }else{
- insts.push_back( qe->getInstantiation( q, terms, true ) );
- }
- }
- }else{
- for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second.getInstantiations( insts, q, terms, qe, useActive, active );
- terms.pop_back();
- }
- }
-}
-
-void InstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
- if( terms.size()==q[0].getNumChildren() ){
- if( hasInstLemma() ){
- Node lem = getInstLemma();
- if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){
- quant[lem] = q;
- tvec[lem].clear();
- tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() );
- }
- }
- }else{
- for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second.getExplanationForInstLemmas( q, terms, lems, quant, tvec );
- terms.pop_back();
- }
- }
-}
-
-CDInstMatchTrie::~CDInstMatchTrie() {
- for(std::map< Node, CDInstMatchTrie* >::iterator i = d_data.begin(),
- iend = d_data.end(); i != iend; ++i) {
- CDInstMatchTrie* current = (*i).second;
- delete current;
- }
- d_data.clear();
-}
-
-
-bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
- context::Context* c, bool modEq, int index, bool onlyExist ){
- bool reset = false;
- if( !d_valid.get() ){
- if( onlyExist ){
- return true;
- }else{
- d_valid.set( true );
- reset = true;
- }
- }
- if( index==(int)f[0].getNumChildren() ){
- return reset;
- }else{
- Node n = m[ index ];
- std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
- if( it!=d_data.end() ){
- bool ret = it->second->addInstMatch( qe, f, m, c, modEq, index+1, onlyExist );
- if( !onlyExist || !ret ){
- return reset || ret;
- }
- }
- if( modEq ){
- //check modulo equality if any other instantiation match exists
- if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
- eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
- qe->getEqualityQuery()->getEngine() );
- while( !eqc.isFinished() ){
- Node en = (*eqc);
- if( en!=n ){
- std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
- if( itc!=d_data.end() ){
- if( itc->second->addInstMatch( qe, f, m, c, modEq, index+1, true ) ){
- return false;
- }
- }
- }
- ++eqc;
- }
- }
- }
-
- if( !onlyExist ){
- // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
- CDInstMatchTrie* imt = new CDInstMatchTrie( c );
- Assert(d_data.find(n) == d_data.end());
- d_data[n] = imt;
- imt->addInstMatch( qe, f, m, c, modEq, index+1, false );
- }
- return true;
- }
-}
-
-bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index ) {
- if( index==(int)q[0].getNumChildren() ){
- if( d_valid.get() ){
- d_valid.set( false );
- return true;
- }else{
- return false;
- }
- }else{
- std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] );
- if( it!=d_data.end() ){
- return it->second->removeInstMatch( qe, q, m, index+1 );
- }else{
- return false;
- }
- }
-}
-
-bool CDInstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index ) {
- if( index==(int)q[0].getNumChildren() ){
- if( d_valid.get() ){
- setInstLemma( lem );
- return true;
- }else{
- return false;
- }
- }else{
- std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] );
- if( it!=d_data.end() ){
- return it->second->recordInstLemma( q, m, lem, index+1 );
- }else{
- return false;
- }
- }
-}
-
-void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
- if( d_valid.get() ){
- if( terms.size()==q[0].getNumChildren() ){
- bool print;
- if( useActive ){
- if( hasInstLemma() ){
- Node lem = getInstLemma();
- print = std::find( active.begin(), active.end(), lem )!=active.end();
- }else{
- print = false;
- }
- }else{
- print = true;
- }
- if( print ){
- if( firstTime ){
- out << "(instantiation " << q << std::endl;
- firstTime = false;
- }
- out << " ( ";
- for( unsigned i=0; i<terms.size(); i++ ){
- if( i>0 ) out << " ";
- out << terms[i];
- }
- out << " )" << std::endl;
- }
- }else{
- for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second->print( out, q, terms, firstTime, useActive, active );
- terms.pop_back();
- }
- }
- }
-}
-
-void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const{
- if( d_valid.get() ){
- if( terms.size()==q[0].getNumChildren() ){
- if( useActive ){
- if( hasInstLemma() ){
- Node lem = getInstLemma();
- if( std::find( active.begin(), active.end(), lem )!=active.end() ){
- insts.push_back( lem );
- }
- }
- }else{
- if( hasInstLemma() ){
- insts.push_back( getInstLemma() );
- }else{
- insts.push_back( qe->getInstantiation( q, terms, true ) );
- }
- }
- }else{
- for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second->getInstantiations( insts, q, terms, qe, useActive, active );
- terms.pop_back();
- }
- }
- }
-}
-
-
-void CDInstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
- if( d_valid.get() ){
- if( terms.size()==q[0].getNumChildren() ){
- if( hasInstLemma() ){
- Node lem;
- if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){
- quant[lem] = q;
- tvec[lem].clear();
- tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() );
- }
- }
- }else{
- for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second->getExplanationForInstLemmas( q, terms, lems, quant, tvec );
- terms.pop_back();
- }
- }
- }
-}
-
}/* CVC4::theory::inst namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
-#include <map>
+#include <vector>
-#include "context/cdlist.h"
-#include "context/cdo.h"
#include "expr/node.h"
namespace CVC4 {
namespace theory {
-class QuantifiersEngine;
class EqualityQuery;
namespace inst {
-/** basic class defining an instantiation */
+/** Inst match
+ *
+ * This is the basic class specifying an instantiation. Its domain size (the
+ * size of d_vals) is the number of bound variables of the quantified formula
+ * that is passed to its constructor.
+ *
+ * The values of d_vals may be null, which indicate that the field has
+ * yet to be initialized.
+ */
class InstMatch {
-public:
- /* map from variable to ground terms */
- std::vector< Node > d_vals;
public:
InstMatch(){}
- explicit InstMatch( TNode f );
+ explicit InstMatch(TNode q);
InstMatch( InstMatch* m );
-
- /** fill all unfilled values with m */
- bool add( InstMatch& m );
- /** if compatible, fill all unfilled values with m and return true
- return false otherwise */
+ /* map from variable to ground terms */
+ std::vector<Node> d_vals;
+ /** add match m
+ *
+ * This adds the initialized fields of m to this match for each field that is
+ * not already initialized in this match.
+ */
+ void add(InstMatch& m);
+ /** merge with match m
+ *
+ * This method returns true if the merge was successful, that is, all jointly
+ * initialized fields of this class and m are equivalent modulo the equalities
+ * given by q.
+ */
bool merge( EqualityQuery* q, InstMatch& m );
- /** debug print method */
- void debugPrint( const char* c );
- /** is complete? */
+ /** is this complete, i.e. are all fields non-null? */
bool isComplete();
- /** make representative */
- void makeRepresentative( QuantifiersEngine* qe );
- /** empty */
+ /** is this empty, i.e. are all fields the null node? */
bool empty();
- /** clear */
+ /** clear the instantiation, i.e. set all fields to the null node */
void clear();
+ /** debug print method */
+ void debugPrint(const char* c);
/** to stream */
inline void toStream(std::ostream& out) const {
out << "INST_MATCH( ";
}
out << " )";
}
- /** apply rewrite */
- void applyRewrite();
- /** get */
- Node get( int i );
- void getTerms( Node f, std::vector< Node >& inst );
- /** set */
+ /** get the i^th term in the instantiation */
+ Node get(int i) const;
+ /** append the terms of this instantiation to inst */
+ void getInst(std::vector<Node>& inst) const;
+ /** set/overwrites the i^th field in the instantiation with n */
void setValue( int i, TNode n );
- bool set( QuantifiersEngine* qe, int i, TNode n );
-};/* class InstMatch */
+ /** set the i^th term in the instantiation to n
+ *
+ * This method returns true if the i^th field was previously uninitialized,
+ * or is equivalent to n modulo the equalities given by q.
+ */
+ bool set(EqualityQuery* q, int i, TNode n);
+};
inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
m.toStream(out);
return out;
}
-/** trie for InstMatch objects */
-class InstMatchTrie {
-public:
- class ImtIndexOrder {
- public:
- std::vector< int > d_order;
- };/* class InstMatchTrie ImtIndexOrder */
- /** the data */
- std::map< Node, InstMatchTrie > d_data;
-private:
- void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const;
- void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const;
- void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const;
-private:
- void setInstLemma( Node n ){
- d_data.clear();
- d_data[n].clear();
- }
- bool hasInstLemma() const { return !d_data.empty(); }
- Node getInstLemma() const { return d_data.begin()->first; }
-public:
- InstMatchTrie(){}
- ~InstMatchTrie(){}
-public:
- /** return true if m exists in this trie
- modEq is if we check modulo equality
- modInst is if we return true if m is an instance of a match that exists
- */
- bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
- ImtIndexOrder* imtio = NULL, int index = 0 ) {
- return !addInstMatch( qe, f, m, modEq, imtio, true, index );
- }
- bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
- ImtIndexOrder* imtio = NULL, int index = 0 ) {
- return !addInstMatch( qe, f, m, modEq, imtio, true, index );
- }
- /** add match m for quantifier f, take into account equalities if modEq = true,
- if imtio is non-null, this is the order to add to trie
- return true if successful
- */
- bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
- ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
- return addInstMatch( qe, f, m.d_vals, modEq, imtio, onlyExist, index );
- }
- bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
- ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
- bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 );
- bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio = NULL, int index = 0 );
- void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
- std::vector< TNode > terms;
- print( out, q, terms, firstTime, useActive, active );
- }
- void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) {
- std::vector< Node > terms;
- getInstantiations( insts, q, terms, qe, useActive, active );
- }
- void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
- std::vector< Node > terms;
- getExplanationForInstLemmas( q, terms, lems, quant, tvec );
- }
- void clear() { d_data.clear(); }
-};/* class InstMatchTrie */
-
-/** trie for InstMatch objects */
-class CDInstMatchTrie {
-private:
- /** the data */
- std::map< Node, CDInstMatchTrie* > d_data;
- /** is valid */
- context::CDO< bool > d_valid;
-private:
- void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const;
- void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const;
- void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const;
-private:
- void setInstLemma( Node n ){
- d_data.clear();
- d_data[n] = NULL;
- }
- bool hasInstLemma() const { return !d_data.empty(); }
- Node getInstLemma() const { return d_data.begin()->first; }
-public:
- CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
- ~CDInstMatchTrie();
-
- /** return true if m exists in this trie
- modEq is if we check modulo equality
- modInst is if we return true if m is an instance of a match that exists
- */
- bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
- int index = 0 ) {
- return !addInstMatch( qe, q, m, c, modEq, index, true );
- }
- bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
- int index = 0 ) {
- return !addInstMatch( qe, q, m, c, modEq, index, true );
- }
- /** add match m for quantifier f, take into account equalities if modEq = true,
- if imtio is non-null, this is the order to add to trie
- return true if successful
- */
- bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
- int index = 0, bool onlyExist = false ) {
- return addInstMatch( qe, q, m.d_vals, c, modEq, index, onlyExist );
- }
- bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
- int index = 0, bool onlyExist = false );
- bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 );
- bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index = 0 );
- void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
- std::vector< TNode > terms;
- print( out, q, terms, firstTime, useActive, active );
- }
- void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) {
- std::vector< Node > terms;
- getInstantiations( insts, q, terms, qe, useActive, active );
- }
- void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
- std::vector< Node > terms;
- getExplanationForInstLemmas( q, terms, lems, quant, tvec );
- }
-};/* class CDInstMatchTrie */
-
-
-class InstMatchTrieOrdered{
-private:
- InstMatchTrie::ImtIndexOrder* d_imtio;
- InstMatchTrie d_imt;
-public:
- InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){}
- ~InstMatchTrieOrdered(){}
- /** get ordering */
- InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
- /** get trie */
- InstMatchTrie* getTrie() { return &d_imt; }
-public:
- /** add match m, return true if successful */
- bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
- return d_imt.addInstMatch( qe, f, m, modEq, d_imtio );
- }
- bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
- return d_imt.existsInstMatch( qe, f, m, modEq, d_imtio );
- }
-};/* class InstMatchTrieOrdered */
-
}/* CVC4::theory::inst namespace */
typedef CVC4::theory::inst::InstMatch InstMatch;
#include "theory/quantifiers/inst_match_generator.h"
#include "expr/datatype.h"
-#include "options/quantifiers_options.h"
#include "options/datatypes_options.h"
+#include "options/quantifiers_options.h"
#include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
if( d_children_types[i]==0 ){
Trace("matching-debug2") << "Setting " << d_var_num[i] << " to " << t[i] << "..." << std::endl;
bool addToPrev = m.get( d_var_num[i] ).isNull();
- if( !m.set( qe, d_var_num[i], t[i] ) ){
+ if (!m.set(q, d_var_num[i], t[i]))
+ {
//match is in conflict
Trace("matching-fail") << "Match fail: " << m.get(d_var_num[i]) << " and " << t[i] << std::endl;
success = false;
//for variable matching
if( d_match_pattern.getKind()==INST_CONSTANT ){
bool addToPrev = m.get( d_var_num[0] ).isNull();
- if( !m.set( qe, d_var_num[0], t ) ){
+ if (!m.set(q, d_var_num[0], t))
+ {
success = false;
}else{
if( addToPrev ){
}
if( !t_match.isNull() ){
bool addToPrev = m.get( v ).isNull();
- if( !m.set( qe, v, t_match ) ){
+ if (!m.set(q, v, t_match))
+ {
success = false;
}else if( addToPrev ){
prev.push_back( v );
Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern ));
d_eq_class = Node::null();
d_rm_prev = m.get( d_var_num[0] ).isNull();
- if( !m.set( qe, d_var_num[0], s ) ){
+ if (!m.set(qe->getEqualityQuery(), d_var_num[0], s))
+ {
return -1;
}else{
ret_val = continueNextMatch(q, m, qe, tparent);
d_eq_class = Node::null();
//if( s.getType().isSubtypeOf( d_var_type ) ){
d_rm_prev = m.get( d_var_num[0] ).isNull();
- if( !m.set( qe, d_var_num[0], s ) ){
+ if (!m.set(qe->getEqualityQuery(), d_var_num[0], s))
+ {
return -1;
}else{
ret_val = continueNextMatch(q, m, qe, tparent);
}
// we do not need the trigger parent for simple triggers (no post-processing
// required)
- if (qe->addInstantiation(d_quant, m))
+ if (qe->getInstantiate()->addInstantiation(d_quant, m))
{
addedLemmas++;
Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
-#include "theory/quantifiers/inst_match.h"
#include <map>
+#include "theory/quantifiers/inst_match_trie.h"
namespace CVC4 {
namespace theory {
--- /dev/null
+/********************* */
+/*! \file inst_match.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of inst match class
+ **/
+
+#include "theory/quantifiers/inst_match_trie.h"
+
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& m,
+ bool modEq,
+ ImtIndexOrder* imtio,
+ bool onlyExist,
+ unsigned index)
+{
+ if (index == f[0].getNumChildren()
+ || (imtio && index == imtio->d_order.size()))
+ {
+ return false;
+ }
+ unsigned i_index = imtio ? imtio->d_order[index] : index;
+ Node n = m[i_index];
+ std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
+ if (it != d_data.end())
+ {
+ bool ret =
+ it->second.addInstMatch(qe, f, m, modEq, imtio, onlyExist, index + 1);
+ if (!onlyExist || !ret)
+ {
+ return ret;
+ }
+ }
+ if (modEq)
+ {
+ // check modulo equality if any other instantiation match exists
+ if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n))
+ {
+ eq::EqClassIterator eqc(
+ qe->getEqualityQuery()->getEngine()->getRepresentative(n),
+ qe->getEqualityQuery()->getEngine());
+ while (!eqc.isFinished())
+ {
+ Node en = (*eqc);
+ if (en != n)
+ {
+ std::map<Node, InstMatchTrie>::iterator itc = d_data.find(en);
+ if (itc != d_data.end())
+ {
+ if (itc->second.addInstMatch(
+ qe, f, m, modEq, imtio, true, index + 1))
+ {
+ return false;
+ }
+ }
+ }
+ ++eqc;
+ }
+ }
+ }
+ if (!onlyExist)
+ {
+ d_data[n].addInstMatch(qe, f, m, modEq, imtio, false, index + 1);
+ }
+ return true;
+}
+
+bool InstMatchTrie::removeInstMatch(Node q,
+ std::vector<Node>& m,
+ ImtIndexOrder* imtio,
+ unsigned index)
+{
+ Assert(index < q[0].getNumChildren());
+ Assert(!imtio || index < imtio->d_order.size());
+ unsigned i_index = imtio ? imtio->d_order[index] : index;
+ Node n = m[i_index];
+ std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
+ if (it != d_data.end())
+ {
+ if ((index + 1) == q[0].getNumChildren()
+ || (imtio && (index + 1) == imtio->d_order.size()))
+ {
+ d_data.erase(n);
+ return true;
+ }
+ return it->second.removeInstMatch(q, m, imtio, index + 1);
+ }
+ return false;
+}
+
+bool InstMatchTrie::recordInstLemma(Node q,
+ std::vector<Node>& m,
+ Node lem,
+ ImtIndexOrder* imtio,
+ unsigned index)
+{
+ if (index == q[0].getNumChildren()
+ || (imtio && index == imtio->d_order.size()))
+ {
+ setInstLemma(lem);
+ return true;
+ }
+ unsigned i_index = imtio ? imtio->d_order[index] : index;
+ std::map<Node, InstMatchTrie>::iterator it = d_data.find(m[i_index]);
+ if (it != d_data.end())
+ {
+ return it->second.recordInstLemma(q, m, lem, imtio, index + 1);
+ }
+ return false;
+}
+
+void InstMatchTrie::print(std::ostream& out,
+ Node q,
+ std::vector<TNode>& terms,
+ bool& firstTime,
+ bool useActive,
+ std::vector<Node>& active) const
+{
+ if (terms.size() == q[0].getNumChildren())
+ {
+ bool print;
+ if (useActive)
+ {
+ if (hasInstLemma())
+ {
+ Node lem = getInstLemma();
+ print = std::find(active.begin(), active.end(), lem) != active.end();
+ }
+ else
+ {
+ print = false;
+ }
+ }
+ else
+ {
+ print = true;
+ }
+ if (print)
+ {
+ if (firstTime)
+ {
+ out << "(instantiation " << q << std::endl;
+ firstTime = false;
+ }
+ out << " ( ";
+ for (unsigned i = 0, size = terms.size(); i < size; i++)
+ {
+ if (i > 0)
+ {
+ out << ", ";
+ }
+ out << terms[i];
+ }
+ out << " )" << std::endl;
+ }
+ }
+ else
+ {
+ for (const std::pair<const Node, InstMatchTrie>& d : d_data)
+ {
+ terms.push_back(d.first);
+ d.second.print(out, q, terms, firstTime, useActive, active);
+ terms.pop_back();
+ }
+ }
+}
+
+void InstMatchTrie::getInstantiations(std::vector<Node>& insts,
+ Node q,
+ std::vector<Node>& terms,
+ QuantifiersEngine* qe,
+ bool useActive,
+ std::vector<Node>& active) const
+{
+ if (terms.size() == q[0].getNumChildren())
+ {
+ if (useActive)
+ {
+ if (hasInstLemma())
+ {
+ Node lem = getInstLemma();
+ if (std::find(active.begin(), active.end(), lem) != active.end())
+ {
+ insts.push_back(lem);
+ }
+ }
+ }
+ else
+ {
+ if (hasInstLemma())
+ {
+ insts.push_back(getInstLemma());
+ }
+ else
+ {
+ insts.push_back(qe->getInstantiate()->getInstantiation(q, terms, true));
+ }
+ }
+ }
+ else
+ {
+ for (const std::pair<const Node, InstMatchTrie>& d : d_data)
+ {
+ terms.push_back(d.first);
+ d.second.getInstantiations(insts, q, terms, qe, useActive, active);
+ terms.pop_back();
+ }
+ }
+}
+
+void InstMatchTrie::getExplanationForInstLemmas(
+ Node q,
+ std::vector<Node>& terms,
+ const std::vector<Node>& lems,
+ std::map<Node, Node>& quant,
+ std::map<Node, std::vector<Node> >& tvec) const
+{
+ if (terms.size() == q[0].getNumChildren())
+ {
+ if (hasInstLemma())
+ {
+ Node lem = getInstLemma();
+ if (std::find(lems.begin(), lems.end(), lem) != lems.end())
+ {
+ quant[lem] = q;
+ tvec[lem].clear();
+ tvec[lem].insert(tvec[lem].end(), terms.begin(), terms.end());
+ }
+ }
+ }
+ else
+ {
+ for (const std::pair<const Node, InstMatchTrie>& d : d_data)
+ {
+ terms.push_back(d.first);
+ d.second.getExplanationForInstLemmas(q, terms, lems, quant, tvec);
+ terms.pop_back();
+ }
+ }
+}
+
+CDInstMatchTrie::~CDInstMatchTrie()
+{
+ for (std::pair<const Node, CDInstMatchTrie*>& d : d_data)
+ {
+ CDInstMatchTrie* current = d.second;
+ delete current;
+ }
+ d_data.clear();
+}
+
+bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& m,
+ context::Context* c,
+ bool modEq,
+ unsigned index,
+ bool onlyExist)
+{
+ bool reset = false;
+ if (!d_valid.get())
+ {
+ if (onlyExist)
+ {
+ return true;
+ }
+ else
+ {
+ d_valid.set(true);
+ reset = true;
+ }
+ }
+ if (index == f[0].getNumChildren())
+ {
+ return reset;
+ }
+ Node n = m[index];
+ std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
+ if (it != d_data.end())
+ {
+ bool ret =
+ it->second->addInstMatch(qe, f, m, c, modEq, index + 1, onlyExist);
+ if (!onlyExist || !ret)
+ {
+ return reset || ret;
+ }
+ }
+ if (modEq)
+ {
+ // check modulo equality if any other instantiation match exists
+ if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n))
+ {
+ eq::EqClassIterator eqc(
+ qe->getEqualityQuery()->getEngine()->getRepresentative(n),
+ qe->getEqualityQuery()->getEngine());
+ while (!eqc.isFinished())
+ {
+ Node en = (*eqc);
+ if (en != n)
+ {
+ std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en);
+ if (itc != d_data.end())
+ {
+ if (itc->second->addInstMatch(qe, f, m, c, modEq, index + 1, true))
+ {
+ return false;
+ }
+ }
+ }
+ ++eqc;
+ }
+ }
+ }
+
+ if (!onlyExist)
+ {
+ // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+ CDInstMatchTrie* imt = new CDInstMatchTrie(c);
+ Assert(d_data.find(n) == d_data.end());
+ d_data[n] = imt;
+ imt->addInstMatch(qe, f, m, c, modEq, index + 1, false);
+ }
+ return true;
+}
+
+bool CDInstMatchTrie::removeInstMatch(Node q,
+ std::vector<Node>& m,
+ unsigned index)
+{
+ if (index == q[0].getNumChildren())
+ {
+ if (d_valid.get())
+ {
+ d_valid.set(false);
+ return true;
+ }
+ return false;
+ }
+ std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]);
+ if (it != d_data.end())
+ {
+ return it->second->removeInstMatch(q, m, index + 1);
+ }
+ return false;
+}
+
+bool CDInstMatchTrie::recordInstLemma(Node q,
+ std::vector<Node>& m,
+ Node lem,
+ unsigned index)
+{
+ if (index == q[0].getNumChildren())
+ {
+ if (d_valid.get())
+ {
+ setInstLemma(lem);
+ return true;
+ }
+ return false;
+ }
+ std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]);
+ if (it != d_data.end())
+ {
+ return it->second->recordInstLemma(q, m, lem, index + 1);
+ }
+ return false;
+}
+
+void CDInstMatchTrie::print(std::ostream& out,
+ Node q,
+ std::vector<TNode>& terms,
+ bool& firstTime,
+ bool useActive,
+ std::vector<Node>& active) const
+{
+ if (d_valid.get())
+ {
+ if (terms.size() == q[0].getNumChildren())
+ {
+ bool print;
+ if (useActive)
+ {
+ if (hasInstLemma())
+ {
+ Node lem = getInstLemma();
+ print = std::find(active.begin(), active.end(), lem) != active.end();
+ }
+ else
+ {
+ print = false;
+ }
+ }
+ else
+ {
+ print = true;
+ }
+ if (print)
+ {
+ if (firstTime)
+ {
+ out << "(instantiation " << q << std::endl;
+ firstTime = false;
+ }
+ out << " ( ";
+ for (unsigned i = 0; i < terms.size(); i++)
+ {
+ if (i > 0) out << " ";
+ out << terms[i];
+ }
+ out << " )" << std::endl;
+ }
+ }
+ else
+ {
+ for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
+ {
+ terms.push_back(d.first);
+ d.second->print(out, q, terms, firstTime, useActive, active);
+ terms.pop_back();
+ }
+ }
+ }
+}
+
+void CDInstMatchTrie::getInstantiations(std::vector<Node>& insts,
+ Node q,
+ std::vector<Node>& terms,
+ QuantifiersEngine* qe,
+ bool useActive,
+ std::vector<Node>& active) const
+{
+ if (d_valid.get())
+ {
+ if (terms.size() == q[0].getNumChildren())
+ {
+ if (useActive)
+ {
+ if (hasInstLemma())
+ {
+ Node lem = getInstLemma();
+ if (std::find(active.begin(), active.end(), lem) != active.end())
+ {
+ insts.push_back(lem);
+ }
+ }
+ }
+ else
+ {
+ if (hasInstLemma())
+ {
+ insts.push_back(getInstLemma());
+ }
+ else
+ {
+ insts.push_back(
+ qe->getInstantiate()->getInstantiation(q, terms, true));
+ }
+ }
+ }
+ else
+ {
+ for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
+ {
+ terms.push_back(d.first);
+ d.second->getInstantiations(insts, q, terms, qe, useActive, active);
+ terms.pop_back();
+ }
+ }
+ }
+}
+
+void CDInstMatchTrie::getExplanationForInstLemmas(
+ Node q,
+ std::vector<Node>& terms,
+ const std::vector<Node>& lems,
+ std::map<Node, Node>& quant,
+ std::map<Node, std::vector<Node> >& tvec) const
+{
+ if (d_valid.get())
+ {
+ if (terms.size() == q[0].getNumChildren())
+ {
+ if (hasInstLemma())
+ {
+ Node lem;
+ if (std::find(lems.begin(), lems.end(), lem) != lems.end())
+ {
+ quant[lem] = q;
+ tvec[lem].clear();
+ tvec[lem].insert(tvec[lem].end(), terms.begin(), terms.end());
+ }
+ }
+ }
+ else
+ {
+ for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
+ {
+ terms.push_back(d.first);
+ d.second->getExplanationForInstLemmas(q, terms, lems, quant, tvec);
+ terms.pop_back();
+ }
+ }
+ }
+}
+
+} /* CVC4::theory::inst namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file inst_match.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Francois Bobot
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief inst match class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
+#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
+
+#include <map>
+
+#include "context/cdlist.h"
+#include "context/cdo.h"
+#include "expr/node.h"
+#include "theory/quantifiers/inst_match.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+class EqualityQuery;
+
+namespace inst {
+
+/** trie for InstMatch objects
+ *
+ * This class is used for storing instantiations of a quantified formula q.
+ * It is a trie data structure for which entries can be added and removed.
+ * This class has interfaces for adding instantiations that are either
+ * represented by std::vectors or InstMatch objects (see inst_match.h).
+ */
+class InstMatchTrie
+{
+ public:
+ /** index ordering */
+ class ImtIndexOrder
+ {
+ public:
+ std::vector<unsigned> d_order;
+ };
+
+ public:
+ InstMatchTrie() {}
+ ~InstMatchTrie() {}
+ /** exists inst match
+ *
+ * This method considers the entry given by m, starting at the given index.
+ * The domain of m is the bound variables of quantified formula q.
+ * It returns true if (the suffix) of m exists in this trie.
+ * If modEq is true, we check for duplication modulo equality the current
+ * equalities in the active equality engine of qe.
+ */
+ bool existsInstMatch(QuantifiersEngine* qe,
+ Node q,
+ InstMatch& m,
+ bool modEq = false,
+ ImtIndexOrder* imtio = NULL,
+ unsigned index = 0)
+ {
+ return !addInstMatch(qe, q, m, modEq, imtio, true, index);
+ }
+ /** exists inst match, vector version */
+ bool existsInstMatch(QuantifiersEngine* qe,
+ Node q,
+ std::vector<Node>& m,
+ bool modEq = false,
+ ImtIndexOrder* imtio = NULL,
+ unsigned index = 0)
+ {
+ return !addInstMatch(qe, q, m, modEq, imtio, true, index);
+ }
+ /** add inst match
+ *
+ * This method adds (the suffix of) m starting at the given index to this
+ * trie, and returns true if and only if m did not already occur in this trie.
+ * The domain of m is the bound variables of quantified formula q.
+ * If modEq is true, we check for duplication modulo equality the current
+ * equalities in the active equality engine of qe.
+ */
+ bool addInstMatch(QuantifiersEngine* qe,
+ Node q,
+ InstMatch& m,
+ bool modEq = false,
+ ImtIndexOrder* imtio = NULL,
+ bool onlyExist = false,
+ unsigned index = 0)
+ {
+ return addInstMatch(qe, q, m.d_vals, modEq, imtio, onlyExist, index);
+ }
+ /** add inst match, vector version */
+ bool addInstMatch(QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& m,
+ bool modEq = false,
+ ImtIndexOrder* imtio = NULL,
+ bool onlyExist = false,
+ unsigned index = 0);
+ /** remove inst match
+ *
+ * This removes (the suffix of) m starting at the given index from this trie.
+ * It returns true if and only if this entry existed in this trie.
+ * The domain of m is the bound variables of quantified formula q.
+ */
+ bool removeInstMatch(Node f,
+ std::vector<Node>& m,
+ ImtIndexOrder* imtio = NULL,
+ unsigned index = 0);
+ /** record instantiation lemma
+ *
+ * This records that the instantiation lemma lem corresponds to the entry
+ * given by (the suffix of) m starting at the given index.
+ */
+ bool recordInstLemma(Node q,
+ std::vector<Node>& m,
+ Node lem,
+ ImtIndexOrder* imtio = NULL,
+ unsigned index = 0);
+
+ /** get instantiations
+ *
+ * This gets the set of instantiation lemmas that were recorded in this trie
+ * via calls to recordInstLemma. If useActive is true, we only add
+ * instantiations that occur in active.
+ */
+ void getInstantiations(std::vector<Node>& insts,
+ Node q,
+ QuantifiersEngine* qe,
+ bool useActive,
+ std::vector<Node>& active)
+ {
+ std::vector<Node> terms;
+ getInstantiations(insts, q, terms, qe, useActive, active);
+ }
+ /** get explanation for inst lemmas
+ *
+ * This gets the explanation for the instantiation lemmas in lems for
+ * quantified formula q, for which this trie stores instantiation matches for.
+ * For each instantiation lemma lem recording in this trie via calls to
+ * recordInstLemma, we map lem to q in map quant, and lem to its corresponding
+ * vector of terms in tvec.
+ */
+ void getExplanationForInstLemmas(
+ Node q,
+ const std::vector<Node>& lems,
+ std::map<Node, Node>& quant,
+ std::map<Node, std::vector<Node> >& tvec) const
+ {
+ std::vector<Node> terms;
+ getExplanationForInstLemmas(q, terms, lems, quant, tvec);
+ }
+
+ /** clear the data of this class */
+ void clear() { d_data.clear(); }
+ /** print this class */
+ void print(std::ostream& out,
+ Node q,
+ bool& firstTime,
+ bool useActive,
+ std::vector<Node>& active) const
+ {
+ std::vector<TNode> terms;
+ print(out, q, terms, firstTime, useActive, active);
+ }
+ /** the data */
+ std::map<Node, InstMatchTrie> d_data;
+
+ private:
+ /** helper for print
+ * terms accumulates the path we are on in the trie.
+ */
+ void print(std::ostream& out,
+ Node q,
+ std::vector<TNode>& terms,
+ bool& firstTime,
+ bool useActive,
+ std::vector<Node>& active) const;
+ /** helper for get instantiations
+ * terms accumulates the path we are on in the trie.
+ */
+ void getInstantiations(std::vector<Node>& insts,
+ Node q,
+ std::vector<Node>& terms,
+ QuantifiersEngine* qe,
+ bool useActive,
+ std::vector<Node>& active) const;
+ /** helper for get explantaion for inst lemmas
+ * terms accumulates the path we are on in the trie.
+ */
+ void getExplanationForInstLemmas(
+ Node q,
+ std::vector<Node>& terms,
+ const std::vector<Node>& lems,
+ std::map<Node, Node>& quant,
+ std::map<Node, std::vector<Node> >& tvec) const;
+ /** set instantiation lemma at this node in the trie */
+ void setInstLemma(Node n)
+ {
+ d_data.clear();
+ d_data[n].clear();
+ }
+ /** does this node of the trie store an instantiation lemma? */
+ bool hasInstLemma() const { return !d_data.empty(); }
+ /** get the instantiation lemma stored in this node of the trie */
+ Node getInstLemma() const { return d_data.begin()->first; }
+};
+
+/** trie for InstMatch objects
+ *
+ * This is a context-dependent version of the above class.
+ */
+class CDInstMatchTrie
+{
+ public:
+ CDInstMatchTrie(context::Context* c) : d_valid(c, false) {}
+ ~CDInstMatchTrie();
+
+ /** exists inst match
+ *
+ * This method considers the entry given by m, starting at the given index.
+ * The domain of m is the bound variables of quantified formula q.
+ * It returns true if (the suffix) of m exists in this trie.
+ * If modEq is true, we check for duplication modulo equality the current
+ * equalities in the active equality engine of qe.
+ * It additionally takes a context c, for which the entry is valid in.
+ */
+ bool existsInstMatch(QuantifiersEngine* qe,
+ Node q,
+ InstMatch& m,
+ context::Context* c,
+ bool modEq = false,
+ unsigned index = 0)
+ {
+ return !addInstMatch(qe, q, m, c, modEq, index, true);
+ }
+ /** exists inst match, vector version */
+ bool existsInstMatch(QuantifiersEngine* qe,
+ Node q,
+ std::vector<Node>& m,
+ context::Context* c,
+ bool modEq = false,
+ unsigned index = 0)
+ {
+ return !addInstMatch(qe, q, m, c, modEq, index, true);
+ }
+ /** add inst match
+ *
+ * This method adds (the suffix of) m starting at the given index to this
+ * trie, and returns true if and only if m did not already occur in this trie.
+ * The domain of m is the bound variables of quantified formula q.
+ * If modEq is true, we check for duplication modulo equality the current
+ * equalities in the active equality engine of qe.
+ * It additionally takes a context c, for which the entry is valid in.
+ */
+ bool addInstMatch(QuantifiersEngine* qe,
+ Node q,
+ InstMatch& m,
+ context::Context* c,
+ bool modEq = false,
+ unsigned index = 0,
+ bool onlyExist = false)
+ {
+ return addInstMatch(qe, q, m.d_vals, c, modEq, index, onlyExist);
+ }
+ /** add inst match, vector version */
+ bool addInstMatch(QuantifiersEngine* qe,
+ Node q,
+ std::vector<Node>& m,
+ context::Context* c,
+ bool modEq = false,
+ unsigned index = 0,
+ bool onlyExist = false);
+ /** remove inst match
+ *
+ * This removes (the suffix of) m starting at the given index from this trie.
+ * It returns true if and only if this entry existed in this trie.
+ * The domain of m is the bound variables of quantified formula q.
+ */
+ bool removeInstMatch(Node q, std::vector<Node>& m, unsigned index = 0);
+ /** record instantiation lemma
+ *
+ * This records that the instantiation lemma lem corresponds to the entry
+ * given by (the suffix of) m starting at the given index.
+ */
+ bool recordInstLemma(Node q,
+ std::vector<Node>& m,
+ Node lem,
+ unsigned index = 0);
+
+ /** get instantiations
+ *
+ * This gets the set of instantiation lemmas that were recorded in this class
+ * via calls to recordInstLemma. If useActive is true, we only add
+ * instantiations that occur in active.
+ */
+ void getInstantiations(std::vector<Node>& insts,
+ Node q,
+ QuantifiersEngine* qe,
+ bool useActive,
+ std::vector<Node>& active)
+ {
+ std::vector<Node> terms;
+ getInstantiations(insts, q, terms, qe, useActive, active);
+ }
+ /** get explanation for inst lemmas
+ *
+ * This gets the explanation for the instantiation lemmas in lems for
+ * quantified formula q, for which this trie stores instantiation matches for.
+ * For each instantiation lemma lem recording in this trie via calls to
+ * recordInstLemma, we map lem to q in map quant, and lem to its corresponding
+ * vector of terms in tvec.
+ */
+ void getExplanationForInstLemmas(
+ Node q,
+ const std::vector<Node>& lems,
+ std::map<Node, Node>& quant,
+ std::map<Node, std::vector<Node> >& tvec) const
+ {
+ std::vector<Node> terms;
+ getExplanationForInstLemmas(q, terms, lems, quant, tvec);
+ }
+
+ /** print this class */
+ void print(std::ostream& out,
+ Node q,
+ bool& firstTime,
+ bool useActive,
+ std::vector<Node>& active) const
+ {
+ std::vector<TNode> terms;
+ print(out, q, terms, firstTime, useActive, active);
+ }
+
+ private:
+ /** the data */
+ std::map<Node, CDInstMatchTrie*> d_data;
+ /** is valid */
+ context::CDO<bool> d_valid;
+ /** helper for print
+ * terms accumulates the path we are on in the trie.
+ */
+ void print(std::ostream& out,
+ Node q,
+ std::vector<TNode>& terms,
+ bool& firstTime,
+ bool useActive,
+ std::vector<Node>& active) const;
+ /** helper for get instantiations
+ * terms accumulates the path we are on in the trie.
+ */
+ void getInstantiations(std::vector<Node>& insts,
+ Node q,
+ std::vector<Node>& terms,
+ QuantifiersEngine* qe,
+ bool useActive,
+ std::vector<Node>& active) const;
+ /** helper for get explanation for inst lemma
+ * terms accumulates the path we are on in the trie.
+ */
+ void getExplanationForInstLemmas(
+ Node q,
+ std::vector<Node>& terms,
+ const std::vector<Node>& lems,
+ std::map<Node, Node>& quant,
+ std::map<Node, std::vector<Node> >& tvec) const;
+ /** set instantiation lemma at this node in the trie */
+ void setInstLemma(Node n)
+ {
+ d_data.clear();
+ d_data[n] = NULL;
+ }
+ /** does this node of the trie store an instantiation lemma? */
+ bool hasInstLemma() const { return !d_data.empty(); }
+ /** get the instantiation lemma stored in this node of the trie */
+ Node getInstLemma() const { return d_data.begin()->first; }
+};
+
+/** inst match trie ordered
+ *
+ * This is an ordered version of the context-independent instantiation match
+ * trie. It stores a variable order and a base InstMatchTrie.
+ */
+class InstMatchTrieOrdered
+{
+ public:
+ InstMatchTrieOrdered(InstMatchTrie::ImtIndexOrder* imtio) : d_imtio(imtio) {}
+ ~InstMatchTrieOrdered() {}
+ /** get the ordering */
+ InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
+ /** get the trie data */
+ InstMatchTrie* getTrie() { return &d_imt; }
+ /** add match m for quantified formula q
+ *
+ * This method returns true if the match m was not previously added to this
+ * class. If modEq is true, we consider duplicates modulo the current
+ * equalities stored in the active equality engine of quantifiers engine.
+ */
+ bool addInstMatch(QuantifiersEngine* qe,
+ Node q,
+ InstMatch& m,
+ bool modEq = false)
+ {
+ return d_imt.addInstMatch(qe, q, m, modEq, d_imtio);
+ }
+ /** returns true if this trie contains m
+ *
+ * This method returns true if the match m exists in this
+ * class. If modEq is true, we consider duplicates modulo the current
+ * equalities stored in the active equality engine of quantifiers engine.
+ */
+ bool existsInstMatch(QuantifiersEngine* qe,
+ Node q,
+ InstMatch& m,
+ bool modEq = false)
+ {
+ return d_imt.existsInstMatch(qe, q, m, modEq, d_imtio);
+ }
+
+ private:
+ /** the ordering */
+ InstMatchTrie::ImtIndexOrder* d_imtio;
+ /** the data of this class */
+ InstMatchTrie d_imt;
+};
+
+} /* CVC4::theory::inst namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
#include <vector>
#include "theory/quantifiers/inst_propagator.h"
-#include "theory/rewriter.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/rewriter.h"
using namespace CVC4;
using namespace std;
for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){
if( !it->second.d_q.isNull() ){
if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
- if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){
+ if (!d_qe->getInstantiate()->removeInstantiation(
+ it->second.d_q, it->second.d_lem, it->second.d_terms))
+ {
Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
Assert( false );
}else{
#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
#include <iostream>
+#include <map>
#include <string>
#include <vector>
-#include <map>
#include "expr/node.h"
#include "expr/type_node.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
#include "theory/arith/theory_arith.h"
#include "theory/arith/theory_arith_private.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_epr.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){
d_cbqi_set_quant_inactive = true;
d_incomplete_check = true;
- d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
+ d_quantEngine->getInstantiate()->recordInstantiation(
+ d_curr_quant, subs, false, false);
return true;
}else{
//check if we need virtual term substitution (if used delta or infinity)
bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false );
- if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){
+ if (d_quantEngine->getInstantiate()->addInstantiation(
+ d_curr_quant, subs, false, false, used_vts))
+ {
++(d_quantEngine->d_statistics.d_instantiations_cbqi);
//d_added_inst.insert( d_curr_quant );
return true;
#include "theory/quantifiers/inst_strategy_enumerative.h"
#include "options/quantifiers_options.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
<< std::endl;
}
}
- if (d_quantEngine->addInstantiation(f, terms))
+ if (d_quantEngine->getInstantiate()->addInstantiation(f, terms))
{
Trace("inst-alg-rd") << "Success!" << std::endl;
++(d_quantEngine->d_statistics.d_instantiations_guess);
--- /dev/null
+/********************* */
+/*! \file instantiate.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of instantiate
+ **/
+
+#include "theory/quantifiers/instantiate.h"
+
+#include "options/quantifiers_options.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/inst_strategy_cbqi.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Instantiate::Instantiate(QuantifiersEngine* qe, context::UserContext* u)
+ : d_qe(qe),
+ d_term_db(nullptr),
+ d_term_util(nullptr),
+ d_total_inst_count_debug(0),
+ d_c_inst_match_trie_dom(u)
+{
+}
+
+Instantiate::~Instantiate()
+{
+ for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+ {
+ delete t.second;
+ }
+ d_c_inst_match_trie.clear();
+}
+
+bool Instantiate::reset(Theory::Effort e)
+{
+ if (!d_recorded_inst.empty())
+ {
+ Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size()
+ << " instantiations..." << std::endl;
+ // remove explicitly recorded instantiations
+ for (std::pair<Node, std::vector<Node> >& r : d_recorded_inst)
+ {
+ removeInstantiationInternal(r.first, r.second);
+ }
+ d_recorded_inst.clear();
+ }
+ d_term_db = d_qe->getTermDatabase();
+ d_term_util = d_qe->getTermUtil();
+ return true;
+}
+
+void Instantiate::registerQuantifier(Node q) {}
+bool Instantiate::checkComplete()
+{
+ if (!d_recorded_inst.empty())
+ {
+ Trace("quant-engine-debug")
+ << "Set incomplete due to recorded instantiations." << std::endl;
+ return false;
+ }
+ return true;
+}
+
+void Instantiate::addNotify(InstantiationNotify* in)
+{
+ d_inst_notify.push_back(in);
+}
+
+void Instantiate::notifyFlushLemmas()
+{
+ for (InstantiationNotify*& in : d_inst_notify)
+ {
+ in->filterInstantiations();
+ }
+}
+
+bool Instantiate::addInstantiation(
+ Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts)
+{
+ Assert(q[0].getNumChildren() == m.d_vals.size());
+ return addInstantiation(q, m.d_vals, mkRep, modEq, doVts);
+}
+
+bool Instantiate::addInstantiation(
+ Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts)
+{
+ // For resource-limiting (also does a time check).
+ d_qe->getOutputChannel().safePoint(options::quantifierStep());
+ Assert(!d_qe->inConflict());
+ Assert(terms.size() == q[0].getNumChildren());
+ Assert(d_term_db != nullptr);
+ Assert(d_term_util != nullptr);
+ Trace("inst-add-debug") << "For quantified formula " << q
+ << ", add instantiation: " << std::endl;
+ for (unsigned i = 0, size = terms.size(); i < size; i++)
+ {
+ Trace("inst-add-debug") << " " << q[0][i];
+ Trace("inst-add-debug2") << " -> " << terms[i];
+ TypeNode tn = q[0][i].getType();
+ if (terms[i].isNull())
+ {
+ terms[i] = getTermForType(tn);
+ }
+ if (mkRep)
+ {
+ // pick the best possible representative for instantiation, based on past
+ // use and simplicity of term
+ terms[i] = d_qe->getInternalRepresentative(terms[i], q, i);
+ }
+ else
+ {
+ // ensure the type is correct
+ terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn);
+ }
+ Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
+ if (terms[i].isNull())
+ {
+ Trace("inst-add-debug")
+ << " --> Failed to make term vector, due to term/type restrictions."
+ << std::endl;
+ return false;
+ }
+#ifdef CVC4_ASSERTIONS
+ bool bad_inst = false;
+ if (quantifiers::TermUtil::containsUninterpretedConstant(terms[i]))
+ {
+ Trace("inst") << "***& inst contains uninterpreted constant : "
+ << terms[i] << std::endl;
+ bad_inst = true;
+ }
+ else if (!terms[i].getType().isSubtypeOf(q[0][i].getType()))
+ {
+ Trace("inst") << "***& inst bad type : " << terms[i] << " "
+ << terms[i].getType() << "/" << q[0][i].getType()
+ << std::endl;
+ bad_inst = true;
+ }
+ else if (options::cbqi())
+ {
+ Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]);
+ if (!icf.isNull())
+ {
+ if (icf == q)
+ {
+ Trace("inst") << "***& inst contains inst constant attr : "
+ << terms[i] << std::endl;
+ bad_inst = true;
+ }
+ else if (quantifiers::TermUtil::containsTerms(
+ terms[i], d_term_util->d_inst_constants[q]))
+ {
+ Trace("inst") << "***& inst contains inst constants : " << terms[i]
+ << std::endl;
+ bad_inst = true;
+ }
+ }
+ }
+ // this assertion is critical to soundness
+ if (bad_inst)
+ {
+ Trace("inst") << "***& Bad Instantiate " << q << " with " << std::endl;
+ for (unsigned j = 0; j < terms.size(); j++)
+ {
+ Trace("inst") << " " << terms[j] << std::endl;
+ }
+ Assert(false);
+ }
+#endif
+ }
+
+ // Note we check for entailment before checking for term vector duplication.
+ // Although checking for term vector duplication is a faster check, it is
+ // included automatically with recordInstantiationInternal, hence we prefer
+ // two checks instead of three. In experiments, it is 1% slower or so to call
+ // existsInstantiation here.
+ // Alternatively, we could return an (index, trie node) in the call to
+ // existsInstantiation here, where this would return the node in the trie
+ // where we determined that there is definitely no duplication, and then
+ // continue from that point in recordInstantiation below. However, for
+ // simplicity, we do not pursue this option (as it would likely only
+ // lead to very small gains).
+
+ // check for positive entailment
+ if (options::instNoEntail())
+ {
+ // should check consistency of equality engine
+ // (if not aborting on utility's reset)
+ std::map<TNode, TNode> subs;
+ for (unsigned i = 0, size = terms.size(); i < size; i++)
+ {
+ subs[q[0][i]] = terms[i];
+ }
+ if (d_term_db->isEntailed(q[1], subs, false, true))
+ {
+ Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
+ ++(d_statistics.d_inst_duplicate_ent);
+ return false;
+ }
+ }
+
+ // check based on instantiation level
+ if (options::instMaxLevel() != -1 || options::lteRestrictInstClosure())
+ {
+ for (Node& t : terms)
+ {
+ if (!d_term_db->isTermEligibleForInstantiation(t, q, true))
+ {
+ return false;
+ }
+ }
+ }
+
+ // record the instantiation
+ bool recorded = recordInstantiationInternal(q, terms, modEq);
+ if (!recorded)
+ {
+ Trace("inst-add-debug") << " --> Already exists (no record)." << std::endl;
+ ++(d_statistics.d_inst_duplicate_eq);
+ return false;
+ }
+
+ // construct the instantiation
+ Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
+ Assert(d_term_util->d_vars[q].size() == terms.size());
+ // get the instantiation
+ Node body = getInstantiation(q, d_term_util->d_vars[q], terms, doVts);
+ Node orig_body = body;
+ if (options::cbqiNestedQE())
+ {
+ InstStrategyCbqi* icbqi = d_qe->getInstStrategyCbqi();
+ if (icbqi)
+ {
+ body = icbqi->doNestedQE(q, terms, body, doVts);
+ }
+ }
+ body = quantifiers::QuantifiersRewriter::preprocess(body, true);
+ Trace("inst-debug") << "...preprocess to " << body << std::endl;
+
+ // construct the lemma
+ Trace("inst-assert") << "(assert " << body << ")" << std::endl;
+
+ if (d_qe->usingModelEqualityEngine() && options::instNoModelTrue())
+ {
+ Node val_body = d_qe->getModel()->getValue(body);
+ if (val_body.isConst() && val_body.getConst<bool>())
+ {
+ Trace("inst-add-debug") << " --> True in model." << std::endl;
+ ++(d_statistics.d_inst_duplicate_model_true);
+ return false;
+ }
+ }
+
+ Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body);
+
+ // get relevancy conditions
+ if (options::instRelevantCond())
+ {
+ std::vector<Node> rlv_cond;
+ for (Node& t : terms)
+ {
+ quantifiers::TermUtil::getRelevancyCondition(t, rlv_cond);
+ }
+ if (!rlv_cond.empty())
+ {
+ rlv_cond.push_back(lem);
+ lem = NodeManager::currentNM()->mkNode(kind::OR, rlv_cond);
+ }
+ }
+
+ lem = Rewriter::rewrite(lem);
+
+ // check for lemma duplication
+ if (!d_qe->addLemma(lem, true, false))
+ {
+ Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
+ ++(d_statistics.d_inst_duplicate);
+ return false;
+ }
+
+ d_total_inst_debug[q]++;
+ d_temp_inst_debug[q]++;
+ d_total_inst_count_debug++;
+ if (Trace.isOn("inst"))
+ {
+ Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
+ for (unsigned i = 0, size = terms.size(); i < size; i++)
+ {
+ if (Trace.isOn("inst"))
+ {
+ Trace("inst") << " " << terms[i];
+ if (Trace.isOn("inst-debug"))
+ {
+ Trace("inst-debug") << ", type=" << terms[i].getType()
+ << ", var_type=" << q[0][i].getType();
+ }
+ Trace("inst") << std::endl;
+ }
+ }
+ }
+ if (options::instMaxLevel() != -1)
+ {
+ if (doVts)
+ {
+ // virtual term substitution/instantiation level features are
+ // incompatible
+ Assert(false);
+ }
+ else
+ {
+ uint64_t maxInstLevel = 0;
+ for (const Node& tc : terms)
+ {
+ if (tc.hasAttribute(InstLevelAttribute())
+ && tc.getAttribute(InstLevelAttribute()) > maxInstLevel)
+ {
+ maxInstLevel = tc.getAttribute(InstLevelAttribute());
+ }
+ }
+ QuantAttributes::setInstantiationLevelAttr(
+ orig_body, q[1], maxInstLevel + 1);
+ }
+ }
+ QuantifiersModule::QEffort elevel = d_qe->getCurrentQEffort();
+ if (elevel > QuantifiersModule::QEFFORT_CONFLICT
+ && elevel < QuantifiersModule::QEFFORT_NONE
+ && !d_inst_notify.empty())
+ {
+ // notify listeners
+ for (InstantiationNotify*& in : d_inst_notify)
+ {
+ if (!in->notifyInstantiation(elevel, q, lem, terms, body))
+ {
+ Trace("inst-add-debug") << "...we are in conflict." << std::endl;
+ d_qe->setConflict();
+ Assert(d_qe->getNumLemmasWaiting() > 0);
+ break;
+ }
+ }
+ }
+ if (options::trackInstLemmas())
+ {
+ bool recorded;
+ if (options::incrementalSolving())
+ {
+ recorded = d_c_inst_match_trie[q]->recordInstLemma(q, terms, lem);
+ }
+ else
+ {
+ recorded = d_inst_match_trie[q].recordInstLemma(q, terms, lem);
+ }
+ Trace("inst-add-debug") << "...was recorded : " << recorded << std::endl;
+ Assert(recorded);
+ }
+ Trace("inst-add-debug") << " --> Success." << std::endl;
+ ++(d_statistics.d_instantiations);
+ return true;
+}
+
+bool Instantiate::removeInstantiation(Node q,
+ Node lem,
+ std::vector<Node>& terms)
+{
+ // lem must occur in d_waiting_lemmas
+ if (d_qe->removeLemma(lem))
+ {
+ return removeInstantiationInternal(q, terms);
+ }
+ return false;
+}
+
+bool Instantiate::recordInstantiation(Node q,
+ std::vector<Node>& terms,
+ bool modEq,
+ bool addedLem)
+{
+ return recordInstantiationInternal(q, terms, modEq, addedLem);
+}
+
+bool Instantiate::existsInstantiation(Node q,
+ std::vector<Node>& terms,
+ bool modEq)
+{
+ if (options::incrementalSolving())
+ {
+ std::map<Node, inst::CDInstMatchTrie*>::iterator it =
+ d_c_inst_match_trie.find(q);
+ if (it != d_c_inst_match_trie.end())
+ {
+ return it->second->existsInstMatch(
+ d_qe, q, terms, d_qe->getUserContext(), modEq);
+ }
+ }
+ else
+ {
+ std::map<Node, inst::InstMatchTrie>::iterator it =
+ d_inst_match_trie.find(q);
+ if (it != d_inst_match_trie.end())
+ {
+ return it->second.existsInstMatch(d_qe, q, terms, modEq);
+ }
+ }
+ return false;
+}
+
+Node Instantiate::getInstantiation(Node q,
+ std::vector<Node>& vars,
+ std::vector<Node>& terms,
+ bool doVts)
+{
+ Node body;
+ Assert(vars.size() == terms.size());
+ Assert(q[0].getNumChildren() == vars.size());
+ // TODO (#1386) : optimize this
+ body = q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end());
+ if (doVts)
+ {
+ // do virtual term substitution
+ body = Rewriter::rewrite(body);
+ Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
+ Node body_r = d_term_util->rewriteVtsSymbols(body);
+ Trace("quant-vts-debug") << " ...result: " << body_r
+ << std::endl;
+ body = body_r;
+ }
+ return body;
+}
+
+Node Instantiate::getInstantiation(Node q, InstMatch& m, bool doVts)
+{
+ Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end());
+ Assert(m.d_vals.size() == q[0].getNumChildren());
+ return getInstantiation(q, d_term_util->d_vars[q], m.d_vals, doVts);
+}
+
+Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts)
+{
+ Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end());
+ return getInstantiation(q, d_term_util->d_vars[q], terms, doVts);
+}
+
+bool Instantiate::recordInstantiationInternal(Node q,
+ std::vector<Node>& terms,
+ bool modEq,
+ bool addedLem)
+{
+ if (!addedLem)
+ {
+ // record the instantiation for deletion later
+ d_recorded_inst.push_back(std::pair<Node, std::vector<Node> >(q, terms));
+ }
+ if (options::incrementalSolving())
+ {
+ Trace("inst-add-debug")
+ << "Adding into context-dependent inst trie, modEq = " << modEq
+ << std::endl;
+ inst::CDInstMatchTrie* imt;
+ std::map<Node, inst::CDInstMatchTrie*>::iterator it =
+ d_c_inst_match_trie.find(q);
+ if (it != d_c_inst_match_trie.end())
+ {
+ imt = it->second;
+ }
+ else
+ {
+ imt = new inst::CDInstMatchTrie(d_qe->getUserContext());
+ d_c_inst_match_trie[q] = imt;
+ }
+ d_c_inst_match_trie_dom.insert(q);
+ return imt->addInstMatch(d_qe, q, terms, d_qe->getUserContext(), modEq);
+ }
+ Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+ return d_inst_match_trie[q].addInstMatch(d_qe, q, terms, modEq);
+}
+
+bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)
+{
+ if (options::incrementalSolving())
+ {
+ std::map<Node, inst::CDInstMatchTrie*>::iterator it =
+ d_c_inst_match_trie.find(q);
+ if (it != d_c_inst_match_trie.end())
+ {
+ return it->second->removeInstMatch(q, terms);
+ }
+ return false;
+ }
+ return d_inst_match_trie[q].removeInstMatch(q, terms);
+}
+
+Node Instantiate::getTermForType(TypeNode tn)
+{
+ if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn))
+ {
+ return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
+ }
+ return d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn);
+}
+
+bool Instantiate::printInstantiations(std::ostream& out)
+{
+ bool useUnsatCore = false;
+ std::vector<Node> active_lemmas;
+ if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas))
+ {
+ useUnsatCore = true;
+ }
+ bool printed = false;
+ if (options::incrementalSolving())
+ {
+ for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+ {
+ bool firstTime = true;
+ t.second->print(out, t.first, firstTime, useUnsatCore, active_lemmas);
+ if (!firstTime)
+ {
+ out << ")" << std::endl;
+ }
+ printed = printed || !firstTime;
+ }
+ }
+ else
+ {
+ for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+ {
+ bool firstTime = true;
+ t.second.print(out, t.first, firstTime, useUnsatCore, active_lemmas);
+ if (!firstTime)
+ {
+ out << ")" << std::endl;
+ }
+ printed = printed || !firstTime;
+ }
+ }
+ return printed;
+}
+
+void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
+{
+ if (options::incrementalSolving())
+ {
+ for (context::CDHashSet<Node, NodeHashFunction>::const_iterator it =
+ d_c_inst_match_trie_dom.begin();
+ it != d_c_inst_match_trie_dom.end();
+ ++it)
+ {
+ qs.push_back(*it);
+ }
+ }
+ else
+ {
+ for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+ {
+ qs.push_back(t.first);
+ }
+ }
+}
+
+bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas)
+{
+ // only if unsat core available
+ if (options::proof())
+ {
+ if (!ProofManager::currentPM()->unsatCoreAvailable())
+ {
+ return false;
+ }
+ }
+
+ Trace("inst-unsat-core") << "Get instantiations in unsat core..."
+ << std::endl;
+ ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS,
+ active_lemmas);
+ if (Trace.isOn("inst-unsat-core"))
+ {
+ Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: "
+ << std::endl;
+ for (const Node& lem : active_lemmas)
+ {
+ Trace("inst-unsat-core") << " " << lem << std::endl;
+ }
+ Trace("inst-unsat-core") << std::endl;
+ }
+ return true;
+}
+
+bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
+ std::map<Node, Node>& weak_imp)
+{
+ if (getUnsatCoreLemmas(active_lemmas))
+ {
+ for (unsigned i = 0, size = active_lemmas.size(); i < size; ++i)
+ {
+ Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore(
+ active_lemmas[i]);
+ if (n != active_lemmas[i])
+ {
+ Trace("inst-unsat-core") << " weaken : " << active_lemmas[i] << " -> "
+ << n << std::endl;
+ }
+ weak_imp[active_lemmas[i]] = n;
+ }
+ return true;
+ }
+ return false;
+}
+
+void Instantiate::getInstantiationTermVectors(
+ Node q, std::vector<std::vector<Node> >& tvecs)
+{
+ std::vector<Node> lemmas;
+ getInstantiations(q, lemmas);
+ std::map<Node, Node> quant;
+ std::map<Node, std::vector<Node> > tvec;
+ getExplanationForInstLemmas(lemmas, quant, tvec);
+ for (std::pair<const Node, std::vector<Node> >& t : tvec)
+ {
+ tvecs.push_back(t.second);
+ }
+}
+
+void Instantiate::getInstantiationTermVectors(
+ std::map<Node, std::vector<std::vector<Node> > >& insts)
+{
+ if (options::incrementalSolving())
+ {
+ for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+ {
+ getInstantiationTermVectors(t.first, insts[t.first]);
+ }
+ }
+ else
+ {
+ for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+ {
+ getInstantiationTermVectors(t.first, insts[t.first]);
+ }
+ }
+}
+
+void Instantiate::getExplanationForInstLemmas(
+ const std::vector<Node>& lems,
+ std::map<Node, Node>& quant,
+ std::map<Node, std::vector<Node> >& tvec)
+{
+ if (options::trackInstLemmas())
+ {
+ if (options::incrementalSolving())
+ {
+ for (std::pair<const Node, inst::CDInstMatchTrie*>& t :
+ d_c_inst_match_trie)
+ {
+ t.second->getExplanationForInstLemmas(t.first, lems, quant, tvec);
+ }
+ }
+ else
+ {
+ for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+ {
+ t.second.getExplanationForInstLemmas(t.first, lems, quant, tvec);
+ }
+ }
+#ifdef CVC4_ASSERTIONS
+ for (unsigned j = 0; j < lems.size(); j++)
+ {
+ Assert(quant.find(lems[j]) != quant.end());
+ Assert(tvec.find(lems[j]) != tvec.end());
+ }
+#endif
+ }
+ Assert(false);
+}
+
+void Instantiate::getInstantiations(std::map<Node, std::vector<Node> >& insts)
+{
+ bool useUnsatCore = false;
+ std::vector<Node> active_lemmas;
+ if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas))
+ {
+ useUnsatCore = true;
+ }
+
+ if (options::incrementalSolving())
+ {
+ for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+ {
+ t.second->getInstantiations(
+ insts[t.first], t.first, d_qe, useUnsatCore, active_lemmas);
+ }
+ }
+ else
+ {
+ for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+ {
+ t.second.getInstantiations(
+ insts[t.first], t.first, d_qe, useUnsatCore, active_lemmas);
+ }
+ }
+}
+
+void Instantiate::getInstantiations(Node q, std::vector<Node>& insts)
+{
+ if (options::incrementalSolving())
+ {
+ std::map<Node, inst::CDInstMatchTrie*>::iterator it =
+ d_c_inst_match_trie.find(q);
+ if (it != d_c_inst_match_trie.end())
+ {
+ std::vector<Node> active_lemmas;
+ it->second->getInstantiations(
+ insts, it->first, d_qe, false, active_lemmas);
+ }
+ }
+ else
+ {
+ std::map<Node, inst::InstMatchTrie>::iterator it =
+ d_inst_match_trie.find(q);
+ if (it != d_inst_match_trie.end())
+ {
+ std::vector<Node> active_lemmas;
+ it->second.getInstantiations(
+ insts, it->first, d_qe, false, active_lemmas);
+ }
+ }
+}
+
+Node Instantiate::getInstantiatedConjunction(Node q)
+{
+ Assert(q.getKind() == FORALL);
+ std::vector<Node> insts;
+ getInstantiations(q, insts);
+ if (insts.empty())
+ {
+ return NodeManager::currentNM()->mkConst(true);
+ }
+ Node ret;
+ if (insts.size() == 1)
+ {
+ ret = insts[0];
+ }
+ else
+ {
+ ret = NodeManager::currentNM()->mkNode(kind::AND, insts);
+ }
+ // have to remove q
+ // may want to do this in a better way
+ TNode tq = q;
+ TNode tt = NodeManager::currentNM()->mkConst(true);
+ ret = ret.substitute(tq, tt);
+ return ret;
+}
+
+void Instantiate::debugPrint()
+{
+ // debug information
+ if (Trace.isOn("inst-per-quant-round"))
+ {
+ for (std::pair<const Node, int>& i : d_temp_inst_debug)
+ {
+ Trace("inst-per-quant-round") << " * " << i.second << " for " << i.first
+ << std::endl;
+ d_temp_inst_debug[i.first] = 0;
+ }
+ }
+}
+
+void Instantiate::debugPrintModel()
+{
+ if (Trace.isOn("inst-per-quant"))
+ {
+ for (std::pair<const Node, int>& i : d_total_inst_debug)
+ {
+ Trace("inst-per-quant") << " * " << i.second << " for " << i.first
+ << std::endl;
+ }
+ }
+}
+
+Instantiate::Statistics::Statistics()
+ : d_instantiations("Instantiate::Instantiations_Total", 0),
+ d_inst_duplicate("Instantiate::Duplicate_Inst", 0),
+ d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0),
+ d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0),
+ d_inst_duplicate_model_true("Instantiate::Duplicate_Inst_Model_True", 0)
+{
+ smtStatisticsRegistry()->registerStat(&d_instantiations);
+ smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
+ smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
+ smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
+ smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true);
+}
+
+Instantiate::Statistics::~Statistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_instantiations);
+ smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
+ smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
+ smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
+ smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true);
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file instantiate.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief instantiate
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "theory/quantifiers/inst_match_trie.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers_engine.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermDb;
+class TermUtil;
+
+/** instantiation notify
+ *
+ * This class is a listener for all instantiations generated with quantifiers.
+ * By default, no notify classes are used. For an example of an instantiation
+ * notify class, see quantifiers/inst_propagate.h, which has a notify class
+ * that recognizes when the set of enqueued instantiations form a conflict.
+ */
+class InstantiationNotify
+{
+ public:
+ InstantiationNotify() {}
+ virtual ~InstantiationNotify() {}
+ /** notify instantiation
+ *
+ * This is called when an instantiation of quantified formula q is
+ * instantiated by a substitution whose range is terms at quantifier effort
+ * quant_e. Furthermore:
+ * body is the substituted, preprocessed body of the quantified formula,
+ * lem is the instantiation lemma ( ~q V body ) after rewriting.
+ */
+ virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
+ Node q,
+ Node lem,
+ std::vector<Node>& terms,
+ Node body) = 0;
+ /** filter instantiations
+ *
+ * This is called just before the quantifiers engine flushes its lemmas to the
+ * output channel. During this call, the instantiation notify object may
+ * call, e.g. QuantifiersEngine::getInstantiate()->removeInstantiation
+ * to remove instantiations that should not be sent on the output channel.
+ */
+ virtual void filterInstantiations() = 0;
+};
+
+/** Instantiate
+ *
+ * This class is used for generating instantiation lemmas. It maintains an
+ * instantiation trie, which is represented by a different data structure
+ * depending on whether incremental solving is enabled (see d_inst_match_trie
+ * and d_c_inst_match_trie).
+ *
+ * Below, we say an instantiation lemma for q = forall x. F under substitution
+ * { x -> t } is the formula:
+ * ( ~forall x. F V F * { x -> t } )
+ * where * is application of substitution.
+ *
+ * Its main interface is ::addInstantiation(...), which is called by many of
+ * the quantifiers modules, which enqueues instantiation lemmas in quantifiers
+ * engine via calls to QuantifiersEngine::addLemma.
+ *
+ * It also has utilities for constructing instantiations, and interfaces for
+ * getting the results of the instantiations produced during check-sat calls.
+ */
+class Instantiate : public QuantifiersUtil
+{
+ public:
+ Instantiate(QuantifiersEngine* qe, context::UserContext* u);
+ ~Instantiate();
+
+ /** reset */
+ virtual bool reset(Theory::Effort e) override;
+ /** register quantifier */
+ virtual void registerQuantifier(Node q) override;
+ /** identify */
+ virtual std::string identify() const override { return "Instantiate"; }
+ /** check incomplete */
+ virtual bool checkComplete() override;
+
+ //--------------------------------------notify objects
+ /** add instantiation notify
+ *
+ * Adds an instantiation notify class to listen to the instantiations reported
+ * to this class.
+ */
+ void addNotify(InstantiationNotify* in);
+ /** get number of instantiation notify added to this class */
+ bool hasNotify() const { return !d_inst_notify.empty(); }
+ /** notify flush lemmas
+ *
+ * This is called just before the quantifiers engine flushes its lemmas to
+ * the output channel.
+ */
+ void notifyFlushLemmas();
+ //--------------------------------------end notify objects
+
+ /** do instantiation specified by m
+ *
+ * This function returns true if the instantiation lemma for quantified
+ * formula q for the substitution specified by m is successfully enqueued
+ * via a call to QuantifiersEngine::addLemma.
+ * mkRep : whether to take the representatives of the terms in the range of
+ * the substitution m,
+ * modEq : whether to check for duplication modulo equality in instantiation
+ * tries (for performance),
+ * doVts : whether we must apply virtual term substitution to the
+ * instantiation lemma.
+ *
+ * This call may fail if it can be determined that the instantiation is not
+ * relevant or legal in the current context. This happens if:
+ * (1) The substitution is not well-typed,
+ * (2) The substitution involves terms whose instantiation level is above the
+ * allowed limit,
+ * (3) The resulting instantiation is entailed in the current context using a
+ * fast entailment check (see TermDb::isEntailed),
+ * (4) The range of the substitution is a duplicate of that of a previously
+ * added instantiation,
+ * (5) The instantiation lemma is a duplicate of previously added lemma.
+ *
+ */
+ bool addInstantiation(Node q,
+ InstMatch& m,
+ bool mkRep = false,
+ bool modEq = false,
+ bool doVts = false);
+ /** add instantiation
+ *
+ * Same as above, but the substitution we are considering maps the variables
+ * of q to the vector terms, in order.
+ */
+ bool addInstantiation(Node q,
+ std::vector<Node>& terms,
+ bool mkRep = false,
+ bool modEq = false,
+ bool doVts = false);
+ /** remove pending instantiation
+ *
+ * Removes the instantiation lemma lem from the instantiation trie.
+ */
+ bool removeInstantiation(Node q, Node lem, std::vector<Node>& terms);
+ /** record instantiation
+ *
+ * Explicitly record that q has been instantiated with terms. This is the
+ * same as addInstantiation, but does not enqueue an instantiation lemma.
+ */
+ bool recordInstantiation(Node q,
+ std::vector<Node>& terms,
+ bool modEq = false,
+ bool addedLem = true);
+ /** exists instantiation
+ *
+ * Returns true if and only if the instantiation already was added or
+ * recorded by this class.
+ * modEq : whether to check for duplication modulo equality
+ */
+ bool existsInstantiation(Node q,
+ std::vector<Node>& terms,
+ bool modEq = false);
+ //--------------------------------------general utilities
+ /** get instantiation
+ *
+ * Returns the instantiation lemma for q under substitution { vars -> terms }.
+ * doVts is whether to apply virtual term substitution to its body.
+ */
+ Node getInstantiation(Node q,
+ std::vector<Node>& vars,
+ std::vector<Node>& terms,
+ bool doVts = false);
+ /** get instantiation
+ *
+ * Same as above, but with vars/terms specified by InstMatch m.
+ */
+ Node getInstantiation(Node q, InstMatch& m, bool doVts = false);
+ /** get instantiation
+ *
+ * Same as above but with vars equal to the bound variables of q.
+ */
+ Node getInstantiation(Node q, std::vector<Node>& terms, bool doVts = false);
+ /** get term for type
+ *
+ * This returns an arbitrary term for type tn.
+ * This term is chosen heuristically to be the best
+ * term for instantiation. Currently, this
+ * heuristic enumerates the first term of the
+ * type if the type is closed enumerable, otherwise
+ * an existing ground term from the term database if
+ * one exists, or otherwise a fresh variable.
+ */
+ Node getTermForType(TypeNode tn);
+ //--------------------------------------end general utilities
+
+ /** debug print, called once per instantiation round. */
+ void debugPrint();
+ /** debug print model, called once, before we terminate with sat/unknown. */
+ void debugPrintModel();
+
+ //--------------------------------------user-level interface utilities
+ /** print instantiations
+ *
+ * Print all instantiations for all quantified formulas on out,
+ * returns true if at least one instantiation was printed.
+ */
+ bool printInstantiations(std::ostream& out);
+ /** get instantiated quantified formulas
+ *
+ * Get the list of quantified formulas that were instantiated in the current
+ * user context, store them in qs.
+ */
+ void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
+ /** get instantiations
+ *
+ * Get the body of all instantiation lemmas added in the current user context
+ * for quantified formula q, store them in insts.
+ */
+ void getInstantiations(Node q, std::vector<Node>& insts);
+ /** get instantiations
+ *
+ * Get the body of all instantiation lemmas added in the current user context
+ * for all quantified formulas stored in the domain of insts, store them in
+ * the range of insts.
+ */
+ void getInstantiations(std::map<Node, std::vector<Node> >& insts);
+ /** get instantiation term vectors
+ *
+ * Get term vectors corresponding to for all instantiations lemmas added in
+ * the current user context for quantified formula q, store them in tvecs.
+ */
+ void getInstantiationTermVectors(Node q,
+ std::vector<std::vector<Node> >& tvecs);
+ /** get instantiation term vectors
+ *
+ * Get term vectors for all instantiations lemmas added in the current user
+ * context for quantified formula q, store them in tvecs.
+ */
+ void getInstantiationTermVectors(
+ std::map<Node, std::vector<std::vector<Node> > >& insts);
+ /** get instantiated conjunction
+ *
+ * This gets a conjunction of the bodies of instantiation lemmas added in the
+ * current user context for quantified formula q. For example, if we added:
+ * ~forall x. P( x ) V P( a )
+ * ~forall x. P( x ) V P( b )
+ * Then, this method returns P( a ) ^ P( b ).
+ */
+ Node getInstantiatedConjunction(Node q);
+ /** get unsat core lemmas
+ *
+ * If this method returns true, then it appends to active_lemmas all lemmas
+ * that are in the unsat core that originated from the theory of quantifiers.
+ * This method returns false if the unsat core is not available.
+ */
+ bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
+ /** get unsat core lemmas
+ *
+ * If this method returns true, then it appends to active_lemmas all lemmas
+ * that are in the unsat core that originated from the theory of quantifiers.
+ * This method returns false if the unsat core is not available.
+ *
+ * It also computes a weak implicant for each of these lemmas. For each lemma
+ * L in active_lemmas, this is a formula L' such that:
+ * L => L'
+ * and replacing L by L' in the unsat core results in a set that is still
+ * unsatisfiable. The map weak_imp stores this formula for each formula in
+ * active_lemmas.
+ */
+ bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
+ std::map<Node, Node>& weak_imp);
+ /** get explanation for instantiation lemmas
+ *
+ *
+ */
+ void getExplanationForInstLemmas(const std::vector<Node>& lems,
+ std::map<Node, Node>& quant,
+ std::map<Node, std::vector<Node> >& tvec);
+ //--------------------------------------end user-level interface utilities
+
+ /** statistics class
+ *
+ * This tracks statistics on the number of instantiations successfully
+ * enqueued on the quantifiers output channel, and the number of redundant
+ * instantiations encountered by various criteria.
+ */
+ class Statistics
+ {
+ public:
+ IntStat d_instantiations;
+ IntStat d_inst_duplicate;
+ IntStat d_inst_duplicate_eq;
+ IntStat d_inst_duplicate_ent;
+ IntStat d_inst_duplicate_model_true;
+ Statistics();
+ ~Statistics();
+ }; /* class Instantiate::Statistics */
+ Statistics d_statistics;
+
+ private:
+ /** record instantiation, return true if it was not a duplicate
+ *
+ * addedLem : whether an instantiation lemma was added for the vector we are
+ * recording. If this is false, we bookkeep the vector.
+ * modEq : whether to check for duplication modulo equality in instantiation
+ * tries (for performance),
+ */
+ bool recordInstantiationInternal(Node q,
+ std::vector<Node>& terms,
+ bool modEq = false,
+ bool addedLem = true);
+ /** remove instantiation from the cache */
+ bool removeInstantiationInternal(Node q, std::vector<Node>& terms);
+
+ /** pointer to the quantifiers engine */
+ QuantifiersEngine* d_qe;
+ /** cache of term database for quantifiers engine */
+ TermDb* d_term_db;
+ /** cache of term util for quantifiers engine */
+ TermUtil* d_term_util;
+ /** instantiation notify classes */
+ std::vector<InstantiationNotify*> d_inst_notify;
+
+ /** statistics for debugging total instantiation */
+ int d_total_inst_count_debug;
+ /** statistics for debugging total instantiations per quantifier */
+ std::map<Node, int> d_total_inst_debug;
+ /** statistics for debugging total instantiations per quantifier per round */
+ std::map<Node, int> d_temp_inst_debug;
+
+ /** list of all instantiations produced for each quantifier
+ *
+ * We store context (dependent, independent) versions. If incremental solving
+ * is disabled, we use d_inst_match_trie for performance reasons.
+ */
+ std::map<Node, inst::InstMatchTrie> d_inst_match_trie;
+ std::map<Node, inst::CDInstMatchTrie*> d_c_inst_match_trie;
+ /**
+ * The list of quantified formulas for which the domain of d_c_inst_match_trie
+ * is valid.
+ */
+ context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom;
+
+ /** explicitly recorded instantiations
+ *
+ * Sometimes an instantiation is recorded internally but not sent out as a
+ * lemma, for instance, for partial quantifier elimination. This is a map
+ * of these instantiations, for each quantified formula.
+ */
+ std::vector<std::pair<Node, std::vector<Node> > > d_recorded_inst;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */
#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/model_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
{
terms.push_back( riter.getCurrentTerm( k ) );
}
- Node n = d_qe->getInstantiation( f, vars, terms );
+ Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms);
Node val = fm->getValue( n );
if (val != d_qe->getTermUtil()->d_true)
{
//try to add it
Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
//add model basis instantiation
- if( d_qe->addInstantiation( fp, d_quant_basis_match[f] ) ){
+ if (d_qe->getInstantiate()->addInstantiation(fp, d_quant_basis_match[f]))
+ {
d_quant_basis_match_added[f] = true;
return 1;
}else{
Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
fmig->resetEvaluate();
Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
+ EqualityQuery* qy = d_qe->getEqualityQuery();
+ Instantiate* inst = d_qe->getInstantiate();
+ TermUtil* util = d_qe->getTermUtil();
while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
d_triedLemmas++;
if( Debug.isOn("inst-fmf-ei-debug") ){
//if evaluate(...)==1, then the instantiation is already true in the model
// depIndex is the index of the least significant variable that this evaluation relies upon
depIndex = riter.getNumTerms()-1;
- Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermUtil()->getInstConstantBody( f ) << std::endl;
- eval = fmig->evaluate( d_qe->getTermUtil()->getInstConstantBody( f ), depIndex, &riter );
+ Debug("fmf-model-eval") << "We will evaluate "
+ << util->getInstConstantBody(f) << std::endl;
+ eval = fmig->evaluate(util->getInstConstantBody(f), depIndex, &riter);
if( eval==1 ){
Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
}else{
InstMatch m( f );
for (unsigned i = 0; i < riter.getNumTerms(); i++)
{
- m.set( d_qe, i, riter.getCurrentTerm( i ) );
+ m.set(qy, i, riter.getCurrentTerm(i));
}
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
//add as instantiation
- if( d_qe->addInstantiation( f, m, true ) ){
+ if (inst->addInstantiation(f, m, true))
+ {
d_addedLemmas++;
if( d_qe->inConflict() ){
break;
#include "theory/quantifiers/ambqi_builder.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
if( !riter.isIncomplete() ){
int triedLemmas = 0;
int addedLemmas = 0;
+ EqualityQuery* qy = d_quantEngine->getEqualityQuery();
+ Instantiate* inst = d_quantEngine->getInstantiate();
while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
//instantiation was not shown to be true, construct the match
InstMatch m( f );
for (unsigned i = 0; i < riter.getNumTerms(); i++)
{
- m.set( d_quantEngine, i, riter.getCurrentTerm( i ) );
+ m.set(qy, i, riter.getCurrentTerm(i));
}
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
triedLemmas++;
//add as instantiation
- if( d_quantEngine->addInstantiation( f, m, true ) ){
+ if (inst->addInstantiation(f, m, true))
+ {
addedLemmas++;
if( d_quantEngine->inConflict() ){
break;
#include "options/quantifiers_options.h"
#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
-#include "theory/quantifiers/first_order_model.h"
#include "theory/theory_engine.h"
using namespace CVC4::kind;
return true;
}
}else{
- Node inst = p->d_quantEngine->getInstantiation( d_q, terms );
+ Node inst =
+ p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms);
Node inst_eval = p->getTermDatabase()->evaluateTerm( inst, NULL, options::qcfTConstraint() );
if( Trace.isOn("qcf-instance-check") ){
Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
if( !tcs ){
//for debugging
if( Debug.isOn("qcf-check-inst") ){
- Node inst = d_quantEngine->getInstantiation( q, terms );
+ Node inst = d_quantEngine->getInstantiate()
+ ->getInstantiation(q, terms);
Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
Assert( !getTermDatabase()->isEntailed( inst, true ) );
Assert(getTermDatabase()->isEntailed(inst, false) ||
e > EFFORT_CONFLICT);
}
- if( d_quantEngine->addInstantiation( q, terms ) ){
+ if (d_quantEngine->getInstantiate()->addInstantiation(
+ q, terms))
+ {
Trace("qcf-check") << " ... Added instantiation" << std::endl;
Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
qi->debugPrintMatch("qcf-inst");
/* reset
* Called at the beginning of an instantiation round
* Returns false if the reset failed. When reset fails, the utility should have
- * added a lemma
- * via a call to qe->addLemma. TODO: improve this contract #1163
+ * added a lemma via a call to qe->addLemma. TODO: improve this contract #1163
*/
virtual bool reset( Theory::Effort e ) = 0;
/* Called for new quantifiers */
virtual void registerQuantifier(Node q) = 0;
/** Identify this module (for debugging, dynamic configuration, etc..) */
virtual std::string identify() const = 0;
+ /** Check complete?
+ *
+ * Returns false if the utility's reasoning was globally incomplete
+ * (e.g. "sat" must be replaced with "incomplete").
+ */
+ virtual bool checkComplete() { return true; }
};
/** Arithmetic utilities regarding monomial sums.
}
}
+void QuantAttributes::setInstantiationLevelAttr(Node n, Node qn, uint64_t level)
+{
+ Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level
+ << std::endl;
+ // if not from the vector of terms we instantiatied
+ if (qn.getKind() != BOUND_VARIABLE && n != qn)
+ {
+ // if this is a new term, without an instantiation level
+ if (!n.hasAttribute(InstLevelAttribute()))
+ {
+ InstLevelAttribute ila;
+ n.setAttribute(ila, level);
+ Trace("inst-level-debug") << "Set instantiation level " << n << " to "
+ << level << std::endl;
+ Assert(n.getNumChildren() == qn.getNumChildren());
+ for (unsigned i = 0; i < n.getNumChildren(); i++)
+ {
+ setInstantiationLevelAttr(n[i], qn[i], level);
+ }
+ }
+ }
+}
+
+void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level)
+{
+ if (!n.hasAttribute(InstLevelAttribute()))
+ {
+ InstLevelAttribute ila;
+ n.setAttribute(ila, level);
+ Trace("inst-level-debug") << "Set instantiation level " << n << " to "
+ << level << std::endl;
+ for (unsigned i = 0; i < n.getNumChildren(); i++)
+ {
+ setInstantiationLevelAttr(n[i], level);
+ }
+ }
+}
+
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
struct SynthesisAttributeId {};
typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
+struct InstLevelAttributeId
+{
+};
+typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
+
/** Attribute for setting printing information for sygus variables
*
* For variable d of sygus datatype type, if
/** get quant id num */
Node getQuantIdNumNode( Node q );
-private:
+ /** set instantiation level attr */
+ static void setInstantiationLevelAttr(Node n, uint64_t level);
+ /** set instantiation level attr */
+ static void setInstantiationLevelAttr(Node n, Node qn, uint64_t level);
+
+ private:
/** pointer to quantifiers engine */
QuantifiersEngine * d_quantEngine;
/** cache of attributes */
#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/inst_match_generator.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
if( inst.size()>f[0].getNumChildren() ){
inst.resize( f[0].getNumChildren() );
}
- if( d_quantEngine->addInstantiation( f, inst ) ){
+ if (d_quantEngine->getInstantiate()->addInstantiation(f, inst))
+ {
addedLemmas++;
tempAddedLemmas++;
/*
#include "theory/quantifiers/skolemize.h"
#include "options/quantifiers_options.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/sort_inference.h"
// if it has an instantiation level, set the skolemized body to that level
if (f.hasAttribute(InstLevelAttribute()))
{
- theory::QuantifiersEngine::setInstantiationLevelAttr(
+ QuantAttributes::setInstantiationLevelAttr(
ret, f.getAttribute(InstLevelAttribute()));
}
<< std::endl;
if (options::instMaxLevel() != -1)
{
- QuantifiersEngine::setInstantiationLevelAttr(k, 0);
+ QuantAttributes::setInstantiationLevelAttr(k, 0);
}
d_type_fv[tn] = k;
return k;
struct BoundVarAttributeId {};
typedef expr::Attribute<BoundVarAttributeId, Node> BoundVarAttribute;
-struct InstLevelAttributeId {};
-typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
-
struct InstVarNumAttributeId {};
typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
namespace quantifiers {
class TermDatabase;
+class Instantiate;
// TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used.
class TermUtil : public QuantifiersUtil
{
// TODO : remove these
friend class ::CVC4::theory::QuantifiersEngine;
-private:
+ friend class Instantiate;
+
+ private:
/** reference to the quantifiers engine */
QuantifiersEngine* d_quantEngine;
public:
#include "theory/quantifiers/candidate_generator.h"
#include "theory/quantifiers/ho_trigger.h"
#include "theory/quantifiers/inst_match_generator.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
bool Trigger::sendInstantiation(InstMatch& m)
{
- return d_quantEngine->addInstantiation(d_f, m);
+ return d_quantEngine->getInstantiate()->addInstantiation(d_f, m);
}
bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) {
#include "theory/quantifiers/inst_strategy_cbqi.h"
#include "theory/quantifiers/inst_strategy_e_matching.h"
#include "theory/quantifiers/inst_strategy_enumerative.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/instantiation_engine.h"
#include "theory/quantifiers/local_theory_ext.h"
#include "theory/quantifiers/model_engine.h"
TheoryEngine* te)
: d_te(te),
d_quant_attr(new quantifiers::QuantAttributes(this)),
+ d_instantiate(new quantifiers::Instantiate(this, u)),
d_skolemize(new quantifiers::Skolemize(this, u)),
d_term_enum(new quantifiers::TermEnumeration),
d_conflict_c(c, false),
// notice that this option is incompatible with options::qcfAllConflict()
d_inst_prop = new quantifiers::InstPropagator( this );
d_util.push_back( d_inst_prop );
- d_inst_notify.push_back( d_inst_prop->getInstantiationNotify() );
+ d_instantiate->addNotify(d_inst_prop->getInstantiationNotify());
}else{
d_inst_prop = NULL;
}
d_eq_inference = NULL;
}
+ d_util.push_back(d_instantiate.get());
+
d_tr_trie = new inst::TriggerTrie;
d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
d_conflict = false;
d_bv_invert = NULL;
d_builder = NULL;
- d_total_inst_count_debug = 0;
//allow theory combination to go first, once initially
d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
d_ierCounter_c = d_ierCounter;
}
QuantifiersEngine::~QuantifiersEngine(){
- for(std::map< Node, inst::CDInstMatchTrie* >::iterator
- i = d_c_inst_match_trie.begin(), iend = d_c_inst_match_trie.end();
- i != iend; ++i)
- {
- delete (*i).second;
- }
- d_c_inst_match_trie.clear();
-
delete d_alpha_equiv;
delete d_builder;
delete d_qepr;
d_qepr != NULL) {
for (unsigned i = 0; i < assertions.size(); i++) {
if (options::instLevelInputOnly() && options::instMaxLevel() != -1) {
- setInstantiationLevelAttr(assertions[i], 0);
+ quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions[i],
+ 0);
}
if (d_qepr != NULL) {
d_qepr->registerAssertion(assertions[i]);
std::vector< QuantifiersModule* > qm;
if( d_model->checkNeeded() ){
needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call
- for( unsigned i=0; i<d_modules.size(); i++ ){
- if( d_modules[i]->needsCheck( e ) ){
- qm.push_back( d_modules[i] );
+ for (QuantifiersModule*& mdl : d_modules)
+ {
+ if (mdl->needsCheck(e))
+ {
+ qm.push_back(mdl);
needsCheck = true;
//can only request model at last call since theory combination can find inconsistencies
if( e>=Theory::EFFORT_LAST_CALL ){
- QuantifiersModule::QEffort me = d_modules[i]->needsModel(e);
+ QuantifiersModule::QEffort me = mdl->needsModel(e);
needsModelE = me<needsModelE ? me : needsModelE;
}
}
if( d_hasAddedLemma ){
return;
}
- if( !d_recorded_inst.empty() ){
- Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size() << " instantiations..." << std::endl;
- //remove explicitly recorded instantiations
- for( unsigned i=0; i<d_recorded_inst.size(); i++ ){
- removeInstantiationInternal( d_recorded_inst[i].first, d_recorded_inst[i].second );
- }
- d_recorded_inst.clear();
- }
double clSet = 0;
if( Trace.isOn("quant-engine") ){
//reset utilities
Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
- for( unsigned i=0; i<d_util.size(); i++ ){
- Trace("quant-engine-debug2") << "Reset " << d_util[i]->identify().c_str() << "..." << std::endl;
- if( !d_util[i]->reset( e ) ){
+ for (QuantifiersUtil*& util : d_util)
+ {
+ Trace("quant-engine-debug2") << "Reset " << util->identify().c_str()
+ << "..." << std::endl;
+ if (!util->reset(e))
+ {
flushLemmas();
if( d_hasAddedLemma ){
return;
//reset the modules
Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
- for( unsigned i=0; i<d_modules.size(); i++ ){
- Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
- d_modules[i]->reset_round( e );
+ for (QuantifiersModule*& mdl : d_modules)
+ {
+ Trace("quant-engine-debug2") << "Reset " << mdl->identify().c_str()
+ << std::endl;
+ mdl->reset_round(e);
}
Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
//reset may have added lemmas
}
if( !d_hasAddedLemma ){
//check each module
- for( unsigned i=0; i<qm.size(); i++ ){
- Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl;
- qm[i]->check( e, quant_e );
+ for (QuantifiersModule*& mdl : qm)
+ {
+ Trace("quant-engine-debug") << "Check " << mdl->identify().c_str()
+ << " at effort " << quant_e << "..."
+ << std::endl;
+ mdl->check(e, quant_e);
if( d_conflict ){
Trace("quant-engine-debug") << "...conflict!" << std::endl;
break;
{
if( e==Theory::EFFORT_LAST_CALL ){
//sources of incompleteness
- if( !d_recorded_inst.empty() ){
- Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl;
- setIncomplete = true;
+ for (QuantifiersUtil*& util : d_util)
+ {
+ if (!util->checkComplete())
+ {
+ Trace("quant-engine-debug") << "Set incomplete because utility "
+ << util->identify().c_str()
+ << " was incomplete." << std::endl;
+ setIncomplete = true;
+ }
}
//if we have a chance not to set incomplete
if( !setIncomplete ){
- setIncomplete = false;
//check if we should set the incomplete flag
- for( unsigned i=0; i<d_modules.size(); i++ ){
- if( !d_modules[i]->checkComplete() ){
- Trace("quant-engine-debug") << "Set incomplete because " << d_modules[i]->identify().c_str() << " was incomplete." << std::endl;
+ for (QuantifiersModule*& mdl : d_modules)
+ {
+ if (!mdl->checkComplete())
+ {
+ Trace("quant-engine-debug")
+ << "Set incomplete because module "
+ << mdl->identify().c_str() << " was incomplete."
+ << std::endl;
setIncomplete = true;
break;
}
d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
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;
- d_temp_inst_debug[it->first] = 0;
- }
- }
+ d_instantiate->debugPrint();
}
if( Trace.isOn("quant-engine") ){
double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
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;
- }
- }
+ d_instantiate->debugPrintModel();
}
}
//}
}
-void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- Node n = m.get( i );
- if( !n.isNull() ){
- vars.push_back( f[0][i] );
- terms.push_back( n );
- }
- }
-}
-
-
-bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool addedLem ) {
- if( !addedLem ){
- //record the instantiation for deletion later
- d_recorded_inst.push_back( std::pair< Node, std::vector< Node > >( q, terms ) );
- }
- if( options::incrementalSolving() ){
- Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << std::endl;
- inst::CDInstMatchTrie* imt;
- std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
- if( it!=d_c_inst_match_trie.end() ){
- imt = it->second;
- }else{
- imt = new CDInstMatchTrie( getUserContext() );
- d_c_inst_match_trie[q] = imt;
- }
- return imt->addInstMatch( this, q, terms, getUserContext(), modEq );
- }else{
- Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
- return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq );
- }
-}
-
-bool QuantifiersEngine::removeInstantiationInternal( Node q, std::vector< Node >& terms ) {
- if( options::incrementalSolving() ){
- std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
- if( it!=d_c_inst_match_trie.end() ){
- return it->second->removeInstMatch( this, q, terms );
- }else{
- return false;
- }
- }else{
- return d_inst_match_trie[q].removeInstMatch( this, q, terms );
- }
-}
-
-void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){
- Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level << std::endl;
- //if not from the vector of terms we instantiatied
- if( qn.getKind()!=BOUND_VARIABLE && n!=qn ){
- //if this is a new term, without an instantiation level
- if( !n.hasAttribute(InstLevelAttribute()) ){
- InstLevelAttribute ila;
- n.setAttribute(ila,level);
- Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
- Assert( n.getNumChildren()==qn.getNumChildren() );
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- setInstantiationLevelAttr( n[i], qn[i], level );
- }
- }
- }
-}
-
-void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
- if( !n.hasAttribute(InstLevelAttribute()) ){
- InstLevelAttribute ila;
- n.setAttribute(ila,level);
- Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- setInstantiationLevelAttr( n[i], level );
- }
- }
-}
-
-Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited ){
- std::map< Node, Node >::iterator itv = visited.find( n );
- if( itv==visited.end() ){
- Node ret = n;
- if( n.getKind()==INST_CONSTANT ){
- Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
- ret = terms[n.getAttribute(InstVarNumAttribute())];
- }else{
- //if( !quantifiers::TermUtil::hasInstConstAttr( n ) ){
- //Debug("check-inst") << "No inst const attr : " << n << std::endl;
- //return n;
- //}else{
- //Debug("check-inst") << "Recurse on : " << n << std::endl;
- std::vector< Node > cc;
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- cc.push_back( n.getOperator() );
- }
- bool changed = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node c = getSubstitute( n[i], terms, visited );
- cc.push_back( c );
- changed = changed || c!=n[i];
- }
- if( changed ){
- ret = NodeManager::currentNM()->mkNode( n.getKind(), cc );
- }
- }
- visited[n] = ret;
- return ret;
- }else{
- return itv->second;
- }
-}
-
-
-Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
- Node body;
- Assert( vars.size()==terms.size() );
- //process partial instantiation if necessary
- if( q[0].getNumChildren()!=vars.size() ){
- body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
- std::vector< Node > uninst_vars;
- //doing a partial instantiation, must add quantifier for all uninstantiated variables
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- if( std::find( vars.begin(), vars.end(), q[0][i] )==vars.end() ){
- uninst_vars.push_back( q[0][i] );
- }
- }
- Trace("partial-inst") << "Partially instantiating with " << vars.size() << " / " << q[0].getNumChildren() << " for " << q << std::endl;
- Assert( !uninst_vars.empty() );
- Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
- body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
- Trace("partial-inst") << "Partial instantiation : " << q << std::endl;
- Trace("partial-inst") << " : " << body << std::endl;
- }else{
- if( options::cbqi() ){
- body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
- }else{
- //do optimized version
- Node icb = d_term_util->getInstConstantBody( q );
- std::map< Node, Node > visited;
- body = getSubstitute( icb, terms, visited );
- if( Debug.isOn("check-inst") ){
- Node body2 = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
- if( body!=body2 ){
- Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
- }
- }
- }
- }
- if( doVts ){
- //do virtual term substitution
- body = Rewriter::rewrite( body );
- Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
- Node body_r = d_term_util->rewriteVtsSymbols( body );
- Trace("quant-vts-debug") << " ...result: " << body_r << std::endl;
- body = body_r;
- }
- return body;
-}
-
-Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){
- std::vector< Node > vars;
- std::vector< Node > terms;
- computeTermVector( q, m, vars, terms );
- return getInstantiation( q, vars, terms, doVts );
-}
-
-Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) {
- Assert( d_term_util->d_vars.find( q )!=d_term_util->d_vars.end() );
- return getInstantiation( q, d_term_util->d_vars[q], terms, doVts );
-}
-
-/*
-bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq ){
- if( options::incrementalSolving() ){
- if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
- if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq ) ){
- return true;
- }
- }
- }else{
- if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
- if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq ) ){
- return true;
- }
- }
- }
- return false;
-}
-*/
-
bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
if( doCache ){
if( doRewrite ){
d_phase_req_waiting[lit] = req;
}
-bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts ){
- std::vector< Node > terms;
- m.getTerms( q, terms );
- return addInstantiation( q, terms, mkRep, modEq, doVts );
-}
-
-bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool doVts ) {
- // For resource-limiting (also does a time check).
- getOutputChannel().safePoint(options::quantifierStep());
- Assert( !d_conflict );
- Assert( terms.size()==q[0].getNumChildren() );
- Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
- std::vector< Node > rlv_cond;
- for( unsigned i=0; i<terms.size(); i++ ){
- Trace("inst-add-debug") << " " << q[0][i];
- Trace("inst-add-debug2") << " -> " << terms[i];
- TypeNode tn = q[0][i].getType();
- if( terms[i].isNull() ){
- terms[i] = getTermForType(tn);
- }
- if( mkRep ){
- //pick the best possible representative for instantiation, based on past use and simplicity of term
- terms[i] = getInternalRepresentative( terms[i], q, i );
- }else{
- //ensure the type is correct
- terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn);
- }
- Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
- if( terms[i].isNull() ){
- Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl;
- return false;
- }else{
- //get relevancy conditions
- if( options::instRelevantCond() ){
- quantifiers::TermUtil::getRelevancyCondition( terms[i], rlv_cond );
- }
- }
-#ifdef CVC4_ASSERTIONS
- bool bad_inst = false;
- if( quantifiers::TermUtil::containsUninterpretedConstant( terms[i] ) ){
- Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl;
- bad_inst = true;
- }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){
- Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl;
- bad_inst = true;
- }else if( options::cbqi() ){
- Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]);
- if( !icf.isNull() ){
- if( icf==q ){
- Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl;
- bad_inst = true;
- }else if( quantifiers::TermUtil::containsTerms( terms[i], d_term_util->d_inst_constants[q] ) ){
- Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl;
- bad_inst = true;
- }
- }
- }
- //this assertion is critical to soundness
- if( bad_inst ){
- Trace("inst")<< "***& Bad Instantiate " << q << " with " << std::endl;
- for( unsigned j=0; j<terms.size(); j++ ){
- Trace("inst") << " " << terms[j] << std::endl;
- }
- Assert( false );
- }
-#endif
- }
-
- //check based on instantiation level
- if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
- for( unsigned i=0; i<terms.size(); i++ ){
- if( !d_term_db->isTermEligibleForInstantiation( terms[i], q, true ) ){
- return false;
- }
- }
- }
-
- //check for positive entailment
- if( options::instNoEntail() ){
- //TODO: check consistency of equality engine (if not aborting on utility's reset)
- std::map< TNode, TNode > subs;
- for( unsigned i=0; i<terms.size(); i++ ){
- subs[q[0][i]] = terms[i];
- }
- if( d_term_db->isEntailed( q[1], subs, false, true ) ){
- Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
- ++(d_statistics.d_inst_duplicate_ent);
- return false;
- }
- //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true );
- //Trace("inst-add-debug2") << "Instantiation evaluates to : " << std::endl;
- //Trace("inst-add-debug2") << " " << eval << std::endl;
- }
-
- //check for term vector duplication
- bool alreadyExists = !recordInstantiationInternal( q, terms, modEq );
- if( alreadyExists ){
- Trace("inst-add-debug") << " --> Already exists." << std::endl;
- ++(d_statistics.d_inst_duplicate_eq);
- return false;
- }
-
- //construct the instantiation
- Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
- Assert( d_term_util->d_vars[q].size()==terms.size() );
- Node body = getInstantiation( q, d_term_util->d_vars[q], terms, doVts ); //do virtual term substitution
- Node orig_body = body;
- if( options::cbqiNestedQE() && d_i_cbqi ){
- body = d_i_cbqi->doNestedQE( q, terms, body, doVts );
- }
- body = quantifiers::QuantifiersRewriter::preprocess( body, true );
- Trace("inst-debug") << "...preprocess to " << body << std::endl;
-
- //construct the lemma
- Trace("inst-assert") << "(assert " << body << ")" << std::endl;
- body = Rewriter::rewrite(body);
-
- if( d_useModelEe && options::instNoModelTrue() ){
- Node val_body = d_model->getValue( body );
- if( val_body==d_term_util->d_true ){
- Trace("inst-add-debug") << " --> True in model." << std::endl;
- ++(d_statistics.d_inst_duplicate_model_true);
- return false;
- }
- }
-
- Node lem;
- if( rlv_cond.empty() ){
- lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body );
- }else{
- rlv_cond.push_back( q.negate() );
- rlv_cond.push_back( body );
- lem = NodeManager::currentNM()->mkNode( kind::OR, rlv_cond );
- }
- lem = Rewriter::rewrite(lem);
-
- //check for lemma duplication
- if( addLemma( lem, true, false ) ){
- d_total_inst_debug[q]++;
- d_temp_inst_debug[q]++;
- d_total_inst_count_debug++;
- if( Trace.isOn("inst") ){
- Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
- for( unsigned i=0; i<terms.size(); i++ ){
- if( Trace.isOn("inst") ){
- Trace("inst") << " " << terms[i];
- if( Trace.isOn("inst-debug") ){
- Trace("inst-debug") << ", type=" << terms[i].getType() << ", var_type=" << q[0][i].getType();
- }
- Trace("inst") << std::endl;
- }
- }
- }
- if( options::instMaxLevel()!=-1 ){
- if( doVts ){
- //virtual term substitution/instantiation level features are incompatible
- Assert( false );
- }else{
- uint64_t maxInstLevel = 0;
- for( unsigned i=0; i<terms.size(); i++ ){
- if( terms[i].hasAttribute(InstLevelAttribute()) ){
- if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
- maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
- }
- }
- }
- setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 );
- }
- }
- if (d_curr_effort_level > QuantifiersModule::QEFFORT_CONFLICT
- && d_curr_effort_level < QuantifiersModule::QEFFORT_NONE)
- {
- //notify listeners
- for( unsigned j=0; j<d_inst_notify.size(); j++ ){
- if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){
- Trace("inst-add-debug") << "...we are in conflict." << std::endl;
- setConflict();
- Assert( !d_lemmas_waiting.empty() );
- break;
- }
- }
- }
- if( options::trackInstLemmas() ){
- bool recorded;
- if( options::incrementalSolving() ){
- recorded = d_c_inst_match_trie[q]->recordInstLemma( q, terms, lem );
- }else{
- recorded = d_inst_match_trie[q].recordInstLemma( q, terms, lem );
- }
- Trace("inst-add-debug") << "...was recorded : " << recorded << std::endl;
- Assert( recorded );
- }
- Trace("inst-add-debug") << " --> Success." << std::endl;
- ++(d_statistics.d_instantiations);
- return true;
- }else{
- Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
- ++(d_statistics.d_inst_duplicate);
- return false;
- }
-}
-
-bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) {
- //lem must occur in d_waiting_lemmas
- if( removeLemma( lem ) ){
- return removeInstantiationInternal( q, terms );
- }else{
- return false;
- }
-}
-
bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
n = Rewriter::rewrite( n );
Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
void QuantifiersEngine::flushLemmas(){
if( !d_lemmas_waiting.empty() ){
//filter based on notify classes
- if( !d_inst_notify.empty() ){
+ if (d_instantiate->hasNotify())
+ {
unsigned prev_lem_sz = d_lemmas_waiting.size();
- for( unsigned j=0; j<d_inst_notify.size(); j++ ){
- d_inst_notify[j]->filterInstantiations();
- }
+ d_instantiate->notifyFlushLemmas();
if( prev_lem_sz!=d_lemmas_waiting.size() ){
Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
}
}
bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) {
- //only if unsat core available
- bool isUnsatCoreAvailable = false;
- if( options::proof() ){
- isUnsatCoreAvailable = ProofManager::currentPM()->unsatCoreAvailable();
- }
- if( isUnsatCoreAvailable ){
- Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl;
- ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, active_lemmas);
- if( Trace.isOn("inst-unsat-core") ){
- Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: " << std::endl;
- for (unsigned i = 0; i < active_lemmas.size(); ++i) {
- Trace("inst-unsat-core") << " " << active_lemmas[i] << std::endl;
- }
- Trace("inst-unsat-core") << std::endl;
- }
- return true;
- }else{
- return false;
- }
+ return d_instantiate->getUnsatCoreLemmas(active_lemmas);
}
bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) {
- if( getUnsatCoreLemmas( active_lemmas ) ){
- for (unsigned i = 0; i < active_lemmas.size(); ++i) {
- Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore(active_lemmas[i]);
- if( n!=active_lemmas[i] ){
- Trace("inst-unsat-core") << " weaken : " << active_lemmas[i] << " -> " << n << std::endl;
- }
- weak_imp[active_lemmas[i]] = n;
- }
- return true;
- }else{
- return false;
- }
+ return d_instantiate->getUnsatCoreLemmas(active_lemmas, weak_imp);
}
void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
- std::vector< Node > lemmas;
- getInstantiations( q, lemmas );
- std::map< Node, Node > quant;
- std::map< Node, std::vector< Node > > tvec;
- getExplanationForInstLemmas( lemmas, quant, tvec );
- for( std::map< Node, std::vector< Node > >::iterator it = tvec.begin(); it != tvec.end(); ++it ){
- tvecs.push_back( it->second );
- }
+ d_instantiate->getInstantiationTermVectors(q, tvecs);
}
void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
- if( options::incrementalSolving() ){
- for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
- getInstantiationTermVectors( it->first, insts[it->first] );
- }
- }else{
- for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
- getInstantiationTermVectors( it->first, insts[it->first] );
- }
- }
+ d_instantiate->getInstantiationTermVectors(insts);
}
-void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) {
- if( options::trackInstLemmas() ){
- if( options::incrementalSolving() ){
- for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
- it->second->getExplanationForInstLemmas( it->first, lems, quant, tvec );
- }
- }else{
- for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
- it->second.getExplanationForInstLemmas( it->first, lems, quant, tvec );
- }
- }
-#ifdef CVC4_ASSERTIONS
- for( unsigned j=0; j<lems.size(); j++ ){
- Assert( quant.find( lems[j] )!=quant.end() );
- Assert( tvec.find( lems[j] )!=tvec.end() );
- }
-#endif
- }else{
- Assert( false );
- }
+void QuantifiersEngine::getExplanationForInstLemmas(
+ const std::vector<Node>& lems,
+ std::map<Node, Node>& quant,
+ std::map<Node, std::vector<Node> >& tvec)
+{
+ d_instantiate->getExplanationForInstLemmas(lems, quant, tvec);
}
void QuantifiersEngine::printInstantiations( std::ostream& out ) {
- bool useUnsatCore = false;
- std::vector< Node > active_lemmas;
- if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){
- useUnsatCore = true;
- }
-
bool printed = false;
// print the skolemizations
if (d_skolemize->printSkolemization(out))
printed = true;
}
// print the instantiations
- if( options::incrementalSolving() ){
- for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
- bool firstTime = true;
- it->second->print( out, it->first, firstTime, useUnsatCore, active_lemmas );
- if( !firstTime ){
- out << ")" << std::endl;
- }
- printed = printed || !firstTime;
- }
- }else{
- for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
- bool firstTime = true;
- it->second.print( out, it->first, firstTime, useUnsatCore, active_lemmas );
- if( !firstTime ){
- out << ")" << std::endl;
- }
- printed = printed || !firstTime;
- }
+ if (d_instantiate->printInstantiations(out))
+ {
+ printed = true;
}
if( !printed ){
out << "No instantiations" << std::endl;
}
void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
- if( options::incrementalSolving() ){
- for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
- qs.push_back( it->first );
- }
- }else{
- for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
- qs.push_back( it->first );
- }
- }
+ d_instantiate->getInstantiatedQuantifiedFormulas(qs);
}
void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
- bool useUnsatCore = false;
- std::vector< Node > active_lemmas;
- if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){
- useUnsatCore = true;
- }
-
- if( options::incrementalSolving() ){
- for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
- it->second->getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas );
- }
- }else{
- for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
- it->second.getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas );
- }
- }
+ d_instantiate->getInstantiations(insts);
}
void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts ) {
- if( options::incrementalSolving() ){
- std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
- if( it!=d_c_inst_match_trie.end() ){
- std::vector< Node > active_lemmas;
- it->second->getInstantiations( insts, it->first, this, false, active_lemmas );
- }
- }else{
- std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.find( q );
- if( it!=d_inst_match_trie.end() ){
- std::vector< Node > active_lemmas;
- it->second.getInstantiations( insts, it->first, this, false, active_lemmas );
- }
- }
+ d_instantiate->getInstantiations(q, insts);
}
Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
- Assert( q.getKind()==FORALL );
- std::vector< Node > insts;
- getInstantiations( q, insts );
- if( insts.empty() ){
- return NodeManager::currentNM()->mkConst(true);
- }else{
- Node ret;
- if( insts.size()==1 ){
- ret = insts[0];
- }else{
- ret = NodeManager::currentNM()->mkNode( kind::AND, insts );
- }
- //have to remove q, TODO: avoid this in a better way
- TNode tq = q;
- TNode tt = d_term_util->d_true;
- ret = ret.substitute( tq, tt );
- return ret;
- }
+ return d_instantiate->getInstantiatedConjunction(q);
}
QuantifiersEngine::Statistics::Statistics()
d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
- d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
- d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
- d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
- d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0),
- d_inst_duplicate_model_true("QuantifiersEngine::Duplicate_Inst_Model_True", 0),
d_triggers("QuantifiersEngine::Triggers", 0),
d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
smtStatisticsRegistry()->registerStat(&d_num_quant);
smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
- smtStatisticsRegistry()->registerStat(&d_instantiations);
- smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
- smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
- smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
- smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true);
smtStatisticsRegistry()->registerStat(&d_triggers);
smtStatisticsRegistry()->registerStat(&d_simple_triggers);
smtStatisticsRegistry()->registerStat(&d_multi_triggers);
smtStatisticsRegistry()->unregisterStat(&d_num_quant);
smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
- smtStatisticsRegistry()->unregisterStat(&d_instantiations);
- smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
- smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
- smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
- smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true);
smtStatisticsRegistry()->unregisterStat(&d_triggers);
smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
return ret;
}
-Node QuantifiersEngine::getTermForType(TypeNode tn)
-{
- if (d_term_enum->isClosedEnumerableType(tn))
- {
- return d_term_enum->getEnumerateTerm(tn, 0);
- }
- else
- {
- return d_term_db->getOrMakeTypeGroundTerm(tn);
- }
-}
-
void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
eq::EqualityEngine* ee = getActiveEqualityEngine();
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
class QuantifiersEngine;
-class InstantiationNotify {
-public:
- InstantiationNotify(){}
- virtual ~InstantiationNotify() {}
- virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
- Node q,
- Node lem,
- std::vector<Node>& terms,
- Node body) = 0;
- virtual void filterInstantiations() = 0;
-};
-
namespace quantifiers {
//TODO: organize this more/review this, github issue #1163
//TODO: include these instead of doing forward declarations? #1307
class TermDb;
class TermDbSygus;
class TermUtil;
+ class Instantiate;
class Skolemize;
class TermEnumeration;
class FirstOrderModel;
class QuantifiersEngine {
+ // TODO: remove these github issue #1163
friend class quantifiers::InstantiationEngine;
friend class quantifiers::InstStrategyCbqi;
friend class quantifiers::InstStrategyCegqi;
std::vector< QuantifiersUtil* > d_util;
/** vector of modules for quantifiers */
std::vector< QuantifiersModule* > d_modules;
- /** instantiation notify */
- std::vector< InstantiationNotify* > d_inst_notify;
/** equality query class */
quantifiers::EqualityQueryQuantifiersEngine* d_eq_query;
/** equality inference class */
quantifiers::TermUtil* d_term_util;
/** quantifiers attributes */
std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
+ /** instantiate utility */
+ std::unique_ptr<quantifiers::Instantiate> d_instantiate;
/** skolemize utility */
std::unique_ptr<quantifiers::Skolemize> d_skolemize;
/** term enumeration utility */
std::vector< Node > d_lemmas_waiting;
/** phase requirements waiting */
std::map< Node, bool > d_phase_req_waiting;
- /** list of all instantiations produced for each quantifier */
- std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
- std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
- /** recorded instantiations */
- std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst;
/** all triggers will be stored in this trie */
inst::TriggerTrie* d_tr_trie;
/** extended model object */
quantifiers::FirstOrderModel* d_model;
- /** statistics for debugging */
- std::map< Node, int > d_total_inst_debug;
- std::map< Node, int > d_temp_inst_debug;
- int d_total_inst_count_debug;
/** inst round counters TODO: make context-dependent? */
context::CDO< int > d_ierCounter_c;
int d_ierCounter;
private:
/** reduceQuantifier, return true if reduced */
bool reduceQuantifier( Node q );
- /** compute term vector */
- void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
- /** record instantiation, return true if it was non-duplicate */
- bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool addedLem = true );
- /** remove instantiation */
- bool removeInstantiationInternal( Node q, std::vector< Node >& terms );
- /** set instantiation level attr */
- static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
/** flush lemmas */
void flushLemmas();
public:
- /** get instantiation */
- Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
- /** get instantiation */
- Node getInstantiation( Node q, InstMatch& m, bool doVts = false );
- /** get instantiation */
- Node getInstantiation( Node q, std::vector< Node >& terms, bool doVts = false );
- /** do substitution */
- Node getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited );
/** add lemma lem */
bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
/** remove pending lemma */
bool removeLemma( Node lem );
/** add require phase */
void addRequirePhase( Node lit, bool req );
- /** do instantiation specified by m */
- bool addInstantiation( Node q, InstMatch& m, bool mkRep = false, bool modEq = false, bool doVts = false );
- /** add instantiation */
- bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = false, bool modEq = false, bool doVts = false );
- /** remove pending instantiation */
- bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms );
/** split on node n */
bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
/** add split equality */
bool inConflict() { return d_conflict; }
/** set conflict */
void setConflict();
+ /** get current q effort */
+ QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
/** get number of waiting lemmas */
unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
/** get needs check */
bool getInstWhenNeedsCheck( Theory::Effort e );
/** get user pat mode */
quantifiers::UserPatMode getInstUserPatMode();
- /** set instantiation level attr */
- static void setInstantiationLevelAttr( Node n, uint64_t level );
public:
/** get model */
quantifiers::FirstOrderModel* getModel() { return d_model; }
quantifiers::QuantAttributes* getQuantAttributes() {
return d_quant_attr.get();
}
+ /** get instantiate utility */
+ quantifiers::Instantiate* getInstantiate() { return d_instantiate.get(); }
/** get skolemize utility */
quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); }
/** get term enumeration utility */
eq::EqualityEngine* getMasterEqualityEngine();
/** get the active equality engine */
eq::EqualityEngine* getActiveEqualityEngine();
+ /** use model equality engine */
+ bool usingModelEqualityEngine() const { return d_useModelEe; }
/** debug print equality engine */
void debugPrintEqualityEngine( const char * c );
/** get internal representative */
Node getInternalRepresentative( Node a, Node q, int index );
- /** get term for type
- *
- * This returns an arbitrary term for type tn.
- * This term is chosen heuristically to be the best
- * term for instantiation. Currently, this
- * heuristic enumerates the first term of the
- * type if the type is closed enumerable, otherwise
- * an existing ground term from the term database if
- * one exists, or otherwise a fresh variable.
- */
- Node getTermForType(TypeNode tn);
public:
+ //----------user interface for instantiations (see quantifiers/instantiate.h)
/** print instantiations */
- void printInstantiations( std::ostream& out );
+ void printInstantiations(std::ostream& out);
/** print solution for synthesis conjectures */
- void printSynthSolution( std::ostream& out );
+ void printSynthSolution(std::ostream& out);
/** get list of quantified formulas that were instantiated */
- void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
+ void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
/** get instantiations */
- void getInstantiations( Node q, std::vector< Node >& insts );
- void getInstantiations( std::map< Node, std::vector< Node > >& insts );
+ void getInstantiations(Node q, std::vector<Node>& insts);
+ void getInstantiations(std::map<Node, std::vector<Node> >& insts);
/** get instantiation term vectors */
- void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
- void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
+ void getInstantiationTermVectors(Node q,
+ std::vector<std::vector<Node> >& tvecs);
+ void getInstantiationTermVectors(
+ std::map<Node, std::vector<std::vector<Node> > >& insts);
/** get instantiated conjunction */
- Node getInstantiatedConjunction( Node q );
+ Node getInstantiatedConjunction(Node q);
/** get unsat core lemmas */
- bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas );
- bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp );
- /** get inst for lemmas */
- void getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec );
+ bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
+ bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
+ std::map<Node, Node>& weak_imp);
+ /** get explanation for instantiation lemmas */
+ void getExplanationForInstLemmas(const std::vector<Node>& lems,
+ std::map<Node, Node>& quant,
+ std::map<Node, std::vector<Node> >& tvec);
+ //----------end user interface for instantiations
+
/** statistics class */
class Statistics {
public:
IntStat d_num_quant;
IntStat d_instantiation_rounds;
IntStat d_instantiation_rounds_lc;
- IntStat d_instantiations;
- IntStat d_inst_duplicate;
- IntStat d_inst_duplicate_eq;
- IntStat d_inst_duplicate_ent;
- IntStat d_inst_duplicate_model_true;
IntStat d_triggers;
IntStat d_simple_triggers;
IntStat d_multi_triggers;
projects / cvc5.git / commitdiff