}else{
//counterexample-guided instantiation for non-sygus
// enable if any quantifiers with arithmetic or datatypes
- if( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ){
+ if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) ||
+ options::cbqiAll() ){
if( !options::cbqi.wasSetByUser() ){
options::cbqi.set( true );
}
}
}
if( options::cbqi() && d_logic.isPure(THEORY_ARITH) ){
+ options::cbqiAll.set( false );
if( !options::quantConflictFind.wasSetByUser() ){
options::quantConflictFind.set( false );
}
void DatatypesEnumerator::init(){
//Assert(type.isDatatype());
- Debug("te") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
- Debug("te") << "datatype is kind " << d_type.getKind() << std::endl;
- Debug("te") << "datatype is " << d_type << std::endl;
- Debug("te") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton() << " " << d_datatype.isFinite() << std::endl;
+ Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
+ Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
+ Debug("dt-enum") << "datatype is " << d_type << std::endl;
+ Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton() << " " << d_datatype.isFinite() << std::endl;
if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
//start with uninterpreted constant
d_sel_sum.push_back( -1 );
}else{
// find the "zero" constructor via mkGroundTerm
+ Debug("dt-enum-debug") << "make ground term..." << std::endl;
Node t = d_type.mkGroundTerm();
+ Debug("dt-enum-debug") << "done : " << t << std::endl;
Assert( t.getKind()==kind::APPLY_CONSTRUCTOR );
// start with the constructor for which a ground term is constructed
d_zeroCtor = Datatype::indexOf( t.getOperator().toExpr() );
d_has_debruijn = 0;
}
+ Debug("dt-enum") << "zero ctor : " << d_zeroCtor << std::endl;
d_ctor = d_zeroCtor;
for( unsigned i=0; i<d_datatype.getNumConstructors(); ++i ){
d_sel_types.push_back( std::vector< TypeNode >() );
CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
d_match_pattern( mpat ), d_qe( qe ){
+ Assert( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF );
+ d_match_pattern_type = d_match_pattern[0].getType();
}
+
void CandidateGeneratorQELitDeq::resetInstantiationRound(){
}
+
void CandidateGeneratorQELitDeq::reset( Node eqc ){
Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) );
d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() );
}
+
Node CandidateGeneratorQELitDeq::getNextCandidate(){
//get next candidate term in equivalence class
while( !d_eqc_false.isFinished() ){
Node n = (*d_eqc_false);
++d_eqc_false;
if( n.getKind()==d_match_pattern.getKind() ){
- //found an iff or equality, try to match it
- //DO_THIS: cache to avoid redundancies?
- //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false?
- return n;
+ if( n[0].getType().isComparableTo( d_match_pattern_type ) ){
+ //found an iff or equality, try to match it
+ //DO_THIS: cache to avoid redundancies?
+ //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false?
+ return n;
+ }
}
}
return Node::null();
eq::EqClassIterator d_eqc_false;
//equality you are trying to match disequalities for
Node d_match_pattern;
+ //type of disequality
+ TypeNode d_match_pattern_type;
//einstantiator pointer
QuantifiersEngine* d_qe;
public:
}
Node eq = eq_lhs.eqNode( eq_rhs );
eq = Rewriter::rewrite( eq );
+ Node vts_coeff_inf;
+ Node vts_coeff_delta;
+ Node val;
+ Node veq_c;
+ //isolate pv in the equality
+ int ires = isolate( pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta );
+ if( ires!=0 ){
+ if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
+ subs_proc[val][veq_c] = true;
+ if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ return true;
+ }
+ }
+ }
+ /*
//cannot contain infinity?
//if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){
Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
}
}
}
+ */
}
}
lhs.push_back( ns );
}
sf.d_subs[index] = veq[1];
if( !veq_c.isNull() ){
- sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c );
+ sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c );
Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl;
//intger division rounding up if from a lower bound
if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
NodeManager::currentNM()->mkNode( ITE,
NodeManager::currentNM()->mkNode( EQUAL,
- NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
+ NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ),
d_zero ),
d_zero, d_one )
);
}
//this isolates the monomial sum into solved form (pv k t), ensures t is Int if pv is Int, and t does not contain vts symbols
-int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
+int CegInstantiator::isolate( Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
int ires = 0;
Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl;
std::map< Node, Node > msum;
if( ires!=0 ){
Node realPart;
Trace("cbqi-inst-debug") << "Isolate : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
+ if( options::cbqiAll() ){
+ // when not pure LIA/LRA, we must check whether the lhs contains pv
+ if( TermDb::containsTerm( val, pv ) ){
+ return 0;
+ }
+ }
if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){
//redo, split integer/non-integer parts
bool useCoeff = false;
if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
//make sure the matching portion of the equality is on the LHS of d_pattern
// and record what d_match_pattern is
- if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) ||
- d_match_pattern[0].getKind()==INST_CONSTANT ){
+ if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) || d_match_pattern[0].getKind()==INST_CONSTANT ){
if( d_match_pattern[1].getKind()!=INST_CONSTANT ){
Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) );
Node mp = d_match_pattern[1];
d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern;
d_match_pattern = mp;
}
- }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) ||
- d_match_pattern[1].getKind()==INST_CONSTANT ){
+ }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) || d_match_pattern[1].getKind()==INST_CONSTANT ){
if( d_match_pattern[0].getKind()!=INST_CONSTANT ){
Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) );
if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching
Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl;
Node s = d_subs.substitute( d_var, d_eq_class );
s = Rewriter::rewrite( s );
- Trace("var-trigger-matching") << "...got " << s << std::endl;
+ Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl;
d_eq_class = Node::null();
//if( s.getType().isSubtypeOf( d_var_type ) ){
d_rm_prev = m.get( d_var_num[0] ).isNull();
void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+ double clSet = 0;
+ if( Trace.isOn("cbqi-engine") ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
+ }
+ unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
for( int ee=0; ee<=1; ee++ ){
- unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
break;
}
}
+ if( Trace.isOn("cbqi-engine") ){
+ if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+ Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
+ }
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
+ }
}
}
using namespace CVC4::theory::quantifiers;
//priority levels :
-//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={ignore,resort})
+//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={resort,ignore})
//2 : user patterns (when user-pat=resort), auto gen patterns (for user pattern quantifiers when user-pat=use)
-//3 :
-//4 :
-//5 : full saturate quantifiers
// user-pat=interleave alternates between use and resort
-//#define MULTI_TRIGGER_FULL_EFFORT_HALF
-
struct sortQuantifiersForSymbol {
QuantifiersEngine* d_qe;
bool operator() (Node i, Node j) {
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++ ){
+ for( unsigned i=0; i<it->second.size(); i++ ){
it->second[i]->resetInstantiationRound();
it->second[i]->reset( Node::null() );
}
return STATUS_UNKNOWN;
}
-void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
+void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
Assert( pat.getKind()==INST_PATTERN );
//add to generators
bool usable = true;
std::vector< Node > nodes;
- for( int i=0; i<(int)pat.getNumChildren(); i++ ){
+ for( unsigned i=0; i<pat.getNumChildren(); i++ ){
nodes.push_back( pat[i] );
- if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], f ) ){
+ if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], q ) ){
Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl;
usable = false;
break;
}
}
if( usable ){
- Trace("user-pat") << "Add user pattern: " << pat << " for " << f << std::endl;
+ Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
//check match option
int matchOption = 0;
if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
- d_user_gen_wait[f].push_back( nodes );
+ d_user_gen_wait[q].push_back( nodes );
}else{
- d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) );
+ d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) );
}
}
}
}
}
-bool InstStrategyAutoGenTriggers::hasUserPatterns( Node f ) {
- if( f.getNumChildren()==3 ){
- std::map< Node, bool >::iterator it = d_hasUserPatterns.find( f );
+bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
+ if( q.getNumChildren()==3 ){
+ std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q );
if( it==d_hasUserPatterns.end() ){
bool hasPat = false;
- for( unsigned i=0; i<f[2].getNumChildren(); i++ ){
- if( f[2][i].getKind()==INST_PATTERN ){
+ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+ if( q[2][i].getKind()==INST_PATTERN ){
hasPat = true;
break;
}
}
- d_hasUserPatterns[f] = hasPat;
+ d_hasUserPatterns[q] = hasPat;
return hasPat;
}else{
return it->second;
}
}
-void InstStrategyAutoGenTriggers::addUserNoPattern( Node f, Node pat ) {
+void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) {
Assert( pat.getKind()==INST_NO_PATTERN && pat.getNumChildren()==1 );
- if( std::find( d_user_no_gen[f].begin(), d_user_no_gen[f].end(), pat[0] )==d_user_no_gen[f].end() ){
- Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << f << std::endl;
- d_user_no_gen[f].push_back( pat[0] );
+ if( std::find( d_user_no_gen[q].begin(), d_user_no_gen[q].end(), pat[0] )==d_user_no_gen[q].end() ){
+ Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << q << std::endl;
+ d_user_no_gen[q].push_back( pat[0] );
}
}
for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
- if( process( q, e ) ){
+ if( process( q, e, quant_e ) ){
//added lemma
addedLemmas++;
}
}
}
-bool FullSaturation::process( Node f, Theory::Effort effort ){
+bool FullSaturation::process( Node f, Theory::Effort effort, unsigned quant_e ){
//first, try from relevant domain
RelevantDomain * rd = d_quantEngine->getRelevantDomain();
unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
- for( unsigned r=rstart; r<2; r++ ){
- if( rd || r>0 ){
- if( r==0 ){
- Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
- }else{
- Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
+ unsigned rend = quant_e==QuantifiersEngine::QEFFORT_STANDARD ? rstart : 2;
+ for( unsigned r=rstart; r<=rend; r++ ){
+ if( r==1 ){
+ //complete guess
+ if( d_guessed.find( f )==d_guessed.end() ){
+ Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
+ d_guessed[f] = true;
+ InstMatch m( f );
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ ++(d_quantEngine->d_statistics.d_instantiations_guess);
+ return true;
+ }
}
- rd->compute();
- unsigned final_max_i = 0;
- std::vector< unsigned > maxs;
- for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
- unsigned ts;
+ }else{
+ if( rd || r>0 ){
if( r==0 ){
- ts = rd->getRDomain( f, i )->d_terms.size();
+ Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
}else{
- ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size();
+ Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
+ }
+ rd->compute();
+ bool max_zero = false;
+ unsigned final_max_i = 0;
+ std::vector< unsigned > maxs;
+ for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ unsigned ts;
+ if( r==0 ){
+ ts = rd->getRDomain( f, i )->d_terms.size();
+ }else{
+ ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size();
+ }
+ maxs.push_back( ts );
+ Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl;
+ if( ts>final_max_i ){
+ final_max_i = ts;
+ }
+ if( ts==0 ){
+ max_zero = true;
+ }
}
- maxs.push_back( ts );
- Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl;
- if( ts>final_max_i ){
- final_max_i = ts;
+ if( max_zero ){
+ final_max_i = 0;
}
- }
- Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
+ Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
- unsigned max_i = 0;
- bool success;
- while( max_i<=final_max_i ){
- Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
- std::vector< unsigned > childIndex;
- int index = 0;
- do {
- while( index>=0 && index<(int)f[0].getNumChildren() ){
- if( index==(int)childIndex.size() ){
- childIndex.push_back( -1 );
- }else{
- Assert( index==(int)(childIndex.size())-1 );
- unsigned nv = childIndex[index]+1;
- if( options::cbqi() ){
- //skip inst constant nodes
- while( nv<maxs[index] && nv<=max_i &&
- r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
- nv++;
- }
- }
- if( nv<maxs[index] && nv<=max_i ){
- childIndex[index] = nv;
- index++;
+ unsigned max_i = 0;
+ bool success;
+ while( max_i<=final_max_i ){
+ Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
+ std::vector< unsigned > childIndex;
+ int index = 0;
+ do {
+ while( index>=0 && index<(int)f[0].getNumChildren() ){
+ if( index==(int)childIndex.size() ){
+ childIndex.push_back( -1 );
}else{
- childIndex.pop_back();
- index--;
+ Assert( index==(int)(childIndex.size())-1 );
+ unsigned nv = childIndex[index]+1;
+ if( options::cbqi() ){
+ //skip inst constant nodes
+ while( nv<maxs[index] && nv<=max_i &&
+ r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
+ nv++;
+ }
+ }
+ if( nv<maxs[index] && nv<=max_i ){
+ childIndex[index] = nv;
+ index++;
+ }else{
+ childIndex.pop_back();
+ index--;
+ }
}
}
- }
- success = index>=0;
- if( success ){
- Trace("inst-alg-rd") << "Try instantiation { ";
- for( unsigned j=0; j<childIndex.size(); j++ ){
- Trace("inst-alg-rd") << childIndex[j] << " ";
- }
- Trace("inst-alg-rd") << "}" << std::endl;
- //try instantiation
- std::vector< Node > terms;
- for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- if( r==0 ){
- terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+ success = index>=0;
+ if( success ){
+ Trace("inst-alg-rd") << "Try instantiation { ";
+ for( unsigned j=0; j<childIndex.size(); j++ ){
+ Trace("inst-alg-rd") << childIndex[j] << " ";
+ }
+ Trace("inst-alg-rd") << "}" << std::endl;
+ //try instantiation
+ std::vector< Node > terms;
+ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ if( r==0 ){
+ terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+ }else{
+ terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
+ }
+ }
+ if( d_quantEngine->addInstantiation( f, terms, false ) ){
+ Trace("inst-alg-rd") << "Success!" << std::endl;
+ ++(d_quantEngine->d_statistics.d_instantiations_guess);
+ return true;
}else{
- terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
+ index--;
}
}
- if( d_quantEngine->addInstantiation( f, terms, false ) ){
- Trace("inst-alg-rd") << "Success!" << std::endl;
- ++(d_quantEngine->d_statistics.d_instantiations_guess);
- return true;
- }else{
- index--;
- }
- }
- }while( success );
- max_i++;
- }
- }
- if( r==0 ){
- //complete guess
- if( d_guessed.find( f )==d_guessed.end() ){
- Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
- d_guessed[f] = true;
- InstMatch m( f );
- if( d_quantEngine->addInstantiation( f, m ) ){
- ++(d_quantEngine->d_statistics.d_instantiations_guess);
- return true;
+ }while( success );
+ max_i++;
}
}
}
~InstStrategyUserPatterns(){}
public:
/** add pattern */
- void addUserPattern( Node f, Node pat );
+ void addUserPattern( Node q, Node pat );
/** get num patterns */
- int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }
+ int getNumUserGenerators( Node q ) { return (int)d_user_gen[q].size(); }
/** get user pattern */
- inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
+ inst::Trigger* getUserGenerator( Node q, int i ) { return d_user_gen[q][ i ]; }
/** identify */
std::string identify() const { return std::string("UserPatterns"); }
};/* class InstStrategyUserPatterns */
private:
/** process functions */
void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
+ int process( Node q, Theory::Effort effort, int e );
/** generate triggers */
- void generateTriggers( Node f, Theory::Effort effort, int e, int& status );
+ void generateTriggers( Node q, Theory::Effort effort, int e, int& status );
//bool addTrigger( inst::Trigger * tr, Node f, unsigned r );
/** has user patterns */
- bool hasUserPatterns( Node f );
+ bool hasUserPatterns( Node q );
/** has user patterns */
std::map< Node, bool > d_hasUserPatterns;
public:
~InstStrategyAutoGenTriggers(){}
public:
/** get auto-generated trigger */
- inst::Trigger* getAutoGenTrigger( Node f );
+ inst::Trigger* getAutoGenTrigger( Node q );
/** identify */
std::string identify() const { return std::string("AutoGenTriggers"); }
/** add pattern */
- void addUserNoPattern( Node f, Node pat );
+ void addUserNoPattern( Node q, Node pat );
};/* class InstStrategyAutoGenTriggers */
class FullSaturation : public QuantifiersModule {
/** guessed instantiations */
std::map< Node, bool > d_guessed;
/** process functions */
- bool process( Node f, Theory::Effort effort );
+ bool process( Node q, Theory::Effort effort, unsigned quant_e );
public:
FullSaturation( QuantifiersEngine* qe );
~FullSaturation(){}
if( !d_quantEngine->hasAddedLemma() ){
return false;
}else{
- Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting) << std::endl;
+ Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
return true;
}
}
}
}
-void InstantiationEngine::addUserPattern( Node f, Node pat ){
+void InstantiationEngine::addUserPattern( Node q, Node pat ){
if( d_isup ){
- d_isup->addUserPattern( f, pat );
+ d_isup->addUserPattern( q, pat );
}
}
-void InstantiationEngine::addUserNoPattern( Node f, Node pat ){
+void InstantiationEngine::addUserNoPattern( Node q, Node pat ){
if( d_i_ag ){
- d_i_ag->addUserNoPattern( f, pat );
+ d_i_ag->addUserNoPattern( q, pat );
}
}
void registerQuantifier( Node q );
Node explain(TNode n){ return Node::null(); }
/** add user pattern */
- void addUserPattern( Node f, Node pat );
- void addUserNoPattern( Node f, Node pat );
+ void addUserPattern( Node q, Node pat );
+ void addUserNoPattern( Node q, Node pat );
public:
/** Identify this module */
std::string identify() const { return "InstEngine"; }
perform aggressive miniscoping for quantifiers
option elimTautQuant --elim-taut-quant bool :default true
eliminate tautological disjuncts of quantified formulas
+option purifyQuant --purify-quant bool :default false
+ purify quantified formulas
#### E-matching options
answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
option cbqiModel --cbqi-model bool :read-write :default true
guide instantiations by model values for counterexample-based quantifier instantiation
-option cbqiAll --cbqi-all bool :default false
+option cbqiAll --cbqi-all bool :read-write :default false
apply counterexample-based instantiation to all quantified formulas
option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false
use integer infinity for vts in counterexample-based quantifier instantiation
it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second );
msum[it->first] = Rewriter::rewrite( r );
}else{
- msum[it->first] = negate( it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second );
+ msum[it->first] = it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(-1) ) : negate( it->second );
}
}
return true;
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/trigger.h"
using namespace std;
using namespace CVC4;
}
}
+int QuantifiersRewriter::getPurifyId( Node n ){
+ if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){
+ return 1;
+ }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL ){
+ return 0;
+ }else{
+ return -1;
+ }
+}
+
void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
if( n.getKind()==OR ){
for( int i=0; i<(int)n.getNumChildren(); i++ ){
return body;
}
+bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) {
+ if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){
+ return false;
+ }else{
+ if( !var_parent.empty() ){
+ std::map< Node, std::vector< int > >::iterator it = var_parent.find( v );
+ if( it!=var_parent.end() ){
+ Assert( !it->second.empty() );
+ int id = getPurifyId( s );
+ return it->second.size()==1 && it->second[0]==id;
+ }
+ }
+ return true;
+ }
+}
-Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
- Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
- QuantPhaseReq qpr( body );
- std::vector< Node > vars;
- std::vector< Node > subs;
- for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
- //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
- if( it->first.getKind()==EQUAL ){
- if( it->second && options::varElimQuant() ){
- TypeNode types[2];
- for( int i=0; i<2; i++ ){
- types[i] = it->first[i].getType();
+bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vector< Node >& args, std::vector< Node >& vars, std::vector< Node >& subs,
+ std::map< Node, std::vector< int > >& var_parent ) {
+ if( lit.getKind()==EQUAL && pol ){
+ for( unsigned i=0; i<2; i++ ){
+ std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[i] );
+ if( ita!=args.end() ){
+ if( isVariableElim( lit[i], lit[1-i], var_parent ) ){
+ vars.push_back( lit[i] );
+ subs.push_back( lit[1-i] );
+ args.erase( ita );
+ return true;
}
- for( int i=0; i<2; i++ ){
- std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] );
+ }
+ }
+ //for arithmetic, solve the equality
+ if( lit[0].getType().isReal() ){
+ std::map< Node, Node > msum;
+ if( QuantArith::getMonomialSumLit( lit, msum ) ){
+ for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
+ std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first );
if( ita!=args.end() ){
- if( !TermDb::containsTerm( it->first[1-i], it->first[i] ) && types[1-i].isSubtypeOf( types[i] ) ){
- vars.push_back( it->first[i] );
- subs.push_back( it->first[1-i] );
+ Node veq_c;
+ Node val;
+ int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL );
+ if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, var_parent ) ){
+ vars.push_back( itm->first );
+ subs.push_back( val );
args.erase( ita );
- break;
+ return true;
}
}
}
- if( !vars.empty() ){
- break;
- }
}
- }else if( it->first.getKind()==APPLY_TESTER ){
- if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){
- Trace("var-elim-dt") << "Expand datatype variable based on : " << it->first << std::endl;
- std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] );
- if( ita!=args.end() ){
- vars.push_back( it->first[0] );
- Expr testerExpr = it->first.getOperator().toExpr();
- int index = Datatype::indexOf( testerExpr );
- const Datatype& dt = Datatype::datatypeOf(testerExpr);
- const DatatypeConstructor& c = dt[index];
- std::vector< Node > newChildren;
- newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
- std::vector< Node > newVars;
- for( unsigned j=0; j<c.getNumArgs(); j++ ){
- TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
- tn = tn[1];
- Node v = NodeManager::currentNM()->mkBoundVar( tn );
- newChildren.push_back( v );
- newVars.push_back( v );
- }
- subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) );
- Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
- args.erase( ita );
- args.insert( args.end(), newVars.begin(), newVars.end() );
- }
- }
- }else if( it->first.getKind()==BOUND_VARIABLE ){
- if( options::varElimQuant() ){
- std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first );
- if( ita!=args.end() ){
- Trace("var-elim-bool") << "Variable eliminate : " << it->first << " in " << body << std::endl;
- vars.push_back( it->first );
- subs.push_back( NodeManager::currentNM()->mkConst( it->second ) );
- args.erase( ita );
- }
+ }
+ }else if( lit.getKind()==APPLY_TESTER && pol && lit[0].getKind()==BOUND_VARIABLE ){
+ Trace("var-elim-dt") << "Expand datatype variable based on : " << lit << std::endl;
+ std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[0] );
+ if( ita!=args.end() ){
+ vars.push_back( lit[0] );
+ Expr testerExpr = lit.getOperator().toExpr();
+ int index = Datatype::indexOf( testerExpr );
+ const Datatype& dt = Datatype::datatypeOf(testerExpr);
+ const DatatypeConstructor& c = dt[index];
+ std::vector< Node > newChildren;
+ newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
+ std::vector< Node > newVars;
+ for( unsigned j=0; j<c.getNumArgs(); j++ ){
+ TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
+ tn = tn[1];
+ Node v = NodeManager::currentNM()->mkBoundVar( tn );
+ newChildren.push_back( v );
+ newVars.push_back( v );
+ }
+ subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) );
+ Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
+ args.erase( ita );
+ args.insert( args.end(), newVars.begin(), newVars.end() );
+ return true;
+ }
+ }else if( lit.getKind()==BOUND_VARIABLE ){
+ std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit );
+ if( ita!=args.end() ){
+ Trace("var-elim-bool") << "Variable eliminate : " << lit << std::endl;
+ vars.push_back( lit );
+ subs.push_back( NodeManager::currentNM()->mkConst( pol ) );
+ args.erase( ita );
+ return true;
+ }
+ }
+ return false;
+}
+
+Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent ){
+ Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
+ QuantPhaseReq qpr( body );
+ std::vector< Node > vars;
+ std::vector< Node > subs;
+ for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
+ //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
+ if( ( it->first.getKind()==EQUAL && it->second && options::varElimQuant() ) ||
+ ( it->first.getKind()==APPLY_TESTER && it->second && it->first[0].getKind()==BOUND_VARIABLE && options::dtVarExpandQuant() ) ||
+ ( it->first.getKind()==BOUND_VARIABLE && options::varElimQuant() ) ){
+ if( computeVariableElimLit( it->first, it->second, args, vars, subs, var_parent ) ){
+ break;
}
}
}
return body;
}
+Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
+ //the parent id's for each variable, if using purifyQuant
+ std::map< Node, std::vector< int > > var_parent;
+ if( options::purifyQuant() ){
+ body = computePurify( body, args, var_parent );
+ }
+ if( options::varElimQuant() || options::dtVarExpandQuant() ){
+ Node prev;
+ do{
+ prev = body;
+ body = computeVarElimination2( body, args, ipl, var_parent );
+ }while( prev!=body && !args.empty() );
+ }
+ return body;
+}
+
Node QuantifiersRewriter::computeClause( Node n ){
Assert( isClause( n ) );
if( isLiteral( n ) ){
}else if( computeOption==COMPUTE_PRENEX ){
return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
- return options::varElimQuant() || options::dtVarExpandQuant();
+ return options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant();
//}else if( computeOption==COMPUTE_CNF ){
// return options::cnfQuant();
}else{
}else if( computeOption==COMPUTE_PRENEX ){
n = computePrenex( n, args, true );
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
- Node prev;
- do{
- prev = n;
- n = computeVarElimination( n, args, ipl );
- }while( prev!=n && !args.empty() );
+ n = computeVarElimination( n, args, ipl );
//}else if( computeOption==COMPUTE_CNF ){
//n = computeCNF( n, args, defs, false );
//ipl = Node::null();
}
return n;
}
+
+
+Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term,
+ std::map< Node, std::vector< int > >& var_parent, int parentId ){
+ std::map< Node, Node >::iterator it = visited.find( body );
+ if( it!=visited.end() ){
+ return it->second;
+ }else{
+ Node ret = body;
+ if( body.getNumChildren()>0 && body.getKind()!=FORALL ){
+ std::vector< Node > children;
+ bool childrenChanged = false;
+ int id = getPurifyId( body );
+ for( unsigned i=0; i<body.getNumChildren(); i++ ){
+ Node bi = computePurify2( body[i], args, visited, var_to_term, var_parent, id );
+ childrenChanged = childrenChanged || bi!=body[i];
+ children.push_back( bi );
+ if( id!=0 && bi.getKind()==BOUND_VARIABLE ){
+ if( std::find( var_parent[bi].begin(), var_parent[bi].end(), id )==var_parent[bi].end() ){
+ var_parent[bi].push_back( id );
+ }
+ }
+ }
+ if( childrenChanged ){
+ if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.insert( children.begin(), body.getOperator() );
+ }
+ ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
+ }
+ if( parentId!=0 && parentId!=id ){
+ //must purify if this has a bound variable
+ if( TermDb::containsTerms( ret, args ) ){
+ Node v = NodeManager::currentNM()->mkBoundVar( ret.getType() );
+ var_to_term[v] = Rewriter::rewrite( v.eqNode( ret ) );
+ ret = v;
+ args.push_back( v );
+ }
+ }
+ }
+ visited[body] = ret;
+ return ret;
+ }
+}
+
+Node QuantifiersRewriter::computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) {
+ std::map< Node, Node > visited;
+ std::map< Node, Node > var_to_term;
+ Node pbody = computePurify2( body, args, visited, var_to_term, var_parent, 0 );
+ if( pbody==body ){
+ return body;
+ }else{
+ Trace("quantifiers-rewrite-purify") << "Purify : " << body << std::endl;
+ Trace("quantifiers-rewrite-purify") << " Got : " << pbody << std::endl;
+ for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){
+ Trace("quantifiers-rewrite-purify") << " " << it->first << " : " << it->second << std::endl;
+ }
+ Trace("quantifiers-rewrite-purify") << "Variable parents : " << std::endl;
+ for( std::map< Node, std::vector< int > >::iterator it = var_parent.begin(); it != var_parent.end(); ++it ){
+ Trace("quantifiers-rewrite-purify") << " " << it->first << " -> ";
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ Trace("quantifiers-rewrite-purify") << it->second[i] << " ";
+ }
+ Trace("quantifiers-rewrite-purify") << std::endl;
+ }
+ Trace("quantifiers-rewrite-purify") << std::endl;
+ std::vector< Node > disj;
+ for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){
+ disj.push_back( it->second.negate() );
+ }
+ Node res;
+ if( disj.empty() ){
+ res = pbody;
+ }else{
+ disj.push_back( pbody );
+ res = NodeManager::currentNM()->mkNode( OR, disj );
+ }
+ Trace("quantifiers-rewrite-purify") << "Constructed : " << res << std::endl << std::endl;
+ return res;
+ }
+}
static bool isClause( Node n );
static bool isLiteral( Node n );
static bool isCube( Node n );
+ static int getPurifyId( Node n );
private:
static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
static Node mkForAll( std::vector< Node >& args, Node body, Node ipl );
static Node computeClause( Node n );
static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
static bool isConditionalVariableElim( Node n, int pol=0 );
+ static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent );
+ static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs,
+ std::map< Node, std::vector< int > >& var_parent );
+ static Node computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term,
+ std::map< Node, std::vector< int > >& var_parent, int parentId );
+ static Node computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent );
private:
static Node computeElimSymbols( Node body );
static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
std::map< Node, Node >& cache, std::map< Node, Node >& icache,
std::vector< Node >& new_vars, std::vector< Node >& new_conds );
static Node computeProcessIte( Node body, Node ipl );
- static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
static Node computeSplit( Node f, std::vector< Node >& args, Node body );
+ static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
+ static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent );
private:
enum{
COMPUTE_ELIM_SYMBOLS = 0,
return !getInstConstAttr(n).isNull();
}
-void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) {
- if (n.getKind()==BOUND_VARIABLE ){
- if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){
- bvs.push_back( n );
- }
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++) {
- getBoundVars(n[i], bvs);
- }
- }
-}
-
-
/** get the i^th instantiation constant of q */
Node TermDb::getInstantiationConstant( Node q, int i ) const {
std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
static Node getInstConstAttr( Node n );
static bool hasInstConstAttr( Node n );
-//for bound variables
-public:
- //get bound variables in n
- static void getBoundVars( Node n, std::vector< Node >& bvs );
//for skolem
return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers );
}
-bool Trigger::isUsable( Node n, Node f ){
- if( quantifiers::TermDb::getInstConstAttr(n)==f ){
+bool Trigger::isUsable( Node n, Node q ){
+ if( quantifiers::TermDb::getInstConstAttr(n)==q ){
if( isAtomicTrigger( n ) ){
for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( !isUsable( n[i], f ) ){
+ if( !isUsable( n[i], q ) ){
return false;
}
}
std::map< Node, Node > coeffs;
if( isBooleanTermTrigger( n ) ){
return true;
- }
- if( options::purifyTriggers() ){
+ }else if( options::purifyTriggers() ){
Node x = getInversionVariable( n );
if( !x.isNull() ){
return true;
}
}
-bool nodeContainsVar( Node n, Node v ){
- if( n==v) {
- return true;
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++) {
- if( nodeContainsVar(n[i], v) ){
- return true;
- }
- }
- return false;
- }
-}
-
Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
+ if( n.getKind()==NOT ){
+ pol = !pol;
+ n = n[0];
+ }
if( options::relationalTriggers() ){
if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
Node rtr;
+ bool do_negate = hasPol && pol;
for( unsigned i=0; i<2; i++) {
- unsigned j = (i==0) ? 1 : 0;
- if( n[j].getKind()==INST_CONSTANT && isUsableTrigger(n[i], f) && !nodeContainsVar( n[i], n[j] ) ) {
- rtr = n;
- break;
+ if( n[1-i].getKind()==INST_CONSTANT ){
+ if( isUsableTrigger(n[i], f) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) ){
+ rtr = n;
+ break;
+ }
+ if( n[i].getKind()==INST_CONSTANT && ( !hasPol || pol ) ){
+ do_negate = true;
+ rtr = n;
+ break;
+ }
}
}
if( n[0].getType().isInteger() ){
//try to rearrange?
std::map< Node, Node > m;
- if (QuantArith::getMonomialSumLit(n, m) ){
+ if( QuantArith::getMonomialSumLit(n, m) ){
for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){
Node veq;
if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){
int vti = veq[0]==it->first ? 1 : 0;
- if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){
+ if( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ){
rtr = veq;
}
}
if( hasPol ){
Trace("relational-trigger") << " polarity : " << pol << std::endl;
}
- Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr;
+ Node rtr2 = do_negate ? rtr.negate() : rtr;
+ Trace("relational-trigger") << " return : " << rtr2 << std::endl;
return rtr2;
}
}
}
}
-bool Trigger::isUsableTrigger( Node n, Node f ){
- Node nu = getIsUsableTrigger(n,f);
+bool Trigger::isUsableTrigger( Node n, Node q ){
+ Node nu = getIsUsableTrigger( n, q );
return !nu.isNull();
}
bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){
if( patMap.find( n )==patMap.end() ){
patMap[ n ] = false;
- bool newHasPol = n.getKind()==IFF ? false : hasPol;
- bool newPol = n.getKind()==NOT ? !pol : pol;
if( tstrt==TS_MIN_TRIGGER ){
if( n.getKind()==FORALL ){
return false;
}else{
bool retVal = false;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
- if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ bool newHasPol, newPol;
+ QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+ if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol ) ){
retVal = true;
}
}
}
}
if( n.getKind()!=FORALL ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
- if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ bool newHasPol, newPol;
+ QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+ if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol ) ){
retVal = true;
}
}
}else if( n.getKind()==MULT ){
Assert( n[i].isConst() );
if( x.getType().isInteger() ){
- Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>() );
- x = NodeManager::currentNM()->mkNode( INTS_DIVISION, x, coeff );
+ Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>().abs() );
+ if( !n[i].getConst<Rational>().abs().isOne() ){
+ x = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, x, coeff );
+ }
+ if( n[i].getConst<Rational>().sgn()<0 ){
+ x = NodeManager::currentNM()->mkNode( UMINUS, x );
+ }
}else{
Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
}
}
+ x = Rewriter::rewrite( x );
}else{
Assert( cindex==-1 );
cindex = i;
bool smartTriggers = false );
private:
/** is subterm of trigger usable */
- static bool isUsable( Node n, Node f );
+ static bool isUsable( Node n, Node q );
static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false );
/** collect all APPLY_UF pattern terms for f in n */
static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol );
static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst = false );
public:
/** is usable trigger */
- static bool isUsableTrigger( Node n, Node f );
+ static bool isUsableTrigger( Node n, Node q );
static bool isAtomicTrigger( Node n );
static bool isAtomicTriggerKind( Kind k );
static bool isCbqiKind( Kind k );
Assert( terms.size()==q[0].getNumChildren() );
Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
for( unsigned i=0; i<terms.size(); i++ ){
- Trace("inst-add-debug") << " " << q[0][i] << " -> " << terms[i];
+ Trace("inst-add-debug") << " " << q[0][i] << " -> " << terms[i] << std::endl;
//make it representative, this is helpful for recognizing duplication
if( mkRep ){
//pick the best possible representative for instantiation, based on past use and simplicity of term
//ensure the type is correct
terms[i] = quantifiers::TermDb::mkNodeType( terms[i], q[0][i].getType() );
}
- Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
+ Trace("inst-add-debug2") << " -> " << terms[i] << std::endl;
Assert( !terms[i].isNull() );
}
}
}
+Expr getSubtermWithType( Expr e, Type t, bool isTop ){
+ if( !isTop && e.getType()==t ){
+ return e;
+ }else{
+ for( unsigned i=0; i<e.getNumChildren(); i++ ){
+ Expr se = getSubtermWithType( e[i], t, false );
+ if( !se.isNull() ){
+ return se;
+ }
+ }
+ return Expr();
+ }
+}
+
Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) {
if( std::find( processing.begin(), processing.end(), d_self )==processing.end() ){
processing.push_back( d_self );
//do nullary constructors first
if( ((*i).getNumArgs()==0)==(r==0)){
Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl;
- Expr e = (*i).computeGroundTerm( t, processing );
+ Expr e = (*i).computeGroundTerm( t, processing, d_ground_term );
if( !e.isNull() ){
+ //must check subterms for the same type to avoid infinite loops in type enumeration
+ Expr se = getSubtermWithType( e, t, true );
+ if( !se.isNull() ){
+ Debug("datatypes") << "Take subterm " << se << std::endl;
+ e = se;
+ }
processing.pop_back();
return e;
}else{
return true;
}
-Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) {
+Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException) {
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_constructor);
}
Expr arg;
if( selType.isDatatype() ){
- const Datatype & dt = DatatypeType(selType).getDatatype();
- arg = dt.computeGroundTerm( selType, processing );
+ std::map< Type, Expr >::iterator itgt = gt.find( selType );
+ if( itgt != gt.end() ){
+ arg = itgt->second;
+ }else{
+ const Datatype & dt = DatatypeType(selType).getDatatype();
+ arg = dt.computeGroundTerm( selType, processing );
+ }
}else{
arg = selType.mkGroundTerm();
}
/** compute whether this datatype is well-founded */
bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException);
/** compute ground term */
- Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException);
+ Expr computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException);
public:
/**
* Create a new Datatype constructor with the given name for the
manos-model.smt2 \
bug625.smt2 \
cdt-model-cade15.smt2 \
- sc-cdt1.smt2
+ sc-cdt1.smt2 \
+ conqueue-dt-enum-iloop.smt2
FAILING_TESTS = \
datatype-dump.cvc
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-fun start!13 () Bool)
+
+(assert start!13)
+
+(declare-fun b!39 () Bool)
+
+(declare-sort T!14 0)
+
+(declare-datatypes () (
+(LazyConQ!5
+ (Lazyarg1!5 (carry!37 Conc!6) (srear!9 LazyConQ!5))
+ (Lazyarg2!5 (t!270 ConQ!6))
+ (Lazyarg3!5 (carry!38 Conc!6) (t!271 ConQ!6))
+ (Lazyarg4!5 (tree!19 Conc!6) (carry!39 Conc!6))
+ (Lazyarg5!5 (tree!20 Conc!6) (carry!40 Conc!6))
+ (PushLeft!5 (ys!22 Conc!6) (xs!60 LazyConQ!5))
+ (PushLeftLazy!5 (ys!23 Conc!6) (xs!61 LazyConQ!5)))
+(Conc!6
+ (CC!5 (left!9 Conc!6) (right!9 Conc!6))
+ (Empty!5)
+ (Single!5 (x!106 T!14)))
+(ConQ!6
+ (Spine!5 (head!10 Conc!6) (rear!5 LazyConQ!5))
+ (Tip!5 (t!272 Conc!6)))
+))
+
+(declare-fun e!41 () LazyConQ!5)
+
+(declare-fun l!2 () LazyConQ!5)
+
+(declare-fun st!3 () (Set LazyConQ!5))
+
+(declare-fun firstUnevaluated!3 (LazyConQ!5 (Set LazyConQ!5)) LazyConQ!5)
+
+(declare-fun evalLazyConQ2!7 (LazyConQ!5) ConQ!6)
+
+(assert (=> b!39 (= e!41 (firstUnevaluated!3 (rear!5 (evalLazyConQ2!7 l!2)) st!3))))
+
+(declare-fun b!40 () Bool)
+
+(declare-fun e!42 () LazyConQ!5)
+
+(assert (=> b!40 (= e!42 e!41)))
+
+(assert (=> b!40 (= b!39 (is-Spine!5 (evalLazyConQ2!7 l!2)))))
+
+(declare-fun b!41 () Bool)
+
+(assert (=> b!40 (or (not b!39) (not b!41))))
+
+(assert (=> b!40 (or b!39 b!41)))
+
+(assert (=> b!41 (= e!41 l!2)))
+
+(declare-fun b!42 () Bool)
+
+(assert (=> b!42 (= e!42 l!2)))
+
+(declare-fun lt!14 () LazyConQ!5)
+
+(declare-fun isTip!5 (ConQ!6) Bool)
+
+(assert (=> start!13 (and (not (isTip!5 (evalLazyConQ2!7 lt!14))) (member lt!14 st!3))))
+
+(assert (=> start!13 (= lt!14 e!42)))
+
+(assert (=> start!13 (= b!40 (member l!2 st!3))))
+
+(assert (=> start!13 (or (not b!40) (not b!42))))
+
+(assert (=> start!13 (or b!40 b!42)))
+
+(check-sat)
mix-simp.smt2 \
mix-coeff.smt2 \
mix-match.smt2 \
- ari056.smt2
+ ari056.smt2 \
+ ext-ex-deq-trigger.smt2 \
+ matching-lia-1arg.smt2
# regression can be solved with --finite-model-find --fmf-inst-engine
--- /dev/null
+; COMMAND-LINE: --relational-triggers
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-const k U)
+(declare-const ff U)
+(declare-const ffk U)
+(declare-fun fun1 (Int) Int)
+(declare-fun fun2 (Int) Int)
+(declare-fun c (U U) U)
+(declare-fun app (U Int) Int)
+
+(assert (forall ((f U) (g U)) (=> (forall ((x Int)) (= (app f x) (app g x))) (= f g)) ))
+
+(assert (forall ((x Int)) (= (app ff x) (+ (fun1 x) (fun2 x)))))
+(assert (forall ((x Int)) (= (app ffk x) (+ (fun1 (app k x)) (fun2 (app k x))))))
+
+(assert (forall ((f U) (g U) (x Int)) (= (app (c f g) x) (app f (app g x)))))
+
+(assert (not (= (c ff k) ffk)))
+
+(check-sat)
+
--- /dev/null
+; COMMAND-LINE: --purify-triggers
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(declare-fun P (Int) Bool)
+(assert (forall ((x Int)) (P (* 2 x))))
+(assert (not (P 38)))
+(check-sat)
+
sygus-dt.sy \
dt-no-syntax.sy \
list-head-x.sy \
- clock-inc-tuple.sy
+ clock-inc-tuple.sy \
+ dt-test-ns.sy
# sygus tests currently taking too long for make regress
EXTRA_DIST = $(TESTS) \
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si --no-dump-synth
+(set-logic LIA)
+
+(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
+
+(synth-fun f ((x Int)) List)
+
+(declare-var x Int)
+
+(constraint (is-cons (f x)))
+(constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x)))))))
+(check-synth)
+
projects / cvc5.git / commitdiff