From 25a01d31bffcdcc339dce332ac893460b5f4cdcf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 4 Jun 2013 12:12:30 -0500 Subject: Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant bounds for bounded integers. --- src/theory/quantifiers/bounded_integers.cpp | 14 +- src/theory/quantifiers/first_order_model.cpp | 127 ++++++++++- src/theory/quantifiers/first_order_model.h | 36 +++ src/theory/quantifiers/full_model_check.cpp | 318 ++++++++++++--------------- src/theory/quantifiers/full_model_check.h | 37 +--- 5 files changed, 320 insertions(+), 212 deletions(-) (limited to 'src/theory/quantifiers') diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index e33cd2131..e402a8969 100755 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -184,7 +184,7 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) { } } }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) { - std::cout << "BoundedIntegers : Bad kind for literal : " << lit << std::endl; + Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl; exit(0); } } @@ -283,11 +283,13 @@ void BoundedIntegers::registerQuantifier( Node f ) { d_range[f][v] = new_range; r = new_range; } - if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){ - Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl; - d_ranges.push_back( r ); - d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() ); - d_rms[r]->initialize(); + if( r.getKind()!=CONST_RATIONAL ){ + if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){ + Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl; + d_ranges.push_back( r ); + d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() ); + d_rms[r]->initialize(); + } } } } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index cf4381c02..4b101de49 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -25,6 +25,7 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; +using namespace CVC4::theory::quantifiers::fmcheck; FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){ @@ -507,4 +508,128 @@ Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & ar }else{ return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex ); } -} \ No newline at end of file +} + + + + + + +FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) : +FirstOrderModel(c, name), d_qe(qe){ + +} + +Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { + //Assert( fm->hasTerm(n) ); + TypeNode tn = n.getType(); + if( tn.isBoolean() ){ + return areEqual(n, d_true) ? d_true : d_false; + }else{ + if( !hasTerm(n) ){ + if( strict ){ + return Node::null(); + }else{ + Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl; + } + } + Node r = getRepresentative(n); + if( d_model_basis_rep.find(tn)!=d_model_basis_rep.end() ){ + if (r==d_model_basis_rep[tn]) { + r = d_qe->getTermDatabase()->getModelBasisTerm(tn); + } + } + return r; + } +} + +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; ievaluate(this, args); +} + +void FirstOrderModelFmc::processInitialize() { + for( std::map::iterator it = d_models.begin(); it != d_models.end(); ++it ){ + it->second->reset(); + } + d_model_basis_rep.clear(); +} + +void FirstOrderModelFmc::processInitializeModelForTerm(Node n) { + if( n.getKind()==APPLY_UF ){ + if( d_models.find(n.getOperator())==d_models.end()) { + d_models[n.getOperator()] = new Def; + } + } +} + +Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){ + //check if there is even any domain elements at all + if (!d_rep_set.hasType(tn)) { + Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; + Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); + d_rep_set.d_type_reps[tn].push_back(mbt); + }else if( d_rep_set.d_type_reps[tn].size()==0 ){ + Message() << "empty reps" << std::endl; + exit(0); + } + return d_rep_set.d_type_reps[tn][0]; +} + + +bool FirstOrderModelFmc::isStar(Node n) { + return n==getStar(n.getType()); +} + +Node FirstOrderModelFmc::getStar(TypeNode tn) { + if( d_type_star.find(tn)==d_type_star.end() ){ + Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" ); + d_type_star[tn] = st; + } + return d_type_star[tn]; +} + +bool FirstOrderModelFmc::isModelBasisTerm(Node n) { + return n==getModelBasisTerm(n.getType()); +} + +Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) { + return d_qe->getTermDatabase()->getModelBasisTerm(tn); +} + +Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { + TypeNode type = op.getType(); + std::vector< Node > vars; + for( size_t i=0; imkBoundVar( ss.str(), type[i] ) ); + } + Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); + Node curr; + for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { + Node v = getUsedRepresentative( d_models[op]->d_value[i] ); + if( curr.isNull() ){ + curr = v; + }else{ + //make the condition + Node cond = d_models[op]->d_cond[i]; + std::vector< Node > children; + for( unsigned j=0; jmkNode( EQUAL, vars[j], c ) ); + } + } + Assert( !children.empty() ); + Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ); + curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr ); + } + } + curr = Rewriter::rewrite( curr ); + return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); +} diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 491e97097..c2d82cc0a 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -120,6 +120,42 @@ private: }; +namespace fmcheck { + +class Def; + +class FirstOrderModelFmc : public FirstOrderModel +{ + friend class FullModelChecker; +private: + /** quant engine */ + QuantifiersEngine * d_qe; + /** models for UF */ + std::map d_models; + std::map d_model_basis_rep; + std::map d_type_star; + 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); + FirstOrderModelFmc * asFirstOrderModelFmc() { return this; } + // initialize the model + void processInitialize(); + + Node getFunctionValue(Node op, const char* argPrefix ); + + bool isStar(Node n); + Node getStar(TypeNode tn); + bool isModelBasisTerm(Node n); + Node getModelBasisTerm(TypeNode tn); + Node getSomeDomainElement(TypeNode tn); +}; + +} + + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 2513cb08e..b16115749 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -190,119 +190,6 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { } - -FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) : -FirstOrderModel(c, name), d_qe(qe){ - -} - -Node FirstOrderModelFmc::getUsedRepresentative(Node n) { - //Assert( fm->hasTerm(n) ); - TypeNode tn = n.getType(); - if( tn.isBoolean() ){ - return areEqual(n, d_true) ? d_true : d_false; - }else{ - Node r = getRepresentative(n); - if (r==d_model_basis_rep[tn]) { - r = d_qe->getTermDatabase()->getModelBasisTerm(tn); - } - return r; - } -} - -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; ievaluate(this, args); -} - -void FirstOrderModelFmc::processInitialize() { - for( std::map::iterator it = d_models.begin(); it != d_models.end(); ++it ){ - it->second->reset(); - } - d_model_basis_rep.clear(); -} - -void FirstOrderModelFmc::processInitializeModelForTerm(Node n) { - if( n.getKind()==APPLY_UF ){ - if( d_models.find(n.getOperator())==d_models.end()) { - d_models[n.getOperator()] = new Def; - } - } -} - -Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){ - //check if there is even any domain elements at all - if (!d_rep_set.hasType(tn)) { - Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; - Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); - d_rep_set.d_type_reps[tn].push_back(mbt); - }else if( d_rep_set.d_type_reps[tn].size()==0 ){ - Message() << "empty reps" << std::endl; - exit(0); - } - return d_rep_set.d_type_reps[tn][0]; -} - - -bool FirstOrderModelFmc::isStar(Node n) { - return n==getStar(n.getType()); -} - -Node FirstOrderModelFmc::getStar(TypeNode tn) { - if( d_type_star.find(tn)==d_type_star.end() ){ - Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" ); - d_type_star[tn] = st; - } - return d_type_star[tn]; -} - -bool FirstOrderModelFmc::isModelBasisTerm(Node n) { - return n==getModelBasisTerm(n.getType()); -} - -Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) { - return d_qe->getTermDatabase()->getModelBasisTerm(tn); -} - -Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { - TypeNode type = op.getType(); - std::vector< Node > vars; - for( size_t i=0; imkBoundVar( ss.str(), type[i] ) ); - } - Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); - Node curr; - for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { - Node v = getUsedRepresentative( d_models[op]->d_value[i] ); - if( curr.isNull() ){ - curr = v; - }else{ - //make the condition - Node cond = d_models[op]->d_cond[i]; - std::vector< Node > children; - for( unsigned j=0; jmkNode( EQUAL, vars[j], c ) ); - } - } - Assert( !children.empty() ); - Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ); - curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr ); - } - } - curr = Rewriter::rewrite( curr ); - return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); -} - - - FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) : QModelBuilder( c, qe ){ d_true = NodeManager::currentNM()->mkConst(true); @@ -369,6 +256,18 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } } } + //also process non-rep set sorts + for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node op = it->first; + TypeNode tno = op.getType(); + for( unsigned i=0; id_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){ + Node mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); + fm->d_model_basis_rep[tn] = fm->getUsedRepresentative( mbn ); + } + } + } //now, make models for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { Node op = it->first; @@ -397,7 +296,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Trace("fmc-model-debug") << "Add default " << nmb << std::endl; addEntry(fm, op, nmb, nmb, conds, values, entry_conds); }else{ - Node vmb = fm->getSomeDomainElement(nmb.getType()); + 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; addEntry(fm, op, nmb, vmb, conds, values, entry_conds); @@ -570,30 +469,24 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Nod if( riter.setQuantifier( f ) ){ std::vector< RepDomain > dom; for (unsigned i=0; iisStar(c[i]) ){ - //add the full range - //for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin(); - // it != d_rep_ids[tn].end(); ++it ){ - // rd.push_back(it->second); - //} - }else{ - if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) { - //rd.push_back(d_rep_ids[tn][c[i]]); - riter.d_domain[i].clear(); - riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]); + if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) { + TypeNode tn = c[i].getType(); + if( d_rep_ids.find(tn)!=d_rep_ids.end() ){ + if( fm->isStar(c[i]) ){ + //add the full range }else{ - return -1; + if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) { + riter.d_domain[i].clear(); + riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]); + }else{ + return -1; + } } + }else{ + return -1; } - //dom.push_back(rd); - }else{ - return -1; } } - //riter.setDomain(dom); //now do full iteration while( !riter.isFinished() ){ Trace("fmc-exh-debug") << "Inst : "; @@ -633,14 +526,6 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n d.addEntry(fm, mkCondDefault(fm, f), n); Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl; } - else if( n.getNumChildren()==0 ){ - Node r = n; - if( !fm->hasTerm(n) ){ - r = fm->getSomeDomainElement(n.getType() ); - } - r = fm->getUsedRepresentative( r); - d.addEntry(fm, mkCondDefault(fm, f), r); - } else if( n.getKind() == kind::NOT ){ //just do directly doCheck( fm, f, d, n[0] ); @@ -649,6 +534,42 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n else if( n.getKind() == kind::FORALL ){ d.addEntry(fm, mkCondDefault(fm, f), Node::null()); } + else if( n.getType().isArray() ){ + //make the definition + Node r = fm->getRepresentative(n); + Trace("fmc-debug") << "Representative for array is " << r << std::endl; + while( r.getKind() == kind::STORE ){ + Node i = fm->getUsedRepresentative( r[1] ); + Node e = fm->getUsedRepresentative( r[2] ); + d.addEntry(fm, mkArrayCond(i), e ); + r = r[0]; + } + Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType())); + bool success = false; + if( r.getKind() == kind::STORE_ALL ){ + ArrayStoreAll storeAll = r.getConst(); + Node defaultValue = Node::fromExpr(storeAll.getExpr()); + defaultValue = fm->getUsedRepresentative( defaultValue, true ); + if( !defaultValue.isNull() ){ + d.addEntry(fm, defC, defaultValue); + success = true; + } + } + if( !success ){ + Trace("fmc-debug") << "Can't process base array " << r << std::endl; + //can't process this array + d.reset(); + d.addEntry(fm, defC, Node::null()); + } + } + else if( n.getNumChildren()==0 ){ + Node r = n; + if( !fm->hasTerm(n) ){ + r = getSomeDomainElement(fm, n.getType() ); + } + r = fm->getUsedRepresentative( r); + d.addEntry(fm, mkCondDefault(fm, f), r); + } else{ std::vector< int > var_ch; std::vector< Def > children; @@ -665,6 +586,14 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl; //uninterpreted compose doUninterpretedCompose( fm, f, d, n.getOperator(), children ); + } else if( n.getKind()==SELECT ){ + Trace("fmc-debug") << "Do select compose " << n << std::endl; + std::vector< Def > children2; + children2.push_back( children[1] ); + std::vector< Node > cond; + mkCondDefaultVec(fm, f, cond); + std::vector< Node > val; + doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val ); } else { if( !var_ch.empty() ){ if( n.getKind()==EQUAL ){ @@ -676,8 +605,8 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n doVariableRelation( fm, f, d, var_ch[0]==0 ? children[1] : children[0], var_ch[0]==0 ? n[0] : n[1] ); } }else{ - std::cout << "Don't know how to check " << n << std::endl; - exit(0); + Trace("fmc-warn") << "Don't know how to check " << n << std::endl; + d.addEntry(fm, mkCondDefault(fm, f), Node::null()); } }else{ Trace("fmc-debug") << "Do interpreted compose " << n << std::endl; @@ -713,7 +642,7 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def int k = getVariableId(f, eq[1]); TypeNode tn = eq[0].getType(); if( !fm->d_rep_set.hasType( tn ) ){ - fm->getSomeDomainElement( tn ); //to verify the type is initialized + getSomeDomainElement( fm, tn ); //to verify the type is initialized } for (unsigned i=0; id_rep_set.d_type_reps[tn].size(); i++) { Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] ); @@ -729,19 +658,23 @@ void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def int j = getVariableId(f, v); for (unsigned i=0; iisStar(dc.d_cond[i][j])) { - std::vector cond; - mkCondVec(dc.d_cond[i],cond); - cond[j+1] = val; - d.addEntry(fm, mkCond(cond), d_true); - cond[j+1] = fm->getStar(val.getType()); - d.addEntry(fm, mkCond(cond), d_false); + if( val.isNull() ){ + d.addEntry( fm, dc.d_cond[i], val); + }else{ + if( dc.d_cond[i][j]!=val ){ + if (fm->isStar(dc.d_cond[i][j])) { + std::vector cond; + mkCondVec(dc.d_cond[i],cond); + cond[j+1] = val; + d.addEntry(fm, mkCond(cond), d_true); + cond[j+1] = fm->getStar(val.getType()); + d.addEntry(fm, mkCond(cond), d_false); + }else{ + d.addEntry( fm, dc.d_cond[i], d_false); + } }else{ - d.addEntry( fm, dc.d_cond[i], d_false); + d.addEntry( fm, dc.d_cond[i], d_true); } - }else{ - d.addEntry( fm, dc.d_cond[i], d_true); } } } @@ -754,11 +687,11 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, std::vector< Node > cond; mkCondDefaultVec(fm, f, cond); std::vector< Node > val; - doUninterpretedCompose( fm, f, op, d, dc, 0, cond, val); + doUninterpretedCompose( fm, f, d, *fm->d_models[op], dc, 0, cond, val); } -void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d, - std::vector< Def > & dc, int index, +void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, + Def & df, std::vector< Def > & dc, int index, std::vector< Node > & cond, std::vector & val ) { Trace("fmc-uf-process") << "process at " << index << std::endl; for( unsigned i=1; i entries; - doUninterpretedCompose2( fm, f, entries, 0, cond, val, fm->d_models[op]->d_et); - //add them to the definition - for( unsigned e=0; ed_models[op]->d_cond.size(); e++ ){ - if ( entries.find(e)!=entries.end() ){ - d.addEntry(fm, entries[e], fm->d_models[op]->d_value[e] ); + doUninterpretedCompose2( fm, f, entries, 0, cond, val, df.d_et); + if( entries.empty() ){ + d.addEntry(fm, mkCond(cond), Node::null()); + }else{ + //add them to the definition + for( unsigned e=0; eisStar(cond[j+1])) { @@ -829,14 +766,16 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, } cond[j+1] = fm->getStar(v.getType()); }else{ - if (curr.d_child.find(v)!=curr.d_child.end()) { - Trace("fmc-uf-process") << "follow value..." << std::endl; - doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]); - } - Node st = fm->getStar(v.getType()); - if (curr.d_child.find(st)!=curr.d_child.end()) { - Trace("fmc-uf-process") << "follow star..." << std::endl; - doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]); + if( !v.isNull() ){ + if (curr.d_child.find(v)!=curr.d_child.end()) { + Trace("fmc-uf-process") << "follow value..." << std::endl; + doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]); + } + Node st = fm->getStar(v.getType()); + if (curr.d_child.find(st)!=curr.d_child.end()) { + Trace("fmc-uf-process") << "follow star..." << std::endl; + doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]); + } } } } @@ -928,9 +867,28 @@ void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) { } } +Node FullModelChecker::mkArrayCond( Node a ) { + if( d_array_term_cond.find(a)==d_array_term_cond.end() ){ + if( d_array_cond.find(a.getType())==d_array_cond.end() ){ + TypeNode typ = NodeManager::currentNM()->mkFunctionType( a.getType(), NodeManager::currentNM()->booleanType() ); + Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" ); + d_array_cond[a.getType()] = op; + } + std::vector< Node > cond; + cond.push_back(d_array_cond[a.getType()]); + cond.push_back(a); + d_array_term_cond[a] = NodeManager::currentNM()->mkNode(APPLY_UF, cond ); + } + return d_array_term_cond[a]; +} + Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) { if( n.getKind()==EQUAL ){ - return vals[0]==vals[1] ? d_true : d_false; + if (!vals[0].isNull() && !vals[1].isNull()) { + return vals[0]==vals[1] ? d_true : d_false; + }else{ + return Node::null(); + } }else if( n.getKind()==ITE ){ if( vals[0]==d_true ){ return vals[1]; @@ -969,6 +927,15 @@ Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) } } +Node FullModelChecker::getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ) { + bool addRepId = !fm->d_rep_set.hasType( tn ); + Node de = fm->getSomeDomainElement(tn); + if( addRepId ){ + d_rep_ids[tn][de] = 0; + } + return de; +} + Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) { return fm->getFunctionValue(op, argPrefix); } @@ -1003,6 +970,9 @@ void FullModelChecker::addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node 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; + } } bool FullModelChecker::useSimpleModels() { diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index ddf298006..c390c9437 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -71,35 +71,6 @@ public: void debugPrint(const char * tr, Node op, FullModelChecker * m); }; -class FirstOrderModelFmc : public FirstOrderModel -{ - friend class FullModelChecker; -private: - /** quant engine */ - QuantifiersEngine * d_qe; - /** models for UF */ - std::map d_models; - std::map d_model_basis_rep; - std::map d_type_star; - Node getUsedRepresentative(Node n); - /** 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); - FirstOrderModelFmc * asFirstOrderModelFmc() { return this; } - // initialize the model - void processInitialize(); - - Node getFunctionValue(Node op, const char* argPrefix ); - - bool isStar(Node n); - Node getStar(TypeNode tn); - bool isModelBasisTerm(Node n); - Node getModelBasisTerm(TypeNode tn); - Node getSomeDomainElement(TypeNode tn); -}; - class FullModelChecker : public QModelBuilder { @@ -109,6 +80,8 @@ protected: std::map > d_rep_ids; std::map d_quant_models; std::map d_quant_cond; + std::map< TypeNode, Node > d_array_cond; + std::map< Node, Node > d_array_term_cond; std::map > d_quant_var_id; std::map > d_star_insts; Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); @@ -126,8 +99,8 @@ private: void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v); void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc ); - void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d, - std::vector< Def > & dc, int index, + void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, + Def & df, std::vector< Def > & dc, int index, std::vector< Node > & cond, std::vector & val ); void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, std::map< int, Node > & entries, int index, @@ -143,7 +116,9 @@ private: Node mkCondDefault( FirstOrderModelFmc * fm, Node f ); void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ); void mkCondVec( Node n, std::vector< Node > & cond ); + Node mkArrayCond( Node a ); Node evaluateInterpreted( Node n, std::vector< Node > & vals ); + Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); public: FullModelChecker( context::Context* c, QuantifiersEngine* qe ); ~FullModelChecker(){} -- cgit v1.2.3