}
return true;
}else if( t.isRecord() && t.isRecord() ){
- //TBD
+ //records are not subtypes of each other in current implementation
}
if(isFunction()) {
// A function is a subtype of another if the args are the same type, and
// the return type is a subtype of the other's. This is enough for now
// (and it's necessary for model generation, since a Real-valued function
// might return a constant Int and thus the model value is typed differently).
- return t.isFunction() &&
- getArgTypes() == t.getArgTypes() &&
- getRangeType().isSubtypeOf(t.getRangeType());
+ return t.isFunction() && getArgTypes() == t.getArgTypes() && getRangeType().isSubtypeOf(t.getRangeType());
}
if(isParametricDatatype() && t.isParametricDatatype()) {
Assert(getKind() == kind::PARAMETRIC_DATATYPE);
if(isSet() && t.isSet()) {
return getSetElementType().isSubtypeOf(t.getSetElementType());
}
+ if(isArray() && t.isArray()) {
+ //reverse for index type
+ return t.getArrayIndexType().isSubtypeOf(getArrayIndexType()) &&
+ getArrayConstituentType().isSubtypeOf(t.getArrayConstituentType());
+ }
return false;
}
}
}
return true;
- }else if( isRecord() && t.isRecord() ){
- //TBD
+ //}else if( isRecord() && t.isRecord() ){
+ //record types are incomparable in current implementation
} else if(isParametricDatatype() && t.isParametricDatatype()) {
Assert(getKind() == kind::PARAMETRIC_DATATYPE);
Assert(t.getKind() == kind::PARAMETRIC_DATATYPE);
} else if(isSet() && t.isSet()) {
return getSetElementType().isComparableTo(t.getSetElementType());
}
-
- if(isPredicateSubtype()) {
- return t.isComparableTo(getSubtypeParentType());
+ if(isArray() && t.isArray()) {
+ return getArrayIndexType().isComparableTo(t.getArrayIndexType()) && getArrayConstituentType().isComparableTo(t.getArrayConstituentType());
}
+ //if(isPredicateSubtype()) {
+ // return t.isComparableTo(getSubtypeParentType());
+ //}
return false;
}
}
TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
+ return commonTypeNode( t0, t1, true );
+}
+
+TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){
+ return commonTypeNode( t0, t1, false );
+}
+
+TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
Assert( NodeManager::currentNM() != NULL,
"There is no current CVC4::NodeManager associated to this thread.\n"
"Perhaps a public-facing function is missing a NodeManagerScope ?" );
return t0; //IntegerType
} else if(t1.isReal()) {
// t0 == IntegerType && t1.isReal() && !t1.isInteger()
- return NodeManager::currentNM()->realType(); // RealType
+ return isLeast ? t1 : t0; // RealType
} else {
return TypeNode(); // null type
}
case REAL_TYPE:
if(t1.isReal()) {
- return t0; // RealType
+ return isLeast ? t0 : t1; // RealType
} else {
return TypeNode(); // null type
}
default:
- if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
- return t0; // t0 is a constant type
- } else {
+ //if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
+ // return t0; // t0 is a constant type
+ //} else {
return TypeNode(); // null type
- }
+ //}
}
} else if(t1.getKind() == kind::TYPE_CONSTANT) {
- return leastCommonTypeNode(t1, t0); // decrease the number of special cases
+ return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases
}
// t0 != t1 &&
// t0.getKind() == kind::TYPE_CONSTANT &&
// t1.getKind() == kind::TYPE_CONSTANT
switch(t0.getKind()) {
- case kind::ARRAY_TYPE:
case kind::BITVECTOR_TYPE:
case kind::SORT_TYPE:
case kind::CONSTRUCTOR_TYPE:
case kind::SELECTOR_TYPE:
case kind::TESTER_TYPE:
- if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
- return t0;
- } else {
+ //if( t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
+ // return t0;
+ //} else {
return TypeNode();
- }
+ //}
case kind::FUNCTION_TYPE:
return TypeNode(); // Not sure if this is right
case kind::SET_TYPE: {
// take the least common subtype of element types
TypeNode elementType;
- if(t1.isSet() &&
- ! (elementType = leastCommonTypeNode(t0[0], t1[0])).isNull() ) {
+ if(t1.isSet() && !(elementType = commonTypeNode(t0[0], t1[0], isLeast)).isNull() ) {
return NodeManager::currentNM()->mkSetType(elementType);
} else {
return TypeNode();
}
}
+ case kind::ARRAY_TYPE: {
+ TypeNode indexType, elementType;
+ if(t1.isArray() &&
+ ! (indexType = commonTypeNode(t0[0], t1[0], !isLeast)).isNull() &&
+ ! (elementType = commonTypeNode(t0[1], t1[1], isLeast)).isNull() ) {
+ return NodeManager::currentNM()->mkArrayType(indexType, elementType);
+ } else {
+ return TypeNode();
+ }
+ }
case kind::SEXPR_TYPE:
Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
return TypeNode();
case kind::SUBTYPE_TYPE:
- if(t1.isPredicateSubtype()){
- // This is the case where both t0 and t1 are predicate subtypes.
- return leastCommonPredicateSubtype(t0, t1);
- }else{ // t0 is a predicate subtype and t1 is not
- return leastCommonTypeNode(t1, t0); //decrease the number of special cases
- }
+ //if(t1.isPredicateSubtype()){
+ // // This is the case where both t0 and t1 are predicate subtypes.
+ // return leastCommonPredicateSubtype(t0, t1);
+ //}else{ // t0 is a predicate subtype and t1 is not
+ // return commonTypeNode(t1, t0, isLeast); //decrease the number of special cases
+ //}
+ return TypeNode();
case kind::SUBRANGE_TYPE:
+ /*
if(t1.isSubrange()) {
const SubrangeBounds& t0SR = t0.getSubrangeBounds();
const SubrangeBounds& t1SR = t1.getSubrangeBounds();
Assert(t1.isInteger());
return TypeNode();
}
+*/
+ return TypeNode();
case kind::DATATYPE_TYPE:
if( t0.isTuple() && t1.isTuple() ){
const Datatype& dt1 = t0.getDatatype();
if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
std::vector< TypeNode > lc_types;
for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
- TypeNode tc = leastCommonTypeNode( TypeNode::fromType( dt1[0][i].getRangeType() ), TypeNode::fromType( dt2[0][i].getRangeType() ) );
+ TypeNode tc = commonTypeNode( TypeNode::fromType( dt1[0][i].getRangeType() ), TypeNode::fromType( dt2[0][i].getRangeType() ), isLeast );
if( tc.isNull() ){
return tc;
}else{
}
return NodeManager::currentNM()->mkTupleType( lc_types );
}
- }else if( t0.isRecord() && t1.isRecord() ){
- //TBD
}
+ //else if( t0.isRecord() && t1.isRecord() ){
+ //record types are not related in current implementation
+ //}
// otherwise no common ancestor
return TypeNode();
case kind::PARAMETRIC_DATATYPE: {
}
vector<Type> v;
for(size_t i = 1; i < t0.getNumChildren(); ++i) {
- v.push_back(leastCommonTypeNode(t0[i], t1[i]).toType());
+ v.push_back(commonTypeNode(t0[i], t1[i], isLeast).toType());
}
return TypeNode::fromType(t0[0].getDatatype().getDatatypeType(v));
}
default:
- Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
+ Unimplemented("don't have a commonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
return TypeNode();
}
}
* For more information see: http://cvc4.cs.nyu.edu/wiki/Cvc4_Type_Lattice
*/
static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
+ static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1);
private:
+ static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
/**
* Returns the leastUpperBound in the extended type lattice of two
d_ground_macros = (r==0);
Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
//first, collect macro definitions
- for( int i=0; i<(int)assertions.size(); i++ ){
+ std::vector< Node > macro_assertions;
+ for( unsigned i=0; i<assertions.size(); i++ ){
Trace("macros-debug") << " process assertion " << assertions[i] << std::endl;
if( processAssertion( assertions[i] ) ){
+ PROOF(
+ if( std::find( macro_assertions.begin(), macro_assertions.end(), assertions[i] )==macro_assertions.end() ){
+ macro_assertions.push_back( assertions[i] );
+ }
+ );
//process this assertion again
i--;
}
if( curr!=assertions[i] ){
curr = Rewriter::rewrite( curr );
Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
- PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
+ //for now, it is dependent upon all assertions involving macros, this is an over-approximation.
+ //a more fine-grained unsat core computation would require caching dependencies for each subterm of the formula,
+ // which is expensive.
+ PROOF(
+ ProofManager::currentPM()->addDependence(curr, assertions[i]);
+ for( unsigned j=0; j<macro_assertions.size(); j++ ){
+ if( macro_assertions[j]!=assertions[i] ){
+ ProofManager::currentPM()->addDependence(curr,macro_assertions[j]);
+ }
+ }
+ );
assertions[i] = curr;
retVal = true;
}
}
}
if( Trace.isOn("macros-warn") ){
- for( int i=0; i<(int)assertions.size(); i++ ){
+ for( unsigned i=0; i<assertions.size(); i++ ){
debugMacroDefinition( assertions[i], assertions[i] );
}
}
bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
Assert( n.getKind()==APPLY_UF );
- TypeNode tn = n.getOperator().getType();
+ TypeNode tno = n.getOperator().getType();
+ std::map< Node, bool > vars;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( n[i].getKind()!=BOUND_VARIABLE ){
return false;
}
- if( n[i].getType()!=tn[i] ){
+ if( n[i].getType()!=tno[i] ){
return false;
}
- for( unsigned j=0; j<i; j++ ){
- if( n[j]==n[i] ){
- return false;
- }
+ if( !tno[i].isSort() && !tno[i].isReal() && ( !tno[i].isDatatype() || tno[i].isParametricDatatype() ) &&
+ !tno[i].isBitVector() && !tno[i].isString() && !tno[i].isFloatingPoint() ){
+ //only non-parametric types are supported
+ return false;
+ }
+ if( vars.find( n[i] )==vars.end() ){
+ vars[n[i]] = true;
+ }else{
+ return false;
}
}
return true;
Node op = n.getOperator();
std::map< Node, Node >::iterator it = d_macro_defs.find( op );
if( it!=d_macro_defs.end() && !it->second.isNull() ){
- //do substitution if necessary
- ret = it->second;
- std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op );
- if( itb!=d_macro_basis.end() ){
- ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() );
+ //only apply if children are subtypes of arguments
+ bool success = true;
+ std::vector< Node > cond;
+ TypeNode tno = op.getType();
+ for( unsigned i=0; i<children.size(); i++ ){
+ if( !TermDb::getEnsureTypeCondition( children[i], tno[i], cond ) ){
+ //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op,
+ // and not ensuring it applies to n when its types are correct.
+ //however, this should never fail: we never process types for which we cannot constuct conditions that ensure correct types, e.g. (is-int t).
+ Assert( false );
+ success = false;
+ break;
+ }
+ }
+ if( success ){
+ //do substitution if necessary
+ ret = it->second;
+ std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op );
+ if( itb!=d_macro_basis.end() ){
+ ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() );
+ }
+ if( !cond.empty() ){
+ Node cc = cond.size()==1 ? cond[0] : NodeManager::currentNM()->mkNode( kind::AND, cond );
+ ret = NodeManager::currentNM()->mkNode( kind::ITE, cc, ret, n );
+ }
+ retSet = true;
}
- retSet = true;
}
}
if( !retSet && childChanged ){
return containsTerms( n, t );
}
-Node TermDb::mkNodeType( Node n, TypeNode tn ) {
+Node TermDb::ensureType( Node n, TypeNode tn ) {
TypeNode ntn = n.getType();
Assert( ntn.isComparableTo( tn ) );
if( ntn.isSubtypeOf( tn ) ){
}
}
+bool TermDb::getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& cond ) {
+ TypeNode ntn = n.getType();
+ Assert( ntn.isComparableTo( tn ) );
+ if( !ntn.isSubtypeOf( tn ) ){
+ if( tn.isInteger() ){
+ cond.push_back( NodeManager::currentNM()->mkNode( IS_INTEGER, n ) );
+ return true;
+ }
+ return false;
+ }else{
+ return true;
+ }
+}
+
bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
if( n==t ){
return true;
bool containsVtsTerm( std::vector< Node >& n, bool isFree = false );
/** simple check for contains term */
bool containsVtsInfinity( Node n, bool isFree = false );
- /** make type */
- static Node mkNodeType( Node n, TypeNode tn );
-
+ /** ensure type */
+ static Node ensureType( Node n, TypeNode tn );
+ /** get ensure type condition */
+ static bool getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& cond );
private:
//helper for contains term
static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );
Assert( f.getKind()==FORALL );
Assert( vars.size()==terms.size() );
Node body = getInstantiation( f, vars, terms, doVts ); //do virtual term substitution
- if( doVts ){
- body = Rewriter::rewrite( body );
- Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
- Node body_r = d_term_db->rewriteVtsSymbols( body );
- Trace("quant-vts-debug") << " ...result: " << body_r << std::endl;
- body = body_r;
- }
body = quantifiers::QuantifiersRewriter::preprocess( body, true );
Trace("inst-debug") << "...preprocess to " << body << std::endl;
Trace("inst-assert") << "(assert " << body << ")" << std::endl;
terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i );
}else{
//ensure the type is correct
- terms[i] = quantifiers::TermDb::mkNodeType( terms[i], q[0][i].getType() );
+ terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() );
}
Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
- Assert( !terms[i].isNull() );
+ if( terms[i].isNull() ){
+ Trace("inst-add-debug") << " -> Failed to make term vector, due to term/type restrictions." << std::endl;
+ return false;
+ }
#ifdef CVC4_ASSERTIONS
Assert( !quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) );
#endif
agg-rew-test.smt2 \
agg-rew-test-cf.smt2 \
rew-to-0211-dd.smt2 \
- rew-to-scala.smt2
+ rew-to-scala.smt2 \
+ macro-subtype-param.smt2 \
+ macros-real-arg.smt2 \
+ subtype-param-unk.smt2 \
+ subtype-param.smt2
# regression can be solved with --finite-model-find --fmf-inst-engine
--- /dev/null
+; COMMAND-LINE: --macros-quant
+; EXPECT: unknown
+; this will fail if type rule for APPLY_UF requires to be subtypes
+(set-logic ALL_SUPPORTED)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+(assert (forall ((x (List Int))) (R x)))
+(declare-fun j1 () (List Real))
+(assert (not (R j1)))
+
+(declare-fun Q ((Array Real Int)) Bool)
+(assert (forall ((x (Array Real Int))) (Q x)))
+(declare-fun j2 () (Array Int Real))
+(assert (not (Q j2)))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --macros-quant
+; EXPECT: unsat
+; this will fail if type rule for APPLY_UF is made strict
+(set-logic UFLIRA)
+(declare-fun P (Int) Bool)
+(assert (forall ((x Int)) (P x)))
+(declare-fun k () Real)
+(declare-fun k2 () Int)
+(assert (or (not (P k)) (not (P k2))))
+(assert (= k 0))
+(check-sat)
--- /dev/null
+; COMMAND-LINE:
+; EXPECT: unknown
+; this will fail if type rule for APPLY_UF requires arguments to be subtypes
+(set-logic ALL_SUPPORTED)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+
+(assert (forall ((x (List Int))) (R x)))
+(declare-fun j1 () (List Real))
+(assert (not (R j1)))
+
+(declare-fun Q ((Array Int Real)) Bool)
+(assert (forall ((x (Array Int Int))) (Q x)))
+(declare-fun j2 () (Array Int Real))
+(assert (not (Q j2)))
+
+(check-sat)
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+(assert (forall ((x (List Real))) (R x)))
+
+(declare-fun Q ((Array Int Real)) Bool)
+(assert (forall ((x (Array Int Int))) (Q x)))
+
+(declare-fun k1 () (List Int))
+(declare-fun k2 () (Array Real Int))
+(assert (or (not (R k1)) (not (Q k2))))
+
+(check-sat)
projects / cvc5.git / commitdiff