}
}
}
+ }else if( !n1.getType().isDatatype() ){
+ //also check for clashes between non-datatypes
+ Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
+ eq = Rewriter::rewrite( eq );
+ if( eq==NodeManager::currentNM()->mkConst(false) ){
+ return true;
+ }
}
return false;
}
d_uf_models.clear();
}
-Node TheoryModel::getValue( TNode n ){
+Node TheoryModel::getValue( TNode n ) const{
//apply substitutions
Node nn = d_substitutions.apply( n );
//get value in model
return getModelValue( nn );
}
-Expr TheoryModel::getValue( Expr expr ){
+Expr TheoryModel::getValue( Expr expr ) const{
Node n = Node::fromExpr( expr );
Node ret = getValue( n );
return ret.toExpr();
}
/** get cardinality for sort */
-Cardinality TheoryModel::getCardinality( Type t ){
+Cardinality TheoryModel::getCardinality( Type t ) const{
TypeNode tn = TypeNode::fromType( t );
//for now, we only handle cardinalities for uninterpreted sorts
if( tn.isSort() ){
if( d_rep_set.hasType( tn ) ){
- return Cardinality( d_rep_set.d_type_reps[tn].size() );
+ return Cardinality( d_rep_set.getNumRepresentatives( tn ) );
}else{
return Cardinality( CardinalityUnknown() );
}
}
}
-Node TheoryModel::getModelValue( TNode n )
-{
+Node TheoryModel::getModelValue( TNode n ) const{
if( n.isConst() ) {
return n;
}
TypeNode t = n.getType();
if (t.isFunction() || t.isPredicate()) {
if (d_enableFuncModels) {
- if (d_uf_models.find(n) != d_uf_models.end()) {
+ std::map< Node, Node >::const_iterator it = d_uf_models.find(n);
+ if (it != d_uf_models.end()) {
// Existing function
- return d_uf_models[n];
+ return it->second;
}
// Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type
vector<TypeNode> argTypes = t.getArgTypes();
std::vector<Node> children;
if (n.getKind() == APPLY_UF) {
Node op = n.getOperator();
- if (d_uf_models.find(op) == d_uf_models.end()) {
+ std::map< Node, Node >::const_iterator it = d_uf_models.find(op);
+ if (it == d_uf_models.end()) {
// Unknown term - return first enumerated value for this type
TypeEnumerator te(n.getType());
return *te;
+ }else{
+ // Plug in uninterpreted function model
+ children.push_back(it->second);
}
- // Plug in uninterpreted function model
- children.push_back(d_uf_models[op]);
}
else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
children.push_back(n.getOperator());
}
Node val = d_equalityEngine.getRepresentative(n);
Assert(d_reps.find(val) != d_reps.end());
- val = d_reps[val];
- return val;
-}
-
-
-Node TheoryModel::getInterpretedValue( TNode n ){
- Trace("model") << "Get interpreted value of " << n << std::endl;
- TypeNode type = n.getType();
- if( type.isFunction() || type.isPredicate() ){
- //for function models
- if( d_enableFuncModels ){
- if( d_uf_models.find( n )!=d_uf_models.end() ){
- //pre-existing function model
- Trace("model") << "Return function value." << std::endl;
- return d_uf_models[n];
- }else{
- Trace("model") << "Return arbitrary function value." << std::endl;
- //otherwise, choose the constant default value
- uf::UfModelTree ufmt( n );
- Node default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValueQueryVar_$$", type.getRangeType(),
- "a placeholder variable to query for a default value in model construction" ) );
- ufmt.setDefaultValue( this, default_v );
- return ufmt.getFunctionValue( "$x" );
- }
- }else{
- return n;
- }
- } else{
- Trace("model-debug") << "check rep..." << std::endl;
- Node ret;
- //check if the representative is defined
- n = d_equalityEngine.hasTerm( n ) ? d_equalityEngine.getRepresentative( n ) : n;
- Trace("model-debug") << "rep is..." << n << std::endl;
- if( d_reps.find( n )!=d_reps.end() ){
- Trace("model") << "Return value in equality engine."<< std::endl;
- return d_reps[n];
- }
- Trace("model-debug") << "check apply uf models..." << std::endl;
- //if it is APPLY_UF, we must consult the corresponding function if it exists
- if( n.getKind()==APPLY_UF ){
- Node op = n.getOperator();
- if( d_uf_models.find( op )!=d_uf_models.end() ){
- std::vector< Node > lam_children;
- lam_children.push_back( d_uf_models[ op ] );
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- lam_children.push_back( n[i] );
- }
- Node app_lam = NodeManager::currentNM()->mkNode( APPLY_UF, lam_children );
- ret = Rewriter::rewrite( app_lam );
- Trace("model") << "Consult UF model." << std::endl;
- }
- }
- Trace("model-debug") << "check existing..." << std::endl;
- if( ret.isNull() ){
- //second, try to choose an existing term as value
- std::vector< Node > v_emp;
- ret = getDomainValue( type, v_emp );
- if( !ret.isNull() ){
- Trace("model") << "Choose existing value." << std::endl;
- }
- }
- Trace("model-debug") << "check new..." << std::endl;
- if( ret.isNull() ){
- //otherwise, choose new value
- ret = getNewDomainValue( type );
- if( !ret.isNull() ){
- Trace("model") << "Choose new value." << std::endl;
- }
- }
- if( !ret.isNull() ){
- return ret;
- }else{
- //otherwise, just return itself (this usually should not happen)
- Trace("model") << "Return self." << std::endl;
- return n;
- }
+ std::map< Node, Node >::const_iterator it = d_reps.find( val );
+ if( it!=d_reps.end() ){
+ return it->second;
+ }else{
+ return Node::null();
}
}
}
}
}
-
-
-Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){
- //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;
- }
-}
/**
* Get model value function. This function is called by getValue
*/
- Node getModelValue( TNode n );
- /** 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 );
+ Node getModelValue( TNode n ) const;
public:
/**
* Get value function. This should be called only after a ModelBuilder has called buildModel(...)
* on this model.
*/
- Node getValue( TNode n );
+ Node getValue( TNode n ) const;
/** get existing domain value, with possible exclusions
* This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
bool areDisequal( Node a, Node b );
public:
/** get value function for Exprs. */
- Expr getValue( Expr expr );
+ Expr getValue( Expr expr ) const;
/** get cardinality for sort */
- Cardinality getCardinality( Type t );
+ Cardinality getCardinality( Type t ) const;
public:
/** print representative debug function */
void printRepresentativeDebug( const char* c, Node r );
return *(*it).second;
}
-};
+};
/** TheoryEngineModelBuilder class
* This model builder will consult all theories in a theory engine for
/** process build model */
virtual void processBuildModel(TheoryModel* m, bool fullModel);
- /** choose representative for unconstrained equivalence class */
- virtual Node chooseRepresentative(TheoryModel* m, Node eqc, bool fullModel);
/** normalize representative */
Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
public:
}
}
-Node FirstOrderModel::getInterpretedValue( TNode n ){
- //Trace("fo-model") << "get interpreted value " << n << std::endl;
- /*TypeNode type = n.getType();
- if( type.isFunction() || type.isPredicate() ){
- if( d_uf_model_tree.find( n )!=d_uf_model_tree.end() ){
- if( d_uf_models.find( n )==d_uf_models.end() ){
- d_uf_models[n] = d_uf_model_tree[n].getFunctionValue( "$x" );
- }
- }
- }*/
- return TheoryModel::getInterpretedValue( n );
-}
-
-
//for evaluation of quantifier bodies
void FirstOrderModel::resetEvaluate(){
virtual ~FirstOrderModel(){}
// reset the model
void reset();
- /** get interpreted value */
- Node getInterpretedValue( TNode n );
public:
// initialize the model
void initialize( bool considerAxioms = true );
d_considerAxioms = true;
}
-Node ModelEngineBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){
- if( fullModel ){
- return TheoryEngineModelBuilder::chooseRepresentative( m, eqc, fullModel );
- }else{
- Assert( m->d_equalityEngine.hasTerm( eqc ) );
- Assert( m->d_equalityEngine.getRepresentative( eqc )==eqc );
- //avoid bad representatives
- 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 ){
- //avoid interpreted symbols
- return n.getKind()==SELECT || n.getKind()==APPLY_SELECTOR;
-}
-
void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
FirstOrderModel* fm = (FirstOrderModel*)m;
if( fullModel ){
std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
//built model uf
std::map< Node, bool > d_uf_model_constructed;
-protected:
/** process build model */
void processBuildModel( TheoryModel* m, bool fullModel );
- /** choose representative for unconstrained equivalence class */
- Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel );
- /** bad representative */
- bool isBadRepresentative( Node n );
protected:
//analyze model
void analyzeModel( FirstOrderModel* fm );
d_tmap.clear();\r
}\r
\r
+int RepSet::getNumRepresentatives( TypeNode tn ) const{\r
+ std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn );\r
+ if( it!=d_type_reps.end() ){\r
+ return (int)it->second.size();\r
+ }else{\r
+ return 0;\r
+ }\r
+}\r
+\r
void RepSet::add( Node n ){\r
TypeNode t = n.getType();\r
d_tmap[ n ] = (int)d_type_reps[t].size();\r
d_type_reps[t].push_back( n );\r
}\r
\r
+int RepSet::getIndexFor( Node n ) const {\r
+ std::map< Node, int >::const_iterator it = d_tmap.find( n );\r
+ if( it!=d_tmap.end() ){\r
+ return it->second;\r
+ }else{\r
+ return -1;\r
+ }\r
+}\r
+\r
void RepSet::complete( TypeNode t ){\r
if( d_type_complete.find( t )==d_type_complete.end() ){\r
d_type_complete[t] = true;\r
/** clear the set */\r
void clear();\r
/** has type */\r
- bool hasType( TypeNode tn ) { return d_type_reps.find( tn )!=d_type_reps.end(); }\r
+ bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }\r
+ /** get cardinality for type */\r
+ int getNumRepresentatives( TypeNode tn ) const;\r
/** add representative for type */\r
void add( Node n );\r
/** returns index in d_type_reps for node n */\r
- int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; }\r
+ int getIndexFor( Node n ) const;\r
/** complete all values */\r
void complete( TypeNode t );\r
/** debug print */\r
public:
/** get value for expression */
- virtual Expr getValue(Expr expr) = 0;
+ virtual Expr getValue(Expr expr) const = 0;
/** get cardinality for sort */
- virtual Cardinality getCardinality(Type t) = 0;
+ virtual Cardinality getCardinality(Type t) const = 0;
};/* class Model */
class ModelBuilder {
projects / cvc5.git / commitdiff