summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/Makefile.am4
-rw-r--r--src/theory/uf/theory_uf_candidate_generator.cpp182
-rw-r--r--src/theory/uf/theory_uf_candidate_generator.h260
-rw-r--r--src/theory/uf/theory_uf_instantiator.cpp35
-rw-r--r--src/theory/uf/theory_uf_instantiator.h4
-rw-r--r--src/theory/uf/theory_uf_model.cpp249
-rw-r--r--src/theory/uf/theory_uf_model.h169
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp26
-rw-r--r--src/theory/uf/theory_uf_strong_solver.h2
9 files changed, 176 insertions, 755 deletions
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_candidate_generator.h b/src/theory/uf/theory_uf_candidate_generator.h
deleted file mode 100644
index a06f04f99..000000000
--- a/src/theory/uf/theory_uf_candidate_generator.h
+++ /dev/null
@@ -1,260 +0,0 @@
-/********************* */
-/*! \file theory_uf_candidate_generator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Theory uf candidate generator
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H
-#define __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/uf/theory_uf_instantiator.h"
-#include "theory/rr_inst_match.h"
-
-using namespace CVC4::theory::quantifiers;
-
-namespace CVC4 {
-namespace theory {
-namespace eq {
-
-namespace rrinst{
-typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
-
-//New CandidateGenerator. They have a simpler semantic than the old one
-
-// Just iterate amoung the equivalence classes
-// node::Null() must be given to reset
-class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{
-private:
- //the equality classes iterator
- eq::EqClassesIterator d_eq;
- //equalityengine pointer
- EqualityEngine* d_ee;
-public:
- CandidateGeneratorTheoryEeClasses( EqualityEngine * ee): d_ee( ee ){}
- ~CandidateGeneratorTheoryEeClasses(){}
- void resetInstantiationRound(){};
- void reset( TNode eqc ){
- Assert(eqc.isNull());
- d_eq = eq::EqClassesIterator( d_ee );
- }; //* the argument is not used
- TNode getNextCandidate(){
- if( !d_eq.isFinished() ) return (*(d_eq++));
- else return Node::null();
- };
-};
-
-// Just iterate amoung the equivalence class of the given node
-// node::Null() *can't* be given to reset
-class CandidateGeneratorTheoryEeClass : public CandidateGenerator{
-private:
- //instantiator pointer
- EqualityEngine* d_ee;
- //the equality class iterator
- eq::EqClassIterator d_eqc;
- /* For the case where the given term doesn't exists in uf */
- Node d_retNode;
-public:
- CandidateGeneratorTheoryEeClass( EqualityEngine* ee): d_ee( ee ){}
- ~CandidateGeneratorTheoryEeClass(){}
- void resetInstantiationRound(){};
- void reset( TNode eqc ){
- Assert(!eqc.isNull());
- if( d_ee->hasTerm( eqc ) ){
- /* eqc is in uf */
- eqc = d_ee->getRepresentative( eqc );
- d_eqc = eq::EqClassIterator( eqc, d_ee );
- d_retNode = Node::null();
- }else{
- /* If eqc if not a term known by uf, it is the only one in its
- equivalence class. So we will return only it */
- d_retNode = eqc;
- d_eqc = eq::EqClassIterator();
- }
- }; //* the argument is not used
- TNode getNextCandidate(){
- if(d_retNode.isNull()){
- if( !d_eqc.isFinished() ) return (*(d_eqc++));
- else return Node::null();
- }else{
- /* the case where eqc not in uf */
- Node ret = d_retNode;
- d_retNode = Node::null(); /* d_eqc.isFinished() must be true */
- return ret;
- }
- };
-};
-
-
-} /* namespace rrinst */
-} /* namespace eq */
-
-namespace uf {
-namespace rrinst {
-
-typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
-
-class CandidateGeneratorTheoryUfOp : public CandidateGenerator{
-private:
- Node d_op;
- //instantiator pointer
- TermDb* d_tdb;
- // Since new term can appears we restrict ourself to the one that
- // exists at resetInstantiationRound
- size_t d_term_iter_limit;
- size_t d_term_iter;
-public:
- CandidateGeneratorTheoryUfOp(Node op, TermDb* tdb): d_op(op), d_tdb( tdb ){}
- ~CandidateGeneratorTheoryUfOp(){}
- void resetInstantiationRound(){
- d_term_iter_limit = d_tdb->d_op_map[d_op].size();
- };
- void reset( TNode eqc ){
- Assert(eqc.isNull());
- d_term_iter = 0;
- }; //* the argument is not used
- TNode getNextCandidate(){
- if( d_term_iter<d_term_iter_limit ){
- TNode n = d_tdb->d_op_map[d_op][d_term_iter];
- ++d_term_iter;
- return n;
- } else return Node::null();
- };
-};
-
-class CandidateGeneratorTheoryUfType : public CandidateGenerator{
-private:
- TypeNode d_type;
- //instantiator pointer
- TermDb* d_tdb;
- // Since new term can appears we restrict ourself to the one that
- // exists at resetInstantiationRound
- size_t d_term_iter_limit;
- size_t d_term_iter;
-public:
- CandidateGeneratorTheoryUfType(TypeNode type, TermDb* tdb): d_type(type), d_tdb( tdb ){}
- ~CandidateGeneratorTheoryUfType(){}
- void resetInstantiationRound(){
- d_term_iter_limit = d_tdb->d_type_map[d_type].size();
- };
- void reset( TNode eqc ){
- Assert(eqc.isNull());
- d_term_iter = 0;
- }; //* the argument is not used
- TNode getNextCandidate(){
- if( d_term_iter<d_term_iter_limit ){
- TNode n = d_tdb->d_type_map[d_type][d_term_iter];
- ++d_term_iter;
- return n;
- } else return Node::null();
- };
-};
-
-} /* namespace rrinst */
-
-namespace inst{
-typedef CVC4::theory::inst::CandidateGenerator CandidateGenerator;
-
-//Old CandidateGenerator
-
-class CandidateGeneratorTheoryUfDisequal;
-
-class CandidateGeneratorTheoryUf : public CandidateGenerator
-{
- friend class CandidateGeneratorTheoryUfDisequal;
-private:
- //operator you are looking for
- Node d_op;
- //instantiator pointer
- InstantiatorTheoryUf* d_ith;
- //the equality class iterator
- eq::EqClassIterator d_eqc;
- int d_term_iter;
- int d_term_iter_limit;
-private:
- Node d_retNode;
-public:
- CandidateGeneratorTheoryUf( InstantiatorTheoryUf* ith, Node op );
- ~CandidateGeneratorTheoryUf(){}
-
- void resetInstantiationRound();
- void reset( Node eqc );
- Node getNextCandidate();
-};
-
-//class CandidateGeneratorTheoryUfDisequal : public CandidateGenerator
-//{
-//private:
-// //equivalence class
-// Node d_eq_class;
-// //equivalence class info
-// EqClassInfo* d_eci;
-// //equivalence class iterator
-// EqClassInfo::BoolMap::const_iterator d_eqci_iter;
-// //instantiator pointer
-// InstantiatorTheoryUf* d_ith;
-//public:
-// CandidateGeneratorTheoryUfDisequal( InstantiatorTheoryUf* ith, Node eqc );
-// ~CandidateGeneratorTheoryUfDisequal(){}
-//
-// void resetInstantiationRound();
-// void reset( Node eqc ); //should be what you want to be disequal from
-// Node getNextCandidate();
-//};
-
-class CandidateGeneratorTheoryUfLitEq : public CandidateGenerator
-{
-private:
- //the equality classes iterator
- eq::EqClassesIterator d_eq;
- //equality you are trying to match equalities for
- Node d_match_pattern;
- //einstantiator pointer
- InstantiatorTheoryUf* d_ith;
-public:
- CandidateGeneratorTheoryUfLitEq( InstantiatorTheoryUf* ith, Node mpat );
- ~CandidateGeneratorTheoryUfLitEq(){}
-
- void resetInstantiationRound();
- void reset( Node eqc );
- Node getNextCandidate();
-};
-
-class CandidateGeneratorTheoryUfLitDeq : public CandidateGenerator
-{
-private:
- //the equality class iterator for false
- eq::EqClassIterator d_eqc_false;
- //equality you are trying to match disequalities for
- Node d_match_pattern;
- //einstantiator pointer
- InstantiatorTheoryUf* d_ith;
-public:
- CandidateGeneratorTheoryUfLitDeq( InstantiatorTheoryUf* ith, Node mpat );
- ~CandidateGeneratorTheoryUfLitDeq(){}
-
- void resetInstantiationRound();
- void reset( Node eqc );
- Node getNextCandidate();
-};
-
-
-}/* CVC4::theory::uf::inst namespace */
-}/* CVC4::theory::uf namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
index 257bed0a2..48092b340 100644
--- a/src/theory/uf/theory_uf_instantiator.cpp
+++ b/src/theory/uf/theory_uf_instantiator.cpp
@@ -17,7 +17,7 @@
#include "theory/uf/theory_uf_instantiator.h"
#include "theory/theory_engine.h"
#include "theory/uf/theory_uf.h"
-#include "theory/uf/theory_uf_candidate_generator.h"
+#include "theory/rr_candidate_generator.h"
#include "theory/uf/equality_engine.h"
#include "theory/quantifiers/term_database.h"
@@ -160,15 +160,19 @@ bool InstantiatorTheoryUf::hasTerm( Node a ){
}
bool InstantiatorTheoryUf::areEqual( Node a, Node b ){
- if( hasTerm( a ) && hasTerm( b ) ){
+ if( a==b ){
+ return true;
+ }else if( hasTerm( a ) && hasTerm( b ) ){
return ((TheoryUF*)d_th)->d_equalityEngine.areEqual( a, b );
}else{
- return a==b;
+ return false;
}
}
bool InstantiatorTheoryUf::areDisequal( Node a, Node b ){
- if( hasTerm( a ) && hasTerm( b ) ){
+ if( a==b ){
+ return false;
+ }else if( hasTerm( a ) && hasTerm( b ) ){
return ((TheoryUF*)d_th)->d_equalityEngine.areDisequal( a, b, false );
}else{
return false;
@@ -195,7 +199,7 @@ Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
return rep;
}else{
//otherwise, must search eq class
- eq::EqClassIterator eqc_iter( rep, &((TheoryUF*)d_th)->d_equalityEngine );
+ eq::EqClassIterator eqc_iter( rep, getEqualityEngine() );
rep = Node::null();
while( !eqc_iter.isFinished() ){
if( !(*eqc_iter).hasAttribute(InstConstantAttribute()) ){
@@ -211,6 +215,23 @@ Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
return d_ground_reps[a];
}
+eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){
+ return &((TheoryUF*)d_th)->d_equalityEngine;
+}
+
+void InstantiatorTheoryUf::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
+ if( hasTerm( a ) ){
+ a = getEqualityEngine()->getRepresentative( a );
+ eq::EqClassIterator eqc_iter( a, getEqualityEngine() );
+ while( !eqc_iter.isFinished() ){
+ if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){
+ eqc.push_back( *eqc_iter );
+ }
+ eqc_iter++;
+ }
+ }
+}
+
InstantiatorTheoryUf::Statistics::Statistics():
//d_instantiations("InstantiatorTheoryUf::Total_Instantiations", 0),
d_instantiations_ce_solved("InstantiatorTheoryUf::Instantiations_CE-Solved", 0),
@@ -527,7 +548,7 @@ void InstantiatorTheoryUf::collectTermsIps( Ips& ips, SetNode& terms, int index
bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, SetNode & terms, bool addRep, bool modEq ){ //modEq default true
bool addedTerm = false;
-
+
if( modEq && ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n )){
Assert( getRepresentative( n )==n );
//collect modulo equality
@@ -731,7 +752,7 @@ void InstantiatorTheoryUf::registerEfficientHandler( EfficientHandler& handler,
d_pat_cand_gens[pats[i]].first->addPcDispatcher(&handler,i);
d_pat_cand_gens[pats[i]].second->addPpDispatcher(&handler,i,i);
d_cand_gens[op].addNewTermDispatcher(&handler,i);
-
+
combineMultiPpIpsMap(pp_ips_map,multi_pp_ips_map,handler,i,pats);
pp_ips_map.clear();
diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h
index 3a2a5cc0e..d15c0103b 100644
--- a/src/theory/uf/theory_uf_instantiator.h
+++ b/src/theory/uf/theory_uf_instantiator.h
@@ -431,6 +431,8 @@ public:
bool areDisequal( Node a, Node b );
Node getRepresentative( Node a );
Node getInternalRepresentative( Node a );
+ eq::EqualityEngine* getEqualityEngine();
+ void getEquivalenceClass( Node a, std::vector< Node >& eqc );
/** general creators of candidate generators */
rrinst::CandidateGenerator* getRRCanGenClasses();
rrinst::CandidateGenerator* getRRCanGenClass();
@@ -520,6 +522,8 @@ public:
bool areEqual( Node a, Node b ) { return d_ith->areEqual( a, b ); }
bool areDisequal( Node a, Node b ) { return d_ith->areDisequal( a, b ); }
Node getInternalRepresentative( Node a ) { return d_ith->getInternalRepresentative( a ); }
+ eq::EqualityEngine* getEngine() { return d_ith->getEqualityEngine(); }
+ void getEquivalenceClass( Node a, std::vector< Node >& eqc ) { d_ith->getEquivalenceClass( a, eqc ); }
}; /* EqualityQueryInstantiatorTheoryUf */
}
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index a85dea997..f68ab1429 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -34,12 +34,12 @@ using namespace CVC4::theory;
using namespace CVC4::theory::uf;
//clear
-void UfModelTree::clear(){
+void UfModelTreeNode::clear(){
d_data.clear();
d_value = Node::null();
}
-bool UfModelTree::hasConcreteArgumentDefinition(){
+bool UfModelTreeNode::hasConcreteArgumentDefinition(){
if( d_data.size()>1 ){
return true;
}else if( d_data.empty() ){
@@ -51,16 +51,16 @@ bool UfModelTree::hasConcreteArgumentDefinition(){
}
//set value function
-void UfModelTree::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
+void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
if( d_data.empty() ){
d_value = v;
}else if( !d_value.isNull() && d_value!=v ){
d_value = Node::null();
}
- if( argIndex<(int)n.getNumChildren() ){
+ if( argIndex<(int)indexOrder.size() ){
//take r = null when argument is the model basis
Node r;
- if( ground || !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ){
+ if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){
r = m->getRepresentative( n[ indexOrder[argIndex] ] );
}
d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 );
@@ -68,7 +68,7 @@ void UfModelTree::setValue( TheoryModel* m, Node n, Node v, std::vector< int >&
}
//get value function
-Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){
+Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){
if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){
//Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl;
depIndex = argIndex;
@@ -82,7 +82,7 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd
if( i==0 ){
r = m->getRepresentative( n[ indexOrder[argIndex] ] );
}
- std::map< Node, UfModelTree >::iterator it = d_data.find( r );
+ std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
if( it!=d_data.end() ){
val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 );
if( !val.isNull() ){
@@ -101,7 +101,7 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd
}
}
-Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){
+Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){
if( argIndex==(int)indexOrder.size() ){
return d_value;
}else{
@@ -113,7 +113,7 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd
if( i==0 ){
r = m->getRepresentative( n[ indexOrder[argIndex] ] );
}
- std::map< Node, UfModelTree >::iterator it = d_data.find( r );
+ std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
if( it!=d_data.end() ){
val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 );
//we have found a value
@@ -136,11 +136,11 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd
}
}
-Node UfModelTree::getFunctionValue(){
+Node UfModelTreeNode::getFunctionValue(){
if( !d_data.empty() ){
Node defaultValue;
std::vector< Node > caseValues;
- for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
+ for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
if( it->first.isNull() ){
defaultValue = it->second.getFunctionValue();
}else{
@@ -166,12 +166,12 @@ Node UfModelTree::getFunctionValue(){
}
//simplify function
-void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){
+void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){
if( argIndex<(int)op.getType().getNumChildren()-1 ){
std::vector< Node > eraseData;
//first process the default argument
Node r;
- std::map< Node, UfModelTree >::iterator it = d_data.find( r );
+ std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
if( it!=d_data.end() ){
if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
eraseData.push_back( r );
@@ -188,7 +188,7 @@ void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){
}
}
//now see if any children can be removed, and simplify the ones that cannot
- for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
+ for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
if( !it->first.isNull() ){
if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
eraseData.push_back( it->first );
@@ -207,12 +207,12 @@ void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){
}
//is total function
-bool UfModelTree::isTotal( Node op, int argIndex ){
+bool UfModelTreeNode::isTotal( Node op, int argIndex ){
if( argIndex==(int)(op.getType().getNumChildren()-1) ){
return !d_value.isNull();
}else{
Node r;
- std::map< Node, UfModelTree >::iterator it = d_data.find( r );
+ std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
if( it!=d_data.end() ){
return it->second.isTotal( op, argIndex+1 );
}else{
@@ -221,7 +221,7 @@ bool UfModelTree::isTotal( Node op, int argIndex ){
}
}
-Node UfModelTree::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){
+Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){
return d_value;
}
@@ -231,9 +231,9 @@ void indent( std::ostream& out, int ind ){
}
}
-void UfModelTree::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){
+void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){
if( !d_data.empty() ){
- for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
+ for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
if( !it->first.isNull() ){
indent( out, ind );
out << "if x_" << indexOrder[arg] << " == " << it->first << std::endl;
@@ -247,54 +247,36 @@ void UfModelTree::debugPrint( std::ostream& out, TheoryModel* m, std::vector< in
indent( out, ind );
out << "return ";
m->printRepresentative( out, d_value );
- //out << " { ";
- //for( int i=0; i<(int)d_explicit.size(); i++ ){
- // out << d_explicit[i] << " ";
- //}
- //out << "}";
out << std::endl;
}
}
-UfModel::UfModel( Node op, quantifiers::FirstOrderModel* m ) : d_model( m ), d_op( op ),
-d_model_constructed( false ){
- d_tree = UfModelTreeOrdered( op );
- TypeNode tn = d_op.getType();
- tn = tn[(int)tn.getNumChildren()-1];
- Assert( tn==NodeManager::currentNM()->booleanType() || tn.isDatatype() || uf::StrongSolverTheoryUf::isRelevantType( tn ) );
- //look at ground assertions
- for( size_t i=0; 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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback