From 795e5ba8a1138a371409ac9c8e9da78ce652bb94 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 13 Nov 2012 21:16:26 +0000 Subject: [PATCH] refactoring of quantifiers rewriter based on code review from yesterday, refactoring code out of instantiators in preparation for quantifiers equality engine --- src/theory/arith/theory_arith.h | 6 +- .../arith/theory_arith_instantiator.cpp | 210 +++++++++--------- src/theory/arith/theory_arith_instantiator.h | 63 +++--- .../theory_datatypes_instantiator.cpp | 81 ++++--- .../datatypes/theory_datatypes_instantiator.h | 35 ++- .../quantifiers/quantifiers_rewriter.cpp | 88 ++++---- src/theory/quantifiers/quantifiers_rewriter.h | 9 +- src/theory/quantifiers/term_database.cpp | 15 +- src/theory/quantifiers/term_database.h | 4 + src/theory/quantifiers/trigger.cpp | 4 +- src/theory/theory_engine.cpp | 3 +- src/theory/uf/theory_uf_instantiator.cpp | 36 +-- src/theory/uf/theory_uf_instantiator.h | 6 - src/util/sort_inference.cpp | 29 ++- 14 files changed, 314 insertions(+), 275 deletions(-) diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 9c2ca7d45..2591143cb 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -52,7 +52,7 @@ namespace CVC4 { namespace theory { namespace arith { -class InstantiatorTheoryArith; +class InstStrategySimplex; /** * Implementation of QF_LRA. @@ -60,7 +60,7 @@ class InstantiatorTheoryArith; * 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: @@ -304,7 +304,7 @@ private: /** 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 diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp index b6c85b7eb..6a783fc41 100644 --- a/src/theory/arith/theory_arith_instantiator.cpp +++ b/src/theory/arith/theory_arith_instantiator.cpp @@ -32,7 +32,49 @@ InstStrategySimplex::InstStrategySimplex( InstantiatorTheoryArith* th, Quantifie 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++; } @@ -43,10 +85,10 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ //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. @@ -54,13 +96,13 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ // 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; @@ -70,7 +112,7 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ } 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; } @@ -91,78 +133,8 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ 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()); @@ -190,23 +162,23 @@ void InstantiatorTheoryArith::addTermToRow( ArithVar x, Node n, Node& f, NodeBui } } -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"; } @@ -254,7 +226,7 @@ void InstantiatorTheoryArith::debugPrint( const char* c ){ // 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); @@ -275,7 +247,7 @@ bool InstantiatorTheoryArith::doInstantiation( Node f, Node term, ArithVar x, In } } -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 ); @@ -295,31 +267,71 @@ bool InstantiatorTheoryArith::doInstantiation2( Node f, Node term, ArithVar x, I 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; +} diff --git a/src/theory/arith/theory_arith_instantiator.h b/src/theory/arith/theory_arith_instantiator.h index 7ffe36b41..70bc97bd8 100644 --- a/src/theory/arith/theory_arith_instantiator.h +++ b/src/theory/arith/theory_arith_instantiator.h @@ -27,9 +27,33 @@ namespace CVC4 { 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; @@ -45,29 +69,21 @@ public: ~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() {} @@ -78,24 +94,13 @@ public: 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 */ } diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp index e9f255c65..cfc45f4cc 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.cpp +++ b/src/theory/datatypes/theory_datatypes_instantiator.cpp @@ -26,50 +26,34 @@ using namespace CVC4::context; 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()) ){ @@ -151,16 +135,45 @@ Node InstantiatorTheoryDatatypes::getValueFor( Node n ){ */ } -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 ); } diff --git a/src/theory/datatypes/theory_datatypes_instantiator.h b/src/theory/datatypes/theory_datatypes_instantiator.h index a9bb739c8..d7806a21d 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.h +++ b/src/theory/datatypes/theory_datatypes_instantiator.h @@ -28,6 +28,31 @@ namespace datatypes { 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: @@ -43,16 +68,6 @@ private: 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 ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index d25e516fe..dabaa2188 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -185,51 +185,55 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { 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& args, Node bo } 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& args, bool pol, bool polReq ); private: enum{ - COMPUTE_NNF = 0, + COMPUTE_MINISCOPING = 0, + COMPUTE_NNF, COMPUTE_PRE_SKOLEM, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, @@ -69,10 +70,10 @@ private: /** 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 */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 591270ab0..b55e8abdf 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -14,7 +14,7 @@ #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" @@ -80,7 +80,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ d_op_map[op].push_back( n ); added.insert( n ); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ + for( size_t i=0; igetEfficientEMatcher(); @@ -100,10 +100,9 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ } 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; iaddTerm( n ); } //Message() << "Terms, added lemmas: " << addedLemmas << std::endl; d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() ); @@ -468,3 +467,9 @@ void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContain } } } + +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 ); + } +} diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 5060ac1a7..2bae5a043 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -205,6 +205,8 @@ private: 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 ); @@ -214,6 +216,8 @@ public: 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 */ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index ae08fe863..67b2e6bd8 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -67,10 +67,8 @@ d_quantEngine( qe ), d_f( f ){ } //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() ); } } } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a4b918984..9d93c6cc0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -321,13 +321,14 @@ void TheoryEngine::check(Theory::Effort effort) { // 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; } } } diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index 099eb5b5e..e45842481 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -132,35 +132,7 @@ Node InstantiatorTheoryUf::getRepresentative( Node a ){ 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; } @@ -224,12 +196,6 @@ void InstantiatorTheoryUf::assertDisequal( TNode a, TNode b, TNode reason ){ } -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 ), diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h index 3cb4f97cc..b5a3aa765 100644 --- a/src/theory/uf/theory_uf_instantiator.h +++ b/src/theory/uf/theory_uf_instantiator.h @@ -107,12 +107,6 @@ public: 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 ); diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index 5dc60dbb0..7e0af3e9f 100755 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -281,6 +281,14 @@ TypeNode SortInference::getTypeForId( int t ){ Node SortInference::getNewSymbol( Node old, TypeNode tn ){ if( tn==old.getType() ){ return old; + }else if( old.isConst() ){ + //must make constant of type tn + if( d_const_map[tn].find( old )==d_const_map[tn].end() ){ + std::stringstream ss; + ss << "ic_" << tn << "_" << old; + d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" ); //use mkConst??? + } + return d_const_map[tn][ old ]; }else{ std::stringstream ss; ss << "i_$$_" << old; @@ -323,6 +331,19 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ var_bound.erase( n[0][i] ); } return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else if( n.getKind()==kind::EQUAL ){ + if( children[0].getType()!=children[1].getType() ){ + if( children[0].isConst() ){ + children[0] = getNewSymbol( children[0], children[1].getType() ); + }else if( children[1].isConst() ){ + children[1] = getNewSymbol( children[1], children[0].getType() ); + }else{ + Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl; + Trace("sort-inference-warn") << " Types : " << children[0].getType() << " " << children[1].getType() << std::endl; + Assert( false ); + } + } + return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children ); }else if( n.getKind()==kind::APPLY_UF ){ Node op = n.getOperator(); if( d_symbol_map.find( op )==d_symbol_map.end() ){ @@ -356,13 +377,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ TypeNode tna = getTypeForId( d_op_arg_types[op][i] ); if( tn!=tna ){ if( n[i].isConst() ){ - //must make constant of type tna - if( d_const_map[tna].find( n[i] )==d_const_map[tna].end() ){ - std::stringstream ss; - ss << "ic_" << tna << "_" << n[i]; - d_const_map[tna][ n[i] ] = NodeManager::currentNM()->mkSkolem( ss.str(), tna, "constant created during sort inference" ); //use mkConst??? - } - children[i+1] = d_const_map[tna][ n[i] ]; + children[i+1] = getNewSymbol( n[i], tna ); }else{ Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl; Assert( false ); -- 2.30.2