From: Andrew Reynolds Date: Fri, 27 Oct 2017 14:03:07 +0000 (-0500) Subject: Implement Hilbert choice operator (#1291) X-Git-Tag: cvc5-1.0.0~5531 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=03cc40cc070df0bc11c1556cef3016f784a95d23;p=cvc5.git Implement Hilbert choice operator (#1291) * Initial support for Hilbert choice operator. * Clang format. * Fix * Minor --- diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 0cd166c87..01cf59c15 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -116,7 +116,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector& output, } //if a lambda, do lambda-lifting if( node.getKind() == kind::LAMBDA && !inQuant ){ - // Make the skolem to represent the ITE + // Make the skolem to represent the lambda skolem = nodeManager->mkSkolem("lambdaF", nodeType, "a function introduced due to term-level lambda removal"); // The new assertion @@ -134,6 +134,25 @@ Node RemoveTermFormulas::run(TNode node, std::vector& output, // axiom defining skolem newAssertion = nodeManager->mkNode( kind::FORALL, children ); } + + // If a Hilbert choice function, witness the choice. + // For details on this operator, see + // http://planetmath.org/hilbertsvarepsilonoperator. + if (node.getKind() == kind::CHOICE && !inQuant) + { + // Make the skolem to witness the choice + skolem = nodeManager->mkSkolem( + "choiceK", + nodeType, + "a skolem introduced due to term-level Hilbert choice removal"); + + Assert(node[0].getNumChildren() == 1); + + // The new assertion is the assumption that the body + // of the choice operator holds for the Skolem + newAssertion = node[1].substitute(node[0], skolem); + } + //if a non-variable Boolean term, replace it if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){ diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 48b1c36c5..f84f9dc37 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -50,30 +50,38 @@ public: /** * By introducing skolem variables, this function removes all occurrences of: - * (1) term ITEs - * (2) terms of type Boolean that are not Boolean term variables, and - * (3) lambdas + * (1) term ITEs + * (2) terms of type Boolean that are not Boolean term variables, + * (3) lambdas, and + * (4) Hilbert choice expressions. * from assertions. * All additional assertions are pushed into assertions. iteSkolemMap * contains a map from introduced skolem variables to the index in * assertions containing the new definition created in conjunction * with that skolem variable. * - * As an example of (1): + * As an example of (1): * f( (ite C 0 1)) = 2 - * becomes + * becomes * f( k ) = 2 ^ ite( C, k=0, k=1 ) * * As an example of (2): * g( (and C1 C2) ) = 3 - * becomes + * becomes * g( k ) = 3 ^ ( k <=> (and C1 C2) ) * - * As an example of (3): + * As an example of (3): * (lambda x. t[x]) = f - * becomes + * becomes * (forall x. k(x) = t[x]) ^ k = f - * where k is a fresh skolem. This is sometimes called "lambda lifting" + * where k is a fresh skolem function. + * This is sometimes called "lambda lifting" + * + * As an example of (4): + * (choice x. P( x ) ) = t + * becomes + * P( k ) ^ k = t + * where k is a fresh skolem constant. * * With reportDeps true, report reasoning dependences to the proof * manager (for unsat cores). diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 6b7b952e2..c1edd81cb 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -302,6 +302,8 @@ operator SEXPR 0: "a symbolic expression (any arity)" operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body" +operator CHOICE 2 "a Hilbert choice (epsilon) expression; first parameter is a BOUND_VAR_LIST, second is the Hilbert choice body" + parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjunction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator" constant CHAIN_OP \ ::CVC4::Chain \ @@ -333,6 +335,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule +typerule CHOICE ::CVC4::theory::builtin::ChoiceTypeRule typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 777f6e57f..a6bd41a0b 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -192,6 +192,41 @@ public: } };/* class LambdaTypeRule */ +class ChoiceTypeRule +{ + public: + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + if (n[0].getType(check) != nodeManager->boundVarListType()) + { + std::stringstream ss; + ss << "expected a bound var list for CHOICE expression, got `" + << n[0].getType().toString() << "'"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + if (n[0].getNumChildren() != 1) + { + std::stringstream ss; + ss << "expected a bound var list with one argument for CHOICE expression"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + if (check) + { + TypeNode rangeType = n[1].getType(check); + if (!rangeType.isBoolean()) + { + std::stringstream ss; + ss << "expected a body of a CHOICE expression to have Boolean type"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + // The type of a choice function is the type of its bound variable. + return n[0][0].getType(); + } +}; /* class ChoiceTypeRule */ + class ChainTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {