summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/command.cpp42
-rw-r--r--src/expr/command.h14
-rw-r--r--src/main/command_executor.cpp4
-rw-r--r--src/main/command_executor_portfolio.cpp10
-rw-r--r--src/smt/options2
-rw-r--r--src/smt/smt_engine.cpp4
-rw-r--r--src/smt/smt_engine.h5
-rwxr-xr-xsrc/theory/quantifiers/ambqi_builder.cpp23
-rwxr-xr-xsrc/theory/quantifiers/ambqi_builder.h1
-rw-r--r--src/theory/quantifiers/first_order_model.cpp35
-rw-r--r--src/theory/quantifiers/first_order_model.h10
-rw-r--r--src/theory/quantifiers/macros.cpp29
-rw-r--r--src/theory/quantifiers/macros.h2
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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback