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 \
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 \
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 );
}
#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"
}
-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<Node, QIntDef * >::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<tno.getNumChildren(); i++) {
- //make sure a representative of the type exists
- if( !d_rep_set.hasType( tno[i] ) ){
- Node e = getSomeDomainElement( tno[i] );
- Trace("qint-debug") << " * Initialize type " << tno[i] << ", add ";
- Trace("qint-debug") << e << " " << e.getType() << std::endl;
- //d_rep_set.add( e );
- }
- }
- }
- }
-}
-
-Node FirstOrderModelQInt::getFunctionValue(Node op, const char* argPrefix ) {
- Trace("qint-debug") << "Get function value for " << op << std::endl;
- TypeNode type = op.getType();
- std::vector< Node > vars;
- for( size_t i=0; i<type.getNumChildren()-1; i++ ){
- std::stringstream ss;
- ss << argPrefix << (i+1);
- Node b = NodeManager::currentNM()->mkBoundVar( 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<rid2;
- }else{
- return false;
- }
-}
-
-Node FirstOrderModelQInt::getMin( Node v1, Node v2 ) {
- return isLessThan( v1, v2 ) ? v1 : v2;
-}
-
-Node FirstOrderModelQInt::getMax( Node v1, Node v2 ) {
- return isLessThan( v1, v2 ) ? v2 : v1;
-}
-
-Node FirstOrderModelQInt::getMaximum( TypeNode tn ) {
- return d_max[tn];
-}
-
-Node FirstOrderModelQInt::getNext( TypeNode tn, Node v ) {
- if( v.isNull() ){
- return d_min[tn];
- }else{
- Assert( getRepId( v )!=-1 );
- int rid = d_rep_id[v];
- if( rid==(int)(d_rep_set.d_type_reps[tn].size()-1) ){
- Assert( false );
- return Node::null();
- }else{
- return d_rep_set.d_type_reps[tn][ rid+1 ];
- }
- }
-}
-Node FirstOrderModelQInt::getPrev( TypeNode tn, Node v ) {
- if( v.isNull() ){
- Assert( false );
- return Node::null();
- }else{
- Assert( getRepId( v )!=-1 );
- int rid = d_rep_id[v];
- if( rid==0 ){
- return Node::null();
- }else{
- return d_rep_set.d_type_reps[tn][ rid-1 ];
- }
- }
-}
-
-bool FirstOrderModelQInt::doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur ) {
- Trace("qint-debug2") << "doMeet " << l1 << "..." << u1 << " with " << l2 << "..." << u2 << std::endl;
- Assert( !u1.isNull() );
- Assert( !u2.isNull() );
- lr = l1.isNull() ? l2 : ( l2.isNull() ? l1 : getMax( l1, l2 ) );
- ur = getMin( u1, u2 );
- //return lr==ur || lr.isNull() || isLessThan( lr, ur );
- return lr.isNull() || isLessThan( lr, ur );
-}
-
-
-
FirstOrderModelAbs::FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name) :
FirstOrderModel(qe, c, name) {
}/* CVC4::theory::quantifiers::fmcheck namespace */
-
-class QIntDef;
-class QuantVarOrder;
-class FirstOrderModelQInt : public FirstOrderModel
-{
- friend class QIntervalBuilder;
-private:
- /** uf op to some representation */
- std::map<Node, QIntDef * > 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<Node, QuantVarOrder * > 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
+++ /dev/null
-/********************* */
-/*! \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; i<n.getNumChildren(); i++ ){
- if( n[i].getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr(n[i]) ){
- d_children.push_back( InstGenProcess( n[i] ) );
- d_children_index.push_back( i );
- d_children_map[ i ] = count;
- count++;
- }
- if( n[i].getKind()==INST_CONSTANT ){
- d_var_num[i] = n[i].getAttribute(InstVarNumAttribute());
- }
- }
-}
-
-void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){
- if( !qe->existsInstantiation( 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; i<newUseConsider.size(); i++ ){
- newUseConsider[i] = false;
- }
-#endif
- for( size_t i=0; i<considerVal.size(); i++ ){
- eq::EqClassIterator eqc( qe->getEqualityQuery()->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; i<considerTerms.size(); i++ ){
- Node n = considerTerms[i];
- bool isSelected = ((QModelBuilderIG*)qe->getModelBuilder())->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; j<d_node.getNumChildren(); j++ ){
- if( d_children_map.find( j )==d_children_map.end() ){
- if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){
- if( d_node[j].getKind()==INST_CONSTANT ){
- if( !considerTermsMatch[t][n].set( qe, d_var_num[j], n[j] ) ){
- Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to ";
- Trace("inst-gen-cm") << considerTermsMatch[t][n].get( d_var_num[j] ) << std::endl;
- considerTermsSuccess[t][n] = false;
- break;
- }
- }else if( !qe->getEqualityQuery()->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; k<d_children.size(); k++ ){
- if( newUseConsider[k] ){
- int childIndex = d_children_index[k];
- //determine if we are restricted or not
- if( t!=0 || !n[childIndex].getAttribute(ModelBasisAttribute()) ){
- Node r = qe->getModel()->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; i<newConsiderVal.size(); i++ ){
- newConsiderVal[i].push_back( ncv );
- }
- //instead we will do a sum
- if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol ) ){
- doProduct = false;
- }
- }else{
- //do not use consider
- for( size_t i=0; i<newUseConsider.size(); i++ ){
- newUseConsider[i] = false;
- }
- }
- }
- }
- }
-
- //calculate all matches for children
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i].calculateMatches( qe, f, newConsiderVal[i], newUseConsider[i] );
- if( doProduct && d_children[i].getNumMatches()==0 ){
- return;
- }
- }
- if( d_node.getKind()==APPLY_UF ){
- //if this is an uninterpreted function
- Node op = d_node.getOperator();
- //process all values
- for( size_t i=0; i<considerTerms.size(); i++ ){
- Node n = considerTerms[i];
- bool isSelected = ((QModelBuilderIG*)qe->getModelBuilder())->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();
- }
- }
- }
- }
-}
+++ /dev/null
-/********************* */
-/*! \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 */
#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"
}
-
-
-////////////////////// 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; i<d_sub_quants[f].size(); i++ ){
- addedLemmas += initializeQuantifier( d_sub_quants[f][i], fp );
- }
- return addedLemmas;
-}
-
-void QModelBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){
- //Node fp = getParentQuantifier( f );//*
- //bool quantRedundant = ( f!=fp && d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) );
- //if( f==fp || d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ){//*
- Trace("sel-form-debug") << "* Analyze " << f << std::endl;
- //determine selection formula, set terms in selection formula as being selected
- Node s = getSelectionFormula( d_qe->getTermDatabase()->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; i<d_sub_quants[f].size(); i++ ){
- analyzeQuantifier( fm, d_sub_quants[f][i] );
- }
- }
-}
-
-
-int QModelBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
- int addedLemmas = 0;
- if( d_quant_sat.find( f )==d_quant_sat.end() ){
- Node fp = d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f];
- if( fp!=f ) Trace("inst-gen") << " ";
- Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl;
- if( fp!=f ) Trace("inst-gen") << " ";
- Trace("inst-gen") << "Sel Form : " << d_quant_selection_formula[f] << std::endl;
- //we wish to add all known exceptions to our selection formula for f. this will help to refine our current model.
- if( !d_quant_selection_formula[f].isNull() ){
- //first, try on sub quantifiers
- bool subQuantSat = true;
- for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
- addedLemmas += doInstGen( fm, d_sub_quants[f][i] );
- if( d_quant_sat.find( d_sub_quants[f][i] )==d_quant_sat.end() ){
- subQuantSat = false;
- }
- }
- if( addedLemmas>0 || !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; i<igp.getNumMatches(); i++ ){
- //if the match is not already true in the model
- if( igp.getMatchValue( i )!=fm->d_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; i<children.size(); i++ ){
- if( children[i].getKind()==AND ){
- for( size_t j=0; j<children[i].getNumChildren(); j++ ){
- ch.push_back( children[i][j] );
- }
- }else{
- ch.push_back( children[i] );
- }
- }
- return NodeManager::currentNM()->mkNode( 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; i<children.size(); i++ ){
- //if it is constant apply uf application, return it for sure
- if( hasConstantDefinition( children[i] ) ){
- min_lit = children[i];
- break;
- }else{
- int score = getSelectionFormulaScore( children[i] );
- if( min_score<0 || score<min_score ){
- min_score = score;
- min_lit = children[i];
- }
- }
- }
- //currently just return the best single literal
- ret = min_lit;
- }else{
- //selection formula must be conjunction of children
- ret = mkAndSelectionFormula( children );
- }
- }else{
- ret = Node::null();
- }
- }else if( n.getKind()==ITE ){
- Node nn;
- Node nc[2];
- //get selection formula for the
- for( int i=0; i<2; i++ ){
- nn = getSelectionFormula( fn[0], n[0], i==0, useOption );
- nc[i] = getSelectionFormula( fn[i+1], n[i+1], polarity, useOption );
- if( !nn.isNull() && !nc[i].isNull() ){
- ret = mkAndSelectionFormula( nn, nc[i] );
- break;
- }
- }
- if( ret.isNull() && !nc[0].isNull() && !nc[1].isNull() ){
- ret = mkAndSelectionFormula( nc[0], nc[1] );
- }
- }else if( n.getKind()==IFF ){
- bool opPol = !polarity;
- for( int p=0; p<2; p++ ){
- Node nn[2];
- for( int i=0; i<2; i++ ){
- bool pol = i==0 ? p==0 : ( opPol ? p!=0 : p==0 );
- nn[i] = getSelectionFormula( fn[i], n[i], pol, useOption );
- if( nn[i].isNull() ){
- break;
- }
- }
- if( !nn[0].isNull() && !nn[1].isNull() ){
- ret = mkAndSelectionFormula( nn[0], nn[1] );
- }
- }
- }else{
- //literal case
- //first, check if it is a usable selection literal
- if( isUsableSelectionLiteral( n, useOption ) ){
- bool value;
- if( d_qe->getValuation().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; i<fn.getNumChildren(); i++ ){
- score += getSelectionFormulaScore( fn[i] );
- }
- return score;
- }
- }else{
- return 0;
- }
-}
-
-void QModelBuilderInstGen::setSelectedTerms( Node s ){
-
- //if it is apply uf and has model basis arguments, then mark term as being "selected"
- if( s.getKind()==APPLY_UF ){
- Assert( s.hasAttribute(ModelBasisArgAttribute()) );
- if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl;
- if( s.getAttribute(ModelBasisArgAttribute())!=0 ){
- d_term_selected[ s ] = true;
- Trace("sel-form-term") << " " << s << " is a selected term." << std::endl;
- }
- }
- for( int i=0; i<(int)s.getNumChildren(); i++ ){
- setSelectedTerms( s[i] );
- }
-}
-
-bool QModelBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){
- if( n.getKind()==FORALL ){
- return false;
- }else if( n.getKind()!=APPLY_UF ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- //if it is a variable, then return false
- if( n[i].getAttribute(ModelBasisAttribute()) ){
- return false;
- }
- }
- }
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( !isUsableSelectionLiteral( n[i], useOption ) ){
- return false;
- }
- }
- return true;
-}
-
-void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){
- if( f!=fp ){
- //std::cout << "gpqm " << fp << " " << f << " " << m << std::endl;
- //std::cout << " " << fp[0].getNumChildren() << " " << f[0].getNumChildren() << std::endl;
- int counter = 0;
- for( size_t i=0; i<fp[0].getNumChildren(); i++ ){
- if( (int)counter< (int)f[0].getNumChildren() ){
- if( fp[0][i]==f[0][counter] ){
- Node n = m.get( counter );
- if( !n.isNull() ){
- mp.set( d_qe, i, n );
- }
- counter++;
- }
- }
- }
- mp.add( d_sub_quant_inst[f] );
- }else{
- mp.add( m );
- }
-}
-
-void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){
- FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
- bool setDefaultVal = true;
- Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
- //set the values in the model
- for( size_t i=0; i<fmig->d_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 );
-}
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 */
#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;
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;
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) */
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") {
+++ /dev/null
-/********************* */
-/*! \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; i<m->getOrderedNumVars( 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; i<l.size(); i++ ){
- if( i>0 ) 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; i<d_def_order.size(); i++ ){
- Debug("qint-error") << "ERR ch #" << i << " : " << d_def_order[i];
- Debug("qint-error") << " " << m->getRepId( 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; i<d_def_order.size(); i++ ){
- Node n = d_def[d_def_order[i]].simplify_r( m, q, il, iu, depth+1 );
- if( i>0 ){
- 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<d_def_order.size(); i++ ){
- u[depth] = d_def_order[i];
- if( !d_def[d_def_order[i]].isTotal_r( m, q, l, u, depth+1 ) ){
- return false;
- }
- }
- u[depth] = pu;
- return true;
- }
- }
-}
-
-bool QIntDef::isTotal( FirstOrderModelQInt * m, Node q ) {
- std::vector< Node > 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; i<depth; i++ ) { Trace("qint-compose") << " "; }
- Trace("qint-compose") << (f ? "U" : "I" ) << "C( ";
- for( unsigned i=0; i<l.size(); i++ ){
- if( i>0 ) 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; i<args.size(); i++ ){
- if( args[i].isNull() ){
- nnSet = true;
- break;
- }
- }
- if( !nnSet ){
- if( n.getKind()==EQUAL ){
- nn = NodeManager::currentNM()->mkConst( 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()<m->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; i<depth; i++ ) { Trace("qint-compose") << " "; }
- for( unsigned i=0; i<currIndex.size(); i++ ){
- Trace("qint-compose") << "[" << currIndex[i] << "/" << endIndex[i] << "]";
- }
- Trace("qint-compose") << std::endl;
- //consider the current
- int activeIndex = visited.size()-1;
- QIntDef * qa = visited.empty() ? &children[depth] : visited[activeIndex]->getChild( 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; i<depth; i++ ) { Trace("qint-compose") << " "; }
- Trace("qint-compose-debug") << "Increment at " << activeIndex << std::endl;
- currIndex[activeIndex]++;
- if( !m->doMeet( 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; i<m->d_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; i<fapps.size(); i++ ){
- Node r = m->getUsedRepresentative( 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; i<d_def_order.size(); i++ ){
- Node n = d_def_order[i];
- if( i==d_def_order.size()-1 ){
- d_def_order[i] = m->getMaximum( 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_id<rep_id );
- for( int j=curr_rep_id; j<rep_id; j++ ){
- c.push_back( vars[depth].eqNode( m->d_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<d_def_order.size() );
- Assert( d_def.find( d_def_order[i] )!=d_def.end() );
- return &d_def[ d_def_order[i] ];
-}
-
-void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t ) {
- /*
- for( unsigned i=0; i<d_def_order.size(); i++ ){
- for( int j=0; j<t; j++ ) { Trace(c) << " "; }
- //Trace(c) << this << " ";
- Trace(c) << d_def_order[i] << " : " << std::endl;
- if( d_def.find( d_def_order[i] )!=d_def.end() ){
- d_def[d_def_order[i]].debugPrint( c, m, t+1 );
- }
- }
- */
- //if( t==0 ){
- QIntDefIter qdi( m, q, this );
- while( !qdi.isFinished() ){
- qdi.debugPrint( c, t );
- qdi.increment();
- }
- //}
-}
-
-
-QIntDefIter::QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid ) : d_fm( m ), d_q( q ){
- resetIndex( qid );
-}
-
-void QIntDefIter::debugPrint( const char * c, int t ) {
- //Trace( c ) << getSize() << " " << d_index_visited.size() << " ";
- for( int j=0; j<t; j++ ) { Trace(c) << " "; }
- std::vector< Node > 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; i<getSize(); i++ ){
- bool added = false;
- if( d_index[i]==0 && !d_q.isNull() ){
- int pnum = d_fm->getVarOrder( 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; i<getSize(); i++ ){
- reps.push_back( getUpper( i ) );
- }
-}
-
-Node QIntDefIter::getValue() {
- return d_index_visited[ d_index_visited.size()-1 ]->getChild( 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<n.getNumChildren(); i++ ){
- if( n[i].getKind()==BOUND_VARIABLE && r==procVarOn ){
- int occ_index = -1;
- for( unsigned j=0; j<d_var_to_num[n[i]].size(); j++ ){
- if( d_var_to_num[n[i]][j]>=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; i<d_q[0].getNumChildren(); i++ ){
- Debug("qint-var-order-debug2") << "Get for " << d_q[0][i] << " " << d_var_to_num[d_q[0][i]].size() << std::endl;
- Node ll = Node::null();
- Node uu = m->getMaximum( d_q[0][i].getType() );
- for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){
- Debug("qint-var-order-debug2") << "Go " << j << std::endl;
- Node cl = ll;
- Node cu = uu;
- int index = d_var_to_num[d_q[0][i]][j];
- Debug("qint-var-order-debug2") << "Do meet for " << index << "..." << std::endl;
- Debug("qint-var-order-debug2") << l[index] << " " << u[index] << " " << cl << " " << cu << std::endl;
- if( !m->doMeet( 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; i<d_q[0].getNumChildren(); i++ ){
- Trace( c ) << d_q[0][i] << " : ";
- for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){
- Trace( c ) << d_var_to_num[d_q[0][i]][j] << " ";
- }
- Trace( c ) << std::endl;
- }
-}
-
-void QuantVarOrder::debugPrint( const char * c, Node n, QIntVarNumIndex& vindex ) {
- if( n.getKind()==FORALL ){
- Trace(c) << "NESTED_QUANT";
- }else{
- Trace(c) << n.getKind() << "(";
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( i>0 ) 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<Node, QIntDef * >::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; i<it->second.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<Node, QIntDef * >::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; i<fm->d_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; i<fm->d_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; j<inst.size(); j++) {
- Trace("qint-inst") << inst[j] << " ";
- }
- Trace("qint-inst") << std::endl;
- d_triedLemmas++;
- if( d_qe->addInstantiation( 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; i<fmqint->getOrderedNumVars( 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; i<n.getNumChildren(); i++ ){
- if( n[i].getKind()==FORALL ){
- bchildren[i] = Node::null();
- }else if( n[i].getKind() == BOUND_VARIABLE ){
- varChCount++;
- bchildren[i] = n[i];
- }else if( m->hasTerm( 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;
-}
+++ /dev/null
-/********************* */
-/*! \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
}
}
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;
#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;
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{
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 );
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() ){
}
return false;
}
+*/
bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
if( doCache ){
/** 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 */
projects / cvc5.git / commitdiff