diff options
53 files changed, 2982 insertions, 2820 deletions
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<Expr> attexprs; + std::vector<Expr> patexprs; std::hash_set<std::string, StringHashFunction> names; std::vector< std::pair<std::string, Expr> > 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; i<f2.getNumChildren(); i++ ){ + patexprs.push_back( f2[i] ); + } } + expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs); + }else{ + expr2 = f2; } } /* constants */ diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 2bd85f712..9d6939ac9 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -45,12 +45,16 @@ libtheory_la_SOURCES = \ rr_inst_match.cpp \ rr_trigger.h \ rr_trigger.cpp \ + rr_candidate_generator.h \ + rr_candidate_generator.cpp \ inst_match.h \ inst_match.cpp \ trigger.h \ trigger.cpp \ model.h \ - model.cpp + model.cpp \ + candidate_generator.h \ + candidate_generator.cpp nodist_libtheory_la_SOURCES = \ rewriter_tables.h \ diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index c429fc0c6..e4c814660 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -18,6 +18,8 @@ libarrays_la_SOURCES = \ static_fact_manager.h \ static_fact_manager.cpp \ theory_arrays_instantiator.h \ - theory_arrays_instantiator.cpp + theory_arrays_instantiator.cpp \ + theory_arrays_model.h \ + theory_arrays_model.cpp EXTRA_DIST = kinds diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp index ca9001fe5..67c42d124 100644 --- a/src/theory/arrays/theory_arrays_instantiator.cpp +++ b/src/theory/arrays/theory_arrays_instantiator.cpp @@ -17,7 +17,7 @@ #include "theory/theory_engine.h" #include "theory/arrays/theory_arrays_instantiator.h" #include "theory/arrays/theory_arrays.h" -#include "theory/uf/theory_uf_candidate_generator.h" +#include "theory/rr_candidate_generator.h" using namespace std; using namespace CVC4; @@ -61,15 +61,19 @@ bool InstantiatorTheoryArrays::hasTerm( Node a ){ } bool InstantiatorTheoryArrays::areEqual( Node a, Node b ){ - if( hasTerm( a ) && hasTerm( b ) ){ + if( a==b ){ + return true; + }else if( hasTerm( a ) && hasTerm( b ) ){ return ((TheoryArrays*)d_th)->getEqualityEngine()->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<arrays::TheoryArrays *>(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; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){
+ Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i];
+ Assert( n.getKind()==SELECT );
+ if( m->areEqual( n[0], arr ) ){
+ //d_model->getTermDatabase()->computeModelBasisArgAttribute( n );
+ //if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
+ Node r = d_model->getRepresentative( n );
+ Node i = d_model->getRepresentative( n[1] );
+ d_values[i] = r;
+ //}
+ }
+ }
+}
+
+Node ArrayModel::getValue( Node n ){
+ Assert( n.getKind()==SELECT );
+ Assert( n[0]==d_arr );
+ std::map< Node, Node >::iterator it = d_values.find( n[0] );
+ if( it!=d_values.end() ){
+ return it->second;
+ }else{
+ return n;
+ //return d_default_value; TODO: guarentee I can return this here
+ }
+}
+
+void ArrayModel::setDefaultValue( Node v ){
+ d_default_value = v;
+}
+
+Node ArrayModel::getArrayValue(){
+ Node curr = d_arr; //TODO: make constant default
+ for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){
+ curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second );
+ }
+ return curr;
+}
diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h 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_iter<d_term_iter_limit ){
+ Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+ d_term_iter++;
+ if( isLegalCandidate( n ) ){
+ return n;
+ }
+ }
+ }else if( d_term_iter==-1 ){
+ if( d_retNode.isNull() ){
+ //get next candidate term in equivalence class
+ while( !d_eqc.isFinished() ){
+ Node n = (*d_eqc);
+ ++d_eqc;
+ if( n.hasOperator() && n.getOperator()==d_op ){
+ if( isLegalCandidate( n ) ){
+ return n;
+ }
+ }
+ }
+ }else{
+ Node ret;
+ if( d_retNode.hasOperator() && d_retNode.getOperator()==d_op ){
+ ret = d_retNode;
+ }
+ d_term_iter = -2; //done returning matches
+ return ret;
+ }
+ }
+ return Node::null();
+}
+
+#else
+
+
+CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
+ d_op( op ), d_qe( qe ), d_term_iter( -1 ){
+ Assert( !d_op.isNull() );
+}
+void CandidateGeneratorQE::resetInstantiationRound(){
+ d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size();
+}
+
+void CandidateGeneratorQE::reset( Node eqc ){
+ d_term_iter = 0;
+ if( eqc.isNull() ){
+ d_using_term_db = true;
+ }else{
+ //create an equivalence class iterator in eq class eqc
+ d_eqc.clear();
+ d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
+ d_using_term_db = false;
+ }
+}
+
+Node CandidateGeneratorQE::getNextCandidate(){
+ if( d_term_iter>=0 ){
+ if( d_using_term_db ){
+ //get next candidate term in the uf term database
+ while( d_term_iter<d_term_iter_limit ){
+ Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+ d_term_iter++;
+ if( isLegalCandidate( n ) ){
+ return n;
+ }
+ }
+ }else{
+ while( d_term_iter<(int)d_eqc.size() ){
+ Node n = d_eqc[d_term_iter];
+ d_term_iter++;
+ if( n.hasOperator() && n.getOperator()==d_op ){
+ if( isLegalCandidate( n ) ){
+ return n;
+ }
+ }
+ }
+ }
+ }
+ return Node::null();
+}
+
+#endif
+
+//CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) :
+// d_qe( qe ), d_eq_class( eqc ){
+// d_eci = NULL;
+//}
+//void CandidateGeneratorQEDisequal::resetInstantiationRound(){
+//
+//}
+////we will iterate over all terms that are disequal from eqc
+//void CandidateGeneratorQEDisequal::reset( Node eqc ){
+// //Assert( !eqc.isNull() );
+// ////begin iterating over equivalence classes that are disequal from eqc
+// //d_eci = d_ith->getEquivalenceClassInfo( eqc );
+// //if( d_eci ){
+// // d_eqci_iter = d_eci->d_disequal.begin();
+// //}
+//}
+//Node CandidateGeneratorQEDisequal::getNextCandidate(){
+// //if( d_eci ){
+// // while( d_eqci_iter != d_eci->d_disequal.end() ){
+// // if( (*d_eqci_iter).second ){
+// // //we have an equivalence class that is disequal from eqc
+// // d_cg->reset( (*d_eqci_iter).first );
+// // Node n = d_cg->getNextCandidate();
+// // //if there is a candidate in this equivalence class, return it
+// // if( !n.isNull() ){
+// // return n;
+// // }
+// // }
+// // ++d_eqci_iter;
+// // }
+// //}
+// return Node::null();
+//}
+
+
+CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
+ d_match_pattern( mpat ), d_qe( qe ){
+
+}
+void CandidateGeneratorQELitEq::resetInstantiationRound(){
+
+}
+void CandidateGeneratorQELitEq::reset( Node eqc ){
+ d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+}
+Node CandidateGeneratorQELitEq::getNextCandidate(){
+ while( d_eq.isFinished() ){
+ Node n = (*d_eq);
+ ++d_eq;
+ if( n.getType()==d_match_pattern[0].getType() ){
+ //an equivalence class with the same type as the pattern, return reflexive equality
+ return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
+ }
+ }
+ return Node::null();
+}
+
+
+CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
+ d_match_pattern( mpat ), d_qe( qe ){
+
+}
+void CandidateGeneratorQELitDeq::resetInstantiationRound(){
+
+}
+void CandidateGeneratorQELitDeq::reset( Node eqc ){
+ Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) );
+ d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() );
+}
+Node CandidateGeneratorQELitDeq::getNextCandidate(){
+ //get next candidate term in equivalence class
+ while( !d_eqc_false.isFinished() ){
+ Node n = (*d_eqc_false);
+ ++d_eqc_false;
+ if( n.getKind()==d_match_pattern.getKind() ){
+ //found an iff or equality, try to match it
+ //DO_THIS: cache to avoid redundancies?
+ //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false?
+ return n;
+ }
+ }
+ return Node::null();
+}
diff --git a/src/theory/candidate_generator.h b/src/theory/candidate_generator.h 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; i<dt.getNumConstructors(); i++ ){ - if( dt[i].getNumArgs()>selIndex && - 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<TNode>(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<TNode>& 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; j<possibleCons.size(); j++ ) { - if( !foundSel && possibleCons[j] ) { - cons = Node::fromExpr( dt[ j ].getConstructor() ); - //if there is a selector, split - for( unsigned int k=0; k<dt[ j ].getNumArgs(); k++ ) { - Node s = NodeManager::currentNM()->mkNode( 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; j<possibleCons.size(); j++ ) { - if( possibleCons[j] && !dt[ j ].isFinite() ) { - Debug("datatypes") << "Did not find selector for " << sf - << " and " << dt[ j ].getConstructor() << " is not finite." << endl; - cons = Node::null(); - break; - } - } - } - if( !cons.isNull() ) { - const DatatypeConstructor& cn = getConstructor( cons ); - Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl; - Node test = NodeManager::currentNM()->mkNode( 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; i<cn.getNumArgs(); i++ ) { - Node s = NodeManager::currentNM()->mkNode( 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; i<cn.getNumArgs(); i++ ) { - Node s = NodeManager::currentNM()->mkNode( 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; j<pcons.size(); j++ ) { + if( pcons[j] ) { + if( consIndex==-1 ){ + consIndex = j; + } + if( !dt[ j ].isFinite() && !eqc->d_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<Node>(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<TNode, TNode> 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<TNode>(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<Node>(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<Node>(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<TNode>(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 <ext/hash_set> #include <iostream> @@ -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<TNode> EqList; - typedef context::CDHashMap<Node, EqList*, NodeHashFunction> EqLists; - typedef context::CDChunkList<Node> EqListN; - typedef context::CDHashMap<Node, EqListN*, NodeHashFunction> EqListsN; + typedef context::CDChunkList<Node> NodeList; + typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - /** for debugging */ - context::CDList<Node> d_currAsserts; - context::CDList<Node> 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<CongruenceChannel, CONGRUENCE_OPERATORS_2 (kind::APPLY_CONSTRUCTOR, kind::APPLY_SELECTOR)> d_cc; - - /** - * Union find for storing the equalities. - */ - UnionFind<Node, NodeHashFunction> 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<CongruenceChannel, CONGRUENCE_OPERATORS_2 (kind::APPLY_CONSTRUCTOR, kind::APPLY_SELECTOR)> d_cce; - - //temporary - std::vector< Node > d_preRegTerms; + */ + NodeListMap d_labels; + /** Are we in conflict */ + context::CDO<bool> 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<TNode>& 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<TheoryDatatypes *>(getTheory()); - return new datatypes::rrinst::CandidateGeneratorTheoryClass(th); + datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes*>(getTheory()); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(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 <ext/hash_set> #include <iostream> #include <map> -#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<bool modEq> -InstMatchTrie2<modEq>::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<bool modEq> -void InstMatchTrie2<modEq>::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 modEq> -bool InstMatchTrie2<modEq>::existsInstMatch(InstMatchTrie2<modEq>::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<modEq>::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<modEq>::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 modEq> -bool InstMatchTrie2<modEq>::addInstMatch( InstMatch& m ) { - mapIter begin = m.d_map.begin(); - mapIter end = m.d_map.end(); - typename InstMatchTrie2<modEq>::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; i<d_ra.d_type_reps[tn].size(); i++ ){
+ //for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){
// if( i>0 ){ 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<d_defines.size(); i++ ){
@@ -178,22 +202,14 @@ Node TheoryModel::getValue( TNode n ){ //otherwise, get the interpreted value in the model
return getInterpretedValue( nn );
}
-
- ////case for equality
- //if( n.getKind()==EQUAL ){
- // Debug("model") << "-> 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<d_ra.d_type_reps[tn].size(); i++ ){
- if( std::find( exclude.begin(), exclude.end(), d_ra.d_type_reps[tn][i] )==exclude.end() ){
- return d_ra.d_type_reps[tn][i];
+ for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){
+ if( std::find( exclude.begin(), exclude.end(), d_rep_set.d_type_reps[tn][i] )==exclude.end() ){
+ return d_rep_set.d_type_reps[tn][i];
}
}
}
@@ -203,10 +219,10 @@ Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& 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; i<d_uf_terms[n].size(); i++ ){
+ Node un = d_uf_terms[n][i];
+ Node v = getRepresentative( un );
+ ufmt.setValue( this, un, v );
+ default_v = v;
+ }
+ if( default_v.isNull() ){
+ default_v = getInterpretedValue( NodeManager::currentNM()->mkVar( type.getRangeType() ) );
+ }
+ ufmt.setDefaultValue( this, default_v );
+ ufmt.simplify();
+ d_uf_models[n] = ufmt.getFunctionValue();
+ }
+ return d_uf_models[n];
+ }else{
+ return n;
+ }
}else{
//first, see if the representative is defined
if( d_equalityEngine.hasTerm( n ) ){
@@ -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; i<ac.getNumChildren(); i++ ){
+ Node acir = ac[i];
+ if( tm->d_equalityEngine.hasTerm( acir ) ){
+ acir = tm->d_equalityEngine.getRepresentative( acir );
+ }
+ if( unresolved_eqc.find( acir )==unresolved_eqc.end() ){
+ Message() << "TheoryEngineModelBuilder::buildModel : Datatype argument does not exist in the model " << acir << std::endl;
+ acir = Node::null();
+ }
+ if( acir.isNull() || unresolved_eqc[ acir ] ){
+ mkRep = false;
+ break;
+ }else{
+ children.push_back( tm->getRepresentative( acir ) );
+ }
+ }
+ if( mkRep ){
+ rep = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+ }
+ }else{
+ Message() << "TheoryEngineModelBuilder::buildModel : Do not know how to resolve datatype equivalence class " << n << std::endl;
+ }
+ mkRep = false;
+ }
+ if( mkRep ){
+ rep = chooseRepresentative( tm, n );
+ }
+ if( !rep.isNull() ){
+ tm->assertEquality( n, rep, true );
+ tm->d_reps[ n ] = rep;
+ tm->d_rep_set.add( rep );
+ unresolved_eqc[ n ] = false;
+ fixedPoint = false;
+ }else{
+ unresolved_types_next[ tn ] = true;
+ }
+ }
+ }
+ //for calculating unresolved types
+ for( std::map< TypeNode, bool >::iterator it = unresolved_types.begin(); it != unresolved_types.end(); ++it ){
+ unresolved_types[ it->first ] = unresolved_types_next[ it->first ];
+ }
+ }while( !fixedPoint );
+
+ //for all unresolved equivalence classes, just get new domain value
+ // this should typically never happen (all equivalence classes should be resolved at this point)
+ for( std::map< Node, bool >::iterator it = unresolved_eqc.begin(); it != unresolved_eqc.end(); ++it ){
+ if( it->second ){
+ Node n = it->first;
+ Node rep = chooseRepresentative( tm, n );
+ tm->assertEquality( n, rep, true );
+ tm->d_reps[ n ] = rep;
+ tm->d_rep_set.add( rep );
+ //FIXME: Assertion failure here?
+ Message() << "Warning : Unresolved eqc, assigning " << rep << " for eqc( " << n << " ), type = " << n.getType() << std::endl;
+ }
+ }
+
+ //model-specific initialization
processBuildModel( tm );
}
-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; i<dt.getNumConstructors(); i++ ){
+ for( size_t j = 0; j<dt[i].getNumArgs(); j++ ){
+ initializeType( TypeNode::fromType( dt[i][j].getType() ), unresolved_types );
+ }
+ }
}
- ++eqc_i;
}
- return Node::null();
}
-void TheoryEngineModelBuilder::processBuildModel( TheoryModel* tm ){
- Debug( "model-builder" ) << "TheoryEngineModelBuilder: Complete model..." << std::endl;
- //create constants for all unresolved equivalence classes
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_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; i<getNumAssertedQuantifiers(); i++ ){
Node f = getAssertedQuantifier( i );
- //initialize model for term
+ //initialize relevant models within bodies of all quantifiers
initializeModelForTerm( f[1] );
}
-
+ //for debugging
if( Options::current()->printModelEngine ){
- for( std::map< TypeNode, std::vector< Node > >::iterator it = d_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<Node> 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; i<fm->getNumAssertedQuantifiers(); 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; i<fm->d_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; i<fm->d_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; i<fm->getNumAssertedQuantifiers(); 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; i<model.d_ground_asserts.size(); i++ ){ - Node n = model.d_ground_asserts[i]; - Node v = model.d_ground_asserts_reps[i]; - //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 - model.setValue( n, v ); - if( model.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 ){ - model.setValue( n, v, false ); - if( n==defaultTerm ){ - //incidentally already set, we will not need to find a default value - setDefaultVal = false; - } - } - }else{ - if( n==defaultTerm ){ - model.setValue( 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() ); - model.setValue( defaultTerm, defaultVal, false ); - } - Debug("fmf-model-cons") << " Making model..."; - model.setModel(); - Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; - } -} - -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); -} - //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; i<f[0].getNumChildren(); i++ ){ - totalInst = totalInst * (int)d_quantEngine->getModel()->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; i<d_model->d_uf_terms[op].size(); i++ ){
+ Node n = d_model->d_uf_terms[op][i];
//add arguments to domain
for( int j=0; j<(int)n.getNumChildren(); j++ ){
- if( d_model->d_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; i<d_model->d_ra.d_type_reps[tn].size(); i++ ){
+ for( size_t i=0; i<d_model->d_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; i<argDepIndex; i++ ){
+ int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
+ Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
+ if( children_depIndex[index]>depIndex ){
+ depIndex = children_depIndex[index];
+ }
+ }
+ setVal = true;
+ }
+ }else if( n.getKind()==SELECT ){
+ //we are free to interpret this term however we want
}
- //recalculate the depIndex
- depIndex = -1;
- for( int i=0; i<argDepIndex; i++ ){
- int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
- Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
- if( children_depIndex[index]>depIndex ){
- depIndex = children_depIndex[index];
+ //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; i<theory::THEORY_LAST; ++i ){ + if( d_qe->getInstantiator( 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/uf/theory_uf_candidate_generator.h b/src/theory/rr_candidate_generator.h index a06f04f99..30f6c067d 100644 --- a/src/theory/uf/theory_uf_candidate_generator.h +++ b/src/theory/rr_candidate_generator.h @@ -1,8 +1,8 @@ /********************* */ -/*! \file theory_uf_candidate_generator.h +/*! \file rr_candidate_generator.h ** \verbatim ** Original author: ajreynol - ** Major contributors: none + ** 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) @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Theory uf candidate generator + ** \brief rr candidate generator **/ #include "cvc4_private.h" @@ -21,7 +21,6 @@ #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; @@ -102,7 +101,7 @@ public: } /* namespace rrinst */ } /* namespace eq */ -namespace uf { +namespace uf{ namespace rrinst { typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; @@ -164,96 +163,46 @@ public: }; } /* namespace rrinst */ +} /* namespace uf */ -namespace inst{ -typedef CVC4::theory::inst::CandidateGenerator CandidateGenerator; +class GenericCandidateGeneratorClasses: public rrinst::CandidateGenerator{ -//Old CandidateGenerator + /** The candidate generators */ + rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST]; + /** The current theory which candidategenerator is used */ + TheoryId d_can_gen_id; -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(){} + GenericCandidateGeneratorClasses(QuantifiersEngine * qe); + ~GenericCandidateGeneratorClasses(); void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); + void reset(TNode eqc); + TNode getNextCandidate(); + void lookForNextTheory(); }; -//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 GenericCandidateGeneratorClass: public rrinst::CandidateGenerator{ -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(); -}; + /** 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; -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(){} - + GenericCandidateGeneratorClass(QuantifiersEngine * qe); + ~GenericCandidateGeneratorClass(); void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); -}; + void reset(TNode eqc); + TNode getNextCandidate(); + void lookForNextTheory(); +}; -}/* CVC4::theory::uf::inst namespace */ -}/* CVC4::theory::uf namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ 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<uf::TheoryUF *>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )); - eq::EqualityEngine* ee = - static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(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<datatypes::TheoryDatatypes *>(qe->getTheoryEngine()->getTheory( theory::THEORY_DATATYPES )); - datatypes::rrinst::CandidateGeneratorTheoryClass cdtDtEq(dt); + eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(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_iter<d_term_iter_limit ){ - Node n = d_ith->getQuantifiersEngine()->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<bool>(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_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; i<d_model->getTermDatabase()->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<d_ground_asserts.size(); i++ ){
- int depIndex;
- Node n = d_tree.getValue( d_model, d_ground_asserts[i], depIndex );
- if( n!=d_ground_asserts_reps[i] ){
- Debug("fmf-bad") << "Bad model : " << d_ground_asserts[i] << " := ";
- d_model->printRepresentativeDebug("fmf-bad", n );
- Debug("fmf-bad") << " != ";
- d_model->printRepresentativeDebug("fmf-bad", d_ground_asserts_reps[i] );
- Debug("fmf-bad") << std::endl;
- }
- }
-}
-
-void UfModel::clearModel(){
+void UfModelTreeGenerator::clear(){
+ d_default_value = Node::null();
for( int j=0; j<2; j++ ){
for( int k=0; k<2; k++ ){
d_set_values[j][k].clear();
}
}
- d_tree.clear();
- d_model_constructed = false;
-}
-
-void UfModel::makeModel( UfModelTreeOrdered& 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( 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<Rational>().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<Rational>().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; |