diff options
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r--[-rwxr-xr-x] | src/theory/quantifiers/inst_strategy_cbqi.cpp | 810 |
1 files changed, 405 insertions, 405 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index ddf763b73..b12fed619 100755..100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -1,405 +1,405 @@ -/********************* */
-/*! \file inst_strategy_cbqi.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 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 cbqi instantiation strategies
- **/
-
-#include "theory/quantifiers/inst_strategy_cbqi.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.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;
-using namespace CVC4::theory::arith;
-using namespace CVC4::theory::datatypes;
-
-#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
-
-InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :
- InstStrategy( ie ), d_th( th ), d_counter( 0 ){
- d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
-}
-
-bool InstStrategySimplex::calculateShouldProcess( Node f ){
- //DO_THIS
- return false;
-}
-
-void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
- Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
- d_instRows.clear();
- d_tableaux_term.clear();
- d_tableaux.clear();
- d_ceTableaux.clear();
- //search for instantiation rows in simplex tableaux
- ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap;
- ArithVarNodeMap::var_iterator vi, vend;
- for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
- ArithVar x = *vi;
- if( d_th->d_partialModel.hasEitherBound( x ) ){
- Node n = avnm.asNode(x);
- Node f;
- NodeBuilder<> t(kind::PLUS);
- if( n.getKind()==PLUS ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- addTermToRow( x, n[i], f, t );
- }
- }else{
- addTermToRow( x, n, f, t );
- }
- if( f!=Node::null() ){
- d_instRows[f].push_back( x );
- //this theory has constraints from f
- Debug("quant-arith") << "Has constraints from " << f << std::endl;
- //set that we should process it
- d_quantActive[ f ] = true;
- //set tableaux term
- if( t.getNumChildren()==0 ){
- d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );
- }else if( t.getNumChildren()==1 ){
- d_tableaux_term[x] = t.getChild( 0 );
- }else{
- d_tableaux_term[x] = t;
- }
- }
- }
- }
- //print debug
- debugPrint( "quant-arith-debug" );
- d_counter++;
-}
-
-int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
- if( e<2 ){
- return STATUS_UNFINISHED;
- }else if( e==2 ){
- //Notice() << f << std::endl;
- //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;
- //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;
- Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl;
- for( int j=0; j<(int)d_instRows[f].size(); j++ ){
- ArithVar x = d_instRows[f][j];
- if( !d_ceTableaux[x].empty() ){
- Debug("quant-arith-simplex") << "Check row " << x << std::endl;
- //instantiation row will be A*e + B*t = beta,
- // where e is a vector of terms , and t is vector of ground terms.
- // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
- // We will construct the term ( beta - B*t)/coeff to use for e_i.
- InstMatch m;
- //By default, choose the first instantiation constant to be e_i.
- Node var = d_ceTableaux[x].begin()->first;
- if( var.getType().isInteger() ){
- std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();
- //try to find coefficent that is +/- 1
- while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){
- ++it;
- if( it==d_ceTableaux[x].end() ){
- var = Node::null();
- }else{
- var = it->first;
- }
- }
- //otherwise, try one that divides all ground term coefficients? DO_THIS
- }
- if( !var.isNull() ){
- Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
- doInstantiation( f, d_tableaux_term[x], x, m, var );
- }else{
- Debug("quant-arith-simplex") << "Could not find var." << std::endl;
- }
- ////choose a new variable based on alternation strategy
- //int index = d_counter%(int)d_th->d_ceTableaux[x].size();
- //Node var;
- //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){
- // if( index==0 ){
- // var = it->first;
- // break;
- // }
- // index--;
- //}
- //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );
- }
- }
- }
- return STATUS_UNKNOWN;
-}
-
-
-void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
- if( n.getKind()==MULT ){
- if( n[1].hasAttribute(InstConstantAttribute()) ){
- f = n[1].getAttribute(InstConstantAttribute());
- if( n[1].getKind()==INST_CONSTANT ){
- d_ceTableaux[x][ n[1] ] = n[0];
- }else{
- d_tableaux_ce_term[x][ n[1] ] = n[0];
- }
- }else{
- d_tableaux[x][ n[1] ] = n[0];
- t << n;
- }
- }else{
- if( n.hasAttribute(InstConstantAttribute()) ){
- f = n.getAttribute(InstConstantAttribute());
- if( n.getKind()==INST_CONSTANT ){
- d_ceTableaux[x][ n ] = Node::null();
- }else{
- d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
- }
- }else{
- d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
- t << n;
- }
- }
-}
-
-void InstStrategySimplex::debugPrint( const char* c ){
- const ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap;
- ArithVarNodeMap::var_iterator vi, vend;
- for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
- ArithVar x = *vi;
- Node n = avnm.asNode(x);
- //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
- Debug(c) << x << " : " << n << ", bounds = ";
- if( d_th->d_partialModel.hasLowerBound( x ) ){
- Debug(c) << d_th->d_partialModel.getLowerBound( x );
- }else{
- Debug(c) << "-infty";
- }
- Debug(c) << " <= ";
- Debug(c) << d_th->d_partialModel.getAssignment( x );
- Debug(c) << " <= ";
- if( d_th->d_partialModel.hasUpperBound( x ) ){
- Debug(c) << d_th->d_partialModel.getUpperBound( x );
- }else{
- Debug(c) << "+infty";
- }
- Debug(c) << std::endl;
- //Debug(c) << " Term = " << d_tableaux_term[x] << std::endl;
- //Debug(c) << " ";
- //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){
- // Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";
- //}
- //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){
- // Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";
- //}
- //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){
- // Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";
- //}
- //Debug(c) << std::endl;
- //}
- }
- Debug(c) << std::endl;
-
- for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){
- Node f = d_quantEngine->getQuantifier( q );
- Debug(c) << f << std::endl;
- Debug(c) << " Inst constants: ";
- for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
- if( i>0 ){
- Debug( c ) << ", ";
- }
- Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
- }
- Debug(c) << std::endl;
- Debug(c) << " Instantiation rows: ";
- for( int i=0; i<(int)d_instRows[f].size(); i++ ){
- if( i>0 ){
- Debug(c) << ", ";
- }
- Debug(c) << d_instRows[f][i];
- }
- Debug(c) << std::endl;
- }
-}
-
-//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,
-// where var is an instantiation constant from f,
-// t[e] is a vector of terms containing instantiation constants from f,
-// and term is a ground term (c1*t1 + ... + cn*tn).
-// We construct the term ( beta - term )/coeff to use as an instantiation for var.
-bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){
- //first try +delta
- if( doInstantiation2( f, term, x, m, var ) ){
- ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith);
- return true;
- }else{
-#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
- //otherwise try -delta
- if( doInstantiation2( f, term, x, m, var, true ) ){
- ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus);
- return true;
- }else{
- return false;
- }
-#else
- return false;
-#endif
- }
-}
-
-bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
- // make term ( beta - term )/coeff
- Node beta = getTableauxValue( x, minus_delta );
- Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
- if( !d_ceTableaux[x][var].isNull() ){
- if( var.getType().isInteger() ){
- Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
- instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal );
- }else{
- Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() );
- instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
- }
- }
- instVal = Rewriter::rewrite( instVal );
- //use as instantiation value for var
- m.set(var, instVal);
- Debug("quant-arith") << "Add instantiation " << m << std::endl;
- return d_quantEngine->addInstantiation( f, m );
-}
-
-Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
- if( d_th->d_arithvarNodeMap.hasArithVar(n) ){
- ArithVar v = d_th->d_arithvarNodeMap.asArithVar( n );
- return getTableauxValue( v, minus_delta );
- }else{
- return NodeManager::currentNM()->mkConst( Rational(0) );
- }
-}
-
-Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
- const Rational& delta = d_th->d_partialModel.getDelta();
- DeltaRational drv = d_th->d_partialModel.getAssignment( v );
- Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
- return mkRationalNode(qmodel);
-}
-
-
-InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) :
- InstStrategy( qe ), d_th( th ){
-
-}
-
-bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){
- //DO_THIS
- return false;
-}
-
-void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){
- Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;
- if( e<2 ){
- return InstStrategy::STATUS_UNFINISHED;
- }else if( e==2 ){
- InstMatch m;
- for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
- Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
- if( i.getType().isDatatype() ){
- Node n = getValueFor( i );
- Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;
- m.set(i,n);
- }
- }
- //d_quantEngine->addInstantiation( f, m );
- }
- return InstStrategy::STATUS_UNKNOWN;
-}
-
-Node InstStrategyDatatypesValue::getValueFor( Node n ){
- //simply get the ground value for n in the current model, if it exists,
- // or return an arbitrary ground term otherwise
- if( !n.hasAttribute(InstConstantAttribute()) ){
- return n;
- }else{
- return n;
- }
- /* FIXME
-
- Debug("quant-datatypes-debug") << "get value for " << n << std::endl;
- if( !n.hasAttribute(InstConstantAttribute()) ){
- return n;
- }else{
- Assert( n.getType().isDatatype() );
- //check if in equivalence class with ground term
- Node rep = getRepresentative( n );
- Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl;
- if( !rep.hasAttribute(InstConstantAttribute()) ){
- return rep;
- }else{
- if( !n.getType().isDatatype() ){
- return n.getType().mkGroundTerm();
- }else{
- if( n.getKind()==APPLY_CONSTRUCTOR ){
- std::vector< Node > children;
- children.push_back( n.getOperator() );
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- children.push_back( getValueFor( n[i] ) );
- }
- return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
- }else{
- const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
- TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels;
- //otherwise, use which constructor the inst constant is current chosen to be
- if( labels->find( n )!=labels->end() ){
- TheoryDatatypes::EqList* lbl = (*labels->find( n )).second;
- int tIndex = -1;
- if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){
- Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl;
- tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr());
- }else{
- Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl;
- //must find a possible choice
- vector< bool > possibleCons;
- possibleCons.resize( dt.getNumConstructors(), true );
- for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {
- Node leqn = (*j);
- possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;
- }
- for( unsigned int j=0; j<possibleCons.size(); j++ ) {
- if( possibleCons[j] ){
- tIndex = j;
- break;
- }
- }
- }
- Assert( tIndex!=-1 );
- Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() );
- Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl;
- std::vector< Node > children;
- children.push_back( cons );
- for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) {
- Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n );
- if( n.hasAttribute(InstConstantAttribute()) ){
- InstConstantAttribute ica;
- sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) );
- }
- Node snn = getValueFor( sn );
- children.push_back( snn );
- }
- return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
- }else{
- return n.getType().mkGroundTerm();
- }
- }
- }
- }
- }
- */
-}
+/********************* */ +/*! \file inst_strategy_cbqi.cpp + ** \verbatim + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of cbqi instantiation strategies + **/ + +#include "theory/quantifiers/inst_strategy_cbqi.h" +#include "theory/arith/theory_arith.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers/options.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; +using namespace CVC4::theory::arith; +using namespace CVC4::theory::datatypes; + +#define ARITH_INSTANTIATOR_USE_MINUS_DELTA + +InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : + InstStrategy( ie ), d_th( th ), d_counter( 0 ){ + d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) ); +} + +bool InstStrategySimplex::calculateShouldProcess( Node f ){ + //DO_THIS + return false; +} + +void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){ + Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl; + d_instRows.clear(); + d_tableaux_term.clear(); + d_tableaux.clear(); + d_ceTableaux.clear(); + //search for instantiation rows in simplex tableaux + ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap; + ArithVarNodeMap::var_iterator vi, vend; + for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ + ArithVar x = *vi; + if( d_th->d_partialModel.hasEitherBound( x ) ){ + Node n = avnm.asNode(x); + Node f; + NodeBuilder<> t(kind::PLUS); + if( n.getKind()==PLUS ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + addTermToRow( x, n[i], f, t ); + } + }else{ + addTermToRow( x, n, f, t ); + } + if( f!=Node::null() ){ + d_instRows[f].push_back( x ); + //this theory has constraints from f + Debug("quant-arith") << "Has constraints from " << f << std::endl; + //set that we should process it + d_quantActive[ f ] = true; + //set tableaux term + if( t.getNumChildren()==0 ){ + d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) ); + }else if( t.getNumChildren()==1 ){ + d_tableaux_term[x] = t.getChild( 0 ); + }else{ + d_tableaux_term[x] = t; + } + } + } + } + //print debug + debugPrint( "quant-arith-debug" ); + d_counter++; +} + +int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ + if( e<2 ){ + return STATUS_UNFINISHED; + }else if( e==2 ){ + //Notice() << f << std::endl; + //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl; + //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl; + Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl; + for( int j=0; j<(int)d_instRows[f].size(); j++ ){ + ArithVar x = d_instRows[f][j]; + if( !d_ceTableaux[x].empty() ){ + Debug("quant-arith-simplex") << "Check row " << x << std::endl; + //instantiation row will be A*e + B*t = beta, + // where e is a vector of terms , and t is vector of ground terms. + // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant + // We will construct the term ( beta - B*t)/coeff to use for e_i. + InstMatch m; + //By default, choose the first instantiation constant to be e_i. + Node var = d_ceTableaux[x].begin()->first; + if( var.getType().isInteger() ){ + std::map< Node, Node >::iterator it = d_ceTableaux[x].begin(); + //try to find coefficent that is +/- 1 + while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){ + ++it; + if( it==d_ceTableaux[x].end() ){ + var = Node::null(); + }else{ + var = it->first; + } + } + //otherwise, try one that divides all ground term coefficients? DO_THIS + } + if( !var.isNull() ){ + Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; + doInstantiation( f, d_tableaux_term[x], x, m, var ); + }else{ + Debug("quant-arith-simplex") << "Could not find var." << std::endl; + } + ////choose a new variable based on alternation strategy + //int index = d_counter%(int)d_th->d_ceTableaux[x].size(); + //Node var; + //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){ + // if( index==0 ){ + // var = it->first; + // break; + // } + // index--; + //} + //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var ); + } + } + } + return STATUS_UNKNOWN; +} + + +void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){ + if( n.getKind()==MULT ){ + if( n[1].hasAttribute(InstConstantAttribute()) ){ + f = n[1].getAttribute(InstConstantAttribute()); + if( n[1].getKind()==INST_CONSTANT ){ + d_ceTableaux[x][ n[1] ] = n[0]; + }else{ + d_tableaux_ce_term[x][ n[1] ] = n[0]; + } + }else{ + d_tableaux[x][ n[1] ] = n[0]; + t << n; + } + }else{ + if( n.hasAttribute(InstConstantAttribute()) ){ + f = n.getAttribute(InstConstantAttribute()); + if( n.getKind()==INST_CONSTANT ){ + d_ceTableaux[x][ n ] = Node::null(); + }else{ + d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); + } + }else{ + d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); + t << n; + } + } +} + +void InstStrategySimplex::debugPrint( const char* c ){ + const ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap; + ArithVarNodeMap::var_iterator vi, vend; + for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ + ArithVar x = *vi; + Node n = avnm.asNode(x); + //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){ + Debug(c) << x << " : " << n << ", bounds = "; + if( d_th->d_partialModel.hasLowerBound( x ) ){ + Debug(c) << d_th->d_partialModel.getLowerBound( x ); + }else{ + Debug(c) << "-infty"; + } + Debug(c) << " <= "; + Debug(c) << d_th->d_partialModel.getAssignment( x ); + Debug(c) << " <= "; + if( d_th->d_partialModel.hasUpperBound( x ) ){ + Debug(c) << d_th->d_partialModel.getUpperBound( x ); + }else{ + Debug(c) << "+infty"; + } + Debug(c) << std::endl; + //Debug(c) << " Term = " << d_tableaux_term[x] << std::endl; + //Debug(c) << " "; + //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){ + // Debug(c) << "( " << it2->first << ", " << it2->second << " ) "; + //} + //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){ + // Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) "; + //} + //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){ + // Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) "; + //} + //Debug(c) << std::endl; + //} + } + Debug(c) << std::endl; + + for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){ + Node f = d_quantEngine->getQuantifier( q ); + Debug(c) << f << std::endl; + Debug(c) << " Inst constants: "; + for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ + if( i>0 ){ + Debug( c ) << ", "; + } + Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); + } + Debug(c) << std::endl; + Debug(c) << " Instantiation rows: "; + for( int i=0; i<(int)d_instRows[f].size(); i++ ){ + if( i>0 ){ + Debug(c) << ", "; + } + Debug(c) << d_instRows[f][i]; + } + Debug(c) << std::endl; + } +} + +//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta, +// where var is an instantiation constant from f, +// t[e] is a vector of terms containing instantiation constants from f, +// and term is a ground term (c1*t1 + ... + cn*tn). +// We construct the term ( beta - term )/coeff to use as an instantiation for var. +bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){ + //first try +delta + if( doInstantiation2( f, term, x, m, var ) ){ + ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith); + return true; + }else{ +#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA + //otherwise try -delta + if( doInstantiation2( f, term, x, m, var, true ) ){ + ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus); + return true; + }else{ + return false; + } +#else + return false; +#endif + } +} + +bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){ + // make term ( beta - term )/coeff + Node beta = getTableauxValue( x, minus_delta ); + Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term ); + if( !d_ceTableaux[x][var].isNull() ){ + if( var.getType().isInteger() ){ + Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); + instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal ); + }else{ + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() ); + instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal ); + } + } + instVal = Rewriter::rewrite( instVal ); + //use as instantiation value for var + m.set(var, instVal); + Debug("quant-arith") << "Add instantiation " << m << std::endl; + return d_quantEngine->addInstantiation( f, m ); +} + +Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){ + if( d_th->d_arithvarNodeMap.hasArithVar(n) ){ + ArithVar v = d_th->d_arithvarNodeMap.asArithVar( n ); + return getTableauxValue( v, minus_delta ); + }else{ + return NodeManager::currentNM()->mkConst( Rational(0) ); + } +} + +Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ + const Rational& delta = d_th->d_partialModel.getDelta(); + DeltaRational drv = d_th->d_partialModel.getAssignment( v ); + Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta ); + return mkRationalNode(qmodel); +} + + +InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) : + InstStrategy( qe ), d_th( th ){ + +} + +bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){ + //DO_THIS + return false; +} + +void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){ + +} + +int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){ + Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl; + if( e<2 ){ + return InstStrategy::STATUS_UNFINISHED; + }else if( e==2 ){ + InstMatch m; + for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){ + Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); + if( i.getType().isDatatype() ){ + Node n = getValueFor( i ); + Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl; + m.set(i,n); + } + } + //d_quantEngine->addInstantiation( f, m ); + } + return InstStrategy::STATUS_UNKNOWN; +} + +Node InstStrategyDatatypesValue::getValueFor( Node n ){ + //simply get the ground value for n in the current model, if it exists, + // or return an arbitrary ground term otherwise + if( !n.hasAttribute(InstConstantAttribute()) ){ + return n; + }else{ + return n; + } + /* FIXME + + Debug("quant-datatypes-debug") << "get value for " << n << std::endl; + if( !n.hasAttribute(InstConstantAttribute()) ){ + return n; + }else{ + Assert( n.getType().isDatatype() ); + //check if in equivalence class with ground term + Node rep = getRepresentative( n ); + Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl; + if( !rep.hasAttribute(InstConstantAttribute()) ){ + return rep; + }else{ + if( !n.getType().isDatatype() ){ + return n.getType().mkGroundTerm(); + }else{ + if( n.getKind()==APPLY_CONSTRUCTOR ){ + std::vector< Node > children; + children.push_back( n.getOperator() ); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + children.push_back( getValueFor( n[i] ) ); + } + return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + }else{ + const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); + TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels; + //otherwise, use which constructor the inst constant is current chosen to be + if( labels->find( n )!=labels->end() ){ + TheoryDatatypes::EqList* lbl = (*labels->find( n )).second; + int tIndex = -1; + if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){ + Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl; + tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr()); + }else{ + Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl; + //must find a possible choice + vector< bool > possibleCons; + possibleCons.resize( dt.getNumConstructors(), true ); + for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) { + Node leqn = (*j); + possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false; + } + for( unsigned int j=0; j<possibleCons.size(); j++ ) { + if( possibleCons[j] ){ + tIndex = j; + break; + } + } + } + Assert( tIndex!=-1 ); + Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() ); + Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl; + std::vector< Node > children; + children.push_back( cons ); + for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) { + Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n ); + if( n.hasAttribute(InstConstantAttribute()) ){ + InstConstantAttribute ica; + sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) ); + } + Node snn = getValueFor( sn ); + children.push_back( snn ); + } + return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + }else{ + return n.getType().mkGroundTerm(); + } + } + } + } + } + */ +} |