diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-22 09:23:57 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-22 09:23:57 -0500 |
commit | c98ba7775ecb8a192e2a93735885163234546be3 (patch) | |
tree | fbfef218b03aeb1aa762da05785fe1d59ef43625 | |
parent | 37107284adaad3d24da0ad15cac8c88af444aeef (diff) |
Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)
Fixes #4092 and fixes #4134.
Typically, APPLY_UF has special treatment in sort inference. It is significantly more complicated when higher-order logic is enabled. This disables special handling when ufHo() is enabled.
-rw-r--r-- | src/theory/sort_inference.cpp | 32 | ||||
-rw-r--r-- | src/theory/sort_inference.h | 8 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress1/ho/issue4092-sinf.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress1/ho/issue4134-sinf.smt2 | 13 |
5 files changed, 49 insertions, 16 deletions
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 9a90e591d..42364f080 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -29,6 +29,7 @@ #include "theory/quantifiers/quant_util.h" using namespace CVC4; +using namespace CVC4::kind; using namespace std; namespace CVC4 { @@ -434,7 +435,9 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map< } d_equality_types[n] = child_types[0]; retType = getIdForType( n.getType() ); - }else if( n.getKind()==kind::APPLY_UF ){ + } + else if (isHandledApplyUf(n.getKind())) + { Node op = n.getOperator(); TypeNode tn_op = op.getType(); if( d_op_return_types.find( op )==d_op_return_types.end() ){ @@ -663,7 +666,8 @@ Node SortInference::simplifyNode( : i >= 1; } if( processChild ){ - if( n.getKind()==kind::APPLY_UF ){ + if (isHandledApplyUf(n.getKind())) + { Assert(d_op_arg_types.find(op) != d_op_arg_types.end()); tnnc = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() ); Assert(!tnnc.isNull()); @@ -704,7 +708,9 @@ Node SortInference::simplifyNode( Assert(false); } ret = NodeManager::currentNM()->mkNode( kind::EQUAL, children ); - }else if( n.getKind()==kind::APPLY_UF ){ + } + else if (isHandledApplyUf(n.getKind())) + { if( d_symbol_map.find( op )==d_symbol_map.end() ){ //make the new operator if necessary bool opChanged = false; @@ -815,7 +821,8 @@ void SortInference::setSkolemVar( Node f, Node v, Node sk ){ } bool SortInference::isWellSortedFormula( Node n ) { - if( n.getType().isBoolean() && n.getKind()!=kind::APPLY_UF ){ + if (n.getType().isBoolean() && !isHandledApplyUf(n.getKind())) + { for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( !isWellSortedFormula( n[i] ) ){ return false; @@ -831,7 +838,8 @@ bool SortInference::isWellSorted( Node n ) { if( getSortId( n )==0 ){ return false; }else{ - if( n.getKind()==kind::APPLY_UF ){ + if (isHandledApplyUf(n.getKind())) + { for( unsigned i=0; i<n.getNumChildren(); i++ ){ int s1 = getSortId( n[i] ); int s2 = d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] ); @@ -847,18 +855,14 @@ bool SortInference::isWellSorted( Node n ) { } } -void SortInference::getSortConstraints( Node n, UnionFind& uf ) { - if( n.getKind()==kind::APPLY_UF ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - getSortConstraints( n[i], uf ); - uf.setEqual( getSortId( n[i] ), d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] ) ); - } - } -} - bool SortInference::isMonotonic( TypeNode tn ) { Assert(tn.isSort()); return d_non_monotonic_sorts_orig.find( tn )==d_non_monotonic_sorts_orig.end(); } +bool SortInference::isHandledApplyUf(Kind k) const +{ + return k == APPLY_UF && !options::ufHo(); +} + }/* CVC4 namespace */ diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h index 5b28f669d..ecf86376c 100644 --- a/src/theory/sort_inference.h +++ b/src/theory/sort_inference.h @@ -154,11 +154,15 @@ public: //is well sorted bool isWellSortedFormula( Node n ); bool isWellSorted( Node n ); - //get constraints for being well-typed according to computed sub-types - void getSortConstraints( Node n, SortInference::UnionFind& uf ); private: // store monotonicity for original sorts as well std::map<TypeNode, bool> d_non_monotonic_sorts_orig; + /** + * Returns true if k is the APPLY_UF kind and we are not using higher-order + * techniques. This is called in places where we want to know whether to + * treat a term as uninterpreted function. + */ + bool isHandledApplyUf(Kind k) const; }; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a8ec4a665..cd83ef3d1 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1302,6 +1302,8 @@ set(regress_1_tests regress1/ho/fta0328.lfho.p regress1/ho/issue3136-fconst-bool-bool.smt2 regress1/ho/issue4065-no-rep.smt2 + regress1/ho/issue4092-sinf.smt2 + regress1/ho/issue4134-sinf.smt2 regress1/ho/nested_lambdas-AGT034^2.smt2 regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/NUM638^1.smt2 diff --git a/test/regress/regress1/ho/issue4092-sinf.smt2 b/test/regress/regress1/ho/issue4092-sinf.smt2 new file mode 100644 index 000000000..96f52fd39 --- /dev/null +++ b/test/regress/regress1/ho/issue4092-sinf.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --uf-ho --sort-inference --no-check-models +; EXPECT: sat +(set-logic ALL) +(set-option :sort-inference true) +(set-option :uf-ho true) +(set-info :status sat) +(declare-fun a ( Int ) Int) +(declare-fun b ( Int ) Int) +(assert (and (distinct 0 (b 5)) (distinct a b ))) +(check-sat) diff --git a/test/regress/regress1/ho/issue4134-sinf.smt2 b/test/regress/regress1/ho/issue4134-sinf.smt2 new file mode 100644 index 000000000..e87845fab --- /dev/null +++ b/test/regress/regress1/ho/issue4134-sinf.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --uf-ho --sort-inference --no-check-models +; EXPECT: sat +(set-logic ALL) +(set-option :uf-ho true) +(set-option :sort-inference true) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b (Int) Int) +(declare-fun c (Int) Int) +(declare-fun d (Int) Int) +(assert (distinct d (ite (= a 0) b c))) +(assert (= (d 0) 0)) +(check-sat) |