From 0b2f9943d55152e0958369083649dd71340864c9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 11 May 2014 14:36:50 -0500 Subject: [PATCH] More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real. --- contrib/run-script-cascj7-fnt | 8 ++--- contrib/run-script-cascj7-fof | 4 +-- contrib/run-script-cascj7-tff | 15 ++++---- src/Makefile.am | 4 +-- src/expr/command.cpp | 6 ++-- src/expr/command.h | 1 + src/main/command_executor.cpp | 2 +- .../{model_format_mode.cpp => modes.cpp} | 18 ++++++++-- src/printer/{model_format_mode.h => modes.h} | 15 ++++++-- src/printer/options | 5 ++- src/printer/options_handlers.h | 25 +++++++++++++- src/smt/smt_engine.cpp | 16 +++++++-- src/smt/smt_engine.h | 2 +- src/theory/quantifiers/ambqi_builder.cpp | 34 ++++++++++++------- src/theory/quantifiers/ambqi_builder.h | 6 ++-- src/theory/quantifiers/first_order_model.cpp | 5 +-- src/theory/quantifiers/full_model_check.cpp | 4 ++- src/theory/quantifiers/inst_match.cpp | 24 ++++++------- src/theory/quantifiers/inst_match.h | 12 +++---- .../quantifiers/instantiation_engine.cpp | 2 +- src/theory/quantifiers_engine.cpp | 22 ++++++------ src/theory/quantifiers_engine.h | 2 +- src/theory/rep_set.cpp | 12 +++---- src/theory/rep_set.h | 2 +- src/theory/theory_engine.cpp | 6 ++++ src/theory/theory_engine.h | 5 +++ src/theory/theory_model.cpp | 6 ++-- src/util/sort_inference.cpp | 15 ++++---- 28 files changed, 184 insertions(+), 94 deletions(-) rename src/printer/{model_format_mode.cpp => modes.cpp} (71%) rename src/printer/{model_format_mode.h => modes.h} (71%) 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 151413ac2..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;; diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff index 445f7b08a..893b69572 100755 --- a/contrib/run-script-cascj7-tff +++ b/contrib/run-script-cascj7-tff @@ -1,8 +1,8 @@ #!/bin/bash -cvc4=./cvc4 +cvc4=cvc4 bench="$1" -let "to = $2 - 150" +let "to = $2 - 170" file=${bench##*/} filename=${file%.*} @@ -14,7 +14,7 @@ filename=${file%.*} function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $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;; @@ -23,7 +23,10 @@ function trywith { if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi } -trywith 30 --full-saturate-quant -trywith 120 --quant-cf --qcf-tconstraint --full-saturate-quant -trywith $to --cbqi --cbqi-recurse --full-saturate-quant --flip-decision +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 similarity index 71% rename from src/printer/model_format_mode.cpp rename to 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 similarity index 71% rename from src/printer/model_format_mode.h rename to 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 @@ -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 5d6a913b0..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; @@ -2898,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; } @@ -3792,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 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 c6a5f4227..e86a96a8f 100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -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; id_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; } } @@ -556,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; } } @@ -654,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; } } @@ -808,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] ); @@ -831,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; @@ -843,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 @@ -850,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; @@ -919,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=0 && 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; i0 ) 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; i0 ) 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/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_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& explanation) { std::set 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 @@ -758,6 +758,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& noRepSet = TypeSet::getSet(it); set::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 ) { -- 2.30.2