include constants when reconstruct solutions for single invocation conjectures in original grammar
option cegqiSingleInvAbort --cegqi-si-abort bool :default false
abort if synthesis conjecture is not single invocation
-option cegqiUnifCondSol --cegqi-unif-csol bool :default false
- enable approach which unifies conditional solutions
option sygusNormalForm --sygus-nf bool :default true
only search for sygus builtin terms that are in normal form
option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode
template mode for sygus invariant synthesis
+option sygusUnifCondSol --sygus-unif-csol bool :default false
+ enable approach which unifies conditional solutions
option sygusDirectEval --sygus-direct-eval bool :default true
direct unfolding of evaluation functions
+option sygusCRefEval --sygus-cref-eval bool :default false
+ direct evaluation of refinement lemmas for conflict analysis
# approach applied to general quantified formulas
option cbqi --cbqi bool :read-write :default false
public:
ModelBuilder() { }
virtual ~ModelBuilder() { }
- virtual void buildModel(Model* m, bool fullModel) = 0;
+ virtual bool buildModel(Model* m) = 0;
};/* class ModelBuilder */
}/* CVC4 namespace */
options::prenexQuant.set( quantifiers::PRENEX_QUANT_NONE );
}
}
+ if( options::mbqiMode()==quantifiers::MBQI_ABS ){
+ if( !d_logic.isPure(THEORY_UF) ){
+ //MBQI_ABS is only supported in pure quantified UF
+ options::mbqiMode.set( quantifiers::MBQI_FMC );
+ }
+ }
if( options::ufssSymBreak() ){
options::sortInference.set( true );
}
//combine the equality engine
m->assertEqualityEngine( &d_equalityEngine, &termSet );
-
//get all constructors
eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
while( !eqccs_i.isFinished() ){
Node eqc = (*eqccs_i);
//for all equivalence classes that are datatypes
- if( termSet.find( eqc )==termSet.end() ){
- Trace("dt-cmi-debug") << "Irrelevant eqc : " << eqc << std::endl;
- }else{
- if( eqc.getType().isDatatype() ){
- EqcInfo* ei = getOrMakeEqcInfo( eqc );
- if( ei && !ei->d_constructor.get().isNull() ){
- Node c = ei->d_constructor.get();
- cons.push_back( c );
- eqc_cons[ eqc ] = c;
- }else{
- //if eqc contains a symbol known to datatypes (a selector), then we must assign
- //should assign constructors to EQC if they have a selector or a tester
- bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc );
- if( shouldConsider ){
- nodes.push_back( eqc );
- }
+ //if( termSet.find( eqc )==termSet.end() ){
+ // Trace("dt-cmi-debug") << "Irrelevant eqc : " << eqc << std::endl;
+ //}
+ if( eqc.getType().isDatatype() ){
+ EqcInfo* ei = getOrMakeEqcInfo( eqc );
+ if( ei && !ei->d_constructor.get().isNull() ){
+ Node c = ei->d_constructor.get();
+ cons.push_back( c );
+ eqc_cons[ eqc ] = c;
+ }else{
+ //if eqc contains a symbol known to datatypes (a selector), then we must assign
+ //should assign constructors to EQC if they have a selector or a tester
+ bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc );
+ if( shouldConsider ){
+ nodes.push_back( eqc );
}
}
}
+ //}
++eqccs_i;
}
// Compute terms appearing in assertions and shared terms
computeRelevantTerms(termSet);
- //also include non-singleton equivalence classes
+ //also include non-singleton equivalence classes TODO : revisit this
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
while( !eqcs_i.isFinished() ){
TNode r = (*eqcs_i);
TNode n = (*eqc_i);
if( first.isNull() ){
first = n;
+ //always include all datatypes
+ if( n.getType().isDatatype() ){
+ addedFirst = true;
+ termSet.insert( n );
+ }
}else{
if( !addedFirst ){
addedFirst = true;
// exit( 10 );
//}
return true;
- }else if( varChCount==1 && n.getKind()==EQUAL ){
+ }else if( varChCount==1 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){
Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl;
//expand the variable based on its finite domain
AbsDef a;
Trace("ambqi-check-debug2") << "Construct compose with variable..." << std::endl;
construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );
return true;
- }else if( varChCount==2 && n.getKind()==EQUAL ){
+ }else if( varChCount==2 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){
Trace("ambqi-check-debug2") << "Construct variable equality..." << std::endl;
//efficient expansion of the equality
construct_var_eq( m, q, vchildren[0], vchildren[1], val_none, val_none );
//------------------------model construction----------------------------
-void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
- Trace("ambqi-debug") << "process build model " << fullModel << std::endl;
+bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) {
+ Trace("ambqi-debug") << "process build model " << std::endl;
FirstOrderModel* f = (FirstOrderModel*)m;
FirstOrderModelAbs* fm = f->asFirstOrderModelAbs();
- if( fullModel ){
- Trace("ambqi-model") << "Construct model representation..." << std::endl;
- //make function values
- for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
- if( it->first.getType().getNumChildren()>1 ){
- Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl;
- m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );
- }
- }
- TheoryEngineModelBuilder::processBuildModel( m, fullModel );
- //mark that the model has been set
- fm->markModelSet();
- //debug the model
- debugModel( fm );
- }else{
- fm->initialize();
- //process representatives
- fm->d_rep_id.clear();
- fm->d_domain.clear();
-
- //initialize boolean sort
- TypeNode b = d_true.getType();
- fm->d_rep_set.d_type_reps[b].clear();
- fm->d_rep_set.d_type_reps[b].push_back( d_false );
- fm->d_rep_set.d_type_reps[b].push_back( d_true );
- fm->d_rep_id[d_false] = 0;
- fm->d_rep_id[d_true] = 1;
-
- //initialize unintpreted sorts
- Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl;
- for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
- it != fm->d_rep_set.d_type_reps.end(); ++it ){
- if( it->first.isSort() ){
- Assert( !it->second.empty() );
- //set the domain
- fm->d_domain[it->first] = 0;
- Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl;
- for( unsigned i=0; i<it->second.size(); i++ ){
- if( i<32 ){
- fm->d_domain[it->first] |= ( 1 << i );
- }
- Trace("ambqi-model") << i << " : " << it->second[i] << std::endl;
- fm->d_rep_id[it->second[i]] = i;
- }
- if( it->second.size()>=32 ){
- fm->d_domain.erase( it->first );
+ fm->initialize();
+ //process representatives
+ fm->d_rep_id.clear();
+ fm->d_domain.clear();
+
+ //initialize boolean sort
+ TypeNode b = d_true.getType();
+ fm->d_rep_set.d_type_reps[b].clear();
+ fm->d_rep_set.d_type_reps[b].push_back( d_false );
+ fm->d_rep_set.d_type_reps[b].push_back( d_true );
+ fm->d_rep_id[d_false] = 0;
+ fm->d_rep_id[d_true] = 1;
+
+ //initialize unintpreted sorts
+ Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl;
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){
+ if( it->first.isSort() ){
+ Assert( !it->second.empty() );
+ //set the domain
+ fm->d_domain[it->first] = 0;
+ Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl;
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ if( i<32 ){
+ fm->d_domain[it->first] |= ( 1 << i );
}
+ Trace("ambqi-model") << i << " : " << it->second[i] << std::endl;
+ fm->d_rep_id[it->second[i]] = i;
+ }
+ if( it->second.size()>=32 ){
+ fm->d_domain.erase( it->first );
}
}
+ }
- Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl;
- //construct the models for functions
- for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
- Node f = it->first;
- Trace("ambqi-model-debug") << "Building Model for " << f << std::endl;
- //reset the model
- it->second->clear();
- //get all (non-redundant) f-applications
- std::vector< TNode > fapps;
- Trace("ambqi-model-debug") << "Initial terms: " << std::endl;
- for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
- Node n = fm->d_uf_terms[f][i];
+ Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl;
+ //construct the models for functions
+ for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ Node f = it->first;
+ Trace("ambqi-model-debug") << "Building Model for " << f << std::endl;
+ //reset the model
+ it->second->clear();
+ //get all (non-redundant) f-applications
+ std::vector< TNode > fapps;
+ Trace("ambqi-model-debug") << "Initial terms: " << std::endl;
+ std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( f );
+ 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 );
}
}
- if( fapps.empty() ){
- //choose arbitrary value
- Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
- Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl;
- fapps.push_back( mbt );
- }
- bool fValid = true;
- for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){
- if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){
- Trace("ambqi-model") << "Interpretation of " << f << " is not valid.";
- Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl;
- fValid = false;
- break;
- }
+ }
+ if( fapps.empty() ){
+ //choose arbitrary value
+ Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
+ Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl;
+ fapps.push_back( mbt );
+ }
+ bool fValid = true;
+ for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){
+ if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){
+ Trace("ambqi-model") << "Interpretation of " << f << " is not valid.";
+ Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl;
+ fValid = false;
+ break;
}
- fm->d_models_valid[f] = fValid;
- if( fValid ){
- //construct the ambqi model
- it->second->construct_func( fm, fapps );
- Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;
- it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );
- Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;
- it->second->simplify( fm, TNode::null(), fapps[0] );
- Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;
- it->second->debugPrint("ambqi-model", fm, fapps[0] );
+ }
+ fm->d_models_valid[f] = fValid;
+ if( fValid ){
+ //construct the ambqi model
+ it->second->construct_func( fm, fapps );
+ Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;
+ it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );
+ Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;
+ it->second->simplify( fm, TNode::null(), fapps[0] );
+ Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;
+ it->second->debugPrint("ambqi-model", fm, fapps[0] );
/*
- if( Debug.isOn("ambqi-model-debug") ){
- for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
- Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
- Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
- Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
- }
+ if( Debug.isOn("ambqi-model-debug") ){
+ for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
+ Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
+ Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
+ Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
}
-*/
}
+*/
+ }
+ }
+ Trace("ambqi-model") << "Construct model representation..." << std::endl;
+ //make function values
+ for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ if( it->first.getType().getNumChildren()>1 ){
+ Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl;
+ m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );
}
}
+ Assert( d_addedLemmas==0 );
+ return TheoryEngineModelBuilder::processBuildModel( m );
}
AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe );
~AbsMbqiBuilder() throw() {}
//process build model
- void processBuildModel(TheoryModel* m, bool fullModel);
+ bool processBuildModel(TheoryModel* m);
//do exhaustive instantiation
int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
};
getBounds( f, v, rsi, l, u );
Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;
if( !l.isNull() ){
- l = d_quantEngine->getModel()->getCurrentModelValue( l );
+ l = d_quantEngine->getModel()->getValue( l );
}
if( !u.isNull() ){
- u = d_quantEngine->getModel()->getCurrentModelValue( u );
+ u = d_quantEngine->getModel()->getValue( u );
}
Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;
return;
Node sr = getSetRange( q, v, rsi );
if( !sr.isNull() ){
Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
- sr = d_quantEngine->getModel()->getCurrentModelValue( sr );
+ sr = d_quantEngine->getModel()->getValue( sr );
//if non-constant, then sr does not occur in the model, we fail
if( !sr.isConst() ){
return Node::null();
for( unsigned i = 0; it != it_end; ++ it, ++i ){
Node lit = (*it).assertion;
if( lit.getKind()==kind::MEMBER ){
- Node vr = d_quantEngine->getModel()->getCurrentModelValue( lit[0] );
+ Node vr = d_quantEngine->getModel()->getValue( lit[0] );
Trace("bound-int-rsi-debug") << "....membership for " << lit << " ==> " << vr << std::endl;
Trace("bound-int-rsi-debug") << " " << (val_to_term.find( vr )!=val_to_term.end()) << " " << d_quantEngine->getEqualityQuery()->areEqual( d_setm_range_lit[q][v][1], lit[1] ) << std::endl;
if( val_to_term.find( vr )!=val_to_term.end() ){
}
}
}
- if( options::cegqiUnifCondSol() ){
+ if( options::sygusUnifCondSol() ){
// for each variable, determine whether we can do conditional counterexamples
for( unsigned i=0; i<d_candidates.size(); i++ ){
registerCandidateConditional( d_candidates[i] );
}
void CegConjecture::getConditionalCandidateList( std::vector< Node >& clist, Node curr, bool reqAdd ){
- Assert( options::cegqiUnifCondSol() );
+ Assert( options::sygusUnifCondSol() );
std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr );
if( it!=d_cinfo.end() ){
if( !it->second.d_csol_cond.isNull() ){
}
void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) {
- if( options::cegqiUnifCondSol() && !forceOrig ){
+ if( options::sygusUnifCondSol() && !forceOrig ){
for( unsigned i=0; i<d_candidates.size(); i++ ){
getConditionalCandidateList( clist, d_candidates[i], true );
}
}
Node CegConjecture::constructConditionalCandidate( std::map< Node, Node >& cmv, Node curr ) {
- Assert( options::cegqiUnifCondSol() );
+ Assert( options::sygusUnifCondSol() );
std::map< Node, Node >::iterator itc = cmv.find( curr );
if( itc!=cmv.end() ){
return itc->second;
bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values ) {
Assert( clist.size()==model_values.size() );
- if( options::cegqiUnifCondSol() ){
+ if( options::sygusUnifCondSol() ){
std::map< Node, Node > cmv;
for( unsigned i=0; i<clist.size(); i++ ){
cmv[ clist[i] ] = model_values[i];
//must get a counterexample to the value of the current candidate
Node inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() );
bool hasActiveConditionalNode = false;
- if( options::cegqiUnifCondSol() ){
+ if( options::sygusUnifCondSol() ){
//TODO
hasActiveConditionalNode = true;
}
}
Node CegConjecture::getActiveConditional( Node curr ) {
- Assert( options::cegqiUnifCondSol() );
+ Assert( options::sygusUnifCondSol() );
std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr );
Assert( it!=d_cinfo.end() );
if( !it->second.d_csol_cond.isNull() ){
std::map< Node, std::vector< Node > > csol_ccond_ret;
std::map< Node, std::map< Node, bool > > csol_cpol;
std::vector< Node > csol_vals;
- if( options::cegqiUnifCondSol() ){
+ if( options::sygusUnifCondSol() ){
std::vector< Node > new_active_measure_sum;
- Trace("cegqi-unif") << "Conditional solution refinement, expand active conditional nodes" << std::endl;
+ Trace("sygus-unif") << "Conditional solution refinement, expand active conditional nodes" << std::endl;
for( unsigned i=0; i<d_candidates.size(); i++ ){
Node v = d_candidates[i];
Node ac = getActiveConditional( v );
//if it is a conditional
if( !d_cinfo[ac].d_csol_cond.isNull() ){
//activate
- Trace("cegqi-unif") << "****** For " << v << ", expanding an active conditional node : " << ac << std::endl;
+ Trace("sygus-unif") << "****** For " << v << ", expanding an active conditional node : " << ac << std::endl;
d_cinfo[ac].d_csol_status = 0; //TODO
- Trace("cegqi-unif") << "...expanded to " << d_cinfo[ac].d_csol_op << "( ";
- Trace("cegqi-unif") << d_cinfo[ac].d_csol_cond << ", " << d_cinfo[ac].d_csol_var[0] << ", ";
- Trace("cegqi-unif") << d_cinfo[ac].d_csol_var[1] << " )" << std::endl;
+ Trace("sygus-unif") << "...expanded to " << d_cinfo[ac].d_csol_op << "( ";
+ Trace("sygus-unif") << d_cinfo[ac].d_csol_cond << ", " << d_cinfo[ac].d_csol_var[0] << ", ";
+ Trace("sygus-unif") << d_cinfo[ac].d_csol_var[1] << " )" << std::endl;
registerCandidateConditional( d_cinfo[ac].d_csol_var[1-d_cinfo[ac].d_csol_status] );
//add to measure sum
Node acfc = getMeasureTermFactor( d_cinfo[ac].d_csol_cond );
csol_cond[v] = d_cinfo[ac].d_csol_cond;
csol_vals.push_back( d_cinfo[ac].d_csol_var[d_cinfo[ac].d_csol_status] );
}else{
- Trace("cegqi-unif") << "* For " << v << ", its active node " << ac << " is not a conditional node." << std::endl;
+ Trace("sygus-unif") << "* For " << v << ", its active node " << ac << " is not a conditional node." << std::endl;
//if we have not already included this in the measure, do so
if( d_cinfo[ac].d_csol_status==0 ){
Node acf = getMeasureTermFactor( ac );
csol_vals.push_back( ac );
}
if( !csol_ccond[v].empty() ){
- Trace("cegqi-unif") << "...it is nested under " << csol_ccond[v].size() << " other conditionals" << std::endl;
+ Trace("sygus-unif") << "...it is nested under " << csol_ccond[v].size() << " other conditionals" << std::endl;
}
}
// must add to active measure
if( !new_active_measure_sum.empty() ){
+ Node mcsum = new_active_measure_sum.size()==1 ? new_active_measure_sum[0] : NodeManager::currentNM()->mkNode( kind::PLUS, new_active_measure_sum );
+ Node mclem = NodeManager::currentNM()->mkNode( kind::LEQ, mcsum, d_active_measure_term );
+ Trace("cegqi-lemma") << "Cegqi::Lemma : Measure component lemma : " << mclem << std::endl;
+ d_qe->getOutputChannel().lemma( mclem );
+/*
+ for( unsigned i=0; i<new_active_measure_sum.size(); i++ ){
+ Node mclem = NodeManager::currentNM()->mkNode( kind::LEQ, new_active_measure_sum[i], d_active_measure_term );
+ Trace("cegqi-lemma") << "Cegqi::Lemma : Measure component lemma : " << mclem << std::endl;
+ d_qe->getOutputChannel().lemma( mclem );
+ }
+ */
+ /*
Node new_active_measure = NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() );
new_active_measure_sum.push_back( new_active_measure );
Node namlem = NodeManager::currentNM()->mkNode( kind::GEQ, new_active_measure, NodeManager::currentNM()->mkConst(Rational(0)));
Trace("cegqi-lemma") << "Cegqi::Lemma : Measure expansion : " << namlem << std::endl;
d_qe->getOutputChannel().lemma( namlem );
d_active_measure_term = new_active_measure;
+ */
}
}
Trace("cegqi-refine") << "Refine " << d_ce_sk.size() << " points." << std::endl;
}
}
//compute the body, inst_cond
- if( options::cegqiUnifCondSol() && !c_disj.isNull() ){
- Trace("cegqi-unif") << "Process " << c_disj << std::endl;
+ if( options::sygusUnifCondSol() && !c_disj.isNull() ){
+ Trace("sygus-unif") << "Process " << c_disj << std::endl;
c_disj = purifyConditionalEvaluations( c_disj, csol_cond, psubs, psubs_visited );
- Trace("cegqi-unif") << "Purified to : " << c_disj << std::endl;
- Trace("cegqi-unif") << "...now with " << psubs.size() << " definitions." << std::endl;
+ Trace("sygus-unif") << "Purified to : " << c_disj << std::endl;
+ Trace("sygus-unif") << "...now with " << psubs.size() << " definitions." << std::endl;
}else{
//standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification
}
}
}
if( success ){
- Trace("cegqi-unif") << "Add conditional assumptions for " << psubs.size() << " evaluations." << std::endl;
+ Assert( sk_vars.size()==sk_subs.size() );
+ Trace("sygus-unif") << "Add conditional assumptions for " << psubs.size() << " evaluations." << std::endl;
//add conditional correctness assumptions
- std::map< Node, Node > psubs_condc;
+ std::vector< Node > psubs_condc;
std::map< Node, std::vector< Node > > psubs_apply;
std::vector< Node > paux_vars;
for( std::map< Node, Node >::iterator itp = psubs.begin(); itp != psubs.end(); ++itp ){
}
Node c = csol_cond[itp->first[0]];
psubs_apply[ c ].push_back( itp->first );
- Trace("cegqi-unif") << " process assumption " << itp->first << " == " << itp->second << ", with current condition " << c;
- Trace("cegqi-unif") << ", and " << csol_ccond[itp->first[0]].size() << " context conditionals." << std::endl;
+ Trace("sygus-unif") << " process assumption " << itp->first << " == " << itp->second << ", with current condition " << c;
+ Trace("sygus-unif") << ", and " << csol_ccond[itp->first[0]].size() << " context conditionals." << std::endl;
std::vector< Node> assm;
if( !c.isNull() ){
assm.push_back( mkConditional( c, args ) );
}
Assert( !assm.empty() );
Node condn = assm.size()==1 ? assm[0] : NodeManager::currentNM()->mkNode( kind::AND, assm );
- Node cond = NodeManager::currentNM()->mkNode( kind::IMPLIES, condn, itp->first.eqNode( itp->second ) );
- psubs_condc[itp->first] = cond;
- Trace("cegqi-unif") << " ...made conditional correctness assumption : " << cond << std::endl;
- }
- for( std::map< Node, Node >::iterator itp = psubs_condc.begin(); itp != psubs_condc.end(); ++itp ){
- lem_c.push_back( itp->second );
+ Node cond = NodeManager::currentNM()->mkNode( kind::OR, condn.negate(), itp->first.eqNode( itp->second ) );
+ cond = cond.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() );
+ cond = cond.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+ psubs_condc.push_back( cond );
+ Trace("sygus-unif") << " ...made conditional correctness assumption : " << cond << std::endl;
}
- Node lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
- //substitute the actual return values
- if( options::cegqiUnifCondSol() ){
- Assert( d_candidates.size()==csol_vals.size() );
- lem = lem.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() );
- }
+ Node base_lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
- //previous non-ground conditional refinement lemmas must satisfy the current point
- for( unsigned i=0; i<d_refinement_lemmas.size(); i++ ){
- Node prev_lem = d_refinement_lemmas[i];
- prev_lem = prev_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
- //do auxiliary variable substitution
- std::vector< Node > subs;
- for( unsigned ii=0; ii<d_refinement_lemmas_aux_vars[i].size(); ii++ ){
- subs.push_back( NodeManager::currentNM()->mkSkolem( "y", d_refinement_lemmas_aux_vars[i][ii].getType(),
- "purification variable for non-ground sygus conditional solution" ) );
- }
- prev_lem = prev_lem.substitute( d_refinement_lemmas_aux_vars[i].begin(), d_refinement_lemmas_aux_vars[i].end(), subs.begin(), subs.end() );
- prev_lem = Rewriter::rewrite( prev_lem );
- prev_lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), prev_lem );
- Trace("cegqi-unif") << "...previous conditional refinement lemma with new counterexample : " << prev_lem << std::endl;
- lems.push_back( prev_lem );
- }
- if( !isGround() && !csol_cond.empty() ){
- Trace("cegqi-unif") << "Lemma " << lem << " is a non-ground conditional refinement lemma, store it for future instantiation." << std::endl;
- d_refinement_lemmas.push_back( lem );
- d_refinement_lemmas_aux_vars.push_back( paux_vars );
- }
-
- if( options::cegqiUnifCondSol() ){
- Trace("cegqi-unif") << "We have lemma : " << lem << std::endl;
- Trace("cegqi-unif") << "Now add progress assertions..." << std::endl;
+ if( options::sygusUnifCondSol() ){
+ //substitute the actual return values
+ Assert( d_candidates.size()==csol_vals.size() );
+ base_lem = base_lem.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() );
+ Trace("sygus-unif") << "We have base lemma : " << base_lem << std::endl;
+ //progress lemmas
+ Trace("sygus-unif") << "Now add progress assertions..." << std::endl;
std::vector< Node > prgr_conj;
std::map< Node, bool > cprocessed;
for( std::map< Node, Node >::iterator itc = csol_cond.begin(); itc !=csol_cond.end(); ++itc ){
Node x = itc->first;
Node c = itc->second;
if( !c.isNull() ){
- Trace("cegqi-unif") << " process conditional " << c << " for " << x << ", which was applied " << psubs_apply[c].size() << " times." << std::endl;
+ Trace("sygus-unif") << " process conditional " << c << " for " << x << ", which was applied " << psubs_apply[c].size() << " times." << std::endl;
//make the progress point
Assert( x.getType().isDatatype() );
const Datatype& dx = ((DatatypeType)x.getType().toType()).getDatatype();
}
}
//the condition holds for the point
- prgr_conj.push_back( mkConditional( c, prgr_pt ) );
+ Node cplem = mkConditional( c, prgr_pt );
// ...and not for its context, if this return point is different from them
//for( unsigned j=0; j<csol_ccond[x].size(); j++ ){
// Node cc = csol_ccond[x][j];
// prgr_conj.push_back( mkConditional( cc, prgr_pt, csol_cpol[x][cc] ) );
//}
//FIXME
+ d_refinement_lemmas_cprogress.push_back( cplem );
+ d_refinement_lemmas_cprogress_pts.push_back( prgr_pt );
+ prgr_conj.push_back( cplem );
}
}
if( !prgr_conj.empty() ){
Node prgr_lem = prgr_conj.size()==1 ? prgr_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, prgr_conj );
prgr_lem = prgr_lem.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() );
- Trace("cegqi-unif") << "Progress lemma is " << prgr_lem << std::endl;
- lem = NodeManager::currentNM()->mkNode( kind::AND, lem, prgr_lem );
+ prgr_lem = prgr_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+ prgr_lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), prgr_lem );
+ Trace("sygus-unif") << "Progress lemma is " << prgr_lem << std::endl;
+ lems.push_back( prgr_lem );
+ }
+
+ //previous non-ground conditional refinement lemmas must satisfy the current point
+ if( !isGround() ){
+ for( unsigned i=0; i<d_refinement_lemmas.size(); i++ ){
+ Node prev_lem = d_refinement_lemmas[i];
+ prev_lem = prev_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+ //do auxiliary variable substitution
+ std::vector< Node > subs;
+ for( unsigned ii=0; ii<d_refinement_lemmas_aux_vars[i].size(); ii++ ){
+ subs.push_back( NodeManager::currentNM()->mkSkolem( "y", d_refinement_lemmas_aux_vars[i][ii].getType(),
+ "purification variable for non-ground sygus conditional solution" ) );
+ }
+ prev_lem = prev_lem.substitute( d_refinement_lemmas_aux_vars[i].begin(), d_refinement_lemmas_aux_vars[i].end(), subs.begin(), subs.end() );
+ prev_lem = Rewriter::rewrite( prev_lem );
+ Trace("sygus-unif") << "...previous conditional refinement lemma with new counterexample : " << prev_lem << std::endl;
+ lems.push_back( prev_lem );
+ }
}
- //make in terms of new values
- Assert( csol_vals.size()==d_candidates.size() );
- Trace("cegqi-unif") << "Now rewrite in terms of new evaluation branches...got " << lem << std::endl;
}
- //apply the substitution
- Assert( sk_vars.size()==sk_subs.size() );
- lem = lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+
+ //make the base lemma
+ base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+ d_refinement_lemmas_base.push_back( base_lem );
+
+ Node lem = base_lem;
+
+ if( options::sygusUnifCondSol() ){
+ d_refinement_lemmas_ceval.push_back( psubs_condc );
+ //add the conditional evaluation
+ if( !psubs_condc.empty() ){
+ std::vector< Node > children;
+ children.push_back( base_lem );
+ children.insert( children.end(), psubs_condc.begin(), psubs_condc.end() );
+ lem = NodeManager::currentNM()->mkNode( AND, children );
+ }
+ }
+
lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem );
lem = Rewriter::rewrite( lem );
lems.push_back( lem );
+
+ d_refinement_lemmas.push_back( lem );
+ d_refinement_lemmas_aux_vars.push_back( paux_vars );
}
}
d_ce_sk.clear();
//fairness
if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
std::vector< Node > mc;
- if( options::cegqiUnifCondSol() ||
+ if( options::sygusUnifCondSol() ||
d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED ){
//measure term is a fresh constant
mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) );
std::vector< Node > model_values;
if( conj->getModelValues( clist, model_values ) ){
if( options::sygusDirectEval() ){
+ bool addedEvalLemmas = false;
+ if( options::sygusCRefEval() ){
+ Trace("cegqi-debug") << "Do cref evaluation..." << std::endl;
+ // see if any refinement lemma is refuted by evaluation
+ std::vector< Node > cre_lems;
+ getCRefEvaluationLemmas( conj, clist, model_values, cre_lems );
+ if( !cre_lems.empty() ){
+ Trace("cegqi-engine") << " *** Do conjecture refinement evaluation..." << std::endl;
+ for( unsigned j=0; j<cre_lems.size(); j++ ){
+ Node lem = cre_lems[j];
+ Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem << std::endl;
+ if( d_quantEngine->addLemma( lem ) ){
+ addedEvalLemmas = true;
+ }
+ }
+ if( addedEvalLemmas ){
+ return;
+ }
+ }
+ }
Trace("cegqi-debug") << "Do direct evaluation..." << std::endl;
- std::vector< Node > eager_eval_lem;
+ std::vector< Node > eager_terms;
+ std::vector< Node > eager_vals;
+ std::vector< Node > eager_exps;
for( unsigned j=0; j<clist.size(); j++ ){
- Trace("cegqi-debug") << " register " << clist[j] << " -> " << model_values[j] << std::endl;
- d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_eval_lem );
+ Trace("cegqi-debug") << " register " << clist[j] << " -> " << model_values[j] << std::endl;
+ d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_terms, eager_vals, eager_exps );
}
- Trace("cegqi-debug") << "...produced " << eager_eval_lem.size() << " eager evaluation lemmas." << std::endl;
- if( !eager_eval_lem.empty() ){
+ Trace("cegqi-debug") << "...produced " << eager_terms.size() << " eager evaluation lemmas." << std::endl;
+ if( !eager_terms.empty() ){
Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl;
- for( unsigned j=0; j<eager_eval_lem.size(); j++ ){
- Node lem = eager_eval_lem[j];
+ for( unsigned j=0; j<eager_terms.size(); j++ ){
+ Node lem = NodeManager::currentNM()->mkNode( kind::OR, eager_exps[j].negate(), eager_terms[j].eqNode( eager_vals[j] ) );
if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){
//FIXME: hack to incorporate hacks from BV for division by zero
lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem );
}
Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl;
- d_quantEngine->addLemma( lem );
+ if( d_quantEngine->addLemma( lem ) ){
+ addedEvalLemmas = true;
+ }
}
+ }
+ if( addedEvalLemmas ){
return;
}
}
}
}
+void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems ) {
+ if( conj->getNumRefinementLemmas()>0 ){
+ Assert( vs.size()==ms.size() );
+ std::map< Node, Node > vtm;
+ for( unsigned i=0; i<vs.size(); i++ ){
+ vtm[vs[i]] = ms[i];
+ }
+ std::map< Node, Node > visited;
+ std::map< Node, std::vector< Node > > exp;
+ for( unsigned i=0; i<conj->getNumRefinementLemmas(); i++ ){
+ Node lem;
+ std::vector< Node > cvars;
+ if( options::sygusUnifCondSol() ){
+ //TODO : progress lemma
+ std::map< Node, Node > visitedc;
+ std::map< Node, std::vector< Node > > expc;
+ for( unsigned j=0; j<conj->getNumConditionalEvaluations( i ); j++ ){
+ Node ce = conj->getConditionalEvaluation( i, j );
+ Node cee = crefEvaluate( ce, vtm, visitedc, expc );
+ Trace("sygus-cref-eval") << "Check conditional evaluation : " << ce << ", evaluates to " << cee << std::endl;
+ if( !cee.isNull() && cee.getKind()==kind::EQUAL ){
+ // the conditional holds, we will apply this as a substitution
+ for( unsigned r=0; r<2; r++ ){
+ if( cee[r].isVar() && cee[1-r].isConst() ){
+ Node v = cee[r];
+ Node c = cee[1-r];
+ cvars.push_back( v );
+ Assert( exp.find( v )==exp.end() );
+ //TODO : should also carry symbolic solution (do not eagerly unfold conclusion of ce)
+ visited[v] = c;
+ exp[v].insert( exp[v].end(), expc[ce].begin(), expc[ce].end() );
+ Trace("sygus-cref-eval") << " consider " << v << " -> " << c << std::endl;
+ break;
+ }
+ }
+ }
+ }
+ if( !cvars.empty() ){
+ lem = conj->getRefinementBaseLemma( i );
+ }
+ }else{
+ lem = conj->getRefinementBaseLemma( i );
+ }
+ if( !lem.isNull() ){
+ Trace("sygus-cref-eval") << "Check refinement lemma " << lem << " against current model." << std::endl;
+ Node elem = crefEvaluate( lem, vtm, visited, exp );
+ Trace("sygus-cref-eval") << "...evaluated to " << elem << ", exp size = " << exp[lem].size() << std::endl;
+ if( !elem.isNull() ){
+ bool success = false;
+ success = elem==d_quantEngine->getTermDatabase()->d_false;
+ if( success ){
+ elem = conj->getGuard().negate();
+ Node cre_lem;
+ if( !exp[lem].empty() ){
+ Node en = exp[lem].size()==1 ? exp[lem][0] : NodeManager::currentNM()->mkNode( kind::AND, exp[lem] );
+ cre_lem = NodeManager::currentNM()->mkNode( kind::OR, en.negate(), elem );
+ }else{
+ cre_lem = elem;
+ }
+ if( std::find( lems.begin(), lems.end(), cre_lem )==lems.end() ){
+ Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem << std::endl;
+ lems.push_back( cre_lem );
+ }
+ }
+ }
+ }
+ // clean up caches
+ for( unsigned j=0; j<cvars.size(); j++ ){
+ visited.erase( cvars[j] );
+ exp.erase( cvars[j] );
+ }
+ }
+ }
+}
+
+Node CegInstantiation::crefEvaluate( Node n, std::map< Node, Node >& vtm, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& exp ){
+ std::map< Node, Node >::iterator itv = visited.find( n );
+ if( itv!=visited.end() ){
+ return itv->second;
+ }else{
+ std::vector< Node > exp_c;
+ Node ret;
+ if( n.getKind()==kind::APPLY_UF ){
+ //it is an evaluation function
+ Trace("sygus-cref-eval-debug") << "Compute evaluation for : " << n << std::endl;
+ //unfold by one step
+ Node nn = d_quantEngine->getTermDatabaseSygus()->unfold( n, vtm, exp[n] );
+ Trace("sygus-cref-eval-debug") << "...unfolded once to " << nn << std::endl;
+ Assert( nn!=n );
+ //it is the result of evaluating the unfolding
+ ret = crefEvaluate( nn, vtm, visited, exp );
+ //carry explanation
+ exp_c.push_back( nn );
+ }
+ if( ret.isNull() ){
+ if( n.getNumChildren()>0 ){
+ std::vector< Node > children;
+ bool childChanged = false;
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nc = crefEvaluate( n[i], vtm, visited, exp );
+ childChanged = nc!=n[i] || childChanged;
+ children.push_back( nc );
+ //Boolean short circuiting
+ if( n.getKind()==kind::AND ){
+ if( nc==d_quantEngine->getTermDatabase()->d_false ){
+ ret = nc;
+ exp_c.clear();
+ }
+ }else if( n.getKind()==kind::OR ){
+ if( nc==d_quantEngine->getTermDatabase()->d_true ){
+ ret = nc;
+ exp_c.clear();
+ }
+ }else if( n.getKind()==kind::ITE && i==0 ){
+ int index = -1;
+ if( nc==d_quantEngine->getTermDatabase()->d_true ){
+ index = 1;
+ }else if( nc==d_quantEngine->getTermDatabase()->d_false ){
+ index = 2;
+ }
+ if( index!=-1 ){
+ ret = crefEvaluate( n[index], vtm, visited, exp );
+ exp_c.push_back( n[index] );
+ }
+ }
+ //carry explanation
+ exp_c.push_back( n[i] );
+ if( !ret.isNull() ){
+ break;
+ }
+ }
+ if( ret.isNull() ){
+ if( childChanged ){
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ ret = Rewriter::rewrite( ret );
+ }else{
+ ret = n;
+ }
+ }
+ }else{
+ ret = n;
+ }
+ }
+ //carry explanation from children
+ for( unsigned i=0; i<exp_c.size(); i++ ){
+ Node nn = exp_c[i];
+ std::map< Node, std::vector< Node > >::iterator itx = exp.find( nn );
+ if( itx!=exp.end() ){
+ for( unsigned j=0; j<itx->second.size(); j++ ){
+ if( std::find( exp[n].begin(), exp[n].end(), itx->second[j] )==exp[n].end() ){
+ exp[n].push_back( itx->second[j] );
+ }
+ }
+ }
+ }
+ Trace("sygus-cref-eval-debug") << "... evaluation of " << n << " is (" << ret.getKind() << ") " << ret << std::endl;
+ Trace("sygus-cref-eval-debug") << "...... exp size = " << exp[n].size() << std::endl;
+ visited[n] = ret;
+ return ret;
+ }
+}
+
void CegInstantiation::registerMeasuredType( TypeNode tn ) {
std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn );
if( it==d_uf_measure.end() ){
/** refinement lemmas */
std::vector< Node > d_refinement_lemmas;
std::vector< std::vector< Node > > d_refinement_lemmas_aux_vars;
+ std::vector< Node > d_refinement_lemmas_base;
+ std::vector< std::vector< Node > > d_refinement_lemmas_ceval;
+ std::vector< Node > d_refinement_lemmas_cprogress;
+ std::vector< std::vector< Node > > d_refinement_lemmas_cprogress_pts;
private: //for condition solutions
/** get candidate list recursively for conditional solutions */
void getConditionalCandidateList( std::vector< Node >& clist, Node curr, bool reqAdd );
bool getModelValues( std::vector< Node >& n, std::vector< Node >& v );
/** get model value */
Node getModelValue( Node n );
+ /** get number of refinement lemmas */
+ unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); }
+ /** get refinement lemma */
+ Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; }
+ /** get refinement lemma */
+ Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; }
+ /** get num conditional evaluations */
+ unsigned getNumConditionalEvaluations( unsigned i ) { return d_refinement_lemmas_ceval[i].size(); }
+ /** get conditional evaluation */
+ Node getConditionalEvaluation( unsigned i, unsigned j ) { return d_refinement_lemmas_ceval[i][j]; }
+ /** get progress lemma */
+ Node getConditionalProgressLemma( unsigned i ) { return d_refinement_lemmas_cprogress[i]; }
};
std::map< Node, std::map< int, Node > > d_size_term_lemma;
/** get measure lemmas */
void getMeasureLemmas( Node n, Node v, std::vector< Node >& lems );
+private: //for direct evaluation
+ /** get refinement evaluation */
+ void getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems );
+ Node crefEvaluate( Node lem, std::map< Node, Node >& vtm, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& exp );
/** get eager unfolding */
Node getEagerUnfold( Node n, std::map< Node, Node >& visited );
private:
FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) :
TheoryModel( c, name, true ),
-d_qe( qe ), d_forall_asserts( c ), d_isModelSet( c, false ){
+d_qe( qe ), d_forall_asserts( c ){
d_rlv_count = 0;
}
}
}
-//AJR : FIXME : this function is only used by bounded integers, can likely be removed.
-Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
- std::vector< Node > children;
- if( n.getNumChildren()>0 ){
- if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.push_back( n.getOperator() );
- }
- for (unsigned i=0; i<n.getNumChildren(); i++) {
- Node nc = getCurrentModelValue( n[i], partial );
- if (nc.isNull()) {
- return Node::null();
- }else{
- children.push_back( nc );
- }
- }
- if( n.getKind()==APPLY_UF ){
- return getCurrentUfModelValue( n, children, partial );
- }else{
- Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
- nn = Rewriter::rewrite( nn );
- return nn;
- }
- }else{
- //return getRepresentative(n);
- return getValue(n);
- }
-}
-
void FirstOrderModel::initialize() {
processInitialize( true );
//this is called after representatives have been chosen and the equality engine has been built
}
}
+/*
Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
std::vector< Node > children;
children.push_back(n.getOperator());
return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex );
}
}
-
+*/
}
}
+/*
Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;
for(unsigned i=0; i<args.size(); i++) {
Assert( n.getKind()==APPLY_UF );
return d_models[n.getOperator()]->evaluate(this, args);
}
+*/
void FirstOrderModelFmc::processInitialize( bool ispre ) {
if( ispre ){
return Node::null();
}
+/*
Node FirstOrderModelAbs::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
Debug("qint-debug") << "get curr uf value " << n << std::endl;
if( d_models_valid[n] ){
return Node::null();
}
}
+*/
void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) {
if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){
std::vector< Node > d_forall_rlv_vec;
Node d_last_forall_rlv;
std::vector< Node > d_forall_rlv_assert;
- /** is model set */
- context::CDO< bool > d_isModelSet;
/** get variable id */
std::map< Node, std::map< Node, int > > d_quant_var_id;
- /** get current model value */
- virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
+ /** get current model value (deprecated) */
+ //virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
public: //for Theory Quantifiers:
/** assert quantifier */
void assertQuantifier( Node n );
// initialize the model
void initialize();
virtual void processInitialize( bool ispre ) = 0;
- /** mark model set */
- void markModelSet() { d_isModelSet = true; }
- /** is model set */
- bool isModelSet() { return d_isModelSet; }
- /** get current model value */
- Node getCurrentModelValue( Node n, bool partial = false );
/** get variable id */
int getVariableId(TNode q, TNode n) {
return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
//index ordering to use for each term
std::map< Node, std::vector< int > > d_eval_term_index_order;
void makeEvalUfIndexOrder( Node n );
- /** get current model value */
- Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
//the following functions are for evaluating quantifier bodies
public:
FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
Node intervalOp;
Node getUsedRepresentative(Node n, bool strict = false);
/** get current model value */
- Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
void processInitializeModelForTerm(Node n);
public:
FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
std::map< Node, std::map< int, int > > d_var_index;
private:
/** get current model value */
- Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
void processInitializeModelForTerm(Node n);
void processInitializeQuantifier( Node q );
void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
}
void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
+ Trace("fmc-simplify") << "Simplify definition, #cond = " << d_cond.size() << std::endl;
basic_simplify( m );
+ Trace("fmc-simplify") << "post-basic simplify, #cond = " << d_cond.size() << std::endl;
//check if the last entry is not all star, if so, we can make the last entry all stars
if( !d_cond.empty() ){
Trace("fmc-cover-simplify") << std::endl;
}
}
+ Trace("fmc-simplify") << "finish simplify, #cond = " << d_cond.size() << std::endl;
}
void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
d_false = NodeManager::currentNM()->mkConst(false);
}
-void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) {
+bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
//standard pre-process
- preProcessBuildModelStd( m, fullModel );
+ if( !preProcessBuildModelStd( m ) ){
+ return false;
+ }
FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
- if( !fullModel ){
- Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
- d_preinitialized_types.clear();
- //traverse equality engine
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
- while( !eqcs_i.isFinished() ){
- TypeNode tr = (*eqcs_i).getType();
- d_preinitialized_types[tr] = true;
- ++eqcs_i;
- }
+ Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
+ d_preinitialized_types.clear();
+ //traverse equality engine
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+ while( !eqcs_i.isFinished() ){
+ TypeNode tr = (*eqcs_i).getType();
+ d_preinitialized_types[tr] = true;
+ ++eqcs_i;
+ }
- //must ensure model basis terms exists in model for each relevant type
- fm->initialize();
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
- Node op = it->first;
- TypeNode tno = op.getType();
- for( unsigned i=0; i<tno.getNumChildren(); i++) {
- preInitializeType( fm, tno[i] );
- }
+ //must ensure model basis terms exists in model for each relevant type
+ fm->initialize();
+ for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ Node op = it->first;
+ TypeNode tno = op.getType();
+ for( unsigned i=0; i<tno.getNumChildren(); i++) {
+ preInitializeType( fm, tno[i] );
}
- //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
- if( !options::fmfEmptySorts() ){
- for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node q = fm->getAssertedQuantifier( i );
- //make sure all types are set
- for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
- preInitializeType( fm, q[0][j].getType() );
- }
+ }
+ //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
+ if( !options::fmfEmptySorts() ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node q = fm->getAssertedQuantifier( i );
+ //make sure all types are set
+ for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+ preInitializeType( fm, q[0][j].getType() );
}
}
}
+ return true;
}
-void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
+bool FullModelChecker::processBuildModel(TheoryModel* m){
FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
- if( !fullModel ){
- Trace("fmc") << "---Full Model Check reset() " << std::endl;
- d_quant_models.clear();
- d_rep_ids.clear();
- d_star_insts.clear();
- //process representatives
- for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
- it != fm->d_rep_set.d_type_reps.end(); ++it ){
- 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] );
- if( Trace.isOn("fmc-model-debug") ){
- std::vector< Node > eqc;
- ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
- Trace("fmc-model-debug") << " " << (it->second[a]==r);
- Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
- //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
- Trace("fmc-model-debug") << " {";
- for( size_t i=0; i<eqc.size(); i++ ){
- Trace("fmc-model-debug") << eqc[i] << ", ";
- }
- Trace("fmc-model-debug") << "}" << std::endl;
+ Trace("fmc") << "---Full Model Check reset() " << std::endl;
+ d_quant_models.clear();
+ d_rep_ids.clear();
+ d_star_insts.clear();
+ //process representatives
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){
+ 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] );
+ if( Trace.isOn("fmc-model-debug") ){
+ std::vector< Node > eqc;
+ ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
+ Trace("fmc-model-debug") << " " << (it->second[a]==r);
+ Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
+ //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
+ Trace("fmc-model-debug") << " {";
+ for( size_t i=0; i<eqc.size(); i++ ){
+ Trace("fmc-model-debug") << eqc[i] << ", ";
}
- d_rep_ids[it->first][r] = (int)a;
+ Trace("fmc-model-debug") << "}" << std::endl;
}
- Trace("fmc-model-debug") << std::endl;
+ d_rep_ids[it->first][r] = (int)a;
}
+ Trace("fmc-model-debug") << std::endl;
}
+ }
- //now, make models
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
- Node op = it->first;
- //reset the model
- fm->d_models[op]->reset();
-
- Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;
- std::vector< Node > add_conds;
- std::vector< Node > add_values;
- bool needsDefault = true;
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
- Node n = fm->d_uf_terms[op][i];
+ //now, make models
+ for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ Node op = it->first;
+ //reset the model
+ fm->d_models[op]->reset();
+
+ std::vector< Node > add_conds;
+ std::vector< Node > add_values;
+ bool needsDefault = true;
+ std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( op );
+ if( itut!=fm->d_uf_terms.end() ){
+ 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( fm->d_uf_terms[op][i], r ) );
+ //AlwaysAssert( fm->areEqual( itut->second[i], r ) );
}else{
if( Trace.isOn("fmc-model-debug") ){
Node r = fm->getUsedRepresentative(n);
}
}
}
- Trace("fmc-model-debug") << std::endl;
- //possibly get default
- if( needsDefault ){
- Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
- //add default value if necessary
- if( fm->hasTerm( nmb ) ){
- Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
- add_conds.push_back( nmb );
- add_values.push_back( nmb );
- }else{
- Node vmb = getSomeDomainElement(fm, nmb.getType());
- Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
- Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
- add_conds.push_back( nmb );
- add_values.push_back( vmb );
- }
+ }else{
+ Trace("fmc-model-debug") << "No model values for " << op << " ... " << std::endl;
+ }
+ Trace("fmc-model-debug") << std::endl;
+ //possibly get default
+ if( needsDefault ){
+ Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+ //add default value if necessary
+ if( fm->hasTerm( nmb ) ){
+ Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
+ add_conds.push_back( nmb );
+ add_values.push_back( nmb );
+ }else{
+ Node vmb = getSomeDomainElement(fm, nmb.getType());
+ Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
+ Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
+ add_conds.push_back( nmb );
+ add_values.push_back( vmb );
}
+ }
- std::vector< Node > conds;
- std::vector< Node > values;
- std::vector< Node > entry_conds;
- //get the entries for the mdoel
- for( size_t i=0; i<add_conds.size(); i++ ){
- Node c = add_conds[i];
- Node v = add_values[i];
- std::vector< Node > children;
- std::vector< Node > entry_children;
- children.push_back(op);
- entry_children.push_back(op);
- bool hasNonStar = false;
- for( unsigned i=0; i<c.getNumChildren(); i++) {
- Node ri = fm->getUsedRepresentative( c[i] );
- children.push_back(ri);
- bool isStar = false;
- if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
- if (fm->isModelBasisTerm(ri) ) {
- ri = fm->getStar( ri.getType() );
- isStar = true;
- }else{
- hasNonStar = true;
- }
- }
- if( !isStar && !ri.isConst() ){
- Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
- Assert( false );
+ std::vector< Node > conds;
+ std::vector< Node > values;
+ std::vector< Node > entry_conds;
+ //get the entries for the mdoel
+ for( size_t i=0; i<add_conds.size(); i++ ){
+ Node c = add_conds[i];
+ Node v = add_values[i];
+ std::vector< Node > children;
+ std::vector< Node > entry_children;
+ children.push_back(op);
+ entry_children.push_back(op);
+ bool hasNonStar = false;
+ for( unsigned i=0; i<c.getNumChildren(); i++) {
+ Node ri = fm->getUsedRepresentative( c[i] );
+ children.push_back(ri);
+ bool isStar = false;
+ if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
+ if (fm->isModelBasisTerm(ri) ) {
+ ri = fm->getStar( ri.getType() );
+ isStar = true;
+ }else{
+ hasNonStar = true;
}
- entry_children.push_back(ri);
}
- Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
- Node nv = fm->getUsedRepresentative( v );
- if( !nv.isConst() ){
- Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
+ if( !isStar && !ri.isConst() ){
+ Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
Assert( false );
}
- Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
- if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
- Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
- conds.push_back(n);
- values.push_back(nv);
- entry_conds.push_back(en);
- }
- else {
- Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
- }
+ entry_children.push_back(ri);
+ }
+ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+ Node nv = fm->getUsedRepresentative( v );
+ if( !nv.isConst() ){
+ Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
+ Assert( false );
+ }
+ Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
+ if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
+ Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
+ conds.push_back(n);
+ values.push_back(nv);
+ entry_conds.push_back(en);
}
+ else {
+ Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
+ }
+ }
- //sort based on # default arguments
- std::vector< int > indices;
- ModelBasisArgSort mbas;
- for (int i=0; i<(int)conds.size(); i++) {
- d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
- mbas.d_terms.push_back(conds[i]);
- indices.push_back(i);
- }
- std::sort( indices.begin(), indices.end(), mbas );
+ //sort based on # default arguments
+ std::vector< int > indices;
+ ModelBasisArgSort mbas;
+ for (int i=0; i<(int)conds.size(); i++) {
+ d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
+ mbas.d_terms.push_back(conds[i]);
+ indices.push_back(i);
+ }
+ std::sort( indices.begin(), indices.end(), mbas );
- for (int i=0; i<(int)indices.size(); i++) {
- fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
- }
+ for (int i=0; i<(int)indices.size(); i++) {
+ fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
+ }
- if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){
- convertIntervalModel( fm, op );
- }
+ if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){
+ convertIntervalModel( fm, op );
+ }
- Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
- fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
- Trace("fmc-model-simplify") << std::endl;
+ Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
+ fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
+ Trace("fmc-model-simplify") << std::endl;
- Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;
- fm->d_models[op]->simplify( this, fm );
+ Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;
+ fm->d_models[op]->simplify( this, fm );
- fm->d_models[op]->debugPrint("fmc-model", op, this);
- Trace("fmc-model") << std::endl;
+ fm->d_models[op]->debugPrint("fmc-model", op, this);
+ Trace("fmc-model") << std::endl;
- //for debugging
- /*
- 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] );
- inst.push_back( r );
- }
- Node ev = fm->d_models[op]->evaluate( fm, inst );
- Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl;
- AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) );
+ //for debugging
+ /*
+ 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] );
+ inst.push_back( r );
}
- */
- }
- }else{
- //make function values
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
- m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );
+ Node ev = fm->d_models[op]->evaluate( fm, inst );
+ Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl;
+ AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) );
}
- TheoryEngineModelBuilder::processBuildModel( m, fullModel );
- //mark that the model has been set
- fm->markModelSet();
- //debug the model
- debugModel( fm );
+ */
+ }
+ Assert( d_addedLemmas==0 );
+
+ //make function values
+ for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
+ m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );
}
+ return TheoryEngineModelBuilder::processBuildModel( m );
}
void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
//model check the quantifier
doCheck(fmfmc, f, d_quant_models[f], f[1]);
Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
+ Assert( !d_quant_models[f].d_cond.empty() );
d_quant_models[f].debugPrint("fmc", Node::null(), this);
Trace("fmc") << std::endl;
*/
} else {
if( !var_ch.empty() ){
- if( n.getKind()==EQUAL ){
+ if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
if( var_ch.size()==2 ){
Trace("fmc-debug") << "Do variable equality " << n << std::endl;
doVariableEquality( fm, f, d, n );
}
Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {
- if( n.getKind()==EQUAL ){
+ if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
if (!vals[0].isNull() && !vals[1].isNull()) {
return vals[0]==vals[1] ? d_true : d_false;
}else{
Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
/** process build model */
- void preProcessBuildModel(TheoryModel* m, bool fullModel);
- void processBuildModel(TheoryModel* m, bool fullModel);
- /** get current model value */
- Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial );
+ bool preProcessBuildModel(TheoryModel* m);
+ bool processBuildModel(TheoryModel* m);
bool useSimpleModels();
};/* class FullModelChecker */
}else{
Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
if( ak==EQUAL ){
- Node atom = n.getKind() ? n[0] : n;
+ Node atom = n.getKind()==NOT ? n[0] : n;
return !atom[0].getType().isBoolean();
}else{
Assert( ak!=NOT );
}else{
Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
}
+ Assert( rd!=NULL );
rd->compute();
unsigned final_max_i = 0;
std::vector< unsigned > maxs;
QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) :
-TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe( qe ){
+TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_qe( qe ){
}
return options::mbqiMode()!=MBQI_NONE || options::fmfBound();
}
-void QModelBuilder::preProcessBuildModel(TheoryModel* m, bool fullModel) {
- preProcessBuildModelStd( m, fullModel );
+bool QModelBuilder::preProcessBuildModel(TheoryModel* m) {
+ return preProcessBuildModelStd( m );
}
-void QModelBuilder::preProcessBuildModelStd(TheoryModel* m, bool fullModel) {
- if( !fullModel ){
- if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){
- FirstOrderModel * fm = (FirstOrderModel*)m;
- //traverse equality engine
- std::map< TypeNode, bool > eqc_usort;
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
- while( !eqcs_i.isFinished() ){
- TypeNode tr = (*eqcs_i).getType();
- eqc_usort[tr] = true;
- ++eqcs_i;
- }
- //look at quantified formulas
- for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node q = fm->getAssertedQuantifier( i, true );
- if( fm->isQuantifierActive( q ) ){
- //check if any of these quantified formulas can be set inactive
- if( options::fmfEmptySorts() ){
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- TypeNode tn = q[0][i].getType();
- //we are allowed to assume the type is empty
- if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){
- Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
- fm->setQuantifierActive( q, false );
- }
+bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
+ d_addedLemmas = 0;
+ d_triedLemmas = 0;
+ if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){
+ FirstOrderModel * fm = (FirstOrderModel*)m;
+ //traverse equality engine
+ std::map< TypeNode, bool > eqc_usort;
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+ while( !eqcs_i.isFinished() ){
+ TypeNode tr = (*eqcs_i).getType();
+ eqc_usort[tr] = true;
+ ++eqcs_i;
+ }
+ //look at quantified formulas
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node q = fm->getAssertedQuantifier( i, true );
+ if( fm->isQuantifierActive( q ) ){
+ //check if any of these quantified formulas can be set inactive
+ if( options::fmfEmptySorts() ){
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ TypeNode tn = q[0][i].getType();
+ //we are allowed to assume the type is empty
+ if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){
+ Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
+ fm->setQuantifierActive( q, false );
}
- }else if( options::fmfFunWellDefinedRelevant() ){
- if( q[0].getNumChildren()==1 ){
- TypeNode tn = q[0][0].getType();
- if( tn.getAttribute(AbsTypeFunDefAttribute()) ){
- //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl;
- //we are allowed to assume the introduced type is empty
- if( eqc_usort.find( tn )==eqc_usort.end() ){
- Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl;
- fm->setQuantifierActive( q, false );
- }
+ }
+ }else if( options::fmfFunWellDefinedRelevant() ){
+ if( q[0].getNumChildren()==1 ){
+ TypeNode tn = q[0][0].getType();
+ if( tn.getAttribute(AbsTypeFunDefAttribute()) ){
+ //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl;
+ //we are allowed to assume the introduced type is empty
+ if( eqc_usort.find( tn )==eqc_usort.end() ){
+ Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl;
+ fm->setQuantifierActive( q, false );
}
}
}
}
}
}
+ return true;
}
-void QModelBuilder::debugModel( FirstOrderModel* fm ){
+void QModelBuilder::debugModel( TheoryModel* m ){
//debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
if( Trace.isOn("quant-check-model") ){
+ FirstOrderModel* fm = (FirstOrderModel*)m;
Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
int tests = 0;
int bad = 0;
}
+/*
Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {
return n;
}
+*/
-void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
+bool QModelBuilderIG::processBuildModel( TheoryModel* m ) {
FirstOrderModel* f = (FirstOrderModel*)m;
FirstOrderModelIG* fm = f->asFirstOrderModelIG();
- Trace("model-engine-debug") << "Process build model, fullModel = " << fullModel << " " << optUseModel() << std::endl;
- if( fullModel ){
- Assert( d_curr_model==fm );
- //update models
- for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
- it->second.update( fm );
- Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl;
- //construct function values
- fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
+ Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl;
+ d_didInstGen = false;
+ //reset the internal information
+ reset( fm );
+ //only construct first order model if optUseModel() is true
+ if( optUseModel() ){
+ Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
+ //check if any quantifiers are un-initialized
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node q = fm->getAssertedQuantifier( i );
+ if( d_qe->getModel()->isQuantifierActive( q ) ){
+ int lems = initializeQuantifier( q, q );
+ d_statistics.d_init_inst_gen_lemmas += lems;
+ d_addedLemmas += lems;
+ if( d_qe->inConflict() ){
+ break;
+ }
+ }
}
- TheoryEngineModelBuilder::processBuildModel( m, fullModel );
- //mark that the model has been set
- fm->markModelSet();
- //debug the model
- debugModel( fm );
- }else{
- d_curr_model = fm;
- d_didInstGen = false;
- //reset the internal information
- reset( fm );
- //only construct first order model if optUseModel() is true
- if( optUseModel() ){
- Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
- //check if any quantifiers are un-initialized
+ if( d_addedLemmas>0 ){
+ Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
+ return false;
+ }else{
+ Assert( !d_qe->inConflict() );
+ //initialize model
+ fm->initialize();
+ //analyze the functions
+ Trace("model-engine-debug") << "Analyzing model..." << std::endl;
+ analyzeModel( fm );
+ //analyze the quantifiers
+ Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
+ d_uf_prefs.clear();
for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node q = fm->getAssertedQuantifier( i );
- if( d_qe->getModel()->isQuantifierActive( q ) ){
- int lems = initializeQuantifier( q, q );
- d_statistics.d_init_inst_gen_lemmas += lems;
- d_addedLemmas += lems;
- if( d_qe->inConflict() ){
- break;
- }
- }
+ analyzeQuantifier( fm, q );
}
- if( d_addedLemmas>0 ){
- Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
- }else{
- Assert( !d_qe->inConflict() );
- //initialize model
- fm->initialize();
- //analyze the functions
- Trace("model-engine-debug") << "Analyzing model..." << std::endl;
- analyzeModel( fm );
- //analyze the quantifiers
- Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
- d_uf_prefs.clear();
- for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node q = fm->getAssertedQuantifier( i );
- analyzeQuantifier( fm, q );
- }
- //if applicable, find exceptions to model via inst-gen
- if( options::fmfInstGen() ){
- d_didInstGen = true;
- d_instGenMatches = 0;
- d_numQuantSat = 0;
- d_numQuantInstGen = 0;
- d_numQuantNoInstGen = 0;
- d_numQuantNoSelForm = 0;
- //now, see if we know that any exceptions via InstGen exist
- Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
- for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- if( d_qe->getModel()->isQuantifierActive( f ) ){
- int lems = doInstGen( fm, f );
- d_statistics.d_inst_gen_lemmas += lems;
- d_addedLemmas += lems;
- //temporary
- if( lems>0 ){
- d_numQuantInstGen++;
- }else if( hasInstGen( f ) ){
- d_numQuantNoInstGen++;
- }else{
- d_numQuantNoSelForm++;
- }
- if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
- break;
- }
+ //if applicable, find exceptions to model via inst-gen
+ if( options::fmfInstGen() ){
+ d_didInstGen = true;
+ d_instGenMatches = 0;
+ d_numQuantSat = 0;
+ d_numQuantInstGen = 0;
+ d_numQuantNoInstGen = 0;
+ d_numQuantNoSelForm = 0;
+ //now, see if we know that any exceptions via InstGen exist
+ Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ if( d_qe->getModel()->isQuantifierActive( f ) ){
+ int lems = doInstGen( fm, f );
+ d_statistics.d_inst_gen_lemmas += lems;
+ d_addedLemmas += lems;
+ //temporary
+ if( lems>0 ){
+ d_numQuantInstGen++;
+ }else if( hasInstGen( f ) ){
+ d_numQuantNoInstGen++;
}else{
- d_numQuantSat++;
+ d_numQuantNoSelForm++;
}
- }
- Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
- Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl;
- Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl;
- if( Trace.isOn("model-engine") ){
- if( d_addedLemmas>0 ){
- Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
- }else{
- Trace("model-engine") << "No InstGen lemmas..." << std::endl;
+ if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
+ break;
}
+ }else{
+ d_numQuantSat++;
}
}
- //construct the model if necessary
- if( d_addedLemmas==0 ){
- //if no immediate exceptions, build the model
- // this model will be an approximation that will need to be tested via exhaustive instantiation
- Trace("model-engine-debug") << "Building model..." << std::endl;
- //build model for UF
- for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
- Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl;
- constructModelUf( fm, it->first );
+ Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
+ Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl;
+ Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl;
+ if( Trace.isOn("model-engine") ){
+ if( d_addedLemmas>0 ){
+ Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
+ }else{
+ Trace("model-engine") << "No InstGen lemmas..." << std::endl;
}
- Trace("model-engine-debug") << "Done building models." << std::endl;
}
}
+ //construct the model if necessary
+ if( d_addedLemmas==0 ){
+ //if no immediate exceptions, build the model
+ // this model will be an approximation that will need to be tested via exhaustive instantiation
+ Trace("model-engine-debug") << "Building model..." << std::endl;
+ //build model for UF
+ for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+ Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl;
+ constructModelUf( fm, it->first );
+ }
+ Trace("model-engine-debug") << "Done building models." << std::endl;
+ }else{
+ return false;
+ }
}
}
+ //update models
+ for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+ it->second.update( fm );
+ Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl;
+ //construct function values
+ fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
+ }
+ Assert( d_addedLemmas==0 );
+ return TheoryEngineModelBuilder::processBuildModel( m );
}
int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){
Node op = it->first;
TermArgBasisTrie tabt;
- for( size_t i=0; i<fmig->d_uf_terms[op].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;
+ std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
+ if( itut!=fmig->d_uf_terms.end() ){
+ 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;
+ }
}
- }
- //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;
+ //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;
+ }
}
}
}
Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
//set the values in the model
- for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
- Node n = fmig->d_uf_terms[op][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 );
+ std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
+ 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{
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;
- }
}
}
}
class QModelBuilder : public TheoryEngineModelBuilder
{
protected:
- //the model we are working with
- context::CDO< FirstOrderModel* > d_curr_model;
//quantifiers engine
QuantifiersEngine* d_qe;
- void preProcessBuildModel(TheoryModel* m, bool fullModel);
- void preProcessBuildModelStd(TheoryModel* m, bool fullModel);
+ bool preProcessBuildModel(TheoryModel* m); //must call preProcessBuildModelStd
+ bool preProcessBuildModelStd(TheoryModel* m);
+ /** number of lemmas generated while building model */
+ unsigned d_addedLemmas;
+ unsigned d_triedLemmas;
public:
QModelBuilder( context::Context* c, QuantifiersEngine* qe );
virtual ~QModelBuilder() throw() {}
virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
//whether to construct model
virtual bool optUseModel();
- /** number of lemmas generated while building model */
- int d_addedLemmas;
- int d_triedLemmas;
/** exist instantiation ? */
virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
//debug model
- void debugModel( FirstOrderModel* fm );
+ virtual void debugModel( TheoryModel* m );
+ //statistics
+ unsigned getNumAddedLemmas() { return d_addedLemmas; }
+ unsigned getNumTriedLemmas() { return d_triedLemmas; }
};
//whether inst gen was done
bool d_didInstGen;
/** process build model */
- virtual void processBuildModel( TheoryModel* m, bool fullModel );
- /** get current model value */
- Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );
+ virtual bool processBuildModel( TheoryModel* m );
protected:
//reset
virtual void reset( FirstOrderModel* fm ) = 0;
void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
//first check if the builder can do the exhaustive instantiation
quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
- mb->d_triedLemmas = 0;
- mb->d_addedLemmas = 0;
+ unsigned prev_alem = mb->getNumAddedLemmas();
+ unsigned prev_tlem = mb->getNumTriedLemmas();
int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort );
if( retEi!=0 ){
if( retEi<0 ){
}else{
Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
}
- d_triedLemmas += mb->d_triedLemmas;
- d_addedLemmas += mb->d_addedLemmas;
- d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->d_addedLemmas;
+ d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem;
+ d_addedLemmas += mb->getNumAddedLemmas()-prev_alem;
+ d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->getNumAddedLemmas();
}else{
if( Trace.isOn("fmf-exh-inst-debug") ){
Trace("fmf-exh-inst-debug") << " Instantiation Constants: ";
-RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){
+RelevantDomain::RelevantDomain( QuantifiersEngine* qe ) : d_qe( qe ){
d_is_computed = false;
}
it2->second->reset();
}
}
- for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
- Node q = d_model->getAssertedQuantifier( i );
+ FirstOrderModel* fm = d_qe->getModel();
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node q = fm->getAssertedQuantifier( i );
Node icf = d_qe->getTermDatabase()->getInstConstantBody( q );
Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
computeRelevantDomain( q, icf, true, true );
}
}
- if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) && TermDb::hasInstConstAttr( n ) ){
+ if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) || n.getKind()==GEQ ) && TermDb::hasInstConstAttr( n ) ){
//compute the information for what this literal does
computeRelevantDomainLit( q, hasPol, pol, n );
if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
std::map< RDomain *, Node > d_rn_map;
std::map< RDomain *, int > d_ri_map;
QuantifiersEngine* d_qe;
- FirstOrderModel* d_model;
void computeRelevantDomain( Node q, Node n, bool hasPol, bool pol );
void computeRelevantDomainOpCh( RDomain * rf, Node n );
bool d_is_computed;
std::map< bool, std::map< bool, std::map< Node, RDomainLit > > > d_rel_dom_lit;
void computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n );
public:
- RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );
+ RelevantDomain( QuantifiersEngine* qe );
virtual ~RelevantDomain();
/* reset */
bool reset( Theory::Effort e );
}
}
-void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems ) {
+void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& terms, std::vector< Node >& vals, std::vector< Node >& exps ) {
std::map< Node, std::map< Node, bool > >::iterator its = d_subterms.find( a );
if( its!=d_subterms.end() ){
Trace("sygus-eager") << "registerModelValue : " << a << ", has " << its->second.size() << " registered subterms." << std::endl;
Node vn = n.substitute( at, vt );
vn = Rewriter::rewrite( vn );
unsigned start = d_node_mv_args_proc[n][vn];
- Node antec = n.eqNode( vn ).negate();
+ Node antec = n.eqNode( vn );
TypeNode tn = n.getType();
Assert( tn.isDatatype() );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
for( unsigned i=start; i<it->second.size(); i++ ){
Assert( vars.size()==it->second[i].size() );
Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
- Node lem = NodeManager::currentNM()->mkNode(EQUAL, d_evals[n][i], sBTerm );
- lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
- Trace("sygus-eager") << "Lemma : " << lem << std::endl;
- lems.push_back( lem );
+ sBTerm = Rewriter::rewrite( sBTerm );
+ //Node lem = NodeManager::currentNM()->mkNode(EQUAL, d_evals[n][i], sBTerm );
+ //lem = NodeManager::currentNM()->mkNode( OR, antec.negate(), lem );
+ terms.push_back( d_evals[n][i] );
+ vals.push_back( sBTerm );
+ exps.push_back( antec );
+ Trace("sygus-eager") << "Conclude : " << d_evals[n][i] << " == " << sBTerm << std::endl;
+ Trace("sygus-eager") << " from " << antec << std::endl;
+ //Trace("sygus-eager") << "Lemma : " << lem << std::endl;
+ //lems.push_back( lem );
}
d_node_mv_args_proc[n][vn] = it->second.size();
}
}
}
+
+Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp ) {
+ if( en.getKind()==kind::APPLY_UF ){
+ std::map< Node, Node >::iterator itv = vtm.find( en[0] );
+ if( itv!=vtm.end() ){
+ Node ev = itv->second;
+ Assert( en[0].getType()==ev.getType() );
+ Assert( ev.isConst() && ev.getKind()==kind::APPLY_CONSTRUCTOR );
+ std::vector< Node > args;
+ for( unsigned i=1; i<en.getNumChildren(); i++ ){
+ args.push_back( en[i] );
+ }
+ const Datatype& dt = ((DatatypeType)(ev.getType()).toType()).getDatatype();
+ unsigned i = Datatype::indexOf( ev.getOperator().toExpr() );
+ //explanation
+ Node ee = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), en[0] );
+ if( std::find( exp.begin(), exp.end(), ee )==exp.end() ){
+ exp.push_back( ee );
+ }
+ std::map< int, Node > pre;
+ for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+ std::vector< Node > cc;
+ //get the evaluation argument for the selector
+ const Datatype & ad = ((DatatypeType)dt[i][j].getRangeType()).getDatatype();
+ cc.push_back( Node::fromExpr( ad.getSygusEvaluationFunc() ) );
+ Node s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[i][j].getSelector() ), en[0] );
+ cc.push_back( s );
+ //update vtm map
+ vtm[s] = ev[j];
+ cc.insert( cc.end(), args.begin(), args.end() );
+ pre[j] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, cc );
+ }
+ std::map< TypeNode, int > var_count;
+ Node ret = mkGeneric( dt, i, var_count, pre );
+ // if it is a variable, apply the substitution
+ if( ret.getKind()==kind::BOUND_VARIABLE ){
+ //replace by argument
+ Node var_list = Node::fromExpr( dt.getSygusVarList() );
+ //TODO : set argument # on sygus variables
+ for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
+ if( var_list[j]==ret ){
+ ret = args[j];
+ break;
+ }
+ }
+ Assert( ret.isConst() );
+ }else if( ret.getKind()==APPLY ){
+ //must expand definitions to account for defined functions in sygus grammars
+ ret = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( ret.toExpr() ) );
+ }
+ return ret;
+ }else{
+ Assert( false );
+ }
+ }else{
+ Assert( en.isConst() );
+ }
+ return en;
+}
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc;
public:
void registerEvalTerm( Node n );
- void registerModelValue( Node n, Node v, std::vector< Node >& lems );
+ void registerModelValue( Node n, Node v, std::vector< Node >& exps, std::vector< Node >& terms, std::vector< Node >& vals );
+ Node unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp );
};
}/* CVC4::theory::quantifiers namespace */
Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
- //the model object
- if( options::mbqiMode()==quantifiers::MBQI_FMC ||
- options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBound() ||
- options::mbqiMode()==quantifiers::MBQI_TRUST ){
- d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
- }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
- d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
- }else{
- d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
- }
if( options::relevantTriggers() ){
d_quant_rel = new QuantRelevance( false );
}else{
d_i_cbqi = NULL;
d_qsplit = NULL;
d_anti_skolem = NULL;
+ d_model = NULL;
d_model_engine = NULL;
d_bint = NULL;
d_rr_engine = NULL;
if( options::cbqi() ){
d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
d_modules.push_back( d_i_cbqi );
- if( options::cbqiModel() ){
- needsBuilder = true;
- }
+ //if( options::cbqiModel() ){
+ // needsBuilder = true;
+ //}
}
if( options::ceGuidedInst() ){
d_ceg_inst = new quantifiers::CegInstantiation( this, c );
d_modules.push_back( d_ceg_inst );
- needsBuilder = true;
+ //needsBuilder = true;
}
//finite model finding
if( options::finiteModelFind() ){
}
d_model_engine = new quantifiers::ModelEngine( c, this );
d_modules.push_back( d_model_engine );
+ //finite model finder has special ways of building the model
needsBuilder = true;
}
if( options::quantRewriteRules() ){
d_modules.push_back( d_fs );
needsRelDom = true;
}
-
+
if( needsRelDom ){
- d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
+ d_rel_dom = new quantifiers::RelevantDomain( this );
d_util.push_back( d_rel_dom );
}
-
+
+ // if we require specialized ways of building the model
if( needsBuilder ){
Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBound() ){
Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
+ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
}else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
+ d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
d_builder = new quantifiers::AbsMbqiBuilder( c, this );
}else{
Trace("quant-engine-debug") << "...make default model builder." << std::endl;
+ d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
d_builder = new quantifiers::QModelBuilderDefault( c, this );
}
+ }else{
+ d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
}
-
}
QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
d_conflict = false;
d_hasAddedLemma = false;
bool setIncomplete = false;
- bool usedModelBuilder = false;
Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
if( needsCheck ){
d_curr_effort_level = quant_e;
bool success = true;
//build the model if any module requested it
- if( needsModelE==quant_e ){
- Assert( d_builder!=NULL );
+ if( needsModelE==quant_e && !d_model->isBuilt() ){
+ // theory engine's model builder is quantifier engine's builder if it has one
+ Assert( !d_builder || d_builder==d_te->getModelBuilder() );
Trace("quant-engine-debug") << "Build model..." << std::endl;
- usedModelBuilder = true;
- d_builder->d_addedLemmas = 0;
- d_builder->buildModel( d_model, false );
- //we are done if model building was unsuccessful
- if( d_builder->d_addedLemmas>0 ){
+ if( !d_te->getModelBuilder()->buildModel( d_model ) ){
+ //we are done if model building was unsuccessful
+ Trace("quant-engine-debug") << "...failed." << std::endl;
success = false;
}
}
//SAT case
if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
if( options::produceModels() ){
- if( usedModelBuilder ){
- Trace("quant-engine-debug") << "Build completed model..." << std::endl;
- d_builder->buildModel( d_model, true );
- }else if( !d_model->isModelSet() ){
+ if( d_model->isBuilt() ){
+ Trace("quant-engine-debug") << "Already built model using model builder, finish..." << std::endl;
+ }else{
//use default model builder when no module built the model
- Trace("quant-engine-debug") << "Build the model..." << std::endl;
- d_te->getModelBuilder()->buildModel( d_model, true );
+ Trace("quant-engine-debug") << "Build the default model..." << std::endl;
+ d_te->getModelBuilder()->buildModel( d_model );
Trace("quant-engine-debug") << "Done building the model." << std::endl;
}
}
void TheoryEngine::finishInit() {
// initialize the quantifiers engine
d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
-
- //initialize the model
+
+ //initialize the quantifiers engine, master equality engine, model, model builder
if( d_logicInfo.isQuantified() ) {
- d_curr_model = d_quantEngine->getModel();
- } else {
- d_curr_model = new theory::TheoryModel(d_userContext, "DefaultModel", true);
- d_aloc_curr_model = true;
- }
-
- if (d_logicInfo.isQuantified()) {
d_quantEngine->finishInit();
Assert(d_masterEqualityEngine == 0);
d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master", false);
d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
}
}
+
+ d_curr_model_builder = d_quantEngine->getModelBuilder();
+ d_curr_model = d_quantEngine->getModel();
+ } else {
+ d_curr_model = new theory::TheoryModel(d_userContext, "DefaultModel", true);
+ d_aloc_curr_model = true;
+ }
+ //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
+ if( d_curr_model_builder==NULL ){
+ d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
+ d_aloc_curr_model_builder = true;
}
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
d_curr_model(NULL),
d_aloc_curr_model(false),
d_curr_model_builder(NULL),
+ d_aloc_curr_model_builder(false),
d_ppCache(),
d_possiblePropagations(context),
d_hasPropagated(context),
d_theoryTable[theoryId] = NULL;
d_theoryOut[theoryId] = NULL;
}
-
- // build model information if applicable
- d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
-
+
smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
}
}
- delete d_curr_model_builder;
+ if( d_aloc_curr_model_builder ){
+ delete d_curr_model_builder;
+ }
if( d_aloc_curr_model ){
delete d_curr_model;
}
}
// Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
- if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
+ if( Theory::fullEffort(effort) && ! d_inConflict && ! needCheck() ) {
Trace("theory::assertions-model") << endl;
if (Trace.isOn("theory::assertions-model")) {
printAssertions("theory::assertions-model");
}
//checks for theories requiring the model go at last call
- bool builtModel = false;
+ d_curr_model->setNeedsBuild();
for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
if( theoryId!=THEORY_QUANTIFIERS ){
Theory* theory = d_theoryTable[theoryId];
if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
if( theory->needsCheckLastEffort() ){
- if( !builtModel ){
- builtModel = true;
- d_curr_model_builder->buildModel(d_curr_model, false);
+ if( !d_curr_model->isBuilt() ){
+ if( !d_curr_model_builder->buildModel(d_curr_model) ){
+ //model building should fail only if the model builder adds lemmas
+ Assert( needCheck() );
+ break;
+ }
}
theory->check(Theory::EFFORT_LAST_CALL);
}
// quantifiers engine must pass effort last call check
d_quantEngine->check(Theory::EFFORT_LAST_CALL);
// if returning incomplete or SAT, we have ensured that d_curr_model has been built with fullModel=true
- } else if(options::produceModels()) {
+ } else if(options::produceModels() && !d_curr_model->isBuilt()) {
// must build model at this point
- d_curr_model_builder->buildModel(d_curr_model, true);
+ d_curr_model_builder->buildModel(d_curr_model);
}
}
}
Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas");
Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
- if(!d_inConflict && Theory::fullEffort(effort) && d_masterEqualityEngine != NULL && !d_lemmasAdded) {
- AlwaysAssert(d_masterEqualityEngine->consistent());
+ if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
+ //we will answer SAT
+ if( d_masterEqualityEngine != NULL ){
+ AlwaysAssert(d_masterEqualityEngine->consistent());
+ }
+ if( options::produceModels() ){
+ d_curr_model_builder->debugCheckModel(d_curr_model);
+ // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model)
+ postProcessModel(d_curr_model);
+ }
}
} catch(const theory::Interrupted&) {
Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
}
void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
+ Assert( fullModel ); // AJR : FIXME : remove/simplify fullModel argument everywhere
//have shared term engine collectModelInfo
// d_sharedTerms.collectModelInfo( m, fullModel );
// Consult each active theory to get all relevant information
* Model builder object
*/
theory::TheoryEngineModelBuilder* d_curr_model_builder;
+ bool d_aloc_curr_model_builder;
typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
namespace theory {
TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) :
- d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
+ d_substitutions(c, false), d_modelBuilt(false), d_enableFuncModels(enableFuncModels)
{
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
cache.insert(n);
}
-void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ) {
- constantReps[eqc] = const_rep;
+void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep ) {
+ d_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;
- }
+ tm->d_rep_set.d_values_to_terms[const_rep] = eqc;
}
bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) {
return false;
}
-void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
+bool TheoryEngineModelBuilder::buildModel(Model* m)
{
- Trace("model-builder") << "TheoryEngineModelBuilder: buildModel, fullModel = " << fullModel << std::endl;
+ Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
TheoryModel* tm = (TheoryModel*)m;
// buildModel with fullModel = true should only be called once in any context
Assert(!tm->isBuilt());
- tm->d_modelBuilt = fullModel;
+ tm->d_modelBuilt = true;
// Reset model
tm->reset();
// Collect model info from the theories
Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
- d_te->collectModelInfo(tm, fullModel);
+ d_te->collectModelInfo(tm, true);
// model-builder specific initialization
- preProcessBuildModel(tm, fullModel);
+ if( !preProcessBuildModel(tm) ){
+ return false;
+ }
// Loop through all terms and make sure that assignable sub-terms are in the equality engine
// Also, record #eqc per type (for finite model finding)
Trace("model-builder") << "Collect representatives..." << std::endl;
// Process all terms in the equality engine, store representatives for each EC
- std::map< Node, Node > assertedReps, constantReps;
+ d_constantReps.clear();
+ std::map< Node, Node > assertedReps;
TypeSet typeConstSet, typeRepSet, typeNoRepSet;
TypeEnumeratorProperties tep;
if( options::finiteModelFind() ){
Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc);
TypeNode eqct = eqc.getType();
Assert(assertedReps.find(eqc) == assertedReps.end());
- Assert(constantReps.find(eqc) == constantReps.end());
+ Assert(d_constantReps.find(eqc) == d_constantReps.end());
// Loop through terms in this EC
Node rep, const_rep;
// Theories should not specify a rep if there is already a constant in the EC
//AJR: I believe this assertion is too strict, eqc with asserted reps may merge with constant eqc
//Assert(rep.isNull() || rep == const_rep);
- assignConstantRep( tm, constantReps, eqc, const_rep, fullModel );
+ assignConstantRep( tm, eqc, const_rep );
typeConstSet.add(eqct.getBaseType(), const_rep);
}
else if (!rep.isNull()) {
}
else {
evaluable = true;
- Node normalized = normalize(tm, n, constantReps, true);
+ Node normalized = normalize(tm, n, true);
if (normalized.isConst()) {
typeConstSet.add(tb, normalized);
- assignConstantRep( tm, constantReps, *i2, normalized, fullModel );
+ assignConstantRep( tm, *i2, normalized);
Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
changed = true;
evaluated = true;
for (i = repSet->begin(); i != repSet->end(); ) {
Assert(assertedReps.find(*i) != assertedReps.end());
Node rep = assertedReps[*i];
- Node normalized = normalize(tm, rep, constantReps, false);
+ Node normalized = normalize(tm, rep, false);
Trace("model-builder") << " Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
if (normalized.isConst()) {
changed = true;
typeConstSet.add(tb, normalized);
- assignConstantRep( tm, constantReps, *i, normalized, fullModel );
+ assignConstantRep( tm, *i, normalized);
assertedReps.erase(*i);
i2 = i;
++i;
n = *te;
}
Assert(!n.isNull());
- assignConstantRep( tm, constantReps, *i2, n, fullModel );
+ assignConstantRep( tm, *i2, n);
changed = true;
noRepSet.erase(i2);
if (assignOne) {
}
#ifdef CVC4_ASSERTIONS
- if (fullModel) {
- // Assert that all representatives have been converted to constants
- for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
- set<Node>& repSet = TypeSet::getSet(it);
- if (!repSet.empty()) {
- Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl;
- Assert(false);
- }
+ // Assert that all representatives have been converted to constants
+ for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
+ set<Node>& repSet = TypeSet::getSet(it);
+ if (!repSet.empty()) {
+ Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl;
+ Assert(false);
}
}
#endif /* CVC4_ASSERTIONS */
Trace("model-builder") << "Copy representatives to model..." << std::endl;
tm->d_reps.clear();
std::map< Node, Node >::iterator itMap;
- for (itMap = constantReps.begin(); itMap != constantReps.end(); ++itMap) {
+ for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap) {
tm->d_reps[itMap->first] = itMap->second;
tm->d_rep_set.add(itMap->second.getType(), itMap->second);
}
- if (!fullModel) {
- Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
- // Make sure every EC has a rep
- for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) {
- tm->d_reps[itMap->first] = itMap->second;
- tm->d_rep_set.add(itMap->second.getType(), itMap->second);
- }
- for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
- set<Node>& noRepSet = TypeSet::getSet(it);
- set<Node>::iterator i;
- for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
- tm->d_reps[*i] = *i;
- tm->d_rep_set.add((*i).getType(), *i);
- }
+ Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
+ // Make sure every EC has a rep
+ for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) {
+ tm->d_reps[itMap->first] = itMap->second;
+ tm->d_rep_set.add(itMap->second.getType(), itMap->second);
+ }
+ for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
+ set<Node>& noRepSet = TypeSet::getSet(it);
+ set<Node>::iterator i;
+ for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
+ tm->d_reps[*i] = *i;
+ tm->d_rep_set.add((*i).getType(), *i);
}
}
//modelBuilder-specific initialization
- processBuildModel( tm, fullModel );
-
- // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model)
- if( fullModel ){
- Trace("model-builder") << "TheoryEngineModelBuilder: Post-process model..." << std::endl;
- d_te->postProcessModel(tm);
+ if( !processBuildModel( tm ) ){
+ return false;
+ }else{
+ return true;
}
-
+}
+
+void TheoryEngineModelBuilder::debugCheckModel(Model* m){
+ TheoryModel* tm = (TheoryModel*)m;
#ifdef CVC4_ASSERTIONS
- if (fullModel) {
- // Check that every term evaluates to its representative in the model
- for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) {
- // eqc is the equivalence class representative
- Node eqc = (*eqcs_i);
- Node rep;
- itMap = constantReps.find(eqc);
- if (itMap == constantReps.end() && eqc.getType().isBoolean()) {
- rep = tm->getValue(eqc);
- Assert(rep.isConst());
- }
- else {
- Assert(itMap != constantReps.end());
- rep = itMap->second;
- }
- eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
- for ( ; !eqc_i.isFinished(); ++eqc_i) {
- Node n = *eqc_i;
- static int repCheckInstance = 0;
- ++repCheckInstance;
-
- Debug("check-model::rep-checking")
- << "( " << repCheckInstance <<") "
- << "n: " << n << endl
- << "getValue(n): " << tm->getValue(n) << endl
- << "rep: " << rep << endl;
- Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details");
- }
+ Assert(tm->isBuilt());
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine );
+ std::map< Node, Node >::iterator itMap;
+ // Check that every term evaluates to its representative in the model
+ for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) {
+ // eqc is the equivalence class representative
+ Node eqc = (*eqcs_i);
+ Node rep;
+ itMap = d_constantReps.find(eqc);
+ if (itMap == d_constantReps.end() && eqc.getType().isBoolean()) {
+ rep = tm->getValue(eqc);
+ Assert(rep.isConst());
+ }
+ else {
+ Assert(itMap != d_constantReps.end());
+ rep = itMap->second;
+ }
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
+ for ( ; !eqc_i.isFinished(); ++eqc_i) {
+ Node n = *eqc_i;
+ static int repCheckInstance = 0;
+ ++repCheckInstance;
+
+ Debug("check-model::rep-checking")
+ << "( " << repCheckInstance <<") "
+ << "n: " << n << endl
+ << "getValue(n): " << tm->getValue(n) << endl
+ << "rep: " << rep << endl;
+ Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details");
}
}
#endif /* CVC4_ASSERTIONS */
+ debugModel( tm );
}
-
-Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps, bool evalOnly)
+Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
{
- std::map<Node, Node>::iterator itMap = constantReps.find(r);
- if (itMap != constantReps.end()) {
+ std::map<Node, Node>::iterator itMap = d_constantReps.find(r);
+ if (itMap != d_constantReps.end()) {
return (*itMap).second;
}
NodeMap::iterator it = d_normalizedCache.find(r);
bool recurse = true;
if (!ri.isConst()) {
if (m->d_equalityEngine->hasTerm(ri)) {
- itMap = constantReps.find(m->d_equalityEngine->getRepresentative(ri));
- if (itMap != constantReps.end()) {
+ itMap = d_constantReps.find(m->d_equalityEngine->getRepresentative(ri));
+ if (itMap != d_constantReps.end()) {
ri = (*itMap).second;
recurse = false;
}
}
}
if (recurse) {
- ri = normalize(m, ri, constantReps, evalOnly);
+ ri = normalize(m, ri, evalOnly);
}
if (!ri.isConst()) {
childrenConst = false;
return retNode;
}
-void TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m, bool fullModel) {
-
+bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m) {
+ return true;
}
-void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel)
-{
- if (fullModel) {
- Trace("model-builder") << "Assigning function values..." << endl;
- //construct function values
- for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
- Node n = it->first;
- if( m->d_uf_models.find( n )==m->d_uf_models.end() ){
- TypeNode type = n.getType();
- uf::UfModelTree ufmt( n );
- Node default_v, un, simp, v;
- for( size_t i=0; i<it->second.size(); i++ ){
- un = it->second[i];
- vector<TNode> children;
- children.push_back(n);
- for (size_t j = 0; j < un.getNumChildren(); ++j) {
- children.push_back(m->getRepresentative(un[j]));
- }
- simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
- v = m->getRepresentative(un);
- Trace("model-builder") << " Setting (" << simp << ") to (" << v << ")" << endl;
- ufmt.setValue(m, simp, v);
- default_v = v;
- }
- if( default_v.isNull() ){
- //choose default value from model if none exists
- TypeEnumerator te(type.getRangeType());
- default_v = (*te);
- }
- ufmt.setDefaultValue( m, default_v );
- if(options::condenseFunctionValues()) {
- ufmt.simplify();
+bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m){
+ Trace("model-builder") << "Assigning function values..." << endl;
+ //construct function values
+ for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
+ Node n = it->first;
+ if( m->d_uf_models.find( n )==m->d_uf_models.end() ){
+ TypeNode type = n.getType();
+ Trace("model-builder") << " Assign function value for " << n << " " << type << std::endl;
+ uf::UfModelTree ufmt( n );
+ Node default_v, un, simp, v;
+ for( size_t i=0; i<it->second.size(); i++ ){
+ un = it->second[i];
+ vector<TNode> children;
+ children.push_back(n);
+ for (size_t j = 0; j < un.getNumChildren(); ++j) {
+ children.push_back(m->getRepresentative(un[j]));
}
- Node val = ufmt.getFunctionValue( "_ufmt_", options::condenseFunctionValues() );
- Trace("model-builder") << " Assigning (" << n << ") to (" << val << ")" << endl;
- m->d_uf_models[n] = val;
- //ufmt.debugPrint( std::cout, m );
+ simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
+ v = m->getRepresentative(un);
+ Trace("model-builder") << " Setting (" << simp << ") to (" << v << ")" << endl;
+ ufmt.setValue(m, simp, v);
+ default_v = v;
+ }
+ if( default_v.isNull() ){
+ //choose default value from model if none exists
+ TypeEnumerator te(type.getRangeType());
+ default_v = (*te);
+ }
+ ufmt.setDefaultValue( m, default_v );
+ if(options::condenseFunctionValues()) {
+ ufmt.simplify();
}
+ Node val = ufmt.getFunctionValue( "_ufmt_", options::condenseFunctionValues() );
+ Trace("model-builder") << " Assigning (" << n << ") to (" << val << ")" << endl;
+ m->d_uf_models[n] = val;
+ //ufmt.debugPrint( std::cout, m );
}
}
+ return true;
}
} /* namespace CVC4::theory */
protected:
/** substitution map for this model */
SubstitutionMap d_substitutions;
- context::CDO<bool> d_modelBuilt;
+ bool d_modelBuilt;
public:
TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
virtual ~TheoryModel() throw();
Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const;
public:
/** is built */
- bool isBuilt() { return d_modelBuilt.get(); }
+ bool isBuilt() { return d_modelBuilt; }
+ /** set need build */
+ void setNeedsBuild() { d_modelBuilt = false; }
/**
* Get value function. This should be called only after a ModelBuilder has called buildModel(...)
* on this model.
typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
NodeMap d_normalizedCache;
typedef std::hash_set<Node, NodeHashFunction> NodeSet;
+ std::map< Node, Node > d_constantReps;
/** process build model */
- virtual void preProcessBuildModel(TheoryModel* m, bool fullModel);
- virtual void processBuildModel(TheoryModel* m, bool fullModel);
+ virtual bool preProcessBuildModel(TheoryModel* m);
+ virtual bool processBuildModel(TheoryModel* m);
+ virtual void debugModel( TheoryModel* m ) {}
/** normalize representative */
- Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
+ Node normalize(TheoryModel* m, TNode r, 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 );
+ void assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep );
/** is v an excluded codatatype value */
bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );
/** Build model function.
* Should be called only on TheoryModels m
*/
- void buildModel(Model* m, bool fullModel);
+ bool buildModel(Model* m);
+ void debugCheckModel(Model* m);
};/* class TheoryEngineModelBuilder */
}/* CVC4::theory namespace */
projects / cvc5.git / commitdiff