From: Andrew Reynolds Date: Fri, 27 Jul 2012 19:27:45 +0000 (+0000) Subject: merging fmf-devel branch, includes refactored datatype theory, updates to model.h... X-Git-Tag: cvc5-1.0.0~7909 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9a994c449d65e64d574a423ad9caad519f8c2148;p=cvc5.git merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 56fa93a94..93d596264 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -384,6 +384,7 @@ extendedCommand[CVC4::Command*& cmd] : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); } { /* open a scope to keep the UnresolvedTypes contained */ PARSER_STATE->pushScope(); } + LPAREN_TOK RPAREN_TOK //TODO: parametric datatypes LPAREN_TOK ( LPAREN_TOK datatypeDef[dts] RPAREN_TOK )+ RPAREN_TOK { PARSER_STATE->popScope(); cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } @@ -569,7 +570,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Expr f, f2; std::string attr; Expr attexpr; - std::vector attexprs; + std::vector patexprs; std::hash_set names; std::vector< std::pair > binders; } @@ -714,8 +715,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] /* attributed expressions */ | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2] ( attribute[expr, attexpr,attr] - { if(! attexpr.isNull()) { - attexprs.push_back(attexpr); + { if( attr == ":pattern" && ! attexpr.isNull()) { + patexprs.push_back( attexpr ); + }else if( attr==":axiom" ){ + //do this? } } )+ RPAREN_TOK @@ -745,10 +748,15 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] else PARSER_STATE->parseError("Error parsing rewrite rule."); expr = MK_EXPR( kind, args ); - } else if(! attexprs.empty()) { - if(attexprs[0].getKind() == kind::INST_PATTERN) { - expr2 = MK_EXPR(kind::INST_PATTERN_LIST, attexprs); + } else if(! patexprs.empty()) { + if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){ + for( size_t i=0; igetEqualityEngine()->areEqual( a, b ); }else{ - return a==b; + return false; } } bool InstantiatorTheoryArrays::areDisequal( Node a, Node b ){ - if( hasTerm( a ) && hasTerm( b ) ){ + if( a==b ){ + return false; + }else if( hasTerm( a ) && hasTerm( b ) ){ return ((TheoryArrays*)d_th)->getEqualityEngine()->areDisequal( a, b, false ); }else{ return false; @@ -84,6 +88,23 @@ Node InstantiatorTheoryArrays::getRepresentative( Node a ){ } } +eq::EqualityEngine* InstantiatorTheoryArrays::getEqualityEngine(){ + return ((TheoryArrays*)d_th)->getEqualityEngine(); +} + +void InstantiatorTheoryArrays::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ + if( hasTerm( a ) ){ + a = getEqualityEngine()->getRepresentative( a ); + eq::EqClassIterator eqc_iter( a, getEqualityEngine() ); + while( !eqc_iter.isFinished() ){ + if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){ + eqc.push_back( *eqc_iter ); + } + eqc_iter++; + } + } +} + rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClasses(){ arrays::TheoryArrays* ar = static_cast(getTheory()); eq::EqualityEngine* ee = diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h index f711229b2..23899afc1 100644 --- a/src/theory/arrays/theory_arrays_instantiator.h +++ b/src/theory/arrays/theory_arrays_instantiator.h @@ -49,6 +49,8 @@ public: bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); Node getRepresentative( Node a ); + eq::EqualityEngine* getEqualityEngine(); + void getEquivalenceClass( Node a, std::vector< Node >& eqc ); /** general creators of candidate generators */ rrinst::CandidateGenerator* getRRCanGenClasses(); rrinst::CandidateGenerator* getRRCanGenClass(); diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp new file mode 100644 index 000000000..49da2f851 --- /dev/null +++ b/src/theory/arrays/theory_arrays_model.cpp @@ -0,0 +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; +} diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h new file mode 100644 index 000000000..3895388e3 --- /dev/null +++ b/src/theory/arrays/theory_arrays_model.h @@ -0,0 +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 */ + +} +} +} + +#endif \ No newline at end of file diff --git a/src/theory/candidate_generator.cpp b/src/theory/candidate_generator.cpp new file mode 100644 index 000000000..ffecaa8da --- /dev/null +++ b/src/theory/candidate_generator.cpp @@ -0,0 +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(); +} diff --git a/src/theory/candidate_generator.h b/src/theory/candidate_generator.h new file mode 100644 index 000000000..2152f1ef6 --- /dev/null +++ b/src/theory/candidate_generator.h @@ -0,0 +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 */ diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am index f282ce74d..0e6197ac1 100644 --- a/src/theory/datatypes/Makefile.am +++ b/src/theory/datatypes/Makefile.am @@ -16,7 +16,6 @@ libdatatypes_la_SOURCES = \ explanation_manager.h \ explanation_manager.cpp \ theory_datatypes_instantiator.h \ - theory_datatypes_instantiator.cpp \ - theory_datatypes_candidate_generator.h - + theory_datatypes_instantiator.cpp + EXTRA_DIST = kinds diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index ea1409108..5bae534e1 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -74,7 +74,8 @@ public: << "Rewrite trivial selector " << in << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); - } else { + } + /* Node gt = in.getType().mkGroundTerm(); TypeNode gtt = gt.getType(); //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); @@ -87,7 +88,7 @@ public: << " to distinguished ground term " << in.getType().mkGroundTerm() << std::endl; return RewriteResponse(REWRITE_DONE,gt ); - } + */ } if(in.getKind() == kind::EQUAL && in[0] == in[1]) { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index cb0f75c12..b7f4f39d5 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -34,993 +34,682 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::datatypes; -const DatatypeConstructor& TheoryDatatypes::getConstructor( Node cons ) -{ - Expr consExpr = cons.toExpr(); - return Datatype::datatypeOf(consExpr)[ Datatype::indexOf(consExpr) ]; -} - -Node TheoryDatatypes::getConstructorForSelector( Node sel ) -{ - size_t selIndex = Datatype::indexOf( sel.toExpr() ); - const Datatype& dt = ((DatatypeType)((sel.getType()[0]).toType())).getDatatype(); - for( unsigned i = 0; iselIndex && - Node::fromExpr( dt[i][selIndex].getSelector() )==sel ){ - return Node::fromExpr( dt[i].getConstructor() ); +void TheoryDatatypes::printModelDebug(){ + /* + //std::cout << "Datatypes model : " << std::endl; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + if( eqc.getType().isDatatype() || eqc.getType().isBoolean() ){ + //std::cout << eqc << " : " << eqc.getType() << " : " << std::endl; + //std::cout << " { "; + //add terms to model + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + //std::cout << (*eqc_i) << " "; + ++eqc_i; + } + //std::cout << "}" << std::endl; + if( eqc.getType().isDatatype() ){ + EqcInfo* ei = getOrMakeEqcInfo( eqc ); + if( ei ){ + //std::cout << " Instantiated : " << ( ei->d_inst ? "yes" : "no" ) << std::endl; + if( ei->d_constructor.get().isNull() ){ + //std::cout << " Constructor : " << std::endl; + //std::cout << " Labels : "; + if( hasLabel( ei, eqc ) ){ + //std::cout << getLabel( eqc ); + }else{ + NodeListMap::iterator lbl_i = d_labels.find( eqc ); + if( lbl_i != d_labels.end() ){ + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){ + //std::cout << *j << " "; + } + } + } + //std::cout << std::endl; + }else{ + //std::cout << " Constructor : " << ei->d_constructor.get() << std::endl; + } + //std::cout << " Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl; + } + } } + ++eqcs_i; } - Assert( false ); - return Node::null(); + */ } TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, qe), - d_currAsserts(c), - d_currEqualities(c), - d_selectors(c), - d_reps(c), - d_selector_eq(c), - d_equivalence_class(c), - d_inst_map(c), d_cycle_check(c), d_hasSeenCycle(c, false), - d_labels(c), - d_ccChannel(this), - d_cc(c, &d_ccChannel), - d_unionFind(c), - d_disequalities(c), - d_em(c), - d_cce(&d_cc){ + d_infer(c), + d_infer_exp(c), + d_notify( *this ), + d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"), + d_labels( c ), + d_conflict( c, false ){ + + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); + d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); } - TheoryDatatypes::~TheoryDatatypes() { } -void TheoryDatatypes::addSharedTerm(TNode t) { - Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): " - << t << endl; +TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake ){ + std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); + if( !hasEqcInfo( n ) ){ + if( doMake ){ + //add to labels + NodeList* lbl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator(getSatContext()->getCMM()) ); + d_labels.insertDataFromContextMemory( n, lbl ); + EqcInfo* ei; + if( eqc_i!=d_eqc_info.end() ){ + ei = eqc_i->second; + }else{ + ei = new EqcInfo( getSatContext() ); + d_eqc_info[n] = ei; + } + if( n.getKind()==APPLY_CONSTRUCTOR ){ + ei->d_constructor = n; + } + return ei; + }else{ + return NULL; + } + }else{ + return (*eqc_i).second; + } } -void TheoryDatatypes::notifyCongruent(TNode lhs, TNode rhs) { - Debug("datatypes") << "TheoryDatatypes::notifyCongruent(): " - << lhs << " = " << rhs << endl; - if(!hasConflict()) { - merge(lhs,rhs); - } - Debug("datatypes-debug") << "TheoryDatatypes::notifyCongruent(): done." << endl; +/** propagate */ +void TheoryDatatypes::propagate(Effort effort){ + } -void TheoryDatatypes::preRegisterTerm(TNode n) { - Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl; - if( n.getType().isDatatype() ){ - d_preRegTerms.push_back( n ); +/** propagate */ +bool TheoryDatatypes::propagate(TNode literal){ + Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal << ")" << std::endl; + // If already in conflict, no more propagation + if (d_conflict) { + Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal << "): already in conflict" << std::endl; + return false; } + // Propagate out + bool ok = d_out->propagate(literal); + if (!ok) { + d_conflict = true; + } + return ok; } - -void TheoryDatatypes::presolve() { - Debug("datatypes") << "TheoryDatatypes::presolve()" << endl; +/** explain */ +void TheoryDatatypes::explain(TNode literal, std::vector& assumptions){ + Debug("datatypes-explain") << "Explain " << literal << std::endl; + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + } else { + d_equalityEngine.explainPredicate(atom, polarity, assumptions); + } } -void TheoryDatatypes::check(Effort e) { +Node TheoryDatatypes::explain( TNode literal ){ + std::vector< TNode > assumptions; + explain( literal, assumptions ); + if( assumptions.empty() ){ + return NodeManager::currentNM()->mkConst( true ); + }else if( assumptions.size()==1 ){ + return assumptions[0]; + }else{ + return NodeManager::currentNM()->mkNode( kind::AND, assumptions ); + } +} - for( int i=0; i<(int)d_currAsserts.size(); i++ ) { - Debug("datatypes") << "currAsserts[" << i << "] = " << d_currAsserts[i] << endl; +/** Conflict when merging two constants */ +void TheoryDatatypes::conflict(TNode a, TNode b){ + if (a.getKind() == kind::CONST_BOOLEAN) { + d_conflictNode = explain( a.iffNode(b) ); + } else { + d_conflictNode = explain( a.eqNode(b) ); } - for( int i=0; i<(int)d_currEqualities.size(); i++ ) { - Debug("datatypes") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl; + Debug("datatypes-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; +} + +/** called when a new equivalance class is created */ +void TheoryDatatypes::eqNotifyNewClass(TNode t){ + if( t.getKind()==APPLY_CONSTRUCTOR ){ + getOrMakeEqcInfo( t, true ); } +} - while(!done()) { - Node assertion = get(); - if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") - || Debug.isOn("datatypes-debug-pf") || Debug.isOn("datatypes-conflict") ) { - Notice() << "*** TheoryDatatypes::check(): " << assertion << endl; - d_currAsserts.push_back( assertion ); - } +/** called when two equivalance classes will merge */ +void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){ - //clear from the derived map - d_checkMap.clear(); - collectTerms( assertion ); - if( !hasConflict() ){ - if( d_em.hasNode( assertion ) ){ - Debug("datatypes") << "Assertion has already been derived" << endl; - d_em.assertTrue( assertion ); - } else { - switch(assertion.getKind()) { - case kind::EQUAL: - case kind::IFF: - addEquality(assertion); - break; - case kind::APPLY_TESTER: - addTester( assertion ); - break; - case kind::NOT: - { - switch( assertion[0].getKind()) { - case kind::EQUAL: - case kind::IFF: - { - Node a = assertion[0][0]; - Node b = assertion[0][1]; - addDisequality(assertion[0]); - d_cc.addTerm(a); - d_cc.addTerm(b); - if(Debug.isOn("datatypes")) { - Debug("datatypes") << " a == > " << a << endl - << " b == > " << b << endl - << " find(a) == > " << debugFind(a) << endl - << " find(b) == > " << debugFind(b) << endl; - } - // There are two ways to get a conflict here. - if(!hasConflict()) { - if(find(a) == find(b)) { - // We get a conflict this way if we WERE previously watching - // a, b and were notified previously (via notifyCongruent()) - // that they were congruent. - Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, assertion[0][0], assertion[0][1] ); - NodeBuilder<> nbc(kind::AND); - nbc << ccEq << assertion; - Node contra = nbc; - d_em.addNode( ccEq, &d_cce ); - d_em.addNodeConflict( contra, Reason::contradiction ); - } else { - // If we get this far, there should be nothing conflicting due - // to this disequality. - Assert(!d_cc.areCongruent(a, b)); - } - } - } - break; - case kind::APPLY_TESTER: - addTester( assertion ); - break; - default: - Unhandled(assertion[0].getKind()); - break; +} + +/** called when two equivalance classes have merged */ +void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){ + if( t1.getType().isDatatype() ){ + d_pending_merge.push_back( t1.eqNode( t2 ) ); + } +} + +void TheoryDatatypes::merge( Node t1, Node t2 ){ + if( !d_conflict ){ + Node trep1 = t1; + Node trep2 = t2; + Debug("datatypes-debug") << "Merge " << t1 << " " << t2 << std::endl; + EqcInfo* eqc2 = getOrMakeEqcInfo( t2 ); + if( eqc2 ){ + bool checkInst = false; + if( !eqc2->d_constructor.get().isNull() ){ + trep2 = eqc2->d_constructor.get(); + } + EqcInfo* eqc1 = getOrMakeEqcInfo( t1 ); + if( eqc1 ){ + if( !eqc1->d_constructor.get().isNull() ){ + trep1 = eqc1->d_constructor.get(); + } + //check for clash + Node cons1 = eqc1->d_constructor; + Node cons2 = eqc2->d_constructor; + if( !cons1.isNull() && !cons2.isNull() ){ + Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl; + if( cons1.getOperator()!=cons2.getOperator() ){ + //check for clash + d_conflictNode = explain( cons1.eqNode( cons2 ) ); + Debug("datatypes-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; + return; + }else{ + //do unification + Node unifEq = cons1.eqNode( cons2 ); + for( int i=0; i<(int)cons1.getNumChildren(); i++ ) { + Node eq = cons1[i].eqNode( cons2[i] ); + d_pending.push_back( eq ); + d_pending_exp[ eq ] = unifEq; + Debug("datatypes-infer") << "DtInfer : " << eq << " by " << unifEq << std::endl; + d_infer.push_back( eq ); + d_infer_exp.push_back( unifEq ); } } - break; - default: - Unhandled(assertion.getKind()); - break; } - } - } - //rules to check for collapse, instantiate - while( !hasConflict() && !d_checkMap.empty() ){ - std::map< Node, bool > temp; - temp = d_checkMap; - d_checkMap.clear(); - std::map< Node, bool >::iterator i; - for( i = temp.begin(); i != temp.end(); i++ ){ - Node n = find( i->first ); - if( temp.find( n )==temp.end() || temp[n] ){ - if( !hasConflict() ) checkInstantiateEqClass( n ); - if( !hasConflict() ) updateSelectors( n ); - temp[n] = false; + if( eqc1->d_inst.get().isNull() && !eqc2->d_inst.get().isNull() ){ + eqc1->d_inst.set( eqc2->d_inst ); } + if( cons1.isNull() && !cons2.isNull() ){ + checkInst = true; + eqc1->d_constructor.set( eqc2->d_constructor ); + } + }else{ + Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl; + //just copy the equivalence class information + eqc1 = getOrMakeEqcInfo( t1, true ); + eqc1->d_inst.set( eqc2->d_inst ); + eqc1->d_constructor.set( eqc2->d_constructor ); } - } - //if there is now a conflict - if( hasConflict() ) { - Debug("datatypes-conflict") << "Constructing conflict..." << endl; - for( int i=0; i<(int)d_currAsserts.size(); i++ ) { - Debug("datatypes-conflict") << "currAsserts[" << i << "] = " << d_currAsserts[i] << endl; - } - //Debug("datatypes-conflict") << d_cc << std::endl; - Node conflict = d_em.getConflict(); - if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || - Debug.isOn("datatypes-cycles") || Debug.isOn("datatypes-conflict") ){ - Notice() << "Conflict constructed : " << conflict << endl; - } - if( conflict.getKind()!=kind::AND ){ - conflict = NodeManager::currentNM()->mkNode(kind::AND, conflict, conflict); - } - d_out->conflict(conflict); - return; - } - } - - if( e == EFFORT_FULL ) { - Debug("datatypes-split") << "Check for splits " << e << endl; - //do splitting - for( EqLists::iterator i = d_labels.begin(); i != d_labels.end(); i++ ) { - Node sf = find( (*i).first ); - if( sf.getKind() != APPLY_CONSTRUCTOR ) { - addTermToLabels( sf ); - EqList* lbl = (sf == (*i).first) ? (*i).second : (*d_labels.find( sf )).second; - Debug("datatypes-split") << "Check for splitting " << (*i).first - << ", label size = " << lbl->size() << endl; - if( lbl->empty() || (*lbl)[ lbl->size()-1 ].getKind() == NOT ) { //there are more than 1 possible constructors for sf - const Datatype& dt = ((DatatypeType)(sf.getType()).toType()).getDatatype(); - vector< bool > possibleCons; - possibleCons.resize( dt.getNumConstructors(), true ); - for( EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) { - TNode leqn = (*j); - possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false; - } - Node cons; - bool foundSel = false; - for( unsigned int j=0; jmkNode( APPLY_SELECTOR, Node::fromExpr( dt[j][k].getSelector() ), sf ); - if( d_selectors.find( s ) != d_selectors.end() ) { - foundSel = true; - break; - } - } - } - } - if( !foundSel ){ - for( unsigned int j=0; jmkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), (*i).first ); - NodeBuilder<> nb(kind::OR); - nb << test << test.notNode(); - Node lemma = nb; - Debug("datatypes-split") << "Lemma is " << lemma << endl; - d_out->lemma( lemma ); + //merge labels + Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl; + NodeListMap::iterator lbl_i = d_labels.find( t2 ); + if( lbl_i != d_labels.end() ){ + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){ + addTester( *j, eqc1, t1 ); + if( d_conflict ){ return; } } - } else { - Debug("datatypes-split") << (*i).first << " is " << sf << endl; - Assert( sf != (*i).first ); } - } - } - if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) { - Notice() << "TheoryDatatypes::check(): done" << endl; - } -} - -bool TheoryDatatypes::checkTester( Node assertion, Node& conflict, unsigned& r ){ - Debug("datatypes") << "Check tester " << assertion << endl; - - Node tassertion = ( assertion.getKind() == NOT ) ? assertion[0] : assertion; - Assert( find( tassertion[0] ) == tassertion[0] ); - - //if argument is a constructor, it is trivial - if( tassertion[0].getKind() == APPLY_CONSTRUCTOR ) { - size_t tIndex = Datatype::indexOf(tassertion.getOperator().toExpr()); - size_t cIndex = Datatype::indexOf(tassertion[0].getOperator().toExpr()); - if( (tIndex==cIndex) == (assertion.getKind() == NOT) ) { - conflict = assertion; - r = Reason::idt_tclash; - } - return false; - } - - addTermToLabels( tassertion[0] ); - EqList* lbl = (*d_labels.find( tassertion[0] )).second; - //check if empty label (no possible constructors for term) - for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - Node leqn = (*i); - Debug("datatypes-debug") << "checking " << leqn << std::endl; - if( leqn.getKind() == kind::NOT ) { - if( leqn[0].getOperator() == tassertion.getOperator() ) { - if( assertion.getKind() != NOT ) { - conflict = NodeManager::currentNM()->mkNode( AND, leqn, assertion ); - r = Reason::contradiction; - Debug("datatypes") << "Contradictory labels " << conflict << endl; + //merge selectors + if( !eqc1->d_selectors && eqc2->d_selectors ){ + eqc1->d_selectors = true; + checkInst = true; + } + if( checkInst ){ + checkInstantiate( eqc1, t1 ); + if( d_conflict ){ + return; } - return false; } - }else{ - if( (leqn.getOperator() == tassertion.getOperator()) == (assertion.getKind() == NOT) ) { - conflict = NodeManager::currentNM()->mkNode( AND, leqn, assertion ); - r = Reason::idt_tclash; - Debug("datatypes") << "Contradictory labels(2) " << conflict << endl; + } + //add this to the transitive closure module + Node oldRep = trep2; + Node newRep = trep1; + if( trep1.getKind()!=APPLY_CONSTRUCTOR && trep2.getKind()==APPLY_CONSTRUCTOR ){ + oldRep = trep1; + newRep = trep2; + } + bool result = d_cycle_check.addEdgeNode( oldRep, newRep ); + d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); + Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << d_hasSeenCycle.get() << endl; + if( d_hasSeenCycle.get() ){ + checkCycles(); + if( d_conflict ){ + return; } - return false; } } - return true; } -void TheoryDatatypes::addTester( Node assertion ){ - Debug("datatypes") << "addTester " << assertion << endl; +/** called when two equivalence classes are made disequal */ +void TheoryDatatypes::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){ - //preprocess the tester - Node tassertion = ( assertion.getKind() == NOT ) ? assertion[0] : assertion; - //add the term into congruence closure consideration - d_cc.addTerm( tassertion[0] ); +} - Node assertionRep; - Node tassertionRep; - Node tRep = tassertion[0]; - tRep = find( tRep ); - //add label instead for the representative (if it is different) - if( tRep != tassertion[0] ) { - //explanation is trivial (do not add to labels) - if( tRep.getKind()==APPLY_CONSTRUCTOR && assertion.getKind()== kind::APPLY_TESTER && - Datatype::indexOf(assertion.getOperator().toExpr())==Datatype::indexOf(tRep.getOperator().toExpr()) ){ - tassertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, tassertion.getOperator(), tRep ); - assertionRep = tassertionRep; - d_em.addNodeAxiom( assertionRep, Reason::idt_taxiom ); - return; - }else{ - tassertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, tassertion.getOperator(), tRep ); - assertionRep = ( assertion.getKind() == NOT ) ? tassertionRep.notNode() : tassertionRep; - //add explanation - Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, tRep, tassertion[0] ); - d_em.addNode( ccEq, &d_cce ); - NodeBuilder<> nb2(kind::AND); - nb2 << assertion << ccEq; - Node expl = nb2; - d_em.addNode( assertionRep, expl, Reason::idt_tcong ); - } - }else{ - tassertionRep = tassertion; - assertionRep = assertion; - } +TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c ) : +d_inst( c, Node::null() ), d_constructor( c, Node::null() ), d_selectors( c, false ){ - Node conflict; - unsigned r; - if( checkTester( assertionRep, conflict, r ) ){ - //it is not redundant/contradictory, add it to labels - EqLists::iterator lbl_i = d_labels.find( tRep ); - EqList* lbl = (*lbl_i).second; - lbl->push_back( assertionRep ); - Debug("datatypes") << "Add to labels " << assertionRep << endl; - if( assertionRep.getKind()==NOT ){ - const Datatype& dt = Datatype::datatypeOf( tassertion.getOperator().toExpr() ); - //we can conclude the final one - if( lbl->size()==dt.getNumConstructors()-1 ){ - vector< bool > possibleCons; - possibleCons.resize( dt.getNumConstructors(), true ); - NodeBuilder<> nb(kind::AND); - for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - possibleCons[ Datatype::indexOf( (*i)[0].getOperator().toExpr() ) ] = false; - nb << (*i); - } - int testerIndex = -1; - for( int i=0; i<(int)possibleCons.size(); i++ ) { - if( possibleCons[i] ){ - testerIndex = i; - } - } - Assert( testerIndex!=-1 ); - assertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(testerIndex)].getTester() ), tRep ); - Node exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; - d_em.addNode( assertionRep, exp, Reason::idt_texhaust ); - addTester( assertionRep ); //add stronger statement - return; - } - } - if( assertionRep.getKind()==APPLY_TESTER ){ - d_checkMap[ tRep ] = true; - } - }else if( !conflict.isNull() ){ - d_em.addNodeConflict( conflict, r ); - } } -//if only one constructor remaining for t, this function will return it -Node TheoryDatatypes::getInstantiateCons( Node t ){ - if( t.getKind() != APPLY_CONSTRUCTOR ){ - Assert( t == find( t ) ); - addTermToLabels( t ); - EqLists::iterator lbl_i = d_labels.find( t ); - if( lbl_i!=d_labels.end() ) { - EqList* lbl = (*lbl_i).second; - if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind() != NOT ) { - const Datatype& dt = ((DatatypeType)(t.getType()).toType()).getDatatype(); - size_t testerIndex = Datatype::indexOf( (*lbl)[ lbl->size()-1 ].getOperator().toExpr() ); - return Node::fromExpr( dt[ testerIndex ].getConstructor() ); - } +bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){ + return !eqc->d_constructor.get().isNull() || !getLabel( n ).isNull(); +} + +Node TheoryDatatypes::getLabel( Node n ) { + NodeListMap::iterator lbl_i = d_labels.find( n ); + if( lbl_i != d_labels.end() ){ + NodeList* lbl = (*lbl_i).second; + if( !(*lbl).empty() && (*lbl)[ (*lbl).size() - 1 ].getKind()==kind::APPLY_TESTER ){ + return (*lbl)[ (*lbl).size() - 1 ]; } } return Node::null(); } -void TheoryDatatypes::checkInstantiateEqClass( Node t ) { - Debug("datatypes") << "TheoryDatatypes::checkInstantiateEqClass() " << t << endl; - Assert( t == find( t ) ); - - //if labels were created for t, and t has not been instantiated - Node cons = getInstantiateCons( t ); - if( !cons.isNull() ){ - //for each term in equivalance class - initializeEqClass( t ); - EqListN* eqc = (*d_equivalence_class.find( t )).second; - for( EqListN::const_iterator iter = eqc->begin(); iter != eqc->end(); iter++ ) { - Node te = *iter; - Assert( find( te ) == t ); - if( checkInstantiate( te, cons ) ){ - return; - } - } +int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){ + if( !eqc->d_constructor.get().isNull() ){ + return Datatype::indexOf( eqc->d_constructor.get().getOperator().toExpr() ); + }else{ + return Datatype::indexOf( getLabel( n ).getOperator().toExpr() ); } } -//pre condition: find( te ) has been proven to be the constructor cons -//that is, is_[cons]( find( te ) ) is stored in d_labels -bool TheoryDatatypes::checkInstantiate( Node te, Node cons ) -{ - Debug("datatypes") << "TheoryDatatypes::checkInstantiate() " << te << endl; - //if term has not yet been instantiated - if( d_inst_map.find( te ) == d_inst_map.end() ) { - //find if selectors have been applied to t - vector< Node > selectorVals; - selectorVals.push_back( cons ); - bool foundSel = false; - const DatatypeConstructor& cn = getConstructor( cons ); - for( unsigned int i=0; imkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te ); - if( d_selectors.find( s ) != d_selectors.end() ) { - foundSel = true; - s = find( s ); - } - selectorVals.push_back( s ); - } - if( cn.isFinite() || foundSel ) { - d_inst_map[ te ] = true; - Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals ); - //instantiate, add equality - if( val.getType()!=te.getType() ){ //IDT-param - Assert( Datatype::datatypeOf( cons.toExpr() ).isParametric() ); - Debug("datatypes-gt") << "Inst: ambiguous type for " << cons << ", ascribe to " << te.getType() << std::endl; - const DatatypeConstructor& dtc = Datatype::datatypeOf(cons.toExpr())[Datatype::indexOf(cons.toExpr())]; - Debug("datatypes-gt") << "constructor is " << dtc << std::endl; - Type tspec = dtc.getSpecializedConstructorType(te.getType().toType()); - Debug("datatypes-gt") << "tpec is " << tspec << std::endl; - selectorVals[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(tspec)), cons); - val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals ); - } - if( find( val ) != find( te ) ) { - //build explaination - NodeBuilder<> nb(kind::AND); - //explanation for tester - Node t = find( te ); - addTermToLabels( t ); - Assert( d_labels.find( t )!=d_labels.end() ); - EqList* lbl = (*d_labels.find( t )).second; - nb << (*lbl)[ lbl->size()-1 ]; //this should be changed to be tester for te, not t for fine-grained - //explanation for arguments - for( unsigned int i=0; imkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te ); - if( selectorVals[i+1]!=s ){ - Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, selectorVals[i+1], s ); - d_em.addNode( ccEq, &d_cce ); - nb << ccEq; - }else{ - //reflexive for s, if we want idt_inst to be fined grained - //Node eq = NodeManager::currentNM()->mkNode( EQUAL, s, s ); - //d_em.addNodeAxiom( s, Reason::refl ); - } - } - Node jeq = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; - Node newEq = NodeManager::currentNM()->mkNode( EQUAL, val, te ); - Debug("datatypes") << "Instantiate: " << newEq << "." << endl; - d_em.addNode( newEq, jeq, Reason::idt_inst_coarse ); - //collect terms of instantiation term - collectTerms( val, false ); - //add equality for the instantiation - addEquality( newEq ); - return true; +void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& pcons ){ + const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); + pcons.resize( dt.getNumConstructors(), !hasLabel( eqc, n ) ); + if( hasLabel( eqc, n ) ){ + pcons[ getLabelIndex( eqc, n ) ] = true; + }else{ + NodeListMap::iterator lbl_i = d_labels.find( n ); + if( lbl_i != d_labels.end() ){ + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + Assert( (*i).getKind()==NOT ); + pcons[ Datatype::indexOf( (*i)[0].getOperator().toExpr() ) ] = false; } - } else { - Debug("datatypes") << "Do not Instantiate: infinite constructor, no selectors " << cons << endl; } - }else{ - Debug("datatypes") << "Do not Instantiate: " << te << " already instantiated" << endl; } - return false; } -bool TheoryDatatypes::collapseSelector( Node t ) { - if( !hasConflict() && t.getKind() == APPLY_SELECTOR ) { - //collapse constructor - TypeNode retTyp = t.getType(); - TypeNode typ = t[0].getType(); - Node sel = t.getOperator(); - TypeNode selType = sel.getType(); - Node cons = getConstructorForSelector( sel ); - const DatatypeConstructor& cn = getConstructor( cons ); - Node tmp = find( t[0] ); - Node retNode = t; - if( tmp.getKind() == APPLY_CONSTRUCTOR ) { - if( tmp.getOperator() == cons ) { - Debug("datatypes") << "Applied selector " << t << " to correct constructor." << endl; - retNode = tmp[ Datatype::indexOf( sel.toExpr() ) ]; - } else { - Debug("datatypes") << "Applied selector " << t << " to wrong constructor." << endl; - retNode = retTyp.mkGroundTerm(); //IDT-param +void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ + if( !d_conflict ){ + Debug("datatypes-labels") << "Add tester " << t << " " << eqc << std::endl; + bool tpolarity = t.getKind()!=NOT; + Node tt = ( t.getKind() == NOT ) ? t[0] : t; + int ttindex = Datatype::indexOf( tt.getOperator().toExpr() ); + Node j, jt; + if( hasLabel( eqc, n ) ){ + int jtindex = getLabelIndex( eqc, n ); + if( (jtindex==ttindex)!=tpolarity ){ + d_conflict = true; + if( !eqc->d_constructor.get().isNull() ){ + std::vector< TNode > assumptions; + explain( t, assumptions ); + explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions ); + d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); + Debug("datatypes-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + return; + }else{ + j = getLabel( n ); + jt = j; + } + }else{ + return; } - if( tmp!=t[0] ){ - t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, t.getOperator(), tmp ); + }else{ + NodeListMap::iterator lbl_i = d_labels.find( n ); + Assert( lbl_i != d_labels.end() ); + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + Assert( (*i).getKind()==NOT ); + j = *i; + jt = j[0]; + int jtindex = Datatype::indexOf( jt.getOperator().toExpr() ); + if( jtindex==ttindex ){ + if( tpolarity ){ //we are in conflict + d_conflict = true; + break; + }else{ //it is redundant + return; + } + } } - Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t ); - d_em.addNodeAxiom( neq, Reason::idt_collapse ); - Debug("datatypes") << "Add collapse equality " << neq << endl; - addEquality( neq ); - return true; - } else { - //see whether we can prove that the selector is applied to the wrong tester - Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), tmp ); - Node conflict; - unsigned r; - checkTester( tester, conflict, r ); - if( !conflict.isNull() ) { - Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor. " << retTyp << endl; - //conflict is c ^ tester, where conflict => false, but we want to say c => ~tester - //must remove tester from conflict - if( conflict.getKind()==kind::AND ){ - NodeBuilder<> jt(kind::AND); - for( int i=0; i<(int)conflict.getNumChildren(); i++ ){ - if( conflict[i]!=tester ){ - jt << conflict[i]; + if( !d_conflict ){ + Debug("datatypes-labels") << "Add to labels " << t << std::endl; + lbl->push_back( t ); + const Datatype& dt = ((DatatypeType)(tt[0].getType()).toType()).getDatatype(); + Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << dt.getNumConstructors() << std::endl; + if( tpolarity ){ + checkInstantiate( eqc, n ); + }else{ + //check if we have reached the maximum number of testers + // in this case, add the positive tester + if( lbl->size()==dt.getNumConstructors()-1 ){ + std::vector< bool > pcons; + getPossibleCons( eqc, n, pcons ); + int testerIndex = -1; + for( int i=0; i<(int)pcons.size(); i++ ) { + if( pcons[i] ){ + testerIndex = i; + break; + } } + Assert( testerIndex!=-1 ); + std::vector< Node > eq_terms; + NodeBuilder<> nb(kind::AND); + for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + nb << (*i); + if( std::find( eq_terms.begin(), eq_terms.end(), (*i)[0][0] )==eq_terms.end() ){ + eq_terms.push_back( (*i)[0][0] ); + if( (*i)[0][0]!=tt[0] ){ + nb << (*i)[0][0].eqNode( tt[0] ); + } + } + } + Node t_concl = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(testerIndex)].getTester() ), tt[0] ); + Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; + d_pending.push_back( t_concl ); + d_pending_exp[ t_concl ] = t_concl_exp; + Debug("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl; + d_infer.push_back( t_concl ); + d_infer_exp.push_back( t_concl_exp ); + return; } - conflict = ( jt.getNumChildren()==1 ) ? jt.getChild( 0 ) : jt; - }else{ - Assert( conflict==tester ); - conflict = Node::null(); - } - if( conflict!=tester.notNode() ){ - d_em.addNode( tester.notNode(), conflict, r ); //note that application of r is non-standard (TODO: fix) } - - if( tmp != t[0] ) { - Node teq = NodeManager::currentNM()->mkNode( EQUAL, tmp, t[0] ); - d_em.addNode( teq, &d_cce ); - Node exp = NodeManager::currentNM()->mkNode( AND, tester.notNode(), teq ); - tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), t[0] ); - d_em.addNode( tester.notNode(), exp, Reason::idt_tcong ); - } - retNode = retTyp.mkGroundTerm(); //IDT-param - Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t ); - - d_em.addNode( neq, tester.notNode(), Reason::idt_collapse2 ); - addEquality( neq ); - return true; } } - } - return false; -} - -//this function will test if each selector whose argument is in the equivalence class of "a" can be collapsed -void TheoryDatatypes::updateSelectors( Node a ) { - Debug("datatypes") << "updateSelectors: " << a << endl; - EqListsN::iterator sel_a_i = d_selector_eq.find( a ); - if( sel_a_i != d_selector_eq.end() ) { - EqListN* sel_a = (*sel_a_i).second; - for( EqListN::const_iterator i = sel_a->begin(); i != sel_a->end(); i++ ) { - Node s = (*i); - //if a is still a representative, and s has not yet been collapsed - if( find( a )==a && !d_selectors[s] ){ - Assert( s.getKind()==APPLY_SELECTOR && find( s[0] ) == a ); - if( a != s[0] ) { - s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, s.getOperator(), a ); - collectTerms( s, false ); - } - d_selectors[s] = collapseSelector( s ); - } + if( d_conflict ){ + std::vector< TNode > assumptions; + explain( j, assumptions ); + explain( t, assumptions ); + explain( jt[0].eqNode( tt[0] ), assumptions ); + d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); + Debug("datatypes-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); } } } -void TheoryDatatypes::collectModelInfo( TheoryModel* m ){ - //temporary - for( int i=0; i<(int)d_preRegTerms.size(); i++ ){ - Node n = find( d_preRegTerms[i] ); - m->assertEquality( n, d_preRegTerms[i], true ); - } -} -void TheoryDatatypes::merge(TNode a, TNode b) { - if( !d_merge_pending.empty() ) { - //Debug("datatypes") << "Append to merge pending list " << d_merge_pending.size() << endl; - d_merge_pending[d_merge_pending.size()-1].push_back( pair< Node, Node >( a, b ) ); - return; - } - Assert(!hasConflict()); - a = find(a); - b = find(b); - if( a == b) { - return; - } - Debug("datatypes") << "Merge "<< a << " " << b << endl; - - // make "a" the one with shorter diseqList - EqLists::iterator deq_ia = d_disequalities.find(a); - EqLists::iterator deq_ib = d_disequalities.find(b); +void TheoryDatatypes::check(Effort e) { - if(deq_ia != d_disequalities.end()) { - if(deq_ib == d_disequalities.end() || - (*deq_ia).second->size() > (*deq_ib).second->size()) { - TNode tmp = a; - a = b; - b = tmp; - } - } + while(!done() && !d_conflict) { + // Get all the assertions + Assertion assertion = get(); + TNode fact = assertion.assertion; + Debug("datatypes-assert") << "Assert " << fact << std::endl; - //if b is a selector, swap a and b - if( b.getKind() == APPLY_SELECTOR && a.getKind() != APPLY_SELECTOR ) { - TNode tmp = a; - a = b; - b = tmp; - } - //make constructors the representatives - if( a.getKind() == APPLY_CONSTRUCTOR ) { - TNode tmp = a; - a = b; - b = tmp; - } - //make sure skolem variable is not representative - if( b.getKind() == SKOLEM ) { - TNode tmp = a; - a = b; - b = tmp; + //reset the maps + d_pending.clear(); + d_pending_exp.clear(); + //assert the fact + assertFact( fact, fact ); + flushPendingFacts(); } - //check for clash - NodeBuilder<> explanation(kind::AND); - if( a.getKind() == kind::APPLY_CONSTRUCTOR && b.getKind() == kind::APPLY_CONSTRUCTOR - && a.getOperator()!=b.getOperator() ){ - Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, a, b ); - d_em.addNode( ccEq, &d_cce ); - d_em.addNodeConflict( ccEq, Reason::idt_clash ); - Debug("datatypes") << "Clash " << a << " " << b << endl; - return; - } - Debug("datatypes-debug") << "Done clash" << endl; - - Debug("datatypes-ae") << "Set canon: "<< a << " " << b << endl; - // b becomes the canon of a - d_unionFind.setCanon(a, b); - d_reps[a] = false; - d_reps[b] = true; - - //add this to the transitive closure module - bool result = d_cycle_check.addEdgeNode( a, b ); - d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); - Debug("datatypes-cycles") << "Equal " << a << " -> " << b << " " << d_hasSeenCycle.get() << endl; - if( d_hasSeenCycle.get() ){ - checkCycles(); - if( hasConflict() ){ - return; + if( e == EFFORT_FULL ) { + Debug("datatypes-split") << "Check for splits " << e << endl; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node n = (*eqcs_i); + if( n.getType().isDatatype() ){ + EqcInfo* eqc = getOrMakeEqcInfo( n, true ); + //if there are more than 1 possible constructors for eqc + if( eqc->d_constructor.get().isNull() && !hasLabel( eqc, n ) ) { + const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); + //if only one constructor, then this term must be this constructor + if( dt.getNumConstructors()==1 ){ + Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n ); + d_pending.push_back( t ); + d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true ); + Debug("datatypes-infer") << "DtInfer : " << t << ", trivial" << std::endl; + d_infer.push_back( t ); + }else{ + std::vector< bool > pcons; + getPossibleCons( eqc, n, pcons ); + //std::cout << "pcons " << n << " = "; + //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; } + //std::cout << std::endl; + //check if we do not need to resolve the constructor type for this equivalence class. + // this is if there are no selectors for this equivalence class, its type is infinite, + // and we are not producing a model, then do not split. + int consIndex = -1; + bool needSplit = true; + for( unsigned int j=0; jd_selectors ) {//&& !Options::current()->produceModels && !Options::current()->finiteModelFind ){ + needSplit = false; + } + } + } + if( needSplit && consIndex!=-1 ) { + Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n ); + Debug("datatypes-split") << "*************Split for possible constructor " << test << " for " << n << endl; + NodeBuilder<> nb(kind::OR); + nb << test << test.notNode(); + Node lemma = nb; + d_out->lemma( lemma ); + d_out->requirePhase( test, true ); + return; + }else{ + Debug("datatypes-split") << "Do not split constructor for " << n << std::endl; + } + } + } + } + ++eqcs_i; } - } - //else{ - // checkCycles(); - // if( hasConflict() ){ - // for( int i=0; i<(int)d_currEqualities.size(); i++ ) { - // Debug("datatypes-cycles") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl; - // } - // d_cycle_check.debugPrint(); - // Assert( false ); - // } - //} - Debug("datatypes-debug") << "Done cycles" << endl; - - //merge equivalence classes - initializeEqClass( b ); - EqListN* eqc_b = (*d_equivalence_class.find( b )).second; - EqListsN::iterator eqc_a_i = d_equivalence_class.find( a ); - if( eqc_a_i!=d_equivalence_class.end() ){ - EqListN* eqc_a = (*eqc_a_i).second; - for( EqListN::const_iterator i = eqc_a->begin(); i != eqc_a->end(); i++ ) { - eqc_b->push_back( *i ); + flushPendingFacts(); + if( !d_conflict ){ + printModelDebug(); } - }else{ - eqc_b->push_back( a ); } - //merge selector lists - EqListsN::iterator sel_a_i = d_selector_eq.find( a ); - if( sel_a_i != d_selector_eq.end() ) { - EqListsN::iterator sel_b_i = d_selector_eq.find( b ); - EqListN* sel_b; - if( sel_b_i == d_selector_eq.end() ) { - sel_b = new(getSatContext()->getCMM()) EqListN(true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM())); - d_selector_eq.insertDataFromContextMemory(b, sel_b); - } else { - sel_b = (*sel_b_i).second; - } - EqListN* sel_a = (*sel_a_i).second; - for( EqListN::const_iterator i = sel_a->begin(); i != sel_a->end(); i++ ) { - sel_b->push_back( *i ); - } - if( !sel_a->empty() ){ - d_checkMap[ b ] = true; - } + if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) { + Notice() << "TheoryDatatypes::check(): done" << endl; } +} - deq_ia = d_disequalities.find(a); - map alreadyDiseqs; - if(deq_ia != d_disequalities.end()) { - /* - * Collecting the disequalities of b, no need to check for conflicts - * since the representative of b does not change and we check all the things - * in a's class when we look at the diseq list of find(a) - */ - EqLists::iterator deq_ib = d_disequalities.find(b); - if(deq_ib != d_disequalities.end()) { - EqList* deq = (*deq_ib).second; - for(EqList::const_iterator j = deq->begin(); j != deq->end(); j++) { - TNode deqn = *j; - TNode s = deqn[0]; - TNode t = deqn[1]; - TNode sp = find(s); - TNode tp = find(t); - Assert(sp == b || tp == b, "test1"); - if(sp == b) { - alreadyDiseqs[tp] = deqn; - } else { - alreadyDiseqs[sp] = deqn; - } - } - } - - /* - * Looking for conflicts in the a disequality list. Note - * that at this point a and b are already merged. Also has - * the side effect that it adds them to the list of b (which - * became the canonical representative) - */ - EqList* deqa = (*deq_ia).second; - for(EqList::const_iterator i = deqa->begin(); i != deqa->end(); i++) { - TNode deqn = (*i); - Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF); - TNode s = deqn[0]; - TNode t = deqn[1]; - - TNode sp = find(s); - TNode tp = find(t); - if(sp == tp) { - Debug("datatypes") << "Construct standard conflict " << deqn << " " << sp << endl; - d_em.addNode( deqn, &d_cce ); - d_em.addNodeConflict( NodeManager::currentNM()->mkNode( kind::AND, deqn, deqn.notNode() ), Reason::contradiction ); - return; - } - Assert( sp == b || tp == b, "test2"); - - // make sure not to add duplicates - if(sp == b) { - if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) { - appendToDiseqList(b, deqn); - alreadyDiseqs[tp] = deqn; - } - } else { - if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) { - appendToDiseqList(b, deqn); - alreadyDiseqs[sp] = deqn; - } - } - - } +void TheoryDatatypes::assertFact( Node fact, Node exp ){ + Assert( d_pending_merge.empty() ); + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + if (atom.getKind() == kind::EQUAL) { + d_equalityEngine.assertEquality( atom, polarity, exp ); + }else{ + d_equalityEngine.assertPredicate( atom, polarity, exp ); + } + //do all pending merges + int i=0; + while( i<(int)d_pending_merge.size() ){ + Assert( d_pending_merge[i].getKind()==EQUAL || d_pending_merge[i].getKind()==IFF ); + merge( d_pending_merge[i][0], d_pending_merge[i][1] ); + i++; + } + d_pending_merge.clear(); + //add to tester if applicable + if( atom.getKind()==kind::APPLY_TESTER ){ + Node rep = getRepresentative( atom[0] ); + EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); + addTester( fact, eqc, rep ); } +} - //merge labels - EqLists::iterator lbl_i = d_labels.find( a ); - if(lbl_i != d_labels.end()) { - EqList* lbl = (*lbl_i).second; - for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - addTester( *i ); - if( hasConflict() ) { - return; - } - } +void TheoryDatatypes::flushPendingFacts(){ + //also assert the pending facts + int i = 0; + while( !d_conflict && i<(int)d_pending.size() ){ + assertFact( d_pending[i], d_pending_exp[ d_pending[i] ] ); + i++; } - Debug("datatypes-debug") << "Done merge labels" << endl; + d_pending.clear(); + d_pending_exp.clear(); +} - //do unification - if( a.getKind() == APPLY_CONSTRUCTOR && b.getKind() == APPLY_CONSTRUCTOR && - a.getOperator() == b.getOperator() ) { - Debug("datatypes") << "Unification: " << a << " and " << b << "." << endl; - for( int i=0; i<(int)a.getNumChildren(); i++ ) { - if( find( a[i] ) != find( b[i] ) ) { - Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, a, b ); - Node newEq = NodeManager::currentNM()->mkNode( EQUAL, a[i], b[i] ); - d_em.addNode( ccEq, &d_cce ); - d_em.addNode( newEq, ccEq, Reason::idt_unify ); - addEquality( newEq ); - if( hasConflict() ) { - return; - } - } +void TheoryDatatypes::preRegisterTerm(TNode n) { + Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl; + collectTerms( n ); + switch (n.getKind()) { + case kind::EQUAL: + // Add the trigger for equality + d_equalityEngine.addTriggerEquality(n); + break; + case kind::APPLY_TESTER: + // Get triggered for both equal and dis-equal + d_equalityEngine.addTriggerPredicate(n); + break; + default: + // Maybe it's a predicate + if (n.getType().isBoolean()) { + // Get triggered for both equal and dis-equal + d_equalityEngine.addTriggerPredicate(n); + } else { + // Function applications/predicates + d_equalityEngine.addTerm(n); } + break; } + Assert( d_pending.empty() ); +} - Debug("datatypes-debug") << "merge(): Done" << endl; +void TheoryDatatypes::presolve() { + Debug("datatypes") << "TheoryDatatypes::presolve()" << endl; } -void TheoryDatatypes::addTermToLabels( Node t ) { - if( t.getType().isDatatype() ) { - Debug("datatypes-debug") << "Add term to labels " << t << std::endl; - Node tmp = find( t ); - if( tmp == t ) { - //add to labels - EqLists::iterator lbl_i = d_labels.find(t); - if(lbl_i == d_labels.end()) { - EqList* lbl = new(getSatContext()->getCMM()) EqList(true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM())); - //if there is only one constructor, then it must be - const Datatype& dt = ((DatatypeType)(t.getType()).toType()).getDatatype(); - if( dt.getNumConstructors()==1 ){ - Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), t ); - lbl->push_back( tester ); - d_checkMap[ t ] = true; - d_em.addNodeAxiom( tester, Reason::idt_texhaust ); - } - d_labels.insertDataFromContextMemory(tmp, lbl); - } - } - } +void TheoryDatatypes::addSharedTerm(TNode t) { + Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): " + << t << endl; } -void TheoryDatatypes::initializeEqClass( Node t ) { - EqListsN::iterator eqc_i = d_equivalence_class.find( t ); - if( eqc_i == d_equivalence_class.end() ) { - EqListN* eqc = new(getSatContext()->getCMM()) EqListN(true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM())); - eqc->push_back( t ); - d_equivalence_class.insertDataFromContextMemory(t, eqc); - } +void TheoryDatatypes::collectModelInfo( TheoryModel* m ){ + printModelDebug(); + m->assertEqualityEngine( &d_equalityEngine ); } -void TheoryDatatypes::collectTerms( Node n, bool recurse ) { - if( recurse ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ) { - collectTerms( n[i] ); - } + +void TheoryDatatypes::collectTerms( Node n ) { + for( int i=0; i<(int)n.getNumChildren(); i++ ) { + collectTerms( n[i] ); } if( n.getKind() == APPLY_CONSTRUCTOR ){ for( int i=0; i<(int)n.getNumChildren(); i++ ) { - Debug("datatypes-cycles") << "Subterm " << n << " -> " << n[i] << endl; - bool result CVC4_UNUSED = d_cycle_check.addEdgeNode( n, n[i] ); - Assert( !result ); //this should not create any new cycles (relevant terms should have been recorded before) + Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl; + bool result = d_cycle_check.addEdgeNode( n, n[i] ); + d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); + } + }else if( n.getKind() == APPLY_SELECTOR ){ + Debug("datatypes") << " Found selector " << n << endl; + if (n.getType().isBoolean()) { + d_equalityEngine.addTriggerPredicate( n ); + }else{ + d_equalityEngine.addTerm( n ); } - }else{ - if( n.getKind() == APPLY_SELECTOR && d_selectors.find( n ) == d_selectors.end() ) { - Debug("datatypes") << " Found selector " << n << endl; - d_selectors[ n ] = false; - d_cc.addTerm( n ); - Node tmp = find( n[0] ); - d_checkMap[ tmp ] = true; - - //add selector to selector eq list - Debug("datatypes") << " Add selector to list " << tmp << " " << n << endl; - EqListsN::iterator sel_i = d_selector_eq.find( tmp ); - EqListN* sel; - if( sel_i == d_selector_eq.end() ) { - sel = new(getSatContext()->getCMM()) EqListN(true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM())); - d_selector_eq.insertDataFromContextMemory(tmp, sel); - } else { - sel = (*sel_i).second; - } - sel->push_back( n ); + Node rep = getRepresentative( n[0] ); + EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); + if( !eqc->d_selectors ){ + eqc->d_selectors = true; + checkInstantiate( eqc, rep ); } - addTermToLabels( n ); } } -void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) { - Debug("datatypes") << "appending " << eq << endl - << " to diseq list of " << of << endl; - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - Assert(of == debugFind(of)); - EqLists::iterator deq_i = d_disequalities.find(of); - EqList* deq; - if(deq_i == d_disequalities.end()) { - deq = new(getSatContext()->getCMM()) EqList(true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM())); - d_disequalities.insertDataFromContextMemory(of, deq); - } else { - deq = (*deq_i).second; - } - deq->push_back(eq); - //if(Debug.isOn("uf")) { - // Debug("uf") << " size is now " << deq->size() << endl; - //} +Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index ){ + //add constructor to equivalence class + std::vector< Node > children; + children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); + for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ + children.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n ) ); + } + Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + collectTerms( n_ic ); + //add type ascription for ambiguous constructor types + if( n_ic.getType()!=n.getType() ){ + Assert( dt.isParametric() ); + Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl; + Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl; + Type tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); + Debug("datatypes-parametric") << "Type specification is " << tspec << std::endl; + children[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(tspec)), children[0] ); + n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + Assert( n_ic.getType()==n.getType() ); + } + return n_ic; } -void TheoryDatatypes::addEquality(TNode eq) { - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - if( !hasConflict() && find( eq[0] ) != find( eq[1] ) ) { - Debug("datatypes") << "Add equality " << eq << "." << endl; - Debug("datatypes-debug-pf") << "Add equality " << eq << "." << endl; -#if 1 //for delayed merging - //setup merge pending list - d_merge_pending.push_back( vector< pair< Node, Node > >() ); - - d_cce.assertTrue(eq); - d_cc.addTerm(eq[0]); - d_cc.addTerm(eq[1]); - - //record which nodes are waiting to be merged - vector< pair< Node, Node > > mp; - mp.insert( mp.begin(), - d_merge_pending[d_merge_pending.size()-1].begin(), - d_merge_pending[d_merge_pending.size()-1].end() ); - d_merge_pending.pop_back(); - - //merge original nodes - if( !hasConflict() ) { - merge( eq[0], eq[1] ); +void TheoryDatatypes::checkInstantiate( EqcInfo* eqc, Node n ){ + //add constructor to equivalence class if not done so already + if( hasLabel( eqc, n ) && eqc->d_inst.get().isNull() ){ + Node exp; + Node tt; + if( !eqc->d_constructor.get().isNull() ){ + exp = NodeManager::currentNM()->mkConst( true ); + tt = eqc->d_constructor; }else{ - Debug("datatypes-debug-pf") << "Forget merge " << eq << std::endl; - } - //merge nodes waiting to be merged - for( int i=0; i<(int)mp.size(); i++ ) { - if( !hasConflict() ) { - merge( mp[i].first, mp[i].second ); - }else{ - Debug("datatypes-debug-pf") << "Forget merge " << mp[i].first << " " << mp[i].second << std::endl; + exp = getLabel( n ); + tt = exp[0]; + } + int index = getLabelIndex( eqc, n ); + const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype(); + //must be finite or have a selector + if( eqc->d_selectors || dt[ index ].isFinite() ){ + eqc->d_inst.set( NodeManager::currentNM()->mkConst( true ) ); + Node tt_cons = getInstantiateCons( tt, dt, index ); + Node eq; + if( tt!=tt_cons ){ + eq = tt.eqNode( tt_cons ); + Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl; + d_pending.push_back( eq ); + d_pending_exp[ eq ] = exp; + Debug("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl; + //eqc->d_inst.set( eq ); + d_infer.push_back( eq ); + d_infer_exp.push_back( exp ); } } -#elif 0 - Debug("datatypes-ae") << "Add equality " << eq << "." << endl; - Debug("datatypes-ae") << " Find is " << find( eq[0] ) << " = " << find( eq[1] ) << std::endl; - //merge original nodes - merge( eq[0], eq[1] ); - d_cce.assertTrue(eq); - d_cc.addTerm(eq[0]); - d_cc.addTerm(eq[1]); -#else - Debug("datatypes-ae") << "Add equality " << eq << "." << endl; - Debug("datatypes-ae") << " Find is " << find( eq[0] ) << " = " << find( eq[1] ) << std::endl; - merge( eq[0], eq[1] ); - if( !hasConflict() ){ - d_cce.assertTrue(eq); - d_cc.addTerm(eq[0]); - d_cc.addTerm(eq[1]); - } -#endif - if( Debug.isOn("datatypes") || Debug.isOn("datatypes-cycles") ){ - d_currEqualities.push_back(eq); - } } } -void TheoryDatatypes::addDisequality(TNode eq) { - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - - TNode a = eq[0]; - TNode b = eq[1]; - - appendToDiseqList(find(a), eq); - appendToDiseqList(find(b), eq); -} - void TheoryDatatypes::checkCycles() { - for( BoolMap::iterator i = d_reps.begin(); i != d_reps.end(); i++ ) { - if( (*i).second ) { - map< Node, bool > visited; - NodeBuilder<> explanation(kind::AND); - if( searchForCycle( (*i).first, (*i).first, visited, explanation ) ) { - Node cCycle = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation; - d_em.addNodeConflict( cCycle, Reason::idt_cycle_coarse ); - Debug("datatypes") << "Detected cycle for " << (*i).first << endl; - Debug("datatypes") << "Conflict is " << cCycle << endl; - return; - } + Debug("datatypes-cycle-check") << "Check cycles" << std::endl; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + map< Node, bool > visited; + NodeBuilder<> explanation(kind::AND); + if( searchForCycle( eqc, eqc, visited, explanation ) ) { + d_conflictNode = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation; + Debug("datatypes-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; + return; } + ++eqcs_i; } } @@ -1028,25 +717,28 @@ void TheoryDatatypes::checkCycles() { bool TheoryDatatypes::searchForCycle( Node n, Node on, map< Node, bool >& visited, NodeBuilder<>& explanation ) { - //Debug("datatypes") << "Search for cycle " << n << " " << on << endl; - if( n.getKind() == APPLY_CONSTRUCTOR ) { - for( int i=0; i<(int)n.getNumChildren(); i++ ) { - Node nn = find( n[i] ); - if( visited.find( nn ) == visited.end() ) { - visited[nn] = true; - if( nn == on || searchForCycle( nn, on, visited, explanation ) ) { - if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, n[i] ) ){ - Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << n[i] << "!!!!" << std::endl; - } - if( nn != n[i] ) { - if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n[i], nn ) ){ - Debug("datatypes-cycles") << "Cycle equality: " << n[i] << " is not -> " << nn << "!!!!" << std::endl; + Debug("datatypes-cycle-check") << "Search for cycle " << n << " " << on << endl; + Node ncons; + EqcInfo* eqc = getOrMakeEqcInfo( n ); + if( eqc ){ + Node ncons = eqc->d_constructor.get(); + if( !ncons.isNull() ) { + for( int i=0; i<(int)ncons.getNumChildren(); i++ ) { + Node nn = getRepresentative( ncons[i] ); + if( visited.find( nn ) == visited.end() ) { + visited[nn] = true; + if( nn == on || searchForCycle( nn, on, visited, explanation ) ) { + if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){ + Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl; + } + if( nn != ncons[i] ) { + if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( ncons[i], nn ) ){ + Debug("datatypes-cycles") << "Cycle equality: " << ncons[i] << " is not -> " << nn << "!!!!" << std::endl; + } + explanation << NodeManager::currentNM()->mkNode( EQUAL, nn, ncons[i] ); } - Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, nn, n[i] ); - d_em.addNode( ccEq, &d_cce ); - explanation << ccEq; + return true; } - return true; } } } @@ -1055,62 +747,33 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on, } bool TheoryDatatypes::hasTerm( Node a ){ - return false; + return d_equalityEngine.hasTerm( a ); } bool TheoryDatatypes::areEqual( Node a, Node b ){ - Node ar = find( a ); - Node br = find( b ); - if( ar==br ){ + if( a==b ){ return true; - }else if( ar.getKind()==APPLY_CONSTRUCTOR && br.getKind()==APPLY_CONSTRUCTOR && - ar.getOperator()==br.getOperator() ){ - //for( int i=0; i<(int)ar.getNumChildren(); i++ ){ - // if( !areEqual( ar[0], br[0] ) ){ - // return false; - // } - //} - //return true; - return false; + }else if( hasTerm( a ) && hasTerm( b ) ){ + return d_equalityEngine.areEqual( a, b ); }else{ return false; } } bool TheoryDatatypes::areDisequal( Node a, Node b ){ - Node ar = find( a ); - Node br = find( b ); - if( ar==br ){ + if( a==b ){ return false; - }else if( ar.getKind()==APPLY_CONSTRUCTOR && br.getKind()==APPLY_CONSTRUCTOR && - ar.getOperator()!=br.getOperator() ){ - return true; + }else if( hasTerm( a ) && hasTerm( b ) ){ + return d_equalityEngine.areDisequal( a, b, false ); }else{ - EqLists::iterator deq_ia = d_disequalities.find( ar ); - EqLists::iterator deq_ib = d_disequalities.find( br ); - if( deq_ia!=d_disequalities.end() && deq_ib!=d_disequalities.end() ){ - EqList* deq; - if( (*deq_ib).second->size()<(*deq_ia).second->size() ){ - deq = (*deq_ib).second; - }else{ - deq = (*deq_ia).second; - } - for(EqList::const_iterator i = deq->begin(); i != deq->end(); i++) { - TNode deqn = (*i); - TNode sp = find(deqn[0]); - TNode tp = find(deqn[1]); - if( sp==a && tp==b ){ - return true; - }else if( sp==b && tp==a ){ - return true; - } - } - } return false; } } Node TheoryDatatypes::getRepresentative( Node a ){ - return find( a ); + if( hasTerm( a ) ){ + return d_equalityEngine.getRepresentative( a ); + }else{ + return a; + } } - diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 80c20a7d9..6d9672f95 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -28,6 +28,7 @@ #include "util/hash.h" #include "util/trans_closure.h" #include "theory/datatypes/explanation_manager.h" +#include "theory/uf/equality_engine.h" #include #include @@ -40,177 +41,192 @@ namespace datatypes { class InstantiatorTheoryDatatypes; class EqualityQueryTheory; -namespace rrinst{ - class CandidateGeneratorTheoryClass; -} - class TheoryDatatypes : public Theory { friend class InstantiatorTheoryDatatypes; friend class EqualityQueryTheory; - friend class rrinst::CandidateGeneratorTheoryClass; - private: - typedef context::CDChunkList EqList; - typedef context::CDHashMap EqLists; - typedef context::CDChunkList EqListN; - typedef context::CDHashMap EqListsN; + typedef context::CDChunkList NodeList; + typedef context::CDHashMap NodeListMap; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - /** for debugging */ - context::CDList d_currAsserts; - context::CDList d_currEqualities; - - /** keeps track of all selectors we care about, value is whether they have been collapsed */ - BoolMap d_selectors; - /** keeps track of which nodes are representatives */ - BoolMap d_reps; - /** map from (representative) nodes to a list of selectors whose arguments are - in the equivalence class of that node */ - EqListsN d_selector_eq; - /** map from (representative) nodes to list of nodes in their eq class */ - EqListsN d_equivalence_class; - /** map from nodes to whether they have been instantiated */ - BoolMap d_inst_map; /** transitive closure to record equivalence/subterm relation. */ TransitiveClosureNode d_cycle_check; /** has seen cycle */ context::CDO< bool > d_hasSeenCycle; - /** get the constructor for the node */ - const DatatypeConstructor& getConstructor( Node cons ); - /** get the constructor for the selector */ - Node getConstructorForSelector( Node sel ); - - /** - * map from (representative) nodes to testers that hold for that node - * for each t, this is either a list of equations of the form + /** inferences */ + NodeList d_infer; + NodeList d_infer_exp; +private: + //notification class for equality engine + class NotifyClass : public eq::EqualityEngineNotify { + TheoryDatatypes& d_dt; + public: + NotifyClass(TheoryDatatypes& dt): d_dt(dt) {} + bool eqNotifyTriggerEquality(TNode equality, bool value) { + Debug("dt") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; + if (value) { + return d_dt.propagate(equality); + } else { + // We use only literal triggers so taking not is safe + return d_dt.propagate(equality.notNode()); + } + } + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + Debug("dt") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; + if (value) { + return d_dt.propagate(predicate); + } else { + return d_dt.propagate(predicate.notNode()); + } + } + bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { + Debug("dt") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; + if (value) { + return d_dt.propagate(t1.eqNode(t2)); + } else { + return d_dt.propagate(t1.eqNode(t2).notNode()); + } + } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { + Debug("dt") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + d_dt.conflict(t1, t2); + } + void eqNotifyNewClass(TNode t) { + Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << std::endl; + d_dt.eqNotifyNewClass(t); + } + void eqNotifyPreMerge(TNode t1, TNode t2) { + Debug("dt") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl; + d_dt.eqNotifyPreMerge(t1, t2); + } + void eqNotifyPostMerge(TNode t1, TNode t2) { + Debug("dt") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl; + d_dt.eqNotifyPostMerge(t1, t2); + } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + Debug("dt") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl; + d_dt.eqNotifyDisequal(t1, t2, reason); + } + };/* class TheoryDatatypes::NotifyClass */ +private: + /** equivalence class info + * d_inst is whether the instantiate rule has been applied, + * d_constructor is a node of kind APPLY_CONSTRUCTOR (if any) in this equivalence class, + * d_selectors is whether a selector has been applied to this equivalence class. + */ + class EqcInfo + { + public: + EqcInfo( context::Context* c ); + ~EqcInfo(){} + //whether we have instantiatied this eqc + context::CDO< Node > d_inst; + //constructor equal to this eqc + context::CDO< Node > d_constructor; + //all selectors whose argument is this eqc + context::CDO< bool > d_selectors; + }; + /** does eqc of n have a label? */ + bool hasLabel( EqcInfo* eqc, Node n ); + /** get the label associated to n */ + Node getLabel( Node n ); + /** get the index of the label associated to n */ + int getLabelIndex( EqcInfo* eqc, Node n ); + /** get the possible constructors for n */ + void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons ); +private: + /** The notify class */ + NotifyClass d_notify; + /** Equaltity engine */ + eq::EqualityEngine d_equalityEngine; + /** information necessary for equivalence classes */ + std::map< Node, EqcInfo* > d_eqc_info; + /** labels for each equivalence class + * for each eqc n, d_labels[n] is testers that hold for this equivalence class, either: + * a list of equations of the form * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers * and n is less than the number of possible constructors for t minus one, * or a list of equations of the form * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ) followed by * is_[constructor_(n+1)]( t ), each of which is a unique tester. - */ - EqLists d_labels; - - class CongruenceChannel { - TheoryDatatypes* d_datatypes; - - public: - CongruenceChannel(TheoryDatatypes* datatypes) : d_datatypes(datatypes) {} - void notifyCongruent(TNode a, TNode b) { - d_datatypes->notifyCongruent(a, b); - } - };/* class CongruenceChannel */ - friend class CongruenceChannel; - - /** - * Output channel connected to the congruence closure module. - */ - CongruenceChannel d_ccChannel; - - /** - * Instance of the congruence closure module. - */ - CongruenceClosure d_cc; - - /** - * Union find for storing the equalities. - */ - UnionFind d_unionFind; - - /** - * Received a notification from the congruence closure algorithm that the two nodes - * a and b have been merged. - */ - void notifyCongruent(TNode a, TNode b); - - /** - * List of all disequalities this theory has seen. - * Maintaints the invariant that if a is in the - * disequality list of b, then b is in that of a. - * */ - EqLists d_disequalities; - - /** - * information for delayed merging (is this necessary?) - */ - std::vector< std::vector< std::pair< Node, Node > > > d_merge_pending; - - /** - * Terms that currently need to be checked for collapse/instantiation rules - */ - std::map< Node, bool > d_checkMap; - - /** - * explanation manager - */ - ExplanationManager d_em; - - /** - * explanation manager for the congruence closure module - */ - CongruenceClosureExplainer d_cce; - - //temporary - std::vector< Node > d_preRegTerms; + */ + NodeListMap d_labels; + /** Are we in conflict */ + context::CDO d_conflict; + /** The conflict node */ + Node d_conflictNode; + /** pending assertions/merges */ + std::vector< Node > d_pending; + std::map< Node, Node > d_pending_exp; + std::vector< Node > d_pending_merge; +private: + /** assert fact */ + void assertFact( Node fact, Node exp ); + /** flush pending facts */ + void flushPendingFacts(); + /** get or make eqc info */ + EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false ); + /** has eqc info */ + bool hasEqcInfo( Node n ) { return d_labels.find( n )!=d_labels.end(); } public: - TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, QuantifiersEngine* qe); ~TheoryDatatypes(); + /** propagate */ + void propagate(Effort effort); + /** propagate */ + bool propagate(TNode literal); + /** explain */ + void explain( TNode literal, std::vector& assumptions ); + Node explain( TNode literal ); + /** Conflict when merging two constants */ + void conflict(TNode a, TNode b); + /** called when a new equivalance class is created */ + void eqNotifyNewClass(TNode t); + /** called when two equivalance classes will merge */ + void eqNotifyPreMerge(TNode t1, TNode t2); + /** called when two equivalance classes have merged */ + void eqNotifyPostMerge(TNode t1, TNode t2); + /** called when two equivalence classes are made disequal */ + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); + + void check(Effort e); void preRegisterTerm(TNode n); void presolve(); - void addSharedTerm(TNode t); - void check(Effort e); void collectModelInfo( TheoryModel* m ); void shutdown() { } std::string identify() const { return std::string("TheoryDatatypes"); } - private: - /* Helper methods */ - bool checkTester( Node assertion, Node& conflict, unsigned& r ); - void addTester( Node assertion ); - Node getInstantiateCons( Node t ); - void checkInstantiateEqClass( Node t ); - bool checkInstantiate( Node te, Node cons ); - bool collapseSelector( Node t ); - void updateSelectors( Node a ); - void addTermToLabels( Node t ); - void initializeEqClass( Node t ); - void collectTerms( Node n, bool recurse = true ); - bool hasConflict(); - - /* from uf_morgan */ - void merge(TNode a, TNode b); - inline TNode find(TNode a); - inline TNode debugFind(TNode a) const; - void appendToDiseqList(TNode of, TNode eq); - void addDisequality(TNode eq); - void addEquality(TNode eq); - + /** add tester to equivalence class info */ + void addTester( Node t, EqcInfo* eqc, Node n ); + /** merge the equivalence class info of t1 and t2 */ + void merge( Node t1, Node t2 ); + /** for checking if cycles exist */ void checkCycles(); bool searchForCycle( Node n, Node on, std::map< Node, bool >& visited, NodeBuilder<>& explanation ); -public: + /** collect terms */ + void collectTerms( Node n ); + /** get instantiate cons */ + Node getInstantiateCons( Node n, const Datatype& dt, int index ); + /** check instantiate */ + void checkInstantiate( EqcInfo* eqc, Node n ); + /** debug print */ + void printModelDebug(); + +private: //equality queries bool hasTerm( Node a ); bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); Node getRepresentative( Node a ); +public: + /** get equality engine */ + eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } };/* class TheoryDatatypes */ -inline bool TheoryDatatypes::hasConflict() { - return d_em.hasConflict(); -} - -inline TNode TheoryDatatypes::find(TNode a) { - return d_unionFind.find(a); -} - -inline TNode TheoryDatatypes::debugFind(TNode a) const { - return d_unionFind.debugFind(a); -} - - }/* CVC4::theory::datatypes namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp index 57e9324df..b4b85c9fb 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.cpp +++ b/src/theory/datatypes/theory_datatypes_instantiator.cpp @@ -15,10 +15,10 @@ **/ #include "theory/datatypes/theory_datatypes_instantiator.h" -#include "theory/datatypes/theory_datatypes_candidate_generator.h" #include "theory/datatypes/theory_datatypes.h" #include "theory/theory_engine.h" #include "theory/quantifiers/term_database.h" +#include "theory/rr_candidate_generator.h" using namespace std; using namespace CVC4; @@ -55,6 +55,7 @@ int InstantiatorTheoryDatatypes::process( Node f, Theory::Effort effort, int e ) if( e<2 ){ return InstStrategy::STATUS_UNFINISHED; }else if( e==2 ){ + /* InstMatch m; for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){ Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); @@ -65,12 +66,15 @@ int InstantiatorTheoryDatatypes::process( Node f, Theory::Effort effort, int e ) } } d_quantEngine->addInstantiation( f, m ); + */ } } return InstStrategy::STATUS_UNKNOWN; } Node InstantiatorTheoryDatatypes::getValueFor( Node n ){ + return n; + /* FIXME //simply get the ground value for n in the current model, if it exists, // or return an arbitrary ground term otherwise Debug("quant-datatypes-debug") << "get value for " << n << std::endl; @@ -142,6 +146,7 @@ Node InstantiatorTheoryDatatypes::getValueFor( Node n ){ } } } + */ } InstantiatorTheoryDatatypes::Statistics::Statistics(): @@ -155,22 +160,57 @@ InstantiatorTheoryDatatypes::Statistics::~Statistics(){ } bool InstantiatorTheoryDatatypes::hasTerm( Node a ){ - return ((TheoryDatatypes*)d_th)->hasTerm( a ); + return ((TheoryDatatypes*)d_th)->getEqualityEngine()->hasTerm( a ); } bool InstantiatorTheoryDatatypes::areEqual( Node a, Node b ){ - return ((TheoryDatatypes*)d_th)->areEqual( a, b ); + if( a==b ){ + return true; + }else if( hasTerm( a ) && hasTerm( b ) ){ + return ((TheoryDatatypes*)d_th)->getEqualityEngine()->areEqual( a, b ); + }else{ + return false; + } } bool InstantiatorTheoryDatatypes::areDisequal( Node a, Node b ){ - return ((TheoryDatatypes*)d_th)->areDisequal( a, b ); + if( a==b ){ + return false; + }else if( hasTerm( a ) && hasTerm( b ) ){ + return ((TheoryDatatypes*)d_th)->getEqualityEngine()->areDisequal( a, b, false ); + }else{ + return false; + } } Node InstantiatorTheoryDatatypes::getRepresentative( Node a ){ - return ((TheoryDatatypes*)d_th)->getRepresentative( a ); + if( hasTerm( a ) ){ + return ((TheoryDatatypes*)d_th)->getEqualityEngine()->getRepresentative( a ); + }else{ + return a; + } +} + +eq::EqualityEngine* InstantiatorTheoryDatatypes::getEqualityEngine(){ + return &((TheoryDatatypes*)d_th)->d_equalityEngine; +} + +void InstantiatorTheoryDatatypes::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ + if( hasTerm( a ) ){ + a = getEqualityEngine()->getRepresentative( a ); + eq::EqClassIterator eqc_iter( a, getEqualityEngine() ); + while( !eqc_iter.isFinished() ){ + if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){ + eqc.push_back( *eqc_iter ); + } + eqc_iter++; + } + } } CVC4::theory::rrinst::CandidateGenerator* InstantiatorTheoryDatatypes::getRRCanGenClass(){ - TheoryDatatypes* th = static_cast(getTheory()); - return new datatypes::rrinst::CandidateGeneratorTheoryClass(th); + datatypes::TheoryDatatypes* dt = static_cast(getTheory()); + eq::EqualityEngine* ee = + static_cast(dt->getEqualityEngine()); + return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee); } diff --git a/src/theory/datatypes/theory_datatypes_instantiator.h b/src/theory/datatypes/theory_datatypes_instantiator.h index fd7190a22..fe43f2cfc 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.h +++ b/src/theory/datatypes/theory_datatypes_instantiator.h @@ -61,6 +61,8 @@ public: bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); Node getRepresentative( Node a ); + eq::EqualityEngine* getEqualityEngine(); + void getEquivalenceClass( Node a, std::vector< Node >& eqc ); /** general creators of candidate generators */ CVC4::theory::rrinst::CandidateGenerator* getRRCanGenClass(); };/* class InstantiatiorTheoryDatatypes */ diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp index 4f1bfe67e..c90483fa3 100644 --- a/src/theory/inst_match.cpp +++ b/src/theory/inst_match.cpp @@ -17,8 +17,8 @@ #include "theory/inst_match.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" +#include "theory/candidate_generator.h" #include "theory/uf/theory_uf_instantiator.h" -#include "theory/uf/theory_uf_candidate_generator.h" #include "theory/uf/equality_engine.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/term_database.h" @@ -33,38 +33,6 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; -bool CandidateGenerator::isLegalCandidate( Node n ){ - return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) ) || - ( Options::current()->finiteModelFind && n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ); -} - -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(); - } -} - InstMatch::InstMatch() { } @@ -130,18 +98,21 @@ void InstMatch::debugPrint( const char* c ){ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ for( int i=0; i<(int)qe->getTermDatabase()->d_inst_constants[f].size(); i++ ){ - if( d_map.find( qe->getTermDatabase()->d_inst_constants[f][i] )==d_map.end() ){ - d_map[ qe->getTermDatabase()->d_inst_constants[f][i] ] = qe->getTermDatabase()->getFreeVariableForInstConstant( qe->getTermDatabase()->d_inst_constants[f][i] ); + Node ic = qe->getTermDatabase()->d_inst_constants[f][i]; + if( d_map.find( ic )==d_map.end() ){ + d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); } } } void InstMatch::makeInternal( QuantifiersEngine* qe ){ - for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ - if( Options::current()->cbqi && it->second.hasAttribute(InstConstantAttribute()) ){ - d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second ); - if( Options::current()->cbqi && it->second.hasAttribute(InstConstantAttribute()) ){ - d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first ); + if( Options::current()->cbqi ){ + for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ + if( it->second.hasAttribute(InstConstantAttribute()) ){ + d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second ); + if( it->second.hasAttribute(InstConstantAttribute()) ){ + d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first ); + } } } } @@ -203,9 +174,9 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m } if( modEq ){ //check modulo equality if any other instantiation match exists - if( ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine()->hasTerm( n ) ){ - eq::EqClassIterator eqc( ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine()->getRepresentative( n ), - ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() ); + if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ + eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ), + qe->getEqualityQuery()->getEngine() ); while( !eqc.isFinished() ){ Node en = (*eqc); if( en!=n ){ @@ -310,10 +281,10 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ //candidates will be all equalities - d_cg = new uf::inst::CandidateGeneratorTheoryUfLitEq( ith, d_match_pattern ); + d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern ); }else{ //candidates will be all disequalities - d_cg = new uf::inst::CandidateGeneratorTheoryUfLitDeq( ith, d_match_pattern ); + d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern ); } }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){ Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); @@ -322,7 +293,7 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ }else{ Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); //we are matching only in a particular equivalence class - d_cg = new uf::inst::CandidateGeneratorTheoryUf( ith, d_match_pattern.getOperator() ); + d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); //store the equivalence class that we will call d_cg->reset( ... ) on d_eq_class = d_pattern[1]; } @@ -331,7 +302,7 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl; //} //we will be scanning lists trying to find d_match_pattern.getOperator() - d_cg = new uf::inst::CandidateGeneratorTheoryUf( ith, d_match_pattern.getOperator() ); + d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); }else{ d_cg = new CandidateGeneratorQueue; if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){ @@ -785,9 +756,9 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I } if( modEq ){ //check modulo equality for other possible instantiations - if( ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine()->hasTerm( n ) ){ - eq::EqClassIterator eqc( qe->getEqualityQuery()->getRepresentative( n ), - ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() ); + if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ + eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ), + qe->getEqualityQuery()->getEngine() ); while( !eqc.isFinished() ){ Node en = (*eqc); if( en!=n ){ diff --git a/src/theory/inst_match.h b/src/theory/inst_match.h index 31a59b261..2b402779d 100644 --- a/src/theory/inst_match.h +++ b/src/theory/inst_match.h @@ -19,16 +19,14 @@ #ifndef __CVC4__INST_MATCH_H #define __CVC4__INST_MATCH_H -#include "theory/theory.h" #include "util/hash.h" #include #include #include -#include "theory/uf/equality_engine.h" -#include "theory/uf/theory_uf.h" #include "context/cdlist.h" +#include "theory/candidate_generator.h" //#define USE_EFFICIENT_E_MATCHING @@ -76,48 +74,6 @@ namespace uf{ namespace inst { -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 EqualityQuery { public: EqualityQuery(){} @@ -135,6 +91,10 @@ public: not contain instantiation constants, if such a term exists. */ virtual Node getInternalRepresentative( Node a ) = 0; + /** get the equality engine associated with this query */ + virtual eq::EqualityEngine* getEngine() = 0; + /** get the equivalence class of a */ + virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; };/* class EqualityQuery */ /** basic class defining an instantiation */ diff --git a/src/theory/inst_match_impl.h b/src/theory/inst_match_impl.h deleted file mode 100644 index 8ac5fd34f..000000000 --- a/src/theory/inst_match_impl.h +++ /dev/null @@ -1,125 +0,0 @@ -/********************* */ -/*! \file inst_match_impl.h - ** \verbatim - ** Original author: bobot - ** Major contributors: none - ** Minor contributors (to current version): taking, 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 inst match class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__INST_MATCH_IMPL_H -#define __CVC4__INST_MATCH_IMPL_H - -#include "theory/inst_match.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers_engine.h" -#include "theory/uf/theory_uf_instantiator.h" -#include "theory/uf/theory_uf_candidate_generator.h" -#include "theory/uf/equality_engine.h" - -namespace CVC4 { -namespace theory { - -template -InstMatchTrie2::InstMatchTrie2(context::Context* c, QuantifiersEngine* qe): - d_data(c->getLevel()), d_context(c), d_mods(c) { - d_eQ = qe->getEqualityQuery(); - d_eE = ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine(); -}; - -/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ -template -void InstMatchTrie2::addSubTree( Tree * root, mapIter current, mapIter end, size_t currLevel ) { - if( current == end ) return; - - Assert(root->e.find(current->second) == root->e.end()); - Tree * root2 = new Tree(currLevel); - root->e.insert(std::make_pair(current->second, root2)); - addSubTree(root2, ++current, end, currLevel ); -} - -/** exists match */ -template -bool InstMatchTrie2::existsInstMatch(InstMatchTrie2::Tree * root, - mapIter & current, mapIter & end, - Tree * & e, mapIter & diverge) const{ - if( current == end ) { - Debug("Trie2") << "Trie2 Bottom " << std::endl; - --current; - return true; - }; //Already their - - if (current->first > diverge->first){ - // this point is the deepest point currently seen map are ordered - e = root; - diverge = current; - }; - - TNode n = current->second; - typename InstMatchTrie2::Tree::MLevel::iterator it = - root->e.find( n ); - if( it!=root->e.end() && - existsInstMatch( (*it).second, ++current, end, e, diverge) ){ - Debug("Trie2") << "Trie2 Directly here " << n << std::endl; - --current; - return true; - } - Assert( it==root->e.end() || e != root ); - - // Even if n is in the trie others of the equivalence class - // can also be in it since the equality can have appeared - // after they have been added - if( modEq && d_eE->hasTerm( n ) ){ - //check modulo equality if any other instantiation match exists - eq::EqClassIterator eqc( d_eQ->getRepresentative( n ), d_eE ); - for( ;!eqc.isFinished();++eqc ){ - TNode en = (*eqc); - if( en == n ) continue; // already tested - typename InstMatchTrie2::Tree::MLevel::iterator itc = - root->e.find( en ); - if( itc!=root->e.end() && - existsInstMatch( (*itc).second, ++current, end, e, diverge) ){ - Debug("Trie2") << "Trie2 Indirectly here by equality " << n << " = " << en << std::endl; - --current; - return true; - } - Assert( itc==root->e.end() || e != root ); - } - } - --current; - return false; -} - -template -bool InstMatchTrie2::addInstMatch( InstMatch& m ) { - mapIter begin = m.d_map.begin(); - mapIter end = m.d_map.end(); - typename InstMatchTrie2::Tree * e = &d_data; - mapIter diverge = begin; - if( !existsInstMatch(e, begin, end, e, diverge ) ){ - Assert(!diverge->second.isNull()); - size_t currLevel = d_context->getLevel(); - addSubTree( e, diverge, end, currLevel ); - if(e->level != currLevel) - //If same level that e, will be removed at the same time than e - d_mods.push_back(std::make_pair(e,diverge->second)); - return true; - }else{ - return false; - } -} - -}/* CVC4::theory namespace */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__INST_MATCH_IMPL_H */ diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 609275a98..aa2c2d938 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -17,6 +17,8 @@ #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; @@ -72,6 +74,11 @@ d_equalityEngine( c, name ){ 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 ); @@ -84,31 +91,32 @@ void TheoryModel::addDefineType( TypeNode tn ){ void TheoryModel::toStreamFunction( Node n, std::ostream& out ){ out << "(" << n; - //out << " : " << n.getType(); + out << " : " << n.getType(); out << " "; Node value = getValue( n ); + /* if( n.getType().isSort() ){ - int index = d_ra.getIndexFor( value ); + int index = d_rep_set.getIndexFor( value ); if( index!=-1 ){ out << value.getType() << "_" << index; }else{ out << value; } }else{ - out << value; - } + */ + out << value; out << ")" << std::endl; } void TheoryModel::toStreamType( TypeNode tn, std::ostream& out ){ out << "(" << tn; if( tn.isSort() ){ - if( d_ra.d_type_reps.find( tn )!=d_ra.d_type_reps.end() ){ - out << " " << d_ra.d_type_reps[tn].size(); + 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_ra.d_type_reps[tn][i]; + // out << d_rep_set.d_type_reps[tn][i]; //} //out << ")"; } @@ -117,6 +125,22 @@ void TheoryModel::toStreamType( TypeNode tn, std::ostream& out ){ } 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 Equality." << std::endl; - // Node n1 = getValue( n[0] ); - // Node n2 = getValue( n[1] ); - // return NodeManager::currentNM()->mkConst( n1==n2 ); - //} } Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){ - if( d_ra.d_type_reps.find( tn )!=d_ra.d_type_reps.end() ){ + if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){ //try to find a pre-existing arbitrary element - for( size_t i=0; i& exclude ){ //FIXME: use the theory enumerator to generate constants here Node TheoryModel::getNewDomainValue( TypeNode tn ){ if( tn==NodeManager::currentNM()->booleanType() ){ - if( d_ra.d_type_reps[tn].empty() ){ + if( d_rep_set.d_type_reps[tn].empty() ){ return d_false; - }else if( d_ra.d_type_reps[tn].size()==1 ){ - return NodeManager::currentNM()->mkConst( areEqual( d_ra.d_type_reps[tn][0], 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(); } @@ -214,7 +230,7 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){ int val = 0; do{ Node r = NodeManager::currentNM()->mkConst( Rational(val) ); - if( std::find( d_ra.d_type_reps[tn].begin(), d_ra.d_type_reps[tn].end(), r )==d_ra.d_type_reps[tn].end() && + 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; } @@ -272,7 +288,8 @@ bool TheoryModel::hasTerm( Node a ){ Node TheoryModel::getRepresentative( Node a ){ if( d_equalityEngine.hasTerm( a ) ){ - return d_reps[ d_equalityEngine.getRepresentative( a ) ]; + Node r = d_equalityEngine.getRepresentative( a ); + return d_reps[ r ]; }else{ return a; } @@ -326,15 +343,49 @@ void TheoryModel::printRepresentative( std::ostream& out, Node r ){ } } -DefaultModel::DefaultModel( context::Context* c, std::string name ) : TheoryModel( c, name ){ +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() ){ - //DO_THIS? - return n; + //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 ) ){ @@ -370,67 +421,195 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t void TheoryEngineModelBuilder::buildModel( Model* m ){ TheoryModel* tm = (TheoryModel*)m; //reset representative information - tm->d_reps.clear(); - tm->d_ra.clear(); - Debug( "model-builder" ) << "TheoryEngineModelBuilder: Collect model info..." << std::endl; + 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 representatives + //populate term database, store constant representatives eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); - //add terms to model + 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() ){ - tm->addTerm( *eqc_i ); + 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; } - //choose representative for this equivalence class - Node rep = chooseRepresentative( tm, eqc ); //store representative in representative set - if( !rep.isNull() ){ - tm->d_reps[ eqc ] = rep; - tm->d_ra.add( rep ); + 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; } - //do model-builder specific initialization - // this should include choosing representatives for equivalence classes that have not yet been - // assigned representatives + //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 ); } -Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* tm, Node eqc ){ - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &tm->d_equalityEngine ); - while( !eqc_i.isFinished() ){ - //if constant, use this as representative - if( (*eqc_i).getMetaKind()==kind::metakind::CONSTANT ){ - return *eqc_i; +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; id_equalityEngine ); - while( !eqcs_i.isFinished() ){ - Node n = *eqcs_i; - if( tm->d_reps.find( n )!=tm->d_reps.end() ){ - TypeNode tn = n.getType(); - //add new constant to equivalence class - Node rep = tm->getNewDomainValue( tn ); - if( !rep.isNull() ){ - tm->assertEquality( n, rep, true ); - }else{ - rep = n; - } - tm->d_reps[ n ] = rep; - tm->d_ra.add( rep ); - } - ++eqcs_i; +Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc ){ + //try to get a new domain value + Node rep = m->getNewDomainValue( eqc.getType() ); + if( !rep.isNull() ){ + return rep; + }else{ + //if we can't get new domain value, just return eqc itself (this typically should not happen) + //FIXME: Assertion failure here? + return eqc; } } diff --git a/src/theory/model.h b/src/theory/model.h index 278f85dfe..415b008ef 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -60,16 +60,23 @@ class TheoryModel : public Model { friend class TheoryEngineModelBuilder; protected: - /** add term */ + /** 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: - /** definitions */ + /** 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: - /** to stream functions */ + /** 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 ); @@ -78,83 +85,102 @@ public: eq::EqualityEngine d_equalityEngine; /** map of representatives of equality engine to used representatives in representative set */ std::map< Node, Node > d_reps; - /** representative alphabet */ - RepSet d_ra; - //true/false nodes + /** stores set of representatives for each type */ + RepSet d_rep_set; + /** true/false nodes */ Node d_true; Node d_false; public: - /** add defined function */ + /** 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 */ + /** 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 interpreted value, should be a representative in d_reps */ - virtual Node getInterpretedValue( TNode n ) = 0; - /** get existing domain value, with possible exclusions */ + /** 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 */ + /** 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 */ + /** assert equality holds in the model */ void assertEquality( Node a, Node b, bool polarity ); - /** assert predicate */ + /** assert predicate holds in the model */ void assertPredicate( Node a, bool polarity ); - /** assert equality engine */ + /** assert all equalities/predicates in equality engine hold in the model */ void assertEqualityEngine( eq::EqualityEngine* ee ); public: - //queries about equality + /** 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 function */ + /** 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: extends model arbitrarily +/** 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 ); + 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 ); }; -//incomplete model class: does not extend model -class IncompleteModel : public TheoryModel -{ -public: - IncompleteModel( context::Context* c, std::string name ) : TheoryModel( c, name ){} - virtual ~IncompleteModel(){} -public: - Node getInterpretedValue( TNode n ) { return Node::null(); } -}; - - +/** 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 */ - virtual Node chooseRepresentative( TheoryModel* tm, Node eqc ); - /** representatives that are current not set */ - virtual void processBuildModel( TheoryModel* tm ); + /** 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. + /** Build model function. + * Should be called only on TheoryModels m */ void buildModel( Model* m ); }; diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index ae5b99c06..316e2fbff 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -24,6 +24,8 @@ libquantifiers_la_SOURCES = \ term_database.h \ term_database.cpp \ first_order_model.h \ - first_order_model.cpp + first_order_model.cpp \ + model_builder.h \ + model_builder.cpp EXTRA_DIST = kinds \ No newline at end of file diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 71a48b33d..766bd31ae 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -17,7 +17,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/rep_set_iterator.h" #include "theory/quantifiers/model_engine.h" -#include "theory/uf/theory_uf_strong_solver.h" +#include "theory/quantifiers/term_database.h" using namespace std; using namespace CVC4; @@ -26,25 +26,37 @@ 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 ), +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::initialize(){ +void FirstOrderModel::reset(){ //rebuild models - d_uf_model.clear(); + 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_ra.d_type_reps.begin(); it != d_ra.d_type_reps.end(); ++it ){ - if( uf::StrongSolverTheoryUf::isRelevantType( it->first ) ){ + 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; } } @@ -54,33 +66,44 @@ void FirstOrderModel::initialize(){ void FirstOrderModel::initializeModelForTerm( Node n ){ if( n.getKind()==APPLY_UF ){ Node op = n.getOperator(); - if( d_uf_model.find( op )==d_uf_model.end() ){ + if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){ TypeNode tn = op.getType(); tn = tn[ (int)tn.getNumChildren()-1 ]; - if( tn==NodeManager::currentNM()->booleanType() || uf::StrongSolverTheoryUf::isRelevantType( tn ) ){ - d_uf_model[ op ] = uf::UfModel( op, this ); + //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.getKind()!=STORE && n.getType().isArray() ){ - d_array_model[n] = Node::null(); + /* + 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() ){ - //out << "(" << n << " " << d_array_model[n] << ")" << std::endl; - // out << "(" << n << " Array)" << std::endl; - }else{ - DefaultModel::toStreamFunction( n, out ); + }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 ){ @@ -91,14 +114,29 @@ 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_model.find( n )!=d_uf_model.end() ){ - return d_uf_model[n].getFunctionValue(); + 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{ - return n; + //std::cout << "no array model generated for " << n << std::endl; } + */ }else if( n.getKind()==APPLY_UF ){ - int depIndex; - return d_uf_model[ n.getOperator() ].getValue( n, depIndex ); + 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 ); } @@ -113,14 +151,14 @@ void FirstOrderModel::toStream(std::ostream& out){ #if 0 out << "---Current Model---" << std::endl; out << "Representatives: " << std::endl; - d_ra.toStream( out ); + 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_ra.toStream( out ); + 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() ){ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 832acbee3..825518ed0 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -21,6 +21,7 @@ #include "theory/model.h" #include "theory/uf/theory_uf_model.h" +#include "theory/arrays/theory_arrays_model.h" namespace CVC4 { namespace theory { @@ -43,6 +44,8 @@ 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 */ @@ -50,10 +53,12 @@ private: void toStreamType( TypeNode tn, std::ostream& out ); public: //for Theory UF: //models for each UF operator - std::map< Node, uf::UfModel > d_uf_model; + 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, Node > d_array_model; + 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; @@ -64,11 +69,13 @@ public: //for Theory Quantifiers: public: FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ); virtual ~FirstOrderModel(){} - // initialize the model - void initialize(); + // 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 */ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp new file mode 100644 index 000000000..9cd5020fb --- /dev/null +++ b/src/theory/quantifiers/model_builder.cpp @@ -0,0 +1,417 @@ +/********************* */ +/*! \file model_builder.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 builder class + **/ + +#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_model.h" +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/arrays/theory_arrays_model.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/model_builder.h" + +//#define ME_PRINT_WARNINGS + +#define RECONSIDER_FUNC_CONSTANT +//#define ONE_QUANT_PER_ROUND_INST_GEN + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) : +TheoryEngineModelBuilder( qe->getTheoryEngine() ), +d_qe( qe ){ + +} + +Node ModelEngineBuilder::chooseRepresentative( TheoryModel* m, Node eqc ){ + Assert( m->d_equalityEngine.hasTerm( eqc ) ); + Assert( m->d_equalityEngine.getRepresentative( eqc )==eqc ); + //avoid interpreted symbols + if( isBadRepresentative( eqc ) ){ + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &m->d_equalityEngine ); + while( !eqc_i.isFinished() ){ + if( !isBadRepresentative( *eqc_i ) ){ + return *eqc_i; + } + ++eqc_i; + } + //otherwise, make new value? + //Message() << "Warning: Bad rep " << eqc << std::endl; + } + return eqc; +} + +bool ModelEngineBuilder::isBadRepresentative( Node n ){ + return n.getKind()==SELECT || n.getKind()==APPLY_SELECTOR; +} + +void ModelEngineBuilder::processBuildModel( TheoryModel* m ) { + d_addedLemmas = 0; + //only construct first order model if optUseModel() is true + if( optUseModel() ){ + FirstOrderModel* fm = (FirstOrderModel*)m; + //initialize model + fm->initialize(); + //analyze the functions + analyzeModel( fm ); + //analyze the quantifiers + Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl; + analyzeQuantifiers( fm ); + //if applicable, find exceptions + if( optInstGen() ){ + //now, see if we know that any exceptions via InstGen exist + Debug("fmf-model-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; + for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + if( d_quant_sat.find( f )==d_quant_sat.end() ){ + d_addedLemmas += doInstGen( fm, f ); + if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){ + break; + } + } + } + if( Options::current()->printModelEngine ){ + if( d_addedLemmas>0 ){ + Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl; + }else{ + Message() << "No InstGen lemmas..." << std::endl; + } + } + Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl; + } + if( d_addedLemmas==0 ){ + //if no immediate exceptions, build the model + // this model will be an approximation that will need to be tested via exhaustive instantiation + Debug("fmf-model-debug") << "Building model..." << std::endl; + finishBuildModel( fm ); + } + } +} + +void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ + //determine if any functions are constant + for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ + Node op = it->first; + for( size_t i=0; id_uf_terms[op].size(); i++ ){ + Node n = fm->d_uf_terms[op][i]; + if( !n.getAttribute(NoMatchAttribute()) ){ + Node v = fm->getRepresentative( n ); + if( i==0 ){ + d_uf_prefs[op].d_const_val = v; + }else if( v!=d_uf_prefs[op].d_const_val ){ + d_uf_prefs[op].d_const_val = Node::null(); + break; + } + } + } + if( !d_uf_prefs[op].d_const_val.isNull() ){ + fm->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val ); + fm->d_uf_model_gen[op].makeModel( fm, it->second ); + Debug("fmf-model-cons") << "Function " << op << " is the constant function "; + fm->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val ); + Debug("fmf-model-cons") << std::endl; + d_uf_model_constructed[op] = true; + }else{ + d_uf_model_constructed[op] = false; + } + } +} + +void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){ + d_quant_selection_lits.clear(); + d_quant_sat.clear(); + d_uf_prefs.clear(); + int quantSatInit = 0; + int nquantSatInit = 0; + //analyze the preferences of each quantifier + for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; + std::vector< Node > pro_con[2]; + std::vector< Node > constantSatOps; + bool constantSatReconsider; + //for each asserted quantifier f, + // - determine which literals form model basis for each quantifier + // - check which function/predicates have good and bad definitions according to f + for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin(); + it != d_qe->d_phase_reqs[f].end(); ++it ){ + Node n = it->first; + Node gn = d_qe->getTermDatabase()->getModelBasis( n ); + Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl; + //calculate preference + int pref = 0; + bool value; + if( d_qe->getValuation().hasSatValue( gn, value ) ){ + if( value!=it->second ){ + //store this literal as a model basis literal + // this literal will force a default values in model that (modulo exceptions) shows + // that f is satisfied by the model + d_quant_selection_lits[f].push_back( value ? n : n.notNode() ); + pref = 1; + }else{ + pref = -1; + } + } + if( pref!=0 ){ + //Store preferences for UF + bool isConst = !n.hasAttribute(InstConstantAttribute()); + std::vector< Node > uf_terms; + if( gn.getKind()==APPLY_UF ){ + uf_terms.push_back( gn ); + isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull(); + }else if( gn.getKind()==EQUAL ){ + isConst = true; + for( int j=0; j<2; j++ ){ + if( n[j].hasAttribute(InstConstantAttribute()) ){ + if( n[j].getKind()==APPLY_UF ){ + Node op = gn[j].getOperator(); + if( fm->d_uf_model_tree.find( op )!=fm->d_uf_model_tree.end() ){ + uf_terms.push_back( gn[j] ); + isConst = isConst && !d_uf_prefs[op].d_const_val.isNull(); + }else{ + isConst = false; + } + }else{ + isConst = false; + } + } + } + } + Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" ); + Debug("fmf-model-prefs") << " the definition of " << n << std::endl; + if( pref==1 && isConst ){ + d_quant_sat[f] = true; + //instead, just note to the model for each uf term that f is pro its definition + constantSatReconsider = false; + constantSatOps.clear(); + for( int j=0; j<(int)uf_terms.size(); j++ ){ + Node op = uf_terms[j].getOperator(); + constantSatOps.push_back( op ); + if( d_uf_prefs[op].d_reconsiderModel ){ + constantSatReconsider = true; + } + } + if( !constantSatReconsider ){ + break; + } + }else{ + int pcIndex = pref==1 ? 0 : 1; + for( int j=0; j<(int)uf_terms.size(); j++ ){ + pro_con[pcIndex].push_back( uf_terms[j] ); + } + } + } + } + if( d_quant_sat.find( f )!=d_quant_sat.end() ){ + Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: "; + for( int i=0; i<(int)constantSatOps.size(); i++ ){ + Debug("fmf-model-prefs") << constantSatOps[i] << " "; + d_uf_prefs[constantSatOps[i]].d_reconsiderModel = false; + } + Debug("fmf-model-prefs") << std::endl; + quantSatInit++; + d_statistics.d_pre_sat_quant += quantSatInit; + }else{ + nquantSatInit++; + d_statistics.d_pre_nsat_quant += quantSatInit; + //note quantifier's value preferences to models + for( int k=0; k<2; k++ ){ + for( int j=0; j<(int)pro_con[k].size(); j++ ){ + Node op = pro_con[k][j].getOperator(); + Node r = fm->getRepresentative( pro_con[k][j] ); + d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); + } + } + } + } + Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl; +} + +int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){ + //we wish to add all known exceptions to our model basis literal(s) + // this will help to refine our current model. + //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms, + // effectively acting as partial instantiations instead of pointwise instantiations. + int addedLemmas = 0; + for( int i=0; i<(int)d_quant_selection_lits[f].size(); i++ ){ + bool phase = d_quant_selection_lits[f][i].getKind()!=NOT; + Node lit = d_quant_selection_lits[f][i].getKind()==NOT ? d_quant_selection_lits[f][i][0] : d_quant_selection_lits[f][i]; + Assert( lit.hasAttribute(InstConstantAttribute()) ); + std::vector< Node > tr_terms; + if( lit.getKind()==APPLY_UF ){ + //only match predicates that are contrary to this one, use literal matching + Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); + fm->getTermDatabase()->setInstantiationConstantAttr( eq, f ); + tr_terms.push_back( eq ); + }else if( lit.getKind()==EQUAL ){ + //collect trigger terms + for( int j=0; j<2; j++ ){ + if( lit[j].hasAttribute(InstConstantAttribute()) ){ + if( lit[j].getKind()==APPLY_UF ){ + tr_terms.push_back( lit[j] ); + }else{ + tr_terms.clear(); + break; + } + } + } + if( tr_terms.size()==1 && !phase ){ + //equality between a function and a ground term, use literal matching + tr_terms.clear(); + tr_terms.push_back( lit ); + } + } + //if applicable, try to add exceptions here + if( !tr_terms.empty() ){ + //make a trigger for these terms, add instantiations + inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms ); + //Notice() << "Trigger = " << (*tr) << std::endl; + tr->resetInstantiationRound(); + tr->reset( Node::null() ); + //d_qe->d_optInstMakeRepresentative = false; + //d_qe->d_optMatchIgnoreModelBasis = true; + addedLemmas += tr->addInstantiations( d_quant_basis_match[f] ); + } + } + return addedLemmas; +} + +void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){ + //build model for UF + for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ + finishBuildModelUf( fm, it->first ); + } + /* + //build model for arrays + for( std::map< Node, arrays::ArrayModel >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){ + //consult the model basis select term + // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term + TypeNode tn = it->first.getType(); + Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) ); + it->second.setDefaultValue( fm->getRepresentative( selModelBasis ) ); + } + */ + Debug("fmf-model-debug") << "Done building models." << std::endl; +} + +void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, Node op ){ +#ifdef RECONSIDER_FUNC_CONSTANT + if( d_uf_model_constructed[op] ){ + if( d_uf_prefs[op].d_reconsiderModel ){ + //if we are allowed to reconsider default value, then see if the default value can be improved + Node v = d_uf_prefs[op].d_const_val; + if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){ + Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl; + fm->d_uf_model_tree[op].clear(); + fm->d_uf_model_gen[op].clear(); + d_uf_model_constructed[op] = false; + } + } + } +#endif + if( !d_uf_model_constructed[op] ){ + //construct the model for the uninterpretted function/predicate + bool setDefaultVal = true; + Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); + Debug("fmf-model-cons") << "Construct model for " << op << "..." << std::endl; + //set the values in the model + for( size_t i=0; id_uf_terms[op].size(); i++ ){ + Node n = fm->d_uf_terms[op][i]; + fm->getTermDatabase()->computeModelBasisArgAttribute( n ); + if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ + Node v = fm->getRepresentative( n ); + //if this assertion did not help the model, just consider it ground + //set n = v in the model tree + Debug("fmf-model-cons") << " Set " << n << " = "; + fm->printRepresentativeDebug( "fmf-model-cons", v ); + Debug("fmf-model-cons") << std::endl; + //set it as ground value + fm->d_uf_model_gen[op].setValue( fm, n, v ); + if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){ + //also set as default value if necessary + //if( n.getAttribute(ModelBasisArgAttribute())==1 && !d_term_pro_con[0][n].empty() ){ + if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){ + fm->d_uf_model_gen[op].setValue( fm, n, v, false ); + if( n==defaultTerm ){ + //incidentally already set, we will not need to find a default value + setDefaultVal = false; + } + } + }else{ + if( n==defaultTerm ){ + fm->d_uf_model_gen[op].setValue( fm, n, v, false ); + //incidentally already set, we will not need to find a default value + setDefaultVal = false; + } + } + } + } + //set the overall default value if not set already (is this necessary??) + if( setDefaultVal ){ + Debug("fmf-model-cons") << " Choose default value..." << std::endl; + //chose defaultVal based on heuristic, currently the best ratio of "pro" responses + Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); + Assert( !defaultVal.isNull() ); + fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); + } + Debug("fmf-model-cons") << " Making model..."; + fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] ); + d_uf_model_constructed[op] = true; + Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; + } +} + +void ModelEngineBuilder::finishProcessBuildModel( TheoryModel* m ){ + for( std::map< Node, Node >::iterator it = m->d_reps.begin(); it != m->d_reps.end(); ++it ){ + //build proper representatives (TODO) + } +} + +bool ModelEngineBuilder::optUseModel() { + return Options::current()->fmfModelBasedInst; +} + +bool ModelEngineBuilder::optInstGen(){ + return Options::current()->fmfInstGen; +} + +bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ +#ifdef ONE_QUANT_PER_ROUND_INST_GEN + return true; +#else + return false; +#endif +} + +ModelEngineBuilder::Statistics::Statistics(): + d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0), + d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0) +{ + StatisticsRegistry::registerStat(&d_pre_sat_quant); + StatisticsRegistry::registerStat(&d_pre_nsat_quant); +} + +ModelEngineBuilder::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_pre_sat_quant); + StatisticsRegistry::unregisterStat(&d_pre_nsat_quant); +} diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h new file mode 100644 index 000000000..13d500d8e --- /dev/null +++ b/src/theory/quantifiers/model_builder.h @@ -0,0 +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 diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 663f270eb..ddaaa5b6f 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -21,16 +21,13 @@ #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/uf/theory_uf_instantiator.h" +#include "theory/arrays/theory_arrays_model.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" //#define ME_PRINT_WARNINGS -//#define DISABLE_EVAL_SKIP_MULTIPLE - -#define RECONSIDER_FUNC_CONSTANT #define EVAL_FAIL_SKIP_MULTIPLE -//#define ONE_QUANT_PER_ROUND_INST_GEN //#define ONE_QUANT_PER_ROUND using namespace std; @@ -41,324 +38,6 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; -ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) : -TheoryEngineModelBuilder( qe->getTheoryEngine() ), -d_qe( qe ){ - -} - -Node ModelEngineBuilder::chooseRepresentative( TheoryModel* tm, Node eqc ){ - return eqc; -} - -void ModelEngineBuilder::processBuildModel( TheoryModel* m ) { - d_addedLemmas = 0; - //only construct first order model if optUseModel() is true - if( optUseModel() ){ - FirstOrderModel* fm = (FirstOrderModel*)m; - //initialize model - fm->initialize(); - //analyze the quantifiers - Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl; - analyzeQuantifiers( fm ); - //if applicable, find exceptions - if( optInstGen() ){ - //now, see if we know that any exceptions via InstGen exist - Debug("fmf-model-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; - for( int i=0; igetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - if( d_quant_sat.find( f )==d_quant_sat.end() ){ - d_addedLemmas += doInstGen( fm, f ); - if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){ - break; - } - } - } - if( Options::current()->printModelEngine ){ - if( d_addedLemmas>0 ){ - Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl; - }else{ - Message() << "No InstGen lemmas..." << std::endl; - } - } - Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl; - } - if( d_addedLemmas==0 ){ - //if no immediate exceptions, build the model - // this model will be an approximation that will need to be tested via exhaustive instantiation - Debug("fmf-model-debug") << "Building model..." << std::endl; - finishBuildModel( fm ); - } - } -} - -void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){ - d_quant_selection_lits.clear(); - d_quant_sat.clear(); - d_uf_prefs.clear(); - int quantSatInit = 0; - int nquantSatInit = 0; - //analyze the preferences of each quantifier - for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; - std::vector< Node > pro_con[2]; - std::vector< Node > constantSatOps; - bool constantSatReconsider; - //for each asserted quantifier f, - // - determine which literals form model basis for each quantifier - // - check which function/predicates have good and bad definitions according to f - for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin(); - it != d_qe->d_phase_reqs[f].end(); ++it ){ - Node n = it->first; - Node gn = d_qe->getTermDatabase()->getModelBasis( n ); - Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl; - //calculate preference - int pref = 0; - bool value; - if( d_qe->getValuation().hasSatValue( gn, value ) ){ - if( value!=it->second ){ - //store this literal as a model basis literal - // this literal will force a default values in model that (modulo exceptions) shows - // that f is satisfied by the model - d_quant_selection_lits[f].push_back( value ? n : n.notNode() ); - pref = 1; - }else{ - pref = -1; - } - } - if( pref!=0 ){ - //Store preferences for UF - bool isConst = !n.hasAttribute(InstConstantAttribute()); - std::vector< Node > uf_terms; - if( gn.getKind()==APPLY_UF ){ - uf_terms.push_back( gn ); - isConst = fm->d_uf_model[gn.getOperator()].isConstant(); - }else if( gn.getKind()==EQUAL ){ - isConst = true; - for( int j=0; j<2; j++ ){ - if( n[j].hasAttribute(InstConstantAttribute()) ){ - if( n[j].getKind()==APPLY_UF ){ - Node op = gn[j].getOperator(); - if( fm->d_uf_model.find( op )!=fm->d_uf_model.end() ){ - uf_terms.push_back( gn[j] ); - isConst = isConst && fm->d_uf_model[op].isConstant(); - }else{ - isConst = false; - } - }else{ - isConst = false; - } - } - } - } - Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" ); - Debug("fmf-model-prefs") << " the definition of " << n << std::endl; - if( pref==1 && isConst ){ - d_quant_sat[f] = true; - //instead, just note to the model for each uf term that f is pro its definition - constantSatReconsider = false; - constantSatOps.clear(); - for( int j=0; j<(int)uf_terms.size(); j++ ){ - Node op = uf_terms[j].getOperator(); - constantSatOps.push_back( op ); - if( d_uf_prefs[op].d_reconsiderModel ){ - constantSatReconsider = true; - } - } - if( !constantSatReconsider ){ - break; - } - }else{ - int pcIndex = pref==1 ? 0 : 1; - for( int j=0; j<(int)uf_terms.size(); j++ ){ - pro_con[pcIndex].push_back( uf_terms[j] ); - } - } - } - } - if( d_quant_sat.find( f )!=d_quant_sat.end() ){ - Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: "; - for( int i=0; i<(int)constantSatOps.size(); i++ ){ - Debug("fmf-model-prefs") << constantSatOps[i] << " "; - d_uf_prefs[constantSatOps[i]].d_reconsiderModel = false; - } - Debug("fmf-model-prefs") << std::endl; - quantSatInit++; - d_statistics.d_pre_sat_quant += quantSatInit; - }else{ - nquantSatInit++; - d_statistics.d_pre_nsat_quant += quantSatInit; - //note quantifier's value preferences to models - for( int k=0; k<2; k++ ){ - for( int j=0; j<(int)pro_con[k].size(); j++ ){ - Node op = pro_con[k][j].getOperator(); - Node r = fm->getRepresentative( pro_con[k][j] ); - d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); - } - } - } - } - Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl; -} - -int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){ - //we wish to add all known exceptions to our model basis literal(s) - // this will help to refine our current model. - //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms, - // effectively acting as partial instantiations instead of pointwise instantiations. - int addedLemmas = 0; - for( int i=0; i<(int)d_quant_selection_lits[f].size(); i++ ){ - bool phase = d_quant_selection_lits[f][i].getKind()!=NOT; - Node lit = d_quant_selection_lits[f][i].getKind()==NOT ? d_quant_selection_lits[f][i][0] : d_quant_selection_lits[f][i]; - Assert( lit.hasAttribute(InstConstantAttribute()) ); - std::vector< Node > tr_terms; - if( lit.getKind()==APPLY_UF ){ - //only match predicates that are contrary to this one, use literal matching - Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); - fm->getTermDatabase()->setInstantiationConstantAttr( eq, f ); - tr_terms.push_back( eq ); - }else if( lit.getKind()==EQUAL ){ - //collect trigger terms - for( int j=0; j<2; j++ ){ - if( lit[j].hasAttribute(InstConstantAttribute()) ){ - if( lit[j].getKind()==APPLY_UF ){ - tr_terms.push_back( lit[j] ); - }else{ - tr_terms.clear(); - break; - } - } - } - if( tr_terms.size()==1 && !phase ){ - //equality between a function and a ground term, use literal matching - tr_terms.clear(); - tr_terms.push_back( lit ); - } - } - //if applicable, try to add exceptions here - if( !tr_terms.empty() ){ - //make a trigger for these terms, add instantiations - Trigger* tr = Trigger::mkTrigger( d_qe, f, tr_terms ); - //Notice() << "Trigger = " << (*tr) << std::endl; - tr->resetInstantiationRound(); - tr->reset( Node::null() ); - //d_qe->d_optInstMakeRepresentative = false; - //d_qe->d_optMatchIgnoreModelBasis = true; - addedLemmas += tr->addInstantiations( d_quant_basis_match[f] ); - } - } - return addedLemmas; -} - -void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){ - //build model for UF - for( std::map< Node, uf::UfModel >::iterator it = fm->d_uf_model.begin(); it != fm->d_uf_model.end(); ++it ){ - finishBuildModelUf( fm, it->second ); - } - //build model for arrays - for( std::map< Node, Node >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){ - //consult the model basis select term - // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term - TypeNode tn = it->first.getType(); - Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) ); - it->second = fm->getRepresentative( selModelBasis ); - } - Debug("fmf-model-debug") << "Done building models." << std::endl; -} - -void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model ){ - Node op = model.getOperator(); -#ifdef RECONSIDER_FUNC_CONSTANT - if( model.isModelConstructed() && model.isConstant() ){ - if( d_uf_prefs[op].d_reconsiderModel ){ - //if we are allowed to reconsider default value, then see if the default value can be improved - Node t = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); - Node v = model.getConstantValue( t ); - if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){ - Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl; - model.clearModel(); - } - } - } -#endif - if( !model.isModelConstructed() ){ - //construct the model for the uninterpretted function/predicate - bool setDefaultVal = true; - Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); - Debug("fmf-model-cons") << "Construct model for " << op << "..." << std::endl; - //set the values in the model - for( size_t i=0; ifmfModelBasedInst; -} - -bool ModelEngineBuilder::optInstGen(){ - return Options::current()->fmfInstGen; -} - -bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ -#ifdef ONE_QUANT_PER_ROUND_INST_GEN - return true; -#else - return false; -#endif -} - -ModelEngineBuilder::Statistics::Statistics(): - d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0), - d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0) -{ - StatisticsRegistry::registerStat(&d_pre_sat_quant); - StatisticsRegistry::registerStat(&d_pre_nsat_quant); -} - -ModelEngineBuilder::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_pre_sat_quant); - StatisticsRegistry::unregisterStat(&d_pre_nsat_quant); -} - //Model Engine constructor ModelEngine::ModelEngine( QuantifiersEngine* qe ) : QuantifiersModule( qe ), @@ -448,6 +127,8 @@ void ModelEngine::check( Theory::Effort e ){ //CVC4 will answer SAT Debug("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); + // finish building the model in the standard way + d_builder.finishProcessBuildModel( d_quantEngine->getModel() ); }else{ //otherwise, the search will continue d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); @@ -601,12 +282,13 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ } } d_statistics.d_eval_formulas += reval.d_eval_formulas; - d_statistics.d_eval_eqs += reval.d_eval_eqs; d_statistics.d_eval_uf_terms += reval.d_eval_uf_terms; + d_statistics.d_eval_lits += reval.d_eval_lits; + d_statistics.d_eval_lits_unknown += reval.d_eval_lits_unknown; int totalInst = 1; int relevantInst = 1; for( size_t i=0; igetModel()->d_ra.d_type_reps[ f[0][i].getType() ].size(); + totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ f[0][i].getType() ].size(); relevantInst = relevantInst * (int)riter.d_domain[i].size(); } d_totalLemmas += totalInst; @@ -658,15 +340,17 @@ void ModelEngine::debugPrint( const char* c ){ ModelEngine::Statistics::Statistics(): d_inst_rounds("ModelEngine::Inst_Rounds", 0), d_eval_formulas("ModelEngine::Eval_Formulas", 0 ), - d_eval_eqs("ModelEngine::Eval_Equalities", 0 ), d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ), + d_eval_lits("ModelEngine::Eval_Lits", 0 ), + d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ), d_num_quants_init("ModelEngine::Num_Quants", 0 ), d_num_quants_init_fail("ModelEngine::Num_Quants_No_Basis", 0 ) { StatisticsRegistry::registerStat(&d_inst_rounds); StatisticsRegistry::registerStat(&d_eval_formulas); - StatisticsRegistry::registerStat(&d_eval_eqs); StatisticsRegistry::registerStat(&d_eval_uf_terms); + StatisticsRegistry::registerStat(&d_eval_lits); + StatisticsRegistry::registerStat(&d_eval_lits_unknown); StatisticsRegistry::registerStat(&d_num_quants_init); StatisticsRegistry::registerStat(&d_num_quants_init_fail); } @@ -674,8 +358,9 @@ ModelEngine::Statistics::Statistics(): ModelEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_inst_rounds); StatisticsRegistry::unregisterStat(&d_eval_formulas); - StatisticsRegistry::unregisterStat(&d_eval_eqs); StatisticsRegistry::unregisterStat(&d_eval_uf_terms); + StatisticsRegistry::unregisterStat(&d_eval_lits); + StatisticsRegistry::unregisterStat(&d_eval_lits_unknown); StatisticsRegistry::unregisterStat(&d_num_quants_init); StatisticsRegistry::unregisterStat(&d_num_quants_init_fail); } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index b01139826..1139332fe 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -11,81 +11,25 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Model Engine classes + ** \brief Model Engine class **/ #include "cvc4_private.h" -#ifndef __CVC4__MODEL_ENGINE_H -#define __CVC4__MODEL_ENGINE_H +#ifndef __CVC4__QUANTIFIERS_MODEL_ENGINE_H +#define __CVC4__QUANTIFIERS_MODEL_ENGINE_H #include "theory/quantifiers_engine.h" -#include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers/model_builder.h" #include "theory/model.h" -#include "theory/uf/theory_uf_model.h" #include "theory/quantifiers/relevant_domain.h" namespace CVC4 { namespace theory { - -namespace uf{ - class StrongSolverTheoryUf; -} - 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; - /** choose representative */ - Node chooseRepresentative( TheoryModel* tm, Node eqc ); - /** use constants for representatives */ - void processBuildModel( TheoryModel* m ); - //analyze quantifiers - void analyzeQuantifiers( FirstOrderModel* fm ); - //build model - void finishBuildModel( FirstOrderModel* fm ); - //theory-specific build models - void finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model ); - //do InstGen techniques for quantifier, return number of lemmas produced - int doInstGen( FirstOrderModel* fm, Node f ); -public: - ModelEngineBuilder( QuantifiersEngine* qe ); - virtual ~ModelEngineBuilder(){} -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; -}; - class ModelEngine : public QuantifiersModule { - friend class uf::UfModel; friend class RepSetIterator; private: /** builder class */ @@ -128,8 +72,9 @@ public: public: IntStat d_inst_rounds; IntStat d_eval_formulas; - IntStat d_eval_eqs; IntStat d_eval_uf_terms; + IntStat d_eval_lits; + IntStat d_eval_lits_unknown; IntStat d_num_quants_init; IntStat d_num_quants_init_fail; Statistics(); diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index e7ae1d1c7..12206e148 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -37,16 +37,16 @@ void RelevantDomain::compute(){ 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::UfModel >::iterator it = d_model->d_uf_model.begin(); - it != d_model->d_uf_model.end(); ++it ){ + 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( int i=0; i<(int)it->second.d_ground_asserts.size(); i++ ){ - Node n = it->second.d_ground_asserts[i]; + 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_ra.hasType( n[j].getType() ) ){ + if( d_model->d_rep_set.hasType( n[j].getType() ) ){ Node ra = d_model->getRepresentative( n[j] ); - int raIndex = d_model->d_ra.getIndexFor( ra ); + 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 ); @@ -54,8 +54,8 @@ void RelevantDomain::compute(){ } } //add to range - Node r = it->second.d_ground_asserts_reps[i]; - int raIndex = d_model->d_ra.getIndexFor( r ); + 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 ); @@ -104,10 +104,10 @@ bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, in if( !domainSet ){ //otherwise, we must consider the entire domain TypeNode tn = n.getType(); - if( d_model->d_ra.hasType( tn ) ){ - if( rd[vi].size()!=d_model->d_ra.d_type_reps[tn].size() ){ + if( d_model->d_rep_set.hasType( tn ) ){ + if( rd[vi].size()!=d_model->d_rep_set.d_type_reps[tn].size() ){ rd[vi].clear(); - for( size_t i=0; id_ra.d_type_reps[tn].size(); i++ ){ + for( size_t i=0; id_rep_set.d_type_reps[tn].size(); i++ ){ rd[vi].push_back( i ); domainChanged = true; } @@ -166,7 +166,7 @@ bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){ } }else{ Node r = d_model->getRepresentative( n ); - range.push_back( d_model->d_ra.getIndexFor( r ) ); + range.push_back( d_model->d_rep_set.getIndexFor( r ) ); } return domainChanged; } diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp index a29f815db..516f85857 100644 --- a/src/theory/quantifiers/rep_set_iterator.cpp +++ b/src/theory/quantifiers/rep_set_iterator.cpp @@ -38,8 +38,28 @@ RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_m d_var_order[i] = i; //store default domain d_domain.push_back( RepDomain() ); - for( int j=0; j<(int)d_model->d_ra.d_type_reps[d_f[0][i].getType()].size(); j++ ){ - d_domain[i].push_back( j ); + TypeNode tn = d_f[0][i].getType(); + if( tn.isSort() ){ + if( d_model->d_rep_set.hasType( tn ) ){ + for( int j=0; j<(int)d_model->d_rep_set.d_type_reps[d_f[0][i].getType()].size(); j++ ){ + d_domain[i].push_back( j ); + } + }else{ + Unimplemented("Cannot create instantiation iterator for unknown uninterpretted sort"); + } + }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ + Unimplemented("Cannot create instantiation iterator for arithmetic quantifier"); + }else if( tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + //if finite, then use type enumerator + if( dt.isFinite() ){ + //DO_THIS: use type enumerator + Unimplemented("Not yet implemented: instantiation iterator for finite datatype quantifier"); + }else{ + Unimplemented("Cannot create instantiation iterator for infinite datatype quantifier"); + } + }else{ + Unimplemented("Cannot create instantiation iterator for quantifier"); } } } @@ -103,9 +123,9 @@ void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){ Node RepSetIterator::getTerm( int i ){ TypeNode tn = d_f[0][d_index_order[i]].getType(); - Assert( d_model->d_ra.d_type_reps.find( tn )!=d_model->d_ra.d_type_reps.end() ); + 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_ra.d_type_reps[tn][d_domain[index][d_index[index]]]; + return d_model->d_rep_set.d_type_reps[tn][d_domain[index][d_index[index]]]; } void RepSetIterator::debugPrint( const char* c ){ @@ -123,14 +143,18 @@ void RepSetIterator::debugPrintSmall( const char* c ){ } 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, phaseReq ) = eVal, -// if eVal = d_riter->d_index.size() -// then the formula n instantiated with d_riter cannot be proven to be equal to phaseReq -// otherwise, -// each n{d_riter->d_index[0]/x_0...d_riter->d_index[eVal]/x_eVal, */x_(eVal+1) ... */x_n } is equal to phaseReq in the current model +//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; @@ -208,6 +232,7 @@ int RepSetEvaluator::evaluate( Node n, int& depIndex ){ }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] ){ @@ -215,89 +240,46 @@ int RepSetEvaluator::evaluate( Node n, int& depIndex ){ // } //} //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl; - //this should be a literal - //Node gn = n.substitute( d_riter->d_ic.begin(), d_riter->d_ic.end(), d_riter->d_terms.begin(), d_riter->d_terms.end() ); - //Debug("fmf-eval-debug") << " Ground version = " << gn << std::endl; int retVal = 0; depIndex = d_riter->getNumTerms()-1; - if( n.getKind()==APPLY_UF ){ - //case for boolean predicates - Node val = evaluateTerm( n, depIndex ); - if( d_model->hasTerm( val ) ){ - if( d_model->areEqual( val, d_model->d_true ) ){ - retVal = 1; - }else{ - retVal = -1; - } - } - }else if( n.getKind()==EQUAL ){ - //case for equality - retVal = evaluateEquality( n[0], n[1], depIndex ); - }else{ - std::vector< int > cdi; - Node val = evaluateTermDefault( n, depIndex, cdi ); - if( !val.isNull() ){ - val = Rewriter::rewrite( val ); - if( val==d_model->d_true ){ - retVal = 1; - }else if( val==d_model->d_false ){ - retVal = -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 << ", depends = " << depIndex << std::endl; + 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; } } -int RepSetEvaluator::evaluateEquality( Node n1, Node n2, int& depIndex ){ - ++d_eval_eqs; - //Notice() << "Eval eq " << n1 << " " << n2 << std::endl; - Debug("fmf-eval-debug") << "Evaluate equality: " << std::endl; - Debug("fmf-eval-debug") << " " << n1 << " = " << n2 << std::endl; - int depIndex1, depIndex2; - Node val1 = evaluateTerm( n1, depIndex1 ); - Node val2 = evaluateTerm( n2, depIndex2 ); - Debug("fmf-eval-debug") << " Values : "; - d_model->printRepresentativeDebug( "fmf-eval-debug", val1 ); - Debug("fmf-eval-debug") << " = "; - d_model->printRepresentativeDebug( "fmf-eval-debug", val2 ); - Debug("fmf-eval-debug") << std::endl; - int retVal = 0; - if( !val1.isNull() && !val2.isNull() ){ - if( d_model->areEqual( val1, val2 ) ){ - retVal = 1; - }else if( d_model->areDisequal( val1, val2 ) ){ - retVal = -1; - }else{ - Node eq = val1.eqNode( val2 ); - eq = Rewriter::rewrite( eq ); - if( eq==d_model->d_true ){ - retVal = 1; - }else if( eq==d_model->d_false ){ - retVal = -1; - } - } - } - if( retVal!=0 ){ - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - Debug("fmf-eval-debug") << " value = " << (retVal==1) << ", depIndex = " << depIndex << std::endl; - }else{ - depIndex = d_riter->getNumTerms()-1; - Debug("fmf-eval-amb") << "Neither equal nor disequal : " << n1 << " , " << n2 << std::endl; - //std::cout << "Neither equal nor disequal : " << n1 << " , " << n2 << std::endl; - } - return retVal; -} - Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){ - //Notice() << "Eval term " << n << std::endl; - if( n.hasAttribute(InstConstantAttribute()) ){ + //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 @@ -311,7 +293,7 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){ if( eval==0 ){ //evaluate children to see if they are the same Node val1 = evaluateTerm( n[ 1 ], depIndex1 ); - Node val2 = evaluateTerm( n[ 1 ], depIndex1 ); + Node val2 = evaluateTerm( n[ 2 ], depIndex2 ); if( val1==val2 ){ val = val1; depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; @@ -323,19 +305,24 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){ depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; } }else{ -#if 0 + std::vector< int > children_depIndex; //for select, pre-process read over writes if( n.getKind()==SELECT ){ - Node selIndex = evaluateTerm( n[1], depIndex ); - if( selIndex.isNull() ){ +#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 = n[0]; + 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 ){ - int tempIndex; - eval = evaluateEquality( selIndex, arr[1], tempIndex ); + eval = evaluate( sel.eqNode( arr[1] ), tempIndex ); depIndex = tempIndex > depIndex ? tempIndex : depIndex; if( eval==1 ){ val = evaluateTerm( arr[2], tempIndex ); @@ -345,90 +332,97 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){ arr = arr[0]; } } - n = NodeManager::currentNM()->mkNode( SELECT, arr, selIndex ); - } + arr = evaluateTerm( arr, tempIndex ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + val = NodeManager::currentNM()->mkNode( SELECT, arr, sel ); +#else + val = evaluateTermDefault( n, depIndex, children_depIndex ); #endif - //default term evaluate : evaluate all children, recreate the value - std::vector< int > children_depIndex; - val = evaluateTermDefault( n, depIndex, children_depIndex ); - //case split on the type of term - 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 - ++d_eval_uf_terms; - int argDepIndex = 0; - if( d_model->d_uf_model.find( op )!=d_model->d_uf_model.end() ){ - //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[op].d_tree.getValue( d_model, val, argDepIndex ); - }else{ - val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex ); - } + }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; - //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe ); - Assert( !val.isNull() ); - }else{ - d_eval_uf_use_default[n] = true; - argDepIndex = (int)n.getNumChildren(); + //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 } - //recalculate the depIndex - depIndex = -1; - for( int i=0; idepIndex ){ - depIndex = children_depIndex[index]; + //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; - }else if( n.getKind()==SELECT ){ - if( d_model->d_array_model.find( n[0] )!=d_model->d_array_model.end() ){ - //consult the default value for the array DO_THIS - //val = Rewriter::rewrite( val ); - //val = d_model->d_array_model[ n[0] ]; - val = Rewriter::rewrite( val ); - }else{ - val = Rewriter::rewrite( val ); - } - }else{ - val = Rewriter::rewrite( val ); } } return val; - }else{ - depIndex = -1; - return n; } } Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){ - //first we must evaluate the arguments - std::vector< Node > children; - if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } depIndex = -1; - //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]; + 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; } - //recreate the value - return NodeManager::currentNM()->mkNode( n.getKind(), children ); } void RepSetEvaluator::clearEvalFailed( int index ){ @@ -443,8 +437,8 @@ void RepSetEvaluator::makeEvalUfModel( Node n ){ makeEvalUfIndexOrder( n ); if( !d_eval_uf_use_default[n] ){ Node op = n.getOperator(); - d_eval_uf_model[n] = uf::UfModelTreeOrdered( op, d_eval_term_index_order[n] ); - d_model->d_uf_model[op].makeModel( d_eval_uf_model[n] ); + 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 ); } diff --git a/src/theory/quantifiers/rep_set_iterator.h b/src/theory/quantifiers/rep_set_iterator.h index 308d09a38..f6312ae5c 100644 --- a/src/theory/quantifiers/rep_set_iterator.h +++ b/src/theory/quantifiers/rep_set_iterator.h @@ -85,7 +85,7 @@ private: 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::UfModelTreeOrdered > d_eval_uf_model; + 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; @@ -103,13 +103,13 @@ public: virtual ~RepSetEvaluator(){} /** evaluate functions */ int evaluate( Node n, int& depIndex ); - int evaluateEquality( Node n1, Node n2, int& depIndex ); Node evaluateTerm( Node n, int& depIndex ); public: //statistics int d_eval_formulas; - int d_eval_eqs; int d_eval_uf_terms; + int d_eval_lits; + int d_eval_lits_unknown; }; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 55715353d..945c82bf9 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -45,7 +45,7 @@ using namespace CVC4::theory::inst; } } -void addTermEfficient( Node n, std::set< Node >& added){ +void TermDb::addTermEfficient( Node n, std::set< Node >& added){ static AvailableInTermDb aitdi; if (Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){ //Already processed but new in this branch @@ -60,70 +60,69 @@ void addTermEfficient( Node n, std::set< Node >& added){ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ - //don't add terms in quantifier bodies + //don't add terms in quantifier bodies if( withinQuant && !Options::current()->registerQuantBodyTerms ){ return; } - if( d_processed.find( n )==d_processed.end() ){ + if( d_processed.find( n )==d_processed.end() ){ ++(d_quantEngine->d_statistics.d_term_in_termdb); d_processed.insert(n); + d_type_map[ n.getType() ].push_back( n ); n.setAttribute(AvailableInTermDb(),true); - //if this is an atomic trigger, consider adding it + //if this is an atomic trigger, consider adding it //Call the children? - if( Trigger::isAtomicTrigger( n ) || n.getKind() == kind::APPLY_CONSTRUCTOR ){ - if( !n.hasAttribute(InstConstantAttribute()) ){ - Debug("term-db") << "register trigger term " << n << std::endl; + if( Trigger::isAtomicTrigger( n ) ){ + if( !n.hasAttribute(InstConstantAttribute()) ){ + Debug("term-db") << "register trigger term " << n << std::endl; //std::cout << "register trigger term " << n << std::endl; - Node op = n.getOperator(); - d_op_map[op].push_back( n ); - d_type_map[ n.getType() ].push_back( n ); + Node op = n.getOperator(); + d_op_map[op].push_back( n ); added.insert( n ); - uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF ); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - addTerm( n[i], added, withinQuant ); - if( Options::current()->efficientEMatching ){ - if( d_parents[n[i]][op].empty() ){ - //must add parent to equivalence class info - Node nir = d_ith->getRepresentative( n[i] ); - uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir ); - if( eci_nir ){ - eci_nir->d_pfuns[ op ] = true; - } - } - //add to parent structure - if( std::find( d_parents[n[i]][op][i].begin(), d_parents[n[i]][op][i].end(), n )==d_parents[n[i]][op][i].end() ){ - d_parents[n[i]][op][i].push_back( n ); + uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF ); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + addTerm( n[i], added, withinQuant ); + if( Options::current()->efficientEMatching ){ + if( d_parents[n[i]][op].empty() ){ + //must add parent to equivalence class info + Node nir = d_ith->getRepresentative( n[i] ); + uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir ); + if( eci_nir ){ + eci_nir->d_pfuns[ op ] = true; + } + } + //add to parent structure + if( std::find( d_parents[n[i]][op][i].begin(), d_parents[n[i]][op][i].end(), n )==d_parents[n[i]][op][i].end() ){ + d_parents[n[i]][op][i].push_back( n ); Assert(!getParents(n[i],op,i).empty()); - } - } - if( Options::current()->eagerInstQuant ){ - if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){ - int addedLemmas = 0; - for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){ - addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n ); - } - //Message() << "Terms, added lemmas: " << addedLemmas << std::endl; - d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->getTheory( THEORY_QUANTIFIERS )->getOutputChannel() ); - } - } - } - } + } + } + if( Options::current()->eagerInstQuant ){ + if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){ + int addedLemmas = 0; + for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){ + addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n ); + } + //Message() << "Terms, added lemmas: " << addedLemmas << std::endl; + d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->getTheory( THEORY_QUANTIFIERS )->getOutputChannel() ); + } + } + } + } }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - addTerm( n[i], added, withinQuant ); - } - } + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + addTerm( n[i], added, withinQuant ); + } + } }else{ - if( Options::current()->efficientEMatching && - !n.hasAttribute(InstConstantAttribute())){ - //Efficient e-matching must be notified - //The term in triggers are not important here - Debug("term-db") << "New in this branch term " << n << std::endl; - addTermEfficient(n,added); - } - } -}; + if( Options::current()->efficientEMatching && !n.hasAttribute(InstConstantAttribute())){ + //Efficient e-matching must be notified + //The term in triggers are not important here + Debug("term-db") << "New in this branch term " << n << std::endl; + addTermEfficient(n,added); + } + } +} void TermDb::reset( Theory::Effort effort ){ int nonCongruentCount = 0; @@ -158,7 +157,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ for( int i=0; i<2; i++ ){ Node n = NodeManager::currentNM()->mkConst( i==1 ); eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getRepresentative( n ), - ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() ); + d_quantEngine->getEqualityQuery()->getEngine() ); while( !eqc.isFinished() ){ Node en = (*eqc); if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){ @@ -194,12 +193,18 @@ void TermDb::registerModelBasis( Node n, Node gn ){ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){ - std::stringstream ss; - ss << Expr::setlanguage(Options::current()->outputLanguage); - ss << "e_" << tn; - d_model_basis_term[tn] = NodeManager::currentNM()->mkVar( ss.str(), tn ); + Node mbt; + if( d_type_map[ tn ].empty() ){ + std::stringstream ss; + ss << Expr::setlanguage(Options::current()->outputLanguage); + ss << "e_" << tn; + mbt = NodeManager::currentNM()->mkVar( ss.str(), tn ); + }else{ + mbt = d_type_map[ tn ][ 0 ]; + } ModelBasisAttribute mba; - d_model_basis_term[tn].setAttribute(mba,true); + mbt.setAttribute(mba,true); + d_model_basis_term[tn] = mbt; } return d_model_basis_term[tn]; } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 5004a82dc..1ebba49b5 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -68,6 +68,9 @@ public: 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 diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 448224b81..471bc9ac1 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/rr_candidate_generator.h" using namespace std; using namespace CVC4; @@ -720,6 +721,30 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a ){ return d_qe->getInstantiator( THEORY_UF )->getInternalRepresentative( a ); } +eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ + return ((uf::TheoryUF*)d_qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine(); +} + +void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ + eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine(); + if( ee->hasTerm( a ) ){ + Node rep = ee->getRepresentative( a ); + eq::EqClassIterator eqc_iter( rep, ee ); + while( !eqc_iter.isFinished() ){ + eqc.push_back( *eqc_iter ); + eqc_iter++; + } + } + for( theory::TheoryId i=theory::THEORY_FIRST; igetInstantiator( i ) ){ + d_qe->getInstantiator( i )->getEquivalenceClass( a, eqc ); + } + } + if( eqc.empty() ){ + eqc.push_back( a ); + } +} + inst::EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) { /** Should use skeleton (in order to have the type and the kind or any needed other information) instead of only the type */ @@ -745,171 +770,6 @@ inst::EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) { } -// // Just iterate amoung the equivalence class of the given node -// // node::Null() *can't* be given to reset -// class CandidateGeneratorClassGeneric : public CandidateGenerator{ -// private: -// //instantiator pointer -// EqualityEngine* d_ee; -// //the equality class iterator -// eq::EqClassIterator d_eqc; -// /* For the case where the given term doesn't exists in uf */ -// Node d_retNode; -// public: -// CandidateGeneratorTheoryEeClass( EqualityEngine* ee): d_ee( ee ){} -// ~CandidateGeneratorTheoryEeClass(){} -// void resetInstantiationRound(){}; -// void reset( TNode eqc ){ -// Assert(!eqc.isNull()); -// if( d_ee->hasTerm( eqc ) ){ -// /* eqc is in uf */ -// eqc = d_ee->getRepresentative( eqc ); -// d_eqc = eq::EqClassIterator( eqc, d_ee ); -// d_retNode = Node::null(); -// }else{ -// /* If eqc if not a term known by uf, it is the only one in its -// equivalence class. So we will return only it */ -// d_retNode = eqc; -// d_eqc = eq::EqClassIterator(); -// } -// }; //* the argument is not used -// TNode getNextCandidate(){ -// if(d_retNode.isNull()){ -// if( !d_eqc.isFinished() ) return (*(d_eqc++)); -// else return Node::null(); -// }else{ -// /* the case where eqc not in uf */ -// Node ret = d_retNode; -// d_retNode = Node::null(); /* d_eqc.isFinished() must be true */ -// return ret; -// } -// }; -// }; - - -class GenericCandidateGeneratorClasses: public rrinst::CandidateGenerator{ - - /** The candidate generators */ - rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST]; - /** The current theory which candidategenerator is used */ - TheoryId d_can_gen_id; - -public: - GenericCandidateGeneratorClasses(QuantifiersEngine * qe){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(qe->getInstantiator(i) != NULL) - d_can_gen[i] = qe->getInstantiator(i)->getRRCanGenClasses(); - else d_can_gen[i] = NULL; - }; - } - - ~GenericCandidateGeneratorClasses(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - delete(d_can_gen[i]); - }; - } - - void resetInstantiationRound(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); - }; - d_can_gen_id=THEORY_FIRST; - } - - void reset(TNode eqc){ - Assert(eqc.isNull()); - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); - }; - d_can_gen_id=THEORY_FIRST; - lookForNextTheory(); - } - - TNode getNextCandidate(){ - Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); - /** No more */ - if(d_can_gen_id == THEORY_LAST) return TNode::null(); - /** Try with this theory */ - TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); - if( !cand.isNull() ) return cand; - lookForNextTheory(); - return getNextCandidate(); - } - - void lookForNextTheory(){ - do{ /* look for the next available generator */ - ++d_can_gen_id; - } while( d_can_gen_id < THEORY_LAST && d_can_gen[d_can_gen_id] == NULL); - } - -}; - -class GenericCandidateGeneratorClass: public rrinst::CandidateGenerator{ - - /** The candidate generators */ - rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST]; - /** The current theory which candidategenerator is used */ - TheoryId d_can_gen_id; - /** current node to look for equivalence class */ - Node d_node; - /** QuantifierEngine */ - QuantifiersEngine* d_qe; - -public: - GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) { - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_qe->getInstantiator(i) != NULL) - d_can_gen[i] = d_qe->getInstantiator(i)->getRRCanGenClass(); - else d_can_gen[i] = NULL; - }; - } - - ~GenericCandidateGeneratorClass(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - delete(d_can_gen[i]); - }; - } - - void resetInstantiationRound(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); - }; - d_can_gen_id=THEORY_FIRST; - } - - void reset(TNode eqc){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); - }; - d_can_gen_id=THEORY_FIRST; - d_node = eqc; - lookForNextTheory(); - } - - TNode getNextCandidate(){ - Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); - /** No more */ - if(d_can_gen_id == THEORY_LAST) return TNode::null(); - /** Try with this theory */ - TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); - if( !cand.isNull() ) return cand; - lookForNextTheory(); - return getNextCandidate(); - } - - void lookForNextTheory(){ - do{ /* look for the next available generator, where the element is */ - ++d_can_gen_id; - } while( - d_can_gen_id < THEORY_LAST && - (d_can_gen[d_can_gen_id] == NULL || - !d_qe->getInstantiator( d_can_gen_id )->hasTerm( d_node )) - ); - } - -}; - - rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses() { return new GenericCandidateGeneratorClasses(this); } @@ -932,4 +792,4 @@ rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) { // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass(); // else return eq; return getRRCanGenClass(); -} +} \ No newline at end of file diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 157c0ac53..2ae620e3d 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -342,6 +342,8 @@ public: bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); Node getInternalRepresentative( Node a ); + eq::EqualityEngine* getEngine(); + void getEquivalenceClass( Node a, std::vector< Node >& eqc ); }; /* EqualityQueryQuantifiersEngine */ }/* CVC4::theory namespace */ diff --git a/src/theory/rr_candidate_generator.cpp b/src/theory/rr_candidate_generator.cpp new file mode 100644 index 000000000..a2e895c7f --- /dev/null +++ b/src/theory/rr_candidate_generator.cpp @@ -0,0 +1,125 @@ +/********************* */ +/*! \file rr_candidate_generator.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: bobot + ** 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 rr candidate generator class + **/ + +#include "theory/rr_candidate_generator.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.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::rrinst; + +GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(qe->getInstantiator(i) != NULL) + d_can_gen[i] = qe->getInstantiator(i)->getRRCanGenClasses(); + else d_can_gen[i] = NULL; + } +} + +GenericCandidateGeneratorClasses::~GenericCandidateGeneratorClasses(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + delete(d_can_gen[i]); + } +} + +void GenericCandidateGeneratorClasses::resetInstantiationRound(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); + } + d_can_gen_id=THEORY_FIRST; +} + +void GenericCandidateGeneratorClasses::reset(TNode eqc){ + Assert(eqc.isNull()); + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); + } + d_can_gen_id=THEORY_FIRST; + lookForNextTheory(); +} + +TNode GenericCandidateGeneratorClasses::getNextCandidate(){ + Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); + /** No more */ + if(d_can_gen_id == THEORY_LAST) return TNode::null(); + /** Try with this theory */ + TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); + if( !cand.isNull() ) return cand; + lookForNextTheory(); + return getNextCandidate(); +} + +void GenericCandidateGeneratorClasses::lookForNextTheory(){ + do{ /* look for the next available generator */ + ++d_can_gen_id; + } while( d_can_gen_id < THEORY_LAST && d_can_gen[d_can_gen_id] == NULL); +} + +GenericCandidateGeneratorClass::GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) { + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_qe->getInstantiator(i) != NULL) + d_can_gen[i] = d_qe->getInstantiator(i)->getRRCanGenClass(); + else d_can_gen[i] = NULL; + } +} + +GenericCandidateGeneratorClass::~GenericCandidateGeneratorClass(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + delete(d_can_gen[i]); + } +} + +void GenericCandidateGeneratorClass::resetInstantiationRound(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); + } + d_can_gen_id=THEORY_FIRST; +} + +void GenericCandidateGeneratorClass::reset(TNode eqc){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); + } + d_can_gen_id=THEORY_FIRST; + d_node = eqc; + lookForNextTheory(); +} + +TNode GenericCandidateGeneratorClass::getNextCandidate(){ + Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); + /** No more */ + if(d_can_gen_id == THEORY_LAST) return TNode::null(); + /** Try with this theory */ + TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); + if( !cand.isNull() ) return cand; + lookForNextTheory(); + return getNextCandidate(); +} + +void GenericCandidateGeneratorClass::lookForNextTheory(){ + do{ /* look for the next available generator, where the element is */ + ++d_can_gen_id; + } while( + d_can_gen_id < THEORY_LAST && + (d_can_gen[d_can_gen_id] == NULL || + !d_qe->getInstantiator( d_can_gen_id )->hasTerm( d_node )) + ); +} diff --git a/src/theory/rr_candidate_generator.h b/src/theory/rr_candidate_generator.h new file mode 100644 index 000000000..30f6c067d --- /dev/null +++ b/src/theory/rr_candidate_generator.h @@ -0,0 +1,209 @@ +/********************* */ +/*! \file rr_candidate_generator.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: bobot + ** 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 rr candidate generator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H +#define __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/term_database.h" +#include "theory/rr_inst_match.h" + +using namespace CVC4::theory::quantifiers; + +namespace CVC4 { +namespace theory { +namespace eq { + +namespace rrinst{ +typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; + +//New CandidateGenerator. They have a simpler semantic than the old one + +// Just iterate amoung the equivalence classes +// node::Null() must be given to reset +class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{ +private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equalityengine pointer + EqualityEngine* d_ee; +public: + CandidateGeneratorTheoryEeClasses( EqualityEngine * ee): d_ee( ee ){} + ~CandidateGeneratorTheoryEeClasses(){} + void resetInstantiationRound(){}; + void reset( TNode eqc ){ + Assert(eqc.isNull()); + d_eq = eq::EqClassesIterator( d_ee ); + }; //* the argument is not used + TNode getNextCandidate(){ + if( !d_eq.isFinished() ) return (*(d_eq++)); + else return Node::null(); + }; +}; + +// Just iterate amoung the equivalence class of the given node +// node::Null() *can't* be given to reset +class CandidateGeneratorTheoryEeClass : public CandidateGenerator{ +private: + //instantiator pointer + EqualityEngine* d_ee; + //the equality class iterator + eq::EqClassIterator d_eqc; + /* For the case where the given term doesn't exists in uf */ + Node d_retNode; +public: + CandidateGeneratorTheoryEeClass( EqualityEngine* ee): d_ee( ee ){} + ~CandidateGeneratorTheoryEeClass(){} + void resetInstantiationRound(){}; + void reset( TNode eqc ){ + Assert(!eqc.isNull()); + if( d_ee->hasTerm( eqc ) ){ + /* eqc is in uf */ + eqc = d_ee->getRepresentative( eqc ); + d_eqc = eq::EqClassIterator( eqc, d_ee ); + d_retNode = Node::null(); + }else{ + /* If eqc if not a term known by uf, it is the only one in its + equivalence class. So we will return only it */ + d_retNode = eqc; + d_eqc = eq::EqClassIterator(); + } + }; //* the argument is not used + TNode getNextCandidate(){ + if(d_retNode.isNull()){ + if( !d_eqc.isFinished() ) return (*(d_eqc++)); + else return Node::null(); + }else{ + /* the case where eqc not in uf */ + Node ret = d_retNode; + d_retNode = Node::null(); /* d_eqc.isFinished() must be true */ + return ret; + } + }; +}; + + +} /* namespace rrinst */ +} /* namespace eq */ + +namespace uf{ +namespace rrinst { + +typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; + +class CandidateGeneratorTheoryUfOp : public CandidateGenerator{ +private: + Node d_op; + //instantiator pointer + TermDb* d_tdb; + // Since new term can appears we restrict ourself to the one that + // exists at resetInstantiationRound + size_t d_term_iter_limit; + size_t d_term_iter; +public: + CandidateGeneratorTheoryUfOp(Node op, TermDb* tdb): d_op(op), d_tdb( tdb ){} + ~CandidateGeneratorTheoryUfOp(){} + void resetInstantiationRound(){ + d_term_iter_limit = d_tdb->d_op_map[d_op].size(); + }; + void reset( TNode eqc ){ + Assert(eqc.isNull()); + d_term_iter = 0; + }; //* the argument is not used + TNode getNextCandidate(){ + if( d_term_iterd_op_map[d_op][d_term_iter]; + ++d_term_iter; + return n; + } else return Node::null(); + }; +}; + +class CandidateGeneratorTheoryUfType : public CandidateGenerator{ +private: + TypeNode d_type; + //instantiator pointer + TermDb* d_tdb; + // Since new term can appears we restrict ourself to the one that + // exists at resetInstantiationRound + size_t d_term_iter_limit; + size_t d_term_iter; +public: + CandidateGeneratorTheoryUfType(TypeNode type, TermDb* tdb): d_type(type), d_tdb( tdb ){} + ~CandidateGeneratorTheoryUfType(){} + void resetInstantiationRound(){ + d_term_iter_limit = d_tdb->d_type_map[d_type].size(); + }; + void reset( TNode eqc ){ + Assert(eqc.isNull()); + d_term_iter = 0; + }; //* the argument is not used + TNode getNextCandidate(){ + if( d_term_iterd_type_map[d_type][d_term_iter]; + ++d_term_iter; + return n; + } else return Node::null(); + }; +}; + +} /* namespace rrinst */ +} /* namespace uf */ + +class GenericCandidateGeneratorClasses: public rrinst::CandidateGenerator{ + + /** The candidate generators */ + rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST]; + /** The current theory which candidategenerator is used */ + TheoryId d_can_gen_id; + +public: + GenericCandidateGeneratorClasses(QuantifiersEngine * qe); + ~GenericCandidateGeneratorClasses(); + + void resetInstantiationRound(); + void reset(TNode eqc); + TNode getNextCandidate(); + void lookForNextTheory(); +}; + +class GenericCandidateGeneratorClass: public rrinst::CandidateGenerator{ + + /** The candidate generators */ + rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST]; + /** The current theory which candidategenerator is used */ + TheoryId d_can_gen_id; + /** current node to look for equivalence class */ + Node d_node; + /** QuantifierEngine */ + QuantifiersEngine* d_qe; + +public: + GenericCandidateGeneratorClass(QuantifiersEngine * qe); + ~GenericCandidateGeneratorClass(); + void resetInstantiationRound(); + + void reset(TNode eqc); + TNode getNextCandidate(); + void lookForNextTheory(); +}; + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */ diff --git a/src/theory/rr_inst_match.cpp b/src/theory/rr_inst_match.cpp index 3ba0c8d32..287f7475a 100644 --- a/src/theory/rr_inst_match.cpp +++ b/src/theory/rr_inst_match.cpp @@ -15,16 +15,16 @@ **/ #include "theory/inst_match.h" -#include "theory/rr_inst_match.h" -#include "theory/rr_trigger.h" -#include "theory/rr_inst_match_impl.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_instantiator.h" -#include "theory/uf/theory_uf_candidate_generator.h" -#include "theory/datatypes/theory_datatypes_candidate_generator.h" #include "theory/uf/equality_engine.h" #include "theory/arrays/theory_arrays.h" +#include "theory/datatypes/theory_datatypes.h" +#include "theory/rr_inst_match.h" +#include "theory/rr_trigger.h" +#include "theory/rr_inst_match_impl.h" +#include "theory/rr_candidate_generator.h" using namespace CVC4; using namespace CVC4::kind; @@ -437,8 +437,7 @@ class OpMatcher: public Matcher{ AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); /** Iter on the equivalence class of the given term */ uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )); - eq::EqualityEngine* ee = - static_cast(uf->getEqualityEngine()); + eq::EqualityEngine* ee = static_cast(uf->getEqualityEngine()); CandidateGeneratorTheoryEeClass cdtUfEq(ee); /* Create a matcher from the candidate generator */ AuxMatcher1 am1(cdtUfEq,am2); @@ -474,7 +473,7 @@ class DatatypesMatcher: public Matcher{ /* The matcher */ typedef ApplyMatcher AuxMatcher3; typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2; - typedef CandidateGeneratorMatcher< datatypes::rrinst::CandidateGeneratorTheoryClass, AuxMatcher2> AuxMatcher1; + typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1; AuxMatcher1 d_cgm; static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ Assert( pat.getKind() == kind::APPLY_CONSTRUCTOR, @@ -485,7 +484,8 @@ class DatatypesMatcher: public Matcher{ AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); /** Iter on the equivalence class of the given term */ datatypes::TheoryDatatypes* dt = static_cast(qe->getTheoryEngine()->getTheory( theory::THEORY_DATATYPES )); - datatypes::rrinst::CandidateGeneratorTheoryClass cdtDtEq(dt); + eq::EqualityEngine* ee = static_cast(dt->getEqualityEngine()); + CandidateGeneratorTheoryEeClass cdtDtEq(ee); /* Create a matcher from the candidate generator */ AuxMatcher1 am1(cdtDtEq,am2); return am1; diff --git a/src/theory/rr_inst_match_impl.h b/src/theory/rr_inst_match_impl.h index 04a15d41f..28bc8c7eb 100644 --- a/src/theory/rr_inst_match_impl.h +++ b/src/theory/rr_inst_match_impl.h @@ -22,7 +22,7 @@ #include "theory/rr_inst_match.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" -#include "theory/uf/theory_uf_candidate_generator.h" +#include "theory/rr_candidate_generator.h" #include "theory/uf/equality_engine.h" namespace CVC4 { diff --git a/src/theory/rr_trigger.cpp b/src/theory/rr_trigger.cpp index 579608b59..52e7efcc2 100644 --- a/src/theory/rr_trigger.cpp +++ b/src/theory/rr_trigger.cpp @@ -18,7 +18,7 @@ #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_instantiator.h" -#include "theory/uf/theory_uf_candidate_generator.h" +#include "theory/rr_candidate_generator.h" #include "theory/uf/equality_engine.h" using namespace std; diff --git a/src/theory/theory.h b/src/theory/theory.h index 0cf7a8774..24551637b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -777,6 +777,10 @@ public: std::ostream& operator<<(std::ostream& os, Theory::Effort level); +namespace eq{ + class EqualityEngine; +} + class Instantiator { friend class QuantifiersEngine; protected: @@ -838,6 +842,8 @@ public: virtual bool areDisequal( Node a, Node b ) { return false; } virtual Node getRepresentative( Node a ) { return a; } virtual Node getInternalRepresentative( Node a ) { return getRepresentative( a ); } + virtual eq::EqualityEngine* getEqualityEngine() { return NULL; } + virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) {} public: /** A Creator of CandidateGenerator for classes (one element in each equivalence class) and class (every element of one equivalence diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 872924385..1fb7305d4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -86,7 +86,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_quantEngine = new QuantifiersEngine(context, this); //build model information if applicable - d_curr_model = new theory::DefaultModel( context, "DefaultModel" ); + d_curr_model = new theory::DefaultModel( context, "DefaultModel", false ); d_curr_model_builder = new theory::TheoryEngineModelBuilder( this ); Rewriter::init(); @@ -409,8 +409,8 @@ void TheoryEngine::combineTheories() { Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst()); Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst()); - Assert(!d_sharedTerms.areEqual(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); - Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); + //AJR-temp Assert(!d_sharedTerms.areEqual(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); + //AJR-temp Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); // The equality in question Node equality = carePair.a < carePair.b ? diff --git a/src/theory/trigger.cpp b/src/theory/trigger.cpp index 14ba88ba1..92573d464 100644 --- a/src/theory/trigger.cpp +++ b/src/theory/trigger.cpp @@ -18,7 +18,7 @@ #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_instantiator.h" -#include "theory/uf/theory_uf_candidate_generator.h" +#include "theory/candidate_generator.h" #include "theory/uf/equality_engine.h" using namespace std; @@ -284,7 +284,8 @@ bool Trigger::isUsableTrigger( Node n, Node f ){ } bool Trigger::isAtomicTrigger( Node n ){ - return n.getKind()==APPLY_UF || n.getKind()==SELECT || n.getKind()==STORE; + return n.getKind()==APPLY_UF || n.getKind()==SELECT || n.getKind()==STORE || + n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER; } bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index b8446761c..61330bbde 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -19,11 +19,9 @@ libuf_la_SOURCES = \ theory_uf_instantiator.cpp \ theory_uf_strong_solver.h \ theory_uf_strong_solver.cpp \ - theory_uf_candidate_generator.h \ - theory_uf_candidate_generator.cpp \ inst_strategy.h \ inst_strategy.cpp \ theory_uf_model.h \ - theory_uf_model.cpp + theory_uf_model.cpp EXTRA_DIST = kinds diff --git a/src/theory/uf/theory_uf_candidate_generator.cpp b/src/theory/uf/theory_uf_candidate_generator.cpp deleted file mode 100644 index 80151d1e1..000000000 --- a/src/theory/uf/theory_uf_candidate_generator.cpp +++ /dev/null @@ -1,182 +0,0 @@ -/********************* */ -/*! \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/uf/theory_uf_candidate_generator.h" -#include "theory/theory_engine.h" -#include "theory/uf/theory_uf.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::uf; - -namespace CVC4{ -namespace theory{ -namespace uf{ -namespace inst{ - -CandidateGeneratorTheoryUf::CandidateGeneratorTheoryUf( InstantiatorTheoryUf* ith, Node op ) : - d_op( op ), d_ith( ith ), d_term_iter( -2 ){ - Assert( !d_op.isNull() ); -} -void CandidateGeneratorTheoryUf::resetInstantiationRound(){ - d_term_iter_limit = d_ith->getQuantifiersEngine()->getTermDatabase()->d_op_map[d_op].size(); -} - -void CandidateGeneratorTheoryUf::reset( Node eqc ){ - if( eqc.isNull() ){ - d_term_iter = 0; - }else{ - //create an equivalence class iterator in eq class eqc - if( ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->hasTerm( eqc ) ){ - eqc = ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->getRepresentative( eqc ); - d_eqc = eq::EqClassIterator( eqc, ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() ); - d_retNode = Node::null(); - }else{ - d_retNode = eqc; - - } - d_term_iter = -1; - } -} - -Node CandidateGeneratorTheoryUf::getNextCandidate(){ - if( d_term_iter>=0 ){ - //get next candidate term in the uf term database - while( d_term_itergetQuantifiersEngine()->getTermDatabase()->d_op_map[d_op][d_term_iter]; - d_term_iter++; - if( isLegalCandidate( n ) ){ - return n; - } - } - }else if( d_term_iter==-1 ){ - if( d_retNode.isNull() ){ - //get next candidate term in equivalence class - while( !d_eqc.isFinished() ){ - Node n = (*d_eqc); - ++d_eqc; - if( n.getKind()==APPLY_UF && 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(); -} - - -//CandidateGeneratorTheoryUfDisequal::CandidateGeneratorTheoryUfDisequal( InstantiatorTheoryUf* ith, Node eqc ) : -// d_ith( ith ), d_eq_class( eqc ){ -// d_eci = NULL; -//} -//void CandidateGeneratorTheoryUfDisequal::resetInstantiationRound(){ -// -//} -////we will iterate over all terms that are disequal from eqc -//void CandidateGeneratorTheoryUfDisequal::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 CandidateGeneratorTheoryUfDisequal::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(); -//} - - -CandidateGeneratorTheoryUfLitEq::CandidateGeneratorTheoryUfLitEq( InstantiatorTheoryUf* ith, Node mpat ) : - d_match_pattern( mpat ), d_ith( ith ){ - -} -void CandidateGeneratorTheoryUfLitEq::resetInstantiationRound(){ - -} -void CandidateGeneratorTheoryUfLitEq::reset( Node eqc ){ - d_eq = eq::EqClassesIterator( ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() ); -} -Node CandidateGeneratorTheoryUfLitEq::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(); -} - - -CandidateGeneratorTheoryUfLitDeq::CandidateGeneratorTheoryUfLitDeq( InstantiatorTheoryUf* ith, Node mpat ) : - d_match_pattern( mpat ), d_ith( ith ){ - -} -void CandidateGeneratorTheoryUfLitDeq::resetInstantiationRound(){ - -} -void CandidateGeneratorTheoryUfLitDeq::reset( Node eqc ){ - Node false_term = ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->getRepresentative( - NodeManager::currentNM()->mkConst(false) ); - d_eqc_false = eq::EqClassIterator( false_term, ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() ); -} -Node CandidateGeneratorTheoryUfLitDeq::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/uf/theory_uf_candidate_generator.h b/src/theory/uf/theory_uf_candidate_generator.h deleted file mode 100644 index a06f04f99..000000000 --- a/src/theory/uf/theory_uf_candidate_generator.h +++ /dev/null @@ -1,260 +0,0 @@ -/********************* */ -/*! \file theory_uf_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__THEORY_UF_CANDIDATE_GENERATOR_H -#define __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H - -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/term_database.h" -#include "theory/uf/theory_uf_instantiator.h" -#include "theory/rr_inst_match.h" - -using namespace CVC4::theory::quantifiers; - -namespace CVC4 { -namespace theory { -namespace eq { - -namespace rrinst{ -typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; - -//New CandidateGenerator. They have a simpler semantic than the old one - -// Just iterate amoung the equivalence classes -// node::Null() must be given to reset -class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{ -private: - //the equality classes iterator - eq::EqClassesIterator d_eq; - //equalityengine pointer - EqualityEngine* d_ee; -public: - CandidateGeneratorTheoryEeClasses( EqualityEngine * ee): d_ee( ee ){} - ~CandidateGeneratorTheoryEeClasses(){} - void resetInstantiationRound(){}; - void reset( TNode eqc ){ - Assert(eqc.isNull()); - d_eq = eq::EqClassesIterator( d_ee ); - }; //* the argument is not used - TNode getNextCandidate(){ - if( !d_eq.isFinished() ) return (*(d_eq++)); - else return Node::null(); - }; -}; - -// Just iterate amoung the equivalence class of the given node -// node::Null() *can't* be given to reset -class CandidateGeneratorTheoryEeClass : public CandidateGenerator{ -private: - //instantiator pointer - EqualityEngine* d_ee; - //the equality class iterator - eq::EqClassIterator d_eqc; - /* For the case where the given term doesn't exists in uf */ - Node d_retNode; -public: - CandidateGeneratorTheoryEeClass( EqualityEngine* ee): d_ee( ee ){} - ~CandidateGeneratorTheoryEeClass(){} - void resetInstantiationRound(){}; - void reset( TNode eqc ){ - Assert(!eqc.isNull()); - if( d_ee->hasTerm( eqc ) ){ - /* eqc is in uf */ - eqc = d_ee->getRepresentative( eqc ); - d_eqc = eq::EqClassIterator( eqc, d_ee ); - d_retNode = Node::null(); - }else{ - /* If eqc if not a term known by uf, it is the only one in its - equivalence class. So we will return only it */ - d_retNode = eqc; - d_eqc = eq::EqClassIterator(); - } - }; //* the argument is not used - TNode getNextCandidate(){ - if(d_retNode.isNull()){ - if( !d_eqc.isFinished() ) return (*(d_eqc++)); - else return Node::null(); - }else{ - /* the case where eqc not in uf */ - Node ret = d_retNode; - d_retNode = Node::null(); /* d_eqc.isFinished() must be true */ - return ret; - } - }; -}; - - -} /* namespace rrinst */ -} /* namespace eq */ - -namespace uf { -namespace rrinst { - -typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; - -class CandidateGeneratorTheoryUfOp : public CandidateGenerator{ -private: - Node d_op; - //instantiator pointer - TermDb* d_tdb; - // Since new term can appears we restrict ourself to the one that - // exists at resetInstantiationRound - size_t d_term_iter_limit; - size_t d_term_iter; -public: - CandidateGeneratorTheoryUfOp(Node op, TermDb* tdb): d_op(op), d_tdb( tdb ){} - ~CandidateGeneratorTheoryUfOp(){} - void resetInstantiationRound(){ - d_term_iter_limit = d_tdb->d_op_map[d_op].size(); - }; - void reset( TNode eqc ){ - Assert(eqc.isNull()); - d_term_iter = 0; - }; //* the argument is not used - TNode getNextCandidate(){ - if( d_term_iterd_op_map[d_op][d_term_iter]; - ++d_term_iter; - return n; - } else return Node::null(); - }; -}; - -class CandidateGeneratorTheoryUfType : public CandidateGenerator{ -private: - TypeNode d_type; - //instantiator pointer - TermDb* d_tdb; - // Since new term can appears we restrict ourself to the one that - // exists at resetInstantiationRound - size_t d_term_iter_limit; - size_t d_term_iter; -public: - CandidateGeneratorTheoryUfType(TypeNode type, TermDb* tdb): d_type(type), d_tdb( tdb ){} - ~CandidateGeneratorTheoryUfType(){} - void resetInstantiationRound(){ - d_term_iter_limit = d_tdb->d_type_map[d_type].size(); - }; - void reset( TNode eqc ){ - Assert(eqc.isNull()); - d_term_iter = 0; - }; //* the argument is not used - TNode getNextCandidate(){ - if( d_term_iterd_type_map[d_type][d_term_iter]; - ++d_term_iter; - return n; - } else return Node::null(); - }; -}; - -} /* namespace rrinst */ - -namespace inst{ -typedef CVC4::theory::inst::CandidateGenerator CandidateGenerator; - -//Old CandidateGenerator - -class CandidateGeneratorTheoryUfDisequal; - -class CandidateGeneratorTheoryUf : public CandidateGenerator -{ - friend class CandidateGeneratorTheoryUfDisequal; -private: - //operator you are looking for - Node d_op; - //instantiator pointer - InstantiatorTheoryUf* d_ith; - //the equality class iterator - eq::EqClassIterator d_eqc; - int d_term_iter; - int d_term_iter_limit; -private: - Node d_retNode; -public: - CandidateGeneratorTheoryUf( InstantiatorTheoryUf* ith, Node op ); - ~CandidateGeneratorTheoryUf(){} - - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); -}; - -//class CandidateGeneratorTheoryUfDisequal : 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 -// InstantiatorTheoryUf* d_ith; -//public: -// CandidateGeneratorTheoryUfDisequal( InstantiatorTheoryUf* ith, Node eqc ); -// ~CandidateGeneratorTheoryUfDisequal(){} -// -// void resetInstantiationRound(); -// void reset( Node eqc ); //should be what you want to be disequal from -// Node getNextCandidate(); -//}; - -class CandidateGeneratorTheoryUfLitEq : 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 - InstantiatorTheoryUf* d_ith; -public: - CandidateGeneratorTheoryUfLitEq( InstantiatorTheoryUf* ith, Node mpat ); - ~CandidateGeneratorTheoryUfLitEq(){} - - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); -}; - -class CandidateGeneratorTheoryUfLitDeq : 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 - InstantiatorTheoryUf* d_ith; -public: - CandidateGeneratorTheoryUfLitDeq( InstantiatorTheoryUf* ith, Node mpat ); - ~CandidateGeneratorTheoryUfLitDeq(){} - - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); -}; - - -}/* CVC4::theory::uf::inst namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */ diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index 257bed0a2..48092b340 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -17,7 +17,7 @@ #include "theory/uf/theory_uf_instantiator.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" -#include "theory/uf/theory_uf_candidate_generator.h" +#include "theory/rr_candidate_generator.h" #include "theory/uf/equality_engine.h" #include "theory/quantifiers/term_database.h" @@ -160,15 +160,19 @@ bool InstantiatorTheoryUf::hasTerm( Node a ){ } bool InstantiatorTheoryUf::areEqual( Node a, Node b ){ - if( hasTerm( a ) && hasTerm( b ) ){ + if( a==b ){ + return true; + }else if( hasTerm( a ) && hasTerm( b ) ){ return ((TheoryUF*)d_th)->d_equalityEngine.areEqual( a, b ); }else{ - return a==b; + return false; } } bool InstantiatorTheoryUf::areDisequal( Node a, Node b ){ - if( hasTerm( a ) && hasTerm( b ) ){ + if( a==b ){ + return false; + }else if( hasTerm( a ) && hasTerm( b ) ){ return ((TheoryUF*)d_th)->d_equalityEngine.areDisequal( a, b, false ); }else{ return false; @@ -195,7 +199,7 @@ Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){ return rep; }else{ //otherwise, must search eq class - eq::EqClassIterator eqc_iter( rep, &((TheoryUF*)d_th)->d_equalityEngine ); + eq::EqClassIterator eqc_iter( rep, getEqualityEngine() ); rep = Node::null(); while( !eqc_iter.isFinished() ){ if( !(*eqc_iter).hasAttribute(InstConstantAttribute()) ){ @@ -211,6 +215,23 @@ Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){ return d_ground_reps[a]; } +eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){ + return &((TheoryUF*)d_th)->d_equalityEngine; +} + +void InstantiatorTheoryUf::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ + if( hasTerm( a ) ){ + a = getEqualityEngine()->getRepresentative( a ); + eq::EqClassIterator eqc_iter( a, getEqualityEngine() ); + while( !eqc_iter.isFinished() ){ + if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){ + eqc.push_back( *eqc_iter ); + } + eqc_iter++; + } + } +} + InstantiatorTheoryUf::Statistics::Statistics(): //d_instantiations("InstantiatorTheoryUf::Total_Instantiations", 0), d_instantiations_ce_solved("InstantiatorTheoryUf::Instantiations_CE-Solved", 0), @@ -527,7 +548,7 @@ void InstantiatorTheoryUf::collectTermsIps( Ips& ips, SetNode& terms, int index bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, SetNode & terms, bool addRep, bool modEq ){ //modEq default true bool addedTerm = false; - + if( modEq && ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n )){ Assert( getRepresentative( n )==n ); //collect modulo equality @@ -731,7 +752,7 @@ void InstantiatorTheoryUf::registerEfficientHandler( EfficientHandler& handler, d_pat_cand_gens[pats[i]].first->addPcDispatcher(&handler,i); d_pat_cand_gens[pats[i]].second->addPpDispatcher(&handler,i,i); d_cand_gens[op].addNewTermDispatcher(&handler,i); - + combineMultiPpIpsMap(pp_ips_map,multi_pp_ips_map,handler,i,pats); pp_ips_map.clear(); diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h index 3a2a5cc0e..d15c0103b 100644 --- a/src/theory/uf/theory_uf_instantiator.h +++ b/src/theory/uf/theory_uf_instantiator.h @@ -431,6 +431,8 @@ public: bool areDisequal( Node a, Node b ); Node getRepresentative( Node a ); Node getInternalRepresentative( Node a ); + eq::EqualityEngine* getEqualityEngine(); + void getEquivalenceClass( Node a, std::vector< Node >& eqc ); /** general creators of candidate generators */ rrinst::CandidateGenerator* getRRCanGenClasses(); rrinst::CandidateGenerator* getRRCanGenClass(); @@ -520,6 +522,8 @@ public: bool areEqual( Node a, Node b ) { return d_ith->areEqual( a, b ); } bool areDisequal( Node a, Node b ) { return d_ith->areDisequal( a, b ); } Node getInternalRepresentative( Node a ) { return d_ith->getInternalRepresentative( a ); } + eq::EqualityEngine* getEngine() { return d_ith->getEqualityEngine(); } + void getEquivalenceClass( Node a, std::vector< Node >& eqc ) { d_ith->getEquivalenceClass( a, eqc ); } }; /* EqualityQueryInstantiatorTheoryUf */ } diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index a85dea997..f68ab1429 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -34,12 +34,12 @@ using namespace CVC4::theory; using namespace CVC4::theory::uf; //clear -void UfModelTree::clear(){ +void UfModelTreeNode::clear(){ d_data.clear(); d_value = Node::null(); } -bool UfModelTree::hasConcreteArgumentDefinition(){ +bool UfModelTreeNode::hasConcreteArgumentDefinition(){ if( d_data.size()>1 ){ return true; }else if( d_data.empty() ){ @@ -51,16 +51,16 @@ bool UfModelTree::hasConcreteArgumentDefinition(){ } //set value function -void UfModelTree::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){ +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)n.getNumChildren() ){ + if( argIndex<(int)indexOrder.size() ){ //take r = null when argument is the model basis Node r; - if( ground || !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ){ + 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 ); @@ -68,7 +68,7 @@ void UfModelTree::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& } //get value function -Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){ +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; @@ -82,7 +82,7 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd if( i==0 ){ r = m->getRepresentative( n[ indexOrder[argIndex] ] ); } - std::map< Node, UfModelTree >::iterator it = d_data.find( r ); + 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() ){ @@ -101,7 +101,7 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd } } -Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){ +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{ @@ -113,7 +113,7 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd if( i==0 ){ r = m->getRepresentative( n[ indexOrder[argIndex] ] ); } - std::map< Node, UfModelTree >::iterator it = d_data.find( r ); + 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 @@ -136,11 +136,11 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd } } -Node UfModelTree::getFunctionValue(){ +Node UfModelTreeNode::getFunctionValue(){ if( !d_data.empty() ){ Node defaultValue; std::vector< Node > caseValues; - for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ + for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ if( it->first.isNull() ){ defaultValue = it->second.getFunctionValue(); }else{ @@ -166,12 +166,12 @@ Node UfModelTree::getFunctionValue(){ } //simplify function -void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){ +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, UfModelTree >::iterator it = d_data.find( 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 ); @@ -188,7 +188,7 @@ void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){ } } //now see if any children can be removed, and simplify the ones that cannot - for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ + 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 ); @@ -207,12 +207,12 @@ void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){ } //is total function -bool UfModelTree::isTotal( Node op, int argIndex ){ +bool UfModelTreeNode::isTotal( Node op, int argIndex ){ if( argIndex==(int)(op.getType().getNumChildren()-1) ){ return !d_value.isNull(); }else{ Node r; - std::map< Node, UfModelTree >::iterator it = d_data.find( r ); + std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); if( it!=d_data.end() ){ return it->second.isTotal( op, argIndex+1 ); }else{ @@ -221,7 +221,7 @@ bool UfModelTree::isTotal( Node op, int argIndex ){ } } -Node UfModelTree::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){ +Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){ return d_value; } @@ -231,9 +231,9 @@ void indent( std::ostream& out, int ind ){ } } -void UfModelTree::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){ +void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){ if( !d_data.empty() ){ - for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ + 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; @@ -247,54 +247,36 @@ void UfModelTree::debugPrint( std::ostream& out, TheoryModel* m, std::vector< in indent( out, ind ); out << "return "; m->printRepresentative( out, d_value ); - //out << " { "; - //for( int i=0; i<(int)d_explicit.size(); i++ ){ - // out << d_explicit[i] << " "; - //} - //out << "}"; out << std::endl; } } -UfModel::UfModel( Node op, quantifiers::FirstOrderModel* m ) : d_model( m ), d_op( op ), -d_model_constructed( false ){ - d_tree = UfModelTreeOrdered( op ); - TypeNode tn = d_op.getType(); - tn = tn[(int)tn.getNumChildren()-1]; - Assert( tn==NodeManager::currentNM()->booleanType() || tn.isDatatype() || uf::StrongSolverTheoryUf::isRelevantType( tn ) ); - //look at ground assertions - for( size_t i=0; igetTermDatabase()->d_op_map[ d_op ].size(); i++ ){ - Node n = d_model->getTermDatabase()->d_op_map[ d_op ][i]; - d_model->getTermDatabase()->computeModelBasisArgAttribute( n ); - if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ - Node r = d_model->getRepresentative( n ); - d_ground_asserts_reps.push_back( r ); - d_ground_asserts.push_back( n ); - } - } - //determine if it is constant - if( !d_ground_asserts.empty() ){ - bool isConstant = true; - for( int i=1; i<(int)d_ground_asserts.size(); i++ ){ - if( d_ground_asserts_reps[0]!=d_ground_asserts_reps[i] ){ - isConstant = false; - break; + +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 ); } - if( isConstant ){ - //set constant value - Node t = d_model->getTermDatabase()->getModelBasisOpTerm( d_op ); - Node r = d_ground_asserts_reps[0]; - setValue( t, r, false ); - setModel(); - Debug("fmf-model-cons") << "Function " << d_op << " is the constant function "; - d_model->printRepresentativeDebug( "fmf-model-cons", r ); - Debug("fmf-model-cons") << std::endl; - } + }else{ + return fm_node; } } -Node UfModel::getIntersection( Node n1, Node n2, bool& isGround ){ + +Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){ //Notice() << "Get intersection " << n1 << " " << n2 << std::endl; isGround = true; std::vector< Node > children; @@ -309,7 +291,7 @@ Node UfModel::getIntersection( Node n1, Node n2, bool& isGround ){ children.push_back( n2[i] ); }else if( n2[i].getAttribute(ModelBasisAttribute()) ){ children.push_back( n1[i] ); - }else if( d_model->areEqual( n1[i], n2[i] ) ){ + }else if( m->areEqual( n1[i], n2[i] ) ){ children.push_back( n1[i] ); }else{ return Node::null(); @@ -318,7 +300,7 @@ Node UfModel::getIntersection( Node n1, Node n2, bool& isGround ){ return NodeManager::currentNM()->mkNode( APPLY_UF, children ); } -void UfModel::setValue( Node n, Node v, bool ground, bool isReq ){ +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; @@ -332,13 +314,13 @@ void UfModel::setValue( Node n, Node v, bool ground, bool isReq ){ // is also defined. //for example, if we have that f( e, a ) = ..., and f( b, e ) = ..., // then we must define f( b, a ). - Node ni = getIntersection( n, d_defaults[i], isGround ); + Node ni = getIntersection( m, n, d_defaults[i], isGround ); if( !ni.isNull() ){ //if the intersection exists, and is not already defined if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() && d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){ //use the current value - setValue( ni, v, isGround, false ); + setValue( m, ni, v, isGround, false ); } } } @@ -350,36 +332,21 @@ void UfModel::setValue( Node n, Node v, bool ground, bool isReq ){ } } -Node UfModel::getValue( Node n, int& depIndex ){ - return d_tree.getValue( d_model, n, depIndex ); -} - -Node UfModel::getValue( Node n, std::vector< int >& depIndex ){ - return d_tree.getValue( d_model, n, depIndex ); -} - -Node UfModel::getConstantValue( Node n ){ - if( d_model_constructed ){ - return d_tree.getConstantValue( d_model, n ); - }else{ - return Node::null(); +void UfModelTreeGenerator::makeModel( TheoryModel* m, UfModelTree& tree ){ + for( int j=0; j<2; j++ ){ + for( int k=0; k<2; k++ ){ + for( std::map< Node, Node >::iterator it = d_set_values[j][k].begin(); it != d_set_values[j][k].end(); ++it ){ + tree.setValue( m, it->first, it->second, k==1 ); + } + } } -} - -Node UfModel::getFunctionValue(){ - if( d_func_value.isNull() && d_model_constructed ){ - d_func_value = d_tree.getFunctionValue(); + if( !d_default_value.isNull() ){ + tree.setDefaultValue( m, d_default_value ); } - return d_func_value; -} - -bool UfModel::isConstant(){ - Node gn = d_model->getTermDatabase()->getModelBasisOpTerm( d_op ); - Node n = getConstantValue( gn ); - return !n.isNull(); + tree.simplify(); } -bool UfModel::optUsePartialDefaults(){ +bool UfModelTreeGenerator::optUsePartialDefaults(){ #ifdef USE_PARTIAL_DEFAULT_VALUES return true; #else @@ -387,114 +354,14 @@ bool UfModel::optUsePartialDefaults(){ #endif } -void UfModel::setModel(){ - makeModel( d_tree ); - d_model_constructed = true; - d_func_value = Node::null(); - - //for debugging, make sure model satisfies all ground assertions - for( size_t i=0; i::iterator it = d_set_values[j][k].begin(); it != d_set_values[j][k].end(); ++it ){ - tree.setValue( d_model, it->first, it->second, k==1 ); - } - } - } - tree.simplify(); -} - -void UfModel::toStream(std::ostream& out){ - //out << "Function " << d_op << std::endl; - //out << " Type: " << d_op.getType() << std::endl; - //out << " Ground asserts:" << std::endl; - //for( int i=0; i<(int)d_ground_asserts.size(); i++ ){ - // out << " " << d_ground_asserts[i] << " = "; - // d_model->printRepresentative( out, d_ground_asserts[i] ); - // out << std::endl; - //} - //out << " Model:" << std::endl; - - TypeNode t = d_op.getType(); - out << d_op << "( "; - for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){ - out << "x_" << i << " : " << t[i]; - if( i<(int)(t.getNumChildren()-2) ){ - out << ", "; - } - } - out << " ) : " << t[(int)t.getNumChildren()-1] << std::endl; - if( d_tree.isEmpty() ){ - out << " [undefined]" << std::endl; - }else{ - d_tree.debugPrint( out, d_model, 3 ); - out << std::endl; - } - //out << " Phase reqs:" << std::endl; //for( int i=0; i<2; i++ ){ - // for( std::map< Node, std::vector< Node > >::iterator it = d_reqs[i].begin(); it != d_reqs[i].end(); ++it ){ - // out << " " << it->first << std::endl; - // for( int j=0; j<(int)it->second.size(); j++ ){ - // out << " " << it->second[j] << " -> " << (i==1) << std::endl; - // } - // } - //} - //out << std::endl; - //for( int i=0; i<2; i++ ){ - // for( std::map< Node, std::map< Node, std::vector< Node > > >::iterator it = d_eq_reqs[i].begin(); it != d_eq_reqs[i].end(); ++it ){ - // out << " " << "For " << it->first << ":" << std::endl; - // for( std::map< Node, std::vector< Node > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - // for( int j=0; j<(int)it2->second.size(); j++ ){ - // out << " " << it2->first << ( i==1 ? "==" : "!=" ) << it2->second[j] << std::endl; - // } - // } - // } - //} -} - -Node UfModel::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; - } + d_defaults.clear(); } diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 406c7ff3c..47b149867 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -23,19 +23,14 @@ namespace CVC4 { namespace theory { - -namespace quantifiers{ - class FirstOrderModel; -} - namespace uf { -class UfModelTree +class UfModelTreeNode { public: - UfModelTree(){} + UfModelTreeNode(){} /** the data */ - std::map< Node, UfModelTree > d_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 */ @@ -45,150 +40,137 @@ public: bool isEmpty() { return d_data.empty() && d_value.isNull(); } //clear void clear(); - /** setValue function - * - * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false - * - */ + /** setValue function */ void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ); - /** 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 - * If ground = true, we are asking whether the term n is constant (assumes that all non-model basis arguments are ground) - * - */ + /** 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 - // * - // * given term n, where n may contain model basis arguments - // * if n is constant for its entire domain, then this function returns the value of its domain - // * otherwise, it returns null - // * for example, 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 - // * - // */ + /** 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 ? + /** 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 UfModelTreeOrdered +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; - UfModelTree d_tree; + //the data + UfModelTreeNode d_tree; public: - UfModelTreeOrdered(){} - UfModelTreeOrdered( Node op ) : d_op( op ){ + //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 ); } } - UfModelTreeOrdered( Node op, std::vector< int >& indexOrder ) : d_op( op ){ + UfModelTree( Node op, std::vector< int >& indexOrder ) : d_op( op ){ d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() ); } - bool isEmpty() { return d_tree.isEmpty(); } + /** 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 UfModel +class UfModelTreeGenerator { private: - quantifiers::FirstOrderModel* d_model; - //the operator this model is for - Node d_op; - //is model constructed - bool d_model_constructed; //store for set values + Node d_default_value; std::map< Node, Node > d_set_values[2][2]; -private: // defaults std::vector< Node > d_defaults; - Node getIntersection( Node n1, Node n2, bool& isGround ); + Node getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ); public: - UfModel(){} - UfModel( Node op, quantifiers::FirstOrderModel* m ); - ~UfModel(){} - //ground terms for this operator - std::vector< Node > d_ground_asserts; - //the representatives they are equal to - std::vector< Node > d_ground_asserts_reps; - //data structure that stores the model - UfModelTreeOrdered d_tree; - //node equivalent of this model - Node d_func_value; -public: - /** get operator */ - Node getOperator() { return d_op; } - /** debug print */ - void toStream( std::ostream& out ); + UfModelTreeGenerator(){} + ~UfModelTreeGenerator(){} + /** set default value */ + void setDefaultValue( Node v ) { d_default_value = v; } /** set value */ - void setValue( Node n, Node v, bool ground = true, bool isReq = true ); - /** get value, return arguments that the value depends on */ - Node getValue( Node n, int& depIndex ); - Node getValue( Node n, std::vector< int >& depIndex ); - /** get constant value */ - Node getConstantValue( Node n ); - /** get function value for this function */ - Node getFunctionValue(); - /** is model constructed */ - bool isModelConstructed() { return d_model_constructed; } - /** is empty */ - bool isEmpty() { return d_ground_asserts.empty(); } - /** is constant */ - bool isConstant(); + 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(); -public: - /** set model */ - void setModel(); - /** clear model */ - void clearModel(); - /** make model */ - void makeModel( UfModelTreeOrdered& tree ); -public: - /** set value preference */ - void setValuePreference( Node f, Node n, bool isPro ); -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() ); } + /** reset */ + void clear(); }; //this class stores temporary information useful to model engine for constructing model @@ -197,6 +179,7 @@ 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]; diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index e5cb7e4f8..895a7d056 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1077,7 +1077,7 @@ void StrongSolverTheoryUf::newEqClass( Node n ){ Debug("uf-ss-solver") << "StrongSolverTheoryUf: New eq class " << n << " " << tn << std::endl; c->newEqClass( n ); } - //else if( isRelevantType( tn ) ){ + //else if( tn.isSort() ){ // //Debug("uf-ss-solver") << "WAIT: StrongSolverTheoryUf: New eq class " << n << " " << tn << std::endl; // //d_new_eq_class_waiting[tn].push_back( n ); //} @@ -1111,7 +1111,7 @@ void StrongSolverTheoryUf::assertNode( Node n, bool isDecision ){ if( n.getKind()==CARDINALITY_CONSTRAINT ){ TypeNode tn = n[0].getType(); Assert( d_conf_find[tn]->getCardinality()>0 ); - Assert( isRelevantType( tn ) ); + Assert( tn.isSort() ); Assert( d_conf_find[tn] ); long nCard = n[1].getConst().getNumerator().getLong(); d_conf_find[tn]->assertCardinality( nCard, true ); @@ -1124,7 +1124,7 @@ void StrongSolverTheoryUf::assertNode( Node n, bool isDecision ){ //must add new lemma Node nn = n[0]; TypeNode tn = nn[0].getType(); - Assert( isRelevantType( tn ) ); + Assert( tn.isSort() ); Assert( d_conf_find[tn] ); long nCard = nn[1].getConst().getNumerator().getLong(); d_conf_find[tn]->assertCardinality( nCard, false ); @@ -1177,7 +1177,7 @@ void StrongSolverTheoryUf::propagate( Theory::Effort level ){ void StrongSolverTheoryUf::preRegisterTerm( TNode n ){ //shouldn't have to preregister this type (it may be that there are no quantifiers over tn) FIXME TypeNode tn = n.getType(); - if( isRelevantType( tn ) ){ + if( tn.isSort() ){ preRegisterType( tn ); } } @@ -1187,9 +1187,10 @@ void StrongSolverTheoryUf::registerQuantifier( Node f ){ //must ensure the quantifier does not quantify over arithmetic for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ TypeNode tn = f[0][i].getType(); - if( isRelevantType( tn ) ){ + if( tn.isSort() ){ preRegisterType( tn ); }else{ + /* if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier"; Debug("uf-ss-na") << " (" << f << ")"; @@ -1201,6 +1202,7 @@ void StrongSolverTheoryUf::registerQuantifier( Node f ){ Debug("uf-ss-na") << std::endl; Unimplemented("Cannot perform finite model finding on datatype quantifier"); } + */ } } } @@ -1233,7 +1235,7 @@ StrongSolverTheoryUf::ConflictFind* StrongSolverTheoryUf::getConflictFind( TypeN std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.find( tn ); //pre-register the type if not done already if( it==d_conf_find.end() ){ - if( isRelevantType( tn ) ){ + if( tn.isSort() ){ preRegisterType( tn ); it = d_conf_find.find( tn ); } @@ -1332,20 +1334,10 @@ StrongSolverTheoryUf::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_max_model_size); } -bool StrongSolverTheoryUf::isRelevantType( TypeNode t ){ - return t!=NodeManager::currentNM()->booleanType() && - t!=NodeManager::currentNM()->integerType() && - t!=NodeManager::currentNM()->realType() && - t!=NodeManager::currentNM()->builtinOperatorType() && - !t.isFunction() && - !t.isDatatype() && - !t.isArray(); -} - bool StrongSolverTheoryUf::involvesRelevantType( Node n ){ if( n.getKind()==APPLY_UF ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( isRelevantType( n[i].getType() ) ){ + if( n[i].getType().isSort() ){ return true; } } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index bd4c4cb22..479fea05f 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -316,8 +316,6 @@ public: /** statistics class */ Statistics d_statistics; - /** is relevant type */ - static bool isRelevantType( TypeNode t ); /** involves relevant type */ static bool involvesRelevantType( Node n ); };/* class StrongSolverTheoryUf */ diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 8785ae0db..f3ea1171d 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -36,7 +36,8 @@ TESTS = \ v2l40025.cvc \ v3l60006.cvc \ v5l30058.cvc \ - bug286.cvc + bug286.cvc \ + wrong-sel-simp.cvc FAILING_TESTS = rec5.cvc diff --git a/test/regress/regress0/datatypes/v1l20009.cvc b/test/regress/regress0/datatypes/v1l20009.cvc index 0adba1da7..64469cbd6 100644 --- a/test/regress/regress0/datatypes/v1l20009.cvc +++ b/test/regress/regress0/datatypes/v1l20009.cvc @@ -1,5 +1,5 @@ -% EXPECT: valid -% EXIT: 20 +% EXPECT: invalid +% EXIT: 10 DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc new file mode 100644 index 000000000..3ba3249f1 --- /dev/null +++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +DATATYPE + nat = succ(pred : nat) | zero +END; + +QUERY pred(zero) = zero;