From: ajreynol Date: Thu, 9 Apr 2015 13:51:26 +0000 (+0200) Subject: Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and string... X-Git-Tag: cvc5-1.0.0~6360 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f59801357808a538934b04ce7bf0894dec1b0dd;p=cvc5.git Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and strings preprocessing. Minor fix for conjecture generation for finite types. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cb18b8464..25ac4c516 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3165,15 +3165,10 @@ void SmtEnginePrivate::processAssertions() { if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { dumpAssertions("pre-strings-pp", d_assertions); CVC4::theory::strings::StringsPreprocess sp; - std::vector newNodes; - newNodes.push_back(d_assertions[d_realAssertionsEnd - 1]); - sp.simplify( d_assertions.ref(), newNodes ); - if(newNodes.size() > 1) { - d_assertions[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes); - } - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions[i] = Rewriter::rewrite( d_assertions[i] ); - } + sp.simplify( d_assertions.ref() ); + //for (unsigned i = 0; i < d_assertions.size(); ++ i) { + // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) ); + //} dumpAssertions("post-strings-pp", d_assertions); } if( d_smt.d_logic.isQuantified() ){ @@ -3182,7 +3177,7 @@ void SmtEnginePrivate::processAssertions() { if( d_assertions[i].getKind() == kind::REWRITE_RULE ){ Node prev = d_assertions[i]; Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl; - d_assertions[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions[i] ) ); + d_assertions.replace(i, Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions[i] ) ) ); Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl; Trace("quantifiers-rewrite") << " ...got " << d_assertions[i] << endl; } @@ -3235,10 +3230,6 @@ void SmtEnginePrivate::processAssertions() { } } - //if( options::quantConflictFind() ){ - // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertions ); - //} - if( options::pbRewrites() ){ d_pbsProcessor.learn(d_assertions.ref()); if(d_pbsProcessor.likelyToHelp()){ diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 48d3f3902..116debb7c 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1159,6 +1159,8 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< vec[i] = 0; } vec_sum = -1; + }else{ + return; } } } diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp index 5435fba34..23e18bb02 100644 --- a/src/theory/quantifiers/first_order_reasoning.cpp +++ b/src/theory/quantifiers/first_order_reasoning.cpp @@ -17,6 +17,7 @@ #include "theory/quantifiers/first_order_reasoning.h" #include "theory/rewriter.h" +#include "proof/proof_manager.h" using namespace CVC4; using namespace std; @@ -100,7 +101,12 @@ void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){ }while( num_processed>0 ); Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl; for( unsigned i=0; iaddDependence(curr, assertions[i]); ); + assertions[i] = curr; + } } } diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index b80d9d744..f47cb8f1e 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -20,6 +20,7 @@ #include "theory/rewriter.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quant_util.h" +#include "proof/proof_manager.h" using namespace CVC4; using namespace std; @@ -75,8 +76,10 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl; Trace("fmf-fun-def") << " to " << std::endl; - assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); - assertions[i] = Rewriter::rewrite( assertions[i] ); + Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); + new_q = Rewriter::rewrite( new_q ); + PROOF( ProofManager::currentPM()->addDependence(new_q, assertions[i]); ); + assertions[i] = new_q; Trace("fmf-fun-def") << " " << assertions[i] << std::endl; fd_assertions.push_back( i ); } @@ -95,6 +98,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl; Trace("fmf-fun-def-rewrite") << " to " << std::endl; Trace("fmf-fun-def-rewrite") << " " << n << std::endl; + PROOF( ProofManager::currentPM()->addDependence(n, assertions[i]); ); assertions[i] = n; } } diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 81cd5948a..d9a31f4b5 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/macros.h" #include "theory/rewriter.h" +#include "proof/proof_manager.h" using namespace CVC4; using namespace std; @@ -36,11 +37,12 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite if( doRewrite && !d_macro_defs.empty() ){ //now, rewrite based on macro definitions for( size_t i=0; iaddDependence(curr, assertions[i]); ); + assertions[i] = curr; retVal = true; } } diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index a8cbcfac0..b27cab223 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Tianyi Liang ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters + ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -19,6 +19,7 @@ #include "theory/strings/options.h" #include "smt/logic_exception.h" #include +#include "proof/proof_manager.h" namespace CVC4 { namespace theory { @@ -550,15 +551,15 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { retNode = t; } }*/ - - Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode << std::endl; - if(!new_nodes.empty()) { - Trace("strings-preprocess") << " ... new nodes (" << new_nodes.size() << "):\n"; - for(unsigned int i=0; i & new_nodes) { } } -void StringsPreprocess::simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes) { +void StringsPreprocess::simplify(std::vector< Node > &vec_node) { for( unsigned i=0; i new_nodes; + Node curr = decompose( vec_node[i], new_nodes ); + if( !new_nodes.empty() ){ + new_nodes.insert( new_nodes.begin(), curr ); + curr = NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); + } + if( curr!=vec_node[i] ){ + curr = Rewriter::rewrite( curr ); + PROOF( ProofManager::currentPM()->addDependence(curr, vec_node[i]); ); + vec_node[i] = curr; + } } } - +/* void StringsPreprocess::simplify(std::vector< Node > &vec_node) { std::vector< Node > new_nodes; simplify(vec_node, new_nodes); vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() ); } +*/ }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 334ac1d61..155b7b236 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Tianyi Liang ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -40,7 +40,6 @@ private: Node simplify( Node t, std::vector< Node > &new_nodes ); Node decompose( Node t, std::vector< Node > &new_nodes ); public: - void simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes); void simplify(std::vector< Node > &vec_node); StringsPreprocess(); }; diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index dbd1dcd16..14d37e068 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -24,6 +24,7 @@ #include "smt/options.h" #include "theory/rewriter.h" #include "theory/quantifiers/options.h" +#include "proof/proof_manager.h" using namespace CVC4; using namespace std; @@ -172,13 +173,15 @@ bool SortInference::simplify( std::vector< Node >& assertions ){ Node prev = assertions[i]; std::map< Node, Node > var_bound; Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl; - assertions[i] = simplify( assertions[i], var_bound ); + Node curr = simplify( assertions[i], var_bound ); Trace("sort-inference-debug") << "Done." << std::endl; - if( prev!=assertions[i] ){ - assertions[i] = theory::Rewriter::rewrite( assertions[i] ); + if( curr!=assertions[i] ){ + curr = theory::Rewriter::rewrite( curr ); rewritten = true; - Trace("sort-inference-rewrite") << prev << std::endl; - Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl; + Trace("sort-inference-rewrite") << assertions << std::endl; + Trace("sort-inference-rewrite") << " --> " << curr << std::endl; + PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); ); + assertions[i] = curr; } } //now, ensure constants are distinct