summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--AUTHORS10
-rwxr-xr-xcontrib/depgraph1
-rw-r--r--src/base/configuration.cpp4
-rw-r--r--src/base/configuration.h2
-rw-r--r--src/base/configuration_private.h6
-rw-r--r--src/expr/expr_manager_template.cpp11
-rw-r--r--src/expr/expr_manager_template.h3
-rw-r--r--src/expr/node_manager.cpp6
-rw-r--r--src/expr/node_manager.h6
-rw-r--r--src/options/options_handler.cpp1
-rw-r--r--src/parser/parser.cpp14
-rw-r--r--src/parser/parser.h5
-rw-r--r--src/parser/smt2/Smt2.g4
-rw-r--r--src/printer/smt2/smt2_printer.cpp73
-rw-r--r--src/smt/smt_engine.cpp7
-rw-r--r--src/smt/smt_engine_scope.cpp1
-rw-r--r--src/theory/evaluator.cpp4
-rw-r--r--src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp61
-rw-r--r--test/regress/Makefile.tests2
-rw-r--r--test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt215
-rw-r--r--test/regress/regress1/quantifiers/repair-const-nterm.smt212
21 files changed, 191 insertions, 57 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 7062eb2f7..32ab85f96 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -252,10 +252,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 06a3a5d9e..a00a6c1d9 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -97,8 +97,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/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 457e54d9b..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 {
@@ -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<NodeManagerListener*>::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/options/options_handler.cpp b/src/options/options_handler.cpp
index 2efc8a5cf..8abe8d541 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1657,7 +1657,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/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<Type>(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<Type>& 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<CVC4::Command>* 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<DatatypeType>(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<DatatypeType>::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<DatatypeType>& dtts) override
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"
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;
}
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<bool>();
}
}
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<bool>())
{
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback