From 485c03a323911142e460bd0a7c428759496dc631 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 27 Jul 2012 22:01:03 +0000 Subject: [PATCH] Minor cleanup after today's commits: * change some uses of "std::cout" to "Message()" * change some files to use Unix newlines instead of DOS newlines * fix compiler warning --- src/theory/arrays/theory_arrays_model.cpp | 140 +- src/theory/arrays/theory_arrays_model.h | 122 +- src/theory/candidate_generator.cpp | 510 +++---- src/theory/candidate_generator.h | 374 ++--- src/theory/inst_match.cpp | 3 - src/theory/model.cpp | 1230 ++++++++--------- src/theory/model.h | 382 ++--- src/theory/quantifiers/first_order_model.cpp | 366 ++--- src/theory/quantifiers/first_order_model.h | 178 +-- src/theory/quantifiers/model_builder.h | 182 +-- src/theory/quantifiers/relevant_domain.cpp | 344 ++--- src/theory/quantifiers/relevant_domain.h | 108 +- src/theory/quantifiers/rep_set_iterator.cpp | 1034 +++++++------- src/theory/quantifiers/rep_set_iterator.h | 240 ++-- src/theory/quantifiers/term_database.h | 312 ++--- src/theory/rr_inst_match.cpp | 4 +- src/theory/rr_trigger.cpp | 444 +++--- src/theory/uf/theory_uf_model.cpp | 840 +++++------ src/theory/uf/theory_uf_model.h | 398 +++--- src/util/model.cpp | 28 +- src/util/model.h | 84 +- .../decision/quant-symmetric_unsat_7.smt2 | 4 +- .../quantifiers/symmetric_unsat_7.smt2 | 4 +- 23 files changed, 3664 insertions(+), 3667 deletions(-) diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp index 49da2f851..7a574fac1 100644 --- a/src/theory/arrays/theory_arrays_model.cpp +++ b/src/theory/arrays/theory_arrays_model.cpp @@ -1,70 +1,70 @@ -/********************* */ -/*! \file theory_arrays_model.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of theory_arrays_model class - **/ - -#include "theory/theory_engine.h" -#include "theory/arrays/theory_arrays_model.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::arrays; - -ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){ - Assert( arr.getKind()!=STORE ); - //look at ground assertions - Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) ); - Node sel_op = sel.getOperator(); //FIXME: easier way to do this? - for( size_t i=0; igetTermDatabase()->d_op_map[ sel_op ].size(); i++ ){ - Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i]; - Assert( n.getKind()==SELECT ); - if( m->areEqual( n[0], arr ) ){ - //d_model->getTermDatabase()->computeModelBasisArgAttribute( n ); - //if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ - Node r = d_model->getRepresentative( n ); - Node i = d_model->getRepresentative( n[1] ); - d_values[i] = r; - //} - } - } -} - -Node ArrayModel::getValue( Node n ){ - Assert( n.getKind()==SELECT ); - Assert( n[0]==d_arr ); - std::map< Node, Node >::iterator it = d_values.find( n[0] ); - if( it!=d_values.end() ){ - return it->second; - }else{ - return n; - //return d_default_value; TODO: guarentee I can return this here - } -} - -void ArrayModel::setDefaultValue( Node v ){ - d_default_value = v; -} - -Node ArrayModel::getArrayValue(){ - Node curr = d_arr; //TODO: make constant default - for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){ - curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second ); - } - return curr; -} +/********************* */ +/*! \file theory_arrays_model.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of theory_arrays_model class + **/ + +#include "theory/theory_engine.h" +#include "theory/arrays/theory_arrays_model.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::arrays; + +ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){ + Assert( arr.getKind()!=STORE ); + //look at ground assertions + Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) ); + Node sel_op = sel.getOperator(); //FIXME: easier way to do this? + for( size_t i=0; igetTermDatabase()->d_op_map[ sel_op ].size(); i++ ){ + Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i]; + Assert( n.getKind()==SELECT ); + if( m->areEqual( n[0], arr ) ){ + //d_model->getTermDatabase()->computeModelBasisArgAttribute( n ); + //if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ + Node r = d_model->getRepresentative( n ); + Node i = d_model->getRepresentative( n[1] ); + d_values[i] = r; + //} + } + } +} + +Node ArrayModel::getValue( Node n ){ + Assert( n.getKind()==SELECT ); + Assert( n[0]==d_arr ); + std::map< Node, Node >::iterator it = d_values.find( n[0] ); + if( it!=d_values.end() ){ + return it->second; + }else{ + return n; + //return d_default_value; TODO: guarentee I can return this here + } +} + +void ArrayModel::setDefaultValue( Node v ){ + d_default_value = v; +} + +Node ArrayModel::getArrayValue(){ + Node curr = d_arr; //TODO: make constant default + for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){ + curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second ); + } + return curr; +} diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h index 3895388e3..28852296d 100644 --- a/src/theory/arrays/theory_arrays_model.h +++ b/src/theory/arrays/theory_arrays_model.h @@ -1,62 +1,62 @@ -/********************* */ -/*! \file theory_arrays_model.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief MODEL for theory of arrays - **/ - - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY_ARRAYS_MODEL_H -#define __CVC4__THEORY_ARRAYS_MODEL_H - -#include "theory/quantifiers_engine.h" - -namespace CVC4 { -namespace theory { - -namespace quantifiers{ - class FirstOrderModel; -} - -namespace arrays { - -class ArrayModel{ -protected: - /** reference to model */ - quantifiers::FirstOrderModel* d_model; - /** the array this model is for */ - Node d_arr; -public: - ArrayModel(){} - ArrayModel( Node arr, quantifiers::FirstOrderModel* m ); - ~ArrayModel() {} -public: - /** pre-defined values */ - std::map< Node, Node > d_values; - /** default value */ - Node d_default_value; - /** get value, return arguments that the value depends on */ - Node getValue( Node n ); - /** set default */ - void setDefaultValue( Node v ); -public: - /** get array value */ - Node getArrayValue(); -};/* class ArrayModel */ - -} -} -} - +/********************* */ +/*! \file theory_arrays_model.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief MODEL for theory of arrays + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_ARRAYS_MODEL_H +#define __CVC4__THEORY_ARRAYS_MODEL_H + +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { + +namespace quantifiers{ + class FirstOrderModel; +} + +namespace arrays { + +class ArrayModel{ +protected: + /** reference to model */ + quantifiers::FirstOrderModel* d_model; + /** the array this model is for */ + Node d_arr; +public: + ArrayModel(){} + ArrayModel( Node arr, quantifiers::FirstOrderModel* m ); + ~ArrayModel() {} +public: + /** pre-defined values */ + std::map< Node, Node > d_values; + /** default value */ + Node d_default_value; + /** get value, return arguments that the value depends on */ + Node getValue( Node n ); + /** set default */ + void setDefaultValue( Node v ); +public: + /** get array value */ + Node getArrayValue(); +};/* class ArrayModel */ + +} +} +} + #endif \ No newline at end of file diff --git a/src/theory/candidate_generator.cpp b/src/theory/candidate_generator.cpp index ffecaa8da..a0f303c21 100644 --- a/src/theory/candidate_generator.cpp +++ b/src/theory/candidate_generator.cpp @@ -1,255 +1,255 @@ -/********************* */ -/*! \file theory_uf_candidate_generator.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of theory uf candidate generator class - **/ - -#include "theory/candidate_generator.h" -#include "theory/theory_engine.h" -#include "theory/uf/theory_uf.h" -#include "theory/quantifiers/term_database.h" -#include "theory/inst_match.h" -#include "theory/quantifiers_engine.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::inst; - -bool CandidateGenerator::isLegalCandidate( Node n ){ - return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) ); -} - -void CandidateGeneratorQueue::addCandidate( Node n ) { - if( isLegalCandidate( n ) ){ - d_candidates.push_back( n ); - } -} - -void CandidateGeneratorQueue::reset( Node eqc ){ - if( d_candidate_index>0 ){ - d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index ); - d_candidate_index = 0; - } - if( !eqc.isNull() ){ - d_candidates.push_back( eqc ); - } -} -Node CandidateGeneratorQueue::getNextCandidate(){ - if( d_candidate_index<(int)d_candidates.size() ){ - Node n = d_candidates[d_candidate_index]; - d_candidate_index++; - return n; - }else{ - d_candidate_index = 0; - d_candidates.clear(); - return Node::null(); - } -} - -#if 0 - -CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) : - d_op( op ), d_qe( qe ), d_term_iter( -2 ){ - Assert( !d_op.isNull() ); -} -void CandidateGeneratorQE::resetInstantiationRound(){ - d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size(); -} - -void CandidateGeneratorQE::reset( Node eqc ){ - if( eqc.isNull() ){ - d_term_iter = 0; - }else{ - //create an equivalence class iterator in eq class eqc - if( d_qe->getEqualityQuery()->getEngine()->hasTerm( eqc ) ){ - eqc = d_qe->getEqualityQuery()->getEngine()->getRepresentative( eqc ); - d_eqc = eq::EqClassIterator( eqc, d_qe->getEqualityQuery()->getEngine() ); - d_retNode = Node::null(); - }else{ - d_retNode = eqc; - } - d_term_iter = -1; - } -} - -Node CandidateGeneratorQE::getNextCandidate(){ - if( d_term_iter>=0 ){ - //get next candidate term in the uf term database - while( d_term_itergetTermDatabase()->d_op_map[d_op][d_term_iter]; - d_term_iter++; - if( isLegalCandidate( n ) ){ - return n; - } - } - }else if( d_term_iter==-1 ){ - if( d_retNode.isNull() ){ - //get next candidate term in equivalence class - while( !d_eqc.isFinished() ){ - Node n = (*d_eqc); - ++d_eqc; - if( n.hasOperator() && n.getOperator()==d_op ){ - if( isLegalCandidate( n ) ){ - return n; - } - } - } - }else{ - Node ret; - if( d_retNode.hasOperator() && d_retNode.getOperator()==d_op ){ - ret = d_retNode; - } - d_term_iter = -2; //done returning matches - return ret; - } - } - return Node::null(); -} - -#else - - -CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) : - d_op( op ), d_qe( qe ), d_term_iter( -1 ){ - Assert( !d_op.isNull() ); -} -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_itergetTermDatabase()->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(false) ); - d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() ); -} -Node CandidateGeneratorQELitDeq::getNextCandidate(){ - //get next candidate term in equivalence class - while( !d_eqc_false.isFinished() ){ - Node n = (*d_eqc_false); - ++d_eqc_false; - if( n.getKind()==d_match_pattern.getKind() ){ - //found an iff or equality, try to match it - //DO_THIS: cache to avoid redundancies? - //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false? - return n; - } - } - return Node::null(); -} +/********************* */ +/*! \file theory_uf_candidate_generator.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of theory uf candidate generator class + **/ + +#include "theory/candidate_generator.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" +#include "theory/quantifiers/term_database.h" +#include "theory/inst_match.h" +#include "theory/quantifiers_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::inst; + +bool CandidateGenerator::isLegalCandidate( Node n ){ + return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) ); +} + +void CandidateGeneratorQueue::addCandidate( Node n ) { + if( isLegalCandidate( n ) ){ + d_candidates.push_back( n ); + } +} + +void CandidateGeneratorQueue::reset( Node eqc ){ + if( d_candidate_index>0 ){ + d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index ); + d_candidate_index = 0; + } + if( !eqc.isNull() ){ + d_candidates.push_back( eqc ); + } +} +Node CandidateGeneratorQueue::getNextCandidate(){ + if( d_candidate_index<(int)d_candidates.size() ){ + Node n = d_candidates[d_candidate_index]; + d_candidate_index++; + return n; + }else{ + d_candidate_index = 0; + d_candidates.clear(); + return Node::null(); + } +} + +#if 0 + +CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) : + d_op( op ), d_qe( qe ), d_term_iter( -2 ){ + Assert( !d_op.isNull() ); +} +void CandidateGeneratorQE::resetInstantiationRound(){ + d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size(); +} + +void CandidateGeneratorQE::reset( Node eqc ){ + if( eqc.isNull() ){ + d_term_iter = 0; + }else{ + //create an equivalence class iterator in eq class eqc + if( d_qe->getEqualityQuery()->getEngine()->hasTerm( eqc ) ){ + eqc = d_qe->getEqualityQuery()->getEngine()->getRepresentative( eqc ); + d_eqc = eq::EqClassIterator( eqc, d_qe->getEqualityQuery()->getEngine() ); + d_retNode = Node::null(); + }else{ + d_retNode = eqc; + } + d_term_iter = -1; + } +} + +Node CandidateGeneratorQE::getNextCandidate(){ + if( d_term_iter>=0 ){ + //get next candidate term in the uf term database + while( d_term_itergetTermDatabase()->d_op_map[d_op][d_term_iter]; + d_term_iter++; + if( isLegalCandidate( n ) ){ + return n; + } + } + }else if( d_term_iter==-1 ){ + if( d_retNode.isNull() ){ + //get next candidate term in equivalence class + while( !d_eqc.isFinished() ){ + Node n = (*d_eqc); + ++d_eqc; + if( n.hasOperator() && n.getOperator()==d_op ){ + if( isLegalCandidate( n ) ){ + return n; + } + } + } + }else{ + Node ret; + if( d_retNode.hasOperator() && d_retNode.getOperator()==d_op ){ + ret = d_retNode; + } + d_term_iter = -2; //done returning matches + return ret; + } + } + return Node::null(); +} + +#else + + +CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) : + d_op( op ), d_qe( qe ), d_term_iter( -1 ){ + Assert( !d_op.isNull() ); +} +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_itergetTermDatabase()->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(false) ); + d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() ); +} +Node CandidateGeneratorQELitDeq::getNextCandidate(){ + //get next candidate term in equivalence class + while( !d_eqc_false.isFinished() ){ + Node n = (*d_eqc_false); + ++d_eqc_false; + if( n.getKind()==d_match_pattern.getKind() ){ + //found an iff or equality, try to match it + //DO_THIS: cache to avoid redundancies? + //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false? + return n; + } + } + return Node::null(); +} diff --git a/src/theory/candidate_generator.h b/src/theory/candidate_generator.h index 2152f1ef6..134b0e1b7 100644 --- a/src/theory/candidate_generator.h +++ b/src/theory/candidate_generator.h @@ -1,187 +1,187 @@ -/********************* */ -/*! \file candidate_generator.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Theory uf candidate generator - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__CANDIDATE_GENERATOR_H -#define __CVC4__CANDIDATE_GENERATOR_H - -#include "theory/theory.h" -#include "theory/uf/equality_engine.h" - -namespace CVC4 { -namespace theory { - -class QuantifiersEngine; - -namespace inst { - -/** base class for generating candidates for matching */ -class CandidateGenerator { -public: - CandidateGenerator(){} - ~CandidateGenerator(){} - - /** Get candidates functions. These set up a context to get all match candidates. - cg->reset( eqc ); - do{ - Node cand = cg->getNextCandidate(); - //....... - }while( !cand.isNull() ); - - eqc is the equivalence class you are searching in - */ - virtual void reset( Node eqc ) = 0; - virtual Node getNextCandidate() = 0; - /** add candidate to list of nodes returned by this generator */ - virtual void addCandidate( Node n ) {} - /** call this at the beginning of each instantiation round */ - virtual void resetInstantiationRound() = 0; -public: - /** legal candidate */ - static bool isLegalCandidate( Node n ); -};/* class CandidateGenerator */ - -/** candidate generator queue (for manual candidate generation) */ -class CandidateGeneratorQueue : public CandidateGenerator { -private: - std::vector< Node > d_candidates; - int d_candidate_index; -public: - CandidateGeneratorQueue() : d_candidate_index( 0 ){} - ~CandidateGeneratorQueue(){} - - void addCandidate( Node n ); - - void resetInstantiationRound(){} - void reset( Node eqc ); - Node getNextCandidate(); -};/* class CandidateGeneratorQueue */ - -class CandidateGeneratorQEDisequal; - -#if 0 - -class CandidateGeneratorQE : public CandidateGenerator -{ - friend class CandidateGeneratorQEDisequal; -private: - //operator you are looking for - Node d_op; - //instantiator pointer - QuantifiersEngine* d_qe; - //the equality class iterator - eq::EqClassIterator d_eqc; - int d_term_iter; - int d_term_iter_limit; -private: - Node d_retNode; -public: - CandidateGeneratorQE( QuantifiersEngine* qe, Node op ); - ~CandidateGeneratorQE(){} - - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); -}; - -#else - -class CandidateGeneratorQE : public CandidateGenerator -{ - friend class CandidateGeneratorQEDisequal; -private: - //operator you are looking for - Node d_op; - //instantiator pointer - QuantifiersEngine* d_qe; - //the equality class iterator - std::vector< Node > d_eqc; - int d_term_iter; - int d_term_iter_limit; - bool d_using_term_db; -public: - CandidateGeneratorQE( QuantifiersEngine* qe, Node op ); - ~CandidateGeneratorQE(){} - - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); -}; - -#endif - -//class CandidateGeneratorQEDisequal : public CandidateGenerator -//{ -//private: -// //equivalence class -// Node d_eq_class; -// //equivalence class info -// EqClassInfo* d_eci; -// //equivalence class iterator -// EqClassInfo::BoolMap::const_iterator d_eqci_iter; -// //instantiator pointer -// QuantifiersEngine* d_qe; -//public: -// CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ); -// ~CandidateGeneratorQEDisequal(){} -// -// void resetInstantiationRound(); -// void reset( Node eqc ); //should be what you want to be disequal from -// Node getNextCandidate(); -//}; - -class CandidateGeneratorQELitEq : public CandidateGenerator -{ -private: - //the equality classes iterator - eq::EqClassesIterator d_eq; - //equality you are trying to match equalities for - Node d_match_pattern; - //einstantiator pointer - QuantifiersEngine* d_qe; -public: - CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ); - ~CandidateGeneratorQELitEq(){} - - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); -}; - -class CandidateGeneratorQELitDeq : public CandidateGenerator -{ -private: - //the equality class iterator for false - eq::EqClassIterator d_eqc_false; - //equality you are trying to match disequalities for - Node d_match_pattern; - //einstantiator pointer - QuantifiersEngine* d_qe; -public: - CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ); - ~CandidateGeneratorQELitDeq(){} - - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); -}; - -}/* CVC4::theory::inst namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */ +/********************* */ +/*! \file candidate_generator.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory uf candidate generator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CANDIDATE_GENERATOR_H +#define __CVC4__CANDIDATE_GENERATOR_H + +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +namespace inst { + +/** base class for generating candidates for matching */ +class CandidateGenerator { +public: + CandidateGenerator(){} + ~CandidateGenerator(){} + + /** Get candidates functions. These set up a context to get all match candidates. + cg->reset( eqc ); + do{ + Node cand = cg->getNextCandidate(); + //....... + }while( !cand.isNull() ); + + eqc is the equivalence class you are searching in + */ + virtual void reset( Node eqc ) = 0; + virtual Node getNextCandidate() = 0; + /** add candidate to list of nodes returned by this generator */ + virtual void addCandidate( Node n ) {} + /** call this at the beginning of each instantiation round */ + virtual void resetInstantiationRound() = 0; +public: + /** legal candidate */ + static bool isLegalCandidate( Node n ); +};/* class CandidateGenerator */ + +/** candidate generator queue (for manual candidate generation) */ +class CandidateGeneratorQueue : public CandidateGenerator { +private: + std::vector< Node > d_candidates; + int d_candidate_index; +public: + CandidateGeneratorQueue() : d_candidate_index( 0 ){} + ~CandidateGeneratorQueue(){} + + void addCandidate( Node n ); + + void resetInstantiationRound(){} + void reset( Node eqc ); + Node getNextCandidate(); +};/* class CandidateGeneratorQueue */ + +class CandidateGeneratorQEDisequal; + +#if 0 + +class CandidateGeneratorQE : public CandidateGenerator +{ + friend class CandidateGeneratorQEDisequal; +private: + //operator you are looking for + Node d_op; + //instantiator pointer + QuantifiersEngine* d_qe; + //the equality class iterator + eq::EqClassIterator d_eqc; + int d_term_iter; + int d_term_iter_limit; +private: + Node d_retNode; +public: + CandidateGeneratorQE( QuantifiersEngine* qe, Node op ); + ~CandidateGeneratorQE(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +#else + +class CandidateGeneratorQE : public CandidateGenerator +{ + friend class CandidateGeneratorQEDisequal; +private: + //operator you are looking for + Node d_op; + //instantiator pointer + QuantifiersEngine* d_qe; + //the equality class iterator + std::vector< Node > d_eqc; + int d_term_iter; + int d_term_iter_limit; + bool d_using_term_db; +public: + CandidateGeneratorQE( QuantifiersEngine* qe, Node op ); + ~CandidateGeneratorQE(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +#endif + +//class CandidateGeneratorQEDisequal : public CandidateGenerator +//{ +//private: +// //equivalence class +// Node d_eq_class; +// //equivalence class info +// EqClassInfo* d_eci; +// //equivalence class iterator +// EqClassInfo::BoolMap::const_iterator d_eqci_iter; +// //instantiator pointer +// QuantifiersEngine* d_qe; +//public: +// CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ); +// ~CandidateGeneratorQEDisequal(){} +// +// void resetInstantiationRound(); +// void reset( Node eqc ); //should be what you want to be disequal from +// Node getNextCandidate(); +//}; + +class CandidateGeneratorQELitEq : public CandidateGenerator +{ +private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equality you are trying to match equalities for + Node d_match_pattern; + //einstantiator pointer + QuantifiersEngine* d_qe; +public: + CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ); + ~CandidateGeneratorQELitEq(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +class CandidateGeneratorQELitDeq : public CandidateGenerator +{ +private: + //the equality class iterator for false + eq::EqClassIterator d_eqc_false; + //equality you are trying to match disequalities for + Node d_match_pattern; + //einstantiator pointer + QuantifiersEngine* d_qe; +public: + CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ); + ~CandidateGeneratorQELitDeq(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +}/* CVC4::theory::inst namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */ diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp index c90483fa3..bad7e34cb 100644 --- a/src/theory/inst_match.cpp +++ b/src/theory/inst_match.cpp @@ -272,9 +272,6 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; - //get the equality engine - Theory* th_uf = qe->getTheoryEngine()->getTheory( theory::THEORY_UF ); - uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator(); //create candidate generator if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); diff --git a/src/theory/model.cpp b/src/theory/model.cpp index aa2c2d938..feedc0c31 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -1,615 +1,615 @@ -/********************* */ -/*! \file model.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of model class - **/ - -#include "theory/model.h" -#include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" -#include "util/datatype.h" -#include "theory/uf/theory_uf_model.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; - -void RepSet::clear(){ - d_type_reps.clear(); - d_tmap.clear(); -} - -void RepSet::add( Node n ){ - TypeNode t = n.getType(); - d_tmap[ n ] = (int)d_type_reps[t].size(); - d_type_reps[t].push_back( n ); -} - -void RepSet::set( TypeNode t, std::vector< Node >& reps ){ - for( size_t i=0; i >::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; i0 ){ 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 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; ibooleanType() ){ - 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; imkVar( 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; id_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; igetNewDomainValue( eqc.getType() ); - if( !rep.isNull() ){ - return rep; - }else{ - //if we can't get new domain value, just return eqc itself (this typically should not happen) - //FIXME: Assertion failure here? - return eqc; - } -} +/********************* */ +/*! \file model.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of model class + **/ + +#include "theory/model.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" +#include "util/datatype.h" +#include "theory/uf/theory_uf_model.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; + +void RepSet::clear(){ + d_type_reps.clear(); + d_tmap.clear(); +} + +void RepSet::add( Node n ){ + TypeNode t = n.getType(); + d_tmap[ n ] = (int)d_type_reps[t].size(); + d_type_reps[t].push_back( n ); +} + +void RepSet::set( TypeNode t, std::vector< Node >& reps ){ + for( size_t i=0; i >::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; i0 ){ 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 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; ibooleanType() ){ + 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; imkVar( 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; id_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; igetNewDomainValue( eqc.getType() ); + if( !rep.isNull() ){ + return rep; + }else{ + //if we can't get new domain value, just return eqc itself (this typically should not happen) + //FIXME: Assertion failure here? + return eqc; + } +} diff --git a/src/theory/model.h b/src/theory/model.h index 415b008ef..940a2f527 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -1,191 +1,191 @@ -/********************* */ -/*! \file model.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Model class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY_MODEL_H -#define __CVC4__THEORY_MODEL_H - -#include "util/model.h" -#include "theory/uf/equality_engine.h" - -namespace CVC4 { -namespace theory { - -class QuantifiersEngine; - -/** this class stores a representative set */ -class RepSet { -public: - RepSet(){} - ~RepSet(){} - std::map< TypeNode, std::vector< Node > > d_type_reps; - std::map< Node, int > d_tmap; - /** clear the set */ - void clear(); - /** has type */ - bool hasType( TypeNode tn ) { return d_type_reps.find( tn )!=d_type_reps.end(); } - /** add representative for type */ - void add( Node n ); - /** set the representatives for type */ - void set( TypeNode t, std::vector< Node >& reps ); - /** returns index in d_type_reps for node n */ - int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; } - /** debug print */ - void toStream(std::ostream& out); -}; - -//representative domain -typedef std::vector< int > RepDomain; - -class TheoryEngineModelBuilder; - -/** Theory Model class - * For Model m, should call m.initialize() before using - */ -class TheoryModel : public Model -{ - friend class TheoryEngineModelBuilder; -protected: - /** add term function - * This should be called on all terms that exist in the model. - * addTerm( n ) will do any model-specific processing necessary for n, - * such as contraining the interpretation of uninterpretted functions. - */ - virtual void addTerm( Node n ) {} -private: - /** List of definitions that the user has given - * This is necessary for supporting the get-model command. - */ - std::vector< Node > d_define_funcs; - std::vector< TypeNode > d_define_types; - std::vector< int > d_defines; -protected: - /** print the value of the function n to stream */ - virtual void toStreamFunction( Node n, std::ostream& out ); - /** print the value of the type tn to stream */ - virtual void toStreamType( TypeNode tn, std::ostream& out ); -public: - TheoryModel( context::Context* c, std::string name ); - virtual ~TheoryModel(){} - /** equality engine containing all known equalities/disequalities */ - eq::EqualityEngine d_equalityEngine; - /** map of representatives of equality engine to used representatives in representative set */ - std::map< Node, Node > d_reps; - /** stores set of representatives for each type */ - RepSet d_rep_set; - /** true/false nodes */ - Node d_true; - Node d_false; -public: - /** reset the model */ - virtual void reset(); - /** get interpreted value - * This function is called when the value of the node cannot be determined by the theory rewriter - * This should function should return a representative in d_reps - */ - virtual Node getInterpretedValue( TNode n ) = 0; -public: - /** add defined function (for get-model) */ - void addDefineFunction( Node n ); - /** add defined type (for get-model) */ - void addDefineType( TypeNode tn ); - /** - * Get value function. This should be called only after a ModelBuilder has called buildModel(...) - * on this model. - */ - Node getValue( TNode n ); - /** get existing domain value, with possible exclusions - * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude - */ - Node getDomainValue( TypeNode tn, std::vector< Node >& exclude ); - /** get new domain value - * This function returns a constant term of type tn that is not in d_rep_set.d_type_reps[tn] - * If it cannot find such a node, it returns null. - */ - Node getNewDomainValue( TypeNode tn ); -public: - /** assert equality holds in the model */ - void assertEquality( Node a, Node b, bool polarity ); - /** assert predicate holds in the model */ - void assertPredicate( Node a, bool polarity ); - /** assert all equalities/predicates in equality engine hold in the model */ - void assertEqualityEngine( eq::EqualityEngine* ee ); -public: - /** general queries */ - bool hasTerm( Node a ); - Node getRepresentative( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); -public: - /** print representative debug function */ - void printRepresentativeDebug( const char* c, Node r ); - /** print representative function */ - void printRepresentative( std::ostream& out, Node r ); - /** to stream function */ - void toStream( std::ostream& out ); -}; - -/** Default model class - * The getInterpretedValue function will choose an existing value arbitrarily. - * If none are found, then it will create a new value. - */ -class DefaultModel : public TheoryModel -{ -protected: - /** whether function models are enabled */ - bool d_enableFuncModels; - /** add term */ - void addTerm( Node n ); -public: - DefaultModel( context::Context* c, std::string name, bool enableFuncModels ); - virtual ~DefaultModel(){} - //necessary information for function models - std::map< Node, std::vector< Node > > d_uf_terms; - std::map< Node, Node > d_uf_models; -public: - void reset(); - Node getInterpretedValue( TNode n ); -}; - -/** TheoryEngineModelBuilder class - * This model builder will consult all theories in a theory engine for - * collectModelInfo( ... ) when building a model. - */ -class TheoryEngineModelBuilder : public ModelBuilder -{ -protected: - /** pointer to theory engine */ - TheoryEngine* d_te; - /** choose representative for unresolved equivalence class */ - void initializeType( TypeNode tn, std::map< TypeNode, bool >& unresolved_types ); - /** process build model */ - virtual void processBuildModel( TheoryModel* m ){} - /** choose representative for unconstrained equivalence class */ - virtual Node chooseRepresentative( TheoryModel* m, Node eqc ); -public: - TheoryEngineModelBuilder( TheoryEngine* te ); - virtual ~TheoryEngineModelBuilder(){} - /** Build model function. - * Should be called only on TheoryModels m - */ - void buildModel( Model* m ); -}; - -} -} - -#endif +/********************* */ +/*! \file model.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Model class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_MODEL_H +#define __CVC4__THEORY_MODEL_H + +#include "util/model.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +/** this class stores a representative set */ +class RepSet { +public: + RepSet(){} + ~RepSet(){} + std::map< TypeNode, std::vector< Node > > d_type_reps; + std::map< Node, int > d_tmap; + /** clear the set */ + void clear(); + /** has type */ + bool hasType( TypeNode tn ) { return d_type_reps.find( tn )!=d_type_reps.end(); } + /** add representative for type */ + void add( Node n ); + /** set the representatives for type */ + void set( TypeNode t, std::vector< Node >& reps ); + /** returns index in d_type_reps for node n */ + int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; } + /** debug print */ + void toStream(std::ostream& out); +}; + +//representative domain +typedef std::vector< int > RepDomain; + +class TheoryEngineModelBuilder; + +/** Theory Model class + * For Model m, should call m.initialize() before using + */ +class TheoryModel : public Model +{ + friend class TheoryEngineModelBuilder; +protected: + /** add term function + * This should be called on all terms that exist in the model. + * addTerm( n ) will do any model-specific processing necessary for n, + * such as contraining the interpretation of uninterpretted functions. + */ + virtual void addTerm( Node n ) {} +private: + /** List of definitions that the user has given + * This is necessary for supporting the get-model command. + */ + std::vector< Node > d_define_funcs; + std::vector< TypeNode > d_define_types; + std::vector< int > d_defines; +protected: + /** print the value of the function n to stream */ + virtual void toStreamFunction( Node n, std::ostream& out ); + /** print the value of the type tn to stream */ + virtual void toStreamType( TypeNode tn, std::ostream& out ); +public: + TheoryModel( context::Context* c, std::string name ); + virtual ~TheoryModel(){} + /** equality engine containing all known equalities/disequalities */ + eq::EqualityEngine d_equalityEngine; + /** map of representatives of equality engine to used representatives in representative set */ + std::map< Node, Node > d_reps; + /** stores set of representatives for each type */ + RepSet d_rep_set; + /** true/false nodes */ + Node d_true; + Node d_false; +public: + /** reset the model */ + virtual void reset(); + /** get interpreted value + * This function is called when the value of the node cannot be determined by the theory rewriter + * This should function should return a representative in d_reps + */ + virtual Node getInterpretedValue( TNode n ) = 0; +public: + /** add defined function (for get-model) */ + void addDefineFunction( Node n ); + /** add defined type (for get-model) */ + void addDefineType( TypeNode tn ); + /** + * Get value function. This should be called only after a ModelBuilder has called buildModel(...) + * on this model. + */ + Node getValue( TNode n ); + /** get existing domain value, with possible exclusions + * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude + */ + Node getDomainValue( TypeNode tn, std::vector< Node >& exclude ); + /** get new domain value + * This function returns a constant term of type tn that is not in d_rep_set.d_type_reps[tn] + * If it cannot find such a node, it returns null. + */ + Node getNewDomainValue( TypeNode tn ); +public: + /** assert equality holds in the model */ + void assertEquality( Node a, Node b, bool polarity ); + /** assert predicate holds in the model */ + void assertPredicate( Node a, bool polarity ); + /** assert all equalities/predicates in equality engine hold in the model */ + void assertEqualityEngine( eq::EqualityEngine* ee ); +public: + /** general queries */ + bool hasTerm( Node a ); + Node getRepresentative( Node a ); + bool areEqual( Node a, Node b ); + bool areDisequal( Node a, Node b ); +public: + /** print representative debug function */ + void printRepresentativeDebug( const char* c, Node r ); + /** print representative function */ + void printRepresentative( std::ostream& out, Node r ); + /** to stream function */ + void toStream( std::ostream& out ); +}; + +/** Default model class + * The getInterpretedValue function will choose an existing value arbitrarily. + * If none are found, then it will create a new value. + */ +class DefaultModel : public TheoryModel +{ +protected: + /** whether function models are enabled */ + bool d_enableFuncModels; + /** add term */ + void addTerm( Node n ); +public: + DefaultModel( context::Context* c, std::string name, bool enableFuncModels ); + virtual ~DefaultModel(){} + //necessary information for function models + std::map< Node, std::vector< Node > > d_uf_terms; + std::map< Node, Node > d_uf_models; +public: + void reset(); + Node getInterpretedValue( TNode n ); +}; + +/** TheoryEngineModelBuilder class + * This model builder will consult all theories in a theory engine for + * collectModelInfo( ... ) when building a model. + */ +class TheoryEngineModelBuilder : public ModelBuilder +{ +protected: + /** pointer to theory engine */ + TheoryEngine* d_te; + /** choose representative for unresolved equivalence class */ + void initializeType( TypeNode tn, std::map< TypeNode, bool >& unresolved_types ); + /** process build model */ + virtual void processBuildModel( TheoryModel* m ){} + /** choose representative for unconstrained equivalence class */ + virtual Node chooseRepresentative( TheoryModel* m, Node eqc ); +public: + TheoryEngineModelBuilder( TheoryEngine* te ); + virtual ~TheoryEngineModelBuilder(){} + /** Build model function. + * Should be called only on TheoryModels m + */ + void buildModel( Model* m ); +}; + +} +} + +#endif diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 766bd31ae..1c6b47867 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -1,184 +1,184 @@ -/********************* */ -/*! \file first_order_model.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of model engine model class - **/ - -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/rep_set_iterator.h" -#include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/term_database.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - -FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name, true ), -d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){ - -} - -void FirstOrderModel::reset(){ - //rebuild models - d_uf_model_tree.clear(); - d_uf_model_gen.clear(); - d_array_model.clear(); - DefaultModel::reset(); -} - -void FirstOrderModel::addTerm( Node n ){ - //std::vector< Node > added; - //d_term_db->addTerm( n, added, false ); - DefaultModel::addTerm( n ); -} - -void FirstOrderModel::initialize(){ - //this is called after representatives have been chosen and the equality engine has been built - //for each quantifier, collect all operators we care about - for( int i=0; iprintModelEngine ){ - for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){ - if( it->first.isSort() ){ - Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; - } - } - } -} - -void FirstOrderModel::initializeModelForTerm( Node n ){ - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){ - TypeNode tn = op.getType(); - tn = tn[ (int)tn.getNumChildren()-1 ]; - //only generate models for predicates and functions with uninterpreted range types - if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){ - d_uf_model_tree[ op ] = uf::UfModelTree( op ); - d_uf_model_gen[ op ].clear(); - } - } - } - /* - if( n.getType().isArray() ){ - while( n.getKind()==STORE ){ - n = n[0]; - } - Node nn = getRepresentative( n ); - if( d_array_model.find( nn )==d_array_model.end() ){ - d_array_model[nn] = arrays::ArrayModel( nn, this ); - } - } - */ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - initializeModelForTerm( n[i] ); - } -} - -void FirstOrderModel::toStreamFunction( Node n, std::ostream& out ){ - /* - if( d_uf_model.find( n )!=d_uf_model.end() ){ - //d_uf_model[n].toStream( out ); - Node value = d_uf_model[n].getFunctionValue(); - out << "(" << n << " " << value << ")"; - }else if( d_array_model.find( n )!=d_array_model.end() ){ - Node value = d_array_model[n].getArrayValue(); - out << "(" << n << " " << value << ")" << std::endl; - } - */ - DefaultModel::toStreamFunction( n, out ); -} - -void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){ - DefaultModel::toStreamType( tn, out ); -} - -Node FirstOrderModel::getInterpretedValue( TNode n ){ - Debug("fo-model") << "get interpreted value " << n << std::endl; - TypeNode type = n.getType(); - if( type.isFunction() || type.isPredicate() ){ - if( d_uf_models.find( n )==d_uf_models.end() ){ - //use the model tree to generate the model - Node fn = d_uf_model_tree[n].getFunctionValue(); - d_uf_models[n] = fn; - return fn; - } - /* - }else if( type.isArray() ){ - if( d_array_model.find( n )!=d_array_model.end() ){ - return d_array_model[n].getArrayValue(); - }else{ - //std::cout << "no array model generated for " << n << std::endl; - } - */ - }else if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){ - //consult the uf model - int depIndex; - return d_uf_model_tree[ op ].getValue( this, n, depIndex ); - } - }else if( n.getKind()==SELECT ){ - - } - return DefaultModel::getInterpretedValue( n ); -} - -TermDb* FirstOrderModel::getTermDatabase(){ - return d_term_db; -} - - -void FirstOrderModel::toStream(std::ostream& out){ - DefaultModel::toStream( out ); -#if 0 - out << "---Current Model---" << std::endl; - out << "Representatives: " << std::endl; - d_rep_set.toStream( out ); - out << "Functions: " << std::endl; - for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){ - it->second.toStream( out ); - out << std::endl; - } -#elif 0 - d_rep_set.toStream( out ); - //print everything not related to UF in equality engine - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - Node rep = getRepresentative( eqc ); - TypeNode type = rep.getType(); - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - //do not print things that have interpretations in model - if( (*eqc_i).getMetaKind()!=kind::metakind::CONSTANT && !hasInterpretedValue( *eqc_i ) ){ - out << "(" << (*eqc_i) << " " << rep << ")" << std::endl; - } - ++eqc_i; - } - ++eqcs_i; - } - //print functions - for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){ - it->second.toStream( out ); - out << std::endl; - } -#endif +/********************* */ +/*! \file first_order_model.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of model engine model class + **/ + +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/rep_set_iterator.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name, true ), +d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){ + +} + +void FirstOrderModel::reset(){ + //rebuild models + d_uf_model_tree.clear(); + d_uf_model_gen.clear(); + d_array_model.clear(); + DefaultModel::reset(); +} + +void FirstOrderModel::addTerm( Node n ){ + //std::vector< Node > added; + //d_term_db->addTerm( n, added, false ); + DefaultModel::addTerm( n ); +} + +void FirstOrderModel::initialize(){ + //this is called after representatives have been chosen and the equality engine has been built + //for each quantifier, collect all operators we care about + for( int i=0; iprintModelEngine ){ + for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){ + if( it->first.isSort() ){ + Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + } + } + } +} + +void FirstOrderModel::initializeModelForTerm( Node n ){ + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){ + TypeNode tn = op.getType(); + tn = tn[ (int)tn.getNumChildren()-1 ]; + //only generate models for predicates and functions with uninterpreted range types + if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){ + d_uf_model_tree[ op ] = uf::UfModelTree( op ); + d_uf_model_gen[ op ].clear(); + } + } + } + /* + if( n.getType().isArray() ){ + while( n.getKind()==STORE ){ + n = n[0]; + } + Node nn = getRepresentative( n ); + if( d_array_model.find( nn )==d_array_model.end() ){ + d_array_model[nn] = arrays::ArrayModel( nn, this ); + } + } + */ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + initializeModelForTerm( n[i] ); + } +} + +void FirstOrderModel::toStreamFunction( Node n, std::ostream& out ){ + /* + if( d_uf_model.find( n )!=d_uf_model.end() ){ + //d_uf_model[n].toStream( out ); + Node value = d_uf_model[n].getFunctionValue(); + out << "(" << n << " " << value << ")"; + }else if( d_array_model.find( n )!=d_array_model.end() ){ + Node value = d_array_model[n].getArrayValue(); + out << "(" << n << " " << value << ")" << std::endl; + } + */ + DefaultModel::toStreamFunction( n, out ); +} + +void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){ + DefaultModel::toStreamType( tn, out ); +} + +Node FirstOrderModel::getInterpretedValue( TNode n ){ + Debug("fo-model") << "get interpreted value " << n << std::endl; + TypeNode type = n.getType(); + if( type.isFunction() || type.isPredicate() ){ + if( d_uf_models.find( n )==d_uf_models.end() ){ + //use the model tree to generate the model + Node fn = d_uf_model_tree[n].getFunctionValue(); + d_uf_models[n] = fn; + return fn; + } + /* + }else if( type.isArray() ){ + if( d_array_model.find( n )!=d_array_model.end() ){ + return d_array_model[n].getArrayValue(); + }else{ + //std::cout << "no array model generated for " << n << std::endl; + } + */ + }else if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){ + //consult the uf model + int depIndex; + return d_uf_model_tree[ op ].getValue( this, n, depIndex ); + } + }else if( n.getKind()==SELECT ){ + + } + return DefaultModel::getInterpretedValue( n ); +} + +TermDb* FirstOrderModel::getTermDatabase(){ + return d_term_db; +} + + +void FirstOrderModel::toStream(std::ostream& out){ + DefaultModel::toStream( out ); +#if 0 + out << "---Current Model---" << std::endl; + out << "Representatives: " << std::endl; + d_rep_set.toStream( out ); + out << "Functions: " << std::endl; + for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){ + it->second.toStream( out ); + out << std::endl; + } +#elif 0 + d_rep_set.toStream( out ); + //print everything not related to UF in equality engine + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + Node rep = getRepresentative( eqc ); + TypeNode type = rep.getType(); + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + //do not print things that have interpretations in model + if( (*eqc_i).getMetaKind()!=kind::metakind::CONSTANT && !hasInterpretedValue( *eqc_i ) ){ + out << "(" << (*eqc_i) << " " << rep << ")" << std::endl; + } + ++eqc_i; + } + ++eqcs_i; + } + //print functions + for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){ + it->second.toStream( out ); + out << std::endl; + } +#endif } \ No newline at end of file diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 825518ed0..afa8dab79 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -1,89 +1,89 @@ -/********************* */ -/*! \file first_order_model.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Model extended classes - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__FIRST_ORDER_MODEL_H -#define __CVC4__FIRST_ORDER_MODEL_H - -#include "theory/model.h" -#include "theory/uf/theory_uf_model.h" -#include "theory/arrays/theory_arrays_model.h" - -namespace CVC4 { -namespace theory { - -struct ModelBasisAttributeId {}; -typedef expr::Attribute 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 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 d_forall_asserts; - /** get number of asserted quantifiers */ - int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); } - /** get asserted quantifier */ - Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; } -public: - FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ); - virtual ~FirstOrderModel(){} - // reset the model - void reset(); - /** get interpreted value */ - Node getInterpretedValue( TNode n ); -public: - // initialize the model - void initialize(); - /** get term database */ - TermDb* getTermDatabase(); - /** to stream function */ - void toStream( std::ostream& out ); -}; - -} -} -} - -#endif +/********************* */ +/*! \file first_order_model.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Model extended classes + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__FIRST_ORDER_MODEL_H +#define __CVC4__FIRST_ORDER_MODEL_H + +#include "theory/model.h" +#include "theory/uf/theory_uf_model.h" +#include "theory/arrays/theory_arrays_model.h" + +namespace CVC4 { +namespace theory { + +struct ModelBasisAttributeId {}; +typedef expr::Attribute 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 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 d_forall_asserts; + /** get number of asserted quantifiers */ + int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); } + /** get asserted quantifier */ + Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; } +public: + FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ); + virtual ~FirstOrderModel(){} + // reset the model + void reset(); + /** get interpreted value */ + Node getInterpretedValue( TNode n ); +public: + // initialize the model + void initialize(); + /** get term database */ + TermDb* getTermDatabase(); + /** to stream function */ + void toStream( std::ostream& out ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 13d500d8e..05eb8f55f 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -1,91 +1,91 @@ -/********************* */ -/*! \file model_builder.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Model Builder class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__QUANTIFIERS_MODEL_BUILDER_H -#define __CVC4__QUANTIFIERS_MODEL_BUILDER_H - -#include "theory/quantifiers_engine.h" -#include "theory/model.h" -#include "theory/uf/theory_uf_model.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -//the model builder -class ModelEngineBuilder : public TheoryEngineModelBuilder -{ -protected: - //quantifiers engine - QuantifiersEngine* d_qe; - //map from operators to model preference data - std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; - //built model uf - std::map< Node, bool > d_uf_model_constructed; - /** process build model */ - void processBuildModel( TheoryModel* m ); - /** choose representative for unconstrained equivalence class */ - Node chooseRepresentative( TheoryModel* m, Node eqc ); - /** bad representative */ - bool isBadRepresentative( Node n ); -protected: - //analyze model - void analyzeModel( FirstOrderModel* fm ); - //analyze quantifiers - void analyzeQuantifiers( FirstOrderModel* fm ); - //build model - void finishBuildModel( FirstOrderModel* fm ); - //theory-specific build models - void finishBuildModelUf( FirstOrderModel* fm, Node op ); - //do InstGen techniques for quantifier, return number of lemmas produced - int doInstGen( FirstOrderModel* fm, Node f ); -public: - ModelEngineBuilder( QuantifiersEngine* qe ); - virtual ~ModelEngineBuilder(){} - /** finish model */ - void finishProcessBuildModel( TheoryModel* m ); -public: - /** number of lemmas generated while building model */ - int d_addedLemmas; - //map from quantifiers to if are constant SAT - std::map< Node, bool > d_quant_sat; - //map from quantifiers to the instantiation literals that their model is dependent upon - std::map< Node, std::vector< Node > > d_quant_selection_lits; -public: - //map from quantifiers to model basis match - std::map< Node, InstMatch > d_quant_basis_match; - //options - bool optUseModel(); - bool optInstGen(); - bool optOneQuantPerRoundInstGen(); - /** statistics class */ - class Statistics { - public: - IntStat d_pre_sat_quant; - IntStat d_pre_nsat_quant; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; -}; - -} -} -} - -#endif +/********************* */ +/*! \file model_builder.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Model Builder class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_MODEL_BUILDER_H +#define __CVC4__QUANTIFIERS_MODEL_BUILDER_H + +#include "theory/quantifiers_engine.h" +#include "theory/model.h" +#include "theory/uf/theory_uf_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +//the model builder +class ModelEngineBuilder : public TheoryEngineModelBuilder +{ +protected: + //quantifiers engine + QuantifiersEngine* d_qe; + //map from operators to model preference data + std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; + //built model uf + std::map< Node, bool > d_uf_model_constructed; + /** process build model */ + void processBuildModel( TheoryModel* m ); + /** choose representative for unconstrained equivalence class */ + Node chooseRepresentative( TheoryModel* m, Node eqc ); + /** bad representative */ + bool isBadRepresentative( Node n ); +protected: + //analyze model + void analyzeModel( FirstOrderModel* fm ); + //analyze quantifiers + void analyzeQuantifiers( FirstOrderModel* fm ); + //build model + void finishBuildModel( FirstOrderModel* fm ); + //theory-specific build models + void finishBuildModelUf( FirstOrderModel* fm, Node op ); + //do InstGen techniques for quantifier, return number of lemmas produced + int doInstGen( FirstOrderModel* fm, Node f ); +public: + ModelEngineBuilder( QuantifiersEngine* qe ); + virtual ~ModelEngineBuilder(){} + /** finish model */ + void finishProcessBuildModel( TheoryModel* m ); +public: + /** number of lemmas generated while building model */ + int d_addedLemmas; + //map from quantifiers to if are constant SAT + std::map< Node, bool > d_quant_sat; + //map from quantifiers to the instantiation literals that their model is dependent upon + std::map< Node, std::vector< Node > > d_quant_selection_lits; +public: + //map from quantifiers to model basis match + std::map< Node, InstMatch > d_quant_basis_match; + //options + bool optUseModel(); + bool optInstGen(); + bool optOneQuantPerRoundInstGen(); + /** statistics class */ + class Statistics { + public: + IntStat d_pre_sat_quant; + IntStat d_pre_nsat_quant; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 12206e148..1563a3d1d 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -1,173 +1,173 @@ -/********************* */ -/*! \file relevant_domain.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of relevant domain class - **/ - -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/relevant_domain.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/first_order_model.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - -RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){ - -} - -void RelevantDomain::compute(){ - d_quant_inst_domain.clear(); - for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ - Node f = d_model->getAssertedQuantifier( i ); - d_quant_inst_domain[f].resize( f[0].getNumChildren() ); - } - //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment) - for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin(); - it != d_model->d_uf_model_tree.end(); ++it ){ - Node op = it->first; - for( size_t i=0; id_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; id_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; id_rep_set.d_type_reps[tn].size(); i++ ){ - rd[vi].push_back( i ); - domainChanged = true; - } - } - }else{ - //infinite domain? - } - } - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){ - domainChanged = true; - } - } - } - return domainChanged; -} - -bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){ - if( n.getKind()==INST_CONSTANT ){ - Node f = n.getAttribute(InstConstantAttribute()); - int var = n.getAttribute(InstVarNumAttribute()); - range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() ); - return false; - }else{ - Node op; - if( n.getKind()==APPLY_UF ){ - op = n.getOperator(); - } - bool domainChanged = false; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - RepDomain childRange; - if( extendFunctionDomains( n[i], childRange ) ){ - domainChanged = true; - } - if( n.getKind()==APPLY_UF ){ - if( d_active_domain.find( op )!=d_active_domain.end() ){ - for( int j=0; j<(int)childRange.size(); j++ ){ - int v = childRange[j]; - if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){ - d_active_domain[op][i].push_back( v ); - domainChanged = true; - } - } - }else{ - //do this? - } - } - } - //get the range - if( n.hasAttribute(InstConstantAttribute()) ){ - if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){ - range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() ); - }else{ - //infinite range? - } - }else{ - Node r = d_model->getRepresentative( n ); - range.push_back( d_model->d_rep_set.getIndexFor( r ) ); - } - return domainChanged; - } +/********************* */ +/*! \file relevant_domain.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of relevant domain class + **/ + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){ + +} + +void RelevantDomain::compute(){ + d_quant_inst_domain.clear(); + for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ + Node f = d_model->getAssertedQuantifier( i ); + d_quant_inst_domain[f].resize( f[0].getNumChildren() ); + } + //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment) + for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin(); + it != d_model->d_uf_model_tree.end(); ++it ){ + Node op = it->first; + for( size_t i=0; id_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; id_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; id_rep_set.d_type_reps[tn].size(); i++ ){ + rd[vi].push_back( i ); + domainChanged = true; + } + } + }else{ + //infinite domain? + } + } + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){ + domainChanged = true; + } + } + } + return domainChanged; +} + +bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){ + if( n.getKind()==INST_CONSTANT ){ + Node f = n.getAttribute(InstConstantAttribute()); + int var = n.getAttribute(InstVarNumAttribute()); + range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() ); + return false; + }else{ + Node op; + if( n.getKind()==APPLY_UF ){ + op = n.getOperator(); + } + bool domainChanged = false; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + RepDomain childRange; + if( extendFunctionDomains( n[i], childRange ) ){ + domainChanged = true; + } + if( n.getKind()==APPLY_UF ){ + if( d_active_domain.find( op )!=d_active_domain.end() ){ + for( int j=0; j<(int)childRange.size(); j++ ){ + int v = childRange[j]; + if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){ + d_active_domain[op][i].push_back( v ); + domainChanged = true; + } + } + }else{ + //do this? + } + } + } + //get the range + if( n.hasAttribute(InstConstantAttribute()) ){ + if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){ + range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() ); + }else{ + //infinite range? + } + }else{ + Node r = d_model->getRepresentative( n ); + range.push_back( d_model->d_rep_set.getIndexFor( r ) ); + } + return domainChanged; + } } \ No newline at end of file diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 362a39d6a..8c8ea6a42 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -1,54 +1,54 @@ -/********************* */ -/*! \file relevant_domain.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief relevant domain class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__RELEVANT_DOMAIN_H -#define __CVC4__RELEVANT_DOMAIN_H - -#include "theory/quantifiers/first_order_model.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class RelevantDomain -{ -private: - FirstOrderModel* d_model; - - //the domain of the arguments for each operator - std::map< Node, std::map< int, RepDomain > > d_active_domain; - //the range for each operator - std::map< Node, RepDomain > d_active_range; - //for computing relevant instantiation domain, return true if changed - bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ); - //for computing extended - bool extendFunctionDomains( Node n, RepDomain& range ); -public: - RelevantDomain( FirstOrderModel* m ); - virtual ~RelevantDomain(){} - //compute the relevant domain - void compute(); - //relevant instantiation domain for each quantifier - std::map< Node, std::vector< RepDomain > > d_quant_inst_domain; -}; - -} -} -} - -#endif +/********************* */ +/*! \file relevant_domain.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief relevant domain class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__RELEVANT_DOMAIN_H +#define __CVC4__RELEVANT_DOMAIN_H + +#include "theory/quantifiers/first_order_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class RelevantDomain +{ +private: + FirstOrderModel* d_model; + + //the domain of the arguments for each operator + std::map< Node, std::map< int, RepDomain > > d_active_domain; + //the range for each operator + std::map< Node, RepDomain > d_active_range; + //for computing relevant instantiation domain, return true if changed + bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ); + //for computing extended + bool extendFunctionDomains( Node n, RepDomain& range ); +public: + RelevantDomain( FirstOrderModel* m ); + virtual ~RelevantDomain(){} + //compute the relevant domain + void compute(); + //relevant instantiation domain for each quantifier + std::map< Node, std::vector< RepDomain > > d_quant_inst_domain; +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp index 516f85857..9c1c4c89e 100644 --- a/src/theory/quantifiers/rep_set_iterator.cpp +++ b/src/theory/quantifiers/rep_set_iterator.cpp @@ -1,517 +1,517 @@ -/********************* */ -/*! \file rep_set_iterator.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of relevant domain class - **/ - -#include "theory/quantifiers/rep_set_iterator.h" -#include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/term_database.h" - -#define USE_INDEX_ORDERING - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - -RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_model( model ){ - //store instantiation constants - for( size_t i=0; id_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( childDepIndexdepIndex2 ? 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; idepIndex ){ - 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) > argIndex; - std::vector< Node > args; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( argIndex.find( n[i] )==argIndex.end() ){ - args.push_back( n[i] ); - } - argIndex[n[i]].push_back( i ); - } - sortGetMaxVariableNum sgmvn; - std::sort( args.begin(), args.end(), sgmvn ); - for( int i=0; i<(int)args.size(); i++ ){ - for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){ - d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] ); - } - } - bool useDefault = true; - for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ - if( i!=d_eval_term_index_order[n][i] ){ - useDefault = false; - break; - } - } - d_eval_uf_use_default[n] = useDefault; - Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : "; - for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ - Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " "; - } - Debug("fmf-index-order") << std::endl; -#else - d_eval_uf_use_default[n] = true; -#endif - } -} - - +/********************* */ +/*! \file rep_set_iterator.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of relevant domain class + **/ + +#include "theory/quantifiers/rep_set_iterator.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/term_database.h" + +#define USE_INDEX_ORDERING + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_model( model ){ + //store instantiation constants + for( size_t i=0; id_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( childDepIndexdepIndex2 ? 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; idepIndex ){ + 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) > argIndex; + std::vector< Node > args; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( argIndex.find( n[i] )==argIndex.end() ){ + args.push_back( n[i] ); + } + argIndex[n[i]].push_back( i ); + } + sortGetMaxVariableNum sgmvn; + std::sort( args.begin(), args.end(), sgmvn ); + for( int i=0; i<(int)args.size(); i++ ){ + for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){ + d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] ); + } + } + bool useDefault = true; + for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ + if( i!=d_eval_term_index_order[n][i] ){ + useDefault = false; + break; + } + } + d_eval_uf_use_default[n] = useDefault; + Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : "; + for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ + Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " "; + } + Debug("fmf-index-order") << std::endl; +#else + d_eval_uf_use_default[n] = true; +#endif + } +} + + diff --git a/src/theory/quantifiers/rep_set_iterator.h b/src/theory/quantifiers/rep_set_iterator.h index f6312ae5c..a5ec266a9 100644 --- a/src/theory/quantifiers/rep_set_iterator.h +++ b/src/theory/quantifiers/rep_set_iterator.h @@ -1,120 +1,120 @@ -/********************* */ -/*! \file rep_set_iterator.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief rep_set_iterator class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__REP_SET_ITERATOR_H -#define __CVC4__REP_SET_ITERATOR_H - -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/first_order_model.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -/** this class iterates over a RepSet */ -class RepSetIterator { -public: - RepSetIterator( Node f, FirstOrderModel* model ); - ~RepSetIterator(){} - //pointer to quantifier - Node d_f; - //pointer to model - FirstOrderModel* d_model; - //index we are considering - std::vector< int > d_index; - //domain we are considering - std::vector< RepDomain > d_domain; - //ordering for variables we are indexing over - // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 }, - // then we consider instantiations in this order: - // a/x a/y a/z - // a/x b/y a/z - // b/x a/y a/z - // b/x b/y a/z - // ... - std::vector< int > d_index_order; - //variables to index they are considered at - // for example, if d_index_order = { 2, 0, 1 } - // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 } - std::map< int, int > d_var_order; - //the instantiation constants of d_f - std::vector< Node > d_ic; - //the current terms we are considering - std::vector< Node > d_terms; -public: - /** set index order */ - void setIndexOrder( std::vector< int >& indexOrder ); - /** set domain */ - void setDomain( std::vector< RepDomain >& domain ); - /** increment the iterator */ - void increment2( int counter ); - void increment(); - /** is the iterator finished? */ - bool isFinished(); - /** produce the match that this iterator represents */ - void getMatch( QuantifiersEngine* qe, InstMatch& m ); - /** get the i_th term we are considering */ - Node getTerm( int i ); - /** get the number of terms we are considering */ - int getNumTerms() { return d_f[0].getNumChildren(); } - /** debug print */ - void debugPrint( const char* c ); - void debugPrintSmall( const char* c ); -}; - -class RepSetEvaluator -{ -private: - FirstOrderModel* d_model; - RepSetIterator* d_riter; -private: //for Theory UF: - //map from terms to the models used to calculate their value - std::map< Node, bool > d_eval_uf_use_default; - std::map< Node, uf::UfModelTree > d_eval_uf_model; - void makeEvalUfModel( Node n ); - //index ordering to use for each term - std::map< Node, std::vector< int > > d_eval_term_index_order; - int getMaxVariableNum( int n ); - void makeEvalUfIndexOrder( Node n ); -private: - //default evaluate term function - Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ); - //temporary storing which literals have failed - void clearEvalFailed( int index ); - std::map< Node, bool > d_eval_failed; - std::map< int, std::vector< Node > > d_eval_failed_lits; -public: - RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ); - virtual ~RepSetEvaluator(){} - /** evaluate functions */ - int evaluate( Node n, int& depIndex ); - Node evaluateTerm( Node n, int& depIndex ); -public: - //statistics - int d_eval_formulas; - int d_eval_uf_terms; - int d_eval_lits; - int d_eval_lits_unknown; -}; - - -} -} -} - -#endif +/********************* */ +/*! \file rep_set_iterator.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief rep_set_iterator class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__REP_SET_ITERATOR_H +#define __CVC4__REP_SET_ITERATOR_H + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/first_order_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** this class iterates over a RepSet */ +class RepSetIterator { +public: + RepSetIterator( Node f, FirstOrderModel* model ); + ~RepSetIterator(){} + //pointer to quantifier + Node d_f; + //pointer to model + FirstOrderModel* d_model; + //index we are considering + std::vector< int > d_index; + //domain we are considering + std::vector< RepDomain > d_domain; + //ordering for variables we are indexing over + // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 }, + // then we consider instantiations in this order: + // a/x a/y a/z + // a/x b/y a/z + // b/x a/y a/z + // b/x b/y a/z + // ... + std::vector< int > d_index_order; + //variables to index they are considered at + // for example, if d_index_order = { 2, 0, 1 } + // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 } + std::map< int, int > d_var_order; + //the instantiation constants of d_f + std::vector< Node > d_ic; + //the current terms we are considering + std::vector< Node > d_terms; +public: + /** set index order */ + void setIndexOrder( std::vector< int >& indexOrder ); + /** set domain */ + void setDomain( std::vector< RepDomain >& domain ); + /** increment the iterator */ + void increment2( int counter ); + void increment(); + /** is the iterator finished? */ + bool isFinished(); + /** produce the match that this iterator represents */ + void getMatch( QuantifiersEngine* qe, InstMatch& m ); + /** get the i_th term we are considering */ + Node getTerm( int i ); + /** get the number of terms we are considering */ + int getNumTerms() { return d_f[0].getNumChildren(); } + /** debug print */ + void debugPrint( const char* c ); + void debugPrintSmall( const char* c ); +}; + +class RepSetEvaluator +{ +private: + FirstOrderModel* d_model; + RepSetIterator* d_riter; +private: //for Theory UF: + //map from terms to the models used to calculate their value + std::map< Node, bool > d_eval_uf_use_default; + std::map< Node, uf::UfModelTree > d_eval_uf_model; + void makeEvalUfModel( Node n ); + //index ordering to use for each term + std::map< Node, std::vector< int > > d_eval_term_index_order; + int getMaxVariableNum( int n ); + void makeEvalUfIndexOrder( Node n ); +private: + //default evaluate term function + Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ); + //temporary storing which literals have failed + void clearEvalFailed( int index ); + std::map< Node, bool > d_eval_failed; + std::map< int, std::vector< Node > > d_eval_failed_lits; +public: + RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ); + virtual ~RepSetEvaluator(){} + /** evaluate functions */ + int evaluate( Node n, int& depIndex ); + Node evaluateTerm( Node n, int& depIndex ); +public: + //statistics + int d_eval_formulas; + int d_eval_uf_terms; + int d_eval_lits; + int d_eval_lits_unknown; +}; + + +} +} +} + +#endif diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 1ebba49b5..2af6992f7 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -1,156 +1,156 @@ -/**********************/ -/*! \file term_database.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief term database class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__QUANTIFIERS_TERM_DATABASE_H -#define __CVC4__QUANTIFIERS_TERM_DATABASE_H - -#include "theory/theory.h" - -#include - -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 & 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 & vars, - const std::vector & nvars); - /** get free variable for instantiation constant */ - Node getFreeVariableForInstConstant( Node n ); -};/* class TermDb */ - -} -} -} - -#endif +/**********************/ +/*! \file term_database.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief term database class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_TERM_DATABASE_H +#define __CVC4__QUANTIFIERS_TERM_DATABASE_H + +#include "theory/theory.h" + +#include + +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 & 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 & vars, + const std::vector & nvars); + /** get free variable for instantiation constant */ + Node getFreeVariableForInstConstant( Node n ); +};/* class TermDb */ + +} +} +} + +#endif diff --git a/src/theory/rr_inst_match.cpp b/src/theory/rr_inst_match.cpp index 287f7475a..21a309610 100644 --- a/src/theory/rr_inst_match.cpp +++ b/src/theory/rr_inst_match.cpp @@ -958,7 +958,7 @@ Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){ arithmetic pattern */ std::map< Node, Node > d_arith_coeffs; if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){ - std::cout << "(?) Unknown matching pattern is " << pat << std::endl; + Message() << "(?) Unknown matching pattern is " << pat << std::endl; Unimplemented("pattern not implemented"); return new DumbMatcher(); }else{ @@ -1010,7 +1010,7 @@ PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){ std::map< Node, Node > d_arith_coeffs; if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){ Debug("inst-match-gen") << "(?) Unknown matching pattern is " << pat << std::endl; - std::cout << "(?) Unknown matching pattern is " << pat << std::endl; + Message() << "(?) Unknown matching pattern is " << pat << std::endl; return new DumbPatMatcher(); }else{ Debug("matching-arith") << "Generated arithmetic pattern for " << pat << ": " << std::endl; diff --git a/src/theory/rr_trigger.cpp b/src/theory/rr_trigger.cpp index 52e7efcc2..ece68d137 100644 --- a/src/theory/rr_trigger.cpp +++ b/src/theory/rr_trigger.cpp @@ -75,156 +75,156 @@ d_quantEngine( qe ), d_f( f ){ }else{ ++(qe->d_statistics.d_simple_triggers); } - }else{ + }else{ Debug("multi-trigger") << "Multi-trigger " << (*this) << std::endl; //std::cout << "Multi-trigger for " << f << " : " << std::endl; //std::cout << " " << (*this) << std::endl; ++(qe->d_statistics.d_multi_triggers); } -} -void Trigger::computeVarContains( Node n ) { - if( d_var_contains.find( n )==d_var_contains.end() ){ - d_var_contains[n].clear(); - computeVarContains2( n, n ); - } -} - -void Trigger::computeVarContains2( Node n, Node parent ){ - if( n.getKind()==INST_CONSTANT ){ - if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){ - d_var_contains[parent].push_back( n ); - } - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - computeVarContains2( n[i], parent ); - } - } } - -void Trigger::resetInstantiationRound(){ - d_mg->resetInstantiationRound( d_quantEngine ); -} - +void Trigger::computeVarContains( Node n ) { + if( d_var_contains.find( n )==d_var_contains.end() ){ + d_var_contains[n].clear(); + computeVarContains2( n, n ); + } +} + +void Trigger::computeVarContains2( Node n, Node parent ){ + if( n.getKind()==INST_CONSTANT ){ + if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){ + d_var_contains[parent].push_back( n ); + } + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + computeVarContains2( n[i], parent ); + } + } +} + +void Trigger::resetInstantiationRound(){ + d_mg->resetInstantiationRound( d_quantEngine ); +} -bool Trigger::getNextMatch(){ - bool retVal = d_mg->getNextMatch( d_quantEngine ); - //m.makeInternal( d_quantEngine->getEqualityQuery() ); - return retVal; -} + +bool Trigger::getNextMatch(){ + bool retVal = d_mg->getNextMatch( d_quantEngine ); + //m.makeInternal( d_quantEngine->getEqualityQuery() ); + return retVal; +} // bool Trigger::getMatch( Node t, InstMatch& m ){ // //FIXME: this assumes d_mg is an inst match generator // return ((InstMatchGenerator*)d_mg)->getMatch( t, m, d_quantEngine ); // } - -int Trigger::addInstantiations( InstMatch& baseMatch ){ + +int Trigger::addInstantiations( InstMatch& baseMatch ){ int addedLemmas = d_mg->addInstantiations( baseMatch, d_nodes[0].getAttribute(InstConstantAttribute()), - d_quantEngine); - if( addedLemmas>0 ){ + d_quantEngine); + if( addedLemmas>0 ){ Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was "; for( int i=0; i<(int)d_nodes.size(); i++ ){ Debug("inst-trigger") << d_nodes[i] << " "; } - Debug("inst-trigger") << std::endl; - } - return addedLemmas; -} - -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption, - bool smartTriggers ){ - std::vector< Node > trNodes; - if( !keepAll ){ - //only take nodes that contribute variables to the trigger when added - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::map< Node, bool > vars; - std::map< Node, std::vector< Node > > patterns; - for( int i=0; i<(int)temp.size(); i++ ){ - bool foundVar = false; - computeVarContains( temp[i] ); - for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){ - Node v = d_var_contains[ temp[i] ][j]; - if( v.getAttribute(InstConstantAttribute())==f ){ - if( vars.find( v )==vars.end() ){ - vars[ v ] = true; - foundVar = true; - } - } - } - if( foundVar ){ - trNodes.push_back( temp[i] ); - for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){ - Node v = d_var_contains[ temp[i] ][j]; - patterns[ v ].push_back( temp[i] ); - } - } - } - //now, minimalize the trigger - for( int i=0; i<(int)trNodes.size(); i++ ){ - bool keepPattern = false; - Node n = trNodes[i]; - for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){ - Node v = d_var_contains[ n ][j]; - if( patterns[v].size()==1 ){ - keepPattern = true; - break; - } - } - if( !keepPattern ){ - //remove from pattern vector - for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){ - Node v = d_var_contains[ n ][j]; - for( int k=0; k<(int)patterns[v].size(); k++ ){ - if( patterns[v][k]==n ){ - patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); - break; - } - } - } - //remove from trigger nodes - trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 ); - i--; - } - } - }else{ - trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() ); - } - - //check for duplicate? - if( trOption==TR_MAKE_NEW ){ - //static int trNew = 0; - //static int trOld = 0; - //Trigger* t = d_tr_trie.getTrigger( trNodes ); - //if( t ){ - // trOld++; - //}else{ - // trNew++; - //} - //if( (trNew+trOld)%100==0 ){ - // std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl; - //} - }else{ - Trigger* t = d_tr_trie.getTrigger( trNodes ); - if( t ){ - if( trOption==TR_GET_OLD ){ - //just return old trigger - return t; - }else{ - return NULL; - } - } - } - Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers ); - d_tr_trie.addTrigger( trNodes, t ); - return t; -} -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){ - std::vector< Node > nodes; - nodes.push_back( n ); - return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers ); -} + Debug("inst-trigger") << std::endl; + } + return addedLemmas; +} + +Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption, + bool smartTriggers ){ + std::vector< Node > trNodes; + if( !keepAll ){ + //only take nodes that contribute variables to the trigger when added + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::map< Node, bool > vars; + std::map< Node, std::vector< Node > > patterns; + for( int i=0; i<(int)temp.size(); i++ ){ + bool foundVar = false; + computeVarContains( temp[i] ); + for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){ + Node v = d_var_contains[ temp[i] ][j]; + if( v.getAttribute(InstConstantAttribute())==f ){ + if( vars.find( v )==vars.end() ){ + vars[ v ] = true; + foundVar = true; + } + } + } + if( foundVar ){ + trNodes.push_back( temp[i] ); + for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){ + Node v = d_var_contains[ temp[i] ][j]; + patterns[ v ].push_back( temp[i] ); + } + } + } + //now, minimalize the trigger + for( int i=0; i<(int)trNodes.size(); i++ ){ + bool keepPattern = false; + Node n = trNodes[i]; + for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){ + Node v = d_var_contains[ n ][j]; + if( patterns[v].size()==1 ){ + keepPattern = true; + break; + } + } + if( !keepPattern ){ + //remove from pattern vector + for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){ + Node v = d_var_contains[ n ][j]; + for( int k=0; k<(int)patterns[v].size(); k++ ){ + if( patterns[v][k]==n ){ + patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); + break; + } + } + } + //remove from trigger nodes + trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 ); + i--; + } + } + }else{ + trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() ); + } + + //check for duplicate? + if( trOption==TR_MAKE_NEW ){ + //static int trNew = 0; + //static int trOld = 0; + //Trigger* t = d_tr_trie.getTrigger( trNodes ); + //if( t ){ + // trOld++; + //}else{ + // trNew++; + //} + //if( (trNew+trOld)%100==0 ){ + // std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl; + //} + }else{ + Trigger* t = d_tr_trie.getTrigger( trNodes ); + if( t ){ + if( trOption==TR_GET_OLD ){ + //just return old trigger + return t; + }else{ + return NULL; + } + } + } + Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers ); + d_tr_trie.addTrigger( trNodes, t ); + return t; +} +Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){ + std::vector< Node > nodes; + nodes.push_back( n ); + return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers ); +} bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ for( int i=0; i<(int)nodes.size(); i++ ){ @@ -233,25 +233,25 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ } } return true; -} - -bool Trigger::isUsable( Node n, Node f ){ - if( n.getAttribute(InstConstantAttribute())==f ){ - if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){ - std::map< Node, Node > coeffs; - return getPatternArithmetic( f, n, coeffs ); - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( !isUsable( n[i], f ) ){ - return false; - } - } - return true; - } - }else{ - return true; - } -} +} + +bool Trigger::isUsable( Node n, Node f ){ + if( n.getAttribute(InstConstantAttribute())==f ){ + if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){ + std::map< Node, Node > coeffs; + return getPatternArithmetic( f, n, coeffs ); + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( !isUsable( n[i], f ) ){ + return false; + } + } + return true; + } + }else{ + return true; + } +} bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ @@ -293,67 +293,67 @@ void Trigger::filterInstances( std::vector< Node >& nodes ){ } -bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){ - if( patMap.find( n )==patMap.end() ){ - patMap[ n ] = false; - if( tstrt==TS_MIN_TRIGGER ){ - if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ); - return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ); -#else - return false; -#endif - }else{ - bool retVal = false; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ - retVal = true; - } - } - if( retVal ){ - return true; - }else if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; - return true; - }else{ - return false; - } - } - }else{ - bool retVal = false; - if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; - if( tstrt==TS_MAX_TRIGGER ){ - return true; - }else{ - retVal = true; - } - } - if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){ - // retVal = true; - //} - if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){ - retVal = true; - } -#endif - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ - retVal = true; - } - } - } - return retVal; - } - }else{ - return patMap[ n ]; - } +bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){ + if( patMap.find( n )==patMap.end() ){ + patMap[ n ] = false; + if( tstrt==TS_MIN_TRIGGER ){ + if( n.getKind()==FORALL ){ +#ifdef NESTED_PATTERN_SELECTION + //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ); + return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ); +#else + return false; +#endif + }else{ + bool retVal = false; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + retVal = true; + } + } + if( retVal ){ + return true; + }else if( isUsableTrigger( n, f ) ){ + patMap[ n ] = true; + return true; + }else{ + return false; + } + } + }else{ + bool retVal = false; + if( isUsableTrigger( n, f ) ){ + patMap[ n ] = true; + if( tstrt==TS_MAX_TRIGGER ){ + return true; + }else{ + retVal = true; + } + } + if( n.getKind()==FORALL ){ +#ifdef NESTED_PATTERN_SELECTION + //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){ + // retVal = true; + //} + if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){ + retVal = true; + } +#endif + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + retVal = true; + } + } + } + return retVal; + } + }else{ + return patMap[ n ]; + } } -void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){ +void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){ std::map< Node, bool > patMap; if( filterInst ){ //immediately do not consider any term t for which another term is an instance of t @@ -387,10 +387,10 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } collectPatTerms2( qe, f, n, patMap, tstrt ); - for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ - if( it->second ){ - patTerms.push_back( it->first ); - } + for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ + if( it->second ){ + patTerms.push_back( it->first ); + } } } @@ -469,15 +469,15 @@ void Trigger::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, } } } - -void Trigger::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){ - computeVarContains( n ); - for( int j=0; j<(int)d_var_contains[n].size(); j++ ){ - if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){ - varContains.push_back( d_var_contains[n][j] ); - } - } -} + +void Trigger::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){ + computeVarContains( n ); + for( int j=0; j<(int)d_var_contains[n].size(); j++ ){ + if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){ + varContains.push_back( d_var_contains[n][j] ); + } + } +} bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){ if( n.getKind()==PLUS ){ diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index f68ab1429..0082f4840 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -1,421 +1,421 @@ -/********************* */ -/*! \file theory_uf_model.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of Theory UF Model - **/ - -#include "theory/quantifiers/model_engine.h" -#include "theory/theory_engine.h" -#include "theory/uf/equality_engine.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/theory_uf_strong_solver.h" -#include "theory/uf/theory_uf_instantiator.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database.h" - -#define RECONSIDER_FUNC_DEFAULT_VALUE -#define USE_PARTIAL_DEFAULT_VALUES - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; - -//clear -void UfModelTreeNode::clear(){ - d_data.clear(); - d_value = Node::null(); -} - -bool UfModelTreeNode::hasConcreteArgumentDefinition(){ - if( d_data.size()>1 ){ - return true; - }else if( d_data.empty() ){ - return false; - }else{ - Node r; - return d_data.find( r )==d_data.end(); - } -} - -//set value function -void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){ - if( d_data.empty() ){ - d_value = v; - }else if( !d_value.isNull() && d_value!=v ){ - d_value = Node::null(); - } - if( argIndex<(int)indexOrder.size() ){ - //take r = null when argument is the model basis - Node r; - if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){ - r = m->getRepresentative( n[ indexOrder[argIndex] ] ); - } - d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 ); - } -} - -//get value function -Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){ - if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){ - //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl; - depIndex = argIndex; - return d_value; - }else{ - Node val; - int childDepIndex[2] = { argIndex, argIndex }; - for( int i=0; i<2; i++ ){ - //first check the argument, then check default - Node r; - if( i==0 ){ - r = m->getRepresentative( n[ indexOrder[argIndex] ] ); - } - std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); - if( it!=d_data.end() ){ - val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 ); - if( !val.isNull() ){ - break; - } - }else{ - //argument is not a defined argument: thus, it depends on this argument - childDepIndex[i] = argIndex+1; - } - } - //update depIndex - depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1]; - //Notice() << "Return " << val << ", depIndex = " << depIndex; - //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl; - return val; - } -} - -Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){ - if( argIndex==(int)indexOrder.size() ){ - return d_value; - }else{ - Node val; - bool depArg = false; - //will try concrete value first, then default - for( int i=0; i<2; i++ ){ - Node r; - if( i==0 ){ - r = m->getRepresentative( n[ indexOrder[argIndex] ] ); - } - std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); - if( it!=d_data.end() ){ - val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 ); - //we have found a value - if( !val.isNull() ){ - if( i==0 ){ - depArg = true; - } - break; - } - } - } - //it depends on this argument if we found it via concrete argument value, - // or if found by default/disequal from some concrete argument value(s). - if( depArg || hasConcreteArgumentDefinition() ){ - if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){ - depIndex.push_back( indexOrder[argIndex] ); - } - } - return val; - } -} - -Node UfModelTreeNode::getFunctionValue(){ - if( !d_data.empty() ){ - Node defaultValue; - std::vector< Node > caseValues; - for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ - if( it->first.isNull() ){ - defaultValue = it->second.getFunctionValue(); - }else{ - caseValues.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE, it->first, it->second.getFunctionValue() ) ); - } - } - if( caseValues.empty() && defaultValue.getKind()!=FUNCTION_CASE_SPLIT && defaultValue.getKind()!=FUNCTION_MODEL ){ - return defaultValue; - }else{ - std::vector< Node > children; - if( !caseValues.empty() ){ - children.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE_SPLIT, caseValues ) ); - } - if( !defaultValue.isNull() ){ - children.push_back( defaultValue ); - } - return NodeManager::currentNM()->mkNode( FUNCTION_MODEL, children ); - } - }else{ - Assert( !d_value.isNull() ); - return d_value; - } -} - -//simplify function -void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){ - if( argIndex<(int)op.getType().getNumChildren()-1 ){ - std::vector< Node > eraseData; - //first process the default argument - Node r; - std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); - if( it!=d_data.end() ){ - if( !defaultVal.isNull() && it->second.d_value==defaultVal ){ - eraseData.push_back( r ); - }else{ - it->second.simplify( op, defaultVal, argIndex+1 ); - if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){ - defaultVal = it->second.d_value; - }else{ - defaultVal = Node::null(); - if( it->second.isEmpty() ){ - eraseData.push_back( r ); - } - } - } - } - //now see if any children can be removed, and simplify the ones that cannot - for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ - if( !it->first.isNull() ){ - if( !defaultVal.isNull() && it->second.d_value==defaultVal ){ - eraseData.push_back( it->first ); - }else{ - it->second.simplify( op, defaultVal, argIndex+1 ); - if( it->second.isEmpty() ){ - eraseData.push_back( it->first ); - } - } - } - } - for( int i=0; i<(int)eraseData.size(); i++ ){ - d_data.erase( eraseData[i] ); - } - } -} - -//is total function -bool UfModelTreeNode::isTotal( Node op, int argIndex ){ - if( argIndex==(int)(op.getType().getNumChildren()-1) ){ - return !d_value.isNull(); - }else{ - Node r; - std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); - if( it!=d_data.end() ){ - return it->second.isTotal( op, argIndex+1 ); - }else{ - return false; - } - } -} - -Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){ - return d_value; -} - -void indent( std::ostream& out, int ind ){ - for( int i=0; i& 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::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; iprintRepresentativeDebug( "fmf-model-cons", v ); - Debug("fmf-model-cons") << " ) = " << score << std::endl; - if( score>maxScore ){ - defaultVal = v; - maxScore = score; - } - } -#ifdef RECONSIDER_FUNC_DEFAULT_VALUE - if( maxScore<1.0 ){ - //consider finding another value, if possible - Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl; - TypeNode tn = defaultTerm.getType(); - Node newDefaultVal = m->getDomainValue( tn, d_values ); - if( !newDefaultVal.isNull() ){ - defaultVal = newDefaultVal; - Debug("fmf-model-cons-debug") << "-> Change default value to "; - m->printRepresentativeDebug( "fmf-model-cons-debug", defaultVal ); - Debug("fmf-model-cons-debug") << std::endl; - }else{ - Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl; - Debug("fmf-model-cons-debug") << " Excluding: "; - for( int i=0; i<(int)d_values.size(); i++ ){ - Debug("fmf-model-cons-debug") << d_values[i] << " "; - } - Debug("fmf-model-cons-debug") << std::endl; - } - } -#endif - //get the default term (this term must be defined non-ground in model) - Debug("fmf-model-cons") << " Choose "; - m->printRepresentativeDebug("fmf-model-cons", defaultVal ); - Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl; - Debug("fmf-model-cons") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl; - Debug("fmf-model-cons") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl; - return defaultVal; +/********************* */ +/*! \file theory_uf_model.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of Theory UF Model + **/ + +#include "theory/quantifiers/model_engine.h" +#include "theory/theory_engine.h" +#include "theory/uf/equality_engine.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/theory_uf_strong_solver.h" +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" + +#define RECONSIDER_FUNC_DEFAULT_VALUE +#define USE_PARTIAL_DEFAULT_VALUES + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; + +//clear +void UfModelTreeNode::clear(){ + d_data.clear(); + d_value = Node::null(); +} + +bool UfModelTreeNode::hasConcreteArgumentDefinition(){ + if( d_data.size()>1 ){ + return true; + }else if( d_data.empty() ){ + return false; + }else{ + Node r; + return d_data.find( r )==d_data.end(); + } +} + +//set value function +void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){ + if( d_data.empty() ){ + d_value = v; + }else if( !d_value.isNull() && d_value!=v ){ + d_value = Node::null(); + } + if( argIndex<(int)indexOrder.size() ){ + //take r = null when argument is the model basis + Node r; + if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){ + r = m->getRepresentative( n[ indexOrder[argIndex] ] ); + } + d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 ); + } +} + +//get value function +Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){ + if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){ + //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl; + depIndex = argIndex; + return d_value; + }else{ + Node val; + int childDepIndex[2] = { argIndex, argIndex }; + for( int i=0; i<2; i++ ){ + //first check the argument, then check default + Node r; + if( i==0 ){ + r = m->getRepresentative( n[ indexOrder[argIndex] ] ); + } + std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); + if( it!=d_data.end() ){ + val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 ); + if( !val.isNull() ){ + break; + } + }else{ + //argument is not a defined argument: thus, it depends on this argument + childDepIndex[i] = argIndex+1; + } + } + //update depIndex + depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1]; + //Notice() << "Return " << val << ", depIndex = " << depIndex; + //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl; + return val; + } +} + +Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){ + if( argIndex==(int)indexOrder.size() ){ + return d_value; + }else{ + Node val; + bool depArg = false; + //will try concrete value first, then default + for( int i=0; i<2; i++ ){ + Node r; + if( i==0 ){ + r = m->getRepresentative( n[ indexOrder[argIndex] ] ); + } + std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); + if( it!=d_data.end() ){ + val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 ); + //we have found a value + if( !val.isNull() ){ + if( i==0 ){ + depArg = true; + } + break; + } + } + } + //it depends on this argument if we found it via concrete argument value, + // or if found by default/disequal from some concrete argument value(s). + if( depArg || hasConcreteArgumentDefinition() ){ + if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){ + depIndex.push_back( indexOrder[argIndex] ); + } + } + return val; + } +} + +Node UfModelTreeNode::getFunctionValue(){ + if( !d_data.empty() ){ + Node defaultValue; + std::vector< Node > caseValues; + for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ + if( it->first.isNull() ){ + defaultValue = it->second.getFunctionValue(); + }else{ + caseValues.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE, it->first, it->second.getFunctionValue() ) ); + } + } + if( caseValues.empty() && defaultValue.getKind()!=FUNCTION_CASE_SPLIT && defaultValue.getKind()!=FUNCTION_MODEL ){ + return defaultValue; + }else{ + std::vector< Node > children; + if( !caseValues.empty() ){ + children.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE_SPLIT, caseValues ) ); + } + if( !defaultValue.isNull() ){ + children.push_back( defaultValue ); + } + return NodeManager::currentNM()->mkNode( FUNCTION_MODEL, children ); + } + }else{ + Assert( !d_value.isNull() ); + return d_value; + } +} + +//simplify function +void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){ + if( argIndex<(int)op.getType().getNumChildren()-1 ){ + std::vector< Node > eraseData; + //first process the default argument + Node r; + std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); + if( it!=d_data.end() ){ + if( !defaultVal.isNull() && it->second.d_value==defaultVal ){ + eraseData.push_back( r ); + }else{ + it->second.simplify( op, defaultVal, argIndex+1 ); + if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){ + defaultVal = it->second.d_value; + }else{ + defaultVal = Node::null(); + if( it->second.isEmpty() ){ + eraseData.push_back( r ); + } + } + } + } + //now see if any children can be removed, and simplify the ones that cannot + for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ + if( !it->first.isNull() ){ + if( !defaultVal.isNull() && it->second.d_value==defaultVal ){ + eraseData.push_back( it->first ); + }else{ + it->second.simplify( op, defaultVal, argIndex+1 ); + if( it->second.isEmpty() ){ + eraseData.push_back( it->first ); + } + } + } + } + for( int i=0; i<(int)eraseData.size(); i++ ){ + d_data.erase( eraseData[i] ); + } + } +} + +//is total function +bool UfModelTreeNode::isTotal( Node op, int argIndex ){ + if( argIndex==(int)(op.getType().getNumChildren()-1) ){ + return !d_value.isNull(); + }else{ + Node r; + std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); + if( it!=d_data.end() ){ + return it->second.isTotal( op, argIndex+1 ); + }else{ + return false; + } + } +} + +Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){ + return d_value; +} + +void indent( std::ostream& out, int ind ){ + for( int i=0; i& 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::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; iprintRepresentativeDebug( "fmf-model-cons", v ); + Debug("fmf-model-cons") << " ) = " << score << std::endl; + if( score>maxScore ){ + defaultVal = v; + maxScore = score; + } + } +#ifdef RECONSIDER_FUNC_DEFAULT_VALUE + if( maxScore<1.0 ){ + //consider finding another value, if possible + Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl; + TypeNode tn = defaultTerm.getType(); + Node newDefaultVal = m->getDomainValue( tn, d_values ); + if( !newDefaultVal.isNull() ){ + defaultVal = newDefaultVal; + Debug("fmf-model-cons-debug") << "-> Change default value to "; + m->printRepresentativeDebug( "fmf-model-cons-debug", defaultVal ); + Debug("fmf-model-cons-debug") << std::endl; + }else{ + Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl; + Debug("fmf-model-cons-debug") << " Excluding: "; + for( int i=0; i<(int)d_values.size(); i++ ){ + Debug("fmf-model-cons-debug") << d_values[i] << " "; + } + Debug("fmf-model-cons-debug") << std::endl; + } + } +#endif + //get the default term (this term must be defined non-ground in model) + Debug("fmf-model-cons") << " Choose "; + m->printRepresentativeDebug("fmf-model-cons", defaultVal ); + Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl; + Debug("fmf-model-cons") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl; + Debug("fmf-model-cons") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl; + return defaultVal; } \ No newline at end of file diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 47b149867..9dba16608 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -1,199 +1,199 @@ -/********************* */ -/*! \file theory_uf_model.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Model for Theory UF - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY_UF_MODEL_H -#define __CVC4__THEORY_UF_MODEL_H - -#include "theory/model.h" - -namespace CVC4 { -namespace theory { -namespace uf { - -class UfModelTreeNode -{ -public: - UfModelTreeNode(){} - /** the data */ - std::map< Node, UfModelTreeNode > d_data; - /** the value of this tree node (if all paths lead to same value) */ - Node d_value; - /** has concrete argument defintion */ - bool hasConcreteArgumentDefinition(); -public: - //is this model tree empty? - bool isEmpty() { return d_data.empty() && d_value.isNull(); } - //clear - void clear(); - /** setValue function */ - void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ); - /** getValue function */ - Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ); - Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ); - /** getConstant Value function */ - Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ); - /** getFunctionValue */ - Node getFunctionValue(); - /** simplify function */ - void simplify( Node op, Node defaultVal, int argIndex ); - /** is total ? */ - bool isTotal( Node op, int argIndex ); -public: - void debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind = 0, int arg = 0 ); -}; - -class UfModelTree -{ -private: - //the op this model is for - Node d_op; - //the order we will treat the arguments - std::vector< int > d_index_order; - //the data - UfModelTreeNode d_tree; -public: - //constructors - UfModelTree(){} - UfModelTree( Node op ) : d_op( op ){ - TypeNode tn = d_op.getType(); - for( int i=0; i<(int)(tn.getNumChildren()-1); i++ ){ - d_index_order.push_back( i ); - } - } - UfModelTree( Node op, std::vector< int >& indexOrder ) : d_op( op ){ - d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() ); - } - /** clear/reset the function */ - void clear() { d_tree.clear(); } - /** setValue function - * - * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false - * - */ - void setValue( TheoryModel* m, Node n, Node v, bool ground = true ){ - d_tree.setValue( m, n, v, d_index_order, ground, 0 ); - } - /** setDefaultValue function */ - void setDefaultValue( TheoryModel* m, Node v ){ - d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 ); - } - /** getValue function - * - * returns val, the value of ground term n - * Say n is f( t_0...t_n ) - * depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to val - * for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c, - * then g( a, a, a ) would return b with depIndex = 1 - * - */ - Node getValue( TheoryModel* m, Node n, int& depIndex ){ - return d_tree.getValue( m, n, d_index_order, depIndex, 0 ); - } - /** -> implementation incomplete */ - Node getValue( TheoryModel* m, Node n, std::vector< int >& depIndex ){ - return d_tree.getValue( m, n, d_index_order, depIndex, 0 ); - } - /** getConstantValue function - * - * given term n, where n may contain "all value" arguments, aka model basis arguments - * if n is null, then every argument of n is considered "all value" - * if n is constant for the entire domain specified by n, then this function returns the value of its domain - * otherwise, it returns null - * for example, say the term e represents "all values" - * if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b, - * then f( a, e ) would return b, while f( e, a ) would return null - * -> implementation incomplete - */ - Node getConstantValue( TheoryModel* m, Node n ) { - return d_tree.getConstantValue( m, n, d_index_order, 0 ); - } - /** getFunctionValue - * Returns a compact representation of this function, of kind FUNCTION_MODEL. - * See documentation in theory/uf/kinds - */ - Node getFunctionValue(){ - return d_tree.getFunctionValue(); - } - /** simplify the tree */ - void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); } - /** is this tree total? */ - bool isTotal() { return d_tree.isTotal( d_op, 0 ); } - /** is this function constant? */ - bool isConstant( TheoryModel* m ) { return !getConstantValue( m, Node::null() ).isNull(); } - /** is this tree empty? */ - bool isEmpty() { return d_tree.isEmpty(); } -public: - void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){ - d_tree.debugPrint( out, m, d_index_order, ind ); - } -private: - //helper for to ITE function. - static Node toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ); -public: - /** to ITE function for function model nodes */ - static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); } -}; - -class UfModelTreeGenerator -{ -private: - //store for set values - Node d_default_value; - std::map< Node, Node > d_set_values[2][2]; - // defaults - std::vector< Node > d_defaults; - Node getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ); -public: - UfModelTreeGenerator(){} - ~UfModelTreeGenerator(){} - /** set default value */ - void setDefaultValue( Node v ) { d_default_value = v; } - /** set value */ - void setValue( TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true ); - /** make model */ - void makeModel( TheoryModel* m, UfModelTree& tree ); - /** uses partial default values */ - bool optUsePartialDefaults(); - /** reset */ - void clear(); -}; - -//this class stores temporary information useful to model engine for constructing model -class UfModelPreferenceData -{ -public: - UfModelPreferenceData() : d_reconsiderModel( false ){} - virtual ~UfModelPreferenceData(){} - Node d_const_val; - // preferences for default values - std::vector< Node > d_values; - std::map< Node, std::vector< Node > > d_value_pro_con[2]; - std::map< Node, std::vector< Node > > d_term_pro_con[2]; - bool d_reconsiderModel; - /** set value preference */ - void setValuePreference( Node f, Node n, Node r, bool isPro ); - /** get best default value */ - Node getBestDefaultValue( Node defaultTerm, TheoryModel* m ); -}; - - -} -} -} - -#endif +/********************* */ +/*! \file theory_uf_model.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Model for Theory UF + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_UF_MODEL_H +#define __CVC4__THEORY_UF_MODEL_H + +#include "theory/model.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +class UfModelTreeNode +{ +public: + UfModelTreeNode(){} + /** the data */ + std::map< Node, UfModelTreeNode > d_data; + /** the value of this tree node (if all paths lead to same value) */ + Node d_value; + /** has concrete argument defintion */ + bool hasConcreteArgumentDefinition(); +public: + //is this model tree empty? + bool isEmpty() { return d_data.empty() && d_value.isNull(); } + //clear + void clear(); + /** setValue function */ + void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ); + /** getValue function */ + Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ); + Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ); + /** getConstant Value function */ + Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ); + /** getFunctionValue */ + Node getFunctionValue(); + /** simplify function */ + void simplify( Node op, Node defaultVal, int argIndex ); + /** is total ? */ + bool isTotal( Node op, int argIndex ); +public: + void debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind = 0, int arg = 0 ); +}; + +class UfModelTree +{ +private: + //the op this model is for + Node d_op; + //the order we will treat the arguments + std::vector< int > d_index_order; + //the data + UfModelTreeNode d_tree; +public: + //constructors + UfModelTree(){} + UfModelTree( Node op ) : d_op( op ){ + TypeNode tn = d_op.getType(); + for( int i=0; i<(int)(tn.getNumChildren()-1); i++ ){ + d_index_order.push_back( i ); + } + } + UfModelTree( Node op, std::vector< int >& indexOrder ) : d_op( op ){ + d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() ); + } + /** clear/reset the function */ + void clear() { d_tree.clear(); } + /** setValue function + * + * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false + * + */ + void setValue( TheoryModel* m, Node n, Node v, bool ground = true ){ + d_tree.setValue( m, n, v, d_index_order, ground, 0 ); + } + /** setDefaultValue function */ + void setDefaultValue( TheoryModel* m, Node v ){ + d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 ); + } + /** getValue function + * + * returns val, the value of ground term n + * Say n is f( t_0...t_n ) + * depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to val + * for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c, + * then g( a, a, a ) would return b with depIndex = 1 + * + */ + Node getValue( TheoryModel* m, Node n, int& depIndex ){ + return d_tree.getValue( m, n, d_index_order, depIndex, 0 ); + } + /** -> implementation incomplete */ + Node getValue( TheoryModel* m, Node n, std::vector< int >& depIndex ){ + return d_tree.getValue( m, n, d_index_order, depIndex, 0 ); + } + /** getConstantValue function + * + * given term n, where n may contain "all value" arguments, aka model basis arguments + * if n is null, then every argument of n is considered "all value" + * if n is constant for the entire domain specified by n, then this function returns the value of its domain + * otherwise, it returns null + * for example, say the term e represents "all values" + * if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b, + * then f( a, e ) would return b, while f( e, a ) would return null + * -> implementation incomplete + */ + Node getConstantValue( TheoryModel* m, Node n ) { + return d_tree.getConstantValue( m, n, d_index_order, 0 ); + } + /** getFunctionValue + * Returns a compact representation of this function, of kind FUNCTION_MODEL. + * See documentation in theory/uf/kinds + */ + Node getFunctionValue(){ + return d_tree.getFunctionValue(); + } + /** simplify the tree */ + void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); } + /** is this tree total? */ + bool isTotal() { return d_tree.isTotal( d_op, 0 ); } + /** is this function constant? */ + bool isConstant( TheoryModel* m ) { return !getConstantValue( m, Node::null() ).isNull(); } + /** is this tree empty? */ + bool isEmpty() { return d_tree.isEmpty(); } +public: + void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){ + d_tree.debugPrint( out, m, d_index_order, ind ); + } +private: + //helper for to ITE function. + static Node toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ); +public: + /** to ITE function for function model nodes */ + static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); } +}; + +class UfModelTreeGenerator +{ +private: + //store for set values + Node d_default_value; + std::map< Node, Node > d_set_values[2][2]; + // defaults + std::vector< Node > d_defaults; + Node getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ); +public: + UfModelTreeGenerator(){} + ~UfModelTreeGenerator(){} + /** set default value */ + void setDefaultValue( Node v ) { d_default_value = v; } + /** set value */ + void setValue( TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true ); + /** make model */ + void makeModel( TheoryModel* m, UfModelTree& tree ); + /** uses partial default values */ + bool optUsePartialDefaults(); + /** reset */ + void clear(); +}; + +//this class stores temporary information useful to model engine for constructing model +class UfModelPreferenceData +{ +public: + UfModelPreferenceData() : d_reconsiderModel( false ){} + virtual ~UfModelPreferenceData(){} + Node d_const_val; + // preferences for default values + std::vector< Node > d_values; + std::map< Node, std::vector< Node > > d_value_pro_con[2]; + std::map< Node, std::vector< Node > > d_term_pro_con[2]; + bool d_reconsiderModel; + /** set value preference */ + void setValuePreference( Node f, Node n, Node r, bool isPro ); + /** get best default value */ + Node getBestDefaultValue( Node defaultTerm, TheoryModel* m ); +}; + + +} +} +} + +#endif diff --git a/src/util/model.cpp b/src/util/model.cpp index 081624c5d..50683fdff 100644 --- a/src/util/model.cpp +++ b/src/util/model.cpp @@ -1,15 +1,15 @@ -/********************* */ -/*! \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 +/********************* */ +/*! \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 diff --git a/src/util/model.h b/src/util/model.h index 7e0f5a723..60f1ab23f 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -1,42 +1,42 @@ -/********************* */ -/*! \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 - -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 */ +/********************* */ +/*! \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 + +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 */ diff --git a/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 b/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 index a4ce611fb..6acf4a3c6 100644 --- a/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 +++ b/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 @@ -1,6 +1,6 @@ (set-logic AUFLIRA) -(set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods. - +(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") diff --git a/test/regress/regress0/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress0/quantifiers/symmetric_unsat_7.smt2 index a4ce611fb..6acf4a3c6 100644 --- a/test/regress/regress0/quantifiers/symmetric_unsat_7.smt2 +++ b/test/regress/regress0/quantifiers/symmetric_unsat_7.smt2 @@ -1,6 +1,6 @@ (set-logic AUFLIRA) -(set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods. - +(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") -- 2.30.2