From 52514cada7c0c7c4fff69c85e0bd735abfdc03fd Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 13 Nov 2014 12:17:46 +0100 Subject: [PATCH] Remove two obsolete versions of MBQI. --- src/Makefile.am | 4 - src/smt/smt_engine.cpp | 4 - src/theory/quantifiers/first_order_model.cpp | 162 --- src/theory/quantifiers/first_order_model.h | 44 - src/theory/quantifiers/inst_gen.cpp | 300 ----- src/theory/quantifiers/inst_gen.h | 60 - src/theory/quantifiers/model_builder.cpp | 387 ------ src/theory/quantifiers/model_builder.h | 52 - src/theory/quantifiers/model_engine.cpp | 1 - src/theory/quantifiers/modes.cpp | 6 - src/theory/quantifiers/modes.h | 4 - src/theory/quantifiers/options_handlers.h | 4 - src/theory/quantifiers/qinterval_builder.cpp | 1111 ------------------ src/theory/quantifiers/qinterval_builder.h | 155 --- src/theory/quantifiers/term_database.cpp | 2 +- src/theory/quantifiers_engine.cpp | 11 +- src/theory/quantifiers_engine.h | 2 +- 17 files changed, 4 insertions(+), 2305 deletions(-) delete mode 100644 src/theory/quantifiers/inst_gen.cpp delete mode 100644 src/theory/quantifiers/inst_gen.h delete mode 100644 src/theory/quantifiers/qinterval_builder.cpp delete mode 100644 src/theory/quantifiers/qinterval_builder.h diff --git a/src/Makefile.am b/src/Makefile.am index 2acefc577..f88dcb3a9 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -295,8 +295,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/model_builder.cpp \ theory/quantifiers/quantifiers_attributes.h \ theory/quantifiers/quantifiers_attributes.cpp \ - theory/quantifiers/inst_gen.h \ - theory/quantifiers/inst_gen.cpp \ theory/quantifiers/quant_util.h \ theory/quantifiers/quant_util.cpp \ theory/quantifiers/inst_match_generator.h \ @@ -319,8 +317,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/relevant_domain.cpp \ theory/quantifiers/symmetry_breaking.h \ theory/quantifiers/symmetry_breaking.cpp \ - theory/quantifiers/qinterval_builder.h \ - theory/quantifiers/qinterval_builder.cpp \ theory/quantifiers/ambqi_builder.h \ theory/quantifiers/ambqi_builder.cpp \ theory/quantifiers/quant_conflict_find.h \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index dc80d65e3..8bf093370 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1305,10 +1305,6 @@ void SmtEngine::setDefaults() { options::mbqiMode.set( quantifiers::MBQI_NONE ); } } - if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ - //must do pre-skolemization - options::preSkolemQuant.set( true ); - } if( options::ufssSymBreak() ){ options::sortInference.set( true ); } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 1570ba306..d4f32becc 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -17,7 +17,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/full_model_check.h" -#include "theory/quantifiers/qinterval_builder.h" #include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/options.h" @@ -754,167 +753,6 @@ bool FirstOrderModelFmc::isInRange( Node v, Node i ) { } -FirstOrderModelQInt::FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name) : -FirstOrderModel(qe, c, name) { - -} - -void FirstOrderModelQInt::processInitialize( bool ispre ) { - if( !ispre ){ - Trace("qint-debug") << "Process initialize" << std::endl; - for( std::map::iterator it = d_models.begin(); it != d_models.end(); ++it ) { - Node op = it->first; - TypeNode tno = op.getType(); - Trace("qint-debug") << " Init " << op << " " << tno << std::endl; - for( unsigned i=0; i vars; - for( size_t i=0; imkBoundVar( ss.str(), type[i] ); - vars.push_back( b ); - } - Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); - Node curr = d_models[op]->getFunctionValue( this, vars ); - Node fv = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); - Trace("qint-debug") << "Return " << fv << std::endl; - return fv; -} - -Node FirstOrderModelQInt::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { - Debug("qint-debug") << "get curr uf value " << n << std::endl; - return d_models[n]->evaluate( this, args ); -} - -void FirstOrderModelQInt::processInitializeModelForTerm(Node n) { - Debug("qint-debug") << "process init " << n << " " << n.getKind() << std::endl; - - if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ - Node op = n.getKind()==APPLY_UF ? n.getOperator() : n; - if( d_models.find(op)==d_models.end()) { - Debug("qint-debug") << "init model for " << op << std::endl; - d_models[op] = new QIntDef; - } - } -} - -Node FirstOrderModelQInt::getUsedRepresentative( Node n ) { - if( hasTerm( n ) ){ - if( n.getType().isBoolean() ){ - return areEqual(n, d_true) ? d_true : d_false; - }else{ - return getRepresentative( n ); - } - }else{ - Trace("qint-debug") << "Get rep " << n << " " << n.getType() << std::endl; - Assert( d_rep_set.hasType( n.getType() ) && !d_rep_set.d_type_reps[n.getType()].empty() ); - return d_rep_set.d_type_reps[n.getType()][0]; - } -} - -void FirstOrderModelQInt::processInitializeQuantifier( Node q ) { - if( d_var_order.find( q )==d_var_order.end() ){ - d_var_order[q] = new QuantVarOrder( q ); - d_var_order[q]->debugPrint("qint-var-order"); - Trace("qint-var-order") << std::endl; - } -} -unsigned FirstOrderModelQInt::getOrderedNumVars( Node q ) { - //return q[0].getNumChildren(); - return d_var_order[q]->getNumVars(); -} - -TypeNode FirstOrderModelQInt::getOrderedVarType( Node q, int i ) { - //return q[0][i].getType(); - return d_var_order[q]->getVar( i ).getType(); -} - -int FirstOrderModelQInt::getOrderedVarNumToVarNum( Node q, int i ) { - return getVariableId( q, d_var_order[q]->getVar( i ) ); -} - -bool FirstOrderModelQInt::isLessThan( Node v1, Node v2 ) { - Assert( !v1.isNull() ); - Assert( !v2.isNull() ); - if( v1.getType().isSort() ){ - Assert( getRepId( v1 )!=-1 ); - Assert( getRepId( v2 )!=-1 ); - int rid1 = d_rep_id[v1]; - int rid2 = d_rep_id[v2]; - return rid1 d_models; - /** representatives to ids */ - std::map< Node, int > d_rep_id; - std::map< TypeNode, Node > d_min; - std::map< TypeNode, Node > d_max; - /** quantifiers to information regarding variable ordering */ - std::map d_var_order; - /** get current model value */ - Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ); - void processInitializeModelForTerm(Node n); -public: - FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name); - FirstOrderModelQInt * asFirstOrderModelQInt() { return this; } - void processInitialize( bool ispre ); - Node getFunctionValue(Node op, const char* argPrefix ); - - Node getUsedRepresentative( Node n ); - int getRepId( Node n ) { return d_rep_id.find( n )==d_rep_id.end() ? -1 : d_rep_id[n]; } - bool isLessThan( Node v1, Node v2 ); - Node getMin( Node v1, Node v2 ); - Node getMax( Node v1, Node v2 ); - Node getMinimum( TypeNode tn ) { return getNext( tn, Node::null() ); } - Node getMaximum( TypeNode tn ); - bool isMinimum( Node n ) { return n==getMinimum( n.getType() ); } - bool isMaximum( Node n ) { return n==getMaximum( n.getType() ); } - Node getNext( TypeNode tn, Node v ); - Node getPrev( TypeNode tn, Node v ); - bool doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur ); - QuantVarOrder * getVarOrder( Node q ) { return d_var_order[q]; } - - void processInitializeQuantifier( Node q ) ; - unsigned getOrderedNumVars( Node q ); - TypeNode getOrderedVarType( Node q, int i ); - int getOrderedVarNumToVarNum( Node q, int i ); -};/* class FirstOrderModelQInt */ - class AbsDef; class FirstOrderModelAbs : public FirstOrderModel diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp deleted file mode 100644 index 33fcaa27a..000000000 --- a/src/theory/quantifiers/inst_gen.cpp +++ /dev/null @@ -1,300 +0,0 @@ -/********************* */ -/*! \file inst_gen.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 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 inst gen classes - **/ - -#include "theory/quantifiers/inst_gen.h" -#include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/model_builder.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database.h" - -//#define CHILD_USE_CONSIDER - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - - - -InstGenProcess::InstGenProcess( Node n ) : d_node( n ){ - Assert( TermDb::hasInstConstAttr(n) ); - int count = 0; - for( size_t i=0; iexistsInstantiation( f, m, true ) ){ - //make sure no duplicates are produced - if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){ - d_match_values.push_back( val ); - d_matches.push_back( InstMatch( &m ) ); - ((QModelBuilderIG*)qe->getModelBuilder())->d_instGenMatches++; - } - } -} - -void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){ - Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl; - //whether we are doing a product or sum or matches - bool doProduct = true; - //get the model - FirstOrderModel* fm = qe->getModel(); - - //calculate terms we will consider - std::vector< Node > considerTerms; - std::vector< std::vector< Node > > newConsiderVal; - std::vector< bool > newUseConsider; - std::map< Node, InstMatch > considerTermsMatch[2]; - std::map< Node, bool > considerTermsSuccess[2]; - newConsiderVal.resize( d_children.size() ); - newUseConsider.resize( d_children.size(), useConsider ); - if( d_node.getKind()==APPLY_UF ){ - Node op = d_node.getOperator(); - if( useConsider ){ -#ifndef CHILD_USE_CONSIDER - for( size_t i=0; igetEqualityQuery()->getEngine()->getRepresentative( considerVal[i] ), - qe->getEqualityQuery()->getEngine() ); - while( !eqc.isFinished() ){ - Node en = (*eqc); - if( en.getKind()==APPLY_UF && en.getOperator()==op ){ - considerTerms.push_back( en ); - } - ++eqc; - } - } - }else{ - considerTerms.insert( considerTerms.begin(), fm->d_uf_terms[op].begin(), fm->d_uf_terms[op].end() ); - } - //for each term we consider, calculate a current match - for( size_t i=0; igetModelBuilder())->isTermSelected( n ); - bool hadSuccess CVC4_UNUSED = false; - for( int t=(isSelected ? 0 : 1); t<2; t++ ){ - if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ - considerTermsMatch[t][n] = InstMatch( f ); - considerTermsSuccess[t][n] = true; - for( size_t j=0; jgetEqualityQuery()->areEqual( d_node[j], n[j] ) ){ - Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl; - considerTermsSuccess[t][n] = false; - break; - } - } - } - } - //if successful, store it - if( considerTermsSuccess[t][n] ){ -#ifdef CHILD_USE_CONSIDER - if( !hadSuccess ){ - hadSuccess = true; - for( size_t k=0; kgetModel()->getRepresentative( n[childIndex] ); - if( std::find( newConsiderVal[k].begin(), newConsiderVal[k].end(), r )==newConsiderVal[k].end() ){ - newConsiderVal[k].push_back( r ); - //check if we now need to consider the entire domain - TypeNode tn = r.getType(); - if( qe->getModel()->d_rep_set.hasType( tn ) ){ - if( (int)newConsiderVal[k].size()>=qe->getModel()->d_rep_set.getNumRepresentatives( tn ) ){ - newConsiderVal[k].clear(); - newUseConsider[k] = false; - } - } - } - }else{ - //matching against selected term, will need to consider all values - newConsiderVal[k].clear(); - newUseConsider[k] = false; - } - } - } - } -#endif - } - } - } - } - }else{ - //the interpretted case - if( d_node.getType().isBoolean() ){ - if( useConsider ){ - //if( considerVal.size()!=1 ) { std::cout << "consider val = " << considerVal.size() << std::endl; } - Assert( considerVal.size()==1 ); - bool reqPol = considerVal[0]==fm->d_true; - Node ncv = considerVal[0]; - if( d_node.getKind()==NOT ){ - ncv = reqPol ? fm->d_false : fm->d_true; - } - if( d_node.getKind()==NOT || d_node.getKind()==AND || d_node.getKind()==OR ){ - for( size_t i=0; igetModelBuilder())->isTermSelected( n ); - for( int t=(isSelected ? 0 : 1); t<2; t++ ){ - //do not consider ground case if it is already congruent to another ground term - if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ - Trace("inst-gen-cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl; - if( considerTermsSuccess[t][n] ){ - //try to find unifier for d_node = n - calculateMatchesUninterpreted( qe, f, considerTermsMatch[t][n], n, 0, t==0 ); - } - } - } - } - }else{ - //if this is an interpreted function - if( doProduct ){ - //combining children matches - InstMatch curr( f ); - std::vector< Node > terms; - calculateMatchesInterpreted( qe, f, curr, terms, 0 ); - }else{ - //summing children matches - Assert( considerVal.size()==1 ); - for( int i=0; i<(int)d_children.size(); i++ ){ - for( int j=0; j<(int)d_children[ i ].getNumMatches(); j++ ){ - InstMatch m( f ); - if( d_children[ i ].getMatch( qe->getEqualityQuery(), j, m ) ){ - addMatchValue( qe, f, considerVal[0], m ); - } - } - } - } - } - Trace("inst-gen-cm") << "done calculate matches" << std::endl; - //can clear information used for finding duplicates - d_inst_trie.clear(); -} - -bool InstGenProcess::getMatch( EqualityQuery* q, int i, InstMatch& m ){ - //FIXME: is this correct? (query may not be accurate) - return m.merge( q, d_matches[i] ); -} - -void InstGenProcess::calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ){ - if( childIndex==(int)d_children.size() ){ - Node val = qe->getModel()->getRepresentative( n ); //FIXME: is this correct? - Trace("inst-gen-cm") << " - u-match : " << val << std::endl; - Trace("inst-gen-cm") << " : " << curr << std::endl; - addMatchValue( qe, f, val, curr ); - }else{ - Trace("inst-gen-cm") << "Consider child index = " << childIndex << ", against ground term argument " << d_children_index[childIndex] << " ... " << n[d_children_index[childIndex]] << std::endl; - bool sel = ( isSelected && n[d_children_index[childIndex]].getAttribute(ModelBasisAttribute()) ); - for( int i=0; i<(int)d_children[ childIndex ].getNumMatches(); i++ ){ - //FIXME: is this correct? - if( sel || qe->getEqualityQuery()->areEqual( d_children[ childIndex ].getMatchValue( i ), n[d_children_index[childIndex]] ) ){ - InstMatch next( &curr ); - if( d_children[ childIndex ].getMatch( qe->getEqualityQuery(), i, next ) ){ - calculateMatchesUninterpreted( qe, f, next, n, childIndex+1, isSelected ); - }else{ - Trace("inst-gen-cm") << curr << " not equal to " << d_children[ childIndex ].d_matches[i] << std::endl; - Trace("inst-gen-cm") << childIndex << " match " << i << " not equal subs." << std::endl; - } - }else{ - Trace("inst-gen-cm") << childIndex << " match " << i << " not equal value." << std::endl; - } - } - } -} - -void InstGenProcess::calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex ){ - FirstOrderModel* fm = qe->getModel(); - if( argIndex==(int)d_node.getNumChildren() ){ - Node val; - if( d_node.getNumChildren()==0 ){ - val = d_node; - }else if( d_node.getKind()==EQUAL ){ - val = qe->getEqualityQuery()->areEqual( terms[0], terms[1] ) ? fm->d_true : fm->d_false; - }else{ - val = NodeManager::currentNM()->mkNode( d_node.getKind(), terms ); - val = Rewriter::rewrite( val ); - } - Trace("inst-gen-cm") << " - i-match : " << d_node << std::endl; - Trace("inst-gen-cm") << " : " << val << std::endl; - Trace("inst-gen-cm") << " : " << curr << std::endl; - addMatchValue( qe, f, val, curr ); - }else{ - if( d_children_map.find( argIndex )==d_children_map.end() ){ - terms.push_back( fm->getRepresentative( d_node[argIndex] ) ); - calculateMatchesInterpreted( qe, f, curr, terms, argIndex+1 ); - terms.pop_back(); - }else{ - for( int i=0; i<(int)d_children[ d_children_map[argIndex] ].getNumMatches(); i++ ){ - InstMatch next( &curr ); - if( d_children[ d_children_map[argIndex] ].getMatch( qe->getEqualityQuery(), i, next ) ){ - terms.push_back( d_children[ d_children_map[argIndex] ].getMatchValue( i ) ); - calculateMatchesInterpreted( qe, f, next, terms, argIndex+1 ); - terms.pop_back(); - } - } - } - } -} diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h deleted file mode 100644 index 6567994f2..000000000 --- a/src/theory/quantifiers/inst_gen.h +++ /dev/null @@ -1,60 +0,0 @@ -/********************* */ -/*! \file inst_gen.h - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Inst Gen classes - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__INST_GEN_H -#define __CVC4__THEORY__QUANTIFIERS__INST_GEN_H - -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/inst_match.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class InstGenProcess -{ -private: - //the node we are processing - Node d_node; - std::map< int, int > d_var_num; - //the sub children for this node - std::vector< InstGenProcess > d_children; - std::vector< int > d_children_index; - std::map< int, int > d_children_map; - //the matches we have produced - std::vector< InstMatch > d_matches; - std::vector< Node > d_match_values; - //add match value - std::map< Node, inst::InstMatchTrie > d_inst_trie; - void addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ); -private: - void calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ); - void calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex ); -public: - InstGenProcess( Node n ); - virtual ~InstGenProcess(){} - - void calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ); - int getNumMatches() { return d_matches.size(); } - bool getMatch( EqualityQuery* q, int i, InstMatch& m ); - Node getMatchValue( int i ) { return d_match_values[i]; } -};/* class InstGenProcess */ - -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__QUANTIFIERS__INST_GEN_H */ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index f6392a0b2..53f55e70b 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -22,7 +22,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/model_builder.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/inst_gen.h" #include "theory/quantifiers/trigger.h" #include "theory/quantifiers/options.h" @@ -754,389 +753,3 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ } - - -////////////////////// Inst-Gen style Model Builder /////////// - -void QModelBuilderInstGen::reset( FirstOrderModel* fm ){ - //for new inst gen - d_quant_selection_formula.clear(); - d_term_selected.clear(); - - //d_sub_quant_inst_trie.clear();//* -} - -int QModelBuilderInstGen::initializeQuantifier( Node f, Node fp ){ - int addedLemmas = QModelBuilderIG::initializeQuantifier( f, fp ); - for( size_t i=0; igetTermDatabase()->getInstConstantBody( f ), - d_qe->getTermDatabase()->getModelBasisBody( f ), true, 0 ); - //if( !s.isNull() ){ - // s = Rewriter::rewrite( s ); - //} - Trace("sel-form-debug") << "Selection formula " << f << std::endl; - Trace("sel-form-debug") << " " << s << std::endl; - if( !s.isNull() ){ - d_quant_selection_formula[f] = s; - Node gs = d_qe->getTermDatabase()->getModelBasis( f, s ); - setSelectedTerms( gs ); - //quick check if it is constant sat - if( hasConstantDefinition( s ) ){ - d_quant_sat[f] = true; - } - }else{ - Trace("sel-form-null") << "*** No selection formula for " << f << std::endl; - } - //analyze sub quantifiers - if( d_quant_sat.find( f )==d_quant_sat.end() ){ - for( size_t i=0; i0 || !subQuantSat ){ - Trace("inst-gen") << " -> children added lemmas or non-satisfied" << std::endl; - return addedLemmas; - }else{ - Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl; - //get all possible values of selection formula - InstGenProcess igp( d_quant_selection_formula[f] ); - std::vector< Node > considered; - considered.push_back( fm->d_false ); - igp.calculateMatches( d_qe, f, considered, true ); - //igp.calculateMatches( d_qe, f); - Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl; - for( int i=0; id_true ){ - InstMatch m( f ); - igp.getMatch( d_qe->getEqualityQuery(), i, m ); - //Trace("inst-gen-debug") << "Inst Gen : " << m << std::endl; - //we only consider matches that are non-empty - // matches that are empty should trigger other instances that are non-empty - if( !m.empty() ){ - Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl; - //translate to be in terms match in terms of fp - InstMatch mp(f); - getParentQuantifierMatch( mp, fp, m, f ); - //if this is a partial instantion - if( !m.isComplete() ){ - //need to make it internal here - //Trace("mkInternal") << "Make internal representative " << mp << std::endl; - //mp.makeInternalRepresentative( d_qe ); - //Trace("mkInternal") << "Got " << mp << std::endl; - //if the instantiation does not yet exist - if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){ - //also add it to children - d_child_sub_quant_inst_trie[f].addInstMatch( d_qe, f, m ); - //get the partial instantiation pf - Node pf = d_qe->getInstantiation( fp, mp ); - Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl; - Trace("inst-gen-pi") << " " << pf << std::endl; - d_sub_quants[ f ].push_back( pf ); - d_sub_quant_inst[ pf ] = InstMatch( &mp ); - d_sub_quant_parent[ pf ] = fp; - //now make mp a complete match - mp.add( d_quant_basis_match[ fp ] ); - d_quant_basis_match[ pf ] = InstMatch( &mp ); - ++(d_statistics.d_num_quants_init); - ++(d_statistics.d_num_partial_quants_init); - addedLemmas += initializeQuantifier( pf, fp ); - Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl; - subQuantSat = false; - } - }else{ - if( d_qe->addInstantiation( fp, mp ) ){ - addedLemmas++; - } - } - } - } - } - if( addedLemmas==0 ){ - //all sub quantifiers must be satisfied as well - if( subQuantSat ){ - d_quant_sat[ f ] = true; - } - } - if( fp!=f ) Trace("inst-gen") << " "; - Trace("inst-gen") << " -> added lemmas = " << addedLemmas << std::endl; - if( d_quant_sat.find( f )!=d_quant_sat.end() ){ - if( fp!=f ) Trace("inst-gen") << " "; - Trace("inst-gen") << " -> *** it is satisfied" << std::endl; - } - } - } - } - return addedLemmas; -} - -Node mkAndSelectionFormula( std::vector< Node >& children ){ - std::vector< Node > ch; - for( size_t i=0; imkNode( AND, ch ); -} -Node mkAndSelectionFormula( Node n1, Node n2 ){ - std::vector< Node > children; - children.push_back( n1 ); - children.push_back( n2 ); - return mkAndSelectionFormula( children ); -} - -//if possible, returns a formula n' such that n' => ( n <=> polarity ), and n' is true in the current context, -// and NULL otherwise -Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){ - Trace("sel-form-debug") << "Looking for selection formula " << n << " " << polarity << std::endl; - Node ret; - if( n.getKind()==NOT ){ - ret = getSelectionFormula( fn[0], n[0], !polarity, useOption ); - }else if( n.getKind()==OR || n.getKind()==AND ){ - //whether we only need to find one or all - bool favorPol = ( n.getKind()!=AND && polarity ) || ( n.getKind()==AND && !polarity ); - std::vector< Node > children; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node fnc = fn[i]; - Node nc = n[i]; - Node nn = getSelectionFormula( fnc, nc, polarity, useOption ); - if( nn.isNull() && !favorPol ){ - //cannot make selection formula - children.clear(); - break; - } - if( !nn.isNull() ){ - //if( favorPol ){ //temporary - // return nn; // - //} // - if( std::find( children.begin(), children.end(), nn )==children.end() ){ - children.push_back( nn ); - } - } - } - if( !children.empty() ){ - if( favorPol ){ - //filter which formulas we wish to keep, make disjunction - Node min_lit; - int min_score = -1; - for( size_t i=0; igetValuation().hasSatValue( n, value ) ){ - if( value==polarity ){ - ret = fn; - if( !polarity ){ - ret = ret.negate(); - } - }else{ - Trace("sel-form-debug") << " (wrong polarity)" << std::endl; - } - }else{ - Trace("sel-form-debug") << " (does not have sat value)" << std::endl; - } - }else{ - Trace("sel-form-debug") << " (is not usable literal)" << std::endl; - } - } - Trace("sel-form-debug") << " return " << ret << std::endl; - return ret; -} - -int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){ - if( fn.getType().isBoolean() ){ - if( fn.getKind()==APPLY_UF ){ - Node op = fn.getOperator(); - //return total number of terms - return d_qe->getTermDatabase()->d_op_nonred_count[op]; - }else{ - int score = 0; - for( size_t i=0; iasFirstOrderModelIG(); - bool setDefaultVal = true; - Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); - //set the values in the model - for( size_t i=0; id_uf_terms[op].size(); i++ ){ - Node n = fmig->d_uf_terms[op][i]; - if( isTermActive( n ) ){ - Node v = fmig->getRepresentative( n ); - fmig->d_uf_model_gen[op].setValue( fm, n, v ); - } - //also possible set as default - if( d_term_selected.find( n )!=d_term_selected.end() || n==defaultTerm ){ - Node v = fmig->getRepresentative( n ); - fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); - if( n==defaultTerm ){ - setDefaultVal = false; - } - } - } - //set the overall default value if not set already (is this necessary??) - if( setDefaultVal ){ - Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); - fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); - } - fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] ); - d_uf_model_constructed[op] = true; -} - -bool QModelBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ - return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, true ); -} diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 3e4471fa4..7679cf93f 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -199,58 +199,6 @@ public: bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); } }; -class QModelBuilderInstGen : public QModelBuilderIG -{ -private: ///information for (new) InstGen - //map from quantifiers to their selection formulas - std::map< Node, Node > d_quant_selection_formula; - //map of terms that are selected - std::map< Node, bool > d_term_selected; - //a collection of (complete) InstMatch structures produced for each root quantifier - std::map< Node, inst::InstMatchTrie > d_sub_quant_inst_trie; - //for each quantifier, a collection of InstMatch structures, representing the children - std::map< Node, inst::InstMatchTrie > d_child_sub_quant_inst_trie; - //children quantifiers for each quantifier, each is an instance - std::map< Node, std::vector< Node > > d_sub_quants; - //instances of each partial instantiation with respect to the root - std::map< Node, InstMatch > d_sub_quant_inst; - //*root* parent of each partial instantiation - std::map< Node, Node > d_sub_quant_parent; -protected: - //reset - void reset( FirstOrderModel* fm ); - //initialize quantifiers, return number of lemmas produced, fp is the parent of quantifier f - int initializeQuantifier( Node f, Node fp ); - //analyze quantifier - void analyzeQuantifier( FirstOrderModel* fm, Node f ); - //do InstGen techniques for quantifier, return number of lemmas produced - int doInstGen( FirstOrderModel* fm, Node f ); - //theory-specific build models - void constructModelUf( FirstOrderModel* fm, Node op ); -private: - //get selection formula for quantifier body - Node getSelectionFormula( Node fn, Node n, bool polarity, int useOption ); - //get a heuristic score for a selection formula - int getSelectionFormulaScore( Node fn ); - //set selected terms in term - void setSelectedTerms( Node s ); - //is usable selection literal - bool isUsableSelectionLiteral( Node n, int useOption ); - //get parent quantifier match - void getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ); - //get parent quantifier - Node getParentQuantifier( Node f ) { return d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f]; } -public: - QModelBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} - ~QModelBuilderInstGen(){} - // is term selected - bool isTermSelected( Node n ) { return d_term_selected.find( n )!=d_term_selected.end(); } - /** exist instantiation ? */ - bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ); - //has inst gen - bool hasInstGen( Node f ) { return !d_quant_selection_formula[f].isNull(); } -}; - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 6ec347031..591034ffc 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -22,7 +22,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/full_model_check.h" -#include "theory/quantifiers/qinterval_builder.h" #include "theory/quantifiers/ambqi_builder.h" using namespace std; diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp index 9e4cab9fa..ebc1088a8 100644 --- a/src/theory/quantifiers/modes.cpp +++ b/src/theory/quantifiers/modes.cpp @@ -85,15 +85,9 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) case theory::quantifiers::MBQI_NONE: out << "MBQI_NONE"; break; - case theory::quantifiers::MBQI_INST_GEN: - out << "MBQI_INST_GEN"; - break; case theory::quantifiers::MBQI_FMC: out << "MBQI_FMC"; break; - case theory::quantifiers::MBQI_INTERVAL: - out << "MBQI_INTERVAL"; - break; case theory::quantifiers::MBQI_ABS: out << "MBQI_ABS"; break; diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index acc883f2a..80dbb783e 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -62,14 +62,10 @@ typedef enum { MBQI_GEN_EVAL, /** no mbqi */ MBQI_NONE, - /** implementation that mimics inst-gen */ - MBQI_INST_GEN, /** default, mbqi from Section 5.4.2 of AJR thesis */ MBQI_FMC, /** mbqi with integer intervals */ MBQI_FMC_INTERVAL, - /** mbqi with interval abstraction of uninterpreted sorts */ - MBQI_INTERVAL, /** abstract mbqi algorithm */ MBQI_ABS, /** mbqi trust (produce no instantiations) */ diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index c2afbbd3e..f01e563df 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -264,14 +264,10 @@ inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngi return MBQI_GEN_EVAL; } else if(optarg == "none") { return MBQI_NONE; - } else if(optarg == "instgen") { - return MBQI_INST_GEN; } else if(optarg == "default" || optarg == "fmc") { return MBQI_FMC; } else if(optarg == "fmc-interval") { return MBQI_FMC_INTERVAL; - } else if(optarg == "interval") { - return MBQI_INTERVAL; } else if(optarg == "abs") { return MBQI_ABS; } else if(optarg == "trust") { diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp deleted file mode 100644 index 5dd6316b3..000000000 --- a/src/theory/quantifiers/qinterval_builder.cpp +++ /dev/null @@ -1,1111 +0,0 @@ -/********************* */ -/*! \file qinterval_builder.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 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 qinterval builder - **/ - - -#include "theory/quantifiers/qinterval_builder.h" -#include "theory/quantifiers/term_database.h" - - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - -//lower bound is exclusive -//upper bound is inclusive - -struct QIntSort -{ - FirstOrderModelQInt * m; - bool operator() (Node i, Node j) { - return m->isLessThan( i, j ); - } -}; - -void QIntDef::init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u ) { - for( unsigned i=0; igetOrderedNumVars( q ); i++ ){ - l.push_back( Node::null() ); - u.push_back( m->getMaximum( m->getOrderedVarType( q, i ) ) ); - } -} - -void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u ) -{ - Trace(c) << "( "; - for( unsigned i=0; i0 ) Trace(c) << ", "; - //Trace(c) << l[i] << "..." << u[i]; - int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1; - int uindex = m->getRepId( u[i] ); - Trace(c) << lindex << "..." << uindex; - } - Trace(c) << " )"; -} - - -int QIntDef::getEvIndex( FirstOrderModelQInt * m, Node n, bool exc ) { - if( n.isNull() ){ - Assert( exc ); - return 0; - }else{ - int min = 0; - int max = (int)(d_def_order.size()-1); - while( min!=max ){ - int index = (min+max)/2; - Assert( index>=0 && index<(int)d_def_order.size() ); - if( n==d_def_order[index] ){ - max = index; - min = index; - }else if( m->isLessThan( n, d_def_order[index] ) ){ - max = index; - }else{ - min = index+1; - } - } - if( n==d_def_order[min] && exc ){ - min++; - } - Assert( min>=0 && min<(int)d_def_order.size() ); - if( ( min!=0 && !m->isLessThan( d_def_order[min-1], n ) && ( !exc || d_def_order[min-1]!=n ) ) || - ( ( exc || d_def_order[min]!=n ) && !m->isLessThan( n, d_def_order[min] ) ) ){ - Debug("qint-error") << "ERR size : " << d_def_order.size() << ", exc : " << exc << std::endl; - for( unsigned i=0; igetRepId( d_def_order[i] ) << std::endl; - } - Debug("qint-error") << " : " << n << " " << min << " " << m->getRepId( n ) << std::endl; - } - - Assert( min==0 || m->isLessThan( d_def_order[min-1], n ) || ( exc && d_def_order[min-1]==n ) ); - Assert( ( !exc && n==d_def_order[min] ) || m->isLessThan( n, d_def_order[min] ) ); - return min; - } -} - -void QIntDef::addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u, - Node v, unsigned depth ) { - if( depth==0 ){ - Trace("qint-compose-debug") << "Add entry "; - debugPrint( "qint-compose-debug", m, q, l, u ); - Trace("qint-compose-debug") << " -> " << v << "..." << std::endl; - } - //Assert( false ); - if( depth==u.size() ){ - Assert( d_def_order.empty() ); - Assert( v.isNull() || v.isConst() || ( v.getType().isSort() && m->getRepId( v )!=-1 ) ); - d_def_order.push_back( v ); - }else{ - /* - if( !d_def_order.empty() && - ( l[depth].isNull() || m->isLessThan( l[depth], d_def_order[d_def_order.size()-1] ) ) ){ - int startEvIndex = getEvIndex( m, l[depth], true ); - int endEvIndex; - if( m->isLessThan( u[depth], d_def_order[d_def_order.size()-1] ) ){ - endEvIndex = getEvIndex( m, u[depth] ); - }else{ - endEvIndex = d_def_order.size()-1; - } - Trace("qint-compose-debug2") << this << " adding for bounds " << l[depth] << "..." << u[depth] << std::endl; - for( int i=startEvIndex; i<=endEvIndex; i++ ){ - Trace("qint-compose-debug2") << this << " add entry " << d_def_order[i] << std::endl; - d_def[d_def_order[i]].addEntry( m, q, l, u, v, depth+1 ); - } - } - if( !d_def_order.empty() && - d_def.find(u[depth])==d_def.end() && - !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){ - Trace("qint-compose-debug2") << "Bad : depth : " << depth << std::endl; - } - Assert( d_def_order.empty() || - d_def.find(u[depth])!=d_def.end() || - m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ); - - if( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){ - Trace("qint-compose-debug2") << this << " add entry new : " << u[depth] << std::endl; - d_def_order.push_back( u[depth] ); - d_def[u[depth]].addEntry( m, q, l, u, v, depth+1 ); - } - */ - //%%%%%% - bool success = true; - int nnum = m->getVarOrder( q )->getNextNum( depth ); - Node pl; - Node pu; - if( nnum!=-1 ){ - Trace("qint-compose-debug2") << "...adding entry #" << depth << " is #" << nnum << std::endl; - //Assert( l[nnum].isNull() || l[nnum]==l[depth] || m->isLessThan( l[nnum], l[depth] ) ); - //Assert( u[nnum]==u[depth] || m->isLessThan( u[depth], u[nnum] ) ); - pl = l[nnum]; - pu = u[nnum]; - if( !m->doMeet( l[nnum], u[nnum], l[depth], u[depth], l[nnum], u[nnum] ) ){ - success = false; - } - } - //%%%%%% - if( success ){ - Node r = u[depth]; - if( d_def.find( r )!=d_def.end() ){ - d_def[r].addEntry( m, q, l, u, v, depth+1 ); - }else{ - if( !d_def_order.empty() && - !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){ - Trace("qint-compose-debug2") << "Bad : depth : " << depth << " "; - Trace("qint-compose-debug2") << d_def_order[d_def_order.size()-1] << " " << u[depth] << std::endl; - } - Assert( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], r ) ); - d_def_order.push_back( r ); - d_def[r].addEntry( m, q, l, u, v, depth+1 ); - } - } - if( nnum!=-1 ){ - l[nnum] = pl; - u[nnum] = pu; - } - } -} - -Node QIntDef::simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu, - unsigned depth ) { - if( d_def.empty() ){ - if( d_def_order.size()!=0 ){ - Debug("qint-error") << "Simplify, size = " << d_def_order.size() << std::endl; - } - Assert( d_def_order.size()==1 ); - return d_def_order[0]; - }else{ - Assert( !d_def_order.empty() ); - std::vector< Node > newDefs; - Node curr; - for( unsigned i=0; i0 ){ - if( n==curr && !n.isNull() ){ - d_def.erase( d_def_order[i-1] ); - }else{ - newDefs.push_back( d_def_order[i-1] ); - } - } - curr = n; - } - newDefs.push_back( d_def_order[d_def_order.size()-1] ); - d_def_order.clear(); - d_def_order.insert( d_def_order.end(), newDefs.begin(), newDefs.end() ); - return d_def_order.size()==1 ? curr : Node::null(); - } -} - -Node QIntDef::simplify( FirstOrderModelQInt * m, Node q ) { - std::vector< Node > l; - std::vector< Node > u; - if( !q.isNull() ){ - //init_vec( m, q, l, u ); - } - return simplify_r( m, q, l, u, 0 ); -} - -bool QIntDef::isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u, - unsigned depth ) { - if( d_def_order.empty() ){ - return false; - }else if( d_def.empty() ){ - return true; - }else{ - //get the current maximum - Node mx; - if( !q.isNull() ){ - int pnum = m->getVarOrder( q )->getPrevNum( depth ); - if( pnum!=-1 ){ - mx = u[pnum]; - } - } - if( mx.isNull() ){ - mx = m->getMaximum( d_def_order[d_def_order.size()-1].getType() ); - } - //if not current maximum - if( d_def_order[d_def_order.size()-1]!=mx ){ - return false; - }else{ - Node pu = u[depth]; - for( unsigned i=0; i l; - std::vector< Node > u; - if( !q.isNull() ){ - init_vec( m, q, l, u ); - } - return isTotal_r( m, q, l, u, 0 ); -} - -void QIntDef::construct_compose_r( FirstOrderModelQInt * m, Node q, - std::vector< Node >& l, std::vector< Node >& u, - Node n, QIntDef * f, - std::vector< Node >& args, - std::map< unsigned, QIntDef >& children, - std::map< unsigned, Node >& bchildren, - QIntVarNumIndex& vindex, unsigned depth ) { - //check for short circuit - if( !f ){ - if( !args.empty() ){ - if( ( n.getKind()==OR && args[args.size()-1]==m->d_true ) || - ( n.getKind()==AND && args[args.size()-1]==m->d_false ) ){ - addEntry( m, q, l, u, args[args.size()-1] ); - return; - } - } - } - - for( unsigned i=0; i0 ) Trace("qint-compose") << ", "; - //Trace("qint-compose") << l[i] << "..." << u[i]; - int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1; - int uindex = m->getRepId( u[i] ); - Trace( "qint-compose" ) << lindex << "..." << uindex; - } - Trace("qint-compose") << " )..."; - - //finished? - if( ( f && f->d_def.empty() ) || args.size()==n.getNumChildren() ){ - if( f ){ - Assert( f->d_def_order.size()==1 ); - Trace("qint-compose") << "UVALUE(" << f->d_def_order[0] << ")" << std::endl; - addEntry( m, q, l, u, f->d_def_order[0] ); - }else{ - Node nn; - bool nnSet = false; - for( unsigned i=0; imkConst( args[0]==args[1] ); - }else{ - //apply the operator to args - nn = NodeManager::currentNM()->mkNode( n.getKind(), args ); - nn = Rewriter::rewrite( nn ); - } - } - Trace("qint-compose") << "IVALUE(" << nn << ")" << std::endl; - addEntry( m, q, l, u, nn ); - Trace("qint-compose-debug2") << "...added entry." << std::endl; - } - }else{ - //if a non-simple child - if( children.find( depth )!=children.end() ){ - //*************************** - Trace("qint-compose") << "compound child, recurse" << std::endl; - std::vector< int > currIndex; - std::vector< int > endIndex; - std::vector< Node > prevL; - std::vector< Node > prevU; - std::vector< QIntDef * > visited; - do{ - Assert( currIndex.size()==visited.size() ); - - //populate the vectors - while( visited.size()getOrderedNumVars( q ) ){ - unsigned i = visited.size(); - QIntDef * qq = visited.empty() ? &children[depth] : visited[i-1]->getChild( currIndex[i-1] ); - visited.push_back( qq ); - Node qq_mx = qq->getMaximum(); - Trace("qint-compose-debug2") << "...Get ev indices " << i << " " << l[i] << " " << u[i] << std::endl; - currIndex.push_back( qq->getEvIndex( m, l[i], true ) ); - Trace("qint-compose-debug2") << "...Done get curr index " << currIndex[currIndex.size()-1] << std::endl; - if( m->isLessThan( qq_mx, u[i] ) ){ - endIndex.push_back( qq->getNumChildren()-1 ); - }else{ - endIndex.push_back( qq->getEvIndex( m, u[i] ) ); - } - Trace("qint-compose-debug2") << "...Done get end index " << endIndex[endIndex.size()-1] << std::endl; - prevL.push_back( l[i] ); - prevU.push_back( u[i] ); - if( !m->doMeet( prevL[i], prevU[i], - qq->getLower( currIndex[i] ), qq->getUpper( currIndex[i] ), l[i], u[i] ) ){ - Assert( false ); - } - } - for( unsigned i=0; igetChild( currIndex[activeIndex] ); - if( f ){ - int fIndex = f->getEvIndex( m, qa->getValue() ); - construct_compose_r( m, q, l, u, n, f->getChild( fIndex ), args, children, bchildren, vindex, depth+1 ); - }else{ - args.push_back( qa->getValue() ); - construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 ); - args.pop_back(); - } - - //increment the index (if possible) - while( activeIndex>=0 && currIndex[activeIndex]==endIndex[activeIndex] ){ - currIndex.pop_back(); - endIndex.pop_back(); - l[activeIndex] = prevL[activeIndex]; - u[activeIndex] = prevU[activeIndex]; - prevL.pop_back(); - prevU.pop_back(); - visited.pop_back(); - activeIndex--; - } - if( activeIndex>=0 ){ - for( unsigned i=0; idoMeet( prevL[activeIndex], prevU[activeIndex], - visited[activeIndex]->getLower( currIndex[activeIndex] ), - visited[activeIndex]->getUpper( currIndex[activeIndex] ), - l[activeIndex], u[activeIndex] ) ){ - Assert( false ); - } - } - }while( !visited.empty() ); - //*************************** - }else{ - Assert( bchildren.find( depth )!=bchildren.end() ); - Node v = bchildren[depth]; - if( f ){ - if( v.getKind()==BOUND_VARIABLE ){ - int vn = vindex.d_var_num[depth]; - Trace("qint-compose") << "variable #" << vn << ", recurse" << std::endl; - //int vn = m->getOrderedVarOccurId( q, n, depth ); - Trace("qint-compose-debug") << "-process " << v << ", which is var #" << vn << std::endl; - Node lprev = l[vn]; - Node uprev = u[vn]; - //restrict to last variable in order - int pnum = m->getVarOrder( q )->getPrevNum( vn ); - if( pnum!=-1 ){ - Trace("qint-compose-debug") << "-restrict to var #" << pnum << " " << l[pnum] << " " << u[pnum] << std::endl; - l[vn] = l[pnum]; - u[vn] = u[pnum]; - } - int startIndex = f->getEvIndex( m, l[vn], true ); - int endIndex = f->getEvIndex( m, u[vn] ); - Trace("qint-compose-debug") << "--will process " << startIndex << " " << endIndex << std::endl; - for( int i=startIndex; i<=endIndex; i++ ){ - if( m->doMeet( lprev, uprev, f->getLower( i ), f->getUpper( i ), l[vn], u[vn] ) ){ - construct_compose_r( m, q, l, u, n, f->getChild( i ), args, children, bchildren, vindex, depth+1 ); - }else{ - Assert( false ); - } - } - l[vn] = lprev; - u[vn] = uprev; - }else{ - Trace("qint-compose") << "value, recurse" << std::endl; - //simple - int ei = f->getEvIndex( m, v ); - construct_compose_r( m, q, l, u, n, f->getChild( ei ), args, children, bchildren, vindex, depth+1 ); - } - }else{ - Trace("qint-compose") << "value, recurse" << std::endl; - args.push_back( v ); - construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 ); - args.pop_back(); - } - } - } -} - - -void QIntDef::construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v ) { - if( depth==m->getOrderedNumVars( q ) ){ - Assert( !v.isNull() ); - d_def_order.push_back( v ); - }else{ - TypeNode tn = m->getOrderedVarType( q, depth ); - //int vnum = m->getVarOrder( q )->getVar( depth )== - if( depth==vn ){ - for( unsigned i=0; id_rep_set.d_type_reps[tn].size(); i++ ){ - Node vv = m->d_rep_set.d_type_reps[tn][i]; - d_def_order.push_back( vv ); - d_def[vv].construct_enum_r( m, q, vn, depth+1, vv ); - } - }else if( m->getVarOrder( q )->getVar( depth )==m->getVarOrder( q )->getVar( vn ) && depth>vn ){ - d_def_order.push_back( v ); - d_def[v].construct_enum_r( m, q, vn, depth+1, v ); - }else{ - Node mx = m->getMaximum( tn ); - d_def_order.push_back( mx ); - d_def[mx].construct_enum_r( m, q, vn, depth+1, v ); - } - } -} - -bool QIntDef::construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn ) { - TypeNode tn = m->getOrderedVarType( q, vn ); - if( tn.isSort() ){ - construct_enum_r( m, q, vn, 0, Node::null() ); - return true; - }else{ - return false; - } -} - -bool QIntDef::construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f, - std::map< unsigned, QIntDef >& children, - std::map< unsigned, Node >& bchildren, int varChCount, - QIntVarNumIndex& vindex ) { - Trace("qint-compose") << "Do " << (f ? "uninterpreted" : "interpreted"); - Trace("qint-compose") << " compose, var count = " << varChCount << "..." << std::endl; - std::vector< Node > l; - std::vector< Node > u; - init_vec( m, q, l, u ); - if( varChCount==0 || f ){ - //standard (no variable child) interpreted compose, or uninterpreted compose - std::vector< Node > args; - construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, 0 ); - }else{ - //special cases - bool success = false; - int varIndex = ( bchildren.find( 0 )!=bchildren.end() && bchildren[0].getKind()==BOUND_VARIABLE ) ? 0 : 1; - if( varChCount>1 ){ - if( n.getKind()==EQUAL ){ - //make it an enumeration - unsigned vn = vindex.d_var_num[0]; - if( children[0].construct_enum( m, q, vn ) ){ - bchildren.erase( 0 ); - varIndex = 1; - success = true; - } - } - }else{ - success = n.getKind()==EQUAL; - } - if( success ){ - int oIndex = varIndex==0 ? 1 : 0; - Node v = bchildren[varIndex]; - unsigned vn = vindex.d_var_num[varIndex]; - if( children.find( oIndex )==children.end() ){ - Assert( bchildren.find( oIndex )!=bchildren.end() ); - Node at = bchildren[oIndex]; - Trace("qint-icompose") << "Basic child, " << at << " with var " << v << std::endl; - Node prev = m->getPrev( bchildren[oIndex].getType(), bchildren[oIndex] ); - Node above = u[vn]; - if( !prev.isNull() ){ - u[vn] = prev; - addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) ); - } - l[vn] = prev; - u[vn] = at; - addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( true ) ); - if( at!=above ){ - l[vn] = at; - u[vn] = above; - addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) ); - } - }else{ - QIntDef * qid = &children[oIndex]; - qid->debugPrint("qint-icompose", m, q ); - Trace("qint-icompose") << " against variable..." << v << ", which is var #" << vn << std::endl; - - TypeNode tn = v.getType(); - QIntDefIter qdi( m, q, qid ); - while( !qdi.isFinished() ){ - std::vector< Node > us; - qdi.getUppers( us ); - std::vector< Node > ls; - qdi.getLowers( ls ); - qdi.debugPrint( "qint-icompose" ); - - Node n_below = ls[vn]; - Node n_prev = m->getPrev( tn, qdi.getValue() ); - Node n_at = qdi.getValue(); - Node n_above = us[vn]; - Trace("qint-icompose") << n_below << " < " << n_prev << " < " << n_at << " < " << n_above << std::endl; - if( n.getKind()==EQUAL ){ - bool atLtAbove = m->isLessThan( n_at, n_above ); - Node currL = n_below; - if( n_at==n_above || atLtAbove ){ - //add for value (at-1) - if( !n_prev.isNull() && ( n_below.isNull() || m->isLessThan( n_below, n_prev ) ) ){ - ls[vn] = currL; - us[vn] = n_prev; - currL = n_prev; - Trace("qint-icompose") << "-add entry(-) at " << ls[vn] << "..." << us[vn] << std::endl; - addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( false ) ); - } - //add for value (at) - if( ( n_below.isNull() || m->isLessThan( n_below, n_at ) ) && atLtAbove ){ - ls[vn] = currL; - us[vn] = n_at; - currL = n_at; - Trace("qint-icompose") << "-add entry(=) at " << ls[vn] << "..." << us[vn] << std::endl; - addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( true ) ); - } - } - ls[vn] = currL; - us[vn] = n_above; - Trace("qint-icompose") << "-add entry(+) at " << ls[vn] << "..." << us[vn] << std::endl; - addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( n_at==n_above ) ); - }else{ - return false; - } - qdi.increment(); - - Trace("qint-icompose-debug") << "Now : " << std::endl; - debugPrint("qint-icompose-debug", m, q ); - Trace("qint-icompose-debug") << std::endl; - } - } - - Trace("qint-icompose") << "Result : " << std::endl; - debugPrint("qint-icompose", m, q ); - Trace("qint-icompose") << std::endl; - - }else{ - return false; - } - } - Trace("qint-compose") << "Done i-compose" << std::endl; - return true; -} - - -void QIntDef::construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth ) { - d_def.clear(); - d_def_order.clear(); - Assert( !fapps.empty() ); - if( depth==fapps[0].getNumChildren() ){ - //get representative in model for this term - Assert( fapps.size()>=1 ); - Node r = m->getUsedRepresentative( fapps[0] ); - d_def_order.push_back( r ); - }else{ - std::map< Node, std::vector< Node > > fapp_child; - //partition based on evaluations of fapps[1][depth]....fapps[n][depth] - for( unsigned i=0; igetUsedRepresentative( fapps[i][depth] ); - fapp_child[r].push_back( fapps[i] ); - } - //sort by QIntSort - for( std::map< Node, std::vector< Node > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){ - d_def_order.push_back( it->first ); - } - QIntSort qis; - qis.m = m; - std::sort( d_def_order.begin(), d_def_order.end(), qis ); - //construct children - for( unsigned i=0; igetMaximum( d_def_order[i].getType() ); - } - Debug("qint-model-debug2") << "Construct for " << n << ", terms = " << fapp_child[n].size() << std::endl; - d_def[d_def_order[i]].construct( m, fapp_child[n], depth+1 ); - } - } -} - -Node QIntDef::getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth ) { - if( d_def.empty() ){ - Assert( d_def_order.size()==1 ); - //must convert to actual domain constant - if( d_def_order[0].getType().isSort() ){ - return m->d_rep_set.d_type_reps[ d_def_order[0].getType() ][ m->getRepId( d_def_order[0] ) ]; - }else{ - return m->getUsedRepresentative( d_def_order[0] ); - } - }else{ - TypeNode tn = vars[depth].getType(); - Node curr; - int rep_id = m->d_rep_set.getNumRepresentatives( tn ); - for( int i=(int)(d_def_order.size()-1); i>=0; i-- ){ - int curr_rep_id = i==0 ? 0 : m->getRepId( d_def_order[i-1] )+1; - Node ccurr = d_def[d_def_order[i]].getFunctionValue( m, vars, depth+1 ); - if( curr.isNull() ){ - curr = ccurr; - }else{ - std::vector< Node > c; - Assert( curr_rep_idd_rep_set.d_type_reps[tn][j] ) ); - } - Node cond = c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( OR, c ); - curr = NodeManager::currentNM()->mkNode( ITE, cond, ccurr, curr ); - } - rep_id = curr_rep_id; - } - return curr; - } -} - -Node QIntDef::evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth ) { - if( depth==reps.size() ){ - Assert( d_def_order.size()==1 ); - return d_def_order[0]; - }else{ - if( d_def.find( reps[depth] )!=d_def.end() ){ - return d_def[reps[depth]].evaluate_r( m, reps, depth+1 ); - }else{ - int ei = getEvIndex( m, reps[depth] ); - return d_def[d_def_order[ei]].evaluate_r( m, reps, depth+1 ); - } - } -} -Node QIntDef::evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth ) { - if( depth==n.getNumChildren() ){ - Assert( d_def_order.size()==1 ); - return d_def_order[0]; - }else{ - Node r = m->getUsedRepresentative( n[depth] ); - if( d_def.find( r )!=d_def.end() ){ - return d_def[r].evaluate_n_r( m, n, depth+1 ); - }else{ - int ei = getEvIndex( m, r ); - return d_def[d_def_order[ei]].evaluate_n_r( m, n, depth+1 ); - } - } -} - - - -QIntDef * QIntDef::getChild( unsigned i ) { - Assert( i l; - std::vector< Node > u; - getLowers( l ); - getUppers( u ); - QIntDef::debugPrint( c, d_fm, d_q, l, u ); - Trace( c ) << " -> " << getValue() << std::endl; -} - -void QIntDefIter::resetIndex( QIntDef * qid ){ - //std::cout << "check : " << qid << " " << qid->d_def_order.size() << " " << qid->d_def.size() << std::endl; - if( !qid->d_def.empty() ){ - //std::cout << "add to visited " << qid << std::endl; - d_index.push_back( 0 ); - d_index_visited.push_back( qid ); - resetIndex( qid->getChild( 0 ) ); - } -} - -bool QIntDefIter::increment( int index ) { - if( !isFinished() ){ - index = index==-1 ? (int)(d_index.size()-1) : index; - while( (int)(d_index.size()-1)>index ){ - //std::cout << "remove from visit 1 " << std::endl; - d_index.pop_back(); - d_index_visited.pop_back(); - } - while( index>=0 && d_index[index]>=(int)(d_index_visited[index]->d_def_order.size()-1) ){ - //std::cout << "remove from visit " << d_index_visited[ d_index_visited.size()-1 ] << std::endl; - d_index.pop_back(); - d_index_visited.pop_back(); - index--; - } - if( index>=0 ){ - //std::cout << "increment at index = " << index << std::endl; - d_index[index]++; - resetIndex( d_index_visited[index]->getChild( d_index[index] ) ); - return true; - }else{ - d_index.clear(); - return false; - } - }else{ - return false; - } -} - -Node QIntDefIter::getLower( int index ) { - if( d_index[index]==0 && !d_q.isNull() ){ - int pnum = d_fm->getVarOrder( d_q )->getPrevNum( index ); - if( pnum!=-1 ){ - return getLower( pnum ); - } - } - return d_index_visited[index]->getLower( d_index[index] ); -} - -Node QIntDefIter::getUpper( int index ) { - return d_index_visited[index]->getUpper( d_index[index] ); -} - -void QIntDefIter::getLowers( std::vector< Node >& reps ) { - for( unsigned i=0; igetVarOrder( d_q )->getPrevNum( i ); - if( pnum!=-1 ){ - added = true; - reps.push_back( reps[pnum] ); - } - } - if( !added ){ - reps.push_back( getLower( i ) ); - } - } -} - -void QIntDefIter::getUppers( std::vector< Node >& reps ) { - for( unsigned i=0; igetChild( d_index[d_index.size()-1] )->getValue(); -} - - -//------------------------variable ordering---------------------------- - -QuantVarOrder::QuantVarOrder( Node q ) : d_q( q ) { - d_var_count = 0; - initialize( q[1], 0, d_var_occur ); -} - -int QuantVarOrder::initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex ) { - if( n.getKind()!=FORALL ){ - //std::vector< Node > vars; - //std::vector< int > args; - int procVarOn = n.getKind()==APPLY_UF ? 0 : 1; - for( int r=0; r<=procVarOn; r++ ){ - for( unsigned i=0; i=minVarIndex ){ - occ_index = d_var_to_num[n[i]][j]; - } - } - if( occ_index==-1 ){ - //need to assign new - d_num_to_var[d_var_count] = n[i]; - if( !d_var_to_num[n[i]].empty() ){ - int v = d_var_to_num[n[i]][ d_var_to_num[n[i]].size()-1 ]; - d_num_to_prev_num[ d_var_count ] = v; - d_num_to_next_num[ v ] = d_var_count; - } - d_var_num_index[ d_var_count ] = d_var_to_num[n[i]].size(); - d_var_to_num[n[i]].push_back( d_var_count ); - occ_index = d_var_count; - d_var_count++; - } - vindex.d_var_num[i] = occ_index; - minVarIndex = occ_index; - }else if( r==0 ){ - minVarIndex = initialize( n[i], minVarIndex, vindex.d_var_index[i] ); - } - } - } - } - return minVarIndex; -} - -bool QuantVarOrder::getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u, - std::vector< Node >& inst ) { - Debug("qint-var-order-debug2") << "Get for " << d_q << " " << l.size() << " " << u.size() << std::endl; - for( unsigned i=0; igetMaximum( d_q[0][i].getType() ); - for( unsigned j=0; jdoMeet( l[index], u[index], cl, cu, ll, uu ) ){ - Debug("qint-var-order-debug2") << "FAILED" << std::endl; - return false; - } - Debug("qint-var-order-debug2") << "Result : " << ll << " " << uu << std::endl; - } - Debug("qint-var-order-debug2") << "Got " << uu << std::endl; - inst.push_back( uu ); - } - return true; -} - -void QuantVarOrder::debugPrint( const char * c ) { - Trace( c ) << "Variable order for " << d_q << " is : " << std::endl; - debugPrint( c, d_q[1], d_var_occur ); - Trace( c ) << std::endl; - for( unsigned i=0; i0 ) Trace( c ) << ","; - Trace( c ) << " "; - if( n[i].getKind()==BOUND_VARIABLE ){ - Trace(c) << "VAR[" << vindex.d_var_num[i] << "]"; - }else{ - debugPrint( c, n[i], vindex.d_var_index[i] ); - } - if( i==n.getNumChildren()-1 ) Trace( c ) << " "; - } - Trace(c) << ")"; - } -} - -QIntervalBuilder::QIntervalBuilder( context::Context* c, QuantifiersEngine* qe ) : -QModelBuilder( c, qe ){ - d_true = NodeManager::currentNM()->mkConst( true ); -} - - -//------------------------model construction---------------------------- - -void QIntervalBuilder::processBuildModel(TheoryModel* m, bool fullModel) { - Trace("fmf-qint-debug") << "process build model " << fullModel << std::endl; - FirstOrderModel* f = (FirstOrderModel*)m; - FirstOrderModelQInt* fm = f->asFirstOrderModelQInt(); - if( fullModel ){ - Trace("qint-model") << "Construct model representation..." << std::endl; - //make function values - for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - if( it->first.getType().getNumChildren()>1 ){ - Trace("qint-model") << "Construct for " << it->first << "..." << std::endl; - m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" ); - } - } - TheoryEngineModelBuilder::processBuildModel( m, fullModel ); - //mark that the model has been set - fm->markModelSet(); - //debug the model - debugModel( fm ); - }else{ - fm->initialize(); - //process representatives - fm->d_rep_id.clear(); - fm->d_max.clear(); - fm->d_min.clear(); - Trace("qint-model") << std::endl << "Making representatives..." << std::endl; - 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( it->second.empty() ){ - std::cout << "Empty rep for " << it->first << std::endl; - exit(0); - } - Trace("qint-model") << "Representatives for " << it->first << " : " << std::endl; - for( unsigned i=0; isecond.size(); i++ ){ - Trace("qint-model") << i << " : " << it->second[i] << std::endl; - fm->d_rep_id[it->second[i]] = i; - } - fm->d_min[it->first] = it->second[0]; - fm->d_max[it->first] = it->second[it->second.size()-1]; - }else{ - //TODO: enumerate? - } - } - Trace("qint-model") << std::endl << "Making function definitions..." << std::endl; - //construct the models for functions - for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node f = it->first; - Trace("qint-model-debug") << "Building Model for " << f << std::endl; - //reset the model - //get all (non-redundant) f-applications - std::vector< Node > fapps; - Trace("qint-model-debug") << "Initial terms: " << std::endl; - for( size_t i=0; id_uf_terms[f].size(); i++ ){ - Node n = fm->d_uf_terms[f][i]; - if( !n.getAttribute(NoMatchAttribute()) ){ - Trace("qint-model-debug") << " " << n << std::endl; - fapps.push_back( n ); - } - } - if( fapps.empty() ){ - //choose arbitrary value - Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f); - Trace("qint-model-debug") << "Initial terms empty, add " << mbt << std::endl; - fapps.push_back( mbt ); - } - //construct the interval model - it->second->construct( fm, fapps ); - Trace("qint-model-debug") << "Definition for " << f << " : " << std::endl; - it->second->debugPrint("qint-model-debug", fm, Node::null() ); - - it->second->simplify( fm, Node::null() ); - Trace("qint-model") << "(Simplified) definition for " << f << " : " << std::endl; - it->second->debugPrint("qint-model", fm, Node::null() ); - - if( Debug.isOn("qint-model-debug") ){ - for( size_t i=0; id_uf_terms[f].size(); i++ ){ - Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] ); - Debug("qint-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl; - Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) ); - } - } - } - } -} - - -//--------------------model checking--------------------------------------- - -//do exhaustive instantiation -bool QIntervalBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) { - Trace("qint-check") << "exhaustive instantiation " << q << " " << effort << std::endl; - if (effort==0) { - - FirstOrderModelQInt * fmqint = fm->asFirstOrderModelQInt(); - QIntDef qid; - doCheck( fmqint, q, qid, q[1], fmqint->d_var_order[q]->d_var_occur ); - //now process entries - Trace("qint-inst") << "Interpretation for " << q << " is : " << std::endl; - qid.debugPrint( "qint-inst", fmqint, q ); - Trace("qint-inst") << std::endl; - Debug("qint-check-debug2") << "Make iterator..." << std::endl; - QIntDefIter qdi( fmqint, q, &qid ); - while( !qdi.isFinished() ){ - if( qdi.getValue()!=d_true ){ - Debug("qint-check-debug2") << "Set up vectors..." << std::endl; - std::vector< Node > l; - std::vector< Node > u; - std::vector< Node > inst; - qdi.getLowers( l ); - qdi.getUppers( u ); - Debug("qint-check-debug2") << "Get instantiation..." << std::endl; - if( fmqint->d_var_order[q]->getInstantiation( fmqint, l, u, inst ) ){ - Trace("qint-inst") << "** Instantiate with "; - //just add the instance - for( unsigned j=0; jaddInstantiation( q, inst ) ){ - Trace("qint-inst") << " ...added instantiation." << std::endl; - d_addedLemmas++; - }else{ - Trace("qint-inst") << " ...duplicate instantiation" << std::endl; - //verify that instantiation is witness for current entry - if( Debug.isOn("qint-check-debug2") ){ - Debug("qint-check-debug2") << "Check if : "; - std::vector< Node > exp_inst; - for( unsigned i=0; igetOrderedNumVars( q ); i++ ){ - int index = fmqint->getOrderedVarNumToVarNum( q, i ); - exp_inst.push_back( inst[ index ] ); - Debug("qint-check-debug2") << inst[index] << " "; - } - Debug("qint-check-debug2") << " evaluates to " << qdi.getValue() << std::endl; - Assert( qid.evaluate( fmqint, exp_inst )==qdi.getValue() ); - } - } - }else{ - Trace("qint-inst") << "** Spurious instantiation." << std::endl; - } - } - qdi.increment(); - } - } - return true; -} - -bool QIntervalBuilder::doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n, - QIntVarNumIndex& vindex ) { - Assert( n.getKind()!=FORALL ); - std::map< unsigned, QIntDef > children; - std::map< unsigned, Node > bchildren; - int varChCount = 0; - for( unsigned i=0; ihasTerm( n[i] ) ){ - bchildren[i] = m->getUsedRepresentative( n[i] ); - }else{ - if( !doCheck( m, q, children[i], n[i], vindex.d_var_index[i] ) ){ - bchildren[i] = Node::null(); - } - } - } - Trace("qint-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl; - if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){ - Node op = n.getKind() == APPLY_UF ? n.getOperator() : n; - //uninterpreted compose - qid.construct_compose( m, q, n, m->d_models[op], children, bchildren, varChCount, vindex ); - }else if( !qid.construct_compose( m, q, n, NULL, children, bchildren, varChCount, vindex ) ){ - Trace("qint-check-debug") << "** Cannot produce definition for " << n << std::endl; - return false; - } - Trace("qint-check-debug2") << "Definition for " << n << " is : " << std::endl; - qid.debugPrint("qint-check-debug2", m, q); - qid.simplify( m, q ); - Trace("qint-check-debug") << "(Simplified) Definition for " << n << " is : " << std::endl; - qid.debugPrint("qint-check-debug", m, q); - Trace("qint-check-debug") << std::endl; - Assert( qid.isTotal( m, q ) ); - return true; -} diff --git a/src/theory/quantifiers/qinterval_builder.h b/src/theory/quantifiers/qinterval_builder.h deleted file mode 100644 index 7515f13c6..000000000 --- a/src/theory/quantifiers/qinterval_builder.h +++ /dev/null @@ -1,155 +0,0 @@ -/********************* */ -/*! \file qinterval_builder.h - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief qinterval model class - **/ - -#include "cvc4_private.h" - -#ifndef QINTERVAL_BUILDER -#define QINTERVAL_BUILDER - -#include "theory/quantifiers/model_builder.h" -#include "theory/quantifiers/first_order_model.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class FirstOrderModelQInt; - -class QIntVarNumIndex -{ -public: - std::map< int, int > d_var_num; - std::map< int, QIntVarNumIndex > d_var_index; -}; - -class QIntDef -{ -private: - Node evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth ); - Node evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth ); - void construct_compose_r( FirstOrderModelQInt * m, Node q, - std::vector< Node >& l, std::vector< Node >& u, Node n, QIntDef * f, - std::vector< Node >& args, - std::map< unsigned, QIntDef >& children, - std::map< unsigned, Node >& bchildren, - QIntVarNumIndex& vindex, - unsigned depth ); - - void construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v ); - int getEvIndex( FirstOrderModelQInt * m, Node n, bool exc = false ); - void addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u, - Node v, unsigned depth = 0 ); - Node simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu, - unsigned depth ); - bool isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu, - unsigned depth ); -public: - QIntDef(){} - std::map< Node, QIntDef > d_def; - std::vector< Node > d_def_order; - - void construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth = 0 ); - bool construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f, - std::map< unsigned, QIntDef >& children, - std::map< unsigned, Node >& bchildren, int varChCount, - QIntVarNumIndex& vindex ); - bool construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn ); - - Node evaluate( FirstOrderModelQInt * m, std::vector< Node >& reps ) { return evaluate_r( m, reps, 0 ); } - Node evaluate_n( FirstOrderModelQInt * m, Node n ) { return evaluate_n_r( m, n, 0 ); } - - void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t = 0 ); - QIntDef * getChild( unsigned i ); - Node getValue() { return d_def_order[0]; } - Node getLower( unsigned i ) { return i==0 ? Node::null() : d_def_order[i-1]; } - Node getUpper( unsigned i ) { return d_def_order[i]; } - Node getMaximum() { return d_def_order.empty() ? Node::null() : getUpper( d_def_order.size()-1 ); } - int getNumChildren() { return d_def_order.size(); } - bool isTotal( FirstOrderModelQInt * m, Node q ); - - Node simplify( FirstOrderModelQInt * m, Node q ); - Node getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth = 0 ); - - static void init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u ); - static void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u ); -}; - -class QIntDefIter { -private: - FirstOrderModelQInt * d_fm; - Node d_q; - void resetIndex( QIntDef * qid ); -public: - QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid ); - void debugPrint( const char * c, int t = 0 ); - std::vector< QIntDef * > d_index_visited; - std::vector< int > d_index; - bool isFinished() { return d_index.empty(); } - bool increment( int index = -1 ); - unsigned getSize() { return d_index.size(); } - Node getLower( int index ); - Node getUpper( int index ); - void getLowers( std::vector< Node >& reps ); - void getUppers( std::vector< Node >& reps ); - Node getValue(); -}; - - -class QuantVarOrder -{ -private: - int initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex ); - int d_var_count; - Node d_q; - void debugPrint( const char * c, Node n, QIntVarNumIndex& vindex ); -public: - QuantVarOrder( Node q ); - std::map< int, Node > d_num_to_var; - std::map< int, int > d_num_to_prev_num; - std::map< int, int > d_num_to_next_num; - std::map< Node, std::vector< int > > d_var_to_num; - std::map< int, int > d_var_num_index; - //std::map< Node, std::map< int, int > > d_var_occur; - //int getVarNum( Node n, int arg ) { return d_var_occur[n][arg]; } - unsigned getNumVars() { return d_var_count; } - Node getVar( int i ) { return d_num_to_var[i]; } - int getPrevNum( int i ) { return d_num_to_prev_num.find( i )!=d_num_to_prev_num.end() ? d_num_to_prev_num[i] : -1; } - int getNextNum( int i ) { return d_num_to_next_num.find( i )!=d_num_to_next_num.end() ? d_num_to_next_num[i] : -1; } - int getVarNumIndex( int i ) { return d_var_num_index[i]; } - bool getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u, - std::vector< Node >& inst ); - void debugPrint( const char * c ); - QIntVarNumIndex d_var_occur; -}; - -class QIntervalBuilder : public QModelBuilder -{ -private: - Node d_true; - bool doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n, - QIntVarNumIndex& vindex ); -public: - QIntervalBuilder( context::Context* c, QuantifiersEngine* qe ); - //process build model - void processBuildModel(TheoryModel* m, bool fullModel); - //do exhaustive instantiation - bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ); -}; - - -} -} -} - -#endif \ No newline at end of file diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index b21494f77..9a4961e2c 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -416,7 +416,7 @@ void TermDb::reset( Theory::Effort effort ){ } } Trace("term-db-stats") << "TermDb: Reset" << std::endl; - Trace("term-db-stats") << "Congruent/Non-Congruent/Non-Relevant = "; + Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = "; Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; if( Debug.isOn("term-db") ){ Debug("term-db") << "functions : " << std::endl; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index eabba85bf..c10992435 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -34,7 +34,6 @@ #include "theory/uf/options.h" #include "theory/uf/theory_uf.h" #include "theory/quantifiers/full_model_check.h" -#include "theory/quantifiers/qinterval_builder.h" #include "theory/quantifiers/ambqi_builder.h" using namespace std; @@ -91,8 +90,6 @@ d_lemmas_produced_c(u){ options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() || options::mbqiMode()==quantifiers::MBQI_TRUST ){ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); - }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ - d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" ); }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" ); }else{ @@ -163,15 +160,9 @@ d_lemmas_produced_c(u){ options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBoundInt() ){ Trace("quant-engine-debug") << "...make fmc builder." << std::endl; d_builder = new quantifiers::fmcheck::FullModelChecker( c, this ); - }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ - Trace("quant-engine-debug") << "...make interval builder." << std::endl; - d_builder = new quantifiers::QIntervalBuilder( c, this ); }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl; d_builder = new quantifiers::AbsMbqiBuilder( c, this ); - }else if( options::mbqiMode()==quantifiers::MBQI_INST_GEN ){ - Trace("quant-engine-debug") << "...make inst-gen builder." << std::endl; - d_builder = new quantifiers::QModelBuilderInstGen( c, this ); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; d_builder = new quantifiers::QModelBuilderDefault( c, this ); @@ -676,6 +667,7 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) { return getInstantiation( f, d_term_db->d_inst_constants[f], terms ); } +/* bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ if( options::incrementalSolving() ){ if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){ @@ -696,6 +688,7 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b } return false; } +*/ bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ if( doCache ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index f56cd0d19..199fe79b9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -256,7 +256,7 @@ public: /** do substitution */ Node getSubstitute( Node n, std::vector< Node >& terms ); /** exist instantiation ? */ - bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ); + //bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ); /** add lemma lem */ bool addLemma( Node lem, bool doCache = true ); /** add require phase */ -- 2.30.2