From 67ea40d24cbbcd3f490248754a6abc1989bacc7b Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 24 Mar 2017 09:37:13 -0500 Subject: [PATCH] Refactor model building for quantifiers to be a single pass, simplification. Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes. --- src/options/quantifiers_options | 6 +- src/smt/model.h | 2 +- src/smt/smt_engine.cpp | 6 + src/theory/datatypes/theory_datatypes.cpp | 40 +- src/theory/quantifiers/ambqi_builder.cpp | 183 +++++---- src/theory/quantifiers/ambqi_builder.h | 2 +- src/theory/quantifiers/bounded_integers.cpp | 8 +- .../quantifiers/ce_guided_instantiation.cpp | 377 ++++++++++++++---- .../quantifiers/ce_guided_instantiation.h | 20 + src/theory/quantifiers/first_order_model.cpp | 37 +- src/theory/quantifiers/first_order_model.h | 16 +- src/theory/quantifiers/full_model_check.cpp | 347 ++++++++-------- src/theory/quantifiers/full_model_check.h | 6 +- src/theory/quantifiers/inst_propagator.cpp | 2 +- .../quantifiers/inst_strategy_e_matching.cpp | 1 + src/theory/quantifiers/model_builder.cpp | 347 ++++++++-------- src/theory/quantifiers/model_builder.h | 21 +- src/theory/quantifiers/model_engine.cpp | 10 +- src/theory/quantifiers/relevant_domain.cpp | 9 +- src/theory/quantifiers/relevant_domain.h | 3 +- src/theory/quantifiers/term_database.cpp | 78 +++- src/theory/quantifiers/term_database.h | 3 +- src/theory/quantifiers_engine.cpp | 58 ++- src/theory/theory_engine.cpp | 62 +-- src/theory/theory_engine.h | 1 + src/theory/theory_model.cpp | 242 ++++++----- src/theory/theory_model.h | 19 +- 27 files changed, 1104 insertions(+), 802 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 585ef3dc2..e5f2922a7 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -253,8 +253,6 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default 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 @@ -271,9 +269,13 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true 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 diff --git a/src/smt/model.h b/src/smt/model.h index fd31655f4..523751d9c 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -75,7 +75,7 @@ class ModelBuilder { public: ModelBuilder() { } virtual ~ModelBuilder() { } - virtual void buildModel(Model* m, bool fullModel) = 0; + virtual bool buildModel(Model* m) = 0; };/* class ModelBuilder */ }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b9ef8f7c4..8e641aca1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1749,6 +1749,12 @@ void SmtEngine::setDefaults() { 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 ); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 11903f863..4a47618f1 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1420,7 +1420,6 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ //combine the equality engine m->assertEqualityEngine( &d_equalityEngine, &termSet ); - //get all constructors eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); @@ -1430,25 +1429,25 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ 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; } @@ -2165,7 +2164,7 @@ void TheoryDatatypes::getRelevantTerms( std::set& termSet ) { // 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); @@ -2176,6 +2175,11 @@ void TheoryDatatypes::getRelevantTerms( std::set& termSet ) { 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; diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 2ccc17e55..de55ecdba 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -586,7 +586,7 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, // 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; @@ -598,7 +598,7 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, 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 ); @@ -721,115 +721,112 @@ QModelBuilder( c, qe ){ //------------------------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::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; isecond.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; isecond.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::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; id_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::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; isecond.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; id_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; id_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; id_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; id_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::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 ); } diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index 0adaef638..68cb27038 100644 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -91,7 +91,7 @@ public: 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 ); }; diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 3d5066c08..41face8f7 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -615,10 +615,10 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node 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; @@ -656,7 +656,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { 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(); @@ -679,7 +679,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { 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() ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 999c554b5..713b9ed6f 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -81,7 +81,7 @@ void CegConjecture::assign( Node q ) { } } } - if( options::cegqiUnifCondSol() ){ + if( options::sygusUnifCondSol() ){ // for each variable, determine whether we can do conditional counterexamples for( unsigned i=0; i& 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() ){ @@ -323,7 +323,7 @@ void CegConjecture::getConditionalCandidateList( std::vector< Node >& clist, Nod } void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) { - if( options::cegqiUnifCondSol() && !forceOrig ){ + if( options::sygusUnifCondSol() && !forceOrig ){ for( unsigned i=0; i& clist, bool forceOrig } 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; @@ -366,7 +366,7 @@ Node CegConjecture::constructConditionalCandidate( std::map< Node, Node >& cmv, 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& lems, std::vector< //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; } @@ -446,7 +446,7 @@ void CegConjecture::doCegConjectureCheck(std::vector< Node >& lems, std::vector< } 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() ){ @@ -541,9 +541,9 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ 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& lems ){ //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 ); @@ -575,7 +575,7 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ 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 ); @@ -587,11 +587,23 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ 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; imkNode( 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))); @@ -600,6 +612,7 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ 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; @@ -635,11 +648,11 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ } } //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 } @@ -662,9 +675,10 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ } } 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 ){ @@ -676,8 +690,8 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ } 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 ) ); @@ -688,53 +702,29 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ } 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 subs; - for( unsigned ii=0; iimkSkolem( "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(); @@ -764,31 +754,69 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ } } //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; jmkNode( 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 subs; + for( unsigned ii=0; iimkSkolem( "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(); @@ -932,7 +960,7 @@ void CegInstantiation::registerQuantifier( Node q ) { //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() ) ); @@ -1049,24 +1077,50 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { 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; jaddLemma( 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 " << 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; jmkNode( 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; } } @@ -1160,6 +1214,171 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } } +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 visited; + std::map< Node, std::vector< Node > > exp; + for( unsigned i=0; igetNumRefinementLemmas(); 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; jgetNumConditionalEvaluations( 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& 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; igetTermDatabase()->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 >::iterator itx = exp.find( nn ); + if( itx!=exp.end() ){ + for( unsigned j=0; jsecond.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() ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index f49298411..2200baf55 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -51,6 +51,10 @@ private: /** 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 ); @@ -173,6 +177,18 @@ public: 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]; } }; @@ -199,6 +215,10 @@ private: //for enforcing fairness 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: diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index b1cc9ed19..16fc4d4b8 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -45,7 +45,7 @@ struct sortQuantifierRelevance { 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; } @@ -70,34 +70,6 @@ Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) { } } -//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; imkNode( 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 @@ -613,6 +585,7 @@ void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){ } } +/* Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { std::vector< Node > children; children.push_back(n.getOperator()); @@ -627,7 +600,7 @@ Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & ar return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex ); } } - +*/ @@ -659,6 +632,7 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { } } +/* 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 & a Assert( n.getKind()==APPLY_UF ); return d_models[n.getOperator()]->evaluate(this, args); } +*/ void FirstOrderModelFmc::processInitialize( bool ispre ) { if( ispre ){ @@ -900,6 +875,7 @@ Node FirstOrderModelAbs::getFunctionValue(Node op, const char* argPrefix ) { 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] ){ @@ -912,6 +888,7 @@ Node FirstOrderModelAbs::getCurrentUfModelValue( Node n, std::vector< Node > & a return Node::null(); } } +*/ void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) { if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 7ded1b05d..05771d1a2 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -55,12 +55,10 @@ protected: 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 ); @@ -82,12 +80,6 @@ public: // 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; @@ -133,8 +125,6 @@ private: //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); @@ -179,7 +169,6 @@ private: 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); @@ -214,7 +203,6 @@ public: 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 ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 7e528fef3..ac23dae29 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -257,7 +257,9 @@ void Def::basic_simplify( FirstOrderModelFmc * m ) { } 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() ){ @@ -300,6 +302,7 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) { 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) { @@ -325,94 +328,96 @@ QModelBuilder( c, qe ){ 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::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node op = it->first; - TypeNode tno = op.getType(); - for( unsigned i=0; iinitialize(); + for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node op = it->first; + TypeNode tno = op.getType(); + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ - Node q = fm->getAssertedQuantifier( i ); - //make sure all types are set - for( unsigned j=0; jgetNumAssertedQuantifiers(); i++ ){ + Node q = fm->getAssertedQuantifier( i ); + //make sure all types are set + for( unsigned j=0; jasFirstOrderModelFmc(); - 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; asecond.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 >::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; asecond.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; ifirst][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::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; id_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + //now, make models + for( std::map::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; isecond.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); @@ -420,127 +425,126 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } } } - 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 children; - std::vector< Node > entry_children; - children.push_back(op); - entry_children.push_back(op); - bool hasNonStar = false; - for( unsigned i=0; igetUsedRepresentative( 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 children; + std::vector< Node > entry_children; + children.push_back(op); + entry_children.push_back(op); + bool hasNonStar = false; + for( unsigned i=0; igetUsedRepresentative( 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; id_uf_terms[op].size(); i++ ){ - std::vector< Node > inst; - for( unsigned j=0; jd_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; id_uf_terms[op].size(); i++ ){ + std::vector< Node > inst; + for( unsigned j=0; jd_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::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::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 ){ @@ -617,6 +621,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i //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; @@ -890,7 +895,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n */ } 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 ); @@ -1273,7 +1278,7 @@ Node FullModelChecker::mkArrayCond( Node a ) { } 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{ diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 7d21b4185..3e7c9918e 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -144,10 +144,8 @@ public: 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 */ diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 41099552d..28b92cc5e 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -367,7 +367,7 @@ bool EqualityQueryInstProp::isPropagateLiteral( Node n ) { }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 ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index f2ed81d8c..a197e057e 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -670,6 +670,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){ }else{ Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl; } + Assert( rd!=NULL ); rd->compute(); unsigned final_max_i = 0; std::vector< unsigned > maxs; diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 090f2735a..7f342c633 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -35,7 +35,7 @@ using namespace CVC4::theory::quantifiers; QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) : -TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe( qe ){ +TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_qe( qe ){ } @@ -43,46 +43,46 @@ bool QModelBuilder::optUseModel() { 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; igetNumAssertedQuantifiers(); 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; isetQuantifierActive( 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; igetNumAssertedQuantifiers(); 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; isetQuantifierActive( 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 ); } } } @@ -90,11 +90,13 @@ void QModelBuilder::preProcessBuildModelStd(TheoryModel* m, bool fullModel) { } } } + 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; @@ -164,122 +166,119 @@ QModelBuilder( c, qe ), d_basisNoMatch( c ) { } +/* 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; igetNumAssertedQuantifiers(); 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; igetNumAssertedQuantifiers(); 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; igetNumAssertedQuantifiers(); 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; igetNumAssertedQuantifiers(); 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; igetNumAssertedQuantifiers(); 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 ){ @@ -330,24 +329,27 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ 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; id_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; isecond.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; + } } } } @@ -733,31 +735,34 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ 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; id_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; isecond.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; - } } } } diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index e1f586585..eedd850d6 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -29,12 +29,13 @@ namespace quantifiers { 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() {} @@ -45,13 +46,13 @@ public: 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; } }; @@ -87,9 +88,7 @@ protected: //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; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 9496f630d..f529a9a27 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -237,8 +237,8 @@ int ModelEngine::checkModel(){ 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 ){ @@ -247,9 +247,9 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ }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: "; diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 8166925c6..f7bac23e2 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -69,7 +69,7 @@ void RelevantDomain::RDomain::removeRedundantTerms( QuantifiersEngine * qe ) { -RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){ +RelevantDomain::RelevantDomain( QuantifiersEngine* qe ) : d_qe( qe ){ d_is_computed = false; } @@ -105,8 +105,9 @@ void RelevantDomain::compute(){ it2->second->reset(); } } - for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ - Node q = d_model->getAssertedQuantifier( i ); + FirstOrderModel* fm = d_qe->getModel(); + for( unsigned i=0; igetNumAssertedQuantifiers(); 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 ); @@ -171,7 +172,7 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po } } - 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 ){ diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 1d6a2af19..be6ebcd9d 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -43,7 +43,6 @@ private: 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; @@ -63,7 +62,7 @@ private: 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 ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d394c8fef..fb123f5b0 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -3274,7 +3274,7 @@ void TermDbSygus::registerEvalTerm( Node n ) { } } -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; @@ -3288,7 +3288,7 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems 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(); @@ -3306,10 +3306,16 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems for( unsigned i=start; isecond.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(); } @@ -3317,6 +3323,66 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems } } + +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; imkNode( 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 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; jexpandDefinitions( ret.toExpr() ) ); + } + return ret; + }else{ + Assert( false ); + } + }else{ + Assert( en.isConst() ); + } + return en; +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 9f43c1d35..fa27f0160 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -672,7 +672,8 @@ private: 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 */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ba50f9ead..bdf2de7f7 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -97,16 +97,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* 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{ @@ -127,6 +117,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* 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; @@ -224,14 +215,14 @@ void QuantifiersEngine::finishInit(){ 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() ){ @@ -241,6 +232,7 @@ void QuantifiersEngine::finishInit(){ } 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() ){ @@ -276,27 +268,32 @@ void QuantifiersEngine::finishInit(){ 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 ) { @@ -405,7 +402,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ 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 ){ @@ -505,14 +501,13 @@ void QuantifiersEngine::check( Theory::Effort e ){ 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; } } @@ -625,13 +620,12 @@ void QuantifiersEngine::check( Theory::Effort e ){ //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; } } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 58f3e4f74..8014a8f22 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -212,16 +212,9 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf) 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); @@ -232,6 +225,17 @@ void TheoryEngine::finishInit() { 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) { @@ -283,6 +287,7 @@ TheoryEngine::TheoryEngine(context::Context* context, 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), @@ -317,10 +322,7 @@ TheoryEngine::TheoryEngine(context::Context* 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(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -344,7 +346,9 @@ TheoryEngine::~TheoryEngine() { } } - 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; } @@ -583,21 +587,24 @@ void TheoryEngine::check(Theory::Effort effort) { } // 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); } @@ -609,9 +616,9 @@ void TheoryEngine::check(Theory::Effort effort) { // 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); } } } @@ -619,8 +626,16 @@ void TheoryEngine::check(Theory::Effort effort) { 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; @@ -828,6 +843,7 @@ bool TheoryEngine::properExplanation(TNode node, TNode expl) const { } 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 diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d8ddf7ffc..f623748cf 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -187,6 +187,7 @@ class TheoryEngine { * Model builder object */ theory::TheoryEngineModelBuilder* d_curr_model_builder; + bool d_aloc_curr_model_builder; typedef std::hash_map NodeMap; typedef std::hash_map TNodeMap; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 8579ad55f..de48c956a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -30,7 +30,7 @@ namespace CVC4 { 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 ); @@ -495,12 +495,10 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac cache.insert(n); } -void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map& 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* repSet, std::map< Node, Node >& assertedReps, Node eqc ) { @@ -583,24 +581,26 @@ bool TheoryEngineModelBuilder::isExcludedUSortValue( std::map< TypeNode, unsigne 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) @@ -627,7 +627,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) 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() ){ @@ -648,7 +649,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) 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; @@ -680,7 +681,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // 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()) { @@ -741,10 +742,10 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) } 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; @@ -772,12 +773,12 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) 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; @@ -901,7 +902,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) n = *te; } Assert(!n.isNull()); - assignConstantRep( tm, constantReps, *i2, n, fullModel ); + assignConstantRep( tm, *i2, n); changed = true; noRepSet.erase(i2); if (assignOne) { @@ -924,14 +925,12 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) } #ifdef CVC4_ASSERTIONS - if (fullModel) { - // Assert that all representatives have been converted to constants - for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) { - set& 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& 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 */ @@ -939,76 +938,76 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) 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& noRepSet = TypeSet::getSet(it); - set::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& noRepSet = TypeSet::getSet(it); + set::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::iterator itMap = constantReps.find(r); - if (itMap != constantReps.end()) { + std::map::iterator itMap = d_constantReps.find(r); + if (itMap != d_constantReps.end()) { return (*itMap).second; } NodeMap::iterator it = d_normalizedCache.find(r); @@ -1027,8 +1026,8 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node 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; } @@ -1037,7 +1036,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node } } if (recurse) { - ri = normalize(m, ri, constantReps, evalOnly); + ri = normalize(m, ri, evalOnly); } if (!ri.isConst()) { childrenConst = false; @@ -1055,50 +1054,49 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node 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; isecond.size(); i++ ){ - un = it->second[i]; - vector 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; isecond.size(); i++ ){ + un = it->second[i]; + vector 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 */ diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index c30d1eabc..82341c377 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -36,7 +36,7 @@ class TheoryModel : public Model protected: /** substitution map for this model */ SubstitutionMap d_substitutions; - context::CDO d_modelBuilt; + bool d_modelBuilt; public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel() throw(); @@ -74,7 +74,9 @@ protected: 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. @@ -266,15 +268,17 @@ protected: typedef std::hash_map NodeMap; NodeMap d_normalizedCache; typedef std::hash_set 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& 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& 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* repSet, std::map< Node, Node >& assertedReps, Node eqc ); bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ); @@ -287,7 +291,8 @@ public: /** 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 */ -- 2.30.2