diff options
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
| -rwxr-xr-x | src/theory/quantifiers/full_model_check.cpp | 571 |
1 files changed, 281 insertions, 290 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index b5d4648a1..2513cb08e 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -24,8 +24,17 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst;
using namespace CVC4::theory::quantifiers::fmcheck;
+struct ModelBasisArgSort
+{
+ std::vector< Node > d_terms;
+ bool operator() (int i,int j) {
+ return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <
+ d_terms[j].getAttribute(ModelBasisArgAttribute()) );
+ }
+};
-bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) {
+
+bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
if (index==(int)c.getNumChildren()) {
return d_data!=-1;
}else{
@@ -44,7 +53,7 @@ bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) { }
}
-int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index ) {
+int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index ) {
if (index==(int)inst.size()) {
return d_data;
}else{
@@ -64,7 +73,7 @@ int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & }
}
-void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int index ) {
+void EntryTrie::addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index ) {
if (index==(int)c.getNumChildren()) {
if(d_data==-1) {
d_data = data;
@@ -75,7 +84,7 @@ void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int in }
}
-void EntryTrie::getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {
+void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {
if (index==(int)c.getNumChildren()) {
if( d_data!=-1) {
if( is_gen ){
@@ -101,13 +110,8 @@ void EntryTrie::getEntries( FullModelChecker * m, Node c, std::vector<int> & com }
}
-bool EntryTrie::getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index) {
-
- return false;
-}
-
-bool Def::addEntry( FullModelChecker * m, Node c, Node v) {
+bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {
if (!d_et.hasGeneralization(m, c)) {
int newIndex = (int)d_cond.size();
if (!d_has_simplified) {
@@ -139,7 +143,7 @@ bool Def::addEntry( FullModelChecker * m, Node c, Node v) { }
}
-Node Def::evaluate( FullModelChecker * m, std::vector<Node>& inst ) {
+Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
int gindex = d_et.getGeneralizationIndex(m, inst);
if (gindex!=-1) {
return d_value[gindex];
@@ -148,11 +152,11 @@ Node Def::evaluate( FullModelChecker * m, std::vector<Node>& inst ) { }
}
-int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst ) {
+int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
return d_et.getGeneralizationIndex(m, inst);
}
-void Def::simplify(FullModelChecker * m) {
+void Def::simplify(FirstOrderModelFmc * m) {
d_has_simplified = true;
std::vector< Node > cond;
cond.insert( cond.end(), d_cond.begin(), d_cond.end() );
@@ -186,16 +190,128 @@ 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; i<args.size(); i++) {
+ args[i] = getUsedRepresentative(args[i]);
+ }
+ Assert( n.getKind()==APPLY_UF );
+ return d_models[n.getOperator()]->evaluate(this, args);
+}
+
+void FirstOrderModelFmc::processInitialize() {
+ for( std::map<Node, Def * >::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; i<type.getNumChildren()-1; i++ ){
+ std::stringstream ss;
+ ss << argPrefix << (i+1);
+ vars.push_back( NodeManager::currentNM()->mkBoundVar( 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; j<cond.getNumChildren(); j++) {
+ if (!isStar(cond[j])){
+ Node c = getUsedRepresentative( cond[j] );
+ children.push_back( NodeManager::currentNM()->mkNode( 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);
d_false = NodeManager::currentNM()->mkConst(false);
}
-
void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
d_addedLemmas = 0;
- FirstOrderModel* fm = (FirstOrderModel*)m;
+ FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
if( fullModel ){
//make function values
for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
@@ -204,15 +320,13 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ TheoryEngineModelBuilder::processBuildModel( m, fullModel );
//mark that the model has been set
fm->markModelSet();
+ //debug the model
+ debugModel( fm );
}else{
Trace("fmc") << "---Full Model Check reset() " << std::endl;
- for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
- it->second->reset();
- }
+ fm->initialize( d_considerAxioms );
d_quant_models.clear();
- d_models_init.clear();
d_rep_ids.clear();
- d_model_basis_rep.clear();
d_star_insts.clear();
//process representatives
for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
@@ -220,13 +334,11 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ if( it->first.isSort() ){
Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);
- Node rmbt = fm->getRepresentative(mbt);
+ Node rmbt = fm->getUsedRepresentative( mbt);
int mbt_index = -1;
Trace("fmc") << " Model basis term : " << mbt << std::endl;
for( size_t a=0; a<it->second.size(); a++ ){
- //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] );
- //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 );
- Node r = fm->getRepresentative( it->second[a] );
+ Node r = fm->getUsedRepresentative( it->second[a] );
std::vector< Node > eqc;
((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt);
@@ -241,7 +353,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ //if this is the model basis eqc, replace with actual model basis term
if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {
- d_model_basis_rep[it->first] = r;
+ fm->d_model_basis_rep[it->first] = r;
r = mbt;
mbt_index = a;
}
@@ -257,150 +369,63 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ }
}
}
- }
-}
-
-Node FullModelChecker::getRepresentative(FirstOrderModel * fm, Node n) {
- //Assert( fm->hasTerm(n) );
- TypeNode tn = n.getType();
- if( tn.isBoolean() ){
- return fm->areEqual(n, d_true) ? d_true : d_false;
- }else{
- Node r = fm->getRepresentative(n);
- if (r==d_model_basis_rep[tn]) {
- r = d_qe->getTermDatabase()->getModelBasisTerm(tn);
- }
- return r;
- }
-}
-
-struct ModelBasisArgSort
-{
- std::vector< Node > d_terms;
- bool operator() (int i,int j) {
- return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <
- d_terms[j].getAttribute(ModelBasisArgAttribute()) );
- }
-};
-
-void FullModelChecker::addEntry( FirstOrderModel * fm, Node op, Node c, Node v,
- std::vector< Node > & conds,
- std::vector< Node > & values,
- std::vector< Node > & entry_conds ) {
- 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 = getRepresentative(fm, c[i]);
- children.push_back(ri);
- if (isModelBasisTerm(ri)) {
- ri = getStar( ri.getType() );
- }else{
- hasNonStar = true;
- }
- entry_children.push_back(ri);
- }
- Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
- Node nv = getRepresentative(fm, v);
- 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);
- }
-}
-
-Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) {
- if( d_models_init.find(op)==d_models_init.end() ){
- if( d_models.find(op)==d_models.end() ){
- d_models[op] = new Def;
- }
- //reset the model
- d_models[op]->reset();
-
- std::vector< Node > conds;
- std::vector< Node > values;
- std::vector< Node > entry_conds;
- Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
- Node r = getRepresentative(fm, fm->d_uf_terms[op][i]);
- Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;
- }
- Trace("fmc-model-debug") << std::endl;
- //initialize the model
- /*
- for( int j=0; j<2; j++ ){
- for( int k=1; k>=0; k-- ){
- Trace("fmc-model-debug")<< "Set values " << j << " " << k << " : " << std::endl;
- for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[j][k].begin();
- it != fm->d_uf_model_gen[op].d_set_values[j][k].end(); ++it ){
- Trace("fmc-model-debug") << " process : " << it->first << " -> " << it->second << std::endl;
- if( j==1 ){
- addEntry(fm, op, it->first, it->second, conds, values, entry_conds);
- }
+ //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 > conds;
+ std::vector< Node > values;
+ std::vector< Node > entry_conds;
+ Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+ Node r = fm->getUsedRepresentative(fm->d_uf_terms[op][i]);
+ Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;
+ }
+ Trace("fmc-model-debug") << std::endl;
+ //initialize the model
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+ Node n = fm->d_uf_terms[op][i];
+ if( !n.getAttribute(NoMatchAttribute()) ){
+ addEntry(fm, op, n, n, conds, values, entry_conds);
}
}
- }
- */
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
- Node n = fm->d_uf_terms[op][i];
- if( !n.getAttribute(NoMatchAttribute()) ){
- addEntry(fm, op, n, n, conds, values, entry_conds);
+ Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+ //add default value
+ if( fm->hasTerm( nmb ) ){
+ 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());
+ 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);
}
- }
- Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
- //add default value
- if( fm->hasTerm( nmb ) ){
- Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
- addEntry(fm, op, nmb, nmb, conds, values, entry_conds);
- }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;
- addEntry(fm, op, nmb, vmb, conds, values, entry_conds);
- }
-
- //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++) {
- d_models[op]->addEntry(this, entry_conds[indices[i]], values[indices[i]]);
- }
- d_models[op]->debugPrint("fmc-model", op, this);
- Trace("fmc-model") << std::endl;
- d_models[op]->simplify( this );
- Trace("fmc-model-simplify") << "After simplification : " << std::endl;
- d_models[op]->debugPrint("fmc-model-simplify", op, this);
- Trace("fmc-model-simplify") << std::endl;
+ for (int i=0; i<(int)indices.size(); i++) {
+ fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
+ }
+ fm->d_models[op]->debugPrint("fmc-model", op, this);
+ Trace("fmc-model") << std::endl;
- d_models_init[op] = true;
+ fm->d_models[op]->simplify( fm );
+ Trace("fmc-model-simplify") << "After simplification : " << std::endl;
+ fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
+ Trace("fmc-model-simplify") << std::endl;
+ }
}
- return d_models[op];
-}
-
-
-bool FullModelChecker::isStar(Node n) {
- return n==getStar(n.getType());
-}
-
-bool FullModelChecker::isModelBasisTerm(Node n) {
- return n==getModelBasisTerm(n.getType());
-}
-
-Node FullModelChecker::getModelBasisTerm(TypeNode tn) {
- return d_qe->getTermDatabase()->getModelBasisTerm(tn);
}
void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {
@@ -413,10 +438,11 @@ void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) { }
void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
+ FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel();
if( n.isNull() ){
Trace(tr) << "null";
}
- else if(isStar(n) && dispStar) {
+ else if(fm->isStar(n) && dispStar) {
Trace(tr) << "*";
}else{
TypeNode tn = n.getType();
@@ -438,6 +464,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, if (!options::fmfModelBasedInst()) {
return false;
}else{
+ FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();
if (effort==0) {
//register the quantifier
if (d_quant_cond.find(f)==d_quant_cond.end()) {
@@ -452,7 +479,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, }
//model check the quantifier
- doCheck(fm, f, d_quant_models[f], f[1]);
+ doCheck(fmfmc, f, d_quant_models[f], f[1]);
Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
d_quant_models[f].debugPrint("fmc", Node::null(), this);
Trace("fmc") << std::endl;
@@ -463,9 +490,9 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, bool hasStar = false;
std::vector< Node > inst;
for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {
- if (isStar(d_quant_models[f].d_cond[i][j])) {
+ if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {
hasStar = true;
- inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
+ inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
}else{
inst.push_back(d_quant_models[f].d_cond[i][j]);
}
@@ -473,14 +500,14 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, bool addInst = true;
if( hasStar ){
//try obvious (specified by inst)
- Node ev = d_quant_models[f].evaluate(this, inst);
+ Node ev = d_quant_models[f].evaluate(fmfmc, inst);
if (ev==d_true) {
addInst = false;
}
}else{
//for debugging
if (Trace.isOn("fmc-test-inst")) {
- Node ev = d_quant_models[f].evaluate(this, inst);
+ Node ev = d_quant_models[f].evaluate(fmfmc, inst);
if( ev==d_true ){
std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;
exit(0);
@@ -518,8 +545,8 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, for( int i=(d_star_insts[f].size()-1); i>=0; i--) {
//get witness for d_star_insts[f][i]
int j = d_star_insts[f][i];
- if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
- int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );
+ if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
+ int lem = exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j );
if( lem==-1 ){
//something went wrong, resort to exhaustive instantiation
return false;
@@ -534,7 +561,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, }
}
-int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {
+int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {
int addedLemmas = 0;
RepSetIterator riter( d_qe, &(fm->d_rep_set) );
Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
@@ -546,7 +573,7 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c TypeNode tn = c[i].getType();
if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
//RepDomain rd;
- if( isStar(c[i]) ){
+ if( fm->isStar(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 ){
@@ -573,13 +600,13 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c std::vector< Node > inst;
for( int i=0; i<riter.getNumTerms(); i++ ){
//m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
- Node r = getRepresentative( fm, riter.getTerm( i ) );
+ Node r = fm->getUsedRepresentative( riter.getTerm( i ) );
debugPrint("fmc-exh-debug", r);
Trace("fmc-exh-debug") << " ";
inst.push_back(r);
}
- int ev_index = d_quant_models[f].getGeneralizationIndex(this, inst);
+ int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);
Trace("fmc-exh-debug") << ", index = " << ev_index;
Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
if (ev!=d_true) {
@@ -600,19 +627,19 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c return addedLemmas;
}
-void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) {
+void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {
Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;
if( n.getKind() == kind::BOUND_VARIABLE ){
- d.addEntry(this, mkCondDefault(f), 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 = getSomeDomainElement( fm, n.getType() );
+ r = fm->getSomeDomainElement(n.getType() );
}
- r = getRepresentative(fm, r);
- d.addEntry(this, mkCondDefault(f), r);
+ r = fm->getUsedRepresentative( r);
+ d.addEntry(fm, mkCondDefault(fm, f), r);
}
else if( n.getKind() == kind::NOT ){
//just do directly
@@ -620,7 +647,7 @@ void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) { doNegate( d );
}
else if( n.getKind() == kind::FORALL ){
- d.addEntry(this, mkCondDefault(f), Node::null());
+ d.addEntry(fm, mkCondDefault(fm, f), Node::null());
}
else{
std::vector< int > var_ch;
@@ -655,13 +682,13 @@ void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) { }else{
Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;
std::vector< Node > cond;
- mkCondDefaultVec(f, cond);
+ mkCondDefaultVec(fm, f, cond);
std::vector< Node > val;
//interpreted compose
doInterpretedCompose( fm, f, d, n, children, 0, cond, val );
}
}
- d.simplify(this);
+ d.simplify(fm);
}
Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;
d.debugPrint("fmc-debug", Node::null(), this);
@@ -676,62 +703,61 @@ void FullModelChecker::doNegate( Def & dc ) { }
}
-void FullModelChecker::doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq ) {
+void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ) {
std::vector<Node> cond;
- mkCondDefaultVec(f, cond);
+ mkCondDefaultVec(fm, f, cond);
if (eq[0]==eq[1]){
- d.addEntry(this, mkCond(cond), d_true);
+ d.addEntry(fm, mkCond(cond), d_true);
}else{
int j = getVariableId(f, eq[0]);
int k = getVariableId(f, eq[1]);
TypeNode tn = eq[0].getType();
if( !fm->d_rep_set.hasType( tn ) ){
- getSomeDomainElement( fm, tn ); //to verify the type is initialized
+ fm->getSomeDomainElement( tn ); //to verify the type is initialized
}
for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {
- Node r = getRepresentative( fm, fm->d_rep_set.d_type_reps[tn][i] );
+ Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );
cond[j+1] = r;
cond[k+1] = r;
- d.addEntry( this, mkCond(cond), d_true);
+ d.addEntry( fm, mkCond(cond), d_true);
}
- d.addEntry(this, mkCondDefault(f), d_false);
+ d.addEntry( fm, mkCondDefault(fm, f), d_false);
}
}
-void FullModelChecker::doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v) {
+void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) {
int j = getVariableId(f, v);
for (unsigned i=0; i<dc.d_cond.size(); i++) {
Node val = dc.d_value[i];
if( dc.d_cond[i][j]!=val ){
- if (isStar(dc.d_cond[i][j])) {
+ if (fm->isStar(dc.d_cond[i][j])) {
std::vector<Node> cond;
mkCondVec(dc.d_cond[i],cond);
cond[j+1] = val;
- d.addEntry(this, mkCond(cond), d_true);
- cond[j+1] = getStar(val.getType());
- d.addEntry(this, mkCond(cond), d_false);
+ d.addEntry(fm, mkCond(cond), d_true);
+ cond[j+1] = fm->getStar(val.getType());
+ d.addEntry(fm, mkCond(cond), d_false);
}else{
- d.addEntry( this, dc.d_cond[i], d_false);
+ d.addEntry( fm, dc.d_cond[i], d_false);
}
}else{
- d.addEntry( this, dc.d_cond[i], d_true);
+ d.addEntry( fm, dc.d_cond[i], d_true);
}
}
}
-void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {
- getModel(fm, op);
+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {
Trace("fmc-uf-debug") << "Definition : " << std::endl;
- d_models[op]->debugPrint("fmc-uf-debug", op, this);
+ fm->d_models[op]->debugPrint("fmc-uf-debug", op, this);
Trace("fmc-uf-debug") << std::endl;
std::vector< Node > cond;
- mkCondDefaultVec(f, cond);
+ mkCondDefaultVec(fm, f, cond);
std::vector< Node > val;
doUninterpretedCompose( fm, f, op, d, dc, 0, cond, val);
}
-void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,
+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,
std::vector< Def > & dc, int index,
std::vector< Node > & cond, std::vector<Node> & val ) {
Trace("fmc-uf-process") << "process at " << index << std::endl;
@@ -743,19 +769,19 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Nod if (index==(int)dc.size()) {
//we have an entry, now do actual compose
std::map< int, Node > entries;
- doUninterpretedCompose2( fm, f, entries, 0, cond, val, d_models[op]->d_et);
+ doUninterpretedCompose2( fm, f, entries, 0, cond, val, fm->d_models[op]->d_et);
//add them to the definition
- for( unsigned e=0; e<d_models[op]->d_cond.size(); e++ ){
+ for( unsigned e=0; e<fm->d_models[op]->d_cond.size(); e++ ){
if ( entries.find(e)!=entries.end() ){
- d.addEntry(this, entries[e], d_models[op]->d_value[e] );
+ d.addEntry(fm, entries[e], fm->d_models[op]->d_value[e] );
}
}
}else{
for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
- if (isCompat(cond, dc[index].d_cond[i])!=0) {
+ if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {
std::vector< Node > new_cond;
new_cond.insert(new_cond.end(), cond.begin(), cond.end());
- if( doMeet(new_cond, dc[index].d_cond[i]) ){
+ if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){
Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;
val.push_back(dc[index].d_value[i]);
doUninterpretedCompose(fm, f, op, d, dc, index+1, new_cond, val);
@@ -768,7 +794,7 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Nod }
}
-void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f,
+void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
std::map< int, Node > & entries, int index,
std::vector< Node > & cond, std::vector< Node > & val,
EntryTrie & curr ) {
@@ -788,7 +814,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f, if( v.getKind()==kind::BOUND_VARIABLE ){
int j = getVariableId(f, v);
Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
- if (!isStar(cond[j+1])) {
+ if (!fm->isStar(cond[j+1])) {
v = cond[j+1];
}else{
bind_var = true;
@@ -801,13 +827,13 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f, cond[j+1] = it->first;
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
}
- cond[j+1] = getStar(v.getType());
+ 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 = getStar(v.getType());
+ 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]);
@@ -816,28 +842,28 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f, }
}
-void FullModelChecker::doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,
+void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,
std::vector< Def > & dc, int index,
std::vector< Node > & cond, std::vector<Node> & val ) {
if ( index==(int)dc.size() ){
Node c = mkCond(cond);
Node v = evaluateInterpreted(n, val);
- d.addEntry(this, c, v);
+ d.addEntry(fm, c, v);
}
else {
TypeNode vtn = n.getType();
for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
- if (isCompat(cond, dc[index].d_cond[i])!=0) {
+ if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {
std::vector< Node > new_cond;
new_cond.insert(new_cond.end(), cond.begin(), cond.end());
- if( doMeet(new_cond, dc[index].d_cond[i]) ){
+ if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){
bool process = true;
if (vtn.isBoolean()) {
//short circuit
if( (n.getKind()==OR && dc[index].d_value[i]==d_true) ||
(n.getKind()==AND && dc[index].d_value[i]==d_false) ){
Node c = mkCond(new_cond);
- d.addEntry(this, c, dc[index].d_value[i]);
+ d.addEntry(fm, c, dc[index].d_value[i]);
process = false;
}
}
@@ -852,23 +878,23 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModel * fm, Node f, Def & }
}
-int FullModelChecker::isCompat( std::vector< Node > & cond, Node c ) {
+int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
Assert(cond.size()==c.getNumChildren()+1);
for (unsigned i=1; i<cond.size(); i++) {
- if( cond[i]!=c[i-1] && !isStar(cond[i]) && !isStar(c[i-1]) ) {
+ if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {
return 0;
}
}
return 1;
}
-bool FullModelChecker::doMeet( std::vector< Node > & cond, Node c ) {
+bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
Assert(cond.size()==c.getNumChildren()+1);
for (unsigned i=1; i<cond.size(); i++) {
if( cond[i]!=c[i-1] ) {
- if( isStar(cond[i]) ){
+ if( fm->isStar(cond[i]) ){
cond[i] = c[i-1];
- }else if( !isStar(c[i-1]) ){
+ }else if( !fm->isStar(c[i-1]) ){
return false;
}
}
@@ -880,38 +906,17 @@ Node FullModelChecker::mkCond( std::vector< Node > & cond ) { return NodeManager::currentNM()->mkNode(APPLY_UF, cond);
}
-Node FullModelChecker::mkCondDefault( Node f) {
+Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {
std::vector< Node > cond;
- mkCondDefaultVec(f, cond);
+ mkCondDefaultVec(fm, f, cond);
return mkCond(cond);
}
-Node FullModelChecker::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];
-}
-
-Node FullModelChecker::getSomeDomainElement(FirstOrderModel * fm, TypeNode tn){
- //check if there is even any domain elements at all
- if (!fm->d_rep_set.hasType(tn)) {
- Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
- Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
- fm->d_rep_set.d_type_reps[tn].push_back(mbt);
- }else if( fm->d_rep_set.d_type_reps[tn].size()==0 ){
- Message() << "empty reps" << std::endl;
- exit(0);
- }
- return fm->d_rep_set.d_type_reps[tn][0];
-}
-
-void FullModelChecker::mkCondDefaultVec( Node f, std::vector< Node > & cond ) {
+void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {
//get function symbol for f
cond.push_back(d_quant_cond[f]);
for (unsigned i=0; i<f[0].getNumChildren(); i++) {
- Node ts = getStar( f[0][i].getType() );
+ Node ts = fm->getStar( f[0][i].getType() );
cond.push_back(ts);
}
}
@@ -964,56 +969,42 @@ Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) }
}
-bool FullModelChecker::useSimpleModels() {
- return options::fmfFullModelCheckSimple();
+Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) {
+ return fm->getFunctionValue(op, argPrefix);
}
-Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix ) {
- getModel( fm, op );
- TypeNode type = op.getType();
- std::vector< Node > vars;
- for( size_t i=0; i<type.getNumChildren()-1; i++ ){
- std::stringstream ss;
- ss << argPrefix << (i+1);
- vars.push_back( NodeManager::currentNM()->mkBoundVar( 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 = fm->getRepresentative( d_models[op]->d_value[i] );
- if( curr.isNull() ){
- curr = v;
+
+
+void FullModelChecker::addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,
+ std::vector< Node > & conds,
+ std::vector< Node > & values,
+ std::vector< Node > & entry_conds ) {
+ 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);
+ if (fm->isModelBasisTerm(ri)) {
+ ri = fm->getStar( ri.getType() );
}else{
- //make the condition
- Node cond = d_models[op]->d_cond[i];
- std::vector< Node > children;
- for( unsigned j=0; j<cond.getNumChildren(); j++) {
- if (!isStar(cond[j])){
- Node c = fm->getRepresentative( cond[j] );
- children.push_back( NodeManager::currentNM()->mkNode( 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 );
+ hasNonStar = true;
}
+ entry_children.push_back(ri);
+ }
+ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+ Node nv = fm->getUsedRepresentative( v);
+ 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);
}
- curr = Rewriter::rewrite( curr );
- return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
}
-Node FullModelChecker::getCurrentUfModelValue( FirstOrderModel* fm, 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++) {
- args[i] = getRepresentative(fm, args[i]);
- }
- if( n.getKind()==VARIABLE ){
- Node r = getRepresentative(fm, n);
- return r;
- }else if( n.getKind()==APPLY_UF ){
- getModel(fm, n.getOperator());
- return d_models[n.getOperator()]->evaluate(this, args);
- }else{
- return Node::null();
- }
-}
\ No newline at end of file +bool FullModelChecker::useSimpleModels() {
+ return options::fmfFullModelCheckSimple();
+}
|