if (!getAttribute(IsInterpretedFiniteComputedAttr()))
{
bool isInterpretedFinite = false;
- if (getCardinality().isFinite())
+ if (isSort())
+ {
+ // If the finite model finding flag is set, we treat uninterpreted sorts
+ // as finite. If it is not set, we treat them implicitly as infinite
+ // sorts (that is, their cardinality is not constrained to be finite).
+ isInterpretedFinite = options::finiteModelFind();
+ }
+ else if (isBitVector() || isFloatingPoint())
{
isInterpretedFinite = true;
}
- else if (options::finiteModelFind())
+ else if (isDatatype())
{
- if( isSort() ){
- isInterpretedFinite = true;
- }else if( isDatatype() ){
- TypeNode tn = *this;
- const Datatype& dt = getDatatype();
- isInterpretedFinite = dt.isInterpretedFinite(tn.toType());
- }else if( isArray() ){
- isInterpretedFinite =
- getArrayIndexType().isInterpretedFinite()
- && getArrayConstituentType().isInterpretedFinite();
- }else if( isSet() ) {
- isInterpretedFinite = getSetElementType().isInterpretedFinite();
+ TypeNode tn = *this;
+ const Datatype& dt = getDatatype();
+ isInterpretedFinite = dt.isInterpretedFinite(tn.toType());
+ }
+ else if (isArray())
+ {
+ TypeNode tnc = getArrayConstituentType();
+ if (!tnc.isInterpretedFinite())
+ {
+ // arrays with consistuent type that is infinite are infinite
+ isInterpretedFinite = false;
}
- else if (isFunction())
+ else if (getArrayIndexType().isInterpretedFinite())
{
+ // arrays with both finite consistuent and index types are finite
isInterpretedFinite = true;
- if (!getRangeType().isInterpretedFinite())
- {
- isInterpretedFinite = false;
- }
- else
+ }
+ else
+ {
+ // If the consistuent type of the array has cardinality one, then the
+ // array type has cardinality one, independent of the index type.
+ isInterpretedFinite = tnc.getCardinality().isOne();
+ }
+ }
+ else if (isSet())
+ {
+ isInterpretedFinite = getSetElementType().isInterpretedFinite();
+ }
+ else if (isFunction())
+ {
+ isInterpretedFinite = true;
+ TypeNode tnr = getRangeType();
+ if (!tnr.isInterpretedFinite())
+ {
+ isInterpretedFinite = false;
+ }
+ else
+ {
+ std::vector<TypeNode> argTypes = getArgTypes();
+ for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
{
- std::vector<TypeNode> argTypes = getArgTypes();
- for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
+ if (!argTypes[i].isInterpretedFinite())
{
- if (!argTypes[i].isInterpretedFinite())
- {
- isInterpretedFinite = false;
- break;
- }
+ isInterpretedFinite = false;
+ break;
}
}
+ if (!isInterpretedFinite)
+ {
+ // similar to arrays, functions are finite if their range type
+ // has cardinality one, regardless of the arguments.
+ isInterpretedFinite = tnr.getCardinality().isOne();
+ }
}
}
+ else
+ {
+ // by default, compute the exact cardinality for the type and check
+ // whether it is finite. This should be avoided in general, since
+ // computing cardinalities for types can be highly expensive.
+ isInterpretedFinite = getCardinality().isFinite();
+ }
setAttribute(IsInterpretedFiniteAttr(), isInterpretedFinite);
setAttribute(IsInterpretedFiniteComputedAttr(), true);
return isInterpretedFinite;
read_only = true
help = "mode for which types of bounds to minimize via first decision heuristics"
+[[option]]
+ name = "fmfTypeCompletionThresh"
+ category = "regular"
+ long = "fmf-type-completion-thresh=N"
+ type = "int"
+ default = "1000"
+ read_only = true
+ help = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted"
+
[[option]]
name = "quantConflictFind"
category = "regular"
unsigned c1 = deq_child[0][i];
unsigned c2 = deq_child[1][i];
TypeNode tnc = children[c1].getType();
- if (tnc == children[c2].getType() && !tnc.getCardinality().isOne())
+ // we may only apply this symmetry breaking scheme (which introduces
+ // disequalities) if the types are infinite.
+ if (tnc == children[c2].getType() && !tnc.isInterpretedFinite())
{
Node sym_lem_deq = children[c1].eqNode(children[c2]).negate();
// notice that this symmetry breaking still allows for
Trace("datatypes-debug") << "No constructor..." << std::endl;
Type tt = tn.toType();
const Datatype& dt = ((DatatypeType)tt).getDatatype();
- Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite( tt ) << " " << dt.isInterpretedFinite( tt ) << " " << dt.isRecursiveSingleton( tt ) << std::endl;
+ Trace("datatypes-debug")
+ << "Datatype " << dt << " is " << dt.isInterpretedFinite(tt)
+ << " " << dt.isRecursiveSingleton(tt) << std::endl;
bool continueProc = true;
if( dt.isRecursiveSingleton( tt ) ){
Trace("datatypes-debug") << "Check recursive singleton..." << std::endl;
if( consIndex==-1 ){
consIndex = j;
}
- if( !dt[ j ].isInterpretedFinite( tt ) ) {
+ Trace("datatypes-debug") << j << " compute finite..."
+ << std::endl;
+ bool ifin = dt[j].isInterpretedFinite(tt);
+ Trace("datatypes-debug") << "...returned " << ifin
+ << std::endl;
+ if (!ifin)
+ {
if( !eqc || !eqc->d_selectors ){
needSplit = false;
}
tt = exp[0];
}
const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
- //must be finite or have a selector
- //if( eqc->d_selectors || dt[ index ].isFinite() ){
//instantiate this equivalence class
eqc->d_inst = true;
Node tt_cons = getInstantiateCons( tt, dt, index );
Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
Debug("dt-enum") << "datatype is " << d_type << std::endl;
Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton( d_type.toType() );
- Debug("dt-enum") << " " << d_datatype.isFinite( d_type.toType() ) << std::endl;
Debug("dt-enum") << " " << d_datatype.isInterpretedFinite( d_type.toType() ) << std::endl;
if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
TypeNode tn = f[0][i].getType();
if( !tn.isSort() ){
- if( !tn.getCardinality().isFinite() ){
+ if (!tn.isInterpretedFinite())
+ {
if( tn.isInteger() ){
if( !options::fmfBound() ){
canHandle = false;
#include "theory/quantifiers/term_enumeration.h"
+#include "options/quantifiers_options.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
if (it == d_may_complete.end())
{
bool mc = false;
- if (isClosedEnumerableType(tn) && tn.getCardinality().isFinite()
- && !tn.getCardinality().isLargeFinite())
+ if (isClosedEnumerableType(tn) && tn.isInterpretedFinite())
{
- Node card = NodeManager::currentNM()->mkConst(
- Rational(tn.getCardinality().getFiniteCardinality()));
- Node oth = NodeManager::currentNM()->mkConst(Rational(1000));
- Node eq = NodeManager::currentNM()->mkNode(LEQ, card, oth);
- eq = Rewriter::rewrite(eq);
- mc = eq.isConst() && eq.getConst<bool>();
+ Cardinality c = tn.getCardinality();
+ if (!c.isLargeFinite())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
+ // check if less than fixed upper bound, default 1000
+ Node oth = nm->mkConst(Rational(options::fmfTypeCompletionThresh()));
+ Node eq = nm->mkNode(LEQ, card, oth);
+ eq = Rewriter::rewrite(eq);
+ mc = eq.isConst() && eq.getConst<bool>();
+ }
}
d_may_complete[tn] = mc;
return mc;
/** Returns true iff this cardinality is finite. */
bool isFinite() const { return d_card > 0; }
/** Returns true iff this cardinality is one */
- bool isOne() const { return d_card == 1; }
-
+ bool isOne() const { return d_card == 2; }
/**
* Returns true iff this cardinality is finite and large (i.e.,
* at the ceiling of representable finite cardinalities).
regress1/strings/username_checker_min.smt2 \
regress1/sygus/VC22_a.sy \
regress1/sygus/array_search_2.sy \
+ regress1/sygus/array_search_5-Q-easy.sy \
regress1/sygus/array_sum_2_5.sy \
regress1/sygus/cegar1.sy \
regress1/sygus/cegisunif-depth1.sy \
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+( set-logic LIA )
+( synth-fun findIdx ( ( y1 Int ) ( y2 Int ) ( y3 Int ) ( y4 Int ) ( y5 Int ) ( k1 Int ) ) Int (
+ (Start Int ( NT1
+ NT3
+ NT4
+ NT7
+ NT8
+ NT9
+ NT10
+ NT11
+ NT13
+ NT14
+))
+ (NT1 Int ( y5
+ k1
+ 1
+ y2
+ 0
+ y1
+ 2
+ 5
+ y4
+ 4
+ y3
+ 3
+))
+ (NT2 Bool ( (< NT1 NT1)
+ (> NT1 NT1)
+ (>= NT1 NT1)
+ (<= NT1 NT1)
+))
+ (NT3 Int ( (ite NT2 NT1 NT1)
+))
+ (NT4 Int ( (ite NT5 NT1 NT1)
+ (ite NT2 NT3 NT1)
+))
+ (NT5 Bool ( (< NT3 NT1)
+ (<= NT3 NT1)
+ (>= NT3 NT1)
+ (> NT3 NT1)
+))
+ (NT6 Bool ( (<= NT4 NT1)
+ (> NT4 NT1)
+ (<= NT3 NT3)
+ (> NT3 NT3)
+ (>= NT4 NT1)
+ (< NT4 NT1)
+ (< NT3 NT3)
+ (>= NT3 NT3)
+))
+ (NT7 Int ( (ite NT6 NT1 NT1)
+ (ite NT2 NT4 NT1)
+))
+ (NT8 Int ( (ite NT2 NT7 NT1)
+ (ite NT5 NT4 NT1)
+ (ite NT15 NT1 NT1)
+ (ite NT5 NT1 NT4)
+))
+ (NT9 Int ( (ite NT2 NT8 NT1)
+ (ite NT12 NT1 NT1)
+ (ite NT6 NT1 NT4)
+ (ite NT6 NT4 NT1)
+ (ite NT5 NT7 NT1)
+))
+ (NT10 Int ( (ite NT5 NT8 NT1)
+ (ite NT16 NT1 NT1)
+ (ite NT2 NT9 NT1)
+ (ite NT6 NT7 NT1)
+ (ite NT5 NT4 NT4)
+))
+ (NT11 Int ( (ite NT6 NT8 NT1)
+ (ite NT2 NT10 NT1)
+ (ite NT5 NT9 NT1)
+ (ite NT17 NT1 NT1)
+ (ite NT6 NT4 NT4)
+))
+ (NT12 Bool ( (< NT4 NT4)
+ (> NT4 NT4)
+ (<= NT8 NT1)
+ (< NT8 NT1)
+ (<= NT4 NT4)
+ (> NT8 NT1)
+ (>= NT8 NT1)
+ (>= NT4 NT4)
+))
+ (NT13 Int ( (ite NT18 NT1 NT1)
+ (ite NT12 NT7 NT1)
+ (ite NT5 NT10 NT1)
+ (ite NT6 NT9 NT1)
+ (ite NT12 NT1 NT7)
+ (ite NT2 NT11 NT1)
+))
+ (NT14 Int ( (ite NT12 NT1 NT8)
+ (ite NT6 NT10 NT1)
+ (ite NT5 NT11 NT1)
+ (ite NT19 NT1 NT1)
+ (ite NT12 NT8 NT1)
+ (ite NT2 NT13 NT1)
+))
+ (NT15 Bool ( (>= NT7 NT1)
+ (< NT7 NT1)
+ (> NT7 NT1)
+ (<= NT7 NT1)
+))
+ (NT16 Bool ( (< NT9 NT1)
+ (>= NT9 NT1)
+ (> NT9 NT1)
+ (<= NT9 NT1)
+))
+ (NT17 Bool ( (< NT7 NT7)
+ (<= NT10 NT1)
+ (>= NT10 NT1)
+ (> NT10 NT1)
+ (< NT10 NT1)
+ (> NT7 NT7)
+ (>= NT7 NT7)
+ (<= NT7 NT7)
+))
+ (NT18 Bool ( (< NT11 NT1)
+ (> NT11 NT1)
+ (>= NT11 NT1)
+ (<= NT11 NT1)
+))
+ (NT19 Bool ( (>= NT13 NT1)
+ (>= NT8 NT8)
+ (< NT13 NT1)
+ (> NT13 NT1)
+ (< NT8 NT8)
+ (> NT8 NT8)
+ (<= NT8 NT8)
+ (<= NT13 NT1)
+))
+))
+ ( declare-var x1 Int )
+ ( declare-var x2 Int )
+ ( declare-var x3 Int )
+ ( declare-var x4 Int )
+ ( declare-var x5 Int )
+ ( declare-var k Int )
+ ( constraint ( => ( and ( < x1 x2 ) ( and ( < x2 x3 ) ( and ( < x3 x4 ) ( < x4 x5 ) ) ) ) ( => ( < k x1 ) ( = ( findIdx x1 x2 x3 x4 x5 k ) 0 ) ) ) )
+ ( check-synth )
+
projects / cvc5.git / commitdiff