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