From: ajreynol Date: Mon, 1 Jun 2015 20:44:40 +0000 (+0200) Subject: When proof enabled, disable uf sym break. Add regression. X-Git-Tag: cvc5-1.0.0~6318 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cbcc5124a8f0f17acd981a80c182616cd0a778ff;p=cvc5.git When proof enabled, disable uf sym break. Add regression. --- diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index b546fcf87..263e1fe8c 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -87,6 +87,7 @@ void LFSCCnfProof::printPreprocess(std::ostream& os, std::ostream& paren) { os << "(th_let_pf _ "; //TODO + Trace("cnf-pf-debug") << "; preprocess assertion : " << e << std::endl; os << "(trust_f "; LFSCTheoryProof::printTerm(e, os); os << ") "; @@ -132,7 +133,9 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { Expr base_assertion = ProofManager::currentPM()->getFormulaForClauseId( id ); ProofRule pr = ProofManager::currentPM()->getProofRuleForClauseId( id ); - + Trace("cnf-pf") << std::endl; + Trace("cnf-pf") << "; formula for clause id " << id << " : " << base_assertion << std::endl; + //get the assertion for the clause id std::map< Expr, unsigned > childIndex; std::map< Expr, bool > childPol; @@ -152,7 +155,6 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { std::map< Expr, unsigned >::iterator itci = childIndex.find( base_assertion ); bool is_in_clause = itci!=childIndex.end(); unsigned base_index = is_in_clause ? itci->second : 0; - Trace("cnf-pf") << std::endl; Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl; if( !is_input ){ Assert( is_in_clause ); diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 2d8c4178a..311d4afeb 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -176,15 +176,16 @@ void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseK d_propVars.insert(lit.getSatVariable()); }*/ if (kind == INPUT) { + Debug("cores") << "; Add to inputClauses " << id << std::endl; d_inputClauses.insert(std::make_pair(id, clause)); Assert(d_satProof->d_inputClauses.find(id) != d_satProof->d_inputClauses.end()); - Debug("cores") << "core id is " << d_satProof->d_inputClauses[id] << std::endl; + Debug("cores") << "; core id is " << d_satProof->d_inputClauses[id] << std::endl; if(d_satProof->d_inputClauses[id] == uint64_t(-1)) { - Debug("cores") << " + constant unit (true or false)" << std::endl; + Debug("cores") << "; + constant unit (true or false)" << std::endl; } else if(options::unsatCores()) { Expr e = d_cnfProof->getAssertion(d_satProof->d_inputClauses[id] & 0xffffffff); - Debug("cores") << "core input assertion from CnfStream is " << e << std::endl; - Debug("cores") << "with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) << std::endl; + Debug("cores") << "; core input assertion from CnfStream is " << e << std::endl; + Debug("cores") << "; with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) << std::endl; // Invalid proof rules are currently used for parts of CVC4 that don't // support proofs (these are e.g. unproven theory lemmas) or don't need // proofs (e.g. split lemmas). We can ignore these safely when @@ -331,12 +332,13 @@ bool ProofManager::isInputAssertion( Expr e, std::ostream& out ) { } void ProofManager::setRegisteringFormula( Node n, ProofRule proof_id ) { + Trace("cnf-pf-debug") << "; set registering formula " << n << " proof rule = " << proof_id << std::endl; d_registering_assertion = n; d_registering_rule = proof_id; } void ProofManager::setRegisteredClauseId( ClauseId id ) { - Trace("cnf-pf-debug") << "set register clause id " << id << " " << d_registering_assertion << std::endl; + Trace("cnf-pf-debug") << "; set register clause id " << id << " " << d_registering_assertion << std::endl; if( !d_registering_assertion.isNull() ){ d_clause_id_to_assertion[id] = d_registering_assertion.toExpr(); d_clause_id_to_rule[id] = d_registering_rule; diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index 7867f1ddc..6854f4940 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -364,12 +364,12 @@ void SatProof::printRes(ResChain* res) { /// registration methods ClauseId SatProof::registerClause(Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) { - Debug("cores") << "registerClause " << proof_id << std::endl; + Debug("cores") << "registerClause, proof id = " << proof_id << std::endl; Assert(clause != CRef_Undef); ClauseIdMap::iterator it = d_clauseId.find(clause); if (it == d_clauseId.end()) { ClauseId newId = ProofManager::currentPM()->nextId(); - d_clauseId.insert(ClauseIdMap::value_type(clause, newId)); + d_clauseId.insert(ClauseIdMap::value_type(clause, newId)); d_idClause.insert(IdCRefMap::value_type(newId, clause)); if (kind == INPUT) { Assert(d_inputClauses.find(newId) == d_inputClauses.end()); diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index f03cc9944..b0b135b04 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -667,7 +667,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated Assert((uint64_t(proof_id) & 0xffffffff00000000llu) == 0 && (assertionTableIndex & 0xffffffff00000000llu) == 0, "proof_id/table_index collision"); d_proofId = assertionTableIndex | (uint64_t(proof_id) << 32); d_assertionTable.push_back(from.isNull() ? node : from); - Debug("cores") << "cnf ix " << assertionTableIndex << " asst " << node << " proof_id " << proof_id << " from " << from << endl; + Debug("cores") << "; cnf is " << assertionTableIndex << " asst " << node << " proof_id " << proof_id << " from " << from << endl; } else { // We aren't producing proofs or unsat cores; use an invalid proof id. d_proofId = uint64_t(-1); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 11a412c75..9fe3a115d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -700,9 +700,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_modelGlobalCommands(), d_modelCommands(NULL), d_dumpCommands(), -#ifdef CVC4_PROOF +#ifdef CVC4_PROOF d_defineCommands(), -#endif +#endif d_logic(), d_originalOptions(em->getOptions()), d_pendingPops(0), @@ -1083,7 +1083,7 @@ void SmtEngine::setDefaults() { // by default, symmetry breaker is on only for QF_UF if(! options::ufSymmetryBreaker.wasSetByUser()) { - bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified(); + bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified() && !options::proof(); Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl; options::ufSymmetryBreaker.set(qf_uf); } @@ -1168,8 +1168,8 @@ void SmtEngine::setDefaults() { if(! options::repeatSimp.wasSetByUser()) { bool repeatSimp = !d_logic.isQuantified() && (d_logic.isTheoryEnabled(THEORY_ARRAY) && - d_logic.isTheoryEnabled(THEORY_UF) && - d_logic.isTheoryEnabled(THEORY_BV)) && + d_logic.isTheoryEnabled(THEORY_UF) && + d_logic.isTheoryEnabled(THEORY_BV)) && !options::unsatCores(); Trace("smt") << "setting repeat simplification to " << repeatSimp << endl; options::repeatSimp.set(repeatSimp); @@ -1713,7 +1713,7 @@ void SmtEngine::defineFunction(Expr func, d_defineCommands.push_back(c.clone()); }); - + // Substitute out any abstract values in formula Expr form = d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr(); @@ -3087,7 +3087,7 @@ void SmtEnginePrivate::processAssertions() { Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl; Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - + if (d_assertions.size() == 0) { // nothing to do return; @@ -3385,7 +3385,7 @@ void SmtEnginePrivate::processAssertions() { d_iteSkolemMap.erase(toErase.back()); toErase.pop_back(); } - d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder)); + d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder)); } // For some reason this is needed for some benchmarks, such as // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 @@ -3497,7 +3497,7 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) } // rewrite rules are by default in the unsat core because // they need to be applied until saturation - if(options::unsatCores() && + if(options::unsatCores() && n.getKind() == kind::REWRITE_RULE ){ ProofManager::currentPM()->addUnsatCore(n.toExpr()); } @@ -4030,8 +4030,8 @@ void SmtEngine::checkUnsatCore() { for (; itg != d_defineCommands.end(); ++itg) { (*itg)->invoke(&coreChecker); } - ); - + ); + Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl; for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl; diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 50de00b61..c9a47c26f 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -49,7 +49,8 @@ TESTS = \ cnf-iff.smt2 \ cnf-iff-base.smt2 \ cnf-ite.smt2 \ - cnf-and-neg.smt2 + cnf-and-neg.smt2 \ + cnf_abc.smt2 EXTRA_DIST = $(TESTS) \ mkpidgeon diff --git a/test/regress/regress0/uf/cnf_abc.smt2 b/test/regress/regress0/uf/cnf_abc.smt2 new file mode 100755 index 000000000..5d011f44c --- /dev/null +++ b/test/regress/regress0/uf/cnf_abc.smt2 @@ -0,0 +1,168 @@ +(set-logic QF_UF) +(set-info :status unsat) + +(declare-sort I 0) +(declare-fun f (I I) I) +(declare-fun a () I) +(declare-fun b () I) +(declare-fun c () I) + + + +(assert + (or + (= (f a a) a) + (= (f a a) b) + (= (f a a) c) + )) + +(assert + (or + (= (f a b) a) + (= (f a b) b) + (= (f a b) c) + )) + +(assert + (or + (= (f a c) a) + (= (f a c) b) + (= (f a c) c) + )) + +(assert + (or + (= (f b a) a) + (= (f b a) b) + (= (f b a) c) + )) + +(assert + (or + (= (f b b) a) + (= (f b b) b) + (= (f b b) c) + )) + +(assert + (or + (= (f b c) a) + (= (f b c) b) + (= (f b c) c) + )) + + +(assert + (or + (= (f c a) a) + (= (f c a) b) + (= (f c a) c) + )) + +(assert + (or + (= (f c b) a) + (= (f c b) b) + (= (f c b) c) + )) + +(assert + (or + (= (f c c) a) + (= (f c c) b) + (= (f c c) c) + )) + + + +(assert + (or + (= (f a a) a) + (= (f b b) a) + (= (f c c) a) + )) + +(assert + (or + (= (f a a) b) + (= (f b b) b) + (= (f c c) b) + )) + +(assert + (or + (= (f a a) c) + (= (f b b) c) + (= (f c c) c) + )) + + + +(assert + (or + (= (f a a) a) + (= (f b a) b) + (= (f c a) c) + )) + +(assert + (or + (= (f a b) a) + (= (f b b) b) + (= (f c b) c) + )) + +(assert + (or + (= (f a c) a) + (= (f b c) b) + (= (f c c) c) + )) + + + + +(assert (not (= (f a a) a))) +(assert (not (= (f b b) b))) +(assert (not (= (f c c) c))) + + +(assert + (or + (not (= (f a (f a a)) a)) + (not (= (f a (f a b)) b)) + (not (= (f a (f a c)) c)) + )) + +(assert + (or + (not (= (f b (f b a)) a)) + (not (= (f b (f b b)) b)) + (not (= (f b (f b c)) c)) + )) + +(assert + (or + (not (= (f c (f c a)) a)) + (not (= (f c (f c b)) b)) + (not (= (f c (f c c)) c)) + )) + + +(assert (not (= (f a a) (f b a)))) +(assert (not (= (f a a) (f c a)))) +(assert (not (= (f b a) (f c a)))) + +(assert (not (= (f a b) (f b b)))) +(assert (not (= (f a b) (f c b)))) +(assert (not (= (f b b) (f c b)))) + +(assert (not (= (f a c) (f b c)))) +(assert (not (= (f a c) (f c c)))) +(assert (not (= (f b c) (f c c)))) + + + +(check-sat) + +(exit)