From 85377f73a331b334437aa0d50d15c81e905869c1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 May 2013 20:02:10 -0500 Subject: [PATCH] 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. --- src/smt/smt_engine.cpp | 7 + src/theory/quantifiers/Makefile.am | 6 +- src/theory/quantifiers/bounded_integers.cpp | 98 ++ src/theory/quantifiers/bounded_integers.h | 47 + src/theory/quantifiers/full_model_check.cpp | 943 ++++++++++++++++++ src/theory/quantifiers/full_model_check.h | 150 +++ src/theory/quantifiers/inst_match.cpp | 21 +- src/theory/quantifiers/inst_match.h | 3 + .../quantifiers/inst_match_generator.cpp | 74 +- .../quantifiers/inst_strategy_e_matching.cpp | 4 + src/theory/quantifiers/model_builder.cpp | 16 +- src/theory/quantifiers/model_engine.cpp | 258 ++--- src/theory/quantifiers/model_engine.h | 6 +- src/theory/quantifiers/options | 11 +- src/theory/quantifiers/quant_util.cpp | 90 ++ src/theory/quantifiers/quant_util.h | 11 + src/theory/quantifiers/term_database.cpp | 3 +- src/theory/quantifiers/term_database.h | 5 + src/theory/quantifiers/trigger.cpp | 118 ++- src/theory/quantifiers/trigger.h | 3 +- src/theory/quantifiers_engine.cpp | 5 + src/theory/quantifiers_engine.h | 5 +- src/theory/uf/options | 2 + src/theory/uf/theory_uf_model.cpp | 19 +- src/theory/uf/theory_uf_model.h | 3 +- src/theory/uf/theory_uf_strong_solver.cpp | 46 +- 26 files changed, 1759 insertions(+), 195 deletions(-) create mode 100755 src/theory/quantifiers/bounded_integers.cpp create mode 100755 src/theory/quantifiers/bounded_integers.h create mode 100755 src/theory/quantifiers/full_model_check.cpp create mode 100755 src/theory/quantifiers/full_model_check.h diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0bfc6e634..37ab9cd48 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1018,11 +1018,18 @@ void SmtEngine::setLogicInternal() throw() { //for finite model finding if( ! options::instWhenMode.wasSetByUser()){ + //instantiate only on last call if( options::fmfInstEngine() ){ Trace("smt") << "setting inst when mode to LAST_CALL" << endl; options::instWhenMode.set( INST_WHEN_LAST_CALL ); } } + if ( ! options::fmfInstGen.wasSetByUser()) { + //if full model checking is on, disable inst-gen techniques + if( options::fmfFullModelCheck() ){ + options::fmfInstGen.set( false ); + } + } //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 7fea8cf3a..1a1413ad6 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -44,7 +44,11 @@ libquantifiers_la_SOURCES = \ inst_strategy_e_matching.h \ inst_strategy_e_matching.cpp \ inst_strategy_cbqi.h \ - inst_strategy_cbqi.cpp + inst_strategy_cbqi.cpp \ + full_model_check.h \ + full_model_check.cpp \ + bounded_integers.h \ + bounded_integers.cpp EXTRA_DIST = \ kinds \ diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp new file mode 100755 index 000000000..7af6456b6 --- /dev/null +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -0,0 +1,98 @@ +/********************* */ +/*! \file bounded_integers.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 Bounded integers module + ** + ** This class manages integer bounds for quantifiers + **/ + +#include "theory/quantifiers/bounded_integers.h" +#include "theory/quantifiers/quant_util.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + +BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe) : QuantifiersModule(qe){ + +} + +void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) { + if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){ + std::map< Node, Node > msum; + if (QuantArith::getMonomialSumLit( lit, msum )){ + Trace("bound-integers") << "Literal " << lit << " is monomial sum : " << std::endl; + for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + Trace("bound-integers") << " "; + if( !it->second.isNull() ){ + Trace("bound-integers") << it->second; + if( !it->first.isNull() ){ + Trace("bound-integers") << " * "; + } + } + if( !it->first.isNull() ){ + Trace("bound-integers") << it->first; + } + Trace("bound-integers") << std::endl; + } + Trace("bound-integers") << std::endl; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){ + Node veq; + if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){ + Trace("bound-integers") << "Isolated for " << it->first << " : " << veq << std::endl; + } + } + } + } + }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) { + std::cout << "BoundedIntegers : Bad kind for literal : " << lit << std::endl; + exit(0); + } +} + +void BoundedIntegers::process( Node f, Node n, bool pol ){ + if( (( n.getKind()==IMPLIES || n.getKind()==OR) && pol) || (n.getKind()==AND && !pol) ){ + for( unsigned i=0; i > d_lowers; + std::map< Node, std::map< Node, Node > > d_uppers; + std::map< Node, std::map< Node, bool > > d_set; + void hasFreeVar( Node f, Node n ); + void process( Node f, Node n, bool pol ); + void processLiteral( Node f, Node lit, bool pol ); +public: + BoundedIntegers( QuantifiersEngine* qe ); + + void check( Theory::Effort e ); + void registerQuantifier( Node f ); + void assertNode( Node n ); + Node getNextDecisionRequest(); +}; + +} +} +} + +#endif \ No newline at end of file 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 & 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 & compat, std::vector & 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::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 & 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 compat; + std::vector gen; + d_et.getEntries(m, c, compat, gen); + for( unsigned i=0; i 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 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; idebugPrintCond(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::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; asecond.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; isecond.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; imkNode( 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; imkSkolem( "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; id_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; j0 ) 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; imkFunctionType( 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 inst; + for (unsigned j=0; jaddInstantiation( 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::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; iaddInstantiation( 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 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; id_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 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 & val ) { + Trace("fmc-uf-process") << "process at " << index << std::endl; + for( unsigned i=1; i entries; + doUninterpretedCompose2( fm, f, entries, 0, cond, val, d_models[op]->d_et); + //add them to the definition + for( unsigned e=0; ed_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 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 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::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 & 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 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, Node c ) { + Assert(cond.size()==c.getNumChildren()+1); + for (unsigned i=1; i & 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 & cond ) { + cond.push_back(n.getOperator()); + for( unsigned i=0; i & 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 children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for (unsigned i=0; imkNode(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(); +} diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h new file mode 100755 index 000000000..3f54b0574 --- /dev/null +++ b/src/theory/quantifiers/full_model_check.h @@ -0,0 +1,150 @@ +/********************* */ +/*! \file full_model_check.h + ** \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 Full model check class + **/ + +#ifndef FULL_MODEL_CHECK +#define FULL_MODEL_CHECK + +#include "theory/quantifiers/model_builder.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { +namespace fmcheck { + + +class FullModelChecker; + +class EntryTrie +{ +public: + EntryTrie() : d_data(-1){} + std::map d_child; + int d_data; + void reset() { d_data = -1; d_child.clear(); } + void addEntry( FullModelChecker * m, Node c, Node v, int data, int index = 0 ); + bool hasGeneralization( FullModelChecker * m, Node c, int index = 0 ); + int getGeneralizationIndex( FullModelChecker * m, std::vector & inst, int index = 0 ); + void getEntries( FullModelChecker * m, Node c, std::vector & compat, std::vector & gen, int index = 0, bool is_gen = true ); + //if possible, get ground instance of c that evaluates to the entry + bool getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector & inst, int index = 0 ); +}; + + +class Def +{ +public: + EntryTrie d_et; + //cond is APPLY_UF whose arguments are returned by FullModelChecker::getRepresentative + std::vector< Node > d_cond; + //value is returned by FullModelChecker::getRepresentative + std::vector< Node > d_value; +private: + enum { + status_unk, + status_redundant, + status_non_redundant + }; + std::vector< int > d_status; + bool d_has_simplified; +public: + Def() : d_has_simplified(false){} + void reset() { + d_et.reset(); + d_cond.clear(); + d_value.clear(); + d_status.clear(); + d_has_simplified = false; + } + bool addEntry( FullModelChecker * m, Node c, Node v); + Node evaluate( FullModelChecker * m, std::vector inst ); + int getGeneralizationIndex( FullModelChecker * m, std::vector inst ); + void simplify( FullModelChecker * m ); + void debugPrint(const char * tr, Node op, FullModelChecker * m); +}; + + +class FullModelChecker +{ +private: + Node d_true; + Node d_false; + QuantifiersEngine* d_qe; + std::map > d_rep_ids; + std::map d_model_basis_rep; + std::map d_models; + std::map d_quant_models; + std::map d_models_init; + std::map d_quant_cond; + std::map d_type_star; + std::map > d_quant_var_id; + std::map > d_star_insts; + Node getRepresentative(FirstOrderModel * fm, Node n); + Node normalizeArgReps(FirstOrderModel * fm, Node op, Node n); + void addEntry( FirstOrderModel * fm, Node op, Node c, Node v, + std::vector< Node > & conds, + std::vector< Node > & values, + std::vector< Node > & entry_conds ); + int exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index); +private: + void doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ); + + void doNegate( Def & dc ); + void doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq ); + void doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v); + void doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n, std::vector< Def > & dc ); + + void doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d, + std::vector< Def > & dc, int index, + std::vector< Node > & cond, std::vector & val ); + void doUninterpretedCompose2( FirstOrderModel * fm, Node f, + std::map< int, Node > & entries, int index, + std::vector< Node > & cond, std::vector< Node > & val, + EntryTrie & curr); + + void doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n, + std::vector< Def > & dc, int index, + std::vector< Node > & cond, std::vector & val ); + int isCompat( std::vector< Node > & cond, Node c ); + bool doMeet( std::vector< Node > & cond, Node c ); + Node mkCond( std::vector< Node > & cond ); + Node mkCondDefault( Node f ); + void mkCondDefaultVec( Node f, std::vector< Node > & cond ); + void mkCondVec( Node n, std::vector< Node > & cond ); + Node evaluateInterpreted( Node n, std::vector< Node > & vals ); +public: + FullModelChecker( QuantifiersEngine* qe ); + ~FullModelChecker(){} + + int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; } + bool isStar(Node n); + Node getStar(TypeNode tn) { return d_type_star[tn]; } + bool isModelBasisTerm(Node n); + Node getModelBasisTerm(TypeNode tn); + void reset(FirstOrderModel * fm); + Def * getModel(FirstOrderModel * fm, Node op); + + void debugPrintCond(const char * tr, Node n, bool dispStar = false); + void debugPrint(const char * tr, Node n, bool dispStar = false); + + int exhaustiveInstantiate(FirstOrderModel * fm, Node f, int effort); + bool hasStarExceptions( Node f ) { return !d_star_insts[f].empty(); } + + bool isActive(); + bool useSimpleModels(); +}; + +} +} +} +} + +#endif diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index f6a0dad11..d4988f223 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -134,18 +134,27 @@ Node InstMatch::getValue( Node var ) const{ } } +Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) { + return get( qe->getTermDatabase()->getInstantiationConstant( f, i ) ); +} + void InstMatch::set(TNode var, TNode n){ Assert( !var.isNull() ); - if( !n.isNull() &&// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations - //var.getType() == n.getType() - !n.getType().isSubtypeOf( var.getType() ) ){ - Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl; - Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ; - Assert(false); + if (Trace.isOn("inst-match-warn")) { + // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations + if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){ + Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl; + Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ; + } } + Assert( n.isNull() || n.getType().isSubtypeOf( var.getType() ) ); d_map[var] = n; } +void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) { + set( qe->getTermDatabase()->getInstantiationConstant( f, i ), n ); +} + /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){ if( long(index)d_order.size()) ) ){ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 127f83c60..72447fd66 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -92,8 +92,11 @@ public: void erase(Node node){ d_map.erase(node); } /** get */ Node get( TNode var ) { return d_map[var]; } + Node get( QuantifiersEngine* qe, Node f, int i ); /** set */ void set(TNode var, TNode n); + void set( QuantifiersEngine* qe, Node f, int i, TNode n ); + /** size */ size_t size(){ return d_map.size(); } /* iterator */ std::map< Node, Node >::iterator begin(){ return d_map.begin(); }; diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index de7f2f373..105575c49 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -52,22 +52,28 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat //we want to add the children of the NOT d_match_pattern = d_pattern[0]; } - if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){ - if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){ + if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){ + if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) || + d_match_pattern[0].getKind()==INST_CONSTANT ){ Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) ); + Node mp = d_match_pattern[1]; //swap sides Node pat = d_pattern; - d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); - d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern; - if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching - d_match_pattern = d_match_pattern[1]; + if(d_match_pattern.getKind()==GEQ){ + d_pattern = NodeManager::currentNM()->mkNode( kind::GT, d_match_pattern[1], d_match_pattern[0] ); + d_pattern = d_pattern.negate(); }else{ - d_match_pattern = d_pattern[0][0]; + d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); } - }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){ + d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern; + d_match_pattern = mp; + }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) || + d_match_pattern[1].getKind()==INST_CONSTANT ){ Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) ); if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching d_match_pattern = d_match_pattern[0]; + }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){ + d_match_pattern = d_match_pattern[0]; } } } @@ -96,17 +102,23 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat //candidates will be all disequalities d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern ); } - }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){ + }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || + d_pattern.getKind()==GEQ || d_pattern.getKind()==GT || d_pattern.getKind()==NOT ){ Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); if( d_pattern.getKind()==NOT ){ - Unimplemented("Disequal generator unimplemented"); + if (d_pattern[0][1].getKind()!=INST_CONSTANT) { + Unimplemented("Disequal generator unimplemented"); + }else{ + d_eq_class = d_pattern[0][1]; + } }else{ - Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); - //we are matching only in a particular equivalence class - d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); //store the equivalence class that we will call d_cg->reset( ... ) on d_eq_class = d_pattern[1]; } + Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); + //we are matching only in a particular equivalence class + d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); + }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){ //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){ //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl; @@ -134,7 +146,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat /** get match (not modulo equality) */ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){ Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" - << m << ")" << ", " << d_children.size() << std::endl; + << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl; Assert( !d_match_pattern.isNull() ); if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){ return true; @@ -182,6 +194,36 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } } } + //for relational matching + if( !d_eq_class.isNull() && d_eq_class.getKind()==INST_CONSTANT ){ + //also must fit match to equivalence class + bool pol = d_pattern.getKind()!=NOT; + Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern; + Node t_match; + if( pol ){ + if (pat.getKind()==GT) { + Node r = NodeManager::currentNM()->mkConst( Rational(-1) ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + }else{ + t_match = t; + } + }else{ + if(pat.getKind()==EQUAL) { + Node r = NodeManager::currentNM()->mkConst( Rational(1) ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + }else if( pat.getKind()==IFF ){ + t_match = NodeManager::currentNM()->mkConst( !q->areEqual( NodeManager::currentNM()->mkConst(true), t ) ); + }else if( pat.getKind()==GEQ ){ + Node r = NodeManager::currentNM()->mkConst( Rational(1) ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + }else if( pat.getKind()==GT ){ + t_match = t; + } + } + if( !t_match.isNull() && !m.setMatch( q, d_eq_class, t_match ) ){ + success = false; + } + } if( success ){ //now, fit children into match //we will be requesting candidates for matching terms for each child @@ -286,7 +328,7 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ //we have a specific equivalence class in mind //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term //just look in equivalence class of the RHS - d_cg->reset( d_eq_class ); + d_cg->reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class ); } bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ @@ -306,7 +348,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* if( !success ){ //Debug("matching") << this << " failed, reset " << d_eq_class << std::endl; //we failed, must reset - reset( d_eq_class, qe ); + reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe ); } return success; } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 0e1266e0d..ef81d55a1 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -144,7 +144,11 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) } if( gen ){ generateTriggers( f, effort, e, status ); + if( d_auto_gen_trigger[f].empty() && f.getNumChildren()==2 ){ + Trace("no-trigger") << "Could not find trigger for " << f << std::endl; + } } + //if( e==4 ){ // d_processed_trigger.clear(); // d_quantEngine->getEqualityQuery()->setLiberal( true ); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 0b74cfc5e..059c76b21 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -192,6 +192,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { 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 ); } /* @@ -273,7 +274,7 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ } } //for calculating terms that we don't need to consider - if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ + if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())!=0 ){ if( !n.getAttribute(BasisNoMatchAttribute()) ){ //need to consider if it is not congruent modulo model basis if( !tabt.addTerm( fm, n ) ){ @@ -352,7 +353,7 @@ bool ModelEngineBuilder::isQuantifierActive( Node f ){ bool ModelEngineBuilder::isTermActive( Node n ){ return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term - ( n.getAttribute(ModelBasisArgAttribute())==1 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments + ( n.getAttribute(ModelBasisArgAttribute())!=0 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments //and is not congruent modulo model basis //to another active term } @@ -597,7 +598,7 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) fm->d_uf_model_gen[op].setValue( fm, n, v ); if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){ //also set as default value if necessary - if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){ + if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){ Trace("fmf-model-cons") << " Set as default." << std::endl; fm->d_uf_model_gen[op].setValue( fm, n, v, false ); if( n==defaultTerm ){ @@ -619,6 +620,13 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) Trace("fmf-model-cons") << " Choose default value..." << std::endl; //chose defaultVal based on heuristic, currently the best ratio of "pro" responses Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); + if( defaultVal.isNull() ){ + if (!fm->d_rep_set.hasType(defaultTerm.getType())) { + Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType()); + fm->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt); + } + defaultVal = fm->d_rep_set.d_type_reps[defaultTerm.getType()][0]; + } Assert( !defaultVal.isNull() ); Trace("fmf-model-cons") << "Set default term : " << fm->d_rep_set.getIndexFor( defaultVal ) << std::endl; fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); @@ -935,7 +943,7 @@ void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){ if( s.getKind()==APPLY_UF ){ Assert( s.hasAttribute(ModelBasisArgAttribute()) ); if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl; - if( s.getAttribute(ModelBasisArgAttribute())==1 ){ + if( s.getAttribute(ModelBasisArgAttribute())!=0 ){ d_term_selected[ s ] = true; Trace("sel-form-term") << " " << s << " is a selected term." << std::endl; } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index a69b278c0..90b8c62ba 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -36,7 +36,8 @@ using namespace CVC4::theory::inst; //Model Engine constructor ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule( qe ), -d_rel_domain( qe, qe->getModel() ){ +d_rel_domain( qe, qe->getModel() ), +d_fmc( qe ){ if( options::fmfNewInstGen() ){ d_builder = new ModelEngineBuilderInstGen( c, qe ); @@ -75,6 +76,11 @@ void ModelEngine::check( Theory::Effort e ){ //let the strong solver verify that the model is minimal //for debugging, this will if there are terms in the model that the strong solver was not notified of ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ); + //for full model checking + if( d_fmc.isActive() ){ + Trace("model-engine-debug") << "Reset full model checker..." << std::endl; + d_fmc.reset( fm ); + } Trace("model-engine-debug") << "Check model..." << std::endl; d_incomplete_check = false; //print debug @@ -161,15 +167,23 @@ int ModelEngine::checkModel( int checkOption ){ if( it->first.isSort() ){ Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; Trace("model-engine-debug") << " "; + Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); for( size_t i=0; isecond.size(); i++ ){ //Trace("model-engine-debug") << it->second[i] << " "; Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] ); Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; + Trace("model-engine-debug") << " Model basis term : " << mbt << std::endl; } } } + //full model checking: construct models for all functions + if( d_fmc.isActive() ){ + for (std::map< Node, uf::UfModelTreeGenerator >::iterator it = fm->d_uf_model_gen.begin(); it != fm->d_uf_model_gen.end(); ++it) { + d_fmc.getModel(fm, it->first); + } + } //compute the relevant domain if necessary if( optUseRelevantDomain() ){ d_rel_domain.compute(); @@ -179,36 +193,41 @@ int ModelEngine::checkModel( int checkOption ){ d_relevantLemmas = 0; d_totalLemmas = 0; Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - for( int i=0; igetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - //keep track of total instantiations for statistics - int totalInst = 1; - for( size_t i=0; id_rep_set.hasType( tn ) ){ - totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size(); - } - } - d_totalLemmas += totalInst; - //determine if we should check this quantifiers - bool checkQuant = false; - if( checkOption==check_model_full ){ - checkQuant = d_builder->isQuantifierActive( f ); - }else if( checkOption==check_model_no_inst_gen ){ - checkQuant = !d_builder->hasInstGen( f ); - } - //if we need to consider this quantifier on this iteration - if( checkQuant ){ - addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() ); - if( Trace.isOn("model-engine-warn") ){ - if( addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); + int e_max = d_fmc.isActive() ? 2 : 1; + for( int e=0; egetNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + //keep track of total instantiations for statistics + int totalInst = 1; + for( size_t i=0; id_rep_set.hasType( tn ) ){ + totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size(); + } + } + d_totalLemmas += totalInst; + //determine if we should check this quantifiers + bool checkQuant = false; + if( checkOption==check_model_full ){ + checkQuant = d_builder->isQuantifierActive( f ); + }else if( checkOption==check_model_no_inst_gen ){ + checkQuant = !d_builder->hasInstGen( f ); + } + //if we need to consider this quantifier on this iteration + if( checkQuant ){ + addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain(), e ); + if( Trace.isOn("model-engine-warn") ){ + if( addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); + } + } + if( optOneQuantPerRound() && addedLemmas>0 ){ + break; + } } - } - if( optOneQuantPerRound() && addedLemmas>0 ){ - break; } } } @@ -222,100 +241,115 @@ int ModelEngine::checkModel( int checkOption ){ return addedLemmas; } -int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ +int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain, int effort ){ int addedLemmas = 0; - Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << "..." << std::endl; - Debug("inst-fmf-ei") << " Instantiation Constants: "; - for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ) << " "; - } - Debug("inst-fmf-ei") << std::endl; - //create a rep set iterator and iterate over the (relevant) domain of the quantifier - RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) ); - if( riter.setQuantifier( f ) ){ - //set the domain for the iterator (the sufficient set of instantiations to try) - if( useRelInstDomain ){ - riter.setDomain( d_rel_domain.d_quant_inst_domain[f] ); + bool useModel = d_builder->optUseModel(); + if (d_fmc.isActive() && effort==0) { + addedLemmas = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort); + }else if( !d_fmc.isActive() || (effort==1 && d_fmc.hasStarExceptions(f)) ) { + if(d_fmc.isActive()){ + useModel = false; + int lem = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort); + if( lem!=-1 ){ + return lem; + } } - d_quantEngine->getModel()->resetEvaluate(); - int tests = 0; - int triedLemmas = 0; - while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){ - d_testLemmas++; - int eval = 0; - int depIndex; - if( d_builder->optUseModel() ){ - //see if instantiation is already true in current model - Debug("fmf-model-eval") << "Evaluating "; - riter.debugPrintSmall("fmf-model-eval"); - Debug("fmf-model-eval") << "Done calculating terms." << std::endl; - tests++; - //if evaluate(...)==1, then the instantiation is already true in the model - // depIndex is the index of the least significant variable that this evaluation relies upon - depIndex = riter.getNumTerms()-1; - eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); - if( eval==1 ){ - Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; - }else{ - Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; - } + Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl; + Debug("inst-fmf-ei") << " Instantiation Constants: "; + for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ) << " "; + } + Debug("inst-fmf-ei") << std::endl; + //create a rep set iterator and iterate over the (relevant) domain of the quantifier + RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) ); + if( riter.setQuantifier( f ) ){ + Debug("inst-fmf-ei") << "Set domain..." << std::endl; + //set the domain for the iterator (the sufficient set of instantiations to try) + if( useRelInstDomain ){ + riter.setDomain( d_rel_domain.d_quant_inst_domain[f] ); } - if( eval==1 ){ - //instantiation is already true -> skip - riter.increment2( depIndex ); - }else{ - //instantiation was not shown to be true, construct the match - InstMatch m; - for( int i=0; igetTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) ); + Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl; + d_quantEngine->getModel()->resetEvaluate(); + Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; + int tests = 0; + int triedLemmas = 0; + while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){ + d_testLemmas++; + int eval = 0; + int depIndex; + if( useModel ){ + //see if instantiation is already true in current model + Debug("fmf-model-eval") << "Evaluating "; + riter.debugPrintSmall("fmf-model-eval"); + Debug("fmf-model-eval") << "Done calculating terms." << std::endl; + tests++; + //if evaluate(...)==1, then the instantiation is already true in the model + // depIndex is the index of the least significant variable that this evaluation relies upon + depIndex = riter.getNumTerms()-1; + eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); + if( eval==1 ){ + Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; + }else{ + Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; + } } - Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; - triedLemmas++; - d_triedLemmas++; - //add as instantiation - if( d_quantEngine->addInstantiation( f, m ) ){ - addedLemmas++; - //if the instantiation is show to be false, and we wish to skip multiple instantiations at once - if( eval==-1 && optExhInstEvalSkipMultiple() ){ - riter.increment2( depIndex ); + if( eval==1 ){ + //instantiation is already true -> skip + riter.increment2( depIndex ); + }else{ + //instantiation was not shown to be true, construct the match + InstMatch m; + for( int i=0; iaddInstantiation( f, m ) ){ + addedLemmas++; + //if the instantiation is show to be false, and we wish to skip multiple instantiations at once + if( eval==-1 && optExhInstEvalSkipMultiple() ){ + riter.increment2( depIndex ); + }else{ + riter.increment(); + } }else{ + Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; riter.increment(); } - }else{ - Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; - riter.increment(); } } + //print debugging information + d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas; + d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms; + d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits; + d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown; + int relevantInst = 1; + for( size_t i=0; i1000 ){ + Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl; + //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl; + Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl; + Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl; + Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl; + Trace("model-engine-warn") << " # Tests: " << tests << std::endl; + Trace("model-engine-warn") << std::endl; + } } - //print debugging information - d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas; - d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms; - d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits; - d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown; - int relevantInst = 1; - for( size_t i=0; i1000 ){ - Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl; - //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl; - Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl; - Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl; - Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl; - Trace("model-engine-warn") << " # Tests: " << tests << std::endl; - Trace("model-engine-warn") << std::endl; - } + //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round + d_incomplete_check = d_incomplete_check || riter.d_incomplete; } - //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - d_incomplete_check = d_incomplete_check || riter.d_incomplete; return addedLemmas; } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 386864164..d2cd8807a 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -21,6 +21,7 @@ #include "theory/quantifiers/model_builder.h" #include "theory/model.h" #include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/full_model_check.h" namespace CVC4 { namespace theory { @@ -35,6 +36,8 @@ private: private: //analysis of current model: //relevant domain RelevantDomain d_rel_domain; + //full model checker + fmcheck::FullModelChecker d_fmc; //is the exhaustive instantiation incomplete? bool d_incomplete_check; private: @@ -51,7 +54,7 @@ private: //check model int checkModel( int checkOption ); //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced - int exhaustiveInstantiate( Node f, bool useRelInstDomain = false ); + int exhaustiveInstantiate( Node f, bool useRelInstDomain = false, int effort = 0 ); private: //temporary statistics int d_triedLemmas; @@ -63,6 +66,7 @@ public: ~ModelEngine(){} //get the builder ModelEngineBuilder* getModelBuilder() { return d_builder; } + fmcheck::FullModelChecker* getFullModelChecker() { return &d_fmc; } public: void check( Theory::Effort e ); void registerQuantifier( Node f ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 60f5a171d..a9b7f269f 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -54,6 +54,8 @@ option smartTriggers /--disable-smart-triggers bool :default true # Whether to use relevent triggers option relevantTriggers /--disable-relevant-triggers bool :default true prefer triggers that are more relevant based on SInE style analysis +option relationalTriggers --relational-triggers bool :default false + choose relational triggers such as x = f(y), x >= f(y) # Whether to consider terms in the bodies of quantifiers for matching option registerQuantBodyTerms --register-quant-body-terms bool :default false @@ -88,6 +90,11 @@ option finiteModelFind --finite-model-find bool :default false option fmfModelBasedInst /--disable-fmf-mbqi bool :default true disable model-based quantifier instantiation for finite model finding +option fmfFullModelCheck --fmf-fmc bool :default false + enable full model check for finite model finding +option fmfFullModelCheckSimple /--disable-fmf-fmc-simple bool :default true + disable simple models in full model check for finite model finding + option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false only add one instantiation per quantifier per round for fmf option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false @@ -98,8 +105,8 @@ option fmfRelevantDomain --fmf-relevant-domain bool :default false use relevant domain computation, similar to complete instantiation (Ge, deMoura 09) option fmfNewInstGen --fmf-new-inst-gen bool :default false use new inst gen technique for answering sat without exhaustive instantiation -option fmfInstGen /--disable-fmf-inst-gen bool :default true - disable Inst-Gen instantiation techniques for finite model finding +option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true + enable/disable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false only perform Inst-Gen instantiation techniques on one quantifier per round option fmfFreshDistConst --fmf-fresh-dc bool :default false diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 36db56d0d..6b07a87e0 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -22,6 +22,96 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; + +bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) { + if ( n.getKind()==MULT ){ + if( n.getNumChildren()==2 && msum.find(n[1])==msum.end() && n[0].isConst() ){ + msum[n[1]] = n[0]; + return true; + } + }else{ + if( msum.find(n)==msum.end() ){ + msum[n] = Node::null(); + return true; + } + } + return false; +} + +bool QuantArith::getMonomialSum( Node n, std::map< Node, Node >& msum ) { + if ( n.getKind()==PLUS ){ + for( unsigned i=0; i& msum ) { + if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){ + if( getMonomialSum( lit[0], msum ) ){ + if( lit[1].isConst() ){ + if( !lit[1].getConst().isZero() ){ + msum[Node::null()] = negate( lit[1] ); + } + return true; + } + } + } + return false; +} + +bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ) { + if( msum.find(v)!=msum.end() ){ + std::vector< Node > children; + Rational r = msum[v].isNull() ? Rational(1) : msum[v].getConst(); + if ( r.sgn()!=0 ){ + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( it->first!=v ){ + Node m; + if( !it->first.isNull() ){ + if ( !it->second.isNull() ){ + m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first ); + }else{ + m = it->first; + } + }else{ + m = it->second; + } + children.push_back(m); + } + } + veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : + (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); + if( !r.isNegativeOne() ){ + if( r.isOne() ){ + veq = negate(veq); + }else{ + //TODO + return false; + } + } + veq = Rewriter::rewrite( veq ); + veq = NodeManager::currentNM()->mkNode( k, r.sgn()==1 ? v : veq, r.sgn()==1 ? veq : v ); + return true; + } + return false; + }else{ + return false; + } +} + +Node QuantArith::negate( Node t ) { + Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t ); + tt = Rewriter::rewrite( tt ); + return tt; +} + + void QuantRelevance::registerQuantifier( Node f ){ //compute symbols in f std::vector< Node > syms; diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 6a5726cc7..d248a8999 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -28,6 +28,17 @@ namespace CVC4 { namespace theory { +class QuantArith +{ +public: + static bool getMonomial( Node n, std::map< Node, Node >& msum ); + static bool getMonomialSum( Node n, std::map< Node, Node >& msum ); + static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum ); + static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ); + static Node negate( Node t ); +}; + + class QuantRelevance { private: diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3153a3c64..417b4ae3a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -254,8 +254,7 @@ void TermDb::computeModelBasisArgAttribute( Node n ){ //determine if it has model basis attribute for( int j=0; j<(int)n.getNumChildren(); j++ ){ if( n[j].getAttribute(ModelBasisAttribute()) ){ - val = 1; - break; + val++; } } ModelBasisArgAttribute mbaa; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 231d0ee9e..e5154476a 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -83,10 +83,15 @@ public: };/* class TermArgTrie */ +namespace fmcheck { + class FullModelChecker; +} + class TermDb { friend class ::CVC4::theory::QuantifiersEngine; friend class ::CVC4::theory::inst::Trigger; friend class ::CVC4::theory::rrinst::Trigger; + friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker; private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index cab94fb5c..1f1667522 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -28,8 +28,6 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::inst; -//#define NESTED_PATTERN_SELECTION - /** trigger class constructor */ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) : d_quantEngine( qe ), d_f( f ){ @@ -249,11 +247,75 @@ bool Trigger::isUsable( Node n, Node f ){ } } -bool Trigger::isUsableTrigger( Node n, Node f ){ - //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF; +bool nodeContainsVar( Node n, Node v ){ + if( n==v) { + return true; + }else{ + for( unsigned i=0; i m; + if (QuantArith::getMonomialSumLit(n, m) ){ + for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){ + if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){ + Node veq; + if( QuantArith::isolate( it->first, m, veq, n.getKind() ) ){ + int vti = veq[0]==it->first ? 1 : 0; + if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){ + rtr = veq; + InstConstantAttribute ica; + rtr.setAttribute(ica,veq[vti].getAttribute(InstConstantAttribute()) ); + } + } + } + } + } + } + if( !rtr.isNull() ){ + Trace("relational-trigger") << "Relational trigger : " << std::endl; + Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl; + Trace("relational-trigger") << " in quantifier " << f << std::endl; + if( hasPol ){ + Trace("relational-trigger") << " polarity : " << pol << std::endl; + } + Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr; + InstConstantAttribute ica; + rtr2.setAttribute(ica,rtr.getAttribute(InstConstantAttribute()) ); + return rtr2; + } + } + } bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f ); Trace("usable") << n << " usable : " << usable << std::endl; - return usable; + if( usable ){ + return n; + }else{ + return Node::null(); + } +} + +bool Trigger::isUsableTrigger( Node n, Node f ){ + Node nu = getIsUsableTrigger(n,f); + return !nu.isNull(); } bool Trigger::isAtomicTrigger( Node n ){ @@ -274,55 +336,51 @@ bool Trigger::isSimpleTrigger( Node n ){ } -bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){ +bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ){ if( patMap.find( n )==patMap.end() ){ patMap[ n ] = false; + bool newHasPol = (n.getKind()==IFF || n.getKind()==XOR) ? false : hasPol; + bool newPol = n.getKind()==NOT ? !pol : pol; if( tstrt==TS_MIN_TRIGGER ){ if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ); - return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ); -#else return false; -#endif }else{ bool retVal = false; for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; + bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ retVal = true; } } if( retVal ){ return true; - }else if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; - return true; }else{ - return false; + Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + if( !nu.isNull() ){ + patMap[ nu ] = true; + return true; + }else{ + return false; + } } } }else{ bool retVal = false; - if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; + Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + if( !nu.isNull() ){ + patMap[ nu ] = true; if( tstrt==TS_MAX_TRIGGER ){ return true; }else{ retVal = true; } } - if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){ - // retVal = true; - //} - if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){ - retVal = true; - } -#endif - }else{ + if( n.getKind()!=FORALL ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; + bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ retVal = true; } } @@ -367,7 +425,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } } - collectPatTerms2( qe, f, n, patMap, tstrt ); + collectPatTerms2( qe, f, n, patMap, tstrt, true, true ); for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ if( it->second ){ patTerms.push_back( it->first ); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index ca9124751..28fb2acda 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -92,8 +92,9 @@ public: private: /** is subterm of trigger usable */ static bool isUsable( Node n, Node f ); + static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ - static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ); + static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ); public: //different strategies for choosing trigger terms enum { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0bb0f1f79..5c24f89b7 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -27,6 +27,7 @@ #include "theory/quantifiers/trigger.h" #include "theory/rewriterules/efficient_e_matching.h" #include "theory/rewriterules/rr_trigger.h" +#include "theory/quantifiers/bounded_integers.h" using namespace std; using namespace CVC4; @@ -60,8 +61,12 @@ d_lemmas_produced_c(u){ if( options::finiteModelFind() ){ d_model_engine = new quantifiers::ModelEngine( c, this ); d_modules.push_back( d_model_engine ); + + d_bint = new quantifiers::BoundedIntegers( this ); + d_modules.push_back( d_bint ); }else{ d_model_engine = NULL; + d_bint = NULL; } //options diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bfa19bb98..85da53087 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -56,7 +56,7 @@ public: virtual void assertNode( Node n ) = 0; virtual void propagate( Theory::Effort level ){} virtual Node getNextDecisionRequest() { return TNode::null(); } - virtual Node explain(TNode n) = 0; + virtual Node explain(TNode n) { return TNode::null(); } };/* class QuantifiersModule */ namespace quantifiers { @@ -64,6 +64,7 @@ namespace quantifiers { class ModelEngine; class TermDb; class FirstOrderModel; + class BoundedIntegers; }/* CVC4::theory::quantifiers */ namespace inst { @@ -99,6 +100,8 @@ private: std::map< Node, QuantPhaseReq* > d_phase_reqs; /** efficient e-matcher */ EfficientEMatcher* d_eem; + /** bounded integers utility */ + quantifiers::BoundedIntegers * d_bint; private: /** list of all quantifiers seen */ std::vector< Node > d_quants; diff --git a/src/theory/uf/options b/src/theory/uf/options index 33d1255ef..bea11621a 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -30,5 +30,7 @@ option ufssSimpleCliques --uf-ss-simple-cliques bool :default true always use simple clique lemmas for uf strong solver option ufssDiseqPropagation --uf-ss-deq-prop bool :default false eagerly propagate disequalities for uf strong solver +option ufssMinimalModel /--disable-uf-ss-min-model bool :default true + disable finding a minimal model in uf strong solver endmodule diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 228cfd2c4..2c853a4fa 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -17,6 +17,7 @@ #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/options.h" #define RECONSIDER_FUNC_DEFAULT_VALUE #define USE_PARTIAL_DEFAULT_VALUES @@ -309,19 +310,21 @@ void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground if( !ground ){ int defSize = (int)d_defaults.size(); for( int i=0; i d_set_values[2][2]; diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index d64f7df60..e868460f8 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -595,9 +595,11 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel if( d_regions[i]->d_valid ){ std::vector< Node > clique; if( d_regions[i]->check( level, d_cardinality, clique ) ){ - //add clique lemma - addCliqueLemma( clique, out ); - return; + if( options::ufssMinimalModel() ){ + //add clique lemma + addCliqueLemma( clique, out ); + return; + } }else{ Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl; } @@ -659,13 +661,17 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel //naive strategy, force region combination involving the first valid region for( int i=0; i<(int)d_regions_index; i++ ){ if( d_regions[i]->d_valid ){ - forceCombineRegion( i, false ); - recheck = true; - break; + int fcr = forceCombineRegion( i, false ); + Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl; + if( options::ufssMinimalModel() || fcr!=-1 ){ + recheck = true; + break; + } } } } if( recheck ){ + Trace("uf-ss-debug") << "Must recheck." << std::endl; check( level, out ); } } @@ -869,8 +875,10 @@ void StrongSolverTheoryUF::SortModel::checkRegion( int ri, bool checkCombine ){ //now check if region is in conflict std::vector< Node > clique; if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){ - //explain clique - addCliqueLemma( clique, &d_thss->getOutputChannel() ); + if( options::ufssMinimalModel() ){ + //explain clique + addCliqueLemma( clique, &d_thss->getOutputChannel() ); + } } } } @@ -1013,8 +1021,8 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ } bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ + Node s; if( r->hasSplits() ){ - Node s; if( !options::ufssSmartSplits() ){ //take the first split you find for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){ @@ -1038,8 +1046,26 @@ bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ } } } + Assert( s!=Node::null() ); + }else{ + if( !options::ufssMinimalModel() ){ + //since candidate clique is not reported, we may need to find splits manually + for ( std::map< Node, Region::RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){ + if ( it->second->d_valid ){ + for ( std::map< Node, Region::RegionNodeInfo* >::iterator it2 = r->d_nodes.begin(); it2 != r->d_nodes.end(); ++it2 ){ + if ( it->second!=it2->second && it2->second->d_valid ){ + if( !r->isDisequal( it->first, it2->first, 1 ) ){ + s = NodeManager::currentNM()->mkNode( EQUAL, it->first, it2->first ); + } + } + } + } + } + } + } + if (!s.isNull() ){ //add lemma to output channel - Assert( s!=Node::null() && s.getKind()==EQUAL ); + Assert( s.getKind()==EQUAL ); s = Rewriter::rewrite( s ); Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; if( options::sortInference()) { -- 2.30.2