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 \
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
#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"
}/* 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());
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()) {
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
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 );
}
}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);
}
}
}
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() ){
}
// 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"));
}
}
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<Node, Node, NodeHashFunction> cache;
unordered_map<Node, Node, NodeHashFunction> bcache;
// 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;
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;
*/
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).
*/
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<Rational>().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<Rational>().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<Rational>().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;
}
--- /dev/null
+/********************* */
+/*! \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<Node>& assertions)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Assert(!assertions.empty());
+
+ Trace("cbqi-gn") << "Global negate : " << std::endl;
+ // collect free variables in all assertions
+ std::vector<Node> free_vars;
+ std::vector<TNode> visit;
+ std::unordered_set<TNode, TNodeHashFunction> 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<Node> 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 */
--- /dev/null
+/********************* */
+/*! \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 <vector>
+#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<Node>& assertions);
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H */
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
--- /dev/null
+; 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
projects / cvc5.git / commitdiff