diff options
33 files changed, 363 insertions, 196 deletions
diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt index 11133cd0f..5d51381da 100755 --- a/contrib/run-script-cascj7-fnt +++ b/contrib/run-script-cascj7-fnt @@ -25,8 +25,8 @@ function trywith { if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi } -trywith 30 --finite-model-find -trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal -trywith 10 --finite-model-find --disable-uf-ss-min-model -trywith $to --finite-model-find --mbqi=abs --pre-skolem-quant +trywith 30 --finite-model-find --sort-inference --uf-ss-fair +trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal --sort-inference --uf-ss-fair +trywith 10 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair +trywith $to --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof index bfaaf722f..eb0478e24 100755 --- a/contrib/run-script-cascj7-fof +++ b/contrib/run-script-cascj7-fof @@ -7,8 +7,6 @@ let "to = $2 - 85" file=${bench##*/} filename=${file%.*} -echo "Run $bench at $2" - # use: trywith [params..] # to attempt a run. Only thing printed on stdout is "sat" or "unsat", in # which case this run script terminates immediately. Otherwise, this @@ -16,7 +14,7 @@ echo "Run $bench at $2" function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --no-checking --no-interactive "$@" $bench) 2>/dev/null | + (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,9 +23,9 @@ function trywith { if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi } -trywith 30 -trywith 10 --decision=internal +trywith 30 --full-saturate-quant +trywith 10 --decision=internal --full-saturate-quant trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev trywith 15 --finite-model-find --decision=justification-stoponly -trywith $to --quant-cf +trywith $to --quant-cf --full-saturate-quant echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff new file mode 100755 index 000000000..893b69572 --- /dev/null +++ b/contrib/run-script-cascj7-tff @@ -0,0 +1,32 @@ +#!/bin/bash + +cvc4=cvc4 +bench="$1" +let "to = $2 - 170" + +file=${bench##*/} +filename=${file%.*} + +# use: trywith [params..] +# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in +# which case this run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + echo "--- Run $@ at $limit..."; + (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench) 2>/dev/null | + (read w1 w2 w3 result w4 w5; + case "$result" in + Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} + +trywith 15 --cbqi-recurse --full-saturate-quant +trywith 15 --decision=internal --full-saturate-quant +trywith 30 --quant-cf --qcf-tconstraint --full-saturate-quant +trywith 20 --finite-model-find +trywith 90 --full-saturate-quant +trywith $to --cbqi-recurse --full-saturate-quant --pre-skolem-quant +echo "% SZS status" "GaveUp for $filename" diff --git a/src/Makefile.am b/src/Makefile.am index 573181ccf..539afc781 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -67,8 +67,8 @@ libcvc4_la_SOURCES = \ printer/printer.cpp \ printer/dagification_visitor.h \ printer/dagification_visitor.cpp \ - printer/model_format_mode.h \ - printer/model_format_mode.cpp \ + printer/modes.h \ + printer/modes.cpp \ printer/ast/ast_printer.h \ printer/ast/ast_printer.cpp \ printer/smt1/smt1_printer.h \ diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 34cdd2e30..9f502c2ea 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1055,7 +1055,7 @@ GetInstantiationsCommand::GetInstantiationsCommand() throw() { void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() { try { - smtEngine->printInstantiations(); + d_smtEngine = smtEngine; d_commandStatus = CommandSuccess::instance(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -1070,19 +1070,21 @@ void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity if(! ok()) { this->Command::printResult(out, verbosity); } else { - //d_result->toStream(out); + d_smtEngine->printInstantiations(out); } } Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { GetInstantiationsCommand* c = new GetInstantiationsCommand(); //c->d_result = d_result; + c->d_smtEngine = d_smtEngine; return c; } Command* GetInstantiationsCommand::clone() const { GetInstantiationsCommand* c = new GetInstantiationsCommand(); //c->d_result = d_result; + c->d_smtEngine = d_smtEngine; return c; } diff --git a/src/expr/command.h b/src/expr/command.h index ad9cd1aa7..ed6be86de 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -578,6 +578,7 @@ public: class CVC4_PUBLIC GetInstantiationsCommand : public Command { protected: //Instantiations* d_result; + SmtEngine* d_smtEngine; public: GetInstantiationsCommand() throw(); ~GetInstantiationsCommand() throw() {} diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 4dc49ee53..a1410d910 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -101,7 +101,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) Command* gp = new GetProofCommand(); status = doCommandSingleton(gp); } else if( d_options[options::dumpInstantiations] && - d_result.asSatisfiabilityResult() == Result::UNSAT ) { + res.asSatisfiabilityResult() == Result::UNSAT ) { Command* gi = new GetInstantiationsCommand(); status = doCommandSingleton(gi); } diff --git a/src/printer/model_format_mode.cpp b/src/printer/modes.cpp index a8f946a8d..4f7242318 100644 --- a/src/printer/model_format_mode.cpp +++ b/src/printer/modes.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file model_format_mode.cpp +/*! \file modes.cpp ** \verbatim ** Original author: Morgan Deters ** Major contributors: Andrew Reynolds @@ -15,7 +15,7 @@ ** \todo document this file **/ -#include "printer/model_format_mode.h" +#include "printer/modes.h" namespace CVC4 { @@ -34,4 +34,18 @@ std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) { return out; } +std::ostream& operator<<(std::ostream& out, InstFormatMode mode) { + switch(mode) { + case INST_FORMAT_MODE_DEFAULT: + out << "INST_FORMAT_MODE_DEFAULT"; + break; + case INST_FORMAT_MODE_SZS: + out << "INST_FORMAT_MODE_SZS"; + break; + default: + out << "InstFormatMode:UNKNOWN![" << unsigned(mode) << "]"; + } + return out; +} + }/* CVC4 namespace */ diff --git a/src/printer/model_format_mode.h b/src/printer/modes.h index c729c6e5d..9673f791c 100644 --- a/src/printer/model_format_mode.h +++ b/src/printer/modes.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file model_format_mode.h +/*! \file modes.h ** \verbatim ** Original author: Morgan Deters ** Major contributors: Andrew Reynolds @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__PRINTER__MODEL_FORMAT_MODE_H -#define __CVC4__PRINTER__MODEL_FORMAT_MODE_H +#ifndef __CVC4__PRINTER__MODES_H +#define __CVC4__PRINTER__MODES_H #include <iostream> @@ -32,7 +32,16 @@ typedef enum { MODEL_FORMAT_MODE_TABLE, } ModelFormatMode; +/** Enumeration of inst_format modes (how to print models from get-model command). */ +typedef enum { + /** default mode (print expressions in the output language format) */ + INST_FORMAT_MODE_DEFAULT, + /** print as SZS proof */ + INST_FORMAT_MODE_SZS, +} InstFormatMode; + std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, InstFormatMode mode) CVC4_PUBLIC; }/* CVC4 namespace */ diff --git a/src/printer/options b/src/printer/options index 7e1b67986..4daa9c77d 100644 --- a/src/printer/options +++ b/src/printer/options @@ -5,7 +5,10 @@ module PRINTER "printer/options.h" Printing -option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::printer::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "printer/model_format_mode.h" :handler-include "printer/options_handlers.h" +option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::printer::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "printer/modes.h" :handler-include "printer/options_handlers.h" print format mode for models, see --model-format=help +option instFormatMode --inst-format=MODE InstFormatMode :handler CVC4::printer::stringToInstFormatMode :default INST_FORMAT_MODE_DEFAULT :read-write :include "printer/modes.h" :handler-include "printer/options_handlers.h" + print format mode for instantiations, see --inst-format=help + endmodule diff --git a/src/printer/options_handlers.h b/src/printer/options_handlers.h index 97d0e64c9..2a89a8d38 100644 --- a/src/printer/options_handlers.h +++ b/src/printer/options_handlers.h @@ -19,7 +19,7 @@ #ifndef __CVC4__PRINTER__OPTIONS_HANDLERS_H #define __CVC4__PRINTER__OPTIONS_HANDLERS_H -#include "printer/model_format_mode.h" +#include "printer/modes.h" namespace CVC4 { namespace printer { @@ -34,6 +34,16 @@ table\n\ + Print functional expressions over finite domains in a table format.\n\ "; +static const std::string instFormatHelp = "\ +Inst format modes currently supported by the --model-format option:\n\ +\n\ +default \n\ ++ Print instantiations as a list in the output language format.\n\ +\n\ +szs\n\ ++ Print instantiations as SZS compliant proof.\n\ +"; + inline ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "default") { return MODEL_FORMAT_MODE_DEFAULT; @@ -48,6 +58,19 @@ inline ModelFormatMode stringToModelFormatMode(std::string option, std::string o } } +inline InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "default") { + return INST_FORMAT_MODE_DEFAULT; + } else if(optarg == "szs") { + return INST_FORMAT_MODE_SZS; + } else if(optarg == "help") { + puts(instFormatHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --inst-format: `") + + optarg + "'. Try --inst-format help."); + } +} }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1397c10d3..0604988d3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -86,6 +86,7 @@ #include "theory/quantifiers/options.h" #include "theory/datatypes/options.h" #include "theory/strings/theory_strings_preprocess.h" +#include "printer/options.h" using namespace std; using namespace CVC4; @@ -1174,6 +1175,9 @@ void SmtEngine::setDefaults() { //must have finite model finding on options::finiteModelFind.set( true ); } + if( options::recurseCbqi() ){ + options::cbqi.set( true ); + } if( options::fmfBoundInt() ){ //must have finite model finding on options::finiteModelFind.set( true ); @@ -2895,8 +2899,9 @@ void SmtEnginePrivate::processAssertions() { Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl; vector< TypeNode > fvTypes; vector< TNode > fvs; - d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ) ); + d_assertionsToPreprocess[i] = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); if( prev!=d_assertionsToPreprocess[i] ){ + d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] ); Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl; Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl; } @@ -3789,8 +3794,16 @@ Proof* SmtEngine::getProof() throw(ModalException) { #endif /* CVC4_PROOF */ } -void SmtEngine::printInstantiations() { - //TODO +void SmtEngine::printInstantiations( std::ostream& out ) { + //if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){ + out << "% SZS CNF output start CNFRefutation for " << d_filename.c_str() << std::endl; + //} + if( d_theoryEngine ){ + d_theoryEngine->printInstantiations( out ); + } + //if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){ + out << "% SZS CNF output end CNFRefutation for " << d_filename.c_str() << std::endl; + //} } vector<Expr> SmtEngine::getAssertions() throw(ModalException) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 88ba55b45..4b981f614 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -500,7 +500,7 @@ public: /** * Print all instantiations made by the quantifiers module. */ - void printInstantiations(); + void printInstantiations( std::ostream& out ); /** * Get the current set of assertions. Only permitted if the diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 0b75c4a77..e86a96a8f 100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -15,7 +15,7 @@ #include "theory/quantifiers/ambqi_builder.h"
#include "theory/quantifiers/term_database.h"
-
+#include "theory/quantifiers/options.h"
using namespace std;
using namespace CVC4;
@@ -73,20 +73,20 @@ void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps }
}
-void AbsDef::simplify( FirstOrderModelAbs * m, TNode n, unsigned depth ) {
+void AbsDef::simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth ) {
if( d_value==val_none && !d_def.empty() ){
//process the default
std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default );
Assert( defd!=d_def.end() );
unsigned newDef = d_default;
std::vector< unsigned > to_erase;
- defd->second.simplify( m, n, depth+1 );
+ defd->second.simplify( m, q, n, depth+1 );
int defVal = defd->second.d_value;
bool isConstant = ( defVal!=val_none );
//process each child
for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
if( it->first!=d_default ){
- it->second.simplify( m, n, depth+1 );
+ it->second.simplify( m, q, n, depth+1 );
if( it->second.d_value==defVal && it->second.d_value!=val_none ){
newDef = newDef | it->first;
to_erase.push_back( it->first );
@@ -101,7 +101,7 @@ void AbsDef::simplify( FirstOrderModelAbs * m, TNode n, unsigned depth ) { d_def.erase( d_default );
//set new default
d_default = newDef;
- d_def[d_default].construct_def_entry( m, n, defVal, depth+1 );
+ d_def[d_default].construct_def_entry( m, q, n, defVal, depth+1 );
//erase redundant entries
for( unsigned i=0; i<to_erase.size(); i++ ){
d_def.erase( to_erase[i] );
@@ -120,6 +120,11 @@ void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const{ for( unsigned i=0; i<dSize; i++ ){
Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
}
+ //Trace(c) << "(";
+ //for( unsigned i=0; i<32; i++ ){
+ // Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
+ //}
+ //Trace(c) << ")";
}
void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth ) const{
@@ -148,48 +153,52 @@ void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsign }
bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ) {
- if( d_value==1 ){
- //instantiations are all true : ignore this
- return true;
- }else{
- if( depth==q[0].getNumChildren() ){
- if( qe->addInstantiation( q, terms ) ){
- Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;
- inst++;
- return true;
- }else{
- Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl;
- //we are incomplete
- return false;
- }
+ if( inst==0 || !options::fmfOneInstPerRound() ){
+ if( d_value==1 ){
+ //instantiations are all true : ignore this
+ return true;
}else{
- bool osuccess = true;
- 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;
- bool success;
- do {
- success = false;
- index = getId( it->first, index );
- if( index<32 ){
- Assert( index<m->d_rep_set.d_type_reps[tn].size() );
- 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++;
- Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl;
- }else{
- success = true;
+ if( depth==q[0].getNumChildren() ){
+ if( qe->addInstantiation( q, terms ) ){
+ Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;
+ inst++;
+ return true;
+ }else{
+ Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl;
+ //we are incomplete
+ return false;
+ }
+ }else{
+ bool osuccess = true;
+ 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;
+ bool success;
+ do {
+ success = false;
+ index = getId( it->first, index );
+ if( index<32 ){
+ Assert( index<m->d_rep_set.d_type_reps[tn].size() );
+ 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++;
+ Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl;
+ }else{
+ success = true;
+ }
}
- }
- }while( !success && index<32 );
- //mark if we are incomplete
- osuccess = osuccess && success;
+ }while( !success && index<32 );
+ //mark if we are incomplete
+ osuccess = osuccess && success;
+ }
+ return osuccess;
}
- return osuccess;
}
+ }else{
+ return true;
}
}
@@ -253,11 +262,12 @@ void AbsDef::construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< }
}
-void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth ) {
+void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth ) {
d_value = v;
if( depth<n.getNumChildren() ){
- unsigned dom = m->d_domain[n[depth].getType()];
- d_def[dom].construct_def_entry( m, n, v, depth+1 );
+ TypeNode tn = q.isNull() ? n[depth].getType() : m->getVariable( q, depth ).getType();
+ unsigned dom = m->d_domain[tn] ;
+ d_def[dom].construct_def_entry( m, q, n, v, depth+1 );
d_default = dom;
}
}
@@ -552,7 +562,7 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, for( std::map< unsigned, int >::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){
if( ( it->second==0 && n.getKind()==AND ) ||
( it->second==1 && n.getKind()==OR ) ){
- construct_def_entry( m, q[0], it->second );
+ construct_def_entry( m, q, q[0], it->second );
return true;
}
}
@@ -650,11 +660,11 @@ bool AbsDef::isSimple( unsigned n ) { return (n & (n - 1))==0;
}
-unsigned AbsDef::getId( unsigned n, unsigned start ) {
+unsigned AbsDef::getId( unsigned n, unsigned start, unsigned end ) {
Assert( n!=0 );
while( (n & ( 1 << start )) == 0 ){
start++;
- if( start==32 ){
+ if( start==end ){
return start;
}
}
@@ -804,7 +814,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;
it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );
Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;
- it->second->simplify( fm, fapps[0] );
+ it->second->simplify( fm, TNode::null(), fapps[0] );
Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;
it->second->debugPrint("ambqi-model", fm, fapps[0] );
@@ -827,7 +837,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { //do exhaustive instantiation
bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
- Trace("ambqi-check") << "exhaustive instantiation " << q << " " << effort << std::endl;
+ Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl;
if (effort==0) {
FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();
bool quantValid = true;
@@ -839,6 +849,7 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in }
}
if( quantValid ){
+ Trace("ambqi-check") << "Compute interpretation..." << std::endl;
AbsDef ad;
doCheck( fma, q, ad, q[1] );
//now process entries
@@ -846,6 +857,7 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl;
ad.debugPrint( "ambqi-inst", fma, q[0] );
Trace("ambqi-inst") << std::endl;
+ Trace("ambqi-check") << "Add instantiations..." << std::endl;
int lem = 0;
quantValid = ad.addInstantiations( fma, d_qe, q, lem );
Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl;
@@ -915,7 +927,7 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod }
Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl;
ad.debugPrint("ambqi-check-try", m, q[0] );
- ad.simplify( m, q[0] );
+ ad.simplify( m, q, q[0] );
Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl;
ad.debugPrint("ambqi-check-debug", m, q[0] );
Trace("ambqi-check-debug") << std::endl;
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index 784fa5093..349073cb4 100755 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -36,7 +36,7 @@ private: std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
std::vector< unsigned >& entry, std::vector< bool >& entry_def );
void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 );
- void construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth = 0 );
+ void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 );
void apply_ucompose( FirstOrderModelAbs * m, TNode q,
std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms,
std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 );
@@ -59,7 +59,7 @@ public: void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 );
void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const;
void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const;
- void simplify( FirstOrderModelAbs * m, TNode q, unsigned depth = 0 );
+ void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 );
int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){
std::vector< Node > terms;
terms.resize( q[0].getNumChildren() );
@@ -73,7 +73,7 @@ public: void negate();
Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );
static bool isSimple( unsigned n );
- static unsigned getId( unsigned n, unsigned start=0 );
+ static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 );
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );
//for debugging
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index e4b588ac1..3edf97467 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -102,7 +102,8 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){ if (!d_rep_set.hasType(tn)) { Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); - d_rep_set.add(mbt); + Trace("fmc-model-debug") << "Add to representative set..." << std::endl; + d_rep_set.add(tn, mbt); }else if( d_rep_set.d_type_reps[tn].size()==0 ){ Message() << "empty reps" << std::endl; exit(0); @@ -986,7 +987,7 @@ void FirstOrderModelAbs::collectEqVars( TNode q, TNode n, std::map< int, bool >& 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() ); + Assert( v>=0 && v<(int)q[0].getNumChildren() ); eq_vars[v] = true; } collectEqVars( q, n[i], eq_vars ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 0f3e53827..63df56392 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -61,7 +61,7 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { return true; } } - if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){ + if( c[index].getType().isSort() ){ //for star: check if all children are defined and have generalizations if( c[index]==st ){ ///options::fmfFmcCoverSimplify() //check if all children exist and are complete @@ -537,7 +537,9 @@ void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){ }else{ mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); } + Trace("fmc") << "Get used rep for " << mbn << std::endl; Node mbnr = fm->getUsedRepresentative( mbn ); + Trace("fmc") << "...got " << mbnr << std::endl; fm->d_model_basis_rep[tn] = mbnr; Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl; } diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 096d0cab2..703a44d03 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -198,18 +198,18 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No } } -void InstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const { +void InstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const { if( terms.size()==q[0].getNumChildren() ){ - Trace(c) << " ( "; + out << " ( "; for( unsigned i=0; i<terms.size(); i++ ){ - if( i>0 ) Trace(c) << ", "; - Trace(c) << terms[i]; + if( i>0 ) out << ", "; + //out << terms[i]; } - Trace(c) << " )" << std::endl; + out << " )" << std::endl; }else{ for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ terms.push_back( it->first ); - it->second.print( c, q, terms ); + it->second.print( out, q, terms ); terms.pop_back(); } } @@ -282,19 +282,19 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< } } -void CDInstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const{ +void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const{ if( d_valid.get() ){ if( terms.size()==q[0].getNumChildren() ){ - Trace(c) << " ( "; + out << " ( "; for( unsigned i=0; i<terms.size(); i++ ){ - if( i>0 ) Trace(c) << ", "; - Trace(c) << terms[i]; + if( i>0 ) out << ", "; + //out << terms[i]; } - Trace(c) << " )" << std::endl; + out << " )" << std::endl; }else{ for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ terms.push_back( it->first ); - it->second->print( c, q, terms ); + it->second->print( out, q, terms ); terms.pop_back(); } } diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 2cf63210b..accd3baed 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -101,7 +101,7 @@ public: /** the data */ std::map< Node, InstMatchTrie > d_data; private: - void print( const char * c, Node q, std::vector< Node >& terms ) const; + void print( std::ostream& out, Node q, std::vector< Node >& terms ) const; public: InstMatchTrie(){} ~InstMatchTrie(){} @@ -128,9 +128,9 @@ public: } bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); - void print( const char * c, Node q ) const{ + void print( std::ostream& out, Node q ) const{ std::vector< Node > terms; - print( c, q, terms ); + print( out, q, terms ); } };/* class InstMatchTrie */ @@ -142,7 +142,7 @@ public: /** is valid */ context::CDO< bool > d_valid; private: - void print( const char * c, Node q, std::vector< Node >& terms ) const; + void print( std::ostream& out, Node q, std::vector< Node >& terms ) const; public: CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} ~CDInstMatchTrie(){} @@ -169,9 +169,9 @@ public: } bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ); - void print( const char * c, Node q ) const{ + void print( std::ostream& out, Node q ) const{ std::vector< Node > terms; - print( c, q, terms ); + print( out, q, terms ); } };/* class CDInstMatchTrie */ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index f9b4dd588..fef6b38d1 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -34,6 +34,7 @@ using namespace CVC4::theory::datatypes; InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : InstStrategy( ie ), d_th( th ), d_counter( 0 ){ d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) ); + d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); } bool InstStrategySimplex::calculateShouldProcess( Node f ){ @@ -65,36 +66,33 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ArithVariables::var_iterator vi, vend; for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ ArithVar x = *vi; - if( d_th->d_internal->d_partialModel.hasEitherBound( x ) ){ - Node n = avnm.asNode(x); - - //collect instantiation constants - std::vector< Node > ics; - getInstantiationConstants( n, ics ); - for( unsigned i=0; i<ics.size(); i++ ){ + Node n = avnm.asNode(x); - NodeBuilder<> t(kind::PLUS); - if( n.getKind()==PLUS ){ - for( int j=0; j<(int)n.getNumChildren(); j++ ){ - addTermToRow( ics[i], x, n[j], t ); - } - }else{ - addTermToRow( ics[i], x, n, t ); - } - d_instRows[ics[i]].push_back( x ); - //this theory has constraints from f - Node f = TermDb::getInstConstAttr(ics[i]); - Debug("quant-arith") << "Has constraints from " << f << std::endl; - //set that we should process it - d_quantActive[ f ] = true; - //set tableaux term - if( t.getNumChildren()==0 ){ - d_tableaux_term[ics[i]][x] = NodeManager::currentNM()->mkConst( Rational(0) ); - }else if( t.getNumChildren()==1 ){ - d_tableaux_term[ics[i]][x] = t.getChild( 0 ); - }else{ - d_tableaux_term[ics[i]][x] = t; + //collect instantiation constants + std::vector< Node > ics; + getInstantiationConstants( n, ics ); + for( unsigned i=0; i<ics.size(); i++ ){ + NodeBuilder<> t(kind::PLUS); + if( n.getKind()==PLUS ){ + for( int j=0; j<(int)n.getNumChildren(); j++ ){ + addTermToRow( ics[i], x, n[j], t ); } + }else{ + addTermToRow( ics[i], x, n, t ); + } + d_instRows[ics[i]].push_back( x ); + //this theory has constraints from f + Node f = TermDb::getInstConstAttr(ics[i]); + Debug("quant-arith") << "Has constraints from " << f << std::endl; + //set that we should process it + d_quantActive[ f ] = true; + //set tableaux term + if( t.getNumChildren()==0 ){ + d_tableaux_term[ics[i]][x] = d_zero; + }else if( t.getNumChildren()==1 ){ + d_tableaux_term[ics[i]][x] = t.getChild( 0 ); + }else{ + d_tableaux_term[ics[i]][x] = t; } } } @@ -134,26 +132,50 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ if( e<2 ){ return STATUS_UNFINISHED; }else if( e==2 ){ - //Notice() << f << std::endl; - //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl; - //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl; + //the point instantiation + InstMatch m_point( f ); + bool m_point_valid = true; + int lem = 0; + //scan over all instantiation rows for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl; for( int j=0; j<(int)d_instRows[ic].size(); j++ ){ ArithVar x = d_instRows[ic][j]; if( !d_ceTableaux[ic][x].empty() ){ - Debug("quant-arith-simplex") << "Check row " << ic << " " << x << std::endl; + if( Debug.isOn("quant-arith-simplex") ){ + Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl; + Debug("quant-arith-simplex") << " "; + for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){ + if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } + Debug("quant-arith-simplex") << it->first << " * " << it->second; + } + Debug("quant-arith-simplex") << " = "; + Node v = getTableauxValue( x, false ); + Debug("quant-arith-simplex") << v << std::endl; + Debug("quant-arith-simplex") << " term : " << d_tableaux_term[ic][x] << std::endl; + Debug("quant-arith-simplex") << " ce-term : "; + for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){ + if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } + Debug("quant-arith-simplex") << it->first << " * " << it->second; + } + Debug("quant-arith-simplex") << std::endl; + } //instantiation row will be A*e + B*t = beta, // where e is a vector of terms , and t is vector of ground terms. // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant // We will construct the term ( beta - B*t)/coeff to use for e_i. InstMatch m( f ); + for( unsigned k=0; k<f[0].getNumChildren(); k++ ){ + if( f[0][k].getType().isInteger() ){ + m.setValue( k, d_zero ); + } + } //By default, choose the first instantiation constant to be e_i. Node var = d_ceTableaux[ic][x].begin()->first; + //if it is integer, we need to find variable with coefficent +/- 1 if( var.getType().isInteger() ){ std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); - //try to find coefficent that is +/- 1 while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){ ++it; if( it==d_ceTableaux[ic][x].end() ){ @@ -162,28 +184,35 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ var = it->first; } } - //otherwise, try one that divides all ground term coefficients? DO_THIS + //Otherwise, try one that divides all ground term coefficients? + // Might be futile, if rewrite ensures gcd of coeffs is 1. } if( !var.isNull() ){ + //add to point instantiation if applicable + if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){ + Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl; + Node v = getTableauxValue( x, false ); + if( !var.getType().isInteger() || v.getType().isInteger() ){ + m_point.setValue( i, v ); + }else{ + m_point_valid = false; + } + } Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; - doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ); + if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){ + lem++; + } }else{ Debug("quant-arith-simplex") << "Could not find var." << std::endl; } - ////choose a new variable based on alternation strategy - //int index = d_counter%(int)d_th->d_ceTableaux[x].size(); - //Node var; - //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){ - // if( index==0 ){ - // var = it->first; - // break; - // } - // index--; - //} - //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var ); } } } + if( lem==0 && m_point_valid ){ + if( d_quantEngine->addInstantiation( f, m_point ) ){ + Debug("quant-arith-simplex") << "...added point instantiation." << std::endl; + } + } } return STATUS_UNKNOWN; } @@ -279,25 +308,30 @@ bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){ // make term ( beta - term )/coeff + bool vIsInteger = var.getType().isInteger(); Node beta = getTableauxValue( x, minus_delta ); - Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term ); - if( !d_ceTableaux[ic][x][var].isNull() ){ - if( var.getType().isInteger() ){ - Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); - instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal ); - }else{ - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst<Rational>() ); - instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal ); + if( !vIsInteger || beta.getType().isInteger() ){ + Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term ); + if( !d_ceTableaux[ic][x][var].isNull() ){ + if( vIsInteger ){ + Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); + instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal ); + }else{ + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst<Rational>() ); + instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal ); + } } + instVal = Rewriter::rewrite( instVal ); + //use as instantiation value for var + int vn = var.getAttribute(InstVarNumAttribute()); + m.setValue( vn, instVal ); + Debug("quant-arith") << "Add instantiation " << m << std::endl; + return d_quantEngine->addInstantiation( f, m ); + }else{ + return false; } - instVal = Rewriter::rewrite( instVal ); - //use as instantiation value for var - int vn = var.getAttribute(InstVarNumAttribute()); - m.setValue( vn, instVal ); - Debug("quant-arith") << "Add instantiation " << m << std::endl; - return d_quantEngine->addInstantiation( f, m ); } - +/* Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){ if( d_th->d_internal->d_partialModel.hasArithVar(n) ){ ArithVar v = d_th->d_internal->d_partialModel.asArithVar( n ); @@ -306,7 +340,7 @@ Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){ return NodeManager::currentNM()->mkConst( Rational(0) ); } } - +*/ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ const Rational& delta = d_th->d_internal->d_partialModel.getDelta(); DeltaRational drv = d_th->d_internal->d_partialModel.getAssignment( v ); diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index c70c90b29..a446c8b35 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -55,7 +55,7 @@ private: /** ce tableaux */ std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_ceTableaux; /** get value */ - Node getTableauxValue( Node n, bool minus_delta = false ); + //Node getTableauxValue( Node n, bool minus_delta = false ); Node getTableauxValue( arith::ArithVar v, bool minus_delta = false ); /** do instantiation */ bool doInstantiation( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var ); @@ -67,7 +67,8 @@ private: private: /** */ int d_counter; - /** negative one */ + /** constants */ + Node d_zero; Node d_negOne; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 06858cf92..123dc02b6 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -210,7 +210,7 @@ void InstantiationEngine::check( Theory::Effort e ){ } ++(d_statistics.d_instantiation_rounds); bool quantActive = false; - Debug("quantifiers") << "quantifiers: check: asserted quantifiers size" + Debug("quantifiers") << "quantifiers: check: asserted quantifiers size=" << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 38db10feb..f02a3bce1 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -82,7 +82,7 @@ option fullSaturateQuant --full-saturate-quant bool :default false option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" choose literal matching mode -option cbqi --enable-cbqi bool :default false +option cbqi --enable-cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation option recurseCbqi --cbqi-recurse bool :default false diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8fecc6ee0..a16f46ace 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -623,18 +623,20 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ } } -void QuantifiersEngine::printInstantiations( const char * c ) { - if( options::incrementalSolving() ){ - for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ - Trace(c) << "Instantiations of " << it->first << " : " << std::endl; - it->second->print( c, it->first ); - } - }else{ +void QuantifiersEngine::printInstantiations( std::ostream& out ) { + //Trace("ajr-temp") << "QE print inst." << std::endl; + //if( options::incrementalSolving() ){ + // for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ + // out << "Instantiations of " << it->first << " : " << std::endl; + // it->second->print( out, it->first ); + // } + //}else{ for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - Trace(c) << "Instantiations of " << it->first << " : " << std::endl; - it->second.print( c, it->first ); + out << "Instantiations of " << it->first << " : " << std::endl; + it->second.print( out, it->first ); + out << std::endl; } - } + //} } QuantifiersEngine::Statistics::Statistics(): diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 7a899db0c..fa3c66f4f 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -236,7 +236,7 @@ public: eq::EqualityEngine* getMasterEqualityEngine() ; public: /** print instantiations */ - void printInstantiations( const char * c ); + void printInstantiations( std::ostream& out ); /** statistics class */ class Statistics { public: diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 2e8eb51b1..7dd8d02f6 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -37,10 +37,10 @@ int RepSet::getNumRepresentatives( TypeNode tn ) const{ } } -void RepSet::add( Node n ){ - TypeNode t = n.getType(); - d_tmap[ n ] = (int)d_type_reps[t].size(); - d_type_reps[t].push_back( n ); +void RepSet::add( TypeNode tn, Node n ){ + d_tmap[ n ] = (int)d_type_reps[tn].size(); + Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl; + d_type_reps[tn].push_back( n ); } int RepSet::getIndexFor( Node n ) const { @@ -59,7 +59,7 @@ void RepSet::complete( TypeNode t ){ while( !te.isFinished() ){ Node n = *te; if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){ - add( n ); + add( t, n ); } ++te; } @@ -143,7 +143,7 @@ bool RepSetIterator::initialize(){ if( !d_rep_set->hasType( tn ) ){ Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; - d_rep_set->add( var ); + d_rep_set->add( tn, var ); } }else if( tn.isInteger() ){ bool inc = false; diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index a619915ee..c72e46e76 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -40,7 +40,7 @@ public: /** get cardinality for type */ int getNumRepresentatives( TypeNode tn ) const; /** add representative for type */ - void add( Node n ); + void add( TypeNode tn, Node n ); /** returns index in d_type_reps for node n */ int getIndexFor( Node n ) const; /** complete all values */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 18968e897..c63df83ee 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1179,6 +1179,12 @@ Node TheoryEngine::getModelValue(TNode var) { return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); } +void TheoryEngine::printInstantiations( std::ostream& out ) { + if( d_quantEngine ){ + d_quantEngine->printInstantiations( out ); + } +} + static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { std::set<TNode> all; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0495a866b..615598e44 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -759,6 +759,11 @@ public: Node getModelValue(TNode var); /** + * Print all instantiations made by the quantifiers module. + */ + void printInstantiations( std::ostream& out ); + + /** * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 7187a373f..203f116bb 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -737,7 +737,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) std::map< Node, Node >::iterator itMap; for (itMap = constantReps.begin(); itMap != constantReps.end(); ++itMap) { tm->d_reps[itMap->first] = itMap->second; - tm->d_rep_set.add(itMap->second); + tm->d_rep_set.add(itMap->second.getType(), itMap->second); } if (!fullModel) { @@ -745,14 +745,14 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // Make sure every EC has a rep for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) { tm->d_reps[itMap->first] = itMap->second; - tm->d_rep_set.add(itMap->second); + tm->d_rep_set.add(itMap->second.getType(), itMap->second); } for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { set<Node>& noRepSet = TypeSet::getSet(it); set<Node>::iterator i; for (i = noRepSet.begin(); i != noRepSet.end(); ++i) { tm->d_reps[*i] = *i; - tm->d_rep_set.add(*i); + tm->d_rep_set.add((*i).getType(), *i); } } } diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index ce12b59f1..b38ed7d63 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -22,7 +22,7 @@ #include "util/sort_inference.h" #include "theory/uf/options.h" #include "smt/options.h" -//#include "theory/rewriter.h" +#include "theory/rewriter.h" using namespace CVC4; using namespace std; @@ -172,6 +172,7 @@ bool SortInference::simplify( std::vector< Node >& assertions ){ std::map< Node, Node > var_bound; assertions[i] = simplify( assertions[i], var_bound ); if( prev!=assertions[i] ){ + assertions[i] = theory::Rewriter::rewrite( assertions[i] ); rewritten = true; Trace("sort-inference-rewrite") << prev << std::endl; Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl; @@ -626,11 +627,13 @@ Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) { Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl; Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 ); Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 ); - return NodeManager::currentNM()->mkNode( kind::FORALL, - NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ), - NodeManager::currentNM()->mkNode( kind::IMPLIES, - NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ), - v1.eqNode( v2 ) ) ); + Node ret = NodeManager::currentNM()->mkNode( kind::FORALL, + NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ), + NodeManager::currentNM()->mkNode( kind::OR, + NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ).negate(), + v1.eqNode( v2 ) ) ); + ret = theory::Rewriter::rewrite( ret ); + return ret; } int SortInference::getSortId( Node n ) { diff --git a/test/regress/regress0/quantifiers/ARI176e1.smt2 b/test/regress/regress0/quantifiers/ARI176e1.smt2 new file mode 100755 index 000000000..dbeb96f29 --- /dev/null +++ b/test/regress/regress0/quantifiers/ARI176e1.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --cbqi-recurse +; EXPECT: unsat +(set-logic UFLIA) +(assert (forall ((U Int) (V Int)) (not (= (* 3 U) (+ 22 (* (- 5) V)))) ) ) +(check-sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index b21311da1..f12e67401 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -40,7 +40,8 @@ TESTS = \ qcft-javafe.filespace.TreeWalker.006.smt2 \ qcft-smtlib3dbc51.smt2 \ symmetric_unsat_7.smt2 \ - javafe.ast.StmtVec.009.smt2 + javafe.ast.StmtVec.009.smt2 \ + ARI176e1.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 |