model_builder.h \
model_builder.cpp \
quantifiers_attributes.h \
- quantifiers_attributes.cpp
+ quantifiers_attributes.cpp \
+ inst_gen.h \
+ inst_gen.cpp
EXTRA_DIST = \
kinds \
}
}
-#if 0
-
-CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
- d_op( op ), d_qe( qe ), d_term_iter( -2 ){
- Assert( !d_op.isNull() );
-}
-void CandidateGeneratorQE::resetInstantiationRound(){
- d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size();
-}
-
-void CandidateGeneratorQE::reset( Node eqc ){
- if( eqc.isNull() ){
- d_term_iter = 0;
- }else{
- //create an equivalence class iterator in eq class eqc
- if( d_qe->getEqualityQuery()->getEngine()->hasTerm( eqc ) ){
- eqc = d_qe->getEqualityQuery()->getEngine()->getRepresentative( eqc );
- d_eqc = eq::EqClassIterator( eqc, d_qe->getEqualityQuery()->getEngine() );
- d_retNode = Node::null();
- }else{
- d_retNode = eqc;
- }
- d_term_iter = -1;
- }
-}
-
-Node CandidateGeneratorQE::getNextCandidate(){
- if( d_term_iter>=0 ){
- //get next candidate term in the uf term database
- while( d_term_iter<d_term_iter_limit ){
- Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
- d_term_iter++;
- if( isLegalCandidate( n ) ){
- return n;
- }
- }
- }else if( d_term_iter==-1 ){
- if( d_retNode.isNull() ){
- //get next candidate term in equivalence class
- while( !d_eqc.isFinished() ){
- Node n = (*d_eqc);
- ++d_eqc;
- if( n.hasOperator() && n.getOperator()==d_op ){
- if( isLegalCandidate( n ) ){
- return n;
- }
- }
- }
- }else{
- Node ret;
- if( d_retNode.hasOperator() && d_retNode.getOperator()==d_op ){
- ret = d_retNode;
- }
- d_term_iter = -2; //done returning matches
- return ret;
- }
- }
- return Node::null();
-}
-
-#else
-
-
CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
d_op( op ), d_qe( qe ), d_term_iter( -1 ){
Assert( !d_op.isNull() );
return Node::null();
}
-#endif
-
//CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) :
// d_qe( qe ), d_eq_class( eqc ){
// d_eci = NULL;
class CandidateGeneratorQEDisequal;
-#if 0
-
-class CandidateGeneratorQE : public CandidateGenerator
-{
- friend class CandidateGeneratorQEDisequal;
-private:
- //operator you are looking for
- Node d_op;
- //instantiator pointer
- QuantifiersEngine* d_qe;
- //the equality class iterator
- eq::EqClassIterator d_eqc;
- int d_term_iter;
- int d_term_iter_limit;
-private:
- Node d_retNode;
-public:
- CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
- ~CandidateGeneratorQE(){}
-
- void resetInstantiationRound();
- void reset( Node eqc );
- Node getNextCandidate();
-};
-
-#else
-
class CandidateGeneratorQE : public CandidateGenerator
{
friend class CandidateGeneratorQEDisequal;
Node getNextCandidate();
};
-#endif
//class CandidateGeneratorQEDisequal : public CandidateGenerator
//{
--- /dev/null
+/********************* */\r
+/*! \file inst_gen.cpp\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)\r
+ ** Courant Institute of Mathematical Sciences\r
+ ** New York University\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Implementation of inst gen classes\r
+ **/\r
+\r
+#include "theory/quantifiers/inst_gen.h"\r
+#include "theory/quantifiers/model_engine.h"\r
+#include "theory/quantifiers/model_builder.h"\r
+#include "theory/quantifiers/first_order_model.h"\r
+\r
+#define RECONSIDER_FUNC_CONSTANT\r
+\r
+using namespace std;\r
+using namespace CVC4;\r
+using namespace CVC4::kind;\r
+using namespace CVC4::context;\r
+using namespace CVC4::theory;\r
+using namespace CVC4::theory::quantifiers;\r
+\r
+\r
+\r
+InstGenProcess::InstGenProcess( Node n ) : d_node( n ){\r
+ Assert( n.hasAttribute(InstConstantAttribute()) );\r
+ int count = 0;\r
+ for( size_t i=0; i<n.getNumChildren(); i++ ){\r
+ if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){\r
+ d_children.push_back( InstGenProcess( n[i] ) );\r
+ d_children_index.push_back( i );\r
+ d_children_map[ i ] = count;\r
+ count++;\r
+ }\r
+ }\r
+}\r
+\r
+void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){\r
+ if( !qe->existsInstantiation( f, m, true, true ) ){\r
+ //if( d_inst_trie[val].addInstMatch( qe, f, m, true, NULL, true ) ){\r
+ d_match_values.push_back( val );\r
+ d_matches.push_back( InstMatch( &m ) );\r
+ //}\r
+ }\r
+}\r
+\r
+void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f ){\r
+ //calculate all matches for children\r
+ for( int i=0; i<(int)d_children.size(); i++ ){\r
+ d_children[i].calculateMatches( qe, f );\r
+ if( d_children[i].getNumMatches()==0 ){\r
+ return;\r
+ }\r
+ }\r
+ Trace("cm") << "calculate matches " << d_node << std::endl;\r
+ //get the model\r
+ FirstOrderModel* fm = qe->getModel();\r
+ if( d_node.getKind()==APPLY_UF ){\r
+ //if this is an uninterpreted function\r
+ Node op = d_node.getOperator();\r
+ //process all values\r
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){\r
+ Node n = fm->d_uf_terms[op][i];\r
+ bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );\r
+ for( int t=(isSelected ? 0 : 1); t<2; t++ ){\r
+ //do not consider ground case if it is already congruent to another ground term\r
+ if( t==0 || !n.getAttribute(NoMatchAttribute()) ){\r
+ Trace("cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl;\r
+ bool success = true;\r
+ InstMatch curr;\r
+ for( size_t j=0; j<d_node.getNumChildren(); j++ ){\r
+ if( d_children_map.find( j )==d_children_map.end() ){\r
+ if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){\r
+ if( d_node[j].getKind()==INST_CONSTANT ){\r
+ //FIXME: is this correct?\r
+ if( !curr.setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){\r
+ Trace("cm") << "fail match: " << n[j] << " is not equal to " << curr.get( d_node[j] ) << std::endl;\r
+ Trace("cm") << " are equal : " << qe->getEqualityQuery()->areEqual( n[j], curr.get( d_node[j] ) ) << std::endl;\r
+ success = false;\r
+ break;\r
+ }\r
+ }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){\r
+ Trace("cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;\r
+ success = false;\r
+ break;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ if( success ){\r
+ //try to find unifier for d_node = n\r
+ calculateMatchesUninterpreted( qe, f, curr, n, 0, t==0 );\r
+ }\r
+ }\r
+ }\r
+ }\r
+\r
+ }else{\r
+ InstMatch curr;\r
+ //if this is an interpreted function\r
+ std::vector< Node > terms;\r
+ calculateMatchesInterpreted( qe, f, curr, terms, 0 );\r
+ }\r
+ Trace("cm") << "done calculate matches" << std::endl;\r
+}\r
+\r
+bool InstGenProcess::getMatch( EqualityQuery* q, int i, InstMatch& m ){\r
+ //FIXME: is this correct? (query may not be accurate)\r
+ return m.merge( q, d_matches[i] );\r
+}\r
+\r
+void InstGenProcess::calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ){\r
+ if( childIndex==(int)d_children.size() ){\r
+ Node val = qe->getModel()->getRepresentative( n ); //FIXME: is this correct?\r
+ Trace("cm") << " - u-match : " << val << std::endl;\r
+ Trace("cm") << " : " << curr << std::endl;\r
+ addMatchValue( qe, f, val, curr );\r
+ }else{\r
+ Trace("cm") << "Consider child index = " << childIndex << ", against ground term argument " << d_children_index[childIndex] << " ... " << n[d_children_index[childIndex]] << std::endl;\r
+ bool sel = ( isSelected && n[d_children_index[childIndex]].getAttribute(ModelBasisAttribute()) );\r
+ for( int i=0; i<(int)d_children[ childIndex ].getNumMatches(); i++ ){\r
+ //FIXME: is this correct?\r
+ if( sel || qe->getEqualityQuery()->areEqual( d_children[ childIndex ].getMatchValue( i ), n[d_children_index[childIndex]] ) ){\r
+ InstMatch next( &curr );\r
+ if( d_children[ childIndex ].getMatch( qe->getEqualityQuery(), i, next ) ){\r
+ calculateMatchesUninterpreted( qe, f, next, n, childIndex+1, isSelected );\r
+ }else{\r
+ Trace("cm") << curr << " not equal to " << d_children[ childIndex ].d_matches[i] << std::endl;\r
+ Trace("cm") << childIndex << " match " << i << " not equal subs." << std::endl;\r
+ }\r
+ }else{\r
+ Trace("cm") << childIndex << " match " << i << " not equal value." << std::endl;\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+void InstGenProcess::calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex ){\r
+ FirstOrderModel* fm = qe->getModel();\r
+ if( argIndex==(int)d_node.getNumChildren() ){\r
+ Node val;\r
+ if( d_node.getNumChildren()==0 ){\r
+ val = d_node;\r
+ }else if( d_node.getKind()==EQUAL ){\r
+ val = qe->getEqualityQuery()->areEqual( terms[0], terms[1] ) ? fm->d_true : fm->d_false;\r
+ }else{\r
+ val = NodeManager::currentNM()->mkNode( d_node.getKind(), terms );\r
+ val = Rewriter::rewrite( val );\r
+ }\r
+ Trace("cm") << " - i-match : " << val << std::endl;\r
+ Trace("cm") << " : " << curr << std::endl;\r
+ addMatchValue( qe, f, val, curr );\r
+ }else{\r
+ if( d_children_map.find( argIndex )==d_children_map.end() ){\r
+ terms.push_back( fm->getRepresentative( d_node[argIndex] ) );\r
+ calculateMatchesInterpreted( qe, f, curr, terms, argIndex+1 );\r
+ terms.pop_back();\r
+ }else{\r
+ for( int i=0; i<(int)d_children[ d_children_map[argIndex] ].getNumMatches(); i++ ){\r
+ InstMatch next( &curr );\r
+ if( d_children[ d_children_map[argIndex] ].getMatch( qe->getEqualityQuery(), i, next ) ){\r
+ terms.push_back( d_children[ d_children_map[argIndex] ].getMatchValue( i ) );\r
+ calculateMatchesInterpreted( qe, f, next, terms, argIndex+1 );\r
+ terms.pop_back();\r
+ }\r
+ }\r
+ }\r
+ }\r
+}\r
--- /dev/null
+/********************* */\r
+/*! \file inst_gen.h\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)\r
+ ** Courant Institute of Mathematical Sciences\r
+ ** New York University\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Inst Gen classes\r
+ **/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__THEORY__QUANTIFIERS__INST_GEN_H\r
+#define __CVC4__THEORY__QUANTIFIERS__INST_GEN_H\r
+\r
+#include "theory/quantifiers_engine.h"\r
+#include "theory/quantifiers/inst_match.h"\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+namespace quantifiers {\r
+\r
+class InstGenProcess\r
+{\r
+private:\r
+ //the node we are processing\r
+ Node d_node;\r
+ //the sub children for this node\r
+ std::vector< InstGenProcess > d_children;\r
+ std::vector< int > d_children_index;\r
+ std::map< int, int > d_children_map;\r
+ //the matches we have produced\r
+ std::vector< InstMatch > d_matches;\r
+ std::vector< Node > d_match_values;\r
+ //add match value\r
+ std::map< Node, inst::InstMatchTrie > d_inst_trie;\r
+ void addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m );\r
+private:\r
+ void calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected );\r
+ void calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex );\r
+public:\r
+ InstGenProcess( Node n );\r
+ virtual ~InstGenProcess(){}\r
+\r
+ void calculateMatches( QuantifiersEngine* qe, Node f );\r
+ int getNumMatches() { return d_matches.size(); }\r
+ bool getMatch( EqualityQuery* q, int i, InstMatch& m );\r
+ Node getMatchValue( int i ) { return d_match_values[i]; }\r
+};\r
+\r
+}\r
+}\r
+}\r
+\r
+#endif\r
bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){
std::map< Node, Node >::iterator vn = d_map.find( v );
- if( vn==d_map.end() ){
+ if( vn==d_map.end() || vn->second.isNull() ){
set = true;
this->set(v,m);
Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl;
bool InstMatch::add( InstMatch& m ){
for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){
- if( d_map.find( it->first )==d_map.end() ){
+ std::map< Node, Node >::iterator itf = d_map.find( it->first );
+ if( itf==d_map.end() || itf->second.isNull() ){
d_map[it->first] = it->second;
}
}
bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){
- if( d_map.find( it->first )==d_map.end() ){
- d_map[ it->first ] = it->second;
- }else{
- if( it->second!=d_map[it->first] ){
- if( !q->areEqual( it->second, d_map[it->first] ) ){
+ if( !it->second.isNull() ){
+ std::map< Node, Node >::iterator itf = d_map.find( it->first );
+ if( itf==d_map.end() || itf->second.isNull() ){
+ d_map[ it->first ] = it->second;
+ }else{
+ if( !q->areEqual( it->second, itf->second ) ){
d_map.clear();
return false;
}
}
}
+/** get value */
+Node InstMatch::getValue( Node var ){
+ std::map< Node, Node >::iterator it = d_map.find( var );
+ if( it!=d_map.end() ){
+ return it->second;
+ }else{
+ return Node::null();
+ }
+}
+/*
void InstMatch::computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match ){
for( int i=0; i<(int)vars.size(); i++ ){
std::map< Node, Node >::iterator it = d_map.find( vars[i] );
}
}
}
+
void InstMatch::computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ){
for( int i=0; i<(int)vars.size(); i++ ){
if( d_map.find( vars[i] )!=d_map.end() && !d_map[ vars[i] ].isNull() ){
}
}
}
-
+*/
/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
}
/** exists match */
-bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio ){
+bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio, bool modInst ){
if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
return true;
}else{
Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
if( it!=d_data.end() ){
- if( it->second.existsInstMatch( qe, f, m, modEq, index+1, imtio ) ){
+ if( it->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){
return true;
}
}
+ //check if m is an instance of another instantiation if modInst is true
+ if( modInst ){
+ if( !n.isNull() ){
+ Node nl;
+ it = d_data.find( nl );
+ if( it!=d_data.end() ){
+ if( it->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){
+ return true;
+ }
+ }
+ }
+ }
if( modEq ){
//check modulo equality if any other instantiation match exists
if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
if( en!=n ){
std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
if( itc!=d_data.end() ){
- if( itc->second.existsInstMatch( qe, f, m, modEq, index+1, imtio ) ){
+ if( itc->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){
return true;
}
}
}
}
-bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, ImtIndexOrder* imtio ){
- if( !existsInstMatch( qe, f, m, modEq, 0, imtio ) ){
+bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, ImtIndexOrder* imtio, bool modInst ){
+ return existsInstMatch2( qe, f, m, modEq, 0, imtio, modInst );
+}
+
+bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, ImtIndexOrder* imtio, bool modInst ){
+ if( !existsInstMatch( qe, f, m, modEq, imtio, modInst ) ){
addInstMatch2( qe, f, m, 0, imtio );
return true;
}else{
bool merge( EqualityQuery* q, InstMatch& m );
/** debug print method */
void debugPrint( const char* c );
+ /** is complete? */
+ bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
/** make complete */
void makeComplete( Node f, QuantifiersEngine* qe );
/** make internal: ensure that no term in d_map contains instantiation constants */
void makeInternal( QuantifiersEngine* qe );
/** make representative */
void makeRepresentative( QuantifiersEngine* qe );
- /** apply rewrite */
- void applyRewrite();
/** compute d_match */
- void computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match );
+ //void computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match );
/** compute d_match */
- void computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match );
+ //void computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match );
+ /** get value */
+ Node getValue( Node var );
/** clear */
void clear(){ d_map.clear(); }
+ /** is_empty */
+ bool empty(){ return d_map.empty(); }
+ /** to stream */
+ inline void toStream(std::ostream& out) const {
+ out << "INST_MATCH( ";
+ for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){
+ if( it != d_map.begin() ){ out << ", "; }
+ out << it->first << " -> " << it->second;
+ }
+ out << " )";
+ }
+
+
+ //for rewrite rules
+
+ /** apply rewrite */
+ void applyRewrite();
/** erase */
template<class Iterator>
void erase(Iterator begin, Iterator end){
};
}
void erase(Node node){ d_map.erase(node); }
- /** is_empty */
- bool empty(){ return d_map.empty(); }
+ /** get */
+ Node get( TNode var ) { return d_map[var]; }
/** set */
void set(TNode var, TNode n){
//std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ;
var.getType() == n.getType() );
d_map[var] = n;
}
- Node get(TNode var){ return d_map[var]; }
size_t size(){ return d_map.size(); }
/* iterator */
std::map< Node, Node >::iterator begin(){ return d_map.begin(); };
/* Node used for matching the trigger only for mono-trigger (just for
efficiency because I need only that) */
Node d_matched;
- /** to stream */
- inline void toStream(std::ostream& out) const {
- out << "INST_MATCH( ";
- for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){
- if( it != d_map.begin() ){ out << ", "; }
- out << it->first << " -> " << it->second;
- }
- out << " )";
- }
};/* class InstMatch */
inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio );
/** exists match */
- bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio );
+ bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio, bool modInst );
public:
/** the data */
std::map< Node, InstMatchTrie > d_data;
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, bool modInst = false );
/** 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 addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
+ ImtIndexOrder* imtio = NULL, bool modInst = false );
};/* class InstMatchTrie */
class InstMatchTrieOrdered {
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/model_builder.h"
#include "theory/quantifiers/quantifiers_attributes.h"
-
-#define RECONSIDER_FUNC_CONSTANT
+#include "theory/quantifiers/inst_gen.h"
using namespace std;
using namespace CVC4;
d_addedLemmas = 0;
//only construct first order model if optUseModel() is true
if( optUseModel() ){
- //initialize model
- fm->initialize( d_considerAxioms );
- //analyze the functions
- Trace("model-engine-debug") << "Analyzing model..." << std::endl;
- analyzeModel( fm );
- //analyze the quantifiers
- Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
- analyzeQuantifiers( fm );
- //if applicable, find exceptions
- if( optInstGen() ){
- //now, see if we know that any exceptions via InstGen exist
- Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
+ if( optUseModel() ){
+ //check if any quantifiers are un-initialized
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
- if( isQuantifierActive( f ) ){
- d_addedLemmas += doInstGen( fm, f );
- if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){
- break;
+ d_addedLemmas += initializeQuantifier( f );
+ }
+ }
+ if( d_addedLemmas>0 ){
+ Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
+ }else{
+ //initialize model
+ fm->initialize( d_considerAxioms );
+ //analyze the functions
+ Trace("model-engine-debug") << "Analyzing model..." << std::endl;
+ analyzeModel( fm );
+ //analyze the quantifiers
+ Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
+ d_quant_sat.clear();
+ d_uf_prefs.clear();
+ analyzeQuantifiers( fm );
+ //if applicable, find exceptions
+ if( optInstGen() ){
+ //now, see if we know that any exceptions via InstGen exist
+ Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
+ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ if( isQuantifierActive( f ) ){
+ d_addedLemmas += doInstGen( fm, f );
+ if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){
+ break;
+ }
}
}
- }
- if( Trace.isOn("model-engine") ){
- if( d_addedLemmas>0 ){
- Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
- }else{
- Trace("model-engine") << "No InstGen lemmas..." << std::endl;
+ if( Trace.isOn("model-engine") ){
+ if( d_addedLemmas>0 ){
+ Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
+ }else{
+ Trace("model-engine") << "No InstGen lemmas..." << std::endl;
+ }
}
}
+ if( d_addedLemmas==0 ){
+ //if no immediate exceptions, build the model
+ // this model will be an approximation that will need to be tested via exhaustive instantiation
+ Trace("model-engine-debug") << "Building model..." << std::endl;
+ constructModel( fm );
+ }
}
- if( d_addedLemmas==0 ){
- //if no immediate exceptions, build the model
- // this model will be an approximation that will need to be tested via exhaustive instantiation
- Trace("model-engine-debug") << "Building model..." << std::endl;
- constructModel( fm );
+ }
+ }
+}
+
+int ModelEngineBuilder::initializeQuantifier( Node f ){
+ if( d_quant_init.find( f )==d_quant_init.end() ){
+ d_quant_init[f] = true;
+ Debug("inst-fmf-init") << "Initialize " << f << std::endl;
+ //add the model basis instantiation
+ // This will help produce the necessary information for model completion.
+ // We do this by extending distinguish ground assertions (those
+ // containing terms with "model basis" attribute) to hold for all cases.
+
+ ////first, check if any variables are required to be equal
+ //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
+ // it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
+ // Node n = it->first;
+ // if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){
+ // Notice() << "Unhandled phase req: " << n << std::endl;
+ // }
+ //}
+ std::vector< Node > vars;
+ std::vector< Node > terms;
+ for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
+ Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, j );
+ Node t = d_qe->getTermDatabase()->getModelBasisTerm( ic.getType() );
+ vars.push_back( f[0][j] );
+ terms.push_back( t );
+ //calculate the basis match for f
+ d_quant_basis_match[f].set( ic, t);
+ }
+ ++(d_statistics.d_num_quants_init);
+ if( optInstGen() ){
+ //add model basis instantiation
+ if( d_qe->addInstantiation( f, vars, terms ) ){
+ return 1;
+ }else{
+ //shouldn't happen usually, but will occur if x != y is a required literal for f.
+ //Notice() << "No model basis for " << f << std::endl;
+ ++(d_statistics.d_num_quants_init_fail);
}
}
}
+ return 0;
}
void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
}
}
-void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){
- d_quant_sat.clear();
- d_quant_selection_lit.clear();
- d_quant_selection_lit_candidates.clear();
- d_quant_selection_lit_terms.clear();
- d_term_selection_lit.clear();
- d_op_selection_terms.clear();
- d_uf_prefs.clear();
- int quantSatInit = 0;
- int nquantSatInit = 0;
- //analyze the preferences of each quantifier
- for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- if( isQuantifierActive( f ) ){
- Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
- //the pro/con preferences for this quantifier
- std::vector< Node > pro_con[2];
- //the terms in the selection literal we choose
- std::vector< Node > selectionLitTerms;
- //for each asserted quantifier f,
- // - determine selection literals
- // - check which function/predicates have good and bad definitions for satisfying f
- for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin();
- it != d_qe->d_phase_reqs[f].end(); ++it ){
- //the literal n is phase-required for quantifier f
- Node n = it->first;
- Node gn = d_qe->getTermDatabase()->getModelBasis( n );
- Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl;
- bool value;
- //if the corresponding ground abstraction literal has a SAT value
- if( d_qe->getValuation().hasSatValue( gn, value ) ){
- //collect the non-ground uf terms that this literal contains
- // and compute if all of the symbols in this literal have
- // constant definitions.
- bool isConst = true;
- std::vector< Node > uf_terms;
- if( n.hasAttribute(InstConstantAttribute()) ){
- isConst = false;
- if( gn.getKind()==APPLY_UF ){
- uf_terms.push_back( gn );
- isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull();
- }else if( gn.getKind()==EQUAL ){
- isConst = true;
- for( int j=0; j<2; j++ ){
- if( n[j].hasAttribute(InstConstantAttribute()) ){
- if( n[j].getKind()==APPLY_UF &&
- fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){
- uf_terms.push_back( gn[j] );
- isConst = isConst && !d_uf_prefs[ gn[j].getOperator() ].d_const_val.isNull();
- }else{
- isConst = false;
- }
- }
- }
- }
- }
- //check if the value in the SAT solver matches the preference according to the quantifier
- int pref = 0;
- if( value!=it->second ){
- //we have a possible selection literal
- bool selectLit = d_quant_selection_lit[f].isNull();
- bool selectLitConstraints = true;
- //it is a constantly defined selection literal : the quantifier is sat
- if( isConst ){
- selectLit = selectLit || d_quant_sat.find( f )==d_quant_sat.end();
- d_quant_sat[f] = true;
- //check if choosing this literal would add any additional constraints to default definitions
- selectLitConstraints = false;
- for( int j=0; j<(int)uf_terms.size(); j++ ){
- Node op = uf_terms[j].getOperator();
- if( d_uf_prefs[op].d_reconsiderModel ){
- selectLitConstraints = true;
- }
- }
- if( !selectLitConstraints ){
- selectLit = true;
- }
- }
- //see if we wish to choose this as a selection literal
- d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() );
- if( selectLit ){
- Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl;
- d_quant_selection_lit[f] = value ? n : n.notNode();
- selectionLitTerms.clear();
- selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() );
- if( !selectLitConstraints ){
- break;
- }
- }
- pref = 1;
- }else{
- pref = -1;
- }
- //if we are not yet SAT, so we will add to preferences
- if( d_quant_sat.find( f )==d_quant_sat.end() ){
- Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" );
- Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
- for( int j=0; j<(int)uf_terms.size(); j++ ){
- pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] );
- }
- }
- }
- }
- //process information about selection literal for f
- if( !d_quant_selection_lit[f].isNull() ){
- d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() );
- for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
- d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f];
- d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] );
- }
- }else{
- Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals (is the body of f clausified?)" << std::endl;
- }
- //process information about requirements and preferences of quantifier f
- if( d_quant_sat.find( f )!=d_quant_sat.end() ){
- Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: ";
- for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
- Debug("fmf-model-prefs") << selectionLitTerms[i] << " ";
- d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false;
- }
- Debug("fmf-model-prefs") << std::endl;
- quantSatInit++;
- ++(d_statistics.d_pre_sat_quant);
- }else{
- nquantSatInit++;
- ++(d_statistics.d_pre_nsat_quant);
- //note quantifier's value preferences to models
- for( int k=0; k<2; k++ ){
- for( int j=0; j<(int)pro_con[k].size(); j++ ){
- Node op = pro_con[k][j].getOperator();
- Node r = fm->getRepresentative( pro_con[k][j] );
- d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
- }
- }
- }
- }
- }
- Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl;
-}
-
-int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){
- int addedLemmas = 0;
- //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
- //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
- // effectively acting as partial instantiations instead of pointwise instantiations.
- if( !d_quant_selection_lit[f].isNull() ){
- Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl;
- for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){
- bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT;
- Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i];
- Assert( lit.hasAttribute(InstConstantAttribute()) );
- std::vector< Node > tr_terms;
- if( lit.getKind()==APPLY_UF ){
- //only match predicates that are contrary to this one, use literal matching
- Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
- d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f );
- tr_terms.push_back( eq );
- }else if( lit.getKind()==EQUAL ){
- //collect trigger terms
- for( int j=0; j<2; j++ ){
- if( lit[j].hasAttribute(InstConstantAttribute()) ){
- if( lit[j].getKind()==APPLY_UF ){
- tr_terms.push_back( lit[j] );
- }else{
- tr_terms.clear();
- break;
- }
- }
- }
- if( tr_terms.size()==1 && !phase ){
- //equality between a function and a ground term, use literal matching
- tr_terms.clear();
- tr_terms.push_back( lit );
- }
- }
- //if applicable, try to add exceptions here
- if( !tr_terms.empty() ){
- //make a trigger for these terms, add instantiations
- inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms );
- //Notice() << "Trigger = " << (*tr) << std::endl;
- tr->resetInstantiationRound();
- tr->reset( Node::null() );
- //d_qe->d_optInstMakeRepresentative = false;
- //d_qe->d_optMatchIgnoreModelBasis = true;
- addedLemmas += tr->addInstantiations( d_quant_basis_match[f] );
- }
- }
- }
- return addedLemmas;
-}
-
void ModelEngineBuilder::constructModel( FirstOrderModel* fm ){
//build model for UF
for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
}
void ModelEngineBuilder::constructModelUf( FirstOrderModel* fm, Node op ){
-#ifdef RECONSIDER_FUNC_CONSTANT
- if( d_uf_model_constructed[op] ){
- if( d_uf_prefs[op].d_reconsiderModel ){
- //if we are allowed to reconsider default value, then see if the default value can be improved
- Node v = d_uf_prefs[op].d_const_val;
- if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){
- Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl;
- fm->d_uf_model_tree[op].clear();
- fm->d_uf_model_gen[op].clear();
- d_uf_model_constructed[op] = false;
+ if( optReconsiderFuncConstants() ){
+ //reconsider constant functions that weren't necessary
+ if( d_uf_model_constructed[op] ){
+ if( d_uf_prefs[op].d_reconsiderModel ){
+ //if we are allowed to reconsider default value, then see if the default value can be improved
+ Node v = d_uf_prefs[op].d_const_val;
+ if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){
+ Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl;
+ fm->d_uf_model_tree[op].clear();
+ fm->d_uf_model_gen[op].clear();
+ d_uf_model_constructed[op] = false;
+ }
}
}
}
-#endif
if( !d_uf_model_constructed[op] ){
//construct the model for the uninterpretted function/predicate
bool setDefaultVal = true;
//set the values in the model
for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
Node n = fm->d_uf_terms[op][i];
- d_qe->getTermDatabase()->computeModelBasisArgAttribute( n );
if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
Node v = fm->getRepresentative( n );
//if this assertion did not help the model, just consider it ground
if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){
//also set as default value if necessary
//if( n.getAttribute(ModelBasisArgAttribute())==1 && !d_term_pro_con[0][n].empty() ){
- if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){
+ if( shouldSetDefaultValue( n ) ){
fm->d_uf_model_gen[op].setValue( fm, n, v, false );
if( n==defaultTerm ){
//incidentally already set, we will not need to find a default value
return options::fmfInstGenOneQuantPerRound();
}
+bool ModelEngineBuilder::optReconsiderFuncConstants(){
+ return false;
+}
+
void ModelEngineBuilder::setEffort( int effort ){
d_considerAxioms = effort>=1;
}
ModelEngineBuilder::Statistics::Statistics():
d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0),
- d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0)
+ d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0),
+ d_num_quants_init("ModelEngine::Num_Quants", 0 ),
+ d_num_quants_init_fail("ModelEngine::Num_Quants_No_Basis", 0 )
{
StatisticsRegistry::registerStat(&d_pre_sat_quant);
StatisticsRegistry::registerStat(&d_pre_nsat_quant);
+ StatisticsRegistry::registerStat(&d_num_quants_init);
+ StatisticsRegistry::registerStat(&d_num_quants_init_fail);
}
ModelEngineBuilder::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_pre_sat_quant);
StatisticsRegistry::unregisterStat(&d_pre_nsat_quant);
+ StatisticsRegistry::unregisterStat(&d_num_quants_init);
+ StatisticsRegistry::unregisterStat(&d_num_quants_init_fail);
}
bool ModelEngineBuilder::isQuantifierActive( Node f ){
return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end();
}
+
+
+
+
+
+void ModelEngineBuilderDefault::analyzeQuantifiers( FirstOrderModel* fm ){
+ d_quant_selection_lit.clear();
+ d_quant_selection_lit_candidates.clear();
+ d_quant_selection_lit_terms.clear();
+ d_term_selection_lit.clear();
+ d_op_selection_terms.clear();
+ //analyze each quantifier
+ for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ if( isQuantifierActive( f ) ){
+ analyzeQuantifier( fm, f );
+ }
+ }
+}
+
+
+void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
+ Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
+ //the pro/con preferences for this quantifier
+ std::vector< Node > pro_con[2];
+ //the terms in the selection literal we choose
+ std::vector< Node > selectionLitTerms;
+ //for each asserted quantifier f,
+ // - determine selection literals
+ // - check which function/predicates have good and bad definitions for satisfying f
+ for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin();
+ it != d_qe->d_phase_reqs[f].end(); ++it ){
+ //the literal n is phase-required for quantifier f
+ Node n = it->first;
+ Node gn = d_qe->getTermDatabase()->getModelBasis( f, n );
+ Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl;
+ bool value;
+ //if the corresponding ground abstraction literal has a SAT value
+ if( d_qe->getValuation().hasSatValue( gn, value ) ){
+ //collect the non-ground uf terms that this literal contains
+ // and compute if all of the symbols in this literal have
+ // constant definitions.
+ bool isConst = true;
+ std::vector< Node > uf_terms;
+ if( n.hasAttribute(InstConstantAttribute()) ){
+ isConst = false;
+ if( gn.getKind()==APPLY_UF ){
+ uf_terms.push_back( gn );
+ isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull();
+ }else if( gn.getKind()==EQUAL ){
+ isConst = true;
+ for( int j=0; j<2; j++ ){
+ if( n[j].hasAttribute(InstConstantAttribute()) ){
+ if( n[j].getKind()==APPLY_UF &&
+ fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){
+ uf_terms.push_back( gn[j] );
+ isConst = isConst && !d_uf_prefs[ gn[j].getOperator() ].d_const_val.isNull();
+ }else{
+ isConst = false;
+ }
+ }
+ }
+ }
+ }
+ //check if the value in the SAT solver matches the preference according to the quantifier
+ int pref = 0;
+ if( value!=it->second ){
+ //we have a possible selection literal
+ bool selectLit = d_quant_selection_lit[f].isNull();
+ bool selectLitConstraints = true;
+ //it is a constantly defined selection literal : the quantifier is sat
+ if( isConst ){
+ selectLit = selectLit || d_quant_sat.find( f )==d_quant_sat.end();
+ d_quant_sat[f] = true;
+ //check if choosing this literal would add any additional constraints to default definitions
+ selectLitConstraints = false;
+ for( int j=0; j<(int)uf_terms.size(); j++ ){
+ Node op = uf_terms[j].getOperator();
+ if( d_uf_prefs[op].d_reconsiderModel ){
+ selectLitConstraints = true;
+ }
+ }
+ if( !selectLitConstraints ){
+ selectLit = true;
+ }
+ }
+ //see if we wish to choose this as a selection literal
+ d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() );
+ if( selectLit ){
+ Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl;
+ d_quant_selection_lit[f] = value ? n : n.notNode();
+ selectionLitTerms.clear();
+ selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() );
+ if( !selectLitConstraints ){
+ break;
+ }
+ }
+ pref = 1;
+ }else{
+ pref = -1;
+ }
+ //if we are not yet SAT, so we will add to preferences
+ if( d_quant_sat.find( f )==d_quant_sat.end() ){
+ Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" );
+ Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
+ for( int j=0; j<(int)uf_terms.size(); j++ ){
+ pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] );
+ }
+ }
+ }
+ }
+ //process information about selection literal for f
+ if( !d_quant_selection_lit[f].isNull() ){
+ d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() );
+ for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
+ d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f];
+ d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] );
+ }
+ }else{
+ Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals (is the body of f clausified?)" << std::endl;
+ }
+ //process information about requirements and preferences of quantifier f
+ if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+ Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: ";
+ for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
+ Debug("fmf-model-prefs") << selectionLitTerms[i] << " ";
+ d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false;
+ }
+ Debug("fmf-model-prefs") << std::endl;
+ ++(d_statistics.d_pre_sat_quant);
+ }else{
+ ++(d_statistics.d_pre_nsat_quant);
+ //note quantifier's value preferences to models
+ for( int k=0; k<2; k++ ){
+ for( int j=0; j<(int)pro_con[k].size(); j++ ){
+ Node op = pro_con[k][j].getOperator();
+ Node r = fm->getRepresentative( pro_con[k][j] );
+ d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
+ }
+ }
+ }
+}
+
+int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
+ int addedLemmas = 0;
+ //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
+ //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
+ // effectively acting as partial instantiations instead of pointwise instantiations.
+ if( !d_quant_selection_lit[f].isNull() ){
+ Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl;
+ for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){
+ bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT;
+ Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i];
+ Assert( lit.hasAttribute(InstConstantAttribute()) );
+ std::vector< Node > tr_terms;
+ if( lit.getKind()==APPLY_UF ){
+ //only match predicates that are contrary to this one, use literal matching
+ Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
+ d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f );
+ tr_terms.push_back( eq );
+ }else if( lit.getKind()==EQUAL ){
+ //collect trigger terms
+ for( int j=0; j<2; j++ ){
+ if( lit[j].hasAttribute(InstConstantAttribute()) ){
+ if( lit[j].getKind()==APPLY_UF ){
+ tr_terms.push_back( lit[j] );
+ }else{
+ tr_terms.clear();
+ break;
+ }
+ }
+ }
+ if( tr_terms.size()==1 && !phase ){
+ //equality between a function and a ground term, use literal matching
+ tr_terms.clear();
+ tr_terms.push_back( lit );
+ }
+ }
+ //if applicable, try to add exceptions here
+ if( !tr_terms.empty() ){
+ //make a trigger for these terms, add instantiations
+ inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms );
+ //Notice() << "Trigger = " << (*tr) << std::endl;
+ tr->resetInstantiationRound();
+ tr->reset( Node::null() );
+ //d_qe->d_optInstMakeRepresentative = false;
+ //d_qe->d_optMatchIgnoreModelBasis = true;
+ addedLemmas += tr->addInstantiations( d_quant_basis_match[f] );
+ }
+ }
+ }
+ return addedLemmas;
+}
+
+bool ModelEngineBuilderDefault::shouldSetDefaultValue( Node n ){
+ return n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1;
+}
+
+
+
+
+
+void ModelEngineBuilderInstGen::analyzeQuantifiers( FirstOrderModel* fm ){
+ //for new inst gen
+ d_quant_selection_formula.clear();
+ d_term_selected.clear();
+ //analyze each quantifier
+ for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ if( isQuantifierActive( f ) ){
+ analyzeQuantifier( fm, f );
+ }
+ }
+ //analyze each partially instantiated quantifier
+ for( std::map< Node, Node >::iterator it = d_sub_quant_parent.begin(); it != d_sub_quant_parent.end(); ++it ){
+ Node fp = getParentQuantifier( it->first );
+ if( isQuantifierActive( fp ) ){
+ analyzeQuantifier( fm, it->first );
+ }
+ }
+}
+
+void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){
+ //determine selection formula, set terms in selection formula as being selected
+ Node s = getSelectionFormula( d_qe->getTermDatabase()->getCounterexampleBody( f ),
+ d_qe->getTermDatabase()->getModelBasisBody( f ), true, 0 );
+ Trace("sel-form") << "Selection formula for " << f << " is " << s << std::endl;
+ if( !s.isNull() ){
+ d_quant_selection_formula[f] = s;
+ Node gs = d_qe->getTermDatabase()->getModelBasis( f, s );
+ setSelectedTerms( gs );
+ }
+}
+
+
+int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
+ int addedLemmas = 0;
+ //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
+ //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
+ // effectively acting as partial instantiations instead of pointwise instantiations.
+ if( !d_quant_selection_formula[f].isNull() ){
+ //first, try on sub quantifiers
+ for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
+ addedLemmas += doInstGen( fm, d_sub_quants[f][i] );
+ }
+ if( addedLemmas>0 ){
+ return addedLemmas;
+ }else{
+ Node fp = getParentQuantifier( f );
+ Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl;
+ Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl;
+ //get all possible values of selection formula
+ InstGenProcess igp( d_quant_selection_formula[f] );
+ igp.calculateMatches( d_qe, f );
+ Trace("inst-gen-debug") << "Add inst-gen instantiations..." << std::endl;
+ for( int i=0; i<igp.getNumMatches(); i++ ){
+ //if the match is not already true in the model
+ if( igp.getMatchValue( i )!=fm->d_true ){
+ InstMatch m;
+ igp.getMatch( d_qe->getEqualityQuery(), i, m );
+ //we only consider matches that are non-empty
+ // matches that are empty should trigger other instances that are non-empty
+ if( !m.empty() ){
+ bool addInst = false;
+ //translate to be in terms match in terms of fp
+ InstMatch mp;
+ getParentQuantifierMatch( mp, fp, m, f );
+
+ //if this is a partial instantion
+ if( !m.isComplete( f ) ){
+ Trace("inst-gen-debug") << "- partial inst" << std::endl;
+ //if the instantiation does not yet exist
+ if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true, NULL ) ){
+ //get the partial instantiation pf
+ Node pf = d_qe->getInstantiation( fp, mp );
+ Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl;
+ Trace("inst-gen-pi") << " " << pf << std::endl;
+ d_sub_quants[ f ].push_back( pf );
+ d_sub_quant_inst[ pf ] = InstMatch( &mp );
+ d_sub_quant_parent[ pf ] = fp;
+ mp.add( d_quant_basis_match[ fp ] );
+ addInst = true;
+ }
+ }else{
+ addInst = true;
+ }
+ if( addInst ){
+ Trace("inst-gen-debug") << "- complete inst" << std::endl;
+ //otherwise, get instantiation and add ground instantiation in terms of root parent
+ if( d_qe->addInstantiation( fp, mp ) ){
+ addedLemmas++;
+ }
+ }
+ }
+ }
+ }
+ if( addedLemmas==0 ){
+ //all sub quantifiers must be satisfied as well
+ bool subQuantSat = true;
+ for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
+ if( d_quant_sat.find( d_sub_quants[f][i] )==d_quant_sat.end() ){
+ subQuantSat = false;
+ break;
+ }
+ }
+ if( subQuantSat ){
+ d_quant_sat[ f ] = true;
+ }
+ }
+ Trace("inst-gen") << " -> added lemmas = " << addedLemmas << std::endl;
+ }
+ }
+ return addedLemmas;
+}
+
+bool ModelEngineBuilderInstGen::shouldSetDefaultValue( Node n ){
+ return d_term_selected.find( n )!=d_term_selected.end();
+}
+
+//if possible, returns a formula n' such that ( n' <=> polarity ) => ( n <=> polarity ), and ( n' <=> polarity ) is true in the current context,
+// and NULL otherwise
+Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){
+ if( n.getKind()==NOT ){
+ Node nn = getSelectionFormula( fn[0], n[0], !polarity, useOption );
+ if( !nn.isNull() ){
+ return nn.negate();
+ }
+ }else if( n.getKind()==OR || n.getKind()==IMPLIES || n.getKind()==AND ){
+ //whether we only need to find one or all
+ bool posPol = (( n.getKind()==OR || n.getKind()==IMPLIES ) && polarity ) || ( n.getKind()==AND && !polarity );
+ std::vector< Node > children;
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ Node fnc = ( i==0 && fn.getKind()==IMPLIES ) ? fn[i].negate() : fn[i];
+ Node nc = ( i==0 && n.getKind()==IMPLIES ) ? n[i].negate() : n[i];
+ Node nn = getSelectionFormula( fnc, nc, polarity, useOption );
+ if( nn.isNull()!=posPol ){ //TODO: may want to weaken selection formula
+ return nn;
+ }
+ children.push_back( nn );
+ }
+ if( !posPol ){
+ return NodeManager::currentNM()->mkNode( n.getKind()==AND ? AND : OR, children );
+ }
+ }else if( n.getKind()==ITE ){
+ Node nn;
+ Node nc[2];
+ //get selection formula for the
+ for( int i=0; i<2; i++ ){
+ nn = getSelectionFormula( i==0 ? fn[0] : fn[0].negate(), i==0 ? n[0] : n[0].negate(), true, useOption );
+ nc[i] = getSelectionFormula( fn[i+1], n[i+1], polarity, useOption );
+ if( !nn.isNull() && !nc[i].isNull() ){
+ return NodeManager::currentNM()->mkNode( AND, nn, nc[i] );
+ }
+ }
+ if( !nc[0].isNull() && !nc[1].isNull() ){
+ return NodeManager::currentNM()->mkNode( AND, nc[0], nc[1] );
+ }
+ }else if( n.getKind()==IFF || n.getKind()==XOR ){
+ bool opPol = polarity ? n.getKind()==XOR : n.getKind()==IFF;
+ for( int p=0; p<2; p++ ){
+ Node nn[2];
+ for( int i=0; i<2; i++ ){
+ bool pol = i==0 ? p==0 : ( opPol ? p!=0 : p==0 );
+ nn[i] = getSelectionFormula( pol ? fn[i] : fn[i].negate(), pol ? n[i] : n[i].negate(), true, useOption );
+ if( nn[i].isNull() ){
+ break;
+ }
+ }
+ if( !nn[0].isNull() && !nn[1].isNull() ){
+ return NodeManager::currentNM()->mkNode( AND, nn[0], nn[1] );
+ }
+ }
+ }else{
+ //literal case
+ //first, check if it is a usable selection literal
+ if( isUsableSelectionLiteral( n, useOption ) ){
+ bool value;
+ if( d_qe->getValuation().hasSatValue( n, value ) ){
+ if( value==polarity ){
+ return fn;
+ }
+ }
+ }
+ }
+ return Node::null();
+}
+
+void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){
+
+ //if it is apply uf and has model basis arguments, then mark term as being "selected"
+ if( s.getKind()==APPLY_UF ){
+ Assert( s.hasAttribute(ModelBasisArgAttribute()) );
+ if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl;
+ if( s.getAttribute(ModelBasisArgAttribute())==1 ){
+ d_term_selected[ s ] = true;
+ Trace("sel-form") << " " << s << " is a selected term." << std::endl;
+ }
+ }
+ for( int i=0; i<(int)s.getNumChildren(); i++ ){
+ setSelectedTerms( s[i] );
+ }
+}
+
+bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){
+ if( n.getKind()==FORALL ){
+ return false;
+ }else if( n.getKind()!=APPLY_UF ){
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ //if it is a variable, then return false
+ if( n[i].getAttribute(ModelBasisAttribute()) ){
+ return false;
+ }
+ }
+ }
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( !isUsableSelectionLiteral( n[i], useOption ) ){
+ return false;
+ }
+ }
+ return true;
+}
+
+Node ModelEngineBuilderInstGen::getParentQuantifier( Node f ){
+ std::map< Node, Node >::iterator it = d_sub_quant_parent.find( f );
+ if( it==d_sub_quant_parent.end() ){
+ return f;
+ }else{
+ return getParentQuantifier( it->second );
+ }
+}
+
+void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){
+ int counter = 0;
+ for( size_t i=0; i<fp[0].getNumChildren(); i++ ){
+ Node icp = d_qe->getTermDatabase()->getInstantiationConstant( fp, i );
+ if( fp[0][i]==f[0][counter] ){
+ Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, counter );
+ Node n = m.getValue( ic );
+ if( !n.isNull() ){
+ mp.setMatch( d_qe->getEqualityQuery(), icp, n );
+ }
+ counter++;
+ }
+ }
+ mp.add( d_sub_quant_inst[f] );
+}
+
/** process build model */
void processBuildModel( TheoryModel* m, bool fullModel );
protected:
+ //initialize quantifiers, return number of lemmas produced
+ int initializeQuantifier( Node f );
//analyze model
void analyzeModel( FirstOrderModel* fm );
//analyze quantifiers
- void analyzeQuantifiers( FirstOrderModel* fm );
+ virtual void analyzeQuantifiers( FirstOrderModel* fm ) = 0;
//build model
void constructModel( FirstOrderModel* fm );
//theory-specific build models
void constructModelUf( FirstOrderModel* fm, Node op );
+ /** set default value */
+ virtual bool shouldSetDefaultValue( Node n ) = 0;
//do InstGen techniques for quantifier, return number of lemmas produced
- int doInstGen( FirstOrderModel* fm, Node f );
+ virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0;
+protected:
+ //map from quantifiers to if are SAT
+ std::map< Node, bool > d_quant_sat;
+ //which quantifiers have been initialized
+ std::map< Node, bool > d_quant_init;
+ //map from quantifiers to model basis match
+ std::map< Node, InstMatch > d_quant_basis_match;
public:
ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe );
virtual ~ModelEngineBuilder(){}
int d_addedLemmas;
//consider axioms
bool d_considerAxioms;
-private: ///information for InstGen
- //map from quantifiers to if are constant SAT
- std::map< Node, bool > d_quant_sat;
- //map from quantifiers to their selection literals
- std::map< Node, Node > d_quant_selection_lit;
- std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates;
- //map from quantifiers to their selection literal terms
- std::map< Node, std::vector< Node > > d_quant_selection_lit_terms;
- //map from terms to the selection literals they exist in
- std::map< Node, Node > d_term_selection_lit;
- //map from operators to terms that appear in selection literals
- std::map< Node, std::vector< Node > > d_op_selection_terms;
-public:
- //map from quantifiers to model basis match
- std::map< Node, InstMatch > d_quant_basis_match;
- //options
- bool optUseModel();
- bool optInstGen();
- bool optOneQuantPerRoundInstGen();
// set effort
void setEffort( int effort );
+public:
+ //options
+ virtual bool optUseModel();
+ virtual bool optInstGen();
+ virtual bool optOneQuantPerRoundInstGen();
+ virtual bool optReconsiderFuncConstants();
/** statistics class */
class Statistics {
public:
IntStat d_pre_sat_quant;
IntStat d_pre_nsat_quant;
+ IntStat d_num_quants_init;
+ IntStat d_num_quants_init_fail;
Statistics();
~Statistics();
};
Statistics d_statistics;
// is quantifier active?
bool isQuantifierActive( Node f );
+ // is term selected
+ virtual bool isTermSelected( Node n ) { return false; }
};/* class ModelEngineBuilder */
+
+class ModelEngineBuilderDefault : public ModelEngineBuilder
+{
+private: ///information for (old) InstGen
+ //map from quantifiers to their selection literals
+ std::map< Node, Node > d_quant_selection_lit;
+ std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates;
+ //map from quantifiers to their selection literal terms
+ std::map< Node, std::vector< Node > > d_quant_selection_lit_terms;
+ //map from terms to the selection literals they exist in
+ std::map< Node, Node > d_term_selection_lit;
+ //map from operators to terms that appear in selection literals
+ std::map< Node, std::vector< Node > > d_op_selection_terms;
+protected:
+ //analyze quantifiers
+ void analyzeQuantifiers( FirstOrderModel* fm );
+ //do InstGen techniques for quantifier, return number of lemmas produced
+ int doInstGen( FirstOrderModel* fm, Node f );
+ /** set default value */
+ bool shouldSetDefaultValue( Node n );
+private:
+ //analyze quantifier
+ void analyzeQuantifier( FirstOrderModel* fm, Node f );
+public:
+ ModelEngineBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){}
+ ~ModelEngineBuilderDefault(){}
+ //options
+ bool optReconsiderFuncConstants() { return true; }
+};
+
+class ModelEngineBuilderInstGen : public ModelEngineBuilder
+{
+private: ///information for (new) InstGen
+ //map from quantifiers to their selection literals
+ std::map< Node, Node > d_quant_selection_formula;
+ //map of terms that are selected
+ std::map< Node, bool > d_term_selected;
+ //a collection of InstMatch structures produced for each quantifier
+ std::map< Node, inst::InstMatchTrie > d_sub_quant_inst_trie;
+ //children quantifiers for each quantifier, each is an instance
+ std::map< Node, std::vector< Node > > d_sub_quants;
+ //instances of each partial instantiation with respect to the root
+ std::map< Node, InstMatch > d_sub_quant_inst;
+ //*root* parent of each partial instantiation
+ std::map< Node, Node > d_sub_quant_parent;
+protected:
+ //analyze quantifiers
+ void analyzeQuantifiers( FirstOrderModel* fm );
+ //do InstGen techniques for quantifier, return number of lemmas produced
+ int doInstGen( FirstOrderModel* fm, Node f );
+ /** set default value */
+ bool shouldSetDefaultValue( Node n );
+private:
+ //analyze quantifier
+ void analyzeQuantifier( FirstOrderModel* fm, Node f );
+ //get selection formula for quantifier body
+ Node getSelectionFormula( Node fn, Node n, bool polarity, int useOption );
+ //set selected terms in term
+ void setSelectedTerms( Node s );
+ //is usable selection literal
+ bool isUsableSelectionLiteral( Node n, int useOption );
+ // get parent quantifier
+ Node getParentQuantifier( Node f );
+ //get parent quantifier match
+ void getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f );
+public:
+ ModelEngineBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){}
+ ~ModelEngineBuilderInstGen(){}
+ // is term selected
+ bool isTermSelected( Node n ) { return d_term_selected.find( n )!=d_term_selected.end(); }
+};
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
//Model Engine constructor
ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
QuantifiersModule( qe ),
-d_builder( c, qe ),
d_rel_domain( qe, qe->getModel() ){
+ if( options::fmfNewInstGen() ){
+ d_builder = new ModelEngineBuilderInstGen( c, qe );
+ }else{
+ d_builder = new ModelEngineBuilderDefault( c, qe );
+ }
+
}
void ModelEngine::check( Theory::Effort e ){
//the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
int addedLemmas = 0;
Trace("model-engine") << "---Model Engine Round---" << std::endl;
- if( d_builder.optUseModel() ){
- //check if any quantifiers are un-initialized
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- addedLemmas += initializeQuantifier( f );
- }
- }
- if( addedLemmas>0 ){
- Trace("model-engine") << "Initialize, Added Lemmas = " << addedLemmas << std::endl;
- }
//two effort levels: first try exhaustive instantiation without axioms, then with.
int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
for( int effort=startEffort; effort<2; effort++ ){
d_quantEngine->resetInstantiationRound( e );
//initialize the model
Trace("model-engine-debug") << "Build model..." << std::endl;
- d_builder.setEffort( effort );
- d_builder.buildModel( fm, false );
+ d_builder->setEffort( effort );
+ d_builder->buildModel( fm, false );
//if builder has lemmas, add and return
- if( d_builder.d_addedLemmas>0 ){
- addedLemmas += (int)d_builder.d_addedLemmas;
+ if( d_builder->d_addedLemmas>0 ){
+ addedLemmas += (int)d_builder->d_addedLemmas;
}else{
Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
//let the strong solver verify that the model is minimal
checkModel( addedLemmas );
//print debug information
if( Trace.isOn("model-engine") ){
- Trace("model-engine") << "Instantiate axioms : " << ( d_builder.d_considerAxioms ? "yes" : "no" ) << std::endl;
+ Trace("model-engine") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
debugPrint("fmf-consistent");
if( options::produceModels() ){
// finish building the model in the standard way
- d_builder.buildModel( fm, true );
+ d_builder->buildModel( fm, true );
d_quantEngine->d_model_set = true;
}
//if the check was incomplete, we must set incomplete flag
#endif
}
-int ModelEngine::initializeQuantifier( Node f ){
- if( d_quant_init.find( f )==d_quant_init.end() ){
- d_quant_init[f] = true;
- Debug("inst-fmf-init") << "Initialize " << f << std::endl;
- //add the model basis instantiation
- // This will help produce the necessary information for model completion.
- // We do this by extending distinguish ground assertions (those
- // containing terms with "model basis" attribute) to hold for all cases.
-
- ////first, check if any variables are required to be equal
- //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
- // it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
- // Node n = it->first;
- // if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){
- // Notice() << "Unhandled phase req: " << n << std::endl;
- // }
- //}
- std::vector< Node > vars;
- std::vector< Node > ics;
- std::vector< Node > terms;
- for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
- Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
- Node t = d_quantEngine->getTermDatabase()->getModelBasisTerm( ic.getType() );
- vars.push_back( f[0][j] );
- ics.push_back( ic );
- terms.push_back( t );
- //calculate the basis match for f
- d_builder.d_quant_basis_match[f].set( ic, t);
- }
- ++(d_statistics.d_num_quants_init);
- //register model basis body
- Node n = d_quantEngine->getTermDatabase()->getCounterexampleBody( f );
- Node gn = n.substitute( ics.begin(), ics.end(), terms.begin(), terms.end() );
- d_quantEngine->getTermDatabase()->registerModelBasis( n, gn );
- if( d_builder.optInstGen() ){
- //add model basis instantiation
- if( d_quantEngine->addInstantiation( f, vars, terms ) ){
- return 1;
- }else{
- //shouldn't happen usually, but will occur if x != y is a required literal for f.
- //Notice() << "No model basis for " << f << std::endl;
- ++(d_statistics.d_num_quants_init_fail);
- }
- }
- }
- return 0;
-}
-
void ModelEngine::checkModel( int& addedLemmas ){
FirstOrderModel* fm = d_quantEngine->getModel();
//for debugging
}
d_totalLemmas += totalInst;
//if we need to consider this quantifier on this iteration
- if( d_builder.isQuantifierActive( f ) ){
+ if( d_builder->isQuantifierActive( f ) ){
//debug printing
Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl;
if( useRelInstDomain ){
d_testLemmas++;
int eval = 0;
int depIndex;
- if( d_builder.optUseModel() ){
+ if( d_builder->optUseModel() ){
//see if instantiation is already true in current model
Debug("fmf-model-eval") << "Evaluating ";
riter.debugPrintSmall("fmf-model-eval");
for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
Trace( c ) << " ";
- if( !d_builder.isQuantifierActive( f ) ){
+ if( !d_builder->isQuantifierActive( f ) ){
Trace( c ) << "*Inactive* ";
}else{
Trace( c ) << " ";
d_eval_formulas("ModelEngine::Eval_Formulas", 0 ),
d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ),
d_eval_lits("ModelEngine::Eval_Lits", 0 ),
- d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ),
- d_num_quants_init("ModelEngine::Num_Quants", 0 ),
- d_num_quants_init_fail("ModelEngine::Num_Quants_No_Basis", 0 )
+ d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 )
{
StatisticsRegistry::registerStat(&d_inst_rounds);
StatisticsRegistry::registerStat(&d_eval_formulas);
StatisticsRegistry::registerStat(&d_eval_uf_terms);
StatisticsRegistry::registerStat(&d_eval_lits);
StatisticsRegistry::registerStat(&d_eval_lits_unknown);
- StatisticsRegistry::registerStat(&d_num_quants_init);
- StatisticsRegistry::registerStat(&d_num_quants_init_fail);
}
ModelEngine::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
StatisticsRegistry::unregisterStat(&d_eval_lits);
StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
- StatisticsRegistry::unregisterStat(&d_num_quants_init);
- StatisticsRegistry::unregisterStat(&d_num_quants_init_fail);
}
friend class RepSetIterator;
private:
/** builder class */
- ModelEngineBuilder d_builder;
-private: //data maintained globally:
- //which quantifiers have been initialized
- std::map< Node, bool > d_quant_init;
+ ModelEngineBuilder* d_builder;
private: //analysis of current model:
//relevant domain
RelevantDomain d_rel_domain;
bool optOneQuantPerRound();
bool optExhInstEvalSkipMultiple();
private:
- //initialize quantifiers, return number of lemmas produced
- int initializeQuantifier( Node f );
//check model
void checkModel( int& addedLemmas );
//exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
public:
ModelEngine( context::Context* c, QuantifiersEngine* qe );
~ModelEngine(){}
+ //get the builder
+ ModelEngineBuilder* getModelBuilder() { return d_builder; }
public:
void check( Theory::Effort e );
void registerQuantifier( Node f );
IntStat d_eval_uf_terms;
IntStat d_eval_lits;
IntStat d_eval_lits_unknown;
- IntStat d_num_quants_init;
- IntStat d_num_quants_init_fail;
Statistics();
~Statistics();
};
use instantiation engine in conjunction with finite model finding
option fmfRelevantDomain --fmf-relevant-domain bool :default false
use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
+option fmfNewInstGen --fmf-new-inst-gen bool :default false
+ use new inst gen technique for answering sat without exhaustive instantiation
option fmfInstGen /--disable-fmf-inst-gen bool :default true
disable Inst-Gen instantiation techniques for finite model finding
option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
#include "theory/uf/theory_uf_instantiator.h"
#include "theory/theory_engine.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/options.h"
using namespace std;
using namespace CVC4;
d_func_map_trie[ it->first ].d_data.clear();
for( int i=0; i<(int)it->second.size(); i++ ){
Node n = it->second[i];
+ computeModelBasisArgAttribute( n );
if( !n.getAttribute(NoMatchAttribute()) ){
if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){
+ //only set no match if not a model basis argument term
NoMatchAttribute nma;
n.setAttribute(nma,true);
congruentCount++;
d_quantEngine->getEqualityQuery()->getEngine() );
while( !eqc.isFinished() ){
Node en = (*eqc);
+ computeModelBasisArgAttribute( en );
if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){
if( !en.getAttribute(NoMatchAttribute()) ){
Node op = en.getOperator();
if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
+ //only set no match if not a model basis argument term
NoMatchAttribute nma;
en.setAttribute(nma,true);
congruentCount++;
Debug("term-db-cong") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << std::endl;
}
-void TermDb::registerModelBasis( Node n, Node gn ){
- if( d_model_basis.find( n )==d_model_basis.end() ){
- d_model_basis[n] = gn;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- registerModelBasis( n[i], gn[i] );
- }
- }
-}
-
Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
Node mbt;
- if( d_type_map[ tn ].empty() ){
+ if( d_type_map[ tn ].empty() || options::fmfNewInstGen() ){
std::stringstream ss;
ss << Expr::setlanguage(options::outputLanguage());
ss << "e_" << tn;
return d_model_basis_op_term[op];
}
+Node TermDb::getModelBasis( Node f, Node n ){
+ //make model basis
+ if( d_model_basis_terms.find( f )==d_model_basis_terms.end() ){
+ for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
+ d_model_basis_terms[f].push_back( getModelBasisTerm( f[0][j].getType() ) );
+ }
+ }
+ Node gn = n.substitute( d_inst_constants[f].begin(), d_inst_constants[f].end(),
+ d_model_basis_terms[f].begin(), d_model_basis_terms[f].end() );
+ return gn;
+}
+
+Node TermDb::getModelBasisBody( Node f ){
+ if( d_model_basis_body.find( f )==d_model_basis_body.end() ){
+ Node n = getCounterexampleBody( f );
+ d_model_basis_body[f] = getModelBasis( f, n );
+ }
+ return d_model_basis_body[f];
+}
+
void TermDb::computeModelBasisArgAttribute( Node n ){
if( !n.hasAttribute(ModelBasisArgAttribute()) ){
+ //ensure that the model basis terms have been defined
+ if( n.getKind()==APPLY_UF ){
+ getModelBasisOpTerm( n.getOperator() );
+ }
uint64_t val = 0;
//determine if it has model basis attribute
for( int j=0; j<(int)n.getNumChildren(); j++ ){
//map from ops to model basis terms
std::map< Node, Node > d_model_basis_op_term;
//map from instantiation terms to their model basis equivalent
- std::map< Node, Node > d_model_basis;
+ std::map< Node, Node > d_model_basis_body;
+ // compute model basis arg
+ void computeModelBasisArgAttribute( Node n );
public:
//get model basis term
Node getModelBasisTerm( TypeNode tn, int i = 0 );
//get model basis term for op
Node getModelBasisOpTerm( Node op );
- // compute model basis arg
- void computeModelBasisArgAttribute( Node n );
- //register instantiation terms with their corresponding model basis terms
- void registerModelBasis( Node n, Node gn );
//get model basis
- Node getModelBasis( Node n ) { return d_model_basis[n]; }
+ Node getModelBasis( Node f, Node n );
+ //get model basis body
+ Node getModelBasisBody( Node f );
private:
/** map from universal quantifiers to the list of variables */
std::map< Node, std::vector< Node > > d_vars;
/** map from universal quantifiers to the list of skolem constants */
std::map< Node, std::vector< Node > > d_skolem_constants;
+ /** model basis terms */
+ std::map< Node, std::vector< Node > > d_model_basis_terms;
/** map from universal quantifiers to their skolemized body */
std::map< Node, Node > d_skolem_body;
/** instantiation constants to universal quantifiers */
}
void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
- std::set< Node > added;
- getTermDatabase()->addTerm( n, added, withinQuant );
- if( options::efficientEMatching() ){
- uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF );
- d_ith->newTerms(added);
- }
+ std::set< Node > added;
+ getTermDatabase()->addTerm( n, added, withinQuant );
+ if( options::efficientEMatching() ){
+ uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF );
+ d_ith->newTerms(added);
+ }
#ifdef COMPUTE_RELEVANCE
- //added contains also the Node that just have been asserted in this branch
- for( std::set< Node >::iterator i=added.begin(), end=added.end();
- i!=end; i++ ){
- if( !withinQuant ){
- setRelevance( i->getOperator(), 0 );
- }
+ //added contains also the Node that just have been asserted in this branch
+ for( std::set< Node >::iterator i=added.begin(), end=added.end();
+ i!=end; i++ ){
+ if( !withinQuant ){
+ setRelevance( i->getOperator(), 0 );
+ }
}
#endif
}
+void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
+ for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){
+ Node n = m.getValue( d_term_db->d_inst_constants[f][i] );
+ if( !n.isNull() ){
+ vars.push_back( f[0][i] );
+ terms.push_back( n );
+ }
+ }
+}
+
+Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
+ Node body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+ //process partial instantiation if necessary
+ if( d_term_db->d_vars[f].size()!=vars.size() ){
+ std::vector< Node > uninst_vars;
+ //doing a partial instantiation, must add quantifier for all uninstantiated variables
+ for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
+ if( std::find( vars.begin(), vars.end(), f[0][i] )==vars.end() ){
+ uninst_vars.push_back( f[0][i] );
+ }
+ }
+ Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
+ body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
+ Trace("partial-inst") << "Partial instantiation : " << d_rewritten_quant[f] << std::endl;
+ Trace("partial-inst") << " : " << body << std::endl;
+ }
+ return body;
+}
+
+Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
+ std::vector< Node > vars;
+ std::vector< Node > terms;
+ computeTermVector( f, m, vars, terms );
+ return getInstantiation( f, vars, terms );
+}
+
+bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
+ return d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, NULL, modInst );
+}
+
bool QuantifiersEngine::addLemma( Node lem ){
- //AJR: the following check is necessary until FULL_CHECK is guarenteed after d_out->lemma(...)
Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
lem = Rewriter::rewrite(lem);
if( d_lemmas_produced.find( lem )==d_lemmas_produced.end() ){
}
}
-bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms )
-{
+bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
Assert( f.getKind()==FORALL );
Assert( !f.hasAttribute(InstConstantAttribute()) );
Assert( vars.size()==terms.size() );
- Node body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
- Node lem;
- if( d_term_db->d_vars[f].size()==vars.size() ){
- NodeBuilder<> nb(kind::OR);
- nb << d_rewritten_quant[f].notNode() << body;
- lem = nb;
- }else{
- //doing a partial instantiation, must add quantifier for all uninstantiated variables
- Notice() << "Partial instantiation not implemented yet." << std::endl;
- Unimplemented();
- }
+ Node body = getInstantiation( f, vars, terms );
+ //make the lemma
+ NodeBuilder<> nb(kind::OR);
+ nb << d_rewritten_quant[f].notNode() << body;
+ Node lem = nb;
+ //check for duplication
if( addLemma( lem ) ){
Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
uint64_t maxInstLevel = 0;
}
}
-bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool makeComplete ){
+bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m ){
//make sure there are values for each variable we are instantiating
- if( makeComplete ){
- m.makeComplete( f, this );
- }
+ m.makeComplete( f, this );
//make it representative, this is helpful for recognizing duplication
m.makeRepresentative( this );
Trace("inst-add") << "Add instantiation: " << m << std::endl;
return false;
}
//compute the vector of terms for the instantiation
- std::vector< Node > match;
- m.computeTermVec( d_term_db->d_inst_constants[f], match );
- //add the instantiation
- bool addedInst = false;
- if( match.size()==d_term_db->d_vars[f].size() ){
- addedInst = addInstantiation( f, d_term_db->d_vars[f], match );
- }else{
- //must compute the subset of variables we are instantiating
- std::vector< Node > vars;
- for( size_t i=0; i<d_term_db->d_vars[f].size(); i++ ){
- Node val = m.get( getTermDatabase()->getInstantiationConstant( f, i ) );
- if( !val.isNull() ){
- vars.push_back( d_term_db->d_vars[f][i] );
- }
- }
- addedInst = addInstantiation( f, vars, match );
+ std::vector< Node > terms;
+ for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){
+ Node n = m.getValue( d_term_db->d_inst_constants[f][i] );
+ Assert( !n.isNull() );
+ terms.push_back( n );
}
+ //add the instantiation
+ bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms );
//report the result
if( addedInst ){
Trace("inst-add") << " -> Success." << std::endl;
//create inst variable
std::vector<Node> createInstVariable( std::vector<Node> & vars );
+private:
+ /** compute term vector */
+ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
public:
+ /** get instantiation */
+ Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
+ /** get instantiation */
+ Node getInstantiation( Node f, InstMatch& m );
+ /** exist instantiation ? */
+ bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
/** add lemma lem */
bool addLemma( Node lem );
/** instantiate f with arguments terms */
bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
/** do instantiation specified by m */
- bool addInstantiation( Node f, InstMatch& m, bool makeComplete = true );
+ bool addInstantiation( Node f, InstMatch& m );
/** split on node n */
bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
/** add split equality */
++r->nb_applied;
++d_statistics.d_cache_miss;
std::vector<Node> subst;
- im.computeTermVec(getQuantifiersEngine(), r->inst_vars , subst);
+ //AJR: replaced computeTermVec with this
+ for( size_t i=0; i<r->inst_vars.size(); i++ ){
+ Node n = im.getValue( r->inst_vars[i] );
+ Assert( !n.isNull() );
+ subst.push_back( n );
+ }
RuleInst * ri = new RuleInst(*this,r,subst,
r->directrr ? im.d_matched : Node::null());
Debug("rewriterules::matching") << "One matching found"
//set value function
void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
if( d_data.empty() ){
+ //overwrite value if either at leaf or this is a fresh tree
d_value = v;
}else if( !d_value.isNull() && d_value!=v ){
+ //value is no longer constant
d_value = Node::null();
}
if( argIndex<(int)indexOrder.size() ){
projects / cvc5.git / commitdiff