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 | |
| 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.
26 files changed, 1759 insertions, 195 deletions
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<n.getNumChildren(); i++) {
+ bool newPol = n.getKind()==IMPLIES && i==0 ? !pol : pol;
+ process( f, n[i], newPol );
+ }
+ }else if( n.getKind()==NOT ){
+ process( f, n[0], !pol );
+ }else {
+ processLiteral( f, n, pol );
+ }
+}
+
+void BoundedIntegers::check( Theory::Effort e ) {
+
+}
+
+void BoundedIntegers::registerQuantifier( Node f ) {
+ bool hasIntType = false;
+ for( unsigned i=0; i<f[0].getNumChildren(); i++) {
+ if( f[0][i].getType().isInteger() ){
+ hasIntType = true;
+ break;
+ }
+ }
+ if( hasIntType ){
+ process( f, f[1], true );
+ }
+}
+
+void BoundedIntegers::assertNode( Node n ) {
+
+}
+
+Node BoundedIntegers::getNextDecisionRequest() {
+ return Node::null();
+}
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h new file mode 100755 index 000000000..570e27a10 --- /dev/null +++ b/src/theory/quantifiers/bounded_integers.h @@ -0,0 +1,47 @@ +/********************* */
+/*! \file bounded_integers.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 This class manages integer bounds for quantifiers
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BOUNDED_INTEGERS_H
+#define __CVC4__BOUNDED_INTEGERS_H
+
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class BoundedIntegers : public QuantifiersModule
+{
+private:
+ std::map< Node, std::map< Node, Node > > 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<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();
+}
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<Node,EntryTrie> 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<Node> & inst, int index = 0 );
+ void getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & 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<Node> & 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<Node> inst );
+ int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> 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<TypeNode, std::map< Node, int > > d_rep_ids;
+ std::map<TypeNode, Node > d_model_basis_rep;
+ std::map<Node, Def * > d_models;
+ std::map<Node, Def > d_quant_models;
+ std::map<Node, bool > d_models_init;
+ std::map<Node, Node > d_quant_cond;
+ std::map<TypeNode, Node > d_type_star;
+ std::map<Node, std::map< Node, int > > d_quant_var_id;
+ std::map<Node, std::vector< int > > 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<Node> & 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<Node> & 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)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->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; i<it->second.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; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - //keep track of total instantiations for statistics - int totalInst = 1; - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - TypeNode tn = f[0][i].getType(); - if( fm->d_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; e<e_max; e++) { + if (addedLemmas==0) { + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + //keep track of total instantiations for statistics + int totalInst = 1; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + TypeNode tn = f[0][i].getType(); + if( fm->d_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; i<f[0].getNumChildren(); i++ ){ - Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->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; i<f[0].getNumChildren(); i++ ){ + Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->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; i<riter.getNumTerms(); i++ ){ - m.set( d_quantEngine->getTermDatabase()->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; i<riter.getNumTerms(); i++ ){ + m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) ); + } + 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 ); + }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; i<f[0].getNumChildren(); i++ ){ + relevantInst = relevantInst * (int)riter.d_domain[i].size(); + } + d_relevantLemmas += relevantInst; + Trace("inst-fmf-ei") << "Finished: " << std::endl; + //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl; + Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; + Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; + Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; + Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl; + if( addedLemmas>1000 ){ + 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; i<f[0].getNumChildren(); i++ ){ - relevantInst = relevantInst * (int)riter.d_domain[i].size(); - } - d_relevantLemmas += relevantInst; - Trace("inst-fmf-ei") << "Finished: " << std::endl; - //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl; - Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; - Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; - Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; - Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl; - if( addedLemmas>1000 ){ - 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<n.getNumChildren(); i++) { + if (!getMonomial( n[i], msum )){ + return false; + } + } + return true; + }else{ + return getMonomial( n, msum ); + } +} + +bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) { + if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){ + if( getMonomialSum( lit[0], msum ) ){ + if( lit[1].isConst() ){ + if( !lit[1].getConst<Rational>().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<Rational>(); + 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<n.getNumChildren(); i++) { + if( nodeContainsVar(n[i], v) ){ + return true; + } + } + return false; + } +} + +Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { + if( options::relationalTriggers() ){ + if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ + Node rtr; + for( unsigned i=0; i<2; i++) { + unsigned j = (i==0) ? 1 : 0; + if( n[j].getKind()==INST_CONSTANT && isUsableTrigger(n[i], f) && !nodeContainsVar( n[i], n[j] ) ) { + rtr = n; + break; + } + } + if( n[0].getType().isInteger() ){ + //try to rearrange? + std::map< Node, Node > 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<defSize; i++ ){ - bool isGround; //for soundness, to allow variable order-independent function interpretations, // we must ensure that the intersection of all default terms // is also defined. //for example, if we have that f( e, a ) = ..., and f( b, e ) = ..., // then we must define f( b, a ). - Node ni = getIntersection( m, n, d_defaults[i], isGround ); - if( !ni.isNull() ){ - //if the intersection exists, and is not already defined - if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() && - d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){ - //use the current value - setValue( m, ni, v, isGround, false ); + if (!options::fmfFullModelCheck()) { + bool isGround; + Node ni = getIntersection( m, n, d_defaults[i], isGround ); + if( !ni.isNull() ){ + //if the intersection exists, and is not already defined + if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() && + d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){ + //use the current value + setValue( m, ni, v, isGround, false ); + } } } } diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 12c1cf244..9140806ec 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -153,9 +153,10 @@ public: static Node toIte( TypeNode type, Node fm_node, const char* argPrefix ); }; + class UfModelTreeGenerator { -private: +public: //store for set values Node d_default_value; std::map< Node, Node > 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()) { |