namespace theory {
namespace arith {
-class InstantiatorTheoryArith;
+class InstStrategySimplex;
/**
* Implementation of QF_LRA.
* http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
*/
class TheoryArith : public Theory {
- friend class InstantiatorTheoryArith;
+ friend class InstStrategySimplex;
private:
bool d_nlIncomplete;
// TODO A better would be:
/** Internal model value for the node */
DeltaRational getDeltaValue(TNode n);
- /** TODO : get rid of this. */
+ /** TODO : get rid of this. */
DeltaRational getDeltaValueWithNonlinear(TNode n, bool& failed);
/** Uninterpretted function symbol for use when interpreting
d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
}
+TheoryArith* InstStrategySimplex::getTheoryArith(){
+ return (TheoryArith*)d_th->getTheory();
+}
+
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
+ ArithVarToNodeMap avtnm = getTheoryArith()->d_arithvarNodeMap.getArithVarToNodeMap();
+ for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
+ ArithVar x = (*it).first;
+ if( getTheoryArith()->d_partialModel.hasEitherBound( x ) ){
+ Node n = (*it).second;
+ 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;
+ d_th->setQuantifierActive( f );
+ //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++;
}
//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_th->d_instRows[f].size() << std::endl;
- for( int j=0; j<(int)d_th->d_instRows[f].size(); j++ ){
- ArithVar x = d_th->d_instRows[f][j];
- if( !d_th->d_ceTableaux[x].empty() ){
+ 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.
// 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_th->d_ceTableaux[x].begin()->first;
+ Node var = d_ceTableaux[x].begin()->first;
if( var.getType().isInteger() ){
- std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin();
+ std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();
//try to find coefficent that is +/- 1
- while( !var.isNull() && !d_th->d_ceTableaux[x][var].isNull() && d_th->d_ceTableaux[x][var]!=d_negOne ){
+ while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){
++it;
- if( it==d_th->d_ceTableaux[x].end() ){
+ if( it==d_ceTableaux[x].end() ){
var = Node::null();
}else{
var = it->first;
}
if( !var.isNull() ){
Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
- d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, m, var );
+ doInstantiation( f, d_tableaux_term[x], x, m, var );
}else{
Debug("quant-arith-simplex") << "Could not find var." << std::endl;
}
return STATUS_UNKNOWN;
}
-InstantiatorTheoryArith::InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-Instantiator( c, ie, th ){
- if( options::cbqi() ){
- addInstStrategy( new InstStrategySimplex( this, d_quantEngine ) );
- }
-}
-
-void InstantiatorTheoryArith::preRegisterTerm( Node t ){
-
-}
-
-void InstantiatorTheoryArith::assertNode( Node assertion ){
- Debug("quant-arith-assert") << "InstantiatorTheoryArith::check: " << assertion << std::endl;
- d_quantEngine->addTermToDatabase( assertion );
- if( options::cbqi() ){
- if( assertion.hasAttribute(InstConstantAttribute()) ){
- setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
- }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
- setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
- }
- }
-}
-
-void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort effort ){
- if( options::cbqi() ){
- 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
- ArithVarToNodeMap avtnm = ((TheoryArith*)getTheory())->d_arithvarNodeMap.getArithVarToNodeMap();
- for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
- ArithVar x = (*it).first;
- if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
- Node n = (*it).second;
- 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;
- setQuantifierActive( f );
- //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" );
- }
-}
-int InstantiatorTheoryArith::process( Node f, Theory::Effort effort, int e ){
- Debug("quant-arith") << "Arith: Try to solve (" << effort << ") for " << f << "... " << std::endl;
- return InstStrategy::STATUS_UNKNOWN;
-}
-
-void InstantiatorTheoryArith::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
+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());
}
}
-void InstantiatorTheoryArith::debugPrint( const char* c ){
- ArithVarToNodeMap avtnm = ((TheoryArith*)getTheory())->d_arithvarNodeMap.getArithVarToNodeMap();
+void InstStrategySimplex::debugPrint( const char* c ){
+ ArithVarToNodeMap avtnm = getTheoryArith()->d_arithvarNodeMap.getArithVarToNodeMap();
for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
ArithVar x = (*it).first;
Node n = (*it).second;
//if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
Debug(c) << x << " : " << n << ", bounds = ";
- if( ((TheoryArith*)getTheory())->d_partialModel.hasLowerBound( x ) ){
- Debug(c) << ((TheoryArith*)getTheory())->d_partialModel.getLowerBound( x );
+ if( getTheoryArith()->d_partialModel.hasLowerBound( x ) ){
+ Debug(c) << getTheoryArith()->d_partialModel.getLowerBound( x );
}else{
Debug(c) << "-infty";
}
Debug(c) << " <= ";
- Debug(c) << ((TheoryArith*)getTheory())->d_partialModel.getAssignment( x );
+ Debug(c) << getTheoryArith()->d_partialModel.getAssignment( x );
Debug(c) << " <= ";
- if( ((TheoryArith*)getTheory())->d_partialModel.hasUpperBound( x ) ){
- Debug(c) << ((TheoryArith*)getTheory())->d_partialModel.getUpperBound( x );
+ if( getTheoryArith()->d_partialModel.hasUpperBound( x ) ){
+ Debug(c) << getTheoryArith()->d_partialModel.getUpperBound( x );
}else{
Debug(c) << "+infty";
}
// 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 InstantiatorTheoryArith::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node 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_statistics.d_instantiations);
}
}
-bool InstantiatorTheoryArith::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
+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 );
return d_quantEngine->addInstantiation( f, m );
}
-Node InstantiatorTheoryArith::getTableauxValue( Node n, bool minus_delta ){
- if( ((TheoryArith*)getTheory())->d_arithvarNodeMap.hasArithVar(n) ){
- ArithVar v = ((TheoryArith*)getTheory())->d_arithvarNodeMap.asArithVar( n );
+Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
+ if( getTheoryArith()->d_arithvarNodeMap.hasArithVar(n) ){
+ ArithVar v = getTheoryArith()->d_arithvarNodeMap.asArithVar( n );
return getTableauxValue( v, minus_delta );
}else{
return NodeManager::currentNM()->mkConst( Rational(0) );
}
}
-Node InstantiatorTheoryArith::getTableauxValue( ArithVar v, bool minus_delta ){
- const Rational& delta = ((TheoryArith*)getTheory())->d_partialModel.getDelta();
- DeltaRational drv = ((TheoryArith*)getTheory())->d_partialModel.getAssignment( v );
+Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
+ const Rational& delta = getTheoryArith()->d_partialModel.getDelta();
+ DeltaRational drv = getTheoryArith()->d_partialModel.getAssignment( v );
Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
return mkRationalNode(qmodel);
}
-InstantiatorTheoryArith::Statistics::Statistics():
- d_instantiations("InstantiatorTheoryArith::Instantiations_Total", 0),
- d_instantiations_minus("InstantiatorTheoryArith::Instantiations_minus_delta", 0)
+
+
+InstStrategySimplex::Statistics::Statistics():
+ d_instantiations("InstStrategySimplex::Instantiations_Total", 0),
+ d_instantiations_minus("InstStrategySimplex::Instantiations_minus_delta", 0)
{
StatisticsRegistry::registerStat(&d_instantiations);
StatisticsRegistry::registerStat(&d_instantiations_minus);
}
-InstantiatorTheoryArith::Statistics::~Statistics(){
+InstStrategySimplex::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_instantiations);
StatisticsRegistry::unregisterStat(&d_instantiations_minus);
}
+
+
+
+
+
+
+
+InstantiatorTheoryArith::InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th) :
+Instantiator( c, ie, th ){
+ if( options::cbqi() ){
+ addInstStrategy( new InstStrategySimplex( this, d_quantEngine ) );
+ }
+}
+
+void InstantiatorTheoryArith::preRegisterTerm( Node t ){
+
+}
+
+void InstantiatorTheoryArith::assertNode( Node assertion ){
+ Debug("quant-arith-assert") << "InstantiatorTheoryArith::check: " << assertion << std::endl;
+ d_quantEngine->addTermToDatabase( assertion );
+ if( options::cbqi() ){
+ if( assertion.hasAttribute(InstConstantAttribute()) ){
+ setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
+ }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
+ setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
+ }
+ }
+}
+
+void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort effort ){
+
+}
+
+int InstantiatorTheoryArith::process( Node f, Theory::Effort effort, int e ){
+ Debug("quant-arith") << "Arith: Try to solve (" << effort << ") for " << f << "... " << std::endl;
+ return InstStrategy::STATUS_UNKNOWN;
+}
namespace theory {
namespace arith {
+class TheoryArith;
class InstantiatorTheoryArith;
class InstStrategySimplex : public InstStrategy{
+private:
+ /** delta */
+ std::map< TypeNode, Node > d_deltas;
+ /** for each quantifier, simplex rows */
+ std::map< Node, std::vector< ArithVar > > d_instRows;
+ /** tableaux */
+ std::map< ArithVar, Node > d_tableaux_term;
+ std::map< ArithVar, std::map< Node, Node > > d_tableaux_ce_term;
+ std::map< ArithVar, std::map< Node, Node > > d_tableaux;
+ /** ce tableaux */
+ std::map< ArithVar, std::map< Node, Node > > d_ceTableaux;
+ /** get value */
+ Node getTableauxValue( Node n, bool minus_delta = false );
+ Node getTableauxValue( ArithVar v, bool minus_delta = false );
+ /** do instantiation */
+ bool doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var );
+ bool doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
+ /** add term to row */
+ void addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t );
+ /** get arith theory */
+ TheoryArith* getTheoryArith();
+ /** print debug */
+ void debugPrint( const char* c );
private:
/** InstantiatorTheoryUf class */
InstantiatorTheoryArith* d_th;
~InstStrategySimplex(){}
/** identify */
std::string identify() const { return std::string("Simplex"); }
+
+ class Statistics {
+ public:
+ IntStat d_instantiations;
+ IntStat d_instantiations_minus;
+ Statistics();
+ ~Statistics();
+ };
+ Statistics d_statistics;
};
class InstantiatorTheoryArith : public Instantiator{
friend class QuantifiersEngine;
friend class InstStrategySimplex;
friend class InstStrategySimplexUfMatch;
-private:
- /** delta */
- std::map< TypeNode, Node > d_deltas;
- /** for each quantifier, simplex rows */
- std::map< Node, std::vector< ArithVar > > d_instRows;
- /** tableaux */
- std::map< ArithVar, Node > d_tableaux_term;
- std::map< ArithVar, std::map< Node, Node > > d_tableaux_ce_term;
- std::map< ArithVar, std::map< Node, Node > > d_tableaux;
- /** ce tableaux */
- std::map< ArithVar, std::map< Node, Node > > d_ceTableaux;
- /** get value */
- Node getTableauxValue( Node n, bool minus_delta = false );
- Node getTableauxValue( ArithVar v, bool minus_delta = false );
- /** do instantiation */
- bool doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var );
- bool doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
public:
InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th);
~InstantiatorTheoryArith() {}
void preRegisterTerm( Node t );
/** identify */
std::string identify() const { return std::string("InstantiatorTheoryArith"); }
- /** print debug */
- void debugPrint( const char* c );
private:
/** reset instantiation */
void processResetInstantiationRound( Theory::Effort effort );
/** process at effort */
int process( Node f, Theory::Effort effort, int e );
- /** add term to row */
- void addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t );
- class Statistics {
- public:
- IntStat d_instantiations;
- IntStat d_instantiations_minus;
- Statistics();
- ~Statistics();
- };
- Statistics d_statistics;
+
};/* class InstantiatiorTheoryArith */
}
using namespace CVC4::theory;
using namespace CVC4::theory::datatypes;
+InstStrategyDatatypesValue::InstStrategyDatatypesValue( QuantifiersEngine* qe ) : InstStrategy( qe ){
-InstantiatorTheoryDatatypes::InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, TheoryDatatypes* th) :
-Instantiator( c, ie, th ){
-}
-
-void InstantiatorTheoryDatatypes::assertNode( Node assertion ){
- Debug("quant-datatypes-assert") << "InstantiatorTheoryDatatypes::check: " << assertion << std::endl;
- d_quantEngine->addTermToDatabase( assertion );
- if( options::cbqi() ){
- if( assertion.hasAttribute(InstConstantAttribute()) ){
- setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
- }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
- setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
- }
- }
}
-void InstantiatorTheoryDatatypes::processResetInstantiationRound( Theory::Effort effort ){
+void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){
}
-
-int InstantiatorTheoryDatatypes::process( Node f, Theory::Effort effort, int e ){
+int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){
Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;
- if( options::cbqi() ){
- 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);
- }
+ 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 );
}
+ //d_quantEngine->addInstantiation( f, m );
}
return InstStrategy::STATUS_UNKNOWN;
}
-Node InstantiatorTheoryDatatypes::getValueFor( Node n ){
+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()) ){
*/
}
-InstantiatorTheoryDatatypes::Statistics::Statistics():
- d_instantiations("InstantiatorTheoryDatatypes::Instantiations_Total", 0)
+InstStrategyDatatypesValue::Statistics::Statistics():
+ d_instantiations("InstStrategyDatatypesValue::Instantiations_Total", 0)
{
StatisticsRegistry::registerStat(&d_instantiations);
}
-InstantiatorTheoryDatatypes::Statistics::~Statistics(){
+InstStrategyDatatypesValue::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_instantiations);
}
+
+
+InstantiatorTheoryDatatypes::InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, TheoryDatatypes* th) :
+Instantiator( c, ie, th ){
+ if( options::cbqi() ){
+ addInstStrategy( new InstStrategyDatatypesValue( ie ) );
+ }
+}
+
+void InstantiatorTheoryDatatypes::assertNode( Node assertion ){
+ Debug("quant-datatypes-assert") << "InstantiatorTheoryDatatypes::check: " << assertion << std::endl;
+ d_quantEngine->addTermToDatabase( assertion );
+ if( options::cbqi() ){
+ if( assertion.hasAttribute(InstConstantAttribute()) ){
+ setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
+ }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
+ setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
+ }
+ }
+}
+
+void InstantiatorTheoryDatatypes::processResetInstantiationRound( Theory::Effort effort ){
+
+}
+
+int InstantiatorTheoryDatatypes::process( Node f, Theory::Effort effort, int e ){
+ return InstStrategy::STATUS_UNKNOWN;
+}
+
bool InstantiatorTheoryDatatypes::hasTerm( Node a ){
return ((TheoryDatatypes*)d_th)->getEqualityEngine()->hasTerm( a );
}
class TheoryDatatypes;
+class InstStrategyDatatypesValue : public InstStrategy
+{
+private:
+ Node getValueFor( Node n );
+public:
+ //constructor
+ InstStrategyDatatypesValue( QuantifiersEngine* qe );
+ ~InstStrategyDatatypesValue(){}
+ /** reset instantiation */
+ void processResetInstantiationRound( Theory::Effort effort );
+ /** process method, returns a status */
+ int process( Node f, Theory::Effort effort, int e );
+ /** identify */
+ std::string identify() const { return std::string("InstStrategyDatatypesValue"); }
+
+ class Statistics {
+ public:
+ IntStat d_instantiations;
+ Statistics();
+ ~Statistics();
+ };
+ Statistics d_statistics;
+};/* class InstStrategy */
+
+
class InstantiatorTheoryDatatypes : public Instantiator{
friend class QuantifiersEngine;
public:
void processResetInstantiationRound( Theory::Effort effort );
/** process at effort */
int process( Node f, Theory::Effort effort, int e );
- /** get value for */
- Node getValueFor( Node n );
-
- class Statistics {
- public:
- IntStat d_instantiations;
- Statistics();
- ~Statistics();
- };
- Statistics d_statistics;
public:
/** general queries about equality */
bool hasTerm( Node a );
RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
+ RewriteStatus status = REWRITE_DONE;
+ Node ret = in;
//get the arguments
std::vector< Node > args;
for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
args.push_back( in[0][i] );
}
- //get the body
- Node body = in[1];
- if( in.getKind()==EXISTS ){
- body = body.getKind()==NOT ? body[0] : body.notNode();
- }
//get the instantiation pattern list
Node ipl;
if( in.getNumChildren()==3 ){
ipl = in[2];
}
- bool isNested = in.hasAttribute(NestedQuantAttribute());
- //compute miniscoping first
- Node n = body;//computeNNF( body ); TODO: compute NNF here (current bad idea since arithmetic rewrites equalities)
- if( body!=n ){
- Notice() << "NNF " << body << " -> " << n << std::endl;
- }
- n = computeMiniscoping( args, n, ipl, isNested );
- if( in.getKind()==kind::EXISTS ){
- n = n.getKind()==NOT ? n[0] : n.notNode();
+ //get the body
+ if( in.getKind()==EXISTS ){
+ std::vector< Node > children;
+ children.push_back( in[0] );
+ children.push_back( in[1].negate() );
+ if( in.getNumChildren()==3 ){
+ children.push_back( in[2] );
+ }
+ ret = NodeManager::currentNM()->mkNode( FORALL, children );
+ ret = ret.negate();
+ status = REWRITE_AGAIN_FULL;
+ }else{
+ bool isNested = in.hasAttribute(NestedQuantAttribute());
+ for( int op=0; op<COMPUTE_LAST; op++ ){
+ if( doOperation( in, isNested, op ) ){
+ ret = computeOperation( in, op );
+ if( ret!=in ){
+ status = REWRITE_AGAIN_FULL;
+ break;
+ }
+ }
+ }
}
- //compute other rewrite options for each produced quantifier
- n = rewriteQuants( n, isNested, true );
//print if changed
- if( in!=n ){
+ if( in!=ret ){
if( in.hasAttribute(NestedQuantAttribute()) ){
- setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) );
+ setNestedQuantifiers( ret, in.getAttribute(NestedQuantAttribute()) );
}
- Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
- Trace("quantifiers-rewrite") << " to " << std::endl;
- Trace("quantifiers-rewrite") << n << std::endl;
if( in.hasAttribute(InstConstantAttribute()) ){
InstConstantAttribute ica;
- n.setAttribute(ica,in.getAttribute(InstConstantAttribute()) );
+ ret.setAttribute(ica,in.getAttribute(InstConstantAttribute()) );
}
-
- // This is required if substitute in computePrenex() is used.
- return RewriteResponse(REWRITE_AGAIN_FULL, n );
- }else{
- return RewriteResponse(REWRITE_DONE, n );
+ Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
+ Trace("quantifiers-rewrite") << " to " << std::endl;
+ Trace("quantifiers-rewrite") << ret << std::endl;
}
+ return RewriteResponse( status, ret );
}
return RewriteResponse(REWRITE_DONE, in);
}
if( f.getNumChildren()==3 ){
ipl = f[2];
}
- if( computeOption==COMPUTE_NNF ){
+ if( computeOption==COMPUTE_MINISCOPING ){
+ //return directly
+ return computeMiniscoping( args, n, ipl, f.hasAttribute(NestedQuantAttribute()) );
+ }else if( computeOption==COMPUTE_NNF ){
n = computeNNF( n );
}else if( computeOption==COMPUTE_PRENEX || computeOption==COMPUTE_PRE_SKOLEM ){
n = computePrenex( n, args, true, computeOption==COMPUTE_PRENEX );
}
return mkForAll( args, body, ipl );
}
-
-Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested, bool duringRewrite ){
+/*
+Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested ){
if( n.getKind()==FORALL ){
- return rewriteQuant( n, isNested, duringRewrite );
+ return rewriteQuant( n, isNested );
}else if( isLiteral( n ) ){
return n;
}else{
NodeBuilder<> tt(n.getKind());
for( int i=0; i<(int)n.getNumChildren(); i++ ){
- tt << rewriteQuants( n[i], isNested, duringRewrite );
+ tt << rewriteQuants( n[i], isNested );
}
return tt.constructNode();
}
}
-Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrite ){
+Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested ){
Node prev = n;
for( int op=0; op<COMPUTE_LAST; op++ ){
- if( doOperation( n, isNested, op, duringRewrite ) ){
+ if( doOperation( n, isNested, op ) ){
Node prev2 = n;
n = computeOperation( n, op );
if( prev2!=n ){
return n;
}else{
//rewrite again until fix point is reached
- return rewriteQuant( n, isNested, duringRewrite );
+ return rewriteQuant( n, isNested );
}
}
+*/
bool QuantifiersRewriter::doMiniscopingNoFreeVar(){
return options::miniscopeQuantFreeVar();
}
}
-bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption, bool duringRewrite ){
- if( computeOption==COMPUTE_NNF ){
+bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){
+ if( computeOption==COMPUTE_MINISCOPING ){
+ return true;
+ }else if( computeOption==COMPUTE_NNF ){
return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
}else if( computeOption==COMPUTE_PRE_SKOLEM ){
- return false;//options::preSkolemQuant() && !duringRewrite;
+ return false;//options::preSkolemQuant();
}else if( computeOption==COMPUTE_PRENEX ){
return options::prenexQuant();
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
return options::varElimQuant();
}else if( computeOption==COMPUTE_CNF ){
- return options::cnfQuant() && !duringRewrite;// || options::finiteModelFind();
+ return false;//return options::cnfQuant() ;
}else{
return false;
}
static Node computePrenex( Node body, std::vector< Node >& args, bool pol, bool polReq );
private:
enum{
- COMPUTE_NNF = 0,
+ COMPUTE_MINISCOPING = 0,
+ COMPUTE_NNF,
COMPUTE_PRE_SKOLEM,
COMPUTE_PRENEX,
COMPUTE_VAR_ELIMINATION,
/** options */
static bool doMiniscopingNoFreeVar();
static bool doMiniscopingAnd();
- static bool doOperation( Node f, bool isNested, int computeOption, bool duringRewrite = true );
+ static bool doOperation( Node f, bool isNested, int computeOption );
public:
- static Node rewriteQuants( Node n, bool isNested = false, bool duringRewrite = true );
- static Node rewriteQuant( Node n, bool isNested = false, bool duringRewrite = true );
+ //static Node rewriteQuants( Node n, bool isNested = false );
+ //static Node rewriteQuant( Node n, bool isNested = false );
};/* class QuantifiersRewriter */
}/* CVC4::theory::quantifiers namespace */
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/options.h"
d_op_map[op].push_back( n );
added.insert( n );
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
addTerm( n[i], added, withinQuant );
if( options::efficientEMatching() ){
EfficientEMatcher* eem = d_quantEngine->getEfficientEMatcher();
}
if( options::eagerInstQuant() ){
if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
- uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
int addedLemmas = 0;
- for( int i=0; i<(int)ith->d_op_triggers[op].size(); i++ ){
- addedLemmas += ith->d_op_triggers[op][i]->addTerm( n );
+ for( size_t i=0; i<d_op_triggers[op].size(); i++ ){
+ addedLemmas += d_op_triggers[op][i]->addTerm( n );
}
//Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() );
}
}
}
+
+void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
+ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
+ d_op_triggers[op].push_back( tr );
+ }
+}
void computeVarContains2( Node n, Node parent );
/** var contains */
std::map< TNode, std::vector< TNode > > d_var_contains;
+ /** triggers for each operator */
+ std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
public:
/** compute var contains */
void computeVarContains( Node n );
void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
/** get var contains for node n */
void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
+ /** register trigger (for eager quantifier instantiation) */
+ void registerTrigger( inst::Trigger* tr, Node op );
};/* class TermDb */
}/* CVC4::theory::quantifiers namespace */
}
//Notice() << "Trigger : " << (*this) << " for " << f << std::endl;
if( options::eagerInstQuant() ){
- Theory* th_uf = qe->getTheoryEngine()->theoryOf( theory::THEORY_UF );
- uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator();
for( int i=0; i<(int)d_nodes.size(); i++ ){
- ith->registerTrigger( this, d_nodes[i].getOperator() );
+ qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() );
}
}
}
// Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
if(d_logicInfo.isQuantified()) {
+ bool prevIncomplete = d_incomplete;
// quantifiers engine must pass effort last call check
d_quantEngine->check(Theory::EFFORT_LAST_CALL);
// if we have given up, then possibly flip decision
if(options::flipDecision()) {
if(d_incomplete && !d_inConflict && !needCheck()) {
if( ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision() ) {
- d_incomplete = false;
+ d_incomplete = prevIncomplete;
}
}
}
return a;
}
}
-/*
-Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
- if( d_ground_reps.find( a )==d_ground_reps.end() ){
- if( !hasTerm( a ) ){
- return a;
- }else{
- Node rep = getRepresentative( a );
- if( !rep.hasAttribute(InstConstantAttribute()) ){
- //return the representative of a
- d_ground_reps[a] = rep;
- return rep;
- }else{
- //otherwise, must search eq class
- eq::EqClassIterator eqc_iter( rep, getEqualityEngine() );
- rep = Node::null();
- while( !eqc_iter.isFinished() ){
- if( !(*eqc_iter).hasAttribute(InstConstantAttribute()) ){
- d_ground_reps[ a ] = *eqc_iter;
- return *eqc_iter;
- }
- eqc_iter++;
- }
- d_ground_reps[ a ] = a;
- }
- }
- }
- return d_ground_reps[a];
-}
-*/
+
eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){
return &((TheoryUF*)d_th)->d_equalityEngine;
}
}
-void InstantiatorTheoryUf::registerTrigger( theory::inst::Trigger* tr, Node op ){
- if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
- d_op_triggers[op].push_back( tr );
- }
-}
-
void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){
if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) ){
eq::EqClassIterator eqc_iter( getRepresentative( n ),
void merge( TNode a, TNode b );
/** assert terms are disequal */
void assertDisequal( TNode a, TNode b, TNode reason );
-private:
- /** triggers */
- std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
-public:
- /** register trigger (for eager quantifier instantiation) */
- void registerTrigger( inst::Trigger* tr, Node op );
public:
/** output eq class */
void outputEqClass( const char* c, Node n );
Node SortInference::getNewSymbol( Node old, TypeNode tn ){\r
if( tn==old.getType() ){\r
return old;\r
+ }else if( old.isConst() ){\r
+ //must make constant of type tn\r
+ if( d_const_map[tn].find( old )==d_const_map[tn].end() ){\r
+ std::stringstream ss;\r
+ ss << "ic_" << tn << "_" << old;\r
+ d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" ); //use mkConst???\r
+ }\r
+ return d_const_map[tn][ old ];\r
}else{\r
std::stringstream ss;\r
ss << "i_$$_" << old;\r
var_bound.erase( n[0][i] );\r
}\r
return NodeManager::currentNM()->mkNode( n.getKind(), children );\r
+ }else if( n.getKind()==kind::EQUAL ){\r
+ if( children[0].getType()!=children[1].getType() ){\r
+ if( children[0].isConst() ){\r
+ children[0] = getNewSymbol( children[0], children[1].getType() );\r
+ }else if( children[1].isConst() ){\r
+ children[1] = getNewSymbol( children[1], children[0].getType() );\r
+ }else{\r
+ Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl;\r
+ Trace("sort-inference-warn") << " Types : " << children[0].getType() << " " << children[1].getType() << std::endl;\r
+ Assert( false );\r
+ }\r
+ }\r
+ return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );\r
}else if( n.getKind()==kind::APPLY_UF ){\r
Node op = n.getOperator();\r
if( d_symbol_map.find( op )==d_symbol_map.end() ){\r
TypeNode tna = getTypeForId( d_op_arg_types[op][i] );\r
if( tn!=tna ){\r
if( n[i].isConst() ){\r
- //must make constant of type tna\r
- if( d_const_map[tna].find( n[i] )==d_const_map[tna].end() ){\r
- std::stringstream ss;\r
- ss << "ic_" << tna << "_" << n[i];\r
- d_const_map[tna][ n[i] ] = NodeManager::currentNM()->mkSkolem( ss.str(), tna, "constant created during sort inference" ); //use mkConst???\r
- }\r
- children[i+1] = d_const_map[tna][ n[i] ];\r
+ children[i+1] = getNewSymbol( n[i], tna );\r
}else{\r
Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl;\r
Assert( false );\r
projects / cvc5.git / commitdiff