diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-08 20:02:10 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-08 20:02:22 -0500 |
| commit | 85377f73a331b334437aa0d50d15c81e905869c1 (patch) | |
| tree | bb98f8ec511f9314731fe4545b6e9b8f64d18b33 /src/theory/quantifiers/full_model_check.cpp | |
| parent | 75d3b086d2cbcb4508446e405e0599788a3a25a5 (diff) | |
Add new method for checking candidate models, --fmf-fmc. Add infrastructure for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp). Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model. Add option for relational triggers such as x = f(y), --relational-trigger.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
| -rwxr-xr-x | src/theory/quantifiers/full_model_check.cpp | 943 |
1 files changed, 943 insertions, 0 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp new file mode 100755 index 000000000..efd193fc5 --- /dev/null +++ b/src/theory/quantifiers/full_model_check.cpp @@ -0,0 +1,943 @@ +
+/********************* */
+/*! \file full_model_check.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of full model check class
+ **/
+
+#include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/options.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::theory::inst;
+using namespace CVC4::theory::quantifiers::fmcheck;
+
+
+bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) {
+ if (index==(int)c.getNumChildren()) {
+ return d_data!=-1;
+ }else{
+ Node st = m->getStar(c[index].getType());
+ if(d_child.find(st)!=d_child.end()) {
+ if( d_child[st].hasGeneralization(m, c, index+1) ){
+ return true;
+ }
+ }
+ if( d_child.find( c[index] )!=d_child.end() ){
+ if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
+int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index ) {
+ if (index==(int)inst.size()) {
+ return d_data;
+ }else{
+ int minIndex = -1;
+ Node st = m->getStar(inst[index].getType());
+ if(d_child.find(st)!=d_child.end()) {
+ minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);
+ }
+ Node cc = inst[index];
+ if( d_child.find( cc )!=d_child.end() ){
+ int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);
+ if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){
+ minIndex = gindex;
+ }
+ }
+ return minIndex;
+ }
+}
+
+void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int index ) {
+ if (index==(int)c.getNumChildren()) {
+ if(d_data==-1) {
+ d_data = data;
+ }
+ }
+ else {
+ d_child[ c[index] ].addEntry(m,c,v,data,index+1);
+ }
+}
+
+void EntryTrie::getEntries( FullModelChecker * 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 ){
+ gen.push_back(d_data);
+ }
+ compat.push_back(d_data);
+ }
+ }else{
+ if (m->isStar(c[index])) {
+ for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
+ it->second.getEntries(m, c, compat, gen, index+1, is_gen );
+ }
+ }else{
+ Node st = m->getStar(c[index].getType());
+ if(d_child.find(st)!=d_child.end()) {
+ d_child[st].getEntries(m, c, compat, gen, index+1, false);
+ }
+ if( d_child.find( c[index] )!=d_child.end() ){
+ d_child[ c[index] ].getEntries(m, c, compat, gen, index+1, is_gen);
+ }
+ }
+
+ }
+}
+
+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) {
+ if (!d_et.hasGeneralization(m, c)) {
+ int newIndex = (int)d_cond.size();
+ if (!d_has_simplified) {
+ std::vector<int> compat;
+ std::vector<int> gen;
+ d_et.getEntries(m, c, compat, gen);
+ for( unsigned i=0; i<compat.size(); i++) {
+ if( d_status[compat[i]]==status_unk ){
+ if( d_value[compat[i]]!=v ){
+ d_status[compat[i]] = status_non_redundant;
+ }
+ }
+ }
+ for( unsigned i=0; i<gen.size(); i++) {
+ if( d_status[gen[i]]==status_unk ){
+ if( d_value[gen[i]]==v ){
+ d_status[gen[i]] = status_redundant;
+ }
+ }
+ }
+ d_status.push_back( status_unk );
+ }
+ d_et.addEntry(m, c, v, newIndex);
+ d_cond.push_back(c);
+ d_value.push_back(v);
+ return true;
+ }else{
+ return false;
+ }
+}
+
+Node Def::evaluate( FullModelChecker * m, std::vector<Node> inst ) {
+ int gindex = d_et.getGeneralizationIndex(m, inst);
+ if (gindex!=-1) {
+ return d_value[gindex];
+ }else{
+ return Node::null();
+ }
+}
+
+int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst ) {
+ return d_et.getGeneralizationIndex(m, inst);
+}
+
+void Def::simplify(FullModelChecker * m) {
+ d_has_simplified = true;
+ std::vector< Node > cond;
+ cond.insert( cond.end(), d_cond.begin(), d_cond.end() );
+ d_cond.clear();
+ std::vector< Node > value;
+ value.insert( value.end(), d_value.begin(), d_value.end() );
+ d_value.clear();
+ d_et.reset();
+ for (unsigned i=0; i<d_status.size(); i++) {
+ if( d_status[i]!=status_redundant ){
+ addEntry(m, d_cond[i], d_value[i]);
+ }
+ }
+ d_status.clear();
+}
+
+void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
+ if (!op.isNull()) {
+ Trace(tr) << "Model for " << op << " : " << std::endl;
+ }
+ for( unsigned i=0; i<d_cond.size(); i++) {
+ //print the condition
+ if (!op.isNull()) {
+ Trace(tr) << op;
+ }
+ m->debugPrintCond(tr, d_cond[i], true);
+ Trace(tr) << " -> ";
+ m->debugPrint(tr, d_value[i]);
+ Trace(tr) << std::endl;
+ }
+}
+
+
+FullModelChecker::FullModelChecker(QuantifiersEngine* qe) : d_qe(qe){
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+void FullModelChecker::reset(FirstOrderModel * fm) {
+ 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();
+ }
+ 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();
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){
+ if( it->first.isSort() ){
+ if( d_type_star.find(it->first)==d_type_star.end() ){
+ Node st = NodeManager::currentNM()->mkSkolem( "star_$$", it->first, "skolem created for full-model checking" );
+ d_type_star[it->first] = st;
+ }
+ Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+ Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);
+ Node rmbt = fm->getRepresentative(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] );
+ std::vector< Node > eqc;
+ ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
+ Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt);
+ Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
+ //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
+ Trace("fmc-model-debug") << " {";
+ //find best selection for representative
+ for( size_t i=0; i<eqc.size(); i++ ){
+ Trace("fmc-model-debug") << eqc[i] << ", ";
+ }
+ Trace("fmc-model-debug") << "}" << std::endl;
+
+ //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;
+ r = mbt;
+ mbt_index = a;
+ }
+ d_rep_ids[it->first][r] = (int)a;
+ }
+ Trace("fmc-model-debug") << std::endl;
+
+ if (mbt_index==-1) {
+ std::cout << " WARNING: model basis term is not a representative!" << std::endl;
+ exit(0);
+ }else{
+ Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;
+ }
+ }
+ }
+}
+
+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 = d_type_star[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;
+ //make sure star's are defined
+ TypeNode tn = op.getType();
+ for(unsigned i=0; i<tn.getNumChildren()-1; i++) {
+ if( d_type_star.find(tn[i])==d_type_star.end() ){
+ Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn[i], "skolem created for full-model checking" );
+ d_type_star[tn[i]] = st;
+ }
+ }
+ }
+ //reset the model
+ d_models[op]->reset();
+
+ std::vector< Node > conds;
+ std::vector< Node > values;
+ std::vector< Node > entry_conds;
+ Trace("fmc-model-debug") << "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);
+ }
+ }
+ }
+ }
+ //add for default value
+ if (!fm->d_uf_model_gen[op].d_default_value.isNull()) {
+ Node n = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+ addEntry(fm, op, n, fm->d_uf_model_gen[op].d_default_value, conds, values, entry_conds);
+ }
+
+ //find other default values (TODO: figure out why these entries are added to d_uf_model_gen)
+ if( conds.empty() ){
+ //for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[1][0].begin();
+ // it != fm->d_uf_model_gen[op].d_set_values[1][0].end(); ++it ){
+ // Trace("fmc-model-debug") << " process : " << it->first << " -> " << it->second << std::endl;
+ // addEntry(fm, op, it->first, it->second, conds, values, entry_conds);
+ //}
+ Trace("fmc-warn") << "WARNING: No entries for " << op << ", make default entry." << std::endl;
+ //choose a complete arbitrary term
+ Node n = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+ TypeNode tn = n.getType();
+ Node v = fm->d_rep_set.d_type_reps[tn][0];
+ addEntry(fm, op, n, v, 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 );
+
+
+ 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;
+
+ d_models_init[op] = true;
+ }
+ return d_models[op];
+}
+
+
+bool FullModelChecker::isStar(Node n) {
+ return n==d_type_star[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) {
+ Trace(tr) << "(";
+ for( unsigned j=0; j<n.getNumChildren(); j++) {
+ if( j>0 ) Trace(tr) << ", ";
+ debugPrint(tr, n[j], dispStar);
+ }
+ Trace(tr) << ")";
+}
+
+void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
+ if( n.isNull() ){
+ Trace(tr) << "null";
+ }
+ else if(isStar(n) && dispStar) {
+ Trace(tr) << "*";
+ }else{
+ TypeNode tn = n.getType();
+ if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
+ if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) {
+ Trace(tr) << d_rep_ids[tn][n];
+ }else{
+ Trace(tr) << n;
+ }
+ }else{
+ Trace(tr) << n;
+ }
+ }
+}
+
+
+int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, int effort) {
+ int addedLemmas = 0;
+ Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
+ if (effort==0) {
+ //register the quantifier
+ if (d_quant_cond.find(f)==d_quant_cond.end()) {
+ std::vector< TypeNode > types;
+ for(unsigned i=0; i<f[0].getNumChildren(); i++){
+ types.push_back(f[0][i].getType());
+ d_quant_var_id[f][f[0][i]] = i;
+ }
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );
+ Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );
+ d_quant_cond[f] = op;
+ }
+
+ //model check the quantifier
+ doCheck(fm, 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;
+ //consider all entries going to false
+ for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {
+ if( d_quant_models[f].d_value[i]!=d_true) {
+ Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
+ 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])) {
+ hasStar = true;
+ inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
+ }else{
+ inst.push_back(d_quant_models[f].d_cond[i][j]);
+ }
+ }
+ bool addInst = true;
+ if( hasStar ){
+ //try obvious (specified by inst)
+ Node ev = d_quant_models[f].evaluate(this, 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);
+ if( ev==d_true ){
+ std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;
+ exit(0);
+ }else{
+ Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;
+ }
+ }
+ }
+ if( addInst ){
+ InstMatch m;
+ for( unsigned j=0; j<inst.size(); j++) {
+ m.set( d_qe, f, j, inst[j] );
+ }
+ if (isActive()) {
+ if( d_qe->addInstantiation( f, m ) ){
+ addedLemmas++;
+ }else{
+ //this can happen if evaluation is unknown
+ //might try it next effort level
+ d_star_insts[f].push_back(i);
+ }
+ }
+ }else{
+ //might try it next effort level
+ d_star_insts[f].push_back(i);
+ }
+ }
+ }
+ }else{
+ //TODO
+ Trace("fmc-exh") << "Definition was : " << std::endl;
+ d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);
+ Trace("fmc-exh") << std::endl;
+ Def temp;
+ //simplify the exceptions?
+ 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( lem==-1 ){
+ return -1;
+ }else{
+ addedLemmas += lem;
+ }
+ }
+ }
+ }
+ return addedLemmas;
+}
+
+int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {
+ int addedLemmas = 0;
+ RepSetIterator riter( &(fm->d_rep_set) );
+ Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
+ debugPrintCond("fmc-exh", c, true);
+ Trace("fmc-exh")<< std::endl;
+ if( riter.setQuantifier( f ) ){
+ std::vector< RepDomain > dom;
+ for (unsigned i=0; i<c.getNumChildren(); i++) {
+ TypeNode tn = c[i].getType();
+ if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
+ RepDomain rd;
+ if( 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 ){
+ 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]]);
+ }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 : ";
+ 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 ) );
+ debugPrint("fmc-exh-debug", r);
+ Trace("fmc-exh-debug") << " ";
+ inst.push_back(r);
+ }
+
+ int ev_index = d_quant_models[f].getGeneralizationIndex(this, 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) {
+ InstMatch m;
+ for( int i=0; i<riter.getNumTerms(); i++ ){
+ m.set( d_qe, f, i, riter.getTerm( i ) );
+ }
+ Trace("fmc-exh-debug") << ", add!";
+ //add as instantiation
+ if( d_qe->addInstantiation( f, m ) ){
+ addedLemmas++;
+ }
+ }
+ Trace("fmc-exh-debug") << std::endl;
+ riter.increment();
+ }
+ }
+ return addedLemmas;
+}
+
+void FullModelChecker::doCheck(FirstOrderModel * 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);
+ }
+ else if( n.getNumChildren()==0 ){
+ Node r = n;
+ if( !fm->hasTerm(n) ){
+ if (fm->d_rep_set.hasType(n.getType())) {
+ r = fm->d_rep_set.d_type_reps[n.getType()][0];
+ }else{
+ //should never happen?
+ }
+ }
+ r = getRepresentative(fm, r);
+ d.addEntry(this, mkCondDefault(f), r);
+ }
+ else if( n.getKind() == kind::NOT ){
+ //just do directly
+ doCheck( fm, f, d, n[0] );
+ doNegate( d );
+ }
+ else if( n.getKind() == kind::FORALL ){
+ d.addEntry(this, mkCondDefault(f), Node::null());
+ }
+ else{
+ std::vector< int > var_ch;
+ std::vector< Def > children;
+ for( int i=0; i<(int)n.getNumChildren(); i++) {
+ Def dc;
+ doCheck(fm, f, dc, n[i]);
+ children.push_back(dc);
+ if( n[i].getKind() == kind::BOUND_VARIABLE ){
+ var_ch.push_back(i);
+ }
+ }
+
+ if( n.getKind()==APPLY_UF ){
+ Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl;
+ //uninterpreted compose
+ doUninterpretedCompose( fm, f, d, n.getOperator(), children );
+ } else {
+ if( !var_ch.empty() ){
+ if( n.getKind()==EQUAL ){
+ if( var_ch.size()==2 ){
+ Trace("fmc-debug") << "Do variable equality " << n << std::endl;
+ doVariableEquality( fm, f, d, n );
+ }else{
+ Trace("fmc-debug") << "Do variable relation " << n << std::endl;
+ 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);
+ }
+ }else{
+ Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;
+ std::vector< Node > cond;
+ mkCondDefaultVec(f, cond);
+ std::vector< Node > val;
+ //interpreted compose
+ doInterpretedCompose( fm, f, d, n, children, 0, cond, val );
+ }
+ }
+ d.simplify(this);
+ }
+ Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;
+ d.debugPrint("fmc-debug", Node::null(), this);
+ Trace("fmc-debug") << std::endl;
+}
+
+void FullModelChecker::doNegate( Def & dc ) {
+ for (unsigned i=0; i<dc.d_cond.size(); i++) {
+ if (!dc.d_value[i].isNull()) {
+ dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true;
+ }
+ }
+}
+
+void FullModelChecker::doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq ) {
+ std::vector<Node> cond;
+ mkCondDefaultVec(f, cond);
+ if (eq[0]==eq[1]){
+ d.addEntry(this, mkCond(cond), d_true);
+ }else{
+ int j = getVariableId(f, eq[0]);
+ int k = getVariableId(f, eq[1]);
+ TypeNode tn = eq[0].getType();
+ 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] );
+ cond[j+1] = r;
+ cond[k+1] = r;
+ d.addEntry( this, mkCond(cond), d_true);
+ }
+ d.addEntry(this, mkCondDefault(f), d_false);
+ }
+}
+
+void FullModelChecker::doVariableRelation( FirstOrderModel * 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])) {
+ std::vector<Node> cond;
+ mkCondVec(dc.d_cond[i],cond);
+ cond[j+1] = val;
+ d.addEntry(this, mkCond(cond), d_true);
+ cond[j+1] = d_type_star[val.getType()];
+ d.addEntry(this, mkCond(cond), d_false);
+ }else{
+ d.addEntry( this, dc.d_cond[i], d_false);
+ }
+ }else{
+ d.addEntry( this, dc.d_cond[i], d_true);
+ }
+ }
+}
+
+void FullModelChecker::doUninterpretedCompose( FirstOrderModel * 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);
+ Trace("fmc-uf-debug") << std::endl;
+
+ std::vector< Node > cond;
+ mkCondDefaultVec(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,
+ std::vector< Def > & dc, int index,
+ std::vector< Node > & cond, std::vector<Node> & val ) {
+ Trace("fmc-uf-process") << "process at " << index << std::endl;
+ for( unsigned i=1; i<cond.size(); i++) {
+ debugPrint("fmc-uf-process", cond[i], true);
+ Trace("fmc-uf-process") << " ";
+ }
+ Trace("fmc-uf-process") << std::endl;
+ 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);
+ //add them to the definition
+ for( unsigned e=0; e<d_models[op]->d_cond.size(); e++ ){
+ if ( entries.find(e)!=entries.end() ){
+ d.addEntry(this, entries[e], 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) {
+ std::vector< Node > new_cond;
+ new_cond.insert(new_cond.end(), cond.begin(), cond.end());
+ if( doMeet(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);
+ val.pop_back();
+ }else{
+ Trace("fmc-uf-process") << "index " << i << " failed meet." << std::endl;
+ }
+ }
+ }
+ }
+}
+
+void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f,
+ std::map< int, Node > & entries, int index,
+ std::vector< Node > & cond, std::vector< Node > & val,
+ EntryTrie & curr ) {
+ Trace("fmc-uf-process") << "compose " << index << std::endl;
+ for( unsigned i=1; i<cond.size(); i++) {
+ debugPrint("fmc-uf-process", cond[i], true);
+ Trace("fmc-uf-process") << " ";
+ }
+ Trace("fmc-uf-process") << std::endl;
+ if (index==(int)val.size()) {
+ Node c = mkCond(cond);
+ Trace("fmc-uf-entry") << "Entry : " << c << " -> index[" << curr.d_data << "]" << std::endl;
+ entries[curr.d_data] = c;
+ }else{
+ Node v = val[index];
+ bool bind_var = false;
+ 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])) {
+ v = cond[j+1];
+ }else{
+ bind_var = true;
+ }
+ }
+ if (bind_var) {
+ Trace("fmc-uf-process") << "bind variable..." << std::endl;
+ int j = getVariableId(f, v);
+ for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
+ cond[j+1] = it->first;
+ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
+ }
+ cond[j+1] = 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 = d_type_star[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]);
+ }
+ }
+ }
+}
+
+void FullModelChecker::doInterpretedCompose( FirstOrderModel * 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);
+ }
+ 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) {
+ std::vector< Node > new_cond;
+ new_cond.insert(new_cond.end(), cond.begin(), cond.end());
+ if( doMeet(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]);
+ process = false;
+ }
+ }
+ if (process) {
+ val.push_back(dc[index].d_value[i]);
+ doInterpretedCompose(fm, f, d, n, dc, index+1, new_cond, val);
+ val.pop_back();
+ }
+ }
+ }
+ }
+ }
+}
+
+int FullModelChecker::isCompat( 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]) ) {
+ return 0;
+ }
+ }
+ return 1;
+}
+
+bool FullModelChecker::doMeet( 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]) ){
+ cond[i] = c[i-1];
+ }else if( !isStar(c[i-1]) ){
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
+Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
+ return NodeManager::currentNM()->mkNode(APPLY_UF, cond);
+}
+
+Node FullModelChecker::mkCondDefault( Node f) {
+ std::vector< Node > cond;
+ mkCondDefaultVec(f, cond);
+ return mkCond(cond);
+}
+
+void FullModelChecker::mkCondDefaultVec( 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++) {
+ cond.push_back(d_type_star[f[0][i].getType()]);
+ }
+}
+
+void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) {
+ cond.push_back(n.getOperator());
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ cond.push_back( n[i] );
+ }
+}
+
+Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {
+ if( n.getKind()==EQUAL ){
+ return vals[0]==vals[1] ? d_true : d_false;
+ }else if( n.getKind()==ITE ){
+ if( vals[0]==d_true ){
+ return vals[1];
+ }else if( vals[0]==d_false ){
+ return vals[2];
+ }else{
+ return vals[1]==vals[2] ? vals[1] : Node::null();
+ }
+ }else if( n.getKind()==AND || n.getKind()==OR ){
+ bool isNull = false;
+ for (unsigned i=0; i<vals.size(); i++) {
+ if((vals[i]==d_true && n.getKind()==OR) || (vals[i]==d_false && n.getKind()==AND)) {
+ return vals[i];
+ }else if( vals[i].isNull() ){
+ isNull = true;
+ }
+ }
+ return isNull ? Node::null() : vals[0];
+ }else{
+ std::vector<Node> children;
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ for (unsigned i=0; i<vals.size(); i++) {
+ if( vals[i].isNull() ){
+ return Node::null();
+ }else{
+ children.push_back( vals[i] );
+ }
+ }
+ Node nc = NodeManager::currentNM()->mkNode(n.getKind(), children);
+ Trace("fmc-eval") << "Evaluate " << nc << " to ";
+ nc = Rewriter::rewrite(nc);
+ Trace("fmc-eval") << nc << std::endl;
+ return nc;
+ }
+}
+
+bool FullModelChecker::isActive() {
+ return options::fmfFullModelCheck();
+}
+
+bool FullModelChecker::useSimpleModels() {
+ return options::fmfFullModelCheckSimple();
+}
|