From 113e7001e03ec7d1c2b79e0bb2cc9b762519bc22 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 1 Aug 2018 16:08:47 -0700 Subject: Fix wrong evaluation of STRING_STOI (#2252) --- src/theory/evaluator.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index dd40ace8a..02083069d 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -434,11 +434,11 @@ EvalResult Evaluator::evalInternal(TNode n, const String& s = results[currNode[0]].d_str; if (s.isNumber()) { - results[currNode] = EvalResult(Rational(-1)); + results[currNode] = EvalResult(Rational(s.toNumber())); } else { - results[currNode] = EvalResult(Rational(s.toNumber())); + results[currNode] = EvalResult(Rational(-1)); } break; } -- cgit v1.2.3 From 7b815181bfd58100478970f52b80461638fd42a8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Aug 2018 19:10:47 -0500 Subject: Fix issues with printing parametric datatypes in smt2 (#2213) --- src/expr/expr_manager_template.cpp | 9 +++-- src/expr/expr_manager_template.h | 3 +- src/expr/node_manager.cpp | 6 ++-- src/expr/node_manager.h | 6 ++-- src/parser/parser.cpp | 14 +++++--- src/parser/parser.h | 5 ++- src/parser/smt2/Smt2.g | 4 +-- src/printer/smt2/smt2_printer.cpp | 73 +++++++++++++++++++++++++++++++++++++- src/smt/smt_engine.cpp | 7 ++-- 9 files changed, 108 insertions(+), 19 deletions(-) diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 457e54d9b..de128b3e5 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -831,10 +831,13 @@ SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const { } SortConstructorType ExprManager::mkSortConstructor(const std::string& name, - size_t arity) const { + size_t arity, + uint32_t flags) const +{ NodeManagerScope nms(d_nodeManager); - return SortConstructorType(Type(d_nodeManager, - new TypeNode(d_nodeManager->mkSortConstructor(name, arity)))); + return SortConstructorType( + Type(d_nodeManager, + new TypeNode(d_nodeManager->mkSortConstructor(name, arity, flags)))); } /** diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index f211aa4c8..a9cdfc587 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -434,7 +434,8 @@ public: /** Make a sort constructor from a name and arity. */ SortConstructorType mkSortConstructor(const std::string& name, - size_t arity) const; + size_t arity, + uint32_t flags = SORT_FLAG_NONE) const; /** * Get the type of an expression. diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index d03bc4b54..74701cf11 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -645,7 +645,9 @@ TypeNode NodeManager::mkSort(TypeNode constructor, } TypeNode NodeManager::mkSortConstructor(const std::string& name, - size_t arity) { + size_t arity, + uint32_t flags) +{ Assert(arity > 0); NodeBuilder<> nb(this, kind::SORT_TYPE); Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); @@ -654,7 +656,7 @@ TypeNode NodeManager::mkSortConstructor(const std::string& name, setAttribute(type, expr::VarNameAttr(), name); setAttribute(type, expr::SortArityAttr(), arity); for(std::vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSortConstructor(type); + (*i)->nmNotifyNewSortConstructor(type, flags); } return type; } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 996caad87..71082ef9d 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -60,7 +60,7 @@ class NodeManagerListener { public: virtual ~NodeManagerListener() {} virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) {} - virtual void nmNotifyNewSortConstructor(TypeNode tn) {} + virtual void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) {} virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) {} virtual void nmNotifyNewDatatypes( @@ -875,7 +875,9 @@ public: uint32_t flags = ExprManager::SORT_FLAG_NONE); /** Make a new sort with the given name and arity. */ - TypeNode mkSortConstructor(const std::string& name, size_t arity); + TypeNode mkSortConstructor(const std::string& name, + size_t arity, + uint32_t flags = ExprManager::SORT_FLAG_NONE); /** * Get the type for the given node and optionally do type checking. diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 1f9c3fd2b..47124a589 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -324,10 +324,13 @@ SortType Parser::mkSort(const std::string& name, uint32_t flags) { } SortConstructorType Parser::mkSortConstructor(const std::string& name, - size_t arity) { + size_t arity, + uint32_t flags) +{ Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - SortConstructorType type = d_exprManager->mkSortConstructor(name, arity); + SortConstructorType type = + d_exprManager->mkSortConstructor(name, arity, flags); defineType(name, vector(arity), type); return type; } @@ -340,7 +343,8 @@ SortType Parser::mkUnresolvedType(const std::string& name) { SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name, size_t arity) { - SortConstructorType unresolved = mkSortConstructor(name, arity); + SortConstructorType unresolved = + mkSortConstructor(name, arity, ExprManager::SORT_FLAG_PLACEHOLDER); d_unresolved.insert(unresolved); return unresolved; } @@ -349,8 +353,8 @@ SortConstructorType Parser::mkUnresolvedTypeConstructor( const std::string& name, const std::vector& params) { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - SortConstructorType unresolved = - d_exprManager->mkSortConstructor(name, params.size()); + SortConstructorType unresolved = d_exprManager->mkSortConstructor( + name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER); defineType(name, params, unresolved); Type t = getSort(name, params); d_unresolved.insert(unresolved); diff --git a/src/parser/parser.h b/src/parser/parser.h index 769f4c812..78cbcaafb 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -540,7 +540,10 @@ public: /** * Creates a new sort constructor with the given name and arity. */ - SortConstructorType mkSortConstructor(const std::string& name, size_t arity); + SortConstructorType mkSortConstructor( + const std::string& name, + size_t arity, + uint32_t flags = ExprManager::SORT_FLAG_NONE); /** * Creates a new "unresolved type," used only during parsing. diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index b52be77bb..d3bec9d42 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1479,7 +1479,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr* cmd] PARSER_STATE->pushScope(true); } LPAREN_TOK /* parametric sorts */ ( symbol[name,CHECK_UNDECLARED,SYM_SORT] - { sorts.push_back( PARSER_STATE->mkSort(name) ); } + { sorts.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); } )* RPAREN_TOK LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK @@ -1550,7 +1550,7 @@ datatypesDef[bool isCo, } ( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] - { params.push_back( PARSER_STATE->mkSort(name) ); } + { params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); } )* RPAREN_TOK { // if the arity was fixed by prelude and is not equal to the number of parameters diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 64a52c23f..9c3bdc539 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -836,6 +836,18 @@ void Smt2Printer::toStream(std::ostream& out, // APPLY_UF, APPLY_CONSTRUCTOR, etc. Assert( n.hasOperator() ); TypeNode opt = n.getOperator().getType(); + if (n.getKind() == kind::APPLY_CONSTRUCTOR) + { + Type tn = n.getType().toType(); + // may be parametric, in which case the constructor type must be + // specialized + const Datatype& dt = static_cast(tn).getDatatype(); + if (dt.isParametric()) + { + unsigned ci = Datatype::indexOf(n.getOperator().toExpr()); + opt = TypeNode::fromType(dt[ci].getSpecializedConstructorType(tn)); + } + } Assert( opt.getNumChildren() == n.getNumChildren() + 1 ); for(size_t i = 0; i < n.getNumChildren(); ++i ) { force_child_type[i] = opt[i]; @@ -1908,15 +1920,74 @@ static void toStream(std::ostream& out, ++i) { const Datatype& d = i->getDatatype(); + if (d.isParametric()) + { + out << "(par ("; + for (unsigned p = 0, nparam = d.getNumParameters(); p < nparam; p++) + { + out << (p > 0 ? " " : "") << d.getParameter(p); + } + out << ")"; + } out << "("; toStream(out, d); out << ")"; + if (d.isParametric()) + { + out << ")"; + } } out << ")"; } else { - out << " () ("; + out << " ("; + // Can only print if all datatypes in this block have the same parameters. + // In theory, given input language 2.6 and output language 2.5, it could + // be impossible to print a datatype block where datatypes were given + // different parameter lists. + bool success = true; + const Datatype& d = datatypes[0].getDatatype(); + unsigned nparam = d.getNumParameters(); + for (unsigned j = 1, ndt = datatypes.size(); j < ndt; j++) + { + const Datatype& dj = datatypes[j].getDatatype(); + if (dj.getNumParameters() != nparam) + { + success = false; + } + else + { + // must also have identical parameter lists + for (unsigned k = 0; k < nparam; k++) + { + if (dj.getParameter(k) != d.getParameter(k)) + { + success = false; + break; + } + } + } + if (!success) + { + break; + } + } + if (success) + { + for (unsigned j = 0; j < nparam; j++) + { + out << (j > 0 ? " " : "") << d.getParameter(j); + } + } + else + { + out << std::endl; + out << "ERROR: datatypes in each block must have identical parameter " + "lists."; + out << std::endl; + } + out << ") ("; for (vector::const_iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cfafd63c4..116d2fe23 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -759,12 +759,15 @@ public: } } - void nmNotifyNewSortConstructor(TypeNode tn) override + void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), tn.getAttribute(expr::SortArityAttr()), tn.toType()); - d_smt.addToModelCommandAndDump(c); + if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) + { + d_smt.addToModelCommandAndDump(c); + } } void nmNotifyNewDatatypes(const std::vector& dtts) override -- cgit v1.2.3 From 551f82a1398c97a5cd1f75b2c411b6fe464cc6ec Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 1 Aug 2018 18:07:34 -0700 Subject: Remove outdated references to TLS (#2245) --- AUTHORS | 10 ++-------- contrib/depgraph | 1 - src/base/configuration.cpp | 4 ---- src/base/configuration.h | 2 -- src/base/configuration_private.h | 6 ------ src/options/options_handler.cpp | 1 - src/smt/smt_engine_scope.cpp | 1 - 7 files changed, 2 insertions(+), 23 deletions(-) diff --git a/AUTHORS b/AUTHORS index 1d4a67e5b..7f056c0e6 100644 --- a/AUTHORS +++ b/AUTHORS @@ -37,14 +37,8 @@ CVC4 contains MiniSAT code by Niklas Een and Niklas Sorensson. The CVC4 parser incorporates some code from ANTLR3, by Jim Idle, Temporal Wave LLC. -CVC4 contains the doxygen.m4 autoconf module by Oren Ben-Kiki. - -CVC4 contains the pkg.m4 autoconf module by Scott James Remnant. - -CVC4 contains the ax_tls.m4 autoconf module by Alan Woodland and Diego Elio -Petteno`. - -CVC4 contains the boost.m4 autoconf module by Benoit Sigoure. +CVC4 contains various autoconf modules in the config directory. Please refer to +the individual files for more information on the authors. CVC4 maintainer versions contain the script autogen.sh by Christopher Sean Morrison, and copyright U.S. Army Research Laboratory. diff --git a/contrib/depgraph b/contrib/depgraph index 2c4eba595..b0e650f40 100755 --- a/contrib/depgraph +++ b/contrib/depgraph @@ -88,7 +88,6 @@ for path in $paths; do if [ -n "$target" -a "$target" != "$package" ]; then continue; fi for inc in $incs; do case "$inc" in - base/tls.h) inc=base/tls.h.in ;; expr/expr.h) inc=expr/expr_template.h ;; expr/expr_manager.h) inc=expr/expr_manager_template.h ;; expr/kind.h) inc=expr/kind_template.h ;; diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 68a6ebdb7..1a53ccfe9 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -254,10 +254,6 @@ bool Configuration::isBuiltWithReadline() { return IS_READLINE_BUILD; } -bool Configuration::isBuiltWithTlsSupport() { - return USING_TLS; -} - bool Configuration::isBuiltWithLfsc() { return IS_LFSC_BUILD; } diff --git a/src/base/configuration.h b/src/base/configuration.h index 8b92a6c67..16c6d7f0d 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -101,8 +101,6 @@ public: static bool isBuiltWithReadline(); - static bool isBuiltWithTlsSupport(); - static bool isBuiltWithLfsc(); static bool isBuiltWithSymFPU(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 106b1ff58..e2974260c 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -150,12 +150,6 @@ namespace CVC4 { # define IS_GPL_BUILD false #endif /* CVC4_GPL_DEPS */ -#ifdef TLS -# define USING_TLS true -#else /* TLS */ -# define USING_TLS false -#endif /* TLS */ - }/* CVC4 namespace */ #endif /* __CVC4__CONFIGURATION_PRIVATE_H */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index b0e46d8cc..e6b5c3204 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1666,7 +1666,6 @@ void OptionsHandler::showConfiguration(std::string option) { print_config_cond("lfsc", Configuration::isBuiltWithLfsc()); print_config_cond("readline", Configuration::isBuiltWithReadline()); print_config_cond("symfpu", Configuration::isBuiltWithSymFPU()); - print_config_cond("tls", Configuration::isBuiltWithTlsSupport()); exit(0); } diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 7166f0ade..288a07bde 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -21,7 +21,6 @@ #include "base/configuration_private.h" #include "base/cvc4_assert.h" #include "base/output.h" -#include "base/tls.h" #include "proof/proof.h" #include "smt/smt_engine.h" -- cgit v1.2.3 From ea426344ed44b28dcdbe4e631b52250ecef0551f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Aug 2018 21:24:42 -0500 Subject: Improvements and fixes in cegqi arithmetic (#2247) This includes several improvements for cegqi with arithmetic: - Randomly choose either lower or upper bounds instead of always using lower bounds (this is similar to cegqi+BV), - Equalities are handled by processAssertions, - Resort to *only* model values at full effort instead of trying to mix model values/bounds (this is also similar to cegqi+BV), - cegqi+arithmetic does not try multiple instantiations unless the flag cbqiMultiInst is set. This makes it so that ceg_instantiator does not have exponential behavior when the strategy is non-monotonic. It also includes a core fix to computing what bound is optimal based on an ordering that incorporates virtual terms. Previously, we would consider, e.g.: `a+b*delta > c+d*delta if a>=c and b>=d` Whereas the correct check is lexicographic: `a+b*delta > c+d*delta if a>c or a=c and b>d` This means e.g. 2+(-1)*delta > 3 was previously wrongly inferred. This is part of merging https://github.com/ajreynol/CVC4/tree/cegqiSingleInst, which is +3-0 on SMTLIB BV and +12-9 on SMTLIB LIA+LRA+NRA+NIA. --- .../quantifiers/cegqi/ceg_arith_instantiator.cpp | 61 +++++++++++++++++----- test/regress/Makefile.tests | 2 + .../quantifiers/RND_4_1-existing-inst.smt2 | 15 ++++++ .../regress1/quantifiers/repair-const-nterm.smt2 | 12 +++++ 4 files changed, 78 insertions(+), 12 deletions(-) create mode 100644 test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 create mode 100644 test/regress/regress1/quantifiers/repair-const-nterm.smt2 diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 5cd7a6892..f1235d185 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -20,6 +20,7 @@ #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/term_util.h" +#include "util/random.h" using namespace std; using namespace CVC4::kind; @@ -118,7 +119,7 @@ bool ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, Node pv, CegInstEffort effort) { - return true; + return effort != CEG_INST_EFFORT_FULL; } Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, @@ -128,10 +129,9 @@ Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, CegInstEffort effort) { Node atom = lit.getKind() == NOT ? lit[0] : lit; - bool pol = lit.getKind() != NOT; // arithmetic inequalities and disequalities if (atom.getKind() == GEQ - || (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal())) + || (atom.getKind() == EQUAL && atom[0].getType().isReal())) { return lit; } @@ -150,7 +150,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, bool pol = lit.getKind() != NOT; // arithmetic inequalities and disequalities Assert(atom.getKind() == GEQ - || (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal())); + || (atom.getKind() == EQUAL && atom[0].getType().isReal())); // get model value for pv Node pv_value = ci->getModelValue(pv); // cannot contain infinity? @@ -165,8 +165,12 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, { return false; } - // disequalities are either strict upper or lower bounds - unsigned rmax = (atom.getKind() == GEQ || options::cbqiModel()) ? 1 : 2; + // compute how many bounds we will consider + unsigned rmax = 1; + if (atom.getKind() == EQUAL && (pol || !options::cbqiModel())) + { + rmax = 2; + } for (unsigned r = 0; r < rmax; r++) { int uires = ires; @@ -190,8 +194,14 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, } } } + else if (pol) + { + // equalities are both non-strict upper and lower bounds + uires = r == 0 ? 1 : -1; + } else { + // disequalities are either strict upper or lower bounds bool is_upper; if (options::cbqiModel()) { @@ -226,11 +236,12 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value); cmp = Rewriter::rewrite(cmp); Assert(cmp.isConst()); - is_upper = (cmp != ci->getQuantifiersEngine()->getTermUtil()->d_true); + is_upper = !cmp.isConst() || !cmp.getConst(); } } else { + // since we are not using the model, we try both. is_upper = (r == 0); } Assert(atom.getKind() == EQUAL && !pol); @@ -319,7 +330,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, bool use_inf = ci->useVtsInfinity() && (d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal()); - bool upper_first = false; + bool upper_first = Random::getRandom().pickWithProb(0.5); if (options::cbqiMinBounds()) { upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size(); @@ -353,6 +364,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } + else if (!options::cbqiMultiInst()) + { + return false; + } } } else @@ -389,6 +404,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, t_values[rr].push_back(Node::null()); // check if it is better than the current best bound : lexicographic // order infinite/finite/infinitesimal parts + bool new_best_set = false; bool new_best = true; for (unsigned t = 0; t < 3; t++) { @@ -435,8 +451,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, value[t]); value[t] = Rewriter::rewrite(value[t]); } - // check if new best - if (best != -1) + // check if new best, if we have not already set it. + if (best != -1 && !new_best_set) { Assert(!value[t].isNull() && !best_bound_value[t].isNull()); if (value[t] != best_bound_value[t]) @@ -444,12 +460,17 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, Kind k = rr == 0 ? GEQ : LEQ; Node cmp_bound = nm->mkNode(k, value[t], best_bound_value[t]); cmp_bound = Rewriter::rewrite(cmp_bound); - if (cmp_bound - != ci->getQuantifiersEngine()->getTermUtil()->d_true) + // Should be comparing two constant values which should rewrite + // to a constant. If a step failed, we assume that this is not + // the new best bound. + Assert(cmp_bound.isConst()); + if (!cmp_bound.isConst() || !cmp_bound.getConst()) { new_best = false; break; } + // indicate that the value of new_best is now established. + new_best_set = true; } } } @@ -504,6 +525,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } + else if (!options::cbqiMultiInst()) + { + return false; + } } } } @@ -531,6 +556,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } + else if (!options::cbqiMultiInst()) + { + return false; + } } } if (options::cbqiMidpoint() && !d_type.isInteger()) @@ -598,6 +627,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } + else if (!options::cbqiMultiInst()) + { + return false; + } } } // generally should not make it to this point, unless we are using a @@ -637,6 +670,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } + else if (!options::cbqiMultiInst()) + { + return false; + } } } } diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 0b9e415fa..017e4f9bd 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1251,6 +1251,7 @@ REG1_TESTS = \ regress1/quantifiers/NUM878.smt2 \ regress1/quantifiers/RND-small.smt2 \ regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 \ + regress1/quantifiers/RND_4_1-existing-inst.smt2 \ regress1/quantifiers/RND_4_16.smt2 \ regress1/quantifiers/anti-sk-simp.smt2 \ regress1/quantifiers/ari118-bv-2occ-x.smt2 \ @@ -1308,6 +1309,7 @@ REG1_TESTS = \ regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \ regress1/quantifiers/qcft-smtlib3dbc51.smt2 \ regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \ + regress1/quantifiers/repair-const-nterm.smt2 \ regress1/quantifiers/recfact.cvc \ regress1/quantifiers/rew-to-0211-dd.smt2 \ regress1/quantifiers/ricart-agrawala6.smt2 \ diff --git a/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 b/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 new file mode 100644 index 000000000..73c278522 --- /dev/null +++ b/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 @@ -0,0 +1,15 @@ +(set-logic LRA) +(set-info :status unsat) +(declare-fun a () Real) +(assert + (forall ((?y2 Real) (?y3 Real)) + (or + (= ?y3 1) + (> ?y3 0) + (and + (< ?y2 0) + (< ?y3 49) + ))) +) +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/repair-const-nterm.smt2 b/test/regress/regress1/quantifiers/repair-const-nterm.smt2 new file mode 100644 index 000000000..f9b1d6829 --- /dev/null +++ b/test/regress/regress1/quantifiers/repair-const-nterm.smt2 @@ -0,0 +1,12 @@ +(set-logic LIA) +(set-info :status unsat) + +(declare-fun k_20 () Int) +(declare-fun k_72 () Int) +(declare-fun k_73 () Int) + +(assert +(forall ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) (not (>= (+ (* 3 x7) (* (- 1) (ite (= x7 k_20) k_72 k_73))) 1)) ) +) + +(check-sat) -- cgit v1.2.3 From 1b89c8628eee3d081e91bf99745a16a21c40bf8a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Aug 2018 23:24:53 -0500 Subject: Fix API call for reg exp. (#2248) --- src/expr/expr_manager_template.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index de128b3e5..425f78555 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -146,7 +146,7 @@ StringType ExprManager::stringType() const { RegExpType ExprManager::regExpType() const { NodeManagerScope nms(d_nodeManager); - return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->regExpType()))); + return RegExpType(Type(d_nodeManager, new TypeNode(d_nodeManager->regExpType()))); } RealType ExprManager::realType() const { -- cgit v1.2.3