arith_unate_lemma_mode.h \
arith_unate_lemma_mode.cpp \
arith_propagation_mode.h \
- arith_propagation_mode.cpp \
- theory_arith_instantiator.h \
- theory_arith_instantiator.cpp
+ arith_propagation_mode.cpp
EXTRA_DIST = \
kinds \
theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h"
typechecker "theory/arith/theory_arith_type_rules.h"
-instantiator ::CVC4::theory::arith::InstantiatorTheoryArith "theory/arith/theory_arith_instantiator.h"
properties stable-infinite
properties check propagate ppStaticLearn presolve notifyRestart
namespace CVC4 {
namespace theory {
-namespace arith {
-class InstStrategySimplex;
+namespace quantifiers {
+ class InstStrategySimplex;
+}
+
+namespace arith {
/**
* Implementation of QF_LRA.
* http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
*/
class TheoryArith : public Theory {
- friend class InstStrategySimplex;
+ friend class quantifiers::InstStrategySimplex;
private:
bool d_nlIncomplete;
// TODO A better would be:
+++ /dev/null
-/********************* */
-/*! \file theory_arith_instantiator.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 instantiator_arith_instantiator class
- **/
-
-#include "theory/arith/theory_arith_instantiator.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::arith;
-
-#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
-
-InstStrategySimplex::InstStrategySimplex( InstantiatorTheoryArith* th, QuantifiersEngine* ie ) :
- InstStrategy( ie ), d_th( th ), d_counter( 0 ){
- 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++;
-}
-
-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 ){
- 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( getTheoryArith()->d_partialModel.hasLowerBound( x ) ){
- Debug(c) << getTheoryArith()->d_partialModel.getLowerBound( x );
- }else{
- Debug(c) << "-infty";
- }
- Debug(c) << " <= ";
- Debug(c) << getTheoryArith()->d_partialModel.getAssignment( x );
- Debug(c) << " <= ";
- if( getTheoryArith()->d_partialModel.hasUpperBound( x ) ){
- Debug(c) << getTheoryArith()->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_statistics.d_instantiations);
- return true;
- }else{
-#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
- //otherwise try -delta
- if( doInstantiation2( f, term, x, m, var, true ) ){
- ++(d_statistics.d_instantiations_minus);
- ++(d_statistics.d_instantiations);
- 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( 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 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);
-}
-
-
-
-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);
-}
-
-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;
- //INST_ELIM_TRY//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;
-}
+++ /dev/null
-/********************* */
-/*! \file theory_arith_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): 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 instantiator_arith_instantiator
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__INSTANTIATOR_ARITH_H
-#define __CVC4__INSTANTIATOR_ARITH_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/arith/arithvar_node_map.h"
-
-#include "util/statistics_registry.h"
-
-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;
- /** */
- int d_counter;
- /** negative one */
- Node d_negOne;
- /** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
-public:
- InstStrategySimplex( InstantiatorTheoryArith* th, QuantifiersEngine* ie );
- ~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;
-public:
- InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th);
- ~InstantiatorTheoryArith() {}
-
- /** assertNode function, assertion is asserted to theory */
- void assertNode( Node assertion );
- /** Pre-register a term. Done one time for a Node, ever. */
- void preRegisterTerm( Node t );
- /** identify */
- std::string identify() const { return std::string("InstantiatorTheoryArith"); }
-private:
- /** reset instantiation */
- void processResetInstantiationRound( Theory::Effort effort );
- /** process at effort */
- int process( Node f, Theory::Effort effort, int e );
-
-
-};/* class InstantiatiorTheoryArith */
-
-}
-}
-}
-
-#endif
\ No newline at end of file
array_info.cpp \
static_fact_manager.h \
static_fact_manager.cpp \
- theory_arrays_instantiator.h \
- theory_arrays_instantiator.cpp \
theory_arrays_model.h \
theory_arrays_model.cpp
theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
typechecker "theory/arrays/theory_arrays_type_rules.h"
-instantiator ::CVC4::theory::arrays::InstantiatorTheoryArrays "theory/arrays/theory_arrays_instantiator.h"
properties polite stable-infinite parametric
properties check propagate presolve getNextDecisionRequest
#include <map>
#include "theory/rewriter.h"
#include "expr/command.h"
-#include "theory/arrays/theory_arrays_instantiator.h"
#include "theory/arrays/theory_arrays_model.h"
#include "theory/model.h"
#include "theory/arrays/options.h"
}
}
- // Find all stores in which n[0] appears and get corresponding read terms
+ // Find all stores in which n[0] appears and get corresponding read terms
const CTNodeList* instores = d_infoMap.getInStores(array_eqc);
size_t it = 0;
for(; it < instores->size(); ++it) {
+++ /dev/null
-/********************* */
-/*! \file theory_arrays_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: bobot
- ** Minor contributors (to current version): 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 theory_arrays_instantiator class
- **/
-
-#include "theory/theory_engine.h"
-#include "theory/arrays/theory_arrays_instantiator.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/quantifiers/options.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arrays;
-
-InstantiatorTheoryArrays::InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-Instantiator( c, ie, th ){
-
-}
-
-void InstantiatorTheoryArrays::preRegisterTerm( Node t ){
-
-}
-
-void InstantiatorTheoryArrays::assertNode( Node assertion ){
- Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl;
- //INST_ELIM_TRY//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 InstantiatorTheoryArrays::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e ){
- return InstStrategy::STATUS_SAT;
-}
-
-bool InstantiatorTheoryArrays::hasTerm( Node a ){
- return ((TheoryArrays*)d_th)->getEqualityEngine()->hasTerm( a );
-}
-
-bool InstantiatorTheoryArrays::areEqual( Node a, Node b ){
- if( a==b ){
- return true;
- }else if( hasTerm( a ) && hasTerm( b ) ){
- return ((TheoryArrays*)d_th)->getEqualityEngine()->areEqual( a, b );
- }else{
- return false;
- }
-}
-
-bool InstantiatorTheoryArrays::areDisequal( Node a, Node b ){
- if( a==b ){
- return false;
- }else if( hasTerm( a ) && hasTerm( b ) ){
- return ((TheoryArrays*)d_th)->getEqualityEngine()->areDisequal( a, b, false );
- }else{
- return false;
- }
-}
-
-Node InstantiatorTheoryArrays::getRepresentative( Node a ){
- if( hasTerm( a ) ){
- return ((TheoryArrays*)d_th)->getEqualityEngine()->getRepresentative( a );
- }else{
- return a;
- }
-}
-
-eq::EqualityEngine* InstantiatorTheoryArrays::getEqualityEngine(){
- return ((TheoryArrays*)d_th)->getEqualityEngine();
-}
-
-void InstantiatorTheoryArrays::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
- if( hasTerm( a ) ){
- a = getEqualityEngine()->getRepresentative( a );
- eq::EqClassIterator eqc_iter( a, getEqualityEngine() );
- while( !eqc_iter.isFinished() ){
- if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){
- eqc.push_back( *eqc_iter );
- }
- eqc_iter++;
- }
- }
-}
-
-rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClasses(){
- arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory());
- eq::EqualityEngine* ee =
- static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
- return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee);
-}
-
-rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClass(){
- arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory());
- eq::EqualityEngine* ee =
- static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
- return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee);
-}
+++ /dev/null
-/********************* */
-/*! \file theory_arrays_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot
- ** 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 Instantiator for theory of arrays
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__INSTANTIATOR_THEORY_ARRAYS_H
-#define __CVC4__INSTANTIATOR_THEORY_ARRAYS_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/uf/equality_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
-class InstantiatorTheoryArrays : public Instantiator{
- friend class QuantifiersEngine;
-protected:
- /** reset instantiation round */
- void processResetInstantiationRound( Theory::Effort effort );
- /** process quantifier */
- int process( Node f, Theory::Effort effort, int e );
-public:
- InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th);
- ~InstantiatorTheoryArrays() {}
- /** Pre-register a term. */
- void preRegisterTerm( Node t );
- /** assertNode function, assertion is asserted to theory */
- void assertNode( Node assertion );
- /** identify */
- std::string identify() const { return std::string("InstantiatorTheoryArrays"); }
-public:
- /** general queries about equality */
- bool hasTerm( Node a );
- bool areEqual( Node a, Node b );
- bool areDisequal( Node a, Node b );
- Node getRepresentative( Node a );
- eq::EqualityEngine* getEqualityEngine();
- void getEquivalenceClass( Node a, std::vector< Node >& eqc );
- /** general creators of candidate generators */
- rrinst::CandidateGenerator* getRRCanGenClasses();
- rrinst::CandidateGenerator* getRRCanGenClass();
-};/* class Instantiatior */
-
-}
-}
-}
-
-#endif
type_enumerator.h \
theory_datatypes.h \
datatypes_rewriter.h \
- theory_datatypes.cpp \
- theory_datatypes_instantiator.h \
- theory_datatypes_instantiator.cpp
+ theory_datatypes.cpp
EXTRA_DIST = \
kinds
theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h"
typechecker "theory/datatypes/theory_datatypes_type_rules.h"
-instantiator ::CVC4::theory::datatypes::InstantiatorTheoryDatatypes "theory/datatypes/theory_datatypes_instantiator.h"
+
properties check presolve parametric propagate
#include "expr/kind.h"
#include "util/datatype.h"
#include "util/cvc4_assert.h"
-#include "theory/datatypes/theory_datatypes_instantiator.h"
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/theory_datatypes_type_rules.h"
#include "theory/model.h"
+++ /dev/null
-/********************* */
-/*! \file theory_datatypes_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters, bobot
- ** 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 theory_datatypes_instantiator class
- **/
-
-#include "theory/datatypes/theory_datatypes_instantiator.h"
-#include "theory/datatypes/theory_datatypes.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::datatypes;
-
-InstStrategyDatatypesValue::InstStrategyDatatypesValue( QuantifiersEngine* qe ) : InstStrategy( qe ){
-
-}
-
-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();
- }
- }
- }
- }
- }
- */
-}
-
-InstStrategyDatatypesValue::Statistics::Statistics():
- d_instantiations("InstStrategyDatatypesValue::Instantiations_Total", 0)
-{
- StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-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;
- //INST_ELIM_TRY//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 );
-}
-
-bool InstantiatorTheoryDatatypes::areEqual( Node a, Node b ){
- if( a==b ){
- return true;
- }else if( hasTerm( a ) && hasTerm( b ) ){
- return ((TheoryDatatypes*)d_th)->getEqualityEngine()->areEqual( a, b );
- }else{
- return false;
- }
-}
-
-bool InstantiatorTheoryDatatypes::areDisequal( Node a, Node b ){
- if( a==b ){
- return false;
- }else if( hasTerm( a ) && hasTerm( b ) ){
- return ((TheoryDatatypes*)d_th)->getEqualityEngine()->areDisequal( a, b, false );
- }else{
- return false;
- }
-}
-
-Node InstantiatorTheoryDatatypes::getRepresentative( Node a ){
- if( hasTerm( a ) ){
- return ((TheoryDatatypes*)d_th)->getEqualityEngine()->getRepresentative( a );
- }else{
- return a;
- }
-}
-
-eq::EqualityEngine* InstantiatorTheoryDatatypes::getEqualityEngine(){
- return &((TheoryDatatypes*)d_th)->d_equalityEngine;
-}
-
-void InstantiatorTheoryDatatypes::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
- if( hasTerm( a ) ){
- a = getEqualityEngine()->getRepresentative( a );
- eq::EqClassIterator eqc_iter( a, getEqualityEngine() );
- while( !eqc_iter.isFinished() ){
- if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){
- eqc.push_back( *eqc_iter );
- }
- eqc_iter++;
- }
- }
-}
-
-CVC4::theory::rrinst::CandidateGenerator* InstantiatorTheoryDatatypes::getRRCanGenClass(){
- datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes*>(getTheory());
- eq::EqualityEngine* ee =
- static_cast<eq::EqualityEngine*>(dt->getEqualityEngine());
- return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee);
-}
+++ /dev/null
-/********************* */
-/*! \file theory_datatypes_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters, bobot
- ** 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 instantiator_datatypes_instantiator
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__INSTANTIATOR_DATATYPES_H
-#define __CVC4__INSTANTIATOR_DATATYPES_H
-
-#include "theory/quantifiers_engine.h"
-
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-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:
- InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, TheoryDatatypes* th);
- ~InstantiatorTheoryDatatypes() {}
-
- /** assertNode function, assertion is asserted to theory */
- void assertNode( Node assertion );
- /** identify */
- std::string identify() const { return std::string("InstantiatorTheoryDatatypes"); }
-private:
- /** reset instantiation */
- void processResetInstantiationRound( Theory::Effort effort );
- /** process at effort */
- int process( Node f, Theory::Effort effort, int e );
-public:
- /** general queries about equality */
- bool hasTerm( Node a );
- bool areEqual( Node a, Node b );
- bool areDisequal( Node a, Node b );
- Node getRepresentative( Node a );
- eq::EqualityEngine* getEqualityEngine();
- void getEquivalenceClass( Node a, std::vector< Node >& eqc );
- /** general creators of candidate generators */
- CVC4::theory::rrinst::CandidateGenerator* getRRCanGenClass();
-};/* class InstantiatiorTheoryDatatypes */
-
-
-}
-}
-}
-
-#endif
quantifiers_rewriter.h \
quantifiers_rewriter.cpp \
theory_quantifiers.cpp \
- theory_quantifiers_instantiator.h \
- theory_quantifiers_instantiator.cpp \
instantiation_engine.h \
instantiation_engine.cpp \
trigger.h \
trigger.cpp \
candidate_generator.h \
candidate_generator.cpp \
- instantiator_default.h \
- instantiator_default.cpp \
inst_match.h \
inst_match.cpp \
model_engine.h \
inst_match_generator.h \
inst_match_generator.cpp \
macros.h \
- macros.cpp
+ macros.cpp \
+ inst_strategy_e_matching.h \
+ inst_strategy_e_matching.cpp \
+ inst_strategy_cbqi.h \
+ inst_strategy_cbqi.cpp
EXTRA_DIST = \
kinds \
--- /dev/null
+/********************* */\r
+/*! \file inst_strategy_cbqi.cpp\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): bobot, mdeters\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Implementation of cbqi instantiation strategies\r
+ **/\r
+\r
+#include "theory/quantifiers/inst_strategy_cbqi.h"\r
+#include "theory/arith/theory_arith.h"\r
+#include "theory/theory_engine.h"\r
+#include "theory/quantifiers/options.h"\r
+#include "theory/quantifiers/term_database.h"\r
+\r
+using namespace std;\r
+using namespace CVC4;\r
+using namespace CVC4::kind;\r
+using namespace CVC4::context;\r
+using namespace CVC4::theory;\r
+using namespace CVC4::theory::quantifiers;\r
+using namespace CVC4::theory::arith;\r
+using namespace CVC4::theory::datatypes;\r
+\r
+#define ARITH_INSTANTIATOR_USE_MINUS_DELTA\r
+\r
+InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :\r
+ InstStrategy( ie ), d_th( th ), d_counter( 0 ){\r
+ d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );\r
+}\r
+\r
+bool InstStrategySimplex::calculateShouldProcess( Node f ){\r
+ //DO_THIS\r
+ return false;\r
+}\r
+\r
+void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){\r
+ Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;\r
+ d_instRows.clear();\r
+ d_tableaux_term.clear();\r
+ d_tableaux.clear();\r
+ d_ceTableaux.clear();\r
+ //search for instantiation rows in simplex tableaux\r
+ ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();\r
+ for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){\r
+ ArithVar x = (*it).first;\r
+ if( d_th->d_partialModel.hasEitherBound( x ) ){\r
+ Node n = (*it).second;\r
+ Node f;\r
+ NodeBuilder<> t(kind::PLUS);\r
+ if( n.getKind()==PLUS ){\r
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){\r
+ addTermToRow( x, n[i], f, t );\r
+ }\r
+ }else{\r
+ addTermToRow( x, n, f, t );\r
+ }\r
+ if( f!=Node::null() ){\r
+ d_instRows[f].push_back( x );\r
+ //this theory has constraints from f\r
+ Debug("quant-arith") << "Has constraints from " << f << std::endl;\r
+ //set that we should process it\r
+ d_quantActive[ f ] = true;\r
+ //set tableaux term\r
+ if( t.getNumChildren()==0 ){\r
+ d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );\r
+ }else if( t.getNumChildren()==1 ){\r
+ d_tableaux_term[x] = t.getChild( 0 );\r
+ }else{\r
+ d_tableaux_term[x] = t;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ //print debug\r
+ debugPrint( "quant-arith-debug" );\r
+ d_counter++;\r
+}\r
+\r
+int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){\r
+ if( e<2 ){\r
+ return STATUS_UNFINISHED;\r
+ }else if( e==2 ){\r
+ //Notice() << f << std::endl;\r
+ //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;\r
+ //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;\r
+ Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl;\r
+ for( int j=0; j<(int)d_instRows[f].size(); j++ ){\r
+ ArithVar x = d_instRows[f][j];\r
+ if( !d_ceTableaux[x].empty() ){\r
+ Debug("quant-arith-simplex") << "Check row " << x << std::endl;\r
+ //instantiation row will be A*e + B*t = beta,\r
+ // where e is a vector of terms , and t is vector of ground terms.\r
+ // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant\r
+ // We will construct the term ( beta - B*t)/coeff to use for e_i.\r
+ InstMatch m;\r
+ //By default, choose the first instantiation constant to be e_i.\r
+ Node var = d_ceTableaux[x].begin()->first;\r
+ if( var.getType().isInteger() ){\r
+ std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();\r
+ //try to find coefficent that is +/- 1\r
+ while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){\r
+ ++it;\r
+ if( it==d_ceTableaux[x].end() ){\r
+ var = Node::null();\r
+ }else{\r
+ var = it->first;\r
+ }\r
+ }\r
+ //otherwise, try one that divides all ground term coefficients? DO_THIS\r
+ }\r
+ if( !var.isNull() ){\r
+ Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;\r
+ doInstantiation( f, d_tableaux_term[x], x, m, var );\r
+ }else{\r
+ Debug("quant-arith-simplex") << "Could not find var." << std::endl;\r
+ }\r
+ ////choose a new variable based on alternation strategy\r
+ //int index = d_counter%(int)d_th->d_ceTableaux[x].size();\r
+ //Node var;\r
+ //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){\r
+ // if( index==0 ){\r
+ // var = it->first;\r
+ // break;\r
+ // }\r
+ // index--;\r
+ //}\r
+ //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );\r
+ }\r
+ }\r
+ }\r
+ return STATUS_UNKNOWN;\r
+}\r
+\r
+\r
+void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){\r
+ if( n.getKind()==MULT ){\r
+ if( n[1].hasAttribute(InstConstantAttribute()) ){\r
+ f = n[1].getAttribute(InstConstantAttribute());\r
+ if( n[1].getKind()==INST_CONSTANT ){\r
+ d_ceTableaux[x][ n[1] ] = n[0];\r
+ }else{\r
+ d_tableaux_ce_term[x][ n[1] ] = n[0];\r
+ }\r
+ }else{\r
+ d_tableaux[x][ n[1] ] = n[0];\r
+ t << n;\r
+ }\r
+ }else{\r
+ if( n.hasAttribute(InstConstantAttribute()) ){\r
+ f = n.getAttribute(InstConstantAttribute());\r
+ if( n.getKind()==INST_CONSTANT ){\r
+ d_ceTableaux[x][ n ] = Node::null();\r
+ }else{\r
+ d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );\r
+ }\r
+ }else{\r
+ d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );\r
+ t << n;\r
+ }\r
+ }\r
+}\r
+\r
+void InstStrategySimplex::debugPrint( const char* c ){\r
+ ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();\r
+ for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){\r
+ ArithVar x = (*it).first;\r
+ Node n = (*it).second;\r
+ //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){\r
+ Debug(c) << x << " : " << n << ", bounds = ";\r
+ if( d_th->d_partialModel.hasLowerBound( x ) ){\r
+ Debug(c) << d_th->d_partialModel.getLowerBound( x );\r
+ }else{\r
+ Debug(c) << "-infty";\r
+ }\r
+ Debug(c) << " <= ";\r
+ Debug(c) << d_th->d_partialModel.getAssignment( x );\r
+ Debug(c) << " <= ";\r
+ if( d_th->d_partialModel.hasUpperBound( x ) ){\r
+ Debug(c) << d_th->d_partialModel.getUpperBound( x );\r
+ }else{\r
+ Debug(c) << "+infty";\r
+ }\r
+ Debug(c) << std::endl;\r
+ //Debug(c) << " Term = " << d_tableaux_term[x] << std::endl;\r
+ //Debug(c) << " ";\r
+ //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){\r
+ // Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";\r
+ //}\r
+ //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){\r
+ // Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";\r
+ //}\r
+ //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){\r
+ // Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";\r
+ //}\r
+ //Debug(c) << std::endl;\r
+ //}\r
+ }\r
+ Debug(c) << std::endl;\r
+\r
+ for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){\r
+ Node f = d_quantEngine->getQuantifier( q );\r
+ Debug(c) << f << std::endl;\r
+ Debug(c) << " Inst constants: ";\r
+ for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){\r
+ if( i>0 ){\r
+ Debug( c ) << ", ";\r
+ }\r
+ Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );\r
+ }\r
+ Debug(c) << std::endl;\r
+ Debug(c) << " Instantiation rows: ";\r
+ for( int i=0; i<(int)d_instRows[f].size(); i++ ){\r
+ if( i>0 ){\r
+ Debug(c) << ", ";\r
+ }\r
+ Debug(c) << d_instRows[f][i];\r
+ }\r
+ Debug(c) << std::endl;\r
+ }\r
+}\r
+\r
+//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,\r
+// where var is an instantiation constant from f,\r
+// t[e] is a vector of terms containing instantiation constants from f,\r
+// and term is a ground term (c1*t1 + ... + cn*tn).\r
+// We construct the term ( beta - term )/coeff to use as an instantiation for var.\r
+bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){\r
+ //first try +delta\r
+ if( doInstantiation2( f, term, x, m, var ) ){\r
+ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith);\r
+ return true;\r
+ }else{\r
+#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA\r
+ //otherwise try -delta\r
+ if( doInstantiation2( f, term, x, m, var, true ) ){\r
+ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus);\r
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+#else\r
+ return false;\r
+#endif\r
+ }\r
+}\r
+\r
+bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){\r
+ // make term ( beta - term )/coeff\r
+ Node beta = getTableauxValue( x, minus_delta );\r
+ Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );\r
+ if( !d_ceTableaux[x][var].isNull() ){\r
+ if( var.getType().isInteger() ){\r
+ Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );\r
+ instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal );\r
+ }else{\r
+ Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() );\r
+ instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );\r
+ }\r
+ }\r
+ instVal = Rewriter::rewrite( instVal );\r
+ //use as instantiation value for var\r
+ m.set(var, instVal);\r
+ Debug("quant-arith") << "Add instantiation " << m << std::endl;\r
+ return d_quantEngine->addInstantiation( f, m );\r
+}\r
+\r
+Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){\r
+ if( d_th->d_arithvarNodeMap.hasArithVar(n) ){\r
+ ArithVar v = d_th->d_arithvarNodeMap.asArithVar( n );\r
+ return getTableauxValue( v, minus_delta );\r
+ }else{\r
+ return NodeManager::currentNM()->mkConst( Rational(0) );\r
+ }\r
+}\r
+\r
+Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){\r
+ const Rational& delta = d_th->d_partialModel.getDelta();\r
+ DeltaRational drv = d_th->d_partialModel.getAssignment( v );\r
+ Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );\r
+ return mkRationalNode(qmodel);\r
+}\r
+\r
+\r
+InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) :\r
+ InstStrategy( qe ), d_th( th ){\r
+\r
+}\r
+\r
+bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){\r
+ //DO_THIS\r
+ return false;\r
+}\r
+\r
+void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){\r
+\r
+}\r
+\r
+int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){\r
+ Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;\r
+ if( e<2 ){\r
+ return InstStrategy::STATUS_UNFINISHED;\r
+ }else if( e==2 ){\r
+ InstMatch m;\r
+ for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){\r
+ Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );\r
+ if( i.getType().isDatatype() ){\r
+ Node n = getValueFor( i );\r
+ Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;\r
+ m.set(i,n);\r
+ }\r
+ }\r
+ //d_quantEngine->addInstantiation( f, m );\r
+ }\r
+ return InstStrategy::STATUS_UNKNOWN;\r
+}\r
+\r
+Node InstStrategyDatatypesValue::getValueFor( Node n ){\r
+ //simply get the ground value for n in the current model, if it exists,\r
+ // or return an arbitrary ground term otherwise\r
+ if( !n.hasAttribute(InstConstantAttribute()) ){\r
+ return n;\r
+ }else{\r
+ return n;\r
+ }\r
+ /* FIXME\r
+\r
+ Debug("quant-datatypes-debug") << "get value for " << n << std::endl;\r
+ if( !n.hasAttribute(InstConstantAttribute()) ){\r
+ return n;\r
+ }else{\r
+ Assert( n.getType().isDatatype() );\r
+ //check if in equivalence class with ground term\r
+ Node rep = getRepresentative( n );\r
+ Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl;\r
+ if( !rep.hasAttribute(InstConstantAttribute()) ){\r
+ return rep;\r
+ }else{\r
+ if( !n.getType().isDatatype() ){\r
+ return n.getType().mkGroundTerm();\r
+ }else{\r
+ if( n.getKind()==APPLY_CONSTRUCTOR ){\r
+ std::vector< Node > children;\r
+ children.push_back( n.getOperator() );\r
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){\r
+ children.push_back( getValueFor( n[i] ) );\r
+ }\r
+ return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );\r
+ }else{\r
+ const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();\r
+ TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels;\r
+ //otherwise, use which constructor the inst constant is current chosen to be\r
+ if( labels->find( n )!=labels->end() ){\r
+ TheoryDatatypes::EqList* lbl = (*labels->find( n )).second;\r
+ int tIndex = -1;\r
+ if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){\r
+ Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl;\r
+ tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr());\r
+ }else{\r
+ Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl;\r
+ //must find a possible choice\r
+ vector< bool > possibleCons;\r
+ possibleCons.resize( dt.getNumConstructors(), true );\r
+ for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {\r
+ Node leqn = (*j);\r
+ possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;\r
+ }\r
+ for( unsigned int j=0; j<possibleCons.size(); j++ ) {\r
+ if( possibleCons[j] ){\r
+ tIndex = j;\r
+ break;\r
+ }\r
+ }\r
+ }\r
+ Assert( tIndex!=-1 );\r
+ Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() );\r
+ Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl;\r
+ std::vector< Node > children;\r
+ children.push_back( cons );\r
+ for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) {\r
+ Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n );\r
+ if( n.hasAttribute(InstConstantAttribute()) ){\r
+ InstConstantAttribute ica;\r
+ sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) );\r
+ }\r
+ Node snn = getValueFor( sn );\r
+ children.push_back( snn );\r
+ }\r
+ return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );\r
+ }else{\r
+ return n.getType().mkGroundTerm();\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
+ */\r
+}\r
--- /dev/null
+/********************* */\r
+/*! \file inst_strategy_cbqi.h\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): mdeters\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief instantiator_arith_instantiator\r
+ **/\r
+\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__INST_STRATEGT_CBQI_H\r
+#define __CVC4__INST_STRATEGT_CBQI_H\r
+\r
+#include "theory/quantifiers/instantiation_engine.h"\r
+#include "theory/arith/arithvar_node_map.h"\r
+\r
+#include "util/statistics_registry.h"\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+\r
+namespace arith {\r
+ class TheoryArith;\r
+}\r
+\r
+namespace datatypes {\r
+ class TheoryDatatypes;\r
+}\r
+\r
+namespace quantifiers {\r
+\r
+\r
+class InstStrategySimplex : public InstStrategy{\r
+protected:\r
+ /** calculate if we should process this quantifier */\r
+ bool calculateShouldProcess( Node f );\r
+private:\r
+ /** reference to theory arithmetic */\r
+ arith::TheoryArith* d_th;\r
+ /** delta */\r
+ std::map< TypeNode, Node > d_deltas;\r
+ /** for each quantifier, simplex rows */\r
+ std::map< Node, std::vector< arith::ArithVar > > d_instRows;\r
+ /** tableaux */\r
+ std::map< arith::ArithVar, Node > d_tableaux_term;\r
+ std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term;\r
+ std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux;\r
+ /** ce tableaux */\r
+ std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux;\r
+ /** get value */\r
+ Node getTableauxValue( Node n, bool minus_delta = false );\r
+ Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );\r
+ /** do instantiation */\r
+ bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var );\r
+ bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );\r
+ /** add term to row */\r
+ void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t );\r
+ /** print debug */\r
+ void debugPrint( const char* c );\r
+private:\r
+ /** */\r
+ int d_counter;\r
+ /** negative one */\r
+ Node d_negOne;\r
+ /** process functions */\r
+ void processResetInstantiationRound( Theory::Effort effort );\r
+ int process( Node f, Theory::Effort effort, int e );\r
+public:\r
+ InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );\r
+ ~InstStrategySimplex(){}\r
+ /** identify */\r
+ std::string identify() const { return std::string("Simplex"); }\r
+};\r
+\r
+\r
+class InstStrategyDatatypesValue : public InstStrategy\r
+{\r
+protected:\r
+ /** calculate if we should process this quantifier */\r
+ bool calculateShouldProcess( Node f );\r
+private:\r
+ /** reference to theory datatypes */\r
+ datatypes::TheoryDatatypes* d_th;\r
+ /** get value function */\r
+ Node getValueFor( Node n );\r
+public:\r
+ //constructor\r
+ InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );\r
+ ~InstStrategyDatatypesValue(){}\r
+ /** reset instantiation */\r
+ void processResetInstantiationRound( Theory::Effort effort );\r
+ /** process method, returns a status */\r
+ int process( Node f, Theory::Effort effort, int e );\r
+ /** identify */\r
+ std::string identify() const { return std::string("InstStrategyDatatypesValue"); }\r
+\r
+};/* class InstStrategy */\r
+\r
+}\r
+}\r
+}\r
+\r
+#endif
\ No newline at end of file
--- /dev/null
+/********************* */\r
+/*! \file inst_strategy_e_matching.cpp\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: mdeters\r
+ ** Minor contributors (to current version): bobot\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Implementation of e matching instantiation strategies\r
+ **/\r
+\r
+#include "theory/quantifiers/inst_strategy_e_matching.h"\r
+\r
+#include "theory/theory_engine.h"\r
+#include "theory/quantifiers/options.h"\r
+#include "theory/quantifiers/term_database.h"\r
+#include "theory/quantifiers/inst_match_generator.h"\r
+\r
+using namespace std;\r
+using namespace CVC4;\r
+using namespace CVC4::kind;\r
+using namespace CVC4::context;\r
+using namespace CVC4::theory;\r
+using namespace CVC4::theory::inst;\r
+using namespace CVC4::theory::quantifiers;\r
+\r
+#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER\r
+//#define MULTI_TRIGGER_FULL_EFFORT_HALF\r
+#define MULTI_MULTI_TRIGGERS\r
+\r
+struct sortQuantifiersForSymbol {\r
+ QuantifiersEngine* d_qe;\r
+ bool operator() (Node i, Node j) {\r
+ int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );\r
+ int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );\r
+ if( nqfsi<nqfsj ){\r
+ return true;\r
+ }else if( nqfsi>nqfsj ){\r
+ return false;\r
+ }else{\r
+ return false;\r
+ }\r
+ }\r
+};\r
+\r
+void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){\r
+ //reset triggers\r
+ for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){\r
+ for( int i=0; i<(int)it->second.size(); i++ ){\r
+ it->second[i]->resetInstantiationRound();\r
+ it->second[i]->reset( Node::null() );\r
+ }\r
+ }\r
+}\r
+\r
+int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){\r
+ if( e==0 ){\r
+ return STATUS_UNFINISHED;\r
+ }else if( e==1 ){\r
+ d_counter[f]++;\r
+ Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl;\r
+ //Notice() << "Try user-provided patterns..." << std::endl;\r
+ for( int i=0; i<(int)d_user_gen[f].size(); i++ ){\r
+ bool processTrigger = true;\r
+ if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){\r
+//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF\r
+// processTrigger = d_counter[f]%2==0;\r
+//#endif\r
+ }\r
+ if( processTrigger ){\r
+ //if( d_user_gen[f][i]->isMultiTrigger() )\r
+ //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;\r
+ InstMatch baseMatch;\r
+ int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );\r
+ //if( d_user_gen[f][i]->isMultiTrigger() )\r
+ //Notice() << " Done, numInst = " << numInst << "." << std::endl;\r
+ d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;\r
+ if( d_user_gen[f][i]->isMultiTrigger() ){\r
+ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;\r
+ }\r
+ //d_quantEngine->d_hasInstantiated[f] = true;\r
+ }\r
+ }\r
+ Debug("quant-uf-strategy") << "done." << std::endl;\r
+ //Notice() << "done" << std::endl;\r
+ }\r
+ return STATUS_UNKNOWN;\r
+}\r
+\r
+void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){\r
+ //add to generators\r
+ std::vector< Node > nodes;\r
+ for( int i=0; i<(int)pat.getNumChildren(); i++ ){\r
+ nodes.push_back( pat[i] );\r
+ }\r
+ if( Trigger::isUsableTrigger( nodes, f ) ){\r
+ //extend to literal matching\r
+ d_quantEngine->getPhaseReqTerms( f, nodes );\r
+ //check match option\r
+ int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;\r
+ d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,\r
+ options::smartTriggers() ) );\r
+ }\r
+}\r
+/*\r
+InstStrategyUserPatterns::Statistics::Statistics():\r
+ d_instantiations("InstStrategyUserPatterns::Instantiations", 0)\r
+{\r
+ StatisticsRegistry::registerStat(&d_instantiations);\r
+}\r
+\r
+InstStrategyUserPatterns::Statistics::~Statistics(){\r
+ StatisticsRegistry::unregisterStat(&d_instantiations);\r
+}\r
+*/\r
+\r
+void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){\r
+ //reset triggers\r
+ for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){\r
+ for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){\r
+ itt->first->resetInstantiationRound();\r
+ itt->first->reset( Node::null() );\r
+ }\r
+ }\r
+}\r
+\r
+int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){\r
+ int peffort = f.getNumChildren()==3 ? 2 : 1;\r
+ //int peffort = f.getNumChildren()==3 ? 2 : 1;\r
+ //int peffort = 1;\r
+ if( e<peffort ){\r
+ return STATUS_UNFINISHED;\r
+ }else{\r
+ bool gen = false;\r
+ if( e==peffort ){\r
+ if( d_counter.find( f )==d_counter.end() ){\r
+ d_counter[f] = 0;\r
+ gen = true;\r
+ }else{\r
+ d_counter[f]++;\r
+ gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;\r
+ }\r
+ }else{\r
+ gen = true;\r
+ }\r
+ if( gen ){\r
+ generateTriggers( f );\r
+ }\r
+ Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;\r
+ //Notice() << "Try auto-generated triggers..." << std::endl;\r
+ for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){\r
+ Trigger* tr = itt->first;\r
+ if( tr ){\r
+ bool processTrigger = itt->second;\r
+ if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){\r
+#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF\r
+ processTrigger = d_counter[f]%2==0;\r
+#endif\r
+ }\r
+ if( processTrigger ){\r
+ //if( tr->isMultiTrigger() )\r
+ Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl;\r
+ InstMatch baseMatch;\r
+ int numInst = tr->addInstantiations( baseMatch );\r
+ //if( tr->isMultiTrigger() )\r
+ Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl;\r
+ if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){\r
+ d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;\r
+ }else{\r
+ d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst;\r
+ }\r
+ if( tr->isMultiTrigger() ){\r
+ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;\r
+ }\r
+ //d_quantEngine->d_hasInstantiated[f] = true;\r
+ }\r
+ }\r
+ }\r
+ Debug("quant-uf-strategy") << "done." << std::endl;\r
+ //Notice() << "done" << std::endl;\r
+ }\r
+ return STATUS_UNKNOWN;\r
+}\r
+\r
+void InstStrategyAutoGenTriggers::generateTriggers( Node f ){\r
+ Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;\r
+ if( d_patTerms[0].find( f )==d_patTerms[0].end() ){\r
+ //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy\r
+ d_patTerms[0][f].clear();\r
+ d_patTerms[1][f].clear();\r
+ std::vector< Node > patTermsF;\r
+ Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );\r
+ Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;\r
+ Debug("auto-gen-trigger") << " ";\r
+ for( int i=0; i<(int)patTermsF.size(); i++ ){\r
+ Debug("auto-gen-trigger") << patTermsF[i] << " ";\r
+ }\r
+ Debug("auto-gen-trigger") << std::endl;\r
+ //extend to literal matching (if applicable)\r
+ d_quantEngine->getPhaseReqTerms( f, patTermsF );\r
+ //sort into single/multi triggers\r
+ std::map< Node, std::vector< Node > > varContains;\r
+ d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains );\r
+ for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){\r
+ if( it->second.size()==f[0].getNumChildren() ){\r
+ d_patTerms[0][f].push_back( it->first );\r
+ d_is_single_trigger[ it->first ] = true;\r
+ }else{\r
+ d_patTerms[1][f].push_back( it->first );\r
+ d_is_single_trigger[ it->first ] = false;\r
+ }\r
+ }\r
+ d_made_multi_trigger[f] = false;\r
+ Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;\r
+ Debug("auto-gen-trigger") << " ";\r
+ for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){\r
+ Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " ";\r
+ }\r
+ Debug("auto-gen-trigger") << std::endl;\r
+ Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;\r
+ Debug("auto-gen-trigger") << " ";\r
+ for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){\r
+ Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " ";\r
+ }\r
+ Debug("auto-gen-trigger") << std::endl;\r
+ }\r
+\r
+ //populate candidate pattern term vector for the current trigger\r
+ std::vector< Node > patTerms;\r
+#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER\r
+ //try to add single triggers first\r
+ for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){\r
+ if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){\r
+ patTerms.push_back( d_patTerms[0][f][i] );\r
+ }\r
+ }\r
+ //if no single triggers exist, add multi trigger terms\r
+ if( patTerms.empty() ){\r
+ patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );\r
+ }\r
+#else\r
+ patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() );\r
+ patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );\r
+#endif\r
+\r
+ if( !patTerms.empty() ){\r
+ Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;\r
+ //sort terms based on relevance\r
+ if( d_rlv_strategy==RELEVANCE_DEFAULT ){\r
+ sortQuantifiersForSymbol sqfs;\r
+ sqfs.d_qe = d_quantEngine;\r
+ //sort based on # occurrences (this will cause Trigger to select rarer symbols)\r
+ std::sort( patTerms.begin(), patTerms.end(), sqfs );\r
+ Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;\r
+ for( int i=0; i<(int)patTerms.size(); i++ ){\r
+ Debug("relevant-trigger") << " " << patTerms[i] << " (";\r
+ Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;\r
+ }\r
+ //Notice() << "Terms based on relevance: " << std::endl;\r
+ //for( int i=0; i<(int)patTerms.size(); i++ ){\r
+ // Notice() << " " << patTerms[i] << " (";\r
+ // Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;\r
+ //}\r
+ }\r
+ //now, generate the trigger...\r
+ int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;\r
+ Trigger* tr = NULL;\r
+ if( d_is_single_trigger[ patTerms[0] ] ){\r
+ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL,\r
+ options::smartTriggers() );\r
+ d_single_trigger_gen[ patTerms[0] ] = true;\r
+ }else{\r
+ //if we are re-generating triggers, shuffle based on some method\r
+ if( d_made_multi_trigger[f] ){\r
+#ifndef MULTI_MULTI_TRIGGERS\r
+ return;\r
+#endif\r
+ std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly\r
+ }else{\r
+ d_made_multi_trigger[f] = true;\r
+ }\r
+ //will possibly want to get an old trigger\r
+ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD,\r
+ options::smartTriggers() );\r
+ }\r
+ if( tr ){\r
+ if( tr->isMultiTrigger() ){\r
+ //disable all other multi triggers\r
+ for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){\r
+ if( it->first->isMultiTrigger() ){\r
+ d_auto_gen_trigger[f][ it->first ] = false;\r
+ }\r
+ }\r
+ }\r
+ //making it during an instantiation round, so must reset\r
+ if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){\r
+ tr->resetInstantiationRound();\r
+ tr->reset( Node::null() );\r
+ }\r
+ d_auto_gen_trigger[f][tr] = true;\r
+ //if we are generating additional triggers...\r
+ if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){\r
+ int index = 0;\r
+ if( index<(int)patTerms.size() ){\r
+ //Notice() << "check add additional" << std::endl;\r
+ //check if similar patterns exist, and if so, add them additionally\r
+ int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );\r
+ index++;\r
+ bool success = true;\r
+ while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){\r
+ success = false;\r
+ if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){\r
+ d_single_trigger_gen[ patTerms[index] ] = true;\r
+ Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,\r
+ options::smartTriggers() );\r
+ if( tr2 ){\r
+ //Notice() << "Add additional trigger " << patTerms[index] << std::endl;\r
+ tr2->resetInstantiationRound();\r
+ tr2->reset( Node::null() );\r
+ d_auto_gen_trigger[f][tr2] = true;\r
+ }\r
+ success = true;\r
+ }\r
+ index++;\r
+ }\r
+ //Notice() << "done check add additional" << std::endl;\r
+ }\r
+ }\r
+ }\r
+ }\r
+}\r
+/*\r
+InstStrategyAutoGenTriggers::Statistics::Statistics():\r
+ d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),\r
+ d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)\r
+{\r
+ StatisticsRegistry::registerStat(&d_instantiations);\r
+ StatisticsRegistry::registerStat(&d_instantiations_min);\r
+}\r
+\r
+InstStrategyAutoGenTriggers::Statistics::~Statistics(){\r
+ StatisticsRegistry::unregisterStat(&d_instantiations);\r
+ StatisticsRegistry::unregisterStat(&d_instantiations_min);\r
+}\r
+*/\r
+\r
+void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){\r
+}\r
+\r
+int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){\r
+ if( e<5 ){\r
+ return STATUS_UNFINISHED;\r
+ }else{\r
+ if( d_guessed.find( f )==d_guessed.end() ){\r
+ d_guessed[f] = true;\r
+ Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;\r
+ InstMatch m;\r
+ if( d_quantEngine->addInstantiation( f, m ) ){\r
+ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);\r
+ //d_quantEngine->d_hasInstantiated[f] = true;\r
+ }\r
+ }\r
+ return STATUS_UNKNOWN;\r
+ }\r
+}\r
+/*\r
+InstStrategyFreeVariable::Statistics::Statistics():\r
+ d_instantiations("InstStrategyGuess::Instantiations", 0)\r
+{\r
+ StatisticsRegistry::registerStat(&d_instantiations);\r
+}\r
+\r
+InstStrategyFreeVariable::Statistics::~Statistics(){\r
+ StatisticsRegistry::unregisterStat(&d_instantiations);\r
+}\r
+*/\r
--- /dev/null
+/********************* */\r
+/*! \file inst_strategy_e_matching.h\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): bobot, mdeters\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief E matching instantiation strategies\r
+ **/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H\r
+#define __CVC4__INST_STRATEGY_E_MATCHING_H\r
+\r
+#include "theory/quantifiers_engine.h"\r
+#include "theory/quantifiers/trigger.h"\r
+\r
+#include "context/context.h"\r
+#include "context/context_mm.h"\r
+\r
+#include "util/statistics_registry.h"\r
+#include "theory/quantifiers/instantiation_engine.h"\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+namespace quantifiers {\r
+\r
+//instantiation strategies\r
+\r
+class InstStrategyUserPatterns : public InstStrategy{\r
+private:\r
+ /** explicitly provided patterns */\r
+ std::map< Node, std::vector< inst::Trigger* > > d_user_gen;\r
+ /** counter for quantifiers */\r
+ std::map< Node, int > d_counter;\r
+ /** process functions */\r
+ void processResetInstantiationRound( Theory::Effort effort );\r
+ int process( Node f, Theory::Effort effort, int e );\r
+public:\r
+ InstStrategyUserPatterns( QuantifiersEngine* ie ) :\r
+ InstStrategy( ie ){}\r
+ ~InstStrategyUserPatterns(){}\r
+public:\r
+ /** add pattern */\r
+ void addUserPattern( Node f, Node pat );\r
+ /** get num patterns */\r
+ int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }\r
+ /** get user pattern */\r
+ inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }\r
+ /** identify */\r
+ std::string identify() const { return std::string("UserPatterns"); }\r
+};/* class InstStrategyUserPatterns */\r
+\r
+class InstStrategyAutoGenTriggers : public InstStrategy{\r
+public:\r
+ enum {\r
+ RELEVANCE_NONE,\r
+ RELEVANCE_DEFAULT,\r
+ };\r
+private:\r
+ /** trigger generation strategy */\r
+ int d_tr_strategy;\r
+ /** relevance strategy */\r
+ int d_rlv_strategy;\r
+ /** regeneration */\r
+ bool d_regenerate;\r
+ int d_regenerate_frequency;\r
+ /** generate additional triggers */\r
+ bool d_generate_additional;\r
+ /** triggers for each quantifier */\r
+ std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;\r
+ std::map< Node, int > d_counter;\r
+ /** single, multi triggers for each quantifier */\r
+ std::map< Node, std::vector< Node > > d_patTerms[2];\r
+ std::map< Node, bool > d_is_single_trigger;\r
+ std::map< Node, bool > d_single_trigger_gen;\r
+ std::map< Node, bool > d_made_multi_trigger;\r
+private:\r
+ /** process functions */\r
+ void processResetInstantiationRound( Theory::Effort effort );\r
+ int process( Node f, Theory::Effort effort, int e );\r
+ /** generate triggers */\r
+ void generateTriggers( Node f );\r
+public:\r
+ InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) :\r
+ InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){\r
+ setRegenerateFrequency( rgfr );\r
+ }\r
+ ~InstStrategyAutoGenTriggers(){}\r
+public:\r
+ /** get auto-generated trigger */\r
+ inst::Trigger* getAutoGenTrigger( Node f );\r
+ /** identify */\r
+ std::string identify() const { return std::string("AutoGenTriggers"); }\r
+ /** set regenerate frequency, if fr<0, turn off regenerate */\r
+ void setRegenerateFrequency( int fr ){\r
+ if( fr<0 ){\r
+ d_regenerate = false;\r
+ }else{\r
+ d_regenerate_frequency = fr;\r
+ d_regenerate = true;\r
+ }\r
+ }\r
+ /** set generate additional */\r
+ void setGenerateAdditional( bool val ) { d_generate_additional = val; }\r
+};/* class InstStrategyAutoGenTriggers */\r
+\r
+class InstStrategyFreeVariable : public InstStrategy{\r
+private:\r
+ /** guessed instantiations */\r
+ std::map< Node, bool > d_guessed;\r
+ /** process functions */\r
+ void processResetInstantiationRound( Theory::Effort effort );\r
+ int process( Node f, Theory::Effort effort, int e );\r
+public:\r
+ InstStrategyFreeVariable( QuantifiersEngine* qe ) :\r
+ InstStrategy( qe ){}\r
+ ~InstStrategyFreeVariable(){}\r
+ /** identify */\r
+ std::string identify() const { return std::string("FreeVariable"); }\r
+};/* class InstStrategyFreeVariable */\r
+\r
+}\r
+}/* CVC4::theory namespace */\r
+}/* CVC4 namespace */\r
+\r
+#endif\r
#include "theory/quantifiers/instantiation_engine.h"
#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/inst_strategy_e_matching.h"
+#include "theory/quantifiers/inst_strategy_cbqi.h"
+#include "theory/quantifiers/trigger.h"
using namespace std;
using namespace CVC4;
using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
+using namespace CVC4::theory::inst;
InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
}
+void InstantiationEngine::finishInit(){
+ //for UF terms
+ if( !options::finiteModelFind() || options::fmfInstEngine() ){
+ //if( options::cbqi() ){
+ // addInstStrategy( new InstStrategyCheckCESolved( this, d_quantEngine ) );
+ //}
+ //these are the instantiation strategies for basic E-matching
+ if( options::userPatternsQuant() ){
+ d_isup = new InstStrategyUserPatterns( d_quantEngine );
+ addInstStrategy( d_isup );
+ }else{
+ d_isup = NULL;
+ }
+ InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL,
+ InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 );
+ i_ag->setGenerateAdditional( true );
+ addInstStrategy( i_ag );
+ //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
+ if( !options::finiteModelFind() ){
+ addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) );
+ }
+ //d_isup->setPriorityOver( i_ag );
+ //d_isup->setPriorityOver( i_agm );
+ //i_ag->setPriorityOver( i_agm );
+ }
+ //CBQI: FIXME
+ //for arithmetic
+ //if( options::cbqi() ){
+ // addInstStrategy( new InstStrategySimplex( d_quantEngine ) );
+ //}
+ //for datatypes
+ //if( options::cbqi() ){
+ // addInstStrategy( new InstStrategyDatatypesValue( d_quantEngine ) );
+ //}
+}
+
bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
//if counterexample-based quantifier instantiation is active
//reset the quantifiers engine
Debug("inst-engine-ctrl") << "Reset IE" << std::endl;
//reset the instantiators
- for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
- if( d_quantEngine->getInstantiator( i ) ){
- d_quantEngine->getInstantiator( i )->resetInstantiationRound( effort );
+ for( size_t i=0; i<d_instStrategies.size(); ++i ){
+ InstStrategy* is = d_instStrategies[i];
+ if( isActiveStrategy( is ) ){
+ is->processResetInstantiationRound( effort );
}
}
//iterate over an internal effort level e
//int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e;
int e_use = e;
if( e_use>=0 ){
- //use each theory instantiator to instantiate f
- for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
- if( d_quantEngine->getInstantiator( i ) ){
- Debug("inst-engine-debug") << "Do " << d_quantEngine->getInstantiator( i )->identify() << " " << e_use << std::endl;
- int quantStatus = d_quantEngine->getInstantiator( i )->doInstantiation( f, effort, e_use );
+ //check each instantiation strategy
+ for( size_t i=0; i<d_instStrategies.size(); ++i ){
+ InstStrategy* is = d_instStrategies[i];
+ if( isActiveStrategy( is ) && is->shouldProcess( f ) ){
+ Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
+ int quantStatus = is->process( f, effort, e_use );
Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
InstStrategy::updateStatus( d_inst_round_status, quantStatus );
}
Debug("inst-engine") << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
//Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
if( !d_quantEngine->hasAddedLemma() ){
- Debug("inst-engine-stuck") << "No instantiations produced at this state: " << std::endl;
- for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
- if( d_quantEngine->getInstantiator( i ) ){
- d_quantEngine->getInstantiator( i )->debugPrint("inst-engine-stuck");
- Debug("inst-engine-stuck") << std::endl;
- }
- }
+ Debug("inst-engine-stuck") << "No instantiations produced at this state." << std::endl;
Debug("inst-engine-ctrl") << "---Fail." << std::endl;
return false;
}else{
Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
if( !doCbqi( f ) ){
d_quantEngine->addTermToDatabase( ceBody, true );
- //need to tell which instantiators will be responsible
- //by default, just chose the UF instantiator
- d_quantEngine->getInstantiator( theory::THEORY_UF )->setQuantifierActive( f );
}
//take into account user patterns
//add patterns
for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
//Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
- ((uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( theory::THEORY_UF ))->addUserPattern( f, subsPat[i] );
+ addUserPattern( f, subsPat[i] );
}
}
}
}
}
return Node::null();
-}
\ No newline at end of file
+}
+
+void InstantiationEngine::addUserPattern( Node f, Node pat ){
+ if( d_isup ){
+ d_isup->addUserPattern( f, pat );
+ }
+}
+
+InstantiationEngine::Statistics::Statistics():
+ d_instantiations_user_patterns("InstantiationEngine::Instantiations_User_Patterns", 0),
+ d_instantiations_auto_gen("InstantiationEngine::Instantiations_Auto_Gen", 0),
+ d_instantiations_auto_gen_min("InstantiationEngine::Instantiations_Auto_Gen_Min", 0),
+ d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0),
+ d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0),
+ d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0),
+ d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0)
+{
+ StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
+ StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
+ StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min);
+ StatisticsRegistry::registerStat(&d_instantiations_guess);
+ StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
+ StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus);
+ StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes);
+}
+
+InstantiationEngine::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns);
+ StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen);
+ StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min);
+ StatisticsRegistry::unregisterStat(&d_instantiations_guess);
+ StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
+ StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
+ StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes);
+}
namespace theory {
namespace quantifiers {
+class InstStrategyUserPatterns;
+
+/** instantiation strategy class */
+class InstStrategy {
+public:
+ enum Status {
+ STATUS_UNFINISHED,
+ STATUS_UNKNOWN,
+ STATUS_SAT,
+ };/* enum Status */
+protected:
+ /** reference to the instantiation engine */
+ QuantifiersEngine* d_quantEngine;
+ /** should process a quantifier */
+ std::map< Node, bool > d_quantActive;
+ /** calculate should process */
+ virtual bool calculateShouldProcess( Node f ) { return true; }
+public:
+ InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
+ virtual ~InstStrategy(){}
+
+ /** should process quantified formula f? */
+ bool shouldProcess( Node f ) {
+ if( d_quantActive.find( f )==d_quantActive.end() ){
+ d_quantActive[f] = calculateShouldProcess( f );
+ }
+ return d_quantActive[f];
+ }
+ /** reset instantiation */
+ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
+ /** process method, returns a status */
+ virtual int process( Node f, Theory::Effort effort, int e ) = 0;
+ /** update status */
+ static void updateStatus( int& currStatus, int addStatus ){
+ if( addStatus==STATUS_UNFINISHED ){
+ currStatus = STATUS_UNFINISHED;
+ }else if( addStatus==STATUS_UNKNOWN ){
+ if( currStatus==STATUS_SAT ){
+ currStatus = STATUS_UNKNOWN;
+ }
+ }
+ }
+ /** identify */
+ virtual std::string identify() const { return std::string("Unknown"); }
+};/* class InstStrategy */
+
class InstantiationEngine : public QuantifiersModule
{
+private:
+ /** instantiation strategies */
+ std::vector< InstStrategy* > d_instStrategies;
+ /** instantiation strategies active */
+ std::map< InstStrategy*, bool > d_instStrategyActive;
+ /** user-pattern instantiation strategy */
+ InstStrategyUserPatterns* d_isup;
+ /** is instantiation strategy active */
+ bool isActiveStrategy( InstStrategy* is ) {
+ return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
+ }
+ /** add inst strategy */
+ void addInstStrategy( InstStrategy* is ){
+ d_instStrategies.push_back( is );
+ d_instStrategyActive[is] = true;
+ }
private:
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
/** status of instantiation round (one of InstStrategy::STATUS_*) */
public:
InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
~InstantiationEngine(){}
+ /** initialize */
+ void finishInit();
bool needsCheck( Theory::Effort e );
void check( Theory::Effort e );
void assertNode( Node f );
Node explain(TNode n){ return Node::null(); }
Node getNextDecisionRequest();
+ /** add user pattern */
+ void addUserPattern( Node f, Node pat );
+public:
+ /** statistics class */
+ class Statistics {
+ public:
+ IntStat d_instantiations_user_patterns;
+ IntStat d_instantiations_auto_gen;
+ IntStat d_instantiations_auto_gen_min;
+ IntStat d_instantiations_guess;
+ IntStat d_instantiations_cbqi_arith;
+ IntStat d_instantiations_cbqi_arith_minus;
+ IntStat d_instantiations_cbqi_datatypes;
+ Statistics();
+ ~Statistics();
+ };
+ Statistics d_statistics;
};/* class InstantiationEngine */
}/* CVC4::theory::quantifiers namespace */
+++ /dev/null
-/********************* */
-/*! \file instantiator_default.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 instantiator_default class
- **/
-
-#include "theory/quantifiers/instantiator_default.h"
-#include "theory/theory_engine.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-
-InstantiatorDefault::InstantiatorDefault(context::Context* c, QuantifiersEngine* ie, Theory* th) :
- Instantiator( c, ie, th ) {
-}
-
-void InstantiatorDefault::assertNode( Node assertion ){
-}
-
-void InstantiatorDefault::processResetInstantiationRound( Theory::Effort effort ){
-}
-
-int InstantiatorDefault::process( Node f, Theory::Effort effort, int e ){
- /*
- if( e < 4 ){
- return InstStrategy::STATUS_UNFINISHED;
- }else if( e == 4 ){
- Debug("quant-default") << "Process " << f << " : " << std::endl;
- InstMatch m;
- for( int j=0; j<(int)d_quantEngine->getNumInstantiationConstants( f ); j++ ){
- Node i = d_quantEngine->getInstantiationConstant( f, j );
- Debug("quant-default") << "Getting value for " << i << std::endl;
- if( d_quantEngine->getTheoryEngine()->theoryOf( i )==getTheory() ){ //if it belongs to this theory
- Node val = d_th->getValue( i );
- Debug("quant-default") << "Default Instantiate for " << d_th->getId() << ", setting " << i << " = " << val << std::endl;
- m.set( i, val);
- }
- }
- d_quantEngine->addInstantiation( f, m );
- }
- */
- return InstStrategy::STATUS_UNKNOWN;
-}
+++ /dev/null
-/********************* */
-/*! \file instantiator_default.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** 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 instantiator_default
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H
-#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H
-
-#include <string>
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-class InstantiatorDefault : public Instantiator {
- friend class QuantifiersEngine;
-protected:
- /** reset instantiation round */
- void processResetInstantiationRound(Theory::Effort effort);
- /** process quantifier */
- int process( Node f, Theory::Effort effort, int e );
-public:
- InstantiatorDefault(context::Context* c, QuantifiersEngine* ie, Theory* th);
- ~InstantiatorDefault() { }
- /** check function, assertion is asserted to theory */
- void assertNode( Node assertion );
- /** identify */
- std::string identify() const { return std::string("InstantiatorDefault"); }
-};/* class InstantiatorDefault */
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H */
theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
-instantiator ::CVC4::theory::quantifiers::InstantiatorTheoryQuantifiers "theory/quantifiers/theory_quantifiers_instantiator.h"
properties check propagate presolve getNextDecisionRequest
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
#include "theory/uf/theory_uf_model.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/uf/theory_uf_strong_solver.h"
#include "theory/arrays/theory_arrays_model.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/model_builder.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/inst_gen.h"
+#include "theory/quantifiers/trigger.h"
using namespace std;
using namespace CVC4;
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
#include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/quantifiers/options.h"
#include "theory/arrays/theory_arrays_model.h"
#include "theory/quantifiers/first_order_model.h"
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() );
+ d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
}
}
}
#include "theory/quantifiers/model_engine.h"
#include "expr/kind.h"
#include "util/cvc4_assert.h"
-#include "theory/quantifiers/theory_quantifiers_instantiator.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/quantifiers_attributes.h"
+++ /dev/null
-/********************* */
-/*! \file theory_quantifiers_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): 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 theory_quantifiers_instantiator class
- **/
-
-#include "theory/quantifiers/theory_quantifiers_instantiator.h"
-#include "theory/quantifiers/theory_quantifiers.h"
-#include "theory/quantifiers/options.h"
-#include "theory/theory_engine.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-InstantiatorTheoryQuantifiers::InstantiatorTheoryQuantifiers(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-Instantiator( c, ie, th ){
-
-}
-
-void InstantiatorTheoryQuantifiers::assertNode( Node assertion ){
- Debug("quant-quant-assert") << "InstantiatorTheoryQuantifiers::check: " << assertion << std::endl;
- if( options::cbqi() ){
- if( assertion.hasAttribute(InstConstantAttribute()) ){
- Debug("quant-quant-assert") << " -> has constraints from " << assertion.getAttribute(InstConstantAttribute()) << std::endl;
- setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
- }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
- Debug("quant-quant-assert") << " -> has constraints from " << assertion[0].getAttribute(InstConstantAttribute()) << std::endl;
- setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
- }
- }
-}
-
-void InstantiatorTheoryQuantifiers::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-
-int InstantiatorTheoryQuantifiers::process( Node f, Theory::Effort effort, int e ){
- Debug("quant-quant") << "Quant: Try to solve (" << e << ") for " << f << "... " << std::endl;
- if( e<5 ){
- return InstStrategy::STATUS_UNFINISHED;
- }else if( e==5 ){
- //add random addition
- InstMatch m;
- if( d_quantEngine->addInstantiation( f, m ) ){
- ++(d_statistics.d_instantiations);
- }
- }
- return InstStrategy::STATUS_UNKNOWN;
-}
-
-InstantiatorTheoryQuantifiers::Statistics::Statistics():
- d_instantiations("InstantiatorTheoryQuantifiers::Instantiations_Total", 0)
-{
- StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstantiatorTheoryQuantifiers::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-
+++ /dev/null
-/********************* */
-/*! \file theory_quantifiers_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** 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 instantiator_quantifiers_instantiator
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H
-
-#include "theory/quantifiers_engine.h"
-
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class InstantiatorTheoryQuantifiers : public Instantiator{
- friend class QuantifiersEngine;
-public:
- InstantiatorTheoryQuantifiers(context::Context* c, QuantifiersEngine* ie, Theory* th);
- ~InstantiatorTheoryQuantifiers() {}
-
- /** check function, assertion is asserted to theory */
- void assertNode( Node assertion );
- /** identify */
- std::string identify() const { return std::string("InstantiatorTheoryQuantifiers"); }
-private:
- /** reset instantiation */
- void processResetInstantiationRound( Theory::Effort effort );
- /** process at effort */
- int process( Node f, Theory::Effort effort, int e );
-
- class Statistics {
- public:
- IntStat d_instantiations;
- Statistics();
- ~Statistics();
- };
- Statistics d_statistics;
-};/* class InstantiatiorTheoryQuantifiers */
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H */
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
#include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/quantifiers/candidate_generator.h"
#include "theory/uf/equality_engine.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/uf/theory_uf_strong_solver.h"
#include "theory/uf/equality_engine.h"
#include "theory/arrays/theory_arrays.h"
#include "theory/quantifiers/instantiation_engine.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/trigger.h"
#include "theory/rewriterules/efficient_e_matching.h"
#include "theory/rewriterules/rr_trigger.h"
return d_eq_query;
}
-Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){
- return d_te->theoryOf( id )->getInstantiator();
-}
+//Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){
+// return d_te->theoryOf( id )->getInstantiator();
+//}
context::Context* QuantifiersEngine::getSatContext(){
return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation();
}
+void QuantifiersEngine::finishInit(){
+ for( int i=0; i<(int)d_modules.size(); i++ ){
+ d_modules[i]->finishInit();
+ }
+}
+
void QuantifiersEngine::check( Theory::Effort e ){
CodeTimer codeTimer(d_time);
bool needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call
virtual ~QuantifiersModule(){}
//get quantifiers engine
QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
+ /** initialize */
+ virtual void finishInit() {}
/* whether this module needs to check this round */
virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
/* Call during quantifier engine's check */
QuantifiersEngine(context::Context* c, TheoryEngine* te);
~QuantifiersEngine();
/** get instantiator for id */
- Instantiator* getInstantiator( theory::TheoryId id );
+ //Instantiator* getInstantiator( theory::TheoryId id );
/** get theory engine */
TheoryEngine* getTheoryEngine() { return d_te; }
/** get equality query object for the given type. The default is the
/** get efficient e-matching utility */
EfficientEMatcher* getEfficientEMatcher() { return d_eem; }
public:
+ /** initialize */
+ void finishInit();
/** check at level */
void check( Theory::Effort e );
/** register quantifier */
}\r
\r
eq::EqualityEngine* EfficientEMatcher::getEqualityEngine(){\r
- return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();\r
+ //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();\r
+ return d_quantEngine->getMasterEqualityEngine();\r
}\r
\r
/** new node */\r
using namespace CVC4::theory;
using namespace CVC4::theory::rrinst;
-GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe){
- for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
- if(qe->getInstantiator(i) != NULL)
- d_can_gen[i] = qe->getInstantiator(i)->getRRCanGenClasses();
- else d_can_gen[i] = NULL;
- }
+GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe) : d_qe(qe){
+ d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClasses(d_qe->getMasterEqualityEngine());
}
GenericCandidateGeneratorClasses::~GenericCandidateGeneratorClasses(){
- for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
- delete(d_can_gen[i]);
- }
+ delete d_master_can_gen;
}
void GenericCandidateGeneratorClasses::resetInstantiationRound(){
- for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
- if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound();
- }
- d_can_gen_id=THEORY_FIRST;
+ d_master_can_gen->resetInstantiationRound();
}
void GenericCandidateGeneratorClasses::reset(TNode eqc){
- Assert(eqc.isNull());
- for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
- if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc);
- }
- d_can_gen_id=THEORY_FIRST;
- lookForNextTheory();
+ d_master_can_gen->reset(eqc);
}
TNode GenericCandidateGeneratorClasses::getNextCandidate(){
- Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST);
- /** No more */
- if(d_can_gen_id == THEORY_LAST) return TNode::null();
- /** Try with this theory */
- TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate();
- if( !cand.isNull() ) return cand;
- lookForNextTheory();
- return getNextCandidate();
+ return d_master_can_gen->getNextCandidate();
}
-void GenericCandidateGeneratorClasses::lookForNextTheory(){
- do{ /* look for the next available generator */
- ++d_can_gen_id;
- } while( d_can_gen_id < THEORY_LAST && d_can_gen[d_can_gen_id] == NULL);
-}
GenericCandidateGeneratorClass::GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) {
- for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
- if(d_qe->getInstantiator(i) != NULL)
- d_can_gen[i] = d_qe->getInstantiator(i)->getRRCanGenClass();
- else d_can_gen[i] = NULL;
- }
+ d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClass(d_qe->getMasterEqualityEngine());
}
GenericCandidateGeneratorClass::~GenericCandidateGeneratorClass(){
- for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
- delete(d_can_gen[i]);
- }
+ delete d_master_can_gen;
}
void GenericCandidateGeneratorClass::resetInstantiationRound(){
- for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
- if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound();
- }
- d_can_gen_id=THEORY_FIRST;
+ d_master_can_gen->resetInstantiationRound();
}
void GenericCandidateGeneratorClass::reset(TNode eqc){
- for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
- if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc);
- }
- d_can_gen_id=THEORY_FIRST;
- d_node = eqc;
- lookForNextTheory();
+ d_master_can_gen->reset(eqc);
}
TNode GenericCandidateGeneratorClass::getNextCandidate(){
- Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST);
- /** No more */
- if(d_can_gen_id == THEORY_LAST) return TNode::null();
- /** Try with this theory */
- TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate();
- if( !cand.isNull() ) return cand;
- lookForNextTheory();
- return getNextCandidate();
+ return d_master_can_gen->getNextCandidate();
}
-void GenericCandidateGeneratorClass::lookForNextTheory(){
- do{ /* look for the next available generator, where the element is */
- ++d_can_gen_id;
- } while(
- d_can_gen_id < THEORY_LAST &&
- (d_can_gen[d_can_gen_id] == NULL ||
- !d_qe->getInstantiator( d_can_gen_id )->hasTerm( d_node ))
- );
-}
class GenericCandidateGeneratorClasses: public rrinst::CandidateGenerator{
/** The candidate generators */
- rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST];
- /** The current theory which candidategenerator is used */
- TheoryId d_can_gen_id;
-
+ rrinst::CandidateGenerator* d_master_can_gen;
+ /** QuantifierEngine */
+ QuantifiersEngine* d_qe;
public:
GenericCandidateGeneratorClasses(QuantifiersEngine * qe);
~GenericCandidateGeneratorClasses();
class GenericCandidateGeneratorClass: public rrinst::CandidateGenerator{
/** The candidate generators */
- rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST];
- /** The current theory which candidategenerator is used */
- TheoryId d_can_gen_id;
- /** current node to look for equivalence class */
- Node d_node;
+ rrinst::CandidateGenerator* d_master_can_gen;
/** QuantifierEngine */
QuantifiersEngine* d_qe;
-
public:
GenericCandidateGeneratorClass(QuantifiersEngine * qe);
~GenericCandidateGeneratorClass();
void resetInstantiationRound();
-
void reset(TNode eqc);
TNode getNextCandidate();
- void lookForNextTheory();
};
}/* CVC4::theory namespace */
#include "theory/quantifiers/inst_match.h"
#include "theory/theory_engine.h"
#include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/uf/equality_engine.h"
#include "theory/arrays/theory_arrays.h"
#include "theory/datatypes/theory_datatypes.h"
#include "theory/rewriterules/rr_trigger.h"
#include "theory/theory_engine.h"
#include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/rewriterules/rr_candidate_generator.h"
#include "theory/uf/equality_engine.h"
#include "theory/theory.h"
#include "util/cvc4_assert.h"
#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/instantiator_default.h"
#include <vector>
}
void Instantiator::resetInstantiationRound(Theory::Effort effort) {
+ /*
for(int i = 0; i < (int) d_instStrategies.size(); ++i) {
if(isActiveStrategy(d_instStrategies[i])) {
d_instStrategies[i]->processResetInstantiationRound(effort);
}
}
processResetInstantiationRound(effort);
+ */
}
int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) {
+ /*
if( getQuantifierActive(f) ) {
int status = process(f, effort, e );
if(d_instStrategies.empty()) {
Debug("inst-engine-inst") << "We have no constraints from this quantifier." << endl;
return InstStrategy::STATUS_SAT;
}
+ */
+ return 0;
}
//void Instantiator::doInstantiation(int effort) {
class EqualityEngine;
}
-/** instantiation strategy class */
-class InstStrategy {
-public:
- enum Status {
- STATUS_UNFINISHED,
- STATUS_UNKNOWN,
- STATUS_SAT,
- };/* enum Status */
-protected:
- /** reference to the instantiation engine */
- QuantifiersEngine* d_quantEngine;
-
-
-public:
- InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
- virtual ~InstStrategy(){}
-
- /** reset instantiation */
- virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
- /** process method, returns a status */
- virtual int process( Node f, Theory::Effort effort, int e ) = 0;
- /** update status */
- static void updateStatus( int& currStatus, int addStatus ){
- if( addStatus==STATUS_UNFINISHED ){
- currStatus = STATUS_UNFINISHED;
- }else if( addStatus==STATUS_UNKNOWN ){
- if( currStatus==STATUS_SAT ){
- currStatus = STATUS_UNKNOWN;
- }
- }
- }
- /** identify */
- virtual std::string identify() const { return std::string("Unknown"); }
-};/* class InstStrategy */
/** instantiator class */
class Instantiator {
QuantifiersEngine* d_quantEngine;
/** reference to the theory that it looks at */
Theory* d_th;
- /** instantiation strategies */
- std::vector< InstStrategy* > d_instStrategies;
- /** instantiation strategies active */
- std::map< InstStrategy*, bool > d_instStrategyActive;
- /** has constraints from quantifier */
- std::map< Node, bool > d_quantActive;
- /** is instantiation strategy active */
- bool isActiveStrategy( InstStrategy* is ) {
- return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
- }
- /** add inst strategy */
- void addInstStrategy( InstStrategy* is ){
- d_instStrategies.push_back( is );
- d_instStrategyActive[is] = true;
- }
/** reset instantiation round */
virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
/** process quantifier */
/** print debug information */
virtual void debugPrint( const char* c ) {}
public:
- /** set has constraints from quantifier f */
- void setQuantifierActive( Node f ) { d_quantActive[f] = true; }
- /** has constraints from */
- bool getQuantifierActive( Node f ) { return d_quantActive.find(f) != d_quantActive.end() && d_quantActive[f]; }
/** reset instantiation round */
void resetInstantiationRound( Theory::Effort effort );
/** do instantiation method*/
void TheoryEngine::finishInit() {
if (d_logicInfo.isQuantified()) {
+ d_quantEngine->finishInit();
Assert(d_masterEqualityEngine == 0);
d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master");
void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
//TODO: add notification to efficient E-matching
+ if (d_logicInfo.isQuantified()) {
+ d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
+ }
}
void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
equality_engine.cpp \
symmetry_breaker.h \
symmetry_breaker.cpp \
- theory_uf_instantiator.h \
- theory_uf_instantiator.cpp \
theory_uf_strong_solver.h \
theory_uf_strong_solver.cpp \
- inst_strategy.h \
- inst_strategy.cpp \
theory_uf_model.h \
theory_uf_model.cpp
+++ /dev/null
-/********************* */
-/*! \file inst_strategy.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): bobot
- ** 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 theory uf instantiation strategies
- **/
-
-#include "theory/uf/inst_strategy.h"
-
-#include "theory/uf/theory_uf_instantiator.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/equality_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::uf;
-using namespace CVC4::theory::inst;
-
-#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
-//#define MULTI_TRIGGER_FULL_EFFORT_HALF
-#define MULTI_MULTI_TRIGGERS
-
-struct sortQuantifiersForSymbol {
- QuantifiersEngine* d_qe;
- bool operator() (Node i, Node j) {
- int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );
- int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );
- if( nqfsi<nqfsj ){
- return true;
- }else if( nqfsi>nqfsj ){
- return false;
- }else{
- return false;
- }
- }
-};
-
-void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
- //reset triggers
- for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
- for( int i=0; i<(int)it->second.size(); i++ ){
- it->second[i]->resetInstantiationRound();
- it->second[i]->reset( Node::null() );
- }
- }
-}
-
-int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
- if( e==0 ){
- return STATUS_UNFINISHED;
- }else if( e==1 ){
- d_counter[f]++;
- Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl;
- //Notice() << "Try user-provided patterns..." << std::endl;
- for( int i=0; i<(int)d_user_gen[f].size(); i++ ){
- bool processTrigger = true;
- if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){
-//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
-// processTrigger = d_counter[f]%2==0;
-//#endif
- }
- if( processTrigger ){
- //if( d_user_gen[f][i]->isMultiTrigger() )
- //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;
- InstMatch baseMatch;
- int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
- //if( d_user_gen[f][i]->isMultiTrigger() )
- //Notice() << " Done, numInst = " << numInst << "." << std::endl;
- //d_statistics.d_instantiations += numInst;
- if( d_user_gen[f][i]->isMultiTrigger() ){
- d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
- }
- //d_quantEngine->d_hasInstantiated[f] = true;
- }
- }
- Debug("quant-uf-strategy") << "done." << std::endl;
- //Notice() << "done" << std::endl;
- }
- return STATUS_UNKNOWN;
-}
-
-void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
- //add to generators
- std::vector< Node > nodes;
- for( int i=0; i<(int)pat.getNumChildren(); i++ ){
- nodes.push_back( pat[i] );
- }
- if( Trigger::isUsableTrigger( nodes, f ) ){
- //extend to literal matching
- d_quantEngine->getPhaseReqTerms( f, nodes );
- //check match option
- int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
- d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,
- options::smartTriggers() ) );
- }
-}
-/*
-InstStrategyUserPatterns::Statistics::Statistics():
- d_instantiations("InstStrategyUserPatterns::Instantiations", 0)
-{
- StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstStrategyUserPatterns::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-*/
-
-void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
- //reset triggers
- for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){
- for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
- itt->first->resetInstantiationRound();
- itt->first->reset( Node::null() );
- }
- }
-}
-
-int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
- int peffort = f.getNumChildren()==3 ? 2 : 1;
- //int peffort = f.getNumChildren()==3 ? 2 : 1;
- //int peffort = 1;
- if( e<peffort ){
- return STATUS_UNFINISHED;
- }else{
- bool gen = false;
- if( e==peffort ){
- if( d_counter.find( f )==d_counter.end() ){
- d_counter[f] = 0;
- gen = true;
- }else{
- d_counter[f]++;
- gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;
- }
- }else{
- gen = true;
- }
- if( gen ){
- generateTriggers( f );
- }
- Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;
- //Notice() << "Try auto-generated triggers..." << std::endl;
- for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){
- Trigger* tr = itt->first;
- if( tr ){
- bool processTrigger = itt->second;
- if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){
-#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
- processTrigger = d_counter[f]%2==0;
-#endif
- }
- if( processTrigger ){
- //if( tr->isMultiTrigger() )
- Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl;
- InstMatch baseMatch;
- int numInst = tr->addInstantiations( baseMatch );
- //if( tr->isMultiTrigger() )
- Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl;
- //if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
- // d_statistics.d_instantiations_min += numInst;
- //}else{
- // d_statistics.d_instantiations += numInst;
- //}
- if( tr->isMultiTrigger() ){
- d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
- }
- //d_quantEngine->d_hasInstantiated[f] = true;
- }
- }
- }
- Debug("quant-uf-strategy") << "done." << std::endl;
- //Notice() << "done" << std::endl;
- }
- return STATUS_UNKNOWN;
-}
-
-void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
- Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
- if( d_patTerms[0].find( f )==d_patTerms[0].end() ){
- //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
- d_patTerms[0][f].clear();
- d_patTerms[1][f].clear();
- std::vector< Node > patTermsF;
- Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );
- Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;
- Debug("auto-gen-trigger") << " ";
- for( int i=0; i<(int)patTermsF.size(); i++ ){
- Debug("auto-gen-trigger") << patTermsF[i] << " ";
- }
- Debug("auto-gen-trigger") << std::endl;
- //extend to literal matching (if applicable)
- d_quantEngine->getPhaseReqTerms( f, patTermsF );
- //sort into single/multi triggers
- std::map< Node, std::vector< Node > > varContains;
- d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains );
- for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
- if( it->second.size()==f[0].getNumChildren() ){
- d_patTerms[0][f].push_back( it->first );
- d_is_single_trigger[ it->first ] = true;
- }else{
- d_patTerms[1][f].push_back( it->first );
- d_is_single_trigger[ it->first ] = false;
- }
- }
- d_made_multi_trigger[f] = false;
- Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;
- Debug("auto-gen-trigger") << " ";
- for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
- Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " ";
- }
- Debug("auto-gen-trigger") << std::endl;
- Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
- Debug("auto-gen-trigger") << " ";
- for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){
- Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " ";
- }
- Debug("auto-gen-trigger") << std::endl;
- }
-
- //populate candidate pattern term vector for the current trigger
- std::vector< Node > patTerms;
-#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
- //try to add single triggers first
- for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
- if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){
- patTerms.push_back( d_patTerms[0][f][i] );
- }
- }
- //if no single triggers exist, add multi trigger terms
- if( patTerms.empty() ){
- patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
- }
-#else
- patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() );
- patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
-#endif
-
- if( !patTerms.empty() ){
- Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
- //sort terms based on relevance
- if( d_rlv_strategy==RELEVANCE_DEFAULT ){
- sortQuantifiersForSymbol sqfs;
- sqfs.d_qe = d_quantEngine;
- //sort based on # occurrences (this will cause Trigger to select rarer symbols)
- std::sort( patTerms.begin(), patTerms.end(), sqfs );
- Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
- for( int i=0; i<(int)patTerms.size(); i++ ){
- Debug("relevant-trigger") << " " << patTerms[i] << " (";
- Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
- }
- //Notice() << "Terms based on relevance: " << std::endl;
- //for( int i=0; i<(int)patTerms.size(); i++ ){
- // Notice() << " " << patTerms[i] << " (";
- // Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
- //}
- }
- //now, generate the trigger...
- int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
- Trigger* tr = NULL;
- if( d_is_single_trigger[ patTerms[0] ] ){
- tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL,
- options::smartTriggers() );
- d_single_trigger_gen[ patTerms[0] ] = true;
- }else{
- //if we are re-generating triggers, shuffle based on some method
- if( d_made_multi_trigger[f] ){
-#ifndef MULTI_MULTI_TRIGGERS
- return;
-#endif
- std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly
- }else{
- d_made_multi_trigger[f] = true;
- }
- //will possibly want to get an old trigger
- tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD,
- options::smartTriggers() );
- }
- if( tr ){
- if( tr->isMultiTrigger() ){
- //disable all other multi triggers
- for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){
- if( it->first->isMultiTrigger() ){
- d_auto_gen_trigger[f][ it->first ] = false;
- }
- }
- }
- //making it during an instantiation round, so must reset
- if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){
- tr->resetInstantiationRound();
- tr->reset( Node::null() );
- }
- d_auto_gen_trigger[f][tr] = true;
- //if we are generating additional triggers...
- if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){
- int index = 0;
- if( index<(int)patTerms.size() ){
- //Notice() << "check add additional" << std::endl;
- //check if similar patterns exist, and if so, add them additionally
- int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
- index++;
- bool success = true;
- while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
- success = false;
- if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
- d_single_trigger_gen[ patTerms[index] ] = true;
- Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,
- options::smartTriggers() );
- if( tr2 ){
- //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
- tr2->resetInstantiationRound();
- tr2->reset( Node::null() );
- d_auto_gen_trigger[f][tr2] = true;
- }
- success = true;
- }
- index++;
- }
- //Notice() << "done check add additional" << std::endl;
- }
- }
- }
- }
-}
-/*
-InstStrategyAutoGenTriggers::Statistics::Statistics():
- d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),
- d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)
-{
- StatisticsRegistry::registerStat(&d_instantiations);
- StatisticsRegistry::registerStat(&d_instantiations_min);
-}
-
-InstStrategyAutoGenTriggers::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_instantiations);
- StatisticsRegistry::unregisterStat(&d_instantiations_min);
-}
-*/
-
-void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
-}
-
-int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
- if( e<5 ){
- return STATUS_UNFINISHED;
- }else{
- if( d_guessed.find( f )==d_guessed.end() ){
- d_guessed[f] = true;
- Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;
- InstMatch m;
- if( d_quantEngine->addInstantiation( f, m ) ){
- //++(d_statistics.d_instantiations);
- //d_quantEngine->d_hasInstantiated[f] = true;
- }
- }
- return STATUS_UNKNOWN;
- }
-}
-/*
-InstStrategyFreeVariable::Statistics::Statistics():
- d_instantiations("InstStrategyGuess::Instantiations", 0)
-{
- StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstStrategyFreeVariable::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-*/
\ No newline at end of file
+++ /dev/null
-/********************* */
-/*! \file inst_strategy.h
- ** \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 Theory uf instantiation strategies
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__INST_STRATEGY_H
-#define __CVC4__INST_STRATEGY_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/trigger.h"
-
-#include "context/context.h"
-#include "context/context_mm.h"
-
-#include "util/statistics_registry.h"
-#include "theory/uf/theory_uf.h"
-
-namespace CVC4 {
-namespace theory {
-namespace uf {
-
-class InstantiatorTheoryUf;
-
-//instantiation strategies
-
-class InstStrategyUserPatterns : public InstStrategy{
-private:
- /** InstantiatorTheoryUf class */
- InstantiatorTheoryUf* d_th;
- /** explicitly provided patterns */
- std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
- /** counter for quantifiers */
- std::map< Node, int > d_counter;
- /** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
-public:
- InstStrategyUserPatterns( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
- InstStrategy( ie ), d_th( th ){}
- ~InstStrategyUserPatterns(){}
-public:
- /** add pattern */
- void addUserPattern( Node f, Node pat );
- /** get num patterns */
- int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }
- /** get user pattern */
- inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
- /** identify */
- std::string identify() const { return std::string("UserPatterns"); }
-public:
- /** statistics class */
- //class Statistics {
- //public:
- // IntStat d_instantiations;
- // Statistics();
- // ~Statistics();
- //};
- //Statistics d_statistics;
-};/* class InstStrategyUserPatterns */
-
-class InstStrategyAutoGenTriggers : public InstStrategy{
-public:
- enum {
- RELEVANCE_NONE,
- RELEVANCE_DEFAULT,
- };
-private:
- /** InstantiatorTheoryUf class */
- InstantiatorTheoryUf* d_th;
- /** trigger generation strategy */
- int d_tr_strategy;
- /** relevance strategy */
- int d_rlv_strategy;
- /** regeneration */
- bool d_regenerate;
- int d_regenerate_frequency;
- /** generate additional triggers */
- bool d_generate_additional;
- /** triggers for each quantifier */
- std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;
- std::map< Node, int > d_counter;
- /** single, multi triggers for each quantifier */
- std::map< Node, std::vector< Node > > d_patTerms[2];
- std::map< Node, bool > d_is_single_trigger;
- std::map< Node, bool > d_single_trigger_gen;
- std::map< Node, bool > d_made_multi_trigger;
-private:
- /** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
- /** generate triggers */
- void generateTriggers( Node f );
-public:
- InstStrategyAutoGenTriggers( InstantiatorTheoryUf* th, QuantifiersEngine* ie, int tstrt, int rstrt, int rgfr = -1 ) :
- InstStrategy( ie ), d_th( th ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){
- setRegenerateFrequency( rgfr );
- }
- ~InstStrategyAutoGenTriggers(){}
-public:
- /** get auto-generated trigger */
- inst::Trigger* getAutoGenTrigger( Node f );
- /** identify */
- std::string identify() const { return std::string("AutoGenTriggers"); }
- /** set regenerate frequency, if fr<0, turn off regenerate */
- void setRegenerateFrequency( int fr ){
- if( fr<0 ){
- d_regenerate = false;
- }else{
- d_regenerate_frequency = fr;
- d_regenerate = true;
- }
- }
- /** set generate additional */
- void setGenerateAdditional( bool val ) { d_generate_additional = val; }
-public:
- /** statistics class */
- //class Statistics {
- //public:
- // IntStat d_instantiations;
- // IntStat d_instantiations_min;
- // Statistics();
- // ~Statistics();
- //};
- //Statistics d_statistics;
-};/* class InstStrategyAutoGenTriggers */
-
-class InstStrategyFreeVariable : public InstStrategy{
-private:
- /** InstantiatorTheoryUf class */
- InstantiatorTheoryUf* d_th;
- /** guessed instantiations */
- std::map< Node, bool > d_guessed;
- /** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
-public:
- InstStrategyFreeVariable( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
- InstStrategy( ie ), d_th( th ){}
- ~InstStrategyFreeVariable(){}
- /** identify */
- std::string identify() const { return std::string("FreeVariable"); }
-public:
- /** statistics class */
- //class Statistics {
- //public:
- // IntStat d_instantiations;
- // Statistics();
- // ~Statistics();
- //};
- //Statistics d_statistics;
-};/* class InstStrategyFreeVariable */
-
-}/* CVC4::theory::uf namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif
theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h"
typechecker "theory/uf/theory_uf_type_rules.h"
-instantiator ::CVC4::theory::uf::InstantiatorTheoryUf "theory/uf/theory_uf_instantiator.h"
properties stable-infinite parametric
properties check propagate ppStaticLearn presolve getNextDecisionRequest
#include "theory/uf/theory_uf.h"
#include "theory/uf/options.h"
#include "theory/quantifiers/options.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/uf/theory_uf_strong_solver.h"
#include "theory/model.h"
#include "theory/type_enumerator.h"
-//included since efficient e matching needs notifications from UF
-#include "theory/rewriterules/efficient_e_matching.h"
using namespace std;
using namespace CVC4;
if (d_thss != NULL) {
d_thss->newEqClass(t);
}
- // this can be called very early, during initialization
- if (!getLogicInfo().isLocked() || getLogicInfo().isQuantified()) {
- //getQuantifiersEngine()->addTermToDatabase( t );
- }
}
void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) {
if (getLogicInfo().isQuantified()) {
- getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 );
+ //getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 );
}
}
+++ /dev/null
-/********************* */
-/*! \file theory_uf_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: bobot
- ** Minor contributors (to current version): 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 theory uf instantiator class
- **/
-
-#include "theory/uf/theory_uf_instantiator.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/rewriterules/options.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
-#include "theory/rewriterules/efficient_e_matching.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
-using namespace CVC4::theory::inst;
-
-namespace CVC4 {
-namespace theory {
-namespace uf {
-
-InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th) :
-Instantiator( c, qe, th )
-{
- if( !options::finiteModelFind() || options::fmfInstEngine() ){
- //if( options::cbqi() ){
- // addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
- //}
- //these are the instantiation strategies for basic E-matching
- if( options::userPatternsQuant() ){
- d_isup = new InstStrategyUserPatterns( this, qe );
- addInstStrategy( d_isup );
- }else{
- d_isup = NULL;
- }
- InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( this, qe, Trigger::TS_ALL,
- InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 );
- i_ag->setGenerateAdditional( true );
- addInstStrategy( i_ag );
- //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
- if( !options::finiteModelFind() ){
- addInstStrategy( new InstStrategyFreeVariable( this, qe ) );
- }
- //d_isup->setPriorityOver( i_ag );
- //d_isup->setPriorityOver( i_agm );
- //i_ag->setPriorityOver( i_agm );
- }
-}
-
-void InstantiatorTheoryUf::preRegisterTerm( Node t ){
- //d_quantEngine->addTermToDatabase( t );
-}
-
-void InstantiatorTheoryUf::assertNode( Node assertion )
-{
- Debug("quant-uf-assert") << "InstantiatorTheoryUf::check: " << assertion << std::endl;
- //preRegisterTerm( assertion );
- //INST_ELIM_TRY//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 InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){
- if( d_isup ){
- d_isup->addUserPattern( f, pat );
- setQuantifierActive( f );
- }
-}
-
-
-void InstantiatorTheoryUf::processResetInstantiationRound( Theory::Effort effort ){
- //d_ground_reps.clear();
-}
-
-int InstantiatorTheoryUf::process( Node f, Theory::Effort effort, int e ){
- Debug("quant-uf") << "UF: Try to solve (" << e << ") for " << f << "... " << std::endl;
- return InstStrategy::STATUS_SAT;
-}
-
-void InstantiatorTheoryUf::debugPrint( const char* c )
-{
-
-}
-
-bool InstantiatorTheoryUf::hasTerm( Node a ){
- return ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( a );
-}
-
-bool InstantiatorTheoryUf::areEqual( Node a, Node b ){
- if( a==b ){
- return true;
- }else if( hasTerm( a ) && hasTerm( b ) ){
- return ((TheoryUF*)d_th)->d_equalityEngine.areEqual( a, b );
- }else{
- return false;
- }
-}
-
-bool InstantiatorTheoryUf::areDisequal( Node a, Node b ){
- if( a==b ){
- return false;
- }else if( hasTerm( a ) && hasTerm( b ) ){
- return ((TheoryUF*)d_th)->d_equalityEngine.areDisequal( a, b, false );
- }else{
- return false;
- }
-}
-
-Node InstantiatorTheoryUf::getRepresentative( Node a ){
- if( hasTerm( a ) ){
- return ((TheoryUF*)d_th)->d_equalityEngine.getRepresentative( a );
- }else{
- return a;
- }
-}
-
-eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){
- return &((TheoryUF*)d_th)->d_equalityEngine;
-}
-
-void InstantiatorTheoryUf::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
- if( hasTerm( a ) ){
- a = getEqualityEngine()->getRepresentative( a );
- eq::EqClassIterator eqc_iter( a, getEqualityEngine() );
- while( !eqc_iter.isFinished() ){
- if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){
- eqc.push_back( *eqc_iter );
- }
- eqc_iter++;
- }
- }
-}
-
-void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){
- if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) ){
- eq::EqClassIterator eqc_iter( getRepresentative( n ),
- &((TheoryUF*)d_th)->d_equalityEngine );
- bool firstTime = true;
- while( !eqc_iter.isFinished() ){
- if( !firstTime ){ Debug(c) << ", "; }
- Debug(c) << (*eqc_iter);
- firstTime = false;
- eqc_iter++;
- }
- }else{
- Debug(c) << n;
- }
-}
-
-rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClasses(){
- uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory());
- eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
- return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee);
-}
-
-rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClass(){
- uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory());
- eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
- return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee);
-}
-
-
-} /* namespace uf */
-} /* namespace theory */
-} /* namespace cvc4 */
+++ /dev/null
-/********************* */
-/*! \file theory_uf_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: bobot
- ** Minor contributors (to current version): 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 Theory uf instantiator
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_UF_INSTANTIATOR_H
-#define __CVC4__THEORY_UF_INSTANTIATOR_H
-
-#include "theory/uf/inst_strategy.h"
-
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "context/cdchunk_list.h"
-
-#include "util/statistics_registry.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/quantifiers/trigger.h"
-#include "theory/quantifiers/inst_match_generator.h"
-#include "util/ntuple.h"
-#include "context/cdqueue.h"
-
-namespace CVC4 {
-namespace theory {
-
-namespace quantifiers{
- class TermDb;
-}
-
-namespace uf {
-
-class InstantiatorTheoryUf : public Instantiator{
-protected:
- /** instantiation strategies */
- InstStrategyUserPatterns* d_isup;
-public:
- InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th);
- ~InstantiatorTheoryUf() {}
- /** assertNode method */
- void assertNode( Node assertion );
- /** Pre-register a term. Done one time for a Node, ever. */
- void preRegisterTerm( Node t );
- /** identify */
- std::string identify() const { return std::string("InstantiatorTheoryUf"); }
- /** debug print */
- void debugPrint( const char* c );
- /** add user pattern */
- void addUserPattern( Node f, Node pat );
-private:
- /** reset instantiation */
- void processResetInstantiationRound( Theory::Effort effort );
- /** calculate matches for quantifier f at effort */
- int process( Node f, Theory::Effort effort, int e );
-public:
- /** general queries about equality */
- bool hasTerm( Node a );
- bool areEqual( Node a, Node b );
- bool areDisequal( Node a, Node b );
- Node getRepresentative( Node a );
- Node getInternalRepresentative( Node a );
- eq::EqualityEngine* getEqualityEngine();
- void getEquivalenceClass( Node a, std::vector< Node >& eqc );
- /** general creators of candidate generators */
- rrinst::CandidateGenerator* getRRCanGenClasses();
- rrinst::CandidateGenerator* getRRCanGenClass();
-public:
- /** output eq class */
- void outputEqClass( const char* c, Node n );
-};/* class InstantiatorTheoryUf */
-
-
-
-}
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */
#include "theory/uf/theory_uf_strong_solver.h"
#include "theory/uf/theory_uf.h"
#include "theory/uf/equality_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/theory_engine.h"
+#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/term_database.h"
#include "theory/uf/options.h"
#include "theory/model.h"
projects / cvc5.git / commitdiff