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 | |
parent | 88907b94e858b701e83bbee67f542ad0ee5ae626 (diff) |
Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/command.cpp | 42 | ||||
-rw-r--r-- | src/expr/command.h | 14 | ||||
-rw-r--r-- | src/main/command_executor.cpp | 4 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 10 | ||||
-rw-r--r-- | src/smt/options | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 4 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 5 | ||||
-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 |
13 files changed, 147 insertions, 34 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 9341c9828..34cdd2e30 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1048,6 +1048,48 @@ std::string GetProofCommand::getCommandName() const throw() { return "get-proof"; } +/* class GetInstantiationsCommand */ + +GetInstantiationsCommand::GetInstantiationsCommand() throw() { +} + +void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->printInstantiations(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +//Instantiations* GetInstantiationsCommand::getResult() const throw() { +// return d_result; +//} + +void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + //d_result->toStream(out); + } +} + +Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetInstantiationsCommand* c = new GetInstantiationsCommand(); + //c->d_result = d_result; + return c; +} + +Command* GetInstantiationsCommand::clone() const { + GetInstantiationsCommand* c = new GetInstantiationsCommand(); + //c->d_result = d_result; + return c; +} + +std::string GetInstantiationsCommand::getCommandName() const throw() { + return "get-instantiations"; +} + /* class GetUnsatCoreCommand */ GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { diff --git a/src/expr/command.h b/src/expr/command.h index 0d173faf6..ad9cd1aa7 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -575,6 +575,20 @@ public: std::string getCommandName() const throw(); };/* class GetProofCommand */ +class CVC4_PUBLIC GetInstantiationsCommand : public Command { +protected: + //Instantiations* d_result; +public: + GetInstantiationsCommand() throw(); + ~GetInstantiationsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + //Instantiations* getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetInstantiationsCommand */ + class CVC4_PUBLIC GetUnsatCoreCommand : public Command { protected: //UnsatCore* d_result; diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 34b484910..4dc49ee53 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -100,6 +100,10 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) res.asSatisfiabilityResult() == Result::UNSAT ) { Command* gp = new GetProofCommand(); status = doCommandSingleton(gp); + } else if( d_options[options::dumpInstantiations] && + d_result.asSatisfiabilityResult() == Result::UNSAT ) { + Command* gi = new GetInstantiationsCommand(); + status = doCommandSingleton(gi); } } return status; diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 7392b2b62..61447afe2 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -204,12 +204,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) } Debug("portfolio::outputmode") << "Mode is " << mode - << "lastWinner is " << d_lastWinner + << "lastWinner is " << d_lastWinner << "d_seq is " << d_seq << std::endl; if(mode == 0) { d_seq->addCommand(cmd->clone()); - Command* cmdExported = + Command* cmdExported = d_lastWinner == 0 ? cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); bool ret = smtEngineInvoke(d_smts[d_lastWinner], @@ -352,12 +352,16 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) d_result.asSatisfiabilityResult() == Result::UNSAT ) { Command* gp = new GetProofCommand(); status = doCommandSingleton(gp); + } else if( d_options[options::dumpInstantiations] && + d_result.asSatisfiabilityResult() == Result::UNSAT ) { + Command* gi = new GetInstantiationsCommand(); + status = doCommandSingleton(gi); } } return status; } else if(mode == 2) { - Command* cmdExported = + Command* cmdExported = d_lastWinner == 0 ? cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); bool ret = smtEngineInvoke(d_smts[d_lastWinner], diff --git a/src/smt/options b/src/smt/options index f3429287f..7b749fc6c 100644 --- a/src/smt/options +++ b/src/smt/options @@ -35,6 +35,8 @@ option checkProofs check-proofs --check-proofs bool :link --proof :link-smt prod after UNSAT/VALID, machine-check the generated proof option dumpProofs --dump-proofs bool :default false :link --proof output proofs after every UNSAT/VALID response +option dumpInstantiations --dump-instantiations bool :default false + output instantiations of quantified formulas after every UNSAT/VALID response # this is just a placeholder for later; it doesn't show up in command-line options listings undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation (NOT YET SUPPORTED) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a411530e6..1397c10d3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3789,6 +3789,10 @@ Proof* SmtEngine::getProof() throw(ModalException) { #endif /* CVC4_PROOF */ } +void SmtEngine::printInstantiations() { + //TODO +} + vector<Expr> SmtEngine::getAssertions() throw(ModalException) { SmtScope smts(this); finalOptionsAreSet(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2991ab21b..88ba55b45 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -498,6 +498,11 @@ public: Proof* getProof() throw(ModalException); /** + * Print all instantiations made by the quantifiers module. + */ + void printInstantiations(); + + /** * Get the current set of assertions. Only permitted if the * SmtEngine is set to operate interactively. */ 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 ); |