diff options
24 files changed, 454 insertions, 439 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 40aa1a5af..6a21566e0 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -77,6 +77,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/bv_intro_pow2.h \ preprocessing/passes/extended_rewriter_pass.cpp \ preprocessing/passes/extended_rewriter_pass.h \ + preprocessing/passes/global_negate.cpp \ + preprocessing/passes/global_negate.h \ preprocessing/passes/int_to_bv.cpp \ preprocessing/passes/int_to_bv.h \ preprocessing/passes/ite_removal.cpp \ @@ -462,8 +464,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/fmf/model_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/instantiate.cpp \ theory/quantifiers/instantiate.h \ theory/quantifiers/inst_match.cpp \ diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index 73a2be9ff..e0c34127a 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -77,15 +77,6 @@ header = "options/uf_options.h" help = "mode of operation for uf strong solver." [[option]] - name = "ufssCliqueSplits" - category = "regular" - long = "uf-ss-clique-splits" - type = "bool" - default = "false" - read_only = true - help = "use cliques instead of splitting on demand to shrink model" - -[[option]] name = "ufssFairness" category = "regular" long = "uf-ss-fair" diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp index 12c1c5c21..26785f15b 100644 --- a/src/preprocessing/passes/bv_ackermann.cpp +++ b/src/preprocessing/passes/bv_ackermann.cpp @@ -23,12 +23,9 @@ #include "preprocessing/passes/bv_ackermann.h" -#include "expr/node.h" #include "options/bv_options.h" #include "theory/bv/theory_bv_utils.h" -#include <unordered_set> - using namespace CVC4; using namespace CVC4::theory; @@ -41,55 +38,142 @@ namespace passes { namespace { -void storeFunction( - TNode func, - TNode term, - FunctionToArgsMap& fun_to_args, - SubstitutionMap& fun_to_skolem) +void addLemmaForPair(TNode args1, + TNode args2, + const TNode func, + AssertionPipeline* assertionsToPreprocess, + NodeManager* nm) { - if (fun_to_args.find(func) == fun_to_args.end()) + Node args_eq; + + if (args1.getKind() == kind::APPLY_UF) { - fun_to_args.insert(make_pair(func, NodeSet())); + Assert(args1.getOperator() == func); + Assert(args2.getKind() == kind::APPLY_UF && args2.getOperator() == func); + Assert(args1.getNumChildren() == args2.getNumChildren()); + + std::vector<Node> eqs(args1.getNumChildren()); + + for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i) + { + eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]); + } + args_eq = bv::utils::mkAnd(eqs); } - NodeSet& set = fun_to_args[func]; - if (set.find(term) == set.end()) + else { - set.insert(term); - TypeNode tn = term.getType(); - Node skolem = NodeManager::currentNM()->mkSkolem( - "BVSKOLEM$$", - tn, - "is a variable created by the ackermannization " - "preprocessing pass for theory BV"); - fun_to_skolem.addSubstitution(term, skolem); + Assert(args1.getKind() == kind::SELECT && args1[0] == func); + Assert(args2.getKind() == kind::SELECT && args2[0] == func); + Assert(args1.getNumChildren() == 2); + Assert(args2.getNumChildren() == 2); + args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]); } + Node func_eq = nm->mkNode(kind::EQUAL, args1, args2); + Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq); + assertionsToPreprocess->push_back(lemma); } -void collectFunctionSymbols( - TNode term, - FunctionToArgsMap& fun_to_args, - SubstitutionMap& fun_to_skolem, - std::unordered_set<TNode, TNodeHashFunction>& seen) +void storeFunctionAndAddLemmas(TNode func, + TNode term, + FunctionToArgsMap& fun_to_args, + SubstitutionMap& fun_to_skolem, + AssertionPipeline* assertions, + NodeManager* nm, + std::vector<TNode>* vec) { - if (seen.find(term) != seen.end()) return; - if (term.getKind() == kind::APPLY_UF) - { - storeFunction(term.getOperator(), term, fun_to_args, fun_to_skolem); - } - else if (term.getKind() == kind::SELECT) + if (fun_to_args.find(func) == fun_to_args.end()) { - storeFunction(term[0], term, fun_to_args, fun_to_skolem); + fun_to_args.insert(make_pair(func, TNodeSet())); } - else + TNodeSet& set = fun_to_args[func]; + if (set.find(term) == set.end()) { - AlwaysAssert(term.getKind() != kind::STORE, - "Cannot use eager bitblasting on QF_ABV formula with stores"); + TypeNode tn = term.getType(); + Node skolem = nm->mkSkolem("BVSKOLEM$$", + tn, + "is a variable created by the ackermannization " + "preprocessing pass for theory BV"); + for (const auto& t : set) + { + addLemmaForPair(t, term, func, assertions, nm); + } + fun_to_skolem.addSubstitution(term, skolem); + set.insert(term); + /* Add the arguments of term (newest element in set) to the vector, so that + * collectFunctionsAndLemmas will process them as well. + * This is only needed if the set has at least two elements + * (otherwise, no lemma is generated). + * Therefore, we defer this for term in case it is the first element in the + * set*/ + if (set.size() == 2) + { + for (TNode elem : set) + { + vec->insert(vec->end(), elem.begin(), elem.end()); + } + } + else if (set.size() > 2) + { + vec->insert(vec->end(), term.begin(), term.end()); + } } - for (const TNode& n : term) +} + +/* We only add top-level applications of functions. + * For example: when we see "f(g(x))", we do not add g as a function and x as a + * parameter. + * Instead, we only include f as a function and g(x) as a parameter. + * However, if we see g(x) later on as a top-level application, we will add it + * as well. + * Another example: for the formula f(g(x))=f(g(y)), + * we first only add f as a function and g(x),g(y) as arguments. + * storeFunctionAndAddLemmas will then add the constraint g(x)=g(y) -> + * f(g(x))=f(g(y)). + * Now that we see g(x) and g(y), we explicitly add them as well. */ +void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args, + SubstitutionMap& fun_to_skolem, + std::vector<TNode>* vec, + AssertionPipeline* assertions) +{ + TNodeSet seen; + NodeManager* nm = NodeManager::currentNM(); + TNode term; + while (!vec->empty()) { - collectFunctionSymbols(n, fun_to_args, fun_to_skolem, seen); + term = vec->back(); + vec->pop_back(); + if (seen.find(term) == seen.end()) + { + TNode func; + if (term.getKind() == kind::APPLY_UF) + { + storeFunctionAndAddLemmas(term.getOperator(), + term, + fun_to_args, + fun_to_skolem, + assertions, + nm, + vec); + } + else if (term.getKind() == kind::SELECT) + { + storeFunctionAndAddLemmas( + term[0], term, fun_to_args, fun_to_skolem, assertions, nm, vec); + } + else + { + AlwaysAssert( + term.getKind() != kind::STORE, + "Cannot use eager bitblasting on QF_ABV formula with stores"); + /* add children to the vector, so that they are processed later */ + for (TNode n : term) + { + vec->push_back(n); + } + } + seen.insert(term); + } } - seen.insert(term); } } // namespace @@ -108,57 +192,15 @@ PreprocessingPassResult BVAckermann::applyInternal( Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); AlwaysAssert(!options::incrementalSolving()); - std::unordered_set<TNode, TNodeHashFunction> seen; - + /* collect all function applications and generate consistency lemmas + * accordingly */ + std::vector<TNode> to_process; for (const Node& a : assertionsToPreprocess->ref()) { - collectFunctionSymbols(a, d_funcToArgs, d_funcToSkolem, seen); - } - - NodeManager* nm = NodeManager::currentNM(); - for (const auto& p : d_funcToArgs) - { - TNode func = p.first; - const NodeSet& args = p.second; - NodeSet::const_iterator it1 = args.begin(); - for (; it1 != args.end(); ++it1) - { - for (NodeSet::const_iterator it2 = it1; it2 != args.end(); ++it2) - { - TNode args1 = *it1; - TNode args2 = *it2; - Node args_eq; - - if (args1.getKind() == kind::APPLY_UF) - { - AlwaysAssert(args1.getKind() == kind::APPLY_UF - && args1.getOperator() == func); - AlwaysAssert(args2.getKind() == kind::APPLY_UF - && args2.getOperator() == func); - AlwaysAssert(args1.getNumChildren() == args2.getNumChildren()); - - std::vector<Node> eqs(args1.getNumChildren()); - - for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i) - { - eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]); - } - args_eq = bv::utils::mkAnd(eqs); - } - else - { - AlwaysAssert(args1.getKind() == kind::SELECT && args1[0] == func); - AlwaysAssert(args2.getKind() == kind::SELECT && args2[0] == func); - AlwaysAssert(args1.getNumChildren() == 2); - AlwaysAssert(args2.getNumChildren() == 2); - args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]); - } - Node func_eq = nm->mkNode(kind::EQUAL, args1, args2); - Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq); - assertionsToPreprocess->push_back(lemma); - } - } + to_process.push_back(a); } + collectFunctionsAndLemmas( + d_funcToArgs, d_funcToSkolem, &to_process, assertionsToPreprocess); /* replace applications of UF by skolems */ // FIXME for model building, github issue #1901 diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/bv_ackermann.h index 197e92178..5f799ffe4 100644 --- a/src/preprocessing/passes/bv_ackermann.h +++ b/src/preprocessing/passes/bv_ackermann.h @@ -26,16 +26,18 @@ #ifndef __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H #define __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H +#include <unordered_map> +#include "expr/node.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" -#include <unordered_map> - namespace CVC4 { namespace preprocessing { namespace passes { -typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgsMap; +using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>; +using FunctionToArgsMap = + std::unordered_map<TNode, TNodeSet, TNodeHashFunction>; class BVAckermann : public PreprocessingPass { diff --git a/src/theory/quantifiers/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index 0670b5c5b..ddebf961f 100644 --- a/src/theory/quantifiers/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -12,21 +12,22 @@ ** \brief Implementation of global_negate **/ -#include "theory/quantifiers/global_negate.h" +#include "preprocessing/passes/global_negate.h" +#include <vector> +#include "expr/node.h" #include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; +using namespace CVC4::theory; namespace CVC4 { -namespace theory { -namespace quantifiers { +namespace preprocessing { +namespace passes { -void GlobalNegate::simplify(std::vector<Node>& assertions) +Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm) { - 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; @@ -90,21 +91,26 @@ void GlobalNegate::simplify(std::vector<Node>& assertions) Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl; body = Rewriter::rewrite(body); Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl; + return body; +} - Node truen = nm->mkConst(true); - for (unsigned i = 0, size = assertions.size(); i < size; i++) +GlobalNegate::GlobalNegate(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "global-negate"){}; + +PreprocessingPassResult GlobalNegate::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + NodeManager* nm = NodeManager::currentNM(); + Node simplifiedNode = simplify(assertionsToPreprocess->ref(), nm); + Node trueNode = nm->mkConst(true); + for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { - if (i == 0) - { - assertions[i] = body; - } - else - { - assertions[i] = truen; - } + assertionsToPreprocess->replace(i, trueNode); } + assertionsToPreprocess->push_back(simplifiedNode); + return PreprocessingPassResult::NO_CONFLICT; } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h new file mode 100644 index 000000000..0330aa10e --- /dev/null +++ b/src/preprocessing/passes/global_negate.h @@ -0,0 +1,52 @@ +/********************* */ +/*! \file global_negate.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 the global_negate preprocessing pass + * Updates a set of assertions 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. + * When this is done, d_globalNegation flag is marked, so that the solver checks + *for unsat instead of sat. +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H +#define __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class GlobalNegate : public PreprocessingPass +{ + public: + GlobalNegate(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + Node simplify(std::vector<Node>& assertions, NodeManager* nm); +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f1a59a580..5e7d52676 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -79,6 +79,7 @@ #include "preprocessing/passes/bv_intro_pow2.h" #include "preprocessing/passes/bv_to_bool.h" #include "preprocessing/passes/extended_rewriter_pass.h" +#include "preprocessing/passes/global_negate.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/ite_removal.h" #include "preprocessing/passes/pseudo_boolean_processor.h" @@ -115,7 +116,6 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.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" @@ -2659,6 +2659,8 @@ void SmtEnginePrivate::finishInit() new BVToBool(d_preprocessingPassContext.get())); std::unique_ptr<ExtRewPre> extRewPre( new ExtRewPre(d_preprocessingPassContext.get())); + std::unique_ptr<GlobalNegate> globalNegate( + new GlobalNegate(d_preprocessingPassContext.get())); std::unique_ptr<IntToBV> intToBV( new IntToBV(d_preprocessingPassContext.get())); std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess( @@ -2700,6 +2702,8 @@ void SmtEnginePrivate::finishInit() std::move(bvIntroPow2)); d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool)); d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre)); + d_preprocessingPassRegistry.registerPass("global-negate", + std::move(globalNegate)); d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); d_preprocessingPassRegistry.registerPass("quantifiers-preprocess", std::move(quantifiersPreprocess)); @@ -4084,8 +4088,7 @@ void SmtEnginePrivate::processAssertions() { if (options::globalNegate()) { // global negation of the formula - quantifiers::GlobalNegate gn; - gn.simplify(d_assertions.ref()); + d_preprocessingPassRegistry.getPass("global-negate")->apply(&d_assertions); d_smt.d_globalNegation = !d_smt.d_globalNegation; } diff --git a/src/theory/quantifiers/global_negate.h b/src/theory/quantifiers/global_negate.h deleted file mode 100644 index f5d92c478..000000000 --- a/src/theory/quantifiers/global_negate.h +++ /dev/null @@ -1,53 +0,0 @@ -/********************* */ -/*! \file global_negate.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 */ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 091c3b673..a16e03420 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -101,10 +101,6 @@ void InstMatch::clear() { } Node InstMatch::get(int i) const { return d_vals[i]; } -void InstMatch::getInst(std::vector<Node>& inst) const -{ - inst.insert(inst.end(), d_vals.begin(), d_vals.end()); -} void InstMatch::setValue( int i, TNode n ) { d_vals[i] = n; diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 86138feb3..5695d1294 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -80,8 +80,6 @@ public: } /** get the i^th term in the instantiation */ Node get(int i) const; - /** append the terms of this instantiation to inst */ - void getInst(std::vector<Node>& inst) const; /** set/overwrites the i^th field in the instantiation with n */ void setValue( int i, TNode n ); /** set the i^th term in the instantiation to n diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp index b9e4d0650..a05388d17 100644 --- a/src/theory/quantifiers/quant_relevance.cpp +++ b/src/theory/quantifiers/quant_relevance.cpp @@ -28,21 +28,6 @@ void QuantRelevance::registerQuantifier(Node f) std::vector<Node> syms; computeSymbols(f[1], syms); d_syms[f].insert(d_syms[f].begin(), syms.begin(), syms.end()); - // set initial relevance - int minRelevance = -1; - for (int i = 0; i < (int)syms.size(); i++) - { - d_syms_quants[syms[i]].push_back(f); - int r = getRelevance(syms[i]); - if (r != -1 && (minRelevance == -1 || r < minRelevance)) - { - minRelevance = r; - } - } - if (minRelevance != -1) - { - setRelevance(f, minRelevance + 1); - } } /** compute symbols */ @@ -65,33 +50,6 @@ void QuantRelevance::computeSymbols(Node n, std::vector<Node>& syms) } } -/** set relevance */ -void QuantRelevance::setRelevance(Node s, int r) -{ - if (d_computeRel) - { - int rOld = getRelevance(s); - if (rOld == -1 || r < rOld) - { - d_relevance[s] = r; - if (s.getKind() == FORALL) - { - for (int i = 0; i < (int)d_syms[s].size(); i++) - { - setRelevance(d_syms[s][i], r); - } - } - else - { - for (int i = 0; i < (int)d_syms_quants[s].size(); i++) - { - setRelevance(d_syms_quants[s][i], r + 1); - } - } - } - } -} - } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 75ae32318..21017e783 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -39,7 +39,7 @@ class QuantRelevance : public QuantifiersUtil * if this is false, then all calls to getRelevance * return -1. */ - QuantRelevance(bool cr) : d_computeRel(cr) {} + QuantRelevance() {} ~QuantRelevance() {} /** reset */ bool reset(Theory::Effort e) override { return true; } @@ -47,13 +47,6 @@ class QuantRelevance : public QuantifiersUtil void registerQuantifier(Node q) override; /** identify */ std::string identify() const override { return "QuantRelevance"; } - /** set relevance of symbol s to r */ - void setRelevance(Node s, int r); - /** get relevance of symbol s */ - int getRelevance(Node s) - { - return d_relevance.find(s) == d_relevance.end() ? -1 : d_relevance[s]; - } /** get number of quantifiers for symbol s */ unsigned getNumQuantifiersForSymbol(Node s) { @@ -61,8 +54,6 @@ class QuantRelevance : public QuantifiersUtil } private: - /** for computing relevance */ - bool d_computeRel; /** map from quantifiers to symbols they contain */ std::map<Node, std::vector<Node> > d_syms; /** map from symbols to quantifiers */ diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index d0f156811..d1217d01d 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -42,27 +42,6 @@ void SygusUnif::initializeCandidate( d_strategy[f].initialize(qe, f, enums); } -bool SygusUnif::constructSolution(std::vector<Node>& sols, - std::vector<Node>& lemmas) -{ - // initialize a call to construct solution - initializeConstructSol(); - for (const Node& f : d_candidates) - { - // initialize a call to construct solution for function f - initializeConstructSolFor(f); - // call the virtual construct solution method - Node e = d_strategy[f].getRootEnumerator(); - Node sol = constructSol(f, e, role_equal, 1, lemmas); - if (sol.isNull()) - { - return false; - } - sols.push_back(sol); - } - return true; -} - Node SygusUnif::constructBestSolvedTerm(const std::vector<Node>& solved) { Assert(!solved.empty()); diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index dd6922351..614a29d1c 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -85,7 +85,7 @@ class SygusUnif * channel by the caller. */ virtual bool constructSolution(std::vector<Node>& sols, - std::vector<Node>& lemmas); + std::vector<Node>& lemmas) = 0; protected: /** reference to quantifier engine */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8c43e98ff..a5cd95d29 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -135,7 +135,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; if( options::relevantTriggers() ){ - d_quant_rel = new quantifiers::QuantRelevance(false); + d_quant_rel = new quantifiers::QuantRelevance; d_util.push_back(d_quant_rel); }else{ d_quant_rel = NULL; @@ -563,9 +563,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( e==Theory::EFFORT_LAST_CALL ){ - //if effort is last call, try to minimize model first - //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); - //if( ufss && !ufss->minimize() ){ return; } ++(d_statistics.d_instantiation_rounds_lc); }else if( e==Theory::EFFORT_FULL ){ ++(d_statistics.d_instantiation_rounds); @@ -908,18 +905,6 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within { d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n); } - - // added contains also the Node that just have been asserted in this - // branch - if (d_quant_rel) - { - for (std::set<Node>::iterator i = added.begin(), end = added.end(); - i != end; - i++) - { - d_quant_rel->setRelevance( i->getOperator(), 0 ); - } - } } } } diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 65f7238c9..4efa6c2ce 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -23,7 +23,6 @@ #include "theory/theory_model.h" //#define ONE_SPLIT_REGION -//#define DISABLE_QUICK_CLIQUE_CHECKS //#define COMBINE_REGIONS_SMALL_INTO_LARGE //#define LAZY_REL_EQC @@ -379,21 +378,6 @@ bool Region::check( Theory::Effort level, int cardinality, return false; } -bool Region::getCandidateClique( int cardinality, std::vector< Node >& clique ) -{ - if( d_testCliqueSize>=unsigned(cardinality+1) ){ - //test clique is a clique - for( NodeBoolMap::iterator it = d_testClique.begin(); - it != d_testClique.end(); ++it ){ - if( (*it).second ){ - clique.push_back( (*it).first ); - } - } - return true; - } - return false; -} - void Region::getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ){ for( Region::iterator it = begin(); it != end(); ++it ){ @@ -713,25 +697,16 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){ //see if we have any recommended splits from large regions for( int i=0; i<(int)d_regions_index; i++ ){ if( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){ - //just add the clique lemma - if( level==Theory::EFFORT_FULL && options::ufssCliqueSplits() ){ - std::vector< Node > clique; - if( d_regions[i]->getCandidateClique( d_cardinality, clique ) ){ - //add clique lemma - addCliqueLemma( clique, out ); - return; - } - }else{ - int sp = addSplit( d_regions[i], out ); - if( sp==1 ){ - addedLemma = true; + + int sp = addSplit( d_regions[i], out ); + if( sp==1 ){ + addedLemma = true; #ifdef ONE_SPLIT_REGION - break; + break; #endif - }else if( sp==-1 ){ - check( level, out ); - return; - } + }else if( sp==-1 ){ + check( level, out ); + return; } } } @@ -815,67 +790,6 @@ Node SortModel::getNextDecisionRequest(){ return Node::null(); } -bool SortModel::minimize( OutputChannel* out, TheoryModel* m ){ - if( options::ufssTotality() ){ - //do nothing - }else{ - if( m ){ -#if 0 - // ensure that the constructed model is minimal - // if the model has terms that the strong solver does not know about - if( (int)rs->d_type_reps[ d_type ].size()>d_cardinality ){ - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->getEqualityEngine() ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - if( eqc.getType()==d_type ){ - //we must ensure that this equivalence class has been accounted for - if( d_regions_map.find( eqc )==d_regions_map.end() ){ - //split on unaccounted for term and cardinality lemma term (as default) - Node splitEq = eqc.eqNode( d_cardinality_term ); - splitEq = Rewriter::rewrite( splitEq ); - Trace("uf-ss-minimize") << "Last chance minimize : " << splitEq << std::endl; - out->split( splitEq ); - //tell the sat solver to explore the equals branch first - out->requirePhase( splitEq, true ); - ++( d_thss->d_statistics.d_split_lemmas ); - return false; - } - } - ++eqcs_i; - } - Assert( false ); - } -#endif - }else{ - Trace("uf-ss-debug") << "Minimize the UF model..." << std::endl; - //internal minimize, ensure that model forms a clique: - // if two equivalence classes are neither equal nor disequal, add a split - int validRegionIndex = -1; - for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->valid() ){ - if( validRegionIndex!=-1 ){ - combineRegions( validRegionIndex, i ); - if( addSplit( d_regions[validRegionIndex], out )!=0 ){ - Trace("uf-ss-debug") << "Minimize model : combined regions, found split. " << std::endl; - return false; - } - }else{ - validRegionIndex = i; - } - } - } - Assert( validRegionIndex!=-1 ); - if( addSplit( d_regions[validRegionIndex], out )!=0 ){ - Trace("uf-ss-debug") << "Minimize model : found split. " << std::endl; - return false; - } - Trace("uf-ss-debug") << "Minimize success. " << std::endl; - } - } - return true; -} - - int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){ int ni = d_regions_map[n]; int counter = 0; @@ -950,21 +864,6 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){ } } }else{ - /* - if( options::ufssModelInference() ){ - //check if we are at decision level 0 - if( d_th->d_valuation.getAssertionLevel()==0 ){ - Trace("uf-ss-mi") << "We have proved that no models of size " << c << " for type " << d_type << " exist." << std::endl; - Trace("uf-ss-mi") << " # Clique lemmas : " << d_cliques[c].size() << std::endl; - if( d_cliques[c].size()==1 ){ - if( d_totality_terms[c+1].empty() ){ - Trace("uf-ss-mi") << "*** Establish model" << std::endl; - //d_totality_terms[c+1].insert( d_totality_terms[c].begin(), d_cliques[c][0].begin(), d_cliques[c][0].end() ); - } - } - } - } - */ //see if we need to request a new cardinality if( !d_hasCard ){ bool needsCard = true; @@ -1248,12 +1147,6 @@ void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out while( clique.size()>size_t(d_cardinality+1) ){ clique.pop_back(); } - //debugging information - if( Trace.isOn("uf-ss-cliques") ){ - std::vector< Node > clique_vec; - clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() ); - addClique( d_cardinality, clique_vec ); - } // add as lemma std::vector<Node> eqs; for (unsigned i = 0, size = clique.size(); i < size; i++) @@ -1323,25 +1216,14 @@ void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){ } } -void SortModel::addClique( int c, std::vector< Node >& clique ) { - //if( d_clique_trie[c].add( clique ) ){ - // d_cliques[ c ].push_back( clique ); - //} -} - - /** apply totality */ bool SortModel::applyTotality( int cardinality ){ return options::ufssTotality() || cardinality<=options::ufssTotalityLimited(); - // || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() ); } /** get totality lemma terms */ Node SortModel::getTotalityLemmaTerm( int cardinality, int i ){ return d_totality_terms[0][i]; - //}else{ - // return d_totality_terms[cardinality][i]; - //} } void SortModel::simpleCheckCardinality() { @@ -1909,8 +1791,6 @@ SortModel* StrongSolverTheoryUF::getSortModel( Node n ){ } } -void StrongSolverTheoryUF::notifyRestart(){} - /** get cardinality for sort */ int StrongSolverTheoryUF::getCardinality( Node n ) { SortModel* c = getSortModel( n ); @@ -1929,18 +1809,6 @@ int StrongSolverTheoryUF::getCardinality( TypeNode tn ) { return -1; } -bool StrongSolverTheoryUF::minimize( TheoryModel* m ){ - for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ - if( !it->second->minimize( d_out, m ) ){ - return false; - } - } - for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ - Trace("uf-ss-minimize") << "Cardinality( " << it->first << " ) : " << it->second->getCardinality() << std::endl; - } - return true; -} - //print debug void StrongSolverTheoryUF::debugPrint( const char* c ){ //EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine ); diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 5108e7ba1..2e219da04 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -200,8 +200,6 @@ public: void getNumExternalDisequalities(std::map< Node, int >& num_ext_disequalities ); /** check for cliques */ bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique ); - /** get candidate clique */ - bool getCandidateClique( int cardinality, std::vector< Node >& clique ); //print debug void debugPrint( const char* c, bool incClique = false ); @@ -260,26 +258,6 @@ public: void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ); /** add totality axiom */ void addTotalityAxiom( Node n, int cardinality, OutputChannel* out ); - - class NodeTrie { - public: - bool add( std::vector< Node >& n, unsigned i = 0 ){ - Assert( i<n.size() ); - if( i==(n.size()-1) ){ - bool ret = d_children.find( n[i] )==d_children.end(); - d_children[n[i]].d_children.clear(); - return ret; - }else{ - return d_children[n[i]].add( n, i+1 ); - } - } - private: - std::map< Node, NodeTrie > d_children; - }; /* class NodeTrie */ - - std::map< int, NodeTrie > d_clique_trie; - void addClique( int c, std::vector< Node >& clique ); - /** Are we in conflict */ context::CDO<bool> d_conflict; /** cardinality */ @@ -338,8 +316,6 @@ public: void propagate( Theory::Effort level, OutputChannel* out ); /** get next decision request */ Node getNextDecisionRequest(); - /** minimize */ - bool minimize( OutputChannel* out, TheoryModel* m ); /** assert cardinality */ void assertCardinality( OutputChannel* out, int c, bool val ); /** is in conflict */ @@ -393,8 +369,6 @@ public: Node getNextDecisionRequest( unsigned& priority ); /** preregister a term */ void preRegisterTerm( TNode n ); - /** notify restart */ - void notifyRestart(); /** identify */ std::string identify() const { return std::string("StrongSolverTheoryUF"); } //print debug @@ -407,8 +381,6 @@ public: int getCardinality( Node n ); /** get cardinality for type */ int getCardinality( TypeNode tn ); - /** minimize */ - bool minimize( TheoryModel* m = NULL ); /** has eqc */ bool hasEqc(Node a); diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index a4d318067..ea3a70362 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -155,6 +155,8 @@ REG0_TESTS = \ regress0/bug605.cvc \ regress0/bug639.smt2 \ regress0/buggy-ite.smt2 \ + regress0/bv/ackermann1.smt2 \ + regress0/bv/ackermann2.smt2 \ regress0/bv/bool-to-bv.smt2 \ regress0/bv/bug260a.smt \ regress0/bv/bug260b.smt \ @@ -1280,6 +1282,7 @@ REG1_TESTS = \ regress1/quantifiers/constfunc.cvc \ regress1/quantifiers/dump-inst.smt2 \ regress1/quantifiers/dump-inst-i.smt2 \ + regress1/quantifiers/dump-inst-proof.smt2 \ regress1/quantifiers/ext-ex-deq-trigger.smt2 \ regress1/quantifiers/extract-nproc.smt2 \ regress1/quantifiers/florian-case-ax.smt2 \ @@ -1293,6 +1296,7 @@ REG1_TESTS = \ regress1/quantifiers/isaplanner-goal20.smt2 \ regress1/quantifiers/is-even.smt2 \ regress1/quantifiers/javafe.ast.StmtVec.009.smt2 \ + regress1/quantifiers/lra-vts-inf.smt2 \ regress1/quantifiers/mix-coeff.smt2 \ regress1/quantifiers/model_6_1_bv.smt2 \ regress1/quantifiers/mutualrec2.cvc \ @@ -1321,6 +1325,8 @@ REG1_TESTS = \ regress1/quantifiers/qbv-test-urem-rewrite.smt2 \ regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \ regress1/quantifiers/qcft-smtlib3dbc51.smt2 \ + regress1/quantifiers/qe.smt2 \ + regress1/quantifiers/qe-partial.smt2 \ regress1/quantifiers/quant-wf-int-ind.smt2 \ regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \ regress1/quantifiers/repair-const-nterm.smt2 \ diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2 new file mode 100644 index 000000000..9b96b38c4 --- /dev/null +++ b/test/regress/regress0/bv/ackermann1.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFBV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v0 () (_ BitVec 4)) +(declare-fun f ((_ BitVec 4)) (_ BitVec 4)) +(declare-fun g ((_ BitVec 4)) (_ BitVec 4)) + +(assert (= (f (f v0)) (g (f v0)))) + + +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2 new file mode 100644 index 000000000..eeca505fe --- /dev/null +++ b/test/regress/regress0/bv/ackermann2.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFBV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v0 () (_ BitVec 4)) +(declare-fun v1 () (_ BitVec 4)) +(declare-fun f ((_ BitVec 4)) (_ BitVec 4)) +(declare-fun g ((_ BitVec 4)) (_ BitVec 4)) +(declare-fun h ((_ BitVec 4)) (_ BitVec 4)) + +(assert (not (= (f (g (h v0))) (f (g (h v1)))))) +(assert (= v0 v1)) + + +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 new file mode 100644 index 000000000..c4eedc16f --- /dev/null +++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --dump-instantiations --proof +; EXPECT: unsat +; EXPECT: (instantiation (forall ((x Int)) (or (P x) (Q x)) ) +; EXPECT: ( 2 ) +; EXPECT: ) +; EXPECT: (instantiation (forall ((x Int)) (or (not (S x)) (not (Q x))) ) +; EXPECT: ( 2 ) +; EXPECT: ) +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) +(declare-fun Q (Int) Bool) +(declare-fun R (Int) Bool) +(declare-fun S (Int) Bool) +(declare-fun W (Int) Bool) +(declare-fun U (Int) Bool) +(assert (forall ((x Int)) (or (P x) (Q x)))) +(assert (forall ((x Int)) (or (R x) (W x)))) +(assert (forall ((x Int)) (or (S x) (U x)))) +(assert (forall ((x Int)) (or (not (S x)) (not (Q x))))) +(assert (and (not (R 0)) (not (R 10)) (not (S 1)) (not (P 2)))) +(assert (S 2)) +; This tests that --proof minimizes the instantiations printed out. +; This regression should require only the 2 instantiations above, but +; may try more. +(check-sat) diff --git a/test/regress/regress1/quantifiers/lra-vts-inf.smt2 b/test/regress/regress1/quantifiers/lra-vts-inf.smt2 new file mode 100644 index 000000000..22d6455fb --- /dev/null +++ b/test/regress/regress1/quantifiers/lra-vts-inf.smt2 @@ -0,0 +1,144 @@ +; COMMAND-LINE: --cbqi-use-inf-int --cbqi-use-inf-real +; EXPECT: unsat +(set-info :smt-lib-version 2.6) +(set-logic LRA) +(set-info :source | + Monniaux, David; Quantifier Elimination by Lazy Model Enumeration, CAV 2010 +|) +(set-info :category "random") +; ./Mjollnir_examples/B5/formula_171.m +(set-info :status unsat) +(assert + (forall ((|v17:0| Real) )(forall ((|v16:1| Real) )(forall ((|v15:2| Real) )(forall ((|v14:3| Real) )(forall ((|v13:4| Real) )(forall ((|v12:5| Real) )(exists ((|v11:6| Real) )(exists ((|v10:7| Real) )(exists ((|v9:8| Real) )(exists ((|v8:9| Real) )(exists ((|v7:10| Real) )(exists ((|v6:11| Real) )(forall ((|v5:12| Real) )(forall ((|v4:13| Real) )(forall ((|v3:14| Real) )(forall ((|v2:15| Real) )(forall ((|v1:16| Real) )(forall ((|v0:17| Real) )(let ((?x104 10)) +(let ((?x10 8)) +(let ((?x457 (* ?x10 |v0:17|))) +(let ((?x538 (+ (+ (* (- 7) |v5:12|) (* 14 |v10:7|)) (* (- 19) |v15:2|)))) +(let ((?x49 19)) +(let ((?x27 (- 15))) +(let ((?x310 (* ?x27 |v10:7|))) +(let ((?x532 (+ (+ (+ (* 7 |v12:5|) (* (- 20) |v4:13|)) ?x310) (* 20 |v16:1|)))) +(let ((?x59 (- 16))) +(let ((?x85 (- 13))) +(let ((?x187 (* ?x85 |v3:14|))) +(let ((?x524 (+ (+ (* (- 20) |v5:12|) (* 4 |v13:4|)) (* (- 10) |v2:15|)))) +(let ((?x266 18)) +(let ((?x170 (- 14))) +(let ((?x308 (* ?x170 |v16:1|))) +(let ((?x520 (+ (+ (+ (* (- 19) |v2:15|) (* 13 |v7:10|)) ?x308) (* (- 12) |v1:16|)))) +(let (($x542 (and (and (<= ?x520 ?x266) (<= (+ ?x524 ?x187) ?x59)) (and (<= ?x532 ?x49) (<= (+ ?x538 ?x457) ?x104))))) +(let ((?x158 (- 11))) +(let ((?x79 6)) +(let ((?x290 (* ?x79 |v3:14|))) +(let ((?x512 (+ (+ (+ (* (- 8) |v9:8|) (* (- 9) |v0:17|)) ?x290) (* (- 18) |v8:9|)))) +(let ((?x504 (+ (+ (* (- 18) |v12:5|) (* (- 18) |v10:7|)) (* 15 |v5:12|)))) +(let ((?x14 (- 18))) +(let ((?x100 7)) +(let ((?x471 (* ?x100 |v6:11|))) +(let (($x499 (<= (+ (+ (+ (* (- 8) |v6:11|) (* ?x100 |v2:15|)) |v17:0|) ?x471) ?x14))) +(let ((?x177 (- 3))) +(let ((?x490 (+ (+ (* (- 19) |v14:3|) (* (- 8) |v13:4|)) (* ?x158 |v16:1|)))) +(let (($x515 (and (or (<= (+ ?x490 (* (- 7) |v10:7|)) ?x177) $x499) (or (<= (+ ?x504 (* ?x79 |v0:17|)) ?x266) (<= ?x512 ?x158))))) +(let ((?x479 (+ (+ (* 13 |v4:13|) (* (- 17) |v4:13|)) (* 11 |v3:14|)))) +(let ((?x110 3)) +(let ((?x33 (* ?x14 |v9:8|))) +(let (($x474 (<= (+ (+ (+ (* ?x110 |v0:17|) (* 16 |v7:10|)) ?x471) ?x33) ?x110))) +(let ((?x233 1)) +(let ((?x464 (+ (+ (* ?x158 |v17:0|) (* 4 |v4:13|)) (* (- 5) |v8:9|)))) +(let ((?x24 12)) +(let ((?x458 (+ (+ (+ (* (- 12) |v5:12|) (* 14 |v16:1|)) |v3:14|) ?x457))) +(let (($x484 (or (and (<= ?x458 ?x24) (<= (+ ?x464 (* (- 12) |v4:13|)) ?x233)) (and $x474 (<= (+ ?x479 (* (- 4) |v12:5|)) ?x59))))) +(let ((?x447 (+ (+ (* (- 20) |v14:3|) (* (- 19) |v16:1|)) (* 2 |v2:15|)))) +(let ((?x439 (+ (+ (* ?x10 |v13:4|) (* 4 |v13:4|)) (* (- 7) |v11:6|)))) +(let (($x451 (or (<= (+ ?x439 (* (- 5) |v7:10|)) ?x24) (<= (+ ?x447 (* ?x170 |v14:3|)) ?x110)))) +(let ((?x62 (- 17))) +(let ((?x430 (+ (+ (* (- 1) |v11:6|) (* 5 |v14:3|)) (* ?x104 |v17:0|)))) +(let ((?x190 11)) +(let ((?x424 (+ (+ (+ (* ?x190 |v5:12|) (* (- 10) |v5:12|)) (* ?x27 |v14:3|)) (* 2 |v12:5|)))) +(let (($x485 (or (and (and (<= ?x424 ?x190) (<= (+ ?x430 (* ?x24 |v16:1|)) ?x62)) $x451) $x484))) +(let ((?x164 4)) +(let ((?x415 (+ (+ (* ?x104 |v15:2|) (* (- 6) |v7:10|)) (* 17 |v1:16|)))) +(let ((?x407 (+ (+ (+ (* ?x59 |v11:6|) (* ?x10 |v14:3|)) (* ?x10 |v7:10|)) (* (- 6) |v8:9|)))) +(let ((?x52 16)) +(let ((?x395 (+ (+ (* (- 5) |v12:5|) (* ?x104 |v15:2|)) (* (- 7) |v1:16|)))) +(let ((?x121 (- 8))) +(let ((?x389 (+ (+ (+ (* (- 9) |v13:4|) (* ?x110 |v0:17|)) (* ?x59 |v17:0|)) (* ?x190 |v4:13|)))) +(let ((?x346 (* ?x27 |v16:1|))) +(let ((?x381 (+ (+ (+ (* ?x158 |v12:5|) (* ?x121 |v16:1|)) (* 5 |v0:17|)) ?x346))) +(let (($x410 (and (or (<= ?x381 ?x104) (<= ?x389 ?x121)) (or (<= (+ ?x395 (* 9 |v9:8|)) ?x52) (<= ?x407 ?x110))))) +(let ((?x370 (+ (+ (* (- 2) |v14:3|) (* (- 1) |v15:2|)) (* ?x85 |v6:11|)))) +(let ((?x97 (- 2))) +(let ((?x361 (+ (+ (* ?x27 |v15:2|) (* (- 20) |v4:13|)) (* 20 |v9:8|)))) +(let (($x374 (or (<= (+ ?x361 (* (- 9) |v7:10|)) ?x97) (<= (+ ?x370 (* (- 19) |v17:0|)) ?x52)))) +(let ((?x195 20)) +(let ((?x354 (+ (+ (+ (* ?x49 |v11:6|) (* ?x59 |v2:15|)) (* 17 |v8:9|)) |v17:0|))) +(let ((?x347 (+ (+ (+ (* (- 7) |v7:10|) (* ?x104 |v10:7|)) (* ?x104 |v6:11|)) ?x346))) +(let (($x419 (or (and (or (or (<= ?x347 ?x100) (<= ?x354 ?x195)) $x374) $x410) (<= (+ ?x415 (* ?x27 |v1:16|)) ?x164)))) +(let ((?x151 (- 20))) +(let ((?x333 (* ?x151 |v5:12|))) +(let (($x335 (<= (+ (+ (+ (* ?x104 |v9:8|) (* ?x151 |v3:14|)) (* ?x110 |v13:4|)) ?x333) ?x151))) +(let ((?x327 (+ (+ (+ (* ?x158 |v5:12|) (* ?x266 |v14:3|)) (* (- 12) |v14:3|)) (* 5 |v1:16|)))) +(let ((?x314 (* ?x14 |v13:4|))) +(let (($x319 (<= (+ (+ (+ (* (- 19) |v4:13|) ?x314) (* ?x62 |v15:2|)) ?x314) ?x164))) +(let ((?x311 (+ (+ (+ (* (- 19) |v6:11|) (* 17 |v0:17|)) ?x308) ?x310))) +(let ((?x302 (+ (+ (+ (* ?x121 |v9:8|) (* ?x97 |v3:14|)) (* ?x59 |v11:6|)) (* ?x158 |v9:8|)))) +(let ((?x135 (- 10))) +(let ((?x293 (+ (+ (+ (* ?x27 |v14:3|) (* ?x190 |v7:10|)) ?x290) (* (- 5) |v3:14|)))) +(let ((?x88 (- 5))) +(let (($x288 (<= (+ (+ (+ (* ?x177 |v1:16|) (* ?x135 |v4:13|)) (* ?x135 |v7:10|)) |v14:3|) ?x88))) +(let (($x338 (and (and (and $x288 (<= ?x293 ?x135)) (<= ?x302 ?x59)) (and (or (<= ?x311 ?x158) $x319) (or (<= ?x327 ?x233) $x335))))) +(let ((?x278 (+ (+ (+ (* ?x27 |v12:5|) (* ?x85 |v9:8|)) (* ?x49 |v5:12|)) (* ?x49 |v15:2|)))) +(let ((?x270 (+ (+ (+ (* ?x10 |v14:3|) (* 17 |v6:11|)) (* ?x266 |v7:10|)) (* ?x24 |v9:8|)))) +(let ((?x41 (- 4))) +(let ((?x259 (+ (+ (+ (* ?x100 |v8:9|) (* ?x177 |v6:11|)) (* 2 |v4:13|)) (* 13 |v12:5|)))) +(let ((?x249 (+ (+ (* 13 |v1:16|) (* ?x151 |v3:14|)) (* 17 |v15:2|)))) +(let (($x281 (and (and (<= (+ ?x249 (* ?x62 |v1:16|)) ?x110) (<= ?x259 ?x41)) (and (<= ?x270 ?x104) (<= ?x278 ?x24))))) +(let ((?x228 15)) +(let ((?x241 (+ (+ (+ (* ?x88 |v5:12|) (* ?x49 |v10:7|)) (* ?x27 |v14:3|)) (* 17 |v7:10|)))) +(let ((?x232 (+ (+ (+ (* ?x24 |v17:0|) (* ?x135 |v4:13|)) (* ?x228 |v17:0|)) (* ?x88 |v1:16|)))) +(let ((?x117 (- 19))) +(let ((?x220 (* ?x117 |v2:15|))) +(let (($x222 (<= (+ (+ (+ (* ?x121 |v17:0|) (* ?x190 |v5:12|)) (* ?x190 |v7:10|)) ?x220) ?x104))) +(let ((?x114 (- 1))) +(let ((?x115 (* ?x114 |v1:16|))) +(let ((?x212 (+ (+ (* 0 |v15:2|) (* 5 |v8:9|)) (* ?x110 |v10:7|)))) +(let (($x244 (and (and (<= (+ ?x212 ?x115) ?x10) $x222) (and (<= ?x232 ?x233) (<= ?x241 ?x228))))) +(let ((?x128 2)) +(let ((?x202 (+ (+ (+ (* ?x195 |v10:7|) (* ?x121 |v10:7|)) (* ?x135 |v4:13|)) (* 17 |v12:5|)))) +(let (($x193 (<= (+ (+ (+ (* ?x151 |v12:5|) (* ?x114 |v4:13|)) ?x187) (* ?x190 |v12:5|)) ?x110))) +(let ((?x181 (+ (+ (+ (* ?x110 |v6:11|) (* ?x164 |v15:2|)) (* ?x177 |v11:6|)) (* ?x10 |v9:8|)))) +(let (($x173 (<= (+ (+ (+ (* ?x164 |v10:7|) |v9:8|) (* ?x104 |v5:12|)) (* ?x170 |v6:11|)) ?x24))) +(let ((?x161 14)) +(let ((?x160 (+ (+ (+ (* ?x151 |v8:9|) (* ?x128 |v16:1|)) (* ?x14 |v12:5|)) (* ?x158 |v0:17|)))) +(let (($x206 (and (<= ?x160 ?x161) (or (or $x173 (<= ?x181 ?x158)) (and $x193 (<= ?x202 ?x128)))))) +(let ((?x144 (+ (+ (+ (* ?x135 |v1:16|) (* ?x14 |v4:13|)) (* ?x10 |v12:5|)) (* 0 |v17:0|)))) +(let ((?x132 (+ (+ (+ (* ?x121 |v8:9|) (* 5 |v17:0|)) (* ?x128 |v13:4|)) (* 13 |v13:4|)))) +(let (($x118 (<= (+ (+ (+ (* ?x104 |v15:2|) (* ?x41 |v7:10|)) (* ?x110 |v6:11|)) ?x115) ?x117))) +(let ((?x98 (* ?x97 |v14:3|))) +(let ((?x99 (+ (+ (+ (* ?x85 |v17:0|) (* ?x88 |v15:2|)) (* 0 |v1:16|)) ?x98))) +(let ((?x78 (+ (+ (+ (* ?x14 |v7:10|) (* (- 7) |v0:17|)) |v3:14|) (* (- 12) |v17:0|)))) +(let ((?x61 (+ (+ (+ (* ?x49 |v8:9|) (* ?x52 |v10:7|)) (* ?x24 |v1:16|)) (* ?x59 |v1:16|)))) +(let ((?x36 13)) +(let (($x44 (<= (+ (+ (+ (* ?x10 |v11:6|) ?x33) (* ?x36 |v15:2|)) (* ?x41 |v2:15|)) ?x36))) +(let ((?x26 (+ (+ (+ (* ?x10 |v16:1|) (* ?x14 |v5:12|)) (* 17 |v10:7|)) (* ?x24 |v13:4|)))) +(let (($x148 (or (and (and (<= ?x26 ?x27) $x44) (and (<= ?x61 ?x62) (<= ?x78 ?x79))) (or (and (<= ?x99 ?x100) $x118) (and (<= ?x132 ?x41) (<= ?x144 ?x104)))))) +(or (and (and $x148 $x206) (and (or $x244 $x281) $x338)) (and $x419 (or $x485 (and $x515 $x542))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +) +) +) +) +) +) +) +) +) +) +) +) +) +) +) +) +) +) +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/qe-partial.smt2 b/test/regress/regress1/quantifiers/qe-partial.smt2 new file mode 100644 index 000000000..6f414fb2c --- /dev/null +++ b/test/regress/regress1/quantifiers/qe-partial.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: +; SCRUBBER: sed -e 's/(not (>= (+ .* (\* (- 1) .*)) 1))$/(not (>= (+ TERMA (\* (- 1) TERMB)) 1))/' +; EXPECT: (not (>= (+ TERMA (* (- 1) TERMB)) 1)) +(set-logic LIA) +(set-info :status unsat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(get-qe-disjunct (exists ((x Int)) (and (<= a x) (or (<= x b) (<= x c))))) diff --git a/test/regress/regress1/quantifiers/qe.smt2 b/test/regress/regress1/quantifiers/qe.smt2 new file mode 100644 index 000000000..673ece05b --- /dev/null +++ b/test/regress/regress1/quantifiers/qe.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: +; EXPECT: (not (>= (+ a (* (- 1) b)) 1)) +(set-logic LIA) +(set-info :status unsat) +(declare-fun a () Int) +(declare-fun b () Int) +(get-qe (exists ((x Int)) (and (<= a x) (<= x b)))) |