if( itut!=fm->d_uf_terms.end() ){
for( size_t i=0; i<itut->second.size(); i++ ){
Node n = itut->second[i];
- if( d_qe->getTermDatabase()->isTermActive( n ) ){
- Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;
- fapps.push_back( n );
- }
+ // only consider unique up to congruence (in model equality engine)?
+ Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;
+ fapps.push_back( n );
}
}
if( fapps.empty() ){
}
}
-Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) {
- //Assert( fm->hasTerm(n) );
- TypeNode tn = n.getType();
- if( tn.isBoolean() ){
- return areEqual(n, d_true) ? d_true : d_false;
- }else{
- if( !hasTerm(n) ){
- if( strict ){
- return Node::null();
- }else{
- Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl;
- }
- }
- return getRepresentative(n);
- }
-}
-
/*
Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;
}
}else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground eqc of this type
d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){
- Node c = getUsedRepresentative( cond[j] );
+ Node c = getRepresentative( cond[j] );
c = getRepresentative( c );
children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
}
std::map<Node, Def * > d_models;
std::map<TypeNode, Node > d_type_star;
Node intervalOp;
- Node getUsedRepresentative(Node n, bool strict = false);
/** get current model value */
void processInitializeModelForTerm(Node n);
public:
void processInitializeModelForTerm(Node n);
void processInitializeQuantifier( Node q );
void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
+ TNode getUsedRepresentative( TNode n );
public:
FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
~FirstOrderModelAbs() throw();
FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
void processInitialize( bool ispre );
unsigned getRepresentativeId( TNode n );
- TNode getUsedRepresentative( TNode n );
bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
Node getFunctionValue(Node op, const char* argPrefix );
Node getVariable( Node q, unsigned i );
if( it->first.isSort() ){
Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
for( size_t a=0; a<it->second.size(); a++ ){
- Node r = fm->getUsedRepresentative( it->second[a] );
+ Node r = fm->getRepresentative( it->second[a] );
if( Trace.isOn("fmc-model-debug") ){
std::vector< Node > eqc;
((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
Trace("fmc-model-debug") << itut->second.size() << " model values for " << op << " ... " << std::endl;
for( size_t i=0; i<itut->second.size(); i++ ){
Node n = itut->second[i];
- if( d_qe->getTermDatabase()->isTermActive( n ) ){
- add_conds.push_back( n );
- add_values.push_back( n );
- Node r = fm->getUsedRepresentative(n);
- Trace("fmc-model-debug") << n << " -> " << r << std::endl;
- //AlwaysAssert( fm->areEqual( itut->second[i], r ) );
- }else{
- if( Trace.isOn("fmc-model-debug") ){
- Node r = fm->getUsedRepresentative(n);
- Trace("fmc-model-debug") << "[redundant] " << n << " -> " << r << std::endl;
- }
- }
+ // only consider unique up to congruence (in model equality engine)?
+ add_conds.push_back( n );
+ add_values.push_back( n );
+ Node r = fm->getRepresentative(n);
+ Trace("fmc-model-debug") << n << " -> " << r << std::endl;
+ //AlwaysAssert( fm->areEqual( itut->second[i], r ) );
}
}else{
Trace("fmc-model-debug") << "No model values for " << op << " ... " << std::endl;
std::vector< Node > conds;
std::vector< Node > values;
std::vector< Node > entry_conds;
- //get the entries for the mdoel
+ //get the entries for the model
for( size_t i=0; i<add_conds.size(); i++ ){
Node c = add_conds[i];
Node v = add_values[i];
entry_children.push_back(op);
bool hasNonStar = false;
for( unsigned i=0; i<c.getNumChildren(); i++) {
- Node ri = fm->getUsedRepresentative( c[i] );
+ Node ri = fm->getRepresentative( c[i] );
children.push_back(ri);
bool isStar = false;
if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
entry_children.push_back(ri);
}
Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
- Node nv = fm->getUsedRepresentative( v );
+ Node nv = fm->getRepresentative( v );
if( !nv.isConst() ){
Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
Assert( false );
for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
std::vector< Node > inst;
for( unsigned j=0; j<fm->d_uf_terms[op][i].getNumChildren(); j++ ){
- Node r = fm->getUsedRepresentative( fm->d_uf_terms[op][i][j] );
+ Node r = fm->getRepresentative( fm->d_uf_terms[op][i][j] );
inst.push_back( r );
}
Node ev = fm->d_models[op]->evaluate( fm, inst );
Node rr = riter.getCurrentTerm( i );
Node r = rr;
//if( r.getType().isSort() ){
- r = fm->getUsedRepresentative( r );
+ r = fm->getRepresentative( r );
//}else{
// r = fm->getCurrentModelValue( r );
//}
if( !fm->hasTerm(n) ){
r = getSomeDomainElement(fm, n.getType() );
}
- r = fm->getUsedRepresentative( r );
+ r = fm->getRepresentative( r );
}
Trace("fmc-debug") << "Add constant entry..." << std::endl;
d.addEntry(fm, mkCondDefault(fm, f), r);
getSomeDomainElement( fm, tn ); //to verify the type is initialized
}
for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {
- Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );
+ Node r = fm->getRepresentative( fm->d_rep_set.d_type_reps[tn][i] );
cond[j+1] = r;
cond[k+1] = r;
d.addEntry( fm, mkCond(cond), d_true);
for( size_t i=0; i<itut->second.size(); i++ ){
Node n = fmig->d_uf_terms[op][i];
//for calculating if op is constant
- if( d_qe->getTermDatabase()->isTermActive( n ) ){
- Node v = fmig->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;
- }
+ Node v = fmig->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;
}
//for calculating terms that we don't need to consider
- if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
- if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){
- //need to consider if it is not congruent modulo model basis
- if( !tabt.addTerm( fmig, n ) ){
- d_basisNoMatch[n] = true;
- }
+ //if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
+ if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){
+ //need to consider if it is not congruent modulo model basis
+ if( !tabt.addTerm( fmig, n ) ){
+ d_basisNoMatch[n] = true;
}
}
}
smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown);
}
-bool QModelBuilderIG::isTermActive( Node n ){
- return d_qe->getTermDatabase()->isTermActive( n ) || //it is not congruent to another active term
- ( n.getAttribute(ModelBasisArgAttribute())!=0 && d_basisNoMatch.find( n )==d_basisNoMatch.end() ); //or it has model basis arguments
- //and is not congruent modulo model basis
- //to another active term
-}
-
//do exhaustive instantiation
int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
if( optUseModel() ){
if( itut!=fmig->d_uf_terms.end() ){
for( size_t i=0; i<itut->second.size(); i++ ){
Node n = itut->second[i];
- if( isTermActive( n ) ){
- Node v = fmig->getRepresentative( n );
- Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl;
- //if this assertion did not help the model, just consider it ground
- //set n = v in the model tree
- //set it as ground value
- fmig->d_uf_model_gen[op].setValue( fm, n, v );
- if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){
- //also set as default value if necessary
- if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
- Trace("fmf-model-cons") << " Set as default." << std::endl;
- fmig->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{
+ // only consider unique up to congruence (in model equality engine)?
+ Node v = fmig->getRepresentative( n );
+ Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl;
+ //if this assertion did not help the model, just consider it ground
+ //set n = v in the model tree
+ //set it as ground value
+ fmig->d_uf_model_gen[op].setValue( fm, n, v );
+ if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){
+ //also set as default value if necessary
+ if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
+ Trace("fmf-model-cons") << " Set as default." << std::endl;
+ fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
if( n==defaultTerm ){
- fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
//incidentally already set, we will not need to find a default value
setDefaultVal = false;
}
}
+ }else{
+ if( n==defaultTerm ){
+ fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
+ //incidentally already set, we will not need to find a default value
+ setDefaultVal = false;
+ }
}
}
}
~Statistics();
};
Statistics d_statistics;
- // is term active
- bool isTermActive( Node n );
// is term selected
virtual bool isTermSelected( Node n ) { return false; }
/** quantifier has inst-gen definition */
bug782.smt2 \
quant_real_univ.cvc \
constr-ground-to.smt2 \
- bug-041417-set-options.cvc
+ bug-041417-set-options.cvc \
+ alg202+1.smt2
EXTRA_DIST = $(TESTS)
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort $$unsorted 0)
+(declare-fun sorti1 ($$unsorted) Bool)
+(declare-fun op1 ($$unsorted $$unsorted) $$unsorted)
+(declare-fun sorti2 ($$unsorted) Bool)
+(declare-fun op2 ($$unsorted $$unsorted) $$unsorted)
+(declare-fun h ($$unsorted) $$unsorted)
+(declare-fun j ($$unsorted) $$unsorted)
+(assert (forall ((U $$unsorted) (BOUND_VARIABLE_345 $$unsorted)) (or (not (sorti1 U)) (not (sorti1 BOUND_VARIABLE_345)) (sorti1 (op1 U BOUND_VARIABLE_345))) ))
+(assert (forall ((U $$unsorted) (BOUND_VARIABLE_364 $$unsorted)) (or (not (sorti2 U)) (not (sorti2 BOUND_VARIABLE_364)) (sorti2 (op2 U BOUND_VARIABLE_364))) ))
+(assert (forall ((U $$unsorted)) (or (not (sorti1 U)) (= U (op1 U U))) ))
+(assert (not (forall ((U $$unsorted)) (or (not (sorti2 U)) (= U (op2 U U))) )))
+(assert (not (=> (and (forall ((U $$unsorted)) (or (not (sorti1 U)) (sorti2 (h U))) ) (forall ((V $$unsorted)) (or (not (sorti2 V)) (sorti1 (j V))) )) (not (and (forall ((W $$unsorted) (BOUND_VARIABLE_406 $$unsorted)) (or (not (sorti1 W)) (not (sorti1 BOUND_VARIABLE_406)) (= (op2 (h W) (h BOUND_VARIABLE_406)) (h (op1 W BOUND_VARIABLE_406)))) ) (forall ((Y $$unsorted) (BOUND_VARIABLE_431 $$unsorted)) (or (not (sorti2 Y)) (not (sorti2 BOUND_VARIABLE_431)) (= (op1 (j Y) (j BOUND_VARIABLE_431)) (j (op2 Y BOUND_VARIABLE_431)))) ) (forall ((X1 $$unsorted)) (or (not (sorti2 X1)) (= X1 (h (j X1)))) ) (forall ((X2 $$unsorted)) (or (not (sorti1 X2)) (= X2 (j (h X2)))) ))))))
+(assert (and (forall ((U $$unsorted)) (or (not (sorti1 U)) (sorti2 (h U))) ) (forall ((V $$unsorted)) (or (not (sorti2 V)) (sorti1 (j V))) ) (forall ((W $$unsorted) (BOUND_VARIABLE_406 $$unsorted)) (or (not (sorti1 W)) (not (sorti1 BOUND_VARIABLE_406)) (= (op2 (h W) (h BOUND_VARIABLE_406)) (h (op1 W BOUND_VARIABLE_406)))) ) (forall ((Y $$unsorted) (BOUND_VARIABLE_431 $$unsorted)) (or (not (sorti2 Y)) (not (sorti2 BOUND_VARIABLE_431)) (= (op1 (j Y) (j BOUND_VARIABLE_431)) (j (op2 Y BOUND_VARIABLE_431)))) ) (forall ((X1 $$unsorted)) (or (not (sorti2 X1)) (= X1 (h (j X1)))) ) (forall ((X2 $$unsorted)) (or (not (sorti1 X2)) (= X2 (j (h X2)))) )))
+(check-sat)
projects / cvc5.git / commitdiff