From bbcfb5208c6c0f343d1a63b129c54914f66b2701 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 16 Oct 2012 17:10:47 +0000 Subject: [PATCH] first draft of new inst gen method (still with bugs), some cleanup of quantifiers code --- src/theory/quantifiers/Makefile.am | 4 +- .../quantifiers/candidate_generator.cpp | 65 -- src/theory/quantifiers/candidate_generator.h | 28 - src/theory/quantifiers/inst_gen.cpp | 177 ++++ src/theory/quantifiers/inst_gen.h | 61 ++ src/theory/quantifiers/inst_match.cpp | 55 +- src/theory/quantifiers/inst_match.h | 52 +- src/theory/quantifiers/model_builder.cpp | 788 ++++++++++++------ src/theory/quantifiers/model_builder.h | 116 ++- src/theory/quantifiers/model_engine.cpp | 91 +- src/theory/quantifiers/model_engine.h | 11 +- src/theory/quantifiers/options | 2 + src/theory/quantifiers/term_database.cpp | 40 +- src/theory/quantifiers/term_database.h | 14 +- src/theory/quantifiers_engine.cpp | 114 ++- src/theory/quantifiers_engine.h | 11 +- .../rewriterules/theory_rewriterules.cpp | 7 +- src/theory/uf/theory_uf_model.cpp | 2 + 18 files changed, 1111 insertions(+), 527 deletions(-) create mode 100755 src/theory/quantifiers/inst_gen.cpp create mode 100755 src/theory/quantifiers/inst_gen.h diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 3a19ff9c6..db0eed31e 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -36,7 +36,9 @@ libquantifiers_la_SOURCES = \ model_builder.h \ model_builder.cpp \ quantifiers_attributes.h \ - quantifiers_attributes.cpp + quantifiers_attributes.cpp \ + inst_gen.h \ + inst_gen.cpp EXTRA_DIST = \ kinds \ diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index af6356577..ddcc2b1ae 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -57,69 +57,6 @@ Node CandidateGeneratorQueue::getNextCandidate(){ } } -#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_itergetTermDatabase()->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() ); @@ -166,8 +103,6 @@ Node CandidateGeneratorQE::getNextCandidate(){ return Node::null(); } -#endif - //CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) : // d_qe( qe ), d_eq_class( eqc ){ // d_eci = NULL; diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index 1be3c3c21..0f52dc7c3 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -71,33 +71,6 @@ public: 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; @@ -120,7 +93,6 @@ public: Node getNextCandidate(); }; -#endif //class CandidateGeneratorQEDisequal : public CandidateGenerator //{ diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp new file mode 100755 index 000000000..324165692 --- /dev/null +++ b/src/theory/quantifiers/inst_gen.cpp @@ -0,0 +1,177 @@ +/********************* */ +/*! \file inst_gen.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of inst gen classes + **/ + +#include "theory/quantifiers/inst_gen.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/model_builder.h" +#include "theory/quantifiers/first_order_model.h" + +#define RECONSIDER_FUNC_CONSTANT + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + + + +InstGenProcess::InstGenProcess( Node n ) : d_node( n ){ + Assert( n.hasAttribute(InstConstantAttribute()) ); + int count = 0; + for( size_t i=0; iexistsInstantiation( f, m, true, true ) ){ + //if( d_inst_trie[val].addInstMatch( qe, f, m, true, NULL, true ) ){ + d_match_values.push_back( val ); + d_matches.push_back( InstMatch( &m ) ); + //} + } +} + +void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f ){ + //calculate all matches for children + for( int i=0; i<(int)d_children.size(); i++ ){ + d_children[i].calculateMatches( qe, f ); + if( d_children[i].getNumMatches()==0 ){ + return; + } + } + Trace("cm") << "calculate matches " << d_node << std::endl; + //get the model + FirstOrderModel* fm = qe->getModel(); + if( d_node.getKind()==APPLY_UF ){ + //if this is an uninterpreted function + Node op = d_node.getOperator(); + //process all values + for( size_t i=0; id_uf_terms[op].size(); i++ ){ + Node n = fm->d_uf_terms[op][i]; + bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n ); + for( int t=(isSelected ? 0 : 1); t<2; t++ ){ + //do not consider ground case if it is already congruent to another ground term + if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ + Trace("cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl; + bool success = true; + InstMatch curr; + for( size_t j=0; jgetEqualityQuery(), d_node[j], n[j] ) ){ + Trace("cm") << "fail match: " << n[j] << " is not equal to " << curr.get( d_node[j] ) << std::endl; + Trace("cm") << " are equal : " << qe->getEqualityQuery()->areEqual( n[j], curr.get( d_node[j] ) ) << std::endl; + success = false; + break; + } + }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){ + Trace("cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl; + success = false; + break; + } + } + } + } + if( success ){ + //try to find unifier for d_node = n + calculateMatchesUninterpreted( qe, f, curr, n, 0, t==0 ); + } + } + } + } + + }else{ + InstMatch curr; + //if this is an interpreted function + std::vector< Node > terms; + calculateMatchesInterpreted( qe, f, curr, terms, 0 ); + } + Trace("cm") << "done calculate matches" << std::endl; +} + +bool InstGenProcess::getMatch( EqualityQuery* q, int i, InstMatch& m ){ + //FIXME: is this correct? (query may not be accurate) + return m.merge( q, d_matches[i] ); +} + +void InstGenProcess::calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ){ + if( childIndex==(int)d_children.size() ){ + Node val = qe->getModel()->getRepresentative( n ); //FIXME: is this correct? + Trace("cm") << " - u-match : " << val << std::endl; + Trace("cm") << " : " << curr << std::endl; + addMatchValue( qe, f, val, curr ); + }else{ + Trace("cm") << "Consider child index = " << childIndex << ", against ground term argument " << d_children_index[childIndex] << " ... " << n[d_children_index[childIndex]] << std::endl; + bool sel = ( isSelected && n[d_children_index[childIndex]].getAttribute(ModelBasisAttribute()) ); + for( int i=0; i<(int)d_children[ childIndex ].getNumMatches(); i++ ){ + //FIXME: is this correct? + if( sel || qe->getEqualityQuery()->areEqual( d_children[ childIndex ].getMatchValue( i ), n[d_children_index[childIndex]] ) ){ + InstMatch next( &curr ); + if( d_children[ childIndex ].getMatch( qe->getEqualityQuery(), i, next ) ){ + calculateMatchesUninterpreted( qe, f, next, n, childIndex+1, isSelected ); + }else{ + Trace("cm") << curr << " not equal to " << d_children[ childIndex ].d_matches[i] << std::endl; + Trace("cm") << childIndex << " match " << i << " not equal subs." << std::endl; + } + }else{ + Trace("cm") << childIndex << " match " << i << " not equal value." << std::endl; + } + } + } +} + +void InstGenProcess::calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex ){ + FirstOrderModel* fm = qe->getModel(); + if( argIndex==(int)d_node.getNumChildren() ){ + Node val; + if( d_node.getNumChildren()==0 ){ + val = d_node; + }else if( d_node.getKind()==EQUAL ){ + val = qe->getEqualityQuery()->areEqual( terms[0], terms[1] ) ? fm->d_true : fm->d_false; + }else{ + val = NodeManager::currentNM()->mkNode( d_node.getKind(), terms ); + val = Rewriter::rewrite( val ); + } + Trace("cm") << " - i-match : " << val << std::endl; + Trace("cm") << " : " << curr << std::endl; + addMatchValue( qe, f, val, curr ); + }else{ + if( d_children_map.find( argIndex )==d_children_map.end() ){ + terms.push_back( fm->getRepresentative( d_node[argIndex] ) ); + calculateMatchesInterpreted( qe, f, curr, terms, argIndex+1 ); + terms.pop_back(); + }else{ + for( int i=0; i<(int)d_children[ d_children_map[argIndex] ].getNumMatches(); i++ ){ + InstMatch next( &curr ); + if( d_children[ d_children_map[argIndex] ].getMatch( qe->getEqualityQuery(), i, next ) ){ + terms.push_back( d_children[ d_children_map[argIndex] ].getMatchValue( i ) ); + calculateMatchesInterpreted( qe, f, next, terms, argIndex+1 ); + terms.pop_back(); + } + } + } + } +} diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h new file mode 100755 index 000000000..3386001af --- /dev/null +++ b/src/theory/quantifiers/inst_gen.h @@ -0,0 +1,61 @@ +/********************* */ +/*! \file inst_gen.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Inst Gen classes + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__INST_GEN_H +#define __CVC4__THEORY__QUANTIFIERS__INST_GEN_H + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/inst_match.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class InstGenProcess +{ +private: + //the node we are processing + Node d_node; + //the sub children for this node + std::vector< InstGenProcess > d_children; + std::vector< int > d_children_index; + std::map< int, int > d_children_map; + //the matches we have produced + std::vector< InstMatch > d_matches; + std::vector< Node > d_match_values; + //add match value + std::map< Node, inst::InstMatchTrie > d_inst_trie; + void addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ); +private: + void calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ); + void calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex ); +public: + InstGenProcess( Node n ); + virtual ~InstGenProcess(){} + + void calculateMatches( QuantifiersEngine* qe, Node f ); + int getNumMatches() { return d_matches.size(); } + bool getMatch( EqualityQuery* q, int i, InstMatch& m ); + Node getMatchValue( int i ) { return d_match_values[i]; } +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 62cee6aed..a74bf0fd5 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -43,7 +43,7 @@ InstMatch::InstMatch( InstMatch* m ) { 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; @@ -61,7 +61,8 @@ bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){ 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; } } @@ -70,11 +71,12 @@ bool InstMatch::add( InstMatch& m ){ 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; } @@ -134,6 +136,16 @@ void InstMatch::applyRewrite(){ } } +/** 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] ); @@ -144,6 +156,7 @@ void InstMatch::computeTermVec( QuantifiersEngine* qe, const std::vector< Node > } } } + 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() ){ @@ -151,7 +164,7 @@ void InstMatch::computeTermVec( const std::vector< Node >& vars, std::vector< No } } } - +*/ /** 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 ){ @@ -163,7 +176,7 @@ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, } /** 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{ @@ -171,10 +184,22 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m 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 ) ){ @@ -185,7 +210,7 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m 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; } } @@ -198,8 +223,12 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m } } -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{ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 90a24322a..feab91837 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -114,20 +114,39 @@ public: 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 void erase(Iterator begin, Iterator end){ @@ -136,8 +155,8 @@ public: }; } 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 ; @@ -146,7 +165,6 @@ public: 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(); }; @@ -155,15 +173,6 @@ public: /* 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) { @@ -182,7 +191,7 @@ private: /** 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; @@ -190,11 +199,18 @@ 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, 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 { diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 66b92e1de..6fa02a8d3 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -24,8 +24,7 @@ #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; @@ -58,43 +57,98 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { 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; igetNumAssertedQuantifiers(); 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; igetNumAssertedQuantifiers(); 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 ){ @@ -127,197 +181,6 @@ 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 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 ){ @@ -337,20 +200,21 @@ void ModelEngineBuilder::constructModel( FirstOrderModel* fm ){ } 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; @@ -359,7 +223,6 @@ void ModelEngineBuilder::constructModelUf( FirstOrderModel* fm, Node op ){ //set the values in the model for( size_t i=0; id_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 @@ -372,7 +235,7 @@ void ModelEngineBuilder::constructModelUf( FirstOrderModel* fm, Node op ){ 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 @@ -415,23 +278,480 @@ bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ 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 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; i0 ){ + 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; id_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 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; igetTermDatabase()->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] ); +} + diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index a57ca2b37..a4c38d608 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -46,16 +46,27 @@ protected: /** 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(){} @@ -63,40 +74,103 @@ public: 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 */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index d2ad6bb33..0b73f3c8b 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -37,9 +37,14 @@ using namespace CVC4::theory::inst; //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 ){ @@ -48,16 +53,6 @@ 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; igetNumAssertedQuantifiers(); 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++ ){ @@ -74,11 +69,11 @@ void ModelEngine::check( Theory::Effort e ){ 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 @@ -93,7 +88,7 @@ void ModelEngine::check( Theory::Effort e ){ 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); @@ -119,7 +114,7 @@ void ModelEngine::check( Theory::Effort e ){ 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 @@ -161,54 +156,6 @@ bool ModelEngine::optExhInstEvalSkipMultiple(){ #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 @@ -264,7 +211,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ } 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 ){ @@ -300,7 +247,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool 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"); @@ -377,7 +324,7 @@ void ModelEngine::debugPrint( const char* c ){ 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 ) << " "; @@ -392,17 +339,13 @@ ModelEngine::Statistics::Statistics(): 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(){ @@ -411,8 +354,6 @@ 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); } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 4550564a2..f930fbec7 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -31,10 +31,7 @@ class ModelEngine : public QuantifiersModule 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; @@ -47,8 +44,6 @@ private: 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 @@ -62,6 +57,8 @@ private: 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 ); @@ -78,8 +75,6 @@ public: 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(); }; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index a28ccb423..724c76e82 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -78,6 +78,8 @@ option fmfInstEngine --fmf-inst-engine bool :default false 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 diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3f5d18adc..0614bb22a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -17,6 +17,7 @@ #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; @@ -164,8 +165,10 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ 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++; @@ -186,10 +189,12 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ 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++; @@ -208,19 +213,10 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ 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; @@ -249,8 +245,32 @@ Node TermDb::getModelBasisOpTerm( Node op ){ 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++ ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index f6f65b5dd..64f3d4980 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -115,23 +115,25 @@ private: //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 */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0388ae7d4..4d7e93ef2 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -275,26 +275,65 @@ void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){ } 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; id_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() ){ @@ -309,22 +348,16 @@ bool QuantifiersEngine::addLemma( Node lem ){ } } -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; @@ -360,11 +393,9 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std } } -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; @@ -375,23 +406,14 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool makeComplet 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; id_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; id_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; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index a658cccf6..d0c5832ff 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -222,13 +222,22 @@ public: //create inst variable std::vector createInstVariable( std::vector & 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 */ diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index b797d25e5..c6fd9611c 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -152,7 +152,12 @@ void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r, ++r->nb_applied; ++d_statistics.d_cache_miss; std::vector subst; - im.computeTermVec(getQuantifiersEngine(), r->inst_vars , subst); + //AJR: replaced computeTermVec with this + for( size_t i=0; iinst_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" diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 7b990c4cd..f7272f7ba 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -51,8 +51,10 @@ bool UfModelTreeNode::hasConcreteArgumentDefinition(){ //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() ){ -- 2.30.2