diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-27 22:01:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-27 22:01:03 +0000 |
commit | 485c03a323911142e460bd0a7c428759496dc631 (patch) | |
tree | 8c512712734dd2862c89acd8681357d0a2e0dabe /src/theory | |
parent | 33fd76601b42599d9883889a03d59d0d85729661 (diff) |
Minor cleanup after today's commits:
* change some uses of "std::cout" to "Message()"
* change some files to use Unix newlines instead of DOS newlines
* fix compiler warning
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/theory_arrays_model.cpp | 140 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_model.h | 122 | ||||
-rw-r--r-- | src/theory/candidate_generator.cpp | 510 | ||||
-rw-r--r-- | src/theory/candidate_generator.h | 374 | ||||
-rw-r--r-- | src/theory/inst_match.cpp | 3 | ||||
-rw-r--r-- | src/theory/model.cpp | 1230 | ||||
-rw-r--r-- | src/theory/model.h | 382 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 366 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 178 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 182 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 344 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.h | 108 | ||||
-rw-r--r-- | src/theory/quantifiers/rep_set_iterator.cpp | 1034 | ||||
-rw-r--r-- | src/theory/quantifiers/rep_set_iterator.h | 240 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 312 | ||||
-rw-r--r-- | src/theory/rr_inst_match.cpp | 4 | ||||
-rw-r--r-- | src/theory/rr_trigger.cpp | 444 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.cpp | 840 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.h | 398 |
19 files changed, 3604 insertions, 3607 deletions
diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp index 49da2f851..7a574fac1 100644 --- a/src/theory/arrays/theory_arrays_model.cpp +++ b/src/theory/arrays/theory_arrays_model.cpp @@ -1,70 +1,70 @@ -/********************* */
-/*! \file theory_arrays_model.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 theory_arrays_model class
- **/
-
-#include "theory/theory_engine.h"
-#include "theory/arrays/theory_arrays_model.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_database.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arrays;
-
-ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){
- Assert( arr.getKind()!=STORE );
- //look at ground assertions
- Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) );
- Node sel_op = sel.getOperator(); //FIXME: easier way to do this?
- for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){
- Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i];
- Assert( n.getKind()==SELECT );
- if( m->areEqual( n[0], arr ) ){
- //d_model->getTermDatabase()->computeModelBasisArgAttribute( n );
- //if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
- Node r = d_model->getRepresentative( n );
- Node i = d_model->getRepresentative( n[1] );
- d_values[i] = r;
- //}
- }
- }
-}
-
-Node ArrayModel::getValue( Node n ){
- Assert( n.getKind()==SELECT );
- Assert( n[0]==d_arr );
- std::map< Node, Node >::iterator it = d_values.find( n[0] );
- if( it!=d_values.end() ){
- return it->second;
- }else{
- return n;
- //return d_default_value; TODO: guarentee I can return this here
- }
-}
-
-void ArrayModel::setDefaultValue( Node v ){
- d_default_value = v;
-}
-
-Node ArrayModel::getArrayValue(){
- Node curr = d_arr; //TODO: make constant default
- for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){
- curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second );
- }
- return curr;
-}
+/********************* */ +/*! \file theory_arrays_model.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 theory_arrays_model class + **/ + +#include "theory/theory_engine.h" +#include "theory/arrays/theory_arrays_model.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::arrays; + +ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){ + Assert( arr.getKind()!=STORE ); + //look at ground assertions + Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) ); + Node sel_op = sel.getOperator(); //FIXME: easier way to do this? + for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){ + Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i]; + Assert( n.getKind()==SELECT ); + if( m->areEqual( n[0], arr ) ){ + //d_model->getTermDatabase()->computeModelBasisArgAttribute( n ); + //if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ + Node r = d_model->getRepresentative( n ); + Node i = d_model->getRepresentative( n[1] ); + d_values[i] = r; + //} + } + } +} + +Node ArrayModel::getValue( Node n ){ + Assert( n.getKind()==SELECT ); + Assert( n[0]==d_arr ); + std::map< Node, Node >::iterator it = d_values.find( n[0] ); + if( it!=d_values.end() ){ + return it->second; + }else{ + return n; + //return d_default_value; TODO: guarentee I can return this here + } +} + +void ArrayModel::setDefaultValue( Node v ){ + d_default_value = v; +} + +Node ArrayModel::getArrayValue(){ + Node curr = d_arr; //TODO: make constant default + for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){ + curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second ); + } + return curr; +} diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h index 3895388e3..28852296d 100644 --- a/src/theory/arrays/theory_arrays_model.h +++ b/src/theory/arrays/theory_arrays_model.h @@ -1,62 +1,62 @@ -/********************* */
-/*! \file theory_arrays_model.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, 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 MODEL for theory of arrays
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_ARRAYS_MODEL_H
-#define __CVC4__THEORY_ARRAYS_MODEL_H
-
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-namespace quantifiers{
- class FirstOrderModel;
-}
-
-namespace arrays {
-
-class ArrayModel{
-protected:
- /** reference to model */
- quantifiers::FirstOrderModel* d_model;
- /** the array this model is for */
- Node d_arr;
-public:
- ArrayModel(){}
- ArrayModel( Node arr, quantifiers::FirstOrderModel* m );
- ~ArrayModel() {}
-public:
- /** pre-defined values */
- std::map< Node, Node > d_values;
- /** default value */
- Node d_default_value;
- /** get value, return arguments that the value depends on */
- Node getValue( Node n );
- /** set default */
- void setDefaultValue( Node v );
-public:
- /** get array value */
- Node getArrayValue();
-};/* class ArrayModel */
-
-}
-}
-}
-
+/********************* */ +/*! \file theory_arrays_model.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, 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 MODEL for theory of arrays + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_ARRAYS_MODEL_H +#define __CVC4__THEORY_ARRAYS_MODEL_H + +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { + +namespace quantifiers{ + class FirstOrderModel; +} + +namespace arrays { + +class ArrayModel{ +protected: + /** reference to model */ + quantifiers::FirstOrderModel* d_model; + /** the array this model is for */ + Node d_arr; +public: + ArrayModel(){} + ArrayModel( Node arr, quantifiers::FirstOrderModel* m ); + ~ArrayModel() {} +public: + /** pre-defined values */ + std::map< Node, Node > d_values; + /** default value */ + Node d_default_value; + /** get value, return arguments that the value depends on */ + Node getValue( Node n ); + /** set default */ + void setDefaultValue( Node v ); +public: + /** get array value */ + Node getArrayValue(); +};/* class ArrayModel */ + +} +} +} + #endif
\ No newline at end of file diff --git a/src/theory/candidate_generator.cpp b/src/theory/candidate_generator.cpp index ffecaa8da..a0f303c21 100644 --- a/src/theory/candidate_generator.cpp +++ b/src/theory/candidate_generator.cpp @@ -1,255 +1,255 @@ -/********************* */
-/*! \file theory_uf_candidate_generator.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 theory uf candidate generator class
- **/
-
-#include "theory/candidate_generator.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/inst_match.h"
-#include "theory/quantifiers_engine.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::inst;
-
-bool CandidateGenerator::isLegalCandidate( Node n ){
- return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) );
-}
-
-void CandidateGeneratorQueue::addCandidate( Node n ) {
- if( isLegalCandidate( n ) ){
- d_candidates.push_back( n );
- }
-}
-
-void CandidateGeneratorQueue::reset( Node eqc ){
- if( d_candidate_index>0 ){
- d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index );
- d_candidate_index = 0;
- }
- if( !eqc.isNull() ){
- d_candidates.push_back( eqc );
- }
-}
-Node CandidateGeneratorQueue::getNextCandidate(){
- if( d_candidate_index<(int)d_candidates.size() ){
- Node n = d_candidates[d_candidate_index];
- d_candidate_index++;
- return n;
- }else{
- d_candidate_index = 0;
- d_candidates.clear();
- return Node::null();
- }
-}
-
-#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() );
-}
-void CandidateGeneratorQE::resetInstantiationRound(){
- d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size();
-}
-
-void CandidateGeneratorQE::reset( Node eqc ){
- d_term_iter = 0;
- if( eqc.isNull() ){
- d_using_term_db = true;
- }else{
- //create an equivalence class iterator in eq class eqc
- d_eqc.clear();
- d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
- d_using_term_db = false;
- }
-}
-
-Node CandidateGeneratorQE::getNextCandidate(){
- if( d_term_iter>=0 ){
- if( d_using_term_db ){
- //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{
- while( d_term_iter<(int)d_eqc.size() ){
- Node n = d_eqc[d_term_iter];
- d_term_iter++;
- if( n.hasOperator() && n.getOperator()==d_op ){
- if( isLegalCandidate( n ) ){
- return n;
- }
- }
- }
- }
- }
- return Node::null();
-}
-
-#endif
-
-//CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) :
-// d_qe( qe ), d_eq_class( eqc ){
-// d_eci = NULL;
-//}
-//void CandidateGeneratorQEDisequal::resetInstantiationRound(){
-//
-//}
-////we will iterate over all terms that are disequal from eqc
-//void CandidateGeneratorQEDisequal::reset( Node eqc ){
-// //Assert( !eqc.isNull() );
-// ////begin iterating over equivalence classes that are disequal from eqc
-// //d_eci = d_ith->getEquivalenceClassInfo( eqc );
-// //if( d_eci ){
-// // d_eqci_iter = d_eci->d_disequal.begin();
-// //}
-//}
-//Node CandidateGeneratorQEDisequal::getNextCandidate(){
-// //if( d_eci ){
-// // while( d_eqci_iter != d_eci->d_disequal.end() ){
-// // if( (*d_eqci_iter).second ){
-// // //we have an equivalence class that is disequal from eqc
-// // d_cg->reset( (*d_eqci_iter).first );
-// // Node n = d_cg->getNextCandidate();
-// // //if there is a candidate in this equivalence class, return it
-// // if( !n.isNull() ){
-// // return n;
-// // }
-// // }
-// // ++d_eqci_iter;
-// // }
-// //}
-// return Node::null();
-//}
-
-
-CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
- d_match_pattern( mpat ), d_qe( qe ){
-
-}
-void CandidateGeneratorQELitEq::resetInstantiationRound(){
-
-}
-void CandidateGeneratorQELitEq::reset( Node eqc ){
- d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
-}
-Node CandidateGeneratorQELitEq::getNextCandidate(){
- while( d_eq.isFinished() ){
- Node n = (*d_eq);
- ++d_eq;
- if( n.getType()==d_match_pattern[0].getType() ){
- //an equivalence class with the same type as the pattern, return reflexive equality
- return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
- }
- }
- return Node::null();
-}
-
-
-CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
- d_match_pattern( mpat ), d_qe( qe ){
-
-}
-void CandidateGeneratorQELitDeq::resetInstantiationRound(){
-
-}
-void CandidateGeneratorQELitDeq::reset( Node eqc ){
- Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) );
- d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() );
-}
-Node CandidateGeneratorQELitDeq::getNextCandidate(){
- //get next candidate term in equivalence class
- while( !d_eqc_false.isFinished() ){
- Node n = (*d_eqc_false);
- ++d_eqc_false;
- if( n.getKind()==d_match_pattern.getKind() ){
- //found an iff or equality, try to match it
- //DO_THIS: cache to avoid redundancies?
- //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false?
- return n;
- }
- }
- return Node::null();
-}
+/********************* */ +/*! \file theory_uf_candidate_generator.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 theory uf candidate generator class + **/ + +#include "theory/candidate_generator.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" +#include "theory/quantifiers/term_database.h" +#include "theory/inst_match.h" +#include "theory/quantifiers_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::inst; + +bool CandidateGenerator::isLegalCandidate( Node n ){ + return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) ); +} + +void CandidateGeneratorQueue::addCandidate( Node n ) { + if( isLegalCandidate( n ) ){ + d_candidates.push_back( n ); + } +} + +void CandidateGeneratorQueue::reset( Node eqc ){ + if( d_candidate_index>0 ){ + d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index ); + d_candidate_index = 0; + } + if( !eqc.isNull() ){ + d_candidates.push_back( eqc ); + } +} +Node CandidateGeneratorQueue::getNextCandidate(){ + if( d_candidate_index<(int)d_candidates.size() ){ + Node n = d_candidates[d_candidate_index]; + d_candidate_index++; + return n; + }else{ + d_candidate_index = 0; + d_candidates.clear(); + return Node::null(); + } +} + +#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() ); +} +void CandidateGeneratorQE::resetInstantiationRound(){ + d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size(); +} + +void CandidateGeneratorQE::reset( Node eqc ){ + d_term_iter = 0; + if( eqc.isNull() ){ + d_using_term_db = true; + }else{ + //create an equivalence class iterator in eq class eqc + d_eqc.clear(); + d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc ); + d_using_term_db = false; + } +} + +Node CandidateGeneratorQE::getNextCandidate(){ + if( d_term_iter>=0 ){ + if( d_using_term_db ){ + //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{ + while( d_term_iter<(int)d_eqc.size() ){ + Node n = d_eqc[d_term_iter]; + d_term_iter++; + if( n.hasOperator() && n.getOperator()==d_op ){ + if( isLegalCandidate( n ) ){ + return n; + } + } + } + } + } + return Node::null(); +} + +#endif + +//CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) : +// d_qe( qe ), d_eq_class( eqc ){ +// d_eci = NULL; +//} +//void CandidateGeneratorQEDisequal::resetInstantiationRound(){ +// +//} +////we will iterate over all terms that are disequal from eqc +//void CandidateGeneratorQEDisequal::reset( Node eqc ){ +// //Assert( !eqc.isNull() ); +// ////begin iterating over equivalence classes that are disequal from eqc +// //d_eci = d_ith->getEquivalenceClassInfo( eqc ); +// //if( d_eci ){ +// // d_eqci_iter = d_eci->d_disequal.begin(); +// //} +//} +//Node CandidateGeneratorQEDisequal::getNextCandidate(){ +// //if( d_eci ){ +// // while( d_eqci_iter != d_eci->d_disequal.end() ){ +// // if( (*d_eqci_iter).second ){ +// // //we have an equivalence class that is disequal from eqc +// // d_cg->reset( (*d_eqci_iter).first ); +// // Node n = d_cg->getNextCandidate(); +// // //if there is a candidate in this equivalence class, return it +// // if( !n.isNull() ){ +// // return n; +// // } +// // } +// // ++d_eqci_iter; +// // } +// //} +// return Node::null(); +//} + + +CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) : + d_match_pattern( mpat ), d_qe( qe ){ + +} +void CandidateGeneratorQELitEq::resetInstantiationRound(){ + +} +void CandidateGeneratorQELitEq::reset( Node eqc ){ + d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); +} +Node CandidateGeneratorQELitEq::getNextCandidate(){ + while( d_eq.isFinished() ){ + Node n = (*d_eq); + ++d_eq; + if( n.getType()==d_match_pattern[0].getType() ){ + //an equivalence class with the same type as the pattern, return reflexive equality + return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n ); + } + } + return Node::null(); +} + + +CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) : + d_match_pattern( mpat ), d_qe( qe ){ + +} +void CandidateGeneratorQELitDeq::resetInstantiationRound(){ + +} +void CandidateGeneratorQELitDeq::reset( Node eqc ){ + Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) ); + d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() ); +} +Node CandidateGeneratorQELitDeq::getNextCandidate(){ + //get next candidate term in equivalence class + while( !d_eqc_false.isFinished() ){ + Node n = (*d_eqc_false); + ++d_eqc_false; + if( n.getKind()==d_match_pattern.getKind() ){ + //found an iff or equality, try to match it + //DO_THIS: cache to avoid redundancies? + //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false? + return n; + } + } + return Node::null(); +} diff --git a/src/theory/candidate_generator.h b/src/theory/candidate_generator.h index 2152f1ef6..134b0e1b7 100644 --- a/src/theory/candidate_generator.h +++ b/src/theory/candidate_generator.h @@ -1,187 +1,187 @@ -/********************* */
-/*! \file candidate_generator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** 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 Theory uf candidate generator
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__CANDIDATE_GENERATOR_H
-#define __CVC4__CANDIDATE_GENERATOR_H
-
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-class QuantifiersEngine;
-
-namespace inst {
-
-/** base class for generating candidates for matching */
-class CandidateGenerator {
-public:
- CandidateGenerator(){}
- ~CandidateGenerator(){}
-
- /** Get candidates functions. These set up a context to get all match candidates.
- cg->reset( eqc );
- do{
- Node cand = cg->getNextCandidate();
- //.......
- }while( !cand.isNull() );
-
- eqc is the equivalence class you are searching in
- */
- virtual void reset( Node eqc ) = 0;
- virtual Node getNextCandidate() = 0;
- /** add candidate to list of nodes returned by this generator */
- virtual void addCandidate( Node n ) {}
- /** call this at the beginning of each instantiation round */
- virtual void resetInstantiationRound() = 0;
-public:
- /** legal candidate */
- static bool isLegalCandidate( Node n );
-};/* class CandidateGenerator */
-
-/** candidate generator queue (for manual candidate generation) */
-class CandidateGeneratorQueue : public CandidateGenerator {
-private:
- std::vector< Node > d_candidates;
- int d_candidate_index;
-public:
- CandidateGeneratorQueue() : d_candidate_index( 0 ){}
- ~CandidateGeneratorQueue(){}
-
- void addCandidate( Node n );
-
- void resetInstantiationRound(){}
- void reset( Node eqc );
- Node getNextCandidate();
-};/* class CandidateGeneratorQueue */
-
-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;
-private:
- //operator you are looking for
- Node d_op;
- //instantiator pointer
- QuantifiersEngine* d_qe;
- //the equality class iterator
- std::vector< Node > d_eqc;
- int d_term_iter;
- int d_term_iter_limit;
- bool d_using_term_db;
-public:
- CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
- ~CandidateGeneratorQE(){}
-
- void resetInstantiationRound();
- void reset( Node eqc );
- Node getNextCandidate();
-};
-
-#endif
-
-//class CandidateGeneratorQEDisequal : public CandidateGenerator
-//{
-//private:
-// //equivalence class
-// Node d_eq_class;
-// //equivalence class info
-// EqClassInfo* d_eci;
-// //equivalence class iterator
-// EqClassInfo::BoolMap::const_iterator d_eqci_iter;
-// //instantiator pointer
-// QuantifiersEngine* d_qe;
-//public:
-// CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc );
-// ~CandidateGeneratorQEDisequal(){}
-//
-// void resetInstantiationRound();
-// void reset( Node eqc ); //should be what you want to be disequal from
-// Node getNextCandidate();
-//};
-
-class CandidateGeneratorQELitEq : public CandidateGenerator
-{
-private:
- //the equality classes iterator
- eq::EqClassesIterator d_eq;
- //equality you are trying to match equalities for
- Node d_match_pattern;
- //einstantiator pointer
- QuantifiersEngine* d_qe;
-public:
- CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
- ~CandidateGeneratorQELitEq(){}
-
- void resetInstantiationRound();
- void reset( Node eqc );
- Node getNextCandidate();
-};
-
-class CandidateGeneratorQELitDeq : public CandidateGenerator
-{
-private:
- //the equality class iterator for false
- eq::EqClassIterator d_eqc_false;
- //equality you are trying to match disequalities for
- Node d_match_pattern;
- //einstantiator pointer
- QuantifiersEngine* d_qe;
-public:
- CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
- ~CandidateGeneratorQELitDeq(){}
-
- void resetInstantiationRound();
- void reset( Node eqc );
- Node getNextCandidate();
-};
-
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */
+/********************* */ +/*! \file candidate_generator.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** 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 Theory uf candidate generator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CANDIDATE_GENERATOR_H +#define __CVC4__CANDIDATE_GENERATOR_H + +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +namespace inst { + +/** base class for generating candidates for matching */ +class CandidateGenerator { +public: + CandidateGenerator(){} + ~CandidateGenerator(){} + + /** Get candidates functions. These set up a context to get all match candidates. + cg->reset( eqc ); + do{ + Node cand = cg->getNextCandidate(); + //....... + }while( !cand.isNull() ); + + eqc is the equivalence class you are searching in + */ + virtual void reset( Node eqc ) = 0; + virtual Node getNextCandidate() = 0; + /** add candidate to list of nodes returned by this generator */ + virtual void addCandidate( Node n ) {} + /** call this at the beginning of each instantiation round */ + virtual void resetInstantiationRound() = 0; +public: + /** legal candidate */ + static bool isLegalCandidate( Node n ); +};/* class CandidateGenerator */ + +/** candidate generator queue (for manual candidate generation) */ +class CandidateGeneratorQueue : public CandidateGenerator { +private: + std::vector< Node > d_candidates; + int d_candidate_index; +public: + CandidateGeneratorQueue() : d_candidate_index( 0 ){} + ~CandidateGeneratorQueue(){} + + void addCandidate( Node n ); + + void resetInstantiationRound(){} + void reset( Node eqc ); + Node getNextCandidate(); +};/* class CandidateGeneratorQueue */ + +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; +private: + //operator you are looking for + Node d_op; + //instantiator pointer + QuantifiersEngine* d_qe; + //the equality class iterator + std::vector< Node > d_eqc; + int d_term_iter; + int d_term_iter_limit; + bool d_using_term_db; +public: + CandidateGeneratorQE( QuantifiersEngine* qe, Node op ); + ~CandidateGeneratorQE(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +#endif + +//class CandidateGeneratorQEDisequal : public CandidateGenerator +//{ +//private: +// //equivalence class +// Node d_eq_class; +// //equivalence class info +// EqClassInfo* d_eci; +// //equivalence class iterator +// EqClassInfo::BoolMap::const_iterator d_eqci_iter; +// //instantiator pointer +// QuantifiersEngine* d_qe; +//public: +// CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ); +// ~CandidateGeneratorQEDisequal(){} +// +// void resetInstantiationRound(); +// void reset( Node eqc ); //should be what you want to be disequal from +// Node getNextCandidate(); +//}; + +class CandidateGeneratorQELitEq : public CandidateGenerator +{ +private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equality you are trying to match equalities for + Node d_match_pattern; + //einstantiator pointer + QuantifiersEngine* d_qe; +public: + CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ); + ~CandidateGeneratorQELitEq(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +class CandidateGeneratorQELitDeq : public CandidateGenerator +{ +private: + //the equality class iterator for false + eq::EqClassIterator d_eqc_false; + //equality you are trying to match disequalities for + Node d_match_pattern; + //einstantiator pointer + QuantifiersEngine* d_qe; +public: + CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ); + ~CandidateGeneratorQELitDeq(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +}/* CVC4::theory::inst namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */ diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp index c90483fa3..bad7e34cb 100644 --- a/src/theory/inst_match.cpp +++ b/src/theory/inst_match.cpp @@ -272,9 +272,6 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; - //get the equality engine - Theory* th_uf = qe->getTheoryEngine()->getTheory( theory::THEORY_UF ); - uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator(); //create candidate generator if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); diff --git a/src/theory/model.cpp b/src/theory/model.cpp index aa2c2d938..feedc0c31 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -1,615 +1,615 @@ -/********************* */
-/*! \file model.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 model class
- **/
-
-#include "theory/model.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
-#include "util/datatype.h"
-#include "theory/uf/theory_uf_model.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-
-void RepSet::clear(){
- d_type_reps.clear();
- d_tmap.clear();
-}
-
-void RepSet::add( Node n ){
- TypeNode t = n.getType();
- d_tmap[ n ] = (int)d_type_reps[t].size();
- d_type_reps[t].push_back( n );
-}
-
-void RepSet::set( TypeNode t, std::vector< Node >& reps ){
- for( size_t i=0; i<reps.size(); i++ ){
- d_tmap[ reps[i] ] = i;
- }
- d_type_reps[t].insert( d_type_reps[t].begin(), reps.begin(), reps.end() );
-}
-
-void RepSet::toStream(std::ostream& out){
-#if 0
- for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
- out << it->first << " : " << std::endl;
- for( int i=0; i<(int)it->second.size(); i++ ){
- out << " " << i << ": " << it->second[i] << std::endl;
- }
- }
-#else
- for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
- if( !it->first.isFunction() && !it->first.isPredicate() ){
- out << "(" << it->first << " " << it->second.size();
- out << " (";
- for( int i=0; i<(int)it->second.size(); i++ ){
- if( i>0 ){ out << " "; }
- out << it->second[i];
- }
- out << ")";
- out << ")" << std::endl;
- }
- }
-#endif
-}
-
-TheoryModel::TheoryModel( context::Context* c, std::string name ) :
-d_equalityEngine( c, name ){
- d_true = NodeManager::currentNM()->mkConst( true );
- d_false = NodeManager::currentNM()->mkConst( false );
-}
-
-void TheoryModel::reset(){
- d_reps.clear();
- d_rep_set.clear();
-}
-
-void TheoryModel::addDefineFunction( Node n ){
- d_define_funcs.push_back( n );
- d_defines.push_back( 0 );
-}
-
-void TheoryModel::addDefineType( TypeNode tn ){
- d_define_types.push_back( tn );
- d_defines.push_back( 1 );
-}
-
-void TheoryModel::toStreamFunction( Node n, std::ostream& out ){
- out << "(" << n;
- out << " : " << n.getType();
- out << " ";
- Node value = getValue( n );
- /*
- if( n.getType().isSort() ){
- int index = d_rep_set.getIndexFor( value );
- if( index!=-1 ){
- out << value.getType() << "_" << index;
- }else{
- out << value;
- }
- }else{
- */
- out << value;
- out << ")" << std::endl;
-}
-
-void TheoryModel::toStreamType( TypeNode tn, std::ostream& out ){
- out << "(" << tn;
- if( tn.isSort() ){
- if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){
- out << " " << d_rep_set.d_type_reps[tn].size();
- //out << " (";
- //for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){
- // if( i>0 ){ out << " "; }
- // out << d_rep_set.d_type_reps[tn][i];
- //}
- //out << ")";
- }
- }
- out << ")" << std::endl;
-}
-
-void TheoryModel::toStream( std::ostream& out ){
- /*//for debugging
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
- while( !eqcs_i.isFinished() ){
- Node eqc = (*eqcs_i);
- Debug("get-model-debug") << eqc << " : " << eqc.getType() << " : " << std::endl;
- out << " ";
- //add terms to model
- eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
- while( !eqc_i.isFinished() ){
- out << (*eqc_i) << " ";
- ++eqc_i;
- }
- out << std::endl;
- ++eqcs_i;
- }
- */
- int funcIndex = 0;
- int typeIndex = 0;
- for( size_t i=0; i<d_defines.size(); i++ ){
- if( d_defines[i]==0 ){
- toStreamFunction( d_define_funcs[funcIndex], out );
- funcIndex++;
- }else if( d_defines[i]==1 ){
- toStreamType( d_define_types[typeIndex], out );
- typeIndex++;
- }
- }
-}
-
-Node TheoryModel::getValue( TNode n ){
- Debug("model") << "TheoryModel::getValue " << n << std::endl;
-
- kind::MetaKind metakind = n.getMetaKind();
-
- //// special case: prop engine handles boolean vars
- //if(metakind == kind::metakind::VARIABLE && n.getType().isBoolean()) {
- // Debug("model") << "-> Propositional variable." << std::endl;
- // return d_te->getPropEngine()->getValue( n );
- //}
-
- // special case: value of a constant == itself
- if(metakind == kind::metakind::CONSTANT) {
- Debug("model") << "-> Constant." << std::endl;
- return n;
- }
-
- Node nn;
- if( n.getNumChildren()>0 ){
- std::vector< Node > children;
- if( metakind == kind::metakind::PARAMETERIZED ){
- Debug("model-debug") << "get operator: " << n.getOperator() << std::endl;
- children.push_back( n.getOperator() );
- }
- //evaluate the children
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- Node val = getValue( n[i] );
- Debug("model-debug") << i << " : " << n[i] << " -> " << val << std::endl;
- Assert( !val.isNull() );
- children.push_back( val );
- }
- Debug("model-debug") << "Done eval children" << std::endl;
- nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
- }else{
- nn = n;
- }
- //interpretation is the rewritten form
- nn = Rewriter::rewrite( nn );
-
- // special case: value of a constant == itself
- if(metakind == kind::metakind::CONSTANT) {
- Debug("model") << "-> Theory-interpreted term." << std::endl;
- return nn;
- }else{
- Debug("model") << "-> Model-interpreted term." << std::endl;
- //otherwise, get the interpreted value in the model
- return getInterpretedValue( nn );
- }
-}
-
-Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
- if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){
- //try to find a pre-existing arbitrary element
- for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){
- if( std::find( exclude.begin(), exclude.end(), d_rep_set.d_type_reps[tn][i] )==exclude.end() ){
- return d_rep_set.d_type_reps[tn][i];
- }
- }
- }
- return Node::null();
-}
-
-//FIXME: use the theory enumerator to generate constants here
-Node TheoryModel::getNewDomainValue( TypeNode tn ){
- if( tn==NodeManager::currentNM()->booleanType() ){
- if( d_rep_set.d_type_reps[tn].empty() ){
- return d_false;
- }else if( d_rep_set.d_type_reps[tn].size()==1 ){
- return NodeManager::currentNM()->mkConst( areEqual( d_rep_set.d_type_reps[tn][0], d_false ) );
- }else{
- return Node::null();
- }
- }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
- int val = 0;
- do{
- Node r = NodeManager::currentNM()->mkConst( Rational(val) );
- if( std::find( d_rep_set.d_type_reps[tn].begin(), d_rep_set.d_type_reps[tn].end(), r )==d_rep_set.d_type_reps[tn].end() &&
- !d_equalityEngine.hasTerm( r ) ){
- return r;
- }
- val++;
- }while( true );
- }else{
- //otherwise must make a variable FIXME: how to make constants for other sorts?
- //return NodeManager::currentNM()->mkVar( tn );
- return Node::null();
- }
-}
-
-/** assert equality */
-void TheoryModel::assertEquality( Node a, Node b, bool polarity ){
- d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() );
-}
-
-/** assert predicate */
-void TheoryModel::assertPredicate( Node a, bool polarity ){
- if( a.getKind()==EQUAL ){
- d_equalityEngine.assertEquality( a, polarity, Node::null() );
- }else{
- d_equalityEngine.assertPredicate( a, polarity, Node::null() );
- }
-}
-
-/** assert equality engine */
-void TheoryModel::assertEqualityEngine( eq::EqualityEngine* ee ){
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
- while( !eqcs_i.isFinished() ){
- Node eqc = (*eqcs_i);
- bool predicate = false;
- bool predPolarity = false;
- if( eqc.getType()==NodeManager::currentNM()->booleanType() ){
- predicate = true;
- predPolarity = ee->areEqual( eqc, d_true );
- //FIXME: do we guarentee that all boolean equivalence classes contain either d_true or d_false?
- }
- eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, ee );
- while( !eqc_i.isFinished() ){
- if( predicate ){
- assertPredicate( *eqc_i, predPolarity );
- }else{
- assertEquality( *eqc_i, eqc, true );
- }
- ++eqc_i;
- }
- ++eqcs_i;
- }
-}
-
-bool TheoryModel::hasTerm( Node a ){
- return d_equalityEngine.hasTerm( a );
-}
-
-Node TheoryModel::getRepresentative( Node a ){
- if( d_equalityEngine.hasTerm( a ) ){
- Node r = d_equalityEngine.getRepresentative( a );
- return d_reps[ r ];
- }else{
- return a;
- }
-}
-
-bool TheoryModel::areEqual( Node a, Node b ){
- if( a==b ){
- return true;
- }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
- return d_equalityEngine.areEqual( a, b );
- }else{
- return false;
- }
-}
-
-bool TheoryModel::areDisequal( Node a, Node b ){
- if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
- return d_equalityEngine.areDisequal( a, b, false );
- }else{
- return false;
- }
-}
-
-//for debugging
-void TheoryModel::printRepresentativeDebug( const char* c, Node r ){
- if( r.isNull() ){
- Debug( c ) << "null";
- }else if( r.getType()==NodeManager::currentNM()->booleanType() ){
- if( areEqual( r, d_true ) ){
- Debug( c ) << "true";
- }else{
- Debug( c ) << "false";
- }
- }else{
- Debug( c ) << getRepresentative( r );
- }
-}
-
-void TheoryModel::printRepresentative( std::ostream& out, Node r ){
- Assert( !r.isNull() );
- if( r.isNull() ){
- out << "null";
- }else if( r.getType()==NodeManager::currentNM()->booleanType() ){
- if( areEqual( r, d_true ) ){
- out << "true";
- }else{
- out << "false";
- }
- }else{
- out << getRepresentative( r );
- }
-}
-
-DefaultModel::DefaultModel( context::Context* c, std::string name, bool enableFuncModels ) :
-TheoryModel( c, name ), d_enableFuncModels( enableFuncModels ){
-
-}
-
-void DefaultModel::addTerm( Node n ){
- //must collect UF terms
- if( d_enableFuncModels && n.getKind()==APPLY_UF ){
- d_uf_terms[ n.getOperator() ].push_back( n );
- }
-}
-
-void DefaultModel::reset(){
- d_uf_terms.clear();
- d_uf_models.clear();
- TheoryModel::reset();
-}
-
-Node DefaultModel::getInterpretedValue( TNode n ){
- TypeNode type = n.getType();
- if( type.isFunction() || type.isPredicate() ){
- //for function models
- if( d_enableFuncModels ){
- if( d_uf_models.find( n )==d_uf_models.end() ){
- uf::UfModelTree ufmt( n );
- Node default_v;
- for( size_t i=0; i<d_uf_terms[n].size(); i++ ){
- Node un = d_uf_terms[n][i];
- Node v = getRepresentative( un );
- ufmt.setValue( this, un, v );
- default_v = v;
- }
- if( default_v.isNull() ){
- default_v = getInterpretedValue( NodeManager::currentNM()->mkVar( type.getRangeType() ) );
- }
- ufmt.setDefaultValue( this, default_v );
- ufmt.simplify();
- d_uf_models[n] = ufmt.getFunctionValue();
- }
- return d_uf_models[n];
- }else{
- return n;
- }
- }else{
- //first, see if the representative is defined
- if( d_equalityEngine.hasTerm( n ) ){
- n = d_equalityEngine.getRepresentative( n );
- //this check is required since d_equalityEngine.hasTerm( n )
- // does not ensure that n is in an equivalence class in d_equalityEngine
- if( d_reps.find( n )!=d_reps.end() ){
- return d_reps[n];
- }
- }
- //second, try to choose an existing term as value
- std::vector< Node > v_emp;
- Node n2 = getDomainValue( type, v_emp );
- if( !n2.isNull() ){
- return n2;
- }else{
- //otherwise, choose new value
- n2 = getNewDomainValue( type );
- if( !n2.isNull() ){
- return n2;
- }else{
- //otherwise, just return itself
- return n;
- }
- }
- }
-}
-
-TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){
-
-}
-
-void TheoryEngineModelBuilder::buildModel( Model* m ){
- TheoryModel* tm = (TheoryModel*)m;
- //reset representative information
- tm->reset();
- //collect model info from the theory engine
- Debug( "model-builder" ) << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
- d_te->collectModelInfo( tm );
- //unresolved equivalence classes
- std::map< Node, bool > unresolved_eqc;
- std::map< TypeNode, bool > unresolved_types;
- std::map< Node, std::vector< Node > > selects;
- std::map< Node, Node > apply_constructors;
- Debug( "model-builder" ) << "TheoryEngineModelBuilder: Build representatives..." << std::endl;
- //populate term database, store constant representatives
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine );
- while( !eqcs_i.isFinished() ){
- Node eqc = (*eqcs_i);
- TypeNode eqct = eqc.getType();
- //initialize unresolved type information
- initializeType( eqct, unresolved_types );
- //add terms to model, get constant rep if possible
- Node const_rep;
- eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &tm->d_equalityEngine );
- while( !eqc_i.isFinished() ){
- Node n = *eqc_i;
- //check if this is constant, if so, we will use it as representative
- if( n.getMetaKind()==kind::metakind::CONSTANT ){
- const_rep = n;
- }
- //theory-specific information needed
- if( n.getKind()==SELECT ){
- selects[ n[0] ].push_back( n );
- }else if( n.getKind()==APPLY_CONSTRUCTOR ){
- apply_constructors[ eqc ] = n;
- }
- //model-specific processing of the term, this will include
- tm->addTerm( n );
- ++eqc_i;
- }
- //store representative in representative set
- if( !const_rep.isNull() ){
- //Message() << "Constant rep " << const_rep << " for " << eqc << std::endl;
- tm->d_reps[ eqc ] = const_rep;
- tm->d_rep_set.add( const_rep );
- }else{
- //Message() << "** unresolved eqc " << eqc << std::endl;
- unresolved_eqc[ eqc ] = true;
- unresolved_types[ eqct ] = true;
- }
- ++eqcs_i;
- }
- //choose representatives for unresolved equivalence classes
- Debug( "model-builder" ) << "TheoryEngineModelBuilder: Complete model..." << std::endl;
- bool fixedPoint;
- do{
- fixedPoint = true;
- //for calculating unresolved types
- std::map< TypeNode, bool > unresolved_types_next;
- for( std::map< TypeNode, bool >::iterator it = unresolved_types.begin(); it != unresolved_types.end(); ++it ){
- unresolved_types_next[ it->first ] = false;
- }
- //try to resolve each unresolved equivalence class
- for( std::map< Node, bool >::iterator it = unresolved_eqc.begin(); it != unresolved_eqc.end(); ++it ){
- if( it->second ){
- Node n = it->first;
- TypeNode tn = n.getType();
- Node rep;
- bool mkRep = true;
- if( tn.isArray() ){
- TypeNode index_t = tn.getArrayIndexType();
- TypeNode elem_t = tn.getArrayConstituentType();
- if( !unresolved_types[ index_t ] && !unresolved_types[ elem_t ] ){
- //collect all relevant set values of n
- std::vector< Node > arr_selects;
- std::vector< Node > arr_select_values;
- Node nbase = n;
- while( nbase.getKind()==STORE ){
- arr_selects.push_back( tm->getRepresentative( nbase[1] ) );
- arr_select_values.push_back( tm->getRepresentative( nbase[2] ) );
- nbase = nbase[0];
- }
- eq::EqClassIterator eqc_i = eq::EqClassIterator( n, &tm->d_equalityEngine );
- while( !eqc_i.isFinished() ){
- for( int i=0; i<(int)selects[ *eqc_i ].size(); i++ ){
- Node r = tm->getRepresentative( selects[ *eqc_i ][i][1] );
- if( std::find( arr_selects.begin(), arr_selects.end(), r )==arr_selects.end() ){
- arr_selects.push_back( r );
- arr_select_values.push_back( tm->getRepresentative( selects[ *eqc_i ][i] ) );
- }
- }
- ++eqc_i;
- }
- //now, construct based on select/value pairs
- //TODO: make this a constant
- rep = chooseRepresentative( tm, nbase );
- for( int i=0; i<(int)arr_selects.size(); i++ ){
- rep = NodeManager::currentNM()->mkNode( STORE, rep, arr_selects[i], arr_select_values[i] );
- }
- }
- mkRep = false;
- }else if( tn.isDatatype() ){
- if( apply_constructors.find( n )!=apply_constructors.end() ){
- Node ac = apply_constructors[n];
- std::vector< Node > children;
- children.push_back( ac.getOperator() );
- for( size_t i = 0; i<ac.getNumChildren(); i++ ){
- Node acir = ac[i];
- if( tm->d_equalityEngine.hasTerm( acir ) ){
- acir = tm->d_equalityEngine.getRepresentative( acir );
- }
- if( unresolved_eqc.find( acir )==unresolved_eqc.end() ){
- Message() << "TheoryEngineModelBuilder::buildModel : Datatype argument does not exist in the model " << acir << std::endl;
- acir = Node::null();
- }
- if( acir.isNull() || unresolved_eqc[ acir ] ){
- mkRep = false;
- break;
- }else{
- children.push_back( tm->getRepresentative( acir ) );
- }
- }
- if( mkRep ){
- rep = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
- }
- }else{
- Message() << "TheoryEngineModelBuilder::buildModel : Do not know how to resolve datatype equivalence class " << n << std::endl;
- }
- mkRep = false;
- }
- if( mkRep ){
- rep = chooseRepresentative( tm, n );
- }
- if( !rep.isNull() ){
- tm->assertEquality( n, rep, true );
- tm->d_reps[ n ] = rep;
- tm->d_rep_set.add( rep );
- unresolved_eqc[ n ] = false;
- fixedPoint = false;
- }else{
- unresolved_types_next[ tn ] = true;
- }
- }
- }
- //for calculating unresolved types
- for( std::map< TypeNode, bool >::iterator it = unresolved_types.begin(); it != unresolved_types.end(); ++it ){
- unresolved_types[ it->first ] = unresolved_types_next[ it->first ];
- }
- }while( !fixedPoint );
-
- //for all unresolved equivalence classes, just get new domain value
- // this should typically never happen (all equivalence classes should be resolved at this point)
- for( std::map< Node, bool >::iterator it = unresolved_eqc.begin(); it != unresolved_eqc.end(); ++it ){
- if( it->second ){
- Node n = it->first;
- Node rep = chooseRepresentative( tm, n );
- tm->assertEquality( n, rep, true );
- tm->d_reps[ n ] = rep;
- tm->d_rep_set.add( rep );
- //FIXME: Assertion failure here?
- Message() << "Warning : Unresolved eqc, assigning " << rep << " for eqc( " << n << " ), type = " << n.getType() << std::endl;
- }
- }
-
- //model-specific initialization
- processBuildModel( tm );
-}
-
-void TheoryEngineModelBuilder::initializeType( TypeNode tn, std::map< TypeNode, bool >& unresolved_types ){
- if( unresolved_types.find( tn )==unresolved_types.end() ){
- unresolved_types[tn] = false;
- if( tn.isArray() ){
- initializeType( tn.getArrayIndexType(), unresolved_types );
- initializeType( tn.getArrayConstituentType(), unresolved_types );
- }else if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- for( size_t i = 0; i<dt.getNumConstructors(); i++ ){
- for( size_t j = 0; j<dt[i].getNumArgs(); j++ ){
- initializeType( TypeNode::fromType( dt[i][j].getType() ), unresolved_types );
- }
- }
- }
- }
-}
-
-Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc ){
- //try to get a new domain value
- Node rep = m->getNewDomainValue( eqc.getType() );
- if( !rep.isNull() ){
- return rep;
- }else{
- //if we can't get new domain value, just return eqc itself (this typically should not happen)
- //FIXME: Assertion failure here?
- return eqc;
- }
-}
+/********************* */ +/*! \file model.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 model class + **/ + +#include "theory/model.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" +#include "util/datatype.h" +#include "theory/uf/theory_uf_model.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; + +void RepSet::clear(){ + d_type_reps.clear(); + d_tmap.clear(); +} + +void RepSet::add( Node n ){ + TypeNode t = n.getType(); + d_tmap[ n ] = (int)d_type_reps[t].size(); + d_type_reps[t].push_back( n ); +} + +void RepSet::set( TypeNode t, std::vector< Node >& reps ){ + for( size_t i=0; i<reps.size(); i++ ){ + d_tmap[ reps[i] ] = i; + } + d_type_reps[t].insert( d_type_reps[t].begin(), reps.begin(), reps.end() ); +} + +void RepSet::toStream(std::ostream& out){ +#if 0 + for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){ + out << it->first << " : " << std::endl; + for( int i=0; i<(int)it->second.size(); i++ ){ + out << " " << i << ": " << it->second[i] << std::endl; + } + } +#else + for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){ + if( !it->first.isFunction() && !it->first.isPredicate() ){ + out << "(" << it->first << " " << it->second.size(); + out << " ("; + for( int i=0; i<(int)it->second.size(); i++ ){ + if( i>0 ){ out << " "; } + out << it->second[i]; + } + out << ")"; + out << ")" << std::endl; + } + } +#endif +} + +TheoryModel::TheoryModel( context::Context* c, std::string name ) : +d_equalityEngine( c, name ){ + d_true = NodeManager::currentNM()->mkConst( true ); + d_false = NodeManager::currentNM()->mkConst( false ); +} + +void TheoryModel::reset(){ + d_reps.clear(); + d_rep_set.clear(); +} + +void TheoryModel::addDefineFunction( Node n ){ + d_define_funcs.push_back( n ); + d_defines.push_back( 0 ); +} + +void TheoryModel::addDefineType( TypeNode tn ){ + d_define_types.push_back( tn ); + d_defines.push_back( 1 ); +} + +void TheoryModel::toStreamFunction( Node n, std::ostream& out ){ + out << "(" << n; + out << " : " << n.getType(); + out << " "; + Node value = getValue( n ); + /* + if( n.getType().isSort() ){ + int index = d_rep_set.getIndexFor( value ); + if( index!=-1 ){ + out << value.getType() << "_" << index; + }else{ + out << value; + } + }else{ + */ + out << value; + out << ")" << std::endl; +} + +void TheoryModel::toStreamType( TypeNode tn, std::ostream& out ){ + out << "(" << tn; + if( tn.isSort() ){ + if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){ + out << " " << d_rep_set.d_type_reps[tn].size(); + //out << " ("; + //for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){ + // if( i>0 ){ out << " "; } + // out << d_rep_set.d_type_reps[tn][i]; + //} + //out << ")"; + } + } + out << ")" << std::endl; +} + +void TheoryModel::toStream( std::ostream& out ){ + /*//for debugging + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + Debug("get-model-debug") << eqc << " : " << eqc.getType() << " : " << std::endl; + out << " "; + //add terms to model + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + out << (*eqc_i) << " "; + ++eqc_i; + } + out << std::endl; + ++eqcs_i; + } + */ + int funcIndex = 0; + int typeIndex = 0; + for( size_t i=0; i<d_defines.size(); i++ ){ + if( d_defines[i]==0 ){ + toStreamFunction( d_define_funcs[funcIndex], out ); + funcIndex++; + }else if( d_defines[i]==1 ){ + toStreamType( d_define_types[typeIndex], out ); + typeIndex++; + } + } +} + +Node TheoryModel::getValue( TNode n ){ + Debug("model") << "TheoryModel::getValue " << n << std::endl; + + kind::MetaKind metakind = n.getMetaKind(); + + //// special case: prop engine handles boolean vars + //if(metakind == kind::metakind::VARIABLE && n.getType().isBoolean()) { + // Debug("model") << "-> Propositional variable." << std::endl; + // return d_te->getPropEngine()->getValue( n ); + //} + + // special case: value of a constant == itself + if(metakind == kind::metakind::CONSTANT) { + Debug("model") << "-> Constant." << std::endl; + return n; + } + + Node nn; + if( n.getNumChildren()>0 ){ + std::vector< Node > children; + if( metakind == kind::metakind::PARAMETERIZED ){ + Debug("model-debug") << "get operator: " << n.getOperator() << std::endl; + children.push_back( n.getOperator() ); + } + //evaluate the children + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + Node val = getValue( n[i] ); + Debug("model-debug") << i << " : " << n[i] << " -> " << val << std::endl; + Assert( !val.isNull() ); + children.push_back( val ); + } + Debug("model-debug") << "Done eval children" << std::endl; + nn = NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + nn = n; + } + //interpretation is the rewritten form + nn = Rewriter::rewrite( nn ); + + // special case: value of a constant == itself + if(metakind == kind::metakind::CONSTANT) { + Debug("model") << "-> Theory-interpreted term." << std::endl; + return nn; + }else{ + Debug("model") << "-> Model-interpreted term." << std::endl; + //otherwise, get the interpreted value in the model + return getInterpretedValue( nn ); + } +} + +Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){ + if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){ + //try to find a pre-existing arbitrary element + for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){ + if( std::find( exclude.begin(), exclude.end(), d_rep_set.d_type_reps[tn][i] )==exclude.end() ){ + return d_rep_set.d_type_reps[tn][i]; + } + } + } + return Node::null(); +} + +//FIXME: use the theory enumerator to generate constants here +Node TheoryModel::getNewDomainValue( TypeNode tn ){ + if( tn==NodeManager::currentNM()->booleanType() ){ + if( d_rep_set.d_type_reps[tn].empty() ){ + return d_false; + }else if( d_rep_set.d_type_reps[tn].size()==1 ){ + return NodeManager::currentNM()->mkConst( areEqual( d_rep_set.d_type_reps[tn][0], d_false ) ); + }else{ + return Node::null(); + } + }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ + int val = 0; + do{ + Node r = NodeManager::currentNM()->mkConst( Rational(val) ); + if( std::find( d_rep_set.d_type_reps[tn].begin(), d_rep_set.d_type_reps[tn].end(), r )==d_rep_set.d_type_reps[tn].end() && + !d_equalityEngine.hasTerm( r ) ){ + return r; + } + val++; + }while( true ); + }else{ + //otherwise must make a variable FIXME: how to make constants for other sorts? + //return NodeManager::currentNM()->mkVar( tn ); + return Node::null(); + } +} + +/** assert equality */ +void TheoryModel::assertEquality( Node a, Node b, bool polarity ){ + d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() ); +} + +/** assert predicate */ +void TheoryModel::assertPredicate( Node a, bool polarity ){ + if( a.getKind()==EQUAL ){ + d_equalityEngine.assertEquality( a, polarity, Node::null() ); + }else{ + d_equalityEngine.assertPredicate( a, polarity, Node::null() ); + } +} + +/** assert equality engine */ +void TheoryModel::assertEqualityEngine( eq::EqualityEngine* ee ){ + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + bool predicate = false; + bool predPolarity = false; + if( eqc.getType()==NodeManager::currentNM()->booleanType() ){ + predicate = true; + predPolarity = ee->areEqual( eqc, d_true ); + //FIXME: do we guarentee that all boolean equivalence classes contain either d_true or d_false? + } + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, ee ); + while( !eqc_i.isFinished() ){ + if( predicate ){ + assertPredicate( *eqc_i, predPolarity ); + }else{ + assertEquality( *eqc_i, eqc, true ); + } + ++eqc_i; + } + ++eqcs_i; + } +} + +bool TheoryModel::hasTerm( Node a ){ + return d_equalityEngine.hasTerm( a ); +} + +Node TheoryModel::getRepresentative( Node a ){ + if( d_equalityEngine.hasTerm( a ) ){ + Node r = d_equalityEngine.getRepresentative( a ); + return d_reps[ r ]; + }else{ + return a; + } +} + +bool TheoryModel::areEqual( Node a, Node b ){ + if( a==b ){ + return true; + }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ + return d_equalityEngine.areEqual( a, b ); + }else{ + return false; + } +} + +bool TheoryModel::areDisequal( Node a, Node b ){ + if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ + return d_equalityEngine.areDisequal( a, b, false ); + }else{ + return false; + } +} + +//for debugging +void TheoryModel::printRepresentativeDebug( const char* c, Node r ){ + if( r.isNull() ){ + Debug( c ) << "null"; + }else if( r.getType()==NodeManager::currentNM()->booleanType() ){ + if( areEqual( r, d_true ) ){ + Debug( c ) << "true"; + }else{ + Debug( c ) << "false"; + } + }else{ + Debug( c ) << getRepresentative( r ); + } +} + +void TheoryModel::printRepresentative( std::ostream& out, Node r ){ + Assert( !r.isNull() ); + if( r.isNull() ){ + out << "null"; + }else if( r.getType()==NodeManager::currentNM()->booleanType() ){ + if( areEqual( r, d_true ) ){ + out << "true"; + }else{ + out << "false"; + } + }else{ + out << getRepresentative( r ); + } +} + +DefaultModel::DefaultModel( context::Context* c, std::string name, bool enableFuncModels ) : +TheoryModel( c, name ), d_enableFuncModels( enableFuncModels ){ + +} + +void DefaultModel::addTerm( Node n ){ + //must collect UF terms + if( d_enableFuncModels && n.getKind()==APPLY_UF ){ + d_uf_terms[ n.getOperator() ].push_back( n ); + } +} + +void DefaultModel::reset(){ + d_uf_terms.clear(); + d_uf_models.clear(); + TheoryModel::reset(); +} + +Node DefaultModel::getInterpretedValue( TNode n ){ + TypeNode type = n.getType(); + if( type.isFunction() || type.isPredicate() ){ + //for function models + if( d_enableFuncModels ){ + if( d_uf_models.find( n )==d_uf_models.end() ){ + uf::UfModelTree ufmt( n ); + Node default_v; + for( size_t i=0; i<d_uf_terms[n].size(); i++ ){ + Node un = d_uf_terms[n][i]; + Node v = getRepresentative( un ); + ufmt.setValue( this, un, v ); + default_v = v; + } + if( default_v.isNull() ){ + default_v = getInterpretedValue( NodeManager::currentNM()->mkVar( type.getRangeType() ) ); + } + ufmt.setDefaultValue( this, default_v ); + ufmt.simplify(); + d_uf_models[n] = ufmt.getFunctionValue(); + } + return d_uf_models[n]; + }else{ + return n; + } + }else{ + //first, see if the representative is defined + if( d_equalityEngine.hasTerm( n ) ){ + n = d_equalityEngine.getRepresentative( n ); + //this check is required since d_equalityEngine.hasTerm( n ) + // does not ensure that n is in an equivalence class in d_equalityEngine + if( d_reps.find( n )!=d_reps.end() ){ + return d_reps[n]; + } + } + //second, try to choose an existing term as value + std::vector< Node > v_emp; + Node n2 = getDomainValue( type, v_emp ); + if( !n2.isNull() ){ + return n2; + }else{ + //otherwise, choose new value + n2 = getNewDomainValue( type ); + if( !n2.isNull() ){ + return n2; + }else{ + //otherwise, just return itself + return n; + } + } + } +} + +TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){ + +} + +void TheoryEngineModelBuilder::buildModel( Model* m ){ + TheoryModel* tm = (TheoryModel*)m; + //reset representative information + tm->reset(); + //collect model info from the theory engine + Debug( "model-builder" ) << "TheoryEngineModelBuilder: Collect model info..." << std::endl; + d_te->collectModelInfo( tm ); + //unresolved equivalence classes + std::map< Node, bool > unresolved_eqc; + std::map< TypeNode, bool > unresolved_types; + std::map< Node, std::vector< Node > > selects; + std::map< Node, Node > apply_constructors; + Debug( "model-builder" ) << "TheoryEngineModelBuilder: Build representatives..." << std::endl; + //populate term database, store constant representatives + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + TypeNode eqct = eqc.getType(); + //initialize unresolved type information + initializeType( eqct, unresolved_types ); + //add terms to model, get constant rep if possible + Node const_rep; + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &tm->d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + //check if this is constant, if so, we will use it as representative + if( n.getMetaKind()==kind::metakind::CONSTANT ){ + const_rep = n; + } + //theory-specific information needed + if( n.getKind()==SELECT ){ + selects[ n[0] ].push_back( n ); + }else if( n.getKind()==APPLY_CONSTRUCTOR ){ + apply_constructors[ eqc ] = n; + } + //model-specific processing of the term, this will include + tm->addTerm( n ); + ++eqc_i; + } + //store representative in representative set + if( !const_rep.isNull() ){ + //Message() << "Constant rep " << const_rep << " for " << eqc << std::endl; + tm->d_reps[ eqc ] = const_rep; + tm->d_rep_set.add( const_rep ); + }else{ + //Message() << "** unresolved eqc " << eqc << std::endl; + unresolved_eqc[ eqc ] = true; + unresolved_types[ eqct ] = true; + } + ++eqcs_i; + } + //choose representatives for unresolved equivalence classes + Debug( "model-builder" ) << "TheoryEngineModelBuilder: Complete model..." << std::endl; + bool fixedPoint; + do{ + fixedPoint = true; + //for calculating unresolved types + std::map< TypeNode, bool > unresolved_types_next; + for( std::map< TypeNode, bool >::iterator it = unresolved_types.begin(); it != unresolved_types.end(); ++it ){ + unresolved_types_next[ it->first ] = false; + } + //try to resolve each unresolved equivalence class + for( std::map< Node, bool >::iterator it = unresolved_eqc.begin(); it != unresolved_eqc.end(); ++it ){ + if( it->second ){ + Node n = it->first; + TypeNode tn = n.getType(); + Node rep; + bool mkRep = true; + if( tn.isArray() ){ + TypeNode index_t = tn.getArrayIndexType(); + TypeNode elem_t = tn.getArrayConstituentType(); + if( !unresolved_types[ index_t ] && !unresolved_types[ elem_t ] ){ + //collect all relevant set values of n + std::vector< Node > arr_selects; + std::vector< Node > arr_select_values; + Node nbase = n; + while( nbase.getKind()==STORE ){ + arr_selects.push_back( tm->getRepresentative( nbase[1] ) ); + arr_select_values.push_back( tm->getRepresentative( nbase[2] ) ); + nbase = nbase[0]; + } + eq::EqClassIterator eqc_i = eq::EqClassIterator( n, &tm->d_equalityEngine ); + while( !eqc_i.isFinished() ){ + for( int i=0; i<(int)selects[ *eqc_i ].size(); i++ ){ + Node r = tm->getRepresentative( selects[ *eqc_i ][i][1] ); + if( std::find( arr_selects.begin(), arr_selects.end(), r )==arr_selects.end() ){ + arr_selects.push_back( r ); + arr_select_values.push_back( tm->getRepresentative( selects[ *eqc_i ][i] ) ); + } + } + ++eqc_i; + } + //now, construct based on select/value pairs + //TODO: make this a constant + rep = chooseRepresentative( tm, nbase ); + for( int i=0; i<(int)arr_selects.size(); i++ ){ + rep = NodeManager::currentNM()->mkNode( STORE, rep, arr_selects[i], arr_select_values[i] ); + } + } + mkRep = false; + }else if( tn.isDatatype() ){ + if( apply_constructors.find( n )!=apply_constructors.end() ){ + Node ac = apply_constructors[n]; + std::vector< Node > children; + children.push_back( ac.getOperator() ); + for( size_t i = 0; i<ac.getNumChildren(); i++ ){ + Node acir = ac[i]; + if( tm->d_equalityEngine.hasTerm( acir ) ){ + acir = tm->d_equalityEngine.getRepresentative( acir ); + } + if( unresolved_eqc.find( acir )==unresolved_eqc.end() ){ + Message() << "TheoryEngineModelBuilder::buildModel : Datatype argument does not exist in the model " << acir << std::endl; + acir = Node::null(); + } + if( acir.isNull() || unresolved_eqc[ acir ] ){ + mkRep = false; + break; + }else{ + children.push_back( tm->getRepresentative( acir ) ); + } + } + if( mkRep ){ + rep = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + } + }else{ + Message() << "TheoryEngineModelBuilder::buildModel : Do not know how to resolve datatype equivalence class " << n << std::endl; + } + mkRep = false; + } + if( mkRep ){ + rep = chooseRepresentative( tm, n ); + } + if( !rep.isNull() ){ + tm->assertEquality( n, rep, true ); + tm->d_reps[ n ] = rep; + tm->d_rep_set.add( rep ); + unresolved_eqc[ n ] = false; + fixedPoint = false; + }else{ + unresolved_types_next[ tn ] = true; + } + } + } + //for calculating unresolved types + for( std::map< TypeNode, bool >::iterator it = unresolved_types.begin(); it != unresolved_types.end(); ++it ){ + unresolved_types[ it->first ] = unresolved_types_next[ it->first ]; + } + }while( !fixedPoint ); + + //for all unresolved equivalence classes, just get new domain value + // this should typically never happen (all equivalence classes should be resolved at this point) + for( std::map< Node, bool >::iterator it = unresolved_eqc.begin(); it != unresolved_eqc.end(); ++it ){ + if( it->second ){ + Node n = it->first; + Node rep = chooseRepresentative( tm, n ); + tm->assertEquality( n, rep, true ); + tm->d_reps[ n ] = rep; + tm->d_rep_set.add( rep ); + //FIXME: Assertion failure here? + Message() << "Warning : Unresolved eqc, assigning " << rep << " for eqc( " << n << " ), type = " << n.getType() << std::endl; + } + } + + //model-specific initialization + processBuildModel( tm ); +} + +void TheoryEngineModelBuilder::initializeType( TypeNode tn, std::map< TypeNode, bool >& unresolved_types ){ + if( unresolved_types.find( tn )==unresolved_types.end() ){ + unresolved_types[tn] = false; + if( tn.isArray() ){ + initializeType( tn.getArrayIndexType(), unresolved_types ); + initializeType( tn.getArrayConstituentType(), unresolved_types ); + }else if( tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for( size_t i = 0; i<dt.getNumConstructors(); i++ ){ + for( size_t j = 0; j<dt[i].getNumArgs(); j++ ){ + initializeType( TypeNode::fromType( dt[i][j].getType() ), unresolved_types ); + } + } + } + } +} + +Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc ){ + //try to get a new domain value + Node rep = m->getNewDomainValue( eqc.getType() ); + if( !rep.isNull() ){ + return rep; + }else{ + //if we can't get new domain value, just return eqc itself (this typically should not happen) + //FIXME: Assertion failure here? + return eqc; + } +} diff --git a/src/theory/model.h b/src/theory/model.h index 415b008ef..940a2f527 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -1,191 +1,191 @@ -/********************* */
-/*! \file model.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, 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 Model class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_MODEL_H
-#define __CVC4__THEORY_MODEL_H
-
-#include "util/model.h"
-#include "theory/uf/equality_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-class QuantifiersEngine;
-
-/** this class stores a representative set */
-class RepSet {
-public:
- RepSet(){}
- ~RepSet(){}
- std::map< TypeNode, std::vector< Node > > d_type_reps;
- std::map< Node, int > d_tmap;
- /** clear the set */
- void clear();
- /** has type */
- bool hasType( TypeNode tn ) { return d_type_reps.find( tn )!=d_type_reps.end(); }
- /** add representative for type */
- void add( Node n );
- /** set the representatives for type */
- void set( TypeNode t, std::vector< Node >& reps );
- /** returns index in d_type_reps for node n */
- int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; }
- /** debug print */
- void toStream(std::ostream& out);
-};
-
-//representative domain
-typedef std::vector< int > RepDomain;
-
-class TheoryEngineModelBuilder;
-
-/** Theory Model class
- * For Model m, should call m.initialize() before using
- */
-class TheoryModel : public Model
-{
- friend class TheoryEngineModelBuilder;
-protected:
- /** add term function
- * This should be called on all terms that exist in the model.
- * addTerm( n ) will do any model-specific processing necessary for n,
- * such as contraining the interpretation of uninterpretted functions.
- */
- virtual void addTerm( Node n ) {}
-private:
- /** List of definitions that the user has given
- * This is necessary for supporting the get-model command.
- */
- std::vector< Node > d_define_funcs;
- std::vector< TypeNode > d_define_types;
- std::vector< int > d_defines;
-protected:
- /** print the value of the function n to stream */
- virtual void toStreamFunction( Node n, std::ostream& out );
- /** print the value of the type tn to stream */
- virtual void toStreamType( TypeNode tn, std::ostream& out );
-public:
- TheoryModel( context::Context* c, std::string name );
- virtual ~TheoryModel(){}
- /** equality engine containing all known equalities/disequalities */
- eq::EqualityEngine d_equalityEngine;
- /** map of representatives of equality engine to used representatives in representative set */
- std::map< Node, Node > d_reps;
- /** stores set of representatives for each type */
- RepSet d_rep_set;
- /** true/false nodes */
- Node d_true;
- Node d_false;
-public:
- /** reset the model */
- virtual void reset();
- /** get interpreted value
- * This function is called when the value of the node cannot be determined by the theory rewriter
- * This should function should return a representative in d_reps
- */
- virtual Node getInterpretedValue( TNode n ) = 0;
-public:
- /** add defined function (for get-model) */
- void addDefineFunction( Node n );
- /** add defined type (for get-model) */
- void addDefineType( TypeNode tn );
- /**
- * Get value function. This should be called only after a ModelBuilder has called buildModel(...)
- * on this model.
- */
- Node getValue( TNode n );
- /** get existing domain value, with possible exclusions
- * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
- */
- Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );
- /** get new domain value
- * This function returns a constant term of type tn that is not in d_rep_set.d_type_reps[tn]
- * If it cannot find such a node, it returns null.
- */
- Node getNewDomainValue( TypeNode tn );
-public:
- /** assert equality holds in the model */
- void assertEquality( Node a, Node b, bool polarity );
- /** assert predicate holds in the model */
- void assertPredicate( Node a, bool polarity );
- /** assert all equalities/predicates in equality engine hold in the model */
- void assertEqualityEngine( eq::EqualityEngine* ee );
-public:
- /** general queries */
- bool hasTerm( Node a );
- Node getRepresentative( Node a );
- bool areEqual( Node a, Node b );
- bool areDisequal( Node a, Node b );
-public:
- /** print representative debug function */
- void printRepresentativeDebug( const char* c, Node r );
- /** print representative function */
- void printRepresentative( std::ostream& out, Node r );
- /** to stream function */
- void toStream( std::ostream& out );
-};
-
-/** Default model class
- * The getInterpretedValue function will choose an existing value arbitrarily.
- * If none are found, then it will create a new value.
- */
-class DefaultModel : public TheoryModel
-{
-protected:
- /** whether function models are enabled */
- bool d_enableFuncModels;
- /** add term */
- void addTerm( Node n );
-public:
- DefaultModel( context::Context* c, std::string name, bool enableFuncModels );
- virtual ~DefaultModel(){}
- //necessary information for function models
- std::map< Node, std::vector< Node > > d_uf_terms;
- std::map< Node, Node > d_uf_models;
-public:
- void reset();
- Node getInterpretedValue( TNode n );
-};
-
-/** TheoryEngineModelBuilder class
- * This model builder will consult all theories in a theory engine for
- * collectModelInfo( ... ) when building a model.
- */
-class TheoryEngineModelBuilder : public ModelBuilder
-{
-protected:
- /** pointer to theory engine */
- TheoryEngine* d_te;
- /** choose representative for unresolved equivalence class */
- void initializeType( TypeNode tn, std::map< TypeNode, bool >& unresolved_types );
- /** process build model */
- virtual void processBuildModel( TheoryModel* m ){}
- /** choose representative for unconstrained equivalence class */
- virtual Node chooseRepresentative( TheoryModel* m, Node eqc );
-public:
- TheoryEngineModelBuilder( TheoryEngine* te );
- virtual ~TheoryEngineModelBuilder(){}
- /** Build model function.
- * Should be called only on TheoryModels m
- */
- void buildModel( Model* m );
-};
-
-}
-}
-
-#endif
+/********************* */ +/*! \file model.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, 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 Model class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_MODEL_H +#define __CVC4__THEORY_MODEL_H + +#include "util/model.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +/** this class stores a representative set */ +class RepSet { +public: + RepSet(){} + ~RepSet(){} + std::map< TypeNode, std::vector< Node > > d_type_reps; + std::map< Node, int > d_tmap; + /** clear the set */ + void clear(); + /** has type */ + bool hasType( TypeNode tn ) { return d_type_reps.find( tn )!=d_type_reps.end(); } + /** add representative for type */ + void add( Node n ); + /** set the representatives for type */ + void set( TypeNode t, std::vector< Node >& reps ); + /** returns index in d_type_reps for node n */ + int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; } + /** debug print */ + void toStream(std::ostream& out); +}; + +//representative domain +typedef std::vector< int > RepDomain; + +class TheoryEngineModelBuilder; + +/** Theory Model class + * For Model m, should call m.initialize() before using + */ +class TheoryModel : public Model +{ + friend class TheoryEngineModelBuilder; +protected: + /** add term function + * This should be called on all terms that exist in the model. + * addTerm( n ) will do any model-specific processing necessary for n, + * such as contraining the interpretation of uninterpretted functions. + */ + virtual void addTerm( Node n ) {} +private: + /** List of definitions that the user has given + * This is necessary for supporting the get-model command. + */ + std::vector< Node > d_define_funcs; + std::vector< TypeNode > d_define_types; + std::vector< int > d_defines; +protected: + /** print the value of the function n to stream */ + virtual void toStreamFunction( Node n, std::ostream& out ); + /** print the value of the type tn to stream */ + virtual void toStreamType( TypeNode tn, std::ostream& out ); +public: + TheoryModel( context::Context* c, std::string name ); + virtual ~TheoryModel(){} + /** equality engine containing all known equalities/disequalities */ + eq::EqualityEngine d_equalityEngine; + /** map of representatives of equality engine to used representatives in representative set */ + std::map< Node, Node > d_reps; + /** stores set of representatives for each type */ + RepSet d_rep_set; + /** true/false nodes */ + Node d_true; + Node d_false; +public: + /** reset the model */ + virtual void reset(); + /** get interpreted value + * This function is called when the value of the node cannot be determined by the theory rewriter + * This should function should return a representative in d_reps + */ + virtual Node getInterpretedValue( TNode n ) = 0; +public: + /** add defined function (for get-model) */ + void addDefineFunction( Node n ); + /** add defined type (for get-model) */ + void addDefineType( TypeNode tn ); + /** + * Get value function. This should be called only after a ModelBuilder has called buildModel(...) + * on this model. + */ + Node getValue( TNode n ); + /** get existing domain value, with possible exclusions + * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude + */ + Node getDomainValue( TypeNode tn, std::vector< Node >& exclude ); + /** get new domain value + * This function returns a constant term of type tn that is not in d_rep_set.d_type_reps[tn] + * If it cannot find such a node, it returns null. + */ + Node getNewDomainValue( TypeNode tn ); +public: + /** assert equality holds in the model */ + void assertEquality( Node a, Node b, bool polarity ); + /** assert predicate holds in the model */ + void assertPredicate( Node a, bool polarity ); + /** assert all equalities/predicates in equality engine hold in the model */ + void assertEqualityEngine( eq::EqualityEngine* ee ); +public: + /** general queries */ + bool hasTerm( Node a ); + Node getRepresentative( Node a ); + bool areEqual( Node a, Node b ); + bool areDisequal( Node a, Node b ); +public: + /** print representative debug function */ + void printRepresentativeDebug( const char* c, Node r ); + /** print representative function */ + void printRepresentative( std::ostream& out, Node r ); + /** to stream function */ + void toStream( std::ostream& out ); +}; + +/** Default model class + * The getInterpretedValue function will choose an existing value arbitrarily. + * If none are found, then it will create a new value. + */ +class DefaultModel : public TheoryModel +{ +protected: + /** whether function models are enabled */ + bool d_enableFuncModels; + /** add term */ + void addTerm( Node n ); +public: + DefaultModel( context::Context* c, std::string name, bool enableFuncModels ); + virtual ~DefaultModel(){} + //necessary information for function models + std::map< Node, std::vector< Node > > d_uf_terms; + std::map< Node, Node > d_uf_models; +public: + void reset(); + Node getInterpretedValue( TNode n ); +}; + +/** TheoryEngineModelBuilder class + * This model builder will consult all theories in a theory engine for + * collectModelInfo( ... ) when building a model. + */ +class TheoryEngineModelBuilder : public ModelBuilder +{ +protected: + /** pointer to theory engine */ + TheoryEngine* d_te; + /** choose representative for unresolved equivalence class */ + void initializeType( TypeNode tn, std::map< TypeNode, bool >& unresolved_types ); + /** process build model */ + virtual void processBuildModel( TheoryModel* m ){} + /** choose representative for unconstrained equivalence class */ + virtual Node chooseRepresentative( TheoryModel* m, Node eqc ); +public: + TheoryEngineModelBuilder( TheoryEngine* te ); + virtual ~TheoryEngineModelBuilder(){} + /** Build model function. + * Should be called only on TheoryModels m + */ + void buildModel( Model* m ); +}; + +} +} + +#endif diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 766bd31ae..1c6b47867 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -1,184 +1,184 @@ -/********************* */
-/*! \file first_order_model.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 model engine model class
- **/
-
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/rep_set_iterator.h"
-#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/term_database.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name, true ),
-d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){
-
-}
-
-void FirstOrderModel::reset(){
- //rebuild models
- d_uf_model_tree.clear();
- d_uf_model_gen.clear();
- d_array_model.clear();
- DefaultModel::reset();
-}
-
-void FirstOrderModel::addTerm( Node n ){
- //std::vector< Node > added;
- //d_term_db->addTerm( n, added, false );
- DefaultModel::addTerm( n );
-}
-
-void FirstOrderModel::initialize(){
- //this is called after representatives have been chosen and the equality engine has been built
- //for each quantifier, collect all operators we care about
- for( int i=0; i<getNumAssertedQuantifiers(); i++ ){
- Node f = getAssertedQuantifier( i );
- //initialize relevant models within bodies of all quantifiers
- initializeModelForTerm( f[1] );
- }
- //for debugging
- if( Options::current()->printModelEngine ){
- for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){
- if( it->first.isSort() ){
- Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
- }
- }
- }
-}
-
-void FirstOrderModel::initializeModelForTerm( Node n ){
- if( n.getKind()==APPLY_UF ){
- Node op = n.getOperator();
- if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){
- TypeNode tn = op.getType();
- tn = tn[ (int)tn.getNumChildren()-1 ];
- //only generate models for predicates and functions with uninterpreted range types
- if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){
- d_uf_model_tree[ op ] = uf::UfModelTree( op );
- d_uf_model_gen[ op ].clear();
- }
- }
- }
- /*
- if( n.getType().isArray() ){
- while( n.getKind()==STORE ){
- n = n[0];
- }
- Node nn = getRepresentative( n );
- if( d_array_model.find( nn )==d_array_model.end() ){
- d_array_model[nn] = arrays::ArrayModel( nn, this );
- }
- }
- */
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- initializeModelForTerm( n[i] );
- }
-}
-
-void FirstOrderModel::toStreamFunction( Node n, std::ostream& out ){
- /*
- if( d_uf_model.find( n )!=d_uf_model.end() ){
- //d_uf_model[n].toStream( out );
- Node value = d_uf_model[n].getFunctionValue();
- out << "(" << n << " " << value << ")";
- }else if( d_array_model.find( n )!=d_array_model.end() ){
- Node value = d_array_model[n].getArrayValue();
- out << "(" << n << " " << value << ")" << std::endl;
- }
- */
- DefaultModel::toStreamFunction( n, out );
-}
-
-void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){
- DefaultModel::toStreamType( tn, out );
-}
-
-Node FirstOrderModel::getInterpretedValue( TNode n ){
- Debug("fo-model") << "get interpreted value " << n << std::endl;
- TypeNode type = n.getType();
- if( type.isFunction() || type.isPredicate() ){
- if( d_uf_models.find( n )==d_uf_models.end() ){
- //use the model tree to generate the model
- Node fn = d_uf_model_tree[n].getFunctionValue();
- d_uf_models[n] = fn;
- return fn;
- }
- /*
- }else if( type.isArray() ){
- if( d_array_model.find( n )!=d_array_model.end() ){
- return d_array_model[n].getArrayValue();
- }else{
- //std::cout << "no array model generated for " << n << std::endl;
- }
- */
- }else if( n.getKind()==APPLY_UF ){
- Node op = n.getOperator();
- if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){
- //consult the uf model
- int depIndex;
- return d_uf_model_tree[ op ].getValue( this, n, depIndex );
- }
- }else if( n.getKind()==SELECT ){
-
- }
- return DefaultModel::getInterpretedValue( n );
-}
-
-TermDb* FirstOrderModel::getTermDatabase(){
- return d_term_db;
-}
-
-
-void FirstOrderModel::toStream(std::ostream& out){
- DefaultModel::toStream( out );
-#if 0
- out << "---Current Model---" << std::endl;
- out << "Representatives: " << std::endl;
- d_rep_set.toStream( out );
- out << "Functions: " << std::endl;
- for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
- it->second.toStream( out );
- out << std::endl;
- }
-#elif 0
- d_rep_set.toStream( out );
- //print everything not related to UF in equality engine
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
- while( !eqcs_i.isFinished() ){
- Node eqc = (*eqcs_i);
- Node rep = getRepresentative( eqc );
- TypeNode type = rep.getType();
- eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
- while( !eqc_i.isFinished() ){
- //do not print things that have interpretations in model
- if( (*eqc_i).getMetaKind()!=kind::metakind::CONSTANT && !hasInterpretedValue( *eqc_i ) ){
- out << "(" << (*eqc_i) << " " << rep << ")" << std::endl;
- }
- ++eqc_i;
- }
- ++eqcs_i;
- }
- //print functions
- for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
- it->second.toStream( out );
- out << std::endl;
- }
-#endif
+/********************* */ +/*! \file first_order_model.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 model engine model class + **/ + +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/rep_set_iterator.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name, true ), +d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){ + +} + +void FirstOrderModel::reset(){ + //rebuild models + d_uf_model_tree.clear(); + d_uf_model_gen.clear(); + d_array_model.clear(); + DefaultModel::reset(); +} + +void FirstOrderModel::addTerm( Node n ){ + //std::vector< Node > added; + //d_term_db->addTerm( n, added, false ); + DefaultModel::addTerm( n ); +} + +void FirstOrderModel::initialize(){ + //this is called after representatives have been chosen and the equality engine has been built + //for each quantifier, collect all operators we care about + for( int i=0; i<getNumAssertedQuantifiers(); i++ ){ + Node f = getAssertedQuantifier( i ); + //initialize relevant models within bodies of all quantifiers + initializeModelForTerm( f[1] ); + } + //for debugging + if( Options::current()->printModelEngine ){ + for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){ + if( it->first.isSort() ){ + Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + } + } + } +} + +void FirstOrderModel::initializeModelForTerm( Node n ){ + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){ + TypeNode tn = op.getType(); + tn = tn[ (int)tn.getNumChildren()-1 ]; + //only generate models for predicates and functions with uninterpreted range types + if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){ + d_uf_model_tree[ op ] = uf::UfModelTree( op ); + d_uf_model_gen[ op ].clear(); + } + } + } + /* + if( n.getType().isArray() ){ + while( n.getKind()==STORE ){ + n = n[0]; + } + Node nn = getRepresentative( n ); + if( d_array_model.find( nn )==d_array_model.end() ){ + d_array_model[nn] = arrays::ArrayModel( nn, this ); + } + } + */ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + initializeModelForTerm( n[i] ); + } +} + +void FirstOrderModel::toStreamFunction( Node n, std::ostream& out ){ + /* + if( d_uf_model.find( n )!=d_uf_model.end() ){ + //d_uf_model[n].toStream( out ); + Node value = d_uf_model[n].getFunctionValue(); + out << "(" << n << " " << value << ")"; + }else if( d_array_model.find( n )!=d_array_model.end() ){ + Node value = d_array_model[n].getArrayValue(); + out << "(" << n << " " << value << ")" << std::endl; + } + */ + DefaultModel::toStreamFunction( n, out ); +} + +void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){ + DefaultModel::toStreamType( tn, out ); +} + +Node FirstOrderModel::getInterpretedValue( TNode n ){ + Debug("fo-model") << "get interpreted value " << n << std::endl; + TypeNode type = n.getType(); + if( type.isFunction() || type.isPredicate() ){ + if( d_uf_models.find( n )==d_uf_models.end() ){ + //use the model tree to generate the model + Node fn = d_uf_model_tree[n].getFunctionValue(); + d_uf_models[n] = fn; + return fn; + } + /* + }else if( type.isArray() ){ + if( d_array_model.find( n )!=d_array_model.end() ){ + return d_array_model[n].getArrayValue(); + }else{ + //std::cout << "no array model generated for " << n << std::endl; + } + */ + }else if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){ + //consult the uf model + int depIndex; + return d_uf_model_tree[ op ].getValue( this, n, depIndex ); + } + }else if( n.getKind()==SELECT ){ + + } + return DefaultModel::getInterpretedValue( n ); +} + +TermDb* FirstOrderModel::getTermDatabase(){ + return d_term_db; +} + + +void FirstOrderModel::toStream(std::ostream& out){ + DefaultModel::toStream( out ); +#if 0 + out << "---Current Model---" << std::endl; + out << "Representatives: " << std::endl; + d_rep_set.toStream( out ); + out << "Functions: " << std::endl; + for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){ + it->second.toStream( out ); + out << std::endl; + } +#elif 0 + d_rep_set.toStream( out ); + //print everything not related to UF in equality engine + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + Node rep = getRepresentative( eqc ); + TypeNode type = rep.getType(); + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + //do not print things that have interpretations in model + if( (*eqc_i).getMetaKind()!=kind::metakind::CONSTANT && !hasInterpretedValue( *eqc_i ) ){ + out << "(" << (*eqc_i) << " " << rep << ")" << std::endl; + } + ++eqc_i; + } + ++eqcs_i; + } + //print functions + for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){ + it->second.toStream( out ); + out << std::endl; + } +#endif }
\ No newline at end of file diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 825518ed0..afa8dab79 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -1,89 +1,89 @@ -/********************* */
-/*! \file first_order_model.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, 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 Model extended classes
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__FIRST_ORDER_MODEL_H
-#define __CVC4__FIRST_ORDER_MODEL_H
-
-#include "theory/model.h"
-#include "theory/uf/theory_uf_model.h"
-#include "theory/arrays/theory_arrays_model.h"
-
-namespace CVC4 {
-namespace theory {
-
-struct ModelBasisAttributeId {};
-typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
-//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
-// 0 : term has no direct child with model basis attribute.
-struct ModelBasisArgAttributeId {};
-typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
-
-class QuantifiersEngine;
-
-namespace quantifiers{
-
-class TermDb;
-
-class FirstOrderModel : public DefaultModel
-{
-private:
- //pointer to term database
- TermDb* d_term_db;
- //add term function
- void addTerm( Node n );
- //for initialize model
- void initializeModelForTerm( Node n );
- /** to stream functions */
- void toStreamFunction( Node n, std::ostream& out );
- void toStreamType( TypeNode tn, std::ostream& out );
-public: //for Theory UF:
- //models for each UF operator
- std::map< Node, uf::UfModelTree > d_uf_model_tree;
- //model generators
- std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
-public: //for Theory Arrays:
- //default value for each non-store array
- std::map< Node, arrays::ArrayModel > d_array_model;
-public: //for Theory Quantifiers:
- /** list of quantifiers asserted in the current context */
- context::CDList<Node> d_forall_asserts;
- /** get number of asserted quantifiers */
- int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
- /** get asserted quantifier */
- Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
-public:
- FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name );
- virtual ~FirstOrderModel(){}
- // reset the model
- void reset();
- /** get interpreted value */
- Node getInterpretedValue( TNode n );
-public:
- // initialize the model
- void initialize();
- /** get term database */
- TermDb* getTermDatabase();
- /** to stream function */
- void toStream( std::ostream& out );
-};
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file first_order_model.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, 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 Model extended classes + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__FIRST_ORDER_MODEL_H +#define __CVC4__FIRST_ORDER_MODEL_H + +#include "theory/model.h" +#include "theory/uf/theory_uf_model.h" +#include "theory/arrays/theory_arrays_model.h" + +namespace CVC4 { +namespace theory { + +struct ModelBasisAttributeId {}; +typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute; +//for APPLY_UF terms, 1 : term has direct child with model basis attribute, +// 0 : term has no direct child with model basis attribute. +struct ModelBasisArgAttributeId {}; +typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute; + +class QuantifiersEngine; + +namespace quantifiers{ + +class TermDb; + +class FirstOrderModel : public DefaultModel +{ +private: + //pointer to term database + TermDb* d_term_db; + //add term function + void addTerm( Node n ); + //for initialize model + void initializeModelForTerm( Node n ); + /** to stream functions */ + void toStreamFunction( Node n, std::ostream& out ); + void toStreamType( TypeNode tn, std::ostream& out ); +public: //for Theory UF: + //models for each UF operator + std::map< Node, uf::UfModelTree > d_uf_model_tree; + //model generators + std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen; +public: //for Theory Arrays: + //default value for each non-store array + std::map< Node, arrays::ArrayModel > d_array_model; +public: //for Theory Quantifiers: + /** list of quantifiers asserted in the current context */ + context::CDList<Node> d_forall_asserts; + /** get number of asserted quantifiers */ + int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); } + /** get asserted quantifier */ + Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; } +public: + FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ); + virtual ~FirstOrderModel(){} + // reset the model + void reset(); + /** get interpreted value */ + Node getInterpretedValue( TNode n ); +public: + // initialize the model + void initialize(); + /** get term database */ + TermDb* getTermDatabase(); + /** to stream function */ + void toStream( std::ostream& out ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 13d500d8e..05eb8f55f 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -1,91 +1,91 @@ -/********************* */
-/*! \file model_builder.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** 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 Model Builder class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_MODEL_BUILDER_H
-#define __CVC4__QUANTIFIERS_MODEL_BUILDER_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/model.h"
-#include "theory/uf/theory_uf_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-//the model builder
-class ModelEngineBuilder : public TheoryEngineModelBuilder
-{
-protected:
- //quantifiers engine
- QuantifiersEngine* d_qe;
- //map from operators to model preference data
- std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
- //built model uf
- std::map< Node, bool > d_uf_model_constructed;
- /** process build model */
- void processBuildModel( TheoryModel* m );
- /** choose representative for unconstrained equivalence class */
- Node chooseRepresentative( TheoryModel* m, Node eqc );
- /** bad representative */
- bool isBadRepresentative( Node n );
-protected:
- //analyze model
- void analyzeModel( FirstOrderModel* fm );
- //analyze quantifiers
- void analyzeQuantifiers( FirstOrderModel* fm );
- //build model
- void finishBuildModel( FirstOrderModel* fm );
- //theory-specific build models
- void finishBuildModelUf( FirstOrderModel* fm, Node op );
- //do InstGen techniques for quantifier, return number of lemmas produced
- int doInstGen( FirstOrderModel* fm, Node f );
-public:
- ModelEngineBuilder( QuantifiersEngine* qe );
- virtual ~ModelEngineBuilder(){}
- /** finish model */
- void finishProcessBuildModel( TheoryModel* m );
-public:
- /** number of lemmas generated while building model */
- int d_addedLemmas;
- //map from quantifiers to if are constant SAT
- std::map< Node, bool > d_quant_sat;
- //map from quantifiers to the instantiation literals that their model is dependent upon
- std::map< Node, std::vector< Node > > d_quant_selection_lits;
-public:
- //map from quantifiers to model basis match
- std::map< Node, InstMatch > d_quant_basis_match;
- //options
- bool optUseModel();
- bool optInstGen();
- bool optOneQuantPerRoundInstGen();
- /** statistics class */
- class Statistics {
- public:
- IntStat d_pre_sat_quant;
- IntStat d_pre_nsat_quant;
- Statistics();
- ~Statistics();
- };
- Statistics d_statistics;
-};
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file model_builder.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: mdeters + ** 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 Model Builder class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_MODEL_BUILDER_H +#define __CVC4__QUANTIFIERS_MODEL_BUILDER_H + +#include "theory/quantifiers_engine.h" +#include "theory/model.h" +#include "theory/uf/theory_uf_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +//the model builder +class ModelEngineBuilder : public TheoryEngineModelBuilder +{ +protected: + //quantifiers engine + QuantifiersEngine* d_qe; + //map from operators to model preference data + std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; + //built model uf + std::map< Node, bool > d_uf_model_constructed; + /** process build model */ + void processBuildModel( TheoryModel* m ); + /** choose representative for unconstrained equivalence class */ + Node chooseRepresentative( TheoryModel* m, Node eqc ); + /** bad representative */ + bool isBadRepresentative( Node n ); +protected: + //analyze model + void analyzeModel( FirstOrderModel* fm ); + //analyze quantifiers + void analyzeQuantifiers( FirstOrderModel* fm ); + //build model + void finishBuildModel( FirstOrderModel* fm ); + //theory-specific build models + void finishBuildModelUf( FirstOrderModel* fm, Node op ); + //do InstGen techniques for quantifier, return number of lemmas produced + int doInstGen( FirstOrderModel* fm, Node f ); +public: + ModelEngineBuilder( QuantifiersEngine* qe ); + virtual ~ModelEngineBuilder(){} + /** finish model */ + void finishProcessBuildModel( TheoryModel* m ); +public: + /** number of lemmas generated while building model */ + int d_addedLemmas; + //map from quantifiers to if are constant SAT + std::map< Node, bool > d_quant_sat; + //map from quantifiers to the instantiation literals that their model is dependent upon + std::map< Node, std::vector< Node > > d_quant_selection_lits; +public: + //map from quantifiers to model basis match + std::map< Node, InstMatch > d_quant_basis_match; + //options + bool optUseModel(); + bool optInstGen(); + bool optOneQuantPerRoundInstGen(); + /** statistics class */ + class Statistics { + public: + IntStat d_pre_sat_quant; + IntStat d_pre_nsat_quant; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 12206e148..1563a3d1d 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -1,173 +1,173 @@ -/********************* */
-/*! \file relevant_domain.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 relevant domain class
- **/
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/relevant_domain.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/first_order_model.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){
-
-}
-
-void RelevantDomain::compute(){
- d_quant_inst_domain.clear();
- for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
- Node f = d_model->getAssertedQuantifier( i );
- d_quant_inst_domain[f].resize( f[0].getNumChildren() );
- }
- //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment)
- for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin();
- it != d_model->d_uf_model_tree.end(); ++it ){
- Node op = it->first;
- for( size_t i=0; i<d_model->d_uf_terms[op].size(); i++ ){
- Node n = d_model->d_uf_terms[op][i];
- //add arguments to domain
- for( int j=0; j<(int)n.getNumChildren(); j++ ){
- if( d_model->d_rep_set.hasType( n[j].getType() ) ){
- Node ra = d_model->getRepresentative( n[j] );
- int raIndex = d_model->d_rep_set.getIndexFor( ra );
- Assert( raIndex!=-1 );
- if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){
- d_active_domain[op][j].push_back( raIndex );
- }
- }
- }
- //add to range
- Node r = d_model->getRepresentative( n );
- int raIndex = d_model->d_rep_set.getIndexFor( r );
- Assert( raIndex!=-1 );
- if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){
- d_active_range[op].push_back( raIndex );
- }
- }
- }
- //find fixed point for relevant domain computation
- bool success;
- do{
- success = true;
- for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
- Node f = d_model->getAssertedQuantifier( i );
- //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment)
- if( computeRelevantInstantiationDomain( d_model->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, d_quant_inst_domain[f] ) ){
- success = false;
- }
- //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment)
- RepDomain range;
- if( extendFunctionDomains( d_model->getTermDatabase()->getCounterexampleBody( f ), range ) ){
- success = false;
- }
- }
- }while( !success );
-}
-
-bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ){
- bool domainChanged = false;
- if( n.getKind()==INST_CONSTANT ){
- bool domainSet = false;
- int vi = n.getAttribute(InstVarNumAttribute());
- Assert( !parent.isNull() );
- if( parent.getKind()==APPLY_UF ){
- //if the child of APPLY_UF term f( ... ), only consider the active domain of f at given argument
- Node op = parent.getOperator();
- if( d_active_domain.find( op )!=d_active_domain.end() ){
- for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){
- int d = d_active_domain[op][arg][i];
- if( std::find( rd[vi].begin(), rd[vi].end(), d )==rd[vi].end() ){
- rd[vi].push_back( d );
- domainChanged = true;
- }
- }
- domainSet = true;
- }
- }
- if( !domainSet ){
- //otherwise, we must consider the entire domain
- TypeNode tn = n.getType();
- if( d_model->d_rep_set.hasType( tn ) ){
- if( rd[vi].size()!=d_model->d_rep_set.d_type_reps[tn].size() ){
- rd[vi].clear();
- for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){
- rd[vi].push_back( i );
- domainChanged = true;
- }
- }
- }else{
- //infinite domain?
- }
- }
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){
- domainChanged = true;
- }
- }
- }
- return domainChanged;
-}
-
-bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
- if( n.getKind()==INST_CONSTANT ){
- Node f = n.getAttribute(InstConstantAttribute());
- int var = n.getAttribute(InstVarNumAttribute());
- range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() );
- return false;
- }else{
- Node op;
- if( n.getKind()==APPLY_UF ){
- op = n.getOperator();
- }
- bool domainChanged = false;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- RepDomain childRange;
- if( extendFunctionDomains( n[i], childRange ) ){
- domainChanged = true;
- }
- if( n.getKind()==APPLY_UF ){
- if( d_active_domain.find( op )!=d_active_domain.end() ){
- for( int j=0; j<(int)childRange.size(); j++ ){
- int v = childRange[j];
- if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){
- d_active_domain[op][i].push_back( v );
- domainChanged = true;
- }
- }
- }else{
- //do this?
- }
- }
- }
- //get the range
- if( n.hasAttribute(InstConstantAttribute()) ){
- if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){
- range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() );
- }else{
- //infinite range?
- }
- }else{
- Node r = d_model->getRepresentative( n );
- range.push_back( d_model->d_rep_set.getIndexFor( r ) );
- }
- return domainChanged;
- }
+/********************* */ +/*! \file relevant_domain.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 relevant domain class + **/ + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){ + +} + +void RelevantDomain::compute(){ + d_quant_inst_domain.clear(); + for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ + Node f = d_model->getAssertedQuantifier( i ); + d_quant_inst_domain[f].resize( f[0].getNumChildren() ); + } + //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment) + for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin(); + it != d_model->d_uf_model_tree.end(); ++it ){ + Node op = it->first; + for( size_t i=0; i<d_model->d_uf_terms[op].size(); i++ ){ + Node n = d_model->d_uf_terms[op][i]; + //add arguments to domain + for( int j=0; j<(int)n.getNumChildren(); j++ ){ + if( d_model->d_rep_set.hasType( n[j].getType() ) ){ + Node ra = d_model->getRepresentative( n[j] ); + int raIndex = d_model->d_rep_set.getIndexFor( ra ); + Assert( raIndex!=-1 ); + if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){ + d_active_domain[op][j].push_back( raIndex ); + } + } + } + //add to range + Node r = d_model->getRepresentative( n ); + int raIndex = d_model->d_rep_set.getIndexFor( r ); + Assert( raIndex!=-1 ); + if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){ + d_active_range[op].push_back( raIndex ); + } + } + } + //find fixed point for relevant domain computation + bool success; + do{ + success = true; + for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ + Node f = d_model->getAssertedQuantifier( i ); + //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment) + if( computeRelevantInstantiationDomain( d_model->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, d_quant_inst_domain[f] ) ){ + success = false; + } + //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment) + RepDomain range; + if( extendFunctionDomains( d_model->getTermDatabase()->getCounterexampleBody( f ), range ) ){ + success = false; + } + } + }while( !success ); +} + +bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ){ + bool domainChanged = false; + if( n.getKind()==INST_CONSTANT ){ + bool domainSet = false; + int vi = n.getAttribute(InstVarNumAttribute()); + Assert( !parent.isNull() ); + if( parent.getKind()==APPLY_UF ){ + //if the child of APPLY_UF term f( ... ), only consider the active domain of f at given argument + Node op = parent.getOperator(); + if( d_active_domain.find( op )!=d_active_domain.end() ){ + for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){ + int d = d_active_domain[op][arg][i]; + if( std::find( rd[vi].begin(), rd[vi].end(), d )==rd[vi].end() ){ + rd[vi].push_back( d ); + domainChanged = true; + } + } + domainSet = true; + } + } + if( !domainSet ){ + //otherwise, we must consider the entire domain + TypeNode tn = n.getType(); + if( d_model->d_rep_set.hasType( tn ) ){ + if( rd[vi].size()!=d_model->d_rep_set.d_type_reps[tn].size() ){ + rd[vi].clear(); + for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){ + rd[vi].push_back( i ); + domainChanged = true; + } + } + }else{ + //infinite domain? + } + } + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){ + domainChanged = true; + } + } + } + return domainChanged; +} + +bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){ + if( n.getKind()==INST_CONSTANT ){ + Node f = n.getAttribute(InstConstantAttribute()); + int var = n.getAttribute(InstVarNumAttribute()); + range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() ); + return false; + }else{ + Node op; + if( n.getKind()==APPLY_UF ){ + op = n.getOperator(); + } + bool domainChanged = false; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + RepDomain childRange; + if( extendFunctionDomains( n[i], childRange ) ){ + domainChanged = true; + } + if( n.getKind()==APPLY_UF ){ + if( d_active_domain.find( op )!=d_active_domain.end() ){ + for( int j=0; j<(int)childRange.size(); j++ ){ + int v = childRange[j]; + if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){ + d_active_domain[op][i].push_back( v ); + domainChanged = true; + } + } + }else{ + //do this? + } + } + } + //get the range + if( n.hasAttribute(InstConstantAttribute()) ){ + if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){ + range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() ); + }else{ + //infinite range? + } + }else{ + Node r = d_model->getRepresentative( n ); + range.push_back( d_model->d_rep_set.getIndexFor( r ) ); + } + return domainChanged; + } }
\ No newline at end of file diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 362a39d6a..8c8ea6a42 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -1,54 +1,54 @@ -/********************* */
-/*! \file relevant_domain.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, 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 relevant domain class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__RELEVANT_DOMAIN_H
-#define __CVC4__RELEVANT_DOMAIN_H
-
-#include "theory/quantifiers/first_order_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class RelevantDomain
-{
-private:
- FirstOrderModel* d_model;
-
- //the domain of the arguments for each operator
- std::map< Node, std::map< int, RepDomain > > d_active_domain;
- //the range for each operator
- std::map< Node, RepDomain > d_active_range;
- //for computing relevant instantiation domain, return true if changed
- bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd );
- //for computing extended
- bool extendFunctionDomains( Node n, RepDomain& range );
-public:
- RelevantDomain( FirstOrderModel* m );
- virtual ~RelevantDomain(){}
- //compute the relevant domain
- void compute();
- //relevant instantiation domain for each quantifier
- std::map< Node, std::vector< RepDomain > > d_quant_inst_domain;
-};
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file relevant_domain.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, 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 relevant domain class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__RELEVANT_DOMAIN_H +#define __CVC4__RELEVANT_DOMAIN_H + +#include "theory/quantifiers/first_order_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class RelevantDomain +{ +private: + FirstOrderModel* d_model; + + //the domain of the arguments for each operator + std::map< Node, std::map< int, RepDomain > > d_active_domain; + //the range for each operator + std::map< Node, RepDomain > d_active_range; + //for computing relevant instantiation domain, return true if changed + bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ); + //for computing extended + bool extendFunctionDomains( Node n, RepDomain& range ); +public: + RelevantDomain( FirstOrderModel* m ); + virtual ~RelevantDomain(){} + //compute the relevant domain + void compute(); + //relevant instantiation domain for each quantifier + std::map< Node, std::vector< RepDomain > > d_quant_inst_domain; +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp index 516f85857..9c1c4c89e 100644 --- a/src/theory/quantifiers/rep_set_iterator.cpp +++ b/src/theory/quantifiers/rep_set_iterator.cpp @@ -1,517 +1,517 @@ -/********************* */
-/*! \file rep_set_iterator.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 relevant domain class
- **/
-
-#include "theory/quantifiers/rep_set_iterator.h"
-#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/term_database.h"
-
-#define USE_INDEX_ORDERING
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_model( model ){
- //store instantiation constants
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- d_index.push_back( 0 );
- }
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- //store default index order
- d_index_order.push_back( i );
- d_var_order[i] = i;
- //store default domain
- d_domain.push_back( RepDomain() );
- TypeNode tn = d_f[0][i].getType();
- if( tn.isSort() ){
- if( d_model->d_rep_set.hasType( tn ) ){
- for( int j=0; j<(int)d_model->d_rep_set.d_type_reps[d_f[0][i].getType()].size(); j++ ){
- d_domain[i].push_back( j );
- }
- }else{
- Unimplemented("Cannot create instantiation iterator for unknown uninterpretted sort");
- }
- }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
- Unimplemented("Cannot create instantiation iterator for arithmetic quantifier");
- }else if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- //if finite, then use type enumerator
- if( dt.isFinite() ){
- //DO_THIS: use type enumerator
- Unimplemented("Not yet implemented: instantiation iterator for finite datatype quantifier");
- }else{
- Unimplemented("Cannot create instantiation iterator for infinite datatype quantifier");
- }
- }else{
- Unimplemented("Cannot create instantiation iterator for quantifier");
- }
- }
-}
-
-void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
- d_index_order.clear();
- d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
- //make the d_var_order mapping
- for( int i=0; i<(int)d_index_order.size(); i++ ){
- d_var_order[d_index_order[i]] = i;
- }
-}
-
-void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
- d_domain.clear();
- d_domain.insert( d_domain.begin(), domain.begin(), domain.end() );
- //we are done if a domain is empty
- for( int i=0; i<(int)d_domain.size(); i++ ){
- if( d_domain[i].empty() ){
- d_index.clear();
- }
- }
-}
-
-void RepSetIterator::increment2( int counter ){
- Assert( !isFinished() );
-#ifdef DISABLE_EVAL_SKIP_MULTIPLE
- counter = (int)d_index.size()-1;
-#endif
- //increment d_index
- while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){
- counter--;
- }
- if( counter==-1 ){
- d_index.clear();
- }else{
- for( int i=(int)d_index.size()-1; i>counter; i-- ){
- d_index[i] = 0;
- //d_model->clearEvalFailed( i );
- }
- d_index[counter]++;
- //d_model->clearEvalFailed( counter );
- }
-}
-
-void RepSetIterator::increment(){
- if( !isFinished() ){
- increment2( (int)d_index.size()-1 );
- }
-}
-
-bool RepSetIterator::isFinished(){
- return d_index.empty();
-}
-
-void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){
- for( int i=0; i<(int)d_index.size(); i++ ){
- m.set( qe->getTermDatabase()->getInstantiationConstant( d_f, d_index_order[i] ), getTerm( i ));
- }
-}
-
-Node RepSetIterator::getTerm( int i ){
- TypeNode tn = d_f[0][d_index_order[i]].getType();
- Assert( d_model->d_rep_set.d_type_reps.find( tn )!=d_model->d_rep_set.d_type_reps.end() );
- int index = d_index_order[i];
- return d_model->d_rep_set.d_type_reps[tn][d_domain[index][d_index[index]]];
-}
-
-void RepSetIterator::debugPrint( const char* c ){
- for( int i=0; i<(int)d_index.size(); i++ ){
- Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl;
- }
-}
-
-void RepSetIterator::debugPrintSmall( const char* c ){
- Debug( c ) << "RI: ";
- for( int i=0; i<(int)d_index.size(); i++ ){
- Debug( c ) << d_index[i] << ": " << getTerm( i ) << " ";
- }
- Debug( c ) << std::endl;
-}
-
-RepSetEvaluator::RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ) : d_model( m ), d_riter( ri ){
- d_eval_formulas = 0;
- d_eval_uf_terms = 0;
- d_eval_lits = 0;
- d_eval_lits_unknown = 0;
-}
-
-//if evaluate( n ) = eVal,
-// let n' = d_riter * n be the formula n instantiated with the current values in r_iter
-// if eVal = 1, then n' is true, if eVal = -1, then n' is false,
-// if eVal = 0, then n' cannot be proven to be equal to phaseReq
-// if eVal is not 0, then
-// each n{d_riter->d_index[0]/x_0...d_riter->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
-int RepSetEvaluator::evaluate( Node n, int& depIndex ){
- ++d_eval_formulas;
- //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
- //Notice() << "Eval " << n << std::endl;
- if( n.getKind()==NOT ){
- int val = evaluate( n[0], depIndex );
- return val==1 ? -1 : ( val==-1 ? 1 : 0 );
- }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){
- int baseVal = n.getKind()==AND ? 1 : -1;
- int eVal = baseVal;
- int posDepIndex = d_riter->getNumTerms();
- int negDepIndex = -1;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- //evaluate subterm
- int childDepIndex;
- Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i];
- int eValT = evaluate( nn, childDepIndex );
- if( eValT==baseVal ){
- if( eVal==baseVal ){
- if( childDepIndex>negDepIndex ){
- negDepIndex = childDepIndex;
- }
- }
- }else if( eValT==-baseVal ){
- eVal = -baseVal;
- if( childDepIndex<posDepIndex ){
- posDepIndex = childDepIndex;
- if( posDepIndex==-1 ){
- break;
- }
- }
- }else if( eValT==0 ){
- if( eVal==baseVal ){
- eVal = 0;
- }
- }
- }
- if( eVal!=0 ){
- depIndex = eVal==-baseVal ? posDepIndex : negDepIndex;
- return eVal;
- }else{
- return 0;
- }
- }else if( n.getKind()==IFF || n.getKind()==XOR ){
- int depIndex1;
- int eVal = evaluate( n[0], depIndex1 );
- if( eVal!=0 ){
- int depIndex2;
- int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 );
- if( eVal2!=0 ){
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- return eVal==eVal2 ? 1 : -1;
- }
- }
- return 0;
- }else if( n.getKind()==ITE ){
- int depIndex1, depIndex2;
- int eVal = evaluate( n[0], depIndex1 );
- if( eVal==0 ){
- //evaluate children to see if they are the same value
- int eval1 = evaluate( n[1], depIndex1 );
- if( eval1!=0 ){
- int eval2 = evaluate( n[1], depIndex2 );
- if( eval1==eval2 ){
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- return eval1;
- }
- }
- }else{
- int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2 );
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- return eValT;
- }
- return 0;
- }else if( n.getKind()==FORALL ){
- return 0;
- }else{
- ++d_eval_lits;
- ////if we know we will fail again, immediately return
- //if( d_eval_failed.find( n )!=d_eval_failed.end() ){
- // if( d_eval_failed[n] ){
- // return -1;
- // }
- //}
- //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;
- int retVal = 0;
- depIndex = d_riter->getNumTerms()-1;
- Node val = evaluateTerm( n, depIndex );
- if( !val.isNull() ){
- if( d_model->areEqual( val, d_model->d_true ) ){
- retVal = 1;
- }else if( d_model->areEqual( val, d_model->d_false ) ){
- retVal = -1;
- }else{
- if( val.getKind()==EQUAL ){
- if( d_model->areEqual( val[0], val[1] ) ){
- retVal = 1;
- }else if( d_model->areDisequal( val[0], val[1] ) ){
- retVal = -1;
- }
- }
- }
- }
- if( retVal!=0 ){
- Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl;
- }else{
- ++d_eval_lits_unknown;
- Debug("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;
- //std::cout << "Neither true nor false : " << n << std::endl;
- //std::cout << " Value : " << val << std::endl;
- //for( int i=0; i<(int)n.getNumChildren(); i++ ){
- // std::cout << " " << i << " : " << n[i].getType() << std::endl;
- //}
- }
- return retVal;
- }
-}
-
-Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
- //Message() << "Eval term " << n << std::endl;
- if( !n.hasAttribute(InstConstantAttribute()) ){
- //if evaluating a ground term, just consult the standard getValue functionality
- depIndex = -1;
- return d_model->getValue( n );
- }else{
- Node val;
- depIndex = d_riter->getNumTerms()-1;
- //check the type of n
- if( n.getKind()==INST_CONSTANT ){
- int v = n.getAttribute(InstVarNumAttribute());
- depIndex = d_riter->d_var_order[ v ];
- val = d_riter->getTerm( v );
- }else if( n.getKind()==ITE ){
- int depIndex1, depIndex2;
- int eval = evaluate( n[0], depIndex1 );
- if( eval==0 ){
- //evaluate children to see if they are the same
- Node val1 = evaluateTerm( n[ 1 ], depIndex1 );
- Node val2 = evaluateTerm( n[ 2 ], depIndex2 );
- if( val1==val2 ){
- val = val1;
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- }else{
- return Node::null();
- }
- }else{
- val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2 );
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- }
- }else{
- std::vector< int > children_depIndex;
- //for select, pre-process read over writes
- if( n.getKind()==SELECT ){
-#if 1
- //std::cout << "Evaluate " << n << std::endl;
- Node sel = evaluateTerm( n[1], depIndex );
- if( sel.isNull() ){
- depIndex = d_riter->getNumTerms()-1;
- return Node::null();
- }
- Node arr = d_model->getRepresentative( n[0] );
- //if( n[0]!=d_model->getRepresentative( n[0] ) ){
- // std::cout << n[0] << " is " << d_model->getRepresentative( n[0] ) << std::endl;
- //}
- int tempIndex;
- int eval = 1;
- while( arr.getKind()==STORE && eval!=0 ){
- eval = evaluate( sel.eqNode( arr[1] ), tempIndex );
- depIndex = tempIndex > depIndex ? tempIndex : depIndex;
- if( eval==1 ){
- val = evaluateTerm( arr[2], tempIndex );
- depIndex = tempIndex > depIndex ? tempIndex : depIndex;
- return val;
- }else if( eval==-1 ){
- arr = arr[0];
- }
- }
- arr = evaluateTerm( arr, tempIndex );
- depIndex = tempIndex > depIndex ? tempIndex : depIndex;
- val = NodeManager::currentNM()->mkNode( SELECT, arr, sel );
-#else
- val = evaluateTermDefault( n, depIndex, children_depIndex );
-#endif
- }else{
- //default term evaluate : evaluate all children, recreate the value
- val = evaluateTermDefault( n, depIndex, children_depIndex );
- }
- if( !val.isNull() ){
- bool setVal = false;
- //custom ways of evaluating terms
- if( n.getKind()==APPLY_UF ){
- Node op = n.getOperator();
- //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
- //if it is a defined UF, then consult the interpretation
- if( d_model->d_uf_model_tree.find( op )!=d_model->d_uf_model_tree.end() ){
- ++d_eval_uf_terms;
- int argDepIndex = 0;
- //make the term model specifically for n
- makeEvalUfModel( n );
- //now, consult the model
- if( d_eval_uf_use_default[n] ){
- val = d_model->d_uf_model_tree[op].getValue( d_model, val, argDepIndex );
- }else{
- val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex );
- }
- //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
- //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );
- Assert( !val.isNull() );
- //recalculate the depIndex
- depIndex = -1;
- for( int i=0; i<argDepIndex; i++ ){
- int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
- Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
- if( children_depIndex[index]>depIndex ){
- depIndex = children_depIndex[index];
- }
- }
- setVal = true;
- }
- }else if( n.getKind()==SELECT ){
- //we are free to interpret this term however we want
- }
- //if not set already, rewrite and consult model for interpretation
- if( !setVal ){
- val = Rewriter::rewrite( val );
- if( val.getMetaKind()!=kind::metakind::CONSTANT ){
- //FIXME: we cannot do this until we trust all theories collectModelInfo!
- //val = d_model->getInterpretedValue( val );
- //val = d_model->getRepresentative( val );
- }
- }
- Debug("fmf-eval-debug") << "Evaluate term " << n << " = ";
- d_model->printRepresentativeDebug( "fmf-eval-debug", val );
- Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl;
- }
- }
- return val;
- }
-}
-
-Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){
- depIndex = -1;
- if( n.getNumChildren()==0 ){
- return n;
- }else{
- //first we must evaluate the arguments
- std::vector< Node > children;
- if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){
- children.push_back( n.getOperator() );
- }
- //for each argument, calculate its value, and the variables its value depends upon
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- childDepIndex.push_back( -1 );
- Node nn = evaluateTerm( n[i], childDepIndex[i] );
- if( nn.isNull() ){
- depIndex = d_riter->getNumTerms()-1;
- return nn;
- }else{
- children.push_back( nn );
- if( childDepIndex[i]>depIndex ){
- depIndex = childDepIndex[i];
- }
- }
- }
- //recreate the value
- Node val = NodeManager::currentNM()->mkNode( n.getKind(), children );
- return val;
- }
-}
-
-void RepSetEvaluator::clearEvalFailed( int index ){
- for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){
- d_eval_failed[ d_eval_failed_lits[index][i] ] = false;
- }
- d_eval_failed_lits[index].clear();
-}
-
-void RepSetEvaluator::makeEvalUfModel( Node n ){
- if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){
- makeEvalUfIndexOrder( n );
- if( !d_eval_uf_use_default[n] ){
- Node op = n.getOperator();
- d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] );
- d_model->d_uf_model_gen[op].makeModel( d_model, d_eval_uf_model[n] );
- //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl;
- //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 );
- }
- }
-}
-
-struct sortGetMaxVariableNum {
- std::map< Node, int > d_max_var_num;
- int computeMaxVariableNum( Node n ){
- if( n.getKind()==INST_CONSTANT ){
- return n.getAttribute(InstVarNumAttribute());
- }else if( n.hasAttribute(InstConstantAttribute()) ){
- int maxVal = -1;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- int val = getMaxVariableNum( n[i] );
- if( val>maxVal ){
- maxVal = val;
- }
- }
- return maxVal;
- }else{
- return -1;
- }
- }
- int getMaxVariableNum( Node n ){
- std::map< Node, int >::iterator it = d_max_var_num.find( n );
- if( it==d_max_var_num.end() ){
- int num = computeMaxVariableNum( n );
- d_max_var_num[n] = num;
- return num;
- }else{
- return it->second;
- }
- }
- bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));}
-};
-
-void RepSetEvaluator::makeEvalUfIndexOrder( Node n ){
- if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
-#ifdef USE_INDEX_ORDERING
- //sort arguments in order of least significant vs. most significant variable in default ordering
- std::map< Node, std::vector< int > > argIndex;
- std::vector< Node > args;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( argIndex.find( n[i] )==argIndex.end() ){
- args.push_back( n[i] );
- }
- argIndex[n[i]].push_back( i );
- }
- sortGetMaxVariableNum sgmvn;
- std::sort( args.begin(), args.end(), sgmvn );
- for( int i=0; i<(int)args.size(); i++ ){
- for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){
- d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] );
- }
- }
- bool useDefault = true;
- for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
- if( i!=d_eval_term_index_order[n][i] ){
- useDefault = false;
- break;
- }
- }
- d_eval_uf_use_default[n] = useDefault;
- Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : ";
- for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
- Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " ";
- }
- Debug("fmf-index-order") << std::endl;
-#else
- d_eval_uf_use_default[n] = true;
-#endif
- }
-}
-
-
+/********************* */ +/*! \file rep_set_iterator.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 relevant domain class + **/ + +#include "theory/quantifiers/rep_set_iterator.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/term_database.h" + +#define USE_INDEX_ORDERING + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_model( model ){ + //store instantiation constants + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + d_index.push_back( 0 ); + } + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + //store default index order + d_index_order.push_back( i ); + d_var_order[i] = i; + //store default domain + d_domain.push_back( RepDomain() ); + TypeNode tn = d_f[0][i].getType(); + if( tn.isSort() ){ + if( d_model->d_rep_set.hasType( tn ) ){ + for( int j=0; j<(int)d_model->d_rep_set.d_type_reps[d_f[0][i].getType()].size(); j++ ){ + d_domain[i].push_back( j ); + } + }else{ + Unimplemented("Cannot create instantiation iterator for unknown uninterpretted sort"); + } + }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ + Unimplemented("Cannot create instantiation iterator for arithmetic quantifier"); + }else if( tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + //if finite, then use type enumerator + if( dt.isFinite() ){ + //DO_THIS: use type enumerator + Unimplemented("Not yet implemented: instantiation iterator for finite datatype quantifier"); + }else{ + Unimplemented("Cannot create instantiation iterator for infinite datatype quantifier"); + } + }else{ + Unimplemented("Cannot create instantiation iterator for quantifier"); + } + } +} + +void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){ + d_index_order.clear(); + d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() ); + //make the d_var_order mapping + for( int i=0; i<(int)d_index_order.size(); i++ ){ + d_var_order[d_index_order[i]] = i; + } +} + +void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){ + d_domain.clear(); + d_domain.insert( d_domain.begin(), domain.begin(), domain.end() ); + //we are done if a domain is empty + for( int i=0; i<(int)d_domain.size(); i++ ){ + if( d_domain[i].empty() ){ + d_index.clear(); + } + } +} + +void RepSetIterator::increment2( int counter ){ + Assert( !isFinished() ); +#ifdef DISABLE_EVAL_SKIP_MULTIPLE + counter = (int)d_index.size()-1; +#endif + //increment d_index + while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){ + counter--; + } + if( counter==-1 ){ + d_index.clear(); + }else{ + for( int i=(int)d_index.size()-1; i>counter; i-- ){ + d_index[i] = 0; + //d_model->clearEvalFailed( i ); + } + d_index[counter]++; + //d_model->clearEvalFailed( counter ); + } +} + +void RepSetIterator::increment(){ + if( !isFinished() ){ + increment2( (int)d_index.size()-1 ); + } +} + +bool RepSetIterator::isFinished(){ + return d_index.empty(); +} + +void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){ + for( int i=0; i<(int)d_index.size(); i++ ){ + m.set( qe->getTermDatabase()->getInstantiationConstant( d_f, d_index_order[i] ), getTerm( i )); + } +} + +Node RepSetIterator::getTerm( int i ){ + TypeNode tn = d_f[0][d_index_order[i]].getType(); + Assert( d_model->d_rep_set.d_type_reps.find( tn )!=d_model->d_rep_set.d_type_reps.end() ); + int index = d_index_order[i]; + return d_model->d_rep_set.d_type_reps[tn][d_domain[index][d_index[index]]]; +} + +void RepSetIterator::debugPrint( const char* c ){ + for( int i=0; i<(int)d_index.size(); i++ ){ + Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl; + } +} + +void RepSetIterator::debugPrintSmall( const char* c ){ + Debug( c ) << "RI: "; + for( int i=0; i<(int)d_index.size(); i++ ){ + Debug( c ) << d_index[i] << ": " << getTerm( i ) << " "; + } + Debug( c ) << std::endl; +} + +RepSetEvaluator::RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ) : d_model( m ), d_riter( ri ){ + d_eval_formulas = 0; + d_eval_uf_terms = 0; + d_eval_lits = 0; + d_eval_lits_unknown = 0; +} + +//if evaluate( n ) = eVal, +// let n' = d_riter * n be the formula n instantiated with the current values in r_iter +// if eVal = 1, then n' is true, if eVal = -1, then n' is false, +// if eVal = 0, then n' cannot be proven to be equal to phaseReq +// if eVal is not 0, then +// each n{d_riter->d_index[0]/x_0...d_riter->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model +int RepSetEvaluator::evaluate( Node n, int& depIndex ){ + ++d_eval_formulas; + //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl; + //Notice() << "Eval " << n << std::endl; + if( n.getKind()==NOT ){ + int val = evaluate( n[0], depIndex ); + return val==1 ? -1 : ( val==-1 ? 1 : 0 ); + }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){ + int baseVal = n.getKind()==AND ? 1 : -1; + int eVal = baseVal; + int posDepIndex = d_riter->getNumTerms(); + int negDepIndex = -1; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + //evaluate subterm + int childDepIndex; + Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i]; + int eValT = evaluate( nn, childDepIndex ); + if( eValT==baseVal ){ + if( eVal==baseVal ){ + if( childDepIndex>negDepIndex ){ + negDepIndex = childDepIndex; + } + } + }else if( eValT==-baseVal ){ + eVal = -baseVal; + if( childDepIndex<posDepIndex ){ + posDepIndex = childDepIndex; + if( posDepIndex==-1 ){ + break; + } + } + }else if( eValT==0 ){ + if( eVal==baseVal ){ + eVal = 0; + } + } + } + if( eVal!=0 ){ + depIndex = eVal==-baseVal ? posDepIndex : negDepIndex; + return eVal; + }else{ + return 0; + } + }else if( n.getKind()==IFF || n.getKind()==XOR ){ + int depIndex1; + int eVal = evaluate( n[0], depIndex1 ); + if( eVal!=0 ){ + int depIndex2; + int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 ); + if( eVal2!=0 ){ + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + return eVal==eVal2 ? 1 : -1; + } + } + return 0; + }else if( n.getKind()==ITE ){ + int depIndex1, depIndex2; + int eVal = evaluate( n[0], depIndex1 ); + if( eVal==0 ){ + //evaluate children to see if they are the same value + int eval1 = evaluate( n[1], depIndex1 ); + if( eval1!=0 ){ + int eval2 = evaluate( n[1], depIndex2 ); + if( eval1==eval2 ){ + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + return eval1; + } + } + }else{ + int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2 ); + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + return eValT; + } + return 0; + }else if( n.getKind()==FORALL ){ + return 0; + }else{ + ++d_eval_lits; + ////if we know we will fail again, immediately return + //if( d_eval_failed.find( n )!=d_eval_failed.end() ){ + // if( d_eval_failed[n] ){ + // return -1; + // } + //} + //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl; + int retVal = 0; + depIndex = d_riter->getNumTerms()-1; + Node val = evaluateTerm( n, depIndex ); + if( !val.isNull() ){ + if( d_model->areEqual( val, d_model->d_true ) ){ + retVal = 1; + }else if( d_model->areEqual( val, d_model->d_false ) ){ + retVal = -1; + }else{ + if( val.getKind()==EQUAL ){ + if( d_model->areEqual( val[0], val[1] ) ){ + retVal = 1; + }else if( d_model->areDisequal( val[0], val[1] ) ){ + retVal = -1; + } + } + } + } + if( retVal!=0 ){ + Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl; + }else{ + ++d_eval_lits_unknown; + Debug("fmf-eval-amb") << "Neither true nor false : " << n << std::endl; + //std::cout << "Neither true nor false : " << n << std::endl; + //std::cout << " Value : " << val << std::endl; + //for( int i=0; i<(int)n.getNumChildren(); i++ ){ + // std::cout << " " << i << " : " << n[i].getType() << std::endl; + //} + } + return retVal; + } +} + +Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){ + //Message() << "Eval term " << n << std::endl; + if( !n.hasAttribute(InstConstantAttribute()) ){ + //if evaluating a ground term, just consult the standard getValue functionality + depIndex = -1; + return d_model->getValue( n ); + }else{ + Node val; + depIndex = d_riter->getNumTerms()-1; + //check the type of n + if( n.getKind()==INST_CONSTANT ){ + int v = n.getAttribute(InstVarNumAttribute()); + depIndex = d_riter->d_var_order[ v ]; + val = d_riter->getTerm( v ); + }else if( n.getKind()==ITE ){ + int depIndex1, depIndex2; + int eval = evaluate( n[0], depIndex1 ); + if( eval==0 ){ + //evaluate children to see if they are the same + Node val1 = evaluateTerm( n[ 1 ], depIndex1 ); + Node val2 = evaluateTerm( n[ 2 ], depIndex2 ); + if( val1==val2 ){ + val = val1; + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + }else{ + return Node::null(); + } + }else{ + val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2 ); + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + } + }else{ + std::vector< int > children_depIndex; + //for select, pre-process read over writes + if( n.getKind()==SELECT ){ +#if 1 + //std::cout << "Evaluate " << n << std::endl; + Node sel = evaluateTerm( n[1], depIndex ); + if( sel.isNull() ){ + depIndex = d_riter->getNumTerms()-1; + return Node::null(); + } + Node arr = d_model->getRepresentative( n[0] ); + //if( n[0]!=d_model->getRepresentative( n[0] ) ){ + // std::cout << n[0] << " is " << d_model->getRepresentative( n[0] ) << std::endl; + //} + int tempIndex; + int eval = 1; + while( arr.getKind()==STORE && eval!=0 ){ + eval = evaluate( sel.eqNode( arr[1] ), tempIndex ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + if( eval==1 ){ + val = evaluateTerm( arr[2], tempIndex ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + return val; + }else if( eval==-1 ){ + arr = arr[0]; + } + } + arr = evaluateTerm( arr, tempIndex ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + val = NodeManager::currentNM()->mkNode( SELECT, arr, sel ); +#else + val = evaluateTermDefault( n, depIndex, children_depIndex ); +#endif + }else{ + //default term evaluate : evaluate all children, recreate the value + val = evaluateTermDefault( n, depIndex, children_depIndex ); + } + if( !val.isNull() ){ + bool setVal = false; + //custom ways of evaluating terms + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; + //if it is a defined UF, then consult the interpretation + if( d_model->d_uf_model_tree.find( op )!=d_model->d_uf_model_tree.end() ){ + ++d_eval_uf_terms; + int argDepIndex = 0; + //make the term model specifically for n + makeEvalUfModel( n ); + //now, consult the model + if( d_eval_uf_use_default[n] ){ + val = d_model->d_uf_model_tree[op].getValue( d_model, val, argDepIndex ); + }else{ + val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex ); + } + //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; + //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe ); + Assert( !val.isNull() ); + //recalculate the depIndex + depIndex = -1; + for( int i=0; i<argDepIndex; i++ ){ + int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i]; + Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl; + if( children_depIndex[index]>depIndex ){ + depIndex = children_depIndex[index]; + } + } + setVal = true; + } + }else if( n.getKind()==SELECT ){ + //we are free to interpret this term however we want + } + //if not set already, rewrite and consult model for interpretation + if( !setVal ){ + val = Rewriter::rewrite( val ); + if( val.getMetaKind()!=kind::metakind::CONSTANT ){ + //FIXME: we cannot do this until we trust all theories collectModelInfo! + //val = d_model->getInterpretedValue( val ); + //val = d_model->getRepresentative( val ); + } + } + Debug("fmf-eval-debug") << "Evaluate term " << n << " = "; + d_model->printRepresentativeDebug( "fmf-eval-debug", val ); + Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl; + } + } + return val; + } +} + +Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){ + depIndex = -1; + if( n.getNumChildren()==0 ){ + return n; + }else{ + //first we must evaluate the arguments + std::vector< Node > children; + if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + //for each argument, calculate its value, and the variables its value depends upon + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + childDepIndex.push_back( -1 ); + Node nn = evaluateTerm( n[i], childDepIndex[i] ); + if( nn.isNull() ){ + depIndex = d_riter->getNumTerms()-1; + return nn; + }else{ + children.push_back( nn ); + if( childDepIndex[i]>depIndex ){ + depIndex = childDepIndex[i]; + } + } + } + //recreate the value + Node val = NodeManager::currentNM()->mkNode( n.getKind(), children ); + return val; + } +} + +void RepSetEvaluator::clearEvalFailed( int index ){ + for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){ + d_eval_failed[ d_eval_failed_lits[index][i] ] = false; + } + d_eval_failed_lits[index].clear(); +} + +void RepSetEvaluator::makeEvalUfModel( Node n ){ + if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){ + makeEvalUfIndexOrder( n ); + if( !d_eval_uf_use_default[n] ){ + Node op = n.getOperator(); + d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] ); + d_model->d_uf_model_gen[op].makeModel( d_model, d_eval_uf_model[n] ); + //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl; + //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 ); + } + } +} + +struct sortGetMaxVariableNum { + std::map< Node, int > d_max_var_num; + int computeMaxVariableNum( Node n ){ + if( n.getKind()==INST_CONSTANT ){ + return n.getAttribute(InstVarNumAttribute()); + }else if( n.hasAttribute(InstConstantAttribute()) ){ + int maxVal = -1; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + int val = getMaxVariableNum( n[i] ); + if( val>maxVal ){ + maxVal = val; + } + } + return maxVal; + }else{ + return -1; + } + } + int getMaxVariableNum( Node n ){ + std::map< Node, int >::iterator it = d_max_var_num.find( n ); + if( it==d_max_var_num.end() ){ + int num = computeMaxVariableNum( n ); + d_max_var_num[n] = num; + return num; + }else{ + return it->second; + } + } + bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));} +}; + +void RepSetEvaluator::makeEvalUfIndexOrder( Node n ){ + if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){ +#ifdef USE_INDEX_ORDERING + //sort arguments in order of least significant vs. most significant variable in default ordering + std::map< Node, std::vector< int > > argIndex; + std::vector< Node > args; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( argIndex.find( n[i] )==argIndex.end() ){ + args.push_back( n[i] ); + } + argIndex[n[i]].push_back( i ); + } + sortGetMaxVariableNum sgmvn; + std::sort( args.begin(), args.end(), sgmvn ); + for( int i=0; i<(int)args.size(); i++ ){ + for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){ + d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] ); + } + } + bool useDefault = true; + for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ + if( i!=d_eval_term_index_order[n][i] ){ + useDefault = false; + break; + } + } + d_eval_uf_use_default[n] = useDefault; + Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : "; + for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ + Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " "; + } + Debug("fmf-index-order") << std::endl; +#else + d_eval_uf_use_default[n] = true; +#endif + } +} + + diff --git a/src/theory/quantifiers/rep_set_iterator.h b/src/theory/quantifiers/rep_set_iterator.h index f6312ae5c..a5ec266a9 100644 --- a/src/theory/quantifiers/rep_set_iterator.h +++ b/src/theory/quantifiers/rep_set_iterator.h @@ -1,120 +1,120 @@ -/********************* */
-/*! \file rep_set_iterator.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, 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 rep_set_iterator class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__REP_SET_ITERATOR_H
-#define __CVC4__REP_SET_ITERATOR_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/first_order_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-/** this class iterates over a RepSet */
-class RepSetIterator {
-public:
- RepSetIterator( Node f, FirstOrderModel* model );
- ~RepSetIterator(){}
- //pointer to quantifier
- Node d_f;
- //pointer to model
- FirstOrderModel* d_model;
- //index we are considering
- std::vector< int > d_index;
- //domain we are considering
- std::vector< RepDomain > d_domain;
- //ordering for variables we are indexing over
- // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
- // then we consider instantiations in this order:
- // a/x a/y a/z
- // a/x b/y a/z
- // b/x a/y a/z
- // b/x b/y a/z
- // ...
- std::vector< int > d_index_order;
- //variables to index they are considered at
- // for example, if d_index_order = { 2, 0, 1 }
- // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
- std::map< int, int > d_var_order;
- //the instantiation constants of d_f
- std::vector< Node > d_ic;
- //the current terms we are considering
- std::vector< Node > d_terms;
-public:
- /** set index order */
- void setIndexOrder( std::vector< int >& indexOrder );
- /** set domain */
- void setDomain( std::vector< RepDomain >& domain );
- /** increment the iterator */
- void increment2( int counter );
- void increment();
- /** is the iterator finished? */
- bool isFinished();
- /** produce the match that this iterator represents */
- void getMatch( QuantifiersEngine* qe, InstMatch& m );
- /** get the i_th term we are considering */
- Node getTerm( int i );
- /** get the number of terms we are considering */
- int getNumTerms() { return d_f[0].getNumChildren(); }
- /** debug print */
- void debugPrint( const char* c );
- void debugPrintSmall( const char* c );
-};
-
-class RepSetEvaluator
-{
-private:
- FirstOrderModel* d_model;
- RepSetIterator* d_riter;
-private: //for Theory UF:
- //map from terms to the models used to calculate their value
- std::map< Node, bool > d_eval_uf_use_default;
- std::map< Node, uf::UfModelTree > d_eval_uf_model;
- void makeEvalUfModel( Node n );
- //index ordering to use for each term
- std::map< Node, std::vector< int > > d_eval_term_index_order;
- int getMaxVariableNum( int n );
- void makeEvalUfIndexOrder( Node n );
-private:
- //default evaluate term function
- Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex );
- //temporary storing which literals have failed
- void clearEvalFailed( int index );
- std::map< Node, bool > d_eval_failed;
- std::map< int, std::vector< Node > > d_eval_failed_lits;
-public:
- RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri );
- virtual ~RepSetEvaluator(){}
- /** evaluate functions */
- int evaluate( Node n, int& depIndex );
- Node evaluateTerm( Node n, int& depIndex );
-public:
- //statistics
- int d_eval_formulas;
- int d_eval_uf_terms;
- int d_eval_lits;
- int d_eval_lits_unknown;
-};
-
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file rep_set_iterator.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, 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 rep_set_iterator class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__REP_SET_ITERATOR_H +#define __CVC4__REP_SET_ITERATOR_H + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/first_order_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** this class iterates over a RepSet */ +class RepSetIterator { +public: + RepSetIterator( Node f, FirstOrderModel* model ); + ~RepSetIterator(){} + //pointer to quantifier + Node d_f; + //pointer to model + FirstOrderModel* d_model; + //index we are considering + std::vector< int > d_index; + //domain we are considering + std::vector< RepDomain > d_domain; + //ordering for variables we are indexing over + // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 }, + // then we consider instantiations in this order: + // a/x a/y a/z + // a/x b/y a/z + // b/x a/y a/z + // b/x b/y a/z + // ... + std::vector< int > d_index_order; + //variables to index they are considered at + // for example, if d_index_order = { 2, 0, 1 } + // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 } + std::map< int, int > d_var_order; + //the instantiation constants of d_f + std::vector< Node > d_ic; + //the current terms we are considering + std::vector< Node > d_terms; +public: + /** set index order */ + void setIndexOrder( std::vector< int >& indexOrder ); + /** set domain */ + void setDomain( std::vector< RepDomain >& domain ); + /** increment the iterator */ + void increment2( int counter ); + void increment(); + /** is the iterator finished? */ + bool isFinished(); + /** produce the match that this iterator represents */ + void getMatch( QuantifiersEngine* qe, InstMatch& m ); + /** get the i_th term we are considering */ + Node getTerm( int i ); + /** get the number of terms we are considering */ + int getNumTerms() { return d_f[0].getNumChildren(); } + /** debug print */ + void debugPrint( const char* c ); + void debugPrintSmall( const char* c ); +}; + +class RepSetEvaluator +{ +private: + FirstOrderModel* d_model; + RepSetIterator* d_riter; +private: //for Theory UF: + //map from terms to the models used to calculate their value + std::map< Node, bool > d_eval_uf_use_default; + std::map< Node, uf::UfModelTree > d_eval_uf_model; + void makeEvalUfModel( Node n ); + //index ordering to use for each term + std::map< Node, std::vector< int > > d_eval_term_index_order; + int getMaxVariableNum( int n ); + void makeEvalUfIndexOrder( Node n ); +private: + //default evaluate term function + Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ); + //temporary storing which literals have failed + void clearEvalFailed( int index ); + std::map< Node, bool > d_eval_failed; + std::map< int, std::vector< Node > > d_eval_failed_lits; +public: + RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ); + virtual ~RepSetEvaluator(){} + /** evaluate functions */ + int evaluate( Node n, int& depIndex ); + Node evaluateTerm( Node n, int& depIndex ); +public: + //statistics + int d_eval_formulas; + int d_eval_uf_terms; + int d_eval_lits; + int d_eval_lits_unknown; +}; + + +} +} +} + +#endif diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 1ebba49b5..2af6992f7 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -1,156 +1,156 @@ -/**********************/
-/*! \file term_database.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, 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 term database class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_TERM_DATABASE_H
-#define __CVC4__QUANTIFIERS_TERM_DATABASE_H
-
-#include "theory/theory.h"
-
-#include <map>
-
-namespace CVC4 {
-namespace theory {
-
-class QuantifiersEngine;
-
-namespace quantifiers {
-
-class TermArgTrie {
-private:
- bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex );
-public:
- /** the data */
- std::map< Node, TermArgTrie > d_data;
-public:
- bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }
-};/* class TermArgTrie */
-
-class TermDb {
- friend class ::CVC4::theory::QuantifiersEngine;
-private:
- /** reference to the quantifiers engine */
- QuantifiersEngine* d_quantEngine;
- /** calculated no match terms */
- bool d_matching_active;
- /** terms processed */
- std::hash_set< Node, NodeHashFunction > d_processed;
-public:
- TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){}
- ~TermDb(){}
- /** map from APPLY_UF operators to ground terms for that operator */
- std::map< Node, std::vector< Node > > d_op_map;
- /** map from APPLY_UF functions to trie */
- std::map< Node, TermArgTrie > d_func_map_trie;
- /** map from APPLY_UF predicates to trie */
- std::map< Node, TermArgTrie > d_pred_map_trie[2];
- /** map from type nodes to terms of that type */
- std::map< TypeNode, std::vector< Node > > d_type_map;
- /** add a term to the database */
- void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
- /** reset (calculate which terms are active) */
- void reset( Theory::Effort effort );
- /** set active */
- void setMatchingActive( bool a ) { d_matching_active = a; }
- /** get active */
- bool getMatchingActive() { return d_matching_active; }
-private:
- /** for efficient e-matching */
- void addTermEfficient( Node n, std::set< Node >& added);
-public:
- /** parent structure (for efficient E-matching):
- n -> op -> index -> L
- map from node "n" to a list of nodes "L", where each node n' in L
- has operator "op", and n'["index"] = n.
- for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... }
- */
- /* Todo replace int by size_t */
- std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction > , NodeHashFunction > d_parents;
- const std::vector<Node> & getParents(TNode n, TNode f, int arg);
-private:
- //map from types to model basis terms
- std::map< TypeNode, Node > d_model_basis_term;
- //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;
-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]; }
-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;
- /** map from universal quantifiers to their skolemized body */
- std::map< Node, Node > d_skolem_body;
- /** instantiation constants to universal quantifiers */
- std::map< Node, Node > d_inst_constants_map;
- /** map from universal quantifiers to their counterexample body */
- std::map< Node, Node > d_counterexample_body;
- /** free variable for instantiation constant type */
- std::map< TypeNode, Node > d_free_vars;
-private:
- /** make instantiation constants for */
- void makeInstantiationConstantsFor( Node f );
-public:
- /** map from universal quantifiers to the list of instantiation constants */
- std::map< Node, std::vector< Node > > d_inst_constants;
- /** set instantiation level attr */
- void setInstantiationLevelAttr( Node n, uint64_t level );
- /** set instantiation constant attr */
- void setInstantiationConstantAttr( Node n, Node f );
- /** get the i^th instantiation constant of f */
- Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; }
- /** get number of instantiation constants for f */
- int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); }
- /** get the ce body f[e/x] */
- Node getCounterexampleBody( Node f );
- /** get the skolemized body f[e/x] */
- Node getSkolemizedBody( Node f );
- /** returns node n with bound vars of f replaced by instantiation constants of f
- node n : is the futur pattern
- node f : is the quantifier containing which bind the variable
- return a pattern where the variable are replaced by variable for
- instantiation.
- */
- Node getSubstitutedNode( Node n, Node f );
- /** same as before but node f is just linked to the new pattern by the
- applied attribute
- vars the bind variable
- nvars the same variable but with an attribute
- */
- Node convertNodeToPattern( Node n, Node f,
- const std::vector<Node> & vars,
- const std::vector<Node> & nvars);
- /** get free variable for instantiation constant */
- Node getFreeVariableForInstConstant( Node n );
-};/* class TermDb */
-
-}
-}
-}
-
-#endif
+/**********************/ +/*! \file term_database.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, 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 term database class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_TERM_DATABASE_H +#define __CVC4__QUANTIFIERS_TERM_DATABASE_H + +#include "theory/theory.h" + +#include <map> + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +namespace quantifiers { + +class TermArgTrie { +private: + bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex ); +public: + /** the data */ + std::map< Node, TermArgTrie > d_data; +public: + bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); } +};/* class TermArgTrie */ + +class TermDb { + friend class ::CVC4::theory::QuantifiersEngine; +private: + /** reference to the quantifiers engine */ + QuantifiersEngine* d_quantEngine; + /** calculated no match terms */ + bool d_matching_active; + /** terms processed */ + std::hash_set< Node, NodeHashFunction > d_processed; +public: + TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){} + ~TermDb(){} + /** map from APPLY_UF operators to ground terms for that operator */ + std::map< Node, std::vector< Node > > d_op_map; + /** map from APPLY_UF functions to trie */ + std::map< Node, TermArgTrie > d_func_map_trie; + /** map from APPLY_UF predicates to trie */ + std::map< Node, TermArgTrie > d_pred_map_trie[2]; + /** map from type nodes to terms of that type */ + std::map< TypeNode, std::vector< Node > > d_type_map; + /** add a term to the database */ + void addTerm( Node n, std::set< Node >& added, bool withinQuant = false ); + /** reset (calculate which terms are active) */ + void reset( Theory::Effort effort ); + /** set active */ + void setMatchingActive( bool a ) { d_matching_active = a; } + /** get active */ + bool getMatchingActive() { return d_matching_active; } +private: + /** for efficient e-matching */ + void addTermEfficient( Node n, std::set< Node >& added); +public: + /** parent structure (for efficient E-matching): + n -> op -> index -> L + map from node "n" to a list of nodes "L", where each node n' in L + has operator "op", and n'["index"] = n. + for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... } + */ + /* Todo replace int by size_t */ + std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction > , NodeHashFunction > d_parents; + const std::vector<Node> & getParents(TNode n, TNode f, int arg); +private: + //map from types to model basis terms + std::map< TypeNode, Node > d_model_basis_term; + //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; +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]; } +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; + /** map from universal quantifiers to their skolemized body */ + std::map< Node, Node > d_skolem_body; + /** instantiation constants to universal quantifiers */ + std::map< Node, Node > d_inst_constants_map; + /** map from universal quantifiers to their counterexample body */ + std::map< Node, Node > d_counterexample_body; + /** free variable for instantiation constant type */ + std::map< TypeNode, Node > d_free_vars; +private: + /** make instantiation constants for */ + void makeInstantiationConstantsFor( Node f ); +public: + /** map from universal quantifiers to the list of instantiation constants */ + std::map< Node, std::vector< Node > > d_inst_constants; + /** set instantiation level attr */ + void setInstantiationLevelAttr( Node n, uint64_t level ); + /** set instantiation constant attr */ + void setInstantiationConstantAttr( Node n, Node f ); + /** get the i^th instantiation constant of f */ + Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; } + /** get number of instantiation constants for f */ + int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); } + /** get the ce body f[e/x] */ + Node getCounterexampleBody( Node f ); + /** get the skolemized body f[e/x] */ + Node getSkolemizedBody( Node f ); + /** returns node n with bound vars of f replaced by instantiation constants of f + node n : is the futur pattern + node f : is the quantifier containing which bind the variable + return a pattern where the variable are replaced by variable for + instantiation. + */ + Node getSubstitutedNode( Node n, Node f ); + /** same as before but node f is just linked to the new pattern by the + applied attribute + vars the bind variable + nvars the same variable but with an attribute + */ + Node convertNodeToPattern( Node n, Node f, + const std::vector<Node> & vars, + const std::vector<Node> & nvars); + /** get free variable for instantiation constant */ + Node getFreeVariableForInstConstant( Node n ); +};/* class TermDb */ + +} +} +} + +#endif diff --git a/src/theory/rr_inst_match.cpp b/src/theory/rr_inst_match.cpp index 287f7475a..21a309610 100644 --- a/src/theory/rr_inst_match.cpp +++ b/src/theory/rr_inst_match.cpp @@ -958,7 +958,7 @@ Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){ arithmetic pattern */ std::map< Node, Node > d_arith_coeffs; if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){ - std::cout << "(?) Unknown matching pattern is " << pat << std::endl; + Message() << "(?) Unknown matching pattern is " << pat << std::endl; Unimplemented("pattern not implemented"); return new DumbMatcher(); }else{ @@ -1010,7 +1010,7 @@ PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){ std::map< Node, Node > d_arith_coeffs; if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){ Debug("inst-match-gen") << "(?) Unknown matching pattern is " << pat << std::endl; - std::cout << "(?) Unknown matching pattern is " << pat << std::endl; + Message() << "(?) Unknown matching pattern is " << pat << std::endl; return new DumbPatMatcher(); }else{ Debug("matching-arith") << "Generated arithmetic pattern for " << pat << ": " << std::endl; diff --git a/src/theory/rr_trigger.cpp b/src/theory/rr_trigger.cpp index 52e7efcc2..ece68d137 100644 --- a/src/theory/rr_trigger.cpp +++ b/src/theory/rr_trigger.cpp @@ -75,156 +75,156 @@ d_quantEngine( qe ), d_f( f ){ }else{ ++(qe->d_statistics.d_simple_triggers); } - }else{
+ }else{ Debug("multi-trigger") << "Multi-trigger " << (*this) << std::endl; //std::cout << "Multi-trigger for " << f << " : " << std::endl; //std::cout << " " << (*this) << std::endl; ++(qe->d_statistics.d_multi_triggers); } -}
-void Trigger::computeVarContains( Node n ) {
- if( d_var_contains.find( n )==d_var_contains.end() ){
- d_var_contains[n].clear();
- computeVarContains2( n, n );
- }
-}
-
-void Trigger::computeVarContains2( Node n, Node parent ){
- if( n.getKind()==INST_CONSTANT ){
- if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){
- d_var_contains[parent].push_back( n );
- }
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- computeVarContains2( n[i], parent );
- }
- }
} -
-void Trigger::resetInstantiationRound(){
- d_mg->resetInstantiationRound( d_quantEngine );
-}
-
+void Trigger::computeVarContains( Node n ) { + if( d_var_contains.find( n )==d_var_contains.end() ){ + d_var_contains[n].clear(); + computeVarContains2( n, n ); + } +} + +void Trigger::computeVarContains2( Node n, Node parent ){ + if( n.getKind()==INST_CONSTANT ){ + if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){ + d_var_contains[parent].push_back( n ); + } + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + computeVarContains2( n[i], parent ); + } + } +} + +void Trigger::resetInstantiationRound(){ + d_mg->resetInstantiationRound( d_quantEngine ); +} -bool Trigger::getNextMatch(){
- bool retVal = d_mg->getNextMatch( d_quantEngine );
- //m.makeInternal( d_quantEngine->getEqualityQuery() );
- return retVal;
-}
+ +bool Trigger::getNextMatch(){ + bool retVal = d_mg->getNextMatch( d_quantEngine ); + //m.makeInternal( d_quantEngine->getEqualityQuery() ); + return retVal; +} // bool Trigger::getMatch( Node t, InstMatch& m ){ // //FIXME: this assumes d_mg is an inst match generator // return ((InstMatchGenerator*)d_mg)->getMatch( t, m, d_quantEngine ); // } -
-int Trigger::addInstantiations( InstMatch& baseMatch ){
+ +int Trigger::addInstantiations( InstMatch& baseMatch ){ int addedLemmas = d_mg->addInstantiations( baseMatch, d_nodes[0].getAttribute(InstConstantAttribute()), - d_quantEngine);
- if( addedLemmas>0 ){
+ d_quantEngine); + if( addedLemmas>0 ){ Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was "; for( int i=0; i<(int)d_nodes.size(); i++ ){ Debug("inst-trigger") << d_nodes[i] << " "; } - Debug("inst-trigger") << std::endl;
- }
- return addedLemmas;
-}
-
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption,
- bool smartTriggers ){
- std::vector< Node > trNodes;
- if( !keepAll ){
- //only take nodes that contribute variables to the trigger when added
- std::vector< Node > temp;
- temp.insert( temp.begin(), nodes.begin(), nodes.end() );
- std::map< Node, bool > vars;
- std::map< Node, std::vector< Node > > patterns;
- for( int i=0; i<(int)temp.size(); i++ ){
- bool foundVar = false;
- computeVarContains( temp[i] );
- for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){
- Node v = d_var_contains[ temp[i] ][j];
- if( v.getAttribute(InstConstantAttribute())==f ){
- if( vars.find( v )==vars.end() ){
- vars[ v ] = true;
- foundVar = true;
- }
- }
- }
- if( foundVar ){
- trNodes.push_back( temp[i] );
- for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){
- Node v = d_var_contains[ temp[i] ][j];
- patterns[ v ].push_back( temp[i] );
- }
- }
- }
- //now, minimalize the trigger
- for( int i=0; i<(int)trNodes.size(); i++ ){
- bool keepPattern = false;
- Node n = trNodes[i];
- for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){
- Node v = d_var_contains[ n ][j];
- if( patterns[v].size()==1 ){
- keepPattern = true;
- break;
- }
- }
- if( !keepPattern ){
- //remove from pattern vector
- for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){
- Node v = d_var_contains[ n ][j];
- for( int k=0; k<(int)patterns[v].size(); k++ ){
- if( patterns[v][k]==n ){
- patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
- break;
- }
- }
- }
- //remove from trigger nodes
- trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
- i--;
- }
- }
- }else{
- trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
- }
-
- //check for duplicate?
- if( trOption==TR_MAKE_NEW ){
- //static int trNew = 0;
- //static int trOld = 0;
- //Trigger* t = d_tr_trie.getTrigger( trNodes );
- //if( t ){
- // trOld++;
- //}else{
- // trNew++;
- //}
- //if( (trNew+trOld)%100==0 ){
- // std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl;
- //}
- }else{
- Trigger* t = d_tr_trie.getTrigger( trNodes );
- if( t ){
- if( trOption==TR_GET_OLD ){
- //just return old trigger
- return t;
- }else{
- return NULL;
- }
- }
- }
- Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers );
- d_tr_trie.addTrigger( trNodes, t );
- return t;
-}
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){
- std::vector< Node > nodes;
- nodes.push_back( n );
- return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers );
-}
+ Debug("inst-trigger") << std::endl; + } + return addedLemmas; +} + +Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption, + bool smartTriggers ){ + std::vector< Node > trNodes; + if( !keepAll ){ + //only take nodes that contribute variables to the trigger when added + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::map< Node, bool > vars; + std::map< Node, std::vector< Node > > patterns; + for( int i=0; i<(int)temp.size(); i++ ){ + bool foundVar = false; + computeVarContains( temp[i] ); + for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){ + Node v = d_var_contains[ temp[i] ][j]; + if( v.getAttribute(InstConstantAttribute())==f ){ + if( vars.find( v )==vars.end() ){ + vars[ v ] = true; + foundVar = true; + } + } + } + if( foundVar ){ + trNodes.push_back( temp[i] ); + for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){ + Node v = d_var_contains[ temp[i] ][j]; + patterns[ v ].push_back( temp[i] ); + } + } + } + //now, minimalize the trigger + for( int i=0; i<(int)trNodes.size(); i++ ){ + bool keepPattern = false; + Node n = trNodes[i]; + for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){ + Node v = d_var_contains[ n ][j]; + if( patterns[v].size()==1 ){ + keepPattern = true; + break; + } + } + if( !keepPattern ){ + //remove from pattern vector + for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){ + Node v = d_var_contains[ n ][j]; + for( int k=0; k<(int)patterns[v].size(); k++ ){ + if( patterns[v][k]==n ){ + patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); + break; + } + } + } + //remove from trigger nodes + trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 ); + i--; + } + } + }else{ + trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() ); + } + + //check for duplicate? + if( trOption==TR_MAKE_NEW ){ + //static int trNew = 0; + //static int trOld = 0; + //Trigger* t = d_tr_trie.getTrigger( trNodes ); + //if( t ){ + // trOld++; + //}else{ + // trNew++; + //} + //if( (trNew+trOld)%100==0 ){ + // std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl; + //} + }else{ + Trigger* t = d_tr_trie.getTrigger( trNodes ); + if( t ){ + if( trOption==TR_GET_OLD ){ + //just return old trigger + return t; + }else{ + return NULL; + } + } + } + Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers ); + d_tr_trie.addTrigger( trNodes, t ); + return t; +} +Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){ + std::vector< Node > nodes; + nodes.push_back( n ); + return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers ); +} bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ for( int i=0; i<(int)nodes.size(); i++ ){ @@ -233,25 +233,25 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ } } return true; -}
-
-bool Trigger::isUsable( Node n, Node f ){
- if( n.getAttribute(InstConstantAttribute())==f ){
- if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){
- std::map< Node, Node > coeffs;
- return getPatternArithmetic( f, n, coeffs );
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( !isUsable( n[i], f ) ){
- return false;
- }
- }
- return true;
- }
- }else{
- return true;
- }
-}
+} + +bool Trigger::isUsable( Node n, Node f ){ + if( n.getAttribute(InstConstantAttribute())==f ){ + if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){ + std::map< Node, Node > coeffs; + return getPatternArithmetic( f, n, coeffs ); + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( !isUsable( n[i], f ) ){ + return false; + } + } + return true; + } + }else{ + return true; + } +} bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ @@ -293,67 +293,67 @@ void Trigger::filterInstances( std::vector< Node >& nodes ){ } -bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){
- if( patMap.find( n )==patMap.end() ){
- patMap[ n ] = false;
- if( tstrt==TS_MIN_TRIGGER ){
- if( n.getKind()==FORALL ){
-#ifdef NESTED_PATTERN_SELECTION
- //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt );
- return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt );
-#else
- return false;
-#endif
- }else{
- bool retVal = false;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
- retVal = true;
- }
- }
- if( retVal ){
- return true;
- }else if( isUsableTrigger( n, f ) ){
- patMap[ n ] = true;
- return true;
- }else{
- return false;
- }
- }
- }else{
- bool retVal = false;
- if( isUsableTrigger( n, f ) ){
- patMap[ n ] = true;
- if( tstrt==TS_MAX_TRIGGER ){
- return true;
- }else{
- retVal = true;
- }
- }
- if( n.getKind()==FORALL ){
-#ifdef NESTED_PATTERN_SELECTION
- //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){
- // retVal = true;
- //}
- if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){
- retVal = true;
- }
-#endif
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
- retVal = true;
- }
- }
- }
- return retVal;
- }
- }else{
- return patMap[ n ];
- }
+bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){ + if( patMap.find( n )==patMap.end() ){ + patMap[ n ] = false; + if( tstrt==TS_MIN_TRIGGER ){ + if( n.getKind()==FORALL ){ +#ifdef NESTED_PATTERN_SELECTION + //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ); + return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ); +#else + return false; +#endif + }else{ + bool retVal = false; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + retVal = true; + } + } + if( retVal ){ + return true; + }else if( isUsableTrigger( n, f ) ){ + patMap[ n ] = true; + return true; + }else{ + return false; + } + } + }else{ + bool retVal = false; + if( isUsableTrigger( n, f ) ){ + patMap[ n ] = true; + if( tstrt==TS_MAX_TRIGGER ){ + return true; + }else{ + retVal = true; + } + } + if( n.getKind()==FORALL ){ +#ifdef NESTED_PATTERN_SELECTION + //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){ + // retVal = true; + //} + if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){ + retVal = true; + } +#endif + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + retVal = true; + } + } + } + return retVal; + } + }else{ + return patMap[ n ]; + } } -void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){
+void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){ std::map< Node, bool > patMap; if( filterInst ){ //immediately do not consider any term t for which another term is an instance of t @@ -387,10 +387,10 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } collectPatTerms2( qe, f, n, patMap, tstrt ); - for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
- if( it->second ){
- patTerms.push_back( it->first );
- }
+ for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ + if( it->second ){ + patTerms.push_back( it->first ); + } } } @@ -469,15 +469,15 @@ void Trigger::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, } } } -
-void Trigger::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
- computeVarContains( n );
- for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
- if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){
- varContains.push_back( d_var_contains[n][j] );
- }
- }
-}
+ +void Trigger::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){ + computeVarContains( n ); + for( int j=0; j<(int)d_var_contains[n].size(); j++ ){ + if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){ + varContains.push_back( d_var_contains[n][j] ); + } + } +} bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){ if( n.getKind()==PLUS ){ diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index f68ab1429..0082f4840 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -1,421 +1,421 @@ -/********************* */
-/*! \file theory_uf_model.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 Theory UF Model
- **/
-
-#include "theory/quantifiers/model_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/uf/theory_uf_instantiator.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_database.h"
-
-#define RECONSIDER_FUNC_DEFAULT_VALUE
-#define USE_PARTIAL_DEFAULT_VALUES
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
-
-//clear
-void UfModelTreeNode::clear(){
- d_data.clear();
- d_value = Node::null();
-}
-
-bool UfModelTreeNode::hasConcreteArgumentDefinition(){
- if( d_data.size()>1 ){
- return true;
- }else if( d_data.empty() ){
- return false;
- }else{
- Node r;
- return d_data.find( r )==d_data.end();
- }
-}
-
-//set value function
-void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
- if( d_data.empty() ){
- d_value = v;
- }else if( !d_value.isNull() && d_value!=v ){
- d_value = Node::null();
- }
- if( argIndex<(int)indexOrder.size() ){
- //take r = null when argument is the model basis
- Node r;
- if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){
- r = m->getRepresentative( n[ indexOrder[argIndex] ] );
- }
- d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 );
- }
-}
-
-//get value function
-Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){
- if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){
- //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl;
- depIndex = argIndex;
- return d_value;
- }else{
- Node val;
- int childDepIndex[2] = { argIndex, argIndex };
- for( int i=0; i<2; i++ ){
- //first check the argument, then check default
- Node r;
- if( i==0 ){
- r = m->getRepresentative( n[ indexOrder[argIndex] ] );
- }
- std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
- if( it!=d_data.end() ){
- val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 );
- if( !val.isNull() ){
- break;
- }
- }else{
- //argument is not a defined argument: thus, it depends on this argument
- childDepIndex[i] = argIndex+1;
- }
- }
- //update depIndex
- depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1];
- //Notice() << "Return " << val << ", depIndex = " << depIndex;
- //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl;
- return val;
- }
-}
-
-Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){
- if( argIndex==(int)indexOrder.size() ){
- return d_value;
- }else{
- Node val;
- bool depArg = false;
- //will try concrete value first, then default
- for( int i=0; i<2; i++ ){
- Node r;
- if( i==0 ){
- r = m->getRepresentative( n[ indexOrder[argIndex] ] );
- }
- std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
- if( it!=d_data.end() ){
- val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 );
- //we have found a value
- if( !val.isNull() ){
- if( i==0 ){
- depArg = true;
- }
- break;
- }
- }
- }
- //it depends on this argument if we found it via concrete argument value,
- // or if found by default/disequal from some concrete argument value(s).
- if( depArg || hasConcreteArgumentDefinition() ){
- if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){
- depIndex.push_back( indexOrder[argIndex] );
- }
- }
- return val;
- }
-}
-
-Node UfModelTreeNode::getFunctionValue(){
- if( !d_data.empty() ){
- Node defaultValue;
- std::vector< Node > caseValues;
- for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
- if( it->first.isNull() ){
- defaultValue = it->second.getFunctionValue();
- }else{
- caseValues.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE, it->first, it->second.getFunctionValue() ) );
- }
- }
- if( caseValues.empty() && defaultValue.getKind()!=FUNCTION_CASE_SPLIT && defaultValue.getKind()!=FUNCTION_MODEL ){
- return defaultValue;
- }else{
- std::vector< Node > children;
- if( !caseValues.empty() ){
- children.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE_SPLIT, caseValues ) );
- }
- if( !defaultValue.isNull() ){
- children.push_back( defaultValue );
- }
- return NodeManager::currentNM()->mkNode( FUNCTION_MODEL, children );
- }
- }else{
- Assert( !d_value.isNull() );
- return d_value;
- }
-}
-
-//simplify function
-void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){
- if( argIndex<(int)op.getType().getNumChildren()-1 ){
- std::vector< Node > eraseData;
- //first process the default argument
- Node r;
- std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
- if( it!=d_data.end() ){
- if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
- eraseData.push_back( r );
- }else{
- it->second.simplify( op, defaultVal, argIndex+1 );
- if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){
- defaultVal = it->second.d_value;
- }else{
- defaultVal = Node::null();
- if( it->second.isEmpty() ){
- eraseData.push_back( r );
- }
- }
- }
- }
- //now see if any children can be removed, and simplify the ones that cannot
- for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
- if( !it->first.isNull() ){
- if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
- eraseData.push_back( it->first );
- }else{
- it->second.simplify( op, defaultVal, argIndex+1 );
- if( it->second.isEmpty() ){
- eraseData.push_back( it->first );
- }
- }
- }
- }
- for( int i=0; i<(int)eraseData.size(); i++ ){
- d_data.erase( eraseData[i] );
- }
- }
-}
-
-//is total function
-bool UfModelTreeNode::isTotal( Node op, int argIndex ){
- if( argIndex==(int)(op.getType().getNumChildren()-1) ){
- return !d_value.isNull();
- }else{
- Node r;
- std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
- if( it!=d_data.end() ){
- return it->second.isTotal( op, argIndex+1 );
- }else{
- return false;
- }
- }
-}
-
-Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){
- return d_value;
-}
-
-void indent( std::ostream& out, int ind ){
- for( int i=0; i<ind; i++ ){
- out << " ";
- }
-}
-
-void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){
- if( !d_data.empty() ){
- for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
- if( !it->first.isNull() ){
- indent( out, ind );
- out << "if x_" << indexOrder[arg] << " == " << it->first << std::endl;
- it->second.debugPrint( out, m, indexOrder, ind+2, arg+1 );
- }
- }
- if( d_data.find( Node::null() )!=d_data.end() ){
- d_data[ Node::null() ].debugPrint( out, m, indexOrder, ind, arg+1 );
- }
- }else{
- indent( out, ind );
- out << "return ";
- m->printRepresentative( out, d_value );
- out << std::endl;
- }
-}
-
-
-Node UfModelTree::toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ){
- if( fm_node.getKind()==FUNCTION_MODEL ){
- if( fm_node[0].getKind()==FUNCTION_CASE_SPLIT ){
- Node retNode;
- Node childDefaultNode = defaultNode;
- //get new default
- if( fm_node.getNumChildren()==2 ){
- childDefaultNode = toIte2( fm_node[1], args, index+1, defaultNode );
- }
- retNode = childDefaultNode;
- for( int i=(int)fm_node[0].getNumChildren()-1; i>=0; i-- ){
- Node childNode = toIte2( fm_node[0][1], args, index+1, childDefaultNode );
- retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( fm_node[0][0] ), childNode, retNode );
- }
- return retNode;
- }else{
- return toIte2( fm_node[0], args, index+1, defaultNode );
- }
- }else{
- return fm_node;
- }
-}
-
-
-Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){
- //Notice() << "Get intersection " << n1 << " " << n2 << std::endl;
- isGround = true;
- std::vector< Node > children;
- children.push_back( n1.getOperator() );
- for( int i=0; i<(int)n1.getNumChildren(); i++ ){
- if( n1[i]==n2[i] ){
- if( n1[i].getAttribute(ModelBasisAttribute()) ){
- isGround = false;
- }
- children.push_back( n1[i] );
- }else if( n1[i].getAttribute(ModelBasisAttribute()) ){
- children.push_back( n2[i] );
- }else if( n2[i].getAttribute(ModelBasisAttribute()) ){
- children.push_back( n1[i] );
- }else if( m->areEqual( n1[i], n2[i] ) ){
- children.push_back( n1[i] );
- }else{
- return Node::null();
- }
- }
- return NodeManager::currentNM()->mkNode( APPLY_UF, children );
-}
-
-void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground, bool isReq ){
- Assert( !n.isNull() );
- Assert( !v.isNull() );
- d_set_values[ isReq ? 1 : 0 ][ ground ? 1 : 0 ][n] = v;
- if( optUsePartialDefaults() ){
- if( !ground ){
- int defSize = (int)d_defaults.size();
- for( int i=0; i<defSize; i++ ){
- bool isGround;
- //for soundness, to allow variable order-independent function interpretations,
- // we must ensure that the intersection of all default terms
- // is also defined.
- //for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,
- // then we must define f( b, a ).
- Node ni = getIntersection( m, n, d_defaults[i], isGround );
- if( !ni.isNull() ){
- //if the intersection exists, and is not already defined
- if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
- d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
- //use the current value
- setValue( m, ni, v, isGround, false );
- }
- }
- }
- d_defaults.push_back( n );
- }
- if( isReq && d_set_values[0][ ground ? 1 : 0 ].find( n )!=d_set_values[0][ ground ? 1 : 0 ].end()){
- d_set_values[0][ ground ? 1 : 0 ].erase( n );
- }
- }
-}
-
-void UfModelTreeGenerator::makeModel( TheoryModel* m, UfModelTree& tree ){
- for( int j=0; j<2; j++ ){
- for( int k=0; k<2; k++ ){
- for( std::map< Node, Node >::iterator it = d_set_values[j][k].begin(); it != d_set_values[j][k].end(); ++it ){
- tree.setValue( m, it->first, it->second, k==1 );
- }
- }
- }
- if( !d_default_value.isNull() ){
- tree.setDefaultValue( m, d_default_value );
- }
- tree.simplify();
-}
-
-bool UfModelTreeGenerator::optUsePartialDefaults(){
-#ifdef USE_PARTIAL_DEFAULT_VALUES
- return true;
-#else
- return false;
-#endif
-}
-
-void UfModelTreeGenerator::clear(){
- d_default_value = Node::null();
- for( int j=0; j<2; j++ ){
- for( int k=0; k<2; k++ ){
- d_set_values[j][k].clear();
- }
- }
- d_defaults.clear();
-}
-
-
-void UfModelPreferenceData::setValuePreference( Node f, Node n, Node r, bool isPro ){
- if( std::find( d_values.begin(), d_values.end(), r )==d_values.end() ){
- d_values.push_back( r );
- }
- int index = isPro ? 0 : 1;
- if( std::find( d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), f )==d_value_pro_con[index][r].end() ){
- d_value_pro_con[index][r].push_back( f );
- }
- d_term_pro_con[index][n].push_back( f );
-}
-
-Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* m ){
- Node defaultVal;
- double maxScore = -1;
- for( size_t i=0; i<d_values.size(); i++ ){
- Node v = d_values[i];
- double score = ( 1.0 + (double)d_value_pro_con[0][v].size() )/( 1.0 + (double)d_value_pro_con[1][v].size() );
- Debug("fmf-model-cons") << " - score( ";
- m->printRepresentativeDebug( "fmf-model-cons", v );
- Debug("fmf-model-cons") << " ) = " << score << std::endl;
- if( score>maxScore ){
- defaultVal = v;
- maxScore = score;
- }
- }
-#ifdef RECONSIDER_FUNC_DEFAULT_VALUE
- if( maxScore<1.0 ){
- //consider finding another value, if possible
- Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl;
- TypeNode tn = defaultTerm.getType();
- Node newDefaultVal = m->getDomainValue( tn, d_values );
- if( !newDefaultVal.isNull() ){
- defaultVal = newDefaultVal;
- Debug("fmf-model-cons-debug") << "-> Change default value to ";
- m->printRepresentativeDebug( "fmf-model-cons-debug", defaultVal );
- Debug("fmf-model-cons-debug") << std::endl;
- }else{
- Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl;
- Debug("fmf-model-cons-debug") << " Excluding: ";
- for( int i=0; i<(int)d_values.size(); i++ ){
- Debug("fmf-model-cons-debug") << d_values[i] << " ";
- }
- Debug("fmf-model-cons-debug") << std::endl;
- }
- }
-#endif
- //get the default term (this term must be defined non-ground in model)
- Debug("fmf-model-cons") << " Choose ";
- m->printRepresentativeDebug("fmf-model-cons", defaultVal );
- Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl;
- Debug("fmf-model-cons") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl;
- Debug("fmf-model-cons") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl;
- return defaultVal;
+/********************* */ +/*! \file theory_uf_model.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 Theory UF Model + **/ + +#include "theory/quantifiers/model_engine.h" +#include "theory/theory_engine.h" +#include "theory/uf/equality_engine.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/theory_uf_strong_solver.h" +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" + +#define RECONSIDER_FUNC_DEFAULT_VALUE +#define USE_PARTIAL_DEFAULT_VALUES + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; + +//clear +void UfModelTreeNode::clear(){ + d_data.clear(); + d_value = Node::null(); +} + +bool UfModelTreeNode::hasConcreteArgumentDefinition(){ + if( d_data.size()>1 ){ + return true; + }else if( d_data.empty() ){ + return false; + }else{ + Node r; + return d_data.find( r )==d_data.end(); + } +} + +//set value function +void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){ + if( d_data.empty() ){ + d_value = v; + }else if( !d_value.isNull() && d_value!=v ){ + d_value = Node::null(); + } + if( argIndex<(int)indexOrder.size() ){ + //take r = null when argument is the model basis + Node r; + if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){ + r = m->getRepresentative( n[ indexOrder[argIndex] ] ); + } + d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 ); + } +} + +//get value function +Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){ + if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){ + //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl; + depIndex = argIndex; + return d_value; + }else{ + Node val; + int childDepIndex[2] = { argIndex, argIndex }; + for( int i=0; i<2; i++ ){ + //first check the argument, then check default + Node r; + if( i==0 ){ + r = m->getRepresentative( n[ indexOrder[argIndex] ] ); + } + std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); + if( it!=d_data.end() ){ + val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 ); + if( !val.isNull() ){ + break; + } + }else{ + //argument is not a defined argument: thus, it depends on this argument + childDepIndex[i] = argIndex+1; + } + } + //update depIndex + depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1]; + //Notice() << "Return " << val << ", depIndex = " << depIndex; + //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl; + return val; + } +} + +Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){ + if( argIndex==(int)indexOrder.size() ){ + return d_value; + }else{ + Node val; + bool depArg = false; + //will try concrete value first, then default + for( int i=0; i<2; i++ ){ + Node r; + if( i==0 ){ + r = m->getRepresentative( n[ indexOrder[argIndex] ] ); + } + std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); + if( it!=d_data.end() ){ + val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 ); + //we have found a value + if( !val.isNull() ){ + if( i==0 ){ + depArg = true; + } + break; + } + } + } + //it depends on this argument if we found it via concrete argument value, + // or if found by default/disequal from some concrete argument value(s). + if( depArg || hasConcreteArgumentDefinition() ){ + if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){ + depIndex.push_back( indexOrder[argIndex] ); + } + } + return val; + } +} + +Node UfModelTreeNode::getFunctionValue(){ + if( !d_data.empty() ){ + Node defaultValue; + std::vector< Node > caseValues; + for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ + if( it->first.isNull() ){ + defaultValue = it->second.getFunctionValue(); + }else{ + caseValues.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE, it->first, it->second.getFunctionValue() ) ); + } + } + if( caseValues.empty() && defaultValue.getKind()!=FUNCTION_CASE_SPLIT && defaultValue.getKind()!=FUNCTION_MODEL ){ + return defaultValue; + }else{ + std::vector< Node > children; + if( !caseValues.empty() ){ + children.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE_SPLIT, caseValues ) ); + } + if( !defaultValue.isNull() ){ + children.push_back( defaultValue ); + } + return NodeManager::currentNM()->mkNode( FUNCTION_MODEL, children ); + } + }else{ + Assert( !d_value.isNull() ); + return d_value; + } +} + +//simplify function +void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){ + if( argIndex<(int)op.getType().getNumChildren()-1 ){ + std::vector< Node > eraseData; + //first process the default argument + Node r; + std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); + if( it!=d_data.end() ){ + if( !defaultVal.isNull() && it->second.d_value==defaultVal ){ + eraseData.push_back( r ); + }else{ + it->second.simplify( op, defaultVal, argIndex+1 ); + if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){ + defaultVal = it->second.d_value; + }else{ + defaultVal = Node::null(); + if( it->second.isEmpty() ){ + eraseData.push_back( r ); + } + } + } + } + //now see if any children can be removed, and simplify the ones that cannot + for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ + if( !it->first.isNull() ){ + if( !defaultVal.isNull() && it->second.d_value==defaultVal ){ + eraseData.push_back( it->first ); + }else{ + it->second.simplify( op, defaultVal, argIndex+1 ); + if( it->second.isEmpty() ){ + eraseData.push_back( it->first ); + } + } + } + } + for( int i=0; i<(int)eraseData.size(); i++ ){ + d_data.erase( eraseData[i] ); + } + } +} + +//is total function +bool UfModelTreeNode::isTotal( Node op, int argIndex ){ + if( argIndex==(int)(op.getType().getNumChildren()-1) ){ + return !d_value.isNull(); + }else{ + Node r; + std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); + if( it!=d_data.end() ){ + return it->second.isTotal( op, argIndex+1 ); + }else{ + return false; + } + } +} + +Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){ + return d_value; +} + +void indent( std::ostream& out, int ind ){ + for( int i=0; i<ind; i++ ){ + out << " "; + } +} + +void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){ + if( !d_data.empty() ){ + for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ + if( !it->first.isNull() ){ + indent( out, ind ); + out << "if x_" << indexOrder[arg] << " == " << it->first << std::endl; + it->second.debugPrint( out, m, indexOrder, ind+2, arg+1 ); + } + } + if( d_data.find( Node::null() )!=d_data.end() ){ + d_data[ Node::null() ].debugPrint( out, m, indexOrder, ind, arg+1 ); + } + }else{ + indent( out, ind ); + out << "return "; + m->printRepresentative( out, d_value ); + out << std::endl; + } +} + + +Node UfModelTree::toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ){ + if( fm_node.getKind()==FUNCTION_MODEL ){ + if( fm_node[0].getKind()==FUNCTION_CASE_SPLIT ){ + Node retNode; + Node childDefaultNode = defaultNode; + //get new default + if( fm_node.getNumChildren()==2 ){ + childDefaultNode = toIte2( fm_node[1], args, index+1, defaultNode ); + } + retNode = childDefaultNode; + for( int i=(int)fm_node[0].getNumChildren()-1; i>=0; i-- ){ + Node childNode = toIte2( fm_node[0][1], args, index+1, childDefaultNode ); + retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( fm_node[0][0] ), childNode, retNode ); + } + return retNode; + }else{ + return toIte2( fm_node[0], args, index+1, defaultNode ); + } + }else{ + return fm_node; + } +} + + +Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){ + //Notice() << "Get intersection " << n1 << " " << n2 << std::endl; + isGround = true; + std::vector< Node > children; + children.push_back( n1.getOperator() ); + for( int i=0; i<(int)n1.getNumChildren(); i++ ){ + if( n1[i]==n2[i] ){ + if( n1[i].getAttribute(ModelBasisAttribute()) ){ + isGround = false; + } + children.push_back( n1[i] ); + }else if( n1[i].getAttribute(ModelBasisAttribute()) ){ + children.push_back( n2[i] ); + }else if( n2[i].getAttribute(ModelBasisAttribute()) ){ + children.push_back( n1[i] ); + }else if( m->areEqual( n1[i], n2[i] ) ){ + children.push_back( n1[i] ); + }else{ + return Node::null(); + } + } + return NodeManager::currentNM()->mkNode( APPLY_UF, children ); +} + +void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground, bool isReq ){ + Assert( !n.isNull() ); + Assert( !v.isNull() ); + d_set_values[ isReq ? 1 : 0 ][ ground ? 1 : 0 ][n] = v; + if( optUsePartialDefaults() ){ + if( !ground ){ + int defSize = (int)d_defaults.size(); + for( int i=0; i<defSize; i++ ){ + bool isGround; + //for soundness, to allow variable order-independent function interpretations, + // we must ensure that the intersection of all default terms + // is also defined. + //for example, if we have that f( e, a ) = ..., and f( b, e ) = ..., + // then we must define f( b, a ). + Node ni = getIntersection( m, n, d_defaults[i], isGround ); + if( !ni.isNull() ){ + //if the intersection exists, and is not already defined + if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() && + d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){ + //use the current value + setValue( m, ni, v, isGround, false ); + } + } + } + d_defaults.push_back( n ); + } + if( isReq && d_set_values[0][ ground ? 1 : 0 ].find( n )!=d_set_values[0][ ground ? 1 : 0 ].end()){ + d_set_values[0][ ground ? 1 : 0 ].erase( n ); + } + } +} + +void UfModelTreeGenerator::makeModel( TheoryModel* m, UfModelTree& tree ){ + for( int j=0; j<2; j++ ){ + for( int k=0; k<2; k++ ){ + for( std::map< Node, Node >::iterator it = d_set_values[j][k].begin(); it != d_set_values[j][k].end(); ++it ){ + tree.setValue( m, it->first, it->second, k==1 ); + } + } + } + if( !d_default_value.isNull() ){ + tree.setDefaultValue( m, d_default_value ); + } + tree.simplify(); +} + +bool UfModelTreeGenerator::optUsePartialDefaults(){ +#ifdef USE_PARTIAL_DEFAULT_VALUES + return true; +#else + return false; +#endif +} + +void UfModelTreeGenerator::clear(){ + d_default_value = Node::null(); + for( int j=0; j<2; j++ ){ + for( int k=0; k<2; k++ ){ + d_set_values[j][k].clear(); + } + } + d_defaults.clear(); +} + + +void UfModelPreferenceData::setValuePreference( Node f, Node n, Node r, bool isPro ){ + if( std::find( d_values.begin(), d_values.end(), r )==d_values.end() ){ + d_values.push_back( r ); + } + int index = isPro ? 0 : 1; + if( std::find( d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), f )==d_value_pro_con[index][r].end() ){ + d_value_pro_con[index][r].push_back( f ); + } + d_term_pro_con[index][n].push_back( f ); +} + +Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* m ){ + Node defaultVal; + double maxScore = -1; + for( size_t i=0; i<d_values.size(); i++ ){ + Node v = d_values[i]; + double score = ( 1.0 + (double)d_value_pro_con[0][v].size() )/( 1.0 + (double)d_value_pro_con[1][v].size() ); + Debug("fmf-model-cons") << " - score( "; + m->printRepresentativeDebug( "fmf-model-cons", v ); + Debug("fmf-model-cons") << " ) = " << score << std::endl; + if( score>maxScore ){ + defaultVal = v; + maxScore = score; + } + } +#ifdef RECONSIDER_FUNC_DEFAULT_VALUE + if( maxScore<1.0 ){ + //consider finding another value, if possible + Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl; + TypeNode tn = defaultTerm.getType(); + Node newDefaultVal = m->getDomainValue( tn, d_values ); + if( !newDefaultVal.isNull() ){ + defaultVal = newDefaultVal; + Debug("fmf-model-cons-debug") << "-> Change default value to "; + m->printRepresentativeDebug( "fmf-model-cons-debug", defaultVal ); + Debug("fmf-model-cons-debug") << std::endl; + }else{ + Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl; + Debug("fmf-model-cons-debug") << " Excluding: "; + for( int i=0; i<(int)d_values.size(); i++ ){ + Debug("fmf-model-cons-debug") << d_values[i] << " "; + } + Debug("fmf-model-cons-debug") << std::endl; + } + } +#endif + //get the default term (this term must be defined non-ground in model) + Debug("fmf-model-cons") << " Choose "; + m->printRepresentativeDebug("fmf-model-cons", defaultVal ); + Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl; + Debug("fmf-model-cons") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl; + Debug("fmf-model-cons") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl; + return defaultVal; }
\ No newline at end of file diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 47b149867..9dba16608 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -1,199 +1,199 @@ -/********************* */
-/*! \file theory_uf_model.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, 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 Model for Theory UF
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_UF_MODEL_H
-#define __CVC4__THEORY_UF_MODEL_H
-
-#include "theory/model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace uf {
-
-class UfModelTreeNode
-{
-public:
- UfModelTreeNode(){}
- /** the data */
- std::map< Node, UfModelTreeNode > d_data;
- /** the value of this tree node (if all paths lead to same value) */
- Node d_value;
- /** has concrete argument defintion */
- bool hasConcreteArgumentDefinition();
-public:
- //is this model tree empty?
- bool isEmpty() { return d_data.empty() && d_value.isNull(); }
- //clear
- void clear();
- /** setValue function */
- void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex );
- /** getValue function */
- Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex );
- Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex );
- /** getConstant Value function */
- Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex );
- /** getFunctionValue */
- Node getFunctionValue();
- /** simplify function */
- void simplify( Node op, Node defaultVal, int argIndex );
- /** is total ? */
- bool isTotal( Node op, int argIndex );
-public:
- void debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind = 0, int arg = 0 );
-};
-
-class UfModelTree
-{
-private:
- //the op this model is for
- Node d_op;
- //the order we will treat the arguments
- std::vector< int > d_index_order;
- //the data
- UfModelTreeNode d_tree;
-public:
- //constructors
- UfModelTree(){}
- UfModelTree( Node op ) : d_op( op ){
- TypeNode tn = d_op.getType();
- for( int i=0; i<(int)(tn.getNumChildren()-1); i++ ){
- d_index_order.push_back( i );
- }
- }
- UfModelTree( Node op, std::vector< int >& indexOrder ) : d_op( op ){
- d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() );
- }
- /** clear/reset the function */
- void clear() { d_tree.clear(); }
- /** setValue function
- *
- * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false
- *
- */
- void setValue( TheoryModel* m, Node n, Node v, bool ground = true ){
- d_tree.setValue( m, n, v, d_index_order, ground, 0 );
- }
- /** setDefaultValue function */
- void setDefaultValue( TheoryModel* m, Node v ){
- d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 );
- }
- /** getValue function
- *
- * returns val, the value of ground term n
- * Say n is f( t_0...t_n )
- * depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to val
- * for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c,
- * then g( a, a, a ) would return b with depIndex = 1
- *
- */
- Node getValue( TheoryModel* m, Node n, int& depIndex ){
- return d_tree.getValue( m, n, d_index_order, depIndex, 0 );
- }
- /** -> implementation incomplete */
- Node getValue( TheoryModel* m, Node n, std::vector< int >& depIndex ){
- return d_tree.getValue( m, n, d_index_order, depIndex, 0 );
- }
- /** getConstantValue function
- *
- * given term n, where n may contain "all value" arguments, aka model basis arguments
- * if n is null, then every argument of n is considered "all value"
- * if n is constant for the entire domain specified by n, then this function returns the value of its domain
- * otherwise, it returns null
- * for example, say the term e represents "all values"
- * if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b,
- * then f( a, e ) would return b, while f( e, a ) would return null
- * -> implementation incomplete
- */
- Node getConstantValue( TheoryModel* m, Node n ) {
- return d_tree.getConstantValue( m, n, d_index_order, 0 );
- }
- /** getFunctionValue
- * Returns a compact representation of this function, of kind FUNCTION_MODEL.
- * See documentation in theory/uf/kinds
- */
- Node getFunctionValue(){
- return d_tree.getFunctionValue();
- }
- /** simplify the tree */
- void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); }
- /** is this tree total? */
- bool isTotal() { return d_tree.isTotal( d_op, 0 ); }
- /** is this function constant? */
- bool isConstant( TheoryModel* m ) { return !getConstantValue( m, Node::null() ).isNull(); }
- /** is this tree empty? */
- bool isEmpty() { return d_tree.isEmpty(); }
-public:
- void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){
- d_tree.debugPrint( out, m, d_index_order, ind );
- }
-private:
- //helper for to ITE function.
- static Node toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode );
-public:
- /** to ITE function for function model nodes */
- static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); }
-};
-
-class UfModelTreeGenerator
-{
-private:
- //store for set values
- Node d_default_value;
- std::map< Node, Node > d_set_values[2][2];
- // defaults
- std::vector< Node > d_defaults;
- Node getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround );
-public:
- UfModelTreeGenerator(){}
- ~UfModelTreeGenerator(){}
- /** set default value */
- void setDefaultValue( Node v ) { d_default_value = v; }
- /** set value */
- void setValue( TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true );
- /** make model */
- void makeModel( TheoryModel* m, UfModelTree& tree );
- /** uses partial default values */
- bool optUsePartialDefaults();
- /** reset */
- void clear();
-};
-
-//this class stores temporary information useful to model engine for constructing model
-class UfModelPreferenceData
-{
-public:
- UfModelPreferenceData() : d_reconsiderModel( false ){}
- virtual ~UfModelPreferenceData(){}
- Node d_const_val;
- // preferences for default values
- std::vector< Node > d_values;
- std::map< Node, std::vector< Node > > d_value_pro_con[2];
- std::map< Node, std::vector< Node > > d_term_pro_con[2];
- bool d_reconsiderModel;
- /** set value preference */
- void setValuePreference( Node f, Node n, Node r, bool isPro );
- /** get best default value */
- Node getBestDefaultValue( Node defaultTerm, TheoryModel* m );
-};
-
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file theory_uf_model.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, 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 Model for Theory UF + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_UF_MODEL_H +#define __CVC4__THEORY_UF_MODEL_H + +#include "theory/model.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +class UfModelTreeNode +{ +public: + UfModelTreeNode(){} + /** the data */ + std::map< Node, UfModelTreeNode > d_data; + /** the value of this tree node (if all paths lead to same value) */ + Node d_value; + /** has concrete argument defintion */ + bool hasConcreteArgumentDefinition(); +public: + //is this model tree empty? + bool isEmpty() { return d_data.empty() && d_value.isNull(); } + //clear + void clear(); + /** setValue function */ + void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ); + /** getValue function */ + Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ); + Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ); + /** getConstant Value function */ + Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ); + /** getFunctionValue */ + Node getFunctionValue(); + /** simplify function */ + void simplify( Node op, Node defaultVal, int argIndex ); + /** is total ? */ + bool isTotal( Node op, int argIndex ); +public: + void debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind = 0, int arg = 0 ); +}; + +class UfModelTree +{ +private: + //the op this model is for + Node d_op; + //the order we will treat the arguments + std::vector< int > d_index_order; + //the data + UfModelTreeNode d_tree; +public: + //constructors + UfModelTree(){} + UfModelTree( Node op ) : d_op( op ){ + TypeNode tn = d_op.getType(); + for( int i=0; i<(int)(tn.getNumChildren()-1); i++ ){ + d_index_order.push_back( i ); + } + } + UfModelTree( Node op, std::vector< int >& indexOrder ) : d_op( op ){ + d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() ); + } + /** clear/reset the function */ + void clear() { d_tree.clear(); } + /** setValue function + * + * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false + * + */ + void setValue( TheoryModel* m, Node n, Node v, bool ground = true ){ + d_tree.setValue( m, n, v, d_index_order, ground, 0 ); + } + /** setDefaultValue function */ + void setDefaultValue( TheoryModel* m, Node v ){ + d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 ); + } + /** getValue function + * + * returns val, the value of ground term n + * Say n is f( t_0...t_n ) + * depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to val + * for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c, + * then g( a, a, a ) would return b with depIndex = 1 + * + */ + Node getValue( TheoryModel* m, Node n, int& depIndex ){ + return d_tree.getValue( m, n, d_index_order, depIndex, 0 ); + } + /** -> implementation incomplete */ + Node getValue( TheoryModel* m, Node n, std::vector< int >& depIndex ){ + return d_tree.getValue( m, n, d_index_order, depIndex, 0 ); + } + /** getConstantValue function + * + * given term n, where n may contain "all value" arguments, aka model basis arguments + * if n is null, then every argument of n is considered "all value" + * if n is constant for the entire domain specified by n, then this function returns the value of its domain + * otherwise, it returns null + * for example, say the term e represents "all values" + * if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b, + * then f( a, e ) would return b, while f( e, a ) would return null + * -> implementation incomplete + */ + Node getConstantValue( TheoryModel* m, Node n ) { + return d_tree.getConstantValue( m, n, d_index_order, 0 ); + } + /** getFunctionValue + * Returns a compact representation of this function, of kind FUNCTION_MODEL. + * See documentation in theory/uf/kinds + */ + Node getFunctionValue(){ + return d_tree.getFunctionValue(); + } + /** simplify the tree */ + void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); } + /** is this tree total? */ + bool isTotal() { return d_tree.isTotal( d_op, 0 ); } + /** is this function constant? */ + bool isConstant( TheoryModel* m ) { return !getConstantValue( m, Node::null() ).isNull(); } + /** is this tree empty? */ + bool isEmpty() { return d_tree.isEmpty(); } +public: + void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){ + d_tree.debugPrint( out, m, d_index_order, ind ); + } +private: + //helper for to ITE function. + static Node toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ); +public: + /** to ITE function for function model nodes */ + static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); } +}; + +class UfModelTreeGenerator +{ +private: + //store for set values + Node d_default_value; + std::map< Node, Node > d_set_values[2][2]; + // defaults + std::vector< Node > d_defaults; + Node getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ); +public: + UfModelTreeGenerator(){} + ~UfModelTreeGenerator(){} + /** set default value */ + void setDefaultValue( Node v ) { d_default_value = v; } + /** set value */ + void setValue( TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true ); + /** make model */ + void makeModel( TheoryModel* m, UfModelTree& tree ); + /** uses partial default values */ + bool optUsePartialDefaults(); + /** reset */ + void clear(); +}; + +//this class stores temporary information useful to model engine for constructing model +class UfModelPreferenceData +{ +public: + UfModelPreferenceData() : d_reconsiderModel( false ){} + virtual ~UfModelPreferenceData(){} + Node d_const_val; + // preferences for default values + std::vector< Node > d_values; + std::map< Node, std::vector< Node > > d_value_pro_con[2]; + std::map< Node, std::vector< Node > > d_term_pro_con[2]; + bool d_reconsiderModel; + /** set value preference */ + void setValuePreference( Node f, Node n, Node r, bool isPro ); + /** get best default value */ + Node getBestDefaultValue( Node defaultTerm, TheoryModel* m ); +}; + + +} +} +} + +#endif |