diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-24 09:37:13 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-24 09:37:32 -0500 |
commit | 67ea40d24cbbcd3f490248754a6abc1989bacc7b (patch) | |
tree | f74d7a52a5046e346035b1c5b5abec1f17004033 /src | |
parent | 2c1e5b35ba688c0df297b0510058454c54bab54d (diff) |
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.
Diffstat (limited to 'src')
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<Node>& 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<Node>& 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<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - if( it->first.getType().getNumChildren()>1 ){ - Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl; - m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" ); - } - } - TheoryEngineModelBuilder::processBuildModel( m, fullModel ); - //mark that the model has been set - fm->markModelSet(); - //debug the model - debugModel( fm ); - }else{ - fm->initialize(); - //process representatives - fm->d_rep_id.clear(); - fm->d_domain.clear(); - - //initialize boolean sort - TypeNode b = d_true.getType(); - fm->d_rep_set.d_type_reps[b].clear(); - fm->d_rep_set.d_type_reps[b].push_back( d_false ); - fm->d_rep_set.d_type_reps[b].push_back( d_true ); - fm->d_rep_id[d_false] = 0; - fm->d_rep_id[d_true] = 1; - - //initialize unintpreted sorts - Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl; - for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); - it != fm->d_rep_set.d_type_reps.end(); ++it ){ - if( it->first.isSort() ){ - Assert( !it->second.empty() ); - //set the domain - fm->d_domain[it->first] = 0; - Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl; - for( unsigned i=0; i<it->second.size(); i++ ){ - if( i<32 ){ - fm->d_domain[it->first] |= ( 1 << i ); - } - Trace("ambqi-model") << i << " : " << it->second[i] << std::endl; - fm->d_rep_id[it->second[i]] = i; - } - if( it->second.size()>=32 ){ - fm->d_domain.erase( it->first ); + fm->initialize(); + //process representatives + fm->d_rep_id.clear(); + fm->d_domain.clear(); + + //initialize boolean sort + TypeNode b = d_true.getType(); + fm->d_rep_set.d_type_reps[b].clear(); + fm->d_rep_set.d_type_reps[b].push_back( d_false ); + fm->d_rep_set.d_type_reps[b].push_back( d_true ); + fm->d_rep_id[d_false] = 0; + fm->d_rep_id[d_true] = 1; + + //initialize unintpreted sorts + Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl; + for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); + it != fm->d_rep_set.d_type_reps.end(); ++it ){ + if( it->first.isSort() ){ + Assert( !it->second.empty() ); + //set the domain + fm->d_domain[it->first] = 0; + Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl; + for( unsigned i=0; i<it->second.size(); i++ ){ + if( i<32 ){ + fm->d_domain[it->first] |= ( 1 << i ); } + Trace("ambqi-model") << i << " : " << it->second[i] << std::endl; + fm->d_rep_id[it->second[i]] = i; + } + if( it->second.size()>=32 ){ + fm->d_domain.erase( it->first ); } } + } - Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl; - //construct the models for functions - for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node f = it->first; - Trace("ambqi-model-debug") << "Building Model for " << f << std::endl; - //reset the model - it->second->clear(); - //get all (non-redundant) f-applications - std::vector< TNode > fapps; - Trace("ambqi-model-debug") << "Initial terms: " << std::endl; - for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){ - Node n = fm->d_uf_terms[f][i]; + Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl; + //construct the models for functions + for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node f = it->first; + Trace("ambqi-model-debug") << "Building Model for " << f << std::endl; + //reset the model + it->second->clear(); + //get all (non-redundant) f-applications + std::vector< TNode > fapps; + Trace("ambqi-model-debug") << "Initial terms: " << std::endl; + std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( f ); + if( itut!=fm->d_uf_terms.end() ){ + for( size_t i=0; i<itut->second.size(); i++ ){ + Node n = itut->second[i]; if( d_qe->getTermDatabase()->isTermActive( n ) ){ Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl; fapps.push_back( n ); } } - if( fapps.empty() ){ - //choose arbitrary value - Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f); - Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl; - fapps.push_back( mbt ); - } - bool fValid = true; - for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){ - if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){ - Trace("ambqi-model") << "Interpretation of " << f << " is not valid."; - Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl; - fValid = false; - break; - } + } + if( fapps.empty() ){ + //choose arbitrary value + Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f); + Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl; + fapps.push_back( mbt ); + } + bool fValid = true; + for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){ + if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){ + Trace("ambqi-model") << "Interpretation of " << f << " is not valid."; + Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl; + fValid = false; + break; } - fm->d_models_valid[f] = fValid; - if( fValid ){ - //construct the ambqi model - it->second->construct_func( fm, fapps ); - Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl; - it->second->debugPrint("ambqi-model-debug", fm, fapps[0] ); - Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl; - it->second->simplify( fm, TNode::null(), fapps[0] ); - Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl; - it->second->debugPrint("ambqi-model", fm, fapps[0] ); + } + fm->d_models_valid[f] = fValid; + if( fValid ){ + //construct the ambqi model + it->second->construct_func( fm, fapps ); + Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl; + it->second->debugPrint("ambqi-model-debug", fm, fapps[0] ); + Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl; + it->second->simplify( fm, TNode::null(), fapps[0] ); + Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl; + it->second->debugPrint("ambqi-model", fm, fapps[0] ); /* - if( Debug.isOn("ambqi-model-debug") ){ - for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){ - Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] ); - Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl; - Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) ); - } + if( Debug.isOn("ambqi-model-debug") ){ + for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){ + Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] ); + Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl; + Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) ); } -*/ } +*/ + } + } + Trace("ambqi-model") << "Construct model representation..." << std::endl; + //make function values + for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + if( it->first.getType().getNumChildren()>1 ){ + Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl; + m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" ); } } + Assert( d_addedLemmas==0 ); + return TheoryEngineModelBuilder::processBuildModel( m ); } 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<d_candidates.size(); i++ ){ registerCandidateConditional( d_candidates[i] ); @@ -295,7 +295,7 @@ bool CegConjecture::needsRefinement() { } void CegConjecture::getConditionalCandidateList( std::vector< Node >& clist, Node curr, bool reqAdd ){ - Assert( options::cegqiUnifCondSol() ); + Assert( options::sygusUnifCondSol() ); std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr ); if( it!=d_cinfo.end() ){ if( !it->second.d_csol_cond.isNull() ){ @@ -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<d_candidates.size(); i++ ){ getConditionalCandidateList( clist, d_candidates[i], true ); } @@ -333,7 +333,7 @@ void CegConjecture::getCandidateList( std::vector< Node >& 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<clist.size(); i++ ){ cmv[ clist[i] ] = model_values[i]; @@ -403,7 +403,7 @@ void CegConjecture::doCegConjectureCheck(std::vector< Node >& 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<d_candidates.size(); i++ ){ Node v = d_candidates[i]; Node ac = getActiveConditional( v ); @@ -557,11 +557,11 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& 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; i<new_active_measure_sum.size(); i++ ){ + Node mclem = NodeManager::currentNM()->mkNode( kind::LEQ, new_active_measure_sum[i], d_active_measure_term ); + Trace("cegqi-lemma") << "Cegqi::Lemma : Measure component lemma : " << mclem << std::endl; + d_qe->getOutputChannel().lemma( mclem ); + } + */ + /* Node new_active_measure = NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ); new_active_measure_sum.push_back( new_active_measure ); Node namlem = NodeManager::currentNM()->mkNode( kind::GEQ, new_active_measure, NodeManager::currentNM()->mkConst(Rational(0))); @@ -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<d_refinement_lemmas.size(); i++ ){ - Node prev_lem = d_refinement_lemmas[i]; - prev_lem = prev_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); - //do auxiliary variable substitution - std::vector< Node > subs; - for( unsigned ii=0; ii<d_refinement_lemmas_aux_vars[i].size(); ii++ ){ - subs.push_back( NodeManager::currentNM()->mkSkolem( "y", d_refinement_lemmas_aux_vars[i][ii].getType(), - "purification variable for non-ground sygus conditional solution" ) ); - } - prev_lem = prev_lem.substitute( d_refinement_lemmas_aux_vars[i].begin(), d_refinement_lemmas_aux_vars[i].end(), subs.begin(), subs.end() ); - prev_lem = Rewriter::rewrite( prev_lem ); - prev_lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), prev_lem ); - Trace("cegqi-unif") << "...previous conditional refinement lemma with new counterexample : " << prev_lem << std::endl; - lems.push_back( prev_lem ); - } - if( !isGround() && !csol_cond.empty() ){ - Trace("cegqi-unif") << "Lemma " << lem << " is a non-ground conditional refinement lemma, store it for future instantiation." << std::endl; - d_refinement_lemmas.push_back( lem ); - d_refinement_lemmas_aux_vars.push_back( paux_vars ); - } - - if( options::cegqiUnifCondSol() ){ - Trace("cegqi-unif") << "We have lemma : " << lem << std::endl; - Trace("cegqi-unif") << "Now add progress assertions..." << std::endl; + if( options::sygusUnifCondSol() ){ + //substitute the actual return values + Assert( d_candidates.size()==csol_vals.size() ); + base_lem = base_lem.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() ); + Trace("sygus-unif") << "We have base lemma : " << base_lem << std::endl; + //progress lemmas + Trace("sygus-unif") << "Now add progress assertions..." << std::endl; std::vector< Node > prgr_conj; std::map< Node, bool > cprocessed; for( std::map< Node, Node >::iterator itc = csol_cond.begin(); itc !=csol_cond.end(); ++itc ){ Node x = itc->first; Node c = itc->second; if( !c.isNull() ){ - Trace("cegqi-unif") << " process conditional " << c << " for " << x << ", which was applied " << psubs_apply[c].size() << " times." << std::endl; + Trace("sygus-unif") << " process conditional " << c << " for " << x << ", which was applied " << psubs_apply[c].size() << " times." << std::endl; //make the progress point Assert( x.getType().isDatatype() ); const Datatype& dx = ((DatatypeType)x.getType().toType()).getDatatype(); @@ -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; j<csol_ccond[x].size(); j++ ){ // Node cc = csol_ccond[x][j]; // prgr_conj.push_back( mkConditional( cc, prgr_pt, csol_cpol[x][cc] ) ); //} //FIXME + d_refinement_lemmas_cprogress.push_back( cplem ); + d_refinement_lemmas_cprogress_pts.push_back( prgr_pt ); + prgr_conj.push_back( cplem ); } } if( !prgr_conj.empty() ){ Node prgr_lem = prgr_conj.size()==1 ? prgr_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, prgr_conj ); prgr_lem = prgr_lem.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() ); - Trace("cegqi-unif") << "Progress lemma is " << prgr_lem << std::endl; - lem = NodeManager::currentNM()->mkNode( kind::AND, lem, prgr_lem ); + prgr_lem = prgr_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + prgr_lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), prgr_lem ); + Trace("sygus-unif") << "Progress lemma is " << prgr_lem << std::endl; + lems.push_back( prgr_lem ); + } + + //previous non-ground conditional refinement lemmas must satisfy the current point + if( !isGround() ){ + for( unsigned i=0; i<d_refinement_lemmas.size(); i++ ){ + Node prev_lem = d_refinement_lemmas[i]; + prev_lem = prev_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + //do auxiliary variable substitution + std::vector< Node > subs; + for( unsigned ii=0; ii<d_refinement_lemmas_aux_vars[i].size(); ii++ ){ + subs.push_back( NodeManager::currentNM()->mkSkolem( "y", d_refinement_lemmas_aux_vars[i][ii].getType(), + "purification variable for non-ground sygus conditional solution" ) ); + } + prev_lem = prev_lem.substitute( d_refinement_lemmas_aux_vars[i].begin(), d_refinement_lemmas_aux_vars[i].end(), subs.begin(), subs.end() ); + prev_lem = Rewriter::rewrite( prev_lem ); + Trace("sygus-unif") << "...previous conditional refinement lemma with new counterexample : " << prev_lem << std::endl; + lems.push_back( prev_lem ); + } } - //make in terms of new values - Assert( csol_vals.size()==d_candidates.size() ); - Trace("cegqi-unif") << "Now rewrite in terms of new evaluation branches...got " << lem << std::endl; } - //apply the substitution - Assert( sk_vars.size()==sk_subs.size() ); - lem = lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + + //make the base lemma + base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + d_refinement_lemmas_base.push_back( base_lem ); + + Node lem = base_lem; + + if( options::sygusUnifCondSol() ){ + d_refinement_lemmas_ceval.push_back( psubs_condc ); + //add the conditional evaluation + if( !psubs_condc.empty() ){ + std::vector< Node > children; + children.push_back( base_lem ); + children.insert( children.end(), psubs_condc.begin(), psubs_condc.end() ); + lem = NodeManager::currentNM()->mkNode( AND, children ); + } + } + lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem ); lem = Rewriter::rewrite( lem ); lems.push_back( lem ); + + d_refinement_lemmas.push_back( lem ); + d_refinement_lemmas_aux_vars.push_back( paux_vars ); } } d_ce_sk.clear(); @@ -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; j<cre_lems.size(); j++ ){ + Node lem = cre_lems[j]; + Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem << std::endl; + if( d_quantEngine->addLemma( lem ) ){ + addedEvalLemmas = true; + } + } + if( addedEvalLemmas ){ + return; + } + } + } Trace("cegqi-debug") << "Do direct evaluation..." << std::endl; - std::vector< Node > eager_eval_lem; + std::vector< Node > eager_terms; + std::vector< Node > eager_vals; + std::vector< Node > eager_exps; for( unsigned j=0; j<clist.size(); j++ ){ - Trace("cegqi-debug") << " register " << clist[j] << " -> " << model_values[j] << std::endl; - d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_eval_lem ); + Trace("cegqi-debug") << " register " << clist[j] << " -> " << model_values[j] << std::endl; + d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_terms, eager_vals, eager_exps ); } - Trace("cegqi-debug") << "...produced " << eager_eval_lem.size() << " eager evaluation lemmas." << std::endl; - if( !eager_eval_lem.empty() ){ + Trace("cegqi-debug") << "...produced " << eager_terms.size() << " eager evaluation lemmas." << std::endl; + if( !eager_terms.empty() ){ Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl; - for( unsigned j=0; j<eager_eval_lem.size(); j++ ){ - Node lem = eager_eval_lem[j]; + for( unsigned j=0; j<eager_terms.size(); j++ ){ + Node lem = NodeManager::currentNM()->mkNode( kind::OR, eager_exps[j].negate(), eager_terms[j].eqNode( eager_vals[j] ) ); if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){ //FIXME: hack to incorporate hacks from BV for division by zero lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem ); } Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl; - d_quantEngine->addLemma( lem ); + if( d_quantEngine->addLemma( lem ) ){ + addedEvalLemmas = true; + } } + } + if( addedEvalLemmas ){ return; } } @@ -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<vs.size(); i++ ){ + vtm[vs[i]] = ms[i]; + } + std::map< Node, Node > visited; + std::map< Node, std::vector< Node > > exp; + for( unsigned i=0; i<conj->getNumRefinementLemmas(); i++ ){ + Node lem; + std::vector< Node > cvars; + if( options::sygusUnifCondSol() ){ + //TODO : progress lemma + std::map< Node, Node > visitedc; + std::map< Node, std::vector< Node > > expc; + for( unsigned j=0; j<conj->getNumConditionalEvaluations( i ); j++ ){ + Node ce = conj->getConditionalEvaluation( i, j ); + Node cee = crefEvaluate( ce, vtm, visitedc, expc ); + Trace("sygus-cref-eval") << "Check conditional evaluation : " << ce << ", evaluates to " << cee << std::endl; + if( !cee.isNull() && cee.getKind()==kind::EQUAL ){ + // the conditional holds, we will apply this as a substitution + for( unsigned r=0; r<2; r++ ){ + if( cee[r].isVar() && cee[1-r].isConst() ){ + Node v = cee[r]; + Node c = cee[1-r]; + cvars.push_back( v ); + Assert( exp.find( v )==exp.end() ); + //TODO : should also carry symbolic solution (do not eagerly unfold conclusion of ce) + visited[v] = c; + exp[v].insert( exp[v].end(), expc[ce].begin(), expc[ce].end() ); + Trace("sygus-cref-eval") << " consider " << v << " -> " << c << std::endl; + break; + } + } + } + } + if( !cvars.empty() ){ + lem = conj->getRefinementBaseLemma( i ); + } + }else{ + lem = conj->getRefinementBaseLemma( i ); + } + if( !lem.isNull() ){ + Trace("sygus-cref-eval") << "Check refinement lemma " << lem << " against current model." << std::endl; + Node elem = crefEvaluate( lem, vtm, visited, exp ); + Trace("sygus-cref-eval") << "...evaluated to " << elem << ", exp size = " << exp[lem].size() << std::endl; + if( !elem.isNull() ){ + bool success = false; + success = elem==d_quantEngine->getTermDatabase()->d_false; + if( success ){ + elem = conj->getGuard().negate(); + Node cre_lem; + if( !exp[lem].empty() ){ + Node en = exp[lem].size()==1 ? exp[lem][0] : NodeManager::currentNM()->mkNode( kind::AND, exp[lem] ); + cre_lem = NodeManager::currentNM()->mkNode( kind::OR, en.negate(), elem ); + }else{ + cre_lem = elem; + } + if( std::find( lems.begin(), lems.end(), cre_lem )==lems.end() ){ + Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem << std::endl; + lems.push_back( cre_lem ); + } + } + } + } + // clean up caches + for( unsigned j=0; j<cvars.size(); j++ ){ + visited.erase( cvars[j] ); + exp.erase( cvars[j] ); + } + } + } +} + +Node CegInstantiation::crefEvaluate( Node n, std::map< Node, Node >& vtm, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& exp ){ + std::map< Node, Node >::iterator itv = visited.find( n ); + if( itv!=visited.end() ){ + return itv->second; + }else{ + std::vector< Node > exp_c; + Node ret; + if( n.getKind()==kind::APPLY_UF ){ + //it is an evaluation function + Trace("sygus-cref-eval-debug") << "Compute evaluation for : " << n << std::endl; + //unfold by one step + Node nn = d_quantEngine->getTermDatabaseSygus()->unfold( n, vtm, exp[n] ); + Trace("sygus-cref-eval-debug") << "...unfolded once to " << nn << std::endl; + Assert( nn!=n ); + //it is the result of evaluating the unfolding + ret = crefEvaluate( nn, vtm, visited, exp ); + //carry explanation + exp_c.push_back( nn ); + } + if( ret.isNull() ){ + if( n.getNumChildren()>0 ){ + std::vector< Node > children; + bool childChanged = false; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = crefEvaluate( n[i], vtm, visited, exp ); + childChanged = nc!=n[i] || childChanged; + children.push_back( nc ); + //Boolean short circuiting + if( n.getKind()==kind::AND ){ + if( nc==d_quantEngine->getTermDatabase()->d_false ){ + ret = nc; + exp_c.clear(); + } + }else if( n.getKind()==kind::OR ){ + if( nc==d_quantEngine->getTermDatabase()->d_true ){ + ret = nc; + exp_c.clear(); + } + }else if( n.getKind()==kind::ITE && i==0 ){ + int index = -1; + if( nc==d_quantEngine->getTermDatabase()->d_true ){ + index = 1; + }else if( nc==d_quantEngine->getTermDatabase()->d_false ){ + index = 2; + } + if( index!=-1 ){ + ret = crefEvaluate( n[index], vtm, visited, exp ); + exp_c.push_back( n[index] ); + } + } + //carry explanation + exp_c.push_back( n[i] ); + if( !ret.isNull() ){ + break; + } + } + if( ret.isNull() ){ + if( childChanged ){ + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + ret = Rewriter::rewrite( ret ); + }else{ + ret = n; + } + } + }else{ + ret = n; + } + } + //carry explanation from children + for( unsigned i=0; i<exp_c.size(); i++ ){ + Node nn = exp_c[i]; + std::map< Node, std::vector< Node > >::iterator itx = exp.find( nn ); + if( itx!=exp.end() ){ + for( unsigned j=0; j<itx->second.size(); j++ ){ + if( std::find( exp[n].begin(), exp[n].end(), itx->second[j] )==exp[n].end() ){ + exp[n].push_back( itx->second[j] ); + } + } + } + } + Trace("sygus-cref-eval-debug") << "... evaluation of " << n << " is (" << ret.getKind() << ") " << ret << std::endl; + Trace("sygus-cref-eval-debug") << "...... exp size = " << exp[n].size() << std::endl; + visited[n] = ret; + return ret; + } +} + void CegInstantiation::registerMeasuredType( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn ); if( it==d_uf_measure.end() ){ 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; i<n.getNumChildren(); i++) { - Node nc = getCurrentModelValue( n[i], partial ); - if (nc.isNull()) { - return Node::null(); - }else{ - children.push_back( nc ); - } - } - if( n.getKind()==APPLY_UF ){ - return getCurrentUfModelValue( n, children, partial ); - }else{ - Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children ); - nn = Rewriter::rewrite( nn ); - return nn; - } - }else{ - //return getRepresentative(n); - return getValue(n); - } -} - void FirstOrderModel::initialize() { processInitialize( true ); //this is called after representatives have been chosen and the equality engine has been built @@ -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<args.size(); i++) { @@ -667,6 +641,7 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & 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<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node op = it->first; - TypeNode tno = op.getType(); - for( unsigned i=0; i<tno.getNumChildren(); i++) { - preInitializeType( fm, tno[i] ); - } + //must ensure model basis terms exists in model for each relevant type + fm->initialize(); + for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node op = it->first; + TypeNode tno = op.getType(); + for( unsigned i=0; i<tno.getNumChildren(); i++) { + preInitializeType( fm, tno[i] ); } - //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts - if( !options::fmfEmptySorts() ){ - for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node q = fm->getAssertedQuantifier( i ); - //make sure all types are set - for( unsigned j=0; j<q[0].getNumChildren(); j++ ){ - preInitializeType( fm, q[0][j].getType() ); - } + } + //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts + if( !options::fmfEmptySorts() ){ + for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node q = fm->getAssertedQuantifier( i ); + //make sure all types are set + for( unsigned j=0; j<q[0].getNumChildren(); j++ ){ + preInitializeType( fm, q[0][j].getType() ); } } } + return true; } -void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ +bool FullModelChecker::processBuildModel(TheoryModel* m){ FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); - if( !fullModel ){ - Trace("fmc") << "---Full Model Check reset() " << std::endl; - d_quant_models.clear(); - d_rep_ids.clear(); - d_star_insts.clear(); - //process representatives - for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); - it != fm->d_rep_set.d_type_reps.end(); ++it ){ - if( it->first.isSort() ){ - Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; - for( size_t a=0; a<it->second.size(); a++ ){ - Node r = fm->getUsedRepresentative( it->second[a] ); - if( Trace.isOn("fmc-model-debug") ){ - std::vector< Node > eqc; - ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); - Trace("fmc-model-debug") << " " << (it->second[a]==r); - Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; - //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; - Trace("fmc-model-debug") << " {"; - for( size_t i=0; i<eqc.size(); i++ ){ - Trace("fmc-model-debug") << eqc[i] << ", "; - } - Trace("fmc-model-debug") << "}" << std::endl; + Trace("fmc") << "---Full Model Check reset() " << std::endl; + d_quant_models.clear(); + d_rep_ids.clear(); + d_star_insts.clear(); + //process representatives + for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); + it != fm->d_rep_set.d_type_reps.end(); ++it ){ + if( it->first.isSort() ){ + Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + for( size_t a=0; a<it->second.size(); a++ ){ + Node r = fm->getUsedRepresentative( it->second[a] ); + if( Trace.isOn("fmc-model-debug") ){ + std::vector< Node > eqc; + ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); + Trace("fmc-model-debug") << " " << (it->second[a]==r); + Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; + //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; + Trace("fmc-model-debug") << " {"; + for( size_t i=0; i<eqc.size(); i++ ){ + Trace("fmc-model-debug") << eqc[i] << ", "; } - d_rep_ids[it->first][r] = (int)a; + Trace("fmc-model-debug") << "}" << std::endl; } - Trace("fmc-model-debug") << std::endl; + d_rep_ids[it->first][r] = (int)a; } + Trace("fmc-model-debug") << std::endl; } + } - //now, make models - for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node op = it->first; - //reset the model - fm->d_models[op]->reset(); - - Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl; - std::vector< Node > add_conds; - std::vector< Node > add_values; - bool needsDefault = true; - for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + //now, make models + for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node op = it->first; + //reset the model + fm->d_models[op]->reset(); + + std::vector< Node > add_conds; + std::vector< Node > add_values; + bool needsDefault = true; + std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( op ); + if( itut!=fm->d_uf_terms.end() ){ + Trace("fmc-model-debug") << itut->second.size() << " model values for " << op << " ... " << std::endl; + for( size_t i=0; i<itut->second.size(); i++ ){ + Node n = itut->second[i]; if( d_qe->getTermDatabase()->isTermActive( n ) ){ add_conds.push_back( n ); add_values.push_back( n ); Node r = fm->getUsedRepresentative(n); Trace("fmc-model-debug") << n << " -> " << r << std::endl; - //AlwaysAssert( fm->areEqual( fm->d_uf_terms[op][i], r ) ); + //AlwaysAssert( fm->areEqual( itut->second[i], r ) ); }else{ if( Trace.isOn("fmc-model-debug") ){ Node r = fm->getUsedRepresentative(n); @@ -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<add_conds.size(); i++ ){ - Node c = add_conds[i]; - Node v = add_values[i]; - std::vector< Node > children; - std::vector< Node > entry_children; - children.push_back(op); - entry_children.push_back(op); - bool hasNonStar = false; - for( unsigned i=0; i<c.getNumChildren(); i++) { - Node ri = fm->getUsedRepresentative( c[i] ); - children.push_back(ri); - bool isStar = false; - if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){ - if (fm->isModelBasisTerm(ri) ) { - ri = fm->getStar( ri.getType() ); - isStar = true; - }else{ - hasNonStar = true; - } - } - if( !isStar && !ri.isConst() ){ - Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; - Assert( false ); + std::vector< Node > conds; + std::vector< Node > values; + std::vector< Node > entry_conds; + //get the entries for the mdoel + for( size_t i=0; i<add_conds.size(); i++ ){ + Node c = add_conds[i]; + Node v = add_values[i]; + std::vector< Node > children; + std::vector< Node > entry_children; + children.push_back(op); + entry_children.push_back(op); + bool hasNonStar = false; + for( unsigned i=0; i<c.getNumChildren(); i++) { + Node ri = fm->getUsedRepresentative( c[i] ); + children.push_back(ri); + bool isStar = false; + if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){ + if (fm->isModelBasisTerm(ri) ) { + ri = fm->getStar( ri.getType() ); + isStar = true; + }else{ + hasNonStar = true; } - entry_children.push_back(ri); } - Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); - Node nv = fm->getUsedRepresentative( v ); - if( !nv.isConst() ){ - Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl; + if( !isStar && !ri.isConst() ){ + Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; Assert( false ); } - Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children ); - if( std::find(conds.begin(), conds.end(), n )==conds.end() ){ - Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl; - conds.push_back(n); - values.push_back(nv); - entry_conds.push_back(en); - } - else { - Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl; - } + entry_children.push_back(ri); + } + Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + Node nv = fm->getUsedRepresentative( v ); + if( !nv.isConst() ){ + Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl; + Assert( false ); + } + Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children ); + if( std::find(conds.begin(), conds.end(), n )==conds.end() ){ + Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl; + conds.push_back(n); + values.push_back(nv); + entry_conds.push_back(en); } + else { + Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl; + } + } - //sort based on # default arguments - std::vector< int > indices; - ModelBasisArgSort mbas; - for (int i=0; i<(int)conds.size(); i++) { - d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] ); - mbas.d_terms.push_back(conds[i]); - indices.push_back(i); - } - std::sort( indices.begin(), indices.end(), mbas ); + //sort based on # default arguments + std::vector< int > indices; + ModelBasisArgSort mbas; + for (int i=0; i<(int)conds.size(); i++) { + d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] ); + mbas.d_terms.push_back(conds[i]); + indices.push_back(i); + } + std::sort( indices.begin(), indices.end(), mbas ); - for (int i=0; i<(int)indices.size(); i++) { - fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]); - } + for (int i=0; i<(int)indices.size(); i++) { + fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]); + } - if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){ - convertIntervalModel( fm, op ); - } + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){ + convertIntervalModel( fm, op ); + } - Trace("fmc-model-simplify") << "Before simplification : " << std::endl; - fm->d_models[op]->debugPrint("fmc-model-simplify", op, this); - Trace("fmc-model-simplify") << std::endl; + Trace("fmc-model-simplify") << "Before simplification : " << std::endl; + fm->d_models[op]->debugPrint("fmc-model-simplify", op, this); + Trace("fmc-model-simplify") << std::endl; - Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl; - fm->d_models[op]->simplify( this, fm ); + Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl; + fm->d_models[op]->simplify( this, fm ); - fm->d_models[op]->debugPrint("fmc-model", op, this); - Trace("fmc-model") << std::endl; + fm->d_models[op]->debugPrint("fmc-model", op, this); + Trace("fmc-model") << std::endl; - //for debugging - /* - for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ - std::vector< Node > inst; - for( unsigned j=0; j<fm->d_uf_terms[op][i].getNumChildren(); j++ ){ - Node r = fm->getUsedRepresentative( fm->d_uf_terms[op][i][j] ); - inst.push_back( r ); - } - Node ev = fm->d_models[op]->evaluate( fm, inst ); - Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl; - AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) ); + //for debugging + /* + for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ + std::vector< Node > inst; + for( unsigned j=0; j<fm->d_uf_terms[op][i].getNumChildren(); j++ ){ + Node r = fm->getUsedRepresentative( fm->d_uf_terms[op][i][j] ); + inst.push_back( r ); } - */ - } - }else{ - //make function values - for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){ - m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" ); + Node ev = fm->d_models[op]->evaluate( fm, inst ); + Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl; + AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) ); } - TheoryEngineModelBuilder::processBuildModel( m, fullModel ); - //mark that the model has been set - fm->markModelSet(); - //debug the model - debugModel( fm ); + */ + } + Assert( d_addedLemmas==0 ); + + //make function values + for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){ + m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" ); } + return TheoryEngineModelBuilder::processBuildModel( m ); } void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){ @@ -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; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node q = fm->getAssertedQuantifier( i, true ); - if( fm->isQuantifierActive( q ) ){ - //check if any of these quantified formulas can be set inactive - if( options::fmfEmptySorts() ){ - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - TypeNode tn = q[0][i].getType(); - //we are allowed to assume the type is empty - if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){ - Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl; - fm->setQuantifierActive( q, false ); - } +bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { + d_addedLemmas = 0; + d_triedLemmas = 0; + if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){ + FirstOrderModel * fm = (FirstOrderModel*)m; + //traverse equality engine + std::map< TypeNode, bool > eqc_usort; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + TypeNode tr = (*eqcs_i).getType(); + eqc_usort[tr] = true; + ++eqcs_i; + } + //look at quantified formulas + for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node q = fm->getAssertedQuantifier( i, true ); + if( fm->isQuantifierActive( q ) ){ + //check if any of these quantified formulas can be set inactive + if( options::fmfEmptySorts() ){ + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + TypeNode tn = q[0][i].getType(); + //we are allowed to assume the type is empty + if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){ + Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl; + fm->setQuantifierActive( q, false ); } - }else if( options::fmfFunWellDefinedRelevant() ){ - if( q[0].getNumChildren()==1 ){ - TypeNode tn = q[0][0].getType(); - if( tn.getAttribute(AbsTypeFunDefAttribute()) ){ - //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl; - //we are allowed to assume the introduced type is empty - if( eqc_usort.find( tn )==eqc_usort.end() ){ - Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl; - fm->setQuantifierActive( q, false ); - } + } + }else if( options::fmfFunWellDefinedRelevant() ){ + if( q[0].getNumChildren()==1 ){ + TypeNode tn = q[0][0].getType(); + if( tn.getAttribute(AbsTypeFunDefAttribute()) ){ + //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl; + //we are allowed to assume the introduced type is empty + if( eqc_usort.find( tn )==eqc_usort.end() ){ + Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl; + fm->setQuantifierActive( q, false ); } } } @@ -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; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node q = fm->getAssertedQuantifier( i ); + if( d_qe->getModel()->isQuantifierActive( q ) ){ + int lems = initializeQuantifier( q, q ); + d_statistics.d_init_inst_gen_lemmas += lems; + d_addedLemmas += lems; + if( d_qe->inConflict() ){ + break; + } + } } - TheoryEngineModelBuilder::processBuildModel( m, fullModel ); - //mark that the model has been set - fm->markModelSet(); - //debug the model - debugModel( fm ); - }else{ - d_curr_model = fm; - d_didInstGen = false; - //reset the internal information - reset( fm ); - //only construct first order model if optUseModel() is true - if( optUseModel() ){ - Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl; - //check if any quantifiers are un-initialized + if( d_addedLemmas>0 ){ + Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl; + return false; + }else{ + Assert( !d_qe->inConflict() ); + //initialize model + fm->initialize(); + //analyze the functions + Trace("model-engine-debug") << "Analyzing model..." << std::endl; + analyzeModel( fm ); + //analyze the quantifiers + Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl; + d_uf_prefs.clear(); for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node q = fm->getAssertedQuantifier( i ); - if( d_qe->getModel()->isQuantifierActive( q ) ){ - int lems = initializeQuantifier( q, q ); - d_statistics.d_init_inst_gen_lemmas += lems; - d_addedLemmas += lems; - if( d_qe->inConflict() ){ - break; - } - } + analyzeQuantifier( fm, q ); } - if( d_addedLemmas>0 ){ - Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl; - }else{ - Assert( !d_qe->inConflict() ); - //initialize model - fm->initialize(); - //analyze the functions - Trace("model-engine-debug") << "Analyzing model..." << std::endl; - analyzeModel( fm ); - //analyze the quantifiers - Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl; - d_uf_prefs.clear(); - for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node q = fm->getAssertedQuantifier( i ); - analyzeQuantifier( fm, q ); - } - //if applicable, find exceptions to model via inst-gen - if( options::fmfInstGen() ){ - d_didInstGen = true; - d_instGenMatches = 0; - d_numQuantSat = 0; - d_numQuantInstGen = 0; - d_numQuantNoInstGen = 0; - d_numQuantNoSelForm = 0; - //now, see if we know that any exceptions via InstGen exist - Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; - for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - if( d_qe->getModel()->isQuantifierActive( f ) ){ - int lems = doInstGen( fm, f ); - d_statistics.d_inst_gen_lemmas += lems; - d_addedLemmas += lems; - //temporary - if( lems>0 ){ - d_numQuantInstGen++; - }else if( hasInstGen( f ) ){ - d_numQuantNoInstGen++; - }else{ - d_numQuantNoSelForm++; - } - if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){ - break; - } + //if applicable, find exceptions to model via inst-gen + if( options::fmfInstGen() ){ + d_didInstGen = true; + d_instGenMatches = 0; + d_numQuantSat = 0; + d_numQuantInstGen = 0; + d_numQuantNoInstGen = 0; + d_numQuantNoSelForm = 0; + //now, see if we know that any exceptions via InstGen exist + Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; + for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + if( d_qe->getModel()->isQuantifierActive( f ) ){ + int lems = doInstGen( fm, f ); + d_statistics.d_inst_gen_lemmas += lems; + d_addedLemmas += lems; + //temporary + if( lems>0 ){ + d_numQuantInstGen++; + }else if( hasInstGen( f ) ){ + d_numQuantNoInstGen++; }else{ - d_numQuantSat++; + d_numQuantNoSelForm++; } - } - Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / "; - Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl; - Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl; - if( Trace.isOn("model-engine") ){ - if( d_addedLemmas>0 ){ - Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl; - }else{ - Trace("model-engine") << "No InstGen lemmas..." << std::endl; + if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){ + break; } + }else{ + d_numQuantSat++; } } - //construct the model if necessary - if( d_addedLemmas==0 ){ - //if no immediate exceptions, build the model - // this model will be an approximation that will need to be tested via exhaustive instantiation - Trace("model-engine-debug") << "Building model..." << std::endl; - //build model for UF - for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ - Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl; - constructModelUf( fm, it->first ); + Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / "; + Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl; + Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl; + if( Trace.isOn("model-engine") ){ + if( d_addedLemmas>0 ){ + Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl; + }else{ + Trace("model-engine") << "No InstGen lemmas..." << std::endl; } - Trace("model-engine-debug") << "Done building models." << std::endl; } } + //construct the model if necessary + if( d_addedLemmas==0 ){ + //if no immediate exceptions, build the model + // this model will be an approximation that will need to be tested via exhaustive instantiation + Trace("model-engine-debug") << "Building model..." << std::endl; + //build model for UF + for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ + Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl; + constructModelUf( fm, it->first ); + } + Trace("model-engine-debug") << "Done building models." << std::endl; + }else{ + return false; + } } } + //update models + for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ + it->second.update( fm ); + Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl; + //construct function values + fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" ); + } + Assert( d_addedLemmas==0 ); + return TheoryEngineModelBuilder::processBuildModel( m ); } int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ @@ -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; i<fmig->d_uf_terms[op].size(); i++ ){ - Node n = fmig->d_uf_terms[op][i]; - //for calculating if op is constant - if( d_qe->getTermDatabase()->isTermActive( n ) ){ - Node v = fmig->getRepresentative( n ); - if( i==0 ){ - d_uf_prefs[op].d_const_val = v; - }else if( v!=d_uf_prefs[op].d_const_val ){ - d_uf_prefs[op].d_const_val = Node::null(); - break; + std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op ); + if( itut!=fmig->d_uf_terms.end() ){ + for( size_t i=0; i<itut->second.size(); i++ ){ + Node n = fmig->d_uf_terms[op][i]; + //for calculating if op is constant + if( d_qe->getTermDatabase()->isTermActive( n ) ){ + Node v = fmig->getRepresentative( n ); + if( i==0 ){ + d_uf_prefs[op].d_const_val = v; + }else if( v!=d_uf_prefs[op].d_const_val ){ + d_uf_prefs[op].d_const_val = Node::null(); + break; + } } - } - //for calculating terms that we don't need to consider - if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){ - if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){ - //need to consider if it is not congruent modulo model basis - if( !tabt.addTerm( fmig, n ) ){ - d_basisNoMatch[n] = true; + //for calculating terms that we don't need to consider + if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){ + if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){ + //need to consider if it is not congruent modulo model basis + if( !tabt.addTerm( fmig, n ) ){ + d_basisNoMatch[n] = true; + } } } } @@ -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; i<fmig->d_uf_terms[op].size(); i++ ){ - Node n = fmig->d_uf_terms[op][i]; - if( isTermActive( n ) ){ - Node v = fmig->getRepresentative( n ); - Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl; - //if this assertion did not help the model, just consider it ground - //set n = v in the model tree - //set it as ground value - fmig->d_uf_model_gen[op].setValue( fm, n, v ); - if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){ - //also set as default value if necessary - if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){ - Trace("fmf-model-cons") << " Set as default." << std::endl; - fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); + std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op ); + if( itut!=fmig->d_uf_terms.end() ){ + for( size_t i=0; i<itut->second.size(); i++ ){ + Node n = itut->second[i]; + if( isTermActive( n ) ){ + Node v = fmig->getRepresentative( n ); + Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl; + //if this assertion did not help the model, just consider it ground + //set n = v in the model tree + //set it as ground value + fmig->d_uf_model_gen[op].setValue( fm, n, v ); + if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){ + //also set as default value if necessary + if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){ + Trace("fmf-model-cons") << " Set as default." << std::endl; + fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); + if( n==defaultTerm ){ + //incidentally already set, we will not need to find a default value + setDefaultVal = false; + } + } + }else{ if( n==defaultTerm ){ + fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); //incidentally already set, we will not need to find a default value setDefaultVal = false; } } - }else{ - if( n==defaultTerm ){ - fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); - //incidentally already set, we will not need to find a default value - setDefaultVal = false; - } } } } 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; i<d_model->getNumAssertedQuantifiers(); i++ ){ - Node q = d_model->getAssertedQuantifier( i ); + FirstOrderModel* fm = d_qe->getModel(); + for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node q = fm->getAssertedQuantifier( i ); Node icf = d_qe->getTermDatabase()->getInstConstantBody( q ); Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl; computeRelevantDomain( q, icf, true, true ); @@ -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; i<it->second.size(); i++ ){ Assert( vars.size()==it->second[i].size() ); Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() ); - Node lem = NodeManager::currentNM()->mkNode(EQUAL, d_evals[n][i], sBTerm ); - lem = NodeManager::currentNM()->mkNode( OR, antec, lem ); - Trace("sygus-eager") << "Lemma : " << lem << std::endl; - lems.push_back( lem ); + sBTerm = Rewriter::rewrite( sBTerm ); + //Node lem = NodeManager::currentNM()->mkNode(EQUAL, d_evals[n][i], sBTerm ); + //lem = NodeManager::currentNM()->mkNode( OR, antec.negate(), lem ); + terms.push_back( d_evals[n][i] ); + vals.push_back( sBTerm ); + exps.push_back( antec ); + Trace("sygus-eager") << "Conclude : " << d_evals[n][i] << " == " << sBTerm << std::endl; + Trace("sygus-eager") << " from " << antec << std::endl; + //Trace("sygus-eager") << "Lemma : " << lem << std::endl; + //lems.push_back( lem ); } d_node_mv_args_proc[n][vn] = it->second.size(); } @@ -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; i<en.getNumChildren(); i++ ){ + args.push_back( en[i] ); + } + const Datatype& dt = ((DatatypeType)(ev.getType()).toType()).getDatatype(); + unsigned i = Datatype::indexOf( ev.getOperator().toExpr() ); + //explanation + Node ee = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), en[0] ); + if( std::find( exp.begin(), exp.end(), ee )==exp.end() ){ + exp.push_back( ee ); + } + std::map< int, Node > pre; + for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ + std::vector< Node > cc; + //get the evaluation argument for the selector + const Datatype & ad = ((DatatypeType)dt[i][j].getRangeType()).getDatatype(); + cc.push_back( Node::fromExpr( ad.getSygusEvaluationFunc() ) ); + Node s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[i][j].getSelector() ), en[0] ); + cc.push_back( s ); + //update vtm map + vtm[s] = ev[j]; + cc.insert( cc.end(), args.begin(), args.end() ); + pre[j] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, cc ); + } + std::map< TypeNode, int > var_count; + Node ret = mkGeneric( dt, i, var_count, pre ); + // if it is a variable, apply the substitution + if( ret.getKind()==kind::BOUND_VARIABLE ){ + //replace by argument + Node var_list = Node::fromExpr( dt.getSygusVarList() ); + //TODO : set argument # on sygus variables + for( unsigned j=0; j<var_list.getNumChildren(); j++ ){ + if( var_list[j]==ret ){ + ret = args[j]; + break; + } + } + Assert( ret.isConst() ); + }else if( ret.getKind()==APPLY ){ + //must expand definitions to account for defined functions in sygus grammars + ret = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( ret.toExpr() ) ); + } + return ret; + }else{ + Assert( false ); + } + }else{ + Assert( en.isConst() ); + } + return en; +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ 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<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(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<Node, Node, NodeHashFunction> NodeMap; typedef std::hash_map<TNode, Node, TNodeHashFunction> 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<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ) { - constantReps[eqc] = const_rep; +void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep ) { + d_constantReps[eqc] = const_rep; Trace("model-builder") << " Assign: Setting constant rep of " << eqc << " to " << const_rep << endl; - if( !fullModel ){ - tm->d_rep_set.d_values_to_terms[const_rep] = eqc; - } + tm->d_rep_set.d_values_to_terms[const_rep] = eqc; } bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) { @@ -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<Node>& repSet = TypeSet::getSet(it); - if (!repSet.empty()) { - Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl; - Assert(false); - } + // Assert that all representatives have been converted to constants + for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) { + set<Node>& repSet = TypeSet::getSet(it); + if (!repSet.empty()) { + Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl; + Assert(false); } } #endif /* CVC4_ASSERTIONS */ @@ -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<Node>& noRepSet = TypeSet::getSet(it); - set<Node>::iterator i; - for (i = noRepSet.begin(); i != noRepSet.end(); ++i) { - tm->d_reps[*i] = *i; - tm->d_rep_set.add((*i).getType(), *i); - } + Trace("model-builder") << "Make sure ECs have reps..." << std::endl; + // Make sure every EC has a rep + for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) { + tm->d_reps[itMap->first] = itMap->second; + tm->d_rep_set.add(itMap->second.getType(), itMap->second); + } + for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { + set<Node>& noRepSet = TypeSet::getSet(it); + set<Node>::iterator i; + for (i = noRepSet.begin(); i != noRepSet.end(); ++i) { + tm->d_reps[*i] = *i; + tm->d_rep_set.add((*i).getType(), *i); } } //modelBuilder-specific initialization - processBuildModel( tm, fullModel ); - - // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model) - if( fullModel ){ - Trace("model-builder") << "TheoryEngineModelBuilder: Post-process model..." << std::endl; - d_te->postProcessModel(tm); + if( !processBuildModel( tm ) ){ + return false; + }else{ + return true; } - +} + +void TheoryEngineModelBuilder::debugCheckModel(Model* m){ + TheoryModel* tm = (TheoryModel*)m; #ifdef CVC4_ASSERTIONS - if (fullModel) { - // Check that every term evaluates to its representative in the model - for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) { - // eqc is the equivalence class representative - Node eqc = (*eqcs_i); - Node rep; - itMap = constantReps.find(eqc); - if (itMap == constantReps.end() && eqc.getType().isBoolean()) { - rep = tm->getValue(eqc); - Assert(rep.isConst()); - } - else { - Assert(itMap != constantReps.end()); - rep = itMap->second; - } - eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); - for ( ; !eqc_i.isFinished(); ++eqc_i) { - Node n = *eqc_i; - static int repCheckInstance = 0; - ++repCheckInstance; - - Debug("check-model::rep-checking") - << "( " << repCheckInstance <<") " - << "n: " << n << endl - << "getValue(n): " << tm->getValue(n) << endl - << "rep: " << rep << endl; - Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details"); - } + Assert(tm->isBuilt()); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine ); + std::map< Node, Node >::iterator itMap; + // Check that every term evaluates to its representative in the model + for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) { + // eqc is the equivalence class representative + Node eqc = (*eqcs_i); + Node rep; + itMap = d_constantReps.find(eqc); + if (itMap == d_constantReps.end() && eqc.getType().isBoolean()) { + rep = tm->getValue(eqc); + Assert(rep.isConst()); + } + else { + Assert(itMap != d_constantReps.end()); + rep = itMap->second; + } + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); + for ( ; !eqc_i.isFinished(); ++eqc_i) { + Node n = *eqc_i; + static int repCheckInstance = 0; + ++repCheckInstance; + + Debug("check-model::rep-checking") + << "( " << repCheckInstance <<") " + << "n: " << n << endl + << "getValue(n): " << tm->getValue(n) << endl + << "rep: " << rep << endl; + Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details"); } } #endif /* CVC4_ASSERTIONS */ + debugModel( tm ); } - -Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps, bool evalOnly) +Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly) { - std::map<Node, Node>::iterator itMap = constantReps.find(r); - if (itMap != constantReps.end()) { + std::map<Node, Node>::iterator itMap = d_constantReps.find(r); + if (itMap != d_constantReps.end()) { return (*itMap).second; } NodeMap::iterator it = d_normalizedCache.find(r); @@ -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; i<it->second.size(); i++ ){ - un = it->second[i]; - vector<TNode> children; - children.push_back(n); - for (size_t j = 0; j < un.getNumChildren(); ++j) { - children.push_back(m->getRepresentative(un[j])); - } - simp = NodeManager::currentNM()->mkNode(un.getKind(), children); - v = m->getRepresentative(un); - Trace("model-builder") << " Setting (" << simp << ") to (" << v << ")" << endl; - ufmt.setValue(m, simp, v); - default_v = v; - } - if( default_v.isNull() ){ - //choose default value from model if none exists - TypeEnumerator te(type.getRangeType()); - default_v = (*te); - } - ufmt.setDefaultValue( m, default_v ); - if(options::condenseFunctionValues()) { - ufmt.simplify(); +bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m){ + Trace("model-builder") << "Assigning function values..." << endl; + //construct function values + for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){ + Node n = it->first; + if( m->d_uf_models.find( n )==m->d_uf_models.end() ){ + TypeNode type = n.getType(); + Trace("model-builder") << " Assign function value for " << n << " " << type << std::endl; + uf::UfModelTree ufmt( n ); + Node default_v, un, simp, v; + for( size_t i=0; i<it->second.size(); i++ ){ + un = it->second[i]; + vector<TNode> children; + children.push_back(n); + for (size_t j = 0; j < un.getNumChildren(); ++j) { + children.push_back(m->getRepresentative(un[j])); } - Node val = ufmt.getFunctionValue( "_ufmt_", options::condenseFunctionValues() ); - Trace("model-builder") << " Assigning (" << n << ") to (" << val << ")" << endl; - m->d_uf_models[n] = val; - //ufmt.debugPrint( std::cout, m ); + simp = NodeManager::currentNM()->mkNode(un.getKind(), children); + v = m->getRepresentative(un); + Trace("model-builder") << " Setting (" << simp << ") to (" << v << ")" << endl; + ufmt.setValue(m, simp, v); + default_v = v; + } + if( default_v.isNull() ){ + //choose default value from model if none exists + TypeEnumerator te(type.getRangeType()); + default_v = (*te); + } + ufmt.setDefaultValue( m, default_v ); + if(options::condenseFunctionValues()) { + ufmt.simplify(); } + Node val = ufmt.getFunctionValue( "_ufmt_", options::condenseFunctionValues() ); + Trace("model-builder") << " Assigning (" << n << ") to (" << val << ")" << endl; + m->d_uf_models[n] = val; + //ufmt.debugPrint( std::cout, m ); } } + return true; } } /* namespace CVC4::theory */ 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<bool> 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<Node, Node, NodeHashFunction> NodeMap; NodeMap d_normalizedCache; typedef std::hash_set<Node, NodeHashFunction> NodeSet; + std::map< Node, Node > d_constantReps; /** process build model */ - virtual void preProcessBuildModel(TheoryModel* m, bool fullModel); - virtual void processBuildModel(TheoryModel* m, bool fullModel); + virtual bool preProcessBuildModel(TheoryModel* m); + virtual bool processBuildModel(TheoryModel* m); + virtual void debugModel( TheoryModel* m ) {} /** normalize representative */ - Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly); + Node normalize(TheoryModel* m, TNode r, bool evalOnly); bool isAssignable(TNode n); void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache); - void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ); + void assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep ); /** is v an excluded codatatype value */ bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ); bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ); @@ -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 */ |