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() {
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;
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;
}
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],
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],
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)
#endif /* CVC4_PROOF */
}
+void SmtEngine::printInstantiations() {
+ //TODO
+}
+
vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
SmtScope smts(this);
finalOptionsAreSet();
*/
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.
}\r
}else{\r
bool osuccess = true;\r
- TypeNode tn = q[0][depth].getType();\r
+ TypeNode tn = m->getVariable( q, depth ).getType();\r
for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
//get witness term\r
unsigned index = 0;\r
index = getId( it->first, index );\r
if( index<32 ){\r
Assert( index<m->d_rep_set.d_type_reps[tn].size() );\r
- terms.push_back( m->d_rep_set.d_type_reps[tn][index] );\r
+ terms[m->d_var_order[q][depth]] = m->d_rep_set.d_type_reps[tn][index];\r
+ //terms[depth] = m->d_rep_set.d_type_reps[tn][index];\r
if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){\r
//if we are incomplete, and have not yet added an instantiation, keep trying\r
index++;\r
}else{\r
success = true;\r
}\r
- terms.pop_back();\r
}\r
}while( !success && index<32 );\r
//mark if we are incomplete\r
Assert( defs.size()==1 );\r
d_value = defs[0]->d_value;\r
}else{\r
- TypeNode tn = q[0][depth].getType();\r
+ TypeNode tn = m->getVariable( q, depth ).getType();\r
unsigned def = m->d_domain[tn];\r
for( unsigned i=0; i<defs.size(); i++ ){\r
//process each simple child\r
if( Trace.isOn("ambqi-check-debug2") ){\r
Trace("ambqi-check-debug2") << "Add entry ( ";\r
for( unsigned i=0; i<entry.size(); i++ ){\r
- unsigned dSize = m->d_rep_set.d_type_reps[q[0][i].getType()].size();\r
+ unsigned dSize = m->d_rep_set.d_type_reps[m->getVariable( q, i ).getType()].size();\r
debugPrintUInt( "ambqi-check-debug2", dSize, entry[i] );\r
Trace("ambqi-check-debug2") << " ";\r
}\r
Assert( currv!=val_none );\r
d_value = currv;\r
}else{\r
- TypeNode tn = q[0][depth].getType();\r
+ TypeNode tn = m->getVariable( q, depth ).getType();\r
unsigned dom = m->d_domain[tn];\r
int vindex = depth==v1 ? 0 : ( depth==v2 ? 1 : val_none );\r
if( vindex==val_none ){\r
}else{\r
Assert( currv==val_none );\r
if( curr==val_none ){\r
- unsigned numReps = m->d_rep_set.d_type_reps[tn].size();\r
+ unsigned numReps = m->d_rep_set.getNumRepresentatives( tn );\r
Assert( numReps < 32 );\r
for( unsigned i=0; i<numReps; i++ ){\r
curr = 1 << i;\r
Assert( currv!=val_none );\r
d_value = currv;\r
}else{\r
- TypeNode tn = q[0][depth].getType();\r
+ TypeNode tn = m->getVariable( q, depth ).getType();\r
if( v==depth ){\r
unsigned numReps = m->d_rep_set.d_type_reps[tn].size();\r
Assert( numReps>0 && numReps < 32 );\r
//std::cout << "Short circuit " << it->second->d_value << " " << entry.size() << "/" << q[0].getNumChildren() << std::endl;\r
unsigned count = q[0].getNumChildren() - entry.size();\r
for( unsigned i=0; i<count; i++ ){\r
- entry.push_back( m->d_domain[q[0][entry.size()].getType()] );\r
+ entry.push_back( m->d_domain[m->getVariable( q, entry.size() ).getType()] );\r
entry_def.push_back( true );\r
}\r
construct_entry( entry, entry_def, it->second->d_value );\r
}\r
}else{\r
//take product of arguments\r
- TypeNode tn = q[0][entry.size()].getType();\r
+ TypeNode tn = m->getVariable( q, entry.size() ).getType();\r
Assert( m->isValidType( tn ) );\r
unsigned def = m->d_domain[tn];\r
if( Trace.isOn("ambqi-check-debug2") ){\r
bchildren[i] = AbsDef::val_unk;\r
}else if( n[i].getKind() == BOUND_VARIABLE ){\r
varChCount++;\r
- vchildren[i] = m->getVariableId( q, n[i] );\r
+ vchildren[i] = m->d_var_index[q][ m->getVariableId( q, n[i] ) ];\r
+ //vchildren[i] = m->getVariableId( q, n[i] );\r
}else if( m->hasTerm( n[i] ) ){\r
bchildren[i] = m->getRepresentativeId( n[i] );\r
}else{\r
void simplify( FirstOrderModelAbs * m, TNode q, unsigned depth = 0 );\r
int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){\r
std::vector< Node > terms;\r
+ terms.resize( q[0].getNumChildren() );\r
return addInstantiations( m, qe, q, terms, inst, 0 );\r
}\r
bool construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,\r
//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] );
}
}
}
+
+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]];
+}
/** 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);
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; }
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 */
}
}
-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;
//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;
}
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 ) ){
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;
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 );
projects / cvc5.git / commitdiff