diff options
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 6 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 118 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.h | 6 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 44 | ||||
-rw-r--r-- | src/theory/builtin/type_enumerator.h | 6 |
6 files changed, 100 insertions, 84 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 3313a684f..15891dfad 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -289,9 +289,6 @@ constant BUILTIN \ "expr/kind.h" \ "the kind of expressions representing built-in operators" -variable FUNCTION "a defined function" -parameterized APPLY FUNCTION 0: "application of a defined function" - operator EQUAL 2 "equality (two parameters only, sorts must match)" operator DISTINCT 2: "disequality (N-ary, sorts must match)" variable VARIABLE "a variable (not permitted in bindings)" @@ -332,7 +329,6 @@ well-founded SEXPR_TYPE \ "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" -typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 3b2a57397..8a7d1bf7b 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H -#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H +#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H +#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H #include "theory/theory.h" @@ -38,4 +38,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */ +#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */ diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 5b893ffc6..63d08b0ef 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -77,7 +77,6 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) { Trace("builtin-rewrite") << "Rewriting lambda " << node << "..." << std::endl; Node anode = getArrayRepresentationForLambda( node ); if( !anode.isNull() ){ - anode = Rewriter::rewrite( anode ); Assert( anode.getType().isArray() ); //must get the standard bound variable list Node varList = NodeManager::currentNM()->getBoundVarListForFunctionType( node.getType() ); @@ -198,6 +197,7 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec(TNode n, TypeNode retType) { Assert( n.getKind()==kind::LAMBDA ); + NodeManager* nm = NodeManager::currentNM(); Trace("builtin-rewrite-debug") << "Get array representation for : " << n << std::endl; Node first_arg = n[0][0]; @@ -207,33 +207,71 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec(TNode n, for( unsigned i=1; i<n[0].getNumChildren(); i++ ){ args.push_back( n[0][i] ); } - rec_bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, args ); + rec_bvl = nm->mkNode(kind::BOUND_VAR_LIST, args); } Trace("builtin-rewrite-debug2") << " process body..." << std::endl; std::vector< Node > conds; std::vector< Node > vals; Node curr = n[1]; - while( curr.getKind()==kind::ITE || curr.getKind()==kind::EQUAL || curr.getKind()==kind::NOT ){ - Trace("builtin-rewrite-debug2") << " process condition : " << curr[0] << std::endl; + Kind ck = curr.getKind(); + while (ck == kind::ITE || ck == kind::EQUAL || ck == kind::NOT + || ck == kind::BOUND_VARIABLE) + { Node index_eq; Node curr_val; Node next; - if( curr.getKind()==kind::ITE ){ + // Each iteration of this loop infers an entry in the function, e.g. it + // has a value under some condition. + + // [1] We infer that the entry has value "curr_val" under condition + // "index_eq". We set "next" to the node that is the remainder of the + // function to process. + if (ck == kind::ITE) + { + Trace("builtin-rewrite-debug2") + << " process condition : " << curr[0] << std::endl; index_eq = curr[0]; curr_val = curr[1]; next = curr[2]; - }else{ - bool pol = curr.getKind()!=kind::NOT; - //Boolean case, e.g. lambda x. (= x v) is lambda x. (ite (= x v) true false) - index_eq = curr.getKind()==kind::NOT ? curr[0] : curr; - curr_val = NodeManager::currentNM()->mkConst( pol ); - next = NodeManager::currentNM()->mkConst( !pol ); } - if( index_eq.getKind()!=kind::EQUAL ){ - // non-equality condition - Trace("builtin-rewrite-debug2") << " ...non-equality condition." << std::endl; - return Node::null(); + else + { + Trace("builtin-rewrite-debug2") + << " process base : " << curr << std::endl; + // Boolean return case, e.g. lambda x. (= x v) becomes + // lambda x. (ite (= x v) true false) + index_eq = curr; + curr_val = nm->mkConst(true); + next = nm->mkConst(false); + } + + // [2] We ensure that "index_eq" is an equality, if possible. + if (index_eq.getKind() != kind::EQUAL) + { + bool pol = index_eq.getKind() != kind::NOT; + Node indexEqAtom = pol ? index_eq : index_eq[0]; + if (indexEqAtom.getKind() == kind::BOUND_VARIABLE) + { + if (!indexEqAtom.getType().isBoolean()) + { + // Catches default case of non-Boolean variable, e.g. + // lambda x : Int. x. In this case, it is not canonical and we fail. + Trace("builtin-rewrite-debug2") + << " ...non-Boolean variable." << std::endl; + return Node::null(); + } + // Boolean argument case, e.g. lambda x. ite( x, t, s ) is processed as + // lambda x. (ite (= x true) t s) + index_eq = indexEqAtom.eqNode(nm->mkConst(pol)); + } + else + { + // non-equality condition + Trace("builtin-rewrite-debug2") + << " ...non-equality condition." << std::endl; + return Node::null(); + } } else if (Rewriter::rewrite(index_eq) != index_eq) { @@ -242,6 +280,9 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec(TNode n, return Node::null(); } + // [3] We ensure that "index_eq" is an equality that is equivalent to + // "first_arg" = "curr_index", where curr_index is a constant, and + // "first_arg" is the current argument we are processing, if possible. Node curr_index; for( unsigned r=0; r<2; r++ ){ Node arg = index_eq[r]; @@ -259,25 +300,36 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec(TNode n, } } } - if( !curr_index.isNull() ){ - if( !rec_bvl.isNull() ){ - curr_val = NodeManager::currentNM()->mkNode( kind::LAMBDA, rec_bvl, curr_val ); - curr_val = getArrayRepresentationForLambdaRec(curr_val, retType); - if( curr_val.isNull() ){ - Trace("builtin-rewrite-debug2") << " ...non-constant value." << std::endl; - return Node::null(); - } - } - Trace("builtin-rewrite-debug2") << " ...condition is index " << curr_val << std::endl; - }else{ - Trace("builtin-rewrite-debug2") << " ...non-constant value." << std::endl; + if (curr_index.isNull()) + { + Trace("builtin-rewrite-debug2") + << " ...could not infer index value." << std::endl; return Node::null(); } + + // [4] Recurse to ensure that "curr_val" has been normalized w.r.t. the + // remaining arguments (rec_bvl). + if (!rec_bvl.isNull()) + { + curr_val = nm->mkNode(kind::LAMBDA, rec_bvl, curr_val); + curr_val = getArrayRepresentationForLambdaRec(curr_val, retType); + if (curr_val.isNull()) + { + Trace("builtin-rewrite-debug2") + << " ...failed to recursively find value." << std::endl; + return Node::null(); + } + } + Trace("builtin-rewrite-debug2") + << " ...condition is index " << curr_val << std::endl; + + // [5] Add the entry conds.push_back( curr_index ); vals.push_back( curr_val ); - TypeNode vtype = curr_val.getType(); - //recurse + + // we will now process the remainder curr = next; + ck = curr.getKind(); } if( !rec_bvl.isNull() ){ curr = NodeManager::currentNM()->mkNode( kind::LAMBDA, rec_bvl, curr ); @@ -314,7 +366,13 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda(TNode n) Assert( n.getKind()==kind::LAMBDA ); // must carry the overall return type to deal with cases like (lambda ((x Int)(y Int)) (ite (= x _) 0.5 0.0)), // where the inner construction for the else case about should be (arraystoreall (Array Int Real) 0.0) - return getArrayRepresentationForLambdaRec(n, n[1].getType()); + Node anode = getArrayRepresentationForLambdaRec(n, n[1].getType()); + if (anode.isNull()) + { + return anode; + } + // must rewrite it to make canonical + return Rewriter::rewrite(anode); } }/* CVC4::theory::builtin namespace */ diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index 2fe91e8cb..5f703fa00 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H -#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H +#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H +#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H #include "theory/rewriter.h" #include "theory/theory.h" @@ -130,4 +130,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */ +#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index adeec48a9..db427d21e 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H -#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H +#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H +#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H #include "expr/node.h" #include "expr/type_node.h" @@ -31,44 +31,6 @@ namespace CVC4 { namespace theory { namespace builtin { -class ApplyTypeRule { - public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - TNode f = n.getOperator(); - TypeNode fType = f.getType(check); - if( !fType.isFunction() && n.getNumChildren() > 0 ) { - throw TypeCheckingExceptionPrivate(n, "operator does not have function type"); - } - if( check ) { - if(fType.isFunction()) { - if(n.getNumChildren() != fType.getNumChildren() - 1) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); - } - TNode::iterator argument_it = n.begin(); - TNode::iterator argument_it_end = n.end(); - TypeNode::iterator argument_type_it = fType.begin(); - for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) { - if(!(*argument_it).getType().isComparableTo(*argument_type_it)) { - std::stringstream ss; - ss << "argument types do not match the function type:\n" - << "argument: " << *argument_it << "\n" - << "has type: " << (*argument_it).getType() << "\n" - << "not equal: " << *argument_type_it; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - } else { - if( n.getNumChildren() > 0 ) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); - } - } - } - return fType.isFunction() ? fType.getRangeType() : fType; - } -};/* class ApplyTypeRule */ - - class EqualityTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, @@ -375,4 +337,4 @@ class SExprProperties { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */ +#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */ diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 63c34161c..8ce17306f 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H -#define __CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H +#ifndef CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H +#define CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H #include "expr/kind.h" #include "expr/type_node.h" @@ -108,4 +108,4 @@ class FunctionEnumerator : public TypeEnumeratorBase<FunctionEnumerator> }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */ +#endif /* CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */ |