summaryrefslogtreecommitdiff
path: root/src/theory/builtin
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/builtin')
-rw-r--r--src/theory/builtin/kinds4
-rw-r--r--src/theory/builtin/theory_builtin.h6
-rw-r--r--src/theory/builtin/theory_builtin_rewriter.cpp118
-rw-r--r--src/theory/builtin/theory_builtin_rewriter.h6
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h44
-rw-r--r--src/theory/builtin/type_enumerator.h6
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback