#include "scccode.h"
-Expr* e_pos;
-Expr* e_neg;
-Expr* e_tt;
-Expr* e_ff;
-Expr* e_cln;
-Expr* e_clc;
-Expr* e_concat;
-Expr* e_clr;
-Expr* e_litvar;
-Expr* e_litpol;
-Expr* e_notb;
-Expr* e_iffb;
-Expr* e_clear_mark;
-Expr* e_append;
-Expr* e_simplify_clause_h;
-Expr* e_simplify_clause;
-
void init_compiled_scc(){
- e_pos = symbols->get("pos").first;
- e_neg = symbols->get("neg").first;
- e_tt = symbols->get("tt").first;
- e_ff = symbols->get("ff").first;
- e_cln = symbols->get("cln").first;
- e_clc = symbols->get("clc").first;
- e_concat = symbols->get("concat").first;
- e_clr = symbols->get("clr").first;
- e_litvar = progs["litvar"];
- e_litpol = progs["litpol"];
- e_notb = progs["notb"];
- e_iffb = progs["iffb"];
- e_clear_mark = progs["clear_mark"];
- e_append = progs["append"];
- e_simplify_clause_h = progs["simplify_clause_h"];
- e_simplify_clause = progs["simplify_clause"];
-}
-
-Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){
- if( p==e_litvar ){
- return f_litvar( args[0] );
- }else if( p==e_litpol ){
- return f_litpol( args[0] );
- }else if( p==e_notb ){
- return f_notb( args[0] );
- }else if( p==e_iffb ){
- return f_iffb( args[0], args[1] );
- }else if( p==e_clear_mark ){
- return f_clear_mark( args[0] );
- }else if( p==e_append ){
- return f_append( args[0], args[1] );
- }else if( p==e_simplify_clause_h ){
- return f_simplify_clause_h( args[0], args[1] );
- }else if( p==e_simplify_clause ){
- return f_simplify_clause( args[0] );
- }else{
- return NULL;
- }
-}
-
-Expr* f_litvar( Expr* l ){
- Expr* e0;
- l->inc();
- Expr* e1 = l->followDefs()->get_head();
- Expr* e2;
- e2 = e_pos;
- e2->inc();
- Expr* e3;
- e3 = e_neg;
- e3->inc();
- if( e1==e2 ){
- Expr* x = ((CExpr*)l->followDefs())->kids[1];
- e0 = x;
- e0->inc();
- }else if( e1==e3 ){
- Expr* x = ((CExpr*)l->followDefs())->kids[1];
- e0 = x;
- e0->inc();
- }else{
- std::cout << "Could not find match for expression in function f_litvar ";
- e1->print( std::cout );
- std::cout << std::endl;
- exit( 1 );
- }
- l->dec();
- e2->dec();
- e3->dec();
- return e0;
-}
-
-Expr* f_litpol( Expr* l ){
- Expr* e0;
- l->inc();
- Expr* e1 = l->followDefs()->get_head();
- Expr* e2;
- e2 = e_pos;
- e2->inc();
- Expr* e3;
- e3 = e_neg;
- e3->inc();
- if( e1==e2 ){
- // Expr* x = ((CExpr*)l->followDefs())->kids[1];
- e0 = e_tt;
- e0->inc();
- }else if( e1==e3 ){
- // Expr* x = ((CExpr*)l->followDefs())->kids[1];
- e0 = e_ff;
- e0->inc();
- }else{
- std::cout << "Could not find match for expression in function f_litpol ";
- e1->print( std::cout );
- std::cout << std::endl;
- exit( 1 );
- }
- l->dec();
- e2->dec();
- e3->dec();
- return e0;
-}
-Expr* f_notb( Expr* b ){
- Expr* e0;
- b->inc();
- Expr* e1 = b->followDefs()->get_head();
- Expr* e2;
- e2 = e_ff;
- e2->inc();
- Expr* e3;
- e3 = e_tt;
- e3->inc();
- if( e1==e2 ){
- e0 = e_tt;
- e0->inc();
- }else if( e1==e3 ){
- e0 = e_ff;
- e0->inc();
- }else{
- std::cout << "Could not find match for expression in function f_notb ";
- e1->print( std::cout );
- std::cout << std::endl;
- exit( 1 );
- }
- b->dec();
- e2->dec();
- e3->dec();
- return e0;
}
-Expr* f_iffb( Expr* b1, Expr* b2 ){
- Expr* e0;
- b1->inc();
- Expr* e1 = b1->followDefs()->get_head();
- Expr* e2;
- e2 = e_tt;
- e2->inc();
- Expr* e3;
- e3 = e_ff;
- e3->inc();
- if( e1==e2 ){
- e0 = b2;
- e0->inc();
- }else if( e1==e3 ){
- b2->inc();
- e0 = f_notb( b2 );
- b2->dec();
- }else{
- std::cout << "Could not find match for expression in function f_iffb ";
- e1->print( std::cout );
- std::cout << std::endl;
- exit( 1 );
- }
- b1->dec();
- e2->dec();
- e3->dec();
- return e0;
-}
-
-Expr* f_clear_mark( Expr* v ){
- Expr* e0;
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(0)){
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(0))
- ((SymExpr*)v->followDefs())->clearmark(0);
- else
- ((SymExpr*)v->followDefs())->setmark(0);
- e0 = v;
- e0->inc();
- v->dec();
- }else{
- e0 = v;
- e0->inc();
- }
- v->dec();
- return e0;
-}
-
-Expr* f_append( Expr* c1, Expr* c2 ){
- Expr* e0;
- c1->inc();
- Expr* e1 = c1->followDefs()->get_head();
- Expr* e2;
- e2 = e_cln;
- e2->inc();
- Expr* e3;
- e3 = e_clc;
- e3->inc();
- if( e1==e2 ){
- e0 = c2;
- e0->inc();
- }else if( e1==e3 ){
- Expr* l = ((CExpr*)c1->followDefs())->kids[1];
- Expr* c1h = ((CExpr*)c1->followDefs())->kids[2];
- l->inc();
- Expr* e4;
- c1h->inc();
- c2->inc();
- e4 = f_append( c1h, c2 );
- c1h->dec();
- c2->dec();
- static Expr* e5;
- e5 = e_clc;
- e5->inc();
- e0 = new CExpr( APP, e5, l, e4 );
- }else{
- std::cout << "Could not find match for expression in function f_append ";
- e1->print( std::cout );
- std::cout << std::endl;
- exit( 1 );
- }
- c1->dec();
- e2->dec();
- e3->dec();
- return e0;
-}
-
-Expr* f_simplify_clause_h( Expr* pol, Expr* c ){
- Expr* e0;
- c->inc();
- Expr* e1 = c->followDefs()->get_head();
- Expr* e2;
- e2 = e_cln;
- e2->inc();
- Expr* e3;
- e3 = e_clc;
- e3->inc();
- Expr* e4;
- e4 = e_concat;
- e4->inc();
- Expr* e5;
- e5 = e_clr;
- e5->inc();
- if( e1==e2 ){
- e0 = e_cln;
- e0->inc();
- }else if( e1==e3 ){
- Expr* l = ((CExpr*)c->followDefs())->kids[1];
- Expr* c1 = ((CExpr*)c->followDefs())->kids[2];
- Expr* v;
- l->inc();
- v = f_litvar( l );
- l->dec();
- Expr* e6;
- Expr* e7;
- l->inc();
- e7 = f_litpol( l );
- l->dec();
- pol->inc();
- e6 = f_iffb( e7, pol );
- e7->dec();
- pol->dec();
- Expr* e8 = e6->followDefs()->get_head();
- Expr* e9;
- e9 = e_tt;
- e9->inc();
- Expr* e10;
- e10 = e_ff;
- e10->inc();
- if( e8==e9 ){
- Expr* m;
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(0)){
- m = e_tt;
- m->inc();
- }else{
- Expr* e11;
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(0))
- ((SymExpr*)v->followDefs())->clearmark(0);
- else
- ((SymExpr*)v->followDefs())->setmark(0);
- e11 = v;
- e11->inc();
- v->dec();
- e11->dec();
- m = e_ff;
- m->inc();
- }
- v->dec();
- Expr* ch;
- pol->inc();
- c1->inc();
- ch = f_simplify_clause_h( pol, c1 );
- pol->dec();
- c1->dec();
- m->inc();
- Expr* e12 = m->followDefs()->get_head();
- Expr* e13;
- e13 = e_tt;
- e13->inc();
- Expr* e14;
- e14 = e_ff;
- e14->inc();
- if( e12==e13 ){
- Expr* e15;
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(1)){
- e15 = v;
- e15->inc();
- }else{
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(1))
- ((SymExpr*)v->followDefs())->clearmark(1);
- else
- ((SymExpr*)v->followDefs())->setmark(1);
- e15 = v;
- e15->inc();
- v->dec();
- }
- v->dec();
- e15->dec();
- e0 = ch;
- e0->inc();
- }else if( e12==e14 ){
- Expr* e16;
- Expr* e17;
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(1)){
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(1))
- ((SymExpr*)v->followDefs())->clearmark(1);
- else
- ((SymExpr*)v->followDefs())->setmark(1);
- e17 = v;
- e17->inc();
- v->dec();
- }else{
- e17 = v;
- e17->inc();
- }
- v->dec();
- e17->dec();
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(0))
- ((SymExpr*)v->followDefs())->clearmark(0);
- else
- ((SymExpr*)v->followDefs())->setmark(0);
- e16 = v;
- e16->inc();
- v->dec();
- e16->dec();
- l->inc();
- ch->inc();
- static Expr* e18;
- e18 = e_clc;
- e18->inc();
- e0 = new CExpr( APP, e18, l, ch );
- }else{
- std::cout << "Could not find match for expression in function f_simplify_clause_h ";
- e12->print( std::cout );
- std::cout << std::endl;
- exit( 1 );
- }
- m->dec();
- e13->dec();
- e14->dec();
- ch->dec();
- m->dec();
- }else if( e8==e10 ){
- l->inc();
- Expr* e19;
- pol->inc();
- c1->inc();
- e19 = f_simplify_clause_h( pol, c1 );
- pol->dec();
- c1->dec();
- static Expr* e20;
- e20 = e_clc;
- e20->inc();
- e0 = new CExpr( APP, e20, l, e19 );
- }else{
- std::cout << "Could not find match for expression in function f_simplify_clause_h ";
- e8->print( std::cout );
- std::cout << std::endl;
- exit( 1 );
- }
- e6->dec();
- e9->dec();
- e10->dec();
- v->dec();
- }else if( e1==e4 ){
- Expr* c1 = ((CExpr*)c->followDefs())->kids[1];
- Expr* c2 = ((CExpr*)c->followDefs())->kids[2];
- pol->inc();
- Expr* e21 = pol->followDefs()->get_head();
- Expr* e22;
- e22 = e_ff;
- e22->inc();
- Expr* e23;
- e23 = e_tt;
- e23->inc();
- if( e21==e22 ){
- Expr* e24;
- pol->inc();
- c1->inc();
- e24 = f_simplify_clause_h( pol, c1 );
- pol->dec();
- c1->dec();
- Expr* e25;
- pol->inc();
- c2->inc();
- e25 = f_simplify_clause_h( pol, c2 );
- pol->dec();
- c2->dec();
- static Expr* e26;
- e26 = e_concat;
- e26->inc();
- e0 = new CExpr( APP, e26, e24, e25 );
- }else if( e21==e23 ){
- Expr* e27;
- pol->inc();
- c1->inc();
- e27 = f_simplify_clause_h( pol, c1 );
- pol->dec();
- c1->dec();
- Expr* e28;
- pol->inc();
- c2->inc();
- e28 = f_simplify_clause_h( pol, c2 );
- pol->dec();
- c2->dec();
- e0 = f_append( e27, e28 );
- e27->dec();
- e28->dec();
- }else{
- std::cout << "Could not find match for expression in function f_simplify_clause_h ";
- e21->print( std::cout );
- std::cout << std::endl;
- exit( 1 );
- }
- pol->dec();
- e22->dec();
- e23->dec();
- }else if( e1==e5 ){
- Expr* l = ((CExpr*)c->followDefs())->kids[1];
- Expr* c1 = ((CExpr*)c->followDefs())->kids[2];
- Expr* e29;
- Expr* e30;
- l->inc();
- e30 = f_litpol( l );
- l->dec();
- pol->inc();
- e29 = f_iffb( e30, pol );
- e30->dec();
- pol->dec();
- Expr* e31 = e29->followDefs()->get_head();
- Expr* e32;
- e32 = e_ff;
- e32->inc();
- Expr* e33;
- e33 = e_tt;
- e33->inc();
- if( e31==e32 ){
- l->inc();
- Expr* e34;
- pol->inc();
- c1->inc();
- e34 = f_simplify_clause_h( pol, c1 );
- pol->dec();
- c1->dec();
- static Expr* e35;
- e35 = e_clr;
- e35->inc();
- e0 = new CExpr( APP, e35, l, e34 );
- }else if( e31==e33 ){
- Expr* v;
- l->inc();
- v = f_litvar( l );
- l->dec();
- Expr* m;
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(0)){
- m = e_tt;
- m->inc();
- }else{
- Expr* e36;
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(0))
- ((SymExpr*)v->followDefs())->clearmark(0);
- else
- ((SymExpr*)v->followDefs())->setmark(0);
- e36 = v;
- e36->inc();
- v->dec();
- e36->dec();
- m = e_ff;
- m->inc();
- }
- v->dec();
- Expr* ch;
- pol->inc();
- c1->inc();
- ch = f_simplify_clause_h( pol, c1 );
- pol->dec();
- c1->dec();
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(1)){
- m->inc();
- Expr* e37 = m->followDefs()->get_head();
- Expr* e38;
- e38 = e_tt;
- e38->inc();
- Expr* e39;
- e39 = e_ff;
- e39->inc();
- if( e37==e38 ){
- e0 = ch;
- e0->inc();
- }else if( e37==e39 ){
- Expr* e40;
- Expr* e41;
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(1))
- ((SymExpr*)v->followDefs())->clearmark(1);
- else
- ((SymExpr*)v->followDefs())->setmark(1);
- e41 = v;
- e41->inc();
- v->dec();
- e41->dec();
- v->inc();
- if ( ((SymExpr*)v->followDefs())->getmark(0))
- ((SymExpr*)v->followDefs())->clearmark(0);
- else
- ((SymExpr*)v->followDefs())->setmark(0);
- e40 = v;
- e40->inc();
- v->dec();
- e40->dec();
- e0 = ch;
- e0->inc();
- }else{
- std::cout << "Could not find match for expression in function f_simplify_clause_h ";
- e37->print( std::cout );
- std::cout << std::endl;
- exit( 1 );
- }
- m->dec();
- e38->dec();
- e39->dec();
- }else{
- e0 = NULL;
- }
- v->dec();
- ch->dec();
- m->dec();
- v->dec();
- }else{
- std::cout << "Could not find match for expression in function f_simplify_clause_h ";
- e31->print( std::cout );
- std::cout << std::endl;
- exit( 1 );
- }
- e29->dec();
- e32->dec();
- e33->dec();
- }else{
- std::cout << "Could not find match for expression in function f_simplify_clause_h ";
- e1->print( std::cout );
- std::cout << std::endl;
- exit( 1 );
- }
- c->dec();
- e2->dec();
- e3->dec();
- e4->dec();
- e5->dec();
- return e0;
+Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){
+ return NULL;
}
-Expr* f_simplify_clause( Expr* c ){
- Expr* e0;
- static Expr* e1;
- e1 = e_tt;
- e1->inc();
- Expr* e2;
- static Expr* e3;
- e3 = e_ff;
- e3->inc();
- c->inc();
- e2 = f_simplify_clause_h( e3, c );
- e3->dec();
- c->dec();
- e0 = f_simplify_clause_h( e1, e2 );
- e1->dec();
- e2->dec();
- return e0;
-}
Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args );
-inline Expr* f_litvar( Expr* l );
-
-inline Expr* f_litpol( Expr* l );
-
-inline Expr* f_notb( Expr* b );
-
-inline Expr* f_iffb( Expr* b1, Expr* b2 );
-
-inline Expr* f_clear_mark( Expr* v );
-
-inline Expr* f_append( Expr* c1, Expr* c2 );
-
-inline Expr* f_simplify_clause_h( Expr* pol, Expr* c );
-
-inline Expr* f_simplify_clause( Expr* c );
-
#endif
{
indent( os, ind );
os << retModString.c_str();
- os << "new IntExpr( " << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl;
+ os << "new IntExpr( (signed long int)" << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl;
indent( os, ind );
os << incString.c_str() << std::endl;
}
indent( os, ind );
os << "Expr* ";
write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, os );
- os << ";" << std::endl;
+ os << " = NULL;" << std::endl;
std::ostringstream ss;
write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, ss );
write_code( ((CExpr*)code)->kids[1], os, ind, ss.str().c_str() );
{
os << "static ";
}
- os << "Expr* " << ss.str().c_str() << ";" << std::endl;
+ os << "Expr* " << ss.str().c_str() << " = NULL;" << std::endl;
//write the expression
std::ostringstream ss2;
ss2 << ss.str().c_str();
(match ti
((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
(default ff)))
- (default
- (match ti
- ((apply si1 si2 ti1 ti2) ff)
- (default (eqterm ti (ifmarked t k t)))))))
+ (default (eqterm ti (ifmarked t k t)))))
(program is_inst_f ((fi formula) (f formula) (k term)) bool
(match f
Trace("ambqi-model-debug") << "Initial terms: " << std::endl;
for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
Node n = fm->d_uf_terms[f][i];
- if( !n.getAttribute(NoMatchAttribute()) ){
+ if( d_qe->getTermDatabase()->isTermActive( n ) ){
Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;
fapps.push_back( n );
}
using namespace CVC4::theory::inst;
bool CandidateGenerator::isLegalCandidate( Node n ){
- return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) ) );
+ return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) );
}
void CandidateGeneratorQueue::addCandidate( Node n ) {
}
CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) :
- d_qe( qe ), d_term_iter( -1 ){
+CandidateGenerator( qe ), d_term_iter( -1 ){
d_op = qe->getTermDatabase()->getMatchOperator( pat );
Assert( !d_op.isNull() );
d_op_arity = pat.getNumChildren();
}
CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
- d_match_pattern( mpat ), d_qe( qe ){
+ CandidateGenerator( qe ), d_match_pattern( mpat ){
Assert( mpat.getKind()==EQUAL );
for( unsigned i=0; i<2; i++ ){
if( !quantifiers::TermDb::hasInstConstAttr(mpat[i]) ){
CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
- d_match_pattern( mpat ), d_qe( qe ){
+CandidateGenerator( qe ), d_match_pattern( mpat ){
Assert( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF );
d_match_pattern_type = d_match_pattern[0].getType();
CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) :
- d_match_pattern( mpat ), d_qe( qe ){
+ CandidateGenerator( qe ), d_match_pattern( mpat ){
d_match_pattern_type = mpat.getType();
Assert( mpat.getKind()==INST_CONSTANT );
d_f = quantifiers::TermDb::getInstConstAttr( mpat );
/** base class for generating candidates for matching */
class CandidateGenerator {
+protected:
+ QuantifiersEngine* d_qe;
public:
- CandidateGenerator(){}
+ CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){}
virtual ~CandidateGenerator(){}
/** Get candidates functions. These set up a context to get all match candidates.
virtual void resetInstantiationRound() = 0;
public:
/** legal candidate */
- static bool isLegalCandidate( Node n );
+ bool isLegalCandidate( Node n );
};/* class CandidateGenerator */
/** candidate generator queue (for manual candidate generation) */
std::vector< Node > d_candidates;
int d_candidate_index;
public:
- CandidateGeneratorQueue() : d_candidate_index( 0 ){}
+ CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){}
~CandidateGeneratorQueue() throw() {}
void addCandidate( Node n );
private:
//operator you are looking for
Node d_op;
- //instantiator pointer
- QuantifiersEngine* d_qe;
//the equality class iterator
unsigned d_op_arity;
std::vector< quantifiers::TermArgTrie* > d_tindex;
Node d_match_pattern;
Node d_match_gterm;
bool d_do_mgt;
- //einstantiator pointer
- QuantifiersEngine* d_qe;
public:
CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
~CandidateGeneratorQELitEq() throw() {}
Node d_match_pattern;
//type of disequality
TypeNode d_match_pattern_type;
- //einstantiator pointer
- QuantifiersEngine* d_qe;
public:
CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
~CandidateGeneratorQELitDeq() throw() {}
//equality you are trying to match equalities for
Node d_match_pattern;
TypeNode d_match_pattern_type;
- //einstantiator pointer
- QuantifiersEngine* d_qe;
// quantifier/index for the variable we are matching
Node d_f;
unsigned d_index;
}
bool ConjectureGenerator::isHandledTerm( TNode n ){
- return !n.getAttribute(NoMatchAttribute()) && inst::Trigger::isAtomicTrigger( n ) && ( n.getKind()!=APPLY_UF || n.getOperator().getKind()!=SKOLEM );
+ return d_quantEngine->getTermDatabase()->isTermActive( n ) && inst::Trigger::isAtomicTrigger( n ) && ( n.getKind()!=APPLY_UF || n.getOperator().getKind()!=SKOLEM );
}
Node ConjectureGenerator::getGroundEqc( TNode r ) {
eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
while( !eqc_i.isFinished() ){
TNode n = (*eqc_i);
- if( getTermDatabase()->hasTermCurrent( n ) && !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){
+ if( getTermDatabase()->hasTermCurrent( n ) && getTermDatabase()->isTermActive( n ) && ( n.getKind()!=EQUAL || isFalse ) ){
if( firstTime ){
Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl;
firstTime = false;
bool needsDefault = true;
for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
Node n = fm->d_uf_terms[op][i];
- if( !n.getAttribute(NoMatchAttribute()) ){
+ if( d_qe->getTermDatabase()->isTermActive( n ) ){
add_conds.push_back( n );
add_values.push_back( n );
Node r = fm->getUsedRepresentative(n);
d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
}
}else{
- d_cg = new CandidateGeneratorQueue;
+ d_cg = new CandidateGeneratorQueue( qe );
Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
}
return addedLemmas;
}
-InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q ), d_match_pattern( pat ) {
+InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe ) : d_f( q ), d_match_pattern( pat ) {
if( d_match_pattern.getKind()==NOT ){
d_match_pattern = d_match_pattern[0];
d_pol = false;
}
d_match_pattern_arg_types.push_back( d_match_pattern[i].getType() );
}
+ d_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
}
void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) {
- d_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
+
}
int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
tat = NULL;
}
}
+ Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl;
if( tat ){
InstMatch m( q );
m.add( baseMatch );
void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
public:
/** constructors */
- InstMatchGeneratorSimple( Node q, Node pat );
+ InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe );
/** destructor */
~InstMatchGeneratorSimple() throw() {}
/** reset instantiation round (call this whenever equivalence classes have changed) */
Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl;
if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
- int matchOption = 0;
for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){
- Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], matchOption, true, Trigger::TR_RETURN_NULL );
+ Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], true, Trigger::TR_RETURN_NULL );
if( t ){
d_user_gen[f].push_back( t );
}
if( usable ){
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[q].push_back( nodes );
}else{
- Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW );
+ Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW );
if( t ){
d_user_gen[q].push_back( t );
}else{
last_weight = curr_w;
}
}
+ d_num_trigger_vars[f] = vcMap.size();
+ if( d_num_trigger_vars[f]>0 && d_num_trigger_vars[f]<f[0].getNumChildren() ){
+ Trace("auto-gen-trigger-partial") << "Quantified formula : " << f << std::endl;
+ Trace("auto-gen-trigger-partial") << "...does not contain all variables in triggers!!!" << std::endl;
+ if( options::partialTriggers() ){
+ std::vector< Node > vcs[2];
+ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+ vcs[ vcMap.find( ic )==vcMap.end() ? 0 : 1 ].push_back( f[0][i] );
+ }
+ for( unsigned i=0; i<2; i++ ){
+ d_vc_partition[i][f] = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, vcs[i] );
+ }
+ }else{
+ return;
+ }
+ }
for( unsigned i=0; i<patTermsF.size(); i++ ){
Node pat = patTermsF[i];
if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){
}
}
//now, generate the trigger...
- int matchOption = 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 );
+ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] );
d_single_trigger_gen[ patTerms[0] ] = true;
}else{
//only generate multi trigger if option set, or if no single triggers exist
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 );
+ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, false, Trigger::TR_GET_OLD, d_num_trigger_vars[f] );
}
if( tr ){
- unsigned tindex;
- if( tr->isMultiTrigger() ){
- //disable all other multi triggers
- for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[1][f].begin(); it != d_auto_gen_trigger[1][f].end(); ++it ){
- d_auto_gen_trigger[1][f][ it->first ] = false;
- }
- tindex = 1;
- }else{
- tindex = 0;
- }
- //making it during an instantiation round, so must reset
- if( d_auto_gen_trigger[tindex][f].find( tr )==d_auto_gen_trigger[tindex][f].end() ){
- tr->resetInstantiationRound();
- tr->reset( Node::null() );
- }
- d_auto_gen_trigger[tindex][f][tr] = true;
+ addTrigger( tr, f );
//if we are generating additional triggers...
- if( tindex==0 ){
- int index = 0;
- if( index<(int)patTerms.size() ){
+ if( !tr->isMultiTrigger() ){
+ unsigned index = 0;
+ if( index<patTerms.size() ){
//Notice() << "check add additional" << std::endl;
//check if similar patterns exist, and if so, add them additionally
int nqfs_curr = 0;
}
index++;
bool success = true;
- while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
+ while( success && index<patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
success = false;
if( !options::relevantTriggers() ||
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 );
- if( tr2 ){
- //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
- tr2->resetInstantiationRound();
- tr2->reset( Node::null() );
- d_auto_gen_trigger[0][f][tr2] = true;
- }
+ Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] );
+ addTrigger( tr2, f );
success = true;
}
index++;
}
void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv ) {
- if( num_fv==q[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
+ unsigned num_vars = options::partialTriggers() ? d_num_trigger_vars[q] : q[0].getNumChildren();
+ if( num_fv==num_vars && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
d_patTerms[0][q].push_back( pat );
d_is_single_trigger[ pat ] = true;
}else{
}
}
+
+void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) {
+ if( tr ){
+ if( d_num_trigger_vars[q]<q[0].getNumChildren() ){
+ //partial trigger : generate implication to mark user pattern
+ Node ipl = NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, d_quantEngine->getTermDatabase()->getVariableNode( tr->getInstPattern(), q ) );
+ Node qq = NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[1][q], NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[0][q], q[1] ), ipl );
+ Trace("auto-gen-trigger-partial") << "Make partially specified user pattern: " << std::endl;
+ Trace("auto-gen-trigger-partial") << " " << qq << std::endl;
+ Node lem = NodeManager::currentNM()->mkNode( OR, q.negate(), qq );
+ d_quantEngine->addLemma( lem );
+ }else{
+ unsigned tindex;
+ if( tr->isMultiTrigger() ){
+ //disable all other multi triggers
+ for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[1][q].begin(); it != d_auto_gen_trigger[1][q].end(); ++it ){
+ d_auto_gen_trigger[1][q][ it->first ] = false;
+ }
+ tindex = 1;
+ }else{
+ tindex = 0;
+ }
+ //making it during an instantiation round, so must reset
+ if( d_auto_gen_trigger[tindex][q].find( tr )==d_auto_gen_trigger[tindex][q].end() ){
+ tr->resetInstantiationRound();
+ tr->reset( Node::null() );
+ }
+ d_auto_gen_trigger[tindex][q][tr] = true;
+ }
+ }
+}
+
bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
if( q.getNumChildren()==3 ){
std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q );
Trace("local-t-ext") << " " << patTerms[i] << std::endl;
}
Trace("local-t-ext") << std::endl;
- int matchOption = 0;
- Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD );
+ Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, true, Trigger::TR_GET_OLD );
d_lte_trigger[f] = tr;
}else{
Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl;
std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger;
//instantiation no patterns
std::map< Node, std::vector< Node > > d_user_no_gen;
+ // number of trigger variables per quantifier
+ std::map< Node, unsigned > d_num_trigger_vars;
+ std::map< Node, Node > d_vc_partition[2];
private:
/** process functions */
void processResetInstantiationRound( Theory::Effort effort );
/** generate triggers */
void generateTriggers( Node q );
void addPatternToPool( Node q, Node pat, unsigned num_fv );
- //bool addTrigger( inst::Trigger * tr, Node f, unsigned r );
+ void addTrigger( inst::Trigger * tr, Node f );
/** has user patterns */
bool hasUserPatterns( Node q );
/** has user patterns */
QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) :
-QModelBuilder( c, qe ) {
+QModelBuilder( c, qe ), d_basisNoMatch( c ) {
}
for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
Node n = fmig->d_uf_terms[op][i];
//for calculating if op is constant
- if( !n.getAttribute(NoMatchAttribute()) ){
+ if( d_qe->getTermDatabase()->isTermActive( n ) ){
Node v = fmig->getRepresentative( n );
if( i==0 ){
d_uf_prefs[op].d_const_val = v;
}
}
//for calculating terms that we don't need to consider
- if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
- if( !n.getAttribute(BasisNoMatchAttribute()) ){
+ if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
+ if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){
//need to consider if it is not congruent modulo model basis
if( !tabt.addTerm( fmig, n ) ){
- BasisNoMatchAttribute bnma;
- n.setAttribute(bnma,true);
+ d_basisNoMatch[n] = true;
}
}
}
}
bool QModelBuilderIG::isTermActive( Node n ){
- return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term
- ( n.getAttribute(ModelBasisArgAttribute())!=0 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments
+ return d_qe->getTermDatabase()->isTermActive( n ) || //it is not congruent to another active term
+ ( n.getAttribute(ModelBasisArgAttribute())!=0 && d_basisNoMatch.find( n )==d_basisNoMatch.end() ); //or it has model basis arguments
//and is not congruent modulo model basis
//to another active term
}
//if applicable, try to add exceptions here
if( !tr_terms.empty() ){
//make a trigger for these terms, add instantiations
- inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, 0, true, inst::Trigger::TR_MAKE_NEW );
+ inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, true, inst::Trigger::TR_MAKE_NEW );
//Notice() << "Trigger = " << (*tr) << std::endl;
tr->resetInstantiationRound();
tr->reset( Node::null() );
-/** Attribute true for nodes that should not be used when considered for inst-gen basis */
-struct BasisNoMatchAttributeId {};
-/** use the special for boolean flag */
-typedef expr::Attribute< BasisNoMatchAttributeId,
- bool,
- expr::attr::NullCleanupStrategy,
- true // context dependent
- > BasisNoMatchAttribute;
-
class TermArgBasisTrie {
private:
bool addTerm2( FirstOrderModel* fm, Node n, int argIndex );
*/
class QModelBuilderIG : public QModelBuilder
{
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
protected:
+ BoolMap d_basisNoMatch;
//map from operators to model preference data
std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
//built model uf
if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << std::endl;
std::vector< Node > args;
- for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
- args.push_back( in[0][i] );
- }
- Node body = in[1];
+ Node body = in;
bool doRewrite = false;
- std::vector< Node > ipl;
- while( body.getNumChildren()>=2 && body.getKind()==in.getKind() ){
- if( body.getNumChildren()==3 ){
- for( unsigned i=0; i<body[2].getNumChildren(); i++ ){
- ipl.push_back( body[2][i] );
- }
- }
- for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+ bool firstTime = true;
+ while( body.getNumChildren()==2 && body.getKind()==body[1].getKind() ){
+ for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
args.push_back( body[0][i] );
}
body = body[1];
std::vector< Node > children;
children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) );
children.push_back( body );
- if( in.getNumChildren()==3 ){
- for( unsigned i=0; i<in[2].getNumChildren(); i++ ){
- ipl.push_back( in[2][i] );
- }
- }
- if( !ipl.empty() ){
- children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, ipl ) );
- }
Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
if( in!=n ){
Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
for( unsigned i=0; i<sz; i++ ){
Node n = it->second[i];
//if it is a non-redundant term
- if( !n.getAttribute(NoMatchAttribute()) ){
+ if( db->isTermActive( n ) ){
for( unsigned j=0; j<n.getNumChildren(); j++ ){
RDomain * rf = getRDomain( op, j );
rf->addTerm( n[j] );
for( unsigned j=0; j<to_remove.size(); j++ ){
Node ns = d_quantEngine->getSubstitute( to_remove[j], inst );
Trace("rewrite-engine-inst-debug") << "Will remove : " << ns << std::endl;
- ns.setAttribute(NoMatchAttribute(),true);
+ d_quantEngine->getTermDatabase()->setTermInactive( ns );
}
*/
}else{
}
}
-TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_id_count( 0 ), d_typ_id_count( 0 ) {
+TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_inactive_map( c ), d_op_id_count( 0 ), d_typ_id_count( 0 ) {
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
}
}
}
+ }else{
+ setTermInactive( n );
}
rec = true;
}
for( unsigned i=0; i<d_op_map[f].size(); i++ ){
TNode n = d_op_map[f][i];
if( hasTermCurrent( n ) ){
- if( !n.getAttribute(NoMatchAttribute()) ){
+ if( isTermActive( n ) ){
computeArgReps( n );
TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n;
d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] );
return isEntailed2( n, subs, subsRep, true, pol, qy );
}
+bool TermDb::isTermActive( Node n ) {
+ return d_inactive_map.find( n )==d_inactive_map.end();
+ //return !n.getAttribute(NoMatchAttribute());
+}
+
+void TermDb::setTermInactive( Node n ) {
+ d_inactive_map[n] = true;
+ //Trace("term-db-debug2") << "set no match attribute" << std::endl;
+ //NoMatchAttribute nma;
+ //n.setAttribute(nma,true);
+}
+
bool TermDb::hasTermCurrent( Node n, bool useMode ) {
if( !useMode ){
return d_has_map.find( n )!=d_has_map.end();
Node n = it->second[i];
//to be added to term index, term must be relevant, and exist in EE
if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
- if( !n.getAttribute(NoMatchAttribute()) ){
+ if( isTermActive( n ) ){
if( options::finiteModelFind() ){
computeModelBasisArgAttribute( n );
}
}
}
Trace("term-db-debug") << std::endl;
- if( ee->hasTerm( n ) ){
- Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl;
- }
+ Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl;
Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] );
+ Trace("term-db-debug2") << "...add term returned " << at << std::endl;
if( at!=n && ee->areEqual( at, n ) ){
- NoMatchAttribute nma;
- n.setAttribute(nma,true);
+ setTermInactive( n );
Trace("term-db-debug") << n << " is redundant." << std::endl;
congruentCount++;
}else{
ic.setAttribute( ivna, i );
InstConstantAttribute ica;
ic.setAttribute( ica, q );
- //also set the no-match attribute
- NoMatchAttribute nma;
- ic.setAttribute(nma,true);
+ //also set the term inactive
+ setTermInactive( ic );
}
}
}
}
InstConstantAttribute ica;
n.setAttribute(ica, q);
- if( !q.isNull() ){
- //also set the no-match attribute
- NoMatchAttribute nma;
- n.setAttribute(nma,true);
- }
}
return n.getAttribute(InstConstantAttribute());
}
Node TermDb::getInstConstantNode( Node n, Node q ){
makeInstantiationConstantsFor( q );
- Node n2 = n.substitute( d_vars[q].begin(), d_vars[q].end(),
- d_inst_constants[q].begin(), d_inst_constants[q].end() );
- return n2;
+ return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() );
+}
+
+Node TermDb::getVariableNode( Node n, Node q ) {
+ makeInstantiationConstantsFor( q );
+ return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() );
}
Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
struct SynthesisAttributeId {};
typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
-/** Attribute true for nodes that should not be used for matching */
-struct NoMatchAttributeId {};
-/** use the special for boolean flag */
-typedef expr::Attribute< NoMatchAttributeId,
- bool,
- expr::attr::NullCleanupStrategy,
- true // context dependent
- > NoMatchAttribute;
-
// attribute for "contains instantiation constants from"
struct InstConstantAttributeId {};
typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
friend class ::CVC4::theory::quantifiers::ConjectureGenerator;
friend class ::CVC4::theory::quantifiers::TermGenEnv;
typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
private:
/** reference to the quantifiers engine */
QuantifiersEngine* d_quantEngine;
std::map< Node, std::vector< Node > > d_op_map;
/** map from type nodes to terms of that type */
std::map< TypeNode, std::vector< Node > > d_type_map;
+ /** inactive map */
+ NodeBoolMap d_inactive_map;
/** count number of non-redundant ground terms per operator */
std::map< Node, int > d_op_nonred_count;
/** is entailed (incomplete check) */
bool isEntailed( TNode n, bool pol, EqualityQuery * qy = NULL );
bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL );
+ /** is active */
+ bool isTermActive( Node n );
+ void setTermInactive( Node n );
/** has term */
bool hasTermCurrent( Node n, bool useMode = true );
/** is term eligble for instantiation? */
instantiation.
*/
Node getInstConstantNode( Node n, Node q );
+ Node getVariableNode( Node n, Node q );
/** get substituted node */
Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms );
}
/** trigger class constructor */
-Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption )
- : d_quantEngine( qe ), d_f( f )
-{
+Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
+ : d_quantEngine( qe ), d_f( f ) {
d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
Trace("trigger") << "Trigger for " << f << ": " << std::endl;
for( unsigned i=0; i<d_nodes.size(); i++ ){
}
if( d_nodes.size()==1 ){
if( isSimpleTrigger( d_nodes[0] ) ){
- d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] );
+ d_mg = new InstMatchGeneratorSimple( f, d_nodes[0], qe );
}else{
d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe );
d_mg->setActiveAdd(true);
return d_mg->addTerm( d_f, t, d_quantEngine );
}
+Node Trigger::getInstPattern(){
+ return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
+}
+
int Trigger::addInstantiations( InstMatch& baseMatch ){
int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine );
if( addedLemmas>0 ){
return addedLemmas;
}
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption ){
- std::vector< Node > trNodes;
- if( !keepAll ){
- //only take nodes that contribute variables to the trigger when added
- std::vector< Node > temp;
- temp.insert( temp.begin(), nodes.begin(), nodes.end() );
- std::map< Node, bool > vars;
- std::map< Node, std::vector< Node > > patterns;
- size_t varCount = 0;
- std::map< Node, std::vector< Node > > varContains;
- quantifiers::TermDb::getVarContains( f, temp, varContains );
- for( unsigned i=0; i<temp.size(); i++ ){
- bool foundVar = false;
+bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) {
+ //only take nodes that contribute variables to the trigger when added
+ std::vector< Node > temp;
+ temp.insert( temp.begin(), nodes.begin(), nodes.end() );
+ std::map< Node, bool > vars;
+ std::map< Node, std::vector< Node > > patterns;
+ size_t varCount = 0;
+ std::map< Node, std::vector< Node > > varContains;
+ quantifiers::TermDb::getVarContains( q, temp, varContains );
+ for( unsigned i=0; i<temp.size(); i++ ){
+ bool foundVar = false;
+ for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
+ Node v = varContains[ temp[i] ][j];
+ Assert( quantifiers::TermDb::getInstConstAttr(v)==q );
+ if( vars.find( v )==vars.end() ){
+ varCount++;
+ vars[ v ] = true;
+ foundVar = true;
+ }
+ }
+ if( foundVar ){
+ trNodes.push_back( temp[i] );
for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
Node v = varContains[ temp[i] ][j];
- Assert( quantifiers::TermDb::getInstConstAttr(v)==f );
- if( vars.find( v )==vars.end() ){
- varCount++;
- vars[ v ] = true;
- foundVar = true;
- }
- }
- if( foundVar ){
- trNodes.push_back( temp[i] );
- for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
- Node v = varContains[ temp[i] ][j];
- patterns[ v ].push_back( temp[i] );
- }
- }
- if( varCount==f[0].getNumChildren() ){
- break;
+ patterns[ v ].push_back( temp[i] );
}
}
- if( varCount<f[0].getNumChildren() && !options::partialTriggers() ){
- Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl;
- for( unsigned i=0; i<nodes.size(); i++) {
- Trace("trigger-debug") << nodes[i] << " ";
- }
- Trace("trigger-debug") << std::endl;
+ if( varCount==n_vars ){
+ break;
+ }
+ }
+ if( varCount<n_vars ){
+ Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl;
+ for( unsigned i=0; i<nodes.size(); i++) {
+ Trace("trigger-debug") << nodes[i] << " ";
+ }
+ Trace("trigger-debug") << std::endl;
- //do not generate multi-trigger if it does not contain all variables
- return NULL;
- }else{
- //now, minimize the trigger
- for( unsigned i=0; i<trNodes.size(); i++ ){
- bool keepPattern = false;
- Node n = trNodes[i];
+ //do not generate multi-trigger if it does not contain all variables
+ return false;
+ }else{
+ //now, minimize the trigger
+ for( unsigned i=0; i<trNodes.size(); i++ ){
+ bool keepPattern = false;
+ Node n = trNodes[i];
+ for( unsigned j=0; j<varContains[ n ].size(); j++ ){
+ Node v = varContains[ n ][j];
+ if( patterns[v].size()==1 ){
+ keepPattern = true;
+ break;
+ }
+ }
+ if( !keepPattern ){
+ //remove from pattern vector
for( unsigned j=0; j<varContains[ n ].size(); j++ ){
Node v = varContains[ n ][j];
- if( patterns[v].size()==1 ){
- keepPattern = true;
- break;
- }
- }
- if( !keepPattern ){
- //remove from pattern vector
- for( unsigned j=0; j<varContains[ n ].size(); j++ ){
- Node v = varContains[ n ][j];
- for( unsigned k=0; k<patterns[v].size(); k++ ){
- if( patterns[v][k]==n ){
- patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
- break;
- }
+ for( unsigned k=0; k<patterns[v].size(); k++ ){
+ if( patterns[v][k]==n ){
+ patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
+ break;
}
}
- //remove from trigger nodes
- trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
- i--;
}
+ //remove from trigger nodes
+ trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
+ i--;
}
}
+ }
+ return true;
+}
+
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, bool keepAll, int trOption, unsigned use_n_vars ){
+ std::vector< Node > trNodes;
+ if( !keepAll ){
+ unsigned n_vars = use_n_vars==0 ? f[0].getNumChildren() : use_n_vars;
+ if( !mkTriggerTerms( f, nodes, n_vars, trNodes ) ){
+ return NULL;
+ }
}else{
trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
}
}
}
}
- Trigger* t = new Trigger( qe, f, trNodes, matchOption );
+ Trigger* t = new Trigger( qe, f, trNodes );
qe->getTriggerDatabase()->addTrigger( trNodes, t );
return t;
}
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption ){
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll, int trOption, unsigned use_n_vars ){
std::vector< Node > nodes;
nodes.push_back( n );
- return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption );
+ return mkTrigger( qe, f, nodes, keepAll, trOption, use_n_vars );
}
bool Trigger::isUsable( Node n, Node q ){
}
bool Trigger::isAtomicTrigger( Node n ){
- Kind k = n.getKind();
- return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) ||
- ( k!=APPLY_UF && isAtomicTriggerKind( k ) );
+ return isAtomicTriggerKind( n.getKind() );
}
bool Trigger::isAtomicTriggerKind( Kind k ) {
int addTerm( Node t );
/** return whether this is a multi-trigger */
bool isMultiTrigger() { return d_nodes.size()>1; }
+ /** get inst pattern list */
+ Node getInstPattern();
/** add all available instantiations exhaustively, in any equivalence class
if limitInst>0, limitInst is the max # of instantiations to try */
ie : quantifier engine;
f : forall something ....
nodes : (multi-)trigger
- matchOption : which policy to use for creating matches
- (one of InstMatchGenerator::MATCH_GEN_* )
keepAll: don't remove unneeded patterns;
trOption : policy for dealing with triggers that already existed
(see below)
TR_GET_OLD, //return a previous trigger if it had already been created
TR_RETURN_NULL //return null if a duplicate is found
};
- static Trigger* mkTrigger( QuantifiersEngine* qe, Node f,
- std::vector< Node >& nodes, int matchOption = 0,
- bool keepAll = true, int trOption = TR_MAKE_NEW );
- static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n,
- int matchOption = 0, bool keepAll = true,
- int trOption = TR_MAKE_NEW );
+ //nodes input, trNodes output
+ static bool mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes );
+ static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes,
+ bool keepAll = true, int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 );
+ static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll = true,
+ int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 );
static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt,
std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo,
bool filterInst = false );
}
private:
/** trigger constructor */
- Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0 );
+ Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes );
/** is subterm of trigger usable */
static bool isUsable( Node n, Node q );
florian-case-ax.smt2 \
double-pattern.smt2 \
qcf-rel-dom-opt.smt2 \
- parametric-lists.smt2
+ parametric-lists.smt2 \
+ partial-trigger.smt2
# regression can be solved with --finite-model-find --fmf-inst-engine
--- /dev/null
+; COMMAND-LINE: --partial-triggers
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun P (Int) Bool)
+(assert (forall ((x Int) (y Int)) (=> (> y 6) (or (> x y) (P x)))))
+
+(assert (not (P 5)))
+
+(check-sat)
projects / cvc5.git / commitdiff