From: Andrew Reynolds Date: Wed, 3 Jan 2018 15:35:27 +0000 (-0600) Subject: Global negate (#1466) X-Git-Tag: cvc5-1.0.0~5390 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1a11e8a71812d1abbf3fb13230c233d741c81fd1;p=cvc5.git Global negate (#1466) --- diff --git a/src/Makefile.am b/src/Makefile.am index 098fe4025..a6c58e281 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -401,6 +401,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/fun_def_engine.h \ theory/quantifiers/fun_def_process.cpp \ theory/quantifiers/fun_def_process.h \ + theory/quantifiers/global_negate.cpp \ + theory/quantifiers/global_negate.h \ theory/quantifiers/ho_trigger.cpp \ theory/quantifiers/ho_trigger.h \ theory/quantifiers/instantiate.cpp \ diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 27671fd82..2166f0add 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -58,6 +58,8 @@ option elimExtArithQuant --elim-ext-arith-quant bool :read-write :default true eliminate extended arithmetic symbols in quantified formulas option condRewriteQuant --cond-rewrite-quant bool :default true conditional rewriting of quantified formulas +option globalNegate --global-negate bool :read-write :default false + do global negation of input formula #### E-matching options diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9b4837d43..b3eaec1fd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -95,6 +95,7 @@ #include "theory/logic_info.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/fun_def_process.h" +#include "theory/quantifiers/global_negate.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" @@ -982,38 +983,39 @@ public: }/* namespace CVC4::smt */ -SmtEngine::SmtEngine(ExprManager* em) throw() : - d_context(new Context()), - d_userLevels(), - d_userContext(new UserContext()), - d_exprManager(em), - d_nodeManager(d_exprManager->getNodeManager()), - d_decisionEngine(NULL), - d_theoryEngine(NULL), - d_propEngine(NULL), - d_proofManager(NULL), - d_definedFunctions(NULL), - d_fmfRecFunctionsDefined(NULL), - d_assertionList(NULL), - d_assignments(NULL), - d_modelGlobalCommands(), - d_modelCommands(NULL), - d_dumpCommands(), - d_defineCommands(), - d_logic(), - d_originalOptions(), - d_pendingPops(0), - d_fullyInited(false), - d_problemExtended(false), - d_queryMade(false), - d_needPostsolve(false), - d_earlyTheoryPP(true), - d_status(), - d_replayStream(NULL), - d_private(NULL), - d_statisticsRegistry(NULL), - d_stats(NULL), - d_channels(new LemmaChannels()) +SmtEngine::SmtEngine(ExprManager* em) throw() + : d_context(new Context()), + d_userLevels(), + d_userContext(new UserContext()), + d_exprManager(em), + d_nodeManager(d_exprManager->getNodeManager()), + d_decisionEngine(NULL), + d_theoryEngine(NULL), + d_propEngine(NULL), + d_proofManager(NULL), + d_definedFunctions(NULL), + d_fmfRecFunctionsDefined(NULL), + d_assertionList(NULL), + d_assignments(NULL), + d_modelGlobalCommands(), + d_modelCommands(NULL), + d_dumpCommands(), + d_defineCommands(), + d_logic(), + d_originalOptions(), + d_pendingPops(0), + d_fullyInited(false), + d_problemExtended(false), + d_queryMade(false), + d_needPostsolve(false), + d_earlyTheoryPP(true), + d_globalNegation(false), + d_status(), + d_replayStream(NULL), + d_private(NULL), + d_statisticsRegistry(NULL), + d_stats(NULL), + d_channels(new LemmaChannels()) { SmtScope smts(this); d_originalOptions.copyValues(em->getOptions()); @@ -1434,6 +1436,17 @@ void SmtEngine::setDefaults() { Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl; setOption("repeat-simp", false); } + + if (options::globalNegate()) + { + if (options::globalNegate.wasSetByUser()) + { + throw OptionException("global-negate not supported with unsat cores"); + } + Notice() << "SmtEngine: turning off global-negate to support unsat-cores" + << endl; + setOption("global-negate", false); + } } if (options::cbqiBv()) { @@ -1743,6 +1756,7 @@ void SmtEngine::setDefaults() { options::sortInference.set( false ); options::ufssFairnessMonotone.set( false ); options::quantEpr.set( false ); + options::globalNegate.set(false); } if( d_logic.hasCardinalityConstraints() ){ //must have finite model finding on @@ -1931,7 +1945,8 @@ void SmtEngine::setDefaults() { if( !options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); } - if( d_logic.isPure(THEORY_ARITH) ){ + if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV)) + { options::cbqiAll.set( false ); if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); @@ -1945,9 +1960,23 @@ void SmtEngine::setDefaults() { } }else{ // only supported in pure arithmetic or pure BV - if (!d_logic.isPure(THEORY_BV)) + options::cbqiNestedQE.set(false); + } + // prenexing + if (options::cbqiNestedQE() + || options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) + { + // only complete with prenex = disj_normal or normal + if (options::prenexQuant() <= quantifiers::PRENEX_QUANT_DISJ_NORMAL) { - options::cbqiNestedQE.set(false); + options::prenexQuant.set(quantifiers::PRENEX_QUANT_DISJ_NORMAL); + } + } + else if (options::globalNegate()) + { + if (!options::prenexQuant.wasSetByUser()) + { + options::prenexQuant.set(quantifiers::PRENEX_QUANT_NONE); } } } @@ -1960,13 +1989,6 @@ void SmtEngine::setDefaults() { if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } - if( options::cbqi() && - ( options::cbqiNestedQE() || options::decisionMode()==decision::DECISION_STRATEGY_INTERNAL ) ){ - //only complete with prenex = disj_normal or normal - if( options::prenexQuant()<=quantifiers::PRENEX_QUANT_DISJ_NORMAL ){ - options::prenexQuant.set( quantifiers::PRENEX_QUANT_DISJ_NORMAL ); - } - } if( options::cbqiNestedQE() ){ options::prenexQuantUser.set( true ); if( !options::preSkolemQuant.wasSetByUser() ){ @@ -2057,26 +2079,40 @@ void SmtEngine::setDefaults() { } // Non-linear arithmetic does not support models unless nlExt is enabled - if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear() && !options::nlExt() ) { + if ((d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear() + && !options::nlExt()) + || options::globalNegate()) + { + std::string reason = + options::globalNegate() ? "--global-negate" : "nonlinear arithmetic"; if (options::produceModels()) { if(options::produceModels.wasSetByUser()) { - throw OptionException("produce-model not supported with nonlinear arith"); + throw OptionException( + std::string("produce-model not supported with " + reason)); } - Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl; + Warning() + << "SmtEngine: turning off produce-models because unsupported for " + << reason << endl; setOption("produce-models", SExpr("false")); } if (options::produceAssignments()) { if(options::produceAssignments.wasSetByUser()) { - throw OptionException("produce-assignments not supported with nonlinear arith"); + throw OptionException( + std::string("produce-assignments not supported with " + reason)); } - Warning() << "SmtEngine: turning off produce-assignments because unsupported for nonlinear arith" << endl; + Warning() << "SmtEngine: turning off produce-assignments because " + "unsupported for " + << reason << endl; setOption("produce-assignments", SExpr("false")); } if (options::checkModels()) { if(options::checkModels.wasSetByUser()) { - throw OptionException("check-models not supported with nonlinear arith"); + throw OptionException( + std::string("check-models not supported with " + reason)); } - Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl; + Warning() + << "SmtEngine: turning off check-models because unsupported for " + << reason << endl; setOption("check-models", SExpr("false")); } } @@ -4170,6 +4206,14 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + // global negation of the formula + if (options::globalNegate()) + { + quantifiers::GlobalNegate gn; + gn.simplify(d_assertions.ref()); + d_smt.d_globalNegation = !d_smt.d_globalNegation; + } + if( options::nlExtPurify() ){ unordered_map cache; unordered_map bcache; @@ -4660,6 +4704,9 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ // Note that a query has been made d_queryMade = true; + // reset global negation + d_globalNegation = false; + // Add the formula if(!e.isNull()) { d_problemExtended = true; @@ -4676,6 +4723,28 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ if ( ( options::solveRealAsInt() || options::solveIntAsBV() > 0 ) && r.asSatisfiabilityResult().isSat() == Result::UNSAT) { r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); } + // flipped if we did a global negation + if (d_globalNegation) + { + Trace("smt") << "SmtEngine::process global negate " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + r = Result(Result::SAT); + } + else if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + // only if satisfaction complete + if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV)) + { + r = Result(Result::UNSAT); + } + else + { + r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + } + } + Trace("smt") << "SmtEngine::global negate returned " << r << std::endl; + } d_needPostsolve = true; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index c628a1952..6d648ccda 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -241,6 +241,11 @@ class CVC4_PUBLIC SmtEngine { */ bool d_earlyTheoryPP; + /* + * Whether we did a global negation of the formula. + */ + bool d_globalNegation; + /** * Most recent result of last checkSat/query or (set-info :status). */ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 8313abd68..0e1dc62e1 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4878,47 +4878,71 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) switch(node.getKind()) { case kind::DIVISION: { - // partial function: division - if(d_divByZero.isNull()) { - d_divByZero = nm->mkSkolem("divByZero", nm->mkFunctionType(nm->realType(), nm->realType()), - "partial real division", NodeManager::SKOLEM_EXACT_NAME); - logicRequest.widenLogic(THEORY_UF); - } TNode num = node[0], den = node[1]; - Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num); - Node divTotalNumDen = nm->mkNode(kind::DIVISION_TOTAL, num, den); - return nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); + Node ret = nm->mkNode(kind::DIVISION_TOTAL, num, den); + if (!den.isConst() || den.getConst().sgn() == 0) + { + // partial function: division + if (d_divByZero.isNull()) + { + d_divByZero = + nm->mkSkolem("divByZero", + nm->mkFunctionType(nm->realType(), nm->realType()), + "partial real division", + NodeManager::SKOLEM_EXACT_NAME); + logicRequest.widenLogic(THEORY_UF); + } + Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); + Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num); + ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret); + } + return ret; break; } case kind::INTS_DIVISION: { // partial function: integer div - if(d_intDivByZero.isNull()) { - d_intDivByZero = nm->mkSkolem("intDivByZero", nm->mkFunctionType(nm->integerType(), nm->integerType()), - "partial integer division", NodeManager::SKOLEM_EXACT_NAME); - logicRequest.widenLogic(THEORY_UF); - } TNode num = node[0], den = node[1]; - Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num); - Node intDivTotalNumDen = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den); - return nm->mkNode(kind::ITE, den_eq_0, intDivByZeroNum, intDivTotalNumDen); + Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den); + if (!den.isConst() || den.getConst().sgn() == 0) + { + if (d_intDivByZero.isNull()) + { + d_intDivByZero = nm->mkSkolem( + "intDivByZero", + nm->mkFunctionType(nm->integerType(), nm->integerType()), + "partial integer division", + NodeManager::SKOLEM_EXACT_NAME); + logicRequest.widenLogic(THEORY_UF); + } + Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); + Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num); + ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret); + } + return ret; break; } case kind::INTS_MODULUS: { // partial function: mod - if(d_modZero.isNull()) { - d_modZero = nm->mkSkolem("modZero", nm->mkFunctionType(nm->integerType(), nm->integerType()), - "partial modulus", NodeManager::SKOLEM_EXACT_NAME); - logicRequest.widenLogic(THEORY_UF); - } TNode num = node[0], den = node[1]; - Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num); - Node modTotalNumDen = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den); - return nm->mkNode(kind::ITE, den_eq_0, modZeroNum, modTotalNumDen); + Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den); + if (!den.isConst() || den.getConst().sgn() == 0) + { + if (d_modZero.isNull()) + { + d_modZero = nm->mkSkolem( + "modZero", + nm->mkFunctionType(nm->integerType(), nm->integerType()), + "partial modulus", + NodeManager::SKOLEM_EXACT_NAME); + logicRequest.widenLogic(THEORY_UF); + } + Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); + Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num); + ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret); + } + return ret; break; } diff --git a/src/theory/quantifiers/global_negate.cpp b/src/theory/quantifiers/global_negate.cpp new file mode 100644 index 000000000..01925ec43 --- /dev/null +++ b/src/theory/quantifiers/global_negate.cpp @@ -0,0 +1,110 @@ +/********************* */ +/*! \file global_negate.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 global_negate + **/ + +#include "theory/quantifiers/global_negate.h" +#include "theory/rewriter.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void GlobalNegate::simplify(std::vector& assertions) +{ + NodeManager* nm = NodeManager::currentNM(); + Assert(!assertions.empty()); + + Trace("cbqi-gn") << "Global negate : " << std::endl; + // collect free variables in all assertions + std::vector free_vars; + std::vector visit; + std::unordered_set visited; + for (const Node& as : assertions) + { + Trace("cbqi-gn") << " " << as << std::endl; + TNode cur = as; + // compute free variables + visit.push_back(cur); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.isVar() && cur.getKind() != BOUND_VARIABLE) + { + free_vars.push_back(cur); + } + for (const TNode& cn : cur) + { + visit.push_back(cn); + } + } + } while (!visit.empty()); + } + + Node body; + if (assertions.size() == 1) + { + body = assertions[0]; + } + else + { + body = nm->mkNode(AND, assertions); + } + + // do the negation + body = body.negate(); + + if (!free_vars.empty()) + { + std::vector bvs; + for (const Node& v : free_vars) + { + Node bv = nm->mkBoundVar(v.getType()); + bvs.push_back(bv); + } + + body = body.substitute( + free_vars.begin(), free_vars.end(), bvs.begin(), bvs.end()); + + Node bvl = nm->mkNode(BOUND_VAR_LIST, bvs); + + body = nm->mkNode(FORALL, bvl, body); + } + + Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl; + body = Rewriter::rewrite(body); + Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl; + + Node truen = nm->mkConst(true); + for (unsigned i = 0, size = assertions.size(); i < size; i++) + { + if (i == 0) + { + assertions[i] = body; + } + else + { + assertions[i] = truen; + } + } +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/global_negate.h b/src/theory/quantifiers/global_negate.h new file mode 100644 index 000000000..814b0014c --- /dev/null +++ b/src/theory/quantifiers/global_negate.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file global_negate.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 global_negate + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H +#define __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H + +#include +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** GlobalNegate + * + * This class updates a set of assertions to be equivalent to the negation of + * these assertions. In detail, if assertions is: + * F1, ..., Fn + * then we update this vector to: + * forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true + * where x1...xm are the free variables of F1...Fn. + */ +class GlobalNegate +{ + public: + GlobalNegate() {} + ~GlobalNegate() {} + /** simplify assertions + * + * Replaces assertions with a set of assertions that is equivalent to its + * negation. + */ + void simplify(std::vector& assertions); +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H */ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index a8c25ae5a..133c2018d 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -135,7 +135,8 @@ TESTS = \ clock-10.smt2 \ javafe.tc.FlowInsensitiveChecks.682.smt2 \ javafe.tc.CheckCompilationUnit.001.smt2 \ - model_6_1_bv.smt2 + model_6_1_bv.smt2 \ + lra-triv-gn.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/lra-triv-gn.smt2 b/test/regress/regress0/quantifiers/lra-triv-gn.smt2 new file mode 100644 index 000000000..ccd31c463 --- /dev/null +++ b/test/regress/regress0/quantifiers/lra-triv-gn.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --global-negate --no-check-unsat-cores +; EXPECT: unsat +(set-logic LRA) +(set-info :status unsat) +(assert (not (exists ((?X Real)) (>= (/ (- 13) 4) ?X)))) +(check-sat) +(exit) \ No newline at end of file