}
//cbqi options
+ // enable if pure arithmetic quantifiers
+ if( d_logic.isQuantified() && d_logic.isPure(THEORY_ARITH) ){
+ if( !options::cbqi.wasSetByUser() && !options::cbqi2.wasSetByUser() ){
+ options::cbqi2.set( true );
+ }
+ }
if( options::recurseCbqi() || options::cbqi2() ){
options::cbqi.set( true );
}
Node progr = d_tds->getNormalized( at, prog );
Node rep_prog;
std::map< Node, Node >::iterator itnp = d_normalized_to_orig[at].find( progr );
- int tsize = d_tds->getTermSize( prog );
+ int tsize = d_tds->getSygusTermSize( prog );
if( itnp==d_normalized_to_orig[at].end() ){
d_normalized_to_orig[at][progr] = prog;
if( progr.getKind()==SKOLEM && d_tds->getSygusType( progr )==at ){
//counterexample-based quantifier instantiation
if( options::cbqi() ){
- if( !options::cbqi2() || options::cbqi.wasSetByUser() ){
+ if( !options::cbqi2() ){
d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine );
d_instStrategies.push_back( d_i_splx );
- }
- if( options::cbqi2() ){
+ }else{
d_i_cegqi = new InstStrategyCegqi( d_quantEngine );
d_instStrategies.push_back( d_i_cegqi );
}
}
//if applicable, find exceptions to model via inst-gen
- if( optInstGen() ){
+ if( options::fmfInstGen() ){
d_didInstGen = true;
d_instGenMatches = 0;
d_numQuantSat = 0;
}else{
d_numQuantNoSelForm++;
}
- if( optOneQuantPerRoundInstGen() && lems>0 ){
+ if( options::fmfInstGenOneQuantPerRound() && lems>0 ){
break;
}
}else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
return false;
}
-bool QModelBuilderIG::optInstGen(){
- return options::fmfInstGen();
-}
-
-bool QModelBuilderIG::optOneQuantPerRoundInstGen(){
- return options::fmfInstGenOneQuantPerRound();
-}
-
QModelBuilderIG::Statistics::Statistics():
d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
virtual ~QModelBuilderIG() throw() {}
public:
- //whether to add inst-gen lemmas
- virtual bool optInstGen();
- //whether to only consider only quantifier per round of inst-gen
- virtual bool optOneQuantPerRoundInstGen();
/** statistics class */
class Statistics {
public:
if( it->first.isSort() ){
Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
if( Trace.isOn("model-engine-debug") ){
- Trace("model-engine-debug") << " ";
- Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+ Trace("model-engine-debug") << " Reps : ";
+ for( size_t i=0; i<it->second.size(); i++ ){
+ Trace("model-engine-debug") << it->second[i] << " ";
+ }
+ Trace("model-engine-debug") << std::endl;
+ Trace("model-engine-debug") << " Term reps : ";
for( size_t i=0; i<it->second.size(); i++ ){
- //Trace("model-engine-debug") << it->second[i] << " ";
Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
Trace("model-engine-debug") << r << " ";
}
Trace("model-engine-debug") << std::endl;
- Trace("model-engine-debug") << " Model basis term : " << mbt << std::endl;
+ Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+ Trace("model-engine-debug") << " Basis term : " << mbt << std::endl;
}
}
}
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
bool isAx = getTermDatabase()->isQAttrAxiom( f );
+ Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
//determine if we should check this quantifier
if( ( ( effort==1 && ( options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT || isAx ) ) || ( effort==0 && !isAx ) ) && mb->isQuantifierActive( f ) ){
exhaustiveInstantiate( f, e );
break;
}
}else{
- Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl;
+ Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
}
}
}
mb->d_addedLemmas = 0;
mb->d_incomplete_check = false;
if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
- Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl;
+ Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
d_triedLemmas += mb->d_triedLemmas;
d_addedLemmas += mb->d_addedLemmas;
d_incomplete_check = d_incomplete_check || mb->d_incomplete_check;
d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
}else{
- Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
- Debug("inst-fmf-ei") << " Instantiation Constants: ";
+ Trace("fmf-exh-inst-debug") << " Instantiation Constants: ";
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+ Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
}
- Debug("inst-fmf-ei") << std::endl;
+ Trace("fmf-exh-inst-debug") << std::endl;
//create a rep set iterator and iterate over the (relevant) domain of the quantifier
RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
if( riter.setQuantifier( f ) ){
- Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
- int triedLemmas = 0;
- int addedLemmas = 0;
- while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
- //instantiation was not shown to be true, construct the match
- InstMatch m( f );
- for( int i=0; i<riter.getNumTerms(); i++ ){
- m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) );
- }
- Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
- triedLemmas++;
- //add as instantiation
- if( d_quantEngine->addInstantiation( f, m ) ){
- addedLemmas++;
- }else{
- Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+ Trace("fmf-exh-inst") << "...exhaustive instantiation incomplete=" << riter.d_incomplete << "..." << std::endl;
+ if( !riter.d_incomplete || options::fmfFullSaturate() ){
+ int triedLemmas = 0;
+ int addedLemmas = 0;
+ while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
+ //instantiation was not shown to be true, construct the match
+ InstMatch m( f );
+ for( int i=0; i<riter.getNumTerms(); i++ ){
+ m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) );
+ }
+ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+ triedLemmas++;
+ //add as instantiation
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ addedLemmas++;
+ }else{
+ Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+ }
+ riter.increment();
}
- riter.increment();
+ d_addedLemmas += addedLemmas;
+ d_triedLemmas += triedLemmas;
+ d_statistics.d_exh_inst_lemmas += addedLemmas;
}
- d_addedLemmas += addedLemmas;
- d_triedLemmas += triedLemmas;
- d_statistics.d_exh_inst_lemmas += addedLemmas;
+ }else{
+ Assert( riter.d_incomplete );
}
//if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
d_incomplete_check = d_incomplete_check || riter.d_incomplete;
option fmfInstEngine --fmf-inst-engine bool :default false
use instantiation engine in conjunction with finite model finding
+option fmfFullSaturate --fmf-full-saturate bool :default false
+ instantiate with all known ground terms for infinite domain quantifiers when finite model finding
option fmfInstGen --fmf-inst-gen bool :default true
- disable Inst-Gen instantiation techniques for finite model finding
+ disable Inst-Gen instantiation techniques for finite model finding
option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
only perform Inst-Gen instantiation techniques on one quantifier per round
option fmfFreshDistConst --fmf-fresh-dc bool :default false
virtual eq::EqualityEngine* getEngine() = 0;
/** get the equivalence class of a */
virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
-
- virtual void setLiberal( bool l ) = 0;
};/* class EqualityQuery */
return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
}
-//checks whether a type is reasonably small enough such that all of its domain elements can be enumerated
+//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated
bool TermDb::mayComplete( TypeNode tn ) {
std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
if( it==d_may_complete.end() ){
}
}
-int TermDbSygus::getTermSize( Node n ){
+int TermDbSygus::getSygusTermSize( Node n ){
if( isVar( n ) ){
return 0;
}else{
int sum = 0;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- sum += getTermSize( n[i] );
+ sum += getSygusTermSize( n[i] );
}
return 1+sum;
}
Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 );
Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true );
- int getTermSize( Node n );
+ int getSygusTermSize( Node n );
/** given a term, construct an equivalent smaller one that respects syntax */
Node minimizeBuiltinTerm( Node n );
/** given a term, expand it into more basic components */
}else{
d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
}
- if( !options::finiteModelFind() ){
+ if( options::fullSaturateQuant() ){
d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
}else{
d_rel_dom = NULL;
//make it representative, this is helpful for recognizing duplication
if( mkRep ){
//pick the best possible representative for instantiation, based on past use and simplicity of term
- Node ti = d_eq_query->getInternalRepresentative( terms[i], f, i );
- //check if it is a subtype (can be violated in mixed int/real) FIXME : do this check inside getInternalRepresentative
- if( ti.getType().isSubtypeOf( f[0][i].getType() ) ){
- terms[i] = ti;
- Trace("inst-add-debug2") << " (" << terms[i] << ")";
- }
+ terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i );
}
}
Trace("inst-add-debug") << std::endl;
return true;
}else{
eq::EqualityEngine* ee = getEngine();
- if( d_liberal ){
- return true;//!areDisequal( a, b );
- }else{
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- if( ee->areEqual( a, b ) ){
- return true;
- }
+ if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+ if( ee->areEqual( a, b ) ){
+ return true;
}
- return false;
}
+ return false;
}
}
}
Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
+ Assert( f.isNull() || f.getKind()==FORALL );
Node r = getRepresentative( a );
if( !options::internalReps() ){
return r;
r = getRepresentative( r );
}else{
if( r.getType().isSort() ){
- //TODO : this can happen in rare cases
- // say x:(Array Int U), select( x, 0 ), x assigned (const @u1).
Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
+ //should never happen : UF constants should never escape model
+ Assert( false );
}
}
}
}
}
- std::map< Node, Node >::iterator itir = d_int_rep.find( r );
- if( itir==d_int_rep.end() ){
+ TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
+ std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
+ if( itir==d_int_rep[v_tn].end() ){
//find best selection for representative
Node r_best;
//if( options::fmfRelevantDomain() && !f.isNull() ){
}
Trace("internal-rep-select") << " } " << std::endl;
int r_best_score = -1;
+ TypeNode v_tn = f[0][index].getType();
for( size_t i=0; i<eqc.size(); i++ ){
- int score = getRepScore( eqc[i], f, index );
+ int score = getRepScore( eqc[i], f, index, v_tn );
if( score!=-2 ){
if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
r_best = eqc[i];
}
}
if( r_best.isNull() ){
- if( !f.isNull() ){
- Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
- r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
- }else{
- r_best = a;
- }
+ Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl;
+ r_best = r;
}
//now, make sure that no other member of the class is an instance
std::hash_map<TNode, Node, TNodeHashFunction> cache;
d_rep_score[ r_best ] = d_reset_count;
}
Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
- d_int_rep[r] = r_best;
+ d_int_rep[v_tn][r] = r_best;
if( r_best!=a ){
Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
}
}
Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
- for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
- Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
+ for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+ for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
+ Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
+ }
}
//store representatives for newly created terms
std::map< Node, Node > temp_rep_map;
bool success;
do {
success = false;
- for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
- if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
- Node ni = it->second;
- std::vector< Node > cc;
- cc.push_back( it->second.getOperator() );
- bool changed = false;
- for( unsigned j=0; j<ni.getNumChildren(); j++ ){
- if( ni[j].getType().isSort() ){
- Node r = getRepresentative( ni[j] );
- if( d_int_rep.find( r )==d_int_rep.end() ){
- Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
- r = temp_rep_map[r];
- }
- if( r==ni ){
- //found sub-term as instance
- Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
- d_int_rep[it->first] = ni[j];
+ for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+ for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
+ if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
+ Node ni = it->second;
+ std::vector< Node > cc;
+ cc.push_back( it->second.getOperator() );
+ bool changed = false;
+ for( unsigned j=0; j<ni.getNumChildren(); j++ ){
+ if( ni[j].getType().isSort() ){
+ Node r = getRepresentative( ni[j] );
+ if( itt->second.find( r )==itt->second.end() ){
+ Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
+ r = temp_rep_map[r];
+ }
+ if( r==ni ){
+ //found sub-term as instance
+ Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
+ itt->second[it->first] = ni[j];
+ changed = false;
+ success = true;
+ break;
+ }else{
+ Node ir = itt->second[r];
+ cc.push_back( ir );
+ if( ni[j]!=ir ){
+ changed = true;
+ }
+ }
+ }else{
changed = false;
- success = true;
break;
- }else{
- Node ir = d_int_rep[r];
- cc.push_back( ir );
- if( ni[j]!=ir ){
- changed = true;
- }
}
- }else{
- changed = false;
- break;
}
- }
- if( changed ){
- Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
- Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
- success = true;
- d_int_rep[it->first] = n;
- temp_rep_map[n] = it->first;
+ if( changed ){
+ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
+ Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
+ success = true;
+ itt->second[it->first] = n;
+ temp_rep_map[n] = it->first;
+ }
}
}
}
}while( success );
Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
- for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
- Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
+ for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+ for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
+ Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
+ }
}
}
}
}
+/*
int getDepth( Node n ){
if( n.getNumChildren()==0 ){
return 0;
return maxDepth;
}
}
+*/
-//smaller the score, the better
-int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
- if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){
+//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
+int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
+ if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ //reject
+ return -2;
+ }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type
return -2;
}else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
return -1;
/** pointer to theory engine */
QuantifiersEngine* d_qe;
/** internal representatives */
- std::map< Node, Node > d_int_rep;
+ std::map< TypeNode, std::map< Node, Node > > d_int_rep;
/** rep score */
std::map< Node, int > d_rep_score;
/** reset count */
int d_reset_count;
-
- bool d_liberal;
private:
/** node contains */
Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
/** get score */
- int getRepScore( Node n, Node f, int index );
+ int getRepScore( Node n, Node f, int index, TypeNode v_tn );
public:
- EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){}
+ EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
~EqualityQueryQuantifiersEngine(){}
/** reset */
void reset();
Node getInternalRepresentative( Node a, Node f, int index );
/** flatten representatives */
void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
-
- void setLiberal( bool l ) { d_liberal = l; }
}; /* EqualityQueryQuantifiersEngine */
}/* CVC4::theory namespace */
#include "theory/type_enumerator.h"
#include "theory/quantifiers/bounded_integers.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
using namespace std;
using namespace CVC4;
TypeNode tn = d_types[i];
Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl;
if( tn.isSort() ){
+ //must ensure uninterpreted type is non-empty.
if( !d_rep_set->hasType( tn ) ){
- Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" );
+ //FIXME:
+ // terms in rep_set are now constants which mapped to terms through TheoryModel
+ // thus, should introduce a constant and a term. for now, just a term.
+
+ //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
+ Node var = d_qe->getModel()->getSomeDomainElement( tn );
Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
d_rep_set->add( tn, var );
}
d_incomplete = true;
}
}
- //enumerate if the sort is reasonably small, not an Array, the upper bound of 1000 is chosen arbitrarily for now
+ //enumerate if the sort is reasonably small
}else if( d_qe->getTermDatabase()->mayComplete( tn ) ){
Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
d_rep_set->complete( tn );
+ //must have succeeded
+ Assert( d_rep_set->hasType( tn ) );
}else{
Trace("rsi") << " variable cannot be bounded." << std::endl;
Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
d_incomplete = true;
}
+ //if we have yet to determine the type of enumeration
if( d_enum_type.size()<=i ){
d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
if( d_rep_set->hasType( tn ) ){
cache.insert(n);
}
+void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ) {
+ constantReps[eqc] = const_rep;
+ Trace("model-builder") << " Assign: Setting constant rep of " << eqc << " to " << const_rep << endl;
+ if( !fullModel ){
+ tm->d_rep_set.d_values_to_terms[const_rep] = eqc;
+ }
+}
+
void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
{
if (!const_rep.isNull()) {
// Theories should not specify a rep if there is already a constant in the EC
Assert(rep.isNull() || rep == const_rep);
- constantReps[eqc] = const_rep;
+ assignConstantRep( tm, constantReps, eqc, const_rep, fullModel );
typeConstSet.add(eqct.getBaseType(), const_rep);
}
else if (!rep.isNull()) {
Node normalized = normalize(tm, n, constantReps, true);
if (normalized.isConst()) {
typeConstSet.add(tb, normalized);
- constantReps[*i2] = normalized;
+ assignConstantRep( tm, constantReps, *i2, normalized, fullModel );
Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
changed = true;
evaluated = true;
if (normalized.isConst()) {
changed = true;
typeConstSet.add(tb, normalized);
- constantReps[*i] = normalized;
+ assignConstantRep( tm, constantReps, *i, normalized, fullModel );
assertedReps.erase(*i);
i2 = i;
++i;
n = *te;
}
Assert(!n.isNull());
- constantReps[*i2] = n;
- Trace("model-builder") << " Assign: Setting constant rep of " << (*i2) << " to " << n << endl;
- if( !fullModel ){
- tm->d_rep_set.d_values_to_terms[n] = (*i2);
- }
+ assignConstantRep( tm, constantReps, *i2, n, fullModel );
changed = true;
noRepSet.erase(i2);
if (assignOne) {
Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
bool isAssignable(TNode n);
void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
-
+ void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel );
public:
TheoryEngineModelBuilder(TheoryEngine* te);
virtual ~TheoryEngineModelBuilder(){}
d_type_types[rt2] = it1->second;
d_type_types.erase( rt1 );
}else{
- //may happen for mixed int/real
+ Trace("sort-inference-debug") << "...fail : associated with types " << d_type_types[rt1] << " and " << d_type_types[rt2] << std::endl;
return;
}
}
int retType;
if( n.getKind()==kind::EQUAL ){
- //we only require that the left and right hand side must be equal
- setEqual( child_types[0], child_types[1] );
+ Trace("sort-inference-debug") << "For equality " << n << ", set equal types from : " << n[0].getType() << " " << n[1].getType() << std::endl;
+ //if original types are mixed (e.g. Int/Real), don't commit type equality in either direction
+ if( n[0].getType()!=n[1].getType() ){
+ //for now, assume the original types
+ for( unsigned i=0; i<2; i++ ){
+ int ct = getIdForType( n[i].getType() );
+ setEqual( child_types[i], ct );
+ }
+ }else{
+ //we only require that the left and right hand side must be equal
+ setEqual( child_types[0], child_types[1] );
+ }
//int eqType = getIdForType( n[0].getType() );
//setEqual( child_types[0], eqType );
//setEqual( child_types[1], eqType );
retType = getIdForType( n.getType() );
}else if( n.getKind()==kind::APPLY_UF ){
Node op = n.getOperator();
+ TypeNode tn_op = op.getType();
if( d_op_return_types.find( op )==d_op_return_types.end() ){
if( n.getType().isBoolean() ){
//use booleans
}
for( size_t i=0; i<n.getNumChildren(); i++ ){
//the argument of the operator must match the return type of the subterm
- setEqual( child_types[i], d_op_arg_types[op][i] );
+ if( n[i].getType()!=tn_op[i] ){
+ //if type mismatch, assume original types
+ Trace("sort-inference-debug") << "Argument " << i << " of " << op << " " << n[i] << " has type " << n[i].getType();
+ Trace("sort-inference-debug") << ", while operator arg has type " << tn_op[i] << std::endl;
+ int ct1 = getIdForType( n[i].getType() );
+ setEqual( child_types[i], ct1 );
+ int ct2 = getIdForType( tn_op[i] );
+ setEqual( d_op_arg_types[op][i], ct2 );
+ }else{
+ setEqual( child_types[i], d_op_arg_types[op][i] );
+ }
}
//return type is the return type
retType = d_op_return_types[op];
lst-no-self-rev-exp.smt2 \
fib-core.smt2 \
fore19-exp2-core.smt2 \
- with-ind-104-core.smt2
+ with-ind-104-core.smt2 \
+ syn002-si-real-int.smt2
EXTRA_DIST = $(TESTS)
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-sort $$unsorted 0)
+(declare-fun $$rtu (Real) $$unsorted)
+(declare-fun $$utr ($$unsorted) Real)
+(declare-fun p ($$unsorted) Bool)
+(assert (and (= ($$utr ($$rtu 12)) 12) (= ($$utr ($$rtu (/ 41 152))) (/ 41 152)) ))
+(assert (forall ((x $$unsorted)) (p x)))
+(check-sat)
projects / cvc5.git / commitdiff