diff options
61 files changed, 2348 insertions, 1878 deletions
diff --git a/.travis.yml b/.travis.yml index 08b7b0241..bb707536c 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,17 +4,24 @@ cache: directories: - $HOME/cxxtest -sudo: false +sudo: required +dist: trusty compiler: - gcc - clang env: - - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c' - - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c' - - TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes - - TRAVIS_LFSC=yes - - TRAVIS_LFSC=yes TRAVIS_LFSC_DISTCHECK=yes + global: + # The next declaration is the encrypted COVERITY_SCAN_TOKEN, created + # via the "travis encrypt" command using the project repo's public key + - secure: "fRfdzYwV10VeW5tVSvy5qpR8ZlkXepR7XWzCulzlHs9SRI2YY20BpzWRjyMBiGu2t7IeJKT7qdjq/CJOQEM8WS76ON7QJ1iymKaRDewDs3OhyPJ71fsFKEGgLky9blk7I9qZh23hnRVECj1oJAVry9IK04bc2zyIEjUYpjRkUAQ=" + matrix: + - TRAVIS_CVC4=yes CXXFLAGS='-std=gnu++11' + - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c' + - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c' + - TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes + - TRAVIS_LFSC=yes + - TRAVIS_LFSC=yes TRAVIS_LFSC_DISTCHECK=yes addons: apt: sources: @@ -45,7 +52,7 @@ script: configureCVC4() { echo "CVC4 config - $TRAVIS_CVC4_CONFIG"; ./configure --enable-unit-testing --enable-proof --with-portfolio $TRAVIS_CVC4_CONFIG CXXTEST=$HOME/cxxtest || - (echo; cat builds/config.log; error "CONFIGURE FAILED"); + (echo; echo "Trying to print config.log"; cat builds/config.log; error "CONFIGURE FAILED"); } error() { echo; @@ -93,11 +100,43 @@ script: [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_DISTCHECK" ] && run makeDistcheck [ -n "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_CVC4_DISTCHECK" ] && run makeCheck && run makeCheckPortfolio && run makeExamples [ -n "$TRAVIS_LFSC" ] && run LFSCchecks - [ -z "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_LFSC" ] && error "Unknown Travis-CI configuration" + [ -n "$TRAVIS_COVERITY" ] && echo "Running coverity. Skipping the normal build." + [ -z "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_LFSC" ] && [ -z "$TRAVIS_COVERITY" ] && error "Unknown Travis-CI configuration" echo "travis_fold:end:load_script" - echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}" matrix: fast_finish: true + # Rule for running Coverity Scan. + include: + - os: linux + compiler: gcc + before_install: echo -n | openssl s_client -connect scan.coverity.com:443 | sed -ne '/-BEGIN CERTIFICATE-/,/-END CERTIFICATE-/p' | sudo tee -a /etc/ssl/certs/ca- + env: + - TRAVIS_COVERITY=yes CVC4_REGRESSION_ARGS='--no-early-exit' CXXTEST="$HOME/cxxtest" + addons: + # Need to duplicate as addons will be over written. + apt: + sources: + - ubuntu-toolchain-r-test + packages: + - libgmp-dev + - libboost-dev + - libboost-thread-dev + - swig + - libcln-dev + - openjdk-7-jdk + - antlr3 + - libantlr3c-dev + coverity_scan: + project: + name: "CVC4/CVC4" + description: "Build submitted via Travis CI" + notification_email: timothy.alan.king@gmail.com + build_command_prepend: "./autogen.sh; ./configure --enable-unit-testing --enable-proof" + build_command: "make V=1 -j4 check" + branch_pattern: coverity_scan + after_failure: + - cat /home/travis/build/CVC4/CVC4/cov-int/build-log.txt notifications: email: on_success: change diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h index 5a505a3d9..a461e847c 100644 --- a/proofs/lfsc_checker/expr.h +++ b/proofs/lfsc_checker/expr.h @@ -88,7 +88,9 @@ protected: : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class) { } -public: + public: + virtual ~Expr() {} + static int markedCount; inline Expr* followDefs(); inline int getclass() const { return data & 7; } @@ -181,7 +183,7 @@ public: C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_H(CExpr,kids); Expr **kids; - ~CExpr() { + virtual ~CExpr() { delete[] kids; } CExpr(int _op) : Expr(CEXPR, _op), kids() { @@ -261,7 +263,7 @@ public: class IntExpr : public Expr { public: mpz_t n; - ~IntExpr() { + virtual ~IntExpr() { mpz_clear(n); } IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() { @@ -280,7 +282,7 @@ class IntExpr : public Expr { class RatExpr : public Expr { public: mpq_t n; - ~RatExpr() { + virtual ~RatExpr() { mpq_clear(n); } RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() { @@ -321,6 +323,9 @@ class SymExpr : public Expr { debugrefcnt(1,CREATE); #endif } + + virtual ~SymExpr() {} + #ifdef MARKVAR_32 private: int mark(); @@ -349,6 +354,8 @@ class SymSExpr : public SymExpr { debugrefcnt(1,CREATE); #endif } + + virtual ~SymSExpr() {} }; class HoleExpr : public Expr { diff --git a/src/Makefile.am b/src/Makefile.am index 235d20deb..f5e3776e5 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -364,6 +364,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/quant_equality_engine.cpp \ theory/quantifiers/ceg_instantiator.h \ theory/quantifiers/ceg_instantiator.cpp \ + theory/quantifiers/ceg_t_instantiator.h \ + theory/quantifiers/ceg_t_instantiator.cpp \ theory/quantifiers/quant_split.h \ theory/quantifiers/quant_split.cpp \ theory/quantifiers/anti_skolem.h \ diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 50da4e412..8c9992164 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -88,13 +88,25 @@ std::string int2string(int n) { } std::ostream& operator<<(std::ostream& out, CLFlagType clft) { - switch(clft) { - case CLFLAG_NULL: out << "CLFLAG_NULL"; - case CLFLAG_BOOL: out << "CLFLAG_BOOL"; - case CLFLAG_INT: out << "CLFLAG_INT"; - case CLFLAG_STRING: out << "CLFLAG_STRING"; - case CLFLAG_STRVEC: out << "CLFLAG_STRVEC"; - default: out << "CLFlagType!UNKNOWN"; + switch (clft) { + case CLFLAG_NULL: + out << "CLFLAG_NULL"; + break; + case CLFLAG_BOOL: + out << "CLFLAG_BOOL"; + break; + case CLFLAG_INT: + out << "CLFLAG_INT"; + break; + case CLFLAG_STRING: + out << "CLFLAG_STRING"; + break; + case CLFLAG_STRVEC: + out << "CLFLAG_STRVEC"; + break; + default: + out << "CLFlagType!UNKNOWN"; + break; } return out; diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 320be701d..f9055f56c 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -129,47 +129,43 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) } // dump the model/proof/unsat core if option is set - if(status) { + if (status) { Command* g = NULL; - if( d_options.getProduceModels() && - d_options.getDumpModels() && - ( res.asSatisfiabilityResult() == Result::SAT || - (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) { + if (d_options.getProduceModels() && d_options.getDumpModels() && + (res.asSatisfiabilityResult() == Result::SAT || + (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) { g = new GetModelCommand(); } - if( d_options.getProof() && - d_options.getDumpProofs() && - res.asSatisfiabilityResult() == Result::UNSAT ) { + if (d_options.getProof() && d_options.getDumpProofs() && + res.asSatisfiabilityResult() == Result::UNSAT) { g = new GetProofCommand(); } - if( d_options.getDumpInstantiations() && - ( ( d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS && - ( res.asSatisfiabilityResult() == Result::SAT || - (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) || - res.asSatisfiabilityResult() == Result::UNSAT ) ) - { + if (d_options.getDumpInstantiations() && + ((d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS && + (res.asSatisfiabilityResult() == Result::SAT || + (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) || + res.asSatisfiabilityResult() == Result::UNSAT)) { g = new GetInstantiationsCommand(); } - if( d_options.getDumpSynth() && - res.asSatisfiabilityResult() == Result::UNSAT ) - { + if (d_options.getDumpSynth() && + res.asSatisfiabilityResult() == Result::UNSAT) { g = new GetSynthSolutionCommand(); } - if( d_options.getDumpUnsatCores() && - res.asSatisfiabilityResult() == Result::UNSAT ) - { + if (d_options.getDumpUnsatCores() && + res.asSatisfiabilityResult() == Result::UNSAT) { g = new GetUnsatCoreCommand(); } - if(g != NULL) { + if (g != NULL) { // set no time limit during dumping if applicable - if( d_options.getForceNoLimitCpuWhileDump() ){ + if (d_options.getForceNoLimitCpuWhileDump()) { setNoLimitCPU(); } status = doCommandSingleton(g); + delete g; } } return status; diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 3fc589b5c..3269b7574 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -182,8 +182,6 @@ option qcfNestedConflict --qcf-nested-conflict bool :default false consider conflicts for nested quantifiers option qcfVoExp --qcf-vo-exp bool :default false qcf experimental variable ordering - - option instNoEntail --inst-no-entail bool :read-write :default true do not consider instances of quantified formulas that are currently entailed @@ -193,8 +191,11 @@ option instPropagate --inst-prop bool :read-write :default false option qcfEagerTest --qcf-eager-test bool :default true optimization, test qcf instances eagerly +option qcfEagerCheckRd --qcf-eager-check-rd bool :default true + optimization, eagerly check relevant domain of matched position option qcfSkipRd --qcf-skip-rd bool :default false optimization, skip instances based on possibly irrelevant portions of quantified formulas + ### rewrite rules options option quantRewriteRules --rewrite-rules bool :default false diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index c89005941..31a2219b9 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -133,70 +133,71 @@ antlr3CommonTokenDebugStreamSourceNew(ANTLR3_UINT32 hint, pANTLR3_TOKEN_SOURCE s return stream; }*/ -pBOUNDED_TOKEN_BUFFER -BoundedTokenBufferSourceNew(ANTLR3_UINT32 k, pANTLR3_TOKEN_SOURCE source) -{ - pBOUNDED_TOKEN_BUFFER buffer; - pANTLR3_COMMON_TOKEN_STREAM stream; - - - assert( k > 0 ); +pBOUNDED_TOKEN_BUFFER BoundedTokenBufferSourceNew(ANTLR3_UINT32 k, + pANTLR3_TOKEN_SOURCE source) { + pBOUNDED_TOKEN_BUFFER buffer; + pANTLR3_COMMON_TOKEN_STREAM stream; - /* Memory for the interface structure - */ - buffer = (pBOUNDED_TOKEN_BUFFER) ANTLR3_MALLOC(sizeof(BOUNDED_TOKEN_BUFFER_struct)); + assert(k > 0); - if (buffer == NULL) - { - return NULL; - } + /* Memory for the interface structure */ + buffer = + (pBOUNDED_TOKEN_BUFFER)ANTLR3_MALLOC(sizeof(BOUNDED_TOKEN_BUFFER_struct)); - buffer->tokenBuffer = (pANTLR3_COMMON_TOKEN*) ANTLR3_MALLOC(2*k*sizeof(pANTLR3_COMMON_TOKEN)); - buffer->currentIndex = 0; - buffer->maxIndex = 0; - buffer->k = k; - buffer->bufferSize = 2*k; - buffer->empty = ANTLR3_TRUE; - buffer->done = ANTLR3_FALSE; - - stream = antlr3CommonTokenStreamSourceNew(k,source); - if (stream == NULL) - { - return NULL; - } + if (buffer == NULL) { + return NULL; + } - stream->super = buffer; - buffer->commonTstream = stream; + buffer->tokenBuffer = (pANTLR3_COMMON_TOKEN*)ANTLR3_MALLOC( + 2 * k * sizeof(pANTLR3_COMMON_TOKEN)); + if (buffer->tokenBuffer == NULL) { + ANTLR3_FREE(buffer); + return NULL; + } - /* Defaults - */ - stream->p = -1; + buffer->currentIndex = 0; + buffer->maxIndex = 0; + buffer->k = k; + buffer->bufferSize = 2 * k; + buffer->empty = ANTLR3_TRUE; + buffer->done = ANTLR3_FALSE; + + stream = antlr3CommonTokenStreamSourceNew(k, source); + if (stream == NULL) { + ANTLR3_FREE(buffer->tokenBuffer); + ANTLR3_FREE(buffer); + return NULL; + } - /* Install the token stream API - */ - stream->tstream->_LT = tokLT; - stream->tstream->get = get; - stream->tstream->getTokenSource = getTokenSource; - stream->tstream->setTokenSource = setTokenSource; - stream->tstream->toString = toString; - stream->tstream->toStringSS = toStringSS; - stream->tstream->toStringTT = toStringTT; - stream->tstream->setDebugListener = setDebugListener; - - /* Install INT_STREAM interface - */ - stream->tstream->istream->_LA = _LA; - stream->tstream->istream->mark = mark; - stream->tstream->istream->release = release; - stream->tstream->istream->size = size; - stream->tstream->istream->index = tindex; - stream->tstream->istream->rewind = rewindStream; - stream->tstream->istream->rewindLast= rewindLast; - stream->tstream->istream->seek = seek; - stream->tstream->istream->consume = consume; - stream->tstream->istream->getSourceName = getSourceName; - - return buffer; + stream->super = buffer; + buffer->commonTstream = stream; + + /* Defaults */ + stream->p = -1; + + /* Install the token stream API */ + stream->tstream->_LT = tokLT; + stream->tstream->get = get; + stream->tstream->getTokenSource = getTokenSource; + stream->tstream->setTokenSource = setTokenSource; + stream->tstream->toString = toString; + stream->tstream->toStringSS = toStringSS; + stream->tstream->toStringTT = toStringTT; + stream->tstream->setDebugListener = setDebugListener; + + /* Install INT_STREAM interface */ + stream->tstream->istream->_LA = _LA; + stream->tstream->istream->mark = mark; + stream->tstream->istream->release = release; + stream->tstream->istream->size = size; + stream->tstream->istream->index = tindex; + stream->tstream->istream->rewind = rewindStream; + stream->tstream->istream->rewindLast = rewindLast; + stream->tstream->istream->seek = seek; + stream->tstream->istream->consume = consume; + stream->tstream->istream->getSourceName = getSourceName; + + return buffer; } // Install a debug listener adn switch to debug mode methods diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index c9515aa92..1554428f7 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -110,6 +110,7 @@ static ANTLR3_UINT32 MemoryMapFile(pANTLR3_INPUT_STREAM input, input->data = mmap(0, input->sizeBuf, PROT_READ, MAP_PRIVATE, fd, 0); errno = 0; + close(fd); if(intptr_t(input->data) == -1) { return ANTLR3_ERR_NOMEM; } diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp index 3a962f987..fb7df4576 100644 --- a/src/proof/lemma_proof.cpp +++ b/src/proof/lemma_proof.cpp @@ -34,7 +34,6 @@ std::set<Node> LemmaProofRecipe::ProofStep::getAssertions() const { } void LemmaProofRecipe::addStep(ProofStep& proofStep) { - std::list<ProofStep>::iterator existingFirstStep = d_proofSteps.begin(); d_proofSteps.push_front(proofStep); } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index e47231128..069d3530c 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2520,34 +2520,37 @@ struct SizeOrd { return a.size() < b.size(); } }; -void TheoryArithPrivate::subsumption(std::vector<ConstraintCPVec>& confs) const { + +void TheoryArithPrivate::subsumption( + std::vector<ConstraintCPVec> &confs) const { int checks CVC4_UNUSED = 0; int subsumed CVC4_UNUSED = 0; - for(size_t i =0, N= confs.size(); i < N; ++i){ - ConstraintCPVec& conf = confs[i]; + for (size_t i = 0, N = confs.size(); i < N; ++i) { + ConstraintCPVec &conf = confs[i]; std::sort(conf.begin(), conf.end()); } std::sort(confs.begin(), confs.end(), SizeOrd()); - for(size_t i = 0; i < confs.size(); i++){ - ConstraintCPVec& a = confs[i]; + for (size_t i = 0; i < confs.size(); i++) { // i is not subsumed - for(size_t j = i+1; j < confs.size();){ + for (size_t j = i + 1; j < confs.size();) { + ConstraintCPVec& a = confs[i]; ConstraintCPVec& b = confs[j]; checks++; bool subsumes = std::includes(a.begin(), a.end(), b.begin(), b.end()); - if(subsumes){ + if (subsumes) { ConstraintCPVec& back = confs.back(); b.swap(back); confs.pop_back(); subsumed++; - }else{ + } else { j++; } } } - Debug("arith::subsumption") << "subsumed " << subsumed << "/" << checks << endl; + Debug("arith::subsumption") << "subsumed " << subsumed << "/" << checks + << endl; } std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth){ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index f0981044b..de596e3d5 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -100,8 +100,10 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, d_subtheoryMap[SUB_BITBLAST] = bb_solver; } - TheoryBV::~TheoryBV() { + if (d_eagerSolver) { + delete d_eagerSolver; + } for (unsigned i = 0; i < d_subtheories.size(); ++i) { delete d_subtheories[i]; } diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index c8d18aced..9ccba38cd 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -14,18 +14,19 @@ **/ #include "theory/quantifiers/anti_skolem.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" -#include "theory/quantifiers/first_order_model.h" -#include "options/quantifiers_options.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; +namespace CVC4 { +namespace theory { +namespace quantifiers { struct sortTypeOrder { TermDb* d_tdb; @@ -74,10 +75,13 @@ bool QuantAntiSkolem::CDSkQuantCache::add( context::Context* c, std::vector< Nod } } -QuantAntiSkolem::QuantAntiSkolem( QuantifiersEngine * qe ) : QuantifiersModule( qe ){ - d_sqc = new CDSkQuantCache( qe->getUserContext() ); +QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe) + : QuantifiersModule(qe) { + d_sqc = new CDSkQuantCache(qe->getUserContext()); } +QuantAntiSkolem::~QuantAntiSkolem() { delete d_sqc; } + /* Call during quantifier engine's check */ void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ @@ -267,3 +271,6 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool } } +}/* namespace CVC4::theory::quantifiers */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index 721371159..48205db9d 100644 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -17,17 +17,39 @@ #ifndef __CVC4__THEORY__QUANT_ANTI_SKOLEM_H #define __CVC4__THEORY__QUANT_ANTI_SKOLEM_H -#include "theory/quantifiers_engine.h" +#include <map> +#include <vector> + +#include "expr/node.h" +#include "expr/type_node.h" +#include "context/cdhashset.h" #include "context/cdo.h" #include "theory/quantifiers/ce_guided_single_inv.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { namespace quantifiers { class QuantAntiSkolem : public QuantifiersModule { +public: + QuantAntiSkolem( QuantifiersEngine * qe ); + virtual ~QuantAntiSkolem(); + + bool sendAntiSkolemizeLemma( std::vector< Node >& quants, + bool pconnected = true ); + + /* Call during quantifier engine's check */ + void check( Theory::Effort e, unsigned quant_e ); + /* Called for new quantifiers */ + void registerQuantifier( Node q ) {} + void assertNode( Node n ) {} + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const { return "QuantAntiSkolem"; } + + private: typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; -private: + std::map< Node, bool > d_quant_processed; std::map< Node, SingleInvocationPartition > d_quant_sip; std::map< Node, std::vector< TypeNode > > d_ask_types; @@ -54,22 +76,10 @@ private: bool add( context::Context* c, std::vector< Node >& quants, unsigned index = 0 ); }; CDSkQuantCache * d_sqc; -public: - bool sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected = true ); -public: - QuantAntiSkolem( QuantifiersEngine * qe ); - - /* Call during quantifier engine's check */ - void check( Theory::Effort e, unsigned quant_e ); - /* Called for new quantifiers */ - void registerQuantifier( Node q ) {} - void assertNode( Node n ) {} - /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const { return "QuantAntiSkolem"; } -}; +}; /* class QuantAntiSkolem */ -} -} -} +}/* namespace CVC4::theory::quantifiers */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ #endif diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index a0d9bda0f..8e8f34cac 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -264,6 +264,7 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp Assert( mpat.getKind()==INST_CONSTANT ); d_f = quantifiers::TermDb::getInstConstAttr( mpat ); d_index = mpat.getAttribute(InstVarNumAttribute()); + d_firstTime = false; } void CandidateGeneratorQEAll::resetInstantiationRound() { diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 718d06c32..54415d974 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -767,7 +767,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { Assert( dt.isSygus() ); //get the solution Node sol; - int status; + int status = -1; if( d_last_inst_si ){ Assert( d_conj->getCegConjectureSingleInv() != NULL ); sol = d_conj->getSingleInvocationSolution( i, tn, status ); diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 981abea94..e0bbbf8ac 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -45,27 +45,41 @@ bool CegqiOutputSingleInv::addLemma( Node n ) { return d_out->addLemma( n ); } +CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe, + CegConjecture* p) + : d_qe(qe), + d_parent(p), + d_sip(new SingleInvocationPartition), + d_sol(new CegConjectureSingleInvSol(qe)), + d_ei(NULL), + d_cosi(new CegqiOutputSingleInv(this)), + d_cinst(NULL), + d_c_inst_match_trie(NULL), + d_has_ites(true) { + // third and fourth arguments set to (false,false) until we have solution + // reconstruction for delta and infinity + d_cinst = new CegInstantiator(d_qe, d_cosi, false, false); -CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ) : d_qe( qe ), d_parent( p ){ - d_has_ites = true; - if( options::incrementalSolving() ){ - d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() ); - }else{ - d_c_inst_match_trie = NULL; + if (options::incrementalSolving()) { + d_c_inst_match_trie = new inst::CDInstMatchTrie(qe->getUserContext()); } - d_cosi = new CegqiOutputSingleInv( this ); - // third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity - d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); - d_sol = new CegConjectureSingleInvSol( qe ); - - d_sip = new SingleInvocationPartition; + if (options::cegqiSingleInvPartial()) { + d_ei = new CegEntailmentInfer(qe, d_sip); + } +} - if( options::cegqiSingleInvPartial() ){ - d_ei = new CegEntailmentInfer( qe, d_sip ); - }else{ - d_ei = NULL; +CegConjectureSingleInv::~CegConjectureSingleInv() { + if (d_c_inst_match_trie) { + delete d_c_inst_match_trie; + } + delete d_cinst; + delete d_cosi; + if (d_ei) { + delete d_ei; } + delete d_sol; // (new CegConjectureSingleInvSol(qe)), + delete d_sip; // d_sip(new SingleInvocationPartition), } void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems ) { diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index feadeca39..449ab7189 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -31,11 +31,10 @@ class CegConjecture; class CegConjectureSingleInv; class CegEntailmentInfer; -class CegqiOutputSingleInv : public CegqiOutput -{ +class CegqiOutputSingleInv : public CegqiOutput { public: CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){} - ~CegqiOutputSingleInv() {} + virtual ~CegqiOutputSingleInv() {} CegConjectureSingleInv * d_out; bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); @@ -45,22 +44,13 @@ public: class SingleInvocationPartition; -class CegConjectureSingleInv -{ +class CegConjectureSingleInv { + private: friend class CegqiOutputSingleInv; -private: - SingleInvocationPartition * d_sip; - QuantifiersEngine * d_qe; - CegConjecture * d_parent; - CegConjectureSingleInvSol * d_sol; - CegEntailmentInfer * d_ei; - //the instantiator - CegqiOutputSingleInv * d_cosi; - CegInstantiator * d_cinst; - //for recognizing templates for invariant synthesis + // for recognizing templates for invariant synthesis Node substituteInvariantTemplates( - Node n, std::map< Node, Node >& prog_templ, - std::map< Node, std::vector< Node > >& prog_templ_vars ); + Node n, std::map<Node, Node>& prog_templ, + std::map<Node, std::vector<Node> >& prog_templ_vars); // partially single invocation Node removeDeepEmbedding( Node n, std::vector< Node >& progs, std::vector< TypeNode >& types, int& type_valid, @@ -73,42 +63,56 @@ private: std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); - //constructing solution - Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index, std::map< Node, Node >& weak_imp ); - Node postProcessSolution( Node n ); -private: - //list of skolems for each argument of programs - std::vector< Node > d_single_inv_arg_sk; - //list of variables/skolems for each program - std::vector< Node > d_single_inv_var; - std::vector< Node > d_single_inv_sk; - std::map< Node, int > d_single_inv_sk_index; - //program to solution index - std::map< Node, unsigned > d_prog_to_sol_index; - //lemmas produced + // constructing solution + Node constructSolution(std::vector<unsigned>& indices, unsigned i, + unsigned index, std::map<Node, Node>& weak_imp); + Node postProcessSolution(Node n); + + private: + QuantifiersEngine* d_qe; + CegConjecture* d_parent; + SingleInvocationPartition* d_sip; + CegConjectureSingleInvSol* d_sol; + CegEntailmentInfer* d_ei; + // the instantiator + CegqiOutputSingleInv* d_cosi; + CegInstantiator* d_cinst; + + // list of skolems for each argument of programs + std::vector<Node> d_single_inv_arg_sk; + // list of variables/skolems for each program + std::vector<Node> d_single_inv_var; + std::vector<Node> d_single_inv_sk; + std::map<Node, int> d_single_inv_sk_index; + // program to solution index + std::map<Node, unsigned> d_prog_to_sol_index; + // lemmas produced inst::InstMatchTrie d_inst_match_trie; - inst::CDInstMatchTrie * d_c_inst_match_trie; - //original conjecture + inst::CDInstMatchTrie* d_c_inst_match_trie; + // original conjecture Node d_orig_conjecture; // solution Node d_orig_solution; Node d_solution; Node d_sygus_solution; bool d_has_ites; -public: - //lemmas produced - std::vector< Node > d_lemmas_produced; - std::vector< std::vector< Node > > d_inst; -private: - std::vector< Node > d_curr_lemmas; - //add instantiation + + public: + // lemmas produced + std::vector<Node> d_lemmas_produced; + std::vector<std::vector<Node> > d_inst; + + private: + std::vector<Node> d_curr_lemmas; + // add instantiation bool doAddInstantiation( std::vector< Node >& subs ); //is eligible for instantiation bool isEligibleForInstantiation( Node n ); // add lemma bool addLemma( Node lem ); -public: + public: CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ); + ~CegConjectureSingleInv(); // original conjecture Node d_quant; // single invocation portion of quantified formula @@ -130,7 +134,7 @@ public: std::map< Node, Node > d_nsi_op_map; std::map< Node, Node > d_nsi_op_map_to_prog; std::map< Node, Node > d_prog_to_eval_op; -public: + public: //get the single invocation lemma(s) void getInitialSingleInvLemma( std::vector< Node >& lems ); //initialize @@ -169,12 +173,12 @@ public: }; -// partitions any formulas given to it into single invocation/non-single invocation -// only processes functions having argument types exactly matching "d_arg_types", -// and all invocations are in the same order across all functions -class SingleInvocationPartition -{ -private: +// partitions any formulas given to it into single invocation/non-single +// invocation only processes functions having argument types exactly matching +// "d_arg_types", and all invocations are in the same order across all +// functions +class SingleInvocationPartition { + private: //options Kind d_checkKind; bool inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited ); diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 987b69522..61a20ad42 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -11,24 +11,18 @@ ** ** \brief Implementation of counterexample-guided quantifier instantiation **/ + #include "theory/quantifiers/ceg_instantiator.h" +#include "theory/quantifiers/ceg_t_instantiator.h" #include "options/quantifiers_options.h" #include "smt/ite_removal.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/theory_arith.h" -#include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" -#include "theory/quantifiers/term_database.h" - -#include "theory/bv/theory_bv_utils.h" -#include "util/bitvector.h" -//#define MBP_STRICT_ASSERTIONS using namespace std; using namespace CVC4; @@ -39,9 +33,6 @@ using namespace CVC4::theory::quantifiers; CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta, bool use_vts_inf ) : d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_vts_inf ){ - d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); - d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - d_true = NodeManager::currentNM()->mkConst( true ); d_is_nested_quant = false; } @@ -83,6 +74,12 @@ bool CegInstantiator::isEligible( Node n ) { return d_inelig.find( n )==d_inelig.end(); } +bool CegInstantiator::hasVariable( Node n, Node pv ) { + computeProgVars( n ); + return d_prog_var[n].find( pv )!=d_prog_var[n].end(); +} + + void CegInstantiator::registerInstantiationVariable( Node v, unsigned index ) { if( d_instantiator.find( v )==d_instantiator.end() ){ TypeNode tn = v.getType(); @@ -116,15 +113,25 @@ void CegInstantiator::unregisterInstantiationVariable( Node v ) { bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ){ if( i==d_vars.size() ){ //solved for all variables, now construct instantiation - bool needsPostprocess = !sf.d_has_coeff.empty(); + bool needsPostprocess = false; + std::map< Instantiator *, Node > pp_inst; + for( std::map< Node, Instantiator * >::iterator ita = d_active_instantiators.begin(); ita != d_active_instantiators.end(); ++ita ){ + if( ita->second->needsPostProcessInstantiation( this, sf, ita->first, effort ) ){ + needsPostprocess = true; + pp_inst[ ita->second ] = ita->first; + } + } if( needsPostprocess ){ //must make copy so that backtracking reverts sf SolvedForm sf_tmp; sf_tmp.copy( sf ); bool postProcessSuccess = true; - if( !processInstantiationCoeff( sf_tmp ) ){ - postProcessSuccess = false; - } + for( std::map< Instantiator *, Node >::iterator itp = pp_inst.begin(); itp != pp_inst.end(); ++itp ){ + if( !itp->first->postProcessInstantiation( this, sf_tmp, itp->second, effort ) ){ + postProcessSuccess = false; + break; + } + } if( postProcessSuccess ){ return doAddInstantiation( sf_tmp.d_subs, sf_tmp.d_vars ); }else{ @@ -153,8 +160,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e vinst = itin->second; } Assert( vinst!=NULL ); - d_active_instantiators[vinst] = true; - vinst->reset( pv, effort ); + d_active_instantiators[pv] = vinst; + vinst->reset( this, sf, pv, effort ); TypeNode pvtn = pv.getType(); TypeNode pvtnb = pvtn.getBaseType(); @@ -202,10 +209,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( vinst->processEqualTerm( this, sf, pv, pv_coeff, ns, effort ) ){ return true; } - //try the substitution - //if( doAddInstantiationInc( pv, ns, pv_coeff, 0, sf, effort ) ){ - // return true; - //} } } } @@ -219,87 +222,60 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e //[3] : we can solve an equality for pv ///iterate over equivalence classes to find cases where we can solve for the variable - Trace("cbqi-inst-debug") << "[3] try based on solving equalities." << std::endl; - for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){ - Node r = d_curr_type_eqc[pvtnb][k]; - std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r ); - std::vector< Node > lhs; - std::vector< bool > lhs_v; - std::vector< Node > lhs_coeff; - Assert( it_reqc!=d_curr_eqc.end() ); - for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){ - Node n = it_reqc->second[kk]; - Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl; - //must be an eligible term - if( isEligible( n ) ){ - Node ns; - Node pv_coeff; - if( !d_prog_var[n].empty() ){ - ns = applySubstitution( pvtn, n, sf, pv_coeff ); - if( !ns.isNull() ){ - computeProgVars( ns ); + if( vinst->hasProcessEquality( this, sf, pv, effort ) ){ + Trace("cbqi-inst-debug") << "[3] try based on solving equalities." << std::endl; + for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){ + Node r = d_curr_type_eqc[pvtnb][k]; + std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r ); + std::vector< Node > lhs; + std::vector< bool > lhs_v; + std::vector< Node > lhs_coeff; + Assert( it_reqc!=d_curr_eqc.end() ); + for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){ + Node n = it_reqc->second[kk]; + Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl; + //must be an eligible term + if( isEligible( n ) ){ + Node ns; + Node pv_coeff; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( pvtn, n, sf, pv_coeff ); + if( !ns.isNull() ){ + computeProgVars( ns ); + } + }else{ + ns = n; } - }else{ - ns = n; - } - if( !ns.isNull() ){ - bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); - Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl; - //std::vector< Node > term_coeffs; - //std::vector< Node > terms; - //term_coeffs.push_back( pv_coeff ); - //terms.push_back( ns ); - for( unsigned j=0; j<lhs.size(); j++ ){ - //if this term or the another has pv in it, try to solve for it - if( hasVar || lhs_v[j] ){ - Trace("cbqi-inst-debug") << "... " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl; - Node val; - Node veq_c; - if( pvtnb.isReal() ){ - Node eq_lhs = lhs[j]; - Node eq_rhs = ns; - //make the same coefficient - if( pv_coeff!=lhs_coeff[j] ){ - if( !pv_coeff.isNull() ){ - Trace("cbqi-inst-debug") << "...mult lhs by " << pv_coeff << std::endl; - eq_lhs = NodeManager::currentNM()->mkNode( MULT, pv_coeff, eq_lhs ); - eq_lhs = Rewriter::rewrite( eq_lhs ); - } - if( !lhs_coeff[j].isNull() ){ - Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; - eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); - eq_rhs = Rewriter::rewrite( eq_rhs ); - } - } - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Node vts_coeff_inf; - Node vts_coeff_delta; - //isolate pv in the equality - int ires = solve_arith( pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta ); - if( ires!=0 ){ - if( doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ - return true; - } - } - }else if( pvtnb.isDatatype() ){ - val = solve_dt( pv, lhs[j], ns, lhs[j], ns ); - if( !val.isNull() ){ - if( doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ - return true; - } + if( !ns.isNull() ){ + bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); + Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl; + std::vector< Node > term_coeffs; + std::vector< Node > terms; + term_coeffs.push_back( pv_coeff ); + terms.push_back( ns ); + for( unsigned j=0; j<lhs.size(); j++ ){ + //if this term or the another has pv in it, try to solve for it + if( hasVar || lhs_v[j] ){ + Trace("cbqi-inst-debug") << "... " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl; + //processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; } + term_coeffs.push_back( lhs_coeff[j] ); + terms.push_back( lhs[j] ); + if( vinst->processEquality( this, sf, pv, term_coeffs, terms, effort ) ){ + return true; } + term_coeffs.pop_back(); + terms.pop_back(); } } + lhs.push_back( ns ); + lhs_v.push_back( hasVar ); + lhs_coeff.push_back( pv_coeff ); + }else{ + Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl; } - lhs.push_back( ns ); - lhs_v.push_back( hasVar ); - lhs_coeff.push_back( pv_coeff ); }else{ - Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl; + Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl; } - }else{ - Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl; } } } @@ -307,12 +283,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e //[4] directly look at assertions if( vinst->hasProcessAssertion( this, sf, pv, effort ) ){ Trace("cbqi-inst-debug") << "[4] try based on assertions." << std::endl; - d_vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false ); - d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false ); - std::vector< Node > mbp_bounds[2]; - std::vector< Node > mbp_coeff[2]; - std::vector< Node > mbp_vts_coeff[2][2]; - std::vector< Node > mbp_lit[2]; std::vector< Node > lits; //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; for( unsigned r=0; r<2; r++ ){ @@ -327,150 +297,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( vinst->processAssertion( this, sf, pv, lit, effort ) ){ return true; } - - - Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; - Node atom = lit.getKind()==NOT ? lit[0] : lit; - bool pol = lit.getKind()!=NOT; - if( pvtn.isReal() ){ - //arithmetic inequalities and disequalities - if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ - Assert( atom.getKind()!=GEQ || atom[1].isConst() ); - Node atom_lhs; - Node atom_rhs; - if( atom.getKind()==GEQ ){ - atom_lhs = atom[0]; - atom_rhs = atom[1]; - }else{ - atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); - atom_lhs = Rewriter::rewrite( atom_lhs ); - atom_rhs = d_zero; - } - //must be an eligible term - if( isEligible( atom_lhs ) ){ - //apply substitution to LHS of atom - if( !d_prog_var[atom_lhs].empty() ){ - Node atom_lhs_coeff; - atom_lhs = applySubstitution( pvtn, atom_lhs, sf, atom_lhs_coeff ); - if( !atom_lhs.isNull() ){ - computeProgVars( atom_lhs ); - if( !atom_lhs_coeff.isNull() ){ - atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); - } - } - } - //if it contains pv, not infinity - if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){ - Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); - //cannot contain infinity? - //if( !d_qe->getTermDatabase()->containsVtsInfinity( atom_lhs ) ){ - Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl; - Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; - Node vts_coeff_inf; - Node vts_coeff_delta; - Node val; - Node veq_c; - //isolate pv in the inequality - int ires = solve_arith( pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta ); - if( ires!=0 ){ - //disequalities are either strict upper or lower bounds - unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2; - for( unsigned r=0; r<rmax; r++ ){ - int uires = ires; - Node uval = val; - if( atom.getKind()==GEQ ){ - //push negation downwards - if( !pol ){ - uires = -ires; - if( pvtn.isInteger() ){ - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( pvtn.isReal() ); - //now is strict inequality - uires = uires*2; - } - } - }else{ - bool is_upper; - if( options::cbqiModel() ){ - // disequality is a disjunction : only consider the bound in the direction of the model - //first check if there is an infinity... - if( !vts_coeff_inf.isNull() ){ - //coefficient or val won't make a difference, just compare with zero - Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl; - Assert( vts_coeff_inf.isConst() ); - is_upper = ( vts_coeff_inf.getConst<Rational>().sgn()==1 ); - }else{ - Node rhs_value = getModelValue( val ); - Node lhs_value = pv_value; - if( !veq_c.isNull() ){ - lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); - lhs_value = Rewriter::rewrite( lhs_value ); - } - Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; - Assert( lhs_value!=rhs_value ); - Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); - cmp = Rewriter::rewrite( cmp ); - Assert( cmp.isConst() ); - is_upper = ( cmp!=d_true ); - } - }else{ - is_upper = (r==0); - } - Assert( atom.getKind()==EQUAL && !pol ); - if( pvtn.isInteger() ){ - uires = is_upper ? -1 : 1; - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( pvtn.isReal() ); - uires = is_upper ? -2 : 2; - } - } - Trace("cbqi-bound-inf") << "From " << lit << ", got : "; - if( !veq_c.isNull() ){ - Trace("cbqi-bound-inf") << veq_c << " * "; - } - Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; - //take into account delta - if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){ - if( options::cbqiModel() ){ - Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); - if( vts_coeff_delta.isNull() ){ - vts_coeff_delta = delta_coeff; - }else{ - vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff ); - vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta ); - } - }else{ - Node delta = d_qe->getTermDatabase()->getVtsDelta(); - uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); - uval = Rewriter::rewrite( uval ); - } - } - if( options::cbqiModel() ){ - //just store bounds, will choose based on tighest bound - unsigned index = uires>0 ? 0 : 1; - mbp_bounds[index].push_back( uval ); - mbp_coeff[index].push_back( veq_c ); - Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; - for( unsigned t=0; t<2; t++ ){ - mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); - } - mbp_lit[index].push_back( lit ); - }else{ - //try this bound - if( doAddInstantiationInc( pv, uval, veq_c, uires>0 ? 1 : -1, sf, effort ) ){ - return true; - } - } - } - } - } - } - } - } } } } @@ -478,206 +304,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( vinst->processAssertions( this, sf, pv, lits, effort ) ){ return true; } - if( options::cbqiModel() ){ - if( pvtn.isInteger() || pvtn.isReal() ){ - bool use_inf = d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); - bool upper_first = false; - if( options::cbqiMinBounds() ){ - upper_first = mbp_bounds[1].size()<mbp_bounds[0].size(); - } - int best_used[2]; - std::vector< Node > t_values[3]; - //try optimal bounds - for( unsigned r=0; r<2; r++ ){ - int rr = upper_first ? (1-r) : r; - best_used[rr] = -1; - if( mbp_bounds[rr].empty() ){ - if( use_inf ){ - Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << pvtn << ")" << std::endl; - //no bounds, we do +- infinity - Node val = d_qe->getTermDatabase()->getVtsInfinity( pvtn ); - //TODO : rho value for infinity? - if( rr==0 ){ - val = NodeManager::currentNM()->mkNode( UMINUS, val ); - val = Rewriter::rewrite( val ); - } - if( doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ - return true; - } - } - }else{ - Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << pvtn << ") : " << std::endl; - int best = -1; - Node best_bound_value[3]; - for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){ - Node value[3]; - if( Trace.isOn("cbqi-bound") ){ - Assert( !mbp_bounds[rr][j].isNull() ); - Trace("cbqi-bound") << " " << j << ": " << mbp_bounds[rr][j]; - if( !mbp_vts_coeff[rr][0][j].isNull() ){ - Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][0][j] << " * INF)"; - } - if( !mbp_vts_coeff[rr][1][j].isNull() ){ - Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][1][j] << " * DELTA)"; - } - if( !mbp_coeff[rr][j].isNull() ){ - Trace("cbqi-bound") << " (div " << mbp_coeff[rr][j] << ")"; - } - Trace("cbqi-bound") << ", value = "; - } - t_values[rr].push_back( Node::null() ); - //check if it is better than the current best bound : lexicographic order infinite/finite/infinitesimal parts - bool new_best = true; - for( unsigned t=0; t<3; t++ ){ - //get the value - if( t==0 ){ - value[0] = mbp_vts_coeff[rr][0][j]; - if( !value[0].isNull() ){ - Trace("cbqi-bound") << "( " << value[0] << " * INF ) + "; - }else{ - value[0] = d_zero; - } - }else if( t==1 ){ - Node t_value = getModelValue( mbp_bounds[rr][j] ); - t_values[rr][j] = t_value; - value[1] = t_value; - Trace("cbqi-bound") << value[1]; - }else{ - value[2] = mbp_vts_coeff[rr][1][j]; - if( !value[2].isNull() ){ - Trace("cbqi-bound") << " + ( " << value[2] << " * DELTA )"; - }else{ - value[2] = d_zero; - } - } - //multiply by coefficient - if( value[t]!=d_zero && !mbp_coeff[rr][j].isNull() ){ - Assert( mbp_coeff[rr][j].isConst() ); - value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / mbp_coeff[rr][j].getConst<Rational>() ), value[t] ); - value[t] = Rewriter::rewrite( value[t] ); - } - //check if new best - if( best!=-1 ){ - Assert( !value[t].isNull() && !best_bound_value[t].isNull() ); - if( value[t]!=best_bound_value[t] ){ - Kind k = rr==0 ? GEQ : LEQ; - Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); - cmp_bound = Rewriter::rewrite( cmp_bound ); - if( cmp_bound!=d_true ){ - new_best = false; - break; - } - } - } - } - Trace("cbqi-bound") << std::endl; - if( new_best ){ - for( unsigned t=0; t<3; t++ ){ - best_bound_value[t] = value[t]; - } - best = j; - } - } - if( best!=-1 ){ - Trace("cbqi-bound") << "...best bound is " << best << " : "; - if( best_bound_value[0]!=d_zero ){ - Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + "; - } - Trace("cbqi-bound") << best_bound_value[1]; - if( best_bound_value[2]!=d_zero ){ - Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; - } - Trace("cbqi-bound") << std::endl; - best_used[rr] = best; - //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict - if( !options::cbqiMidpoint() || pvtn.isInteger() || mbp_vts_coeff[rr][1][best].isNull() ){ - Node val = mbp_bounds[rr][best]; - val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.d_theta, - mbp_vts_coeff[rr][0][best], mbp_vts_coeff[rr][1][best] ); - if( !val.isNull() ){ - if( doAddInstantiationInc( pv, val, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, effort ) ){ - return true; - } - } - } - } - } - } - //if not using infinity, use model value of zero - if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){ - Node val = d_zero; - Node c; //null (one) coefficient - val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, sf.d_theta, Node::null(), Node::null() ); - if( !val.isNull() ){ - if( doAddInstantiationInc( pv, val, c, 0, sf, effort ) ){ - return true; - } - } - } - if( options::cbqiMidpoint() && !pvtn.isInteger() ){ - Node vals[2]; - bool bothBounds = true; - Trace("cbqi-bound") << "Try midpoint of bounds..." << std::endl; - for( unsigned rr=0; rr<2; rr++ ){ - int best = best_used[rr]; - if( best==-1 ){ - bothBounds = false; - }else{ - vals[rr] = mbp_bounds[rr][best]; - vals[rr] = getModelBasedProjectionValue( pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.d_theta, - mbp_vts_coeff[rr][0][best], Node::null() ); - } - Trace("cbqi-bound") << "Bound : " << vals[rr] << std::endl; - } - Node val; - if( bothBounds ){ - Assert( !vals[0].isNull() && !vals[1].isNull() ); - if( vals[0]==vals[1] ){ - val = vals[0]; - }else{ - val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ), - NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) ); - val = Rewriter::rewrite( val ); - } - }else{ - if( !vals[0].isNull() ){ - val = NodeManager::currentNM()->mkNode( PLUS, vals[0], d_one ); - val = Rewriter::rewrite( val ); - }else if( !vals[1].isNull() ){ - val = NodeManager::currentNM()->mkNode( MINUS, vals[1], d_one ); - val = Rewriter::rewrite( val ); - } - } - Trace("cbqi-bound") << "Midpoint value : " << val << std::endl; - if( !val.isNull() ){ - if( doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ - return true; - } - } - } - #ifdef MBP_STRICT_ASSERTIONS - Assert( false ); - #endif - if( options::cbqiNopt() ){ - //try non-optimal bounds (heuristic, may help when nested quantification) ? - Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; - for( unsigned r=0; r<2; r++ ){ - int rr = upper_first ? (1-r) : r; - for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){ - if( (int)j!=best_used[rr] && ( !options::cbqiMidpoint() || mbp_vts_coeff[rr][1][j].isNull() ) ){ - Node val = getModelBasedProjectionValue( pv, mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], sf.d_theta, - mbp_vts_coeff[rr][0][j], mbp_vts_coeff[rr][1][j] ); - if( !val.isNull() ){ - if( doAddInstantiationInc( pv, val, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, effort ) ){ - return true; - } - } - } - } - } - } - } - } } } @@ -685,7 +311,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype bool use_model_value = vinst->useModelValue( this, sf, pv, effort ); if( ( effort>0 || use_model_value || is_cv ) && vinst->allowModelValue( this, sf, pv, effort ) ){ - #ifdef CVC4_ASSERTIONS if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){ Trace("cbqi-warn") << "Had to resort to model value." << std::endl; @@ -696,10 +321,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e Node pv_coeff_m; Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl; int new_effort = use_model_value ? effort : 1; -#ifdef MBP_STRICT_ASSERTIONS - //we only resort to values in the case of booleans - Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); -#endif if( doAddInstantiationInc( pv, mv, pv_coeff_m, 0, sf, new_effort ) ){ return true; } @@ -708,9 +329,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( is_cv ){ d_stack_vars.push_back( pv ); } - if( vinst!=NULL ){ - d_active_instantiators.erase( vinst ); - } + d_active_instantiators.erase( pv ); unregisterInstantiationVariable( pv ); return false; } @@ -842,59 +461,6 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int } } -bool CegInstantiator::processInstantiationCoeff( SolvedForm& sf ) { - for( unsigned j=0; j<sf.d_has_coeff.size(); j++ ){ - Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), sf.d_has_coeff[j] )!=sf.d_vars.end() ); - unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), sf.d_has_coeff[j] )-sf.d_vars.begin(); - Assert( !sf.d_coeff[index].isNull() ); - Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl; - Assert( sf.d_vars[index].getType().isInteger() ); - //must ensure that divisibility constraints are met - //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful - Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], sf.d_vars[index] ); - Node eq_rhs = sf.d_subs[index]; - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - Node veq; - if( QuantArith::isolate( sf.d_vars[index], msum, veq, EQUAL, true )!=0 ){ - Node veq_c; - if( veq[0]!=sf.d_vars[index] ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==sf.d_vars[index] ); - } - } - sf.d_subs[index] = veq[1]; - if( !veq_c.isNull() ){ - sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c ); - Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_btyp[index] << std::endl; - //intger division rounding up if from a lower bound - if( sf.d_btyp[index]==1 && options::cbqiRoundUpLowerLia() ){ - sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index], - NodeManager::currentNM()->mkNode( ITE, - NodeManager::currentNM()->mkNode( EQUAL, - NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ), - d_zero ), - d_zero, d_one ) - ); - } - } - Trace("cbqi-inst-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl; - }else{ - Trace("cbqi-inst-debug") << "...failed." << std::endl; - return false; - } - }else{ - Trace("cbqi-inst-debug") << "...failed." << std::endl; - return false; - } - } - return true; -} - bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ) { if( vars.size()>d_vars.size() ){ Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl; @@ -920,9 +486,6 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector } } bool ret = d_out->doAddInstantiation( subs ); -#ifdef MBP_STRICT_ASSERTIONS - Assert( ret ); -#endif return ret; } @@ -1030,66 +593,6 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node } } -Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { - Node val = t; - Trace("cbqi-bound2") << "Value : " << val << std::endl; - Assert( !e.getType().isInteger() || t.getType().isInteger() ); - Assert( !e.getType().isInteger() || mt.getType().isInteger() ); - //add rho value - //get the value of c*e - Node ceValue = me; - Node new_theta = theta; - if( !c.isNull() ){ - Assert( c.getType().isInteger() ); - ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c ); - ceValue = Rewriter::rewrite( ceValue ); - if( new_theta.isNull() ){ - new_theta = c; - }else{ - new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c ); - new_theta = Rewriter::rewrite( new_theta ); - } - Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl; - Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl; - } - if( !new_theta.isNull() && e.getType().isInteger() ){ - Node rho; - //if( !mt.getType().isInteger() ){ - //round up/down - //mt = NodeManager::currentNM()->mkNode( - //} - if( isLower ){ - rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); - }else{ - rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue ); - } - rho = Rewriter::rewrite( rho ); - Trace("cbqi-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; - Trace("cbqi-bound2") << "..." << rho << " mod " << new_theta << " = "; - rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); - rho = Rewriter::rewrite( rho ); - Trace("cbqi-bound2") << rho << std::endl; - Kind rk = isLower ? PLUS : MINUS; - val = NodeManager::currentNM()->mkNode( rk, val, rho ); - val = Rewriter::rewrite( val ); - Trace("cbqi-bound2") << "(after rho) : " << val << std::endl; - } - if( !inf_coeff.isNull() ){ - Assert( !d_vts_sym[0].isNull() ); - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) ); - val = Rewriter::rewrite( val ); - } - if( !delta_coeff.isNull() ){ - //create delta here if necessary - if( d_vts_sym[1].isNull() ){ - d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta(); - } - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, d_vts_sym[1] ) ); - val = Rewriter::rewrite( val ); - } - return val; -} - bool CegInstantiator::check() { if( d_qe->getTheoryEngine()->needCheck() ){ Trace("cbqi-engine") << " CEGQI instantiator : wait until all ground theories are finished." << std::endl; @@ -1292,9 +795,7 @@ void CegInstantiator::processAssertions() { addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second ); }else{ Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!!" << std::endl; -#ifdef MBP_STRICT_ASSERTIONS Assert( false ); -#endif } } @@ -1474,169 +975,6 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } } -//this isolates the atom into solved form -// veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf -// ensures val is Int if pv is Int, and val does not contain vts symbols -int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { - int ires = 0; - Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( atom, msum ) ){ - Trace("cbqi-inst-debug") << "got monomial sum: " << std::endl; - if( Trace.isOn("cbqi-inst-debug") ){ - QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); - } - TypeNode pvtn = pv.getType(); - //remove vts symbols from polynomial - Node vts_coeff[2]; - for( unsigned t=0; t<2; t++ ){ - if( !d_vts_sym[t].isNull() ){ - std::map< Node, Node >::iterator itminf = msum.find( d_vts_sym[t] ); - if( itminf!=msum.end() ){ - vts_coeff[t] = itminf->second; - if( vts_coeff[t].isNull() ){ - vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - } - //negate if coefficient on variable is positive - std::map< Node, Node >::iterator itv = msum.find( pv ); - if( itv!=msum.end() ){ - //multiply by the coefficient we will isolate for - if( itv->second.isNull() ){ - vts_coeff[t] = QuantArith::negate(vts_coeff[t]); - }else{ - if( !pvtn.isInteger() ){ - vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] ); - vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); - }else if( itv->second.getConst<Rational>().sgn()==1 ){ - vts_coeff[t] = QuantArith::negate(vts_coeff[t]); - } - } - } - Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; - msum.erase( d_vts_sym[t] ); - } - } - } - - ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); - if( ires!=0 ){ - Node realPart; - if( Trace.isOn("cbqi-inst-debug") ){ - Trace("cbqi-inst-debug") << "Isolate : "; - if( !veq_c.isNull() ){ - Trace("cbqi-inst-debug") << veq_c << " * "; - } - Trace("cbqi-inst-debug") << pv << " " << atom.getKind() << " " << val << std::endl; - } - if( options::cbqiAll() ){ - // when not pure LIA/LRA, we must check whether the lhs contains pv - if( TermDb::containsTerm( val, pv ) ){ - Trace("cbqi-inst-debug") << "fail : contains bad term" << std::endl; - return 0; - } - } - if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){ - //redo, split integer/non-integer parts - bool useCoeff = false; - Integer coeff = d_one.getConst<Rational>().getNumerator(); - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if( it->first.isNull() || it->first.getType().isInteger() ){ - if( !it->second.isNull() ){ - coeff = coeff.lcm( it->second.getConst<Rational>().getDenominator() ); - useCoeff = true; - } - } - } - //multiply everything by this coefficient - Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) ); - std::vector< Node > real_part; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if( useCoeff ){ - if( it->second.isNull() ){ - msum[it->first] = rcoeff; - }else{ - msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) ); - } - } - if( !it->first.isNull() && !it->first.getType().isInteger() ){ - real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) ); - } - } - //remove delta TODO: check this - vts_coeff[1] = Node::null(); - //multiply inf - if( !vts_coeff[0].isNull() ){ - vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) ); - } - realPart = real_part.empty() ? d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); - Assert( d_out->isEligibleForInstantiation( realPart ) ); - //re-isolate - Trace("cbqi-inst-debug") << "Re-isolate..." << std::endl; - ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); - Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; - Trace("cbqi-inst-debug") << " real part : " << realPart << std::endl; - if( ires!=0 ){ - int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().sgn()==1 ) ? 1 : -1; - val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS, - NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ), - NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); //TODO: round up for upper bounds? - Trace("cbqi-inst-debug") << "result : " << val << std::endl; - Assert( val.getType().isInteger() ); - } - } - } - vts_coeff_inf = vts_coeff[0]; - vts_coeff_delta = vts_coeff[1]; - Trace("cbqi-inst-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl; - }else{ - Trace("cbqi-inst-debug") << "fail : could not get monomial sum" << std::endl; - } - return ires; -} - -Node CegInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { - Trace("cbqi-inst-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl; - Node ret; - if( !a.isNull() && a==v ){ - ret = sb; - }else if( !b.isNull() && b==v ){ - ret = sa; - }else if( !a.isNull() && a.getKind()==APPLY_CONSTRUCTOR ){ - if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ - if( a.getOperator()==b.getOperator() ){ - for( unsigned i=0; i<a.getNumChildren(); i++ ){ - Node s = solve_dt( v, a[i], b[i], sa[i], sb[i] ); - if( !s.isNull() ){ - return s; - } - } - } - }else{ - unsigned cindex = Datatype::indexOf( a.getOperator().toExpr() ); - TypeNode tn = a.getType(); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - for( unsigned i=0; i<a.getNumChildren(); i++ ){ - Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), sb ); - Node s = solve_dt( v, a[i], Node::null(), sa[i], nn ); - if( !s.isNull() ){ - return s; - } - } - } - }else if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ - return solve_dt( v, b, a, sb, sa ); - } - if( !ret.isNull() ){ - //ensure does not contain - if( TermDb::containsTerm( ret, v ) ){ - ret = Node::null(); - } - } - return ret; -} - - - Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){ d_closed_enum_type = qe->getTermDatabase()->isClosedEnumerableType( tn ); @@ -1648,182 +986,3 @@ bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node } -void ArithInstantiator::reset( Node pv, unsigned effort ) { - -} - -bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { - return false; -} - -bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { - return false; -} - -bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { - return false; -} - -bool ArithInstantiator::needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, unsigned effort ) { - return !sf.d_has_coeff.empty(); -} - -bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, unsigned effort ) { - return true; -} - -void DtInstantiator::reset( Node pv, unsigned effort ) { - -} - -bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { - Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl; - //[2] look in equivalence class for a constructor - for( unsigned k=0; k<eqc.size(); k++ ){ - Node n = eqc[k]; - if( n.getKind()==APPLY_CONSTRUCTOR ){ - Trace("cbqi-inst-debug") << "...try based on constructor term " << n << std::endl; - std::vector< Node > children; - children.push_back( n.getOperator() ); - const Datatype& dt = ((DatatypeType)(d_type).toType()).getDatatype(); - unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() ); - //now must solve for selectors applied to pv - for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ - Node c = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ); - ci->pushStackVariable( c ); - children.push_back( c ); - } - Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); - if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ - return true; - }else{ - //cleanup - for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ - ci->popStackVariable(); - } - break; - } - } - } - return false; -} - -bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { - return false; -} - -void EprInstantiator::reset( Node pv, unsigned effort ) { - d_equal_terms.clear(); -} - -bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) { - if( options::quantEprMatching() ){ - Assert( pv_coeff.isNull() ); - d_equal_terms.push_back( n ); - return false; - }else{ - return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort ); - } -} - -void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ) { - if( index==catom.getNumChildren() ){ - Assert( tat->hasNodeData() ); - Node gcatom = tat->getNodeData(); - Trace("epr-inst") << "Matched : " << catom << " and " << gcatom << std::endl; - for( unsigned i=0; i<catom.getNumChildren(); i++ ){ - if( catom[i]==pv ){ - Trace("epr-inst") << "...increment " << gcatom[i] << std::endl; - match_score[gcatom[i]]++; - }else{ - //recursive matching - computeMatchScore( ci, pv, catom[i], gcatom[i], match_score ); - } - } - }else{ - std::map< TNode, TermArgTrie >::iterator it = tat->d_data.find( arg_reps[index] ); - if( it!=tat->d_data.end() ){ - computeMatchScore( ci, pv, catom, arg_reps, &it->second, index+1, match_score ); - } - } -} - -void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) { - if( inst::Trigger::isAtomicTrigger( catom ) && TermDb::containsTerm( catom, pv ) ){ - Trace("epr-inst") << "Find matches for " << catom << "..." << std::endl; - std::vector< Node > arg_reps; - for( unsigned j=0; j<catom.getNumChildren(); j++ ){ - arg_reps.push_back( ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( catom[j] ) ); - } - if( ci->getQuantifiersEngine()->getMasterEqualityEngine()->hasTerm( eqc ) ){ - Node rep = ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( eqc ); - Node op = ci->getQuantifiersEngine()->getTermDatabase()->getMatchOperator( catom ); - TermArgTrie * tat = ci->getQuantifiersEngine()->getTermDatabase()->getTermArgTrie( rep, op ); - Trace("epr-inst") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat!=NULL) << std::endl; - if( tat ){ - computeMatchScore( ci, pv, catom, arg_reps, tat, 0, match_score ); - } - } - } -} - -struct sortEqTermsMatch { - std::map< Node, int > d_match_score; - bool operator() (Node i, Node j) { - int match_score_i = d_match_score[i]; - int match_score_j = d_match_score[j]; - return match_score_i>match_score_j || ( match_score_i==match_score_j && i<j ); - } -}; - - -bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { - if( options::quantEprMatching() ){ - //heuristic for best matching constant - sortEqTermsMatch setm; - for( unsigned i=0; i<ci->getNumCEAtoms(); i++ ){ - Node catom = ci->getCEAtom( i ); - computeMatchScore( ci, pv, catom, catom, setm.d_match_score ); - } - //sort by match score - std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm ); - Node pv_coeff; - for( unsigned i=0; i<d_equal_terms.size(); i++ ){ - if( ci->doAddInstantiationInc( pv, d_equal_terms[i], pv_coeff, 0, sf, effort ) ){ - return true; - } - } - } - return false; -} - -bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { - /* TODO: algebraic reasoning for bitvector instantiation - if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){ - for( unsigned t=0; t<2; t++ ){ - if( atom[t]==pv ){ - computeProgVars( atom[1-t] ); - if( d_inelig.find( atom[1-t] )==d_inelig.end() ){ - //only ground terms TODO: more - if( d_prog_var[atom[1-t]].empty() ){ - Node veq_c; - Node uval; - if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){ - uval = atom[1-t]; - }else{ - uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], - bv::utils::mkConst(pvtn.getConst<BitVectorSize>(), 1) ); - } - if( doAddInstantiationInc( pv, uval, veq_c, 0, sf, effort ) ){ - return true; - } - } - } - } - } - } - */ - - return false; -} - diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 259c604dc..94d02de9b 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -82,13 +82,8 @@ class CegInstantiator { private: QuantifiersEngine * d_qe; CegqiOutput * d_out; - //constants - Node d_zero; - Node d_one; - Node d_true; bool d_use_vts_delta; bool d_use_vts_inf; - Node d_vts_sym[2]; //program variable contains cache std::map< Node, std::map< Node, bool > > d_prog_var; std::map< Node, bool > d_inelig; @@ -107,6 +102,8 @@ private: //atoms of the CE lemma bool d_is_nested_quant; std::vector< Node > d_ce_atoms; + //collect atoms + void collectCeAtoms( Node n, std::map< Node, bool >& visited ); private: //map from variables to their instantiators std::map< Node, Instantiator * > d_instantiator; @@ -116,33 +113,19 @@ private: //stack of temporary variables we are solving (e.g. subfields of datatypes) std::vector< Node > d_stack_vars; //used instantiators - std::map< Instantiator *, bool > d_active_instantiators; + std::map< Node, Instantiator * > d_active_instantiators; //register variable void registerInstantiationVariable( Node v, unsigned index ); void unregisterInstantiationVariable( Node v ); private: - //collect atoms - void collectCeAtoms( Node n, std::map< Node, bool >& visited ); //for adding instantiations during check void computeProgVars( Node n ); - // is eligible - bool isEligible( Node n ); // effort=0 : do not use model value, 1: use model value, 2: one must use model value bool doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ); - bool processInstantiationCoeff( SolvedForm& sf ); bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ); - Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, Node& pv_coeff, bool try_coeff = true ) { - return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff ); - } - Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, - std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); - - Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ); + //process void processAssertions(); void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); -private: - int solve_arith( Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ); - Node solve_dt( Node v, Node a, Node b, Node sa, Node sb ); public: CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); virtual ~CegInstantiator(); @@ -152,17 +135,33 @@ public: void presolve( Node q ); //register the counterexample lemma (stored in lems), modify vector void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); - -//interface for instantiators -public: + //output + CegqiOutput * getOutput() { return d_out; } //get quantifiers engine QuantifiersEngine* getQuantifiersEngine() { return d_qe; } + +//interface for instantiators +public: void pushStackVariable( Node v ); void popStackVariable(); bool doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ); Node getModelValue( Node n ); + // TODO: move to solved form? + Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, Node& pv_coeff, bool try_coeff = true ) { + return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff ); + } + Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, + std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); +public: unsigned getNumCEAtoms() { return d_ce_atoms.size(); } Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; } + // is eligible + bool isEligible( Node n ); + // has variable + bool hasVariable( Node n, Node pv ); + bool useVtsDelta() { return d_use_vts_delta; } + bool useVtsInfinity() { return d_use_vts_inf; } + bool hasNestedQuantification() { return d_is_nested_quant; } }; @@ -176,7 +175,7 @@ protected: public: Instantiator( QuantifiersEngine * qe, TypeNode tn ); virtual ~Instantiator(){} - virtual void reset( Node pv, unsigned effort ) {} + virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {} //called when pv_coeff * pv = n, and n is eligible for instantiation virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ); @@ -187,7 +186,7 @@ public: virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; } - //called when assertion lit holds and contains pv + //called when assertion lit holds. note that lit is unsubstituted, first must substitute/solve/check eligible virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } virtual bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; } virtual bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { return false; } @@ -197,8 +196,8 @@ public: virtual bool allowModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return d_closed_enum_type; } //do we need to postprocess the solved form? did we successfully postprocess - virtual bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, unsigned effort ) { return false; } - virtual bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, unsigned effort ) { return true; } + virtual bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + virtual bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } /** Identify this module (for debugging) */ virtual std::string identify() const { return "Default"; } @@ -212,59 +211,6 @@ public: std::string identify() const { return "ModelValue"; } }; -class ArithInstantiator : public Instantiator { -private: - -public: - ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} - virtual ~ArithInstantiator(){} - void reset( Node pv, unsigned effort ); - bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ); - bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); - bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ); - bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, unsigned effort ); - bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, unsigned effort ); - std::string identify() const { return "Arith"; } -}; - -class DtInstantiator : public Instantiator { -public: - DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} - virtual ~DtInstantiator(){} - void reset( Node pv, unsigned effort ); - bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); - bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ); - std::string identify() const { return "Dt"; } -}; - -class TermArgTrie; - -class EprInstantiator : public Instantiator { -private: - std::vector< Node > d_equal_terms; - void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ); - void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ); -public: - EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} - virtual ~EprInstantiator(){} - void reset( Node pv, unsigned effort ); - bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ); - bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); - std::string identify() const { return "Epr"; } -}; - -class BvInstantiator : public Instantiator { -public: - BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} - virtual ~BvInstantiator(){} - bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); - bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - std::string identify() const { return "Bv"; } -}; - } } diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp new file mode 100644 index 000000000..3282872d6 --- /dev/null +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -0,0 +1,868 @@ +/********************* */ +/*! \file ceg_t_instantiator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of theory-specific counterexample-guided quantifier instantiation + **/ + +#include "theory/quantifiers/ceg_t_instantiator.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/trigger.h" + +#include "theory/arith/partial_model.h" +#include "theory/arith/theory_arith.h" +#include "theory/arith/theory_arith_private.h" +#include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { + Node val = t; + Trace("cbqi-bound2") << "Value : " << val << std::endl; + Assert( !e.getType().isInteger() || t.getType().isInteger() ); + Assert( !e.getType().isInteger() || mt.getType().isInteger() ); + //add rho value + //get the value of c*e + Node ceValue = me; + Node new_theta = theta; + if( !c.isNull() ){ + Assert( c.getType().isInteger() ); + ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c ); + ceValue = Rewriter::rewrite( ceValue ); + if( new_theta.isNull() ){ + new_theta = c; + }else{ + new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c ); + new_theta = Rewriter::rewrite( new_theta ); + } + Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl; + Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl; + } + if( !new_theta.isNull() && e.getType().isInteger() ){ + Node rho; + //if( !mt.getType().isInteger() ){ + //round up/down + //mt = NodeManager::currentNM()->mkNode( + //} + if( isLower ){ + rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); + }else{ + rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue ); + } + rho = Rewriter::rewrite( rho ); + Trace("cbqi-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; + Trace("cbqi-bound2") << "..." << rho << " mod " << new_theta << " = "; + rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); + rho = Rewriter::rewrite( rho ); + Trace("cbqi-bound2") << rho << std::endl; + Kind rk = isLower ? PLUS : MINUS; + val = NodeManager::currentNM()->mkNode( rk, val, rho ); + val = Rewriter::rewrite( val ); + Trace("cbqi-bound2") << "(after rho) : " << val << std::endl; + } + if( !inf_coeff.isNull() ){ + Assert( !d_vts_sym[0].isNull() ); + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) ); + val = Rewriter::rewrite( val ); + } + if( !delta_coeff.isNull() ){ + //create delta here if necessary + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta() ) ); + val = Rewriter::rewrite( val ); + } + return val; +} + +//this isolates the atom into solved form +// veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf +// ensures val is Int if pv is Int, and val does not contain vts symbols +int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { + int ires = 0; + Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( atom, msum ) ){ + Trace("cbqi-inst-debug") << "got monomial sum: " << std::endl; + if( Trace.isOn("cbqi-inst-debug") ){ + QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); + } + TypeNode pvtn = pv.getType(); + //remove vts symbols from polynomial + Node vts_coeff[2]; + for( unsigned t=0; t<2; t++ ){ + if( !d_vts_sym[t].isNull() ){ + std::map< Node, Node >::iterator itminf = msum.find( d_vts_sym[t] ); + if( itminf!=msum.end() ){ + vts_coeff[t] = itminf->second; + if( vts_coeff[t].isNull() ){ + vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + } + //negate if coefficient on variable is positive + std::map< Node, Node >::iterator itv = msum.find( pv ); + if( itv!=msum.end() ){ + //multiply by the coefficient we will isolate for + if( itv->second.isNull() ){ + vts_coeff[t] = QuantArith::negate(vts_coeff[t]); + }else{ + if( !pvtn.isInteger() ){ + vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] ); + vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); + }else if( itv->second.getConst<Rational>().sgn()==1 ){ + vts_coeff[t] = QuantArith::negate(vts_coeff[t]); + } + } + } + Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; + msum.erase( d_vts_sym[t] ); + } + } + } + + ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); + if( ires!=0 ){ + Node realPart; + if( Trace.isOn("cbqi-inst-debug") ){ + Trace("cbqi-inst-debug") << "Isolate : "; + if( !veq_c.isNull() ){ + Trace("cbqi-inst-debug") << veq_c << " * "; + } + Trace("cbqi-inst-debug") << pv << " " << atom.getKind() << " " << val << std::endl; + } + if( options::cbqiAll() ){ + // when not pure LIA/LRA, we must check whether the lhs contains pv + if( TermDb::containsTerm( val, pv ) ){ + Trace("cbqi-inst-debug") << "fail : contains bad term" << std::endl; + return 0; + } + } + if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){ + //redo, split integer/non-integer parts + bool useCoeff = false; + Integer coeff = ci->getQuantifiersEngine()->getTermDatabase()->d_one.getConst<Rational>().getNumerator(); + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( it->first.isNull() || it->first.getType().isInteger() ){ + if( !it->second.isNull() ){ + coeff = coeff.lcm( it->second.getConst<Rational>().getDenominator() ); + useCoeff = true; + } + } + } + //multiply everything by this coefficient + Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) ); + std::vector< Node > real_part; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( useCoeff ){ + if( it->second.isNull() ){ + msum[it->first] = rcoeff; + }else{ + msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) ); + } + } + if( !it->first.isNull() && !it->first.getType().isInteger() ){ + real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) ); + } + } + //remove delta TODO: check this + vts_coeff[1] = Node::null(); + //multiply inf + if( !vts_coeff[0].isNull() ){ + vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) ); + } + realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermDatabase()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); + Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) ); + //re-isolate + Trace("cbqi-inst-debug") << "Re-isolate..." << std::endl; + ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); + Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; + Trace("cbqi-inst-debug") << " real part : " << realPart << std::endl; + if( ires!=0 ){ + int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().sgn()==1 ) ? 1 : -1; + val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS, + NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ), + NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); //TODO: round up for upper bounds? + Trace("cbqi-inst-debug") << "result : " << val << std::endl; + Assert( val.getType().isInteger() ); + } + } + } + vts_coeff_inf = vts_coeff[0]; + vts_coeff_delta = vts_coeff[1]; + Trace("cbqi-inst-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl; + }else{ + Trace("cbqi-inst-debug") << "fail : could not get monomial sum" << std::endl; + } + return ires; +} + +void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + d_vts_sym[0] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type, false, false ); + d_vts_sym[1] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta( false, false ); + for( unsigned i=0; i<2; i++ ){ + d_mbp_bounds[i].clear(); + d_mbp_coeff[i].clear(); + for( unsigned j=0; j<2; j++ ){ + d_mbp_vts_coeff[i][j].clear(); + } + d_mbp_lit[i].clear(); + } +} + +bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { + Node eq_lhs = terms[0]; + Node eq_rhs = terms[1]; + Node lhs_coeff = term_coeffs[0]; + Node rhs_coeff = term_coeffs[1]; + //make the same coefficient + if( rhs_coeff!=lhs_coeff ){ + if( !rhs_coeff.isNull() ){ + Trace("cbqi-inst-debug") << "...mult lhs by " << rhs_coeff << std::endl; + eq_lhs = NodeManager::currentNM()->mkNode( MULT, rhs_coeff, eq_lhs ); + eq_lhs = Rewriter::rewrite( eq_lhs ); + } + if( !lhs_coeff.isNull() ){ + Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff << std::endl; + eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff, eq_rhs ); + eq_rhs = Rewriter::rewrite( eq_rhs ); + } + } + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Node val; + Node veq_c; + Node vts_coeff_inf; + Node vts_coeff_delta; + //isolate pv in the equality + int ires = solve_arith( ci, pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta ); + if( ires!=0 ){ + if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ + return true; + } + } + + return false; +} + +bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { + Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + //arithmetic inequalities and disequalities + if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ + Assert( atom.getKind()!=GEQ || atom[1].isConst() ); + Node atom_lhs; + Node atom_rhs; + if( atom.getKind()==GEQ ){ + atom_lhs = atom[0]; + atom_rhs = atom[1]; + }else{ + atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); + atom_lhs = Rewriter::rewrite( atom_lhs ); + atom_rhs = ci->getQuantifiersEngine()->getTermDatabase()->d_zero; + } + //must be an eligible term + if( ci->isEligible( atom_lhs ) ){ + //apply substitution to LHS of atom + Node atom_lhs_coeff; + atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_coeff ); + if( !atom_lhs.isNull() ){ + if( !atom_lhs_coeff.isNull() ){ + atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); + } + } + //if it contains pv, not infinity + if( !atom_lhs.isNull() && ci->hasVariable( atom_lhs, pv ) ){ + Node pv_value = ci->getModelValue( pv ); + Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); + //cannot contain infinity? + Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl; + Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; + Node vts_coeff_inf; + Node vts_coeff_delta; + Node val; + Node veq_c; + //isolate pv in the inequality + int ires = solve_arith( ci, pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta ); + if( ires!=0 ){ + //disequalities are either strict upper or lower bounds + unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2; + for( unsigned r=0; r<rmax; r++ ){ + int uires = ires; + Node uval = val; + if( atom.getKind()==GEQ ){ + //push negation downwards + if( !pol ){ + uires = -ires; + if( d_type.isInteger() ){ + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( d_type.isReal() ); + //now is strict inequality + uires = uires*2; + } + } + }else{ + bool is_upper; + if( options::cbqiModel() ){ + // disequality is a disjunction : only consider the bound in the direction of the model + //first check if there is an infinity... + if( !vts_coeff_inf.isNull() ){ + //coefficient or val won't make a difference, just compare with zero + Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl; + Assert( vts_coeff_inf.isConst() ); + is_upper = ( vts_coeff_inf.getConst<Rational>().sgn()==1 ); + }else{ + Node rhs_value = ci->getModelValue( val ); + Node lhs_value = pv_value; + if( !veq_c.isNull() ){ + lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); + lhs_value = Rewriter::rewrite( lhs_value ); + } + Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; + Assert( lhs_value!=rhs_value ); + Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); + cmp = Rewriter::rewrite( cmp ); + Assert( cmp.isConst() ); + is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermDatabase()->d_true ); + } + }else{ + is_upper = (r==0); + } + Assert( atom.getKind()==EQUAL && !pol ); + if( d_type.isInteger() ){ + uires = is_upper ? -1 : 1; + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( d_type.isReal() ); + uires = is_upper ? -2 : 2; + } + } + Trace("cbqi-bound-inf") << "From " << lit << ", got : "; + if( !veq_c.isNull() ){ + Trace("cbqi-bound-inf") << veq_c << " * "; + } + Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; + //take into account delta + if( ci->useVtsDelta() && ( uires==2 || uires==-2 ) ){ + if( options::cbqiModel() ){ + Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); + if( vts_coeff_delta.isNull() ){ + vts_coeff_delta = delta_coeff; + }else{ + vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff ); + vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta ); + } + }else{ + Node delta = ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta(); + uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); + uval = Rewriter::rewrite( uval ); + } + } + if( options::cbqiModel() ){ + //just store bounds, will choose based on tighest bound + unsigned index = uires>0 ? 0 : 1; + d_mbp_bounds[index].push_back( uval ); + d_mbp_coeff[index].push_back( veq_c ); + Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; + for( unsigned t=0; t<2; t++ ){ + d_mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); + } + d_mbp_lit[index].push_back( lit ); + }else{ + //try this bound + if( ci->doAddInstantiationInc( pv, uval, veq_c, uires>0 ? 1 : -1, sf, effort ) ){ + return true; + } + } + } + } + } + } + } + + + return false; +} + +bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { + if( options::cbqiModel() ){ + bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); + bool upper_first = false; + if( options::cbqiMinBounds() ){ + upper_first = d_mbp_bounds[1].size()<d_mbp_bounds[0].size(); + } + int best_used[2]; + std::vector< Node > t_values[3]; + Node zero = ci->getQuantifiersEngine()->getTermDatabase()->d_zero; + Node one = ci->getQuantifiersEngine()->getTermDatabase()->d_one; + Node pv_value = ci->getModelValue( pv ); + //try optimal bounds + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + best_used[rr] = -1; + if( d_mbp_bounds[rr].empty() ){ + if( use_inf ){ + Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl; + //no bounds, we do +- infinity + Node val = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type ); + //TODO : rho value for infinity? + if( rr==0 ){ + val = NodeManager::currentNM()->mkNode( UMINUS, val ); + val = Rewriter::rewrite( val ); + } + if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ + return true; + } + } + }else{ + Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << d_type << ") : " << std::endl; + int best = -1; + Node best_bound_value[3]; + for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){ + Node value[3]; + if( Trace.isOn("cbqi-bound") ){ + Assert( !d_mbp_bounds[rr][j].isNull() ); + Trace("cbqi-bound") << " " << j << ": " << d_mbp_bounds[rr][j]; + if( !d_mbp_vts_coeff[rr][0][j].isNull() ){ + Trace("cbqi-bound") << " (+ " << d_mbp_vts_coeff[rr][0][j] << " * INF)"; + } + if( !d_mbp_vts_coeff[rr][1][j].isNull() ){ + Trace("cbqi-bound") << " (+ " << d_mbp_vts_coeff[rr][1][j] << " * DELTA)"; + } + if( !d_mbp_coeff[rr][j].isNull() ){ + Trace("cbqi-bound") << " (div " << d_mbp_coeff[rr][j] << ")"; + } + Trace("cbqi-bound") << ", value = "; + } + t_values[rr].push_back( Node::null() ); + //check if it is better than the current best bound : lexicographic order infinite/finite/infinitesimal parts + bool new_best = true; + for( unsigned t=0; t<3; t++ ){ + //get the value + if( t==0 ){ + value[0] = d_mbp_vts_coeff[rr][0][j]; + if( !value[0].isNull() ){ + Trace("cbqi-bound") << "( " << value[0] << " * INF ) + "; + }else{ + value[0] = zero; + } + }else if( t==1 ){ + Node t_value = ci->getModelValue( d_mbp_bounds[rr][j] ); + t_values[rr][j] = t_value; + value[1] = t_value; + Trace("cbqi-bound") << value[1]; + }else{ + value[2] = d_mbp_vts_coeff[rr][1][j]; + if( !value[2].isNull() ){ + Trace("cbqi-bound") << " + ( " << value[2] << " * DELTA )"; + }else{ + value[2] = zero; + } + } + //multiply by coefficient + if( value[t]!=zero && !d_mbp_coeff[rr][j].isNull() ){ + Assert( d_mbp_coeff[rr][j].isConst() ); + value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / d_mbp_coeff[rr][j].getConst<Rational>() ), value[t] ); + value[t] = Rewriter::rewrite( value[t] ); + } + //check if new best + if( best!=-1 ){ + Assert( !value[t].isNull() && !best_bound_value[t].isNull() ); + if( value[t]!=best_bound_value[t] ){ + Kind k = rr==0 ? GEQ : LEQ; + Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); + cmp_bound = Rewriter::rewrite( cmp_bound ); + if( cmp_bound!=ci->getQuantifiersEngine()->getTermDatabase()->d_true ){ + new_best = false; + break; + } + } + } + } + Trace("cbqi-bound") << std::endl; + if( new_best ){ + for( unsigned t=0; t<3; t++ ){ + best_bound_value[t] = value[t]; + } + best = j; + } + } + if( best!=-1 ){ + Trace("cbqi-bound") << "...best bound is " << best << " : "; + if( best_bound_value[0]!=zero ){ + Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + "; + } + Trace("cbqi-bound") << best_bound_value[1]; + if( best_bound_value[2]!=zero ){ + Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; + } + Trace("cbqi-bound") << std::endl; + best_used[rr] = best; + //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict + if( !options::cbqiMidpoint() || d_type.isInteger() || d_mbp_vts_coeff[rr][1][best].isNull() ){ + Node val = d_mbp_bounds[rr][best]; + val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.d_theta, + d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] ); + if( !val.isNull() ){ + if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, effort ) ){ + return true; + } + } + } + } + } + } + //if not using infinity, use model value of zero + if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){ + Node val = zero; + Node c; //null (one) coefficient + val = getModelBasedProjectionValue( ci, pv, val, true, c, pv_value, zero, sf.d_theta, Node::null(), Node::null() ); + if( !val.isNull() ){ + if( ci->doAddInstantiationInc( pv, val, c, 0, sf, effort ) ){ + return true; + } + } + } + if( options::cbqiMidpoint() && !d_type.isInteger() ){ + Node vals[2]; + bool bothBounds = true; + Trace("cbqi-bound") << "Try midpoint of bounds..." << std::endl; + for( unsigned rr=0; rr<2; rr++ ){ + int best = best_used[rr]; + if( best==-1 ){ + bothBounds = false; + }else{ + vals[rr] = d_mbp_bounds[rr][best]; + vals[rr] = getModelBasedProjectionValue( ci, pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.d_theta, + d_mbp_vts_coeff[rr][0][best], Node::null() ); + } + Trace("cbqi-bound") << "Bound : " << vals[rr] << std::endl; + } + Node val; + if( bothBounds ){ + Assert( !vals[0].isNull() && !vals[1].isNull() ); + if( vals[0]==vals[1] ){ + val = vals[0]; + }else{ + val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ), + NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) ); + val = Rewriter::rewrite( val ); + } + }else{ + if( !vals[0].isNull() ){ + val = NodeManager::currentNM()->mkNode( PLUS, vals[0], one ); + val = Rewriter::rewrite( val ); + }else if( !vals[1].isNull() ){ + val = NodeManager::currentNM()->mkNode( MINUS, vals[1], one ); + val = Rewriter::rewrite( val ); + } + } + Trace("cbqi-bound") << "Midpoint value : " << val << std::endl; + if( !val.isNull() ){ + if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ + return true; + } + } + } + //generally should not make it to this point FIXME: write proper assertion + //Assert( ( ci->hasNestedQuantification() && !options::cbqiNestedQE() ) || options::cbqiAll() ); + + if( options::cbqiNopt() ){ + //try non-optimal bounds (heuristic, may help when nested quantification) ? + Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){ + if( (int)j!=best_used[rr] && ( !options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull() ) ){ + Node val = getModelBasedProjectionValue( ci, pv, d_mbp_bounds[rr][j], rr==0, d_mbp_coeff[rr][j], pv_value, t_values[rr][j], sf.d_theta, + d_mbp_vts_coeff[rr][0][j], d_mbp_vts_coeff[rr][1][j] ); + if( !val.isNull() ){ + if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, effort ) ){ + return true; + } + } + } + } + } + } + } + return false; +} + +bool ArithInstantiator::needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + return std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end(); +} + +bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end() ); + Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() ); + unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin(); + Assert( !sf.d_coeff[index].isNull() ); + Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl; + Assert( sf.d_vars[index].getType().isInteger() ); + //must ensure that divisibility constraints are met + //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful + Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], sf.d_vars[index] ); + Node eq_rhs = sf.d_subs[index]; + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + Node veq; + if( QuantArith::isolate( sf.d_vars[index], msum, veq, EQUAL, true )!=0 ){ + Node veq_c; + if( veq[0]!=sf.d_vars[index] ){ + Node veq_v; + if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ + Assert( veq_v==sf.d_vars[index] ); + } + } + sf.d_subs[index] = veq[1]; + if( !veq_c.isNull() ){ + sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c ); + Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_btyp[index] << std::endl; + //intger division rounding up if from a lower bound + if( sf.d_btyp[index]==1 && options::cbqiRoundUpLowerLia() ){ + sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index], + NodeManager::currentNM()->mkNode( ITE, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ), + ci->getQuantifiersEngine()->getTermDatabase()->d_zero ), + ci->getQuantifiersEngine()->getTermDatabase()->d_zero, ci->getQuantifiersEngine()->getTermDatabase()->d_one ) + ); + } + } + Trace("cbqi-inst-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl; + }else{ + Trace("cbqi-inst-debug") << "...failed to isolate." << std::endl; + return false; + } + }else{ + Trace("cbqi-inst-debug") << "...failed to get monomial sum." << std::endl; + return false; + } + return true; +} + +void DtInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + +} + +Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { + Trace("cbqi-inst-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl; + Node ret; + if( !a.isNull() && a==v ){ + ret = sb; + }else if( !b.isNull() && b==v ){ + ret = sa; + }else if( !a.isNull() && a.getKind()==APPLY_CONSTRUCTOR ){ + if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ + if( a.getOperator()==b.getOperator() ){ + for( unsigned i=0; i<a.getNumChildren(); i++ ){ + Node s = solve_dt( v, a[i], b[i], sa[i], sb[i] ); + if( !s.isNull() ){ + return s; + } + } + } + }else{ + unsigned cindex = Datatype::indexOf( a.getOperator().toExpr() ); + TypeNode tn = a.getType(); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for( unsigned i=0; i<a.getNumChildren(); i++ ){ + Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), sb ); + Node s = solve_dt( v, a[i], Node::null(), sa[i], nn ); + if( !s.isNull() ){ + return s; + } + } + } + }else if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ + return solve_dt( v, b, a, sb, sa ); + } + if( !ret.isNull() ){ + //ensure does not contain + if( TermDb::containsTerm( ret, v ) ){ + ret = Node::null(); + } + } + return ret; +} + +bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { + Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl; + //[2] look in equivalence class for a constructor + for( unsigned k=0; k<eqc.size(); k++ ){ + Node n = eqc[k]; + if( n.getKind()==APPLY_CONSTRUCTOR ){ + Trace("cbqi-inst-debug") << "...try based on constructor term " << n << std::endl; + std::vector< Node > children; + children.push_back( n.getOperator() ); + const Datatype& dt = ((DatatypeType)(d_type).toType()).getDatatype(); + unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() ); + //now must solve for selectors applied to pv + for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ + Node c = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ); + ci->pushStackVariable( c ); + children.push_back( c ); + } + Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); + if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ + return true; + }else{ + //cleanup + for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ + ci->popStackVariable(); + } + break; + } + } + } + return false; +} + +bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { + Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] ); + if( !val.isNull() ){ + Node veq_c; + if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ + return true; + } + } + return false; +} + +void EprInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + d_equal_terms.clear(); +} + +bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) { + if( options::quantEprMatching() ){ + Assert( pv_coeff.isNull() ); + d_equal_terms.push_back( n ); + return false; + }else{ + return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort ); + } +} + +void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ) { + if( index==catom.getNumChildren() ){ + Assert( tat->hasNodeData() ); + Node gcatom = tat->getNodeData(); + Trace("epr-inst") << "Matched : " << catom << " and " << gcatom << std::endl; + for( unsigned i=0; i<catom.getNumChildren(); i++ ){ + if( catom[i]==pv ){ + Trace("epr-inst") << "...increment " << gcatom[i] << std::endl; + match_score[gcatom[i]]++; + }else{ + //recursive matching + computeMatchScore( ci, pv, catom[i], gcatom[i], match_score ); + } + } + }else{ + std::map< TNode, TermArgTrie >::iterator it = tat->d_data.find( arg_reps[index] ); + if( it!=tat->d_data.end() ){ + computeMatchScore( ci, pv, catom, arg_reps, &it->second, index+1, match_score ); + } + } +} + +void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) { + if( inst::Trigger::isAtomicTrigger( catom ) && TermDb::containsTerm( catom, pv ) ){ + Trace("epr-inst") << "Find matches for " << catom << "..." << std::endl; + std::vector< Node > arg_reps; + for( unsigned j=0; j<catom.getNumChildren(); j++ ){ + arg_reps.push_back( ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( catom[j] ) ); + } + if( ci->getQuantifiersEngine()->getMasterEqualityEngine()->hasTerm( eqc ) ){ + Node rep = ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( eqc ); + Node op = ci->getQuantifiersEngine()->getTermDatabase()->getMatchOperator( catom ); + TermArgTrie * tat = ci->getQuantifiersEngine()->getTermDatabase()->getTermArgTrie( rep, op ); + Trace("epr-inst") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat!=NULL) << std::endl; + if( tat ){ + computeMatchScore( ci, pv, catom, arg_reps, tat, 0, match_score ); + } + } + } +} + +struct sortEqTermsMatch { + std::map< Node, int > d_match_score; + bool operator() (Node i, Node j) { + int match_score_i = d_match_score[i]; + int match_score_j = d_match_score[j]; + return match_score_i>match_score_j || ( match_score_i==match_score_j && i<j ); + } +}; + + +bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { + if( options::quantEprMatching() ){ + //heuristic for best matching constant + sortEqTermsMatch setm; + for( unsigned i=0; i<ci->getNumCEAtoms(); i++ ){ + Node catom = ci->getCEAtom( i ); + computeMatchScore( ci, pv, catom, catom, setm.d_match_score ); + } + //sort by match score + std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm ); + Node pv_coeff; + for( unsigned i=0; i<d_equal_terms.size(); i++ ){ + if( ci->doAddInstantiationInc( pv, d_equal_terms[i], pv_coeff, 0, sf, effort ) ){ + return true; + } + } + } + return false; +} + +bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { + /* TODO: algebraic reasoning for bitvector instantiation + if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){ + for( unsigned t=0; t<2; t++ ){ + if( atom[t]==pv ){ + computeProgVars( atom[1-t] ); + if( d_inelig.find( atom[1-t] )==d_inelig.end() ){ + //only ground terms TODO: more + if( d_prog_var[atom[1-t]].empty() ){ + Node veq_c; + Node uval; + if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){ + uval = atom[1-t]; + }else{ + uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], + bv::utils::mkConst(pvtn.getConst<BitVectorSize>(), 1) ); + } + if( doAddInstantiationInc( pv, uval, veq_c, 0, sf, effort ) ){ + return true; + } + } + } + } + } + } + */ + + return false; +} + + diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h new file mode 100644 index 000000000..2df7946d5 --- /dev/null +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file ceg_t_instantiator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief theory-specific counterexample-guided quantifier instantiation + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__CEG_T_INSTANTIATOR_H +#define __CVC4__CEG_T_INSTANTIATOR_H + +#include "theory/quantifiers/ceg_instantiator.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class ArithInstantiator : public Instantiator { +private: + Node d_vts_sym[2]; + std::vector< Node > d_mbp_bounds[2]; + std::vector< Node > d_mbp_coeff[2]; + std::vector< Node > d_mbp_vts_coeff[2][2]; + std::vector< Node > d_mbp_lit[2]; + int solve_arith( CegInstantiator * ci, Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ); + Node getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ); +public: + ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~ArithInstantiator(){} + void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ); + bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); + bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ); + bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + std::string identify() const { return "Arith"; } +}; + +class DtInstantiator : public Instantiator { +private: + Node solve_dt( Node v, Node a, Node b, Node sa, Node sb ); +public: + DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~DtInstantiator(){} + void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); + bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ); + std::string identify() const { return "Dt"; } +}; + +class TermArgTrie; + +class EprInstantiator : public Instantiator { +private: + std::vector< Node > d_equal_terms; + void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ); + void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ); +public: + EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~EprInstantiator(){} + void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ); + bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); + std::string identify() const { return "Epr"; } +}; + +class BvInstantiator : public Instantiator { +public: + BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~BvInstantiator(){} + bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); + bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + std::string identify() const { return "Bv"; } +}; + + +} +} +} + +#endif diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index f4eb67d74..11adc61fd 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -84,6 +84,9 @@ d_notify( *this ), d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false), d_ee_conjectures( c ){ d_fullEffortCount = 0; + d_conj_count = 0; + d_subs_confirmCount = 0; + d_subs_unkCount = 0; d_uequalityEngine.addFunctionKind( kind::APPLY_UF ); d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR ); diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index ceae3e4c8..2a940f1fd 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -741,17 +741,19 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q Node r = qe->getEqualityQuery()->getRepresentative( d_eqc ); //iterate over all classes except r tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op ); - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ - if( it->first!=r ){ - InstMatch m( q ); - m.add( baseMatch ); - addInstantiations( m, qe, addedLemmas, 0, &(it->second) ); - if( qe->inConflict() ){ - break; + if( tat ){ + for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ + if( it->first!=r ){ + InstMatch m( q ); + m.add( baseMatch ); + addInstantiations( m, qe, addedLemmas, 0, &(it->second) ); + if( qe->inConflict() ){ + break; + } } } + tat = NULL; } - tat = NULL; } } Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl; diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 41c9c40c8..1f68fb787 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -597,6 +597,8 @@ void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& term InstPropagator::InstPropagator( QuantifiersEngine* qe ) : d_qe( qe ), d_notify(*this), d_qy( qe ){ + d_icount = 1; + d_conflict = false; } bool InstPropagator::reset( Theory::Effort e ) { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 9ee62964b..ac6e1edbe 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -406,7 +406,6 @@ Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< No } Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ) { - std::map< Node, Node >::iterator it = visited.find( n ); if( visited.find( n )==visited.end() ){ Node ret = n; if( n.getKind()==FORALL ){ @@ -626,6 +625,7 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategyCbqi( qe ) { d_out = new CegqiOutputInstStrategy( this ); d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); + d_check_vts_lemma_lc = false; } InstStrategyCegqi::~InstStrategyCegqi() throw () { @@ -690,6 +690,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { //check if we need virtual term substitution (if used delta or infinity) bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false ); if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){ + ++(d_quantEngine->d_statistics.d_instantiations_cbqi); //d_added_inst.insert( d_curr_quant ); return true; }else{ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index eab267747..c9f62243f 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -79,7 +79,7 @@ protected: //elimination information (for delayed elimination) class NestedQEInfo { public: - NestedQEInfo(){} + NestedQEInfo() : d_doVts(false){} ~NestedQEInfo(){} Node d_q; std::vector< Node > d_inst_terms; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 49e0a698f..c4bf61b28 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -155,6 +155,7 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe d_regenerate_frequency = 3; d_regenerate = true; }else{ + d_regenerate_frequency = 1; d_regenerate = false; } } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index f46d08f08..afeed1e5d 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -114,6 +114,7 @@ void InstantiationEngine::reset_round( Theory::Effort e ){ } void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ + CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time); if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ double clSet = 0; if( Trace.isOn("inst-engine") ){ diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 582599680..976b81e60 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -33,6 +33,10 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; +QuantifierMacros::QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){ + d_ground_macros = false; +} + bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1; for( unsigned r=0; r<rmax; r++ ){ diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h index 39ec2f0a1..60af7ad0a 100644 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h @@ -60,7 +60,7 @@ private: void addMacro( Node op, Node n, std::vector< Node >& opc ); void debugMacroDefinition( Node oo, Node n ); public: - QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){} + QuantifierMacros( QuantifiersEngine * qe ); ~QuantifierMacros(){} bool simplify( std::vector< Node >& assertions, bool doRewrite = false ); diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 7f560b74c..9c09371c4 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -73,7 +73,6 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ Trace("model-engine") << "---Model Engine Round---" << std::endl; clSet = double(clock())/double(CLOCKS_PER_SEC); } - ++(d_statistics.d_inst_rounds); Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; //let the strong solver verify that the model is minimal @@ -275,7 +274,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } d_triedLemmas += mb->d_triedLemmas; d_addedLemmas += mb->d_addedLemmas; - d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas; + d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->d_addedLemmas; }else{ if( Trace.isOn("fmf-exh-inst-debug") ){ Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; @@ -312,7 +311,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } d_addedLemmas += addedLemmas; d_triedLemmas += triedLemmas; - d_statistics.d_exh_inst_lemmas += addedLemmas; + d_quantEngine->d_statistics.d_instantiations_fmf_exh += addedLemmas; } }else{ Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl; @@ -339,18 +338,3 @@ void ModelEngine::debugPrint( const char* c ){ //d_quantEngine->getModel()->debugPrint( c ); } -ModelEngine::Statistics::Statistics(): - d_inst_rounds("ModelEngine::Inst_Rounds", 0), - d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ), - d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 ) -{ - smtStatisticsRegistry()->registerStat(&d_inst_rounds); - smtStatisticsRegistry()->registerStat(&d_exh_inst_lemmas); - smtStatisticsRegistry()->registerStat(&d_mbqi_inst_lemmas); -} - -ModelEngine::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); - smtStatisticsRegistry()->unregisterStat(&d_exh_inst_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_mbqi_inst_lemmas); -} diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 8575792b4..e89be8d2b 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -61,17 +61,6 @@ public: void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } void debugPrint( const char* c ); -public: - /** statistics class */ - class Statistics { - public: - IntStat d_inst_rounds; - IntStat d_exh_inst_lemmas; - IntStat d_mbqi_inst_lemmas; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; /** Identify this module */ std::string identify() const { return "ModelEngine"; } };/* class ModelEngine */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 522f4dfce..1e484311c 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -108,7 +108,7 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { } Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl; - if( d_mg->isValid() ){ + if( d_mg->isValid() && options::qcfEagerCheckRd() ){ //optimization : record variable argument positions for terms that must be matched std::vector< TNode > vars; //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137) @@ -967,7 +967,11 @@ MatchGen::MatchGen() d_n(), d_type( typ_invalid ), d_type_not() -{} +{ + d_qni_size = 0; + d_child_counter = -1; + d_use_children = true; +} MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) @@ -980,6 +984,10 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) d_type(), d_type_not() { + //initialize temporary + d_child_counter = -1; + d_use_children = true; + Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl; std::vector< Node > qni_apps; d_qni_size = 0; @@ -2024,6 +2032,7 @@ void QuantConflictFind::setIrrelevantFunction( TNode f ) { /** check */ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { + CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time); if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){ Trace("qcf-check") << "QCF : check : " << level << std::endl; if( d_conflict ){ @@ -2098,7 +2107,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { ++addedLemmas; if( e==effort_conflict ){ d_quantEngine->markRelevant( q ); - ++(d_statistics.d_conflict_inst); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); if( options::qcfAllConflict() ){ isConflict = true; }else{ @@ -2107,7 +2116,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { break; }else if( e==effort_prop_eq ){ d_quantEngine->markRelevant( q ); - ++(d_statistics.d_prop_inst); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); } }else{ Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; @@ -2234,20 +2243,14 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo QuantConflictFind::Statistics::Statistics(): d_inst_rounds("QuantConflictFind::Inst_Rounds", 0), - d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ), - d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ), d_entailment_checks("QuantConflictFind::Entailment_Checks",0) { smtStatisticsRegistry()->registerStat(&d_inst_rounds); - smtStatisticsRegistry()->registerStat(&d_conflict_inst); - smtStatisticsRegistry()->registerStat(&d_prop_inst); smtStatisticsRegistry()->registerStat(&d_entailment_checks); } QuantConflictFind::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); - smtStatisticsRegistry()->unregisterStat(&d_conflict_inst); - smtStatisticsRegistry()->unregisterStat(&d_prop_inst); smtStatisticsRegistry()->unregisterStat(&d_entailment_checks); } diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 47a66b1b1..dc8a9acb2 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -260,8 +260,6 @@ public: class Statistics { public: IntStat d_inst_rounds; - IntStat d_conflict_inst; - IntStat d_prop_inst; IntStat d_entailment_checks; Statistics(); ~Statistics(); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 3bf7749a4..de8875ae3 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -20,11 +20,12 @@ #include "theory/quantifiers/trigger.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; + +namespace CVC4 { +namespace theory { +namespace quantifiers { bool QuantifiersRewriter::isClause( Node n ){ if( isLiteral( n ) ){ @@ -1138,12 +1139,13 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ if( containsQuantifiers( n ) ){ if( topLevel && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){ std::vector< Node > children; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node nc = computePrenexAgg( n[i], true ); + Node nc = n.getKind()==NOT ? n[0] : n; + for( unsigned i=0; i<nc.getNumChildren(); i++ ){ + Node ncc = computePrenexAgg( nc[i], true ); if( n.getKind()==NOT ){ - nc = nc.negate(); + ncc = ncc.negate(); } - children.push_back( nc ); + children.push_back( ncc ); } return NodeManager::currentNM()->mkNode( AND, children ); }else if( n.getKind()==NOT ){ @@ -1414,21 +1416,25 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo } Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body ){ - std::map< Node, std::vector< Node > > varLits; - std::map< Node, std::vector< Node > > litVars; - if( body.getKind()==OR ){ + std::map<Node, std::vector<Node> > varLits; + std::map<Node, std::vector<Node> > litVars; + if (body.getKind() == OR) { Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl; - for( size_t i=0; i<body.getNumChildren(); i++ ){ - std::vector< Node > activeArgs; - computeArgVec( args, activeArgs, body[i] ); - for (unsigned j=0; j<activeArgs.size(); j++ ){ - varLits[activeArgs[j]].push_back( body[i] ); - } - litVars[body[i]].insert( litVars[body[i]].begin(), activeArgs.begin(), activeArgs.end() ); + for (size_t i = 0; i < body.getNumChildren(); i++) { + std::vector<Node> activeArgs; + computeArgVec(args, activeArgs, body[i]); + for (unsigned j = 0; j < activeArgs.size(); j++) { + varLits[activeArgs[j]].push_back(body[i]); + } + std::vector<Node>& lit_body_i = litVars[body[i]]; + std::vector<Node>::iterator lit_body_i_begin = lit_body_i.begin(); + std::vector<Node>::const_iterator active_begin = activeArgs.begin(); + std::vector<Node>::const_iterator active_end = activeArgs.end(); + lit_body_i.insert(lit_body_i_begin, active_begin, active_end); } //find the variable in the least number of literals Node bestVar; - for( std::map< Node, std::vector< Node > >::iterator it = varLits.begin(); it != varLits.end(); ++it ){ + for( std::map< Node, std::vector<Node> >::iterator it = varLits.begin(); it != varLits.end(); ++it ){ if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){ bestVar = it->first; } @@ -1438,9 +1444,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg //we can miniscope Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl; //make the bodies - std::vector< Node > qlit1; + std::vector<Node> qlit1; qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() ); - std::vector< Node > qlitt; + std::vector<Node> qlitt; //for all literals not containing bestVar for( size_t i=0; i<body.getNumChildren(); i++ ){ if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){ @@ -1448,9 +1454,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg } } //make the variable lists - std::vector< Node > qvl1; - std::vector< Node > qvl2; - std::vector< Node > qvsh; + std::vector<Node> qvl1; + std::vector<Node> qvl2; + std::vector<Node> qvsh; for( unsigned i=0; i<args.size(); i++ ){ bool found1 = false; bool found2 = false; @@ -1478,8 +1484,8 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg Assert( !qvl1.empty() ); Assert( !qvl2.empty() || !qvsh.empty() ); //check for literals that only contain shared variables - std::vector< Node > qlitsh; - std::vector< Node > qlit2; + std::vector<Node> qlitsh; + std::vector<Node> qlit2; for( size_t i=0; i<qlitt.size(); i++ ){ bool hasVar2 = false; for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){ @@ -1835,3 +1841,6 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { return n; } +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 8bc8e1f04..aae8f6c5b 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -51,7 +51,10 @@ private: //what each literal does class RDomainLit { public: - RDomainLit() : d_merge(false){} + RDomainLit() : d_merge(false){ + d_rd[0] = NULL; + d_rd[1] = NULL; + } ~RDomainLit(){} bool d_merge; RDomain * d_rd[2]; diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index a2a2e99c6..ec1b41a98 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -205,6 +205,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl; } } + d_quantEngine->d_statistics.d_instantiations_rr += addedLemmas; Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl; return addedLemmas; } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index ff11babc9..2c6bfb7d3 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -33,14 +33,14 @@ #include "util/bitvector.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - using namespace CVC4::theory::inst; +namespace CVC4 { +namespace theory { +namespace quantifiers { + TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) { if( argIndex==(int)reps.size() ){ if( d_data.empty() ){ @@ -84,15 +84,25 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { } } -TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_inactive_map( c ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { - d_true = NodeManager::currentNM()->mkConst( true ); - d_false = NodeManager::currentNM()->mkConst( false ); - d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); - d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - if( options::ceGuidedInst() ){ - d_sygus_tdb = new TermDbSygus( c, qe ); - }else{ - d_sygus_tdb = NULL; +TermDb::TermDb(context::Context* c, context::UserContext* u, + QuantifiersEngine* qe) + : d_quantEngine(qe), + d_inactive_map(c), + d_op_id_count(0), + d_typ_id_count(0), + d_sygus_tdb(NULL) { + d_consistent_ee = true; + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_one = NodeManager::currentNM()->mkConst(Rational(1)); + if (options::ceGuidedInst()) { + d_sygus_tdb = new TermDbSygus(c, qe); + } +} +TermDb::~TermDb(){ + if(d_sygus_tdb) { + delete d_sygus_tdb; } } @@ -3298,3 +3308,6 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems } } +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index dd91cde33..d4fdaa5e5 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -188,23 +188,25 @@ private: std::map< Node, std::map< TypeNode, Node > > d_par_op_map; /** whether master equality engine is UF-inconsistent */ bool d_consistent_ee; -public: - TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); - ~TermDb(){} + + public: + TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe); + ~TermDb(); /** boolean terms */ Node d_true; Node d_false; /** constants */ Node d_zero; Node d_one; -public: + + public: /** presolve (called once per user check-sat) */ void presolve(); /** reset (calculate which terms are active) */ bool reset( Theory::Effort effort ); /** identify */ std::string identify() const { return "TermDb"; } -private: + private: /** map from operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; /** map from type nodes to terms of that type */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ec20d1ede..67990ef69 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1133,6 +1133,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } if( d_term_db->isEntailed( q[1], subs, false, true ) ){ Trace("inst-add-debug") << " --> Currently entailed." << std::endl; + ++(d_statistics.d_inst_duplicate_ent); return false; } //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true ); @@ -1512,60 +1513,81 @@ Node QuantifiersEngine::getInstantiatedConjunction( Node q ) { QuantifiersEngine::Statistics::Statistics() : d_time("theory::QuantifiersEngine::time"), + d_qcf_time("theory::QuantifiersEngine::time_qcf"), + d_ematching_time("theory::QuantifiersEngine::time_ematching"), d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), d_instantiations("QuantifiersEngine::Instantiations_Total", 0), d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), + d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0), d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0), - d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0), d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0), d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0), d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0), - d_instantiations_cbqi_arith("QuantifiersEngine::Instantiations_Cbqi_Arith", 0) + d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0), + d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0), + d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0), + d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0), + d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0), + d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0) { smtStatisticsRegistry()->registerStat(&d_time); + smtStatisticsRegistry()->registerStat(&d_qcf_time); + smtStatisticsRegistry()->registerStat(&d_ematching_time); smtStatisticsRegistry()->registerStat(&d_num_quant); smtStatisticsRegistry()->registerStat(&d_instantiation_rounds); smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc); smtStatisticsRegistry()->registerStat(&d_instantiations); smtStatisticsRegistry()->registerStat(&d_inst_duplicate); smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent); smtStatisticsRegistry()->registerStat(&d_triggers); smtStatisticsRegistry()->registerStat(&d_simple_triggers); smtStatisticsRegistry()->registerStat(&d_multi_triggers); smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations); smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv); - smtStatisticsRegistry()->registerStat(&d_red_lte_partial_inst); smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns); smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen); smtStatisticsRegistry()->registerStat(&d_instantiations_guess); - smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi_arith); + smtStatisticsRegistry()->registerStat(&d_instantiations_qcf); + smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop); + smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh); + smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi); + smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi); + smtStatisticsRegistry()->registerStat(&d_instantiations_rr); } QuantifiersEngine::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_time); + smtStatisticsRegistry()->unregisterStat(&d_qcf_time); + smtStatisticsRegistry()->unregisterStat(&d_ematching_time); smtStatisticsRegistry()->unregisterStat(&d_num_quant); smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds); smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc); smtStatisticsRegistry()->unregisterStat(&d_instantiations); smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate); smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent); smtStatisticsRegistry()->unregisterStat(&d_triggers); smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations); smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv); - smtStatisticsRegistry()->unregisterStat(&d_red_lte_partial_inst); smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns); smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen); smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi_arith); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr); } eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 25542e49e..232d1d889 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -388,22 +388,29 @@ public: class Statistics { public: TimerStat d_time; + TimerStat d_qcf_time; + TimerStat d_ematching_time; IntStat d_num_quant; IntStat d_instantiation_rounds; IntStat d_instantiation_rounds_lc; IntStat d_instantiations; IntStat d_inst_duplicate; IntStat d_inst_duplicate_eq; + IntStat d_inst_duplicate_ent; IntStat d_triggers; IntStat d_simple_triggers; IntStat d_multi_triggers; IntStat d_multi_trigger_instantiations; IntStat d_red_alpha_equiv; - IntStat d_red_lte_partial_inst; IntStat d_instantiations_user_patterns; IntStat d_instantiations_auto_gen; IntStat d_instantiations_guess; - IntStat d_instantiations_cbqi_arith; + IntStat d_instantiations_qcf; + IntStat d_instantiations_qcf_prop; + IntStat d_instantiations_fmf_exh; + IntStat d_instantiations_fmf_mbqi; + IntStat d_instantiations_cbqi; + IntStat d_instantiations_rr; Statistics(); ~Statistics(); };/* class QuantifiersEngine::Statistics */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index ec6bb7fcd..6fb90fea3 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -853,6 +853,7 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) //processCard2 begin if(Debug.isOn("sets-card")) { + print_graph(true); for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) { Node n = nm->mkNode(kind::CARD, *it); Debug("sets-card") << "[sets-card] " << n << " = "; @@ -1040,7 +1041,7 @@ Node mkAnd(const std::vector<TNode>& conjunctions) { if (t.getKind() == kind::AND) { for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) { - Assert((*child_it).getKind() != kind::AND); + // Assert((*child_it).getKind() != kind::AND); all.insert(*child_it); } } @@ -1436,7 +1437,11 @@ Node TheorySetsPrivate::explain(TNode literal) Unhandled(); } - return mkAnd(assumptions); + if(assumptions.size()) { + return mkAnd(assumptions); + } else { + return d_trueNode; + } } bool TheorySetsPrivate::lemma(Node n, SetsLemmaTag t) @@ -2333,7 +2338,8 @@ void TheorySetsPrivate::merge_nodes(std::set<TNode> leaves1, std::set<TNode> lea } -void TheorySetsPrivate::print_graph() { +void TheorySetsPrivate::print_graph(bool printmodel) { + NodeManager* nm = NodeManager::currentNM(); std::string tag = "sets-graph"; if(Trace.isOn("sets-graph")) { Trace(tag) << "[sets-graph] Graph : " << std::endl; @@ -2358,13 +2364,38 @@ void TheorySetsPrivate::print_graph() { oss << "digraph G { "; for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) { TNode v = *it; + + std::ostringstream v_oss; + v_oss << v; + if(printmodel) + { + Node n = nm->mkNode(kind::CARD, v); + if((Rewriter::rewrite(n)).isConst()) { + v_oss << " " << (Rewriter::rewrite(n)); + } else { + v_oss << " " << d_external.d_valuation.getModelValue(n); + } + } + if(d_E.find(v) != d_E.end()) { BOOST_FOREACH(TNode w, d_E[v].get()) { + + std::ostringstream w_oss; + w_oss << w; + if(printmodel) { + Node n = nm->mkNode(kind::CARD, w); + if((Rewriter::rewrite(n)).isConst()) { + w_oss << " " << (Rewriter::rewrite(n)); + } else { + w_oss << " " << d_external.d_valuation.getModelValue(n); + } + } + //oss << v.getId() << " -> " << w.getId() << "; "; - oss << "\"" << v << "\" -> \"" << w << "\"; "; + oss << "\"" << v_oss.str() << "\" -> \"" << w_oss.str() << "\"; "; } } else { - oss << "\"" << v << "\";"; + oss << "\"" << v_oss.str() << "\";"; } } oss << "}"; @@ -2468,6 +2499,14 @@ void TheorySetsPrivate::processCard2(Theory::Effort level) { NodeManager* nm = NodeManager::currentNM(); + if(options::setsGuessEmpty() == 0) { + Trace("sets-guess-empty") << "[sets-guess-empty] Generating lemmas before introduce." << std::endl; + guessLeavesEmptyLemmas(); + if(d_newLemmaGenerated) { + return; + } + } + // Introduce for(CDNodeSet::const_iterator it = d_cardTerms.begin(); it != d_cardTerms.end(); ++it) { diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 71a6d9b2d..049e95786 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -280,7 +280,7 @@ private: std::set<TNode> get_leaves(Node vertex1, Node vertex2); std::set<TNode> get_leaves(Node vertex1, Node vertex2, Node vertex3); std::set<TNode> non_empty(std::set<TNode> vertices); - void print_graph(); + void print_graph(bool printmodel=false); context::CDQueue < std::pair<TNode, TNode> > d_graphMergesPending; context::CDList<Node> d_allSetEqualitiesSoFar; Node eqSoFar(); diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 40863b0f2..f2d6bae68 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -153,14 +153,16 @@ public: } while (d_constituentVec.size() < d_index) { - TypeEnumerator *d_newEnumerator = new TypeEnumerator(*d_constituentVec.back()); - ++(*d_newEnumerator); - if( (*d_newEnumerator).isFinished() ) { + TypeEnumerator* newEnumerator = + new TypeEnumerator(*d_constituentVec.back()); + ++(*newEnumerator); + if (newEnumerator->isFinished()) { Trace("set-type-enum") << "operator++ finished!" << std::endl; + delete newEnumerator; d_finished = true; return *this; } - d_constituentVec.push_back(d_newEnumerator); + d_constituentVec.push_back(newEnumerator); } Trace("set-type-enum") << "operator++ returning, **this = " << **this << std::endl; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4526300f8..3ef6df3fc 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -331,6 +331,92 @@ bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& var return true; } +int TheoryStrings::getReduction( int effort, Node n, Node& nr ) { + //determine the effort level to process the extf at + // 0 - at assertion time, 1+ - after no other reduction is applicable + Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() ); + if( d_extf_info_tmp[n].d_model_active ){ + int r_effort = -1; + int pol = d_extf_info_tmp[n].d_pol; + if( n.getKind()==kind::STRING_STRCTN ){ + if( pol==1 ){ + r_effort = 1; + }else if( pol==-1 ){ + if( effort==2 ){ + Node x = n[0]; + Node s = n[1]; + std::vector< Node > lexp; + Node lenx = getLength( x, lexp ); + Node lens = getLength( s, lexp ); + if( areEqual( lenx, lens ) ){ + Trace("strings-extf-debug") << " resolve extf : " << n << " based on equal lengths disequality." << std::endl; + //we can reduce to disequality when lengths are equal + if( !areDisequal( x, s ) ){ + lexp.push_back( lenx.eqNode(lens) ); + lexp.push_back( n.negate() ); + Node xneqs = x.eqNode(s).negate(); + sendInference( lexp, xneqs, "NEG-CTN-EQL", true ); + } + return 1; + }else if( !areDisequal( lenx, lens ) ){ + //split on their lenths + sendSplit( lenx, lens, "NEG-CTN-SP" ); + }else{ + r_effort = 2; + } + } + } + }else{ + if( options::stringLazyPreproc() ){ + if( n.getKind()==kind::STRING_SUBSTR ){ + r_effort = 1; + }else if( n.getKind()!=kind::STRING_IN_REGEXP ){ + r_effort = 2; + } + } + } + if( effort==r_effort ){ + Node c_n = pol==-1 ? n.negate() : n; + if( d_preproc_cache.find( c_n )==d_preproc_cache.end() ){ + d_preproc_cache[ c_n ] = true; + Trace("strings-process-debug") << "Process reduction for " << n << ", pol = " << pol << std::endl; + if( n.getKind()==kind::STRING_STRCTN && pol==1 ){ + Node x = n[0]; + Node s = n[1]; + //positive contains reduces to a equality + Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" ); + Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" ); + Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) ); + std::vector< Node > exp_vec; + exp_vec.push_back( n ); + sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true ); + //we've reduced this n + Trace("strings-extf-debug") << " resolve extf : " << n << " based on positive contain reduction." << std::endl; + return 1; + }else{ + // for STRING_SUBSTR, STRING_STRCTN with pol=-1, + // STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL + std::vector< Node > new_nodes; + Node res = d_preproc.simplify( n, new_nodes ); + Assert( res!=n ); + new_nodes.push_back( NodeManager::currentNM()->mkNode( res.getType().isBoolean() ? kind::IFF : kind::EQUAL, res, n ) ); + Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); + nnlem = Rewriter::rewrite( nnlem ); + Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl; + Trace("strings-red-lemma") << "...from " << n << std::endl; + sendInference( d_empty_vec, nnlem, "Reduction", true ); + //we've reduced this n + Trace("strings-extf-debug") << " resolve extf : " << n << " based on reduction." << std::endl; + return 1; + } + }else{ + return 1; + } + } + } + return 0; +} + ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS ///////////////////////////////////////////////////////////////////////////// @@ -404,15 +490,13 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { for( unsigned j=0; j<col[i].size(); j++ ) { Trace("strings-model") << col[i][j] << " "; //check if col[i][j] has only variables - EqcInfo* ei = getOrMakeEqcInfo( col[i][j], false ); - Node cst = ei ? ei->d_const_term : Node::null(); - if( cst.isNull() ){ + if( !col[i][j].isConst() ){ Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() ); if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){ pure_eq.push_back( col[i][j] ); } }else{ - processed[col[i][j]] = cst; + processed[col[i][j]] = col[i][j]; } } Trace("strings-model") << "have length " << lts_values[i] << std::endl; @@ -692,104 +776,29 @@ bool TheoryStrings::needsCheckLastEffort() { } void TheoryStrings::checkExtfReductions( int effort ) { + //standardize this? + //std::vector< Node > nred; + //d_extt->doReductions( effort, nred, false ); + std::vector< Node > extf; d_extt->getActive( extf ); + Trace("strings-process") << "checking " << extf.size() << " active extf" << std::endl; for( unsigned i=0; i<extf.size(); i++ ){ Node n = extf[i]; - if( d_extf_info_tmp[n].d_model_active ){ - Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() ); - if( checkExtfReduction( n, d_extf_info_tmp[n].d_pol, effort ) ){ - d_extt->markReduced( n ); - } - if( hasProcessed() ){ + Trace("strings-process") << "Check " << n << ", active in model=" << d_extf_info_tmp[n].d_model_active << std::endl; + Node nr; + int ret = getReduction( effort, n, nr ); + Assert( nr.isNull() ); + if( ret!=0 ){ + d_extt->markReduced( extf[i] ); + if( options::stringOpt1() && hasProcessed() ){ return; } } } } -bool TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) { - //determine the effort level to process the extf at - // 0 - at assertion time, 1+ - after no other reduction is applicable - int r_effort = -1; - if( atom.getKind()==kind::STRING_STRCTN ){ - if( pol==1 ){ - r_effort = 1; - }else{ - Assert( pol==-1 ); - if( effort==2 ){ - Node x = atom[0]; - Node s = atom[1]; - std::vector< Node > lexp; - Node lenx = getLength( x, lexp ); - Node lens = getLength( s, lexp ); - if( areEqual( lenx, lens ) ){ - Trace("strings-extf-debug") << " resolve extf : " << atom << " based on equal lengths disequality." << std::endl; - //we can reduce to disequality when lengths are equal - if( !areDisequal( x, s ) ){ - lexp.push_back( lenx.eqNode(lens) ); - lexp.push_back( atom.negate() ); - Node xneqs = x.eqNode(s).negate(); - sendInference( lexp, xneqs, "NEG-CTN-EQL", true ); - } - return true; - }else if( !areDisequal( lenx, lens ) ){ - //split on their lenths - sendSplit( lenx, lens, "NEG-CTN-SP" ); - }else{ - r_effort = 2; - } - } - } - }else{ - if( options::stringLazyPreproc() ){ - if( atom.getKind()==kind::STRING_SUBSTR ){ - r_effort = 1; - }else if( atom.getKind()!=kind::STRING_IN_REGEXP ){ - r_effort = 2; - } - } - } - if( effort==r_effort ){ - Node c_atom = pol==-1 ? atom.negate() : atom; - if( d_preproc_cache.find( c_atom )==d_preproc_cache.end() ){ - d_preproc_cache[ c_atom ] = true; - Trace("strings-process-debug") << "Process reduction for " << atom << ", pol = " << pol << std::endl; - if( atom.getKind()==kind::STRING_STRCTN && pol==1 ){ - Node x = atom[0]; - Node s = atom[1]; - //positive contains reduces to a equality - Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" ); - Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" ); - Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) ); - std::vector< Node > exp_vec; - exp_vec.push_back( atom ); - sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true ); - //we've reduced this atom - Trace("strings-extf-debug") << " resolve extf : " << atom << " based on positive contain reduction." << std::endl; - return true; - }else{ - // for STRING_SUBSTR, STRING_STRCTN with pol=-1, - // STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL - std::vector< Node > new_nodes; - Node res = d_preproc.simplify( atom, new_nodes ); - Assert( res!=atom ); - new_nodes.push_back( NodeManager::currentNM()->mkNode( res.getType().isBoolean() ? kind::IFF : kind::EQUAL, res, atom ) ); - Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); - nnlem = Rewriter::rewrite( nnlem ); - Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl; - Trace("strings-red-lemma") << "...from " << atom << std::endl; - sendInference( d_empty_vec, nnlem, "Reduction", true ); - //we've reduced this atom - Trace("strings-extf-debug") << " resolve extf : " << atom << " based on reduction." << std::endl; - return true; - } - } - } - return false; -} - -TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) { +TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) { } @@ -827,10 +836,6 @@ void TheoryStrings::conflict(TNode a, TNode b){ /** called when a new equivalance class is created */ void TheoryStrings::eqNotifyNewClass(TNode t){ - if( t.getKind() == kind::CONST_STRING ){ - EqcInfo * ei =getOrMakeEqcInfo( t, true ); - ei->d_const_term = t; - } if( t.getKind() == kind::STRING_LENGTH ){ Trace("strings-debug") << "New length eqc : " << t << std::endl; Node r = d_equalityEngine.getRepresentative(t[0]); @@ -838,6 +843,8 @@ void TheoryStrings::eqNotifyNewClass(TNode t){ ei->d_length_term = t[0]; //we care about the length of this string registerTerm( t[0], 1 ); + }else{ + //d_extt->registerTerm( t ); } } @@ -847,9 +854,6 @@ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){ if( e2 ){ EqcInfo * e1 = getOrMakeEqcInfo( t1 ); //add information from e2 to e1 - if( !e2->d_const_term.get().isNull() ){ - e1->d_const_term.set( e2->d_const_term ); - } if( !e2->d_length_term.get().isNull() ){ e1->d_length_term.set( e2->d_length_term ); } @@ -987,7 +991,6 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { d_equalityEngine.assertPredicate( atom, polarity, exp ); //process extf if( atom.getKind()==kind::STRING_IN_REGEXP ){ - d_extt->registerTerm( atom ); if( polarity && atom[1].getKind()==kind::REGEXP_RANGE ){ if( d_extf_infer_cache_u.find( atom )==d_extf_infer_cache_u.end() ){ d_extf_infer_cache_u.insert( atom ); @@ -999,6 +1002,8 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { } } } + //register the atom here, since it may not create a new equivalence class + //d_extt->registerTerm( atom ); } Trace("strings-pending-debug") << " Now collect terms" << std::endl; //collect extended function terms in the atom @@ -1292,7 +1297,8 @@ void TheoryStrings::checkExtfEval( int effort ) { std::vector< Node > terms; std::vector< Node > sterms; std::vector< std::vector< Node > > exp; - d_extt->getInferences( effort, terms, sterms, exp ); + d_extt->getActive( terms ); + d_extt->getSubstitutedTerms( effort, terms, sterms, exp ); for( unsigned i=0; i<terms.size(); i++ ){ Node n = terms[i]; Node sn = sterms[i]; @@ -2954,7 +2960,7 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { } }else{ Node sk = mkSkolemCached( nconst_k, firstChar, sk_id_dc_spt, "dc_spt", 2 ); - Node skr = mkSkolemCached( nconst_k, firstChar, sk_id_dc_spt_rem, "dc_spt_rem", -1 ); + Node skr = mkSkolemCached( nconst_k, firstChar, sk_id_dc_spt_rem, "dc_spt_rem" ); Node eq1 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, skr ) ); eq1 = Rewriter::rewrite( eq1 ); Node eq2 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, skr ) ); @@ -3875,16 +3881,6 @@ Node TheoryStrings::ppRewrite(TNode atom) { return atom; } -void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) { - if( visited.find( n )==visited.end() ){ - visited[n] = true; - d_extt->registerTerm( n ); - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - collectExtendedFuncTerms( n[i], visited ); - } - } -} - // Stats TheoryStrings::Statistics::Statistics(): d_splits("TheoryStrings::NumOfSplitOnDemands", 0), @@ -4867,6 +4863,16 @@ Node TheoryStrings::getNormalSymRegExp(Node r, std::vector<Node> &nf_exp) { return ret; } +void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) { + if( visited.find( n )==visited.end() ){ + visited[n] = true; + d_extt->registerTerm( n ); + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + collectExtendedFuncTerms( n[i], visited ); + } + } +} + }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index fe72bd8e7..fd984bd58 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -72,6 +72,7 @@ public: Node explain( TNode literal ); eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; } bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); + int getReduction( int effort, Node n, Node& nr ); // NotifyClass for equality engine class NotifyClass : public eq::EqualityEngineNotify { @@ -237,7 +238,6 @@ private: EqcInfo( context::Context* c ); ~EqcInfo(){} //constant in this eqc - context::CDO< Node > d_const_term; context::CDO< Node > d_length_term; context::CDO< unsigned > d_cardinality_lem_k; // 1 = added length lemma @@ -274,8 +274,6 @@ private: int d_pol; //explanation std::vector< Node > d_exp; - //reps -> list of variables - //std::map< Node, std::vector< Node > > d_rep_vars; //false if it is reduced in the model bool d_model_active; }; @@ -321,7 +319,6 @@ private: Node getSymbolicDefinition( Node n, std::vector< Node >& exp ); //check extf reduction void checkExtfReductions( int effort ); - bool checkExtfReduction( Node atom, int pol, int effort ); //flat forms check void checkFlatForms(); Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ); @@ -523,6 +520,7 @@ public: ~Statistics(); };/* class TheoryStrings::Statistics */ Statistics d_statistics; + };/* class TheoryStrings */ }/* CVC4::theory::strings namespace */ diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 92b18eed0..2ee367cfc 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -741,6 +741,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i return ( s2 == r[0].getConst<String>() ); } else { Assert( false, "RegExp contains variables" ); + return false; } } case kind::REGEXP_CONCAT: { diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 7fa74df6a..9e71a1ddf 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -314,15 +314,18 @@ EntailmentCheckSideEffects::~EntailmentCheckSideEffects() { ExtTheory::ExtTheory( Theory * p ) : d_parent( p ), -d_ext_func_terms( p->getSatContext() ), d_has_extf( p->getSatContext() ){ - +d_ext_func_terms( p->getSatContext() ), d_ci_inactive( p->getUserContext() ), +d_lemmas( p->getUserContext() ), d_pp_lemmas( p->getUserContext() ), d_has_extf( p->getSatContext() ){ + d_true = NodeManager::currentNM()->mkConst( true ); } +//gets all leaf terms in n void ExtTheory::collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) { if( !n.isConst() ){ if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getNumChildren()>0 ){ + //treat terms not belonging to this theory as leaf + if( n.getNumChildren()>0 ){//&& Theory::theoryOf(n)==d_parent->getId() ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ collectVars( n[i], vars, visited ); } @@ -334,17 +337,17 @@ void ExtTheory::collectVars( Node n, std::vector< Node >& vars, std::map< Node, } //do inferences -void ExtTheory::getInferences( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ) { - //all variables we need to find a substitution for - std::vector< Node > vars; - std::vector< Node > sub; - std::map< Node, std::vector< Node > > expc; - Trace("extt-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl; - for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ - //if not already reduced - if( (*it).second ){ - Node n = (*it).first; - terms.push_back( n ); +void ExtTheory::getSubstitutedTerms( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ) { + Trace("extt-debug") << "Currently " << d_ext_func_terms.size() << " extended functions." << std::endl; + Trace("extt-debug") << "..." << terms.size() << " to reduce." << std::endl; + if( !terms.empty() ){ + //all variables we need to find a substitution for + std::vector< Node > vars; + std::vector< Node > sub; + std::map< Node, std::vector< Node > > expc; + for( unsigned i=0; i<terms.size(); i++ ){ + //do substitution, rewrite + Node n = terms[i]; std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); Assert( iti!=d_extf_info.end() ); for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){ @@ -353,13 +356,11 @@ void ExtTheory::getInferences( int effort, std::vector< Node >& terms, std::vect } } } - } - Trace("extt-debug") << "..." << terms.size() << " unreduced." << std::endl; - if( !terms.empty() ){ - //get the current substitution + //get the current substitution for all variables if( d_parent->getCurrentSubstitution( effort, vars, sub, expc ) ){ + Assert( vars.size()==sub.size() ); for( unsigned i=0; i<terms.size(); i++ ){ - //do substitution, rewrite + //do substitution Node n = terms[i]; Node ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() ); std::vector< Node > expn; @@ -392,13 +393,134 @@ void ExtTheory::getInferences( int effort, std::vector< Node >& terms, std::vect } } +bool ExtTheory::doInferencesInternal( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch, bool isRed ) { + if( batch ){ + bool addedLemma = false; + if( isRed ){ + for( unsigned i=0; i<terms.size(); i++ ){ + Node n = terms[i]; + Node nr; + //TODO: reduction with substitution? + int ret = d_parent->getReduction( effort, n, nr ); + if( ret==0 ){ + nred.push_back( n ); + }else{ + if( !nr.isNull() && n!=nr ){ + Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? kind::IFF : kind::EQUAL, n, nr ); + if( sendLemma( lem, true ) ){ + Trace("extt-lemma") << "ExtTheory : Reduction lemma : " << lem << std::endl; + addedLemma = true; + } + } + markReduced( terms[i], ret<0 ); + } + } + }else{ + std::vector< Node > sterms; + std::vector< std::vector< Node > > exp; + getSubstitutedTerms( effort, terms, sterms, exp ); + for( unsigned i=0; i<terms.size(); i++ ){ + bool processed = false; + if( sterms[i]!=terms[i] ){ + Node sr = Rewriter::rewrite( sterms[i] ); + if( sr.isConst() ){ + processed = true; + markReduced( terms[i] ); + Node eq = terms[i].eqNode( sr ); + Node expn = exp[i].size()>1 ? NodeManager::currentNM()->mkNode( kind::AND, exp[i] ) : ( exp[i].size()==1 ? exp[i][0] : d_true ); + Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq << " by " << expn << std::endl; + Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, expn, eq ); + Trace("extt-debug") << "...send lemma " << lem << std::endl; + if( sendLemma( lem ) ){ + Trace("extt-lemma") << "ExtTheory : Constant rewrite lemma : " << lem << std::endl; + addedLemma = true; + } + } + } + if( !processed ){ + nred.push_back( terms[i] ); + } + } + } + return addedLemma; + }else{ + std::vector< Node > nnred; + if( terms.empty() ){ + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + if( (*it).second && !isContextIndependentInactive( (*it).first ) ){ + std::vector< Node > nterms; + nterms.push_back( (*it).first ); + if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){ + return true; + } + } + } + }else{ + for( unsigned i=0; i<terms.size(); i++ ){ + std::vector< Node > nterms; + nterms.push_back( terms[i] ); + if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){ + return true; + } + } + } + return false; + } +} + +bool ExtTheory::sendLemma( Node lem, bool preprocess ) { + if( preprocess ){ + if( d_pp_lemmas.find( lem )==d_pp_lemmas.end() ){ + d_pp_lemmas.insert( lem ); + d_parent->getOutputChannel().lemma( lem, false, true ); + return true; + } + }else{ + if( d_lemmas.find( lem )==d_lemmas.end() ){ + d_lemmas.insert( lem ); + d_parent->getOutputChannel().lemma( lem ); + return true; + } + } + return false; +} + +bool ExtTheory::doInferences( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch ) { + if( !terms.empty() ){ + return doInferencesInternal( effort, terms, nred, batch, false ); + }else{ + return false; + } +} + +bool ExtTheory::doInferences( int effort, std::vector< Node >& nred, bool batch ) { + std::vector< Node > terms; + getActive( terms ); + return doInferencesInternal( effort, terms, nred, batch, false ); +} + +bool ExtTheory::doReductions( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch ) { + if( !terms.empty() ){ + return doInferencesInternal( effort, terms, nred, batch, true ); + }else{ + return false; + } +} + +bool ExtTheory::doReductions( int effort, std::vector< Node >& nred, bool batch ) { + std::vector< Node > terms; + getActive( terms ); + return doInferencesInternal( effort, terms, nred, batch, true ); +} + + //register term void ExtTheory::registerTerm( Node n ) { if( d_extf_kind.find( n.getKind() )!=d_extf_kind.end() ){ if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){ Trace("extt-debug") << "Found extended function : " << n << " in " << d_parent->getId() << std::endl; d_ext_func_terms[n] = true; - d_has_extf = true; + d_has_extf = n; std::map< Node, bool > visited; collectVars( n, d_extf_info[n].d_vars, visited ); } @@ -406,9 +528,22 @@ void ExtTheory::registerTerm( Node n ) { } //mark reduced -void ExtTheory::markReduced( Node n ) { +void ExtTheory::markReduced( Node n, bool contextDepend ) { d_ext_func_terms[n] = false; - //TODO update has_extf + if( !contextDepend ){ + d_ci_inactive.insert( n ); + } + + //update has_extf + if( d_has_extf.get()==n ){ + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + //if not already reduced + if( (*it).second && !isContextIndependentInactive( (*it).first ) ){ + d_has_extf = (*it).first; + } + } + + } } //mark congruent @@ -424,11 +559,19 @@ void ExtTheory::markCongruent( Node a, Node b ) { } } +bool ExtTheory::isContextIndependentInactive( Node n ) { + return d_ci_inactive.find( n )!=d_ci_inactive.end(); +} + +bool ExtTheory::hasActiveTerm() { + return !d_has_extf.get().isNull(); +} + //is active bool ExtTheory::isActive( Node n ) { NodeBoolMap::const_iterator it = d_ext_func_terms.find( n ); if( it!=d_ext_func_terms.end() ){ - return (*it).second; + return (*it).second && !isContextIndependentInactive( n ); }else{ return false; } @@ -437,7 +580,7 @@ bool ExtTheory::isActive( Node n ) { void ExtTheory::getActive( std::vector< Node >& active ) { for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ //if not already reduced - if( (*it).second ){ + if( (*it).second && !isContextIndependentInactive( (*it).first ) ){ active.push_back( (*it).first ); } } @@ -446,7 +589,7 @@ void ExtTheory::getActive( std::vector< Node >& active ) { void ExtTheory::getActive( std::vector< Node >& active, Kind k ) { for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ //if not already reduced - if( (*it).second && (*it).first.getKind()==k ){ + if( (*it).first.getKind()==k && (*it).second && !isContextIndependentInactive( (*it).first ) ){ active.push_back( (*it).first ); } } diff --git a/src/theory/theory.h b/src/theory/theory.h index 08505be66..5d64c6446 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -24,6 +24,7 @@ #include <string> #include "context/cdlist.h" +#include "context/cdhashset.h" #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" @@ -891,8 +892,11 @@ public: */ virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); - /* equality engine */ + /* equality engine TODO: use? */ virtual eq::EqualityEngine * getEqualityEngine() { return NULL; } + + /* get extended theory */ + virtual ExtTheory * getExtTheory() { return d_extt; } /* get current substitution at an effort * input : vars @@ -900,6 +904,13 @@ public: * where ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i */ virtual bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { return false; } + + /* get reduction for node + if return value is not 0, then n is reduced. + if return value <0 then n is reduced SAT-context-independently (e.g. by a lemma that persists at this user-context level). + if nr is non-null, then ( n = nr ) should be added as a lemma by caller, and return value should be <0. + */ + virtual int getReduction( int effort, Node n, Node& nr ) { return 0; } /** * Turn on proof-production mode. @@ -974,15 +985,23 @@ public: class ExtTheory { friend class Theory; typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; + typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; protected: Theory * d_parent; + Node d_true; //extended string terms, map to whether they are active NodeBoolMap d_ext_func_terms; - //any non-reduced extended functions exist - context::CDO< bool > d_has_extf; + //set of terms from d_ext_func_terms that are SAT-context-independently inactive + // (e.g. term t when a reduction lemma of the form t = t' was added) + NodeSet d_ci_inactive; + //cache of all lemmas sent + NodeSet d_lemmas; + NodeSet d_pp_lemmas; + //watched term for checking if any non-reduced extended functions exist + context::CDO< Node > d_has_extf; //extf kind std::map< Kind, bool > d_extf_kind; - //information for extf + //information for each term in d_ext_func_terms class ExtfInfo { public: //all variables in this term @@ -991,25 +1010,49 @@ protected: std::map< Node, ExtfInfo > d_extf_info; //collect variables void collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ); + // is context dependent inactive + bool isContextIndependentInactive( Node n ); + //do inferences internal + bool doInferencesInternal( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch, bool isRed ); + //send lemma + bool sendLemma( Node lem, bool preprocess = false ); public: ExtTheory( Theory * p ); virtual ~ExtTheory(){} //add extf kind void addFunctionKind( Kind k ) { d_extf_kind[k] = true; } - //do inferences - // input : effort - // output : terms, sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i - void getInferences( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ); //register term + // adds n to d_ext_func_terms if addFunctionKind( n.getKind() ) was called void registerTerm( Node n ); - //mark reduced - void markReduced( Node n ); - //mark congruent + // set n as reduced/inactive + // if contextDepend = false, then n remains inactive in the duration of this user-context level + void markReduced( Node n, bool contextDepend = true ); + // mark that a and b are congruent terms: set b inactive, set a to inactive if b was inactive void markCongruent( Node a, Node b ); - //is active + + //getSubstitutedTerms + // input : effort, terms + // output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i + void getSubstitutedTerms( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ); + //doInferences + // * input : effort, terms, batch (whether to send one lemma or lemmas for all terms) + // * sends rewriting lemmas of the form ( exp => t = c ) where t is in terms and c is a constant, c = rewrite( t*sigma ) where exp |= sigma + // * output : nred (the terms that are still active) + // * return : true iff lemma is sent + bool doInferences( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch=true ); + bool doInferences( int effort, std::vector< Node >& nred, bool batch=true ); + //doReductions + // same as doInferences, but will send reduction lemmas of the form ( t = t' ) where t is in terms, t' is equivalent, reduced term + bool doReductions( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch=true ); + bool doReductions( int effort, std::vector< Node >& nred, bool batch=true ); + + //has active term + bool hasActiveTerm(); + //is n active bool isActive( Node n ); - //get active + //get the set of active terms from d_ext_func_terms void getActive( std::vector< Node >& active ); + //get the set of active terms from d_ext_func_terms of kind k void getActive( std::vector< Node >& active, Kind k ); }; diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index cda94e1c4..4713c7dcf 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1645,34 +1645,37 @@ Node SortModel::getCardinalityLiteral( int c ) { StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, - OutputChannel& out, - TheoryUF* th) - : d_out( &out ) - , d_th( th ) - , d_conflict( c, false ) - , d_rep_model() - , d_aloc_com_card( u, 0 ) - , d_com_card_assertions( c ) - , d_min_pos_com_card( c, -1 ) - , d_card_assertions_eqv_lemma( u ) - , d_min_pos_tn_master_card( c, -1 ) - , d_rel_eqc( c ) -{ - if( options::ufssDiseqPropagation() ){ - d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this ); - }else{ - d_deq_prop = NULL; + OutputChannel& out, TheoryUF* th) + : d_out(&out), + d_th(th), + d_conflict(c, false), + d_rep_model(), + d_aloc_com_card(u, 0), + d_com_card_assertions(c), + d_min_pos_com_card(c, -1), + d_card_assertions_eqv_lemma(u), + d_min_pos_tn_master_card(c, -1), + d_rel_eqc(c), + d_deq_prop(NULL), + d_sym_break(NULL) { + if (options::ufssDiseqPropagation()) { + d_deq_prop = new DisequalityPropagator(th->getQuantifiersEngine(), this); + } + if (options::ufssSymBreak()) { + d_sym_break = new SubsortSymmetryBreaker(th->getQuantifiersEngine(), c); + } +} + +StrongSolverTheoryUF::~StrongSolverTheoryUF() { + for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin(); + it != d_rep_model.end(); ++it) { + delete it->second; } - if( options::ufssSymBreak() ){ - d_sym_break = new SubsortSymmetryBreaker( th->getQuantifiersEngine(), c ); - }else{ - d_sym_break = NULL; + if (d_sym_break) { + delete d_sym_break; } -} - -StrongSolverTheoryUF::~StrongSolverTheoryUF() { - for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ - delete it->second; + if (d_deq_prop) { + delete d_deq_prop; } } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 4e4dbef83..40026522d 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -365,55 +365,10 @@ public: /** get number of regions (for debugging) */ int getNumRegions(); }; /** class SortModel */ -private: - /** The output channel for the strong solver. */ - OutputChannel* d_out; - /** theory uf pointer */ - TheoryUF* d_th; - /** Are we in conflict */ - context::CDO<bool> d_conflict; - /** rep model structure, one for each type */ - std::map< TypeNode, SortModel* > d_rep_model; - /** get sort model */ - SortModel* getSortModel( Node n ); -private: - /** allocated combined cardinality */ - context::CDO< int > d_aloc_com_card; - /** combined cardinality constraints */ - std::map< int, Node > d_com_card_literal; - /** combined cardinality assertions (indexed by cardinality literals ) */ - NodeBoolMap d_com_card_assertions; - /** minimum positive combined cardinality */ - context::CDO< int > d_min_pos_com_card; - /** cardinality literals for which we have added */ - NodeBoolMap d_card_assertions_eqv_lemma; - /** the master monotone type (if ufssFairnessMonotone enabled) */ - TypeNode d_tn_mono_master; - std::map< TypeNode, bool > d_tn_mono_slave; - context::CDO< int > d_min_pos_tn_master_card; - /** initialize */ - void initializeCombinedCardinality(); - /** allocateCombinedCardinality */ - void allocateCombinedCardinality(); - /** check */ - void checkCombinedCardinality(); -private: - /** relevant eqc */ - NodeBoolMap d_rel_eqc; - /** ensure eqc */ - void ensureEqc( SortModel* c, Node a ); - /** ensure eqc for all subterms of n */ - void ensureEqcRec( Node n ); -public: - /** has eqc */ - bool hasEqc( Node a ); -private: - /** disequality propagator */ - DisequalityPropagator* d_deq_prop; - /** symmetry breaking techniques */ - SubsortSymmetryBreaker* d_sym_break; + public: - StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th); + StrongSolverTheoryUF(context::Context* c, context::UserContext* u, + OutputChannel& out, TheoryUF* th); ~StrongSolverTheoryUF(); /** get theory */ TheoryUF* getTheory() { return d_th; } @@ -437,7 +392,6 @@ public: void assertNode( Node n, bool isDecision ); /** are disequal */ bool areDisequal( Node a, Node b ); -public: /** check */ void check( Theory::Effort level ); /** presolve */ @@ -448,18 +402,14 @@ public: Node getNextDecisionRequest(); /** preregister a term */ void preRegisterTerm( TNode n ); - /** preregister a quantifier */ - //void registerQuantifier( Node f ); /** notify restart */ void notifyRestart(); -public: /** identify */ std::string identify() const { return std::string("StrongSolverTheoryUF"); } //print debug void debugPrint( const char* c ); /** debug a model */ bool debugModel( TheoryModel* m ); -public: /** get is in conflict */ bool isConflict() { return d_conflict; } /** get cardinality for node */ @@ -468,9 +418,11 @@ public: int getCardinality( TypeNode tn ); /** minimize */ bool minimize( TheoryModel* m = NULL ); + /** has eqc */ + bool hasEqc(Node a); class Statistics { - public: + public: IntStat d_clique_conflicts; IntStat d_clique_lemmas; IntStat d_split_lemmas; @@ -483,7 +435,50 @@ public: }; /** statistics class */ Statistics d_statistics; -};/* class StrongSolverTheoryUF */ + + private: + /** get sort model */ + SortModel* getSortModel(Node n); + /** initialize */ + void initializeCombinedCardinality(); + /** allocateCombinedCardinality */ + void allocateCombinedCardinality(); + /** check */ + void checkCombinedCardinality(); + /** ensure eqc */ + void ensureEqc(SortModel* c, Node a); + /** ensure eqc for all subterms of n */ + void ensureEqcRec(Node n); + + /** The output channel for the strong solver. */ + OutputChannel* d_out; + /** theory uf pointer */ + TheoryUF* d_th; + /** Are we in conflict */ + context::CDO<bool> d_conflict; + /** rep model structure, one for each type */ + std::map<TypeNode, SortModel*> d_rep_model; + /** allocated combined cardinality */ + context::CDO<int> d_aloc_com_card; + /** combined cardinality constraints */ + std::map<int, Node> d_com_card_literal; + /** combined cardinality assertions (indexed by cardinality literals ) */ + NodeBoolMap d_com_card_assertions; + /** minimum positive combined cardinality */ + context::CDO<int> d_min_pos_com_card; + /** cardinality literals for which we have added */ + NodeBoolMap d_card_assertions_eqv_lemma; + /** the master monotone type (if ufssFairnessMonotone enabled) */ + TypeNode d_tn_mono_master; + std::map<TypeNode, bool> d_tn_mono_slave; + context::CDO<int> d_min_pos_tn_master_card; + /** relevant eqc */ + NodeBoolMap d_rel_eqc; + /** disequality propagator */ + DisequalityPropagator* d_deq_prop; + /** symmetry breaking techniques */ + SubsortSymmetryBreaker* d_sym_break; +}; /* class StrongSolverTheoryUF */ class DisequalityPropagator { public: diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 393a7c559..d13cc1f03 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -563,39 +563,56 @@ void UnconstrainedSimplifier::processUnconstrained() } break; - // Bit-vector comparisons: replace with new Boolean variable, but have to also conjoin with a side condition - // as there is always one case when the comparison is forced to be false + // Bit-vector comparisons: replace with new Boolean variable, but have + // to also conjoin with a side condition as there is always one case + // when the comparison is forced to be false case kind::BITVECTOR_ULT: - strict = true; case kind::BITVECTOR_UGE: - goto bvineq; - case kind::BITVECTOR_UGT: - strict = true; case kind::BITVECTOR_ULE: - swap = true; - goto bvineq; - case kind::BITVECTOR_SLT: - strict = true; case kind::BITVECTOR_SGE: - isSigned = true; - goto bvineq; - case kind::BITVECTOR_SGT: - strict = true; - case kind::BITVECTOR_SLE: - isSigned = true; - swap = true; - - bvineq: { + case kind::BITVECTOR_SLE: { + // Tuples over (signed, swap, strict). + switch (parent.getKind()) { + case kind::BITVECTOR_UGE: + break; + case kind::BITVECTOR_ULT: + strict = true; + break; + case kind::BITVECTOR_ULE: + swap = true; + break; + case kind::BITVECTOR_UGT: + swap = true; + strict = true; + break; + case kind::BITVECTOR_SGE: + isSigned = true; + break; + case kind::BITVECTOR_SLT: + isSigned = true; + strict = true; + break; + case kind::BITVECTOR_SLE: + isSigned = true; + swap = true; + break; + case kind::BITVECTOR_SGT: + isSigned = true; + swap = true; + strict = true; + break; + default: + Unreachable(); + } TNode other; bool left = false; if (parent[0] == current) { other = parent[1]; left = true; - } - else { + } else { Assert(parent[1] == current); other = parent[0]; } @@ -608,14 +625,14 @@ void UnconstrainedSimplifier::processUnconstrained() } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; - } - else { + } else { currentSub = Node(); } - } - else { + } else { unsigned size = current.getType().getBitVectorSize(); - BitVector bv = isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) : BitVector(size, unsigned(0)); + BitVector bv = + isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) + : BitVector(size, unsigned(0)); if (swap == left) { bv = ~bv; } @@ -625,14 +642,14 @@ void UnconstrainedSimplifier::processUnconstrained() currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; NodeManager* nm = NodeManager::currentNM(); - Node test = Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv))); + Node test = + Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv))); if (test == nm->mkConst<bool>(false)) { break; } if (strict) { currentSub = currentSub.andNode(test.notNode()); - } - else { + } else { currentSub = currentSub.orNode(test); } // Delay adding this substitution - see comment at end of function diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index efb90302f..a34689d1e 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -17,9 +17,9 @@ ** this being implemented on SExpr and not on the Printer class is that the ** Printer class lives in libcvc4. It has to currently as it prints fairly ** complicated objects, like Model, which in turn uses SmtEngine pointers. - ** However, SExprs need to be printed by Statistics. To get the output consistent - ** with the previous version, the printing of SExprs in different languages is - ** handled in the SExpr class and the libexpr library. + ** However, SExprs need to be printed by Statistics. To get the output + ** consistent with the previous version, the printing of SExprs in different + ** languages is handled in the SExpr class and the libexpr library. **/ #include "util/sexpr.h" @@ -41,9 +41,8 @@ std::ostream& operator<<(std::ostream& out, PrettySExprs ps) { return out; } - SExpr::~SExpr() { - if(d_children != NULL){ + if (d_children != NULL) { delete d_children; d_children = NULL; } @@ -56,98 +55,88 @@ SExpr& SExpr::operator=(const SExpr& other) { d_rationalValue = other.d_rationalValue; d_stringValue = other.d_stringValue; - if(d_children == NULL && other.d_children == NULL){ + if (d_children == NULL && other.d_children == NULL) { // Do nothing. - } else if(d_children == NULL){ + } else if (d_children == NULL) { d_children = new SExprVector(*other.d_children); - } else if(other.d_children == NULL){ + } else if (other.d_children == NULL) { delete d_children; d_children = NULL; } else { (*d_children) = other.getChildren(); } - Assert( isAtom() == other.isAtom() ); - Assert( (d_children == NULL) == isAtom() ); + Assert(isAtom() == other.isAtom()); + Assert((d_children == NULL) == isAtom()); return *this; } -SExpr::SExpr() : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { -} - - -SExpr::SExpr(const SExpr& other) : - d_sexprType(other.d_sexprType), - d_integerValue(other.d_integerValue), - d_rationalValue(other.d_rationalValue), - d_stringValue(other.d_stringValue), - d_children(NULL) -{ - d_children = (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children); +SExpr::SExpr() + : d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(const SExpr& other) + : d_sexprType(other.d_sexprType), + d_integerValue(other.d_integerValue), + d_rationalValue(other.d_rationalValue), + d_stringValue(other.d_stringValue), + d_children(NULL) { + d_children = + (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children); // d_children being NULL is equivalent to the node being an atom. - Assert( (d_children == NULL) == isAtom() ); -} - - -SExpr::SExpr(const CVC4::Integer& value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { - } - -SExpr::SExpr(int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { -} - -SExpr::SExpr(long int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { -} - -SExpr::SExpr(unsigned int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { -} - -SExpr::SExpr(unsigned long int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { -} - -SExpr::SExpr(const CVC4::Rational& value) : - d_sexprType(SEXPR_RATIONAL), - d_integerValue(0), - d_rationalValue(value), - d_stringValue(""), - d_children(NULL) { -} - -SExpr::SExpr(const std::string& value) : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value), - d_children(NULL) { -} + Assert((d_children == NULL) == isAtom()); +} + +SExpr::SExpr(const CVC4::Integer& value) + : d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(int value) + : d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(long int value) + : d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(unsigned int value) + : d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(unsigned long int value) + : d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(const CVC4::Rational& value) + : d_sexprType(SEXPR_RATIONAL), + d_integerValue(0), + d_rationalValue(value), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(const std::string& value) + : d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children(NULL) {} /** * This constructs a string expression from a const char* value. @@ -155,37 +144,33 @@ SExpr::SExpr(const std::string& value) : * Given the other constructors this SExpr("foo") converts to bool. * instead of SExpr(string("foo")). */ -SExpr::SExpr(const char* value) : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value), - d_children(NULL) { -} - -SExpr::SExpr(bool value) : - d_sexprType(SEXPR_KEYWORD), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value ? "true" : "false"), - d_children(NULL) { -} - -SExpr::SExpr(const Keyword& value) : - d_sexprType(SEXPR_KEYWORD), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value.getString()), - d_children(NULL) { -} - -SExpr::SExpr(const std::vector<SExpr>& children) : - d_sexprType(SEXPR_NOT_ATOM), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(""), - d_children(new SExprVector(children)) { -} +SExpr::SExpr(const char* value) + : d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children(NULL) {} + +SExpr::SExpr(bool value) + : d_sexprType(SEXPR_KEYWORD), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value ? "true" : "false"), + d_children(NULL) {} + +SExpr::SExpr(const Keyword& value) + : d_sexprType(SEXPR_KEYWORD), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value.getString()), + d_children(NULL) {} + +SExpr::SExpr(const std::vector<SExpr>& children) + : d_sexprType(SEXPR_NOT_ATOM), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children(new SExprVector(children)) {} std::string SExpr::toString() const { std::stringstream ss; @@ -194,68 +179,61 @@ std::string SExpr::toString() const { } /** Is this S-expression an atom? */ -bool SExpr::isAtom() const { - return d_sexprType != SEXPR_NOT_ATOM; -} +bool SExpr::isAtom() const { return d_sexprType != SEXPR_NOT_ATOM; } /** Is this S-expression an integer? */ -bool SExpr::isInteger() const { - return d_sexprType == SEXPR_INTEGER; -} +bool SExpr::isInteger() const { return d_sexprType == SEXPR_INTEGER; } /** Is this S-expression a rational? */ -bool SExpr::isRational() const { - return d_sexprType == SEXPR_RATIONAL; -} +bool SExpr::isRational() const { return d_sexprType == SEXPR_RATIONAL; } /** Is this S-expression a string? */ -bool SExpr::isString() const { - return d_sexprType == SEXPR_STRING; -} +bool SExpr::isString() const { return d_sexprType == SEXPR_STRING; } /** Is this S-expression a keyword? */ -bool SExpr::isKeyword() const { - return d_sexprType == SEXPR_KEYWORD; -} - +bool SExpr::isKeyword() const { return d_sexprType == SEXPR_KEYWORD; } std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) { SExpr::toStream(out, sexpr); return out; } -void SExpr::toStream(std::ostream& out, const SExpr& sexpr) throw() { +void SExpr::toStream(std::ostream& out, const SExpr& sexpr) { toStream(out, sexpr, language::SetLanguage::getLanguage(out)); } -void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() { - toStream(out, sexpr, language, PrettySExprs::getPrettySExprs(out) ? 2 : 0); +void SExpr::toStream(std::ostream& out, const SExpr& sexpr, + OutputLanguage language) { + const int indent = PrettySExprs::getPrettySExprs(out) ? 2 : 0; + toStream(out, sexpr, language, indent); } -void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() { - if( sexpr.isKeyword() && languageQuotesKeywords(language) ){ +void SExpr::toStream(std::ostream& out, const SExpr& sexpr, + OutputLanguage language, int indent) { + if (sexpr.isKeyword() && languageQuotesKeywords(language)) { out << quoteSymbol(sexpr.getValue()); } else { toStreamRec(out, sexpr, language, indent); } } - -void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() { - if(sexpr.isInteger()) { +void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, + OutputLanguage language, int indent) { + if (sexpr.isInteger()) { out << sexpr.getIntegerValue(); - } else if(sexpr.isRational()) { - out << std::fixed << sexpr.getRationalValue().getDouble(); - } else if(sexpr.isKeyword()) { + } else if (sexpr.isRational()) { + const double approximation = sexpr.getRationalValue().getDouble(); + out << std::fixed << approximation; + } else if (sexpr.isKeyword()) { out << sexpr.getValue(); - } else if(sexpr.isString()) { + } else if (sexpr.isString()) { std::string s = sexpr.getValue(); // escape backslash and quote - for(size_t i = 0; i < s.length(); ++i) { - if(s[i] == '"') { + for (size_t i = 0; i < s.length(); ++i) { + if (s[i] == '"') { s.replace(i, 1, "\\\""); ++i; - } else if(s[i] == '\\') { + } else if (s[i] == '\\') { s.replace(i, 1, "\\\\"); ++i; } @@ -265,31 +243,32 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage la const std::vector<SExpr>& kids = sexpr.getChildren(); out << (indent > 0 && kids.size() > 1 ? "( " : "("); bool first = true; - for(std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) { - if(first) { + for (std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); + ++i) { + if (first) { first = false; } else { - if(indent > 0) { + if (indent > 0) { out << "\n" << std::string(indent, ' '); } else { out << ' '; } } - toStreamRec(out, *i, language, indent <= 0 || indent > 2 ? 0 : indent + 2); + toStreamRec(out, *i, language, + indent <= 0 || indent > 2 ? 0 : indent + 2); } - if(indent > 0 && kids.size() > 1) { + if (indent > 0 && kids.size() > 1) { out << '\n'; - if(indent > 2) { + if (indent > 2) { out << std::string(indent - 2, ' '); } } out << ')'; } -}/* toStreamRec() */ - +} /* toStreamRec() */ bool SExpr::languageQuotesKeywords(OutputLanguage language) { - switch(language) { + switch (language) { case language::output::LANG_SMTLIB_V1: case language::output::LANG_SMTLIB_V2_0: case language::output::LANG_SMTLIB_V2_5: @@ -305,83 +284,76 @@ bool SExpr::languageQuotesKeywords(OutputLanguage language) { }; } - - std::string SExpr::getValue() const { - PrettyCheckArgument( isAtom(), this ); - switch(d_sexprType) { - case SEXPR_INTEGER: - return d_integerValue.toString(); - case SEXPR_RATIONAL: { - // We choose to represent rationals as decimal strings rather than - // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL - // could be added if we need both styles, even if it's backed by - // the same Rational object. - std::stringstream ss; - ss << std::fixed << d_rationalValue.getDouble(); - return ss.str(); - } - case SEXPR_STRING: - case SEXPR_KEYWORD: - return d_stringValue; - case SEXPR_NOT_ATOM: - return std::string(); + PrettyCheckArgument(isAtom(), this); + switch (d_sexprType) { + case SEXPR_INTEGER: + return d_integerValue.toString(); + case SEXPR_RATIONAL: { + // We choose to represent rationals as decimal strings rather than + // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL + // could be added if we need both styles, even if it's backed by + // the same Rational object. + std::stringstream ss; + ss << std::fixed << d_rationalValue.getDouble(); + return ss.str(); + } + case SEXPR_STRING: + case SEXPR_KEYWORD: + return d_stringValue; + case SEXPR_NOT_ATOM: + return std::string(); } return std::string(); - } const CVC4::Integer& SExpr::getIntegerValue() const { - PrettyCheckArgument( isInteger(), this ); + PrettyCheckArgument(isInteger(), this); return d_integerValue; } const CVC4::Rational& SExpr::getRationalValue() const { - PrettyCheckArgument( isRational(), this ); + PrettyCheckArgument(isRational(), this); return d_rationalValue; } const std::vector<SExpr>& SExpr::getChildren() const { - PrettyCheckArgument( !isAtom(), this ); - Assert( d_children != NULL ); + PrettyCheckArgument(!isAtom(), this); + Assert(d_children != NULL); return *d_children; } bool SExpr::operator==(const SExpr& s) const { - if (d_sexprType == s.d_sexprType && - d_integerValue == s.d_integerValue && + if (d_sexprType == s.d_sexprType && d_integerValue == s.d_integerValue && d_rationalValue == s.d_rationalValue && d_stringValue == s.d_stringValue) { - if(d_children == NULL && s.d_children == NULL){ + if (d_children == NULL && s.d_children == NULL) { return true; - } else if(d_children != NULL && s.d_children != NULL){ + } else if (d_children != NULL && s.d_children != NULL) { return getChildren() == s.getChildren(); } } return false; } -bool SExpr::operator!=(const SExpr& s) const { - return !(*this == s); -} - +bool SExpr::operator!=(const SExpr& s) const { return !(*this == s); } SExpr SExpr::parseAtom(const std::string& atom) { - if(atom == "true"){ + if (atom == "true") { return SExpr(true); - } else if(atom == "false"){ + } else if (atom == "false") { return SExpr(false); } else { try { Integer z(atom); return SExpr(z); - }catch(std::invalid_argument&){ + } catch (std::invalid_argument&) { // Fall through to the next case } try { Rational q(atom); return SExpr(q); - }catch(std::invalid_argument&){ + } catch (std::invalid_argument&) { // Fall through to the next case } return SExpr(atom); @@ -391,21 +363,21 @@ SExpr SExpr::parseAtom(const std::string& atom) { SExpr SExpr::parseListOfAtoms(const std::vector<std::string>& atoms) { std::vector<SExpr> parsedAtoms; typedef std::vector<std::string>::const_iterator const_iterator; - for(const_iterator i = atoms.begin(), i_end=atoms.end(); i != i_end; ++i){ + for (const_iterator i = atoms.begin(), i_end = atoms.end(); i != i_end; ++i) { parsedAtoms.push_back(parseAtom(*i)); } return SExpr(parsedAtoms); } -SExpr SExpr::parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists) { +SExpr SExpr::parseListOfListOfAtoms( + const std::vector<std::vector<std::string> >& atoms_lists) { std::vector<SExpr> parsedListsOfAtoms; - typedef std::vector< std::vector<std::string> >::const_iterator const_iterator; - for(const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end(); i != i_end; ++i){ + typedef std::vector<std::vector<std::string> >::const_iterator const_iterator; + for (const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end(); + i != i_end; ++i) { parsedListsOfAtoms.push_back(parseListOfAtoms(*i)); } return SExpr(parsedListsOfAtoms); } - - -}/* CVC4 namespace */ +} /* CVC4 namespace */ diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 9c80a1b1f..2948cba4b 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -40,18 +40,18 @@ namespace CVC4 { class CVC4_PUBLIC SExprKeyword { std::string d_str; -public: + + public: SExprKeyword(const std::string& s) : d_str(s) {} const std::string& getString() const { return d_str; } -};/* class SExpr::Keyword */ +}; /* class SExpr::Keyword */ /** * A simple S-expression. An S-expression is either an atom with a * string value, or a list of other S-expressions. */ class CVC4_PUBLIC SExpr { -public: - + public: typedef SExprKeyword Keyword; SExpr(); @@ -138,7 +138,6 @@ public: /** Is this S-expression different from another? */ bool operator!=(const SExpr& s) const; - /** * This returns the best match in the following order: * match atom with @@ -157,21 +156,23 @@ public: /** * Parses a list of list of atoms. */ - static SExpr parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists); - + static SExpr parseListOfListOfAtoms( + const std::vector<std::vector<std::string> >& atoms_lists); /** * Outputs the SExpr onto the ostream out. This version reads defaults to the - * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level is + * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level + * is * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise. */ - static void toStream(std::ostream& out, const SExpr& sexpr) throw(); + static void toStream(std::ostream& out, const SExpr& sexpr); /** * Outputs the SExpr onto the ostream out. This version sets the indent level * to 2 if PrettySExprs::getPrettySExprs() is on. */ - static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw(); + static void toStream(std::ostream& out, const SExpr& sexpr, + OutputLanguage language); /** * Outputs the SExpr onto the ostream out. @@ -181,19 +182,20 @@ public: * Otherwise this prints using toStreamRec(). * * TIM: Keywords that are children are not currently quoted. This seems - * incorrect but I am just reproduicing the old behavior even if it does not make + * incorrect but I am just reproduicing the old behavior even if it does not + * make * sense. */ - static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw(); - -private: + static void toStream(std::ostream& out, const SExpr& sexpr, + OutputLanguage language, int indent); + private: /** * Simple printer for SExpr to an ostream. * The current implementation is language independent. */ - static void toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw(); - + static void toStreamRec(std::ostream& out, const SExpr& sexpr, + OutputLanguage language, int indent); /** Returns true if this language quotes Keywords when printing. */ static bool languageQuotesKeywords(OutputLanguage language); @@ -222,11 +224,12 @@ private: * Whenever the SExpr isAtom() holds, this points at NULL. * * This should be a pointer in case the implementation of vector<SExpr> ever - * directly contained or allocated an SExpr. If this happened this would trigger, + * directly contained or allocated an SExpr. If this happened this would + * trigger, * either the size being infinite or SExpr() being an infinite loop. */ SExprVector* d_children; -};/* class SExpr */ +}; /* class SExpr */ /** Prints an SExpr. */ std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC; @@ -245,7 +248,7 @@ class CVC4_PUBLIC PrettySExprs { */ bool d_prettySExprs; -public: + public: /** * Construct a PrettySExprs with the given setting. */ @@ -273,21 +276,17 @@ public: std::ostream& d_out; bool d_oldPrettySExprs; - public: - - inline Scope(std::ostream& out, bool prettySExprs) : - d_out(out), - d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) { + public: + inline Scope(std::ostream& out, bool prettySExprs) + : d_out(out), d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) { PrettySExprs::setPrettySExprs(out, prettySExprs); } - inline ~Scope() { - PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); - } + inline ~Scope() { PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); } - };/* class PrettySExprs::Scope */ + }; /* class PrettySExprs::Scope */ -};/* class PrettySExprs */ +}; /* class PrettySExprs */ /** * Sets the default pretty-sexprs setting for an ostream. Use like this: @@ -299,7 +298,6 @@ public: */ std::ostream& operator<<(std::ostream& out, PrettySExprs ps); - -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__SEXPR_H */ diff --git a/src/util/subrange_bound.cpp b/src/util/subrange_bound.cpp index 085ecb930..a33c22f72 100644 --- a/src/util/subrange_bound.cpp +++ b/src/util/subrange_bound.cpp @@ -25,36 +25,34 @@ namespace CVC4 { -std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) -throw() { +std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) { out << bounds.lower << ".." << bounds.upper; return out; } /** Get the finite SubrangeBound, failing an assertion if infinite. */ -const Integer& SubrangeBound::getBound() const throw(IllegalArgumentException) { +const Integer& SubrangeBound::getBound() const { PrettyCheckArgument(!d_nobound, this, "SubrangeBound is infinite"); return d_bound; } -SubrangeBounds::SubrangeBounds(const SubrangeBound& l, - const SubrangeBound& u) - : lower(l) - , upper(u) -{ - PrettyCheckArgument(!l.hasBound() || !u.hasBound() || - l.getBound() <= u.getBound(), - l, "Bad subrange bounds specified"); +SubrangeBounds::SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u) + : lower(l), upper(u) { + PrettyCheckArgument( + !l.hasBound() || !u.hasBound() || l.getBound() <= u.getBound(), l, + "Bad subrange bounds specified"); } -bool SubrangeBounds::joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){ +bool SubrangeBounds::joinIsBounded(const SubrangeBounds& a, + const SubrangeBounds& b) { return (a.lower.hasBound() && b.lower.hasBound()) || - (a.upper.hasBound() && b.upper.hasBound()); + (a.upper.hasBound() && b.upper.hasBound()); } -SubrangeBounds SubrangeBounds::join(const SubrangeBounds& a, const SubrangeBounds& b){ - DebugCheckArgument(joinIsBounded(a,b), a); +SubrangeBounds SubrangeBounds::join(const SubrangeBounds& a, + const SubrangeBounds& b) { + DebugCheckArgument(joinIsBounded(a, b), a); SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower); SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper); return SubrangeBounds(newLower, newUpper); diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index 86c88e187..91c91af41 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -34,41 +34,33 @@ namespace CVC4 { * has a lower bound of -5 and an infinite upper bound. */ class CVC4_PUBLIC SubrangeBound { -public: - + public: /** Construct an infinite SubrangeBound. */ - SubrangeBound() throw() : - d_nobound(true), - d_bound() { - } + SubrangeBound() : d_nobound(true), d_bound() {} /** Construct a finite SubrangeBound. */ - SubrangeBound(const Integer& i) throw() : - d_nobound(false), - d_bound(i) { - } + SubrangeBound(const Integer& i) : d_nobound(false), d_bound(i) {} - ~SubrangeBound() throw() { - } + ~SubrangeBound() {} - /** Get the finite SubrangeBound, failing an assertion if infinite. */ - const Integer& getBound() const throw(IllegalArgumentException); + /** + * Get the finite SubrangeBound, failing an assertion if infinite. + * + * @throws IllegalArgumentException if the bound is infinite. + */ + const Integer& getBound() const; /** Returns true iff this is a finite SubrangeBound. */ - bool hasBound() const throw() { - return !d_nobound; - } + bool hasBound() const { return !d_nobound; } /** Test two SubrangeBounds for equality. */ - bool operator==(const SubrangeBound& b) const throw() { + bool operator==(const SubrangeBound& b) const { return hasBound() == b.hasBound() && - (!hasBound() || getBound() == b.getBound()); + (!hasBound() || getBound() == b.getBound()); } /** Test two SubrangeBounds for disequality. */ - bool operator!=(const SubrangeBound& b) const throw() { - return !(*this == b); - } + bool operator!=(const SubrangeBound& b) const { return !(*this == b); } /** * Is this SubrangeBound "less than" another? For two @@ -78,9 +70,9 @@ public: * behavior is due to the fact that a SubrangeBound without a bound * is the representation for both +infinity and -infinity. */ - bool operator<(const SubrangeBound& b) const throw() { + bool operator<(const SubrangeBound& b) const { return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) || - ( hasBound() && b.hasBound() && getBound() < b.getBound() ); + (hasBound() && b.hasBound() && getBound() < b.getBound()); } /** @@ -91,9 +83,9 @@ public: * behavior is due to the fact that a SubrangeBound without a bound * is the representation for both +infinity and -infinity. */ - bool operator<=(const SubrangeBound& b) const throw() { + bool operator<=(const SubrangeBound& b) const { return !hasBound() || !b.hasBound() || - ( hasBound() && b.hasBound() && getBound() <= b.getBound() ); + (hasBound() && b.hasBound() && getBound() <= b.getBound()); } /** @@ -104,9 +96,9 @@ public: * behavior is due to the fact that a SubrangeBound without a bound * is the representation for both +infinity and -infinity. */ - bool operator>(const SubrangeBound& b) const throw() { + bool operator>(const SubrangeBound& b) const { return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) || - ( hasBound() && b.hasBound() && getBound() < b.getBound() ); + (hasBound() && b.hasBound() && getBound() < b.getBound()); } /** @@ -117,36 +109,34 @@ public: * strange behavior is due to the fact that a SubrangeBound without * a bound is the representation for both +infinity and -infinity. */ - bool operator>=(const SubrangeBound& b) const throw() { + bool operator>=(const SubrangeBound& b) const { return !hasBound() || !b.hasBound() || - ( hasBound() && b.hasBound() && getBound() <= b.getBound() ); + (hasBound() && b.hasBound() && getBound() <= b.getBound()); } - - static SubrangeBound min(const SubrangeBound& a, const SubrangeBound& b){ - if(a.hasBound() && b.hasBound()){ + static SubrangeBound min(const SubrangeBound& a, const SubrangeBound& b) { + if (a.hasBound() && b.hasBound()) { return SubrangeBound(Integer::min(a.getBound(), b.getBound())); - }else{ + } else { return SubrangeBound(); } } - static SubrangeBound max(const SubrangeBound& a, const SubrangeBound& b){ - if(a.hasBound() && b.hasBound()){ + static SubrangeBound max(const SubrangeBound& a, const SubrangeBound& b) { + if (a.hasBound() && b.hasBound()) { return SubrangeBound(Integer::max(a.getBound(), b.getBound())); - }else{ + } else { return SubrangeBound(); } - } + } -private: + private: bool d_nobound; Integer d_bound; -};/* class SubrangeBound */ +}; /* class SubrangeBound */ class CVC4_PUBLIC SubrangeBounds { -public: - + public: SubrangeBound lower; SubrangeBound upper; @@ -167,7 +157,7 @@ public: */ bool operator<(const SubrangeBounds& bounds) const { return (lower > bounds.lower && upper <= bounds.upper) || - (lower >= bounds.lower && upper < bounds.upper); + (lower >= bounds.lower && upper < bounds.upper); } /** @@ -186,7 +176,7 @@ public: */ bool operator>(const SubrangeBounds& bounds) const { return (lower < bounds.lower && upper >= bounds.upper) || - (lower <= bounds.lower && upper > bounds.upper); + (lower <= bounds.lower && upper > bounds.upper); } /** @@ -209,24 +199,25 @@ public: */ static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b); -};/* class SubrangeBounds */ +}; /* class SubrangeBounds */ struct CVC4_PUBLIC SubrangeBoundsHashFunction { inline size_t operator()(const SubrangeBounds& bounds) const { // We use Integer::hash() rather than Integer::getUnsignedLong() // because the latter might overflow and throw an exception - size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() : std::numeric_limits<size_t>::max(); - size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() : std::numeric_limits<size_t>::max(); + size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() + : std::numeric_limits<size_t>::max(); + size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() + : std::numeric_limits<size_t>::max(); return l + 0x9e3779b9 + (u << 6) + (u >> 2); } -};/* struct SubrangeBoundsHashFunction */ +}; /* struct SubrangeBoundsHashFunction */ -inline std::ostream& -operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, + const SubrangeBound& bound) CVC4_PUBLIC; -inline std::ostream& -operator<<(std::ostream& out, const SubrangeBound& bound) throw() { - if(bound.hasBound()) { +inline std::ostream& operator<<(std::ostream& out, const SubrangeBound& bound) { + if (bound.hasBound()) { out << bound.getBound(); } else { out << '_'; @@ -235,9 +226,9 @@ operator<<(std::ostream& out, const SubrangeBound& bound) throw() { return out; } -std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) -throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, + const SubrangeBounds& bounds) CVC4_PUBLIC; -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__SUBRANGE_BOUND_H */ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 6608ae22d..43c77973f 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -86,7 +86,9 @@ TESTS = \ z3.620661-no-fv-trigger.smt2 \ bug_743.smt2 \ quaternion_ds1_symm_0428.fof.smt2 \ - bug749-rounding.smt2 + bug749-rounding.smt2 \ + RNDPRE_4_1-dd-nqe.smt2 \ + mix-complete-strat.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 b/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 new file mode 100644 index 000000000..6379d6cec --- /dev/null +++ b/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --cbqi-nested-qe +; EXPECT: unsat +(set-logic LRA) + +(declare-fun c () Real) + +(assert +(forall ((?x2 Real)) +(exists ((?x3 Real)) +(and +(forall ((?x4 Real)) (or +(not (>= ?x4 4)) +(and (> c (+ ?x2 ?x3)) (> (+ c ?x3 ?x4) 0))) ) +(not (> (+ c ?x2 ?x3) 0)) ) +)) ) + +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/mix-complete-strat.smt2 b/test/regress/regress0/quantifiers/mix-complete-strat.smt2 new file mode 100644 index 000000000..c2209f697 --- /dev/null +++ b/test/regress/regress0/quantifiers/mix-complete-strat.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) + +(declare-sort U 0) +(declare-fun P (U) Bool) + +(assert (forall ((x U)) (P x))) + +(declare-fun u () U) +(assert (P u)) + +(declare-const a Int) +(declare-const b Int) +(assert (forall ((x Int)) (or (> x a) (< x b)))) + +(check-sat) diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 558d170d7..2f36cc188 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -64,7 +64,8 @@ TESTS = \ union-1b.smt2 \ union-2.smt2 \ dt-simp-mem.smt2 \ - card3-ground.smt2 + card3-ground.smt2 \ + card-vc6-minimized.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/card-vc6-minimized.smt2 b/test/regress/regress0/sets/card-vc6-minimized.smt2 new file mode 100644 index 000000000..d7f4bdf1e --- /dev/null +++ b/test/regress/regress0/sets/card-vc6-minimized.smt2 @@ -0,0 +1,15 @@ +; EXPECT: unsat +(set-logic QF_UFLIAFS) +(declare-fun x () Int) +(declare-fun c () (Set Int)) +(declare-fun alloc0 () (Set Int)) +(declare-fun alloc1 () (Set Int)) +(declare-fun alloc2 () (Set Int)) +(assert +(and (member x c) + (<= (card (setminus alloc1 alloc0)) 1) + (<= (card (setminus alloc2 alloc1)) + (card (setminus c (singleton x)))) + (> (card (setminus alloc2 alloc0)) (card c)) +)) +(check-sat) |