diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-09 06:51:43 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-09 06:51:43 -0500 |
commit | cc01e2119801bbd4fd99548b79c297fa57a1977d (patch) | |
tree | cf9c64efbc286089a898d93abb3150e79138e5a7 /src/theory/quantifiers | |
parent | 88907b94e858b701e83bbee67f542ad0ee5ae626 (diff) |
Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs.
Diffstat (limited to 'src/theory/quantifiers')
-rwxr-xr-x | src/theory/quantifiers/ambqi_builder.cpp | 23 | ||||
-rwxr-xr-x | src/theory/quantifiers/ambqi_builder.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 35 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/macros.cpp | 29 | ||||
-rw-r--r-- | src/theory/quantifiers/macros.h | 2 |
6 files changed, 69 insertions, 31 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 7f119ae93..0b75c4a77 100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -164,7 +164,7 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, }
}else{
bool osuccess = true;
- TypeNode tn = q[0][depth].getType();
+ TypeNode tn = m->getVariable( q, depth ).getType();
for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
//get witness term
unsigned index = 0;
@@ -174,7 +174,8 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, index = getId( it->first, index );
if( index<32 ){
Assert( index<m->d_rep_set.d_type_reps[tn].size() );
- terms.push_back( m->d_rep_set.d_type_reps[tn][index] );
+ terms[m->d_var_order[q][depth]] = m->d_rep_set.d_type_reps[tn][index];
+ //terms[depth] = m->d_rep_set.d_type_reps[tn][index];
if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){
//if we are incomplete, and have not yet added an instantiation, keep trying
index++;
@@ -182,7 +183,6 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, }else{
success = true;
}
- terms.pop_back();
}
}while( !success && index<32 );
//mark if we are incomplete
@@ -218,7 +218,7 @@ void AbsDef::construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< Assert( defs.size()==1 );
d_value = defs[0]->d_value;
}else{
- TypeNode tn = q[0][depth].getType();
+ TypeNode tn = m->getVariable( q, depth ).getType();
unsigned def = m->d_domain[tn];
for( unsigned i=0; i<defs.size(); i++ ){
//process each simple child
@@ -270,7 +270,7 @@ void AbsDef::apply_ucompose( FirstOrderModelAbs * m, TNode q, if( Trace.isOn("ambqi-check-debug2") ){
Trace("ambqi-check-debug2") << "Add entry ( ";
for( unsigned i=0; i<entry.size(); i++ ){
- unsigned dSize = m->d_rep_set.d_type_reps[q[0][i].getType()].size();
+ unsigned dSize = m->d_rep_set.d_type_reps[m->getVariable( q, i ).getType()].size();
debugPrintUInt( "ambqi-check-debug2", dSize, entry[i] );
Trace("ambqi-check-debug2") << " ";
}
@@ -313,7 +313,7 @@ void AbsDef::construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, uns Assert( currv!=val_none );
d_value = currv;
}else{
- TypeNode tn = q[0][depth].getType();
+ TypeNode tn = m->getVariable( q, depth ).getType();
unsigned dom = m->d_domain[tn];
int vindex = depth==v1 ? 0 : ( depth==v2 ? 1 : val_none );
if( vindex==val_none ){
@@ -322,7 +322,7 @@ void AbsDef::construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, uns }else{
Assert( currv==val_none );
if( curr==val_none ){
- unsigned numReps = m->d_rep_set.d_type_reps[tn].size();
+ unsigned numReps = m->d_rep_set.getNumRepresentatives( tn );
Assert( numReps < 32 );
for( unsigned i=0; i<numReps; i++ ){
curr = 1 << i;
@@ -344,7 +344,7 @@ void AbsDef::construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int cur Assert( currv!=val_none );
d_value = currv;
}else{
- TypeNode tn = q[0][depth].getType();
+ TypeNode tn = m->getVariable( q, depth ).getType();
if( v==depth ){
unsigned numReps = m->d_rep_set.d_type_reps[tn].size();
Assert( numReps>0 && numReps < 32 );
@@ -372,7 +372,7 @@ void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef //std::cout << "Short circuit " << it->second->d_value << " " << entry.size() << "/" << q[0].getNumChildren() << std::endl;
unsigned count = q[0].getNumChildren() - entry.size();
for( unsigned i=0; i<count; i++ ){
- entry.push_back( m->d_domain[q[0][entry.size()].getType()] );
+ entry.push_back( m->d_domain[m->getVariable( q, entry.size() ).getType()] );
entry_def.push_back( true );
}
construct_entry( entry, entry_def, it->second->d_value );
@@ -454,7 +454,7 @@ void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef }
}else{
//take product of arguments
- TypeNode tn = q[0][entry.size()].getType();
+ TypeNode tn = m->getVariable( q, entry.size() ).getType();
Assert( m->isValidType( tn ) );
unsigned def = m->d_domain[tn];
if( Trace.isOn("ambqi-check-debug2") ){
@@ -877,7 +877,8 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod bchildren[i] = AbsDef::val_unk;
}else if( n[i].getKind() == BOUND_VARIABLE ){
varChCount++;
- vchildren[i] = m->getVariableId( q, n[i] );
+ vchildren[i] = m->d_var_index[q][ m->getVariableId( q, n[i] ) ];
+ //vchildren[i] = m->getVariableId( q, n[i] );
}else if( m->hasTerm( n[i] ) ){
bchildren[i] = m->getRepresentativeId( n[i] );
}else{
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index def074177..784fa5093 100755 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -62,6 +62,7 @@ public: void simplify( FirstOrderModelAbs * m, TNode q, unsigned depth = 0 );
int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){
std::vector< Node > terms;
+ terms.resize( q[0].getNumChildren() );
return addInstantiations( m, qe, q, terms, inst, 0 );
}
bool construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 0b2fae5d4..e4b588ac1 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -76,12 +76,12 @@ void FirstOrderModel::initialize( bool considerAxioms ) { //for each quantifier, collect all operators we care about for( int i=0; i<getNumAssertedQuantifiers(); i++ ){ Node f = getAssertedQuantifier( i ); - processInitializeQuantifier( f ); if( d_quant_var_id.find( f )==d_quant_var_id.end() ){ for(unsigned i=0; i<f[0].getNumChildren(); i++){ d_quant_var_id[f][f[0][i]] = i; } } + processInitializeQuantifier( f ); if( considerAxioms || !f.hasAttribute(AxiomAttribute()) ){ //initialize relevant models within bodies of all quantifiers initializeModelForTerm( f[1] ); @@ -981,3 +981,36 @@ void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) { } } } + +void FirstOrderModelAbs::collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars ) { + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( n.getKind()==EQUAL && n[i].getKind()==BOUND_VARIABLE ){ + int v = getVariableId( q, n[i] ); + Assert( v>=0 && v<q.getNumChildren() ); + eq_vars[v] = true; + } + collectEqVars( q, n[i], eq_vars ); + } +} + +void FirstOrderModelAbs::processInitializeQuantifier( Node q ) { + if( d_var_order.find( q )==d_var_order.end() ){ + std::map< int, bool > eq_vars; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + eq_vars[i] = false; + } + collectEqVars( q, q[1], eq_vars ); + for( unsigned r=0; r<2; r++ ){ + for( std::map< int, bool >::iterator it = eq_vars.begin(); it != eq_vars.end(); ++it ){ + if( it->second==(r==1) ){ + d_var_index[q][it->first] = d_var_order[q].size(); + d_var_order[q].push_back( it->first ); + } + } + } + } +} + +Node FirstOrderModelAbs::getVariable( Node q, unsigned i ) { + return q[0][d_var_order[q][i]]; +} diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index d799cfad3..6ab17543f 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -87,8 +87,8 @@ public: /** get current model value */ Node getCurrentModelValue( Node n, bool partial = false ); /** get variable id */ - int getVariableId(Node f, Node n) { - return d_quant_var_id.find( f )!=d_quant_var_id.end() ? d_quant_var_id[f][n] : -1; + int getVariableId(TNode q, TNode n) { + return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1; } /** get some domain element */ Node getSomeDomainElement(TypeNode tn); @@ -231,9 +231,14 @@ public: std::map< Node, bool > d_models_valid; std::map< TNode, unsigned > d_rep_id; std::map< TypeNode, unsigned > d_domain; + std::map< Node, std::vector< int > > d_var_order; + std::map< Node, std::map< int, int > > d_var_index; +private: /** get current model value */ Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ); void processInitializeModelForTerm(Node n); + void processInitializeQuantifier( Node q ); + void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars ); public: FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name); FirstOrderModelAbs * asFirstOrderModelAbs() { return this; } @@ -242,6 +247,7 @@ public: TNode getUsedRepresentative( TNode n ); bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); } Node getFunctionValue(Node op, const char* argPrefix ); + Node getVariable( Node q, unsigned i ); }; }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 24fb53d7f..5ddecf037 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -77,21 +77,16 @@ bool QuantifierMacros::contains( Node n, Node n_s ){ } } -bool QuantifierMacros::containsBadOp( Node n, Node n_op ){ - if( n!=n_op ){ - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - if( op==n_op.getOperator() ){ - return true; - } - if( d_macro_defs.find( op )!=d_macro_defs.end() ){ - return true; - } +bool QuantifierMacros::containsBadOp( Node n, Node op ){ + if( n.getKind()==APPLY_UF ){ + Node nop = n.getOperator(); + if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){ + return true; } - for( size_t i=0; i<n.getNumChildren(); i++ ){ - if( containsBadOp( n[i], n_op ) ){ - return true; - } + } + for( size_t i=0; i<n.getNumChildren(); i++ ){ + if( containsBadOp( n[i], op ) ){ + return true; } } return false; @@ -230,6 +225,7 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod //predicate case if( isBoundVarApplyUf( n ) ){ Node n_def = NodeManager::currentNM()->mkConst( pol ); + Trace("macros-quant") << "Macro found for " << f << std::endl; Trace("macros") << "* " << n_def << " is a macro for " << n.getOperator() << std::endl; d_macro_defs[ n.getOperator() ] = n_def; } @@ -243,13 +239,13 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod for( size_t i=0; i<candidates.size(); i++ ){ Node m = candidates[i]; Node op = m.getOperator(); - if( d_macro_defs.find( op )==d_macro_defs.end() && !containsBadOp( n, m ) ){ + if( d_macro_defs.find( op )==d_macro_defs.end() ){ std::vector< Node > fvs; getFreeVariables( m, args, fvs, false ); //get definition and condition Node n_def = solveInEquality( m, n ); //definition for the macro //definition must exist and not contain any free variables apart from fvs - if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) ){ + if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) && !containsBadOp( n_def, op ) ){ Node n_cond; //condition when this definition holds //conditional must not contain any free variables apart from fvs if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){ @@ -272,6 +268,7 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod std::vector< Node > subs; if( getSubstitution( fvs, solved, vars, subs, true ) ){ n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + Trace("macros-quant") << "Macro found for " << f << std::endl; Trace("macros") << "* " << n_def << " is a macro for " << op << std::endl; d_macro_defs[op] = n_def; return; diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h index 682e47930..4fd9df5ff 100644 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h @@ -34,7 +34,7 @@ private: bool isBoundVarApplyUf( Node n ); void process( Node n, bool pol, std::vector< Node >& args, Node f ); bool contains( Node n, Node n_s ); - bool containsBadOp( Node n, Node n_op ); + bool containsBadOp( Node n, Node op ); bool isMacroLiteral( Node n, bool pol ); void getMacroCandidates( Node n, std::vector< Node >& candidates ); Node solveInEquality( Node n, Node lit ); |