From cc01e2119801bbd4fd99548b79c297fa57a1977d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 9 May 2014 06:51:43 -0500 Subject: [PATCH] Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs. --- src/expr/command.cpp | 42 ++++++++++++++++++++ src/expr/command.h | 14 +++++++ src/main/command_executor.cpp | 4 ++ src/main/command_executor_portfolio.cpp | 10 +++-- src/smt/options | 2 + src/smt/smt_engine.cpp | 4 ++ src/smt/smt_engine.h | 5 +++ src/theory/quantifiers/ambqi_builder.cpp | 23 ++++++----- src/theory/quantifiers/ambqi_builder.h | 1 + src/theory/quantifiers/first_order_model.cpp | 35 +++++++++++++++- src/theory/quantifiers/first_order_model.h | 10 ++++- src/theory/quantifiers/macros.cpp | 29 ++++++-------- 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 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 @@ -497,6 +497,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( indexd_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; id_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; igetVariable( 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; id_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& eq_vars ) { + for( unsigned i=0; i=0 && v eq_vars; + for( unsigned i=0; i::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& 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 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 ); -- 2.30.2